Rqe/inferpsign_thms.ml

   1 let EVEN_DIV_LEM = prove_by_refinement(
   2   `!set p q c d a n.
   3      (!x. a pow n * p x = c x * q x + d x) ==>
   4      a <> &0 ==>
   5      EVEN n ==>
   6        ((interpsign set q Zero) ==>
   7         (interpsign set d Neg)  ==>
   8          (interpsign set p Neg)) /\
   9        ((interpsign set q Zero) ==>
  10         (interpsign set d Pos)  ==>
  11          (interpsign set p Pos)) /\
  12        ((interpsign set q Zero) ==>
  13         (interpsign set d Zero)  ==>
  14          (interpsign set p Zero))`,
  15 (* {{{ Proof *)
  16
  17 [
  18   REWRITE_TAC[interpsign];
  19   REPEAT STRIP_TAC;
  20   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  21   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  22   POP_ASSUM MP_TAC;
  23   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  24   STRIP_TAC;
  25   CLAIM `&0 < a pow n`;
  26   ASM_MESON_TAC[EVEN_ODD_POW;real_gt];
  27   STRIP_TAC;
  28   CLAIM `a pow n * p x < &0`;
  29   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  30   REWRITE_TAC[REAL_MUL_LT];
  31   REPEAT STRIP_TAC;
  32   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  33   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  34   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  35   POP_ASSUM MP_TAC;
  36   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  37   STRIP_TAC;
  38   CLAIM `&0 < a pow n`;
  39   ASM_MESON_TAC[EVEN_ODD_POW;real_gt];
  40   STRIP_TAC;
  41   CLAIM `a pow n * p x > &0`;
  42   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  43   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  44   REPEAT STRIP_TAC;
  45   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  46   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  47   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  48   POP_ASSUM MP_TAC;
  49   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  50   STRIP_TAC;
  51   CLAIM `&0 < a pow n`;
  52   ASM_MESON_TAC[EVEN_ODD_POW;real_gt];
  53   STRIP_TAC;
  54   CLAIM `a pow n * p x = &0`;
  55   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  56   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
  57   REPEAT STRIP_TAC;
  58   ASM_MESON_TAC[REAL_ENTIRE;REAL_POS_NZ];
  59 ]);;
  60
  61 (* }}} *)
  62
  63 let GT_DIV_LEM = prove_by_refinement(
  64   `!set p q c d a n.
  65      (!x. a pow n * p x = c x * q x + d x) ==>
  66      a > &0 ==>
  67        ((interpsign set q Zero) ==>
  68         (interpsign set d Neg)  ==>
  69          (interpsign set p Neg)) /\
  70        ((interpsign set q Zero) ==>
  71         (interpsign set d Pos)  ==>
  72          (interpsign set p Pos)) /\
  73        ((interpsign set q Zero) ==>
  74         (interpsign set d Zero)  ==>
  75          (interpsign set p Zero))`,
  76 (* {{{ Proof *)
  77 [
  78   REWRITE_TAC[interpsign];
  79   REPEAT_N 9 STRIP_TAC;
  80   CLAIM `a pow n > &0`;
  81   ASM_MESON_TAC[REAL_POW_LT;real_gt;];
  82   STRIP_TAC;
  83   REPEAT STRIP_TAC;
  84   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  85   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  86   POP_ASSUM MP_TAC;
  87   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  88   STRIP_TAC;
  89   CLAIM `a pow n * p x < &0`;
  90   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  91   REWRITE_TAC[REAL_MUL_LT];
  92   REPEAT STRIP_TAC;
  93   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  94   (* save *)
  95   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
  96   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
  97   POP_ASSUM MP_TAC;
  98   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
  99   STRIP_TAC;
 100   CLAIM `a pow n * p x > &0`;
 101   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 102   REWRITE_TAC[REAL_MUL_GT;real_gt];
 103   REPEAT STRIP_TAC;
 104   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 105   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
 106   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
 107   POP_ASSUM MP_TAC;
 108   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
 109   STRIP_TAC;
 110   CLAIM `a pow n * p x = &0`;
 111   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 112   ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
 113 ]);;
 114 (* }}} *)
 115
 116 let NEG_ODD_LEM = prove_by_refinement(
 117   `!set p q c d a n.
 118      (!x. a pow n * p x = c x * q x + d x) ==>
 119      a < &0 ==>
 120      ODD n ==>
 121        ((interpsign set q Zero) ==>
 122         (interpsign set (\x. -- d x) Neg)  ==>
 123          (interpsign set p Neg)) /\
 124        ((interpsign set q Zero) ==>
 125         (interpsign set (\x. -- d x) Pos)  ==>
 126          (interpsign set p Pos)) /\
 127        ((interpsign set q Zero) ==>
 128         (interpsign set (\x. -- d x) Zero)  ==>
 129          (interpsign set p Zero))`,
 130 (* {{{ Proof *)
 131 [
 132   REWRITE_TAC[interpsign;POLY_NEG];
 133   REPEAT_N 10 STRIP_TAC;
 134   CLAIM `a pow n < &0`;
 135   ASM_MESON_TAC[PARITY_POW_LT;real_gt;];
 136   STRIP_TAC;
 137   REAL_SIMP_TAC;
 138   REPEAT STRIP_TAC;
 139   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
 140   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
 141   POP_ASSUM MP_TAC;
 142   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
 143   STRIP_TAC;
 144   CLAIM `a pow n * p x > &0`;
 145   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 146   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
 147   REPEAT STRIP_TAC;
 148   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 149   (* save *)
 150   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
 151   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
 152   POP_ASSUM MP_TAC;
 153   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
 154   STRIP_TAC;
 155   CLAIM `a pow n * p x < &0`;
 156   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 157   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
 158   REPEAT STRIP_TAC;
 159   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 160   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
 161   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
 162   POP_ASSUM MP_TAC;
 163   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
 164   STRIP_TAC;
 165   CLAIM `a pow n * p x = &0`;
 166   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 167   ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
 168 ]);;
 169 (* }}} *)
 170
 171 let NEQ_ODD_LEM = prove_by_refinement(
 172   `!set p q c d a n.
 173      (!x. a pow n * p x = c x * q x + d x) ==>
 174      a <> &0 ==>
 175      ODD n ==>
 176        ((interpsign set q Zero) ==>
 177         (interpsign set (\x. a * d x) Neg)  ==>
 178          (interpsign set p Neg)) /\
 179        ((interpsign set q Zero) ==>
 180         (interpsign set (\x. a * d x) Pos)  ==>
 181          (interpsign set p Pos)) /\
 182        ((interpsign set q Zero) ==>
 183         (interpsign set (\x. a * d x) Zero)  ==>
 184          (interpsign set p Zero))`,
 185 (* {{{ Proof *)
 186 [
 187   REWRITE_TAC[interpsign;POLY_CMUL];
 188   REPEAT_N 10 STRIP_TAC;
 189   CLAIM `a < &0 \/ a > &0 \/ (a = &0)`;
 190   REAL_ARITH_TAC;
 191   REWRITE_ASSUMS[NEQ];
 192   ASM_REWRITE_TAC[];
 193   LABEL_ALL_TAC;
 194   STRIP_TAC;
 195   (* save *)
 196   CLAIM `a pow n < &0`;
 197   ASM_MESON_TAC[PARITY_POW_LT];
 198   STRIP_TAC;
 199   REPEAT STRIP_TAC;
 200   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
 201   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
 202   POP_ASSUM MP_TAC;
 203   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
 204   STRIP_TAC;
 205   CLAIM `d x > &0`;
 206   POP_ASSUM MP_TAC;
 207   ASM_REWRITE_TAC[real_gt;REAL_MUL_LT];
 208   REPEAT STRIP_TAC;
 209   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 210   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
 211   REPEAT STRIP_TAC;
 212   POP_ASSUM MP_TAC;
 213   POP_ASSUM MP_TAC;
 214   REWRITE_TAC[REAL_MUL_LT];
 215   REPEAT STRIP_TAC;
 216   CLAIM `&0 < a pow n * p x`;
 217   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 218   REWRITE_TAC[REAL_MUL_GT];
 219   REPEAT STRIP_TAC;
 220   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 221   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 222   (* save *)
 223   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
 224   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
 225   POP_ASSUM MP_TAC;
 226   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
 227   STRIP_TAC;
 228   CLAIM `d x < &0`;
 229   POP_ASSUM MP_TAC;
 230   REWRITE_TAC[REAL_MUL_GT;real_gt];
 231   REPEAT STRIP_TAC;
 232   CLAIM `a pow n * p x < &0`;
 233   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 234   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
 235   REPEAT STRIP_TAC;
 236   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 237   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 238   STRIP_TAC;
 239   CLAIM `a pow n * p x < &0`;
 240   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 241   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
 242   REPEAT STRIP_TAC;
 243   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 244   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
 245   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
 246   POP_ASSUM MP_TAC;
 247   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
 248   STRIP_TAC;
 249   CLAIM `d x = &0`;
 250   ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
 251   STRIP_TAC;
 252   CLAIM `a pow n * p x = &0`;
 253   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 254   ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
 255   (* save *)
 256   CLAIM `a pow n > &0`;
 257   ASM_MESON_TAC[EVEN_ODD_POW;NEQ;real_gt];
 258   STRIP_TAC;
 259   REPEAT STRIP_TAC;
 260   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
 261   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
 262   POP_ASSUM MP_TAC;
 263   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
 264   STRIP_TAC;
 265   CLAIM `d x < &0`;
 266   POP_ASSUM MP_TAC;
 267   ASM_REWRITE_TAC[real_gt;REAL_MUL_LT];
 268   REPEAT STRIP_TAC;
 269   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 270   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
 271   REPEAT STRIP_TAC;
 272   POP_ASSUM MP_TAC;
 273   POP_ASSUM MP_TAC;
 274   REWRITE_TAC[REAL_MUL_LT];
 275   REPEAT STRIP_TAC;
 276   CLAIM `a pow n * p x < &0`;
 277   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 278   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
 279   REPEAT STRIP_TAC;
 280   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 281   CLAIM `a pow n * p x < &0`;
 282   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 283   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
 284   REPEAT STRIP_TAC;
 285   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 286   (* save *)
 287   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
 288   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
 289   POP_ASSUM MP_TAC;
 290   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
 291   STRIP_TAC;
 292   CLAIM `d x > &0`;
 293   POP_ASSUM MP_TAC;
 294   REWRITE_TAC[REAL_MUL_GT;real_gt];
 295   REPEAT STRIP_TAC;
 296   CLAIM `a pow n * p x < &0`;
 297   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 298   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
 299   REPEAT STRIP_TAC;
 300   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 301   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 302   STRIP_TAC;
 303   CLAIM `a pow n * p x > &0`;
 304   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 305   REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt];
 306   REPEAT STRIP_TAC;
 307   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 308   RULE_ASSUM_TAC (fun y -> try ISPEC `x:real` y with _ -> y);
 309   POP_ASSUM (fun x -> REWRITE_ASSUMS[x]);
 310   POP_ASSUM MP_TAC;
 311   POP_ASSUM (fun x -> REWRITE_ASSUMS[x;REAL_MUL_RZERO;REAL_ADD_LID;]);
 312   STRIP_TAC;
 313   CLAIM `d x = &0`;
 314   ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
 315   STRIP_TAC;
 316   CLAIM `a pow n * p x = &0`;
 317   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 318   ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
 319 ]);;
 320 (* }}} *)
 321
 322 let NEQ_MULT_LT_LEM = prove_by_refinement(
 323   `!a q d d' set.
 324      a < &0 ==>
 325        ((interpsign set d Neg)  ==>
 326         (interpsign set (\x. a * d x) Pos)) /\
 327        ((interpsign set d Pos)  ==>
 328          (interpsign set (\x. a * d x) Neg)) /\
 329        ((interpsign set d Zero)  ==>
 330          (interpsign set (\x. a * d x) Zero))`,
 331 (* {{{ Proof *)
 332 [
 333   REWRITE_TAC[interpsign;POLY_NEG];
 334   REPEAT STRIP_TAC;
 335   ASM_MESON_TAC[REAL_MUL_GT;real_gt];
 336   ASM_MESON_TAC[REAL_MUL_LT;real_gt];
 337   ASM_MESON_TAC[REAL_ENTIRE;REAL_NOT_EQ;real_gt];
 338 ]);;
 339 (* }}} *)
 340
 341 let NEQ_MULT_GT_LEM = prove_by_refinement(
 342   `!a q d d' set.
 343      a > &0 ==>
 344        ((interpsign set d Neg)  ==>
 345          (interpsign set (\x. a * d x) Neg)) /\
 346        ((interpsign set d Pos)  ==>
 347          (interpsign set (\x. a * d x) Pos)) /\
 348        ((interpsign set d Zero)  ==>
 349          (interpsign set (\x. a * d x) Zero))`,
 350 (* {{{ Proof *)
 351 [
 352   REWRITE_TAC[interpsign;POLY_NEG] THEN
 353   MESON_TAC[REAL_MUL_LT;REAL_ENTIRE;REAL_NOT_EQ;REAL_MUL_GT;real_gt];
 354 ]);;
 355 (* }}} *)
 356
 357 let unknown_thm = prove(
 358   `!set p. (interpsign set p Unknown)`,
 359     MESON_TAC[interpsign]);;
 360
 361 let ips_gt_nz_thm = prove_by_refinement(
 362   `!x. x > &0 ==> x <> &0`,
 363 (* {{{ Proof *)
 364 [
 365   REWRITE_TAC[NEQ];
 366   REAL_ARITH_TAC;
 367 ]);;
 368 (* }}} *)
 369
 370 let ips_lt_nz_thm = prove_by_refinement(
 371   `!x. x < &0 ==> x <> &0`,
 372 (* {{{ Proof *)
 373 [
 374   REWRITE_TAC[NEQ];
 375   REAL_ARITH_TAC;
 376 ]);;
 377 (* }}} *)