1(* ========================================================================= *)
2(* Properties of real polynomials (not canonically represented).             *)
3(* ========================================================================= *)
4
5(*
6app load ["numLib",
7          "mesonLib",
8          "tautLib",
9          "numLib",
10          "simpLib",
11          "boolSimps",
12          "arithSimps",
13          "pairSimps",
14          "Ho_Rewrite",
15          "jrhUtils",
16          "limTheory",
17          "listTheory",
18          "pred_setTheory",
19          "realSimps", "RealArith"];
20*)
21
22open HolKernel Parse boolLib hol88Lib reduceLib pairLib numLib
23     mesonLib tautLib simpLib boolSimps numSimps realSimps
24     pairTheory numTheory prim_recTheory arithmeticTheory listTheory
25     Ho_Rewrite jrhUtils Canon_Port AC realTheory limTheory listTheory
26     pred_setTheory RealArith;
27
28infix THEN THENL ORELSE ORELSEC ## THENC ORELSE_TCL;
29
30val _ = new_theory "poly";
31val _ = ParseExtras.temp_loose_equality()
32
33
34(* ------------------------------------------------------------------------- *)
35(* Extras needed to port polyTheory to hol98.                                *)
36(* ------------------------------------------------------------------------- *)
37
38fun LIST_INDUCT_TAC g =
39  let
40    val v = (fst o dest_forall o snd) g
41    val v' = mk_var ("t", type_of v)
42    val tac =
43      CONV_TAC (GEN_ALPHA_CONV v')
44      THEN INDUCT_THEN list_INDUCT ASSUME_TAC
45      THENL [ALL_TAC,GEN_TAC]
46  in
47    tac g
48  end;
49
50val ARITH_TAC = CONV_TAC ARITH_CONV;
51fun ARITH_RULE tm = prove (tm, ARITH_TAC);
52
53val FORALL = LIST_CONJ (map SPEC_ALL (CONJUNCTS EVERY_DEF));
54
55(* Basic extra theorems *)
56
57val FUN_EQ_THM = prove (Term`!f g.  (f = g) = (!x. f x = g x)`,
58  REPEAT GEN_TAC THEN EQ_TAC THENL
59   [DISCH_THEN SUBST1_TAC THEN GEN_TAC THEN REFL_TAC,
60    MATCH_ACCEPT_TAC EQ_EXT]);
61
62val RIGHT_IMP_EXISTS_THM = prove (
63  Term`!P Q. P ==> (?x. Q x) = (?x. P ==> Q x)`,
64  MESON_TAC []);
65
66val LEFT_IMP_EXISTS_THM = prove (
67  Term`!P Q. (?x. P x) ==> Q = (!x. P x ==> Q)`,
68  MESON_TAC []);
69
70(* Extra theorems needed about the naturals *)
71
72val NOT_LE = arithmeticTheory.NOT_LESS_EQUAL;
73val SUC_INJ = prim_recTheory.INV_SUC_EQ
74
75val LT_SUC_LE = prove (Term`!m n. m < SUC n = m <= n`, ARITH_TAC);
76
77val LT = prove(
78  Term`(!m:num. m < 0 = F) /\ (!m n. m < SUC n = (m = n) \/ m < n)`,
79  ARITH_TAC);
80
81val LT_ADD_LCANCEL = prove (
82  Term`!m n p:num. m + n < m + p = n < p`,
83  ARITH_TAC);
84
85val LE_EXISTS = prove (
86  Term`!m n:num. m <= n = (?d. n = m + d)`,
87  REPEAT (STRIP_TAC ORELSE EQ_TAC)
88  THENL [
89    EXISTS_TAC (Term`n - m:num`),
90    ALL_TAC
91  ]
92  THEN POP_ASSUM (MP_TAC)
93  THEN ARITH_TAC);
94
95val LE_SUC_LT = prove (
96  Term`!m n. SUC m <= n = m < n`,
97  ARITH_TAC);
98
99val LT_CASES = prove (
100  Term`!m n:num. m < n \/ n < m \/ (m = n)`,
101  ARITH_TAC);
102
103val LE_REFL = prove (Term`!n:num. n <= n`, ARITH_TAC);
104
105(* Extra theorems needed about sets *)
106
107val FINITE_SUBSET = prove (Term`!s t. FINITE t /\ s SUBSET t ==> FINITE s`,
108  MESON_TAC [SUBSET_FINITE]);
109
110val FINITE_RULES = prove (
111  Term`FINITE {} /\ (!x s. FINITE s ==> FINITE (x INSERT s))`,
112  MESON_TAC [FINITE_EMPTY, FINITE_INSERT]);
113
114val GSPEC_DEF = prove (Term`!f. GSPEC f = \v. ?z. f z = (v,T)`,
115GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN BETA_TAC THEN GEN_TAC
116  THEN ONCE_REWRITE_TAC[BETA_RULE
117        (ONCE_REWRITE_CONV[GSYM SPECIFICATION](Term`(\x. GSPEC f x) x`))]
118  THEN CONV_TAC (ONCE_DEPTH_CONV ETA_CONV)
119  THEN REWRITE_TAC[GSPECIFICATION]
120  THEN MESON_TAC[]);
121
122(* ------------------------------------------------------------------------- *)
123(* Application of polynomial as a real function.                             *)
124(* ------------------------------------------------------------------------- *)
125
126fun new_recursive_definition ax name def =
127     Prim_rec.new_recursive_definition
128       {name=name, def=def, rec_axiom=ax};
129
130val poly = new_recursive_definition list_Axiom "poly_def"
131  (Term`(poly [] x = 0r) /\
132        (poly (h::t) x = h + x * poly t x)`);
133
134
135(* ------------------------------------------------------------------------- *)
136(* Arithmetic operations on polynomials. Overloaded (not sure this is wise). *)
137(* ------------------------------------------------------------------------- *)
138
139val poly_add = new_recursive_definition list_Axiom "poly_add_def"
140 (Term`(poly_add [] l2 = l2) /\
141       (poly_add (h::t) l2 = if (l2 = []) then h::t
142                             else  ((h:real) + HD l2)::poly_add t (TL l2))`);
143
144val _ = overload_on ("+", Term`poly_add`);
145
146val _ = Parse.hide "##";
147
148val poly_cmul = new_recursive_definition list_Axiom "poly_cmul_def"
149 (Term`($## c [] = []) /\
150       ($## c (h::t) = (c:real * h) :: ($## c t))`);
151val _ = set_fixity "##" (Infixl 600);
152
153val poly_neg = new_definition ("poly_neg_def", Term`poly_neg = $## (~(&1))`);
154
155val _ = overload_on ("~", Term`poly_neg`);
156
157val poly_mul = new_recursive_definition list_Axiom "poly_mul_def"
158 (Term`(poly_mul [] l2     = []) /\
159       (poly_mul (h::t) l2 = if (t = []) then h ## l2
160                             else (h ## l2) + (0r :: poly_mul t l2))`);
161
162val _ = overload_on ("*", Term`poly_mul`);
163
164val poly_exp = new_recursive_definition num_Axiom "poly_exp_def"
165 (Term`(poly_exp p 0       = [1r]) /\
166       (poly_exp p (SUC n) = poly_mul p (poly_exp p n))`);
167
168val _ = set_fixity "poly_exp" (Infixr 700) ;
169
170
171(* ------------------------------------------------------------------------- *)
172(* Differentiation of polynomials (needs an auxiliary function).             *)
173(* ------------------------------------------------------------------------- *)
174
175val poly_diff_aux = new_recursive_definition list_Axiom
176  "poly_diff_aux_def"
177   (Term`(poly_diff_aux n [] = []) /\
178         (poly_diff_aux n (h::t) = (&n * h) :: poly_diff_aux (SUC n) t)`);
179
180val poly_diff = new_definition ("poly_diff_def",
181  Term`diff l = if l = [] then [] else poly_diff_aux 1 (TL l)`);
182
183
184(* ------------------------------------------------------------------------- *)
185(* Useful clausifications.                                                   *)
186(* ------------------------------------------------------------------------- *)
187
188val POLY_ADD_CLAUSES = store_thm("POLY_ADD_CLAUSES",
189 Term`([] + p2 = p2) /\
190      (p1 + [] = p1) /\
191   ((h1::t1) + (h2::t2) =  (h1 + h2) :: (t1 + t2))`,
192  REWRITE_TAC[poly_add, NOT_CONS_NIL, HD, TL] THEN
193  SPEC_TAC(Term`p1:real list`,Term`p1:real list`) THEN
194  LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[poly_add]);
195
196val POLY_CMUL_CLAUSES = store_thm("POLY_CMUL_CLAUSES",
197 Term`(c ## [] = []) /\
198      (c ## (h::t) = (c * h) :: (c ## t))`,
199  REWRITE_TAC[poly_cmul]);
200
201val POLY_NEG_CLAUSES = store_thm("POLY_NEG_CLAUSES",
202 Term`(poly_neg [] = []) /\
203      (poly_neg (h::t) = ~h::poly_neg t)`,
204  REWRITE_TAC[poly_neg, POLY_CMUL_CLAUSES, REAL_MUL_LNEG, REAL_MUL_LID]);
205
206val POLY_MUL_CLAUSES = store_thm("POLY_MUL_CLAUSES",
207 Term`([] * p2 = []) /\
208    ([h1] * p2 = h1 ## p2) /\
209   ((h1::k1::t1) * p2 = (h1 ## p2) + (&0 :: ((k1::t1) * p2)))`,
210  REWRITE_TAC[poly_mul, NOT_CONS_NIL]);
211
212val POLY_DIFF_CLAUSES = store_thm("POLY_DIFF_CLAUSES",
213 Term`(diff [] = []) /\
214   (diff [c] = []) /\
215   (diff (h::t) = poly_diff_aux 1 t)`,
216  REWRITE_TAC[poly_diff, NOT_CONS_NIL, HD, TL, poly_diff_aux]);
217
218(* ------------------------------------------------------------------------- *)
219(* Various natural consequences of syntactic definitions.                    *)
220(* ------------------------------------------------------------------------- *)
221
222val POLY_ADD = store_thm("POLY_ADD",
223 Term`!p1 p2 x. poly (p1 + p2) x = poly p1 x + poly p2 x`,
224  LIST_INDUCT_TAC THEN REWRITE_TAC[poly_add, poly, REAL_ADD_LID] THEN
225  LIST_INDUCT_TAC THEN
226  ASM_REWRITE_TAC[NOT_CONS_NIL, HD, TL, poly, REAL_ADD_RID] THEN
227  REAL_ARITH_TAC);
228
229val POLY_CMUL = store_thm("POLY_CMUL",
230 Term`!p c x. poly (c ## p) x = c * poly p x`,
231  LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[poly, poly_cmul] THEN
232  REAL_ARITH_TAC);
233
234val POLY_NEG = store_thm("POLY_NEG",
235 Term`!p x. poly (poly_neg p) x = ~(poly p x)`,
236  REWRITE_TAC[poly_neg, POLY_CMUL] THEN
237  REAL_ARITH_TAC);
238
239val POLY_MUL = store_thm("POLY_MUL",
240 Term`!x p1 p2. poly (p1 * p2) x = poly p1 x * poly p2 x`,
241  GEN_TAC THEN LIST_INDUCT_TAC THEN
242  REWRITE_TAC[poly_mul, poly, REAL_MUL_LZERO, POLY_CMUL, POLY_ADD] THEN
243  SPEC_TAC(Term`h:real`,Term`h:real`) THEN
244  SPEC_TAC(Term`t:real list`,Term`t:real list`) THEN
245  LIST_INDUCT_TAC THEN
246  REWRITE_TAC[poly_mul, POLY_CMUL, POLY_ADD, poly, POLY_CMUL,
247    REAL_MUL_RZERO, REAL_ADD_RID, NOT_CONS_NIL] THEN
248  ASM_REWRITE_TAC[POLY_ADD, POLY_CMUL, poly] THEN
249  REAL_ARITH_TAC);
250
251val POLY_EXP = store_thm("POLY_EXP",
252 Term`!p n (x:real). poly (p poly_exp n) x = (poly p x) pow n`,
253  GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[poly_exp, pow, POLY_MUL] THEN
254  REWRITE_TAC[poly] THEN REAL_ARITH_TAC);
255
256(* ------------------------------------------------------------------------- *)
257(* The derivative is a bit more complicated.                                 *)
258(* ------------------------------------------------------------------------- *)
259
260val POLY_DIFF_LEMMA = store_thm("POLY_DIFF_LEMMA",
261 (Term`!l n x. ((\x. (x pow (SUC n)) * poly l x) diffl
262                   ((x pow n) * poly (poly_diff_aux (SUC n) l) x))(x)`),
263  LIST_INDUCT_TAC THEN
264  REWRITE_TAC[poly, poly_diff_aux, REAL_MUL_RZERO, DIFF_CONST] THEN
265  MAP_EVERY X_GEN_TAC [(Term`n:num`), (Term`x:real`)] THEN
266  REWRITE_TAC[REAL_LDISTRIB, REAL_MUL_ASSOC] THEN
267  ONCE_REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[REAL_MUL_SYM] (CONJUNCT2 pow))] THEN
268  POP_ASSUM(MP_TAC o SPECL [(Term`SUC n`), (Term`x:real`)]) THEN
269  SUBGOAL_THEN ((Term`(((\x. (x pow (SUC n)) * h)) diffl
270                        ((x pow n) * &(SUC n) * h))(x)`))
271  (fn th => DISCH_THEN(MP_TAC o CONJ th)) THENL
272   [REWRITE_TAC[REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
273    MP_TAC(SPEC ((Term`\x. x pow (SUC n)`)) DIFF_CMUL) THEN BETA_TAC THEN
274    DISCH_THEN MATCH_MP_TAC THEN
275    MP_TAC(SPEC ((Term`SUC n`)) DIFF_POW) THEN REWRITE_TAC[SUC_SUB1] THEN
276    DISCH_THEN(MATCH_ACCEPT_TAC o ONCE_REWRITE_RULE[REAL_MUL_SYM]),
277    DISCH_THEN(MP_TAC o MATCH_MP DIFF_ADD) THEN BETA_TAC THEN
278    REWRITE_TAC[REAL_MUL_ASSOC]]);
279
280val POLY_DIFF = store_thm("POLY_DIFF",
281 (Term`!l x. ((\x. poly l x) diffl (poly (diff l) x))(x)`),
282  LIST_INDUCT_TAC THEN REWRITE_TAC[POLY_DIFF_CLAUSES] THEN
283  ONCE_REWRITE_TAC[SYM(ETA_CONV (Term`\x. poly l x`))] THEN
284  REWRITE_TAC[poly, DIFF_CONST] THEN
285  MAP_EVERY X_GEN_TAC [(Term`x:real`)] THEN
286  MP_TAC(SPECL [(Term`t:real list`), (Term`0:num`), (Term`x:real`)]
287         POLY_DIFF_LEMMA) THEN
288  REWRITE_TAC[SYM ONE] THEN REWRITE_TAC[pow, REAL_MUL_LID] THEN
289  REWRITE_TAC[POW_1] THEN
290  DISCH_THEN(MP_TAC o CONJ (SPECL [(Term`h:real`), (Term`x:real`)] DIFF_CONST))
291  THEN DISCH_THEN(MP_TAC o MATCH_MP DIFF_ADD) THEN BETA_TAC THEN
292  REWRITE_TAC[REAL_ADD_LID]);
293
294(* ------------------------------------------------------------------------- *)
295(* Trivial consequences.                                                     *)
296(* ------------------------------------------------------------------------- *)
297
298val POLY_DIFFERENTIABLE = store_thm("POLY_DIFFERENTIABLE",
299 (Term`!l x. (\x. poly l x) differentiable x`),
300  REPEAT GEN_TAC THEN REWRITE_TAC[differentiable] THEN
301  EXISTS_TAC (Term`poly (diff l) x`) THEN
302  REWRITE_TAC[POLY_DIFF]);
303
304val POLY_CONT = store_thm("POLY_CONT",
305 (Term`!l x. (\x. poly l x) contl x`),
306  REPEAT GEN_TAC THEN MATCH_MP_TAC DIFF_CONT THEN
307  EXISTS_TAC (Term`poly (diff l) x`) THEN
308  MATCH_ACCEPT_TAC POLY_DIFF);
309
310val POLY_IVT_POS = store_thm("POLY_IVT_POS",
311 (Term`!p a b. a < b /\ poly p a < &0 /\ poly p b > &0
312           ==> ?x. a < x /\ x < b /\ (poly p x = &0)`),
313  REWRITE_TAC[real_gt] THEN REPEAT STRIP_TAC THEN
314  MP_TAC(SPECL [(Term`\x. poly p x`), (Term`a:real`), (Term`b:real`), (Term`&0`)] IVT) THEN
315  SIMP_TAC bool_ss [POLY_CONT] THEN
316  EVERY_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_LT_IMP_LE th]) THEN
317  DISCH_THEN(X_CHOOSE_THEN (Term`x:real`) STRIP_ASSUME_TAC) THEN
318  EXISTS_TAC (Term`x:real`) THEN ASM_REWRITE_TAC[REAL_LT_LE] THEN
319  CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
320  FIRST_ASSUM SUBST_ALL_TAC THEN
321  RULE_ASSUM_TAC(REWRITE_RULE[REAL_LT_REFL]) THEN
322  FIRST_ASSUM CONTR_TAC);
323
324val POLY_IVT_NEG = store_thm("POLY_IVT_NEG",
325 (Term`!p a b. a < b /\ poly p a > &0 /\ poly p b < &0
326           ==> ?x. a < x /\ x < b /\ (poly p x = &0)`),
327  REPEAT STRIP_TAC THEN MP_TAC(SPEC (Term`poly_neg p`) POLY_IVT_POS) THEN
328  REWRITE_TAC[POLY_NEG,
329              REAL_ARITH (Term`(~x < &0 = x > &0) /\ (~x > &0 = x < &0)`)] THEN
330  DISCH_THEN(MP_TAC o SPECL [(Term`a:real`), (Term`b:real`)]) THEN
331  ASM_REWRITE_TAC[REAL_ARITH (Term`(~x = &0) = (x = &0)`)]);
332
333val POLY_MVT = store_thm("POLY_MVT",
334 (Term`!p a b. a < b ==>
335           ?x. a < x /\ x < b /\
336              (poly p b - poly p a = (b - a) * poly (diff p) x)`),
337  REPEAT STRIP_TAC THEN
338  MP_TAC(SPECL [(Term`poly p`), (Term`a:real`), (Term`b:real`)] MVT) THEN
339  ASM_REWRITE_TAC[CONV_RULE(DEPTH_CONV ETA_CONV) (SPEC_ALL POLY_CONT),
340    CONV_RULE(DEPTH_CONV ETA_CONV) (SPEC_ALL POLY_DIFFERENTIABLE)] THEN
341  DISCH_THEN(X_CHOOSE_THEN (Term`l:real`) MP_TAC) THEN
342  DISCH_THEN(X_CHOOSE_THEN (Term`x:real`) STRIP_ASSUME_TAC) THEN
343  EXISTS_TAC (Term`x:real`) THEN ASM_REWRITE_TAC[] THEN
344  AP_TERM_TAC THEN MATCH_MP_TAC DIFF_UNIQ THEN
345  EXISTS_TAC (Term`poly p`) THEN EXISTS_TAC (Term`x:real`) THEN
346  ASM_REWRITE_TAC[CONV_RULE(DEPTH_CONV ETA_CONV) (SPEC_ALL POLY_DIFF)]);
347
348(* ------------------------------------------------------------------------- *)
349(* Lemmas.                                                                   *)
350(* ------------------------------------------------------------------------- *)
351
352val POLY_ADD_RZERO = store_thm("POLY_ADD_RZERO",
353 (Term`!p. poly (p + []) = poly p`),
354  REWRITE_TAC[FUN_EQ_THM, POLY_ADD, poly, REAL_ADD_RID]);
355
356val POLY_MUL_ASSOC = store_thm("POLY_MUL_ASSOC",
357 (Term`!p q r. poly (p * (q * r)) = poly ((p * q) * r)`),
358  REWRITE_TAC[FUN_EQ_THM, POLY_MUL, REAL_MUL_ASSOC]);
359
360val POLY_EXP_ADD = store_thm("POLY_EXP_ADD",
361 (Term`!d n p. poly(p poly_exp (n + d)) = poly(p poly_exp n * p poly_exp d)`),
362  REWRITE_TAC[FUN_EQ_THM, POLY_MUL] THEN
363  INDUCT_TAC THEN ASM_REWRITE_TAC[POLY_MUL, ADD_CLAUSES, poly_exp, poly] THEN
364  REAL_ARITH_TAC);
365
366(* ------------------------------------------------------------------------- *)
367(* Lemmas for derivatives.                                                   *)
368(* ------------------------------------------------------------------------- *)
369
370val POLY_DIFF_AUX_ADD = store_thm("POLY_DIFF_AUX_ADD",
371(Term`!p1 p2 n. poly (poly_diff_aux n (p1 + p2)) =
372             poly (poly_diff_aux n p1 + poly_diff_aux n p2)`),
373  REPEAT(LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff_aux, poly_add]) THEN
374  ASM_REWRITE_TAC[poly_diff_aux, FUN_EQ_THM, poly, NOT_CONS_NIL, HD, TL] THEN
375  REAL_ARITH_TAC);
376
377val POLY_DIFF_AUX_CMUL = store_thm("POLY_DIFF_AUX_CMUL",
378 (Term`!p c n. poly (poly_diff_aux n (c ## p)) =
379           poly (c ## poly_diff_aux n p)`),
380  LIST_INDUCT_TAC THEN
381  ASM_SIMP_TAC real_ac_ss [FUN_EQ_THM, poly, poly_diff_aux, poly_cmul]);
382
383val POLY_DIFF_AUX_NEG = store_thm("POLY_DIFF_AUX_NEG",
384 (Term`!p n.  poly (poly_diff_aux n (poly_neg p)) =
385          poly (poly_neg (poly_diff_aux n p))`),
386  REWRITE_TAC[poly_neg, POLY_DIFF_AUX_CMUL]);
387
388val POLY_DIFF_AUX_MUL_LEMMA = store_thm("POLY_DIFF_AUX_MUL_LEMMA",
389 (Term`!p n. poly (poly_diff_aux (SUC n) p) = poly (poly_diff_aux n p + p)`),
390  LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff_aux, poly_add, NOT_CONS_NIL] THEN
391  ASM_REWRITE_TAC[HD, TL, poly, FUN_EQ_THM] THEN
392  REWRITE_TAC[GSYM REAL_OF_NUM_SUC, REAL_ADD_RDISTRIB, REAL_MUL_LID]);
393
394(* ------------------------------------------------------------------------- *)
395(* Final results for derivatives.                                            *)
396(* ------------------------------------------------------------------------- *)
397
398val POLY_DIFF_ADD = store_thm("POLY_DIFF_ADD",
399 (Term`!p1 p2. poly (diff (p1 + p2)) =
400           poly (diff p1  + diff p2)`),
401  REPEAT LIST_INDUCT_TAC THEN
402  REWRITE_TAC[poly_add, poly_diff, NOT_CONS_NIL, POLY_ADD_RZERO] THEN
403  ASM_REWRITE_TAC[HD, TL, POLY_DIFF_AUX_ADD]);
404
405val POLY_DIFF_CMUL = store_thm("POLY_DIFF_CMUL",
406 (Term`!p c. poly (diff (c ## p)) = poly (c ## diff p)`),
407  LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff, poly_cmul] THEN
408  REWRITE_TAC[NOT_CONS_NIL, HD, TL, POLY_DIFF_AUX_CMUL]);
409
410val POLY_DIFF_NEG = store_thm("POLY_DIFF_NEG",
411 (Term`!p. poly (diff (poly_neg p)) = poly (poly_neg (diff p))`),
412  REWRITE_TAC[poly_neg, POLY_DIFF_CMUL]);
413
414val POLY_DIFF_MUL_LEMMA = store_thm("POLY_DIFF_MUL_LEMMA",
415 (Term`!t h. poly (diff (CONS h t)) =
416         poly (CONS (&0) (diff t) + t)`),
417  REWRITE_TAC[poly_diff, NOT_CONS_NIL] THEN
418  LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff_aux, NOT_CONS_NIL, HD, TL] THENL
419   [REWRITE_TAC[FUN_EQ_THM, poly, poly_add, REAL_MUL_RZERO, REAL_ADD_LID],
420    REWRITE_TAC[FUN_EQ_THM, poly, POLY_DIFF_AUX_MUL_LEMMA, POLY_ADD] THEN
421    REAL_ARITH_TAC]);
422
423val POLY_DIFF_MUL = store_thm("POLY_DIFF_MUL",
424 (Term`!p1 p2. poly (diff (p1 * p2)) =
425           poly (p1 * diff p2 + diff p1 * p2)`),
426  LIST_INDUCT_TAC THEN REWRITE_TAC[poly_mul] THENL
427   [REWRITE_TAC[poly_diff, poly_add, poly_mul], ALL_TAC] THEN
428  GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
429   [REWRITE_TAC[POLY_DIFF_CLAUSES] THEN
430    REWRITE_TAC[poly_add, poly_mul, POLY_ADD_RZERO, POLY_DIFF_CMUL],
431    ALL_TAC] THEN
432  REWRITE_TAC[FUN_EQ_THM, POLY_DIFF_ADD, POLY_ADD] THEN
433  REWRITE_TAC[poly, POLY_ADD, POLY_DIFF_MUL_LEMMA, POLY_MUL] THEN
434  ASM_REWRITE_TAC[POLY_DIFF_CMUL, POLY_ADD, POLY_MUL] THEN
435  REAL_ARITH_TAC);
436
437val POLY_DIFF_EXP = store_thm("POLY_DIFF_EXP",
438 (Term`!p n. poly (diff (p poly_exp (SUC n))) =
439         poly (&(SUC n) ## (p poly_exp n) * diff p)`),
440  GEN_TAC THEN INDUCT_TAC THEN ONCE_REWRITE_TAC[poly_exp] THENL
441   [REWRITE_TAC[poly_exp, POLY_DIFF_MUL] THEN
442    REWRITE_TAC[FUN_EQ_THM, POLY_MUL, POLY_ADD, POLY_CMUL] THEN
443    REWRITE_TAC[poly, POLY_DIFF_CLAUSES, ADD1, ADD_CLAUSES] THEN
444    REAL_ARITH_TAC,
445    REWRITE_TAC[POLY_DIFF_MUL] THEN
446    ASM_REWRITE_TAC[POLY_MUL, POLY_ADD, FUN_EQ_THM, POLY_CMUL] THEN
447    REWRITE_TAC[poly_exp, POLY_MUL] THEN
448    REWRITE_TAC[ADD1, GSYM REAL_OF_NUM_ADD] THEN
449    REAL_ARITH_TAC]);
450
451val POLY_DIFF_EXP_PRIME = store_thm("POLY_DIFF_EXP_PRIME",
452 (Term`!n a. poly (diff ([~a; &1] poly_exp (SUC n))) =
453         poly (&(SUC n) ## ([~a; &1] poly_exp n))`),
454  REPEAT GEN_TAC THEN SIMP_TAC real_ac_ss [POLY_DIFF_EXP] THEN
455  SIMP_TAC real_ac_ss [FUN_EQ_THM, POLY_CMUL, POLY_MUL] THEN
456  SIMP_TAC real_ac_ss [poly_diff, poly_diff_aux, TL, NOT_CONS_NIL] THEN
457  SIMP_TAC real_ac_ss [poly] THEN REAL_ARITH_TAC);
458
459(* ------------------------------------------------------------------------- *)
460(* Key property that f(a) = 0 ==> (x - a) divides p(x). Very delicate!       *)
461(* ------------------------------------------------------------------------- *)
462
463val POLY_LINEAR_REM = store_thm("POLY_LINEAR_REM",
464 (Term`!t h. ?q r. h::t = [r] + [~a; &1] * q`),
465  LIST_INDUCT_TAC THEN REWRITE_TAC[] THENL
466   [GEN_TAC THEN EXISTS_TAC (Term`[]:real list`) THEN
467    EXISTS_TAC (Term`h:real`) THEN
468    REWRITE_TAC[poly_add, poly_mul, poly_cmul, NOT_CONS_NIL] THEN
469    REWRITE_TAC[HD, TL, REAL_ADD_RID],
470    X_GEN_TAC (Term`k:real`) THEN
471    POP_ASSUM(STRIP_ASSUME_TAC o SPEC (Term`h:real`)) THEN
472    EXISTS_TAC (Term`CONS (r:real) q`) THEN
473    EXISTS_TAC (Term`r * a + k:real`) THEN
474    ASM_REWRITE_TAC[POLY_ADD_CLAUSES, POLY_MUL_CLAUSES, poly_cmul] THEN
475    REWRITE_TAC[CONS_11] THEN CONJ_TAC THENL
476     [REAL_ARITH_TAC, ALL_TAC] THEN
477    SPEC_TAC((Term`q:real list`),(Term`q:real list`)) THEN
478    LIST_INDUCT_TAC THEN
479    REWRITE_TAC[POLY_ADD_CLAUSES, POLY_MUL_CLAUSES, poly_cmul] THEN
480    REWRITE_TAC[REAL_ADD_RID, REAL_MUL_LID] THEN
481    SIMP_TAC real_ac_ss []]);
482
483val POLY_LINEAR_DIVIDES = store_thm("POLY_LINEAR_DIVIDES",
484 (Term`!a p. (poly p a = &0) = (p = []) \/ ?q. p = [~a; &1] * q`),
485  GEN_TAC THEN LIST_INDUCT_TAC THENL
486   [REWRITE_TAC[poly], ALL_TAC] THEN
487  EQ_TAC THEN STRIP_TAC THENL
488   [DISJ2_TAC THEN STRIP_ASSUME_TAC(SPEC_ALL POLY_LINEAR_REM) THEN
489    EXISTS_TAC (Term`q:real list`) THEN ASM_REWRITE_TAC[] THEN
490    SUBGOAL_THEN (Term`r = &0`) SUBST_ALL_TAC THENL
491     [UNDISCH_TAC (Term`poly (CONS h t) a = &0`) THEN
492      ASM_REWRITE_TAC[] THEN REWRITE_TAC[POLY_ADD, POLY_MUL] THEN
493      REWRITE_TAC[poly, REAL_MUL_RZERO, REAL_ADD_RID, REAL_MUL_RID] THEN
494      REWRITE_TAC[REAL_ARITH (Term`~a + a = &0`)] THEN REAL_ARITH_TAC,
495      REWRITE_TAC[poly_mul] THEN REWRITE_TAC[NOT_CONS_NIL] THEN
496      SPEC_TAC((Term`q:real list`),(Term`q:real list`)) THEN LIST_INDUCT_TAC THENL
497       [REWRITE_TAC[poly_cmul, poly_add, NOT_CONS_NIL, HD, TL, REAL_ADD_LID],
498        REWRITE_TAC[poly_cmul, poly_add, NOT_CONS_NIL, HD, TL, REAL_ADD_LID]]],
499    ASM_REWRITE_TAC[] THEN REWRITE_TAC[poly],
500    ASM_REWRITE_TAC[] THEN REWRITE_TAC[poly] THEN
501    REWRITE_TAC[POLY_MUL] THEN REWRITE_TAC[poly] THEN
502    REWRITE_TAC[poly, REAL_MUL_RZERO, REAL_ADD_RID, REAL_MUL_RID] THEN
503    REWRITE_TAC[REAL_ARITH (Term`~a + a = &0`)] THEN REAL_ARITH_TAC]);
504
505(* ------------------------------------------------------------------------- *)
506(* Thanks to the finesse of the above, we can use length rather than degree. *)
507(* ------------------------------------------------------------------------- *)
508
509val POLY_LENGTH_MUL = store_thm("POLY_LENGTH_MUL",
510 (Term`!q. LENGTH([~a; &1] * q) = SUC(LENGTH q)`),
511  let
512    val lemma = prove
513   ((Term`!p h k a. LENGTH (k ## p + CONS h (a ## p)) = SUC(LENGTH p)`),
514    LIST_INDUCT_TAC THEN
515    ASM_REWRITE_TAC[poly_cmul, POLY_ADD_CLAUSES, LENGTH])
516  in
517    REWRITE_TAC[poly_mul, NOT_CONS_NIL, lemma]
518  end);
519
520(* ------------------------------------------------------------------------- *)
521(* Thus a nontrivial polynomial of degree n has no more than n roots.        *)
522(* ------------------------------------------------------------------------- *)
523
524val POLY_ROOTS_INDEX_LEMMA = store_thm("POLY_ROOTS_INDEX_LEMMA",
525 (Term`!n. !p. ~(poly p = poly []) /\ (LENGTH p = n)
526           ==> ?i. !x. (poly p (x) = &0) ==> ?m. m <= n /\ (x = i m)`),
527  INDUCT_TAC THENL
528   [SIMP_TAC real_ac_ss [LENGTH_NIL],
529    REPEAT STRIP_TAC THEN ASM_CASES_TAC (Term`?a. poly p a = &0`) THENL
530     [UNDISCH_TAC (Term`?a. poly p a = &0`) THEN DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
531      GEN_REWRITE_TAC LAND_CONV [POLY_LINEAR_DIVIDES] THEN
532      DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [ASM_MESON_TAC[], ALL_TAC] THEN
533      DISCH_THEN(X_CHOOSE_THEN (Term`q:real list`) SUBST_ALL_TAC) THEN
534      FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN
535      UNDISCH_TAC (Term`~(poly ([~a; &1] * q) = poly [])`) THEN
536      POP_ASSUM MP_TAC THEN REWRITE_TAC[POLY_LENGTH_MUL, SUC_INJ] THEN
537      DISCH_TAC THEN ASM_CASES_TAC (Term`poly q = poly []`) THENL
538       [ASM_REWRITE_TAC[POLY_MUL, poly, REAL_MUL_RZERO, FUN_EQ_THM],
539        DISCH_THEN(K ALL_TAC)] THEN
540      DISCH_THEN(MP_TAC o SPEC (Term`q:real list`)) THEN ASM_REWRITE_TAC[] THEN
541      DISCH_THEN(X_CHOOSE_TAC (Term`i:num->real`)) THEN
542      EXISTS_TAC (Term`\m. if m = SUC n then (a:real) else i m`) THEN
543      REWRITE_TAC[POLY_MUL, LE, REAL_ENTIRE] THEN
544      X_GEN_TAC (Term`x:real`) THEN DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
545       [DISCH_THEN(fn th => EXISTS_TAC (Term`SUC n`) THEN MP_TAC th) THEN
546        SIMP_TAC real_ac_ss [] THEN REWRITE_TAC[poly] THEN REAL_ARITH_TAC,
547        DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
548        DISCH_THEN(X_CHOOSE_THEN (Term`m:num`) STRIP_ASSUME_TAC) THEN
549        EXISTS_TAC (Term`m:num`) THEN ASM_SIMP_TAC real_ac_ss [] THEN
550        COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
551        UNDISCH_TAC (Term`m:num <= n`) THEN ASM_SIMP_TAC real_ac_ss []],
552      UNDISCH_TAC (Term`~(?a. poly p a = &0)`) THEN
553      REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_TAC
554      THEN ASM_SIMP_TAC bool_ss []]]);
555
556val POLY_ROOTS_INDEX_LENGTH = store_thm("POLY_ROOTS_INDEX_LENGTH",
557 (Term`!p. ~(poly p = poly [])
558       ==> ?i. !x. (poly p(x) = &0) ==> ?n. n <= LENGTH p /\ (x = i n)`),
559  MESON_TAC[POLY_ROOTS_INDEX_LEMMA]);
560
561val POLY_ROOTS_FINITE_LEMMA = store_thm("POLY_ROOTS_FINITE_LEMMA",
562 (Term`!p. ~(poly p = poly [])
563       ==> ?N i. !x. (poly p(x) = &0) ==> ?n:num. n < N /\ (x = i n)`),
564  MESON_TAC[POLY_ROOTS_INDEX_LENGTH, LT_SUC_LE]);
565
566val FINITE_LEMMA = store_thm("FINITE_LEMMA",
567 (Term`!i N P. (!x. P x ==> ?n:num. n < N /\ (x = i n))
568           ==> ?a. !x. P x ==> x < a`),
569  GEN_TAC THEN ONCE_REWRITE_TAC[RIGHT_IMP_EXISTS_THM] THEN INDUCT_TAC THENL
570   [REWRITE_TAC[LT] THEN MESON_TAC[], ALL_TAC] THEN
571  X_GEN_TAC (Term`P:real->bool`) THEN
572  POP_ASSUM(MP_TAC o SPEC (Term`\z. P z /\ ~(z = (i:num->real) N)`)) THEN
573  DISCH_THEN(X_CHOOSE_TAC (Term`a:real`)) THEN
574  EXISTS_TAC (Term`abs(a) + abs(i(N:num)) + &1`) THEN
575  POP_ASSUM MP_TAC THEN REWRITE_TAC[LT] THEN
576  MP_TAC(REAL_ARITH (Term`!x v. x < abs(v) + abs(x) + &1`)) THEN
577  MP_TAC(REAL_ARITH (Term`!u v x. x < v ==> x < abs(v) + abs(u) + &1`)) THEN
578  MESON_TAC[]);
579
580val POLY_ROOTS_FINITE = store_thm("POLY_ROOTS_FINITE",
581 (Term`!p. ~(poly p = poly []) =
582       ?N i. !x. (poly p(x) = &0) ==> ?n:num. n < N /\ (x = i n)`),
583  GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE_LEMMA] THEN
584  REWRITE_TAC[FUN_EQ_THM, LEFT_IMP_EXISTS_THM, NOT_FORALL_THM, poly] THEN
585  MP_TAC(GENL [(Term`i:num->real`), (Term`N:num`)]
586   (SPECL [(Term`i:num->real`), (Term`N:num`), (Term`\x. poly p x = &0`)] FINITE_LEMMA)) THEN
587  REWRITE_TAC[] THEN MESON_TAC[REAL_LT_REFL]);
588
589(* ------------------------------------------------------------------------- *)
590(* Hence get entirety and cancellation for polynomials.                      *)
591(* ------------------------------------------------------------------------- *)
592
593val POLY_ENTIRE_LEMMA = store_thm("POLY_ENTIRE_LEMMA",
594 (Term`!p q. ~(poly p = poly []) /\ ~(poly q = poly [])
595         ==> ~(poly (p * q) = poly [])`),
596  REPEAT GEN_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE] THEN
597  DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
598  DISCH_THEN(X_CHOOSE_THEN (Term`N2:num`) (X_CHOOSE_TAC (Term`i2:num->real`))) THEN
599  DISCH_THEN(X_CHOOSE_THEN (Term`N1:num`) (X_CHOOSE_TAC (Term`i1:num->real`))) THEN
600  EXISTS_TAC (Term`N1 + N2:num`) THEN
601  EXISTS_TAC (Term`\n:num. if n < N1 then i1(n):real else i2(n - N1)`) THEN
602  X_GEN_TAC (Term`x:real`) THEN REWRITE_TAC[REAL_ENTIRE, POLY_MUL] THEN
603  DISCH_THEN(DISJ_CASES_THEN (ANTE_RES_THEN (X_CHOOSE_TAC (Term`n:num`)))) THENL
604   [EXISTS_TAC (Term`n:num`) THEN ASM_SIMP_TAC real_ac_ss [],
605    EXISTS_TAC (Term`N1 + n:num`) THEN ASM_SIMP_TAC real_ac_ss [LT_ADD_LCANCEL]]);
606
607val POLY_ENTIRE = store_thm("POLY_ENTIRE",
608 (Term`!p q. (poly (p * q) = poly []) = (poly p = poly []) \/ (poly q = poly [])`),
609  REPEAT GEN_TAC THEN EQ_TAC THENL
610   [MESON_TAC[POLY_ENTIRE_LEMMA],
611    REWRITE_TAC[FUN_EQ_THM, POLY_MUL] THEN
612    STRIP_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RZERO, REAL_MUL_LZERO, poly]]);
613
614val POLY_MUL_LCANCEL = store_thm("POLY_MUL_LCANCEL",
615 (Term`!p q r. (poly (p * q) = poly (p * r)) =
616           (poly p = poly []) \/ (poly q = poly r)`),
617  let
618    val lemma1 = prove
619     ((Term`!p q. (poly (p + poly_neg q) = poly []) = (poly p = poly q)`),
620      REWRITE_TAC[FUN_EQ_THM, POLY_ADD, POLY_NEG, poly] THEN
621      REWRITE_TAC[REAL_ARITH (Term`(p + ~q = &0) = (p = q)`)])
622    val lemma2 = prove
623     ((Term`!p q r. poly (p * q + poly_neg(p * r)) = poly (p * (q + poly_neg(r)))`),
624      REWRITE_TAC[FUN_EQ_THM, POLY_ADD, POLY_NEG, POLY_MUL] THEN
625      REAL_ARITH_TAC)
626  in
627    ONCE_REWRITE_TAC[GSYM lemma1] THEN
628    REWRITE_TAC[lemma2, POLY_ENTIRE] THEN
629    REWRITE_TAC[lemma1]
630  end);
631
632val POLY_EXP_EQ_0 = store_thm("POLY_EXP_EQ_0",
633 (Term`!p n. (poly (p poly_exp n) = poly []) = (poly p = poly []) /\ ~(n = 0)`),
634  REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM, poly] THEN
635  REWRITE_TAC [LEFT_AND_FORALL_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN
636  SPEC_TAC((Term`n:num`),(Term`n:num`)) THEN INDUCT_TAC THEN
637  SIMP_TAC real_ac_ss [poly_exp, poly, REAL_MUL_RZERO, REAL_ADD_RID,
638    REAL_OF_NUM_EQ, NOT_SUC] THEN
639  ASM_REWRITE_TAC[POLY_MUL, poly, REAL_ENTIRE] THEN
640  MESON_TAC []);
641
642val POLY_PRIME_EQ_0 = store_thm("POLY_PRIME_EQ_0",
643 (Term`!a. ~(poly [a; &1] = poly [])`),
644  GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM, poly] THEN
645  DISCH_THEN(MP_TAC o SPEC (Term`&1 - a`)) THEN
646  REAL_ARITH_TAC);
647
648val POLY_EXP_PRIME_EQ_0 = store_thm("POLY_EXP_PRIME_EQ_0",
649 (Term`!a n. ~(poly ([a; &1] poly_exp n) = poly [])`),
650  MESON_TAC[POLY_EXP_EQ_0, POLY_PRIME_EQ_0]);
651
652(* ------------------------------------------------------------------------- *)
653(* Can also prove a more "constructive" notion of polynomial being trivial.  *)
654(* ------------------------------------------------------------------------- *)
655
656val POLY_ZERO_LEMMA = store_thm("POLY_ZERO_LEMMA",
657 (Term`!h t. (poly (CONS h t) = poly []) ==> (h = &0) /\ (poly t = poly [])`),
658  let
659    val lemma = REWRITE_RULE[FUN_EQ_THM, poly] POLY_ROOTS_FINITE
660  in
661    REPEAT GEN_TAC
662    THEN SIMP_TAC real_ac_ss [FUN_EQ_THM, poly]
663    THEN ASM_CASES_TAC (Term`h = &0`)
664    THEN ASM_SIMP_TAC real_ac_ss []
665    THENL [
666      SIMP_TAC real_ac_ss [REAL_ADD_LID]
667      THEN CONV_TAC CONTRAPOS_CONV
668      THEN DISCH_THEN(MP_TAC o REWRITE_RULE[lemma])
669      THEN DISCH_THEN(X_CHOOSE_THEN (Term`N:num`) (X_CHOOSE_TAC (Term`i:num->real`)))
670      THEN MP_TAC
671        (SPECL [(Term`i:num->real`), (Term`N:num`), (Term`\x. poly t x = &0`)] FINITE_LEMMA)
672      THEN ASM_SIMP_TAC real_ac_ss []
673      THEN DISCH_THEN(X_CHOOSE_TAC (Term`a:real`))
674      THEN EXISTS_TAC (Term`abs(a) + &1`)
675      THEN POP_ASSUM (MP_TAC o SPEC (Term`abs(a) + &1`))
676      THEN REWRITE_TAC [REAL_ENTIRE]
677      THEN REAL_ARITH_TAC,
678      EXISTS_TAC (Term`&0`)
679      THEN ASM_SIMP_TAC real_ac_ss []
680    ]
681  end);
682
683val POLY_ZERO = store_thm("POLY_ZERO",
684 (Term`!p. (poly p = poly []) = EVERY (\c. c = &0) p`),
685  LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[FORALL] THEN EQ_TAC THENL
686   [DISCH_THEN(MP_TAC o MATCH_MP POLY_ZERO_LEMMA) THEN ASM_REWRITE_TAC[],
687    POP_ASSUM(SUBST1_TAC o SYM) THEN STRIP_TAC THEN
688    ASM_REWRITE_TAC[FUN_EQ_THM, poly] THEN REAL_ARITH_TAC]);
689
690(* ------------------------------------------------------------------------- *)
691(* Useful triviality.                                                        *)
692(* ------------------------------------------------------------------------- *)
693
694val POLY_DIFF_AUX_ISZERO = store_thm("POLY_DIFF_AUX_ISZERO",
695 (Term`!p n. EVERY (\c. c = &0) (poly_diff_aux (SUC n) p) =
696         EVERY (\c. c = &0) p`),
697  LIST_INDUCT_TAC THEN ASM_REWRITE_TAC
698   [FORALL, poly_diff_aux, REAL_ENTIRE, REAL_OF_NUM_EQ, NOT_SUC]);
699
700
701val POLY_DIFF_ISZERO = store_thm("POLY_DIFF_ISZERO",
702 (Term`!p. (poly (diff p) = poly []) ==> ?h. poly p = poly [h]`),
703  REWRITE_TAC[POLY_ZERO] THEN
704  LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[POLY_DIFF_CLAUSES, FORALL] THENL
705   [EXISTS_TAC (Term`&0`) THEN REWRITE_TAC[FUN_EQ_THM, poly] THEN REAL_ARITH_TAC,
706    REWRITE_TAC[ONE, POLY_DIFF_AUX_ISZERO] THEN
707    REWRITE_TAC[GSYM POLY_ZERO] THEN DISCH_TAC THEN
708    EXISTS_TAC (Term`h:real`) THEN ASM_REWRITE_TAC[poly, FUN_EQ_THM]]);
709
710val POLY_DIFF_ZERO = store_thm("POLY_DIFF_ZERO",
711 (Term`!p. (poly p = poly []) ==> (poly (diff p) = poly [])`),
712  REWRITE_TAC[POLY_ZERO] THEN
713  LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff, NOT_CONS_NIL] THEN
714  REWRITE_TAC[FORALL, TL] THEN
715  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
716  SPEC_TAC((Term`1:num`),(Term`n:num`)) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
717  SPEC_TAC((Term`t:real list`),(Term`t:real list`)) THEN
718  LIST_INDUCT_TAC THEN REWRITE_TAC[FORALL, poly_diff_aux] THEN
719  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RZERO] THEN
720  FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
721
722val POLY_DIFF_WELLDEF = store_thm("POLY_DIFF_WELLDEF",
723 (Term`!p q. (poly p = poly q) ==> (poly (diff p) = poly (diff q))`),
724  REPEAT STRIP_TAC THEN MP_TAC(SPEC (Term`p + poly_neg(q)`) POLY_DIFF_ZERO) THEN
725  REWRITE_TAC[FUN_EQ_THM, POLY_DIFF_ADD, POLY_DIFF_NEG, POLY_ADD] THEN
726  ASM_REWRITE_TAC[POLY_NEG, poly, REAL_ARITH (Term`a + ~a = &0`)] THEN
727  REWRITE_TAC[REAL_ARITH (Term`(a + ~b = &0) = (a = b)`)]);
728
729(* ------------------------------------------------------------------------- *)
730(* Basics of divisibility.                                                   *)
731(* ------------------------------------------------------------------------- *)
732
733val poly_divides = new_infixl_definition ("poly_divides",
734  (Term`$poly_divides p1 p2 = ?q. poly p2 = poly (p1 * q)`), 475);
735
736val POLY_PRIMES = store_thm("POLY_PRIMES",
737 (Term`!a p q. [a; &1] poly_divides (p * q)
738                           =
739               [a; &1] poly_divides p \/ [a; &1] poly_divides q`),
740 REPEAT GEN_TAC THEN REWRITE_TAC[poly_divides, POLY_MUL, FUN_EQ_THM, poly] THEN
741 REWRITE_TAC[REAL_MUL_RZERO, REAL_ADD_RID, REAL_MUL_RID] THEN EQ_TAC THENL
742 [DISCH_THEN(X_CHOOSE_THEN (Term`r:real list`)
743  (MP_TAC o SPEC (Term`~a:real`))) THEN
744   REWRITE_TAC[REAL_ENTIRE, GSYM real_sub, REAL_SUB_REFL, REAL_MUL_LZERO] THEN
745    DISCH_THEN DISJ_CASES_TAC THENL [DISJ1_TAC, DISJ2_TAC] THEN
746    (POP_ASSUM(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) THEN
747     REWRITE_TAC[REAL_NEG_NEG] THEN
748     DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC
749        (X_CHOOSE_THEN (Term`s:real list`) SUBST_ALL_TAC)) THENL
750      [EXISTS_TAC (Term`[]:real list`) THEN REWRITE_TAC[poly, REAL_MUL_RZERO],
751       EXISTS_TAC (Term`s:real list`) THEN GEN_TAC THEN
752       REWRITE_TAC[POLY_MUL, poly] THEN REAL_ARITH_TAC]),
753    DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_TAC (Term`s:real list`))) THEN
754    ASM_REWRITE_TAC[] THENL
755     [EXISTS_TAC (Term`s * q`), EXISTS_TAC (Term`p * s`)] THEN
756    GEN_TAC THEN REWRITE_TAC[POLY_MUL] THEN REAL_ARITH_TAC]);
757
758val POLY_DIVIDES_REFL = store_thm("POLY_DIVIDES_REFL",
759 (Term`!p. p poly_divides p`),
760  GEN_TAC THEN REWRITE_TAC[poly_divides] THEN EXISTS_TAC (Term`[&1]`) THEN
761  REWRITE_TAC[FUN_EQ_THM, POLY_MUL, poly] THEN REAL_ARITH_TAC);
762
763val POLY_DIVIDES_TRANS = store_thm("POLY_DIVIDES_TRANS",
764 (Term`!p q r. p poly_divides q /\ q poly_divides r ==> p poly_divides r`),
765  REPEAT GEN_TAC THEN REWRITE_TAC[poly_divides] THEN
766  DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
767  DISCH_THEN(X_CHOOSE_THEN (Term`s:real list`) ASSUME_TAC) THEN
768  DISCH_THEN(X_CHOOSE_THEN (Term`t:real list`) ASSUME_TAC) THEN
769  EXISTS_TAC (Term`t * s`) THEN
770  ASM_REWRITE_TAC[FUN_EQ_THM, POLY_MUL, REAL_MUL_ASSOC]);
771
772val POLY_DIVIDES_EXP = store_thm("POLY_DIVIDES_EXP",
773 (Term`!p m n. m <= n ==> (p poly_exp m) poly_divides (p poly_exp n)`),
774  REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
775  DISCH_THEN(X_CHOOSE_THEN (Term`d:num`) SUBST1_TAC) THEN
776  SPEC_TAC((Term`d:num`),(Term`d:num`)) THEN INDUCT_TAC THEN
777  REWRITE_TAC[ADD_CLAUSES, POLY_DIVIDES_REFL] THEN
778  MATCH_MP_TAC POLY_DIVIDES_TRANS THEN
779  EXISTS_TAC (Term`p poly_exp (m + d)`) THEN ASM_REWRITE_TAC[] THEN
780  REWRITE_TAC[poly_divides] THEN EXISTS_TAC (Term`p:real list`) THEN
781  REWRITE_TAC[poly_exp, FUN_EQ_THM, POLY_MUL] THEN
782  REAL_ARITH_TAC);
783
784val POLY_EXP_DIVIDES = store_thm("POLY_EXP_DIVIDES",
785 (Term`!p q m n.
786      (p poly_exp n) poly_divides q /\ m <= n ==> (p poly_exp m) poly_divides q`),
787  MESON_TAC[POLY_DIVIDES_TRANS, POLY_DIVIDES_EXP]);
788
789val POLY_DIVIDES_ADD = store_thm("POLY_DIVIDES_ADD",
790 (Term`!p q r. p poly_divides q /\ p poly_divides r ==> p poly_divides (q + r)`),
791  REPEAT GEN_TAC THEN REWRITE_TAC[poly_divides] THEN
792  DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
793  DISCH_THEN(X_CHOOSE_THEN (Term`s:real list`) ASSUME_TAC) THEN
794  DISCH_THEN(X_CHOOSE_THEN (Term`t:real list`) ASSUME_TAC) THEN
795  EXISTS_TAC (Term`t + s`) THEN
796  ASM_REWRITE_TAC[FUN_EQ_THM, POLY_ADD, POLY_MUL] THEN
797  REAL_ARITH_TAC);
798
799val POLY_DIVIDES_SUB = store_thm("POLY_DIVIDES_SUB",
800 (Term`!p q r. p poly_divides q /\ p poly_divides (q + r) ==> p poly_divides r`),
801  REPEAT GEN_TAC THEN REWRITE_TAC[poly_divides] THEN
802  DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
803  DISCH_THEN(X_CHOOSE_THEN (Term`s:real list`) ASSUME_TAC) THEN
804  DISCH_THEN(X_CHOOSE_THEN (Term`t:real list`) ASSUME_TAC) THEN
805  EXISTS_TAC (Term`s + poly_neg(t)`) THEN
806  POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
807  REWRITE_TAC[FUN_EQ_THM, POLY_ADD, POLY_MUL, POLY_NEG] THEN
808  DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
809  REWRITE_TAC[REAL_ADD_LDISTRIB, REAL_MUL_RNEG] THEN
810  ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
811
812val POLY_DIVIDES_SUB2 = store_thm("POLY_DIVIDES_SUB2",
813 (Term`!p q r. p poly_divides r /\ p poly_divides (q + r) ==> p poly_divides q`),
814  REPEAT STRIP_TAC THEN MATCH_MP_TAC POLY_DIVIDES_SUB THEN
815  EXISTS_TAC (Term`r:real list`) THEN ASM_REWRITE_TAC[] THEN
816  UNDISCH_TAC (Term`p poly_divides (q + r)`) THEN
817  REWRITE_TAC[poly_divides, POLY_ADD, FUN_EQ_THM, POLY_MUL] THEN
818  DISCH_THEN(X_CHOOSE_TAC (Term`s:real list`)) THEN
819  EXISTS_TAC (Term`s:real list`) THEN
820  X_GEN_TAC (Term`x:real`) THEN POP_ASSUM(MP_TAC o SPEC (Term`x:real`)) THEN
821  REAL_ARITH_TAC);
822
823val POLY_DIVIDES_ZERO = store_thm("POLY_DIVIDES_ZERO",
824 (Term`!p q. (poly p = poly []) ==> q poly_divides p`),
825  REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[poly_divides] THEN
826  EXISTS_TAC (Term`[]:real list`) THEN
827  ASM_REWRITE_TAC[FUN_EQ_THM, POLY_MUL, poly, REAL_MUL_RZERO]);
828
829(* ------------------------------------------------------------------------- *)
830(* At last, we can consider the order of a root.                             *)
831(* ------------------------------------------------------------------------- *)
832
833val POLY_ORDER_EXISTS = store_thm("POLY_ORDER_EXISTS",
834 (Term`!a d. !p. (LENGTH p = d) /\ ~(poly p = poly [])
835             ==> ?n. ([~a; &1] poly_exp n) poly_divides p /\
836                     ~(([~a; &1] poly_exp (SUC n)) poly_divides p)`),
837  GEN_TAC
838  THEN (STRIP_ASSUME_TAC o prove_rec_fn_exists num_Axiom)
839    (Term`(!p q. mulexp 0 p q = q) /\
840     (!p q n. mulexp (SUC n) p q = p * (mulexp n p q))`)
841  THEN SUBGOAL_THEN
842    (Term`!d. !p. (LENGTH p = d) /\ ~(poly p = poly [])
843           ==> ?n q. (p = mulexp (n:num) [~a; &1] q) /\
844                     ~(poly q a = &0)`) MP_TAC
845  THENL [ INDUCT_TAC THENL [SIMP_TAC real_ac_ss [LENGTH_NIL], ALL_TAC]
846    THEN X_GEN_TAC (Term`p:real list`)
847    THEN ASM_CASES_TAC (Term`poly p a = &0`)
848    THENL [
849      STRIP_TAC
850      THEN UNDISCH_TAC (Term`poly p a = &0`)
851      THEN DISCH_THEN(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES])
852      THEN DISCH_THEN(DISJ_CASES_THEN MP_TAC)
853      THENL [
854        ASM_MESON_TAC[],
855        ALL_TAC
856      ]
857      THEN DISCH_THEN(X_CHOOSE_THEN (Term`q:real list`) SUBST_ALL_TAC)
858      THEN UNDISCH_TAC
859        (Term`!p. (LENGTH p = d) /\ ~(poly p = poly [])
860         ==> ?n q. (p = mulexp (n:num) [~a; &1] q) /\
861                   ~(poly q a = &0)`)
862      THEN DISCH_THEN(MP_TAC o SPEC (Term`q:real list`))
863      THEN RULE_ASSUM_TAC(REWRITE_RULE[POLY_LENGTH_MUL, POLY_ENTIRE,
864        DE_MORGAN_THM, SUC_INJ])
865      THEN ASM_REWRITE_TAC[]
866      THEN DISCH_THEN(X_CHOOSE_THEN (Term`n:num`)
867        (X_CHOOSE_THEN (Term`s:real list`) STRIP_ASSUME_TAC))
868      THEN EXISTS_TAC (Term`SUC n`)
869      THEN EXISTS_TAC (Term`s:real list`)
870      THEN ASM_REWRITE_TAC[],
871      STRIP_TAC
872      THEN EXISTS_TAC (Term`0:num`)
873      THEN EXISTS_TAC (Term`p:real list`)
874      THEN ASM_REWRITE_TAC[]
875    ],
876    DISCH_TAC
877    THEN REPEAT GEN_TAC
878    THEN DISCH_THEN(ANTE_RES_THEN MP_TAC)
879    THEN DISCH_THEN(X_CHOOSE_THEN (Term`n:num`)
880      (X_CHOOSE_THEN (Term`s:real list`) STRIP_ASSUME_TAC))
881    THEN EXISTS_TAC (Term`n:num`)
882    THEN ASM_REWRITE_TAC[]
883    THEN REWRITE_TAC[poly_divides]
884    THEN CONJ_TAC
885    THENL [
886      EXISTS_TAC (Term`s:real list`)
887      THEN SPEC_TAC((Term`n:num`),(Term`n:num`))
888      THEN INDUCT_TAC
889      THEN ASM_REWRITE_TAC[poly_exp, FUN_EQ_THM, POLY_MUL, poly]
890      THEN REAL_ARITH_TAC,
891      DISCH_THEN(X_CHOOSE_THEN (Term`r:real list`) MP_TAC)
892      THEN SPEC_TAC((Term`n:num`),(Term`n:num`))
893      THEN INDUCT_TAC
894      THEN ASM_SIMP_TAC bool_ss []
895      THENL [
896        UNDISCH_TAC (Term`~(poly s a = &0)`)
897        THEN CONV_TAC CONTRAPOS_CONV
898        THEN REWRITE_TAC[]
899        THEN DISCH_THEN SUBST1_TAC
900        THEN REWRITE_TAC[poly, poly_exp, POLY_MUL]
901        THEN REAL_ARITH_TAC,
902        REWRITE_TAC[]
903        THEN ONCE_ASM_REWRITE_TAC[]
904        THEN ONCE_REWRITE_TAC[poly_exp]
905        THEN REWRITE_TAC[GSYM POLY_MUL_ASSOC, POLY_MUL_LCANCEL]
906        THEN REWRITE_TAC[DE_MORGAN_THM]
907        THEN CONJ_TAC
908        THENL [
909          REWRITE_TAC[FUN_EQ_THM]
910          THEN DISCH_THEN(MP_TAC o SPEC (Term`a + &1`))
911          THEN REWRITE_TAC[poly]
912          THEN REAL_ARITH_TAC,
913          DISCH_THEN(ANTE_RES_THEN MP_TAC)
914          THEN REWRITE_TAC[]
915        ]
916      ]
917    ]
918  ]);
919
920val POLY_ORDER = store_thm("POLY_ORDER",
921 (Term`!p a. ~(poly p = poly [])
922         ==> ?!n. ([~a; &1] poly_exp n) poly_divides p /\
923                      ~(([~a; &1] poly_exp (SUC n)) poly_divides p)`),
924  MESON_TAC[POLY_ORDER_EXISTS, POLY_EXP_DIVIDES, LE_SUC_LT, LT_CASES]);
925
926(* ------------------------------------------------------------------------- *)
927(* Definition of order.                                                      *)
928(* ------------------------------------------------------------------------- *)
929
930val poly_order = new_definition ("poly_order",
931  (Term`poly_order a p = @n. ([~a; &1] poly_exp n) poly_divides p /\
932                   ~(([~a; &1] poly_exp (SUC n)) poly_divides p)`));
933
934val ORDER = store_thm("ORDER",
935 (Term`!p a n. ([~a; &1] poly_exp n) poly_divides p /\
936           ~(([~a; &1] poly_exp (SUC n)) poly_divides p) =
937           (n = poly_order a p) /\
938           ~(poly p = poly [])`),
939  REPEAT GEN_TAC THEN REWRITE_TAC[poly_order] THEN
940  EQ_TAC THEN STRIP_TAC THENL
941   [SUBGOAL_THEN (Term`~(poly p = poly [])`) ASSUME_TAC THENL
942     [FIRST_ASSUM(UNDISCH_TAC o assert is_neg o concl) THEN
943      CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[poly_divides] THEN
944      DISCH_THEN SUBST1_TAC THEN EXISTS_TAC (Term`[]:real list`) THEN
945      REWRITE_TAC[FUN_EQ_THM, POLY_MUL, poly, REAL_MUL_RZERO],
946      ASM_REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN
947      MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[]],
948    ONCE_ASM_REWRITE_TAC[] THEN CONV_TAC SELECT_CONV] THEN
949  ASM_MESON_TAC[POLY_ORDER]);
950
951val ORDER_THM = store_thm("ORDER_THM",
952 (Term`!p a. ~(poly p = poly [])
953         ==> ([~a; &1] poly_exp (poly_order a p)) poly_divides p /\
954             ~(([~a; &1] poly_exp (SUC(poly_order a p))) poly_divides p)`),
955  MESON_TAC[ORDER]);
956
957val ORDER_UNIQUE = store_thm("ORDER_UNIQUE",
958 (Term`!p a n. ~(poly p = poly []) /\
959           ([~a; &1] poly_exp n) poly_divides p /\
960           ~(([~a; &1] poly_exp (SUC n)) poly_divides p)
961           ==> (n = poly_order a p)`),
962  MESON_TAC[ORDER]);
963
964val ORDER_POLY = store_thm("ORDER_POLY",
965 (Term`!p q a. (poly p = poly q) ==> (poly_order a p = poly_order a q)`),
966  REPEAT STRIP_TAC THEN
967  ASM_REWRITE_TAC[poly_order, poly_divides, FUN_EQ_THM, POLY_MUL]);
968
969val ORDER_ROOT = store_thm("ORDER_ROOT",
970 (Term`!p a. (poly p a = &0) = (poly p = poly []) \/ ~(poly_order a p = 0)`),
971  REPEAT GEN_TAC THEN ASM_CASES_TAC (Term`poly p = poly []`) THEN
972  ASM_REWRITE_TAC[poly] THEN EQ_TAC THENL
973   [DISCH_THEN(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) THEN
974    ASM_CASES_TAC (Term`p:real list = []`) THENL [ASM_MESON_TAC[], ALL_TAC] THEN
975    ASM_REWRITE_TAC[] THEN
976    DISCH_THEN(X_CHOOSE_THEN (Term`q:real list`) SUBST_ALL_TAC) THEN DISCH_TAC THEN
977    FIRST_ASSUM(MP_TAC o SPEC (Term`a:real`) o MATCH_MP ORDER_THM) THEN
978    ASM_REWRITE_TAC[poly_exp, DE_MORGAN_THM] THEN DISJ2_TAC THEN
979    REWRITE_TAC[poly_divides] THEN EXISTS_TAC (Term`q:real list`) THEN
980    REWRITE_TAC[FUN_EQ_THM, POLY_MUL, poly] THEN REAL_ARITH_TAC,
981    DISCH_TAC THEN
982    FIRST_ASSUM(MP_TAC o SPEC (Term`a:real`) o MATCH_MP ORDER_THM) THEN
983    UNDISCH_TAC (Term`~(poly_order a p = 0)`) THEN
984    SPEC_TAC((Term`poly_order a p`),(Term`n:num`)) THEN
985    INDUCT_TAC THEN ASM_REWRITE_TAC[poly_exp, NOT_SUC] THEN
986    DISCH_THEN(MP_TAC o CONJUNCT1) THEN REWRITE_TAC[poly_divides] THEN
987    DISCH_THEN(X_CHOOSE_THEN (Term`s:real list`) SUBST1_TAC) THEN
988    REWRITE_TAC[POLY_MUL, poly] THEN REAL_ARITH_TAC]);
989
990val ORDER_DIVIDES = store_thm("ORDER_DIVIDES",
991 (Term`!p a n. ([~a; &1] poly_exp n) poly_divides p =
992           (poly p = poly []) \/ n <= poly_order a p`),
993  REPEAT GEN_TAC THEN ASM_CASES_TAC (Term`poly p = poly []`) THEN
994  ASM_REWRITE_TAC[] THENL
995   [ASM_REWRITE_TAC[poly_divides] THEN EXISTS_TAC (Term`[]:real list`) THEN
996    REWRITE_TAC[FUN_EQ_THM, POLY_MUL, poly, REAL_MUL_RZERO],
997    ASM_MESON_TAC[ORDER_THM, POLY_EXP_DIVIDES, NOT_LE, LE_SUC_LT]]);
998
999val ORDER_DECOMP = store_thm("ORDER_DECOMP",
1000 (Term`!p a. ~(poly p = poly [])
1001         ==> ?q. (poly p = poly (([~a; &1] poly_exp (poly_order a p)) * q)) /\
1002                 ~([~a; &1] poly_divides q)`),
1003  REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP ORDER_THM) THEN
1004  DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC o SPEC (Term`a:real`)) THEN
1005  DISCH_THEN(X_CHOOSE_TAC (Term`q:real list`) o REWRITE_RULE[poly_divides]) THEN
1006  EXISTS_TAC (Term`q:real list`) THEN ASM_REWRITE_TAC[] THEN
1007  DISCH_THEN(X_CHOOSE_TAC (Term`r: real list`) o REWRITE_RULE[poly_divides]) THEN
1008  UNDISCH_TAC (Term`~([~ a; &1] poly_exp SUC (poly_order a p) poly_divides p)`) THEN
1009  ASM_REWRITE_TAC[] THEN REWRITE_TAC[poly_divides] THEN
1010  EXISTS_TAC (Term`r:real list`) THEN
1011  ASM_REWRITE_TAC[POLY_MUL, FUN_EQ_THM, poly_exp] THEN
1012  REAL_ARITH_TAC);
1013
1014(* ------------------------------------------------------------------------- *)
1015(* Important composition properties of orders.                               *)
1016(* ------------------------------------------------------------------------- *)
1017
1018val ORDER_MUL = store_thm("ORDER_MUL",
1019 (Term`!a p q. ~(poly (p * q) = poly []) ==>
1020           (poly_order a (p * q) = poly_order a p + poly_order a q)`),
1021  REPEAT GEN_TAC
1022  THEN DISCH_THEN(fn th => ASSUME_TAC th THEN MP_TAC th)
1023  THEN REWRITE_TAC[POLY_ENTIRE, DE_MORGAN_THM]
1024  THEN STRIP_TAC
1025  THEN SUBGOAL_THEN (Term`(poly_order a p + poly_order a q
1026    = poly_order a (p * q)) /\ ~(poly (p * q) = poly [])`) MP_TAC
1027  THENL [
1028    ALL_TAC,
1029    MESON_TAC[]
1030  ]
1031  THEN REWRITE_TAC[GSYM ORDER]
1032  THEN CONJ_TAC
1033  THENL [
1034    MP_TAC(CONJUNCT1 (SPEC (Term`a:real`)
1035      (MATCH_MP ORDER_THM (ASSUME (Term`~(poly p = poly [])`)))))
1036    THEN DISCH_THEN(X_CHOOSE_TAC (Term`r: real list`) o REWRITE_RULE[poly_divides])
1037    THEN MP_TAC(CONJUNCT1 (SPEC (Term`a:real`)
1038      (MATCH_MP ORDER_THM (ASSUME (Term`~(poly q = poly [])`)))))
1039    THEN DISCH_THEN(X_CHOOSE_TAC (Term`s: real list`) o REWRITE_RULE[poly_divides])
1040    THEN REWRITE_TAC[poly_divides, FUN_EQ_THM]
1041    THEN EXISTS_TAC (Term`s * r`)
1042    THEN ASM_REWRITE_TAC[POLY_MUL, POLY_EXP_ADD]
1043    THEN REAL_ARITH_TAC,
1044    X_CHOOSE_THEN (Term`r: real list`) STRIP_ASSUME_TAC
1045    (SPEC (Term`a:real`) (MATCH_MP ORDER_DECOMP (ASSUME (Term`~(poly p = poly [])`))))
1046    THEN X_CHOOSE_THEN (Term`s: real list`) STRIP_ASSUME_TAC
1047    (SPEC (Term`a:real`) (MATCH_MP ORDER_DECOMP (ASSUME (Term`~(poly q = poly [])`))))
1048    THEN ASM_REWRITE_TAC[poly_divides, FUN_EQ_THM, POLY_EXP_ADD, POLY_MUL, poly_exp]
1049    THEN DISCH_THEN(X_CHOOSE_THEN (Term`t:real list`) STRIP_ASSUME_TAC)
1050    THEN SUBGOAL_THEN (Term`[~a; &1] poly_divides (r * s)`) MP_TAC
1051    THENL [
1052      ALL_TAC,
1053      ASM_REWRITE_TAC[POLY_PRIMES]
1054    ]
1055    THEN REWRITE_TAC[poly_divides]
1056    THEN EXISTS_TAC (Term`t:real list`)
1057    THEN SUBGOAL_THEN (Term`poly ([~ a; &1] poly_exp (poly_order a p) * (r * s)) =
1058      poly ([~ a; &1] poly_exp (poly_order a p) * ([~ a; &1] * t))`) MP_TAC
1059    THENL [
1060      ALL_TAC,
1061      MESON_TAC[POLY_MUL_LCANCEL, POLY_EXP_PRIME_EQ_0]
1062    ]
1063    THEN SUBGOAL_THEN (Term`poly ([~ a; &1] poly_exp (poly_order a q) *
1064                        ([~ a; &1] poly_exp (poly_order a p) * (r * s))) =
1065                  poly ([~ a; &1] poly_exp (poly_order a q) *
1066                        ([~ a; &1] poly_exp (poly_order a p) *
1067                         ([~ a; &1] * t)))`) MP_TAC
1068    THENL [
1069      ALL_TAC,
1070      MESON_TAC[POLY_MUL_LCANCEL, POLY_EXP_PRIME_EQ_0]
1071    ]
1072    THEN REWRITE_TAC[FUN_EQ_THM, POLY_MUL, POLY_ADD]
1073    THEN FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl)
1074    THEN SIMP_TAC real_ac_ss []
1075  ]);
1076
1077val ORDER_DIFF = store_thm("ORDER_DIFF",
1078 (Term`!p a. ~(poly (diff p) = poly []) /\
1079         ~(poly_order a p = 0)
1080         ==> (poly_order a p = SUC (poly_order a (diff p)))`),
1081  REPEAT GEN_TAC THEN
1082  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1083  SUBGOAL_THEN (Term`~(poly p = poly [])`) MP_TAC THENL
1084   [ASM_MESON_TAC[POLY_DIFF_ZERO], ALL_TAC] THEN
1085  DISCH_THEN(X_CHOOSE_THEN (Term`q:real list`) MP_TAC o
1086    SPEC (Term`a:real`) o MATCH_MP ORDER_DECOMP) THEN
1087  SPEC_TAC((Term`poly_order a p`),(Term`n:num`)) THEN
1088  INDUCT_TAC THEN REWRITE_TAC[NOT_SUC, SUC_INJ] THEN
1089  STRIP_TAC THEN MATCH_MP_TAC ORDER_UNIQUE THEN
1090  ASM_REWRITE_TAC[] THEN
1091  SUBGOAL_THEN (Term`!r. r poly_divides (diff p) =
1092                    r poly_divides (diff ([~ a; &1] poly_exp SUC n * q))`)
1093  (fn th => REWRITE_TAC[th]) THENL
1094   [GEN_TAC THEN REWRITE_TAC[poly_divides] THEN
1095    FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP POLY_DIFF_WELLDEF th]),
1096    ALL_TAC] THEN
1097  CONJ_TAC THENL
1098   [REWRITE_TAC[poly_divides, FUN_EQ_THM] THEN
1099    EXISTS_TAC (Term`[~a; &1] * (diff q) + &(SUC n) ## q`) THEN
1100    REWRITE_TAC[POLY_DIFF_MUL, POLY_DIFF_EXP_PRIME,
1101      POLY_ADD, POLY_MUL, POLY_CMUL] THEN
1102    REWRITE_TAC[poly_exp, POLY_MUL] THEN REAL_ARITH_TAC,
1103    REWRITE_TAC[FUN_EQ_THM, poly_divides, POLY_DIFF_MUL, POLY_DIFF_EXP_PRIME,
1104      POLY_ADD, POLY_MUL, POLY_CMUL] THEN
1105    DISCH_THEN(X_CHOOSE_THEN (Term`r:real list`) ASSUME_TAC) THEN
1106    UNDISCH_TAC (Term`~([~ a; &1] poly_divides q)`) THEN
1107    REWRITE_TAC[poly_divides] THEN
1108    EXISTS_TAC (Term`inv(&(SUC n)) ## (r + poly_neg(diff q))`) THEN
1109    SUBGOAL_THEN
1110        (Term`poly ([~a; &1] poly_exp n * q) =
1111         poly ([~a; &1] poly_exp n * ([~ a; &1] * (inv (&(SUC n)) ##
1112                                   (r + poly_neg (diff q)))))`)
1113    MP_TAC THENL
1114     [ALL_TAC, MESON_TAC[POLY_MUL_LCANCEL, POLY_EXP_PRIME_EQ_0]] THEN
1115    REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC (Term`x:real`) THEN
1116    SUBGOAL_THEN
1117        (Term`!a b. (&(SUC n) * a = &(SUC n) * b) ==> (a = b)`)
1118    MATCH_MP_TAC THENL
1119     [REWRITE_TAC[REAL_EQ_MUL_LCANCEL, REAL_OF_NUM_EQ, NOT_SUC], ALL_TAC] THEN
1120    REWRITE_TAC[POLY_MUL, POLY_CMUL] THEN
1121    SUBGOAL_THEN (Term`!a b c. &(SUC n) * (a * (b * (inv(&(SUC n)) * c))) =
1122                          a * (b * c)`)
1123    (fn th => REWRITE_TAC[th]) THENL
1124      [REPEAT GEN_TAC THEN
1125       GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
1126       REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN
1127       AP_TERM_TAC THEN
1128       GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
1129       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
1130       REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN
1131       MATCH_MP_TAC REAL_MUL_RINV THEN
1132       REWRITE_TAC[REAL_OF_NUM_EQ, NOT_SUC], ALL_TAC] THEN
1133    FIRST_ASSUM(MP_TAC o SPEC (Term`x:real`)) THEN
1134    REWRITE_TAC[poly_exp, POLY_MUL, POLY_ADD, POLY_NEG] THEN
1135    REAL_ARITH_TAC]);
1136
1137(* ------------------------------------------------------------------------- *)
1138(* Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').    *)
1139(* ------------------------------------------------------------------------- *)
1140
1141val POLY_SQUAREFREE_DECOMP_ORDER = store_thm("POLY_SQUAREFREE_DECOMP_ORDER",
1142 (Term`!p q d e r s.
1143        ~(poly (diff p) = poly []) /\
1144        (poly p = poly (q * d)) /\
1145        (poly (diff p) = poly (e * d)) /\
1146        (poly d = poly (r * p + s * diff p))
1147        ==> !a. poly_order a q = (if (poly_order a p = 0) then 0 else 1)`),
1148  REPEAT STRIP_TAC THEN
1149  SUBGOAL_THEN (Term`poly_order a p = poly_order a q + poly_order a d`) MP_TAC THENL
1150   [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC (Term`poly_order a (q * d)`) THEN
1151    CONJ_TAC THENL
1152     [MATCH_MP_TAC ORDER_POLY THEN ASM_REWRITE_TAC[],
1153      MATCH_MP_TAC ORDER_MUL THEN
1154      FIRST_ASSUM(fn th =>
1155        GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [SYM th]) THEN
1156      ASM_MESON_TAC[POLY_DIFF_ZERO]], ALL_TAC] THEN
1157  ASM_CASES_TAC (Term`poly_order a p = 0`) THEN ASM_REWRITE_TAC[] THENL
1158   [ARITH_TAC, ALL_TAC] THEN
1159  SUBGOAL_THEN (Term`poly_order a (diff p) =
1160                poly_order a e + poly_order a d`) MP_TAC THENL
1161   [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC (Term`poly_order a (e * d)`) THEN
1162    CONJ_TAC THENL
1163     [ASM_MESON_TAC[ORDER_POLY], ASM_MESON_TAC[ORDER_MUL]], ALL_TAC] THEN
1164  SUBGOAL_THEN (Term`~(poly p = poly [])`) ASSUME_TAC THENL
1165   [ASM_MESON_TAC[POLY_DIFF_ZERO], ALL_TAC] THEN
1166  MP_TAC(SPECL [(Term`p:real list`), (Term`a:real`)] ORDER_DIFF) THEN
1167  ASM_REWRITE_TAC[] THEN
1168  DISCH_THEN(fn th => MP_TAC th THEN MP_TAC(AP_TERM (Term`PRE`) th)) THEN
1169  REWRITE_TAC[PRE] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
1170  SUBGOAL_THEN (Term`poly_order a (diff p) <= poly_order a d`) MP_TAC THENL
1171   [SUBGOAL_THEN (Term`([~a; &1] poly_exp (poly_order a (diff p))) poly_divides d`)
1172    MP_TAC THENL [ALL_TAC, ASM_MESON_TAC[POLY_ENTIRE, ORDER_DIVIDES]] THEN
1173    SUBGOAL_THEN
1174      (Term`([~a; &1] poly_exp (poly_order a (diff p))) poly_divides p /\
1175       ([~a; &1] poly_exp (poly_order a (diff p))) poly_divides (diff p)`)
1176    MP_TAC THENL
1177     [REWRITE_TAC[ORDER_DIVIDES, LE_REFL] THEN DISJ2_TAC THEN
1178      REWRITE_TAC[ASSUME (Term`poly_order a (diff p) = PRE (poly_order a p)`)] THEN
1179      ARITH_TAC,
1180      DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN REWRITE_TAC[poly_divides] THEN
1181      REWRITE_TAC[ASSUME (Term`poly d = poly (r * p + s * diff p)`)] THEN
1182      POP_ASSUM_LIST(K ALL_TAC) THEN
1183      SIMP_TAC bool_ss [FUN_EQ_THM, POLY_MUL, POLY_ADD] THEN
1184      DISCH_THEN(X_CHOOSE_THEN (Term`f:real list`) ASSUME_TAC) THEN
1185      DISCH_THEN(X_CHOOSE_THEN (Term`g:real list`) ASSUME_TAC) THEN
1186      EXISTS_TAC (Term`r * g + s * f`)
1187      THEN GEN_TAC
1188      THEN SIMP_TAC real_ac_ss [POLY_MUL, POLY_ADD, REAL_LDISTRIB]
1189      THEN ASM_REWRITE_TAC [] THEN REAL_ARITH_TAC],
1190    ARITH_TAC]);
1191
1192(* ------------------------------------------------------------------------- *)
1193(* Define being "squarefree" --- NB with respect to real roots only.         *)
1194(* ------------------------------------------------------------------------- *)
1195
1196val rsquarefree = new_definition ("rsquarefree",
1197  (Term`rsquarefree p = ~(poly p = poly []) /\
1198                   !a. (poly_order a p = 0) \/ (poly_order a p = 1)`));
1199
1200(* ------------------------------------------------------------------------- *)
1201(* Standard squarefree criterion and rephasing of squarefree decomposition.  *)
1202(* ------------------------------------------------------------------------- *)
1203
1204val RSQUAREFREE_ROOTS = store_thm("RSQUAREFREE_ROOTS",
1205 (Term`!p. rsquarefree p = !a. ~((poly p a = &0) /\ (poly (diff p) a = &0))`),
1206  GEN_TAC THEN REWRITE_TAC[rsquarefree] THEN
1207  ASM_CASES_TAC (Term`poly p = poly []`) THEN ASM_REWRITE_TAC[] THENL
1208   [FIRST_ASSUM(SUBST1_TAC o MATCH_MP POLY_DIFF_ZERO) THEN
1209    ASM_REWRITE_TAC[poly, NOT_FORALL_THM],
1210    ASM_CASES_TAC (Term`poly(diff p) = poly []`) THEN ASM_REWRITE_TAC[] THENL
1211     [FIRST_ASSUM(X_CHOOSE_THEN (Term`h:real`) MP_TAC o
1212        MATCH_MP POLY_DIFF_ISZERO) THEN
1213      DISCH_THEN(fn th => ASSUME_TAC th THEN MP_TAC th) THEN
1214      DISCH_THEN(fn th => REWRITE_TAC[MATCH_MP ORDER_POLY th]) THEN
1215      UNDISCH_TAC (Term`~(poly p = poly [])`) THEN ASM_REWRITE_TAC[poly] THEN
1216      REWRITE_TAC[FUN_EQ_THM, poly, REAL_MUL_RZERO, REAL_ADD_RID] THEN
1217      DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1218      X_GEN_TAC (Term`a:real`) THEN DISJ1_TAC THEN
1219      MP_TAC(SPECL [(Term`[h:real]`), (Term`a:real`)] ORDER_ROOT) THEN
1220      ASM_REWRITE_TAC[FUN_EQ_THM, poly, REAL_MUL_RZERO, REAL_ADD_RID],
1221      ASM_REWRITE_TAC[ORDER_ROOT, DE_MORGAN_THM, ONE] THEN
1222      ASM_MESON_TAC[ORDER_DIFF, SUC_INJ]]]);
1223
1224val RSQUAREFREE_DECOMP = store_thm("RSQUAREFREE_DECOMP",
1225 (Term`!p a. rsquarefree p /\ (poly p a = &0)
1226         ==> ?q. (poly p = poly ([~a; &1] * q)) /\
1227                 ~(poly q a = &0)`),
1228  REPEAT GEN_TAC THEN REWRITE_TAC[rsquarefree] THEN STRIP_TAC THEN
1229  FIRST_ASSUM(MP_TAC o MATCH_MP ORDER_DECOMP) THEN
1230  DISCH_THEN(X_CHOOSE_THEN (Term`q:real list`) MP_TAC o SPEC (Term`a:real`)) THEN
1231  FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ORDER_ROOT]) THEN
1232  FIRST_ASSUM(DISJ_CASES_TAC o SPEC (Term`a:real`)) THEN
1233  ASM_SIMP_TAC real_ac_ss [] THEN
1234  DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN
1235  EXISTS_TAC (Term`q:real list`) THEN CONJ_TAC THENL
1236   [REWRITE_TAC[FUN_EQ_THM, POLY_MUL] THEN GEN_TAC THEN
1237    AP_THM_TAC THEN AP_TERM_TAC THEN
1238    GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV) [ONE] THEN
1239    REWRITE_TAC[poly_exp, POLY_MUL] THEN
1240    REWRITE_TAC[poly] THEN REAL_ARITH_TAC,
1241    DISCH_TAC THEN UNDISCH_TAC (Term`~([~a; &1] poly_divides q)`) THEN
1242    REWRITE_TAC[poly_divides] THEN
1243    UNDISCH_TAC (Term`poly q a = &0`) THEN
1244    GEN_REWRITE_TAC LAND_CONV [POLY_LINEAR_DIVIDES] THEN
1245    ASM_CASES_TAC (Term`q:real list = []`) THEN ASM_REWRITE_TAC[] THENL
1246     [EXISTS_TAC (Term`[] : real list`) THEN REWRITE_TAC[FUN_EQ_THM] THEN
1247      REWRITE_TAC[POLY_MUL, poly, REAL_MUL_RZERO],
1248      MESON_TAC[]]]);
1249
1250val POLY_SQUAREFREE_DECOMP = store_thm("POLY_SQUAREFREE_DECOMP",
1251 (Term`!p q d e r s.
1252        ~(poly (diff p) = poly []) /\
1253        (poly p = poly (q * d)) /\
1254        (poly (diff p) = poly (e * d)) /\
1255        (poly d = poly (r * p + s * diff p))
1256        ==> rsquarefree q /\ (!a. (poly q a = &0) = (poly p a = &0))`),
1257  REPEAT GEN_TAC THEN DISCH_THEN(fn th => MP_TAC th THEN
1258    ASSUME_TAC(MATCH_MP POLY_SQUAREFREE_DECOMP_ORDER th)) THEN
1259  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1260  SUBGOAL_THEN (Term`~(poly p = poly [])`) ASSUME_TAC THENL
1261   [ASM_MESON_TAC[POLY_DIFF_ZERO], ALL_TAC] THEN
1262  DISCH_THEN(ASSUME_TAC o CONJUNCT1) THEN
1263  UNDISCH_TAC (Term`~(poly p = poly [])`) THEN
1264  DISCH_THEN(fn th => MP_TAC th THEN MP_TAC th) THEN
1265  DISCH_THEN(fn th => ASM_REWRITE_TAC[] THEN ASSUME_TAC th) THEN
1266  ASM_REWRITE_TAC[] THEN
1267  REWRITE_TAC[POLY_ENTIRE, DE_MORGAN_THM] THEN STRIP_TAC THEN
1268  UNDISCH_TAC (Term`poly p = poly (q * d)`) THEN
1269  DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
1270  ASM_REWRITE_TAC[rsquarefree, ORDER_ROOT] THEN
1271  CONJ_TAC THEN GEN_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC real_ac_ss []);
1272
1273(* ------------------------------------------------------------------------- *)
1274(* Normalization of a polynomial.                                            *)
1275(* ------------------------------------------------------------------------- *)
1276
1277val normalize = new_recursive_definition list_Axiom "normalize"
1278  (Term`(normalize [] = []) /\
1279   (normalize (CONS h t) = (if (normalize t = []) then
1280                              if (h = &0) then [] else [h]
1281                            else CONS h (normalize t)))`);
1282
1283val POLY_NORMALIZE = store_thm("POLY_NORMALIZE",
1284 (Term`!p. poly (normalize p) = poly p`),
1285  LIST_INDUCT_TAC THEN REWRITE_TAC[normalize, poly] THEN
1286  ASM_CASES_TAC (Term`h = &0`) THEN ASM_REWRITE_TAC[] THEN
1287  COND_CASES_TAC THEN ASM_REWRITE_TAC[poly, FUN_EQ_THM] THEN
1288  UNDISCH_TAC (Term`poly (normalize t) = poly t`) THEN
1289  DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[poly] THEN
1290  REWRITE_TAC[REAL_MUL_RZERO, REAL_ADD_LID]);
1291
1292(* ------------------------------------------------------------------------- *)
1293(* The degree of a polynomial.                                               *)
1294(* ------------------------------------------------------------------------- *)
1295
1296val degree = new_definition ("degree",
1297  (Term`degree p = PRE(LENGTH(normalize p))`));
1298
1299val DEGREE_ZERO = store_thm("DEGREE_ZERO",
1300 (Term`!p. (poly p = poly []) ==> (degree p = 0)`),
1301  REPEAT STRIP_TAC THEN REWRITE_TAC[degree] THEN
1302  SUBGOAL_THEN (Term`normalize p = []`) SUBST1_TAC THENL
1303   [POP_ASSUM MP_TAC THEN SPEC_TAC((Term`p:real list`),(Term`p:real list`)) THEN
1304    REWRITE_TAC[POLY_ZERO] THEN
1305    LIST_INDUCT_TAC THEN REWRITE_TAC[normalize, FORALL] THEN
1306    STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1307    SUBGOAL_THEN (Term`normalize t = []`) (fn th => REWRITE_TAC[th]) THEN
1308    FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[],
1309    REWRITE_TAC[LENGTH, PRE]]);
1310
1311(* ------------------------------------------------------------------------- *)
1312(* Tidier versions of finiteness of roots.                                   *)
1313(* ------------------------------------------------------------------------- *)
1314
1315val POLY_ROOTS_FINITE_SET = store_thm("POLY_ROOTS_FINITE_SET",
1316 (Term`!p. ~(poly p = poly []) ==> FINITE {x | poly p x = &0}`),
1317  GEN_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE] THEN
1318  DISCH_THEN(X_CHOOSE_THEN (Term`N:num`) MP_TAC) THEN
1319  DISCH_THEN(X_CHOOSE_THEN (Term`i:num->real`) ASSUME_TAC) THEN
1320  MATCH_MP_TAC FINITE_SUBSET THEN
1321  EXISTS_TAC (Term`{x:real | ?n:num. n < N /\ (x = i n)}`) THEN
1322  CONJ_TAC THENL
1323   [SPEC_TAC((Term`N:num`),(Term`N:num`)) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
1324    INDUCT_TAC THENL
1325     [SUBGOAL_THEN (Term`{x:real | ?n:num. n < 0 /\ (x = i n)} = {}`)
1326      (fn th => REWRITE_TAC[th, FINITE_RULES]) THEN
1327      SIMP_TAC bool_ss [GSPEC_DEF, EMPTY_DEF, pairTheory.CLOSED_PAIR_EQ,
1328        NOT_LESS, EQT_ELIM (ARITH_CONV (Term`!n:num. ~(n < 0)`))],
1329      SUBGOAL_THEN (Term`{x:real | ?n. n < SUC N /\ (x = i n)} =
1330                    (i N) INSERT {x:real | ?n:num. n < N /\ (x = i n)}`)
1331      SUBST1_TAC THENL
1332       [SIMP_TAC bool_ss [LT, EXTENSION, IN_INSERT, SPECIFICATION,
1333                          GSPEC_DEF,pairTheory.CLOSED_PAIR_EQ]
1334        THEN MESON_TAC[],
1335        MATCH_MP_TAC(CONJUNCT2 FINITE_RULES) THEN ASM_REWRITE_TAC[]]],
1336    ASM_SIMP_TAC bool_ss [SUBSET_DEF, SPECIFICATION, GSPEC_DEF,
1337                          pairTheory.CLOSED_PAIR_EQ]
1338    THEN ASM_MESON_TAC[]]);
1339
1340(* ------------------------------------------------------------------------- *)
1341(* Crude bound for polynomial.                                               *)
1342(* ------------------------------------------------------------------------- *)
1343
1344val POLY_MONO = store_thm("POLY_MONO",
1345 (Term`!x k p. abs(x) <= k ==> abs(poly p x) <= poly (MAP abs p) k`),
1346  GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1347  DISCH_TAC THEN LIST_INDUCT_TAC THEN
1348  REWRITE_TAC[poly, REAL_LE_REFL, MAP, REAL_ABS_0] THEN
1349  MATCH_MP_TAC REAL_LE_TRANS THEN
1350  EXISTS_TAC (Term`abs(h) + abs(x * poly t x)`) THEN
1351  REWRITE_TAC[REAL_ABS_TRIANGLE, REAL_LE_LADD] THEN
1352  REWRITE_TAC[REAL_ABS_MUL] THEN
1353  MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[REAL_ABS_POS]);
1354
1355(* ------------------------------------------------------------------------- *)
1356(* Conversions to perform operations if coefficients are rational constants. *)
1357(* ------------------------------------------------------------------------- *)
1358
1359(*
1360val POLY_DIFF_CONV =
1361  let
1362    val aux_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 poly_diff_aux]
1363    val aux_conv1 = GEN_REWRITE_CONV I [CONJUNCT2 poly_diff_aux]
1364    val diff_conv0 = GEN_REWRITE_CONV I (butlast (CONJUNCTS POLY_DIFF_CLAUSES))
1365    val diff_conv1 = GEN_REWRITE_CONV I [last (CONJUNCTS POLY_DIFF_CLAUSES)]
1366    fun POLY_DIFF_AUX_CONV tm =
1367      (aux_conv0 ORELSEC
1368      (aux_conv1 THENC
1369      LAND_CONV REAL_RAT_MUL_CONV THENC
1370      RAND_CONV (LAND_CONV NUM_SUC_CONV THENC POLY_DIFF_AUX_CONV))) tm
1371  in
1372    diff_conv0 ORELSEC (diff_conv1 THENC POLY_DIFF_AUX_CONV)
1373  end;
1374
1375val POLY_CMUL_CONV =
1376  let cmul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 poly_cmul]
1377  and cmul_conv1 = GEN_REWRITE_CONV I [CONJUNCT2 poly_cmul] in
1378  let rec POLY_CMUL_CONV tm =
1379   (cmul_conv0 ORELSEC
1380    (cmul_conv1 THENC
1381     LAND_CONV REAL_RAT_MUL_CONV THENC
1382     RAND_CONV POLY_CMUL_CONV)) tm in
1383  POLY_CMUL_CONV;
1384
1385val POLY_ADD_CONV =
1386  let add_conv0 = GEN_REWRITE_CONV I (butlast (CONJUNCTS POLY_ADD_CLAUSES))
1387  and add_conv1 = GEN_REWRITE_CONV I [last (CONJUNCTS POLY_ADD_CLAUSES)] in
1388  let rec POLY_ADD_CONV tm =
1389   (add_conv0 ORELSEC
1390    (add_conv1 THENC
1391     LAND_CONV REAL_RAT_ADD_CONV THENC
1392     RAND_CONV POLY_ADD_CONV)) tm in
1393  POLY_ADD_CONV;
1394
1395val POLY_MUL_CONV =
1396  let mul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 POLY_MUL_CLAUSES]
1397  and mul_conv1 = GEN_REWRITE_CONV I [CONJUNCT1(CONJUNCT2 POLY_MUL_CLAUSES)]
1398  and mul_conv2 = GEN_REWRITE_CONV I [CONJUNCT2(CONJUNCT2 POLY_MUL_CLAUSES)] in
1399  let rec POLY_MUL_CONV tm =
1400   (mul_conv0 ORELSEC
1401    (mul_conv1 THENC POLY_CMUL_CONV) ORELSEC
1402    (mul_conv2 THENC
1403     LAND_CONV POLY_CMUL_CONV THENC
1404     RAND_CONV(RAND_CONV POLY_MUL_CONV) THENC
1405     POLY_ADD_CONV)) tm in
1406  POLY_MUL_CONV;
1407
1408val POLY_NORMALIZE_CONV =
1409  let pth = prove
1410   ((Term`normalize (CONS h t) =
1411      (\n. (n = []) => (h = &0) => [] | [h] | CONS h n) (normalize t)`),
1412    REWRITE_TAC[normalize]) in
1413  let norm_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 normalize]
1414  and norm_conv1 = GEN_REWRITE_CONV I [pth]
1415  and norm_conv2 = GEN_REWRITE_CONV DEPTH_CONV
1416   [COND_CLAUSES, NOT_CONS_NIL, EQT_INTRO(SPEC_ALL EQ_REFL)] in
1417  let rec POLY_NORMALIZE_CONV tm =
1418   (norm_conv0 ORELSEC
1419    (norm_conv1 THENC
1420     RAND_CONV POLY_NORMALIZE_CONV THENC
1421     BETA_CONV THENC
1422     RATOR_CONV(RAND_CONV(RATOR_CONV(LAND_CONV REAL_RAT_EQ_CONV))) THENC
1423     norm_conv2)) tm in
1424  POLY_NORMALIZE_CONV;
1425*)
1426
1427val _ = export_theory ();
1428