Library/poly.ml

   1 (* ========================================================================= *)
   2 (* Properties of real polynomials (not canonically represented).             *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/analysis.ml";;
   6
   7 prioritize_real();;
   8
   9 parse_as_infix("++",(16,"right"));;
  10 parse_as_infix("**",(20,"right"));;
  11 parse_as_infix("##",(20,"right"));;
  12 parse_as_infix("divides",(14,"right"));;
  13 parse_as_infix("exp",(22,"right"));;
  14
  15 do_list override_interface
  16   ["++",`poly_add:real list->real list->real list`;
  17    "**",`poly_mul:real list->real list->real list`;
  18    "##",`poly_cmul:real->real list->real list`;
  19    "neg",`poly_neg:real list->real list`;
  20    "exp",`poly_exp:real list -> num -> real list`;
  21    "diff",`poly_diff:real list->real list`];;
  22
  23 overload_interface ("divides",`poly_divides:real list->real list->bool`);;
  24
  25 (* ------------------------------------------------------------------------- *)
  26 (* Application of polynomial as a real function.                             *)
  27 (* ------------------------------------------------------------------------- *)
  28
  29 let poly = new_recursive_definition list_RECURSION
  30   `(poly [] x = &0) /\
  31    (poly (CONS h t) x = h + x * poly t x)`;;
  32
  33 let POLY_CONST = prove
  34  (`!c x. poly [c] x = c`,
  35   REWRITE_TAC[poly] THEN REAL_ARITH_TAC);;
  36
  37 let POLY_X = prove
  38  (`!c x. poly [&0; &1] x = x`,
  39   REWRITE_TAC[poly] THEN REAL_ARITH_TAC);;
  40
  41 (* ------------------------------------------------------------------------- *)
  42 (* Arithmetic operations on polynomials.                                     *)
  43 (* ------------------------------------------------------------------------- *)
  44
  45 let poly_add = new_recursive_definition list_RECURSION
  46   `([] ++ l2 = l2) /\
  47    ((CONS h t) ++ l2 =
  48         (if l2 = [] then CONS h t
  49                     else CONS (h + HD l2) (t ++ TL l2)))`;;
  50
  51 let poly_cmul = new_recursive_definition list_RECURSION
  52   `(c ## [] = []) /\
  53    (c ## (CONS h t) = CONS (c * h) (c ## t))`;;
  54
  55 let poly_neg = new_definition
  56   `neg = (##) (--(&1))`;;
  57
  58 let poly_mul = new_recursive_definition list_RECURSION
  59   `([] ** l2 = []) /\
  60    ((CONS h t) ** l2 =
  61        (if t = [] then h ## l2
  62                   else (h ## l2) ++ CONS (&0) (t ** l2)))`;;
  63
  64 let poly_exp = new_recursive_definition num_RECURSION
  65   `(p exp 0 = [&1]) /\
  66    (p exp (SUC n) = p ** p exp n)`;;
  67
  68 (* ------------------------------------------------------------------------- *)
  69 (* Differentiation of polynomials (needs an auxiliary function).             *)
  70 (* ------------------------------------------------------------------------- *)
  71
  72 let poly_diff_aux = new_recursive_definition list_RECURSION
  73   `(poly_diff_aux n [] = []) /\
  74    (poly_diff_aux n (CONS h t) = CONS (&n * h) (poly_diff_aux (SUC n) t))`;;
  75
  76 let poly_diff = new_definition
  77   `diff l = (if l = [] then [] else (poly_diff_aux 1 (TL l)))`;;
  78
  79 (* ------------------------------------------------------------------------- *)
  80 (* Lengths.                                                                  *)
  81 (* ------------------------------------------------------------------------- *)
  82
  83 let LENGTH_POLY_DIFF_AUX = prove
  84  (`!l n. LENGTH(poly_diff_aux n l) = LENGTH l`,
  85   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[LENGTH; poly_diff_aux]);;
  86
  87 let LENGTH_POLY_DIFF = prove
  88  (`!l. LENGTH(poly_diff l) = PRE(LENGTH l)`,
  89   LIST_INDUCT_TAC THEN
  90   SIMP_TAC[poly_diff; LENGTH; LENGTH_POLY_DIFF_AUX; NOT_CONS_NIL; TL; PRE]);;
  91
  92 (* ------------------------------------------------------------------------- *)
  93 (* Useful clausifications.                                                   *)
  94 (* ------------------------------------------------------------------------- *)
  95
  96 let POLY_ADD_CLAUSES = prove
  97  (`([] ++ p2 = p2) /\
  98    (p1 ++ [] = p1) /\
  99    ((CONS h1 t1) ++ (CONS h2 t2) = CONS (h1 + h2) (t1 ++ t2))`,
 100   REWRITE_TAC[poly_add; NOT_CONS_NIL; HD; TL] THEN
 101   SPEC_TAC(`p1:real list`,`p1:real list`) THEN
 102   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[poly_add]);;
 103
 104 let POLY_CMUL_CLAUSES = prove
 105  (`(c ## [] = []) /\
 106    (c ## (CONS h t) = CONS (c * h) (c ## t))`,
 107   REWRITE_TAC[poly_cmul]);;
 108
 109 let POLY_NEG_CLAUSES = prove
 110  (`(neg [] = []) /\
 111    (neg (CONS h t) = CONS (--h) (neg t))`,
 112   REWRITE_TAC[poly_neg; POLY_CMUL_CLAUSES; REAL_MUL_LNEG; REAL_MUL_LID]);;
 113
 114 let POLY_MUL_CLAUSES = prove
 115  (`([] ** p2 = []) /\
 116    ([h1] ** p2 = h1 ## p2) /\
 117    ((CONS h1 (CONS k1 t1)) ** p2 = h1 ## p2 ++ CONS (&0) (CONS k1 t1 ** p2))`,
 118   REWRITE_TAC[poly_mul; NOT_CONS_NIL]);;
 119
 120 let POLY_DIFF_CLAUSES = prove
 121  (`(diff [] = []) /\
 122    (diff [c] = []) /\
 123    (diff (CONS h t) = poly_diff_aux 1 t)`,
 124   REWRITE_TAC[poly_diff; NOT_CONS_NIL; HD; TL; poly_diff_aux]);;
 125
 126 (* ------------------------------------------------------------------------- *)
 127 (* Various natural consequences of syntactic definitions.                    *)
 128 (* ------------------------------------------------------------------------- *)
 129
 130 let POLY_ADD = prove
 131  (`!p1 p2 x. poly (p1 ++ p2) x = poly p1 x + poly p2 x`,
 132   LIST_INDUCT_TAC THEN REWRITE_TAC[poly_add; poly; REAL_ADD_LID] THEN
 133   LIST_INDUCT_TAC THEN
 134   ASM_REWRITE_TAC[NOT_CONS_NIL; HD; TL; poly; REAL_ADD_RID] THEN
 135   REAL_ARITH_TAC);;
 136
 137 let POLY_CMUL = prove
 138  (`!p c x. poly (c ## p) x = c * poly p x`,
 139   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[poly; poly_cmul] THEN
 140   REAL_ARITH_TAC);;
 141
 142 let POLY_NEG = prove
 143  (`!p x. poly (neg p) x = --(poly p x)`,
 144   REWRITE_TAC[poly_neg; POLY_CMUL] THEN
 145   REAL_ARITH_TAC);;
 146
 147 let POLY_MUL = prove
 148  (`!x p1 p2. poly (p1 ** p2) x = poly p1 x * poly p2 x`,
 149   GEN_TAC THEN LIST_INDUCT_TAC THEN
 150   REWRITE_TAC[poly_mul; poly; REAL_MUL_LZERO; POLY_CMUL; POLY_ADD] THEN
 151   SPEC_TAC(`h:real`,`h:real`) THEN
 152   SPEC_TAC(`t:real list`,`t:real list`) THEN
 153   LIST_INDUCT_TAC THEN
 154   REWRITE_TAC[poly_mul; POLY_CMUL; POLY_ADD; poly; POLY_CMUL;
 155     REAL_MUL_RZERO; REAL_ADD_RID; NOT_CONS_NIL] THEN
 156   ASM_REWRITE_TAC[POLY_ADD; POLY_CMUL; poly] THEN
 157   REAL_ARITH_TAC);;
 158
 159 let POLY_EXP = prove
 160  (`!p n x. poly (p exp n) x = (poly p x) pow n`,
 161   GEN_TAC THEN INDUCT_TAC THEN
 162   ASM_REWRITE_TAC[poly_exp; real_pow; POLY_MUL] THEN
 163   REWRITE_TAC[poly] THEN REAL_ARITH_TAC);;
 164
 165 (* ------------------------------------------------------------------------- *)
 166 (* The derivative is a bit more complicated.                                 *)
 167 (* ------------------------------------------------------------------------- *)
 168
 169 let POLY_DIFF_LEMMA = prove
 170  (`!l n x. ((\x. (x pow (SUC n)) * poly l x) diffl
 171                    ((x pow n) * poly (poly_diff_aux (SUC n) l) x))(x)`,
 172   LIST_INDUCT_TAC THEN
 173   REWRITE_TAC[poly; poly_diff_aux; REAL_MUL_RZERO; DIFF_CONST] THEN
 174   MAP_EVERY X_GEN_TAC [`n:num`; `x:real`] THEN
 175   REWRITE_TAC[REAL_LDISTRIB; REAL_MUL_ASSOC] THEN
 176   ONCE_REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[REAL_MUL_SYM] (CONJUNCT2 pow))] THEN
 177   POP_ASSUM(MP_TAC o SPECL [`SUC n`; `x:real`]) THEN
 178   SUBGOAL_THEN `(((\x. (x pow (SUC n)) * h)) diffl
 179                         ((x pow n) * &(SUC n) * h))(x)`
 180   (fun th -> DISCH_THEN(MP_TAC o CONJ th)) THENL
 181    [REWRITE_TAC[REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
 182     MP_TAC(SPEC `\x. x pow (SUC n)` DIFF_CMUL) THEN BETA_TAC THEN
 183     DISCH_THEN MATCH_MP_TAC THEN
 184     MP_TAC(SPEC `SUC n` DIFF_POW) THEN REWRITE_TAC[SUC_SUB1] THEN
 185     DISCH_THEN(MATCH_ACCEPT_TAC o ONCE_REWRITE_RULE[REAL_MUL_SYM]);
 186     DISCH_THEN(MP_TAC o MATCH_MP DIFF_ADD) THEN BETA_TAC THEN
 187     REWRITE_TAC[REAL_MUL_ASSOC]]);;
 188
 189 let POLY_DIFF = prove
 190  (`!l x. ((\x. poly l x) diffl (poly (diff l) x))(x)`,
 191   LIST_INDUCT_TAC THEN REWRITE_TAC[POLY_DIFF_CLAUSES] THEN
 192   ONCE_REWRITE_TAC[SYM(ETA_CONV `\x. poly l x`)] THEN
 193   REWRITE_TAC[poly; DIFF_CONST] THEN
 194   MAP_EVERY X_GEN_TAC [`x:real`] THEN
 195   MP_TAC(SPECL [`t:(real)list`; `0`; `x:real`] POLY_DIFF_LEMMA) THEN
 196   REWRITE_TAC[SYM(num_CONV `1`)] THEN REWRITE_TAC[pow; REAL_MUL_LID] THEN
 197   REWRITE_TAC[POW_1] THEN
 198   DISCH_THEN(MP_TAC o CONJ (SPECL [`h:real`; `x:real`] DIFF_CONST)) THEN
 199   DISCH_THEN(MP_TAC o MATCH_MP DIFF_ADD) THEN BETA_TAC THEN
 200   REWRITE_TAC[REAL_ADD_LID]);;
 201
 202 (* ------------------------------------------------------------------------- *)
 203 (* Trivial consequences.                                                     *)
 204 (* ------------------------------------------------------------------------- *)
 205
 206 let POLY_DIFFERENTIABLE = prove
 207  (`!l x. (\x. poly l x) differentiable x`,
 208   REPEAT GEN_TAC THEN REWRITE_TAC[differentiable] THEN
 209   EXISTS_TAC `poly (diff l) x` THEN
 210   REWRITE_TAC[POLY_DIFF]);;
 211
 212 let POLY_CONT = prove
 213  (`!l x. (\x. poly l x) contl x`,
 214   REPEAT GEN_TAC THEN MATCH_MP_TAC DIFF_CONT THEN
 215   EXISTS_TAC `poly (diff l) x` THEN
 216   MATCH_ACCEPT_TAC POLY_DIFF);;
 217
 218 let POLY_IVT_POS = prove
 219  (`!p a b. a < b /\ poly p a < &0 /\ poly p b > &0
 220            ==> ?x. a < x /\ x < b /\ (poly p x = &0)`,
 221   REWRITE_TAC[real_gt] THEN REPEAT STRIP_TAC THEN
 222   MP_TAC(SPECL [`\x. poly p x`; `a:real`; `b:real`; `&0`] IVT) THEN
 223   REWRITE_TAC[POLY_CONT] THEN
 224   EVERY_ASSUM(fun th -> REWRITE_TAC[MATCH_MP REAL_LT_IMP_LE th]) THEN
 225   DISCH_THEN(X_CHOOSE_THEN `x:real` STRIP_ASSUME_TAC) THEN
 226   EXISTS_TAC `x:real` THEN ASM_REWRITE_TAC[REAL_LT_LE] THEN
 227   CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
 228   FIRST_ASSUM SUBST_ALL_TAC THEN
 229   RULE_ASSUM_TAC(REWRITE_RULE[REAL_LT_REFL]) THEN
 230   FIRST_ASSUM CONTR_TAC);;
 231
 232 let POLY_IVT_NEG = prove
 233  (`!p a b. a < b /\ poly p a > &0 /\ poly p b < &0
 234            ==> ?x. a < x /\ x < b /\ (poly p x = &0)`,
 235   REPEAT STRIP_TAC THEN MP_TAC(SPEC `poly_neg p` POLY_IVT_POS) THEN
 236   REWRITE_TAC[POLY_NEG;
 237               REAL_ARITH `(--x < &0 <=> x > &0) /\ (--x > &0 <=> x < &0)`] THEN
 238   DISCH_THEN(MP_TAC o SPECL [`a:real`; `b:real`]) THEN
 239   ASM_REWRITE_TAC[REAL_ARITH `(--x = &0) <=> (x = &0)`]);;
 240
 241 let POLY_MVT = prove
 242  (`!p a b. a < b ==>
 243            ?x. a < x /\ x < b /\
 244               (poly p b - poly p a = (b - a) * poly (diff p) x)`,
 245   REPEAT STRIP_TAC THEN
 246   MP_TAC(SPECL [`poly p`; `a:real`; `b:real`] MVT) THEN
 247   ASM_REWRITE_TAC[CONV_RULE(DEPTH_CONV ETA_CONV) (SPEC_ALL POLY_CONT);
 248     CONV_RULE(DEPTH_CONV ETA_CONV) (SPEC_ALL POLY_DIFFERENTIABLE)] THEN
 249   DISCH_THEN(X_CHOOSE_THEN `l:real` MP_TAC) THEN
 250   DISCH_THEN(X_CHOOSE_THEN `x:real` STRIP_ASSUME_TAC) THEN
 251   EXISTS_TAC `x:real` THEN ASM_REWRITE_TAC[] THEN
 252   AP_TERM_TAC THEN MATCH_MP_TAC DIFF_UNIQ THEN
 253   EXISTS_TAC `poly p` THEN EXISTS_TAC `x:real` THEN
 254   ASM_REWRITE_TAC[CONV_RULE(DEPTH_CONV ETA_CONV) (SPEC_ALL POLY_DIFF)]);;
 255
 256 let POLY_MVT_ADD = prove
 257  (`!p a x. ?y. abs(y) <= abs(x) /\
 258                (poly p (a + x) = poly p a + x * poly (diff p) (a + y))`,
 259   REPEAT GEN_TAC THEN
 260   REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC `x:real` REAL_LT_NEGTOTAL) THENL
 261    [EXISTS_TAC `&0` THEN
 262     ASM_REWRITE_TAC[REAL_LE_REFL; REAL_ADD_RID; REAL_MUL_LZERO];
 263     MP_TAC(SPECL [`p:real list`; `a:real`; `a + x`] POLY_MVT) THEN
 264     ASM_REWRITE_TAC[REAL_LT_ADDR] THEN
 265     DISCH_THEN(X_CHOOSE_THEN `z:real` MP_TAC) THEN
 266     REWRITE_TAC[REAL_ARITH `(x - y = ((a + b) - a) * z) <=>
 267                             (x = y + b * z)`] THEN
 268     STRIP_TAC THEN ASM_REWRITE_TAC[REAL_EQ_ADD_LCANCEL] THEN
 269     EXISTS_TAC `z - a` THEN REWRITE_TAC[REAL_ARITH `x + (y - x) = y`] THEN
 270     MAP_EVERY UNDISCH_TAC [`&0 < x`; `a < z`; `z < a + x`] THEN
 271     REAL_ARITH_TAC;
 272     MP_TAC(SPECL [`p:real list`; `a + x`; `a:real`] POLY_MVT) THEN
 273     ASM_REWRITE_TAC[REAL_ARITH `a + x < a <=> &0 < --x`] THEN
 274     DISCH_THEN(X_CHOOSE_THEN `z:real` MP_TAC) THEN
 275     REWRITE_TAC[REAL_ARITH `(x - y = (a - (a + b)) * z) <=>
 276                             (x = y + b * --z)`] THEN
 277     STRIP_TAC THEN ASM_REWRITE_TAC[REAL_EQ_ADD_LCANCEL] THEN
 278     EXISTS_TAC `z - a` THEN REWRITE_TAC[REAL_ARITH `x + (y - x) = y`] THEN
 279     MAP_EVERY UNDISCH_TAC [`&0 < --x`; `a + x < z`; `z < a`] THEN
 280     REAL_ARITH_TAC]);;
 281
 282 (* ------------------------------------------------------------------------- *)
 283 (* Lemmas.                                                                   *)
 284 (* ------------------------------------------------------------------------- *)
 285
 286 let POLY_ADD_RZERO = prove
 287  (`!p. poly (p ++ []) = poly p`,
 288   REWRITE_TAC[FUN_EQ_THM; POLY_ADD; poly; REAL_ADD_RID]);;
 289
 290 let POLY_MUL_ASSOC = prove
 291  (`!p q r. poly (p ** (q ** r)) = poly ((p ** q) ** r)`,
 292   REWRITE_TAC[FUN_EQ_THM; POLY_MUL; REAL_MUL_ASSOC]);;
 293
 294 let POLY_EXP_ADD = prove
 295  (`!d n p. poly(p exp (n + d)) = poly(p exp n ** p exp d)`,
 296   REWRITE_TAC[FUN_EQ_THM; POLY_MUL] THEN
 297   INDUCT_TAC THEN ASM_REWRITE_TAC[POLY_MUL; ADD_CLAUSES; poly_exp; poly] THEN
 298   REAL_ARITH_TAC);;
 299
 300 (* ------------------------------------------------------------------------- *)
 301 (* Lemmas for derivatives.                                                   *)
 302 (* ------------------------------------------------------------------------- *)
 303
 304 let POLY_DIFF_AUX_ADD = prove
 305  (`!p1 p2 n. poly (poly_diff_aux n (p1 ++ p2)) =
 306              poly (poly_diff_aux n p1 ++ poly_diff_aux n p2)`,
 307   REPEAT(LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff_aux; poly_add]) THEN
 308   ASM_REWRITE_TAC[poly_diff_aux; FUN_EQ_THM; poly; NOT_CONS_NIL; HD; TL] THEN
 309   REAL_ARITH_TAC);;
 310
 311 let POLY_DIFF_AUX_CMUL = prove
 312  (`!p c n. poly (poly_diff_aux n (c ## p)) =
 313            poly (c ## poly_diff_aux n p)`,
 314   LIST_INDUCT_TAC THEN
 315   ASM_REWRITE_TAC[FUN_EQ_THM; poly; poly_diff_aux; poly_cmul; REAL_MUL_AC]);;
 316
 317 let POLY_DIFF_AUX_NEG = prove
 318  (`!p n.  poly (poly_diff_aux n (neg p)) =
 319           poly (neg (poly_diff_aux n p))`,
 320   REWRITE_TAC[poly_neg; POLY_DIFF_AUX_CMUL]);;
 321
 322 let POLY_DIFF_AUX_MUL_LEMMA = prove
 323  (`!p n. poly (poly_diff_aux (SUC n) p) = poly (poly_diff_aux n p ++ p)`,
 324   LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff_aux; poly_add; NOT_CONS_NIL] THEN
 325   ASM_REWRITE_TAC[HD; TL; poly; FUN_EQ_THM] THEN
 326   REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_ADD_RDISTRIB; REAL_MUL_LID]);;
 327
 328 (* ------------------------------------------------------------------------- *)
 329 (* Final results for derivatives.                                            *)
 330 (* ------------------------------------------------------------------------- *)
 331
 332 let POLY_DIFF_ADD = prove
 333  (`!p1 p2. poly (diff (p1 ++ p2)) =
 334            poly (diff p1  ++ diff p2)`,
 335   REPEAT LIST_INDUCT_TAC THEN
 336   REWRITE_TAC[poly_add; poly_diff; NOT_CONS_NIL; POLY_ADD_RZERO] THEN
 337   ASM_REWRITE_TAC[HD; TL; POLY_DIFF_AUX_ADD]);;
 338
 339 let POLY_DIFF_CMUL = prove
 340  (`!p c. poly (diff (c ## p)) = poly (c ## diff p)`,
 341   LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff; poly_cmul] THEN
 342   REWRITE_TAC[NOT_CONS_NIL; HD; TL; POLY_DIFF_AUX_CMUL]);;
 343
 344 let POLY_DIFF_NEG = prove
 345  (`!p. poly (diff (neg p)) = poly (neg (diff p))`,
 346   REWRITE_TAC[poly_neg; POLY_DIFF_CMUL]);;
 347
 348 let POLY_DIFF_MUL_LEMMA = prove
 349  (`!t h. poly (diff (CONS h t)) =
 350          poly (CONS (&0) (diff t) ++ t)`,
 351   REWRITE_TAC[poly_diff; NOT_CONS_NIL] THEN
 352   LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff_aux; NOT_CONS_NIL; HD; TL] THENL
 353    [REWRITE_TAC[FUN_EQ_THM; poly; poly_add; REAL_MUL_RZERO; REAL_ADD_LID];
 354     REWRITE_TAC[FUN_EQ_THM; poly; POLY_DIFF_AUX_MUL_LEMMA; POLY_ADD] THEN
 355     REAL_ARITH_TAC]);;
 356
 357 let POLY_DIFF_MUL = prove
 358  (`!p1 p2. poly (diff (p1 ** p2)) =
 359            poly (p1 ** diff p2 ++ diff p1 ** p2)`,
 360   LIST_INDUCT_TAC THEN REWRITE_TAC[poly_mul] THENL
 361    [REWRITE_TAC[poly_diff; poly_add; poly_mul]; ALL_TAC] THEN
 362   GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
 363    [REWRITE_TAC[POLY_DIFF_CLAUSES] THEN
 364     REWRITE_TAC[poly_add; poly_mul; POLY_ADD_RZERO; POLY_DIFF_CMUL];
 365     ALL_TAC] THEN
 366   REWRITE_TAC[FUN_EQ_THM; POLY_DIFF_ADD; POLY_ADD] THEN
 367   REWRITE_TAC[poly; POLY_ADD; POLY_DIFF_MUL_LEMMA; POLY_MUL] THEN
 368   ASM_REWRITE_TAC[POLY_DIFF_CMUL; POLY_ADD; POLY_MUL] THEN
 369   REAL_ARITH_TAC);;
 370
 371 let POLY_DIFF_EXP = prove
 372  (`!p n. poly (diff (p exp (SUC n))) =
 373          poly ((&(SUC n) ## (p exp n)) ** diff p)`,
 374   GEN_TAC THEN INDUCT_TAC THEN ONCE_REWRITE_TAC[poly_exp] THENL
 375    [REWRITE_TAC[poly_exp; POLY_DIFF_MUL] THEN
 376     REWRITE_TAC[FUN_EQ_THM; POLY_MUL; POLY_ADD; POLY_CMUL] THEN
 377     REWRITE_TAC[poly; POLY_DIFF_CLAUSES; ADD1; ADD_CLAUSES] THEN
 378     REAL_ARITH_TAC;
 379     REWRITE_TAC[POLY_DIFF_MUL] THEN
 380     ASM_REWRITE_TAC[POLY_MUL; POLY_ADD; FUN_EQ_THM; POLY_CMUL] THEN
 381     REWRITE_TAC[poly_exp; POLY_MUL] THEN
 382     REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_ADD] THEN
 383     REAL_ARITH_TAC]);;
 384
 385 let POLY_DIFF_EXP_PRIME = prove
 386  (`!n a. poly (diff ([--a; &1] exp (SUC n))) =
 387          poly (&(SUC n) ## ([--a; &1] exp n))`,
 388   REPEAT GEN_TAC THEN REWRITE_TAC[POLY_DIFF_EXP] THEN
 389   REWRITE_TAC[FUN_EQ_THM; POLY_MUL] THEN
 390   REWRITE_TAC[poly_diff; poly_diff_aux; TL; NOT_CONS_NIL] THEN
 391   REWRITE_TAC[poly] THEN REAL_ARITH_TAC);;
 392
 393 (* ------------------------------------------------------------------------- *)
 394 (* Key property that f(a) = 0 ==> (x - a) divides p(x). Very delicate!       *)
 395 (* ------------------------------------------------------------------------- *)
 396
 397 let POLY_LINEAR_REM = prove
 398  (`!t h. ?q r. CONS h t = [r] ++ [--a; &1] ** q`,
 399   LIST_INDUCT_TAC THEN REWRITE_TAC[] THENL
 400    [GEN_TAC THEN EXISTS_TAC `[]:real list` THEN
 401     EXISTS_TAC `h:real` THEN
 402     REWRITE_TAC[poly_add; poly_mul; poly_cmul; NOT_CONS_NIL] THEN
 403     REWRITE_TAC[HD; TL; REAL_ADD_RID];
 404     X_GEN_TAC `k:real` THEN POP_ASSUM(STRIP_ASSUME_TAC o SPEC `h:real`) THEN
 405     EXISTS_TAC `CONS (r:real) q` THEN EXISTS_TAC `r * a + k` THEN
 406     ASM_REWRITE_TAC[POLY_ADD_CLAUSES; POLY_MUL_CLAUSES; poly_cmul] THEN
 407     REWRITE_TAC[CONS_11] THEN CONJ_TAC THENL
 408      [REAL_ARITH_TAC; ALL_TAC] THEN
 409     SPEC_TAC(`q:real list`,`q:real list`) THEN
 410     LIST_INDUCT_TAC THEN
 411     REWRITE_TAC[POLY_ADD_CLAUSES; POLY_MUL_CLAUSES; poly_cmul] THEN
 412     REWRITE_TAC[REAL_ADD_RID; REAL_MUL_LID] THEN
 413     REWRITE_TAC[REAL_ADD_AC]]);;
 414
 415 let POLY_LINEAR_DIVIDES = prove
 416  (`!a p. (poly p a = &0) <=> (p = []) \/ ?q. p = [--a; &1] ** q`,
 417   GEN_TAC THEN LIST_INDUCT_TAC THENL
 418    [REWRITE_TAC[poly]; ALL_TAC] THEN
 419   EQ_TAC THEN STRIP_TAC THENL
 420    [DISJ2_TAC THEN STRIP_ASSUME_TAC(SPEC_ALL POLY_LINEAR_REM) THEN
 421     EXISTS_TAC `q:real list` THEN ASM_REWRITE_TAC[] THEN
 422     SUBGOAL_THEN `r = &0` SUBST_ALL_TAC THENL
 423      [UNDISCH_TAC `poly (CONS h t) a = &0` THEN
 424       ASM_REWRITE_TAC[] THEN REWRITE_TAC[POLY_ADD; POLY_MUL] THEN
 425       REWRITE_TAC[poly; REAL_MUL_RZERO; REAL_ADD_RID; REAL_MUL_RID] THEN
 426       REWRITE_TAC[REAL_ARITH `--a + a = &0`] THEN REAL_ARITH_TAC;
 427       REWRITE_TAC[poly_mul] THEN REWRITE_TAC[NOT_CONS_NIL] THEN
 428       SPEC_TAC(`q:real list`,`q:real list`) THEN LIST_INDUCT_TAC THENL
 429        [REWRITE_TAC[poly_cmul; poly_add; NOT_CONS_NIL; HD; TL; REAL_ADD_LID];
 430         REWRITE_TAC[poly_cmul; poly_add; NOT_CONS_NIL; HD; TL; REAL_ADD_LID]]];
 431     ASM_REWRITE_TAC[] THEN REWRITE_TAC[poly];
 432     ASM_REWRITE_TAC[] THEN REWRITE_TAC[poly] THEN
 433     REWRITE_TAC[POLY_MUL] THEN REWRITE_TAC[poly] THEN
 434     REWRITE_TAC[poly; REAL_MUL_RZERO; REAL_ADD_RID; REAL_MUL_RID] THEN
 435     REWRITE_TAC[REAL_ARITH `--a + a = &0`] THEN REAL_ARITH_TAC]);;
 436
 437 (* ------------------------------------------------------------------------- *)
 438 (* Thanks to the finesse of the above, we can use length rather than degree. *)
 439 (* ------------------------------------------------------------------------- *)
 440
 441 let POLY_LENGTH_MUL = prove
 442  (`!q. LENGTH([--a; &1] ** q) = SUC(LENGTH q)`,
 443   let lemma = prove
 444    (`!p h k a. LENGTH (k ## p ++ CONS h (a ## p)) = SUC(LENGTH p)`,
 445     LIST_INDUCT_TAC THEN
 446     ASM_REWRITE_TAC[poly_cmul; POLY_ADD_CLAUSES; LENGTH]) in
 447   REWRITE_TAC[poly_mul; NOT_CONS_NIL; lemma]);;
 448
 449 (* ------------------------------------------------------------------------- *)
 450 (* Thus a nontrivial polynomial of degree n has no more than n roots.        *)
 451 (* ------------------------------------------------------------------------- *)
 452
 453 let POLY_ROOTS_INDEX_LEMMA = prove
 454  (`!n. !p. ~(poly p = poly []) /\ (LENGTH p = n)
 455            ==> ?i. !x. (poly p (x) = &0) ==> ?m. m <= n /\ (x = i m)`,
 456   INDUCT_TAC THENL
 457    [REWRITE_TAC[LENGTH_EQ_NIL] THEN MESON_TAC[];
 458     REPEAT STRIP_TAC THEN ASM_CASES_TAC `?a. poly p a = &0` THENL
 459      [UNDISCH_TAC `?a. poly p a = &0` THEN DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
 460       GEN_REWRITE_TAC LAND_CONV [POLY_LINEAR_DIVIDES] THEN
 461       DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 462       DISCH_THEN(X_CHOOSE_THEN `q:real list` SUBST_ALL_TAC) THEN
 463       FIRST_ASSUM(UNDISCH_TAC o check is_forall o concl) THEN
 464       UNDISCH_TAC `~(poly ([-- a; &1] ** q) = poly [])` THEN
 465       POP_ASSUM MP_TAC THEN REWRITE_TAC[POLY_LENGTH_MUL; SUC_INJ] THEN
 466       DISCH_TAC THEN ASM_CASES_TAC `poly q = poly []` THENL
 467        [ASM_REWRITE_TAC[POLY_MUL; poly; REAL_MUL_RZERO; FUN_EQ_THM];
 468         DISCH_THEN(K ALL_TAC)] THEN
 469       DISCH_THEN(MP_TAC o SPEC `q:real list`) THEN ASM_REWRITE_TAC[] THEN
 470       DISCH_THEN(X_CHOOSE_TAC `i:num->real`) THEN
 471       EXISTS_TAC `\m. if m = SUC n then (a:real) else i m` THEN
 472       REWRITE_TAC[POLY_MUL; LE; REAL_ENTIRE] THEN
 473       X_GEN_TAC `x:real` THEN DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
 474        [DISCH_THEN(fun th -> EXISTS_TAC `SUC n` THEN MP_TAC th) THEN
 475         REWRITE_TAC[poly] THEN REAL_ARITH_TAC;
 476         DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
 477         DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN
 478         EXISTS_TAC `m:num` THEN ASM_REWRITE_TAC[] THEN
 479         COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 480         UNDISCH_TAC `m:num <= n` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC];
 481       UNDISCH_TAC `~(?a. poly p a = &0)` THEN
 482       REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]]]);;
 483
 484 let POLY_ROOTS_INDEX_LENGTH = prove
 485  (`!p. ~(poly p = poly [])
 486        ==> ?i. !x. (poly p(x) = &0) ==> ?n. n <= LENGTH p /\ (x = i n)`,
 487   MESON_TAC[POLY_ROOTS_INDEX_LEMMA]);;
 488
 489 let POLY_ROOTS_FINITE_LEMMA = prove
 490  (`!p. ~(poly p = poly [])
 491        ==> ?N i. !x. (poly p(x) = &0) ==> ?n:num. n < N /\ (x = i n)`,
 492   MESON_TAC[POLY_ROOTS_INDEX_LENGTH; LT_SUC_LE]);;
 493
 494 let FINITE_LEMMA = prove
 495  (`!i N P. (!x. P x ==> ?n:num. n < N /\ (x = i n))
 496            ==> ?a. !x. P x ==> x < a`,
 497   GEN_TAC THEN ONCE_REWRITE_TAC[RIGHT_IMP_EXISTS_THM] THEN INDUCT_TAC THENL
 498    [REWRITE_TAC[LT] THEN MESON_TAC[]; ALL_TAC] THEN
 499   X_GEN_TAC `P:real->bool` THEN
 500   POP_ASSUM(MP_TAC o SPEC `\z. P z /\ ~(z = (i:num->real) N)`) THEN
 501   DISCH_THEN(X_CHOOSE_TAC `a:real`) THEN
 502   EXISTS_TAC `abs(a) + abs(i(N:num)) + &1` THEN
 503   POP_ASSUM MP_TAC THEN REWRITE_TAC[LT] THEN
 504   MP_TAC(REAL_ARITH `!x v. x < abs(v) + abs(x) + &1`) THEN
 505   MP_TAC(REAL_ARITH `!u v x. x < v ==> x < abs(v) + abs(u) + &1`) THEN
 506   MESON_TAC[]);;
 507
 508 let POLY_ROOTS_FINITE = prove
 509  (`!p. ~(poly p = poly []) <=>
 510        ?N i. !x. (poly p(x) = &0) ==> ?n:num. n < N /\ (x = i n)`,
 511   GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE_LEMMA] THEN
 512   REWRITE_TAC[FUN_EQ_THM; LEFT_IMP_EXISTS_THM; NOT_FORALL_THM; poly] THEN
 513   MP_TAC(GENL [`i:num->real`; `N:num`]
 514    (SPECL [`i:num->real`; `N:num`; `\x. poly p x = &0`] FINITE_LEMMA)) THEN
 515   REWRITE_TAC[] THEN MESON_TAC[REAL_LT_REFL]);;
 516
 517 (* ------------------------------------------------------------------------- *)
 518 (* Hence get entirety and cancellation for polynomials.                      *)
 519 (* ------------------------------------------------------------------------- *)
 520
 521 let POLY_ENTIRE_LEMMA = prove
 522  (`!p q. ~(poly p = poly []) /\ ~(poly q = poly [])
 523          ==> ~(poly (p ** q) = poly [])`,
 524   REPEAT GEN_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE] THEN
 525   DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
 526   DISCH_THEN(X_CHOOSE_THEN `N2:num` (X_CHOOSE_TAC `i2:num->real`)) THEN
 527   DISCH_THEN(X_CHOOSE_THEN `N1:num` (X_CHOOSE_TAC `i1:num->real`)) THEN
 528   EXISTS_TAC `N1 + N2:num` THEN
 529   EXISTS_TAC `\n:num. if n < N1 then i1(n):real else i2(n - N1)` THEN
 530   X_GEN_TAC `x:real` THEN REWRITE_TAC[REAL_ENTIRE; POLY_MUL] THEN
 531   DISCH_THEN(DISJ_CASES_THEN (ANTE_RES_THEN (X_CHOOSE_TAC `n:num`))) THENL
 532    [EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN
 533     FIRST_ASSUM(MP_TAC o CONJUNCT1) THEN ARITH_TAC;
 534     EXISTS_TAC `N1 + n:num` THEN ASM_REWRITE_TAC[LT_ADD_LCANCEL] THEN
 535     REWRITE_TAC[ARITH_RULE `~(m + n < m:num)`] THEN
 536     AP_TERM_TAC THEN ARITH_TAC]);;
 537
 538 let POLY_ENTIRE = prove
 539  (`!p q. (poly (p ** q) = poly []) <=>
 540          (poly p = poly []) \/ (poly q = poly [])`,
 541   REPEAT GEN_TAC THEN EQ_TAC THENL
 542    [MESON_TAC[POLY_ENTIRE_LEMMA];
 543     REWRITE_TAC[FUN_EQ_THM; POLY_MUL] THEN
 544     STRIP_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_MUL_LZERO; poly]]);;
 545
 546 let POLY_MUL_LCANCEL = prove
 547  (`!p q r. (poly (p ** q) = poly (p ** r)) <=>
 548            (poly p = poly []) \/ (poly q = poly r)`,
 549   let lemma1 = prove
 550    (`!p q. (poly (p ++ neg q) = poly []) <=> (poly p = poly q)`,
 551     REWRITE_TAC[FUN_EQ_THM; POLY_ADD; POLY_NEG; poly] THEN
 552     REWRITE_TAC[REAL_ARITH `(p + --q = &0) <=> (p = q)`]) in
 553   let lemma2 = prove
 554    (`!p q r. poly (p ** q ++ neg(p ** r)) = poly (p ** (q ++ neg(r)))`,
 555     REWRITE_TAC[FUN_EQ_THM; POLY_ADD; POLY_NEG; POLY_MUL] THEN
 556     REAL_ARITH_TAC) in
 557   ONCE_REWRITE_TAC[GSYM lemma1] THEN
 558   REWRITE_TAC[lemma2; POLY_ENTIRE] THEN
 559   REWRITE_TAC[lemma1]);;
 560
 561 let POLY_EXP_EQ_0 = prove
 562  (`!p n. (poly (p exp n) = poly []) <=> (poly p = poly []) /\ ~(n = 0)`,
 563   REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; poly] THEN
 564   REWRITE_TAC[LEFT_AND_FORALL_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN
 565   SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
 566   REWRITE_TAC[poly_exp; poly; REAL_MUL_RZERO; REAL_ADD_RID;
 567     REAL_OF_NUM_EQ; ARITH; NOT_SUC] THEN
 568   ASM_REWRITE_TAC[POLY_MUL; poly; REAL_ENTIRE] THEN
 569   CONV_TAC TAUT);;
 570
 571 let POLY_PRIME_EQ_0 = prove
 572  (`!a. ~(poly [a ; &1] = poly [])`,
 573   GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; poly] THEN
 574   DISCH_THEN(MP_TAC o SPEC `&1 - a`) THEN
 575   REAL_ARITH_TAC);;
 576
 577 let POLY_EXP_PRIME_EQ_0 = prove
 578  (`!a n. ~(poly ([a ; &1] exp n) = poly [])`,
 579   MESON_TAC[POLY_EXP_EQ_0; POLY_PRIME_EQ_0]);;
 580
 581 (* ------------------------------------------------------------------------- *)
 582 (* Can also prove a more "constructive" notion of polynomial being trivial.  *)
 583 (* ------------------------------------------------------------------------- *)
 584
 585 let POLY_ZERO_LEMMA = prove
 586  (`!h t. (poly (CONS h t) = poly []) ==> (h = &0) /\ (poly t = poly [])`,
 587   let lemma = REWRITE_RULE[FUN_EQ_THM; poly] POLY_ROOTS_FINITE in
 588   REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; poly] THEN
 589   ASM_CASES_TAC `h = &0` THEN ASM_REWRITE_TAC[] THENL
 590    [REWRITE_TAC[REAL_ADD_LID];
 591     DISCH_THEN(MP_TAC o SPEC `&0`) THEN
 592     POP_ASSUM MP_TAC THEN REAL_ARITH_TAC] THEN
 593   CONV_TAC CONTRAPOS_CONV THEN
 594   DISCH_THEN(MP_TAC o REWRITE_RULE[lemma]) THEN
 595   DISCH_THEN(X_CHOOSE_THEN `N:num` (X_CHOOSE_TAC `i:num->real`)) THEN
 596   MP_TAC(SPECL [`i:num->real`; `N:num`; `\x. poly t x = &0`] FINITE_LEMMA) THEN
 597   ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_TAC `a:real`) THEN
 598   DISCH_THEN(MP_TAC o SPEC `abs(a) + &1`) THEN
 599   REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM] THEN CONJ_TAC THENL
 600    [REAL_ARITH_TAC;
 601     DISCH_THEN(MP_TAC o MATCH_MP (ASSUME `!x. (poly t x = &0) ==> x < a`)) THEN
 602     REAL_ARITH_TAC]);;
 603
 604 let POLY_ZERO = prove
 605  (`!p. (poly p = poly []) <=> ALL (\c. c = &0) p`,
 606   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL] THEN EQ_TAC THENL
 607    [DISCH_THEN(MP_TAC o MATCH_MP POLY_ZERO_LEMMA) THEN ASM_REWRITE_TAC[];
 608     POP_ASSUM(SUBST1_TAC o SYM) THEN STRIP_TAC THEN
 609     ASM_REWRITE_TAC[FUN_EQ_THM; poly] THEN REAL_ARITH_TAC]);;
 610
 611 (* ------------------------------------------------------------------------- *)
 612 (* Useful triviality.                                                        *)
 613 (* ------------------------------------------------------------------------- *)
 614
 615 let POLY_DIFF_AUX_ISZERO = prove
 616  (`!p n. ALL (\c. c = &0) (poly_diff_aux (SUC n) p) <=>
 617          ALL (\c. c = &0) p`,
 618   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC
 619    [ALL; poly_diff_aux; REAL_ENTIRE; REAL_OF_NUM_EQ; NOT_SUC]);;
 620
 621 let POLY_DIFF_ISZERO = prove
 622  (`!p. (poly (diff p) = poly []) ==> ?h. poly p = poly [h]`,
 623   REWRITE_TAC[POLY_ZERO] THEN
 624   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[POLY_DIFF_CLAUSES; ALL] THENL
 625    [EXISTS_TAC `&0` THEN REWRITE_TAC[FUN_EQ_THM; poly] THEN REAL_ARITH_TAC;
 626     REWRITE_TAC[num_CONV `1`; POLY_DIFF_AUX_ISZERO] THEN
 627     REWRITE_TAC[GSYM POLY_ZERO] THEN DISCH_TAC THEN
 628     EXISTS_TAC `h:real` THEN ASM_REWRITE_TAC[poly; FUN_EQ_THM]]);;
 629
 630 let POLY_DIFF_ZERO = prove
 631  (`!p. (poly p = poly []) ==> (poly (diff p) = poly [])`,
 632   REWRITE_TAC[POLY_ZERO] THEN
 633   LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff; NOT_CONS_NIL] THEN
 634   REWRITE_TAC[ALL; TL] THEN
 635   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 636   SPEC_TAC(`1`,`n:num`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
 637   SPEC_TAC(`t:real list`,`t:real list`) THEN
 638   LIST_INDUCT_TAC THEN REWRITE_TAC[ALL; poly_diff_aux] THEN
 639   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RZERO] THEN
 640   FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 641
 642 let POLY_DIFF_WELLDEF = prove
 643  (`!p q. (poly p = poly q) ==> (poly (diff p) = poly (diff q))`,
 644   REPEAT STRIP_TAC THEN MP_TAC(SPEC `p ++ neg(q)` POLY_DIFF_ZERO) THEN
 645   REWRITE_TAC[FUN_EQ_THM; POLY_DIFF_ADD; POLY_DIFF_NEG; POLY_ADD] THEN
 646   ASM_REWRITE_TAC[POLY_NEG; poly; REAL_ARITH `a + --a = &0`] THEN
 647   REWRITE_TAC[REAL_ARITH `(a + --b = &0) <=> (a = b)`]);;
 648
 649 (* ------------------------------------------------------------------------- *)
 650 (* Basics of divisibility.                                                   *)
 651 (* ------------------------------------------------------------------------- *)
 652
 653 let divides = new_definition
 654   `p1 divides p2 <=> ?q. poly p2 = poly (p1 ** q)`;;
 655
 656 let POLY_PRIMES = prove
 657  (`!a p q. [a; &1] divides (p ** q) <=>
 658           [a; &1] divides p \/ [a; &1] divides q`,
 659   REPEAT GEN_TAC THEN REWRITE_TAC[divides; POLY_MUL; FUN_EQ_THM; poly] THEN
 660   REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_RID; REAL_MUL_RID] THEN EQ_TAC THENL
 661    [DISCH_THEN(X_CHOOSE_THEN `r:real list` (MP_TAC o SPEC `--a`)) THEN
 662     REWRITE_TAC[REAL_ENTIRE; GSYM real_sub; REAL_SUB_REFL; REAL_MUL_LZERO] THEN
 663     DISCH_THEN DISJ_CASES_TAC THENL [DISJ1_TAC; DISJ2_TAC] THEN
 664     (POP_ASSUM(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) THEN
 665      REWRITE_TAC[REAL_NEG_NEG] THEN
 666      DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC
 667         (X_CHOOSE_THEN `s:real list` SUBST_ALL_TAC)) THENL
 668       [EXISTS_TAC `[]:real list` THEN REWRITE_TAC[poly; REAL_MUL_RZERO];
 669        EXISTS_TAC `s:real list` THEN GEN_TAC THEN
 670        REWRITE_TAC[POLY_MUL; poly] THEN REAL_ARITH_TAC]);
 671     DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_TAC `s:real list`)) THEN
 672     ASM_REWRITE_TAC[] THENL
 673      [EXISTS_TAC `s ** q`; EXISTS_TAC `p ** s`] THEN
 674     GEN_TAC THEN REWRITE_TAC[POLY_MUL] THEN REAL_ARITH_TAC]);;
 675
 676 let POLY_DIVIDES_REFL = prove
 677  (`!p. p divides p`,
 678   GEN_TAC THEN REWRITE_TAC[divides] THEN EXISTS_TAC `[&1]` THEN
 679   REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly] THEN REAL_ARITH_TAC);;
 680
 681 let POLY_DIVIDES_TRANS = prove
 682  (`!p q r. p divides q /\ q divides r ==> p divides r`,
 683   REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
 684   DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
 685   DISCH_THEN(X_CHOOSE_THEN `s:real list` ASSUME_TAC) THEN
 686   DISCH_THEN(X_CHOOSE_THEN `t:real list` ASSUME_TAC) THEN
 687   EXISTS_TAC `t ** s` THEN
 688   ASM_REWRITE_TAC[FUN_EQ_THM; POLY_MUL; REAL_MUL_ASSOC]);;
 689
 690 let POLY_DIVIDES_EXP = prove
 691  (`!p m n. m <= n ==> (p exp m) divides (p exp n)`,
 692   REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
 693   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
 694   SPEC_TAC(`d:num`,`d:num`) THEN INDUCT_TAC THEN
 695   REWRITE_TAC[ADD_CLAUSES; POLY_DIVIDES_REFL] THEN
 696   MATCH_MP_TAC POLY_DIVIDES_TRANS THEN
 697   EXISTS_TAC `p exp (m + d)` THEN ASM_REWRITE_TAC[] THEN
 698   REWRITE_TAC[divides] THEN EXISTS_TAC `p:real list` THEN
 699   REWRITE_TAC[poly_exp; FUN_EQ_THM; POLY_MUL] THEN
 700   REAL_ARITH_TAC);;
 701
 702 let POLY_EXP_DIVIDES = prove
 703  (`!p q m n. (p exp n) divides q /\ m <= n ==> (p exp m) divides q`,
 704   MESON_TAC[POLY_DIVIDES_TRANS; POLY_DIVIDES_EXP]);;
 705
 706 let POLY_DIVIDES_ADD = prove
 707  (`!p q r. p divides q /\ p divides r ==> p divides (q ++ r)`,
 708   REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
 709   DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
 710   DISCH_THEN(X_CHOOSE_THEN `s:real list` ASSUME_TAC) THEN
 711   DISCH_THEN(X_CHOOSE_THEN `t:real list` ASSUME_TAC) THEN
 712   EXISTS_TAC `t ++ s` THEN
 713   ASM_REWRITE_TAC[FUN_EQ_THM; POLY_ADD; POLY_MUL] THEN
 714   REAL_ARITH_TAC);;
 715
 716 let POLY_DIVIDES_SUB = prove
 717  (`!p q r. p divides q /\ p divides (q ++ r) ==> p divides r`,
 718   REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
 719   DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
 720   DISCH_THEN(X_CHOOSE_THEN `s:real list` ASSUME_TAC) THEN
 721   DISCH_THEN(X_CHOOSE_THEN `t:real list` ASSUME_TAC) THEN
 722   EXISTS_TAC `s ++ neg(t)` THEN
 723   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
 724   REWRITE_TAC[FUN_EQ_THM; POLY_ADD; POLY_MUL; POLY_NEG] THEN
 725   DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
 726   REWRITE_TAC[REAL_ADD_LDISTRIB; REAL_MUL_RNEG] THEN
 727   ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
 728
 729 let POLY_DIVIDES_SUB2 = prove
 730  (`!p q r. p divides r /\ p divides (q ++ r) ==> p divides q`,
 731   REPEAT STRIP_TAC THEN MATCH_MP_TAC POLY_DIVIDES_SUB THEN
 732   EXISTS_TAC `r:real list` THEN ASM_REWRITE_TAC[] THEN
 733   UNDISCH_TAC `p divides (q ++ r)` THEN
 734   REWRITE_TAC[divides; POLY_ADD; FUN_EQ_THM; POLY_MUL] THEN
 735   DISCH_THEN(X_CHOOSE_TAC `s:real list`) THEN
 736   EXISTS_TAC `s:real list` THEN
 737   X_GEN_TAC `x:real` THEN POP_ASSUM(MP_TAC o SPEC `x:real`) THEN
 738   REAL_ARITH_TAC);;
 739
 740 let POLY_DIVIDES_ZERO = prove
 741  (`!p q. (poly p = poly []) ==> q divides p`,
 742   REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[divides] THEN
 743   EXISTS_TAC `[]:real list` THEN
 744   ASM_REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly; REAL_MUL_RZERO]);;
 745
 746 (* ------------------------------------------------------------------------- *)
 747 (* At last, we can consider the order of a root.                             *)
 748 (* ------------------------------------------------------------------------- *)
 749
 750 let POLY_ORDER_EXISTS = prove
 751  (`!a d. !p. (LENGTH p = d) /\ ~(poly p = poly [])
 752              ==> ?n. ([--a; &1] exp n) divides p /\
 753                      ~(([--a; &1] exp (SUC n)) divides p)`,
 754   GEN_TAC THEN
 755   (STRIP_ASSUME_TAC o prove_recursive_functions_exist num_RECURSION)
 756     `(!p q. mulexp 0 p q = q) /\
 757      (!p q n. mulexp (SUC n) p q = p ** (mulexp n p q))` THEN
 758   SUBGOAL_THEN
 759    `!d. !p. (LENGTH p = d) /\ ~(poly p = poly [])
 760            ==> ?n q. (p = mulexp (n:num) [--a; &1] q) /\
 761                      ~(poly q a = &0)`
 762   MP_TAC THENL
 763    [INDUCT_TAC THENL
 764      [REWRITE_TAC[LENGTH_EQ_NIL] THEN MESON_TAC[]; ALL_TAC] THEN
 765     X_GEN_TAC `p:real list` THEN
 766     ASM_CASES_TAC `poly p a = &0` THENL
 767      [STRIP_TAC THEN UNDISCH_TAC `poly p a = &0` THEN
 768       DISCH_THEN(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) THEN
 769       DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 770       DISCH_THEN(X_CHOOSE_THEN `q:real list` SUBST_ALL_TAC) THEN
 771       UNDISCH_TAC
 772        `!p. (LENGTH p = d) /\ ~(poly p = poly [])
 773             ==> ?n q. (p = mulexp (n:num) [--a; &1] q) /\
 774                       ~(poly q a = &0)` THEN
 775       DISCH_THEN(MP_TAC o SPEC `q:real list`) THEN
 776       RULE_ASSUM_TAC(REWRITE_RULE[POLY_LENGTH_MUL; POLY_ENTIRE;
 777         DE_MORGAN_THM; SUC_INJ]) THEN
 778       ASM_REWRITE_TAC[] THEN
 779       DISCH_THEN(X_CHOOSE_THEN `n:num`
 780        (X_CHOOSE_THEN `s:real list` STRIP_ASSUME_TAC)) THEN
 781       EXISTS_TAC `SUC n` THEN EXISTS_TAC `s:real list` THEN
 782       ASM_REWRITE_TAC[];
 783       STRIP_TAC THEN EXISTS_TAC `0` THEN EXISTS_TAC `p:real list` THEN
 784       ASM_REWRITE_TAC[]];
 785     DISCH_TAC THEN REPEAT GEN_TAC THEN
 786     DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
 787     DISCH_THEN(X_CHOOSE_THEN `n:num`
 788        (X_CHOOSE_THEN `s:real list` STRIP_ASSUME_TAC)) THEN
 789     EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN
 790     REWRITE_TAC[divides] THEN CONJ_TAC THENL
 791      [EXISTS_TAC `s:real list` THEN
 792       SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
 793       ASM_REWRITE_TAC[poly_exp; FUN_EQ_THM; POLY_MUL; poly] THEN
 794       REAL_ARITH_TAC;
 795       DISCH_THEN(X_CHOOSE_THEN `r:real list` MP_TAC) THEN
 796       SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
 797       ASM_REWRITE_TAC[] THENL
 798        [UNDISCH_TAC `~(poly s a = &0)` THEN CONV_TAC CONTRAPOS_CONV THEN
 799         REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
 800         REWRITE_TAC[poly; poly_exp; POLY_MUL] THEN REAL_ARITH_TAC;
 801         REWRITE_TAC[] THEN ONCE_ASM_REWRITE_TAC[] THEN
 802         ONCE_REWRITE_TAC[poly_exp] THEN
 803         REWRITE_TAC[GSYM POLY_MUL_ASSOC; POLY_MUL_LCANCEL] THEN
 804         REWRITE_TAC[DE_MORGAN_THM] THEN CONJ_TAC THENL
 805          [REWRITE_TAC[FUN_EQ_THM] THEN
 806           DISCH_THEN(MP_TAC o SPEC `a + &1`) THEN
 807           REWRITE_TAC[poly] THEN REAL_ARITH_TAC;
 808           DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN REWRITE_TAC[]]]]]);;
 809
 810 let POLY_ORDER = prove
 811  (`!p a. ~(poly p = poly [])
 812          ==> ?!n. ([--a; &1] exp n) divides p /\
 813                       ~(([--a; &1] exp (SUC n)) divides p)`,
 814   MESON_TAC[POLY_ORDER_EXISTS; POLY_EXP_DIVIDES; LE_SUC_LT; LT_CASES]);;
 815
 816 (* ------------------------------------------------------------------------- *)
 817 (* Definition of order.                                                      *)
 818 (* ------------------------------------------------------------------------- *)
 819
 820 let order = new_definition
 821   `order a p = @n. ([--a; &1] exp n) divides p /\
 822                    ~(([--a; &1] exp (SUC n)) divides p)`;;
 823
 824 let ORDER = prove
 825  (`!p a n. ([--a; &1] exp n) divides p /\
 826            ~(([--a; &1] exp (SUC n)) divides p) <=>
 827            (n = order a p) /\
 828            ~(poly p = poly [])`,
 829   REPEAT GEN_TAC THEN REWRITE_TAC[order] THEN
 830   EQ_TAC THEN STRIP_TAC THENL
 831    [SUBGOAL_THEN `~(poly p = poly [])` ASSUME_TAC THENL
 832      [FIRST_ASSUM(UNDISCH_TAC o check is_neg o concl) THEN
 833       CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[divides] THEN
 834       DISCH_THEN SUBST1_TAC THEN EXISTS_TAC `[]:real list` THEN
 835       REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly; REAL_MUL_RZERO];
 836       ASM_REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN
 837       MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[]];
 838     ONCE_ASM_REWRITE_TAC[] THEN CONV_TAC SELECT_CONV] THEN
 839   ASM_MESON_TAC[POLY_ORDER]);;
 840
 841 let ORDER_THM = prove
 842  (`!p a. ~(poly p = poly [])
 843          ==> ([--a; &1] exp (order a p)) divides p /\
 844              ~(([--a; &1] exp (SUC(order a p))) divides p)`,
 845   MESON_TAC[ORDER]);;
 846
 847 let ORDER_UNIQUE = prove
 848  (`!p a n. ~(poly p = poly []) /\
 849            ([--a; &1] exp n) divides p /\
 850            ~(([--a; &1] exp (SUC n)) divides p)
 851            ==> (n = order a p)`,
 852   MESON_TAC[ORDER]);;
 853
 854 let ORDER_POLY = prove
 855  (`!p q a. (poly p = poly q) ==> (order a p = order a q)`,
 856   REPEAT STRIP_TAC THEN
 857   ASM_REWRITE_TAC[order; divides; FUN_EQ_THM; POLY_MUL]);;
 858
 859 let ORDER_ROOT = prove
 860  (`!p a. (poly p a = &0) <=> (poly p = poly []) \/ ~(order a p = 0)`,
 861   REPEAT GEN_TAC THEN ASM_CASES_TAC `poly p = poly []` THEN
 862   ASM_REWRITE_TAC[poly] THEN EQ_TAC THENL
 863    [DISCH_THEN(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) THEN
 864     ASM_CASES_TAC `p:real list = []` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 865     ASM_REWRITE_TAC[] THEN
 866     DISCH_THEN(X_CHOOSE_THEN `q:real list` SUBST_ALL_TAC) THEN DISCH_TAC THEN
 867     FIRST_ASSUM(MP_TAC o SPEC `a:real` o MATCH_MP ORDER_THM) THEN
 868     ASM_REWRITE_TAC[poly_exp; DE_MORGAN_THM] THEN DISJ2_TAC THEN
 869     REWRITE_TAC[divides] THEN EXISTS_TAC `q:real list` THEN
 870     REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly] THEN REAL_ARITH_TAC;
 871     DISCH_TAC THEN
 872     FIRST_ASSUM(MP_TAC o SPEC `a:real` o MATCH_MP ORDER_THM) THEN
 873     UNDISCH_TAC `~(order a p = 0)` THEN
 874     SPEC_TAC(`order a p`,`n:num`) THEN
 875     INDUCT_TAC THEN ASM_REWRITE_TAC[poly_exp; NOT_SUC] THEN
 876     DISCH_THEN(MP_TAC o CONJUNCT1) THEN REWRITE_TAC[divides] THEN
 877     DISCH_THEN(X_CHOOSE_THEN `s:real list` SUBST1_TAC) THEN
 878     REWRITE_TAC[POLY_MUL; poly] THEN REAL_ARITH_TAC]);;
 879
 880 let ORDER_DIVIDES = prove
 881  (`!p a n. ([--a; &1] exp n) divides p <=>
 882            (poly p = poly []) \/ n <= order a p`,
 883   REPEAT GEN_TAC THEN ASM_CASES_TAC `poly p = poly []` THEN
 884   ASM_REWRITE_TAC[] THENL
 885    [ASM_REWRITE_TAC[divides] THEN EXISTS_TAC `[]:real list` THEN
 886     REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly; REAL_MUL_RZERO];
 887     ASM_MESON_TAC[ORDER_THM; POLY_EXP_DIVIDES; NOT_LE; LE_SUC_LT]]);;
 888
 889 let ORDER_DECOMP = prove
 890  (`!p a. ~(poly p = poly [])
 891          ==> ?q. (poly p = poly (([--a; &1] exp (order a p)) ** q)) /\
 892                  ~([--a; &1] divides q)`,
 893   REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP ORDER_THM) THEN
 894   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC o SPEC `a:real`) THEN
 895   DISCH_THEN(X_CHOOSE_TAC `q:real list` o REWRITE_RULE[divides]) THEN
 896   EXISTS_TAC `q:real list` THEN ASM_REWRITE_TAC[] THEN
 897   DISCH_THEN(X_CHOOSE_TAC `r: real list` o REWRITE_RULE[divides]) THEN
 898   UNDISCH_TAC `~([-- a; &1] exp SUC (order a p) divides p)` THEN
 899   ASM_REWRITE_TAC[] THEN REWRITE_TAC[divides] THEN
 900   EXISTS_TAC `r:real list` THEN
 901   ASM_REWRITE_TAC[POLY_MUL; FUN_EQ_THM; poly_exp] THEN
 902   REAL_ARITH_TAC);;
 903
 904 (* ------------------------------------------------------------------------- *)
 905 (* Important composition properties of orders.                               *)
 906 (* ------------------------------------------------------------------------- *)
 907
 908 let ORDER_MUL = prove
 909  (`!a p q. ~(poly (p ** q) = poly []) ==>
 910            (order a (p ** q) = order a p + order a q)`,
 911   REPEAT GEN_TAC THEN
 912   DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
 913   REWRITE_TAC[POLY_ENTIRE; DE_MORGAN_THM] THEN STRIP_TAC THEN
 914   SUBGOAL_THEN `(order a p + order a q = order a (p ** q)) /\
 915                 ~(poly (p ** q) = poly [])`
 916   MP_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
 917   REWRITE_TAC[GSYM ORDER] THEN CONJ_TAC THENL
 918    [MP_TAC(CONJUNCT1 (SPEC `a:real`
 919       (MATCH_MP ORDER_THM (ASSUME `~(poly p = poly [])`)))) THEN
 920     DISCH_THEN(X_CHOOSE_TAC `r: real list` o REWRITE_RULE[divides]) THEN
 921     MP_TAC(CONJUNCT1 (SPEC `a:real`
 922       (MATCH_MP ORDER_THM (ASSUME `~(poly q = poly [])`)))) THEN
 923     DISCH_THEN(X_CHOOSE_TAC `s: real list` o REWRITE_RULE[divides]) THEN
 924     REWRITE_TAC[divides; FUN_EQ_THM] THEN EXISTS_TAC `s ** r` THEN
 925     ASM_REWRITE_TAC[POLY_MUL; POLY_EXP_ADD] THEN REAL_ARITH_TAC;
 926     X_CHOOSE_THEN `r: real list` STRIP_ASSUME_TAC
 927     (SPEC `a:real` (MATCH_MP ORDER_DECOMP (ASSUME `~(poly p = poly [])`))) THEN
 928     X_CHOOSE_THEN `s: real list` STRIP_ASSUME_TAC
 929     (SPEC `a:real` (MATCH_MP ORDER_DECOMP (ASSUME `~(poly q = poly [])`))) THEN
 930     ASM_REWRITE_TAC[divides; FUN_EQ_THM; POLY_EXP_ADD; POLY_MUL; poly_exp] THEN
 931     DISCH_THEN(X_CHOOSE_THEN `t:real list` STRIP_ASSUME_TAC) THEN
 932     SUBGOAL_THEN `[--a; &1] divides (r ** s)` MP_TAC THENL
 933      [ALL_TAC; ASM_REWRITE_TAC[POLY_PRIMES]] THEN
 934     REWRITE_TAC[divides] THEN EXISTS_TAC `t:real list` THEN
 935     SUBGOAL_THEN `poly ([-- a; &1] exp (order a p) ** r ** s) =
 936                   poly ([-- a; &1] exp (order a p) ** ([-- a; &1] ** t))`
 937     MP_TAC THENL
 938      [ALL_TAC; MESON_TAC[POLY_MUL_LCANCEL; POLY_EXP_PRIME_EQ_0]] THEN
 939     SUBGOAL_THEN `poly ([-- a; &1] exp (order a q) **
 940                         [-- a; &1] exp (order a p) ** r ** s) =
 941                   poly ([-- a; &1] exp (order a q) **
 942                         [-- a; &1] exp (order a p) **
 943                         [-- a; &1] ** t)`
 944     MP_TAC THENL
 945      [ALL_TAC; MESON_TAC[POLY_MUL_LCANCEL; POLY_EXP_PRIME_EQ_0]] THEN
 946     REWRITE_TAC[FUN_EQ_THM; POLY_MUL; POLY_ADD] THEN
 947     FIRST_ASSUM(UNDISCH_TAC o check is_forall o concl) THEN
 948     REWRITE_TAC[REAL_MUL_AC]]);;
 949
 950 let ORDER_DIFF = prove
 951  (`!p a. ~(poly (diff p) = poly []) /\
 952          ~(order a p = 0)
 953          ==> (order a p = SUC (order a (diff p)))`,
 954   REPEAT GEN_TAC THEN
 955   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 956   SUBGOAL_THEN `~(poly p = poly [])` MP_TAC THENL
 957    [ASM_MESON_TAC[POLY_DIFF_ZERO]; ALL_TAC] THEN
 958   DISCH_THEN(X_CHOOSE_THEN `q:real list` MP_TAC o
 959     SPEC `a:real` o MATCH_MP ORDER_DECOMP) THEN
 960   SPEC_TAC(`order a p`,`n:num`) THEN
 961   INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; SUC_INJ] THEN
 962   STRIP_TAC THEN MATCH_MP_TAC ORDER_UNIQUE THEN
 963   ASM_REWRITE_TAC[] THEN
 964   SUBGOAL_THEN `!r. r divides (diff p) <=>
 965                     r divides (diff ([-- a; &1] exp SUC n ** q))`
 966   (fun th -> REWRITE_TAC[th]) THENL
 967    [GEN_TAC THEN REWRITE_TAC[divides] THEN
 968     FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP POLY_DIFF_WELLDEF th]);
 969     ALL_TAC] THEN
 970   CONJ_TAC THENL
 971    [REWRITE_TAC[divides; FUN_EQ_THM] THEN
 972     EXISTS_TAC `[--a; &1] ** (diff q) ++ &(SUC n) ## q` THEN
 973     REWRITE_TAC[POLY_DIFF_MUL; POLY_DIFF_EXP_PRIME;
 974       POLY_ADD; POLY_MUL; POLY_CMUL] THEN
 975     REWRITE_TAC[poly_exp; POLY_MUL] THEN REAL_ARITH_TAC;
 976     REWRITE_TAC[FUN_EQ_THM; divides; POLY_DIFF_MUL; POLY_DIFF_EXP_PRIME;
 977       POLY_ADD; POLY_MUL; POLY_CMUL] THEN
 978     DISCH_THEN(X_CHOOSE_THEN `r:real list` ASSUME_TAC) THEN
 979     UNDISCH_TAC `~([-- a; &1] divides q)` THEN
 980     REWRITE_TAC[divides] THEN
 981     EXISTS_TAC `inv(&(SUC n)) ## (r ++ neg(diff q))` THEN
 982     SUBGOAL_THEN
 983         `poly ([--a; &1] exp n ** q) =
 984          poly ([--a; &1] exp n ** ([-- a; &1] ** (inv (&(SUC n)) ##
 985                                    (r ++ neg (diff q)))))`
 986     MP_TAC THENL
 987      [ALL_TAC; MESON_TAC[POLY_MUL_LCANCEL; POLY_EXP_PRIME_EQ_0]] THEN
 988     REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `x:real` THEN
 989     SUBGOAL_THEN
 990         `!a b. (&(SUC n) * a = &(SUC n) * b) ==> (a = b)`
 991     MATCH_MP_TAC THENL
 992      [REWRITE_TAC[REAL_EQ_MUL_LCANCEL; REAL_OF_NUM_EQ; NOT_SUC]; ALL_TAC] THEN
 993     REWRITE_TAC[POLY_MUL; POLY_CMUL] THEN
 994     SUBGOAL_THEN `!a b c. &(SUC n) * a * b * inv(&(SUC n)) * c =
 995                           a * b * c`
 996     (fun th -> REWRITE_TAC[th]) THENL
 997       [REPEAT GEN_TAC THEN
 998        GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
 999        REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN
1000        AP_TERM_TAC THEN
1001        GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
1002        GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
1003        REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN
1004        MATCH_MP_TAC REAL_MUL_RINV THEN
1005        REWRITE_TAC[REAL_OF_NUM_EQ; NOT_SUC]; ALL_TAC] THEN
1006     FIRST_ASSUM(MP_TAC o SPEC `x:real`) THEN
1007     REWRITE_TAC[poly_exp; POLY_MUL; POLY_ADD; POLY_NEG] THEN
1008     REAL_ARITH_TAC]);;
1009
1010 (* ------------------------------------------------------------------------- *)
1011 (* Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').    *)
1012 (* ------------------------------------------------------------------------- *)
1013
1014 let POLY_SQUAREFREE_DECOMP_ORDER = prove
1015  (`!p q d e r s.
1016         ~(poly (diff p) = poly []) /\
1017         (poly p = poly (q ** d)) /\
1018         (poly (diff p) = poly (e ** d)) /\
1019         (poly d = poly (r ** p ++ s ** diff p))
1020         ==> !a. order a q = (if order a p = 0 then 0 else 1)`,
1021   REPEAT STRIP_TAC THEN
1022   SUBGOAL_THEN `order a p = order a q + order a d` MP_TAC THENL
1023    [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `order a (q ** d)` THEN
1024     CONJ_TAC THENL
1025      [MATCH_MP_TAC ORDER_POLY THEN ASM_REWRITE_TAC[];
1026       MATCH_MP_TAC ORDER_MUL THEN
1027       FIRST_ASSUM(fun th ->
1028         GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [SYM th]) THEN
1029       ASM_MESON_TAC[POLY_DIFF_ZERO]]; ALL_TAC] THEN
1030   ASM_CASES_TAC `order a p = 0` THEN ASM_REWRITE_TAC[] THENL
1031    [ARITH_TAC; ALL_TAC] THEN
1032   SUBGOAL_THEN `order a (diff p) =
1033                 order a e + order a d` MP_TAC THENL
1034    [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `order a (e ** d)` THEN
1035     CONJ_TAC THENL
1036      [ASM_MESON_TAC[ORDER_POLY]; ASM_MESON_TAC[ORDER_MUL]]; ALL_TAC] THEN
1037   SUBGOAL_THEN `~(poly p = poly [])` ASSUME_TAC THENL
1038    [ASM_MESON_TAC[POLY_DIFF_ZERO]; ALL_TAC] THEN
1039   MP_TAC(SPECL [`p:real list`; `a:real`] ORDER_DIFF) THEN
1040   ASM_REWRITE_TAC[] THEN
1041   DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(AP_TERM `PRE` th)) THEN
1042   REWRITE_TAC[PRE] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
1043   SUBGOAL_THEN `order a (diff p) <= order a d` MP_TAC THENL
1044    [SUBGOAL_THEN `([--a; &1] exp (order a (diff p))) divides d`
1045     MP_TAC THENL [ALL_TAC; ASM_MESON_TAC[POLY_ENTIRE; ORDER_DIVIDES]] THEN
1046     SUBGOAL_THEN
1047       `([--a; &1] exp (order a (diff p))) divides p /\
1048        ([--a; &1] exp (order a (diff p))) divides (diff p)`
1049     MP_TAC THENL
1050      [REWRITE_TAC[ORDER_DIVIDES; LE_REFL] THEN DISJ2_TAC THEN
1051       REWRITE_TAC[ASSUME `order a (diff p) = PRE (order a p)`] THEN
1052       ARITH_TAC;
1053       DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN REWRITE_TAC[divides] THEN
1054       REWRITE_TAC[ASSUME `poly d = poly (r ** p ++ s ** diff p)`] THEN
1055       POP_ASSUM_LIST(K ALL_TAC) THEN
1056       DISCH_THEN(X_CHOOSE_THEN `f:real list` ASSUME_TAC) THEN
1057       DISCH_THEN(X_CHOOSE_THEN `g:real list` ASSUME_TAC) THEN
1058       EXISTS_TAC `r ** g ++ s ** f` THEN ASM_REWRITE_TAC[] THEN
1059       ASM_REWRITE_TAC[FUN_EQ_THM; POLY_MUL; POLY_ADD] THEN ARITH_TAC];
1060     ARITH_TAC]);;
1061
1062 (* ------------------------------------------------------------------------- *)
1063 (* Define being "squarefree" --- NB with respect to real roots only.         *)
1064 (* ------------------------------------------------------------------------- *)
1065
1066 let rsquarefree = new_definition
1067   `rsquarefree p <=> ~(poly p = poly []) /\
1068                      !a. (order a p = 0) \/ (order a p = 1)`;;
1069
1070 (* ------------------------------------------------------------------------- *)
1071 (* Standard squarefree criterion and rephasing of squarefree decomposition.  *)
1072 (* ------------------------------------------------------------------------- *)
1073
1074 let RSQUAREFREE_ROOTS = prove
1075  (`!p. rsquarefree p <=> !a. ~((poly p a = &0) /\ (poly (diff p) a = &0))`,
1076   GEN_TAC THEN REWRITE_TAC[rsquarefree] THEN
1077   ASM_CASES_TAC `poly p = poly []` THEN ASM_REWRITE_TAC[] THENL
1078    [FIRST_ASSUM(SUBST1_TAC o MATCH_MP POLY_DIFF_ZERO) THEN
1079     ASM_REWRITE_TAC[poly; NOT_FORALL_THM];
1080     ASM_CASES_TAC `poly(diff p) = poly []` THEN ASM_REWRITE_TAC[] THENL
1081      [FIRST_ASSUM(X_CHOOSE_THEN `h:real` MP_TAC o
1082         MATCH_MP POLY_DIFF_ISZERO) THEN
1083       DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
1084       DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP ORDER_POLY th]) THEN
1085       UNDISCH_TAC `~(poly p = poly [])` THEN ASM_REWRITE_TAC[poly] THEN
1086       REWRITE_TAC[FUN_EQ_THM; poly; REAL_MUL_RZERO; REAL_ADD_RID] THEN
1087       DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1088       X_GEN_TAC `a:real` THEN DISJ1_TAC THEN
1089       MP_TAC(SPECL [`[h:real]`; `a:real`] ORDER_ROOT) THEN
1090       ASM_REWRITE_TAC[FUN_EQ_THM; poly; REAL_MUL_RZERO; REAL_ADD_RID];
1091       ASM_REWRITE_TAC[ORDER_ROOT; DE_MORGAN_THM; num_CONV `1`] THEN
1092       ASM_MESON_TAC[ORDER_DIFF; SUC_INJ]]]);;
1093
1094 let RSQUAREFREE_DECOMP = prove
1095  (`!p a. rsquarefree p /\ (poly p a = &0)
1096          ==> ?q. (poly p = poly ([--a; &1] ** q)) /\
1097                  ~(poly q a = &0)`,
1098   REPEAT GEN_TAC THEN REWRITE_TAC[rsquarefree] THEN STRIP_TAC THEN
1099   FIRST_ASSUM(MP_TAC o MATCH_MP ORDER_DECOMP) THEN
1100   DISCH_THEN(X_CHOOSE_THEN `q:real list` MP_TAC o SPEC `a:real`) THEN
1101   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ORDER_ROOT]) THEN
1102   FIRST_ASSUM(DISJ_CASES_TAC o SPEC `a:real`) THEN ASM_REWRITE_TAC[] THEN
1103   REWRITE_TAC[ARITH] THEN
1104   DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
1105   EXISTS_TAC `q:real list` THEN CONJ_TAC THENL
1106    [REWRITE_TAC[FUN_EQ_THM; POLY_MUL] THEN GEN_TAC THEN
1107     AP_THM_TAC THEN AP_TERM_TAC THEN
1108     GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV) [num_CONV `1`] THEN
1109     REWRITE_TAC[poly_exp; POLY_MUL] THEN
1110     REWRITE_TAC[poly] THEN REAL_ARITH_TAC;
1111     DISCH_TAC THEN UNDISCH_TAC `~([-- a; &1] divides q)` THEN
1112     REWRITE_TAC[divides] THEN
1113     UNDISCH_TAC `poly q a = &0` THEN
1114     GEN_REWRITE_TAC LAND_CONV [POLY_LINEAR_DIVIDES] THEN
1115     ASM_CASES_TAC `q:real list = []` THEN ASM_REWRITE_TAC[] THENL
1116      [EXISTS_TAC `[] : real list` THEN REWRITE_TAC[FUN_EQ_THM] THEN
1117       REWRITE_TAC[POLY_MUL; poly; REAL_MUL_RZERO];
1118       MESON_TAC[]]]);;
1119
1120 let POLY_SQUAREFREE_DECOMP = prove
1121  (`!p q d e r s.
1122         ~(poly (diff p) = poly []) /\
1123         (poly p = poly (q ** d)) /\
1124         (poly (diff p) = poly (e ** d)) /\
1125         (poly d = poly (r ** p ++ s ** diff p))
1126         ==> rsquarefree q /\ (!a. (poly q a = &0) <=> (poly p a = &0))`,
1127   REPEAT GEN_TAC THEN DISCH_THEN(fun th -> MP_TAC th THEN
1128     ASSUME_TAC(MATCH_MP POLY_SQUAREFREE_DECOMP_ORDER th)) THEN
1129   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1130   SUBGOAL_THEN `~(poly p = poly [])` ASSUME_TAC THENL
1131    [ASM_MESON_TAC[POLY_DIFF_ZERO]; ALL_TAC] THEN
1132   DISCH_THEN(ASSUME_TAC o CONJUNCT1) THEN
1133   UNDISCH_TAC `~(poly p = poly [])` THEN
1134   DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC th) THEN
1135   DISCH_THEN(fun th -> ASM_REWRITE_TAC[] THEN ASSUME_TAC th) THEN
1136   ASM_REWRITE_TAC[] THEN
1137   REWRITE_TAC[POLY_ENTIRE; DE_MORGAN_THM] THEN STRIP_TAC THEN
1138   UNDISCH_TAC `poly p = poly (q ** d)` THEN
1139   DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
1140   ASM_REWRITE_TAC[rsquarefree; ORDER_ROOT] THEN
1141   CONJ_TAC THEN GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[ARITH]);;
1142
1143 (* ------------------------------------------------------------------------- *)
1144 (* Normalization of a polynomial.                                            *)
1145 (* ------------------------------------------------------------------------- *)
1146
1147 let normalize = new_recursive_definition list_RECURSION
1148   `(normalize [] = []) /\
1149    (normalize (CONS h t) =
1150       if normalize t = [] then if h = &0 then [] else [h]
1151                           else CONS h (normalize t))`;;
1152
1153 let POLY_NORMALIZE = prove
1154  (`!p. poly (normalize p) = poly p`,
1155   LIST_INDUCT_TAC THEN REWRITE_TAC[normalize; poly] THEN
1156   ASM_CASES_TAC `h = &0` THEN ASM_REWRITE_TAC[] THEN
1157   COND_CASES_TAC THEN ASM_REWRITE_TAC[poly; FUN_EQ_THM] THEN
1158   UNDISCH_TAC `poly (normalize t) = poly t` THEN
1159   DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[poly] THEN
1160   REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID]);;
1161
1162 (* ------------------------------------------------------------------------- *)
1163 (* The degree of a polynomial.                                               *)
1164 (* ------------------------------------------------------------------------- *)
1165
1166 let degree = new_definition
1167   `degree p = PRE(LENGTH(normalize p))`;;
1168
1169 let DEGREE_ZERO = prove
1170  (`!p. (poly p = poly []) ==> (degree p = 0)`,
1171   REPEAT STRIP_TAC THEN REWRITE_TAC[degree] THEN
1172   SUBGOAL_THEN `normalize p = []` SUBST1_TAC THENL
1173    [POP_ASSUM MP_TAC THEN SPEC_TAC(`p:real list`,`p:real list`) THEN
1174     REWRITE_TAC[POLY_ZERO] THEN
1175     LIST_INDUCT_TAC THEN REWRITE_TAC[normalize; ALL] THEN
1176     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1177     SUBGOAL_THEN `normalize t = []` (fun th -> REWRITE_TAC[th]) THEN
1178     FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1179     REWRITE_TAC[LENGTH; PRE]]);;
1180
1181 (* ------------------------------------------------------------------------- *)
1182 (* Tidier versions of finiteness of roots.                                   *)
1183 (* ------------------------------------------------------------------------- *)
1184
1185 let POLY_ROOTS_FINITE_SET = prove
1186  (`!p. ~(poly p = poly []) ==> FINITE { x | poly p x = &0}`,
1187   GEN_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE] THEN
1188   DISCH_THEN(X_CHOOSE_THEN `N:num` MP_TAC) THEN
1189   DISCH_THEN(X_CHOOSE_THEN `i:num->real` ASSUME_TAC) THEN
1190   MATCH_MP_TAC FINITE_SUBSET THEN
1191   EXISTS_TAC `{x:real | ?n:num. n < N /\ (x = i n)}` THEN
1192   CONJ_TAC THENL
1193    [SPEC_TAC(`N:num`,`N:num`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
1194     INDUCT_TAC THENL
1195      [SUBGOAL_THEN `{x:real | ?n. n < 0 /\ (x = i n)} = {}`
1196       (fun th -> REWRITE_TAC[th; FINITE_RULES]) THEN
1197       REWRITE_TAC[EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY; LT];
1198       SUBGOAL_THEN `{x:real | ?n. n < SUC N /\ (x = i n)} =
1199                     (i N) INSERT {x:real | ?n. n < N /\ (x = i n)}`
1200       SUBST1_TAC THENL
1201        [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; LT] THEN MESON_TAC[];
1202         MATCH_MP_TAC(CONJUNCT2 FINITE_RULES) THEN ASM_REWRITE_TAC[]]];
1203     ASM_REWRITE_TAC[SUBSET; IN_ELIM_THM]]);;
1204
1205 (* ------------------------------------------------------------------------- *)
1206 (* Crude bound for polynomial.                                               *)
1207 (* ------------------------------------------------------------------------- *)
1208
1209 let POLY_MONO = prove
1210  (`!x k p. abs(x) <= k ==> abs(poly p x) <= poly (MAP abs p) k`,
1211   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1212   DISCH_TAC THEN LIST_INDUCT_TAC THEN
1213   REWRITE_TAC[poly; REAL_LE_REFL; MAP; REAL_ABS_0] THEN
1214   MATCH_MP_TAC REAL_LE_TRANS THEN
1215   EXISTS_TAC `abs(h) + abs(x * poly t x)` THEN
1216   REWRITE_TAC[REAL_ABS_TRIANGLE; REAL_LE_LADD] THEN
1217   REWRITE_TAC[REAL_ABS_MUL] THEN
1218   MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[REAL_ABS_POS]);;
1219
1220 (* ------------------------------------------------------------------------- *)
1221 (* Conversions to perform operations if coefficients are rational constants. *)
1222 (* ------------------------------------------------------------------------- *)
1223
1224 let POLY_DIFF_CONV =
1225   let aux_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 poly_diff_aux]
1226   and aux_conv1 = GEN_REWRITE_CONV I [CONJUNCT2 poly_diff_aux]
1227   and diff_conv0 = GEN_REWRITE_CONV I (butlast (CONJUNCTS POLY_DIFF_CLAUSES))
1228   and diff_conv1 = GEN_REWRITE_CONV I [last (CONJUNCTS POLY_DIFF_CLAUSES)] in
1229   let rec POLY_DIFF_AUX_CONV tm =
1230    (aux_conv0 ORELSEC
1231     (aux_conv1 THENC
1232      LAND_CONV REAL_RAT_MUL_CONV THENC
1233      RAND_CONV (LAND_CONV NUM_SUC_CONV THENC POLY_DIFF_AUX_CONV))) tm in
1234   diff_conv0 ORELSEC
1235   (diff_conv1 THENC POLY_DIFF_AUX_CONV);;
1236
1237 let POLY_CMUL_CONV =
1238   let cmul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 poly_cmul]
1239   and cmul_conv1 = GEN_REWRITE_CONV I [CONJUNCT2 poly_cmul] in
1240   let rec POLY_CMUL_CONV tm =
1241    (cmul_conv0 ORELSEC
1242     (cmul_conv1 THENC
1243      LAND_CONV REAL_RAT_MUL_CONV THENC
1244      RAND_CONV POLY_CMUL_CONV)) tm in
1245   POLY_CMUL_CONV;;
1246
1247 let POLY_ADD_CONV =
1248   let add_conv0 = GEN_REWRITE_CONV I (butlast (CONJUNCTS POLY_ADD_CLAUSES))
1249   and add_conv1 = GEN_REWRITE_CONV I [last (CONJUNCTS POLY_ADD_CLAUSES)] in
1250   let rec POLY_ADD_CONV tm =
1251    (add_conv0 ORELSEC
1252     (add_conv1 THENC
1253      LAND_CONV REAL_RAT_ADD_CONV THENC
1254      RAND_CONV POLY_ADD_CONV)) tm in
1255   POLY_ADD_CONV;;
1256
1257 let POLY_MUL_CONV =
1258   let mul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 POLY_MUL_CLAUSES]
1259   and mul_conv1 = GEN_REWRITE_CONV I [CONJUNCT1(CONJUNCT2 POLY_MUL_CLAUSES)]
1260   and mul_conv2 = GEN_REWRITE_CONV I [CONJUNCT2(CONJUNCT2 POLY_MUL_CLAUSES)] in
1261   let rec POLY_MUL_CONV tm =
1262    (mul_conv0 ORELSEC
1263     (mul_conv1 THENC POLY_CMUL_CONV) ORELSEC
1264     (mul_conv2 THENC
1265      LAND_CONV POLY_CMUL_CONV THENC
1266      RAND_CONV(RAND_CONV POLY_MUL_CONV) THENC
1267      POLY_ADD_CONV)) tm in
1268   POLY_MUL_CONV;;
1269
1270 let POLY_NORMALIZE_CONV =
1271   let pth = prove
1272    (`normalize (CONS h t) =
1273       (\n. if n = [] then if h = &0 then [] else [h] else CONS h n)
1274       (normalize t)`,
1275     REWRITE_TAC[normalize]) in
1276   let norm_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 normalize]
1277   and norm_conv1 = GEN_REWRITE_CONV I [pth]
1278   and norm_conv2 = GEN_REWRITE_CONV DEPTH_CONV
1279    [COND_CLAUSES; NOT_CONS_NIL; EQT_INTRO(SPEC_ALL EQ_REFL)] in
1280   let rec POLY_NORMALIZE_CONV tm =
1281    (norm_conv0 ORELSEC
1282     (norm_conv1 THENC
1283      RAND_CONV POLY_NORMALIZE_CONV THENC
1284      BETA_CONV THENC
1285      RATOR_CONV(RAND_CONV(RATOR_CONV(LAND_CONV REAL_RAT_EQ_CONV))) THENC
1286      norm_conv2)) tm in
1287   POLY_NORMALIZE_CONV;;
1288
1289 (* ------------------------------------------------------------------------- *)
1290 (* Some theorems asserting that operations give non-nil results.             *)
1291 (* ------------------------------------------------------------------------- *)
1292
1293 let NOT_POLY_CMUL_NIL = prove
1294  (`!h p. ~(p = []) ==> ~((h ## p) = [])`,
1295   STRIP_TAC THEN LIST_INDUCT_TAC THENL
1296    [SIMP_TAC[]; SIMP_TAC[poly_cmul; NOT_CONS_NIL]]);;
1297
1298 let NOT_POLY_MUL_NIL = prove
1299  (`!p1 p2. ~(p1 = []) /\ ~(p2 = []) ==> ~((p1 ** p2) = [])`,
1300   LIST_INDUCT_TAC THENL
1301    [SIMP_TAC[];
1302     LIST_INDUCT_TAC THENL
1303      [SIMP_TAC[];
1304       SIMP_TAC[poly_mul;NOT_CONS_NIL] THEN
1305       SPEC_TAC (`t:(real)list`,`t:(real)list`) THEN LIST_INDUCT_TAC THENL
1306        [SIMP_TAC[poly_cmul;NOT_CONS_NIL];
1307         SIMP_TAC[poly_cmul;poly_add;NOT_CONS_NIL]]
1308      ]
1309    ]);;
1310
1311 let NOT_POLY_EXP_NIL =  prove
1312  (`!n p . ~(p = []) ==> ~((poly_exp p n) = [])`,
1313   let lem001 = ASSUME `!p . ~(p = []) ==> ~(poly_exp p n = [])` in
1314   let lem002 = SIMP_RULE[NOT_CONS_NIL] (SPEC `CONS (h:real) t` lem001) in
1315   INDUCT_TAC THENL
1316    [SIMP_TAC[poly_exp;NOT_CONS_NIL];
1317     LIST_INDUCT_TAC THENL
1318      [SIMP_TAC[];
1319       SIMP_TAC[lem002;NOT_POLY_MUL_NIL;poly_exp;NOT_CONS_NIL]
1320      ]
1321    ]);;
1322
1323 let NOT_POLY_EXP_X_NIL = prove
1324  (`!n. ~((poly_exp [&0;&1] n) = [])`,
1325   let lem01 = prove(`~([&0;&1] = [])`,SIMP_TAC[NOT_CONS_NIL]) in
1326   INDUCT_TAC THENL
1327    [SIMP_TAC[poly_exp;NOT_CONS_NIL];
1328     ASM_SIMP_TAC[poly_exp;NOT_POLY_MUL_NIL;lem01]]);;
1329
1330 (* ------------------------------------------------------------------------- *)
1331 (* Some general lemmas.                                                      *)
1332 (* ------------------------------------------------------------------------- *)
1333
1334 let POLY_CMUL_LID = prove
1335  (`!p. &1 ## p = p`,
1336   LIST_INDUCT_TAC THENL
1337    [SIMP_TAC[poly_cmul];
1338     ASM_SIMP_TAC[poly_cmul] THEN SIMP_TAC[REAL_ARITH `&1 * h = h`]]);;
1339
1340 let POLY_MUL_LID = prove
1341  (`!p. [&1] ** p = p`,
1342   LIST_INDUCT_TAC THENL
1343    [SIMP_TAC[poly_mul;poly_cmul];
1344     ONCE_REWRITE_TAC[poly_mul] THEN SIMP_TAC[POLY_CMUL_LID]]);;
1345
1346 let POLY_MUL_RID = prove
1347  (`!p. p ** [&1] = p`,
1348   LIST_INDUCT_TAC THENL
1349    [SIMP_TAC[poly_mul];
1350     ASM_CASES_TAC `t:(real)list = []` THEN
1351     ASM_SIMP_TAC[poly_mul;poly_cmul;poly_add;NOT_CONS_NIL;HD;TL;
1352      REAL_ARITH `h + (real_of_num 0) = h`;REAL_ARITH `h * (real_of_num 1) = h`]
1353    ]);;
1354
1355 let POLY_ADD_SYM = prove
1356  (`!x y . x ++ y = y ++ x`,
1357   let lem1 = ASSUME `!y . t ++ y = y ++ t` in
1358   let lem2 = SPEC `t':(real)list` lem1 in
1359   LIST_INDUCT_TAC THENL
1360    [LIST_INDUCT_TAC THENL [SIMP_TAC[poly_add]; SIMP_TAC[poly_add]];
1361     LIST_INDUCT_TAC THENL
1362       [SIMP_TAC[poly_add];
1363        SIMP_TAC[POLY_ADD_CLAUSES] THEN
1364        ONCE_REWRITE_TAC[lem2] THEN
1365        SIMP_TAC[SPECL [`h:real`;`h':real`] REAL_ADD_SYM]
1366       ]
1367    ]);;
1368
1369 let POLY_ADD_ASSOC = prove
1370  (`!x y z . x ++ (y ++ z) = (x ++ y) ++ z`,
1371   let lem1 = ASSUME `!y z. t ++ y ++ z = (t ++ y) ++ z` in
1372   let lem2 = SPECL [`t':(real)list`;`t'':(real)list`] lem1 in
1373   LIST_INDUCT_TAC THENL
1374    [SIMP_TAC[POLY_ADD_CLAUSES];
1375     LIST_INDUCT_TAC THENL
1376      [SIMP_TAC[POLY_ADD_CLAUSES];
1377       LIST_INDUCT_TAC THENL
1378       [SIMP_TAC[POLY_ADD_CLAUSES];
1379        SIMP_TAC[POLY_ADD_CLAUSES] THEN
1380        SIMP_TAC[REAL_ADD_ASSOC] THEN
1381        SIMP_TAC[lem2]
1382       ]
1383      ]
1384    ]);;
1385
1386 (* ------------------------------------------------------------------------- *)
1387 (* Heads and tails resulting from operations.                                *)
1388 (* ------------------------------------------------------------------------- *)
1389
1390 let TL_POLY_MUL_X = prove
1391  (`!p. TL ([&0;&1] ** p) = p`,
1392   LIST_INDUCT_TAC THENL
1393    [ONCE_REWRITE_TAC[poly_mul] THEN
1394     SIMP_TAC[NOT_CONS_NIL;poly_cmul;poly_add;TL;poly_mul];
1395     ONCE_REWRITE_TAC[poly_mul] THEN SIMP_TAC[NOT_CONS_NIL] THEN
1396     ONCE_REWRITE_TAC[poly_cmul] THEN ONCE_REWRITE_TAC[poly_add] THEN
1397     SIMP_TAC[NOT_CONS_NIL] THEN SIMP_TAC[TL;POLY_MUL_LID] THEN
1398     SPEC_TAC (`h:real`,`h:real`) THEN
1399     SPEC_TAC (`t:(real)list`,`t:(real)list`) THEN
1400     LIST_INDUCT_TAC THENL
1401      [SIMP_TAC[poly_cmul;poly_add];
1402       ASM_SIMP_TAC[poly_cmul;poly_add;NOT_CONS_NIL;HD;TL;
1403                    REAL_ARITH `(&0) * h + h' = h'`]
1404      ]
1405    ]);;
1406
1407 let HD_POLY_MUL_X = prove
1408  (`!p. HD ([&0;&1] ** p) = &0`,
1409   LIST_INDUCT_TAC THEN
1410   SIMP_TAC[poly_mul;NOT_CONS_NIL;poly_cmul;poly_add;HD;
1411            REAL_ARITH `&0 * h + &0 = &0`]);;
1412
1413 let TL_POLY_EXP_X_SUC = prove
1414  (`!n . TL (poly_exp [&0;&1] (SUC n)) = poly_exp [&0;&1] n`,
1415    SIMP_TAC[poly_exp;TL_POLY_MUL_X]);;
1416
1417 let HD_POLY_EXP_X_SUC = prove
1418  (`!n . HD (poly_exp [&0;&1] (SUC n)) = &0`,
1419   INDUCT_TAC THENL
1420    [SIMP_TAC[poly_exp;poly_add;HD;TL;poly_cmul;poly_mul;NOT_CONS_NIL;
1421              REAL_ARITH `&0 * &1 + &0 = &0`];
1422     SIMP_TAC[poly_exp;HD_POLY_MUL_X]]);;
1423
1424 let HD_POLY_ADD = prove
1425  (`!p1 p2. ~(p1 = []) /\ ~(p2 = []) ==> HD (p1 ++ p2) = (HD p1) + (HD p2)`,
1426    LIST_INDUCT_TAC THENL
1427     [SIMP_TAC[];
1428       LIST_INDUCT_TAC THENL
1429        [SIMP_TAC[];
1430         SIMP_TAC[NOT_CONS_NIL;poly_add] THEN
1431         ONCE_REWRITE_TAC[ISPECL [`h':real`;`t':(real)list`] NOT_CONS_NIL] THEN
1432         SIMP_TAC[HD]
1433        ]
1434     ]);;
1435
1436 let HD_POLY_CMUL = prove
1437  (`!x p . ~(p = []) ==> HD (x ## p) = x * (HD p)`,
1438   STRIP_TAC THEN LIST_INDUCT_TAC THENL
1439    [SIMP_TAC[]; SIMP_TAC[NOT_CONS_NIL;poly_cmul;HD]]);;
1440
1441 let TL_POLY_CMUL = prove
1442  (`!x p . ~(p = []) ==> TL (x ## p) = x ## (TL p)`,
1443   STRIP_TAC THEN LIST_INDUCT_TAC THENL
1444    [SIMP_TAC[]; SIMP_TAC[NOT_CONS_NIL;poly_cmul;TL]]);;
1445
1446 let HD_POLY_MUL = prove
1447  (`!p1 p2 . ~(p1 = []) /\ ~(p2 = [])  ==> HD (p1 ** p2) = (HD p1) * (HD p2)`,
1448   LIST_INDUCT_TAC THENL
1449    [SIMP_TAC[];
1450     LIST_INDUCT_TAC THENL
1451      [SIMP_TAC[];
1452       SIMP_TAC[NOT_CONS_NIL;poly_mul] THEN
1453       ASM_CASES_TAC `(t:(real)list) = []` THENL
1454        [ASM_SIMP_TAC[poly_cmul;HD];
1455         ASM_SIMP_TAC[poly_cmul;poly_add;NOT_CONS_NIL;HD] THEN REAL_ARITH_TAC
1456        ]
1457      ]
1458    ]);;
1459
1460 let HD_POLY_EXP = prove
1461  (`!n p . ~(p = []) ==> HD (poly_exp p n) = (HD p) pow n`,
1462   INDUCT_TAC THENL
1463    [SIMP_TAC[poly_exp] THEN LIST_INDUCT_TAC THENL
1464      [SIMP_TAC[]; SIMP_TAC[HD;pow]];
1465     SIMP_TAC[poly_exp] THEN LIST_INDUCT_TAC THENL
1466      [SIMP_TAC[];
1467       SIMP_TAC[HD;GSYM pow;NOT_CONS_NIL;poly_mul] THEN
1468       ASM_CASES_TAC `(t:(real)list) = []` THENL
1469        [ASM_SIMP_TAC[HD_POLY_CMUL;NOT_POLY_CMUL_NIL;NOT_POLY_EXP_NIL;
1470                      NOT_CONS_NIL;HD;GSYM pow];
1471         ASM_SIMP_TAC[NOT_POLY_CMUL_NIL;NOT_POLY_EXP_NIL;NOT_CONS_NIL;
1472                      HD_POLY_ADD;HD;HD_POLY_CMUL;GSYM pow] THEN
1473         REAL_ARITH_TAC]
1474      ]
1475    ]);;
1476
1477 (* ------------------------------------------------------------------------- *)
1478 (* Additional general lemmas.                                                *)
1479 (* ------------------------------------------------------------------------- *)
1480
1481 let POLY_ADD_IDENT = prove
1482  (`neutral (++) = []`,
1483   let l1 = ASSUME `!x. (!y. x ++ y = y /\ y ++ x = y)
1484                      ==> (!y. (CONS h t) ++ y = y /\ y ++ (CONS h t) = y)` in
1485   let l2 = SPEC `[]:(real)list` l1 in
1486   let l3 = SIMP_RULE[POLY_ADD_CLAUSES] l2 in
1487   let l4 = SPEC `[]:(real)list` l3 in
1488   let l5 = CONJUNCT1 l4 in
1489   let l6 = SIMP_RULE[POLY_ADD_CLAUSES;NOT_CONS_NIL] l5 in
1490   let l7 = NOT_INTRO (DISCH_ALL l6) in
1491   ONCE_REWRITE_TAC[neutral] THEN SELECT_ELIM_TAC THEN LIST_INDUCT_TAC THENL
1492   [SIMP_TAC[];SIMP_TAC[l7]]);;
1493
1494 let POLY_ADD_NEUTRAL = prove
1495  (`!x. neutral (++) ++ x = x`,
1496   SIMP_TAC[POLY_ADD_IDENT;POLY_ADD_CLAUSES]);;
1497
1498 let MONOIDAL_POLY_ADD = prove
1499  (`monoidal poly_add`,
1500   let lem1 = CONJ POLY_ADD_SYM (CONJ POLY_ADD_ASSOC  POLY_ADD_NEUTRAL) in
1501   ONCE_REWRITE_TAC[monoidal] THEN ACCEPT_TAC lem1);;
1502
1503 let POLY_DIFF_AUX_ADD_LEMMA = prove
1504  (`!t1 t2 n. poly_diff_aux n (t1 ++ t2) =
1505              (poly_diff_aux n t1) ++ (poly_diff_aux n t2)`,
1506   let lem = REAL_ARITH `!n h h'. (&n * h) + (&n * h') = &n * (h + h')` in
1507   LIST_INDUCT_TAC THEN SIMP_TAC[POLY_ADD_CLAUSES;poly_diff_aux] THEN
1508   LIST_INDUCT_TAC THEN SIMP_TAC[POLY_ADD_CLAUSES;poly_diff_aux] THEN
1509   STRIP_TAC THEN
1510   ONCE_REWRITE_TAC[POLY_ADD_CLAUSES] THEN
1511   ONCE_REWRITE_TAC[poly_diff_aux] THEN
1512   ONCE_REWRITE_TAC[POLY_ADD_CLAUSES] THEN
1513   ONCE_REWRITE_TAC[lem] THEN
1514   ASM_SIMP_TAC[]);;
1515
1516 let POLYDIFF_ADD = prove
1517  (`!p1 p2. (poly_diff (p1 ++ p2)) = (poly_diff p1  ++ poly_diff p2)`,
1518   let lem1 = prove
1519    (`!h0 t0 h1 t1. ~(((CONS h0 t0) ++ (CONS h1 t1)) = [])`,
1520      SIMP_TAC[POLY_ADD_CLAUSES;NOT_CONS_NIL]) in
1521   let lem2 = prove
1522    (`!h0 t0 h1 t1.
1523           (TL ((CONS h0 t0) ++ (CONS h1 t1))
1524         = (TL (CONS h0 t0)) ++ (TL (CONS h1 t1)))`,
1525     REPEAT STRIP_TAC THEN REWRITE_TAC[poly_add] THEN
1526     ONCE_REWRITE_TAC[NOT_CONS_NIL] THEN REWRITE_TAC[TL]
1527     THEN SIMP_TAC[]) in
1528   REPEAT LIST_INDUCT_TAC THENL
1529    [SIMP_TAC[poly_add;poly_diff];
1530     SIMP_TAC[poly_add;poly_diff];
1531     SIMP_TAC[poly_add;poly_diff;POLY_ADD_CLAUSES];
1532     SIMP_TAC[poly_diff] THEN
1533     ONCE_REWRITE_TAC[lem1;NOT_CONS_NIL] THEN
1534     SIMP_TAC[lem2;POLY_DIFF_AUX_ADD_LEMMA]
1535    ]);;
1536
1537 let POLY_DIFF_AUX_POLY_CMUL =  prove
1538  (`!p c n. poly_diff_aux n (c ## p) = c ## (poly_diff_aux n p)`,
1539   let lem01 = ASSUME
1540    `!c n. poly_diff_aux n (c ## t) = c ## poly_diff_aux n t` in
1541   let lem02 = SPECL [`c:real`;`SUC n`] lem01 in
1542   LIST_INDUCT_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
1543   SIMP_TAC[poly_cmul;poly_diff_aux;lem02;
1544            REAL_ARITH `(a:real) * b * c = b * a * c`]);;
1545
1546 let POLY_CMUL_POLY_DIFF = prove
1547  (`!p c. poly_diff (c ## p) = c ## (poly_diff p)`,
1548   LIST_INDUCT_TAC THEN
1549   SIMP_TAC[poly_diff;POLY_DIFF_AUX_POLY_CMUL;TL_POLY_CMUL;
1550            poly_cmul;NOT_CONS_NIL]);;
1551
1552 (* ------------------------------------------------------------------------- *)
1553 (* Theorems about the lengths of lists from the polynomial operations.       *)
1554 (* ------------------------------------------------------------------------- *)
1555
1556 let POLY_CMUL_LENGTH = prove
1557  (`!c p. LENGTH (c ## p) =  LENGTH p`,
1558   STRIP_TAC THEN LIST_INDUCT_TAC THENL
1559    [SIMP_TAC[poly_cmul];
1560     SIMP_TAC[poly_cmul] THEN ASM_SIMP_TAC[LENGTH]
1561    ]);;
1562
1563 let POLY_ADD_LENGTH = prove
1564  (`!p q. LENGTH (p ++ q) =  MAX (LENGTH p) (LENGTH q)`,
1565   LIST_INDUCT_TAC THENL
1566    [SIMP_TAC[poly_add;LENGTH] THEN ARITH_TAC;
1567     LIST_INDUCT_TAC THENL
1568      [SIMP_TAC[poly_add;LENGTH] THEN ARITH_TAC;
1569       SIMP_TAC[poly_add;LENGTH] THEN
1570       ONCE_REWRITE_TAC[NOT_CONS_NIL] THEN SIMP_TAC[HD;TL;LENGTH] THEN
1571       ASM_SIMP_TAC[] THEN
1572       ONCE_REWRITE_TAC[ARITH_RULE `MAX x y = if (x > y) then x else y`] THEN
1573       ASM_CASES_TAC `LENGTH (t:(real)list) > LENGTH (t':(real)list)` THENL
1574        [ASM_SIMP_TAC[ARITH_RULE `x > y ==> (SUC x) > (SUC y)`];
1575         ASM_SIMP_TAC[ARITH_RULE `~(x > y) ==> ~((SUC x) > (SUC y))`]]
1576      ]
1577    ]);;
1578
1579 let POLY_MUL_LENGTH = prove
1580  (`!p h t. LENGTH (p ** (CONS h t)) >= LENGTH p`,
1581   let lemma01 = ASSUME `!h t'. LENGTH (t ** CONS h t') >= LENGTH t` in
1582   let lemma02 = SPECL [`h':real`;`t':(real)list`] lemma01 in
1583   let lemma03 = ONCE_REWRITE_RULE[ARITH_RULE `(x:num) >= y <=> SUC x >= SUC y`]
1584      lemma02 in
1585   let lemma05 = ARITH_RULE `(y:num) >= z ==> (x + (y - x) >= z) ` in
1586   let lemma06 = SPECL [`SUC (LENGTH (t ** (CONS (h':real) t')))`;
1587                        `LENGTH (h ## (CONS h' t'))`;
1588                        `SUC (LENGTH (t:(real)list))`] (GEN_ALL lemma05) in
1589   let lemma07 = MATCH_MP (lemma06) (lemma03) in
1590   LIST_INDUCT_TAC THENL
1591    [SIMP_TAC[POLY_MUL_CLAUSES] THEN ARITH_TAC;
1592     SIMP_TAC[poly_mul] THEN ASM_CASES_TAC `(t:(real)list) = []` THENL
1593      [ASM_SIMP_TAC[POLY_CMUL_LENGTH;LENGTH] THEN ARITH_TAC;
1594       ASM_SIMP_TAC[POLY_ADD_LENGTH;LENGTH;lemma07;
1595                    ARITH_RULE `!x y. (MAX x y) = x + (y - x)`]
1596      ]
1597    ]);;
1598
1599 let POLY_EXP_X_REC = prove
1600  (`!n. poly_exp [&0;&1] (SUC n) = CONS (&0) (poly_exp [&0;&1] n)`,
1601   let lem01 = MATCH_MP CONS_HD_TL  (SPEC `(SUC n)` NOT_POLY_EXP_X_NIL)  in
1602   let lem02 = ONCE_REWRITE_RULE[HD_POLY_EXP_X_SUC; TL_POLY_EXP_X_SUC] lem01 in
1603   ACCEPT_TAC (GEN_ALL lem02));;
1604
1605 let POLY_MUL_LENGTH2 = prove
1606  (`!q p. ~(q = []) ==> LENGTH (p ** q) >= LENGTH p`,
1607    LIST_INDUCT_TAC THEN SIMP_TAC[NOT_CONS_NIL; POLY_MUL_LENGTH]);;
1608
1609 let POLY_EXP_X_LENGTH = prove
1610  (`!n. LENGTH (poly_exp [&0;&1] n) = SUC n`,
1611   INDUCT_TAC THEN
1612   ASM_SIMP_TAC[poly_exp;LENGTH; POLY_EXP_X_REC;
1613                ARITH_RULE `(SUC x) = (SUC y) <=> x = y`]);;
1614
1615 (* ------------------------------------------------------------------------- *)
1616 (* Expansion of a polynomial as a power sum.                                 *)
1617 (* ------------------------------------------------------------------------- *)
1618
1619 let POLY_SUM_EQUIV = prove
1620  (`!p x.
1621      ~(p = []) ==>
1622      poly p x = sum (0..(PRE (LENGTH p))) (\i. (EL i p)*(x pow i))`,
1623   let lem000 = ARITH_RULE `0 <= 0 + 1 /\ 0 <= (LENGTH (t:(real)list))` in
1624   let lem001 = SPECL
1625                  [`f:num->real`;`0`;`0`;`LENGTH (t:(real)list)`]
1626                  SUM_COMBINE_R in
1627   let lem002 = MP lem001 lem000 in
1628   let lem003 = SPECL
1629                  [`f:num->real`;`1`;`LENGTH (t:(real)list)`]
1630                  SUM_OFFSET_0 in
1631   let lem004 = ASSUME `~((t:(real)list) = [])` in
1632   let lem005 = ONCE_REWRITE_RULE[GSYM LENGTH_EQ_NIL] lem004 in
1633   let lem006 = ONCE_REWRITE_RULE[ARITH_RULE `~(x = 0) <=> (1 <= x)`] lem005 in
1634   let lem007 = MP lem003 lem006 in
1635   let lem017 = ARITH_RULE `1 <= (LENGTH (t:(real)list))
1636                        ==> ((LENGTH t) - 1 = PRE (LENGTH t))` in
1637   let lem018 = MP lem017 lem006 in
1638   LIST_INDUCT_TAC THENL
1639     [     SIMP_TAC[NOT_CONS_NIL]
1640           ;
1641           ASM_CASES_TAC `(t:(real)list) = []` THENL
1642      [
1643           ASM_SIMP_TAC[POLY_CONST;LENGTH;PRE]
1644      THEN ONCE_REWRITE_TAC[NUMSEG_CONV `0..0`]
1645      THEN ONCE_REWRITE_TAC[SUM_SING]
1646      THEN BETA_TAC
1647      THEN ONCE_REWRITE_TAC[EL]
1648      THEN ONCE_REWRITE_TAC[HD]
1649      THEN REAL_ARITH_TAC
1650      ;
1651           ASM_SIMP_TAC[POLY_CONST;LENGTH;PRE]
1652      THEN ONCE_REWRITE_TAC[poly]
1653      THEN ONCE_REWRITE_TAC[GSYM lem002]
1654      THEN ONCE_REWRITE_TAC[ARITH_RULE `0 + 1 = 1`]
1655      THEN ONCE_REWRITE_TAC[NUMSEG_CONV `0..0`]
1656      THEN ONCE_REWRITE_TAC[SUM_SING]
1657      THEN BETA_TAC
1658      THEN SIMP_TAC[EL;HD]
1659      THEN ONCE_REWRITE_TAC[lem007]
1660      THEN BETA_TAC
1661      THEN ONCE_REWRITE_TAC[GSYM ADD1]
1662      THEN SIMP_TAC[EL;TL]
1663      THEN ONCE_REWRITE_TAC[real_pow]
1664      THEN ONCE_REWRITE_TAC[REAL_MUL_RID]
1665      THEN ONCE_REWRITE_TAC[REAL_ARITH `(A:real) * B * C = B * (A * C)`]
1666      THEN ONCE_REWRITE_TAC[NSUM_LMUL]
1667      THEN ONCE_REWRITE_TAC[SUM_LMUL]
1668      THEN ASM_SIMP_TAC[]
1669      THEN SIMP_TAC[NOT_CONS_NIL]
1670      THEN ONCE_REWRITE_TAC[lem018]
1671      THEN SIMP_TAC[]
1672     ]]);;
1673
1674 let ITERATE_RADD_POLYADD = prove
1675  (`!n x f. iterate (+) (0..n) (\i.poly (f i) x) =
1676            poly (iterate (++) (0..n) f) x`,
1677   INDUCT_TAC THEN
1678   ASM_SIMP_TAC[ITERATE_CLAUSES_NUMSEG; MONOIDAL_REAL_ADD; MONOIDAL_POLY_ADD;
1679                LE_0; POLY_ADD]);;
1680
1681 (* ------------------------------------------------------------------------- *)
1682 (* Now we're finished with polynomials...                                    *)
1683 (* ------------------------------------------------------------------------- *)
1684
1685 do_list reduce_interface
1686  ["divides",`poly_divides:real list->real list->bool`;
1687   "exp",`poly_exp:real list -> num -> real list`;
1688   "diff",`poly_diff:real list->real list`];;
1689
1690 unparse_as_infix "exp";;