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