Update from HH
[hl193./.git] / 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";;