1 (* Title: Poly.thy |
|
2 ID: $Id$ |
|
3 Author: Jacques D. Fleuriot |
|
4 Copyright: 2000 University of Edinburgh |
|
5 |
|
6 Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 |
|
7 *) |
|
8 |
|
9 header{*Univariate Real Polynomials*} |
|
10 |
|
11 theory Poly |
|
12 imports Deriv |
|
13 begin |
|
14 |
|
15 text{*Application of polynomial as a real function.*} |
|
16 |
|
17 consts poly :: "real list => real => real" |
|
18 primrec |
|
19 poly_Nil: "poly [] x = 0" |
|
20 poly_Cons: "poly (h#t) x = h + x * poly t x" |
|
21 |
|
22 |
|
23 subsection{*Arithmetic Operations on Polynomials*} |
|
24 |
|
25 text{*addition*} |
|
26 consts padd :: "[real list, real list] => real list" (infixl "+++" 65) |
|
27 primrec |
|
28 padd_Nil: "[] +++ l2 = l2" |
|
29 padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t |
|
30 else (h + hd l2)#(t +++ tl l2))" |
|
31 |
|
32 text{*Multiplication by a constant*} |
|
33 consts cmult :: "[real, real list] => real list" (infixl "%*" 70) |
|
34 primrec |
|
35 cmult_Nil: "c %* [] = []" |
|
36 cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)" |
|
37 |
|
38 text{*Multiplication by a polynomial*} |
|
39 consts pmult :: "[real list, real list] => real list" (infixl "***" 70) |
|
40 primrec |
|
41 pmult_Nil: "[] *** l2 = []" |
|
42 pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2 |
|
43 else (h %* l2) +++ ((0) # (t *** l2)))" |
|
44 |
|
45 text{*Repeated multiplication by a polynomial*} |
|
46 consts mulexp :: "[nat, real list, real list] => real list" |
|
47 primrec |
|
48 mulexp_zero: "mulexp 0 p q = q" |
|
49 mulexp_Suc: "mulexp (Suc n) p q = p *** mulexp n p q" |
|
50 |
|
51 text{*Exponential*} |
|
52 consts pexp :: "[real list, nat] => real list" (infixl "%^" 80) |
|
53 primrec |
|
54 pexp_0: "p %^ 0 = [1]" |
|
55 pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)" |
|
56 |
|
57 text{*Quotient related value of dividing a polynomial by x + a*} |
|
58 (* Useful for divisor properties in inductive proofs *) |
|
59 consts "pquot" :: "[real list, real] => real list" |
|
60 primrec |
|
61 pquot_Nil: "pquot [] a= []" |
|
62 pquot_Cons: "pquot (h#t) a = (if t = [] then [h] |
|
63 else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))" |
|
64 |
|
65 text{*Differentiation of polynomials (needs an auxiliary function).*} |
|
66 consts pderiv_aux :: "nat => real list => real list" |
|
67 primrec |
|
68 pderiv_aux_Nil: "pderiv_aux n [] = []" |
|
69 pderiv_aux_Cons: "pderiv_aux n (h#t) = |
|
70 (real n * h)#(pderiv_aux (Suc n) t)" |
|
71 |
|
72 text{*normalization of polynomials (remove extra 0 coeff)*} |
|
73 consts pnormalize :: "real list => real list" |
|
74 primrec |
|
75 pnormalize_Nil: "pnormalize [] = []" |
|
76 pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = []) |
|
77 then (if (h = 0) then [] else [h]) |
|
78 else (h#(pnormalize p)))" |
|
79 |
|
80 definition "pnormal p = ((pnormalize p = p) \<and> p \<noteq> [])" |
|
81 definition "nonconstant p = (pnormal p \<and> (\<forall>x. p \<noteq> [x]))" |
|
82 text{*Other definitions*} |
|
83 |
|
84 definition |
|
85 poly_minus :: "real list => real list" ("-- _" [80] 80) where |
|
86 "-- p = (- 1) %* p" |
|
87 |
|
88 definition |
|
89 pderiv :: "real list => real list" where |
|
90 "pderiv p = (if p = [] then [] else pderiv_aux 1 (tl p))" |
|
91 |
|
92 definition |
|
93 divides :: "[real list,real list] => bool" (infixl "divides" 70) where |
|
94 "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))" |
|
95 |
|
96 definition |
|
97 order :: "real => real list => nat" where |
|
98 --{*order of a polynomial*} |
|
99 "order a p = (SOME n. ([-a, 1] %^ n) divides p & |
|
100 ~ (([-a, 1] %^ (Suc n)) divides p))" |
|
101 |
|
102 definition |
|
103 degree :: "real list => nat" where |
|
104 --{*degree of a polynomial*} |
|
105 "degree p = length (pnormalize p) - 1" |
|
106 |
|
107 definition |
|
108 rsquarefree :: "real list => bool" where |
|
109 --{*squarefree polynomials --- NB with respect to real roots only.*} |
|
110 "rsquarefree p = (poly p \<noteq> poly [] & |
|
111 (\<forall>a. (order a p = 0) | (order a p = 1)))" |
|
112 |
|
113 |
|
114 |
|
115 lemma padd_Nil2: "p +++ [] = p" |
|
116 by (induct p) auto |
|
117 declare padd_Nil2 [simp] |
|
118 |
|
119 lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)" |
|
120 by auto |
|
121 |
|
122 lemma pminus_Nil: "-- [] = []" |
|
123 by (simp add: poly_minus_def) |
|
124 declare pminus_Nil [simp] |
|
125 |
|
126 lemma pmult_singleton: "[h1] *** p1 = h1 %* p1" |
|
127 by simp |
|
128 |
|
129 lemma poly_ident_mult: "1 %* t = t" |
|
130 by (induct "t", auto) |
|
131 declare poly_ident_mult [simp] |
|
132 |
|
133 lemma poly_simple_add_Cons: "[a] +++ ((0)#t) = (a#t)" |
|
134 by simp |
|
135 declare poly_simple_add_Cons [simp] |
|
136 |
|
137 text{*Handy general properties*} |
|
138 |
|
139 lemma padd_commut: "b +++ a = a +++ b" |
|
140 apply (subgoal_tac "\<forall>a. b +++ a = a +++ b") |
|
141 apply (induct_tac [2] "b", auto) |
|
142 apply (rule padd_Cons [THEN ssubst]) |
|
143 apply (case_tac "aa", auto) |
|
144 done |
|
145 |
|
146 lemma padd_assoc [rule_format]: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)" |
|
147 apply (induct "a", simp, clarify) |
|
148 apply (case_tac b, simp_all) |
|
149 done |
|
150 |
|
151 lemma poly_cmult_distr [rule_format]: |
|
152 "\<forall>q. a %* ( p +++ q) = (a %* p +++ a %* q)" |
|
153 apply (induct "p", simp, clarify) |
|
154 apply (case_tac "q") |
|
155 apply (simp_all add: right_distrib) |
|
156 done |
|
157 |
|
158 lemma pmult_by_x: "[0, 1] *** t = ((0)#t)" |
|
159 apply (induct "t", simp) |
|
160 apply (auto simp add: poly_ident_mult padd_commut) |
|
161 done |
|
162 declare pmult_by_x [simp] |
|
163 |
|
164 |
|
165 text{*properties of evaluation of polynomials.*} |
|
166 |
|
167 lemma poly_add: "poly (p1 +++ p2) x = poly p1 x + poly p2 x" |
|
168 apply (subgoal_tac "\<forall>p2. poly (p1 +++ p2) x = poly (p1) x + poly (p2) x") |
|
169 apply (induct_tac [2] "p1", auto) |
|
170 apply (case_tac "p2") |
|
171 apply (auto simp add: right_distrib) |
|
172 done |
|
173 |
|
174 lemma poly_cmult: "poly (c %* p) x = c * poly p x" |
|
175 apply (induct "p") |
|
176 apply (case_tac [2] "x=0") |
|
177 apply (auto simp add: right_distrib mult_ac) |
|
178 done |
|
179 |
|
180 lemma poly_minus: "poly (-- p) x = - (poly p x)" |
|
181 apply (simp add: poly_minus_def) |
|
182 apply (auto simp add: poly_cmult) |
|
183 done |
|
184 |
|
185 lemma poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x" |
|
186 apply (subgoal_tac "\<forall>p2. poly (p1 *** p2) x = poly p1 x * poly p2 x") |
|
187 apply (simp (no_asm_simp)) |
|
188 apply (induct "p1") |
|
189 apply (auto simp add: poly_cmult) |
|
190 apply (case_tac p1) |
|
191 apply (auto simp add: poly_cmult poly_add left_distrib right_distrib mult_ac) |
|
192 done |
|
193 |
|
194 lemma poly_exp: "poly (p %^ n) x = (poly p x) ^ n" |
|
195 apply (induct "n") |
|
196 apply (auto simp add: poly_cmult poly_mult) |
|
197 done |
|
198 |
|
199 text{*More Polynomial Evaluation Lemmas*} |
|
200 |
|
201 lemma poly_add_rzero: "poly (a +++ []) x = poly a x" |
|
202 by simp |
|
203 declare poly_add_rzero [simp] |
|
204 |
|
205 lemma poly_mult_assoc: "poly ((a *** b) *** c) x = poly (a *** (b *** c)) x" |
|
206 by (simp add: poly_mult real_mult_assoc) |
|
207 |
|
208 lemma poly_mult_Nil2: "poly (p *** []) x = 0" |
|
209 by (induct "p", auto) |
|
210 declare poly_mult_Nil2 [simp] |
|
211 |
|
212 lemma poly_exp_add: "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d) x" |
|
213 apply (induct "n") |
|
214 apply (auto simp add: poly_mult real_mult_assoc) |
|
215 done |
|
216 |
|
217 text{*The derivative*} |
|
218 |
|
219 lemma pderiv_Nil: "pderiv [] = []" |
|
220 |
|
221 apply (simp add: pderiv_def) |
|
222 done |
|
223 declare pderiv_Nil [simp] |
|
224 |
|
225 lemma pderiv_singleton: "pderiv [c] = []" |
|
226 by (simp add: pderiv_def) |
|
227 declare pderiv_singleton [simp] |
|
228 |
|
229 lemma pderiv_Cons: "pderiv (h#t) = pderiv_aux 1 t" |
|
230 by (simp add: pderiv_def) |
|
231 |
|
232 lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c" |
|
233 by (simp add: DERIV_cmult mult_commute [of _ c]) |
|
234 |
|
235 lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)" |
|
236 by (rule lemma_DERIV_subst, rule DERIV_pow, simp) |
|
237 declare DERIV_pow2 [simp] DERIV_pow [simp] |
|
238 |
|
239 lemma lemma_DERIV_poly1: "\<forall>n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :> |
|
240 x ^ n * poly (pderiv_aux (Suc n) p) x " |
|
241 apply (induct "p") |
|
242 apply (auto intro!: DERIV_add DERIV_cmult2 |
|
243 simp add: pderiv_def right_distrib real_mult_assoc [symmetric] |
|
244 simp del: realpow_Suc) |
|
245 apply (subst mult_commute) |
|
246 apply (simp del: realpow_Suc) |
|
247 apply (simp add: mult_commute realpow_Suc [symmetric] del: realpow_Suc) |
|
248 done |
|
249 |
|
250 lemma lemma_DERIV_poly: "DERIV (%x. (x ^ (Suc n) * poly p x)) x :> |
|
251 x ^ n * poly (pderiv_aux (Suc n) p) x " |
|
252 by (simp add: lemma_DERIV_poly1 del: realpow_Suc) |
|
253 |
|
254 lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (%x. a + f x :: real) x :> D" |
|
255 by (rule lemma_DERIV_subst, rule DERIV_add, auto) |
|
256 |
|
257 lemma poly_DERIV: "DERIV (%x. poly p x) x :> poly (pderiv p) x" |
|
258 apply (induct "p") |
|
259 apply (auto simp add: pderiv_Cons) |
|
260 apply (rule DERIV_add_const) |
|
261 apply (rule lemma_DERIV_subst) |
|
262 apply (rule lemma_DERIV_poly [where n=0, simplified], simp) |
|
263 done |
|
264 declare poly_DERIV [simp] |
|
265 |
|
266 |
|
267 text{* Consequences of the derivative theorem above*} |
|
268 |
|
269 lemma poly_differentiable: "(%x. poly p x) differentiable x" |
|
270 |
|
271 apply (simp add: differentiable_def) |
|
272 apply (blast intro: poly_DERIV) |
|
273 done |
|
274 declare poly_differentiable [simp] |
|
275 |
|
276 lemma poly_isCont: "isCont (%x. poly p x) x" |
|
277 by (rule poly_DERIV [THEN DERIV_isCont]) |
|
278 declare poly_isCont [simp] |
|
279 |
|
280 lemma poly_IVT_pos: "[| a < b; poly p a < 0; 0 < poly p b |] |
|
281 ==> \<exists>x. a < x & x < b & (poly p x = 0)" |
|
282 apply (cut_tac f = "%x. poly p x" and a = a and b = b and y = 0 in IVT_objl) |
|
283 apply (auto simp add: order_le_less) |
|
284 done |
|
285 |
|
286 lemma poly_IVT_neg: "[| a < b; 0 < poly p a; poly p b < 0 |] |
|
287 ==> \<exists>x. a < x & x < b & (poly p x = 0)" |
|
288 apply (insert poly_IVT_pos [where p = "-- p" ]) |
|
289 apply (simp add: poly_minus neg_less_0_iff_less) |
|
290 done |
|
291 |
|
292 lemma poly_MVT: "a < b ==> |
|
293 \<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)" |
|
294 apply (drule_tac f = "poly p" in MVT, auto) |
|
295 apply (rule_tac x = z in exI) |
|
296 apply (auto simp add: real_mult_left_cancel poly_DERIV [THEN DERIV_unique]) |
|
297 done |
|
298 |
|
299 text{*Lemmas for Derivatives*} |
|
300 |
|
301 lemma lemma_poly_pderiv_aux_add: "\<forall>p2 n. poly (pderiv_aux n (p1 +++ p2)) x = |
|
302 poly (pderiv_aux n p1 +++ pderiv_aux n p2) x" |
|
303 apply (induct "p1", simp, clarify) |
|
304 apply (case_tac "p2") |
|
305 apply (auto simp add: right_distrib) |
|
306 done |
|
307 |
|
308 lemma poly_pderiv_aux_add: "poly (pderiv_aux n (p1 +++ p2)) x = |
|
309 poly (pderiv_aux n p1 +++ pderiv_aux n p2) x" |
|
310 apply (simp add: lemma_poly_pderiv_aux_add) |
|
311 done |
|
312 |
|
313 lemma lemma_poly_pderiv_aux_cmult: "\<forall>n. poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x" |
|
314 apply (induct "p") |
|
315 apply (auto simp add: poly_cmult mult_ac) |
|
316 done |
|
317 |
|
318 lemma poly_pderiv_aux_cmult: "poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x" |
|
319 by (simp add: lemma_poly_pderiv_aux_cmult) |
|
320 |
|
321 lemma poly_pderiv_aux_minus: |
|
322 "poly (pderiv_aux n (-- p)) x = poly (-- pderiv_aux n p) x" |
|
323 apply (simp add: poly_minus_def poly_pderiv_aux_cmult) |
|
324 done |
|
325 |
|
326 lemma lemma_poly_pderiv_aux_mult1: "\<forall>n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x" |
|
327 apply (induct "p") |
|
328 apply (auto simp add: real_of_nat_Suc left_distrib) |
|
329 done |
|
330 |
|
331 lemma lemma_poly_pderiv_aux_mult: "poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x" |
|
332 by (simp add: lemma_poly_pderiv_aux_mult1) |
|
333 |
|
334 lemma lemma_poly_pderiv_add: "\<forall>q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x" |
|
335 apply (induct "p", simp, clarify) |
|
336 apply (case_tac "q") |
|
337 apply (auto simp add: poly_pderiv_aux_add poly_add pderiv_def) |
|
338 done |
|
339 |
|
340 lemma poly_pderiv_add: "poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x" |
|
341 by (simp add: lemma_poly_pderiv_add) |
|
342 |
|
343 lemma poly_pderiv_cmult: "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x" |
|
344 apply (induct "p") |
|
345 apply (auto simp add: poly_pderiv_aux_cmult poly_cmult pderiv_def) |
|
346 done |
|
347 |
|
348 lemma poly_pderiv_minus: "poly (pderiv (--p)) x = poly (--(pderiv p)) x" |
|
349 by (simp add: poly_minus_def poly_pderiv_cmult) |
|
350 |
|
351 lemma lemma_poly_mult_pderiv: |
|
352 "poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x" |
|
353 apply (simp add: pderiv_def) |
|
354 apply (induct "t") |
|
355 apply (auto simp add: poly_add lemma_poly_pderiv_aux_mult) |
|
356 done |
|
357 |
|
358 lemma poly_pderiv_mult: "\<forall>q. poly (pderiv (p *** q)) x = |
|
359 poly (p *** (pderiv q) +++ q *** (pderiv p)) x" |
|
360 apply (induct "p") |
|
361 apply (auto simp add: poly_add poly_cmult poly_pderiv_cmult poly_pderiv_add poly_mult) |
|
362 apply (rule lemma_poly_mult_pderiv [THEN ssubst]) |
|
363 apply (rule lemma_poly_mult_pderiv [THEN ssubst]) |
|
364 apply (rule poly_add [THEN ssubst]) |
|
365 apply (rule poly_add [THEN ssubst]) |
|
366 apply (simp (no_asm_simp) add: poly_mult right_distrib add_ac mult_ac) |
|
367 done |
|
368 |
|
369 lemma poly_pderiv_exp: "poly (pderiv (p %^ (Suc n))) x = |
|
370 poly ((real (Suc n)) %* (p %^ n) *** pderiv p) x" |
|
371 apply (induct "n") |
|
372 apply (auto simp add: poly_add poly_pderiv_cmult poly_cmult poly_pderiv_mult |
|
373 real_of_nat_zero poly_mult real_of_nat_Suc |
|
374 right_distrib left_distrib mult_ac) |
|
375 done |
|
376 |
|
377 lemma poly_pderiv_exp_prime: "poly (pderiv ([-a, 1] %^ (Suc n))) x = |
|
378 poly (real (Suc n) %* ([-a, 1] %^ n)) x" |
|
379 apply (simp add: poly_pderiv_exp poly_mult del: pexp_Suc) |
|
380 apply (simp add: poly_cmult pderiv_def) |
|
381 done |
|
382 |
|
383 subsection{*Key Property: if @{term "f(a) = 0"} then @{term "(x - a)"} divides |
|
384 @{term "p(x)"} *} |
|
385 |
|
386 lemma lemma_poly_linear_rem: "\<forall>h. \<exists>q r. h#t = [r] +++ [-a, 1] *** q" |
|
387 apply (induct "t", safe) |
|
388 apply (rule_tac x = "[]" in exI) |
|
389 apply (rule_tac x = h in exI, simp) |
|
390 apply (drule_tac x = aa in spec, safe) |
|
391 apply (rule_tac x = "r#q" in exI) |
|
392 apply (rule_tac x = "a*r + h" in exI) |
|
393 apply (case_tac "q", auto) |
|
394 done |
|
395 |
|
396 lemma poly_linear_rem: "\<exists>q r. h#t = [r] +++ [-a, 1] *** q" |
|
397 by (cut_tac t = t and a = a in lemma_poly_linear_rem, auto) |
|
398 |
|
399 |
|
400 lemma poly_linear_divides: "(poly p a = 0) = ((p = []) | (\<exists>q. p = [-a, 1] *** q))" |
|
401 apply (auto simp add: poly_add poly_cmult right_distrib) |
|
402 apply (case_tac "p", simp) |
|
403 apply (cut_tac h = aa and t = list and a = a in poly_linear_rem, safe) |
|
404 apply (case_tac "q", auto) |
|
405 apply (drule_tac x = "[]" in spec, simp) |
|
406 apply (auto simp add: poly_add poly_cmult add_assoc) |
|
407 apply (drule_tac x = "aa#lista" in spec, auto) |
|
408 done |
|
409 |
|
410 lemma lemma_poly_length_mult: "\<forall>h k a. length (k %* p +++ (h # (a %* p))) = Suc (length p)" |
|
411 by (induct "p", auto) |
|
412 declare lemma_poly_length_mult [simp] |
|
413 |
|
414 lemma lemma_poly_length_mult2: "\<forall>h k. length (k %* p +++ (h # p)) = Suc (length p)" |
|
415 by (induct "p", auto) |
|
416 declare lemma_poly_length_mult2 [simp] |
|
417 |
|
418 lemma poly_length_mult: "length([-a,1] *** q) = Suc (length q)" |
|
419 by auto |
|
420 declare poly_length_mult [simp] |
|
421 |
|
422 |
|
423 subsection{*Polynomial length*} |
|
424 |
|
425 lemma poly_cmult_length: "length (a %* p) = length p" |
|
426 by (induct "p", auto) |
|
427 declare poly_cmult_length [simp] |
|
428 |
|
429 lemma poly_add_length [rule_format]: |
|
430 "\<forall>p2. length (p1 +++ p2) = |
|
431 (if (length p1 < length p2) then length p2 else length p1)" |
|
432 apply (induct "p1", simp_all) |
|
433 apply arith |
|
434 done |
|
435 |
|
436 lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)" |
|
437 by (simp add: poly_cmult_length poly_add_length) |
|
438 declare poly_root_mult_length [simp] |
|
439 |
|
440 lemma poly_mult_not_eq_poly_Nil: "(poly (p *** q) x \<noteq> poly [] x) = |
|
441 (poly p x \<noteq> poly [] x & poly q x \<noteq> poly [] x)" |
|
442 apply (auto simp add: poly_mult) |
|
443 done |
|
444 declare poly_mult_not_eq_poly_Nil [simp] |
|
445 |
|
446 lemma poly_mult_eq_zero_disj: "(poly (p *** q) x = 0) = (poly p x = 0 | poly q x = 0)" |
|
447 by (auto simp add: poly_mult) |
|
448 |
|
449 text{*Normalisation Properties*} |
|
450 |
|
451 lemma poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)" |
|
452 by (induct "p", auto) |
|
453 |
|
454 text{*A nontrivial polynomial of degree n has no more than n roots*} |
|
455 |
|
456 lemma poly_roots_index_lemma [rule_format]: |
|
457 "\<forall>p x. poly p x \<noteq> poly [] x & length p = n |
|
458 --> (\<exists>i. \<forall>x. (poly p x = (0::real)) --> (\<exists>m. (m \<le> n & x = i m)))" |
|
459 apply (induct "n", safe) |
|
460 apply (rule ccontr) |
|
461 apply (subgoal_tac "\<exists>a. poly p a = 0", safe) |
|
462 apply (drule poly_linear_divides [THEN iffD1], safe) |
|
463 apply (drule_tac x = q in spec) |
|
464 apply (drule_tac x = x in spec) |
|
465 apply (simp del: poly_Nil pmult_Cons) |
|
466 apply (erule exE) |
|
467 apply (drule_tac x = "%m. if m = Suc n then a else i m" in spec, safe) |
|
468 apply (drule poly_mult_eq_zero_disj [THEN iffD1], safe) |
|
469 apply (drule_tac x = "Suc (length q)" in spec) |
|
470 apply simp |
|
471 apply (drule_tac x = xa in spec, safe) |
|
472 apply (drule_tac x = m in spec, simp, blast) |
|
473 done |
|
474 lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma, standard] |
|
475 |
|
476 lemma poly_roots_index_length: "poly p x \<noteq> poly [] x ==> |
|
477 \<exists>i. \<forall>x. (poly p x = 0) --> (\<exists>n. n \<le> length p & x = i n)" |
|
478 by (blast intro: poly_roots_index_lemma2) |
|
479 |
|
480 lemma poly_roots_finite_lemma: "poly p x \<noteq> poly [] x ==> |
|
481 \<exists>N i. \<forall>x. (poly p x = 0) --> (\<exists>n. (n::nat) < N & x = i n)" |
|
482 apply (drule poly_roots_index_length, safe) |
|
483 apply (rule_tac x = "Suc (length p)" in exI) |
|
484 apply (rule_tac x = i in exI) |
|
485 apply (simp add: less_Suc_eq_le) |
|
486 done |
|
487 |
|
488 (* annoying proof *) |
|
489 lemma real_finite_lemma [rule_format (no_asm)]: |
|
490 "\<forall>P. (\<forall>x. P x --> (\<exists>n. n < N & x = (j::nat=>real) n)) |
|
491 --> (\<exists>a. \<forall>x. P x --> x < a)" |
|
492 apply (induct "N", simp, safe) |
|
493 apply (drule_tac x = "%z. P z & (z \<noteq> j N)" in spec) |
|
494 apply (auto simp add: less_Suc_eq) |
|
495 apply (rename_tac N P a) |
|
496 apply (rule_tac x = "abs a + abs (j N) + 1" in exI) |
|
497 apply safe |
|
498 apply (drule_tac x = x in spec, safe) |
|
499 apply (drule_tac x = "j n" in spec) |
|
500 apply arith |
|
501 apply arith |
|
502 done |
|
503 |
|
504 lemma poly_roots_finite: "(poly p \<noteq> poly []) = |
|
505 (\<exists>N j. \<forall>x. poly p x = 0 --> (\<exists>n. (n::nat) < N & x = j n))" |
|
506 apply safe |
|
507 apply (erule contrapos_np, rule ext) |
|
508 apply (rule ccontr) |
|
509 apply (clarify dest!: poly_roots_finite_lemma) |
|
510 apply (clarify dest!: real_finite_lemma) |
|
511 apply (drule_tac x = a in fun_cong, auto) |
|
512 done |
|
513 |
|
514 text{*Entirety and Cancellation for polynomials*} |
|
515 |
|
516 lemma poly_entire_lemma: "[| poly p \<noteq> poly [] ; poly q \<noteq> poly [] |] |
|
517 ==> poly (p *** q) \<noteq> poly []" |
|
518 apply (auto simp add: poly_roots_finite) |
|
519 apply (rule_tac x = "N + Na" in exI) |
|
520 apply (rule_tac x = "%n. if n < N then j n else ja (n - N)" in exI) |
|
521 apply (auto simp add: poly_mult_eq_zero_disj, force) |
|
522 done |
|
523 |
|
524 lemma poly_entire: "(poly (p *** q) = poly []) = ((poly p = poly []) | (poly q = poly []))" |
|
525 apply (auto intro: ext dest: fun_cong simp add: poly_entire_lemma poly_mult) |
|
526 apply (blast intro: ccontr dest: poly_entire_lemma poly_mult [THEN subst]) |
|
527 done |
|
528 |
|
529 lemma poly_entire_neg: "(poly (p *** q) \<noteq> poly []) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))" |
|
530 by (simp add: poly_entire) |
|
531 |
|
532 lemma fun_eq: " (f = g) = (\<forall>x. f x = g x)" |
|
533 by (auto intro!: ext) |
|
534 |
|
535 lemma poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)" |
|
536 by (auto simp add: poly_add poly_minus_def fun_eq poly_cmult) |
|
537 |
|
538 lemma poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))" |
|
539 by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib) |
|
540 |
|
541 lemma poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)" |
|
542 apply (rule_tac p1 = "p *** q" in poly_add_minus_zero_iff [THEN subst]) |
|
543 apply (auto intro: ext simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff) |
|
544 done |
|
545 |
|
546 lemma real_mult_zero_disj_iff: "(x * y = 0) = (x = (0::real) | y = 0)" |
|
547 by simp |
|
548 |
|
549 lemma poly_exp_eq_zero: |
|
550 "(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)" |
|
551 apply (simp only: fun_eq add: all_simps [symmetric]) |
|
552 apply (rule arg_cong [where f = All]) |
|
553 apply (rule ext) |
|
554 apply (induct_tac "n") |
|
555 apply (auto simp add: poly_mult real_mult_zero_disj_iff) |
|
556 done |
|
557 declare poly_exp_eq_zero [simp] |
|
558 |
|
559 lemma poly_prime_eq_zero: "poly [a,1] \<noteq> poly []" |
|
560 apply (simp add: fun_eq) |
|
561 apply (rule_tac x = "1 - a" in exI, simp) |
|
562 done |
|
563 declare poly_prime_eq_zero [simp] |
|
564 |
|
565 lemma poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])" |
|
566 by auto |
|
567 declare poly_exp_prime_eq_zero [simp] |
|
568 |
|
569 text{*A more constructive notion of polynomials being trivial*} |
|
570 |
|
571 lemma poly_zero_lemma: "poly (h # t) = poly [] ==> h = 0 & poly t = poly []" |
|
572 apply (simp add: fun_eq) |
|
573 apply (case_tac "h = 0") |
|
574 apply (drule_tac [2] x = 0 in spec, auto) |
|
575 apply (case_tac "poly t = poly []", simp) |
|
576 apply (auto simp add: poly_roots_finite real_mult_zero_disj_iff) |
|
577 apply (drule real_finite_lemma, safe) |
|
578 apply (drule_tac x = "abs a + 1" in spec)+ |
|
579 apply arith |
|
580 done |
|
581 |
|
582 |
|
583 lemma poly_zero: "(poly p = poly []) = list_all (%c. c = 0) p" |
|
584 apply (induct "p", simp) |
|
585 apply (rule iffI) |
|
586 apply (drule poly_zero_lemma, auto) |
|
587 done |
|
588 |
|
589 declare real_mult_zero_disj_iff [simp] |
|
590 |
|
591 lemma pderiv_aux_iszero [rule_format, simp]: |
|
592 "\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p" |
|
593 by (induct "p", auto) |
|
594 |
|
595 lemma pderiv_aux_iszero_num: "(number_of n :: nat) \<noteq> 0 |
|
596 ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) = |
|
597 list_all (%c. c = 0) p)" |
|
598 apply(drule not0_implies_Suc, clarify) |
|
599 apply (rule_tac n1 = "m" in pderiv_aux_iszero [THEN subst]) |
|
600 apply (simp (no_asm_simp) del: pderiv_aux_iszero) |
|
601 done |
|
602 |
|
603 lemma pderiv_iszero [rule_format]: |
|
604 "poly (pderiv p) = poly [] --> (\<exists>h. poly p = poly [h])" |
|
605 apply (simp add: poly_zero) |
|
606 apply (induct "p", force) |
|
607 apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons) |
|
608 apply (auto simp add: poly_zero [symmetric]) |
|
609 done |
|
610 |
|
611 lemma pderiv_zero_obj: "poly p = poly [] --> (poly (pderiv p) = poly [])" |
|
612 apply (simp add: poly_zero) |
|
613 apply (induct "p", force) |
|
614 apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons) |
|
615 done |
|
616 |
|
617 lemma pderiv_zero: "poly p = poly [] ==> (poly (pderiv p) = poly [])" |
|
618 by (blast elim: pderiv_zero_obj [THEN impE]) |
|
619 declare pderiv_zero [simp] |
|
620 |
|
621 lemma poly_pderiv_welldef: "poly p = poly q ==> (poly (pderiv p) = poly (pderiv q))" |
|
622 apply (cut_tac p = "p +++ --q" in pderiv_zero_obj) |
|
623 apply (simp add: fun_eq poly_add poly_minus poly_pderiv_add poly_pderiv_minus del: pderiv_zero) |
|
624 done |
|
625 |
|
626 text{*Basics of divisibility.*} |
|
627 |
|
628 lemma poly_primes: "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)" |
|
629 apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric]) |
|
630 apply (drule_tac x = "-a" in spec) |
|
631 apply (auto simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric]) |
|
632 apply (rule_tac x = "qa *** q" in exI) |
|
633 apply (rule_tac [2] x = "p *** qa" in exI) |
|
634 apply (auto simp add: poly_add poly_mult poly_cmult mult_ac) |
|
635 done |
|
636 |
|
637 lemma poly_divides_refl: "p divides p" |
|
638 apply (simp add: divides_def) |
|
639 apply (rule_tac x = "[1]" in exI) |
|
640 apply (auto simp add: poly_mult fun_eq) |
|
641 done |
|
642 declare poly_divides_refl [simp] |
|
643 |
|
644 lemma poly_divides_trans: "[| p divides q; q divides r |] ==> p divides r" |
|
645 apply (simp add: divides_def, safe) |
|
646 apply (rule_tac x = "qa *** qaa" in exI) |
|
647 apply (auto simp add: poly_mult fun_eq real_mult_assoc) |
|
648 done |
|
649 |
|
650 lemma poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)" |
|
651 apply (auto simp add: le_iff_add) |
|
652 apply (induct_tac k) |
|
653 apply (rule_tac [2] poly_divides_trans) |
|
654 apply (auto simp add: divides_def) |
|
655 apply (rule_tac x = p in exI) |
|
656 apply (auto simp add: poly_mult fun_eq mult_ac) |
|
657 done |
|
658 |
|
659 lemma poly_exp_divides: "[| (p %^ n) divides q; m\<le>n |] ==> (p %^ m) divides q" |
|
660 by (blast intro: poly_divides_exp poly_divides_trans) |
|
661 |
|
662 lemma poly_divides_add: |
|
663 "[| p divides q; p divides r |] ==> p divides (q +++ r)" |
|
664 apply (simp add: divides_def, auto) |
|
665 apply (rule_tac x = "qa +++ qaa" in exI) |
|
666 apply (auto simp add: poly_add fun_eq poly_mult right_distrib) |
|
667 done |
|
668 |
|
669 lemma poly_divides_diff: |
|
670 "[| p divides q; p divides (q +++ r) |] ==> p divides r" |
|
671 apply (simp add: divides_def, auto) |
|
672 apply (rule_tac x = "qaa +++ -- qa" in exI) |
|
673 apply (auto simp add: poly_add fun_eq poly_mult poly_minus right_diff_distrib compare_rls add_ac) |
|
674 done |
|
675 |
|
676 lemma poly_divides_diff2: "[| p divides r; p divides (q +++ r) |] ==> p divides q" |
|
677 apply (erule poly_divides_diff) |
|
678 apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac) |
|
679 done |
|
680 |
|
681 lemma poly_divides_zero: "poly p = poly [] ==> q divides p" |
|
682 apply (simp add: divides_def) |
|
683 apply (auto simp add: fun_eq poly_mult) |
|
684 done |
|
685 |
|
686 lemma poly_divides_zero2: "q divides []" |
|
687 apply (simp add: divides_def) |
|
688 apply (rule_tac x = "[]" in exI) |
|
689 apply (auto simp add: fun_eq) |
|
690 done |
|
691 declare poly_divides_zero2 [simp] |
|
692 |
|
693 text{*At last, we can consider the order of a root.*} |
|
694 |
|
695 |
|
696 lemma poly_order_exists_lemma [rule_format]: |
|
697 "\<forall>p. length p = d --> poly p \<noteq> poly [] |
|
698 --> (\<exists>n q. p = mulexp n [-a, 1] q & poly q a \<noteq> 0)" |
|
699 apply (induct "d") |
|
700 apply (simp add: fun_eq, safe) |
|
701 apply (case_tac "poly p a = 0") |
|
702 apply (drule_tac poly_linear_divides [THEN iffD1], safe) |
|
703 apply (drule_tac x = q in spec) |
|
704 apply (drule_tac poly_entire_neg [THEN iffD1], safe, force, blast) |
|
705 apply (rule_tac x = "Suc n" in exI) |
|
706 apply (rule_tac x = qa in exI) |
|
707 apply (simp del: pmult_Cons) |
|
708 apply (rule_tac x = 0 in exI, force) |
|
709 done |
|
710 |
|
711 (* FIXME: Tidy up *) |
|
712 lemma poly_order_exists: |
|
713 "[| length p = d; poly p \<noteq> poly [] |] |
|
714 ==> \<exists>n. ([-a, 1] %^ n) divides p & |
|
715 ~(([-a, 1] %^ (Suc n)) divides p)" |
|
716 apply (drule poly_order_exists_lemma [where a=a], assumption, clarify) |
|
717 apply (rule_tac x = n in exI, safe) |
|
718 apply (unfold divides_def) |
|
719 apply (rule_tac x = q in exI) |
|
720 apply (induct_tac "n", simp) |
|
721 apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac) |
|
722 apply safe |
|
723 apply (subgoal_tac "poly (mulexp n [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc n *** qa)") |
|
724 apply simp |
|
725 apply (induct_tac "n") |
|
726 apply (simp del: pmult_Cons pexp_Suc) |
|
727 apply (erule_tac Q = "poly q a = 0" in contrapos_np) |
|
728 apply (simp add: poly_add poly_cmult) |
|
729 apply (rule pexp_Suc [THEN ssubst]) |
|
730 apply (rule ccontr) |
|
731 apply (simp add: poly_mult_left_cancel poly_mult_assoc del: pmult_Cons pexp_Suc) |
|
732 done |
|
733 |
|
734 lemma poly_one_divides: "[1] divides p" |
|
735 by (simp add: divides_def, auto) |
|
736 declare poly_one_divides [simp] |
|
737 |
|
738 lemma poly_order: "poly p \<noteq> poly [] |
|
739 ==> EX! n. ([-a, 1] %^ n) divides p & |
|
740 ~(([-a, 1] %^ (Suc n)) divides p)" |
|
741 apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc) |
|
742 apply (metis Suc_leI less_linear poly_exp_divides) |
|
743 done |
|
744 |
|
745 text{*Order*} |
|
746 |
|
747 lemma some1_equalityD: "[| n = (@n. P n); EX! n. P n |] ==> P n" |
|
748 by (blast intro: someI2) |
|
749 |
|
750 lemma order: |
|
751 "(([-a, 1] %^ n) divides p & |
|
752 ~(([-a, 1] %^ (Suc n)) divides p)) = |
|
753 ((n = order a p) & ~(poly p = poly []))" |
|
754 apply (unfold order_def) |
|
755 apply (rule iffI) |
|
756 apply (blast dest: poly_divides_zero intro!: some1_equality [symmetric] poly_order) |
|
757 apply (blast intro!: poly_order [THEN [2] some1_equalityD]) |
|
758 done |
|
759 |
|
760 lemma order2: "[| poly p \<noteq> poly [] |] |
|
761 ==> ([-a, 1] %^ (order a p)) divides p & |
|
762 ~(([-a, 1] %^ (Suc(order a p))) divides p)" |
|
763 by (simp add: order del: pexp_Suc) |
|
764 |
|
765 lemma order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p; |
|
766 ~(([-a, 1] %^ (Suc n)) divides p) |
|
767 |] ==> (n = order a p)" |
|
768 by (insert order [of a n p], auto) |
|
769 |
|
770 lemma order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p & |
|
771 ~(([-a, 1] %^ (Suc n)) divides p)) |
|
772 ==> (n = order a p)" |
|
773 by (blast intro: order_unique) |
|
774 |
|
775 lemma order_poly: "poly p = poly q ==> order a p = order a q" |
|
776 by (auto simp add: fun_eq divides_def poly_mult order_def) |
|
777 |
|
778 lemma pexp_one: "p %^ (Suc 0) = p" |
|
779 apply (induct "p") |
|
780 apply (auto simp add: numeral_1_eq_1) |
|
781 done |
|
782 declare pexp_one [simp] |
|
783 |
|
784 lemma lemma_order_root [rule_format]: |
|
785 "\<forall>p a. n > 0 & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p |
|
786 --> poly p a = 0" |
|
787 apply (induct "n", blast) |
|
788 apply (auto simp add: divides_def poly_mult simp del: pmult_Cons) |
|
789 done |
|
790 |
|
791 lemma order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)" |
|
792 apply (case_tac "poly p = poly []", auto) |
|
793 apply (simp add: poly_linear_divides del: pmult_Cons, safe) |
|
794 apply (drule_tac [!] a = a in order2) |
|
795 apply (rule ccontr) |
|
796 apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast) |
|
797 apply (blast intro: lemma_order_root) |
|
798 done |
|
799 |
|
800 lemma order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)" |
|
801 apply (case_tac "poly p = poly []", auto) |
|
802 apply (simp add: divides_def fun_eq poly_mult) |
|
803 apply (rule_tac x = "[]" in exI) |
|
804 apply (auto dest!: order2 [where a=a] |
|
805 intro: poly_exp_divides simp del: pexp_Suc) |
|
806 done |
|
807 |
|
808 lemma order_decomp: |
|
809 "poly p \<noteq> poly [] |
|
810 ==> \<exists>q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) & |
|
811 ~([-a, 1] divides q)" |
|
812 apply (unfold divides_def) |
|
813 apply (drule order2 [where a = a]) |
|
814 apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe) |
|
815 apply (rule_tac x = q in exI, safe) |
|
816 apply (drule_tac x = qa in spec) |
|
817 apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons) |
|
818 done |
|
819 |
|
820 text{*Important composition properties of orders.*} |
|
821 |
|
822 lemma order_mult: "poly (p *** q) \<noteq> poly [] |
|
823 ==> order a (p *** q) = order a p + order a q" |
|
824 apply (cut_tac a = a and p = "p***q" and n = "order a p + order a q" in order) |
|
825 apply (auto simp add: poly_entire simp del: pmult_Cons) |
|
826 apply (drule_tac a = a in order2)+ |
|
827 apply safe |
|
828 apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe) |
|
829 apply (rule_tac x = "qa *** qaa" in exI) |
|
830 apply (simp add: poly_mult mult_ac del: pmult_Cons) |
|
831 apply (drule_tac a = a in order_decomp)+ |
|
832 apply safe |
|
833 apply (subgoal_tac "[-a,1] divides (qa *** qaa) ") |
|
834 apply (simp add: poly_primes del: pmult_Cons) |
|
835 apply (auto simp add: divides_def simp del: pmult_Cons) |
|
836 apply (rule_tac x = qb in exI) |
|
837 apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))") |
|
838 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
|
839 apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) = poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ") |
|
840 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
|
841 apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons) |
|
842 done |
|
843 |
|
844 (* FIXME: too too long! *) |
|
845 lemma lemma_order_pderiv [rule_format]: |
|
846 "\<forall>p q a. n > 0 & |
|
847 poly (pderiv p) \<noteq> poly [] & |
|
848 poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q |
|
849 --> n = Suc (order a (pderiv p))" |
|
850 apply (induct "n", safe) |
|
851 apply (rule order_unique_lemma, rule conjI, assumption) |
|
852 apply (subgoal_tac "\<forall>r. r divides (pderiv p) = r divides (pderiv ([-a, 1] %^ Suc n *** q))") |
|
853 apply (drule_tac [2] poly_pderiv_welldef) |
|
854 prefer 2 apply (simp add: divides_def del: pmult_Cons pexp_Suc) |
|
855 apply (simp del: pmult_Cons pexp_Suc) |
|
856 apply (rule conjI) |
|
857 apply (simp add: divides_def fun_eq del: pmult_Cons pexp_Suc) |
|
858 apply (rule_tac x = "[-a, 1] *** (pderiv q) +++ real (Suc n) %* q" in exI) |
|
859 apply (simp add: poly_pderiv_mult poly_pderiv_exp_prime poly_add poly_mult poly_cmult right_distrib mult_ac del: pmult_Cons pexp_Suc) |
|
860 apply (simp add: poly_mult right_distrib left_distrib mult_ac del: pmult_Cons) |
|
861 apply (erule_tac V = "\<forall>r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q)" in thin_rl) |
|
862 apply (unfold divides_def) |
|
863 apply (simp (no_asm) add: poly_pderiv_mult poly_pderiv_exp_prime fun_eq poly_add poly_mult del: pmult_Cons pexp_Suc) |
|
864 apply (rule contrapos_np, assumption) |
|
865 apply (rotate_tac 3, erule contrapos_np) |
|
866 apply (simp del: pmult_Cons pexp_Suc, safe) |
|
867 apply (rule_tac x = "inverse (real (Suc n)) %* (qa +++ -- (pderiv q))" in exI) |
|
868 apply (subgoal_tac "poly ([-a, 1] %^ n *** q) = poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* (qa +++ -- (pderiv q))))) ") |
|
869 apply (drule poly_mult_left_cancel [THEN iffD1], simp) |
|
870 apply (simp add: fun_eq poly_mult poly_add poly_cmult poly_minus del: pmult_Cons mult_cancel_left, safe) |
|
871 apply (rule_tac c1 = "real (Suc n)" in real_mult_left_cancel [THEN iffD1]) |
|
872 apply (simp (no_asm)) |
|
873 apply (subgoal_tac "real (Suc n) * (poly ([- a, 1] %^ n) xa * poly q xa) = |
|
874 (poly qa xa + - poly (pderiv q) xa) * |
|
875 (poly ([- a, 1] %^ n) xa * |
|
876 ((- a + xa) * (inverse (real (Suc n)) * real (Suc n))))") |
|
877 apply (simp only: mult_ac) |
|
878 apply (rotate_tac 2) |
|
879 apply (drule_tac x = xa in spec) |
|
880 apply (simp add: left_distrib mult_ac del: pmult_Cons) |
|
881 done |
|
882 |
|
883 lemma order_pderiv: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |] |
|
884 ==> (order a p = Suc (order a (pderiv p)))" |
|
885 apply (case_tac "poly p = poly []") |
|
886 apply (auto dest: pderiv_zero) |
|
887 apply (drule_tac a = a and p = p in order_decomp) |
|
888 apply (metis lemma_order_pderiv length_0_conv length_greater_0_conv) |
|
889 done |
|
890 |
|
891 text{*Now justify the standard squarefree decomposition, i.e. f / gcd(f,f'). *) |
|
892 (* `a la Harrison*} |
|
893 |
|
894 lemma poly_squarefree_decomp_order: "[| poly (pderiv p) \<noteq> poly []; |
|
895 poly p = poly (q *** d); |
|
896 poly (pderiv p) = poly (e *** d); |
|
897 poly d = poly (r *** p +++ s *** pderiv p) |
|
898 |] ==> order a q = (if order a p = 0 then 0 else 1)" |
|
899 apply (subgoal_tac "order a p = order a q + order a d") |
|
900 apply (rule_tac [2] s = "order a (q *** d)" in trans) |
|
901 prefer 2 apply (blast intro: order_poly) |
|
902 apply (rule_tac [2] order_mult) |
|
903 prefer 2 apply force |
|
904 apply (case_tac "order a p = 0", simp) |
|
905 apply (subgoal_tac "order a (pderiv p) = order a e + order a d") |
|
906 apply (rule_tac [2] s = "order a (e *** d)" in trans) |
|
907 prefer 2 apply (blast intro: order_poly) |
|
908 apply (rule_tac [2] order_mult) |
|
909 prefer 2 apply force |
|
910 apply (case_tac "poly p = poly []") |
|
911 apply (drule_tac p = p in pderiv_zero, simp) |
|
912 apply (drule order_pderiv, assumption) |
|
913 apply (subgoal_tac "order a (pderiv p) \<le> order a d") |
|
914 apply (subgoal_tac [2] " ([-a, 1] %^ (order a (pderiv p))) divides d") |
|
915 prefer 2 apply (simp add: poly_entire order_divides) |
|
916 apply (subgoal_tac [2] " ([-a, 1] %^ (order a (pderiv p))) divides p & ([-a, 1] %^ (order a (pderiv p))) divides (pderiv p) ") |
|
917 prefer 3 apply (simp add: order_divides) |
|
918 prefer 2 apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe) |
|
919 apply (rule_tac x = "r *** qa +++ s *** qaa" in exI) |
|
920 apply (simp add: fun_eq poly_add poly_mult left_distrib right_distrib mult_ac del: pexp_Suc pmult_Cons, auto) |
|
921 done |
|
922 |
|
923 |
|
924 lemma poly_squarefree_decomp_order2: "[| poly (pderiv p) \<noteq> poly []; |
|
925 poly p = poly (q *** d); |
|
926 poly (pderiv p) = poly (e *** d); |
|
927 poly d = poly (r *** p +++ s *** pderiv p) |
|
928 |] ==> \<forall>a. order a q = (if order a p = 0 then 0 else 1)" |
|
929 apply (blast intro: poly_squarefree_decomp_order) |
|
930 done |
|
931 |
|
932 lemma order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)" |
|
933 by (rule order_root [THEN ssubst], auto) |
|
934 |
|
935 lemma order_pderiv2: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |] |
|
936 ==> (order a (pderiv p) = n) = (order a p = Suc n)" |
|
937 by (metis Suc_Suc_eq order_pderiv) |
|
938 |
|
939 lemma rsquarefree_roots: |
|
940 "rsquarefree p = (\<forall>a. ~(poly p a = 0 & poly (pderiv p) a = 0))" |
|
941 apply (simp add: rsquarefree_def) |
|
942 apply (case_tac "poly p = poly []", simp, simp) |
|
943 apply (case_tac "poly (pderiv p) = poly []") |
|
944 apply simp |
|
945 apply (drule pderiv_iszero, clarify) |
|
946 apply (subgoal_tac "\<forall>a. order a p = order a [h]") |
|
947 apply (simp add: fun_eq) |
|
948 apply (rule allI) |
|
949 apply (cut_tac p = "[h]" and a = a in order_root) |
|
950 apply (simp add: fun_eq) |
|
951 apply (blast intro: order_poly) |
|
952 apply (metis One_nat_def order_pderiv2 order_root rsquarefree_def) |
|
953 done |
|
954 |
|
955 lemma pmult_one: "[1] *** p = p" |
|
956 by auto |
|
957 declare pmult_one [simp] |
|
958 |
|
959 lemma poly_Nil_zero: "poly [] = poly [0]" |
|
960 by (simp add: fun_eq) |
|
961 |
|
962 lemma rsquarefree_decomp: |
|
963 "[| rsquarefree p; poly p a = 0 |] |
|
964 ==> \<exists>q. (poly p = poly ([-a, 1] *** q)) & poly q a \<noteq> 0" |
|
965 apply (simp add: rsquarefree_def, safe) |
|
966 apply (frule_tac a = a in order_decomp) |
|
967 apply (drule_tac x = a in spec) |
|
968 apply (drule_tac a = a in order_root2 [symmetric]) |
|
969 apply (auto simp del: pmult_Cons) |
|
970 apply (rule_tac x = q in exI, safe) |
|
971 apply (simp add: poly_mult fun_eq) |
|
972 apply (drule_tac p1 = q in poly_linear_divides [THEN iffD1]) |
|
973 apply (simp add: divides_def del: pmult_Cons, safe) |
|
974 apply (drule_tac x = "[]" in spec) |
|
975 apply (auto simp add: fun_eq) |
|
976 done |
|
977 |
|
978 lemma poly_squarefree_decomp: "[| poly (pderiv p) \<noteq> poly []; |
|
979 poly p = poly (q *** d); |
|
980 poly (pderiv p) = poly (e *** d); |
|
981 poly d = poly (r *** p +++ s *** pderiv p) |
|
982 |] ==> rsquarefree q & (\<forall>a. (poly q a = 0) = (poly p a = 0))" |
|
983 apply (frule poly_squarefree_decomp_order2, assumption+) |
|
984 apply (case_tac "poly p = poly []") |
|
985 apply (blast dest: pderiv_zero) |
|
986 apply (simp (no_asm) add: rsquarefree_def order_root del: pmult_Cons) |
|
987 apply (simp add: poly_entire del: pmult_Cons) |
|
988 done |
|
989 |
|
990 |
|
991 text{*Normalization of a polynomial.*} |
|
992 |
|
993 lemma poly_normalize: "poly (pnormalize p) = poly p" |
|
994 apply (induct "p") |
|
995 apply (auto simp add: fun_eq) |
|
996 done |
|
997 declare poly_normalize [simp] |
|
998 |
|
999 |
|
1000 text{*The degree of a polynomial.*} |
|
1001 |
|
1002 lemma lemma_degree_zero: |
|
1003 "list_all (%c. c = 0) p \<longleftrightarrow> pnormalize p = []" |
|
1004 by (induct "p", auto) |
|
1005 |
|
1006 lemma degree_zero: "(poly p = poly []) \<Longrightarrow> (degree p = 0)" |
|
1007 apply (simp add: degree_def) |
|
1008 apply (case_tac "pnormalize p = []") |
|
1009 apply (auto simp add: poly_zero lemma_degree_zero ) |
|
1010 done |
|
1011 |
|
1012 lemma pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0" by simp |
|
1013 lemma pnormalize_pair: "y \<noteq> 0 \<longleftrightarrow> (pnormalize [x, y] = [x, y])" by simp |
|
1014 lemma pnormal_cons: "pnormal p \<Longrightarrow> pnormal (c#p)" |
|
1015 unfolding pnormal_def by simp |
|
1016 lemma pnormal_tail: "p\<noteq>[] \<Longrightarrow> pnormal (c#p) \<Longrightarrow> pnormal p" |
|
1017 unfolding pnormal_def |
|
1018 apply (cases "pnormalize p = []", auto) |
|
1019 by (cases "c = 0", auto) |
|
1020 lemma pnormal_last_nonzero: "pnormal p ==> last p \<noteq> 0" |
|
1021 apply (induct p, auto simp add: pnormal_def) |
|
1022 apply (case_tac "pnormalize p = []", auto) |
|
1023 by (case_tac "a=0", auto) |
|
1024 lemma pnormal_length: "pnormal p \<Longrightarrow> 0 < length p" |
|
1025 unfolding pnormal_def length_greater_0_conv by blast |
|
1026 lemma pnormal_last_length: "\<lbrakk>0 < length p ; last p \<noteq> 0\<rbrakk> \<Longrightarrow> pnormal p" |
|
1027 apply (induct p, auto) |
|
1028 apply (case_tac "p = []", auto) |
|
1029 apply (simp add: pnormal_def) |
|
1030 by (rule pnormal_cons, auto) |
|
1031 lemma pnormal_id: "pnormal p \<longleftrightarrow> (0 < length p \<and> last p \<noteq> 0)" |
|
1032 using pnormal_last_length pnormal_length pnormal_last_nonzero by blast |
|
1033 |
|
1034 text{*Tidier versions of finiteness of roots.*} |
|
1035 |
|
1036 lemma poly_roots_finite_set: "poly p \<noteq> poly [] ==> finite {x. poly p x = 0}" |
|
1037 apply (auto simp add: poly_roots_finite) |
|
1038 apply (rule_tac B = "{x::real. \<exists>n. (n::nat) < N & (x = j n) }" in finite_subset) |
|
1039 apply (induct_tac [2] "N", auto) |
|
1040 apply (subgoal_tac "{x::real. \<exists>na. na < Suc n & (x = j na) } = { (j n) } Un {x. \<exists>na. na < n & (x = j na) }") |
|
1041 apply (auto simp add: less_Suc_eq) |
|
1042 done |
|
1043 |
|
1044 text{*bound for polynomial.*} |
|
1045 |
|
1046 lemma poly_mono: "abs(x) \<le> k ==> abs(poly p x) \<le> poly (map abs p) k" |
|
1047 apply (induct "p", auto) |
|
1048 apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans) |
|
1049 apply (rule abs_triangle_ineq) |
|
1050 apply (auto intro!: mult_mono simp add: abs_mult) |
|
1051 done |
|
1052 |
|
1053 lemma poly_Sing: "poly [c] x = c" by simp |
|
1054 end |
|