Rqe/main_thms.ml

   1 let empty_mat = prove_by_refinement(
   2    `interpmat [] [] [[]]`,
   3 (* {{{ Proof *)
   4
   5 [
   6   REWRITE_TAC[interpmat;ROL_EMPTY;interpsigns;ALL2;partition_line];
   7 ]);;
   8
   9 (* }}} *)
  10
  11 let empty_sgns = [ARITH_RULE `&1 > &0`];;
  12
  13 let monic_isign_lem = prove(
  14   `(!s c mp p. (!x. c * p x = mp x) ==> c > &0 ==> interpsign s mp Pos ==> interpsign s p Pos) /\
  15    (!s c mp p. (!x. c * p x = mp x) ==> c < &0 ==> interpsign s mp Pos ==> interpsign s p Neg) /\
  16    (!s c mp p. (!x. c * p x = mp x) ==> c > &0 ==> interpsign s mp Neg ==> interpsign s p Neg) /\
  17    (!s c mp p. (!x. c * p x = mp x) ==> c < &0 ==> interpsign s mp Neg ==> interpsign s p Pos) /\
  18    (!s c mp p. (!x. c * p x = mp x) ==> c > &0 ==> interpsign s mp Zero ==> interpsign s p Zero) /\
  19    (!s c mp p. (!x. c * p x = mp x) ==> c < &0 ==> interpsign s mp Zero ==> interpsign s p Zero)`,
  20 (* {{{ Proof *)
  21
  22   REWRITE_TAC[interpsign] THEN REPEAT STRIP_TAC THEN
  23   POP_ASSUM (fun x -> POP_ASSUM (fun y -> MP_TAC (MATCH_MP y x))) THEN
  24   POP_ASSUM MP_TAC THEN
  25   POP_ASSUM (ASSUME_TAC o GSYM o (ISPEC `x:real`)) THEN
  26   ASM_REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt;REAL_ENTIRE] THEN
  27   REAL_ARITH_TAC);;
  28
  29 (* }}} *)
  30
  31 let gtpos::ltpos::gtneg::ltneg::gtzero::ltzero::[] = CONJUNCTS monic_isign_lem;;
  32
  33 let main_lem000 = prove_by_refinement(
  34   `!l n. (LENGTH l = SUC n) ==> 0 < LENGTH l`,
  35 (* {{{ Proof *)
  36
  37 [
  38   LIST_INDUCT_TAC;
  39   REWRITE_TAC[LENGTH];
  40   ARITH_TAC;
  41   ARITH_TAC;
  42 ]);;
  43
  44 (* }}} *)
  45
  46 let main_lem001 = prove_by_refinement(
  47   `x <> &0 ==> (LAST l = x) ==> LAST l <> &0`,
  48 [MESON_TAC[]]);;
  49
  50 let main_lem002 = prove_by_refinement(
  51   `(x <> y ==> x <> y) /\
  52    (x < y ==> x <> y) /\
  53    (x > y ==> x <> y) /\
  54    (~(x >= y) ==> x <> y) /\
  55    (~(x <= y) ==> x <> y) /\
  56    (~(x = y) ==> x <> y)`,
  57 (* {{{ Proof *)
  58
  59 [
  60   REWRITE_TAC[NEQ] THEN REAL_ARITH_TAC
  61 ]);;
  62
  63 (* }}} *)
  64
  65 let factor_pos_pos = prove_by_refinement(
  66   `interpsign s (\x. &0 + x * &1) Pos ==> interpsign s p Pos ==>
  67    (!x. x pow k * p x = q x) ==> interpsign s q Pos`,
  68 (* {{{ Proof *)
  69 [
  70   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
  71   REPEAT STRIP_TAC;
  72   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
  73   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
  74   ASM_REWRITE_TAC[];
  75   REWRITE_TAC[REAL_MUL_GT;real_gt];
  76   DISJ2_TAC;
  77   ASM_MESON_TAC[REAL_POW_LT;real_gt];
  78 ]);;
  79 (* }}} *)
  80
  81 let factor_pos_neg = prove_by_refinement(
  82   `interpsign s (\x. &0 + x * &1) Pos ==> interpsign s p Neg ==>
  83    (!x. x pow k * p x = q x) ==> interpsign s q Neg`,
  84 (* {{{ Proof *)
  85 [
  86   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
  87   REPEAT STRIP_TAC;
  88   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
  89   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
  90   ASM_REWRITE_TAC[];
  91   REWRITE_TAC[REAL_MUL_LT;real_gt];
  92   DISJ2_TAC;
  93   ASM_MESON_TAC[REAL_POW_LT;real_gt];
  94 ]);;
  95 (* }}} *)
  96
  97 let factor_pos_zero = prove_by_refinement(
  98   `interpsign s (\x. &0 + x * &1) Pos ==> interpsign s p Zero ==>
  99    (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
 100 (* {{{ Proof *)
 101 [
 102   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
 103   REPEAT STRIP_TAC;
 104   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
 105   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
 106   ASM_REWRITE_TAC[];
 107   REWRITE_TAC[REAL_MUL_LT;REAL_ENTIRE;real_gt];
 108 ]);;
 109 (* }}} *)
 110
 111 let factor_zero_pos = prove_by_refinement(
 112   `interpsign s (\x. &0 + x * &1) Zero ==> interpsign s p Pos ==> ~(k = 0) ==>
 113    (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
 114 (* {{{ Proof *)
 115 [
 116   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
 117   REPEAT STRIP_TAC;
 118   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
 119   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
 120   ASM_REWRITE_TAC[];
 121   REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;REAL_ENTIRE];
 122   DISJ1_TAC;
 123   ASM_MESON_TAC[POW_0;num_CASES;];
 124 ]);;
 125 (* }}} *)
 126
 127 let factor_zero_neg = prove_by_refinement(
 128   `interpsign s (\x. &0 + x * &1) Zero ==> interpsign s p Neg ==> ~(k = 0) ==>
 129    (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
 130 (* {{{ Proof *)
 131 [
 132   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
 133   REPEAT STRIP_TAC;
 134   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
 135   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
 136   ASM_REWRITE_TAC[];
 137   REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;REAL_ENTIRE];
 138   DISJ1_TAC;
 139   ASM_MESON_TAC[POW_0;num_CASES;];
 140 ]);;
 141 (* }}} *)
 142
 143 let factor_zero_zero = prove_by_refinement(
 144   `interpsign s (\x. &0 + x * &1) Zero ==> interpsign s p Zero ==> ~(k = 0) ==>
 145    (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
 146 (* {{{ Proof *)
 147 [
 148   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
 149   REPEAT STRIP_TAC;
 150   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
 151   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
 152   ASM_REWRITE_TAC[];
 153   REAL_ARITH_TAC;
 154 ]);;
 155 (* }}} *)
 156
 157 let factor_neg_even_pos = prove_by_refinement(
 158   `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Pos ==> EVEN k ==> ~(k = 0) ==>
 159    (!x. x pow k * p x = q x) ==> interpsign s q Pos`,
 160 (* {{{ Proof *)
 161 [
 162   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
 163   REPEAT STRIP_TAC;
 164   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
 165   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
 166   ASM_REWRITE_TAC[];
 167   REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt];
 168   DISJ2_TAC;
 169   ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT];
 170 ]);;
 171 (* }}} *)
 172
 173 let factor_neg_even_neg = prove_by_refinement(
 174   `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Neg ==> EVEN k ==> ~(k = 0) ==>
 175    (!x. x pow k * p x = q x) ==> interpsign s q Neg`,
 176 (* {{{ Proof *)
 177 [
 178   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
 179   REPEAT STRIP_TAC;
 180   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
 181   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
 182   ASM_REWRITE_TAC[];
 183   REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt];
 184   DISJ2_TAC;
 185   ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT];
 186 ]);;
 187 (* }}} *)
 188
 189 let factor_neg_even_zero = prove_by_refinement(
 190   `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Zero ==> EVEN k ==> ~(k = 0) ==>
 191    (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
 192 (* {{{ Proof *)
 193 [
 194   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
 195   REPEAT STRIP_TAC;
 196   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
 197   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
 198   ASM_REWRITE_TAC[];
 199   REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE];
 200 ]);;
 201 (* }}} *)
 202
 203 let factor_neg_odd_pos = prove_by_refinement(
 204   `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Pos ==> ODD k ==> ~(k = 0) ==>
 205    (!x. x pow k * p x = q x) ==> interpsign s q Neg`,
 206 (* {{{ Proof *)
 207 [
 208   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
 209   REPEAT STRIP_TAC;
 210   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
 211   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
 212   ASM_REWRITE_TAC[];
 213   REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE];
 214   DISJ1_TAC;
 215   ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT];
 216 ]);;
 217 (* }}} *)
 218
 219 let factor_neg_odd_neg = prove_by_refinement(
 220   `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Neg ==> ODD k ==> ~(k = 0) ==>
 221    (!x. x pow k * p x = q x) ==> interpsign s q Pos`,
 222 (* {{{ Proof *)
 223 [
 224   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
 225   REPEAT STRIP_TAC;
 226   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
 227   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
 228   ASM_REWRITE_TAC[];
 229   REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE];
 230   DISJ1_TAC;
 231   ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT];
 232 ]);;
 233 (* }}} *)
 234
 235 let factor_neg_odd_zero = prove_by_refinement(
 236   `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Zero ==> ODD k ==> ~(k = 0) ==>
 237    (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
 238 (* {{{ Proof *)
 239 [
 240   REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
 241   REPEAT STRIP_TAC;
 242   POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
 243   POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
 244   ASM_REWRITE_TAC[];
 245   REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE];
 246 ]);;
 247 (* }}} *)