Rqe/inferisign_thms.ml

   1 let inferisign_lem00 = prove_by_refinement(
   2   `x1 < x3 ==> x3 < x2 ==> (!x. x1 < x /\ x < x2 ==> P x) ==>
   3     (!x. x1 < x /\ x < x3 ==> P x) /\
   4     (!x. (x = x3) ==> P x) /\
   5     (!x. x3 < x /\ x < x2 ==> P x)`,
   6 (* {{{ Proof *)
   7
   8 [
   9   REPEAT STRIP_TAC;
  10   FIRST_ASSUM MATCH_MP_TAC;
  11   ASM_REWRITE_TAC[];
  12   MATCH_MP_TAC REAL_LT_TRANS;
  13   EXISTS_TAC `x3`;
  14   ASM_REWRITE_TAC[];
  15   FIRST_ASSUM MATCH_MP_TAC;
  16   ASM_REWRITE_TAC[];
  17   FIRST_ASSUM MATCH_MP_TAC;
  18   ASM_REWRITE_TAC[];
  19   MATCH_MP_TAC REAL_LT_TRANS;
  20   EXISTS_TAC `x3`;
  21   ASM_REWRITE_TAC[];
  22 ]);;
  23
  24 (* }}} *)
  25
  26 let neg_neg_neq_thm = prove_by_refinement(
  27   `!x y p. x < y /\ poly p x < &0 /\ poly p y < &0 /\
  28             (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
  29             (!z. x < z /\ z < y ==> poly p z < &0)`,
  30 (* {{{ Proof *)
  31 [
  32   REPEAT STRIP_TAC;
  33   REWRITE_TAC[ARITH_RULE `x < y <=> ~(y <= x)`];
  34   STRIP_TAC;
  35   MP_TAC (ISPECL [`p:real list`;`x:real`;`z:real`] POLY_MVT);
  36   ASM_REWRITE_TAC[];
  37   STRIP_TAC;
  38   CLAIM `&0 < poly p z - poly p x`;
  39   LABEL_ALL_TAC;
  40   USE_THEN "Z-3" MP_TAC;
  41   USE_THEN "Z-8" MP_TAC;
  42   REAL_ARITH_TAC;
  43   STRIP_TAC;
  44   CLAIM `&0 < (z - x) * poly (poly_diff p) x'`;
  45   REPEAT_N 2 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
  46   ASM_REWRITE_TAC[REAL_MUL_GT];
  47   REPEAT STRIP_TAC;
  48   CLAIM `&0 < z - x`;
  49   LABEL_ALL_TAC;
  50   USE_THEN "Z-8" MP_TAC THEN REAL_ARITH_TAC;
  51   LABEL_ALL_TAC;
  52   USE_THEN "Z-1" MP_TAC THEN REAL_ARITH_TAC;
  53   (* save *)
  54   MP_TAC (ISPECL [`p:real list`;`z:real`;`y:real`] POLY_MVT);
  55   ASM_REWRITE_TAC[];
  56   STRIP_TAC;
  57   CLAIM `poly p y - poly p z < &0`;
  58   LABEL_ALL_TAC;
  59   USE_THEN "Z-13" MP_TAC;
  60   USE_THEN "Z-9" MP_TAC;
  61   REAL_ARITH_TAC;
  62   STRIP_TAC;
  63   CLAIM `&0 < y - z`;
  64   LABEL_ALL_TAC;
  65   USE_THEN "Z-11" MP_TAC THEN REAL_ARITH_TAC;
  66   STRIP_TAC;
  67   CLAIM `(y - z) * poly (poly_diff p) x'' < &0`;
  68   POP_ASSUM IGNORE;
  69   POP_ASSUM MP_TAC;
  70   POP_ASSUM MP_TAC;
  71   REAL_ARITH_TAC;
  72   ASM_REWRITE_TAC[REAL_MUL_LT];
  73   REPEAT STRIP_TAC;
  74   REPEAT_N 3 (POP_ASSUM MP_TAC);
  75   REAL_ARITH_TAC;
  76   CLAIM `x' < x''`;
  77   MATCH_MP_TAC REAL_LT_TRANS;
  78   EXISTS_TAC `z`;
  79   ASM_REWRITE_TAC[];
  80   STRIP_TAC;
  81   MP_TAC (ISPECL [`poly_diff p`;`x':real`;`x'':real`] (REWRITE_RULE[real_gt] POLY_IVT_NEG));
  82   ASM_REWRITE_TAC[];
  83   STRIP_TAC;
  84   CLAIM `x < x''' /\  x''' < y`;
  85   STRIP_TAC;
  86   MATCH_MP_TAC REAL_LT_TRANS;
  87   EXISTS_TAC `x'`;
  88   ASM_REWRITE_TAC[];
  89   MATCH_MP_TAC REAL_LT_TRANS;
  90   EXISTS_TAC `x''`;
  91   ASM_REWRITE_TAC[];
  92   ASM_MESON_TAC[];
  93 ]);;
  94 (* }}} *)
  95
  96 let neg_neg_neq_thm2 = prove_by_refinement(
  97   `!x y p. x < y ==> poly p x < &0 ==> poly p y < &0 ==>
  98             (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
  99             (!z. x < z /\ z < y ==> poly p z < &0)`,
 100 (* {{{ Proof *)
 101 [
 102   REPEAT_N 7 STRIP_TAC;
 103   MATCH_MP_TAC neg_neg_neq_thm;
 104   ASM_MESON_TAC[];
 105 ]);;
 106 (* }}} *)
 107
 108 let pos_pos_neq_thm = prove_by_refinement(
 109   `!x y p. x < y /\ &0 < poly p x /\ &0 < poly p y /\
 110             (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
 111             (!z. x < z /\ z < y ==> &0 < poly p z)`,
 112 (* {{{ Proof *)
 113 [
 114   REPEAT STRIP_TAC;
 115   REWRITE_TAC[ARITH_RULE `x < y <=> ~(y <= x)`];
 116   STRIP_TAC;
 117   MP_TAC (ISPECL [`p:real list`;`x:real`;`z:real`] POLY_MVT);
 118   ASM_REWRITE_TAC[];
 119   STRIP_TAC;
 120   CLAIM `poly p z - poly p x < &0`;
 121   LABEL_ALL_TAC;
 122   USE_THEN "Z-3" MP_TAC;
 123   USE_THEN "Z-8" MP_TAC;
 124   REAL_ARITH_TAC;
 125   STRIP_TAC;
 126   CLAIM `(z - x) * poly (poly_diff p) x' < &0`;
 127   REPEAT_N 2 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 128   ASM_REWRITE_TAC[REAL_MUL_LT];
 129   REPEAT STRIP_TAC;
 130   CLAIM `&0 < z - x`;
 131   LABEL_ALL_TAC;
 132   USE_THEN "Z-8" MP_TAC THEN REAL_ARITH_TAC;
 133   LABEL_ALL_TAC;
 134   USE_THEN "Z-1" MP_TAC THEN REAL_ARITH_TAC;
 135   (* save *)
 136   MP_TAC (ISPECL [`p:real list`;`z:real`;`y:real`] POLY_MVT);
 137   ASM_REWRITE_TAC[];
 138   STRIP_TAC;
 139   CLAIM `&0 < poly p y - poly p z`;
 140   LABEL_ALL_TAC;
 141   USE_THEN "Z-13" MP_TAC;
 142   USE_THEN "Z-9" MP_TAC;
 143   REAL_ARITH_TAC;
 144   STRIP_TAC;
 145   CLAIM `&0 < y - z`;
 146   LABEL_ALL_TAC;
 147   USE_THEN "Z-11" MP_TAC THEN REAL_ARITH_TAC;
 148   STRIP_TAC;
 149   CLAIM `&0 < (y - z) * poly (poly_diff p) x''`;
 150   POP_ASSUM IGNORE;
 151   POP_ASSUM MP_TAC;
 152   POP_ASSUM MP_TAC;
 153   REAL_ARITH_TAC;
 154   ASM_REWRITE_TAC[REAL_MUL_GT];
 155   REPEAT STRIP_TAC;
 156   REPEAT_N 3 (POP_ASSUM MP_TAC);
 157   REAL_ARITH_TAC;
 158   CLAIM `x' < x''`;
 159   MATCH_MP_TAC REAL_LT_TRANS;
 160   EXISTS_TAC `z`;
 161   ASM_REWRITE_TAC[];
 162   STRIP_TAC;
 163   MP_TAC (ISPECL [`poly_diff p`;`x':real`;`x'':real`] (REWRITE_RULE[real_gt] POLY_IVT_POS));
 164   ASM_REWRITE_TAC[];
 165   STRIP_TAC;
 166   CLAIM `x < x''' /\  x''' < y`;
 167   STRIP_TAC;
 168   MATCH_MP_TAC REAL_LT_TRANS;
 169   EXISTS_TAC `x'`;
 170   ASM_REWRITE_TAC[];
 171   MATCH_MP_TAC REAL_LT_TRANS;
 172   EXISTS_TAC `x''`;
 173   ASM_REWRITE_TAC[];
 174   ASM_MESON_TAC[];
 175 ]);;
 176 (* }}} *)
 177
 178 let pos_pos_neq_thm2 = prove_by_refinement(
 179   `!x y p. x < y ==> poly p x > &0 ==> poly p y > &0 ==>
 180             (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
 181             (!z. x < z /\ z < y ==> poly p z > &0)`,
 182 (* {{{ Proof *)
 183 [
 184   REWRITE_TAC[real_gt];
 185   REPEAT_N 7 STRIP_TAC;
 186   MATCH_MP_TAC pos_pos_neq_thm;
 187   ASM_MESON_TAC[];
 188 ]);;
 189 (* }}} *)
 190
 191 let pos_neg_neq_thm = prove_by_refinement(
 192   `!x y p. x < y /\ &0 < poly p x /\ poly p y < &0 /\
 193             (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
 194             ?X. x < X /\ X < y /\ (poly p X = &0) /\
 195               (!z. x < z /\ z < X ==> &0 < poly p z) /\
 196               (!z. X < z /\ z < y ==> poly p z < &0)`,
 197 (* {{{ Proof *)
 198
 199 [
 200   REPEAT STRIP_TAC;
 201   MP_TAC (ISPECL [`p:real list`;`x:real`;`y:real`] POLY_IVT_NEG);
 202   REWRITE_TAC[real_gt];
 203   ASM_REWRITE_TAC[];
 204   DISCH_THEN (X_CHOOSE_TAC `X:real`);
 205   POP_ASSUM MP_TAC THEN STRIP_TAC;
 206   EXISTS_TAC `X`;
 207   ASM_REWRITE_TAC[];
 208   STRIP_TAC;
 209   REPEAT STRIP_TAC;
 210   (* save *)
 211   ONCE_REWRITE_TAC[ARITH_RULE `x < y <=> ~(y < x \/ (x = y))`];
 212   STRIP_TAC;
 213   MP_TAC (ISPECL [`p:real list`;`x:real`;`z:real`] POLY_MVT);
 214   ASM_REWRITE_TAC[];
 215   DISCH_THEN (X_CHOOSE_TAC `N:real`);
 216   POP_ASSUM MP_TAC THEN STRIP_TAC;
 217   CLAIM `poly p z - poly p x < &0`;
 218   LABEL_ALL_TAC;
 219   USE_THEN "Z-3" MP_TAC;
 220   USE_THEN "Z-11" MP_TAC;
 221   REAL_ARITH_TAC;
 222   STRIP_TAC;
 223   CLAIM `(z - x) * poly (poly_diff p) N < &0`;
 224   REPEAT_N 2 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 225   ASM_REWRITE_TAC[REAL_MUL_LT];
 226   REPEAT STRIP_TAC;
 227   CLAIM `&0 < z - x`;
 228   LABEL_ALL_TAC;
 229   USE_THEN "Z-8" MP_TAC THEN REAL_ARITH_TAC;
 230   LABEL_ALL_TAC;
 231   USE_THEN "Z-1" MP_TAC THEN REAL_ARITH_TAC;
 232   (* save *)
 233   MP_TAC (ISPECL [`p:real list`;`z:real`;`X:real`] POLY_MVT);
 234   ASM_REWRITE_TAC[];
 235   DISCH_THEN (X_CHOOSE_TAC `M:real`);
 236   POP_ASSUM MP_TAC THEN STRIP_TAC;
 237   CLAIM `&0 < &0 - poly p z`;
 238   LABEL_ALL_TAC;
 239   USE_THEN "Z-9" MP_TAC;
 240   REAL_ARITH_TAC;
 241   STRIP_TAC;
 242   CLAIM `&0 < X - z`;
 243   LABEL_ALL_TAC;
 244   USE_THEN "Z-11" MP_TAC THEN REAL_ARITH_TAC;
 245   STRIP_TAC;
 246   CLAIM `&0 < (X - z) * poly (poly_diff p) M`;
 247   POP_ASSUM IGNORE;
 248   POP_ASSUM MP_TAC;
 249   POP_ASSUM MP_TAC;
 250   REAL_ARITH_TAC;
 251   REWRITE_TAC[REAL_MUL_GT];
 252   REPEAT STRIP_TAC;
 253   POP_ASSUM IGNORE;
 254   POP_ASSUM MP_TAC;
 255   POP_ASSUM MP_TAC;
 256   REAL_ARITH_TAC;
 257   CLAIM `N < M`;
 258   MATCH_MP_TAC REAL_LT_TRANS;
 259   EXISTS_TAC `z`;
 260   ASM_REWRITE_TAC[];
 261   STRIP_TAC;
 262   MP_TAC (ISPECL [`poly_diff p`;`N:real`;`M:real`] (REWRITE_RULE[real_gt] POLY_IVT_POS));
 263   ASM_REWRITE_TAC[];
 264   DISCH_THEN (X_CHOOSE_TAC `K:real`);
 265   POP_ASSUM MP_TAC THEN STRIP_TAC;
 266   (* save *)
 267   CLAIM `x < K /\  K < y`;
 268   STRIP_TAC;
 269   MATCH_MP_TAC REAL_LT_TRANS;
 270   EXISTS_TAC `N`;
 271   ASM_REWRITE_TAC[];
 272   MATCH_MP_TAC REAL_LT_TRANS;
 273   EXISTS_TAC `M`;
 274   ASM_REWRITE_TAC[];
 275   MATCH_MP_TAC REAL_LT_TRANS;
 276   EXISTS_TAC `X`;
 277   ASM_REWRITE_TAC[];
 278   ASM_MESON_TAC[];
 279   (* save *)
 280   POP_ASSUM (ASSUME_TAC o GSYM);
 281   MP_TAC (ISPECL [`p:real list`;`z:real`;`X:real`] POLY_MVT);
 282   ASM_REWRITE_TAC[];
 283   REAL_SIMP_TAC;
 284   ONCE_REWRITE_TAC[REAL_ARITH `(x:real = y) <=> (y = x)`];
 285   ASM_REWRITE_TAC[REAL_ENTIRE];
 286   DISCH_THEN (X_CHOOSE_TAC `M:real`);
 287   POP_ASSUM MP_TAC THEN STRIP_TAC;
 288   LABEL_ALL_TAC;
 289   POP_ASSUM MP_TAC;
 290   USE_THEN "Z-4" MP_TAC THEN REAL_ARITH_TAC;
 291   CLAIM `x < M /\  M < y`;
 292   STRIP_TAC;
 293   MATCH_MP_TAC REAL_LT_TRANS;
 294   EXISTS_TAC `z`;
 295   ASM_REWRITE_TAC[];
 296   MATCH_MP_TAC REAL_LT_TRANS;
 297   EXISTS_TAC `X`;
 298   ASM_REWRITE_TAC[];
 299   ASM_MESON_TAC[];
 300   (* save *)
 301   REPEAT STRIP_TAC;
 302   ONCE_REWRITE_TAC[ARITH_RULE `x < y <=> ~(y < x \/ (x = y))`];
 303   STRIP_TAC;
 304   MP_TAC (ISPECL [`p:real list`;`X:real`;`z:real`] POLY_MVT);
 305   ASM_REWRITE_TAC[];
 306   DISCH_THEN (X_CHOOSE_TAC `N:real`);
 307   POP_ASSUM MP_TAC THEN STRIP_TAC;
 308   POP_ASSUM MP_TAC;
 309   REAL_SIMP_TAC;
 310   STRIP_TAC;
 311   CLAIM `&0 < (z - X) * poly (poly_diff p) N`;
 312   LABEL_ALL_TAC;
 313   USE_THEN "Z-3" MP_TAC;
 314   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 315   ASM_REWRITE_TAC[REAL_MUL_GT];
 316   REPEAT STRIP_TAC;
 317   CLAIM `&0 < z - X`;
 318   LABEL_ALL_TAC;
 319   USE_THEN "Z-7" MP_TAC THEN REAL_ARITH_TAC;
 320   LABEL_ALL_TAC;
 321   USE_THEN "Z-1" MP_TAC THEN REAL_ARITH_TAC;
 322   (* save *)
 323   MP_TAC (ISPECL [`p:real list`;`z:real`;`y:real`] POLY_MVT);
 324   LABEL_ALL_TAC;
 325   USE_THEN "Z-6" (REWRITE_TAC o list);
 326   DISCH_THEN (X_CHOOSE_TAC `M:real`);
 327   POP_ASSUM MP_TAC THEN STRIP_TAC;
 328   CLAIM `poly p y - poly p z < &0`;
 329   LABEL_ALL_TAC;
 330   USE_THEN "Z-12" MP_TAC;
 331   USE_THEN "Z-5" MP_TAC;
 332   REAL_ARITH_TAC;
 333   STRIP_TAC;
 334   CLAIM `&0 < y - z`;
 335   LABEL_ALL_TAC;
 336   USE_THEN "Z-6" MP_TAC THEN REAL_ARITH_TAC;
 337   STRIP_TAC;
 338   CLAIM `(y - z) * poly (poly_diff p) M < &0`;
 339   POP_ASSUM IGNORE;
 340   POP_ASSUM MP_TAC;
 341   POP_ASSUM MP_TAC;
 342   REAL_ARITH_TAC;
 343   REWRITE_TAC[REAL_MUL_LT];
 344   REPEAT STRIP_TAC;
 345   POP_ASSUM IGNORE;
 346   POP_ASSUM MP_TAC;
 347   POP_ASSUM MP_TAC;
 348   REAL_ARITH_TAC;
 349   CLAIM `N < M`;
 350   MATCH_MP_TAC REAL_LT_TRANS;
 351   EXISTS_TAC `z`;
 352   ASM_REWRITE_TAC[];
 353   STRIP_TAC;
 354   MP_TAC (ISPECL [`poly_diff p`;`N:real`;`M:real`] (REWRITE_RULE[real_gt] POLY_IVT_NEG));
 355   ASM_REWRITE_TAC[];
 356   DISCH_THEN (X_CHOOSE_TAC `K:real`);
 357   POP_ASSUM MP_TAC THEN STRIP_TAC;
 358   (* save *)
 359   CLAIM `x < K /\  K < y`;
 360   STRIP_TAC;
 361   MATCH_MP_TAC REAL_LT_TRANS;
 362   EXISTS_TAC `N`;
 363   ASM_REWRITE_TAC[];
 364   MATCH_MP_TAC REAL_LT_TRANS;
 365   EXISTS_TAC `X`;
 366   ASM_REWRITE_TAC[];
 367   MATCH_MP_TAC REAL_LT_TRANS;
 368   EXISTS_TAC `M`;
 369   ASM_REWRITE_TAC[];
 370   ASM_MESON_TAC[];
 371   (* save *)
 372   MP_TAC (ISPECL [`p:real list`;`X:real`;`z:real`] POLY_MVT);
 373   ASM_REWRITE_TAC[];
 374   REAL_SIMP_TAC;
 375   ONCE_REWRITE_TAC[REAL_ARITH `(x:real = y) <=> (y = x)`];
 376   ASM_REWRITE_TAC[REAL_ENTIRE];
 377   DISCH_THEN (X_CHOOSE_TAC `M:real`);
 378   POP_ASSUM MP_TAC THEN STRIP_TAC;
 379   LABEL_ALL_TAC;
 380   POP_ASSUM MP_TAC;
 381   USE_THEN "Z-5" MP_TAC THEN REAL_ARITH_TAC;
 382   CLAIM `x < M /\  M < y`;
 383   STRIP_TAC;
 384   MATCH_MP_TAC REAL_LT_TRANS;
 385   EXISTS_TAC `X`;
 386   ASM_REWRITE_TAC[];
 387   MATCH_MP_TAC REAL_LT_TRANS;
 388   EXISTS_TAC `z`;
 389   ASM_REWRITE_TAC[];
 390   ASM_MESON_TAC[];
 391 ]);;
 392
 393 (* }}} *)
 394
 395
 396 let pos_neg_neq_thm2 = prove_by_refinement(
 397   `!x y p. x < y ==> poly p x > &0 ==> poly p y < &0 ==>
 398             (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
 399             ?X. x < X /\ X < y /\
 400               (!z. (z = X) ==> (poly p z = &0)) /\
 401               (!z. x < z /\ z < X ==> poly p z > &0) /\
 402               (!z. X < z /\ z < y ==> poly p z < &0)`,
 403 (* {{{ Proof *)
 404 [
 405   REWRITE_TAC[real_gt];
 406   REPEAT STRIP_TAC;
 407   MP_TAC (ISPECL[`x:real`;`y:real`;`p:real list`] pos_neg_neq_thm);
 408   ASM_REWRITE_TAC[];
 409   REPEAT STRIP_TAC;
 410   EXISTS_TAC `X`;
 411   ASM_MESON_TAC[];
 412 ]);;
 413 (* }}} *)
 414
 415 let neg_pos_neq_thm = prove_by_refinement(
 416   `!x y p. x < y /\ poly p x < &0 /\ &0 < poly p y /\
 417             (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
 418             ?X. x < X /\ X < y /\ (poly p X = &0) /\
 419               (!z. x < z /\ z < X ==> poly p z < &0) /\
 420               (!z. X < z /\ z < y ==> &0 < poly p z)`,
 421 (* {{{ Proof *)
 422
 423 [
 424   REPEAT STRIP_TAC;
 425   MP_TAC (ISPECL [`p:real list`;`x:real`;`y:real`] POLY_IVT_POS);
 426   REWRITE_TAC[real_gt];
 427   ASM_REWRITE_TAC[];
 428   DISCH_THEN (X_CHOOSE_TAC `X:real`);
 429   POP_ASSUM MP_TAC THEN STRIP_TAC;
 430   EXISTS_TAC `X`;
 431   ASM_REWRITE_TAC[];
 432   STRIP_TAC;
 433   REPEAT STRIP_TAC;
 434   (* save *)
 435   ONCE_REWRITE_TAC[ARITH_RULE `x < y <=> ~(y < x \/ (x = y))`];
 436   STRIP_TAC;
 437   MP_TAC (ISPECL [`p:real list`;`x:real`;`z:real`] POLY_MVT);
 438   ASM_REWRITE_TAC[];
 439   DISCH_THEN (X_CHOOSE_TAC `N:real`);
 440   POP_ASSUM MP_TAC THEN STRIP_TAC;
 441   CLAIM `&0 < poly p z - poly p x`;
 442   LABEL_ALL_TAC;
 443   USE_THEN "Z-3" MP_TAC;
 444   USE_THEN "Z-11" MP_TAC;
 445   REAL_ARITH_TAC;
 446   STRIP_TAC;
 447   CLAIM `&0 < (z - x) * poly (poly_diff p) N`;
 448   REPEAT_N 2 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 449   ASM_REWRITE_TAC[REAL_MUL_GT];
 450   REPEAT STRIP_TAC;
 451   CLAIM `&0 < z - x`;
 452   LABEL_ALL_TAC;
 453   USE_THEN "Z-8" MP_TAC THEN REAL_ARITH_TAC;
 454   LABEL_ALL_TAC;
 455   USE_THEN "Z-1" MP_TAC THEN REAL_ARITH_TAC;
 456   (* save *)
 457   MP_TAC (ISPECL [`p:real list`;`z:real`;`X:real`] POLY_MVT);
 458   ASM_REWRITE_TAC[];
 459   DISCH_THEN (X_CHOOSE_TAC `M:real`);
 460   POP_ASSUM MP_TAC THEN STRIP_TAC;
 461   CLAIM `&0 - poly p z < &0`;
 462   LABEL_ALL_TAC;
 463   USE_THEN "Z-9" MP_TAC;
 464   REAL_ARITH_TAC;
 465   STRIP_TAC;
 466   CLAIM `&0 < X - z`;
 467   LABEL_ALL_TAC;
 468   USE_THEN "Z-11" MP_TAC THEN REAL_ARITH_TAC;
 469   STRIP_TAC;
 470   CLAIM `(X - z) * poly (poly_diff p) M < &0`;
 471   POP_ASSUM IGNORE;
 472   POP_ASSUM MP_TAC;
 473   POP_ASSUM MP_TAC;
 474   REAL_ARITH_TAC;
 475   REWRITE_TAC[REAL_MUL_LT];
 476   REPEAT STRIP_TAC;
 477   POP_ASSUM IGNORE;
 478   POP_ASSUM MP_TAC;
 479   POP_ASSUM MP_TAC;
 480   REAL_ARITH_TAC;
 481   CLAIM `N < M`;
 482   MATCH_MP_TAC REAL_LT_TRANS;
 483   EXISTS_TAC `z`;
 484   ASM_REWRITE_TAC[];
 485   STRIP_TAC;
 486   MP_TAC (ISPECL [`poly_diff p`;`N:real`;`M:real`] (REWRITE_RULE[real_gt] POLY_IVT_NEG));
 487   ASM_REWRITE_TAC[];
 488   DISCH_THEN (X_CHOOSE_TAC `K:real`);
 489   POP_ASSUM MP_TAC THEN STRIP_TAC;
 490   (* save *)
 491   CLAIM `x < K /\  K < y`;
 492   STRIP_TAC;
 493   MATCH_MP_TAC REAL_LT_TRANS;
 494   EXISTS_TAC `N`;
 495   ASM_REWRITE_TAC[];
 496   MATCH_MP_TAC REAL_LT_TRANS;
 497   EXISTS_TAC `M`;
 498   ASM_REWRITE_TAC[];
 499   MATCH_MP_TAC REAL_LT_TRANS;
 500   EXISTS_TAC `X`;
 501   ASM_REWRITE_TAC[];
 502   ASM_MESON_TAC[];
 503   (* save *)
 504   MP_TAC (ISPECL [`p:real list`;`z:real`;`X:real`] POLY_MVT);
 505   ASM_REWRITE_TAC[];
 506   REAL_SIMP_TAC;
 507   ONCE_REWRITE_TAC[REAL_ARITH `(x:real = y) <=> (y = x)`];
 508   ASM_REWRITE_TAC[REAL_ENTIRE];
 509   DISCH_THEN (X_CHOOSE_TAC `M:real`);
 510   POP_ASSUM MP_TAC THEN STRIP_TAC;
 511   LABEL_ALL_TAC;
 512   POP_ASSUM MP_TAC;
 513   USE_THEN "Z-4" MP_TAC THEN REAL_ARITH_TAC;
 514   CLAIM `x < M /\  M < y`;
 515   STRIP_TAC;
 516   MATCH_MP_TAC REAL_LT_TRANS;
 517   EXISTS_TAC `z`;
 518   ASM_REWRITE_TAC[];
 519   MATCH_MP_TAC REAL_LT_TRANS;
 520   EXISTS_TAC `X`;
 521   ASM_REWRITE_TAC[];
 522   ASM_MESON_TAC[];
 523   (* save *)
 524   REPEAT STRIP_TAC;
 525   ONCE_REWRITE_TAC[ARITH_RULE `x < y <=> ~(y < x \/ (x = y))`];
 526   STRIP_TAC;
 527   MP_TAC (ISPECL [`p:real list`;`X:real`;`z:real`] POLY_MVT);
 528   ASM_REWRITE_TAC[];
 529   DISCH_THEN (X_CHOOSE_TAC `N:real`);
 530   POP_ASSUM MP_TAC THEN STRIP_TAC;
 531   POP_ASSUM MP_TAC;
 532   REAL_SIMP_TAC;
 533   STRIP_TAC;
 534   CLAIM `(z - X) * poly (poly_diff p) N < &0`;
 535   LABEL_ALL_TAC;
 536   USE_THEN "Z-3" MP_TAC;
 537   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 538   ASM_REWRITE_TAC[REAL_MUL_LT];
 539   REPEAT STRIP_TAC;
 540   CLAIM `&0 < z - X`;
 541   LABEL_ALL_TAC;
 542   USE_THEN "Z-7" MP_TAC THEN REAL_ARITH_TAC;
 543   LABEL_ALL_TAC;
 544   USE_THEN "Z-1" MP_TAC THEN REAL_ARITH_TAC;
 545   (* save *)
 546   MP_TAC (ISPECL [`p:real list`;`z:real`;`y:real`] POLY_MVT);
 547   LABEL_ALL_TAC;
 548   USE_THEN "Z-6" (REWRITE_TAC o list);
 549   DISCH_THEN (X_CHOOSE_TAC `M:real`);
 550   POP_ASSUM MP_TAC THEN STRIP_TAC;
 551   CLAIM `&0 < poly p y - poly p z`;
 552   LABEL_ALL_TAC;
 553   USE_THEN "Z-12" MP_TAC;
 554   USE_THEN "Z-5" MP_TAC;
 555   REAL_ARITH_TAC;
 556   STRIP_TAC;
 557   CLAIM `&0 < y - z`;
 558   LABEL_ALL_TAC;
 559   USE_THEN "Z-6" MP_TAC THEN REAL_ARITH_TAC;
 560   STRIP_TAC;
 561   CLAIM `&0 < (y - z) * poly (poly_diff p) M`;
 562   POP_ASSUM IGNORE;
 563   POP_ASSUM MP_TAC;
 564   POP_ASSUM MP_TAC;
 565   REAL_ARITH_TAC;
 566   REWRITE_TAC[REAL_MUL_GT];
 567   REPEAT STRIP_TAC;
 568   POP_ASSUM IGNORE;
 569   POP_ASSUM MP_TAC;
 570   POP_ASSUM MP_TAC;
 571   REAL_ARITH_TAC;
 572   CLAIM `N < M`;
 573   MATCH_MP_TAC REAL_LT_TRANS;
 574   EXISTS_TAC `z`;
 575   ASM_REWRITE_TAC[];
 576   STRIP_TAC;
 577   MP_TAC (ISPECL [`poly_diff p`;`N:real`;`M:real`] (REWRITE_RULE[real_gt] POLY_IVT_POS));
 578   ASM_REWRITE_TAC[];
 579   DISCH_THEN (X_CHOOSE_TAC `K:real`);
 580   POP_ASSUM MP_TAC THEN STRIP_TAC;
 581   (* save *)
 582   CLAIM `x < K /\  K < y`;
 583   STRIP_TAC;
 584   MATCH_MP_TAC REAL_LT_TRANS;
 585   EXISTS_TAC `N`;
 586   ASM_REWRITE_TAC[];
 587   MATCH_MP_TAC REAL_LT_TRANS;
 588   EXISTS_TAC `X`;
 589   ASM_REWRITE_TAC[];
 590   MATCH_MP_TAC REAL_LT_TRANS;
 591   EXISTS_TAC `M`;
 592   ASM_REWRITE_TAC[];
 593   ASM_MESON_TAC[];
 594   (* save *)
 595   POP_ASSUM (ASSUME_TAC o GSYM);
 596   MP_TAC (ISPECL [`p:real list`;`X:real`;`z:real`] POLY_MVT);
 597   ASM_REWRITE_TAC[];
 598   REAL_SIMP_TAC;
 599   ONCE_REWRITE_TAC[REAL_ARITH `(x:real = y) <=> (y = x)`];
 600   ASM_REWRITE_TAC[REAL_ENTIRE];
 601   DISCH_THEN (X_CHOOSE_TAC `M:real`);
 602   POP_ASSUM MP_TAC THEN STRIP_TAC;
 603   LABEL_ALL_TAC;
 604   POP_ASSUM MP_TAC;
 605   USE_THEN "Z-5" MP_TAC THEN REAL_ARITH_TAC;
 606   CLAIM `x < M /\  M < y`;
 607   STRIP_TAC;
 608   MATCH_MP_TAC REAL_LT_TRANS;
 609   EXISTS_TAC `X`;
 610   ASM_REWRITE_TAC[];
 611   MATCH_MP_TAC REAL_LT_TRANS;
 612   EXISTS_TAC `z`;
 613   ASM_REWRITE_TAC[];
 614   ASM_MESON_TAC[];
 615 ]);;
 616
 617 (* }}} *)
 618
 619 let neg_pos_neq_thm2 = prove_by_refinement(
 620   `!x y p. x < y ==> poly p x < &0 ==> poly p y > &0 ==>
 621             (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
 622             ?X. x < X /\ X < y /\
 623               (!z. (z = X) ==> (poly p z = &0)) /\
 624               (!z. x < z /\ z < X ==> poly p z < &0) /\
 625               (!z. X < z /\ z < y ==> poly p z > &0)`,
 626 (* {{{ Proof *)
 627 [
 628   REWRITE_TAC[real_gt];
 629   REPEAT STRIP_TAC;
 630   MP_TAC (ISPECL[`x:real`;`y:real`;`p:real list`] neg_pos_neq_thm);
 631   ASM_REWRITE_TAC[];
 632   REPEAT STRIP_TAC;
 633   EXISTS_TAC `X`;
 634   ASM_MESON_TAC[];
 635 ]);;
 636 (* }}} *)
 637
 638
 639 let lt_nz_thm = prove_by_refinement(
 640   `(!x. x1 < x /\ x < x2 ==> poly p x < &0) ==> (!x. x1 < x /\ x < x2 ==> ~(poly p x = &0))`,
 641 (* {{{ Proof *)
 642 [
 643   MESON_TAC[REAL_LT_NZ];
 644 ]);;
 645 (* }}} *)
 646
 647 let gt_nz_thm = prove_by_refinement(
 648   `(!x. x1 < x /\ x < x2 ==> poly p x > &0) ==> (!x. x1 < x /\ x < x2 ==> ~(poly p x = &0))`,
 649 (* {{{ Proof *)
 650 [
 651   MESON_TAC[REAL_LT_NZ;real_gt];
 652 ]);;
 653 (* }}} *)
 654
 655 let eq_eq_false_thm = prove_by_refinement(
 656   `!x y p. x < y ==> (poly p x = &0) ==> (poly p y = &0) ==>
 657        (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==> F`,
 658 (* {{{ Proof *)
 659
 660 [
 661   REPEAT_N 3 STRIP_TAC;
 662   DISCH_THEN (fun x -> MP_TAC (MATCH_MP (ISPEC `p:real list` POLY_MVT) x) THEN ASSUME_TAC x);
 663   REPEAT STRIP_TAC;
 664   LABEL_ALL_TAC;
 665   CLAIM `poly p y - poly p x = &0`;
 666   REWRITE_TAC[real_sub];
 667   ASM_REWRITE_TAC[];
 668   REAL_ARITH_TAC;
 669   DISCH_THEN (REWRITE_ASSUMS o list);
 670   CLAIM `&0 < y - x`;
 671   USE_THEN "Z-6" MP_TAC THEN REAL_ARITH_TAC;
 672   POP_ASSUM (MP_TAC o ISPEC `x':real`);
 673   RULE_ASSUM_TAC GSYM;
 674   POP_ASSUM IGNORE THEN POP_ASSUM IGNORE;
 675   ASM_REWRITE_TAC[];
 676   STRIP_TAC;
 677   STRIP_TAC;
 678   ASM_MESON_TAC[REAL_ENTIRE;REAL_POS_NZ];
 679 ]);;
 680
 681 (* }}} *)
 682
 683 let neg_zero_neg_thm = prove_by_refinement(
 684   `!x y p. x < y ==> poly p x < &0 ==> (poly p y = &0) ==>
 685      (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
 686      (!z. x < z /\ z < y ==> poly p z < &0)`,
 687 (* {{{ Proof *)
 688
 689 [
 690   REPEAT STRIP_TAC;
 691   REWRITE_TAC[ARITH_RULE `x < y <=> ~(y <= x)`];
 692   REWRITE_TAC[ARITH_RULE `x <= y <=> (x < y \/ (x = y))`];
 693   STRIP_TAC;
 694   MP_TAC (ISPECL [`p:real list`;`x:real`;`z:real`] POLY_MVT);
 695   ASM_REWRITE_TAC[];
 696   STRIP_TAC;
 697   CLAIM `poly p z - poly p x > &0`;
 698   LABEL_ALL_TAC;
 699   USE_THEN "Z-3" MP_TAC;
 700   USE_THEN "Z-8" MP_TAC;
 701   REAL_ARITH_TAC;
 702   STRIP_TAC;
 703   CLAIM `(z - x) * poly (poly_diff p) x' > &0`;
 704   REPEAT_N 2 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 705   REWRITE_TAC[real_gt];
 706   ASM_REWRITE_TAC[REAL_MUL_GT];
 707   REPEAT STRIP_TAC;
 708   CLAIM `&0 < z - x`;
 709   LABEL_ALL_TAC;
 710   USE_THEN "Z-8" MP_TAC THEN REAL_ARITH_TAC;
 711   STRIP_TAC;
 712   CLAIM `(z - x) * poly (poly_diff p) x' < &0`;
 713   REWRITE_TAC[REAL_MUL_LT];
 714   DISJ2_TAC;
 715   ASM_REWRITE_TAC[];
 716   ASM_MESON_TAC[REAL_LT_ANTISYM];
 717   (* save *)
 718   MP_TAC (ISPECL [`p:real list`;`z:real`;`y:real`] POLY_MVT);
 719   ASM_REWRITE_TAC[];
 720   STRIP_TAC;
 721   CLAIM `&0 - poly p z < &0`;
 722   LABEL_ALL_TAC;
 723   USE_THEN "Z-9" MP_TAC;
 724   REAL_ARITH_TAC;
 725   STRIP_TAC;
 726   CLAIM `&0 < y - z`;
 727   LABEL_ALL_TAC;
 728   USE_THEN "Z-11" MP_TAC THEN REAL_ARITH_TAC;
 729   STRIP_TAC;
 730   CLAIM `(y - z) * poly (poly_diff p) x'' < &0`;
 731   POP_ASSUM IGNORE;
 732   POP_ASSUM MP_TAC;
 733   POP_ASSUM MP_TAC;
 734   REAL_ARITH_TAC;
 735   ASM_REWRITE_TAC[REAL_MUL_LT];
 736   REPEAT STRIP_TAC;
 737   REPEAT_N 3 (POP_ASSUM MP_TAC);
 738   REAL_ARITH_TAC;
 739   (* save *)
 740   CLAIM `x' < x''`;
 741   MATCH_MP_TAC REAL_LT_TRANS;
 742   EXISTS_TAC `z`;
 743   ASM_REWRITE_TAC[];
 744   STRIP_TAC;
 745   MP_TAC (ISPECL [`poly_diff p`;`x':real`;`x'':real`] (REWRITE_RULE[real_gt] POLY_IVT_NEG));
 746   REWRITE_ASSUMS[real_gt];
 747   ASM_REWRITE_TAC[];
 748   STRIP_TAC;
 749   CLAIM `x < x''' /\  x''' < y`;
 750   STRIP_TAC;
 751   MATCH_MP_TAC REAL_LT_TRANS;
 752   EXISTS_TAC `x'`;
 753   ASM_REWRITE_TAC[];
 754   MATCH_MP_TAC REAL_LT_TRANS;
 755   EXISTS_TAC `x''`;
 756   ASM_REWRITE_TAC[];
 757   ASM_MESON_TAC[];
 758   (* save *)
 759   MP_TAC  (ISPECL[`z:real`;`y:real`;`p:real list`] eq_eq_false_thm);
 760   POP_ASSUM (ASSUME_TAC o GSYM);
 761   ASM_REWRITE_TAC[];
 762   REPEAT_N 2 STRIP_TAC;
 763   FIRST_ASSUM MATCH_MP_TAC;
 764   ASM_REWRITE_TAC[];
 765   MATCH_MP_TAC REAL_LT_TRANS;
 766   EXISTS_TAC `z`;
 767   ASM_REWRITE_TAC[];
 768 ]);;
 769
 770 (* }}} *)
 771
 772 let pos_zero_pos_thm = prove_by_refinement(
 773   `!x y p. x < y ==> poly p x > &0 ==> (poly p y = &0) ==>
 774      (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
 775      (!z. x < z /\ z < y ==> poly p z > &0)`,
 776 (* {{{ Proof *)
 777
 778 [
 779   REPEAT STRIP_TAC;
 780   REWRITE_TAC[ARITH_RULE `x > y <=> ~(y >= x)`];
 781   REWRITE_TAC[ARITH_RULE `x >= y <=> (x > y \/ (x = y))`];
 782   STRIP_TAC;
 783   MP_TAC (ISPECL [`p:real list`;`x:real`;`z:real`] POLY_MVT);
 784   ASM_REWRITE_TAC[];
 785   STRIP_TAC;
 786   CLAIM `poly p z - poly p x < &0`;
 787   LABEL_ALL_TAC;
 788   USE_THEN "Z-3" MP_TAC;
 789   USE_THEN "Z-8" MP_TAC;
 790   REAL_ARITH_TAC;
 791   STRIP_TAC;
 792   CLAIM `(z - x) * poly (poly_diff p) x' < &0`;
 793   REPEAT_N 2 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 794   REWRITE_TAC[real_gt];
 795   ASM_REWRITE_TAC[REAL_MUL_LT];
 796   REPEAT STRIP_TAC;
 797   CLAIM `&0 < z - x`;
 798   LABEL_ALL_TAC;
 799   USE_THEN "Z-8" MP_TAC THEN REAL_ARITH_TAC;
 800   STRIP_TAC;
 801   CLAIM `&0 < (z - x) * poly (poly_diff p) x'`;
 802   REWRITE_TAC[REAL_MUL_GT];
 803   DISJ2_TAC;
 804   ASM_REWRITE_TAC[];
 805   ASM_MESON_TAC[REAL_LT_ANTISYM];
 806   (* save *)
 807   MP_TAC (ISPECL [`p:real list`;`z:real`;`y:real`] POLY_MVT);
 808   ASM_REWRITE_TAC[];
 809   STRIP_TAC;
 810   CLAIM `&0 - poly p z > &0`;
 811   LABEL_ALL_TAC;
 812   USE_THEN "Z-9" MP_TAC;
 813   REAL_ARITH_TAC;
 814   STRIP_TAC;
 815   CLAIM `&0 < y - z`;
 816   LABEL_ALL_TAC;
 817   USE_THEN "Z-11" MP_TAC THEN REAL_ARITH_TAC;
 818   STRIP_TAC;
 819   CLAIM `(y - z) * poly (poly_diff p) x'' > &0`;
 820   POP_ASSUM IGNORE;
 821   POP_ASSUM MP_TAC;
 822   POP_ASSUM MP_TAC;
 823   REAL_ARITH_TAC;
 824   ASM_REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;];
 825   REPEAT STRIP_TAC;
 826   REPEAT_N 3 (POP_ASSUM MP_TAC);
 827   REAL_ARITH_TAC;
 828   (* save *)
 829   CLAIM `x' < x''`;
 830   MATCH_MP_TAC REAL_LT_TRANS;
 831   EXISTS_TAC `z`;
 832   ASM_REWRITE_TAC[];
 833   STRIP_TAC;
 834   MP_TAC (ISPECL [`poly_diff p`;`x':real`;`x'':real`] (REWRITE_RULE[real_gt] POLY_IVT_POS));
 835   REWRITE_ASSUMS[real_gt];
 836   ASM_REWRITE_TAC[];
 837   STRIP_TAC;
 838   CLAIM `x < x''' /\  x''' < y`;
 839   STRIP_TAC;
 840   MATCH_MP_TAC REAL_LT_TRANS;
 841   EXISTS_TAC `x'`;
 842   ASM_REWRITE_TAC[];
 843   MATCH_MP_TAC REAL_LT_TRANS;
 844   EXISTS_TAC `x''`;
 845   ASM_REWRITE_TAC[];
 846   ASM_MESON_TAC[];
 847   (* save *)
 848   MP_TAC  (ISPECL[`z:real`;`y:real`;`p:real list`] eq_eq_false_thm);
 849   POP_ASSUM (ASSUME_TAC o GSYM);
 850   ASM_REWRITE_TAC[];
 851   REPEAT_N 2 STRIP_TAC;
 852   FIRST_ASSUM MATCH_MP_TAC;
 853   ASM_REWRITE_TAC[];
 854   MATCH_MP_TAC REAL_LT_TRANS;
 855   EXISTS_TAC `z`;
 856   ASM_REWRITE_TAC[];
 857 ]);;
 858
 859 (* }}} *)
 860
 861 let zero_neg_neg_thm = prove_by_refinement(
 862   `!x y p. x < y ==> (poly p x = &0) ==> (poly p y < &0) ==>
 863      (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
 864      (!z. x < z /\ z < y ==> poly p z < &0)`,
 865 (* {{{ Proof *)
 866
 867 [
 868   REPEAT STRIP_TAC;
 869   REWRITE_TAC[ARITH_RULE `x < y <=> ~(y <= x)`];
 870   REWRITE_TAC[ARITH_RULE `x <= y <=> (x < y \/ (x = y))`];
 871   STRIP_TAC;
 872   MP_TAC (ISPECL [`p:real list`;`x:real`;`z:real`] POLY_MVT);
 873   ASM_REWRITE_TAC[];
 874   STRIP_TAC;
 875   CLAIM `poly p z - &0 > &0`;
 876   LABEL_ALL_TAC;
 877   USE_THEN "Z-3" MP_TAC;
 878   USE_THEN "Z-8" MP_TAC;
 879   REAL_ARITH_TAC;
 880   STRIP_TAC;
 881   CLAIM `(z - x) * poly (poly_diff p) x' > &0`;
 882   REPEAT_N 2 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 883   REWRITE_TAC[real_gt];
 884   ASM_REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;];
 885   REPEAT STRIP_TAC;
 886   CLAIM `&0 < z - x`;
 887   LABEL_ALL_TAC;
 888   USE_THEN "Z-8" MP_TAC THEN REAL_ARITH_TAC;
 889   STRIP_TAC;
 890   CLAIM `&0 > (z - x) * poly (poly_diff p) x'`;
 891   REWRITE_TAC[REAL_MUL_GT;real_gt;REAL_MUL_LT;];
 892   DISJ2_TAC;
 893   ASM_REWRITE_TAC[];
 894   ASM_MESON_TAC[REAL_LT_ANTISYM];
 895   (* save *)
 896   MP_TAC (ISPECL [`p:real list`;`z:real`;`y:real`] POLY_MVT);
 897   ASM_REWRITE_TAC[];
 898   STRIP_TAC;
 899   CLAIM `poly p y - poly p z < &0`;
 900   LABEL_ALL_TAC;
 901   USE_THEN "Z-13" MP_TAC;
 902   USE_THEN "Z-9" MP_TAC;
 903   REAL_ARITH_TAC;
 904   STRIP_TAC;
 905   CLAIM `&0 < y - z`;
 906   LABEL_ALL_TAC;
 907   USE_THEN "Z-11" MP_TAC THEN REAL_ARITH_TAC;
 908   STRIP_TAC;
 909   CLAIM `(y - z) * poly (poly_diff p) x'' < &0`;
 910   POP_ASSUM IGNORE;
 911   POP_ASSUM MP_TAC;
 912   POP_ASSUM MP_TAC;
 913   REAL_ARITH_TAC;
 914   ASM_REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;];
 915   REPEAT STRIP_TAC;
 916   REPEAT_N 3 (POP_ASSUM MP_TAC);
 917   REAL_ARITH_TAC;
 918   (* save *)
 919   CLAIM `x' < x''`;
 920   MATCH_MP_TAC REAL_LT_TRANS;
 921   EXISTS_TAC `z`;
 922   ASM_REWRITE_TAC[];
 923   STRIP_TAC;
 924   MP_TAC (ISPECL [`poly_diff p`;`x':real`;`x'':real`] (REWRITE_RULE[real_gt] POLY_IVT_NEG));
 925   REWRITE_ASSUMS[real_gt];
 926   ASM_REWRITE_TAC[];
 927   STRIP_TAC;
 928   CLAIM `x < x''' /\  x''' < y`;
 929   STRIP_TAC;
 930   MATCH_MP_TAC REAL_LT_TRANS;
 931   EXISTS_TAC `x'`;
 932   ASM_REWRITE_TAC[];
 933   MATCH_MP_TAC REAL_LT_TRANS;
 934   EXISTS_TAC `x''`;
 935   ASM_REWRITE_TAC[];
 936   ASM_MESON_TAC[];
 937   (* save *)
 938   MP_TAC  (ISPECL[`x:real`;`z:real`;`p:real list`] eq_eq_false_thm);
 939   POP_ASSUM (ASSUME_TAC o GSYM);
 940   ASM_REWRITE_TAC[];
 941   REPEAT_N 2 STRIP_TAC;
 942   FIRST_ASSUM MATCH_MP_TAC;
 943   ASM_REWRITE_TAC[];
 944   MATCH_MP_TAC REAL_LT_TRANS;
 945   EXISTS_TAC `z`;
 946   ASM_REWRITE_TAC[];
 947 ]);;
 948
 949 (* }}} *)
 950
 951 let zero_pos_pos_thm = prove_by_refinement(
 952   `!x y p. x < y ==> (poly p x = &0) ==> (poly p y > &0) ==>
 953      (!z. x < z /\ z < y ==> ~(poly (poly_diff p) z = &0)) ==>
 954      (!z. x < z /\ z < y ==> poly p z > &0)`,
 955 (* {{{ Proof *)
 956
 957 [
 958   REPEAT STRIP_TAC;
 959   REWRITE_TAC[ARITH_RULE `x > y <=> ~(y >= x)`];
 960   REWRITE_TAC[ARITH_RULE `x >= y <=> (x > y \/ (x = y))`];
 961   STRIP_TAC;
 962   MP_TAC (ISPECL [`p:real list`;`z:real`;`y:real`] POLY_MVT);
 963   ASM_REWRITE_TAC[];
 964   STRIP_TAC;
 965   CLAIM `poly p y - poly p z > &0`;
 966   LABEL_ALL_TAC;
 967   USE_THEN "Z-7" MP_TAC;
 968   USE_THEN "Z-3" MP_TAC;
 969   REAL_ARITH_TAC;
 970   STRIP_TAC;
 971   CLAIM `(y - z) * poly (poly_diff p) x' > &0`;
 972   REPEAT_N 2 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
 973   REWRITE_TAC[real_gt];
 974   ASM_REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;];
 975   REPEAT STRIP_TAC;
 976   LABEL_ALL_TAC;
 977   USE_THEN "Z-1" MP_TAC;
 978   USE_THEN "Z-7" MP_TAC;
 979   REAL_ARITH_TAC;
 980   (* save *)
 981   MP_TAC (ISPECL [`p:real list`;`x:real`;`z:real`] POLY_MVT);
 982   ASM_REWRITE_TAC[];
 983   STRIP_TAC;
 984   CLAIM `poly p z - &0 < &0`;
 985   LABEL_ALL_TAC;
 986   USE_THEN "Z-9" MP_TAC;
 987   REAL_ARITH_TAC;
 988   STRIP_TAC;
 989   CLAIM `&0 < z - x`;
 990   LABEL_ALL_TAC;
 991   USE_THEN "Z-12" MP_TAC THEN REAL_ARITH_TAC;
 992   STRIP_TAC;
 993   CLAIM `(z - x) * poly (poly_diff p) x'' < &0`;
 994   POP_ASSUM IGNORE;
 995   POP_ASSUM MP_TAC;
 996   POP_ASSUM MP_TAC;
 997   REAL_ARITH_TAC;
 998   ASM_REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;];
 999   REPEAT STRIP_TAC;
1000   REPEAT_N 3 (POP_ASSUM MP_TAC);
1001   REAL_ARITH_TAC;
1002   (* save *)
1003   CLAIM `x'' < x'`;
1004   MATCH_MP_TAC REAL_LT_TRANS;
1005   EXISTS_TAC `z`;
1006   ASM_REWRITE_TAC[];
1007   STRIP_TAC;
1008   MP_TAC (ISPECL [`poly_diff p`;`x'':real`;`x':real`] (REWRITE_RULE[real_gt] POLY_IVT_POS));
1009   REWRITE_ASSUMS[real_gt];
1010   ASM_REWRITE_TAC[];
1011   STRIP_TAC;
1012   CLAIM `x < x''' /\  x''' < y`;
1013   STRIP_TAC;
1014   MATCH_MP_TAC REAL_LT_TRANS;
1015   EXISTS_TAC `x''`;
1016   ASM_REWRITE_TAC[];
1017   MATCH_MP_TAC REAL_LT_TRANS;
1018   EXISTS_TAC `x'`;
1019   ASM_REWRITE_TAC[];
1020   ASM_MESON_TAC[];
1021   (* save *)
1022   MP_TAC  (ISPECL[`x:real`;`z:real`;`p:real list`] eq_eq_false_thm);
1023   POP_ASSUM (ASSUME_TAC o GSYM);
1024   ASM_REWRITE_TAC[];
1025   REPEAT_N 2 STRIP_TAC;
1026   FIRST_ASSUM MATCH_MP_TAC;
1027   ASM_REWRITE_TAC[];
1028   MATCH_MP_TAC REAL_LT_TRANS;
1029   EXISTS_TAC `z`;
1030   ASM_REWRITE_TAC[];
1031 ]);;
1032
1033 (* }}} *)