|
1 (* Title: Poly.ML |
|
2 Author: Jacques D. Fleuriot |
|
3 Copyright: 2000 University of Edinburgh |
|
4 Description: Properties of real polynomials following |
|
5 John Harrison's HOL-Light implementation. |
|
6 Some early theorems by Lucas Dixon |
|
7 *) |
|
8 |
|
9 Goal "p +++ [] = p"; |
|
10 by (induct_tac "p" 1); |
|
11 by Auto_tac; |
|
12 qed "padd_Nil2"; |
|
13 Addsimps [padd_Nil2]; |
|
14 |
|
15 Goal "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)"; |
|
16 by Auto_tac; |
|
17 qed "padd_Cons_Cons"; |
|
18 |
|
19 Goal "-- [] = []"; |
|
20 by (rewtac poly_minus_def); |
|
21 by (Auto_tac); |
|
22 qed "pminus_Nil"; |
|
23 Addsimps [pminus_Nil]; |
|
24 |
|
25 Goal "[h1] *** p1 = h1 %* p1"; |
|
26 by (Simp_tac 1); |
|
27 qed "pmult_singleton"; |
|
28 |
|
29 Goal "1 %* t = t"; |
|
30 by (induct_tac "t" 1); |
|
31 by Auto_tac; |
|
32 qed "poly_ident_mult"; |
|
33 Addsimps [poly_ident_mult]; |
|
34 |
|
35 Goal "[a] +++ ((0)#t) = (a#t)"; |
|
36 by (Simp_tac 1); |
|
37 qed "poly_simple_add_Cons"; |
|
38 Addsimps [poly_simple_add_Cons]; |
|
39 |
|
40 (*-------------------------------------------------------------------------*) |
|
41 (* Handy general properties *) |
|
42 (*-------------------------------------------------------------------------*) |
|
43 |
|
44 Goal "b +++ a = a +++ b"; |
|
45 by (subgoal_tac "ALL a. b +++ a = a +++ b" 1); |
|
46 by (induct_tac "b" 2); |
|
47 by Auto_tac; |
|
48 by (rtac (padd_Cons RS ssubst) 1); |
|
49 by (case_tac "aa" 1); |
|
50 by Auto_tac; |
|
51 qed "padd_commut"; |
|
52 |
|
53 Goal "(a +++ b) +++ c = a +++ (b +++ c)"; |
|
54 by (subgoal_tac "ALL b c. (a +++ b) +++ c = a +++ (b +++ c)" 1); |
|
55 by (Asm_simp_tac 1); |
|
56 by (induct_tac "a" 1); |
|
57 by (Step_tac 2); |
|
58 by (case_tac "b" 2); |
|
59 by (Asm_simp_tac 2); |
|
60 by (Asm_simp_tac 2); |
|
61 by (Asm_simp_tac 1); |
|
62 qed "padd_assoc"; |
|
63 |
|
64 Goal "a %* ( p +++ q ) = (a %* p +++ a %* q)"; |
|
65 by (subgoal_tac "ALL q. a %* ( p +++ q ) = (a %* p +++ a %* q) " 1); |
|
66 by (induct_tac "p" 2); |
|
67 by (Simp_tac 2); |
|
68 by (rtac allI 2 ); |
|
69 by (case_tac "q" 2); |
|
70 by (Asm_simp_tac 2); |
|
71 by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib2] ) 2); |
|
72 by (Asm_simp_tac 1); |
|
73 qed "poly_cmult_distr"; |
|
74 |
|
75 Goal "[0, 1] *** t = ((0)#t)"; |
|
76 by (induct_tac "t" 1); |
|
77 by (Simp_tac 1); |
|
78 by (simp_tac (simpset() addsimps [poly_ident_mult, padd_commut]) 1); |
|
79 by (case_tac "list" 1); |
|
80 by (Asm_simp_tac 1); |
|
81 by (asm_full_simp_tac (simpset() addsimps [poly_ident_mult, padd_commut]) 1); |
|
82 qed "pmult_by_x"; |
|
83 Addsimps [pmult_by_x]; |
|
84 |
|
85 |
|
86 (*-------------------------------------------------------------------------*) |
|
87 (* properties of evaluation of polynomials. *) |
|
88 (*-------------------------------------------------------------------------*) |
|
89 |
|
90 Goal "poly (p1 +++ p2) x = poly p1 x + poly p2 x"; |
|
91 by (subgoal_tac "ALL p2. poly (p1 +++ p2) x = poly( p1 ) x + poly( p2 ) x" 1); |
|
92 by (induct_tac "p1" 2); |
|
93 by Auto_tac; |
|
94 by (case_tac "p2" 1); |
|
95 by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2])); |
|
96 qed "poly_add"; |
|
97 |
|
98 Goal "poly (c %* p) x = c * poly p x"; |
|
99 by (induct_tac "p" 1); |
|
100 by (case_tac "x=0" 2); |
|
101 by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2] |
|
102 @ real_mult_ac)); |
|
103 qed "poly_cmult"; |
|
104 |
|
105 Goalw [poly_minus_def] "poly (-- p) x = - (poly p x)"; |
|
106 by (auto_tac (claset(),simpset() addsimps [poly_cmult])); |
|
107 qed "poly_minus"; |
|
108 |
|
109 Goal "poly (p1 *** p2) x = poly p1 x * poly p2 x"; |
|
110 by (subgoal_tac "ALL p2. poly (p1 *** p2) x = poly p1 x * poly p2 x" 1); |
|
111 by (Asm_simp_tac 1); |
|
112 by (induct_tac "p1" 1); |
|
113 by (auto_tac (claset(),simpset() addsimps [poly_cmult])); |
|
114 by (case_tac "list" 1); |
|
115 by (auto_tac (claset(),simpset() addsimps [poly_cmult,poly_add, |
|
116 real_add_mult_distrib,real_add_mult_distrib2] @ real_mult_ac)); |
|
117 qed "poly_mult"; |
|
118 |
|
119 Goal "poly (p %^ n) x = (poly p x) ^ n"; |
|
120 by (induct_tac "n" 1); |
|
121 by (auto_tac (claset(),simpset() addsimps [poly_cmult, poly_mult])); |
|
122 qed "poly_exp"; |
|
123 |
|
124 (*-------------------------------------------------------------------------*) |
|
125 (* More Polynomial Evaluation Lemmas *) |
|
126 (*-------------------------------------------------------------------------*) |
|
127 |
|
128 Goal "poly (a +++ []) x = poly a x"; |
|
129 by (Simp_tac 1); |
|
130 qed "poly_add_rzero"; |
|
131 Addsimps [poly_add_rzero]; |
|
132 |
|
133 Goal "poly ((a *** b) *** c) x = poly (a *** (b *** c)) x"; |
|
134 by (simp_tac (simpset() addsimps [poly_mult,real_mult_assoc]) 1); |
|
135 qed "poly_mult_assoc"; |
|
136 |
|
137 Goal "poly (p *** []) x = 0"; |
|
138 by (induct_tac "p" 1); |
|
139 by Auto_tac; |
|
140 qed "poly_mult_Nil2"; |
|
141 Addsimps [poly_mult_Nil2]; |
|
142 |
|
143 Goal "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d ) x"; |
|
144 by (induct_tac "n" 1); |
|
145 by (auto_tac (claset(), simpset() addsimps [poly_mult,real_mult_assoc])); |
|
146 qed "poly_exp_add"; |
|
147 |
|
148 (*-------------------------------------------------------------------------*) |
|
149 (* The derivative *) |
|
150 (*-------------------------------------------------------------------------*) |
|
151 |
|
152 Goalw [pderiv_def] "pderiv [] = []"; |
|
153 by (Simp_tac 1); |
|
154 qed "pderiv_Nil"; |
|
155 Addsimps [pderiv_Nil]; |
|
156 |
|
157 Goalw [pderiv_def] "pderiv [c] = []"; |
|
158 by (Simp_tac 1); |
|
159 qed "pderiv_singleton"; |
|
160 Addsimps [pderiv_singleton]; |
|
161 |
|
162 Goalw [pderiv_def] "pderiv (h#t) = pderiv_aux 1 t"; |
|
163 by (Simp_tac 1); |
|
164 qed "pderiv_Cons"; |
|
165 |
|
166 Goal "DERIV f x :> D ==> DERIV (%x. (f x) * c) x :> D * c"; |
|
167 by (auto_tac (claset() addIs [DERIV_cmult,real_mult_commute RS subst], |
|
168 simpset() addsimps [real_mult_commute])); |
|
169 qed "DERIV_cmult2"; |
|
170 |
|
171 Goal "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"; |
|
172 by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_pow 1); |
|
173 by (Simp_tac 1); |
|
174 qed "DERIV_pow2"; |
|
175 Addsimps [DERIV_pow2,DERIV_pow]; |
|
176 |
|
177 Goal "ALL n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :> \ |
|
178 \ x ^ n * poly (pderiv_aux (Suc n) p) x "; |
|
179 by (induct_tac "p" 1); |
|
180 by (auto_tac (claset() addSIs [DERIV_add,DERIV_cmult2],simpset() addsimps |
|
181 [pderiv_def,real_add_mult_distrib2,real_mult_assoc RS sym] delsimps |
|
182 [realpow_Suc])); |
|
183 by (rtac (real_mult_commute RS subst) 1); |
|
184 by (simp_tac (simpset() delsimps [realpow_Suc]) 1); |
|
185 by (asm_full_simp_tac (simpset() addsimps [real_mult_commute,realpow_Suc RS sym] |
|
186 delsimps [realpow_Suc]) 1); |
|
187 qed "lemma_DERIV_poly1"; |
|
188 |
|
189 Goal "DERIV (%x. (x ^ (Suc n) * poly p x)) x :> \ |
|
190 \ x ^ n * poly (pderiv_aux (Suc n) p) x "; |
|
191 by (simp_tac (simpset() addsimps [lemma_DERIV_poly1] delsimps [realpow_Suc]) 1); |
|
192 qed "lemma_DERIV_poly"; |
|
193 |
|
194 Goal "DERIV f x :> D ==> DERIV (%x. a + f x) x :> D"; |
|
195 by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_add 1); |
|
196 by Auto_tac; |
|
197 qed "DERIV_add_const"; |
|
198 |
|
199 Goal "DERIV (%x. poly p x) x :> poly (pderiv p) x"; |
|
200 by (induct_tac "p" 1); |
|
201 by (auto_tac (claset(),simpset() addsimps [pderiv_Cons])); |
|
202 by (rtac DERIV_add_const 1); |
|
203 by (rtac lemma_DERIV_subst 1); |
|
204 by (rtac (full_simplify (simpset()) |
|
205 (read_instantiate [("n","0")] lemma_DERIV_poly)) 1); |
|
206 by (simp_tac (simpset() addsimps [CLAIM "1 = 1"]) 1); |
|
207 qed "poly_DERIV"; |
|
208 Addsimps [poly_DERIV]; |
|
209 |
|
210 |
|
211 (*-------------------------------------------------------------------------*) |
|
212 (* Consequences of the derivative theorem above *) |
|
213 (*-------------------------------------------------------------------------*) |
|
214 |
|
215 Goalw [differentiable_def] "(%x. poly p x) differentiable x"; |
|
216 by (blast_tac (claset() addIs [poly_DERIV]) 1); |
|
217 qed "poly_differentiable"; |
|
218 Addsimps [poly_differentiable]; |
|
219 |
|
220 Goal "isCont (%x. poly p x) x"; |
|
221 by (rtac (poly_DERIV RS DERIV_isCont) 1); |
|
222 qed "poly_isCont"; |
|
223 Addsimps [poly_isCont]; |
|
224 |
|
225 Goal "[| a < b; poly p a < 0; 0 < poly p b |] \ |
|
226 \ ==> EX x. a < x & x < b & (poly p x = 0)"; |
|
227 by (cut_inst_tac [("f","%x. poly p x"),("a","a"),("b","b"),("y","0")] |
|
228 IVT_objl 1); |
|
229 by (auto_tac (claset(),simpset() addsimps [real_le_less])); |
|
230 qed "poly_IVT_pos"; |
|
231 |
|
232 Goal "[| a < b; 0 < poly p a; poly p b < 0 |] \ |
|
233 \ ==> EX x. a < x & x < b & (poly p x = 0)"; |
|
234 by (blast_tac (claset() addIs [full_simplify (simpset() |
|
235 addsimps [poly_minus, rename_numerals real_minus_zero_less_iff2]) |
|
236 (read_instantiate [("p","-- p")] poly_IVT_pos)]) 1); |
|
237 qed "poly_IVT_neg"; |
|
238 |
|
239 Goal "a < b ==> \ |
|
240 \ EX x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"; |
|
241 by (dres_inst_tac [("f","poly p")] MVT 1); |
|
242 by Auto_tac; |
|
243 by (res_inst_tac [("x","z")] exI 1); |
|
244 by (auto_tac (claset() addDs [ARITH_PROVE |
|
245 "[| a < z; z < b |] ==> (b - (a::real)) ~= 0"],simpset() |
|
246 addsimps [real_mult_left_cancel,poly_DERIV RS DERIV_unique])); |
|
247 qed "poly_MVT"; |
|
248 |
|
249 |
|
250 (*-------------------------------------------------------------------------*) |
|
251 (* Lemmas for Derivatives *) |
|
252 (*-------------------------------------------------------------------------*) |
|
253 |
|
254 Goal "ALL p2 n. poly (pderiv_aux n (p1 +++ p2)) x = \ |
|
255 \ poly (pderiv_aux n p1 +++ pderiv_aux n p2) x"; |
|
256 by (induct_tac "p1" 1); |
|
257 by (Step_tac 2); |
|
258 by (case_tac "p2" 2); |
|
259 by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2])); |
|
260 qed "lemma_poly_pderiv_aux_add"; |
|
261 |
|
262 Goal "poly (pderiv_aux n (p1 +++ p2)) x = \ |
|
263 \ poly (pderiv_aux n p1 +++ pderiv_aux n p2) x"; |
|
264 by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_add]) 1); |
|
265 qed "poly_pderiv_aux_add"; |
|
266 |
|
267 Goal "ALL n. poly (pderiv_aux n (c %* p) ) x = poly (c %* pderiv_aux n p) x"; |
|
268 by (induct_tac "p" 1); |
|
269 by (auto_tac (claset(),simpset() addsimps [poly_cmult] @ real_mult_ac)); |
|
270 qed "lemma_poly_pderiv_aux_cmult"; |
|
271 |
|
272 Goal "poly (pderiv_aux n (c %* p) ) x = poly (c %* pderiv_aux n p) x"; |
|
273 by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_cmult]) 1); |
|
274 qed "poly_pderiv_aux_cmult"; |
|
275 |
|
276 Goalw [poly_minus_def] |
|
277 "poly (pderiv_aux n (-- p)) x = poly (-- pderiv_aux n p) x"; |
|
278 by (simp_tac (simpset() addsimps [poly_pderiv_aux_cmult]) 1); |
|
279 qed "poly_pderiv_aux_minus"; |
|
280 |
|
281 Goal "ALL n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"; |
|
282 by (induct_tac "p" 1); |
|
283 by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc, |
|
284 real_add_mult_distrib])); |
|
285 qed "lemma_poly_pderiv_aux_mult1"; |
|
286 |
|
287 Goal "poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"; |
|
288 by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_mult1]) 1); |
|
289 qed "lemma_poly_pderiv_aux_mult"; |
|
290 |
|
291 Goal "ALL q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x"; |
|
292 by (induct_tac "p" 1); |
|
293 by (Step_tac 2); |
|
294 by (case_tac "q" 2); |
|
295 by (auto_tac (claset(),simpset() addsimps [poly_pderiv_aux_add,poly_add, |
|
296 pderiv_def])); |
|
297 qed "lemma_poly_pderiv_add"; |
|
298 |
|
299 Goal "poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x"; |
|
300 by (simp_tac (simpset() addsimps [lemma_poly_pderiv_add]) 1); |
|
301 qed "poly_pderiv_add"; |
|
302 |
|
303 Goal "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x"; |
|
304 by (induct_tac "p" 1); |
|
305 by (auto_tac (claset(),simpset() addsimps [poly_pderiv_aux_cmult,poly_cmult, |
|
306 pderiv_def])); |
|
307 qed "poly_pderiv_cmult"; |
|
308 |
|
309 Goalw [poly_minus_def] "poly (pderiv (--p)) x = poly (--(pderiv p)) x"; |
|
310 by (simp_tac (simpset() addsimps [poly_pderiv_cmult]) 1); |
|
311 qed "poly_pderiv_minus"; |
|
312 |
|
313 Goalw [pderiv_def] |
|
314 "poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x"; |
|
315 by (induct_tac "t" 1); |
|
316 by (auto_tac (claset(),simpset() addsimps [poly_add, |
|
317 lemma_poly_pderiv_aux_mult])); |
|
318 qed "lemma_poly_mult_pderiv"; |
|
319 |
|
320 Goal "ALL q. poly (pderiv (p *** q)) x = \ |
|
321 \ poly (p *** (pderiv q) +++ q *** (pderiv p)) x"; |
|
322 by (induct_tac "p" 1); |
|
323 by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult, |
|
324 poly_pderiv_cmult,poly_pderiv_add,poly_mult])); |
|
325 by (rtac (lemma_poly_mult_pderiv RS ssubst) 1); |
|
326 by (rtac (lemma_poly_mult_pderiv RS ssubst) 1); |
|
327 by (rtac (poly_add RS ssubst) 1); |
|
328 by (rtac (poly_add RS ssubst) 1); |
|
329 by (asm_simp_tac (simpset() addsimps [poly_mult,real_add_mult_distrib2] |
|
330 @ real_add_ac @ real_mult_ac) 1); |
|
331 qed "poly_pderiv_mult"; |
|
332 |
|
333 Goal "poly (pderiv (p %^ (Suc n))) x = \ |
|
334 \ poly ((real (Suc n)) %* (p %^ n) *** pderiv p ) x"; |
|
335 by (induct_tac "n" 1); |
|
336 by (auto_tac (claset(),simpset() addsimps [poly_add,poly_pderiv_cmult, |
|
337 poly_cmult,poly_pderiv_mult,real_of_nat_zero,poly_mult, |
|
338 real_of_nat_Suc,real_add_mult_distrib2,real_add_mult_distrib] |
|
339 @ real_mult_ac)); |
|
340 qed "poly_pderiv_exp"; |
|
341 |
|
342 Goal "poly (pderiv ([-a, 1] %^ (Suc n))) x = \ |
|
343 \ poly (real (Suc n) %* ([-a, 1] %^ n)) x"; |
|
344 by (simp_tac (simpset() addsimps [poly_pderiv_exp,poly_mult] |
|
345 delsimps [pexp_Suc]) 1); |
|
346 by (simp_tac (simpset() addsimps [poly_cmult,pderiv_def]) 1); |
|
347 qed "poly_pderiv_exp_prime"; |
|
348 |
|
349 (* ----------------------------------------------------------------------- *) |
|
350 (* Key property that f(a) = 0 ==> (x - a) divides p(x). *) |
|
351 (* ----------------------------------------------------------------------- *) |
|
352 |
|
353 Goal "ALL h. EX q r. h#t = [r] +++ [-a, 1] *** q"; |
|
354 by (induct_tac "t" 1); |
|
355 by (Step_tac 1); |
|
356 by (res_inst_tac [("x","[]")] exI 1); |
|
357 by (res_inst_tac [("x","h")] exI 1); |
|
358 by (Simp_tac 1); |
|
359 by (dres_inst_tac [("x","aa")] spec 1); |
|
360 by (Step_tac 1); |
|
361 by (res_inst_tac [("x","r#q")] exI 1); |
|
362 by (res_inst_tac [("x","a*r + h")] exI 1); |
|
363 by (case_tac "q" 1); |
|
364 by (auto_tac (claset(),simpset() addsimps [real_minus_mult_eq1 RS sym])); |
|
365 qed "lemma_poly_linear_rem"; |
|
366 |
|
367 Goal "EX q r. h#t = [r] +++ [-a, 1] *** q"; |
|
368 by (cut_inst_tac [("t","t"),("a","a")] lemma_poly_linear_rem 1); |
|
369 by Auto_tac; |
|
370 qed "poly_linear_rem"; |
|
371 |
|
372 |
|
373 Goal "(poly p a = 0) = ((p = []) | (EX q. p = [-a, 1] *** q))"; |
|
374 by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult, |
|
375 real_add_mult_distrib2])); |
|
376 by (case_tac "p" 1); |
|
377 by (cut_inst_tac [("h","aa"),("t","list"),("a","a")] poly_linear_rem 2); |
|
378 by (Step_tac 2); |
|
379 by (case_tac "q" 1); |
|
380 by Auto_tac; |
|
381 by (dres_inst_tac [("x","[]")] spec 1); |
|
382 by (Asm_full_simp_tac 1); |
|
383 by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult, |
|
384 real_add_assoc])); |
|
385 by (dres_inst_tac [("x","aa#lista")] spec 1); |
|
386 by Auto_tac; |
|
387 qed "poly_linear_divides"; |
|
388 |
|
389 Goal "ALL h k a. length (k %* p +++ (h # (a %* p))) = Suc (length p)"; |
|
390 by (induct_tac "p" 1); |
|
391 by Auto_tac; |
|
392 qed "lemma_poly_length_mult"; |
|
393 Addsimps [lemma_poly_length_mult]; |
|
394 |
|
395 Goal "ALL h k. length (k %* p +++ (h # p)) = Suc (length p)"; |
|
396 by (induct_tac "p" 1); |
|
397 by Auto_tac; |
|
398 qed "lemma_poly_length_mult2"; |
|
399 Addsimps [lemma_poly_length_mult2]; |
|
400 |
|
401 Goal "length([-a ,1] *** q) = Suc (length q)"; |
|
402 by Auto_tac; |
|
403 qed "poly_length_mult"; |
|
404 Addsimps [poly_length_mult]; |
|
405 |
|
406 |
|
407 (*-------------------------------------------------------------------------*) |
|
408 (* Polynomial length *) |
|
409 (*-------------------------------------------------------------------------*) |
|
410 |
|
411 Goal "length (a %* p) = length p"; |
|
412 by (induct_tac "p" 1); |
|
413 by Auto_tac; |
|
414 qed "poly_cmult_length"; |
|
415 Addsimps [poly_cmult_length]; |
|
416 |
|
417 Goal "length (p1 +++ p2) = (if (length( p1 ) < length( p2 )) \ |
|
418 \ then (length( p2 )) else (length( p1) ))"; |
|
419 by (subgoal_tac "ALL p2. length (p1 +++ p2) = (if (length( p1 ) < \ |
|
420 \ length( p2 )) then (length( p2 )) else (length( p1) ))" 1); |
|
421 by (induct_tac "p1" 2); |
|
422 by (Simp_tac 2); |
|
423 by (Simp_tac 2); |
|
424 by (Step_tac 2); |
|
425 by (Asm_full_simp_tac 2); |
|
426 by (arith_tac 2); |
|
427 by (Asm_full_simp_tac 2); |
|
428 by (arith_tac 2); |
|
429 by (induct_tac "p2" 1); |
|
430 by (Asm_full_simp_tac 1); |
|
431 by (Asm_full_simp_tac 1); |
|
432 qed "poly_add_length"; |
|
433 |
|
434 Goal "length([a,b] *** p) = Suc (length p)"; |
|
435 by (asm_full_simp_tac (simpset() addsimps [poly_cmult_length, |
|
436 poly_add_length]) 1); |
|
437 qed "poly_root_mult_length"; |
|
438 Addsimps [poly_root_mult_length]; |
|
439 |
|
440 Goal "(poly (p *** q) x ~= poly [] x) = \ |
|
441 \ (poly p x ~= poly [] x & poly q x ~= poly [] x)"; |
|
442 by (auto_tac (claset(),simpset() addsimps [poly_mult,rename_numerals |
|
443 real_mult_not_zero])); |
|
444 qed "poly_mult_not_eq_poly_Nil"; |
|
445 Addsimps [poly_mult_not_eq_poly_Nil]; |
|
446 |
|
447 Goal "(poly (p *** q) x = 0) = (poly p x = 0 | poly q x = 0)"; |
|
448 by (auto_tac (claset() addDs [CLAIM "x * y = 0 ==> x = 0 | y = (0::real)"], |
|
449 simpset() addsimps [poly_mult])); |
|
450 qed "poly_mult_eq_zero_disj"; |
|
451 |
|
452 (*-------------------------------------------------------------------------*) |
|
453 (* Normalisation Properties *) |
|
454 (*-------------------------------------------------------------------------*) |
|
455 |
|
456 Goal "(pnormalize p = []) --> (poly p x = 0)"; |
|
457 by (induct_tac "p" 1); |
|
458 by Auto_tac; |
|
459 qed "poly_normalized_nil"; |
|
460 |
|
461 (*-------------------------------------------------------------------------*) |
|
462 (* A nontrivial polynomial of degree n has no more than n roots *) |
|
463 (*-------------------------------------------------------------------------*) |
|
464 |
|
465 Goal |
|
466 "ALL p x. (poly p x ~= poly [] x & length p = n \ |
|
467 \ --> (EX i. ALL x. (poly p x = (0::real)) --> (EX m. (m <= n & x = i m))))"; |
|
468 by (induct_tac "n" 1); |
|
469 by (Step_tac 1); |
|
470 by (rtac ccontr 1); |
|
471 by (subgoal_tac "EX a. poly p a = 0" 1 THEN Step_tac 1); |
|
472 by (dtac (poly_linear_divides RS iffD1) 1); |
|
473 by (Step_tac 1); |
|
474 by (dres_inst_tac [("x","q")] spec 1); |
|
475 by (dres_inst_tac [("x","x")] spec 1); |
|
476 by (asm_full_simp_tac (simpset() delsimps [poly_Nil,pmult_Cons]) 1); |
|
477 by (etac exE 1); |
|
478 by (dres_inst_tac [("x","%m. if m = Suc n then a else i m")] spec 1); |
|
479 by (Step_tac 1); |
|
480 by (dtac (poly_mult_eq_zero_disj RS iffD1) 1); |
|
481 by (Step_tac 1); |
|
482 by (dres_inst_tac [("x","Suc(length q)")] spec 1); |
|
483 by (Asm_full_simp_tac 1); |
|
484 by (dres_inst_tac [("x","xa")] spec 1 THEN Step_tac 1); |
|
485 by (dres_inst_tac [("x","m")] spec 1); |
|
486 by (Asm_full_simp_tac 1); |
|
487 by (Blast_tac 1); |
|
488 qed_spec_mp "poly_roots_index_lemma"; |
|
489 bind_thm ("poly_roots_index_lemma2",conjI RS poly_roots_index_lemma); |
|
490 |
|
491 Goal "poly p x ~= poly [] x ==> \ |
|
492 \ EX i. ALL x. (poly p x = 0) --> (EX n. n <= length p & x = i n)"; |
|
493 by (blast_tac (claset() addIs [poly_roots_index_lemma2]) 1); |
|
494 qed "poly_roots_index_length"; |
|
495 |
|
496 Goal "poly p x ~= poly [] x ==> \ |
|
497 \ EX N i. ALL x. (poly p x = 0) --> (EX n. (n::nat) < N & x = i n)"; |
|
498 by (dtac poly_roots_index_length 1 THEN Step_tac 1); |
|
499 by (res_inst_tac [("x","Suc (length p)")] exI 1); |
|
500 by (res_inst_tac [("x","i")] exI 1); |
|
501 by (auto_tac (claset(),simpset() addsimps |
|
502 [ARITH_PROVE "(m < Suc n) = (m <= n)"])); |
|
503 qed "poly_roots_finite_lemma"; |
|
504 |
|
505 (* annoying proof *) |
|
506 Goal "ALL P. (ALL x. P x --> (EX n. (n::nat) < N & x = (j::nat=>real) n)) \ |
|
507 \ --> (EX a. ALL x. P x --> x < a)"; |
|
508 by (induct_tac "N" 1); |
|
509 by (Asm_full_simp_tac 1); |
|
510 by (Step_tac 1); |
|
511 by (dres_inst_tac [("x","%z. P z & (z ~= (j::nat=>real) n)")] spec 1); |
|
512 by Auto_tac; |
|
513 by (dres_inst_tac [("x","x")] spec 1); |
|
514 by (Step_tac 1); |
|
515 by (res_inst_tac [("x","na")] exI 1); |
|
516 by (auto_tac (claset() addDs [ARITH_PROVE "na < Suc n ==> na = n | na < n"], |
|
517 simpset())); |
|
518 by (res_inst_tac [("x","abs a + abs(j n) + 1")] exI 1); |
|
519 by (Step_tac 1); |
|
520 by (dres_inst_tac [("x","x")] spec 1); |
|
521 by (Step_tac 1); |
|
522 by (dres_inst_tac [("x","j na")] spec 1); |
|
523 by (Step_tac 1); |
|
524 by (ALLGOALS(arith_tac)); |
|
525 qed_spec_mp "real_finite_lemma"; |
|
526 |
|
527 Goal "(poly p ~= poly []) = \ |
|
528 \ (EX N j. ALL x. poly p x = 0 --> (EX n. (n::nat) < N & x = j n))"; |
|
529 by (Step_tac 1); |
|
530 by (etac swap 1 THEN rtac ext 1); |
|
531 by (rtac ccontr 1); |
|
532 by (clarify_tac (claset() addSDs [poly_roots_finite_lemma]) 1); |
|
533 by (clarify_tac (claset() addSDs [real_finite_lemma]) 1); |
|
534 by (dres_inst_tac [("x","a")] fun_cong 1); |
|
535 by Auto_tac; |
|
536 qed "poly_roots_finite"; |
|
537 |
|
538 (*-------------------------------------------------------------------------*) |
|
539 (* Entirety and Cancellation for polynomials *) |
|
540 (*-------------------------------------------------------------------------*) |
|
541 |
|
542 Goal "[| poly p ~= poly [] ; poly q ~= poly [] |] \ |
|
543 \ ==> poly (p *** q) ~= poly []"; |
|
544 by (auto_tac (claset(),simpset() addsimps [poly_roots_finite])); |
|
545 by (res_inst_tac [("x","N + Na")] exI 1); |
|
546 by (res_inst_tac [("x","%n. if n < N then j n else ja (n - N)")] exI 1); |
|
547 by (auto_tac (claset(),simpset() addsimps [poly_mult_eq_zero_disj])); |
|
548 by (flexflex_tac THEN rotate_tac 1 1); |
|
549 by (dtac spec 1 THEN Auto_tac); |
|
550 qed "poly_entire_lemma"; |
|
551 |
|
552 Goal "(poly (p *** q) = poly []) = ((poly p = poly []) | (poly q = poly []))"; |
|
553 by (auto_tac (claset() addIs [ext] addDs [fun_cong],simpset() |
|
554 addsimps [poly_entire_lemma,poly_mult])); |
|
555 by (blast_tac (claset() addIs [ccontr] addDs [poly_entire_lemma, |
|
556 poly_mult RS subst]) 1); |
|
557 qed "poly_entire"; |
|
558 |
|
559 Goal "(poly (p *** q) ~= poly []) = ((poly p ~= poly []) & (poly q ~= poly []))"; |
|
560 by (asm_full_simp_tac (simpset() addsimps [poly_entire]) 1); |
|
561 qed "poly_entire_neg"; |
|
562 |
|
563 Goal " (f = g) = (ALL x. f x = g x)"; |
|
564 by (auto_tac (claset() addSIs [ext],simpset())); |
|
565 qed "fun_eq"; |
|
566 |
|
567 Goal "(poly (p +++ -- q) = poly []) = (poly p = poly q)"; |
|
568 by (auto_tac (claset(),simpset() addsimps [poly_add,poly_minus_def, |
|
569 fun_eq,poly_cmult,ARITH_PROVE "(p + -q = 0) = (p = (q::real))"])); |
|
570 qed "poly_add_minus_zero_iff"; |
|
571 |
|
572 Goal "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"; |
|
573 by (auto_tac (claset(),simpset() addsimps [poly_add,poly_minus_def, |
|
574 fun_eq,poly_mult,poly_cmult,real_add_mult_distrib2])); |
|
575 qed "poly_add_minus_mult_eq"; |
|
576 |
|
577 Goal "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"; |
|
578 by (res_inst_tac [("p1","p *** q")] (poly_add_minus_zero_iff RS subst) 1); |
|
579 by (auto_tac (claset() addIs [ext], simpset() addsimps [poly_add_minus_mult_eq, |
|
580 poly_entire,poly_add_minus_zero_iff])); |
|
581 qed "poly_mult_left_cancel"; |
|
582 |
|
583 Goal "(x * y = 0) = (x = (0::real) | y = 0)"; |
|
584 by (auto_tac (claset() addDs [CLAIM "x * y = 0 ==> x = 0 | y = (0::real)"], |
|
585 simpset())); |
|
586 qed "real_mult_zero_disj_iff"; |
|
587 |
|
588 Goal "(poly (p %^ n) = poly []) = (poly p = poly [] & n ~= 0)"; |
|
589 by (simp_tac (simpset() addsimps [fun_eq]) 1); |
|
590 by (rtac (CLAIM "((ALL x. P x) & Q) = (ALL x. P x & Q)" RS ssubst) 1); |
|
591 by (rtac (CLAIM "f = g ==> (ALL x. f x) = (ALL x. g x)") 1); |
|
592 by (rtac ext 1); |
|
593 by (induct_tac "n" 1); |
|
594 by (auto_tac (claset(),simpset() addsimps [poly_mult, |
|
595 real_mult_zero_disj_iff])); |
|
596 qed "poly_exp_eq_zero"; |
|
597 Addsimps [poly_exp_eq_zero]; |
|
598 |
|
599 Goal "poly [a,1] ~= poly []"; |
|
600 by (simp_tac (simpset() addsimps [fun_eq]) 1); |
|
601 by (res_inst_tac [("x","1 - a")] exI 1); |
|
602 by (Simp_tac 1); |
|
603 qed "poly_prime_eq_zero"; |
|
604 Addsimps [poly_prime_eq_zero]; |
|
605 |
|
606 Goal "(poly ([a, 1] %^ n) ~= poly [])"; |
|
607 by Auto_tac; |
|
608 qed "poly_exp_prime_eq_zero"; |
|
609 Addsimps [poly_exp_prime_eq_zero]; |
|
610 |
|
611 (*-------------------------------------------------------------------------*) |
|
612 (* A more constructive notion of polynomials being trivial *) |
|
613 (*-------------------------------------------------------------------------*) |
|
614 |
|
615 Goal "poly (h # t) = poly [] ==> h = 0 & poly t = poly []"; |
|
616 by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1); |
|
617 by (case_tac "h = 0" 1); |
|
618 by (dres_inst_tac [("x","0")] spec 2); |
|
619 by (rtac conjI 1); |
|
620 by (rtac ((simplify (simpset()) (read_instantiate [("g","poly []")] fun_eq)) |
|
621 RS iffD1) 2 THEN rtac ccontr 2); |
|
622 by (auto_tac (claset(),simpset() addsimps [poly_roots_finite, |
|
623 real_mult_zero_disj_iff])); |
|
624 by (dtac real_finite_lemma 1 THEN Step_tac 1); |
|
625 by (REPEAT(dres_inst_tac [("x","abs a + 1")] spec 1)); |
|
626 by (arith_tac 1); |
|
627 qed "poly_zero_lemma"; |
|
628 |
|
629 Goal "(poly p = poly []) = list_all (%c. c = 0) p"; |
|
630 by (induct_tac "p" 1); |
|
631 by (Asm_full_simp_tac 1); |
|
632 by (rtac iffI 1); |
|
633 by (dtac poly_zero_lemma 1); |
|
634 by Auto_tac; |
|
635 qed "poly_zero"; |
|
636 |
|
637 Addsimps [real_mult_zero_disj_iff]; |
|
638 Goal "ALL n. (list_all (%c. c = 0) (pderiv_aux (Suc n) p) = \ |
|
639 \ list_all (%c. c = 0) p)"; |
|
640 by (induct_tac "p" 1); |
|
641 by Auto_tac; |
|
642 qed_spec_mp "pderiv_aux_iszero"; |
|
643 Addsimps [pderiv_aux_iszero]; |
|
644 |
|
645 Goal "(number_of n :: nat) ~= 0 \ |
|
646 \ ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) = \ |
|
647 \ list_all (%c. c = 0) p)"; |
|
648 by (res_inst_tac [("n1","number_of n"),("m1","0")] (less_imp_Suc_add RS exE) 1); |
|
649 by (Force_tac 1); |
|
650 by (res_inst_tac [("n1","0 + x")] (pderiv_aux_iszero RS subst) 1); |
|
651 by (asm_simp_tac (simpset() delsimps [pderiv_aux_iszero]) 1); |
|
652 qed "pderiv_aux_iszero_num"; |
|
653 |
|
654 Goal "poly (pderiv p) = poly [] --> (EX h. poly p = poly [h])"; |
|
655 by (asm_full_simp_tac (simpset() addsimps [poly_zero]) 1); |
|
656 by (induct_tac "p" 1); |
|
657 by (Force_tac 1); |
|
658 by (asm_full_simp_tac (simpset() addsimps [pderiv_Cons, |
|
659 pderiv_aux_iszero_num] delsimps [poly_Cons]) 1); |
|
660 by (auto_tac (claset(),simpset() addsimps [poly_zero RS sym])); |
|
661 qed_spec_mp "pderiv_iszero"; |
|
662 |
|
663 Goal "poly p = poly [] --> (poly (pderiv p) = poly [])"; |
|
664 by (asm_full_simp_tac (simpset() addsimps [poly_zero]) 1); |
|
665 by (induct_tac "p" 1); |
|
666 by (Force_tac 1); |
|
667 by (asm_full_simp_tac (simpset() addsimps [pderiv_Cons, |
|
668 pderiv_aux_iszero_num] delsimps [poly_Cons]) 1); |
|
669 qed "pderiv_zero_obj"; |
|
670 |
|
671 Goal "poly p = poly [] ==> (poly (pderiv p) = poly [])"; |
|
672 by (blast_tac (claset() addEs [pderiv_zero_obj RS impE]) 1); |
|
673 qed "pderiv_zero"; |
|
674 Addsimps [pderiv_zero]; |
|
675 |
|
676 Goal "poly p = poly q ==> (poly (pderiv p) = poly (pderiv q))"; |
|
677 by (cut_inst_tac [("p","p +++ --q")] pderiv_zero_obj 1); |
|
678 by (auto_tac (claset() addIs [ ARITH_PROVE "x + - y = 0 ==> x = (y::real)"], |
|
679 simpset() addsimps [fun_eq,poly_add,poly_minus,poly_pderiv_add, |
|
680 poly_pderiv_minus] delsimps [pderiv_zero])); |
|
681 qed "poly_pderiv_welldef"; |
|
682 |
|
683 (* ------------------------------------------------------------------------- *) |
|
684 (* Basics of divisibility. *) |
|
685 (* ------------------------------------------------------------------------- *) |
|
686 |
|
687 Goal "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"; |
|
688 by (auto_tac (claset(),simpset() addsimps [divides_def,fun_eq,poly_mult, |
|
689 poly_add,poly_cmult,real_add_mult_distrib RS sym])); |
|
690 by (dres_inst_tac [("x","-a")] spec 1); |
|
691 by (auto_tac (claset(),simpset() addsimps [poly_linear_divides,poly_add, |
|
692 poly_cmult,real_add_mult_distrib RS sym])); |
|
693 by (res_inst_tac [("x","qa *** q")] exI 1); |
|
694 by (res_inst_tac [("x","p *** qa")] exI 2); |
|
695 by (auto_tac (claset(),simpset() addsimps [poly_add,poly_mult, |
|
696 poly_cmult] @ real_mult_ac)); |
|
697 qed "poly_primes"; |
|
698 |
|
699 Goalw [divides_def] "p divides p"; |
|
700 by (res_inst_tac [("x","[1]")] exI 1); |
|
701 by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq])); |
|
702 qed "poly_divides_refl"; |
|
703 Addsimps [poly_divides_refl]; |
|
704 |
|
705 Goalw [divides_def] "[| p divides q; q divides r |] ==> p divides r"; |
|
706 by (Step_tac 1); |
|
707 by (res_inst_tac [("x","qa *** qaa")] exI 1); |
|
708 by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq, |
|
709 real_mult_assoc])); |
|
710 qed "poly_divides_trans"; |
|
711 |
|
712 Goal "(m::nat) <= n = (EX d. n = m + d)"; |
|
713 by (auto_tac (claset(),simpset() addsimps [le_eq_less_or_eq, |
|
714 less_iff_Suc_add])); |
|
715 qed "le_iff_add"; |
|
716 |
|
717 Goal "m <= n ==> (p %^ m) divides (p %^ n)"; |
|
718 by (auto_tac (claset(),simpset() addsimps [le_iff_add])); |
|
719 by (induct_tac "d" 1); |
|
720 by (rtac poly_divides_trans 2); |
|
721 by (auto_tac (claset(),simpset() addsimps [divides_def])); |
|
722 by (res_inst_tac [("x","p")] exI 1); |
|
723 by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq] |
|
724 @ real_mult_ac)); |
|
725 qed "poly_divides_exp"; |
|
726 |
|
727 Goal "[| (p %^ n) divides q; m <= n |] ==> (p %^ m) divides q"; |
|
728 by (blast_tac (claset() addIs [poly_divides_exp,poly_divides_trans]) 1); |
|
729 qed "poly_exp_divides"; |
|
730 |
|
731 Goalw [divides_def] |
|
732 "[| p divides q; p divides r |] ==> p divides (q +++ r)"; |
|
733 by Auto_tac; |
|
734 by (res_inst_tac [("x","qa +++ qaa")] exI 1); |
|
735 by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult, |
|
736 real_add_mult_distrib2])); |
|
737 qed "poly_divides_add"; |
|
738 |
|
739 Goalw [divides_def] |
|
740 "[| p divides q; p divides (q +++ r) |] ==> p divides r"; |
|
741 by Auto_tac; |
|
742 by (res_inst_tac [("x","qaa +++ -- qa")] exI 1); |
|
743 by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult, |
|
744 poly_minus,real_add_mult_distrib2,real_minus_mult_eq2 RS sym, |
|
745 ARITH_PROVE "(x = y + -z) = (z + x = (y::real))"])); |
|
746 qed "poly_divides_diff"; |
|
747 |
|
748 Goal "[| p divides r; p divides (q +++ r) |] ==> p divides q"; |
|
749 by (etac poly_divides_diff 1); |
|
750 by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult, |
|
751 divides_def] @ real_add_ac)); |
|
752 qed "poly_divides_diff2"; |
|
753 |
|
754 Goalw [divides_def] "poly p = poly [] ==> q divides p"; |
|
755 by (auto_tac (claset(),simpset() addsimps [fun_eq,poly_mult])); |
|
756 qed "poly_divides_zero"; |
|
757 |
|
758 Goalw [divides_def] "q divides []"; |
|
759 by (res_inst_tac [("x","[]")] exI 1); |
|
760 by (auto_tac (claset(),simpset() addsimps [fun_eq])); |
|
761 qed "poly_divides_zero2"; |
|
762 Addsimps [poly_divides_zero2]; |
|
763 |
|
764 (* ------------------------------------------------------------------------- *) |
|
765 (* At last, we can consider the order of a root. *) |
|
766 (* ------------------------------------------------------------------------- *) |
|
767 |
|
768 (* FIXME: Tidy up *) |
|
769 Goal "[| length p = d; poly p ~= poly [] |] \ |
|
770 \ ==> EX n. ([-a, 1] %^ n) divides p & \ |
|
771 \ ~(([-a, 1] %^ (Suc n)) divides p)"; |
|
772 by (subgoal_tac "ALL p. length p = d & poly p ~= poly [] \ |
|
773 \ --> (EX n q. p = mulexp n [-a, 1] q & poly q a ~= 0)" 1); |
|
774 by (induct_tac "d" 2); |
|
775 by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 2); |
|
776 by (Step_tac 2); |
|
777 by (case_tac "poly pa a = 0" 2); |
|
778 by (dtac (poly_linear_divides RS iffD1) 2); |
|
779 by (Step_tac 2); |
|
780 by (dres_inst_tac [("x","q")] spec 2); |
|
781 by (dtac (poly_entire_neg RS iffD1) 2); |
|
782 by (Step_tac 2); |
|
783 by (Force_tac 2 THEN Blast_tac 2); |
|
784 by (res_inst_tac [("x","Suc na")] exI 2); |
|
785 by (res_inst_tac [("x","qa")] exI 2); |
|
786 by (asm_full_simp_tac (simpset() delsimps [pmult_Cons]) 2); |
|
787 by (res_inst_tac [("x","0")] exI 2); |
|
788 by (Force_tac 2); |
|
789 by (dres_inst_tac [("x","p")] spec 1 THEN Step_tac 1); |
|
790 by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1); |
|
791 by (rewtac divides_def); |
|
792 by (res_inst_tac [("x","q")] exI 1); |
|
793 by (induct_tac "n" 1); |
|
794 by (Simp_tac 1); |
|
795 by (asm_simp_tac (simpset() addsimps [poly_add,poly_cmult,poly_mult, |
|
796 real_add_mult_distrib2] @ real_mult_ac) 1); |
|
797 by (Step_tac 1); |
|
798 by (rotate_tac 2 1); |
|
799 by (rtac swap 1 THEN assume_tac 2); |
|
800 by (induct_tac "n" 1); |
|
801 by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1); |
|
802 by (eres_inst_tac [("Pa","poly q a = 0")] swap 1); |
|
803 by (asm_full_simp_tac (simpset() addsimps [poly_add,poly_cmult, |
|
804 real_minus_mult_eq1 RS sym]) 1); |
|
805 by (rtac (pexp_Suc RS ssubst) 1); |
|
806 by (rtac ccontr 1); |
|
807 by (asm_full_simp_tac (simpset() addsimps [poly_mult_left_cancel, |
|
808 poly_mult_assoc] delsimps [pmult_Cons,pexp_Suc]) 1); |
|
809 qed "poly_order_exists"; |
|
810 |
|
811 Goalw [divides_def] "[1] divides p"; |
|
812 by Auto_tac; |
|
813 qed "poly_one_divides"; |
|
814 Addsimps [poly_one_divides]; |
|
815 |
|
816 Goal "poly p ~= poly [] \ |
|
817 \ ==> EX! n. ([-a, 1] %^ n) divides p & \ |
|
818 \ ~(([-a, 1] %^ (Suc n)) divides p)"; |
|
819 by (auto_tac (claset() addIs [poly_order_exists], |
|
820 simpset() addsimps [less_linear] delsimps [pmult_Cons,pexp_Suc])); |
|
821 by (cut_inst_tac [("m","y"),("n","n")] less_linear 1); |
|
822 by (dres_inst_tac [("m","n")] poly_exp_divides 1); |
|
823 by (auto_tac (claset() addDs [ARITH_PROVE "n < m ==> Suc n <= m" RSN |
|
824 (2,poly_exp_divides)],simpset() delsimps [pmult_Cons,pexp_Suc])); |
|
825 qed "poly_order"; |
|
826 |
|
827 (* ------------------------------------------------------------------------- *) |
|
828 (* Order *) |
|
829 (* ------------------------------------------------------------------------- *) |
|
830 |
|
831 Goal "[| n = (@n. P n); EX! n. P n |] ==> P n"; |
|
832 by (blast_tac (claset() addIs [someI2]) 1); |
|
833 qed "some1_equalityD"; |
|
834 |
|
835 Goalw [order_def] |
|
836 "(([-a, 1] %^ n) divides p & \ |
|
837 \ ~(([-a, 1] %^ (Suc n)) divides p)) = \ |
|
838 \ ((n = order a p) & ~(poly p = poly []))"; |
|
839 by (rtac iffI 1); |
|
840 by (blast_tac (claset() addDs [poly_divides_zero] |
|
841 addSIs [some1_equality RS sym, poly_order]) 1); |
|
842 by (blast_tac (claset() addSIs [poly_order RSN (2,some1_equalityD)]) 1); |
|
843 qed "order"; |
|
844 |
|
845 Goal "[| poly p ~= poly [] |] \ |
|
846 \ ==> ([-a, 1] %^ (order a p)) divides p & \ |
|
847 \ ~(([-a, 1] %^ (Suc(order a p))) divides p)"; |
|
848 by (asm_full_simp_tac (simpset() addsimps [order] delsimps [pexp_Suc]) 1); |
|
849 qed "order2"; |
|
850 |
|
851 Goal "[| poly p ~= poly []; ([-a, 1] %^ n) divides p; \ |
|
852 \ ~(([-a, 1] %^ (Suc n)) divides p) \ |
|
853 \ |] ==> (n = order a p)"; |
|
854 by (cut_inst_tac [("p","p"),("a","a"),("n","n")] order 1); |
|
855 by Auto_tac; |
|
856 qed "order_unique"; |
|
857 |
|
858 Goal "(poly p ~= poly [] & ([-a, 1] %^ n) divides p & \ |
|
859 \ ~(([-a, 1] %^ (Suc n)) divides p)) \ |
|
860 \ ==> (n = order a p)"; |
|
861 by (blast_tac (claset() addIs [order_unique]) 1); |
|
862 qed "order_unique_lemma"; |
|
863 |
|
864 Goal "poly p = poly q ==> order a p = order a q"; |
|
865 by (auto_tac (claset(),simpset() addsimps [fun_eq,divides_def,poly_mult, |
|
866 order_def])); |
|
867 qed "order_poly"; |
|
868 |
|
869 Goal "p %^ (Suc 0) = p"; |
|
870 by (induct_tac "p" 1); |
|
871 by (auto_tac (claset(),simpset() addsimps [numeral_1_eq_1])); |
|
872 qed "pexp_one"; |
|
873 Addsimps [pexp_one]; |
|
874 |
|
875 Goal "ALL p a. 0 < n & [- a, 1] %^ n divides p & \ |
|
876 \ ~ [- a, 1] %^ (Suc n) divides p \ |
|
877 \ --> poly p a = 0"; |
|
878 by (induct_tac "n" 1); |
|
879 by (Blast_tac 1); |
|
880 by (auto_tac (claset(),simpset() addsimps [divides_def,poly_mult] |
|
881 delsimps [pmult_Cons])); |
|
882 qed_spec_mp "lemma_order_root"; |
|
883 |
|
884 Goal "(poly p a = 0) = ((poly p = poly []) | order a p ~= 0)"; |
|
885 by (case_tac "poly p = poly []" 1); |
|
886 by Auto_tac; |
|
887 by (asm_full_simp_tac (simpset() addsimps [poly_linear_divides] |
|
888 delsimps [pmult_Cons]) 1); |
|
889 by (Step_tac 1); |
|
890 by (ALLGOALS(dres_inst_tac [("a","a")] order2)); |
|
891 by (rtac ccontr 1); |
|
892 by (asm_full_simp_tac (simpset() addsimps [divides_def,poly_mult,fun_eq] |
|
893 delsimps [pmult_Cons]) 1); |
|
894 by (Blast_tac 1); |
|
895 by (blast_tac (claset() addIs [lemma_order_root]) 1); |
|
896 qed "order_root"; |
|
897 |
|
898 Goal "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n <= order a p)"; |
|
899 by (case_tac "poly p = poly []" 1); |
|
900 by Auto_tac; |
|
901 by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq,poly_mult]) 1); |
|
902 by (res_inst_tac [("x","[]")] exI 1); |
|
903 by (TRYALL(dres_inst_tac [("a","a")] order2)); |
|
904 by (auto_tac (claset() addIs [poly_exp_divides],simpset() |
|
905 delsimps [pexp_Suc])); |
|
906 qed "order_divides"; |
|
907 |
|
908 Goalw [divides_def] |
|
909 "poly p ~= poly [] \ |
|
910 \ ==> EX q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) & \ |
|
911 \ ~([-a, 1] divides q)"; |
|
912 by (dres_inst_tac [("a","a")] order2 1); |
|
913 by (asm_full_simp_tac (simpset() addsimps [divides_def] |
|
914 delsimps [pexp_Suc,pmult_Cons]) 1); |
|
915 by (Step_tac 1); |
|
916 by (res_inst_tac [("x","q")] exI 1); |
|
917 by (Step_tac 1); |
|
918 by (dres_inst_tac [("x","qa")] spec 1); |
|
919 by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq,poly_exp] |
|
920 @ real_mult_ac delsimps [pmult_Cons])); |
|
921 qed "order_decomp"; |
|
922 |
|
923 (* ------------------------------------------------------------------------- *) |
|
924 (* Important composition properties of orders. *) |
|
925 (* ------------------------------------------------------------------------- *) |
|
926 |
|
927 Goal "poly (p *** q) ~= poly [] \ |
|
928 \ ==> order a (p *** q) = order a p + order a q"; |
|
929 by (cut_inst_tac [("a","a"),("p","p***q"),("n","order a p + order a q")] |
|
930 order 1); |
|
931 by (auto_tac (claset(),simpset() addsimps [poly_entire] delsimps [pmult_Cons])); |
|
932 by (REPEAT(dres_inst_tac [("a","a")] order2 1)); |
|
933 by (Step_tac 1); |
|
934 by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq,poly_exp_add, |
|
935 poly_mult] delsimps [pmult_Cons]) 1); |
|
936 by (Step_tac 1); |
|
937 by (res_inst_tac [("x","qa *** qaa")] exI 1); |
|
938 by (asm_full_simp_tac (simpset() addsimps [poly_mult] @ real_mult_ac |
|
939 delsimps [pmult_Cons]) 1); |
|
940 by (REPEAT(dres_inst_tac [("a","a")] order_decomp 1)); |
|
941 by (Step_tac 1); |
|
942 by (subgoal_tac "[-a,1] divides (qa *** qaa)" 1); |
|
943 by (asm_full_simp_tac (simpset() addsimps [poly_primes] |
|
944 delsimps [pmult_Cons]) 1); |
|
945 by (auto_tac (claset(),simpset() addsimps [divides_def] |
|
946 delsimps [pmult_Cons])); |
|
947 by (res_inst_tac [("x","qb")] exI 1); |
|
948 by (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = \ |
|
949 \ poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))" 1); |
|
950 by (dtac (poly_mult_left_cancel RS iffD1) 1); |
|
951 by (Force_tac 1); |
|
952 by (subgoal_tac "poly ([-a, 1] %^ (order a q) *** \ |
|
953 \ ([-a, 1] %^ (order a p) *** (qa *** qaa))) = \ |
|
954 \ poly ([-a, 1] %^ (order a q) *** \ |
|
955 \ ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb)))" 1); |
|
956 by (dtac (poly_mult_left_cancel RS iffD1) 1); |
|
957 by (Force_tac 1); |
|
958 by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_exp_add,poly_mult] |
|
959 @ real_mult_ac delsimps [pmult_Cons]) 1); |
|
960 qed "order_mult"; |
|
961 |
|
962 (* FIXME: too too long! *) |
|
963 Goal "ALL p q a. 0 < n & \ |
|
964 \ poly (pderiv p) ~= poly [] & \ |
|
965 \ poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q \ |
|
966 \ --> n = Suc (order a (pderiv p))"; |
|
967 by (induct_tac "n" 1); |
|
968 by (Step_tac 1); |
|
969 by (rtac order_unique_lemma 1 THEN rtac conjI 1); |
|
970 by (assume_tac 1); |
|
971 by (subgoal_tac "ALL r. r divides (pderiv p) = \ |
|
972 \ r divides (pderiv ([-a, 1] %^ Suc n *** q))" 1); |
|
973 by (dtac poly_pderiv_welldef 2); |
|
974 by (asm_full_simp_tac (simpset() addsimps [divides_def] delsimps [pmult_Cons, |
|
975 pexp_Suc]) 2); |
|
976 by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1); |
|
977 by (rtac conjI 1); |
|
978 by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq] |
|
979 delsimps [pmult_Cons,pexp_Suc]) 1); |
|
980 by (res_inst_tac |
|
981 [("x","[-a, 1] *** (pderiv q) +++ real (Suc n) %* q")] exI 1); |
|
982 by (asm_full_simp_tac (simpset() addsimps [poly_pderiv_mult, |
|
983 poly_pderiv_exp_prime,poly_add,poly_mult,poly_cmult, |
|
984 real_add_mult_distrib2] @ real_mult_ac |
|
985 delsimps [pmult_Cons,pexp_Suc]) 1); |
|
986 by (asm_full_simp_tac (simpset() addsimps [poly_mult,real_add_mult_distrib2, |
|
987 real_add_mult_distrib] @ real_mult_ac delsimps [pmult_Cons]) 1); |
|
988 by (thin_tac "ALL r. \ |
|
989 \ r divides pderiv p = \ |
|
990 \ r divides pderiv ([- a, 1] %^ Suc n *** q)" 1); |
|
991 by (rewtac divides_def); |
|
992 by (simp_tac (simpset() addsimps [poly_pderiv_mult, |
|
993 poly_pderiv_exp_prime,fun_eq,poly_add,poly_mult] |
|
994 delsimps [pmult_Cons,pexp_Suc]) 1); |
|
995 by (rtac swap 1 THEN assume_tac 1); |
|
996 by (rotate_tac 3 1 THEN etac swap 1); |
|
997 by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1); |
|
998 by (Step_tac 1); |
|
999 by (res_inst_tac [("x","inverse(real (Suc n)) %* (qa +++ --(pderiv q))")] |
|
1000 exI 1); |
|
1001 by (subgoal_tac "poly ([-a, 1] %^ n *** q) = \ |
|
1002 \ poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* \ |
|
1003 \ (qa +++ -- (pderiv q)))))" 1); |
|
1004 by (dtac (poly_mult_left_cancel RS iffD1) 1); |
|
1005 by (Asm_full_simp_tac 1); |
|
1006 by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_mult,poly_add,poly_cmult, |
|
1007 poly_minus] delsimps [pmult_Cons]) 1); |
|
1008 by (Step_tac 1); |
|
1009 by (res_inst_tac [("c1","real (Suc n)")] (real_mult_left_cancel |
|
1010 RS iffD1) 1); |
|
1011 by (Simp_tac 1); |
|
1012 by (rtac ((CLAIM_SIMP |
|
1013 "a * (b * (c * (d * e))) = e * (b * (c * (d * (a::real))))" |
|
1014 real_mult_ac) RS ssubst) 1); |
|
1015 by (rotate_tac 2 1); |
|
1016 by (dres_inst_tac [("x","xa")] spec 1); |
|
1017 by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib, |
|
1018 real_minus_mult_eq1 RS sym] @ real_mult_ac |
|
1019 delsimps [pmult_Cons]) 1); |
|
1020 qed_spec_mp "lemma_order_pderiv"; |
|
1021 |
|
1022 Goal "[| poly (pderiv p) ~= poly []; order a p ~= 0 |] \ |
|
1023 \ ==> (order a p = Suc (order a (pderiv p)))"; |
|
1024 by (case_tac "poly p = poly []" 1); |
|
1025 by (auto_tac (claset() addDs [pderiv_zero],simpset())); |
|
1026 by (dres_inst_tac [("a","a"),("p","p")] order_decomp 1); |
|
1027 by (blast_tac (claset() addIs [lemma_order_pderiv]) 1); |
|
1028 qed "order_pderiv"; |
|
1029 |
|
1030 (* ------------------------------------------------------------------------- *) |
|
1031 (* Now justify the standard squarefree decomposition, i.e. f / gcd(f,f'). *) |
|
1032 (* `a la Harrison *) |
|
1033 (* ------------------------------------------------------------------------- *) |
|
1034 |
|
1035 Goal "[| poly (pderiv p) ~= poly []; \ |
|
1036 \ poly p = poly (q *** d); \ |
|
1037 \ poly (pderiv p) = poly (e *** d); \ |
|
1038 \ poly d = poly (r *** p +++ s *** pderiv p) \ |
|
1039 \ |] ==> order a q = (if order a p = 0 then 0 else 1)"; |
|
1040 by (subgoal_tac "order a p = order a q + order a d" 1); |
|
1041 by (res_inst_tac [("s","order a (q *** d)")] trans 2); |
|
1042 by (blast_tac (claset() addIs [order_poly]) 2); |
|
1043 by (rtac order_mult 2); |
|
1044 by (rtac notI 2 THEN Asm_full_simp_tac 2); |
|
1045 by (dres_inst_tac [("p","p")] pderiv_zero 2); |
|
1046 by (Asm_full_simp_tac 2); |
|
1047 by (case_tac "order a p = 0" 1); |
|
1048 by (Asm_full_simp_tac 1); |
|
1049 by (subgoal_tac "order a (pderiv p) = order a e + order a d" 1); |
|
1050 by (res_inst_tac [("s","order a (e *** d)")] trans 2); |
|
1051 by (blast_tac (claset() addIs [order_poly]) 2); |
|
1052 by (rtac order_mult 2); |
|
1053 by (rtac notI 2 THEN Asm_full_simp_tac 2); |
|
1054 by (case_tac "poly p = poly []" 1); |
|
1055 by (dres_inst_tac [("p","p")] pderiv_zero 1); |
|
1056 by (Asm_full_simp_tac 1); |
|
1057 by (dtac order_pderiv 1 THEN assume_tac 1); |
|
1058 by (subgoal_tac "order a (pderiv p) <= order a d" 1); |
|
1059 by (subgoal_tac "([-a, 1] %^ (order a (pderiv p))) divides d" 2); |
|
1060 by (asm_full_simp_tac (simpset() addsimps [poly_entire,order_divides]) 2); |
|
1061 by (subgoal_tac "([-a, 1] %^ (order a (pderiv p))) divides p & \ |
|
1062 \ ([-a, 1] %^ (order a (pderiv p))) divides (pderiv p)" 2); |
|
1063 by (asm_simp_tac (simpset() addsimps [order_divides]) 3); |
|
1064 by (asm_full_simp_tac (simpset() addsimps [divides_def] |
|
1065 delsimps [pexp_Suc,pmult_Cons]) 2); |
|
1066 by (Step_tac 2); |
|
1067 by (res_inst_tac [("x","r *** qa +++ s *** qaa")] exI 2); |
|
1068 by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_add,poly_mult, |
|
1069 real_add_mult_distrib, real_add_mult_distrib2] @ real_mult_ac |
|
1070 delsimps [pexp_Suc,pmult_Cons]) 2); |
|
1071 by Auto_tac; |
|
1072 qed "poly_squarefree_decomp_order"; |
|
1073 |
|
1074 |
|
1075 Goal "[| poly (pderiv p) ~= poly []; \ |
|
1076 \ poly p = poly (q *** d); \ |
|
1077 \ poly (pderiv p) = poly (e *** d); \ |
|
1078 \ poly d = poly (r *** p +++ s *** pderiv p) \ |
|
1079 \ |] ==> ALL a. order a q = (if order a p = 0 then 0 else 1)"; |
|
1080 by (blast_tac (claset() addIs [poly_squarefree_decomp_order]) 1); |
|
1081 qed "poly_squarefree_decomp_order2"; |
|
1082 |
|
1083 Goal "poly p ~= poly [] ==> (poly p a = 0) = (order a p ~= 0)"; |
|
1084 by (rtac (order_root RS ssubst) 1); |
|
1085 by Auto_tac; |
|
1086 qed "order_root2"; |
|
1087 |
|
1088 Goal "[| poly (pderiv p) ~= poly []; order a p ~= 0 |] \ |
|
1089 \ ==> (order a (pderiv p) = n) = (order a p = Suc n)"; |
|
1090 by (auto_tac (claset() addDs [order_pderiv],simpset())); |
|
1091 qed "order_pderiv2"; |
|
1092 |
|
1093 Goalw [rsquarefree_def] |
|
1094 "rsquarefree p = (ALL a. ~(poly p a = 0 & poly (pderiv p) a = 0))"; |
|
1095 by (case_tac "poly p = poly []" 1); |
|
1096 by (Asm_full_simp_tac 1); |
|
1097 by (Asm_full_simp_tac 1); |
|
1098 by (case_tac "poly (pderiv p) = poly []" 1); |
|
1099 by (Asm_full_simp_tac 1); |
|
1100 by (dtac pderiv_iszero 1 THEN Clarify_tac 1); |
|
1101 by (subgoal_tac "ALL a. order a p = order a [h]" 1); |
|
1102 by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1); |
|
1103 by (rtac allI 1); |
|
1104 by (cut_inst_tac [("p","[h]"),("a","a")] order_root 1); |
|
1105 by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1); |
|
1106 by (blast_tac (claset() addIs [order_poly]) 1); |
|
1107 by (auto_tac (claset(),simpset() addsimps [order_root,order_pderiv2])); |
|
1108 by (dtac spec 1 THEN Auto_tac); |
|
1109 qed "rsquarefree_roots"; |
|
1110 |
|
1111 Goal "[1] *** p = p"; |
|
1112 by Auto_tac; |
|
1113 qed "pmult_one"; |
|
1114 Addsimps [pmult_one]; |
|
1115 |
|
1116 Goal "poly [] = poly [0]"; |
|
1117 by (simp_tac (simpset() addsimps [fun_eq]) 1); |
|
1118 qed "poly_Nil_zero"; |
|
1119 |
|
1120 Goalw [rsquarefree_def] |
|
1121 "[| rsquarefree p; poly p a = 0 |] \ |
|
1122 \ ==> EX q. (poly p = poly ([-a, 1] *** q)) & poly q a ~= 0"; |
|
1123 by (Step_tac 1); |
|
1124 by (forw_inst_tac [("a","a")] order_decomp 1); |
|
1125 by (dres_inst_tac [("x","a")] spec 1); |
|
1126 by (dres_inst_tac [("a1","a")] (order_root2 RS sym) 1); |
|
1127 by (auto_tac (claset(),simpset() delsimps [pmult_Cons])); |
|
1128 by (res_inst_tac [("x","q")] exI 1 THEN Step_tac 1); |
|
1129 by (asm_full_simp_tac (simpset() addsimps [poly_mult,fun_eq]) 1); |
|
1130 by (dres_inst_tac [("p1","q")] (poly_linear_divides RS iffD1) 1); |
|
1131 by (asm_full_simp_tac (simpset() addsimps [divides_def] |
|
1132 delsimps [pmult_Cons]) 1); |
|
1133 by (Step_tac 1); |
|
1134 by (dres_inst_tac [("x","[]")] spec 1); |
|
1135 by (auto_tac (claset(),simpset() addsimps [fun_eq])); |
|
1136 qed "rsquarefree_decomp"; |
|
1137 |
|
1138 Goal "[| poly (pderiv p) ~= poly []; \ |
|
1139 \ poly p = poly (q *** d); \ |
|
1140 \ poly (pderiv p) = poly (e *** d); \ |
|
1141 \ poly d = poly (r *** p +++ s *** pderiv p) \ |
|
1142 \ |] ==> rsquarefree q & (ALL a. (poly q a = 0) = (poly p a = 0))"; |
|
1143 by (ftac poly_squarefree_decomp_order2 1); |
|
1144 by (TRYALL(assume_tac)); |
|
1145 by (case_tac "poly p = poly []" 1); |
|
1146 by (blast_tac (claset() addDs [pderiv_zero]) 1); |
|
1147 by (simp_tac (simpset() addsimps [rsquarefree_def, |
|
1148 order_root] delsimps [pmult_Cons]) 1); |
|
1149 by (asm_full_simp_tac (simpset() addsimps [poly_entire] |
|
1150 delsimps [pmult_Cons]) 1); |
|
1151 qed "poly_squarefree_decomp"; |
|
1152 |
|
1153 |
|
1154 (* ------------------------------------------------------------------------- *) |
|
1155 (* Normalization of a polynomial. *) |
|
1156 (* ------------------------------------------------------------------------- *) |
|
1157 |
|
1158 Goal "poly (pnormalize p) = poly p"; |
|
1159 by (induct_tac "p" 1); |
|
1160 by (auto_tac (claset(),simpset() addsimps [fun_eq])); |
|
1161 qed "poly_normalize"; |
|
1162 Addsimps [poly_normalize]; |
|
1163 |
|
1164 |
|
1165 (* ------------------------------------------------------------------------- *) |
|
1166 (* The degree of a polynomial. *) |
|
1167 (* ------------------------------------------------------------------------- *) |
|
1168 |
|
1169 Goal "list_all (%c. c = 0) p --> pnormalize p = []"; |
|
1170 by (induct_tac "p" 1); |
|
1171 by Auto_tac; |
|
1172 qed_spec_mp "lemma_degree_zero"; |
|
1173 |
|
1174 Goalw [degree_def] "poly p = poly [] ==> degree p = 0"; |
|
1175 by (case_tac "pnormalize p = []" 1); |
|
1176 by (auto_tac (claset() addDs [lemma_degree_zero],simpset() |
|
1177 addsimps [poly_zero])); |
|
1178 qed "degree_zero"; |
|
1179 |
|
1180 (* ------------------------------------------------------------------------- *) |
|
1181 (* Tidier versions of finiteness of roots. *) |
|
1182 (* ------------------------------------------------------------------------- *) |
|
1183 |
|
1184 Goal "poly p ~= poly [] ==> finite {x. poly p x = 0}"; |
|
1185 by (auto_tac (claset(),simpset() addsimps [poly_roots_finite])); |
|
1186 by (res_inst_tac [("B","{x::real. EX n. (n::nat) < N & (x = j n)}")] |
|
1187 finite_subset 1); |
|
1188 by (induct_tac "N" 2); |
|
1189 by Auto_tac; |
|
1190 by (subgoal_tac "{x::real. EX na. na < Suc n & (x = j na)} = \ |
|
1191 \ {(j n)} Un {x. EX na. na < n & (x = j na)}" 1); |
|
1192 by (auto_tac (claset(),simpset() addsimps [ARITH_PROVE |
|
1193 "(na < Suc n) = (na = n | na < n)"])); |
|
1194 qed "poly_roots_finite_set"; |
|
1195 |
|
1196 (* ------------------------------------------------------------------------- *) |
|
1197 (* bound for polynomial. *) |
|
1198 (* ------------------------------------------------------------------------- *) |
|
1199 |
|
1200 Goal "abs(x) <= k --> abs(poly p x) <= poly (map abs p) k"; |
|
1201 by (induct_tac "p" 1); |
|
1202 by Auto_tac; |
|
1203 by (res_inst_tac [("j","abs a + abs(x * poly list x)")] real_le_trans 1); |
|
1204 by (rtac abs_triangle_ineq 1); |
|
1205 by (auto_tac (claset() addSIs [real_mult_le_mono],simpset() |
|
1206 addsimps [abs_mult])); |
|
1207 by (arith_tac 1); |
|
1208 qed_spec_mp "poly_mono"; |