Rqe/asym.ml

   1 override_interface ("-->",`(tends_num_real)`);;
   2 prioritize_real();;
   3
   4 (* ---------------------------------------------------------------------- *)
   5 (*  properites of num sequences                                           *)
   6 (* ---------------------------------------------------------------------- *)
   7
   8 let LIM_INV_1N = prove_by_refinement(
   9   `(\n. &1 / &n) --> &0`,
  10 (* {{{ Proof *)
  11
  12 [
  13   REWRITE_TAC[SEQ;real_sub;REAL_ADD_RID;REAL_NEG_0;real_gt;real_ge;GT;GE];
  14   REPEAT STRIP_TAC;
  15   MP_TAC (ISPEC `&2 / e` REAL_ARCH_SIMPLE);
  16   STRIP_TAC;
  17   EXISTS_TAC `n`;
  18   REPEAT STRIP_TAC;
  19   CLAIM `&0 < &2 / e`;
  20   ASM_MESON_TAC[REAL_LT_RDIV_0;REAL_ARITH `&0 < &2`];
  21   STRIP_TAC;
  22   CLAIM `&0 < &n`;
  23   ASM_MESON_TAC[REAL_LTE_TRANS;REAL_LE];
  24   STRIP_TAC;
  25   CLAIM `&0 < &n'`;
  26   ASM_MESON_TAC[REAL_LTE_TRANS;REAL_LE];
  27   STRIP_TAC;
  28   CLAIM `~(&n' = &0)`;
  29   ASM_MESON_TAC[REAL_LT_IMP_NZ];
  30   STRIP_TAC;
  31   ASM_SIMP_TAC[ABS_DIV];
  32   REWRITE_TAC[REAL_ABS_NUM];
  33   ASM_SIMP_TAC[REAL_LT_LDIV_EQ];
  34   CLAIM `&2 <= e * &n`;
  35   ASM_MESON_TAC[REAL_LE_LDIV_EQ;REAL_MUL_SYM];
  36   STRIP_TAC;
  37   CLAIM `e * &n <= e * &n'`;
  38   MATCH_MP_TAC REAL_LE_LMUL;
  39   ASM_MESON_TAC [REAL_LT_LE;REAL_LE];
  40   STRIP_TAC;
  41   ASM_MESON_TAC[REAL_LTE_TRANS;REAL_LE_TRANS;REAL_ARITH `&1 < &2`];
  42 ]);;
  43
  44 (* }}} *)
  45
  46 let LIM_INV_CONST = prove_by_refinement(
  47   `!c. (\n. c / &n) --> &0`,
  48 (* {{{ Proof *)
  49
  50 [
  51   ONCE_REWRITE_TAC[REAL_ARITH  `c / &n = c * &1 / &n`];
  52   STRIP_TAC;
  53   CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[REAL_ARITH `&0 = c * &0`]));
  54   MATCH_MP_TAC SEQ_MUL;
  55   CONJ_TAC THENL [MATCH_ACCEPT_TAC SEQ_CONST;MATCH_ACCEPT_TAC LIM_INV_1N];
  56 ]);;
  57
  58 (* }}} *)
  59
  60 let LIM_INV_1NP = prove_by_refinement(
  61   `!c k. 0 < k ==> (\n. c / &n pow k) --> &0`,
  62 (* {{{ Proof *)
  63 [
  64   STRIP_TAC;
  65   INDUCT_TAC;
  66   REWRITE_TAC[ARITH_RULE `~(0 < 0)`];
  67   REWRITE_TAC[real_pow;REAL_DIV_DISTRIB_R];
  68   STRIP_TAC;
  69   CASES_ON `k = 0`;
  70   ASM_REWRITE_TAC[real_pow;GSYM REAL_DIV_DISTRIB_R;REAL_MUL_RID];
  71   MATCH_ACCEPT_TAC LIM_INV_CONST;
  72   CLAIM `(\n. c / &n pow k) --> &0`;
  73   FIRST_ASSUM MATCH_MP_TAC;
  74   EVERY_ASSUM MP_TAC THEN ARITH_TAC;
  75   STRIP_TAC;
  76   ONCE_REWRITE_TAC[REAL_ARITH `&0 = &0 * &0`];
  77   MATCH_MP_TAC SEQ_MUL;
  78   CONJ_TAC THENL [MATCH_ACCEPT_TAC LIM_INV_1N;FIRST_ASSUM MATCH_ACCEPT_TAC];
  79 ]);;
  80 (* }}} *)
  81
  82 let LIM_INV_CON = prove_by_refinement(
  83   `!c d k. 0 < k ==> (\n. c / (d * &n pow k)) --> &0`,
  84 (* {{{ Proof *)
  85 [
  86   REWRITE_TAC[REAL_DIV_DISTRIB_R];
  87   REPEAT STRIP_TAC;
  88   ONCE_REWRITE_TAC[REAL_ARITH `&0 = (&1 / d) * &0`];
  89   MATCH_MP_TAC SEQ_MUL;
  90   CONJ_TAC;
  91   MATCH_ACCEPT_TAC SEQ_CONST;
  92   POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC LIM_INV_1NP;
  93 ]);;
  94 (* }}} *)
  95
  96 let LIM_NN = prove_by_refinement(
  97   `(\n. &n / &n) --> &1`,
  98 (* {{{ Proof *)
  99 [
 100   REWRITE_TAC[SEQ];
 101   REPEAT STRIP_TAC;
 102   EXISTS_TAC `1`;
 103   REWRITE_TAC[GT;GE];
 104   REPEAT STRIP_TAC;
 105   CLAIM `~(&n = &0)`;
 106   MATCH_MP_TAC REAL_LT_IMP_NZ;
 107   ASM_MESON_TAC[REAL_LE;REAL_ARITH `&0 < &1`;REAL_LTE_TRANS];
 108   STRIP_TAC;
 109   ASM_SIMP_TAC[REAL_DIV_REFL;real_sub;REAL_ADD_RINV;ABS_0];
 110 ]);;
 111 (* }}} *)
 112
 113 let LIM_NNC = prove_by_refinement(
 114   `~(k = &0) ==> (\n. (k * &n) / (k * &n)) --> &1`,
 115 (* {{{ Proof *)
 116 [
 117   REWRITE_TAC[REAL_DIV_DISTRIB_2];
 118   ONCE_REWRITE_TAC[REAL_ARITH `&1 = &1 * &1`];
 119   STRIP_TAC;
 120   MATCH_MP_TAC SEQ_MUL;
 121   CONJ_TAC;
 122   ASM_SIMP_TAC[real_div;REAL_MUL_RINV];
 123   MATCH_ACCEPT_TAC SEQ_CONST;
 124   MATCH_ACCEPT_TAC LIM_NN;
 125 ]);;
 126 (* }}} *)
 127
 128 let LIM_MONO = prove_by_refinement(
 129   `!c d a b. ~(d = &0) /\ a < b ==> (\n. (c * &n pow a) / (d * &n pow b)) --> &0`,
 130 (* {{{ Proof *)
 131 [
 132   STRIP_TAC THEN STRIP_TAC;
 133   INDUCT_TAC;
 134   REPEAT STRIP_TAC;
 135   REWRITE_TAC[real_pow;REAL_MUL_RID];
 136   POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC LIM_INV_CON;
 137   REPEAT STRIP_TAC;
 138   REWRITE_TAC[real_pow];
 139   CLAIM `(b = SUC(PRE b))`;
 140   POP_ASSUM MP_TAC THEN ARITH_TAC;
 141   STRIP_TAC;
 142   ONCE_ASM_REWRITE_TAC[];
 143   REWRITE_TAC[real_pow];
 144   ONCE_REWRITE_TAC[ARITH_RULE `a * b * c = b * a * c`];
 145   ONCE_REWRITE_TAC[REAL_DIV_DISTRIB_2];
 146   ONCE_REWRITE_TAC[REAL_ARITH `&0 = &1 * &0`];
 147   MATCH_MP_TAC SEQ_MUL;
 148   CONJ_TAC;
 149   MATCH_ACCEPT_TAC LIM_NN;
 150   FIRST_ASSUM MATCH_MP_TAC;
 151   ASM_REWRITE_TAC[];
 152   LABEL_ALL_TAC;
 153   USE_THEN "Z-1" MP_TAC;
 154   ARITH_TAC;
 155 ]);;
 156 (* }}} *)
 157
 158 let LIM_POLY_LT = prove_by_refinement(
 159   `!p k. LENGTH p <= k ==> (\n. poly p (&n) / &n pow k) --> &0`,
 160 (* {{{ Proof *)
 161
 162 [
 163   LIST_INDUCT_TAC;
 164   REWRITE_TAC[poly;LENGTH];
 165   REPEAT STRIP_TAC;
 166   REWRITE_TAC[REAL_DIV_LZERO;SEQ_CONST];
 167   REWRITE_TAC[poly;LENGTH];
 168   REPEAT STRIP_TAC;
 169   CLAIM `~(k = 0)`;
 170   POP_ASSUM MP_TAC THEN ARITH_TAC;
 171   STRIP_TAC;
 172   LABEL_ALL_TAC;
 173   CLAIM `LENGTH t <= PRE k`;
 174   USE_THEN "Z-1" MP_TAC THEN ARITH_TAC;
 175   DISCH_THEN (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x)));
 176   STRIP_TAC;
 177   REWRITE_TAC[REAL_DIV_ADD_DISTRIB];
 178   ONCE_REWRITE_TAC[REAL_ARITH `&0 = &0 + &0`];
 179   MATCH_MP_TAC SEQ_ADD;
 180   CONJ_TAC;
 181   ONCE_REWRITE_TAC[ARITH_RULE `n pow k = &1 * n pow k`];
 182   MATCH_MP_TAC LIM_INV_CON;
 183   USE_THEN "Z-0" MP_TAC THEN ARITH_TAC;
 184   CLAIM `k = SUC (PRE k)`;
 185   USE_THEN "Z-0" MP_TAC THEN ARITH_TAC;
 186   STRIP_TAC;
 187   ONCE_ASM_REWRITE_TAC[];
 188   REWRITE_TAC[real_pow];
 189   REWRITE_TAC[REAL_DIV_DISTRIB_2];
 190   ONCE_REWRITE_TAC[REAL_ARITH `&0 = &1 * &0`];
 191   MATCH_MP_TAC SEQ_MUL;
 192   CONJ_TAC;
 193   MATCH_ACCEPT_TAC LIM_NN;
 194   FIRST_ASSUM MATCH_MP_TAC;
 195   USE_THEN "Z-1" MP_TAC THEN ARITH_TAC;
 196 ]);;
 197
 198 (* }}} *)
 199
 200 let LIM_POLY = prove_by_refinement(
 201   `!p. (0 < LENGTH p /\ ~(LAST p = &0)) ==>
 202      (\n. poly p (&n) / (LAST p * &n pow PRE (LENGTH p))) --> &1`,
 203 (* {{{ Proof *)
 204
 205 [
 206   LIST_INDUCT_TAC;
 207   REWRITE_TAC[LENGTH;LT];
 208   ASM_REWRITE_TAC[LENGTH;poly];
 209   REPEAT STRIP_TAC;
 210   CASES_ON `t = []`;
 211   ASM_REWRITE_TAC[PRE;real_pow;REAL_POW_1;LAST;poly;REAL_MUL_RZERO;REAL_ADD_RID;LENGTH;REAL_DIV_DISTRIB_L];
 212   CLAIM `~(h = &0)`;
 213   ASM_MESON_TAC[LAST];
 214   STRIP_TAC;
 215   CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[REAL_ARITH `&1 = &1 * &1`]));
 216   MATCH_MP_TAC SEQ_MUL;
 217   CONJ_TAC;
 218   ASM_SIMP_TAC[DIV_ID];
 219   MATCH_ACCEPT_TAC SEQ_CONST;
 220   ASM_SIMP_TAC[DIV_ID;REAL_10];
 221   MATCH_ACCEPT_TAC SEQ_CONST;
 222   CLAIM `LAST (CONS h t) = LAST t`;
 223   ASM_REWRITE_TAC[LAST];
 224   STRIP_TAC;
 225   ASM_REWRITE_TAC[LAST;PRE];
 226   REWRITE_TAC[REAL_DIV_ADD_DISTRIB];
 227   ONCE_REWRITE_TAC [REAL_ARITH `&1 = &0 + &1`];
 228   MATCH_MP_TAC SEQ_ADD;
 229   CLAIM `~(LENGTH t = 0)`;
 230   ASM_MESON_TAC[LENGTH_0];
 231   STRIP_TAC;
 232   CONJ_TAC;
 233   MATCH_MP_TAC LIM_INV_CON;
 234   POP_ASSUM MP_TAC THEN ARITH_TAC;
 235   CLAIM `(LENGTH t = SUC (PRE (LENGTH t)))`;
 236   POP_ASSUM MP_TAC THEN ARITH_TAC;
 237   STRIP_TAC;
 238   ONCE_ASM_REWRITE_TAC[];
 239   REWRITE_TAC[real_pow];
 240   ONCE_REWRITE_TAC[ARITH_RULE `a * b * c = b * a * c`];
 241   REWRITE_TAC[REAL_DIV_DISTRIB_2];
 242   ONCE_REWRITE_TAC [REAL_ARITH `&1 = &1 * &1`];
 243   MATCH_MP_TAC SEQ_MUL;
 244   CONJ_TAC;
 245   MATCH_ACCEPT_TAC LIM_NN;
 246   FIRST_ASSUM MATCH_MP_TAC;
 247   CONJ_TAC;
 248   LABEL_ALL_TAC;
 249   USE_THEN "Z-1" MP_TAC THEN ARITH_TAC;
 250   ASM_MESON_TAC[];
 251 ]);;
 252
 253 (* }}} *)
 254
 255 let mono_inc = new_definition(
 256   `mono_inc (f:num -> real) = !(m:num) n. m <= n ==> f m <= f n`);;
 257
 258 let mono_dec = new_definition(
 259   `mono_dec (f:num -> real) = !(m:num) n. m <= n ==> f n <= f m`);;
 260
 261 let mono_inc_dec = prove_by_refinement(
 262   `!f. mono f <=> mono_inc f \/ mono_dec f`,
 263 (* {{{ Proof *)
 264 [
 265   REWRITE_TAC[mono_inc;mono_dec;mono;real_ge]
 266 ]);;
 267 (* }}} *)
 268
 269 let mono_inc_pow = prove_by_refinement(
 270  `!k. mono_inc (\n. &n pow k)`,
 271 (* {{{ Proof *)
 272
 273 [
 274   REWRITE_TAC[mono_inc];
 275   INDUCT_TAC THEN REWRITE_TAC[real_pow;REAL_LE_REFL];
 276   GEN_TAC THEN GEN_TAC;
 277   DISCH_THEN (fun x -> (RULE_ASSUM_TAC (fun y -> MATCH_MP y x)) THEN ASSUME_TAC x);
 278   MATCH_MP_TAC REAL_LE_MUL2;
 279   REPEAT STRIP_TAC;
 280   MATCH_ACCEPT_TAC REAL_NUM_LE_0;
 281   ASM_REWRITE_TAC[REAL_LE];
 282   MATCH_MP_TAC REAL_POW_LE;
 283   MATCH_ACCEPT_TAC REAL_NUM_LE_0;
 284   FIRST_ASSUM MATCH_ACCEPT_TAC;
 285 ]);;
 286
 287 (* }}} *)
 288
 289 let mono_inc_pow_const = prove_by_refinement(
 290  `!k c. &0 < c ==> mono_inc (\n. c * &n pow k)`,
 291 (* {{{ Proof *)
 292
 293 [
 294   REWRITE_TAC[mono_inc];
 295   REPEAT STRIP_TAC;
 296   MATCH_MP_TAC REAL_LE_MUL2;
 297   REPEAT STRIP_TAC;
 298   ASM_MESON_TAC[REAL_LT_LE];
 299   REAL_ARITH_TAC;
 300   MATCH_MP_TAC REAL_POW_LE;
 301   MATCH_ACCEPT_TAC REAL_NUM_LE_0;
 302   ASM_MESON_TAC[mono_inc_pow;mono_inc]
 303 ]);;
 304
 305 (* }}} *)
 306
 307 (* ---------------------------------------------------------------------- *)
 308 (*  Unbounded sequences                                                   *)
 309 (* ---------------------------------------------------------------------- *)
 310
 311 let mono_unbounded_above = new_definition(
 312  `mono_unbounded_above (f:num -> real) = !c. ?N. !n. N <= n ==> c < f n`);;
 313
 314 let mono_unbounded_below = new_definition(
 315  `mono_unbounded_below (f:num -> real) = !c. ?N. !n. N <= n ==> f n < c`);;
 316
 317 let mono_unbounded_above_pos = prove_by_refinement(
 318  `mono_unbounded_above (f:num -> real) = !c. &0 <= c ==> ?N. !n. N <= n ==> c < f n`,
 319 (* {{{ Proof *)
 320 [
 321   REWRITE_TAC[mono_unbounded_above];
 322   EQ_TAC THENL [ASM_MESON_TAC[];ALL_TAC];
 323   REPEAT STRIP_TAC;
 324   POP_ASSUM (ASSUME_TAC o ISPEC `abs c`);
 325   POP_ASSUM (MP_TAC o (C MATCH_MP) (ISPEC `c:real` ABS_POS));
 326   STRIP_TAC;
 327   EXISTS_TAC `N`;
 328   GEN_TAC;
 329   DISCH_THEN (fun x -> POP_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x)));
 330   ASM_MESON_TAC[ABS_LE;REAL_LET_TRANS];
 331 ]);;
 332 (* }}} *)
 333
 334 let mono_unbounded_below_neg = prove_by_refinement(
 335  `mono_unbounded_below (f:num -> real) = !c. c <= &0 ==> ?N. !n. N <= n ==> f n < c`,
 336 (* {{{ Proof *)
 337 [
 338   REWRITE_TAC[mono_unbounded_below];
 339   EQ_TAC THENL [ASM_MESON_TAC[];ALL_TAC];
 340   REPEAT STRIP_TAC;
 341   POP_ASSUM (ASSUME_TAC o ISPEC `-- (abs c)`);
 342   POP_ASSUM (MP_TAC o (C MATCH_MP) (ISPEC `c:real` NEG_ABS));
 343   STRIP_TAC;
 344   EXISTS_TAC `N`;
 345   GEN_TAC;
 346   DISCH_THEN (fun x -> POP_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x)));
 347   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 348 ]);;
 349 (* }}} *)
 350
 351 let mua_quotient_limit = prove_by_refinement(
 352  `!k f g. &0 < k /\ (\n. f n / g n) --> k /\ mono_unbounded_above g
 353     ==> mono_unbounded_above f`,
 354 (* {{{ Proof *)
 355 [
 356   REWRITE_TAC[SEQ;mono_unbounded_above_pos;AND_IMP_THM];
 357   REPEAT GEN_TAC;
 358   STRIP_TAC;
 359   CLAIM `&0 < k / &2`;
 360   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 361   DISCH_THEN (fun x -> DISCH_THEN (fun y -> (ASSUME_TAC (MATCH_MP (ISPEC `k / &2` y) x))));
 362   POP_ASSUM (X_CHOOSE_TAC `M:num`);
 363   STRIP_TAC;
 364   X_GEN_TAC `d:real`;
 365   STRIP_TAC;
 366   CLAIM `&0 <= &2 * d / k`;
 367   MATCH_MP_TAC REAL_LE_MUL;
 368   CONJ_TAC THENL [REAL_ARITH_TAC;ALL_TAC];
 369   MATCH_MP_TAC REAL_LE_DIV;
 370   CONJ_TAC THENL [FIRST_ASSUM MATCH_ACCEPT_TAC;ASM_MESON_TAC[REAL_LT_LE]];
 371   STRIP_TAC;
 372   LABEL_ALL_TAC;
 373   MOVE_TO_FRONT "Z-2";
 374   POP_ASSUM (fun x -> USE_THEN "Z-0" (fun y -> MP_TAC (MATCH_MP x y)));
 375   DISCH_THEN (X_CHOOSE_TAC `K:num`);
 376   EXISTS_TAC `nmax M K`;
 377   REPEAT STRIP_TAC;
 378   CLAIM `M <= n /\ K <= (n:num)`;
 379   POP_ASSUM MP_TAC THEN REWRITE_TAC[nmax] THEN COND_CASES_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
 380   STRIP_TAC;
 381   RULE_ASSUM_TAC (REWRITE_RULE[GE]);
 382   FIRST_X_ASSUM (fun x -> FIRST_X_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x)));
 383   FIRST_X_ASSUM (fun x -> FIRST_X_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x)));
 384   RULE_ASSUM_TAC (REWRITE_RULE[real_div]);
 385   CASES_ON `k <= f n * inv (g n)`;
 386   MATCH_MP_TAC (prove(`d <= &2 * d /\ &2 * d < k * (g n) /\ k * (g n) <= f n ==> d < f n`,MESON_TAC !REAL_REWRITES));
 387   REPEAT STRIP_TAC;
 388   USE_THEN "Z-1" MP_TAC THEN REAL_ARITH_TAC;
 389   FIRST_ASSUM (fun x -> ASSUME_TAC (MATCH_MP (REWRITE_RULE[AND_IMP_THM] REAL_LT_LMUL) x));
 390   LABEL_ALL_TAC;
 391   POP_ASSUM (fun y -> USE_THEN "Z-6" (fun x -> ASSUME_TAC (MATCH_MP y x)));
 392   CLAIM `k * &2 * d * inv k = (k * inv k) * &2 * d`;
 393   REAL_ARITH_TAC;
 394   CLAIM `k * inv k = &1`;
 395   ASM_MESON_TAC[REAL_MUL_RINV;REAL_LT_NZ];
 396   STRIP_TAC;
 397   ASM_REWRITE_TAC[REAL_MUL_LID];
 398   ASM_MESON_TAC[];
 399   (* *)
 400   MATCH_MP_TAC REAL_LE_RCANCEL_IMP;
 401   EXISTS_TAC `inv (g n)`;
 402   REWRITE_TAC[GSYM REAL_MUL_ASSOC];
 403   CLAIM `&0 < inv (g n)`;
 404   CLAIM `&0 < inv k`;
 405   MATCH_MP_TAC REAL_LT_INV THEN FIRST_ASSUM MATCH_ACCEPT_TAC;
 406   STRIP_TAC;
 407   CLAIM `&0 < g n`;
 408   ASM_MESON_TAC !REAL_REWRITES;
 409   STRIP_TAC;
 410   ASM_MESON_TAC[REAL_LT_INV];
 411   STRIP_TAC;
 412   ASM_REWRITE_TAC[];
 413   CLAIM `g n * inv (g n) = &1`;
 414   ASM_MESON_TAC[REAL_MUL_RINV;REAL_LT_NZ;REAL_LT_INV_EQ];
 415   DISCH_THEN SUBST1_TAC;
 416   REWRITE_TAC[REAL_MUL_RID];
 417   FIRST_ASSUM MATCH_ACCEPT_TAC;
 418   (* *)
 419   RULE_ASSUM_TAC (REWRITE_RULE[REAL_NOT_LE]);
 420   CLAIM `f n * inv (g n) - k < &0`;
 421   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 422   STRIP_TAC;
 423   CLAIM `abs (f n * inv (g n) - k) = k - (f n * inv (g n))`;
 424   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 425   DISCH_THEN (RULE_ASSUM_TAC o REWRITE_RULE o list);
 426   CLAIM `k * inv(&2) < f n * inv (g n)`;
 427   LABEL_ALL_TAC;
 428   USE_THEN "Z-5" MP_TAC THEN REAL_ARITH_TAC;
 429   STRIP_TAC;
 430   CLAIM `k * g n < &2 * f n`;
 431   CLAIM `&0 < g n`;
 432   LABEL_ALL_TAC;
 433   MATCH_MP_TAC REAL_LET_TRANS;
 434   EXISTS_TAC `&2 * d * inv k`;
 435   CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC;
 436   STRIP_TAC;
 437   MATCH_MP_TAC REAL_LT_LCANCEL_IMP;
 438   EXISTS_TAC `inv(&2)`;
 439   CONJ_TAC THENL [REAL_ARITH_TAC;ALL_TAC];
 440   REWRITE_TAC[ARITH_RULE `inv(&2) * &2 = &1`;REAL_MUL_LID;REAL_MUL_ASSOC];
 441   MATCH_MP_TAC REAL_LT_LCANCEL_IMP;
 442   EXISTS_TAC `inv(g n)`;
 443   CONJ_TAC;
 444   ASM_MESON_TAC[REAL_LT_INV];
 445   ONCE_REWRITE_TAC[ARITH_RULE `a * (b * c) * d = c * b * (d * a)`];
 446   CLAIM `g n * inv (g n) = &1`;
 447   POP_ASSUM MP_TAC THEN ASM_MESON_TAC[REAL_MUL_RINV;REAL_POS_NZ];
 448   DISCH_THEN SUBST1_TAC;
 449   ASM_MESON_TAC[REAL_MUL_RID;REAL_MUL_SYM];
 450   STRIP_TAC;
 451   CLAIM `&2 * d < k * g n`;
 452   MATCH_MP_TAC REAL_LT_RCANCEL_IMP;
 453   EXISTS_TAC `inv k`;
 454   STRIP_TAC;
 455   ASM_MESON_TAC[REAL_LT_INV];
 456   MATCH_MP_TAC REAL_LTE_TRANS;
 457   EXISTS_TAC `g n`;
 458   CONJ_TAC;
 459   REWRITE_TAC[GSYM REAL_MUL_ASSOC];
 460   FIRST_ASSUM MATCH_ACCEPT_TAC;
 461   LABEL_ALL_TAC;
 462   ONCE_REWRITE_TAC[ARITH_RULE `(a * b) * c = b * (a * c)`];
 463   CLAIM `k * inv k = &1`;
 464   ASM_MESON_TAC[REAL_MUL_RINV;REAL_POS_NZ];
 465   DISCH_THEN SUBST1_TAC;
 466   REAL_ARITH_TAC;
 467   STRIP_TAC;
 468   CLAIM `&2 * d < &2 * f n`;
 469   POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 470   REAL_ARITH_TAC;
 471 ]);;
 472 (* }}} *)
 473
 474 let mua_neg = prove_by_refinement(
 475  `!f. mono_unbounded_above f = mono_unbounded_below (\n. -- (f n))`,
 476 (* {{{ Proof *)
 477
 478 [
 479   MESON_TAC[mono_unbounded_above;mono_unbounded_below;REAL_ARITH `x < y ==> --y < -- x`;REAL_ARITH `-- (-- x) = x`];
 480 ]);;
 481
 482 (* }}} *)
 483
 484 let mua_neg2 = prove_by_refinement(
 485  `!f. mono_unbounded_below f = mono_unbounded_above (\n. -- (f n))`,
 486 (* {{{ Proof *)
 487 [
 488   MESON_TAC[mono_unbounded_above;mono_unbounded_below;REAL_ARITH `x < y ==> --y < -- x`;REAL_ARITH `-- (-- x) = x`];
 489 ]);;
 490 (* }}} *)
 491
 492 let mua_quotient_limit_neg = prove_by_refinement(
 493  `!k f g. &0 < k /\ (\n. f n / g n) --> k /\ mono_unbounded_below g
 494     ==> mono_unbounded_below f`,
 495 (* {{{ Proof *)
 496
 497 [
 498   REWRITE_TAC[mua_neg2];
 499   REPEAT STRIP_TAC;
 500   MATCH_MP_TAC (mua_quotient_limit);
 501   EXISTS_TAC `k`;
 502   EXISTS_TAC `\n. -- g n`;
 503   ASM_REWRITE_TAC[];
 504   POP_ASSUM (fun x -> ALL_TAC);
 505   POP_ASSUM MP_TAC;
 506   REWRITE_TAC[SEQ];
 507   DISCH_THEN (fun x -> REPEAT STRIP_TAC THEN MP_TAC x);
 508   DISCH_THEN (MP_TAC o ISPEC `e:real`);
 509   ANTS_TAC;
 510   FIRST_ASSUM MATCH_ACCEPT_TAC;
 511   STRIP_TAC;
 512   EXISTS_TAC `N`;
 513   REPEAT STRIP_TAC;
 514   REWRITE_TAC[real_div;REAL_NEG_MUL2;REAL_INV_NEG];
 515   ASM_MESON_TAC[real_div];
 516 ]);;
 517
 518 (* }}} *)
 519
 520 (* ---------------------------------------------------------------------- *)
 521 (*  Polynomial properties                                                 *)
 522 (* ---------------------------------------------------------------------- *)
 523
 524 let normal = new_definition(
 525  `normal p <=> ((normalize p = p) /\ ~(p = []))`);;
 526
 527 let nonconstant = new_definition(
 528  `nonconstant p <=> normal p /\ (!x. ~(p = [x]))`);;
 529
 530 let NORMALIZE_SING = prove_by_refinement(
 531   `!x. (normalize [x] = [x]) <=> ~(x = &0)`,
 532 (* {{{ Proof *)
 533 [
 534   MESON_TAC[NOT_CONS_NIL;normalize];
 535 ]);;
 536 (* }}} *)
 537
 538 let NORMALIZE_PAIR = prove_by_refinement(
 539   `!x y. ~(y = &0) <=> (normalize [x; y] = [x; y])`,
 540 (* {{{ Proof *)
 541 [
 542   REWRITE_TAC[normalize;NOT_CONS_NIL];
 543   REPEAT GEN_TAC;
 544   COND_CASES_TAC;
 545   CLAIM `y = &0`;
 546   ASM_MESON_TAC !LIST_REWRITES;
 547   DISCH_THEN SUBST1_TAC;
 548   ASM_MESON_TAC !LIST_REWRITES;
 549   ASM_MESON_TAC !LIST_REWRITES;
 550 ]);;
 551 (* }}} *)
 552
 553 let POLY_NORMALIZE = prove
 554  (`!p. poly (normalize p) = poly p`,
 555 (* {{{ Proof *)
 556   LIST_INDUCT_TAC THEN REWRITE_TAC[normalize; poly] THEN
 557   ASM_CASES_TAC `h = &0` THEN ASM_REWRITE_TAC[] THEN
 558   COND_CASES_TAC THEN ASM_REWRITE_TAC[poly; FUN_EQ_THM] THEN
 559   UNDISCH_TAC `poly (normalize t) = poly t` THEN
 560   DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[poly] THEN
 561   REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID]);;
 562 (* }}} *)
 563
 564 let NORMAL_CONS = prove_by_refinement(
 565  `!h t. normal t ==> normal (CONS h t)`,
 566  (* {{{ Proof *)
 567 [
 568   REWRITE_TAC[normal;normalize];
 569   REPEAT STRIP_TAC;
 570   ASM_REWRITE_TAC[];
 571   ASM_MESON_TAC[NOT_CONS_NIL];
 572 ]);;
 573 (* }}} *)
 574
 575 let NORMAL_TAIL = prove_by_refinement(
 576  `!h t. ~(t = []) /\ normal (CONS h t) ==> normal t`,
 577 (* {{{ Proof *)
 578 [
 579   REWRITE_TAC[normal;normalize];
 580   REPEAT STRIP_TAC  THENL [ALL_TAC;ASM_MESON_TAC[]];
 581   CASES_ON `normalize t = []`;
 582   ASM_MESON_TAC[NOT_CONS_NIL;CONS_11];
 583   ASM_MESON_TAC[NOT_CONS_NIL;CONS_11];
 584 ]);;
 585 (* }}} *)
 586
 587 let NORMAL_LAST_NONZERO = prove_by_refinement(
 588  `!p. normal p ==> ~(LAST p = &0)`,
 589 (* {{{ Proof *)
 590
 591 [
 592   LIST_INDUCT_TAC;
 593   ASM_MESON_TAC[normal];
 594   CASES_ON `t = []`;
 595   ASM_REWRITE_TAC[normal;normalize;NOT_CONS_NIL;LAST];
 596   MESON_TAC[NOT_CONS_NIL];
 597   ASM_SIMP_TAC[GSYM LAST_CONS];
 598   ASM_REWRITE_TAC[LAST;NOT_CONS_NIL;];
 599   STRIP_TAC;
 600   FIRST_ASSUM MATCH_MP_TAC;
 601   MATCH_MP_TAC NORMAL_TAIL;
 602   ASM_MESON_TAC[];
 603 ]);;
 604
 605 (* }}} *)
 606
 607 let NORMAL_LENGTH = prove_by_refinement(
 608   `!p. normal p ==> 0 < LENGTH p`,
 609 (* {{{ Proof *)
 610
 611 [
 612   MESON_TAC[normal;LENGTH_0;ARITH_RULE `~(n = 0) <=> 0 < n`]
 613 ]);;
 614
 615 (* }}} *)
 616
 617 let NORMAL_LAST_LENGTH = prove_by_refinement(
 618   `!p. 0 < LENGTH p /\ ~(LAST p = &0) ==> normal p`,
 619 (* {{{ Proof *)
 620
 621 [
 622   LIST_INDUCT_TAC;
 623   MESON_TAC[LENGTH;LT_REFL];
 624   STRIP_TAC;
 625   CASES_ON `t = []`;
 626   ASM_REWRITE_TAC[normal;NORMALIZE_SING;NOT_CONS_NIL;];
 627   ASM_MESON_TAC[LAST];
 628   MATCH_MP_TAC NORMAL_CONS;
 629   FIRST_ASSUM MATCH_MP_TAC;
 630   STRIP_TAC;
 631   ASM_MESON_TAC[LENGTH_0;ARITH_RULE `~(n = 0) <=> 0 < n`];
 632   ASM_MESON_TAC[LAST_CONS];
 633 ]);;
 634
 635 (* }}} *)
 636
 637 let NORMAL_ID = prove_by_refinement(
 638  `!p. normal p <=> 0 < LENGTH p /\ ~(LAST p = &0)`,
 639 (* {{{ Proof *)
 640 [
 641   MESON_TAC[NORMAL_LAST_LENGTH;NORMAL_LENGTH;NORMAL_LAST_NONZERO];
 642 ]);;
 643 (* }}} *)
 644
 645 let LIM_POLY2 = prove_by_refinement(
 646   `!p. normal p ==> (\n. poly p (&n) / (LAST p * &n pow (degree p))) --> &1`,
 647 (* {{{ Proof *)
 648
 649 [
 650   REPEAT STRIP_TAC;
 651   REWRITE_TAC[degree];
 652   CLAIM `normalize p = p`;
 653   ASM_MESON_TAC[normal];
 654   DISCH_THEN SUBST1_TAC;
 655   MATCH_MP_TAC LIM_POLY;
 656   ASM_MESON_TAC[NORMAL_ID];
 657 ]);;
 658
 659 (* }}} *)
 660
 661 let POW_UNB = prove_by_refinement(
 662   `!k. 0 < k ==> mono_unbounded_above (\n. (&n) pow k)`,
 663 (* {{{ Proof *)
 664
 665 [
 666   REWRITE_TAC[mono_unbounded_above];
 667   REPEAT STRIP_TAC;
 668   MP_TAC (ISPEC `max (&1) c` REAL_ARCH_SIMPLE_LT);
 669   STRIP_TAC;
 670   EXISTS_TAC `n`;
 671   REPEAT STRIP_TAC;
 672   MATCH_MP_TAC REAL_LTE_TRANS;
 673   EXISTS_TAC `&n`;
 674   CONJ_TAC;
 675   MATCH_MP_TAC REAL_LET_TRANS;
 676   EXISTS_TAC `max (&1) c`;
 677   ASM_MESON_TAC[REAL_MAX_MAX];
 678   MATCH_MP_TAC REAL_LE_TRANS;
 679   EXISTS_TAC `&n'`;
 680   STRIP_TAC;
 681   ASM_MESON_TAC[REAL_LE];
 682   CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[REAL_ARITH `x = x pow 1`]));
 683   MATCH_MP_TAC REAL_POW_MONO;
 684   STRIP_TAC;
 685   MATCH_MP_TAC REAL_LE_TRANS;
 686   EXISTS_TAC `max (&1) c`;
 687   CONJ_TAC THENL [ASM_MESON_TAC[REAL_MAX_MAX];ALL_TAC];
 688   MATCH_MP_TAC REAL_LE_TRANS;
 689   EXISTS_TAC `&n`;
 690   ASM_MESON_TAC (!REAL_REWRITES @ [REAL_LE;REAL_LT_LE]);
 691   EVERY_ASSUM MP_TAC THEN ARITH_TAC;
 692 ]);;
 693
 694 (* }}} *)
 695
 696 let POW_UNB_CON = prove_by_refinement(
 697   `!k a. 0 < k /\ &0 < a ==> mono_unbounded_above (\n. a * (&n) pow k)`,
 698 (* {{{ Proof *)
 699
 700 [
 701   REWRITE_TAC[mono_unbounded_above;AND_IMP_THM;];
 702   REPEAT STRIP_TAC;
 703   LABEL_ALL_TAC;
 704   MOVE_TO_FRONT "Z-1";
 705   POP_ASSUM (fun x ->  MP_TAC (MATCH_MP POW_UNB x));
 706   REWRITE_TAC[mono_unbounded_above];
 707   DISCH_THEN (MP_TAC o ISPEC `inv a * c`);
 708   STRIP_TAC;
 709   EXISTS_TAC `N`;
 710   STRIP_TAC;
 711   DISCH_THEN (fun x -> POP_ASSUM (fun y -> ASSUME_TAC (MATCH_MP  y x)));
 712   CLAIM `inv a * a = &1`;
 713   MATCH_MP_TAC REAL_MUL_LINV;
 714   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 715   STRIP_TAC;
 716   MATCH_MP_TAC REAL_LT_LCANCEL_IMP;
 717   EXISTS_TAC `inv a`;
 718   CONJ_TAC;
 719   ASM_MESON_TAC[REAL_LT_INV];
 720   ASM_REWRITE_TAC[REAL_MUL_ASSOC;REAL_MUL_LID];
 721 ]);;
 722
 723 (* }}} *)
 724
 725 let POW_UNBB_CON = prove_by_refinement(
 726   `!k a. 0 < k /\ a < &0 ==> mono_unbounded_below (\n. a * (&n) pow k)`,
 727 (* {{{ Proof *)
 728
 729 [
 730   REWRITE_TAC[mua_neg2;ARITH_RULE `--(x * y) = -- x * y`];
 731   REPEAT STRIP_TAC;
 732   MATCH_MP_TAC POW_UNB_CON;
 733   STRIP_TAC;
 734   FIRST_ASSUM MATCH_ACCEPT_TAC;
 735   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 736 ]);;
 737
 738 (* }}} *)
 739
 740 let POLY_SING = prove_by_refinement(
 741   `!x y. poly [x] y = x`,
 742 (* {{{ Proof *)
 743 [
 744   REWRITE_TAC[poly];
 745   REAL_ARITH_TAC;
 746 ]);;
 747 (* }}} *)
 748
 749 let POLY_LAST_GT = prove_by_refinement(
 750   `!p. normal p /\ (?X. !x. X < x ==> &0 < poly p x) ==> &0 < LAST p`,
 751 (* {{{ Proof *)
 752
 753 [
 754   GEN_TAC;
 755   CASES_ON `LENGTH p = 1`;
 756   RULE_ASSUM_TAC (REWRITE_RULE[LENGTH_1]);
 757   POP_ASSUM MP_TAC THEN STRIP_TAC;
 758   ASM_REWRITE_TAC[LAST_SING;POLY_SING];
 759   REPEAT STRIP_TAC;
 760   FIRST_ASSUM MATCH_MP_TAC;
 761   EXISTS_TAC `X + &1`;
 762   REAL_ARITH_TAC;
 763   (* *)
 764   REWRITE_TAC[AND_IMP_THM;];
 765   DISCH_THEN (fun x -> MP_TAC (MATCH_MP LIM_POLY2 x) THEN ASSUME_TAC x);
 766   REPEAT STRIP_TAC;
 767   DISJ_CASES_TAC (ISPECL [`&0`;`LAST (p:real list)`] REAL_LT_TOTAL);
 768   ASM_MESON_TAC[NORMAL_ID];
 769   POP_ASSUM DISJ_CASES_TAC;
 770   FIRST_ASSUM MATCH_ACCEPT_TAC;
 771   (* save *)
 772   CLAIM `mono_unbounded_below (\n. LAST p * &n pow degree p)`;
 773   MATCH_MP_TAC POW_UNBB_CON;
 774   REWRITE_TAC[degree];
 775   CONJ_TAC THENL [ALL_TAC;FIRST_ASSUM MATCH_ACCEPT_TAC];
 776   CLAIM `normalize p = p`;
 777   ASM_MESON_TAC[normal];
 778   DISCH_THEN SUBST1_TAC;
 779   CLAIM `~(LENGTH p = 0)`;
 780   ASM_MESON_TAC[normal;LENGTH_EQ_NIL];
 781   LABEL_ALL_TAC;
 782   USE_THEN "Z-4" MP_TAC;
 783   ARITH_TAC;
 784   (* save *)
 785   STRIP_TAC;
 786   CLAIM `mono_unbounded_below (\n. poly p (&n))`;
 787   MATCH_MP_TAC mua_quotient_limit_neg;
 788   BETA_TAC;
 789   EXISTS_TAC `&1`;
 790   EXISTS_TAC `(\n. LAST p * &n pow degree p)`;
 791   REPEAT STRIP_TAC;
 792   REAL_ARITH_TAC;
 793   BETA_TAC;
 794   FIRST_ASSUM MATCH_ACCEPT_TAC;
 795   FIRST_ASSUM MATCH_ACCEPT_TAC;
 796   REWRITE_TAC[mono_unbounded_below];
 797   DISCH_THEN (MP_TAC o ISPEC `&0`);
 798   STRIP_TAC;
 799   LABEL_ALL_TAC;
 800   USE_THEN "Z-3" MP_TAC;
 801   POP_ASSUM MP_TAC;
 802   POP_ASSUM_LIST (fun x -> ALL_TAC);
 803   MP_TAC (ISPEC `X:real` REAL_ARCH_SIMPLE);
 804   STRIP_TAC;
 805   DISCH_THEN (ASSUME_TAC o ISPEC `1 + nmax N n`);
 806   DISCH_THEN (ASSUME_TAC o ISPEC `&1 + &(nmax N n)`);
 807   POP_ASSUM MP_TAC THEN ANTS_TAC;
 808   REWRITE_TAC[nmax];
 809   COND_CASES_TAC;
 810   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 811   RULE_ASSUM_TAC (REWRITE_RULE[NOT_LE;GSYM REAL_LT]);
 812   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 813   POP_ASSUM MP_TAC THEN ANTS_TAC;
 814   REWRITE_TAC[nmax];
 815   ARITH_TAC;
 816   ASM_MESON_TAC[ARITH_RULE `~(x < y /\ y < x)`;GSYM REAL_OF_NUM_ADD];
 817 ]);;
 818
 819 (* }}} *)
 820
 821 let POLY_LAST_LT = prove_by_refinement(
 822   `!p. normal p /\ (?X. !x. X < x ==> poly p x < &0) ==> LAST p < &0`,
 823 (* {{{ Proof *)
 824
 825 [
 826   GEN_TAC;
 827   CASES_ON `LENGTH p = 1`;
 828   RULE_ASSUM_TAC (REWRITE_RULE[LENGTH_1]);
 829   POP_ASSUM MP_TAC THEN STRIP_TAC;
 830   ASM_REWRITE_TAC[LAST_SING;POLY_SING];
 831   REPEAT STRIP_TAC;
 832   FIRST_ASSUM MATCH_MP_TAC;
 833   EXISTS_TAC `X + &1`;
 834   REAL_ARITH_TAC;
 835   (* *)
 836   REWRITE_TAC[AND_IMP_THM;];
 837   DISCH_THEN (fun x -> MP_TAC (MATCH_MP LIM_POLY2 x) THEN ASSUME_TAC x);
 838   REPEAT STRIP_TAC;
 839   DISJ_CASES_TAC (ISPECL [`&0`;`LAST (p:real list)`] REAL_LT_TOTAL);
 840   ASM_MESON_TAC[NORMAL_ID];
 841   POP_ASSUM DISJ_CASES_TAC THENL [ALL_TAC;FIRST_ASSUM MATCH_ACCEPT_TAC];
 842   (* save *)
 843   CLAIM `mono_unbounded_above (\n. LAST p * &n pow degree p)`;
 844   MATCH_MP_TAC POW_UNB_CON;
 845   REWRITE_TAC[degree];
 846   CONJ_TAC THENL [ALL_TAC;FIRST_ASSUM MATCH_ACCEPT_TAC];
 847   CLAIM `normalize p = p`;
 848   ASM_MESON_TAC[normal];
 849   DISCH_THEN SUBST1_TAC;
 850   CLAIM `~(LENGTH p = 0)`;
 851   ASM_MESON_TAC[normal;LENGTH_EQ_NIL];
 852   LABEL_ALL_TAC;
 853   USE_THEN "Z-4" MP_TAC;
 854   ARITH_TAC;
 855   (* save *)
 856   STRIP_TAC;
 857   CLAIM `mono_unbounded_above (\n. poly p (&n))`;
 858   MATCH_MP_TAC mua_quotient_limit;
 859   BETA_TAC;
 860   EXISTS_TAC `&1`;
 861   EXISTS_TAC `(\n. LAST p * &n pow degree p)`;
 862   REPEAT STRIP_TAC;
 863   REAL_ARITH_TAC;
 864   BETA_TAC;
 865   FIRST_ASSUM MATCH_ACCEPT_TAC;
 866   FIRST_ASSUM MATCH_ACCEPT_TAC;
 867   REWRITE_TAC[mono_unbounded_above];
 868   DISCH_THEN (MP_TAC o ISPEC `&0`);
 869   STRIP_TAC;
 870   LABEL_ALL_TAC;
 871   USE_THEN "Z-3" MP_TAC;
 872   POP_ASSUM MP_TAC;
 873   POP_ASSUM_LIST (fun x -> ALL_TAC);
 874   MP_TAC (ISPEC `X:real` REAL_ARCH_SIMPLE);
 875   STRIP_TAC;
 876   DISCH_THEN (ASSUME_TAC o ISPEC `1 + nmax N n`);
 877   DISCH_THEN (ASSUME_TAC o ISPEC `&1 + &(nmax N n)`);
 878   POP_ASSUM MP_TAC THEN ANTS_TAC;
 879   REWRITE_TAC[nmax];
 880   COND_CASES_TAC;
 881   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 882   RULE_ASSUM_TAC (REWRITE_RULE[NOT_LE;GSYM REAL_LT]);
 883   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
 884   POP_ASSUM MP_TAC THEN ANTS_TAC;
 885   REWRITE_TAC[nmax];
 886   ARITH_TAC;
 887   ASM_MESON_TAC[ARITH_RULE `~(x < y /\ y < x)`;GSYM REAL_OF_NUM_ADD];
 888 ]);;
 889
 890 (* }}} *)
 891
 892 let NORMALIZE_LENGTH_MONO = prove_by_refinement(
 893   `!l. LENGTH (normalize l) <= LENGTH l`,
 894 (* {{{ Proof *)
 895 [
 896   LIST_INDUCT_TAC;
 897   MESON_TAC[normalize;LE_REFL];
 898   REWRITE_TAC[LENGTH;normalize];
 899   REPEAT COND_CASES_TAC THEN REWRITE_TAC[LENGTH] THEN EVERY_ASSUM MP_TAC THEN ARITH_TAC;
 900 ]);;
 901 (* }}} *)
 902
 903 let DEGREE_SING = prove_by_refinement(
 904   `!x. (degree [x] = 0)`,
 905 (* {{{ Proof *)
 906 [
 907   REWRITE_TAC[degree];
 908   STRIP_TAC;
 909   CASES_ON `x = &0`;
 910   ASM_REWRITE_TAC[normalize;LENGTH];
 911   ARITH_TAC;
 912   CLAIM `normalize [x] = [x]`;
 913   ASM_MESON_TAC[NORMALIZE_SING];
 914   DISCH_THEN SUBST1_TAC;
 915   REWRITE_TAC[LENGTH];
 916   ARITH_TAC;
 917 ]);;
 918 (* }}} *)
 919
 920 let DEGREE_CONS = prove_by_refinement(
 921   `!h t. normal t ==> (degree (CONS h t) = 1 + degree t)`,
 922 (* {{{ Proof *)
 923
 924 [
 925   REPEAT STRIP_TAC;
 926   CLAIM `normal (CONS h t)`;
 927   ASM_MESON_TAC[NORMAL_CONS];
 928   REWRITE_TAC[normal;degree];
 929   STRIP_TAC;
 930   ASM_REWRITE_TAC[];
 931   RULE_ASSUM_TAC (REWRITE_RULE[normal]);
 932   CLAIM `~(LENGTH t = 0)`;
 933   ASM_MESON_TAC[LENGTH_0];
 934   STRIP_TAC;
 935   ASM_REWRITE_TAC[LENGTH];
 936   POP_ASSUM MP_TAC THEN ARITH_TAC;
 937 ]);;
 938
 939 (* }}} *)
 940
 941 (* ---------------------------------------------------------------------- *)
 942 (*  Now the derivative                                                    *)
 943 (* ---------------------------------------------------------------------- *)
 944
 945 let PDA_LENGTH = prove_by_refinement(
 946  `!p n. ~(p = []) ==> (LENGTH(poly_diff_aux n p) = LENGTH p)`,
 947 (* {{{ Proof *)
 948 [
 949   LIST_INDUCT_TAC;
 950   REWRITE_TAC[];
 951   GEN_TAC THEN DISCH_THEN IGNORE;
 952   REWRITE_TAC[LENGTH;poly_diff_aux;];
 953   CASES_ON `t = []`;
 954   ASM_REWRITE_TAC[LENGTH;poly_diff_aux;];
 955   ASM_MESON_TAC[];
 956 ]);;
 957 (* }}} *)
 958
 959 let POLY_DIFF_LENGTH = prove_by_refinement(
 960  `!p. LENGTH (poly_diff p) = PRE (LENGTH p)`,
 961 (* {{{ Proof *)
 962 [
 963   LIST_INDUCT_TAC;
 964   REWRITE_TAC[poly_diff;LENGTH;PRE];
 965   CASES_ON `t = []`;
 966   ASM_REWRITE_TAC[LENGTH;PRE];
 967   REWRITE_TAC[poly_diff;NOT_CONS_NIL;TL;PRE;poly_diff_aux;LENGTH;];
 968   REWRITE_TAC[poly_diff;TL;LENGTH;PRE;NOT_CONS_NIL;];
 969   MATCH_MP_TAC PDA_LENGTH;
 970   FIRST_ASSUM MATCH_ACCEPT_TAC;
 971 ]);;
 972 (* }}} *)
 973
 974 let POLY_DIFF_SING = prove_by_refinement(
 975  `!p h. (poly_diff p = [h]) <=> ?x. p = [x; h]`,
 976 (* {{{ Proof *)
 977 [
 978   REPEAT STRIP_TAC;
 979   DISJ_CASES_TAC (ISPEC `LENGTH (p:real list)` (ARITH_RULE `!n. (n = 0) \/ (n = 1) \/ (n = 2) \/ 2 < n`));
 980   ASM_MESON_TAC[poly_diff;LENGTH_0;NOT_CONS_NIL;];
 981   POP_ASSUM DISJ_CASES_TAC;
 982   RULE_ASSUM_TAC (REWRITE_RULE[LENGTH_1]);
 983   POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM SUBST1_TAC;
 984   REWRITE_TAC[poly_diff;NOT_CONS_NIL;TL;poly_diff_aux;];
 985   ASM_MESON_TAC !LIST_REWRITES;
 986   POP_ASSUM DISJ_CASES_TAC;
 987   RULE_ASSUM_TAC (MATCH_EQ_MP LENGTH_PAIR);
 988   POP_ASSUM MP_TAC THEN STRIP_TAC;
 989   ASM_REWRITE_TAC[poly_diff;NOT_CONS_NIL;TL;poly_diff_aux;REAL_MUL_LID;];
 990   ASM_MESON_TAC[CONS_11];
 991   EQ_TAC;
 992   STRIP_TAC;
 993   POP_ASSUM (ASSUME_TAC o (AP_TERM `LENGTH:((real) list) -> num`));
 994   RULE_ASSUM_TAC(REWRITE_RULE[LENGTH]);
 995   CLAIM `PRE (LENGTH p) = 1`;
 996   ASM_MESON_TAC[POLY_DIFF_LENGTH;ARITH_RULE `SUC 0 = 1`];
 997   STRIP_TAC;
 998   CLAIM `LENGTH p = 2`;
 999   POP_ASSUM MP_TAC THEN ARITH_TAC;
1000   ASM_MESON_TAC[LT_REFL];
1001   REPEAT STRIP_TAC;
1002   ASM_REWRITE_TAC[];
1003   REWRITE_TAC[poly_diff;NOT_CONS_NIL;TL;poly_diff_aux;REAL_MUL_LID;];
1004 ]);;
1005 (* }}} *)
1006
1007 let lem = prove_by_refinement(
1008   `!p n. ~(p = []) ==> (LAST (poly_diff_aux n p) = LAST p * &(PRE(LENGTH p) + n))`,
1009 (* {{{ Proof *)
1010
1011 [
1012   LIST_INDUCT_TAC;
1013   REWRITE_TAC[];
1014   REPEAT STRIP_TAC;
1015   POP_ASSUM IGNORE;
1016   REWRITE_TAC[LENGTH;poly_diff_aux;];
1017   CASES_ON `t = []`;
1018   ASM_REWRITE_TAC[poly_diff_aux;LAST;LENGTH;GSYM REAL_OF_NUM_ADD];
1019   CLAIM `((SUC 0) - 1) + n = n`;
1020   ARITH_TAC;
1021   DISCH_THEN SUBST1_TAC;
1022   REWRITE_TAC[PRE];
1023   REAL_ARITH_TAC;
1024   POP_ASSUM (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x)) THEN ASSUME_TAC x);
1025   STRIP_TAC;
1026   ASM_REWRITE_TAC[];
1027   LIST_SIMP_TAC;
1028   ASM_REWRITE_TAC[];
1029   COND_CASES_TAC;
1030   REWRITE_TAC[PRE];
1031   ASM_MESON_TAC[PDA_LENGTH;LENGTH;LENGTH_0];
1032   REWRITE_TAC[PRE];
1033   MATCH_EQ_MP_TAC (GSYM REAL_EQ_MUL_LCANCEL);
1034   DISJ2_TAC;
1035   AP_TERM_TAC;
1036   CLAIM `~(LENGTH t = 0)`;
1037   ASM_MESON_TAC[LENGTH_0];
1038   ARITH_TAC;
1039 ]);;
1040
1041 (* }}} *)
1042
1043 let NONCONSTANT_LENGTH = prove_by_refinement(
1044   `!p. nonconstant p ==> 1 < LENGTH p`,
1045 (* {{{ Proof *)
1046
1047 [
1048   REWRITE_TAC[nonconstant;normal];
1049   ASM_MESON_TAC[LENGTH_0;LENGTH_1;ARITH_RULE `(x = 0) \/ (x = 1) \/ 1 < x`];
1050 ]);;
1051
1052 (* }}} *)
1053
1054 let NONCONSTANT_DIFF_NIL = prove_by_refinement(
1055   `!p. nonconstant p ==> ~(poly_diff p = [])`,
1056 (* {{{ Proof *)
1057 [
1058   REPEAT STRIP_TAC;
1059   CLAIM `1 < LENGTH p`;
1060   ASM_MESON_TAC[NONCONSTANT_LENGTH];
1061   STRIP_TAC;
1062   CLAIM `0 < LENGTH (poly_diff p)`;
1063   REWRITE_TAC[POLY_DIFF_LENGTH];
1064   POP_ASSUM MP_TAC THEN ARITH_TAC;
1065   ASM_REWRITE_TAC[LENGTH];
1066   ARITH_TAC;
1067 ]);;
1068 (* }}} *)
1069
1070 let NONCONSTANT_DEGREE = prove_by_refinement(
1071   `!p. nonconstant p ==> 0 < degree p`,
1072 (* {{{ Proof *)
1073 [
1074   GEN_TAC;
1075   DISCH_THEN (fun x -> ASSUME_TAC x THEN MP_TAC x);
1076   REWRITE_TAC[nonconstant;degree];
1077   REPEAT STRIP_TAC;
1078   CLAIM `normalize p = p`;
1079   ASM_MESON_TAC[normal];
1080   STRIP_TAC;
1081   ASM_REWRITE_TAC[];
1082   CLAIM `1 < LENGTH p`;
1083   ASM_MESON_TAC[NONCONSTANT_LENGTH];
1084   ARITH_TAC;
1085 ]);;
1086 (* }}} *)
1087
1088 let POLY_DIFF_LAST_LEM = prove_by_refinement(
1089   `!p. nonconstant p ==> (LAST (poly_diff p) = LAST p * &(degree p))`,
1090 (* {{{ Proof *)
1091 [
1092   REWRITE_TAC[nonconstant;poly_diff;];
1093   REPEAT STRIP_TAC;
1094   COND_CASES_TAC;
1095   ASM_MESON_TAC[normal];
1096   CLAIM `~(TL p = [])`;
1097   ASM_MESON_TAC[TL;NOT_CONS_NIL;list_CASES;TL_NIL];
1098   DISCH_THEN (fun x -> MP_TAC (MATCH_MP lem x) THEN ASSUME_TAC x);
1099   DISCH_THEN (ASSUME_TAC o ISPEC `1`);
1100   ASM_REWRITE_TAC[];
1101   CLAIM `LAST (TL p) = LAST p`;
1102   ASM_MESON_TAC[LAST_TL];
1103   DISCH_THEN SUBST1_TAC;
1104   REWRITE_TAC[degree];
1105   CLAIM `normalize p = p`;
1106   ASM_MESON_TAC[normal];
1107   DISCH_THEN SUBST1_TAC;
1108   MATCH_EQ_MP_TAC (GSYM REAL_EQ_MUL_LCANCEL);
1109   DISJ2_TAC;
1110   AP_TERM_TAC;
1111   ASM_SIMP_TAC[LENGTH_TL];
1112   CLAIM `~(LENGTH p = 0)`;
1113   ASM_MESON_TAC[LENGTH_0];
1114   CLAIM `~(LENGTH p = 1)`;
1115   ASM_MESON_TAC[LENGTH_1];
1116   ARITH_TAC;
1117 ]);;
1118 (* }}} *)
1119
1120 let NONCONSTANT_DIFF_0 = prove_by_refinement(
1121   `!p. nonconstant p ==> ~(poly_diff p = [&0])`,
1122 (* {{{ Proof *)
1123
1124 [
1125   STRIP_TAC;
1126   DISCH_THEN (fun x -> MP_TAC x THEN ASSUME_TAC x);
1127   REWRITE_TAC[nonconstant];
1128   REPEAT STRIP_TAC;
1129   CLAIM `~(p = [])`;
1130   ASM_MESON_TAC[normal];
1131   DISCH_THEN (fun x -> RULE_ASSUM_TAC (REWRITE_RULE[x]) THEN ASSUME_TAC x);
1132   CLAIM `~(LAST p = &0)`;
1133   MATCH_MP_TAC NORMAL_LAST_NONZERO;
1134   FIRST_ASSUM MATCH_ACCEPT_TAC;
1135   STRIP_TAC;
1136   CLAIM `LAST p * &(degree p) = &0`;
1137   ASM_SIMP_TAC[GSYM POLY_DIFF_LAST_LEM];
1138   REWRITE_TAC[LAST];
1139   STRIP_TAC;
1140   CLAIM `(LAST p = &0) \/ (&(degree p) = &0)`;
1141   ASM_MESON_TAC[REAL_ENTIRE];
1142   STRIP_TAC;
1143   ASM_MESON_TAC[];
1144   CLAIM `?h t. p = CONS h t`;
1145   ASM_MESON_TAC[list_CASES];
1146   STRIP_TAC;
1147   CLAIM `normal t`;
1148   ASM_MESON_TAC[NORMAL_TAIL];
1149   STRIP_TAC;
1150   FIRST_ASSUM (MP_TAC o (MATCH_MP (ISPECL [`h:real`;`t:real list`] DEGREE_CONS)));
1151   STRIP_TAC;
1152   CLAIM `degree p = 0`;
1153   ASM_MESON_TAC [REAL_OF_NUM_EQ];
1154   ASM_REWRITE_TAC[];
1155   ARITH_TAC;
1156 ]);;
1157
1158 (* }}} *)
1159
1160 let POLY_DIFF_LAST_LT = prove_by_refinement(
1161  `!p. nonconstant p ==> (LAST (poly_diff p) < &0 <=> LAST p < &0)`,
1162 (* {{{ Proof *)
1163 [
1164   REPEAT STRIP_TAC;
1165   ASM_SIMP_TAC[POLY_DIFF_LAST_LEM];
1166   CLAIM `&0 <= &(degree p)`;
1167   REAL_ARITH_TAC;
1168   STRIP_TAC;
1169   EQ_TAC;
1170   ASM_MESON_TAC([REAL_MUL_LT] @ !REAL_REWRITES);
1171   STRIP_TAC;
1172   CLAIM `0 < degree p`;
1173   ASM_MESON_TAC[NONCONSTANT_DEGREE];
1174   STRIP_TAC;
1175   CLAIM `&0 < &(degree p)`;
1176   REAL_SIMP_TAC;
1177   FIRST_ASSUM MATCH_ACCEPT_TAC;
1178   STRIP_TAC;
1179   MATCH_EQ_MP_TAC (GSYM REAL_MUL_LT);
1180   ASM_REWRITE_TAC[];
1181 ]);;
1182 (* }}} *)
1183
1184 let POLY_DIFF_LAST_GT = prove_by_refinement(
1185  `!p. nonconstant p ==> (&0 < LAST (poly_diff p) <=> &0 < LAST p)`,
1186 (* {{{ Proof *)
1187 [
1188   REPEAT STRIP_TAC;
1189   ASM_SIMP_TAC[POLY_DIFF_LAST_LEM];
1190   CLAIM `&0 < &(degree p)`;
1191   ASM_MESON_TAC[NONCONSTANT_DEGREE;REAL_OF_NUM_LT];
1192   STRIP_TAC;
1193   EQ_TAC;
1194   REWRITE_TAC[REAL_MUL_GT];
1195   STRIP_TAC;
1196   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1197   STRIP_TAC;
1198   ONCE_REWRITE_TAC [ARITH_RULE `&0 = &0 * &0`];
1199   MATCH_MP_TAC REAL_LT_MUL2;
1200   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1201 ]);;
1202 (* }}} *)
1203
1204 let NONCONSTANT_DIFF_NORMAL = prove_by_refinement(
1205   `!p. nonconstant p ==> normal (poly_diff p)`,
1206 (* {{{ Proof *)
1207 [
1208   GEN_TAC;
1209   DISCH_THEN (fun x ->  ASSUME_TAC x THEN MP_TAC x);
1210   REWRITE_TAC[nonconstant];
1211   REPEAT STRIP_TAC;
1212   MATCH_MP_TAC NORMAL_LAST_LENGTH;
1213   STRIP_TAC;
1214   CLAIM `1 < LENGTH p`;
1215   ASM_MESON_TAC[NONCONSTANT_LENGTH];
1216   STRIP_TAC;
1217   CLAIM `LENGTH (poly_diff p) = PRE (LENGTH p)`;
1218   ASM_MESON_TAC[POLY_DIFF_LENGTH];
1219   POP_ASSUM MP_TAC THEN ARITH_TAC;
1220   STRIP_TAC;
1221   CASES_ON `LAST p < &0`;
1222   CLAIM `LAST (poly_diff p) < &0`;
1223   ASM_MESON_TAC[POLY_DIFF_LAST_LT];
1224   ASM_REWRITE_TAC[];
1225   REAL_ARITH_TAC;
1226   REWRITE_ASSUMS !REAL_REWRITES;
1227   REWRITE_ASSUMS[REAL_LE_LT];
1228   POP_ASSUM MP_TAC THEN STRIP_TAC;
1229   CLAIM `&0 < LAST (poly_diff p)`;
1230   ASM_MESON_TAC[POLY_DIFF_LAST_GT];
1231   ASM_REWRITE_TAC[];
1232   REAL_ARITH_TAC;
1233   ASM_MESON_TAC[NORMAL_ID];
1234 ]);;
1235 (* }}} *)
1236
1237 let PDIFF_POS_LAST = prove_by_refinement(
1238   `!p. nonconstant p /\ (?X. !x. X < x ==> &0 < poly (poly_diff p) x) ==> &0 < LAST p`,
1239 (* {{{ Proof *)
1240 [
1241   REPEAT STRIP_TAC;
1242   CLAIM `&0 < LAST (poly_diff p)`;
1243   MATCH_MP_TAC POLY_LAST_GT;
1244   ASM_SIMP_TAC[NONCONSTANT_DIFF_NORMAL];
1245   ASM_MESON_TAC[];
1246   STRIP_TAC;
1247   ASM_SIMP_TAC[GSYM POLY_DIFF_LAST_GT];
1248 ]);;
1249 (* }}} *)
1250
1251 let LAST_UNB = prove_by_refinement(
1252  `!p. nonconstant p /\ &0 < LAST p ==> mono_unbounded_above (\n. poly p (&n))`,
1253 (* {{{ Proof *)
1254 [
1255   REPEAT STRIP_TAC;
1256   MATCH_MP_TAC mua_quotient_limit;
1257   EXISTS_TAC `&1`;
1258   EXISTS_TAC `(\n. (LAST p) * (&n) pow (degree p))`;
1259   BETA_TAC;
1260   STRIP_TAC;
1261   REAL_ARITH_TAC;
1262   STRIP_TAC;
1263   MATCH_MP_TAC LIM_POLY2;
1264   ASM_MESON_TAC[nonconstant];
1265   MATCH_MP_TAC POW_UNB_CON;
1266   ASM_REWRITE_TAC[];
1267   ASM_MESON_TAC[NONCONSTANT_DEGREE];
1268 ]);;
1269 (* }}} *)
1270
1271 (* ---------------------------------------------------------------------- *)
1272 (*  Finally, the positive theorems                                        *)
1273 (* ---------------------------------------------------------------------- *)
1274
1275
1276 let POLY_DIFF_UP_RIGHT = prove_by_refinement(
1277  `nonconstant p /\ (?X. !x. X < x ==> &0 < poly (poly_diff p) x) ==>
1278    (?Y. !y. Y < y ==> &0 < poly p y)`,
1279 (* {{{ Proof *)
1280 [
1281   REPEAT STRIP_TAC;
1282   CLAIM `mono_unbounded_above (\n. poly p (&n))`;
1283   MATCH_MP_TAC LAST_UNB;
1284   ASM_MESON_TAC[PDIFF_POS_LAST];
1285   REWRITE_TAC[mono_unbounded_above];
1286   DISCH_THEN (MP_TAC o (ISPEC `&0`));
1287   STRIP_TAC;
1288   CLAIM `?K. max X (&N) < &K`;
1289   ASM_MESON_TAC[REAL_ARCH_SIMPLE_LT];
1290   STRIP_TAC;
1291   EXISTS_TAC `&K`;
1292   REPEAT STRIP_TAC;
1293   CCONTR_TAC;
1294   REWRITE_ASSUMS[REAL_NOT_LT];
1295   CLAIM `&N < y /\ X < y`;
1296   ASM_MESON_TAC([REAL_MAX_MAX] @ !REAL_REWRITES);
1297   REPEAT STRIP_TAC;
1298   MP_TAC (ISPECL [`p:real list`;`&K`;`y:real`] POLY_MVT);
1299   ANTS_TAC;
1300   FIRST_ASSUM MATCH_ACCEPT_TAC;
1301   STRIP_TAC;
1302   CLAIM `poly p y - poly p (&K) <= &0`;
1303   MATCH_MP_TAC (REAL_ARITH `x <= &0 /\ &0 < y ==> x - y <= &0`);
1304   ASM_REWRITE_TAC[];
1305   FIRST_ASSUM MATCH_MP_TAC;
1306   CLAIM `&N < &K`;
1307   ASM_MESON_TAC [REAL_MAX_MAX;REAL_LET_TRANS];
1308   STRIP_TAC;
1309   CLAIM `N:num < K`;
1310   ASM_MESON_TAC [REAL_OF_NUM_LT];
1311   ARITH_TAC;
1312   STRIP_TAC;
1313   CLAIM `&0 < y - &K`;
1314   LABEL_ALL_TAC;
1315   USE_THEN "Z-7" MP_TAC;
1316   REAL_ARITH_TAC;
1317   STRIP_TAC;
1318   CLAIM `&0 < poly (poly_diff p) x`;
1319   FIRST_ASSUM MATCH_MP_TAC;
1320   ASM_MESON_TAC[REAL_MAX_MAX;REAL_LET_TRANS;REAL_LT_TRANS];
1321   STRIP_TAC;
1322   CLAIM `&0 < (y - &K) * poly (poly_diff p) x`;
1323   ONCE_REWRITE_TAC [ARITH_RULE `&0 = &0 * &0`];
1324   MATCH_MP_TAC REAL_LT_MUL2 THEN REPEAT STRIP_TAC THEN TRY REAL_ARITH_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC;
1325   STRIP_TAC;
1326   REAL_SOLVE_TAC;
1327 ]);;
1328 (* }}} *)
1329
1330 let PDIFF_NEG_LAST = prove_by_refinement(
1331   `!p. nonconstant p /\ (?X. !x. X < x ==> poly (poly_diff p) x < &0) ==> LAST p < &0`,
1332 (* {{{ Proof *)
1333 [
1334   REPEAT STRIP_TAC;
1335   CLAIM `LAST (poly_diff p) < &0`;
1336   MATCH_MP_TAC POLY_LAST_LT;
1337   ASM_SIMP_TAC[NONCONSTANT_DIFF_NORMAL];
1338   ASM_MESON_TAC[];
1339   STRIP_TAC;
1340   ASM_SIMP_TAC[GSYM POLY_DIFF_LAST_LT];
1341 ]);;
1342 (* }}} *)
1343
1344 let LAST_UNB_NEG = prove_by_refinement(
1345  `!p. nonconstant p /\ LAST p < &0 ==> mono_unbounded_below (\n. poly p (&n))`,
1346 (* {{{ Proof *)
1347 [
1348   REPEAT STRIP_TAC;
1349   MATCH_MP_TAC mua_quotient_limit_neg;
1350   EXISTS_TAC `&1`;
1351   EXISTS_TAC `(\n. (LAST p) * (&n) pow (degree p))`;
1352   BETA_TAC;
1353   STRIP_TAC;
1354   REAL_ARITH_TAC;
1355   STRIP_TAC;
1356   MATCH_MP_TAC LIM_POLY2;
1357   ASM_MESON_TAC[nonconstant];
1358   MATCH_MP_TAC POW_UNBB_CON;
1359   ASM_REWRITE_TAC[];
1360   ASM_MESON_TAC[NONCONSTANT_DEGREE];
1361 ]);;
1362 (* }}} *)
1363
1364 let POLY_DIFF_DOWN_RIGHT = prove_by_refinement(
1365  `nonconstant p /\ (?X. !x. X < x ==> poly (poly_diff p) x < &0) ==>
1366    (?Y. !y. Y < y ==> poly p y < &0)`,
1367 (* {{{ Proof *)
1368 [
1369   REPEAT STRIP_TAC;
1370   CLAIM `mono_unbounded_below (\n. poly p (&n))`;
1371   MATCH_MP_TAC LAST_UNB_NEG;
1372   ASM_MESON_TAC[PDIFF_NEG_LAST];
1373   REWRITE_TAC[mono_unbounded_below];
1374   DISCH_THEN (MP_TAC o (ISPEC `&0`));
1375   STRIP_TAC;
1376   CLAIM `?K. max X (&N) < &K`;
1377   ASM_MESON_TAC[REAL_ARCH_SIMPLE_LT];
1378   STRIP_TAC;
1379   EXISTS_TAC `&K`;
1380   REPEAT STRIP_TAC;
1381   CCONTR_TAC;
1382   REWRITE_ASSUMS[REAL_NOT_LT];
1383   CLAIM `&N < y /\ X < y`;
1384   ASM_MESON_TAC([REAL_MAX_MAX] @ !REAL_REWRITES);
1385   REPEAT STRIP_TAC;
1386   MP_TAC (ISPECL [`p:real list`;`&K`;`y:real`] POLY_MVT);
1387   ANTS_TAC;
1388   FIRST_ASSUM MATCH_ACCEPT_TAC;
1389   STRIP_TAC;
1390   CLAIM `&0 <= poly p y - poly p (&K)`;
1391   MATCH_MP_TAC (REAL_ARITH `&0 <= x /\ y < &0 ==> &0 <= x - y`);
1392   ASM_REWRITE_TAC[];
1393   FIRST_ASSUM MATCH_MP_TAC;
1394   CLAIM `&N < &K`;
1395   ASM_MESON_TAC (!REAL_REWRITES @ !NUM_REWRITES);
1396   STRIP_TAC;
1397   CLAIM `N:num < K`;
1398   ASM_MESON_TAC [REAL_OF_NUM_LT];
1399   ARITH_TAC;
1400   STRIP_TAC;
1401   CLAIM `&0 < y - &K`;
1402   LABEL_ALL_TAC;
1403   USE_THEN "Z-7" MP_TAC;
1404   REAL_ARITH_TAC;
1405   STRIP_TAC;
1406   CLAIM `poly (poly_diff p) x < &0`;
1407   FIRST_ASSUM MATCH_MP_TAC;
1408   REAL_SOLVE_TAC;
1409   STRIP_TAC;
1410   CLAIM `(y - &K) * poly (poly_diff p) x < &0`;
1411   ASM_MESON_TAC[REAL_MUL_LT];
1412   REPEAT STRIP_TAC;
1413   REAL_SOLVE_TAC;
1414 ]);;
1415 (* }}} *)
1416
1417 (* ---------------------------------------------------------------------- *)
1418 (*  Now the negative ones                                                 *)
1419 (* ---------------------------------------------------------------------- *)
1420
1421 let UNB_LEFT_EVEN = prove_by_refinement(
1422  `!k. 0 < k /\ EVEN k ==> mono_unbounded_above (\n. (-- &n) pow k)`,
1423 (* {{{ Proof *)
1424 [
1425   REPEAT STRIP_TAC;
1426   ASM_REWRITE_TAC[REAL_POW_NEG];
1427   MATCH_MP_TAC POW_UNB;
1428   FIRST_ASSUM MATCH_ACCEPT_TAC;
1429 ]);;
1430 (* }}} *)
1431
1432 let UNB_LEFT_ODD = prove_by_refinement(
1433  `!k. 0 < k /\ ODD k ==> mono_unbounded_below (\n. (-- &n) pow k)`,
1434 (* {{{ Proof *)
1435 [
1436   REPEAT STRIP_TAC;
1437   REWRITE_ASSUMS[GSYM NOT_EVEN];
1438   ASM_REWRITE_TAC[REAL_POW_NEG];
1439   MATCH_EQ_MP_TAC mua_neg;
1440   MATCH_MP_TAC POW_UNB;
1441   FIRST_ASSUM MATCH_ACCEPT_TAC;
1442 ]);;
1443 (* }}} *)
1444
1445 let EVEN_CONS = prove_by_refinement(
1446   `!t h. ODD (LENGTH (CONS h t)) = EVEN (LENGTH t)`,
1447 (* {{{ Proof *)
1448 [
1449   LIST_INDUCT_TAC THEN
1450   ASM_MESON_TAC[LENGTH_SING;LENGTH;EVEN;ODD;ONE];
1451 ]);;
1452 (* }}} *)
1453
1454 let ODD_CONS = prove_by_refinement(
1455   `!t h. EVEN (LENGTH (CONS h t)) = ODD (LENGTH t)`,
1456 (* {{{ Proof *)
1457 [
1458   LIST_INDUCT_TAC THEN
1459   ASM_MESON_TAC[LENGTH_SING;LENGTH;EVEN;ODD;ONE];
1460 ]);;
1461 (* }}} *)
1462
1463 let MUA_DIV_CONST = prove_by_refinement(
1464   `!a b p. mono_unbounded_above (\n. p n) ==> (\n. a / (b + p n)) --> &0`,
1465 (* {{{ Proof *)
1466
1467 [
1468   REWRITE_TAC[mono_unbounded_above;SEQ];
1469   REPEAT STRIP_TAC;
1470   REAL_SIMP_TAC;
1471   CASES_ON `a = &0`;
1472   ASM_REWRITE_TAC[real_div;REAL_MUL_LZERO;ABS_0];
1473   ABBREV_TAC `k = (max (&1) (abs a / e - b))`;
1474   FIRST_ASSUM (MP_TAC o (ISPEC `k:real`));
1475   STRIP_TAC;
1476   EXISTS_TAC `N`;
1477   REPEAT STRIP_TAC;
1478   REWRITE_ASSUMS (!REAL_REWRITES @ !NUM_REWRITES);
1479   POP_ASSUM (fun x -> POP_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x)));
1480   REWRITE_TAC[REAL_ABS_DIV];
1481   MATCH_MP_TAC REAL_LTE_TRANS;
1482   EXISTS_TAC `abs a / (b + k)`;
1483   STRIP_TAC;
1484   MATCH_MP_TAC REAL_DIV_DENOM_LT;
1485   REPEAT STRIP_TAC;
1486   ASM_MESON_TAC[REAL_ABS_NZ];
1487   LABEL_ALL_TAC;
1488   CLAIM `(abs a / e - b) <= k`;
1489   ASM_MESON_TAC[REAL_MAX_MAX];
1490   STRIP_TAC;
1491   CLAIM `&0 < abs a / e`;
1492   REWRITE_TAC[real_div];
1493   MATCH_MP_TAC REAL_LT_MUL;
1494   ASM_MESON_TAC[REAL_INV_POS;REAL_ABS_NZ];
1495   STRIP_TAC;
1496   POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1497   CLAIM `-- b < p n`;
1498   MATCH_MP_TAC REAL_LET_TRANS;
1499   EXISTS_TAC `k`;
1500   ASM_REWRITE_TAC[];
1501   CLAIM `(abs a / e - b) <= k`;
1502   ASM_MESON_TAC[REAL_MAX_MAX];
1503   STRIP_TAC;
1504   CLAIM `&0 < abs a / e`;
1505   REWRITE_TAC[real_div];
1506   MATCH_MP_TAC REAL_LT_MUL;
1507   ASM_MESON_TAC[REAL_INV_POS;REAL_ABS_NZ];
1508   STRIP_TAC;
1509   POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1510   STRIP_TAC;
1511   CLAIM `abs (b + p n) = b + p n`;
1512   MATCH_EQ_MP_TAC REAL_ABS_REFL;
1513   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1514   DISCH_THEN SUBST1_TAC;
1515   POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
1516   CLAIM `(abs a / e - b) <= k`;
1517   ASM_MESON_TAC[REAL_MAX_MAX];
1518   STRIP_TAC;
1519   CLAIM `&0 < abs a / e`;
1520   REWRITE_TAC[real_div];
1521   MATCH_MP_TAC REAL_LT_MUL;
1522   ASM_MESON_TAC[REAL_INV_POS;REAL_ABS_NZ];
1523   STRIP_TAC;
1524   LABEL_ALL_TAC;
1525   CLAIM `abs a / e <= b + k`;
1526   USE_THEN "Z-1" MP_TAC THEN REAL_ARITH_TAC;
1527   STRIP_TAC;
1528   CASES_ON `&1 <= abs a / e - b`;
1529   CLAIM `k = abs a / e - b`;
1530   USE_THEN "Z-3" (SUBST1_TAC o GSYM);
1531   ASM_REWRITE_TAC[real_max];
1532   ASM_MESON_TAC[real_max];
1533   DISCH_THEN SUBST1_TAC;
1534   REWRITE_TAC[ARITH_RULE `b + a - b = a`];
1535   REWRITE_TAC[real_div;];
1536   REAL_SIMP_TAC;
1537   REWRITE_TAC[REAL_MUL_ASSOC];
1538   CLAIM `~(abs a = &0)`;
1539   ASM_MESON_TAC[REAL_ABS_NZ;REAL_LT_LE];
1540   STRIP_TAC;
1541   ASM_SIMP_TAC[REAL_MUL_RINV];
1542   REAL_SIMP_TAC;
1543   (* save *)
1544   REWRITE_ASSUMS !REAL_REWRITES;
1545   CLAIM `k = &1`;
1546   ASM_MESON_TAC([real_max] @ !REAL_REWRITES);
1547   STRIP_TAC;
1548   CLAIM `&0 < b + k`;
1549   MATCH_MP_TAC REAL_LTE_TRANS;
1550   EXISTS_TAC `abs a / e`;
1551   ASM_MESON_TAC[];
1552   STRIP_TAC;
1553   MATCH_MP_TAC REAL_LE_RCANCEL_IMP;
1554   EXISTS_TAC `b + k`;
1555   ASM_REWRITE_TAC[];
1556   REWRITE_TAC[real_div];
1557   REWRITE_TAC[GSYM REAL_MUL_ASSOC];
1558   CLAIM `inv (b + &1) * (b + &1) = &1`;
1559   LABEL_ALL_TAC;
1560   POP_ASSUM MP_TAC;
1561   ASM_REWRITE_TAC[];
1562   STRIP_TAC;
1563   ASM_MESON_TAC[REAL_MUL_LINV;REAL_LT_LE];
1564   DISCH_THEN SUBST1_TAC;
1565   REWRITE_TAC[REAL_MUL_RID];
1566   MATCH_MP_TAC REAL_LE_LCANCEL_IMP;
1567   EXISTS_TAC `inv e`;
1568   REPEAT STRIP_TAC;
1569   USE_THEN "Z-5" MP_TAC;
1570   MESON_TAC[REAL_INV_POS;REAL_LT_LE];
1571   REWRITE_TAC[REAL_MUL_ASSOC];
1572   CLAIM `~(e = &0)`;
1573   ASM_MESON_TAC[REAL_INV_NZ;REAL_LT_LE];
1574   STRIP_TAC;
1575   ASM_SIMP_TAC[REAL_MUL_LINV];
1576   REAL_SIMP_TAC;
1577   ASM_MESON_TAC[real_div;REAL_MUL_SYM]
1578 ]);;
1579
1580 (* }}} *)
1581
1582 let SEQ_0_NEG = prove_by_refinement(
1583   `!p. (\n. p n) --> &0 <=> (\n. -- p n) --> &0`,
1584 (* {{{ Proof *)
1585 [
1586   REWRITE_TAC[SEQ];
1587   GEN_TAC THEN EQ_TAC;
1588   REPEAT STRIP_TAC;
1589   LABEL_ALL_TAC;
1590   USE_THEN "Z-0" (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x)));
1591   STRIP_TAC;
1592   EXISTS_TAC `N`;
1593   REPEAT STRIP_TAC;
1594   POP_ASSUM  (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x)));
1595   REAL_SIMP_TAC;
1596   STRIP_TAC;
1597   ASM_MESON_TAC[REAL_ABS_NEG];
1598   REPEAT STRIP_TAC;
1599   LABEL_ALL_TAC;
1600   USE_THEN "Z-0" (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x)));
1601   STRIP_TAC;
1602   EXISTS_TAC `N`;
1603   REPEAT STRIP_TAC;
1604   POP_ASSUM  (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x)));
1605   REAL_SIMP_TAC;
1606   STRIP_TAC;
1607   ASM_MESON_TAC[REAL_ABS_NEG];
1608 ]);;
1609 (* }}} *)
1610
1611 let lem = prove_by_refinement(
1612   `!x y z. --(x / (y + z)) = x / (-- y + -- z)`,
1613 (* {{{ Proof *)
1614 [
1615   REPEAT STRIP_TAC;
1616   REWRITE_TAC[real_div];
1617   REWRITE_TAC[ARITH_RULE `--(x * y) = x * -- y`];
1618   REWRITE_TAC[ARITH_RULE `-- y + -- z = --(y + z)`];
1619   REWRITE_TAC[REAL_INV_NEG];
1620 ]);;
1621 (* }}} *)
1622
1623 let MUB_DIV_CONST = prove_by_refinement(
1624   `!a b p. mono_unbounded_below (\n. p n) ==> (\n. a / (b + p n)) --> &0`,
1625 (* {{{ Proof *)
1626 [
1627   REWRITE_TAC[mua_neg2];
1628   REPEAT STRIP_TAC;
1629   ONCE_REWRITE_TAC[SEQ_0_NEG];
1630   REWRITE_TAC[lem];
1631   MATCH_MP_TAC MUA_DIV_CONST;
1632   FIRST_ASSUM MATCH_ACCEPT_TAC;
1633 ]);;
1634 (* }}} *)
1635
1636 let mono_unbounded = new_definition(
1637   `mono_unbounded p <=> mono_unbounded_above p \/ mono_unbounded_below p`);;
1638
1639 let MU_DIV_CONST = prove_by_refinement(
1640   `!a b p. mono_unbounded p ==> (\n. a / (b + p n)) --> &0`,
1641 (* {{{ Proof *)
1642 [
1643   REWRITE_TAC[mono_unbounded];
1644   REPEAT STRIP_TAC;
1645   MATCH_MP_TAC MUA_DIV_CONST;
1646   REWRITE_TAC[ETA_AX];
1647   POP_ASSUM MATCH_ACCEPT_TAC;
1648   MATCH_MP_TAC MUB_DIV_CONST;
1649   REWRITE_TAC[ETA_AX];
1650   POP_ASSUM MATCH_ACCEPT_TAC;
1651 ]);;
1652 (* }}} *)
1653
1654 let MUA_MUA = prove_by_refinement(
1655   `!p q. mono_unbounded_above (\n. p n) /\ mono_unbounded_above (\n. q n) ==>
1656            mono_unbounded_above (\n. p n * q n)`,
1657 (* {{{ Proof *)
1658 [
1659   REWRITE_TAC[mono_unbounded_above_pos];
1660   REPEAT STRIP_TAC;
1661   CLAIM `&0 <= max c (&1)`;
1662   REWRITE_TAC[real_max];
1663   COND_CASES_TAC;
1664   REAL_ARITH_TAC;
1665   ASM_REWRITE_TAC[];
1666   DISCH_THEN (fun y -> POP_ASSUM (fun x -> RULE_ASSUM_TAC (C MATCH_MP y) THEN ASSUME_TAC x));
1667   EVERY_ASSUM MP_TAC THEN REPEAT STRIP_TAC;
1668   EXISTS_TAC `nmax N N'`;
1669   REPEAT STRIP_TAC;
1670   MATCH_MP_TAC REAL_LET_TRANS;
1671   EXISTS_TAC `max c (&1)`;
1672   ASM_REWRITE_TAC[REAL_MAX_MAX];
1673   MATCH_MP_TAC REAL_LET_TRANS;
1674   EXISTS_TAC `max c (&1) * max c (&1)`;
1675   REPEAT STRIP_TAC;
1676   CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [GSYM REAL_MUL_RID]));
1677   MATCH_MP_TAC REAL_LE_MUL2;
1678   REPEAT STRIP_TAC;
1679   REAL_SOLVE_TAC;
1680   REAL_SIMP_TAC;
1681   REAL_ARITH_TAC;
1682   REAL_SOLVE_TAC;
1683   MATCH_MP_TAC REAL_LT_MUL2;
1684   REPEAT STRIP_TAC;
1685   REAL_SOLVE_TAC;
1686   CLAIM `N <= n /\ N' <= (n:num)`;
1687   POP_ASSUM MP_TAC;
1688   REWRITE_TAC[nmax];
1689   COND_CASES_TAC;
1690   REPEAT STRIP_TAC;
1691   POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
1692   FIRST_ASSUM MATCH_ACCEPT_TAC;
1693   REPEAT STRIP_TAC;
1694   FIRST_ASSUM MATCH_ACCEPT_TAC;
1695   POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
1696   REPEAT STRIP_TAC;
1697   FIRST_ASSUM MATCH_MP_TAC;
1698   FIRST_ASSUM MATCH_ACCEPT_TAC;
1699   REAL_SOLVE_TAC;
1700   FIRST_ASSUM MATCH_MP_TAC;
1701   POP_ASSUM MP_TAC THEN REWRITE_TAC[nmax] THEN ARITH_TAC;
1702 ]);;
1703 (* }}} *)
1704
1705 let MUA_MUB = prove_by_refinement(
1706   `!p q. mono_unbounded_above (\n. p n) /\ mono_unbounded_below (\n. q n) ==>
1707            mono_unbounded_below (\n. p n * q n)`,
1708 (* {{{ Proof *)
1709 [
1710   REWRITE_TAC[mua_neg2];
1711   REWRITE_TAC[ARITH_RULE `--(x * y) = x * -- y`];
1712   REPEAT STRIP_TAC;
1713   MATCH_MP_TAC MUA_MUA;
1714   ASM_REWRITE_TAC[];
1715 ]);;
1716 (* }}} *)
1717
1718 let MUB_MUA = prove_by_refinement(
1719   `!p q. mono_unbounded_below (\n. p n) /\ mono_unbounded_above (\n. q n) ==>
1720            mono_unbounded_below (\n. p n * q n)`,
1721 (* {{{ Proof *)
1722 [
1723   REWRITE_TAC[mua_neg2];
1724   REWRITE_TAC[ARITH_RULE `--(x * y) = -- x * y`];
1725   REPEAT STRIP_TAC;
1726   MATCH_MP_TAC MUA_MUA;
1727   ASM_REWRITE_TAC[];
1728 ]);;
1729 (* }}} *)
1730
1731 let MUB_MUB = prove_by_refinement(
1732   `!p q. mono_unbounded_below (\n. p n) /\ mono_unbounded_below (\n. q n) ==>
1733            mono_unbounded_above (\n. p n * q n)`,
1734 (* {{{ Proof *)
1735 [
1736   REWRITE_TAC[mua_neg2];
1737   ONCE_REWRITE_TAC[ARITH_RULE `(x * y) = -- x * -- y`];
1738   REPEAT STRIP_TAC;
1739   MATCH_MP_TAC MUA_MUA;
1740   ASM_REWRITE_TAC[];
1741 ]);;
1742 (* }}} *)
1743
1744 let MU_PROD = prove_by_refinement(
1745   `!p q. mono_unbounded (\n. p n) /\ mono_unbounded (\n. q n) ==> mono_unbounded (\n. p n * q n)`,
1746 (* {{{ Proof *)
1747 [
1748   REWRITE_TAC[mono_unbounded];
1749   ASM_MESON_TAC[MUA_MUA;MUA_MUB;MUB_MUA;MUB_MUB];
1750 ]);;
1751 (* }}} *)
1752
1753 let mub_quotient_limit = prove_by_refinement(
1754  `!k f g. &0 < k /\ (\n. f n / g n) --> k /\ mono_unbounded_below g
1755     ==> mono_unbounded_below f`,
1756 (* {{{ Proof *)
1757 [
1758   REWRITE_TAC[mua_neg2];
1759   REPEAT STRIP_TAC;
1760   MATCH_MP_TAC mua_quotient_limit;
1761   EXISTS_TAC `k`;
1762   EXISTS_TAC `\n. -- g n`;
1763   REPEAT STRIP_TAC;
1764   FIRST_ASSUM MATCH_ACCEPT_TAC;
1765   BETA_TAC;
1766   REWRITE_TAC[REAL_NEG_DIV];
1767   FIRST_ASSUM MATCH_ACCEPT_TAC;
1768   FIRST_ASSUM MATCH_ACCEPT_TAC;
1769 ]);;
1770 (* }}} *)
1771
1772 let POLY_UB = prove_by_refinement(
1773   `!p. nonconstant p ==> mono_unbounded (\n. poly p (&n))`,
1774 (* {{{ Proof *)
1775
1776 [
1777   GEN_TAC;
1778   DISCH_THEN (fun x -> ASSUME_TAC x THEN MP_TAC x);
1779   REWRITE_TAC[nonconstant];
1780   REPEAT STRIP_TAC;
1781   FIRST_ASSUM (fun x -> ASSUME_TAC (MATCH_MP LIM_POLY2 x));
1782   CASES_ON `LAST p < &0`;
1783   REWRITE_TAC[mono_unbounded];
1784   DISJ2_TAC;
1785   MATCH_MP_TAC mub_quotient_limit;
1786   EXISTS_TAC `&1`;
1787   EXISTS_TAC `(\n. LAST p * &n pow degree p)`;
1788   REPEAT STRIP_TAC;
1789   REAL_ARITH_TAC;
1790   BETA_TAC;
1791   MATCH_MP_TAC LIM_POLY2;
1792   FIRST_ASSUM MATCH_ACCEPT_TAC;
1793   MATCH_MP_TAC POW_UNBB_CON;
1794   ASM_REWRITE_TAC[];
1795   MATCH_MP_TAC NONCONSTANT_DEGREE;
1796   FIRST_ASSUM MATCH_ACCEPT_TAC;
1797   REWRITE_ASSUMS !REAL_REWRITES;
1798   REWRITE_ASSUMS[REAL_LE_LT];
1799   POP_ASSUM MP_TAC THEN STRIP_TAC;
1800   (* save *)
1801   REWRITE_TAC[mono_unbounded];
1802   DISJ1_TAC;
1803   MATCH_MP_TAC mua_quotient_limit;
1804   EXISTS_TAC `&1`;
1805   EXISTS_TAC `(\n. LAST p * &n pow degree p)`;
1806   REPEAT STRIP_TAC;
1807   REAL_ARITH_TAC;
1808   BETA_TAC;
1809   MATCH_MP_TAC LIM_POLY2;
1810   FIRST_ASSUM MATCH_ACCEPT_TAC;
1811   MATCH_MP_TAC POW_UNB_CON;
1812   ASM_REWRITE_TAC[];
1813   MATCH_MP_TAC NONCONSTANT_DEGREE;
1814   FIRST_ASSUM MATCH_ACCEPT_TAC;
1815   ASM_MESON_TAC[NORMAL_LAST_NONZERO];
1816 ]);;
1817
1818 (* }}} *)
1819
1820 (* ---------------------------------------------------------------------- *)
1821 (*  A polynomial applied to a negative argument                           *)
1822 (* ---------------------------------------------------------------------- *)
1823
1824 let pneg_aux = new_recursive_definition list_RECURSION
1825  `(pneg_aux n [] = []) /\
1826   (pneg_aux n (CONS h t) = CONS (--(&1) pow n * h) (pneg_aux (SUC n) t))`;;
1827
1828 let pneg = new_recursive_definition list_RECURSION
1829  `(pneg [] = []) /\
1830   (pneg (CONS h t) = pneg_aux 0 (CONS h t))`;;
1831
1832 let POLY_PNEG_AUX_SUC = prove_by_refinement(
1833   `!t n. pneg_aux (SUC (SUC n)) t = pneg_aux n t`,
1834 (* {{{ Proof *)
1835 [
1836   LIST_INDUCT_TAC;
1837   STRIP_TAC;
1838   REWRITE_TAC[pneg_aux];
1839   REWRITE_TAC[pneg_aux;pow];
1840   REAL_SIMP_TAC;
1841   STRIP_TAC;
1842   AP_TERM_TAC;
1843   ASM_MESON_TAC[];
1844 ]);;
1845 (* }}} *)
1846
1847 let POLY_NEG_NEG = prove_by_refinement(
1848  `!p. poly_neg (poly_neg p) = p`,
1849 (* {{{ Proof *)
1850 [
1851   LIST_INDUCT_TAC;
1852   REWRITE_TAC[poly_neg;poly_cmul];
1853   REWRITE_TAC[poly_neg;poly_cmul];
1854   REAL_SIMP_TAC;
1855   AP_TERM_TAC;
1856   ASM_MESON_TAC[poly_neg;poly_cmul];
1857 ]);;
1858 (* }}} *)
1859
1860 let POLY_PNEG_NEG = prove_by_refinement(
1861  `!p n. poly_neg (pneg_aux (SUC n) p) = pneg_aux n p`,
1862 (* {{{ Proof *)
1863 [
1864   LIST_INDUCT_TAC;
1865   ASM_REWRITE_TAC[pneg_aux;poly_neg;poly_cmul];
1866   REWRITE_TAC[pneg_aux];
1867   REPEAT STRIP_TAC;
1868   REWRITE_TAC[POLY_PNEG_AUX_SUC];
1869   REWRITE_TAC[poly_neg;poly_cmul];
1870   REAL_SIMP_TAC;
1871   AP_TERM_TAC;
1872   REWRITE_TAC[GSYM poly_neg];
1873   CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[GSYM POLY_NEG_NEG]));
1874   POP_ASSUM (ONCE_REWRITE_TAC o list);
1875   REWRITE_TAC[];
1876 ]);;
1877 (* }}} *)
1878
1879 let POLY_PNEG_AUX = prove_by_refinement(
1880  `!k p n. EVEN n ==> (poly p (-- k) = poly (pneg_aux n p) k)`,
1881 (* {{{ Proof *)
1882 [
1883   STRIP_TAC;
1884   LIST_INDUCT_TAC;
1885   REPEAT STRIP_TAC;
1886   REWRITE_TAC[pneg_aux;poly];
1887   REPEAT STRIP_TAC;
1888   POP_ASSUM (fun x -> RULE_ASSUM_TAC (fun y -> MATCH_MP y x) THEN ASSUME_TAC x);
1889   REWRITE_TAC[poly;pneg_aux];
1890   REAL_SIMP_TAC;
1891   ASM_REWRITE_TAC[];
1892   REAL_SIMP_TAC;
1893   CLAIM `-- &1 pow n = &1`;
1894   REWRITE_TAC[REAL_POW_NEG];
1895   ASM_REWRITE_TAC[];
1896   REAL_SIMP_TAC;
1897   DISCH_THEN SUBST1_TAC;
1898   REAL_SIMP_TAC;
1899   AP_TERM_TAC;
1900   CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[GSYM POLY_PNEG_NEG]));
1901   REWRITE_TAC[POLY_NEG];
1902   REAL_SIMP_TAC;
1903 ]);;
1904 (* }}} *)
1905
1906 let POLY_PNEG = prove_by_refinement(
1907  `!p x. poly p (-- x) = poly (pneg p) x`,
1908 (* {{{ Proof *)
1909 [
1910   LIST_INDUCT_TAC;
1911   REWRITE_TAC[pneg;poly];
1912   REWRITE_TAC[pneg;poly];
1913   REPEAT STRIP_TAC;
1914   CLAIM `poly (pneg_aux 0 (CONS h t)) x = poly (CONS h t) (--x)`;
1915   ASM_MESON_TAC[POLY_PNEG_AUX;EVEN];
1916   DISCH_THEN SUBST1_TAC;
1917   REWRITE_TAC[poly];
1918 ]);;
1919 (* }}} *)
1920
1921 let DEGREE_0 = prove_by_refinement(
1922  `degree [] = 0 `,
1923 (* {{{ Proof *)
1924 [
1925   REWRITE_TAC[degree];
1926   REWRITE_TAC[normalize;LENGTH];
1927   ARITH_TAC;
1928 ]);;
1929 (* }}} *)
1930
1931 let EVEN_ODD = prove_by_refinement(
1932  `!x. EVEN (SUC x) = ODD x`,
1933 (* {{{ Proof *)
1934 [
1935   REWRITE_TAC[EVEN;NOT_EVEN];
1936 ]);;
1937 (* }}} *)
1938
1939 let ODD_EVEN = prove_by_refinement(
1940  `!x. ODD (SUC x) = EVEN x`,
1941 (* {{{ Proof *)
1942 [
1943   REWRITE_TAC[ODD;NOT_ODD];
1944 ]);;
1945 (* }}} *)
1946
1947 let PNEG_CONS = prove_by_refinement(
1948  `!p. pneg (CONS h t) = CONS h (neg (pneg t))`,
1949 (* {{{ Proof *)
1950 [
1951   REWRITE_TAC[pneg;pneg_aux];
1952   REAL_SIMP_TAC;
1953   ONCE_REWRITE_TAC[GSYM POLY_PNEG_NEG];
1954   REWRITE_TAC[POLY_PNEG_AUX_SUC];
1955   CASES_ON `t = []`;
1956   ASM_REWRITE_TAC[pneg;pneg_aux;];
1957   REWRITE_ASSUMS !LIST_REWRITES;
1958   POP_ASSUM MP_TAC THEN STRIP_TAC;
1959   ASM_REWRITE_TAC[];
1960   REWRITE_TAC[GSYM pneg];
1961 ]);;
1962 (* }}} *)
1963
1964 let PNEG_NIL = prove_by_refinement(
1965  `!p. (pneg p = []) <=> (p = [])`,
1966 (* {{{ Proof *)
1967 [
1968   LIST_INDUCT_TAC THEN
1969   MESON_TAC[pneg;NOT_CONS_NIL;pneg_aux];
1970 ]);;
1971 (* }}} *)
1972
1973 let PNEG_AUX_NIL = prove_by_refinement(
1974  `!p n. (pneg_aux n p = []) <=> (p = [])`,
1975 (* {{{ Proof *)
1976 [
1977   LIST_INDUCT_TAC THEN
1978   MESON_TAC[pneg;NOT_CONS_NIL;pneg_aux];
1979 ]);;
1980 (* }}} *)
1981
1982 let POLY_CMUL_NIL = prove_by_refinement(
1983  `!p. (c ## p = []) <=> (p = [])`,
1984 (* {{{ Proof *)
1985 [
1986   LIST_INDUCT_TAC THEN
1987   MESON_TAC[poly_cmul;NOT_CONS_NIL;pneg_aux];
1988 ]);;
1989 (* }}} *)
1990
1991 let POLY_NEG_NIL = prove_by_refinement(
1992  `!p. (poly_neg p = []) <=> (p = [])`,
1993 (* {{{ Proof *)
1994 [
1995   LIST_INDUCT_TAC THEN
1996   MESON_TAC[poly_neg;poly_cmul;NOT_CONS_NIL];
1997 ]);;
1998 (* }}} *)
1999
2000 let NEG_LAST = prove_by_refinement(
2001  `!p. ~(p = []) ==> (LAST (neg p) = -- LAST p)`,
2002 (* {{{ Proof *)
2003 [
2004   LIST_INDUCT_TAC;
2005   REWRITE_TAC[];
2006   DISCH_THEN IGNORE;
2007   CASES_ON `t = []`;
2008   ASM_REWRITE_TAC[poly_neg;poly_cmul;LAST;];
2009   REAL_ARITH_TAC;
2010   POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
2011   ASM_SIMP_TAC[LAST_CONS;poly_neg;poly_cmul;];
2012   CLAIM `~(-- &1 ## t = [])`;
2013   ASM_MESON_TAC[POLY_CMUL_NIL];
2014   STRIP_TAC;
2015   ASM_SIMP_TAC[LAST_CONS];
2016   ASM_MESON_TAC[poly_neg;];
2017 ]);;
2018 (* }}} *)
2019
2020 let POLY_PNEG_LAST = prove_by_refinement(
2021  `!p. normal p ==>
2022       (EVEN (degree p) ==> (LAST p = LAST (pneg p))) /\
2023       (ODD (degree p) ==> (LAST p = -- LAST (pneg p)))`,
2024 (* {{{ Proof *)
2025 [
2026   LIST_INDUCT_TAC;
2027   REWRITE_TAC[normal];
2028   STRIP_TAC;
2029   CASES_ON `t = []`;
2030   ASM_REWRITE_TAC[LAST;pneg;pneg_aux];
2031   REAL_SIMP_TAC;
2032   ASM_MESON_TAC[DEGREE_SING;EVEN;NOT_EVEN];
2033   CLAIM `normal t`;
2034   MATCH_MP_TAC NORMAL_TAIL;
2035   ASM_MESON_TAC[];
2036   DISCH_THEN (fun x -> RULE_ASSUM_TAC (REWRITE_RULE [x]) THEN ASSUME_TAC x);
2037   STRIP_TAC;
2038   STRIP_TAC;
2039   CLAIM `ODD (degree t)`;
2040   MATCH_EQ_MP_TAC EVEN_ODD;
2041   ASM_MESON_TAC[DEGREE_CONS;ADD1;ADD_SYM];
2042   DISCH_THEN (fun x -> RULE_ASSUM_TAC (REWRITE_RULE [x]) THEN ASSUME_TAC x);
2043   ASM_SIMP_TAC[LAST_CONS];
2044   REWRITE_TAC[PNEG_CONS];
2045   CLAIM `~(neg (pneg t) = [])`;
2046   ASM_MESON_TAC[POLY_NEG_NIL;PNEG_NIL];
2047   STRIP_TAC;
2048   ASM_SIMP_TAC[LAST_CONS];
2049   ASM_MESON_TAC[NEG_LAST;PNEG_NIL];
2050   CLAIM `normal t`;
2051   MATCH_MP_TAC NORMAL_TAIL;
2052   ASM_MESON_TAC[];
2053   REPEAT STRIP_TAC;
2054   CLAIM `EVEN (degree t)`;
2055   MATCH_EQ_MP_TAC ODD_EVEN;
2056   ASM_MESON_TAC[DEGREE_CONS;ADD1;ADD_SYM];
2057   DISCH_THEN (fun x -> RULE_ASSUM_TAC (REWRITE_RULE [x]) THEN ASSUME_TAC x);
2058   ASM_SIMP_TAC[LAST_CONS];
2059   REWRITE_TAC[PNEG_CONS];
2060   CLAIM `~(neg (pneg t) = [])`;
2061   ASM_MESON_TAC[POLY_NEG_NIL;PNEG_NIL];
2062   STRIP_TAC;
2063   ASM_SIMP_TAC[LAST_CONS];
2064   ASM_SIMP_TAC[NEG_LAST;PNEG_NIL];
2065   REAL_SIMP_TAC;
2066 ]);;
2067 (* }}} *)
2068
2069 let PNEG_AUX_LENGTH = prove_by_refinement(
2070  `!p n. LENGTH (pneg_aux n p) = LENGTH p`,
2071 (* {{{ Proof *)
2072 [
2073   LIST_INDUCT_TAC;
2074   REWRITE_TAC[LENGTH;pneg;pneg_aux;];
2075   REWRITE_TAC[LENGTH;pneg;pneg_aux;];
2076   ASM_MESON_TAC[];
2077 ]);;
2078 (* }}} *)
2079
2080 let PNEG_LENGTH = prove_by_refinement(
2081  `!p. LENGTH (pneg p) = LENGTH p`,
2082 (* {{{ Proof *)
2083 [
2084   LIST_INDUCT_TAC;
2085   REWRITE_TAC[LENGTH;pneg;pneg_aux;];
2086   REWRITE_TAC[LENGTH;pneg;pneg_aux;];
2087   ASM_MESON_TAC[PNEG_AUX_LENGTH];
2088 ]);;
2089 (* }}} *)
2090
2091 let LAST_PNEG_AUX_0 = prove_by_refinement(
2092  `!p n. ~(p = []) ==> ((LAST p = &0) <=> (LAST (pneg_aux n p) = &0))`,
2093 (* {{{ Proof *)
2094 [
2095   LIST_INDUCT_TAC;
2096   REWRITE_TAC[];
2097   STRIP_TAC;
2098   DISCH_THEN IGNORE;
2099   CASES_ON `t = []`;
2100   ASM_REWRITE_TAC[LAST;pneg;pneg_aux;];
2101   REAL_SIMP_TAC;
2102   ASM_SIMP_TAC[LAST_CONS;pneg;pneg_aux;];
2103   REAL_SIMP_TAC;
2104   EQ_TAC;
2105   DISCH_THEN SUBST1_TAC;
2106   REAL_SIMP_TAC;
2107   STRIP_TAC;
2108   MP_TAC (ISPECL[`-- &1`;`n:num`] POW_NZ);
2109   REAL_SIMP_TAC;
2110   REWRITE_TAC[ARITH_RULE `~(-- &1 = &0)`];
2111   STRIP_TAC;
2112   ASM_MESON_TAC[REAL_ENTIRE];
2113   ASM_SIMP_TAC[LAST_CONS];
2114   REWRITE_TAC[pneg_aux];
2115   CLAIM `~(pneg_aux (SUC n) t = [])`;
2116   ASM_MESON_TAC[PNEG_AUX_NIL];
2117   STRIP_TAC;
2118   ASM_SIMP_TAC[LAST_CONS];
2119   ASM_MESON_TAC[];
2120 ]);;
2121 (* }}} *)
2122
2123 let LAST_PNEG_0 = prove_by_refinement(
2124  `!p n. ~(p = []) ==> ((LAST p = &0) = (LAST (pneg p) = &0))`,
2125 (* {{{ Proof *)
2126 [
2127   LIST_INDUCT_TAC THEN MESON_TAC[LAST_PNEG_AUX_0;pneg];
2128 ]);;
2129 (* }}} *)
2130
2131 let PNEG_LAST = prove_by_refinement(
2132   `!p. ~(p = []) ==> (LAST (pneg p) = LAST p) \/ (LAST (pneg p) = -- LAST p)`,
2133 (* {{{ Proof *)
2134 [
2135   REPEAT STRIP_TAC;
2136   CASES_ON `normal p`;
2137   MP_TAC (ISPEC `p:real list` POLY_PNEG_LAST);
2138   ASM_REWRITE_TAC[];
2139   STRIP_TAC;
2140   DISJ_CASES_TAC (ISPEC `degree p` EVEN_OR_ODD);
2141   ASM_MESON_TAC[];
2142   ASM_MESON_TAC !REAL_REWRITES;
2143   REWRITE_ASSUMS[NORMAL_ID;DE_MORGAN_THM;];
2144   POP_ASSUM MP_TAC THEN STRIP_TAC;
2145   CLAIM `LENGTH p = 0`;
2146   POP_ASSUM MP_TAC THEN ARITH_TAC;
2147   ASM_MESON_TAC[LENGTH_0];
2148   ASM_REWRITE_TAC[];
2149   DISJ1_TAC;
2150   ASM_MESON_TAC[LAST_PNEG_0];
2151 ]);;
2152 (* }}} *)
2153
2154 let NORMAL_PNEG = prove_by_refinement(
2155  `!p. normal p = normal (pneg p)`,
2156 (* {{{ Proof *)
2157 [
2158   REWRITE_TAC[NORMAL_ID];
2159   REPEAT STRIP_TAC;
2160   EQ_TAC;
2161   REPEAT STRIP_TAC;
2162   ASM_MESON_TAC[PNEG_LENGTH];
2163   MP_TAC (ISPEC `p:real list` PNEG_LAST);
2164   CLAIM `~(p = [])`;
2165   ASM_MESON_TAC[LENGTH_NZ];
2166   STRIP_TAC;
2167   ASM_REWRITE_TAC[];
2168   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2169   (* save *)
2170   REPEAT STRIP_TAC;
2171   ONCE_REWRITE_TAC[GSYM PNEG_LENGTH];
2172   ASM_REWRITE_TAC[];
2173   MP_TAC (ISPEC `p:real list` PNEG_LAST);
2174   CLAIM `~(p = [])`;
2175   ASM_MESON_TAC[LENGTH_NZ;PNEG_LENGTH];
2176   STRIP_TAC;
2177   ASM_REWRITE_TAC[];
2178   EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2179 ]);;
2180 (* }}} *)
2181
2182 let PNEG_AUX_NORMALIZE_LENGTH = prove_by_refinement(
2183  `!p n. LENGTH (normalize (pneg_aux n p)) = LENGTH (normalize p)`,
2184 (* {{{ Proof *)
2185
2186 [
2187   LIST_INDUCT_TAC;
2188   REWRITE_TAC[normalize;LENGTH;pneg_aux;];
2189   REWRITE_TAC[normalize;LENGTH;pneg;pneg_aux;];
2190   STRIP_TAC;
2191   REPEAT COND_CASES_TAC THEN TRY (ASM_SIMP_TAC !LIST_REWRITES);
2192   LABEL_ALL_TAC;
2193   KEEP ["Z-2";"Z-0"];
2194   CLAIM `~(-- &1 pow n = &0)`;
2195   MATCH_MP_TAC REAL_POW_NZ;
2196   REAL_ARITH_TAC;
2197   STRIP_TAC;
2198   ASM_MESON_TAC[REAL_ENTIRE];
2199   ASM_MESON_TAC[LENGTH_0];
2200   CLAIM `~(-- &1 pow n = &0)`;
2201   MATCH_MP_TAC REAL_POW_NZ;
2202   REAL_ARITH_TAC;
2203   STRIP_TAC;
2204   ASM_MESON_TAC[REAL_ENTIRE];
2205   ASM_MESON_TAC[LENGTH_0];
2206   ASM_MESON_TAC[LENGTH_0];
2207 ]);;
2208
2209 (* }}} *)
2210
2211 let PNEG_NORMALIZE_LENGTH = prove_by_refinement(
2212  `!p n. LENGTH (normalize (pneg p)) = LENGTH (normalize p)`,
2213 (* {{{ Proof *)
2214 [
2215   LIST_INDUCT_TAC;
2216   REWRITE_TAC[pneg];
2217   ASM_MESON_TAC[PNEG_AUX_NORMALIZE_LENGTH;pneg;pneg_aux;];
2218 ]);;
2219 (* }}} *)
2220
2221 let DEGREE_PNEG = prove_by_refinement(
2222  `!p. degree (pneg p) = degree p`,
2223 (* {{{ Proof *)
2224 [
2225   REWRITE_TAC[degree];
2226   ASM_MESON_TAC[PNEG_NORMALIZE_LENGTH];
2227 ]);;
2228 (* }}} *)
2229
2230 let PNEG_SING = prove_by_refinement(
2231  `!p. (pneg p = [x]) <=> (p = [x])`,
2232 (* {{{ Proof *)
2233 [
2234   LIST_INDUCT_TAC;
2235   REWRITE_TAC[pneg;pneg_aux];
2236   EQ_TAC;
2237   REPEAT STRIP_TAC;
2238   LIST_SIMP_TAC;
2239   STRIP_TAC;
2240   REWRITE_ASSUMS[pneg;pneg_aux];
2241   POP_ASSUM MP_TAC;
2242   REAL_SIMP_TAC;
2243   LIST_SIMP_TAC;
2244   MESON_TAC[];
2245   POP_ASSUM MP_TAC;
2246   REWRITE_TAC[pneg;pneg_aux];
2247   LIST_SIMP_TAC;
2248   ASM_MESON_TAC[PNEG_AUX_NIL];
2249   REWRITE_TAC[pneg;pneg_aux];
2250   REAL_SIMP_TAC;
2251   LIST_SIMP_TAC;
2252   STRIP_TAC;
2253   ASM_MESON_TAC[pneg_aux];
2254 ]);;
2255 (* }}} *)
2256
2257 let PNEG_NONCONSTANT = prove_by_refinement(
2258  `!p. nonconstant (pneg p) = nonconstant p`,
2259 (* {{{ Proof *)
2260 [
2261   REWRITE_TAC[nonconstant];
2262   STRIP_TAC THEN EQ_TAC;
2263   REPEAT STRIP_TAC;
2264   ASM_MESON_TAC[NORMAL_PNEG];
2265   POP_ASSUM (REWRITE_ASSUMS o list);
2266   REWRITE_ASSUMS[pneg;pneg_aux];
2267   POP_ASSUM MP_TAC;
2268   REAL_SIMP_TAC;
2269   MESON_TAC[];
2270   REPEAT STRIP_TAC;
2271   ASM_MESON_TAC[NORMAL_PNEG];
2272   ASM_MESON_TAC[PNEG_SING];
2273 ]);;
2274 (* }}} *)
2275
2276 let LAST_UNBB_EVEN_NEG = prove_by_refinement(
2277  `!p. nonconstant p /\ EVEN (degree p) /\ LAST p < &0 ==>
2278        mono_unbounded_below (\n. poly p (-- &n))`,
2279 (* {{{ Proof *)
2280 [
2281   REPEAT STRIP_TAC;
2282   REWRITE_TAC[POLY_PNEG];
2283   MATCH_MP_TAC LAST_UNB_NEG;
2284   ASM_REWRITE_TAC[PNEG_NONCONSTANT];
2285   ASM_MESON_TAC[POLY_PNEG_LAST;nonconstant;];
2286 ]);;
2287 (* }}} *)
2288
2289 let POLY_PNEG_LAST2 = prove_by_refinement(
2290   `!p. normal p
2291          ==> (EVEN (degree p) ==> (LAST (pneg p) = LAST p)) /\
2292              (ODD (degree p) ==> (LAST (pneg p) = -- LAST p))`,
2293 (* {{{ Proof *)
2294 [
2295   REPEAT STRIP_TAC;
2296   ASM_MESON_TAC[POLY_PNEG_LAST];
2297   ASM_MESON_TAC([POLY_PNEG_LAST; ARITH_RULE `(--x = y) <=> (x = -- y)` ]);
2298 ]);;
2299 (* }}} *)
2300
2301 let LAST_UNB_ODD_NEG = prove_by_refinement(
2302  `!p. nonconstant p /\ ODD (degree p) /\ LAST p < &0 ==>
2303        mono_unbounded_above (\n. poly p (-- &n))`,
2304 (* {{{ Proof *)
2305 [
2306   REPEAT STRIP_TAC;
2307   REWRITE_TAC[POLY_PNEG];
2308   MATCH_MP_TAC LAST_UNB;
2309   ASM_REWRITE_TAC[PNEG_NONCONSTANT];
2310   CLAIM `LAST (pneg p) = -- LAST p`;
2311   ASM_MESON_TAC[POLY_PNEG_LAST2;nonconstant;];
2312   DISCH_THEN SUBST1_TAC;
2313   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2314 ]);;
2315 (* }}} *)
2316
2317 let LAST_UNB_EVEN_POS = prove_by_refinement(
2318  `!p. nonconstant p /\ EVEN (degree p) /\ &0 < LAST p ==>
2319        mono_unbounded_above (\n. poly p (-- &n))`,
2320 (* {{{ Proof *)
2321 [
2322   REPEAT STRIP_TAC;
2323   REWRITE_TAC[POLY_PNEG];
2324   MATCH_MP_TAC LAST_UNB;
2325   ASM_REWRITE_TAC[PNEG_NONCONSTANT];
2326   ASM_MESON_TAC[POLY_PNEG_LAST2;nonconstant;];
2327 ]);;
2328 (* }}} *)
2329
2330 let LAST_UNB_ODD_POS = prove_by_refinement(
2331  `!p. nonconstant p /\ ODD (degree p) /\ &0 < LAST p ==>
2332        mono_unbounded_below (\n. poly p (-- &n))`,
2333 (* {{{ Proof *)
2334 [
2335   REPEAT STRIP_TAC;
2336   REWRITE_TAC[POLY_PNEG];
2337   MATCH_MP_TAC LAST_UNB_NEG;
2338   ASM_REWRITE_TAC[PNEG_NONCONSTANT];
2339   CLAIM `LAST (pneg p) = -- LAST p`;
2340   ASM_MESON_TAC[POLY_PNEG_LAST2;nonconstant;];
2341   DISCH_THEN SUBST1_TAC;
2342   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2343 ]);;
2344 (* }}} *)
2345
2346 let PNEG_NORMALIZE_LENGTH = prove_by_refinement(
2347  `!p n. LENGTH (normalize (pneg p)) = LENGTH (normalize p)`,
2348 (* {{{ Proof *)
2349 [
2350   LIST_INDUCT_TAC;
2351   REWRITE_TAC[pneg];
2352   ASM_MESON_TAC[PNEG_AUX_NORMALIZE_LENGTH;pneg;pneg_aux;];
2353 ]);;
2354 (* }}} *)
2355
2356 let POLY_DIFF_AUX_NORMAL = prove_by_refinement(
2357  `!p n. ~(n = 0) ==> (normal p = normal (poly_diff_aux n p))`,
2358 (* {{{ Proof *)
2359
2360 [
2361   LIST_INDUCT_TAC;
2362   REWRITE_TAC[normal;poly_diff_aux;];
2363   REPEAT STRIP_TAC;
2364   REWRITE_TAC[poly_diff_aux];
2365   CASES_ON `t = []`;
2366   ASM_REWRITE_TAC[poly_diff_aux;];
2367   REWRITE_TAC[normal];
2368   EQ_TAC;
2369   REPEAT STRIP_TAC;
2370   REWRITE_TAC[normalize];
2371   COND_CASES_TAC;
2372   CLAIM `~(h = &0)`;
2373   ASM_MESON_TAC[normal;normalize];
2374   STRIP_TAC;
2375   ASM_MESON_TAC[REAL_ENTIRE;REAL_INJ];
2376   ASM_REWRITE_TAC[];
2377   ASM_MESON_TAC[NOT_CONS_NIL];
2378   STRIP_TAC;
2379   ASM_REWRITE_TAC[NOT_CONS_NIL];
2380   REWRITE_TAC[NORMALIZE_SING];
2381   CLAIM `~(&n * h = &0)`;
2382   ASM_MESON_TAC[normalize];
2383   ASM_MESON_TAC[REAL_ENTIRE;REAL_INJ;normalize];
2384   EQ_TAC;
2385   REPEAT STRIP_TAC;
2386   CLAIM `normal t`;
2387   ASM_MESON_TAC[NORMAL_TAIL];
2388   STRIP_TAC;
2389   MATCH_MP_TAC NORMAL_CONS;
2390   ASM_MESON_TAC[ARITH_RULE `~(SUC x = 0)`];
2391   STRIP_TAC;
2392   MATCH_MP_TAC NORMAL_CONS;
2393   MP_TAC (ARITH_RULE  `~(SUC n = 0)`);
2394   DISCH_THEN (fun x -> FIRST_ASSUM (fun y -> (MP_TAC (MATCH_MP y x))));
2395   STRIP_TAC;
2396   ASM_REWRITE_TAC[];
2397   MATCH_MP_TAC NORMAL_TAIL;
2398   EXISTS_TAC `&n * h`;
2399   ASM_REWRITE_TAC[];
2400   ASM_MESON_TAC[poly_diff_aux;NOT_CONS_NIL;list_CASES];
2401 ]);;
2402
2403 (* }}} *)
2404
2405 let POLY_DIFF_NORMAL = prove_by_refinement(
2406  `!p. nonconstant p ==> normal (poly_diff p)`,
2407 (* {{{ Proof *)
2408
2409 [
2410   LIST_INDUCT_TAC;
2411   ASM_MESON_TAC[normal;poly_diff;poly_diff_aux;POLY_DIFF_AUX_NORMAL;ARITH_RULE `~(1 = 0)`;nonconstant;];
2412   REWRITE_TAC[poly_diff;NOT_CONS_NIL;TL];
2413   REWRITE_TAC[nonconstant];
2414   STRIP_TAC;
2415   CLAIM `normal t`;
2416   MATCH_MP_TAC NORMAL_TAIL;
2417   EXISTS_TAC `h:real`;
2418   ASM_MESON_TAC[normal];
2419   STRIP_TAC;
2420   ASM_MESON_TAC[normal;poly_diff;poly_diff_aux;POLY_DIFF_AUX_NORMAL;ARITH_RULE `~(1 = 0)`];
2421 ]);;
2422
2423 (* }}} *)
2424
2425 let POLY_DIFF_AUX_NORMAL2 = prove_by_refinement(
2426  `!p n. ~(n = 0) ==> (normal (poly_diff_aux n p) <=> normal p)`,
2427 (* {{{ Proof *)
2428 [MESON_TAC[POLY_DIFF_AUX_NORMAL]]);;
2429 (* }}} *)
2430
2431 let POLY_DIFF_AUX_DEGREE = prove_by_refinement(
2432  `!p m n. ~(n = 0) /\ ~(m = 0) /\ normal p ==>
2433     (degree (poly_diff_aux n p) = degree (poly_diff_aux m p))`,
2434 (* {{{ Proof *)
2435 [
2436   LIST_INDUCT_TAC;
2437   REWRITE_TAC[poly_diff_aux];
2438   REPEAT STRIP_TAC;
2439   REWRITE_TAC[poly_diff_aux];
2440   CASES_ON `t = []`;
2441   ASM_REWRITE_TAC[poly_diff_aux;DEGREE_SING];
2442   CLAIM `normal (poly_diff_aux (SUC n) t)`;
2443   ASM_SIMP_TAC[POLY_DIFF_AUX_NORMAL2;NOT_SUC];
2444   MATCH_MP_TAC NORMAL_TAIL;
2445   ASM_REWRITE_TAC[];
2446   EXISTS_TAC `h:real`;
2447   ASM_REWRITE_TAC[];
2448   STRIP_TAC;
2449   CLAIM `normal (poly_diff_aux (SUC m) t)`;
2450   ASM_SIMP_TAC[POLY_DIFF_AUX_NORMAL2;NOT_SUC];
2451   MATCH_MP_TAC NORMAL_TAIL;
2452   ASM_REWRITE_TAC[];
2453   EXISTS_TAC `h:real`;
2454   ASM_REWRITE_TAC[];
2455   STRIP_TAC;
2456   ASM_SIMP_TAC[DEGREE_CONS];
2457   AP_TERM_TAC;
2458   FIRST_ASSUM MATCH_MP_TAC;
2459   STRIP_TAC;
2460   ARITH_TAC;
2461   STRIP_TAC;
2462   ARITH_TAC;
2463   MATCH_MP_TAC NORMAL_TAIL;
2464   ASM_MESON_TAC[];
2465 ]);;
2466 (* }}} *)
2467
2468 let poly_diff_aux_odd = prove_by_refinement(
2469  `!p n. nonconstant p ==>
2470   (EVEN (degree p) = EVEN (degree (poly_diff_aux n p))) /\
2471   (ODD (degree p) = ODD (degree (poly_diff_aux n p)))`,
2472 (* {{{ Proof *)
2473 [
2474   LIST_INDUCT_TAC;
2475   REWRITE_TAC[normal;nonconstant;];
2476   STRIP_TAC;
2477   DISCH_THEN (fun x -> ASSUME_TAC x THEN MP_TAC x);
2478   REWRITE_TAC[nonconstant];
2479   STRIP_TAC;
2480   CASES_ON `t = []`;
2481   ASM_MESON_TAC[nonconstant;normal];
2482   REWRITE_TAC[poly_diff_aux];
2483   CLAIM `normal t`;
2484   ASM_MESON_TAC[NORMAL_TAIL];
2485   STRIP_TAC;
2486   CLAIM `normal (poly_diff_aux (SUC n) t)`;
2487   ASM_MESON_TAC[nonconstant;normal;POLY_DIFF_AUX_NORMAL;NOT_SUC];
2488   STRIP_TAC;
2489   CASES_ON `?x. t = [x]`;
2490   POP_ASSUM MP_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[];
2491   CLAIM `~(x = &0)`;
2492   ASM_MESON_TAC[normal;normalize];
2493   STRIP_TAC;
2494   CLAIM `degree [h; x] = 1`;
2495   CLAIM `normalize [h; x] = [h; x]`;
2496   ASM_MESON_TAC[normal];
2497   DISCH_THEN SUBST1_TAC;
2498   CLAIM `LENGTH [h; x] = 2`;
2499   ASM_MESON_TAC[LENGTH_PAIR];
2500   STRIP_TAC;
2501   REWRITE_TAC[degree];
2502   CLAIM `normal [h; x]`;
2503   ASM_MESON_TAC[normal;normalize];
2504   DISCH_THEN (fun x -> ASSUME_TAC x THEN MP_TAC x);
2505   REWRITE_TAC[normal];
2506   STRIP_TAC;
2507   ASM_REWRITE_TAC[];
2508   ARITH_TAC;
2509   STRIP_TAC;
2510   ASM_REWRITE_TAC[poly_diff_aux;];
2511   CLAIM `~(&(SUC n) * x = &0)`;
2512   ASM_MESON_TAC[normal;normalize;REAL_ENTIRE;ARITH_RULE `~(SUC n = 0)`;REAL_INJ];
2513   STRIP_TAC;
2514   CLAIM `degree [&n * h; &(SUC n) * x] = 1`;
2515   REWRITE_TAC[degree];
2516   ASM_REWRITE_TAC[normalize;NOT_CONS_NIL;LENGTH;];
2517   ARITH_TAC;
2518   STRIP_TAC;
2519   ASM_REWRITE_TAC[];
2520   ASM_SIMP_TAC[DEGREE_CONS];
2521   CLAIM `nonconstant t`;
2522   ASM_MESON_TAC[nonconstant];
2523   STRIP_TAC;
2524   ONCE_REWRITE_TAC[ADD_SYM];
2525   REWRITE_TAC[GSYM ADD1];
2526   ASM_SIMP_TAC[EVEN;ODD];
2527   ASM_MESON_TAC[POLY_DIFF_AUX_DEGREE];
2528 ]);;
2529 (* }}} *)
2530
2531 let poly_diff_parity = prove_by_refinement(
2532  `!p n. nonconstant p ==>
2533   (EVEN (degree p) = ODD (degree (poly_diff p))) /\
2534   (ODD (degree p) = EVEN (degree (poly_diff p)))`,
2535 (* {{{ Proof *)
2536 [
2537   LIST_INDUCT_TAC;
2538   REWRITE_TAC[nonconstant;normal];
2539   STRIP_TAC;
2540   DISCH_ASS;
2541   REWRITE_TAC[nonconstant];
2542   STRIP_TAC;
2543   REWRITE_TAC[poly_diff];
2544   LIST_SIMP_TAC;
2545   CLAIM `~(1 = 0)`;
2546   ARITH_TAC;
2547   STRIP_TAC;
2548   CLAIM `normal t`;
2549   MATCH_MP_TAC NORMAL_TAIL;
2550   ASM_MESON_TAC[nonconstant;normal];
2551   STRIP_TAC;
2552   ASM_SIMP_TAC[DEGREE_CONS];
2553   CASES_ON `?x. t = [x]`;
2554   POP_ASSUM MP_TAC THEN STRIP_TAC;
2555   CLAIM `~(x = &0)`;
2556   ASM_MESON_TAC[normal;normalize];
2557   STRIP_TAC;
2558   ASM_REWRITE_TAC[poly_diff_aux;DEGREE_SING;degree;normalize;LENGTH;NOT_CONS_NIL;];
2559   CLAIM `~(&1 * x = &0)`;
2560   ASM_MESON_TAC[REAL_ENTIRE;ARITH_RULE `~(&1 = &0)`];
2561   STRIP_TAC;
2562   ASM_REWRITE_TAC[LENGTH];
2563   REWRITE_TAC[ARITH_RULE `1 + x = SUC x`];
2564   ASM_MESON_TAC[EVEN;ODD;NOT_EVEN;NOT_ODD;];
2565   CLAIM `nonconstant t`;
2566   ASM_MESON_TAC[nonconstant];
2567   DISCH_ASS;
2568   DISCH_THEN (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x);
2569   ONCE_REWRITE_TAC[ADD_SYM];
2570   REWRITE_TAC[GSYM ADD1;EVEN;ODD];
2571   CLAIM `?h' t'. t = CONS h' t'`;
2572   ASM_MESON_TAC[nonconstant;normal;list_CASES];
2573   STRIP_TAC;
2574   POP_ASSUM (fun x -> REWRITE_ASSUMS [x] THEN REWRITE_TAC[x] THEN ASSUME_TAC x);
2575   REWRITE_ASSUMS[poly_diff;NOT_CONS_NIL;TL];
2576   REWRITE_TAC[poly_diff_aux];
2577   CLAIM `normal t'`;
2578   ASM_MESON_TAC[nonconstant;NORMAL_TAIL;normal];
2579   STRIP_TAC;
2580   CLAIM `normal (poly_diff_aux (SUC 1) t')`;
2581   ASM_MESON_TAC[POLY_DIFF_AUX_NORMAL2;NOT_SUC];
2582   STRIP_TAC;
2583   ASM_SIMP_TAC[DEGREE_CONS];
2584   ONCE_REWRITE_TAC[ADD_SYM];
2585   REWRITE_TAC[GSYM ADD1;EVEN;ODD];
2586   CLAIM `normal (poly_diff_aux 1 t')`;
2587   ASM_MESON_TAC[POLY_DIFF_AUX_NORMAL2;ONE;NOT_SUC];
2588   STRIP_TAC;
2589   ASM_MESON_TAC[POLY_DIFF_AUX_DEGREE;ONE;NOT_SUC];
2590 ]);;
2591 (* }}} *)
2592
2593 let poly_diff_parity2 = prove_by_refinement(
2594  `!p n. nonconstant p ==>
2595   (ODD (degree (poly_diff p)) = EVEN (degree p)) /\
2596   (EVEN (degree (poly_diff p)) = ODD (degree p))`,
2597 (* {{{ Proof *)
2598 [MESON_TAC[poly_diff_parity]]);;
2599 (* }}} *)
2600
2601 let normal_nonconstant = prove_by_refinement(
2602  `!p. normal p /\ 0 < degree p ==> nonconstant p`,
2603 (* {{{ Proof *)
2604 [
2605   REWRITE_TAC[nonconstant];
2606   ASM_MESON_TAC[DEGREE_SING;LT_REFL];
2607 ]);;
2608 (* }}} *)
2609
2610 let nmax_le = prove_by_refinement(
2611  `!n m. n <= nmax n m /\ m <= nmax n m`,
2612 (* {{{ Proof *)
2613 [
2614   REWRITE_TAC[nmax];
2615   REPEAT STRIP_TAC;
2616   COND_CASES_TAC;
2617   ARITH_TAC;
2618   ARITH_TAC;
2619 ]);;
2620 (* }}} *)
2621
2622 let POLY_DIFF_UP_LEFT = prove_by_refinement(
2623  `!p. nonconstant p /\ (?X. !x. x < X ==> poly (poly_diff p) x < &0) ==>
2624    (?Y. !y. y < Y ==> &0 < poly p y)`,
2625 (* {{{ Proof *)
2626 [
2627   REPEAT STRIP_TAC;
2628   CLAIM `mono_unbounded_above (\n. poly p (-- &n))`;
2629   REWRITE_TAC[POLY_PNEG];
2630   DISJ_CASES_TAC (ISPEC `degree p` EVEN_OR_ODD);
2631   MATCH_MP_TAC mua_quotient_limit;
2632   EXISTS_TAC `&1`;
2633   EXISTS_TAC `(\n. LAST (pneg p) * &n pow degree (pneg p))`;
2634   REPEAT STRIP_TAC;
2635   REAL_ARITH_TAC;
2636   BETA_TAC;
2637   MATCH_MP_TAC LIM_POLY2;
2638   MATCH_EQ_MP_TAC NORMAL_PNEG;
2639   ASM_MESON_TAC[nonconstant];
2640   MATCH_MP_TAC POW_UNB_CON;
2641   STRIP_TAC;
2642   REWRITE_TAC[DEGREE_PNEG];
2643   REWRITE_TAC[degree];
2644   CLAIM `normalize p = p`;
2645   ASM_MESON_TAC[nonconstant;normal];
2646   DISCH_THEN SUBST1_TAC;
2647   CLAIM `~(LENGTH p = 0)`;
2648   ASM_MESON_TAC[nonconstant;normal;LENGTH_NZ;LENGTH_0;degree];
2649   STRIP_TAC;
2650   CLAIM `~(LENGTH p = 1)`;
2651   ASM_MESON_TAC[nonconstant;normal;LENGTH_NZ;LENGTH_1;degree];
2652   POP_ASSUM MP_TAC THEN ARITH_TAC;
2653   (* save *)
2654   CLAIM `LAST (pneg p) = LAST p`;
2655   ASM_MESON_TAC[GSYM POLY_PNEG_LAST;nonconstant;];
2656   DISCH_THEN SUBST1_TAC;
2657   ONCE_REWRITE_TAC[REAL_ARITH `x < y <=> ~(x = y) /\ ~(y < x)`];
2658   STRIP_TAC;
2659   ASM_MESON_TAC[NORMAL_ID;nonconstant];
2660   STRIP_TAC;
2661   CLAIM `ODD (degree (poly_diff p))`;
2662   ASM_SIMP_TAC[poly_diff_parity2];
2663   STRIP_TAC;
2664   CLAIM `nonconstant (poly_diff p)`;
2665   MATCH_MP_TAC normal_nonconstant;
2666   STRIP_TAC;
2667   MATCH_MP_TAC NONCONSTANT_DIFF_NORMAL;
2668   FIRST_ASSUM MATCH_ACCEPT_TAC;
2669   POP_ASSUM MP_TAC THEN ARITH_TAC;
2670   STRIP_TAC;
2671   CLAIM `mono_unbounded_above (\n. poly (poly_diff p) (-- &n))`;
2672   MATCH_MP_TAC LAST_UNB_ODD_NEG;
2673   ASM_REWRITE_TAC[];
2674   ASM_MESON_TAC[POLY_DIFF_LAST_LT];
2675   REWRITE_TAC[mono_unbounded_above];
2676   DISCH_THEN (MP_TAC o ISPEC `&0`);
2677   STRIP_TAC;
2678   (* save *)
2679   MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE);
2680   DISCH_THEN (X_CHOOSE_TAC `M:num`);
2681   CLAIM `-- &M <= X - &1`;
2682   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2683   STRIP_TAC;
2684   LABEL_ALL_TAC;
2685   USE_THEN "Z-2" (MP_TAC o ISPEC `nmax M N`);
2686   STRIP_TAC;
2687   CLAIM `N <= nmax M N`;
2688   REWRITE_TAC[nmax_le];
2689   DISCH_THEN (REWRITE_ASSUMS o list);
2690   CLAIM `-- &(nmax M N) < X`;
2691   MATCH_MP_TAC REAL_LET_TRANS;
2692   EXISTS_TAC `-- &M`;
2693   STRIP_TAC;
2694   REWRITE_TAC[nmax];
2695   REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC;
2696   USE_THEN "Z-0" MP_TAC THEN ARITH_TAC;
2697   STRIP_TAC;
2698   ASM_MESON_TAC[ARITH_RULE `~(x < &0 /\ &0 < x)`];
2699   (* save *)
2700   REWRITE_TAC[GSYM POLY_PNEG];
2701   MATCH_MP_TAC LAST_UNB_ODD_NEG;
2702   ASM_REWRITE_TAC[];
2703   ASM_SIMP_TAC[GSYM POLY_DIFF_LAST_LT];
2704   CASES_ON `?x. poly_diff p = [x]`;
2705   POP_ASSUM MP_TAC THEN STRIP_TAC;
2706   ASM_REWRITE_TAC[LAST];
2707   LABEL_ALL_TAC;
2708   USE_THEN "Z-2" MP_TAC;
2709   POP_ASSUM (fun x -> REWRITE_TAC[x] THEN ASSUME_TAC x);
2710   REWRITE_TAC[poly];
2711   REAL_SIMP_TAC;
2712   REPEAT STRIP_TAC;
2713   FIRST_ASSUM MATCH_MP_TAC;
2714   EXISTS_TAC `X - &1`;
2715   REAL_ARITH_TAC;
2716   CLAIM `nonconstant (poly_diff p)`;
2717   REWRITE_TAC[nonconstant];
2718   STRIP_TAC;
2719   MATCH_MP_TAC POLY_DIFF_NORMAL;
2720   FIRST_ASSUM MATCH_ACCEPT_TAC;
2721   ASM_MESON_TAC[];
2722   STRIP_TAC;
2723   CLAIM `EVEN (degree (poly_diff p))`;
2724   ASM_MESON_TAC[poly_diff_parity];
2725   STRIP_TAC;
2726   ONCE_REWRITE_TAC[ARITH_RULE `x < y <=> ~(y < x) /\ ~(y = x)`];
2727   REPEAT STRIP_TAC;
2728   CLAIM `mono_unbounded_above (\n. poly (poly_diff p) (-- (&n)))`;
2729   MATCH_MP_TAC LAST_UNB_EVEN_POS;
2730   ASM_REWRITE_TAC[];
2731   REWRITE_TAC[mono_unbounded_above];
2732   DISCH_THEN (MP_TAC o ISPEC `&0`);
2733   STRIP_TAC;
2734   (* save *)
2735   MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE);
2736   DISCH_THEN (X_CHOOSE_TAC `M:num`);
2737   CLAIM `-- &M <= X - &1`;
2738   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2739   STRIP_TAC;
2740   LABEL_ALL_TAC;
2741   USE_THEN "Z-2" (MP_TAC o ISPEC `nmax M N`);
2742   STRIP_TAC;
2743   CLAIM `N <= nmax M N`;
2744   REWRITE_TAC[nmax_le];
2745   DISCH_THEN (REWRITE_ASSUMS o list);
2746   CLAIM `-- &(nmax M N) < X`;
2747   MATCH_MP_TAC REAL_LET_TRANS;
2748   EXISTS_TAC `-- &M`;
2749   STRIP_TAC;
2750   REWRITE_TAC[nmax];
2751   REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC;
2752   USE_THEN "Z-0" MP_TAC THEN ARITH_TAC;
2753   STRIP_TAC;
2754   ASM_MESON_TAC[ARITH_RULE `~(x < &0 /\ &0 < x)`];
2755   ASM_MESON_TAC[nonconstant;NORMAL_ID];
2756   (* save xxx *)
2757   REWRITE_TAC[mono_unbounded_above];
2758   DISCH_THEN (MP_TAC o ISPEC `&0`);
2759   STRIP_TAC;
2760   MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE);
2761   DISCH_THEN (X_CHOOSE_TAC `M:num`);
2762   ABBREV_TAC `k = nmax N M`;
2763   EXISTS_TAC `-- &k`;
2764   REPEAT STRIP_TAC;
2765   REWRITE_TAC [ARITH_RULE `x < y <=> ~(y <= x)`];
2766   STRIP_TAC;
2767   MP_TAC (ISPECL [`p:real list`;`y:real`;`-- &k`] POLY_MVT);
2768   ASM_REWRITE_TAC[];
2769   STRIP_TAC;
2770   LABEL_ALL_TAC;
2771   CLAIM `&0 < (-- &k) - y`;
2772   USE_THEN "Z-4" MP_TAC THEN REAL_ARITH_TAC;
2773   STRIP_TAC;
2774   CLAIM `poly (poly_diff p) x < &0`;
2775   FIRST_ASSUM MATCH_MP_TAC;
2776   MATCH_MP_TAC REAL_LTE_TRANS;
2777   EXISTS_TAC `-- &k`;
2778   ASM_REWRITE_TAC[];
2779   MATCH_MP_TAC REAL_LE_TRANS;
2780   EXISTS_TAC `-- &M`;
2781   STRIP_TAC;
2782   USE_THEN "Z-5" (SUBST1_TAC o GSYM);
2783   REWRITE_TAC[nmax];
2784   REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC;
2785   USE_THEN "Z-6" MP_TAC THEN REAL_ARITH_TAC;
2786   STRIP_TAC;
2787   (* save *)
2788   CLAIM `N <= k:num`;
2789   USE_THEN "Z-5" (SUBST1_TAC o GSYM);
2790   REWRITE_TAC[nmax] THEN ARITH_TAC;
2791   STRIP_TAC;
2792   CLAIM `&0 < poly p (-- &k)`;
2793   ASM_MESON_TAC[];
2794   STRIP_TAC;
2795   CLAIM `&0 < poly p (-- &k) - poly p y`;
2796   LABEL_ALL_TAC;
2797   USE_ASSUM_LIST ["Z-10";"Z-3"] MP_TAC THEN REAL_ARITH_TAC;
2798   STRIP_TAC;
2799   CLAIM `(-- &k - y) * poly (poly_diff p) x < &0`;
2800   REWRITE_TAC[REAL_MUL_LT];
2801   ASM_REWRITE_TAC[];
2802   POP_ASSUM MP_TAC;
2803   USE_THEN "Z-0" MP_TAC;
2804   REAL_ARITH_TAC;
2805 ]);;
2806 (* }}} *)
2807
2808 let POLY_DIFF_DOWN_LEFT = prove_by_refinement(
2809  `!p. nonconstant p /\ (?X. !x. x < X ==> &0 < poly (poly_diff p) x) ==>
2810    (?Y. !y. y < Y ==> poly p y < &0)`,
2811 (* {{{ Proof *)
2812 [
2813   REPEAT STRIP_TAC;
2814   CLAIM `mono_unbounded_below (\n. poly p (-- &n))`;
2815   REWRITE_TAC[POLY_PNEG];
2816   DISJ_CASES_TAC (ISPEC `degree p` EVEN_OR_ODD);
2817   MATCH_MP_TAC mua_quotient_limit_neg;
2818   EXISTS_TAC `&1`;
2819   EXISTS_TAC `(\n. LAST (pneg p) * &n pow degree (pneg p))`;
2820   REPEAT STRIP_TAC;
2821   REAL_ARITH_TAC;
2822   BETA_TAC;
2823   MATCH_MP_TAC LIM_POLY2;
2824   MATCH_EQ_MP_TAC NORMAL_PNEG;
2825   ASM_MESON_TAC[nonconstant];
2826   MATCH_MP_TAC POW_UNBB_CON;
2827   STRIP_TAC;
2828   REWRITE_TAC[DEGREE_PNEG];
2829   REWRITE_TAC[degree];
2830   CLAIM `normalize p = p`;
2831   ASM_MESON_TAC[nonconstant;normal];
2832   DISCH_THEN SUBST1_TAC;
2833   CLAIM `~(LENGTH p = 0)`;
2834   ASM_MESON_TAC[nonconstant;normal;LENGTH_NZ;LENGTH_0;degree];
2835   STRIP_TAC;
2836   CLAIM `~(LENGTH p = 1)`;
2837   ASM_MESON_TAC[nonconstant;normal;LENGTH_NZ;LENGTH_1;degree];
2838   POP_ASSUM MP_TAC THEN ARITH_TAC;
2839   (* save *)
2840   CLAIM `LAST (pneg p) = LAST p`;
2841   ASM_MESON_TAC[GSYM POLY_PNEG_LAST;nonconstant;];
2842   DISCH_THEN SUBST1_TAC;
2843   ONCE_REWRITE_TAC[REAL_ARITH `x < y <=> ~(x = y) /\ ~(y < x)`];
2844   STRIP_TAC;
2845   ASM_MESON_TAC[NORMAL_ID;nonconstant];
2846   STRIP_TAC;
2847   CLAIM `ODD (degree (poly_diff p))`;
2848   ASM_SIMP_TAC[poly_diff_parity2];
2849   STRIP_TAC;
2850   CLAIM `nonconstant (poly_diff p)`;
2851   MATCH_MP_TAC normal_nonconstant;
2852   STRIP_TAC;
2853   MATCH_MP_TAC NONCONSTANT_DIFF_NORMAL;
2854   FIRST_ASSUM MATCH_ACCEPT_TAC;
2855   POP_ASSUM MP_TAC THEN ARITH_TAC;
2856   STRIP_TAC;
2857   CLAIM `mono_unbounded_below (\n. poly (poly_diff p) (-- &n))`;
2858   MATCH_MP_TAC LAST_UNB_ODD_POS;
2859   ASM_REWRITE_TAC[];
2860   ASM_MESON_TAC[POLY_DIFF_LAST_GT];
2861   REWRITE_TAC[mono_unbounded_below];
2862   DISCH_THEN (MP_TAC o ISPEC `&0`);
2863   STRIP_TAC;
2864   (* save *)
2865   MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE);
2866   DISCH_THEN (X_CHOOSE_TAC `M:num`);
2867   CLAIM `-- &M <= X - &1`;
2868   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2869   STRIP_TAC;
2870   LABEL_ALL_TAC;
2871   USE_THEN "Z-2" (MP_TAC o ISPEC `nmax M N`);
2872   STRIP_TAC;
2873   CLAIM `N <= nmax M N`;
2874   REWRITE_TAC[nmax_le];
2875   DISCH_THEN (REWRITE_ASSUMS o list);
2876   CLAIM `-- &(nmax M N) < X`;
2877   MATCH_MP_TAC REAL_LET_TRANS;
2878   EXISTS_TAC `-- &M`;
2879   STRIP_TAC;
2880   REWRITE_TAC[nmax];
2881   REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC;
2882   USE_THEN "Z-0" MP_TAC THEN ARITH_TAC;
2883   STRIP_TAC;
2884   ASM_MESON_TAC[ARITH_RULE `~(x < &0 /\ &0 < x)`];
2885   (* save *)
2886   REWRITE_TAC[GSYM POLY_PNEG];
2887   MATCH_MP_TAC LAST_UNB_ODD_POS;
2888   ASM_REWRITE_TAC[];
2889   ASM_SIMP_TAC[GSYM POLY_DIFF_LAST_GT];
2890   CASES_ON `?x. poly_diff p = [x]`;
2891   POP_ASSUM MP_TAC THEN STRIP_TAC;
2892   ASM_REWRITE_TAC[LAST];
2893   LABEL_ALL_TAC;
2894   USE_THEN "Z-2" MP_TAC;
2895   POP_ASSUM (fun x -> REWRITE_TAC[x] THEN ASSUME_TAC x);
2896   REWRITE_TAC[poly];
2897   REAL_SIMP_TAC;
2898   REPEAT STRIP_TAC;
2899   FIRST_ASSUM MATCH_MP_TAC;
2900   EXISTS_TAC `X - &1`;
2901   REAL_ARITH_TAC;
2902   CLAIM `nonconstant (poly_diff p)`;
2903   REWRITE_TAC[nonconstant];
2904   STRIP_TAC;
2905   MATCH_MP_TAC POLY_DIFF_NORMAL;
2906   FIRST_ASSUM MATCH_ACCEPT_TAC;
2907   ASM_MESON_TAC[];
2908   STRIP_TAC;
2909   CLAIM `EVEN (degree (poly_diff p))`;
2910   ASM_MESON_TAC[poly_diff_parity];
2911   STRIP_TAC;
2912   ONCE_REWRITE_TAC[ARITH_RULE `x < y <=> ~(y < x) /\ ~(y = x)`];
2913   REPEAT STRIP_TAC;
2914   CLAIM `mono_unbounded_below (\n. poly (poly_diff p) (-- (&n)))`;
2915   MATCH_MP_TAC LAST_UNBB_EVEN_NEG;
2916   ASM_REWRITE_TAC[];
2917   REWRITE_TAC[mono_unbounded_below];
2918   DISCH_THEN (MP_TAC o ISPEC `&0`);
2919   STRIP_TAC;
2920   (* save *)
2921   MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE);
2922   DISCH_THEN (X_CHOOSE_TAC `M:num`);
2923   CLAIM `-- &M <= X - &1`;
2924   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
2925   STRIP_TAC;
2926   LABEL_ALL_TAC;
2927   USE_THEN "Z-2" (MP_TAC o ISPEC `nmax M N`);
2928   STRIP_TAC;
2929   CLAIM `N <= nmax M N`;
2930   REWRITE_TAC[nmax_le];
2931   DISCH_THEN (REWRITE_ASSUMS o list);
2932   CLAIM `-- &(nmax M N) < X`;
2933   MATCH_MP_TAC REAL_LET_TRANS;
2934   EXISTS_TAC `-- &M`;
2935   STRIP_TAC;
2936   REWRITE_TAC[nmax];
2937   REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC;
2938   USE_THEN "Z-0" MP_TAC THEN ARITH_TAC;
2939   STRIP_TAC;
2940   ASM_MESON_TAC[ARITH_RULE `~(x < &0 /\ &0 < x)`];
2941   ASM_MESON_TAC[nonconstant;NORMAL_ID];
2942   (* save *)
2943   REWRITE_TAC[mono_unbounded_below];
2944   DISCH_THEN (MP_TAC o ISPEC `&0`);
2945   STRIP_TAC;
2946   MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE);
2947   DISCH_THEN (X_CHOOSE_TAC `M:num`);
2948   ABBREV_TAC `k = nmax N M`;
2949   EXISTS_TAC `-- &k`;
2950   REPEAT STRIP_TAC;
2951   REWRITE_TAC [ARITH_RULE `x < y <=> ~(y <= x)`];
2952   STRIP_TAC;
2953   MP_TAC (ISPECL [`p:real list`;`y:real`;`-- &k`] POLY_MVT);
2954   ASM_REWRITE_TAC[];
2955   STRIP_TAC;
2956   LABEL_ALL_TAC;
2957   CLAIM `&0 < (-- &k) - y`;
2958   USE_THEN "Z-4" MP_TAC THEN REAL_ARITH_TAC;
2959   STRIP_TAC;
2960   CLAIM `&0 < poly (poly_diff p) x`;
2961   FIRST_ASSUM MATCH_MP_TAC;
2962   MATCH_MP_TAC REAL_LTE_TRANS;
2963   EXISTS_TAC `-- &k`;
2964   ASM_REWRITE_TAC[];
2965   MATCH_MP_TAC REAL_LE_TRANS;
2966   EXISTS_TAC `-- &M`;
2967   STRIP_TAC;
2968   USE_THEN "Z-5" (SUBST1_TAC o GSYM);
2969   REWRITE_TAC[nmax];
2970   REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC;
2971   USE_THEN "Z-6" MP_TAC THEN REAL_ARITH_TAC;
2972   STRIP_TAC;
2973   (* save *)
2974   CLAIM `N <= k:num`;
2975   USE_THEN "Z-5" (SUBST1_TAC o GSYM);
2976   REWRITE_TAC[nmax] THEN ARITH_TAC;
2977   STRIP_TAC;
2978   CLAIM `poly p (-- &k) < &0`;
2979   ASM_MESON_TAC[];
2980   STRIP_TAC;
2981   CLAIM `poly p (-- &k) - poly p y < &0`;
2982   LABEL_ALL_TAC;
2983   USE_ASSUM_LIST ["Z-10";"Z-3"] MP_TAC THEN REAL_ARITH_TAC;
2984   STRIP_TAC;
2985   CLAIM `&0 < (-- &k - y) * poly (poly_diff p) x`;
2986   REWRITE_TAC[REAL_MUL_GT];
2987   ASM_REWRITE_TAC[];
2988   POP_ASSUM MP_TAC;
2989   USE_THEN "Z-0" MP_TAC;
2990   REAL_ARITH_TAC;
2991 ]);;
2992 (* }}} *)
2993
2994 let POLY_DIFF_DOWN_LEFT2 = prove_by_refinement(
2995  `!p X. nonconstant p /\ (!x. x < X ==> &0 < poly (poly_diff p) x) ==>
2996    (?Y. Y < X /\ (!y. y < Y ==> poly p y < &0))`,
2997 (* {{{ Proof *)
2998 [
2999   REPEAT STRIP_TAC;
3000   MP_TAC (ISPEC `p:real list` POLY_DIFF_DOWN_LEFT);
3001   ASM_REWRITE_TAC[];
3002   ANTS_TAC;
3003   ASM_MESON_TAC[];
3004   STRIP_TAC;
3005   EXISTS_TAC `min X Y - &1`;
3006   REPEAT STRIP_TAC;
3007   REAL_ARITH_TAC;
3008   FIRST_ASSUM MATCH_MP_TAC;
3009   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
3010 ]);;
3011 (* }}} *)
3012
3013 let POLY_DIFF_UP_LEFT2 = prove_by_refinement(
3014  `!p X. nonconstant p /\ (!x. x < X ==> poly (poly_diff p) x < &0) ==>
3015    (?Y. Y < X /\ (!y. y < Y ==> &0 < poly p y))`,
3016 (* {{{ Proof *)
3017 [
3018   REPEAT STRIP_TAC;
3019   MP_TAC (ISPEC `p:real list` POLY_DIFF_UP_LEFT);
3020   ASM_REWRITE_TAC[];
3021   ANTS_TAC;
3022   ASM_MESON_TAC[];
3023   STRIP_TAC;
3024   EXISTS_TAC `min X Y - &1`;
3025   REPEAT STRIP_TAC;
3026   REAL_ARITH_TAC;
3027   FIRST_ASSUM MATCH_MP_TAC;
3028   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
3029 ]);;
3030 (* }}} *)
3031
3032 let POLY_DIFF_DOWN_LEFT3 = prove_by_refinement(
3033  `!p p' X. nonconstant p ==> (poly_diff p = p') ==>
3034    (!x. x < X ==> &0 < poly p' x) ==>
3035      (?Y. Y < X /\ (!y. y < Y ==> poly p y < &0))`,
3036 (* {{{ Proof *)
3037 [
3038   REPEAT STRIP_TAC;
3039   MP_TAC (ISPEC `p:real list` POLY_DIFF_DOWN_LEFT);
3040   ASM_REWRITE_TAC[];
3041   ANTS_TAC;
3042   ASM_MESON_TAC[];
3043   STRIP_TAC;
3044   EXISTS_TAC `min X Y - &1`;
3045   REPEAT STRIP_TAC;
3046   REAL_ARITH_TAC;
3047   FIRST_ASSUM MATCH_MP_TAC;
3048   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
3049 ]);;
3050 (* }}} *)
3051
3052 let POLY_DIFF_UP_LEFT3 = prove_by_refinement(
3053  `!p p' X. nonconstant p ==> (poly_diff p = p') ==>
3054    (!x. x < X ==> poly p' x < &0) ==>
3055      (?Y. Y < X /\ (!y. y < Y ==> &0 < poly p y))`,
3056 (* {{{ Proof *)
3057 [
3058   REPEAT STRIP_TAC;
3059   MP_TAC (ISPEC `p:real list` POLY_DIFF_UP_LEFT);
3060   ASM_REWRITE_TAC[];
3061   ANTS_TAC;
3062   ASM_MESON_TAC[];
3063   STRIP_TAC;
3064   EXISTS_TAC `min X Y - &1`;
3065   REPEAT STRIP_TAC;
3066   REAL_ARITH_TAC;
3067   FIRST_ASSUM MATCH_MP_TAC;
3068   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
3069 ]);;
3070 (* }}} *)
3071
3072 let POLY_DIFF_DOWN_LEFT4 = prove_by_refinement(
3073  `!p p' X. nonconstant p ==> (poly_diff p = p') ==>
3074    (!x. x < X ==> &0 < poly p' x) ==>
3075      (?Y. Y < X /\ (!y. y <= Y ==> poly p y < &0))`,
3076 (* {{{ Proof *)
3077 [
3078   REPEAT STRIP_TAC;
3079   MP_TAC (ISPECL[ `p:real list`;`p':real list`;`X:real`] POLY_DIFF_DOWN_LEFT3);
3080   ASM_REWRITE_TAC[];
3081   REPEAT STRIP_TAC;
3082   EXISTS_TAC `Y - &1`;
3083   STRIP_TAC;
3084   POP_ASSUM IGNORE;
3085   POP_ASSUM MP_TAC;
3086   REAL_ARITH_TAC;
3087   REPEAT STRIP_TAC;
3088   FIRST_ASSUM MATCH_MP_TAC;
3089   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
3090 ]);;
3091 (* }}} *)
3092
3093 let POLY_DIFF_UP_LEFT4 = prove_by_refinement(
3094  `!p p' X. nonconstant p ==> (poly_diff p = p') ==>
3095    (!x. x < X ==> poly p' x < &0) ==>
3096      (?Y. Y < X /\ (!y. y <= Y ==> &0 < poly p y))`,
3097 (* {{{ Proof *)
3098 [
3099   REPEAT STRIP_TAC;
3100   MP_TAC (ISPECL[ `p:real list`;`p':real list`;`X:real`] POLY_DIFF_UP_LEFT3);
3101   ASM_REWRITE_TAC[];
3102   REPEAT STRIP_TAC;
3103   EXISTS_TAC `Y - &1`;
3104   STRIP_TAC;
3105   POP_ASSUM IGNORE;
3106   POP_ASSUM MP_TAC;
3107   REAL_ARITH_TAC;
3108   REPEAT STRIP_TAC;
3109   FIRST_ASSUM MATCH_MP_TAC;
3110   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
3111 ]);;
3112 (* }}} *)
3113
3114 let POLY_DIFF_DOWN_LEFT5 = prove_by_refinement(
3115  `!p p' X. nonconstant p ==> (poly_diff p = p') ==>
3116    (!x. x < X ==> poly p' x > &0) ==>
3117      (?Y. Y < X /\ (!y. y <= Y ==> poly p y < &0))`,
3118 (* {{{ Proof *)
3119 [
3120   REWRITE_TAC[real_gt];
3121   ASM_MESON_TAC[POLY_DIFF_DOWN_LEFT4];
3122 ]);;
3123 (* }}} *)
3124
3125 let POLY_DIFF_UP_LEFT5 = prove_by_refinement(
3126  `!p p' X. nonconstant p ==> (poly_diff p = p') ==>
3127    (!x. x < X ==> poly p' x < &0) ==>
3128      (?Y. Y < X /\ (!y. y <= Y ==> poly p y > &0))`,
3129 (* {{{ Proof *)
3130 [
3131   REWRITE_TAC[real_gt];
3132   MESON_TAC[POLY_DIFF_UP_LEFT4];
3133 ]);;
3134 (* }}} *)
3135
3136 let NORMAL_PDIFF_LEM = prove_by_refinement(
3137  `!p. normal (poly_diff p) ==> nonconstant p`,
3138 (* {{{ Proof *)
3139 [
3140   LIST_INDUCT_TAC;
3141   REWRITE_TAC[normal;poly_diff;poly_diff_aux];
3142   REWRITE_TAC[nonconstant];
3143   REWRITE_TAC[poly_diff;poly_diff_aux;NOT_CONS_NIL;TL;];
3144   REPEAT STRIP_TAC;
3145   MATCH_MP_TAC NORMAL_CONS;
3146   ASM_MESON_TAC[POLY_DIFF_AUX_NORMAL;ARITH_RULE `~(1 = 0)`];
3147   CLAIM `t = []`;
3148   ASM_MESON_TAC !LIST_REWRITES;
3149   DISCH_THEN (REWRITE_ASSUMS o list);
3150   ASM_MESON_TAC[normal;poly_diff_aux];
3151 ]);;
3152 (* }}} *)
3153
3154 let NORMAL_PDIFF = prove_by_refinement(
3155  `!p. nonconstant p = normal (poly_diff p)`,
3156 (* {{{ Proof *)
3157 [
3158   MESON_TAC[NORMAL_PDIFF_LEM;POLY_DIFF_NORMAL];
3159 ]);;
3160 (* }}} *)
3161
3162 let POLY_DIFF_UP_RIGHT2 = prove_by_refinement(
3163  `!p p' X. nonconstant p ==> (poly_diff p = p') ==>
3164      (!x. X < x ==> &0 < poly p' x) ==>
3165      (?Y. X < Y /\ (!y. Y <= y ==> &0 < poly p y))`,
3166 (* {{{ Proof *)
3167 [
3168   REPEAT STRIP_TAC;
3169   MP_TAC (ISPECL[ `p:real list`] (GEN_ALL POLY_DIFF_UP_RIGHT));
3170   ASM_REWRITE_TAC[];
3171   ANTS_TAC;
3172   ASM_MESON_TAC[];
3173   REPEAT STRIP_TAC;
3174   EXISTS_TAC `(max X Y) + &1`;
3175   STRIP_TAC;
3176   REAL_ARITH_TAC;
3177   REPEAT STRIP_TAC;
3178   FIRST_ASSUM MATCH_MP_TAC;
3179   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
3180 ]);;
3181 (* }}} *)
3182
3183 let POLY_DIFF_DOWN_RIGHT2 = prove_by_refinement(
3184  `!p p' X. nonconstant p ==> (poly_diff p = p') ==>
3185      (!x. X < x ==> poly p' x < &0) ==>
3186      (?Y. X < Y /\ (!y. Y <= y ==> poly p y < &0))`,
3187 (* {{{ Proof *)
3188 [
3189   REPEAT STRIP_TAC;
3190   MP_TAC (ISPECL[ `p:real list`] (GEN_ALL POLY_DIFF_DOWN_RIGHT));
3191   ASM_REWRITE_TAC[];
3192   ANTS_TAC;
3193   ASM_MESON_TAC[];
3194   REPEAT STRIP_TAC;
3195   EXISTS_TAC `(max X Y) + &1`;
3196   STRIP_TAC;
3197   REAL_ARITH_TAC;
3198   REPEAT STRIP_TAC;
3199   FIRST_ASSUM MATCH_MP_TAC;
3200   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
3201 ]);;
3202 (* }}} *)
3203
3204 let POLY_DIFF_UP_RIGHT3 = prove_by_refinement(
3205  `!p p' X. nonconstant p ==> (poly_diff p = p') ==>
3206      (!x. X < x ==> poly p' x > &0) ==>
3207      (?Y. X < Y /\ (!y. Y <= y ==> poly p y > &0))`,
3208 (* {{{ Proof *)
3209 [
3210   REWRITE_TAC[real_gt;real_ge];
3211   MESON_TAC[POLY_DIFF_UP_RIGHT2];
3212 ]);;
3213 (* }}} *)
3214
3215 let POLY_DIFF_DOWN_RIGHT3 = prove_by_refinement(
3216  `!p p' X. nonconstant p ==> (poly_diff p = p') ==>
3217      (!x. X < x ==> poly p' x < &0) ==>
3218      (?Y. X < Y /\ (!y. Y <= y ==> poly p y < &0))`,
3219 (* {{{ Proof *)
3220 [
3221   REWRITE_TAC[real_gt;real_ge];
3222   MESON_TAC[POLY_DIFF_DOWN_RIGHT2];
3223 ]);;
3224 (* }}} *)
3225
3226
3227