77 definition (in ring_1) order :: "'a => 'a list => nat" where |
77 definition (in ring_1) order :: "'a => 'a list => nat" where |
78 "order a p = (SOME n. ([-a, 1] %^ n) divides p & |
78 "order a p = (SOME n. ([-a, 1] %^ n) divides p & |
79 ~ (([-a, 1] %^ (Suc n)) divides p))" |
79 ~ (([-a, 1] %^ (Suc n)) divides p))" |
80 |
80 |
81 --{*degree of a polynomial*} |
81 --{*degree of a polynomial*} |
82 definition (in semiring_0) degree :: "'a list => nat" where |
82 definition (in semiring_0) degree :: "'a list => nat" where |
83 "degree p = length (pnormalize p) - 1" |
83 "degree p = length (pnormalize p) - 1" |
84 |
84 |
85 --{*squarefree polynomials --- NB with respect to real roots only.*} |
85 --{*squarefree polynomials --- NB with respect to real roots only.*} |
86 definition (in ring_1) |
86 definition (in ring_1) |
87 rsquarefree :: "'a list => bool" where |
87 rsquarefree :: "'a list => bool" where |
138 |
138 |
139 lemma (in semiring_0) poly_add: "poly (p1 +++ p2) x = poly p1 x + poly p2 x" |
139 lemma (in semiring_0) poly_add: "poly (p1 +++ p2) x = poly p1 x + poly p2 x" |
140 proof(induct p1 arbitrary: p2) |
140 proof(induct p1 arbitrary: p2) |
141 case Nil thus ?case by simp |
141 case Nil thus ?case by simp |
142 next |
142 next |
143 case (Cons a as p2) thus ?case |
143 case (Cons a as p2) thus ?case |
144 by (cases p2, simp_all add: add_ac right_distrib) |
144 by (cases p2, simp_all add: add_ac right_distrib) |
145 qed |
145 qed |
146 |
146 |
147 lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x" |
147 lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x" |
148 apply (induct "p") |
148 apply (induct "p") |
149 apply (case_tac [2] "x=zero") |
149 apply (case_tac [2] "x=zero") |
150 apply (auto simp add: right_distrib mult_ac) |
150 apply (auto simp add: right_distrib mult_ac) |
151 done |
151 done |
152 |
152 |
153 lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c*poly p x" |
153 lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c*poly p x" |
211 case Nil |
211 case Nil |
212 {fix h have "[h] = [h] +++ [- a, 1] *** []" by simp} |
212 {fix h have "[h] = [h] +++ [- a, 1] *** []" by simp} |
213 thus ?case by blast |
213 thus ?case by blast |
214 next |
214 next |
215 case (Cons x xs) |
215 case (Cons x xs) |
216 {fix h |
216 {fix h |
217 from Cons.hyps[rule_format, of x] |
217 from Cons.hyps[rule_format, of x] |
218 obtain q r where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast |
218 obtain q r where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast |
219 have "h#x#xs = [a*r + h] +++ [-a, 1] *** (r#q)" |
219 have "h#x#xs = [a*r + h] +++ [-a, 1] *** (r#q)" |
220 using qr by(cases q, simp_all add: algebra_simps diff_def[symmetric] |
220 using qr by(cases q, simp_all add: algebra_simps diff_def[symmetric] |
221 minus_mult_left[symmetric] right_minus) |
221 minus_mult_left[symmetric] right_minus) |
222 hence "\<exists>q r. h#x#xs = [r] +++ [-a, 1] *** q" by blast} |
222 hence "\<exists>q r. h#x#xs = [r] +++ [-a, 1] *** q" by blast} |
223 thus ?case by blast |
223 thus ?case by blast |
224 qed |
224 qed |
225 |
225 |
230 lemma (in comm_ring_1) poly_linear_divides: "(poly p a = 0) = ((p = []) | (\<exists>q. p = [-a, 1] *** q))" |
230 lemma (in comm_ring_1) poly_linear_divides: "(poly p a = 0) = ((p = []) | (\<exists>q. p = [-a, 1] *** q))" |
231 proof- |
231 proof- |
232 {assume p: "p = []" hence ?thesis by simp} |
232 {assume p: "p = []" hence ?thesis by simp} |
233 moreover |
233 moreover |
234 {fix x xs assume p: "p = x#xs" |
234 {fix x xs assume p: "p = x#xs" |
235 {fix q assume "p = [-a, 1] *** q" hence "poly p a = 0" |
235 {fix q assume "p = [-a, 1] *** q" hence "poly p a = 0" |
236 by (simp add: poly_add poly_cmult minus_mult_left[symmetric])} |
236 by (simp add: poly_add poly_cmult minus_mult_left[symmetric])} |
237 moreover |
237 moreover |
238 {assume p0: "poly p a = 0" |
238 {assume p0: "poly p a = 0" |
239 from poly_linear_rem[of x xs a] obtain q r |
239 from poly_linear_rem[of x xs a] obtain q r |
240 where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast |
240 where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast |
241 have "r = 0" using p0 by (simp only: p qr poly_mult poly_add) simp |
241 have "r = 0" using p0 by (simp only: p qr poly_mult poly_add) simp |
242 hence "\<exists>q. p = [- a, 1] *** q" using p qr apply - apply (rule exI[where x=q])apply auto apply (cases q) apply auto done} |
242 hence "\<exists>q. p = [- a, 1] *** q" using p qr apply - apply (rule exI[where x=q])apply auto apply (cases q) apply auto done} |
243 ultimately have ?thesis using p by blast} |
243 ultimately have ?thesis using p by blast} |
244 ultimately show ?thesis by (cases p, auto) |
244 ultimately show ?thesis by (cases p, auto) |
264 done |
264 done |
265 |
265 |
266 lemma (in semiring_0) poly_root_mult_length[simp]: "length([a,b] *** p) = Suc (length p)" |
266 lemma (in semiring_0) poly_root_mult_length[simp]: "length([a,b] *** p) = Suc (length p)" |
267 by (simp add: poly_add_length) |
267 by (simp add: poly_add_length) |
268 |
268 |
269 lemma (in idom) poly_mult_not_eq_poly_Nil[simp]: |
269 lemma (in idom) poly_mult_not_eq_poly_Nil[simp]: |
270 "poly (p *** q) x \<noteq> poly [] x \<longleftrightarrow> poly p x \<noteq> poly [] x \<and> poly q x \<noteq> poly [] x" |
270 "poly (p *** q) x \<noteq> poly [] x \<longleftrightarrow> poly p x \<noteq> poly [] x \<and> poly q x \<noteq> poly [] x" |
271 by (auto simp add: poly_mult) |
271 by (auto simp add: poly_mult) |
272 |
272 |
273 lemma (in idom) poly_mult_eq_zero_disj: "poly (p *** q) x = 0 \<longleftrightarrow> poly p x = 0 \<or> poly q x = 0" |
273 lemma (in idom) poly_mult_eq_zero_disj: "poly (p *** q) x = 0 \<longleftrightarrow> poly p x = 0 \<or> poly q x = 0" |
274 by (auto simp add: poly_mult) |
274 by (auto simp add: poly_mult) |
278 lemma (in semiring_0) poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)" |
278 lemma (in semiring_0) poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)" |
279 by (induct "p", auto) |
279 by (induct "p", auto) |
280 |
280 |
281 text{*A nontrivial polynomial of degree n has no more than n roots*} |
281 text{*A nontrivial polynomial of degree n has no more than n roots*} |
282 lemma (in idom) poly_roots_index_lemma: |
282 lemma (in idom) poly_roots_index_lemma: |
283 assumes p: "poly p x \<noteq> poly [] x" and n: "length p = n" |
283 assumes p: "poly p x \<noteq> poly [] x" and n: "length p = n" |
284 shows "\<exists>i. \<forall>x. poly p x = 0 \<longrightarrow> (\<exists>m\<le>n. x = i m)" |
284 shows "\<exists>i. \<forall>x. poly p x = 0 \<longrightarrow> (\<exists>m\<le>n. x = i m)" |
285 using p n |
285 using p n |
286 proof(induct n arbitrary: p x) |
286 proof(induct n arbitrary: p x) |
287 case 0 thus ?case by simp |
287 case 0 thus ?case by simp |
288 next |
288 next |
289 case (Suc n p x) |
289 case (Suc n p x) |
290 {assume C: "\<And>i. \<exists>x. poly p x = 0 \<and> (\<forall>m\<le>Suc n. x \<noteq> i m)" |
290 {assume C: "\<And>i. \<exists>x. poly p x = 0 \<and> (\<forall>m\<le>Suc n. x \<noteq> i m)" |
291 from Suc.prems have p0: "poly p x \<noteq> 0" "p\<noteq> []" by auto |
291 from Suc.prems have p0: "poly p x \<noteq> 0" "p\<noteq> []" by auto |
292 from p0(1)[unfolded poly_linear_divides[of p x]] |
292 from p0(1)[unfolded poly_linear_divides[of p x]] |
293 have "\<forall>q. p \<noteq> [- x, 1] *** q" by blast |
293 have "\<forall>q. p \<noteq> [- x, 1] *** q" by blast |
294 from C obtain a where a: "poly p a = 0" by blast |
294 from C obtain a where a: "poly p a = 0" by blast |
295 from a[unfolded poly_linear_divides[of p a]] p0(2) |
295 from a[unfolded poly_linear_divides[of p a]] p0(2) |
296 obtain q where q: "p = [-a, 1] *** q" by blast |
296 obtain q where q: "p = [-a, 1] *** q" by blast |
297 have lg: "length q = n" using q Suc.prems(2) by simp |
297 have lg: "length q = n" using q Suc.prems(2) by simp |
298 from q p0 have qx: "poly q x \<noteq> poly [] x" |
298 from q p0 have qx: "poly q x \<noteq> poly [] x" |
299 by (auto simp add: poly_mult poly_add poly_cmult) |
299 by (auto simp add: poly_mult poly_add poly_cmult) |
300 from Suc.hyps[OF qx lg] obtain i where |
300 from Suc.hyps[OF qx lg] obtain i where |
301 i: "\<forall>x. poly q x = 0 \<longrightarrow> (\<exists>m\<le>n. x = i m)" by blast |
301 i: "\<forall>x. poly q x = 0 \<longrightarrow> (\<exists>m\<le>n. x = i m)" by blast |
302 let ?i = "\<lambda>m. if m = Suc n then a else i m" |
302 let ?i = "\<lambda>m. if m = Suc n then a else i m" |
303 from C[of ?i] obtain y where y: "poly p y = 0" "\<forall>m\<le> Suc n. y \<noteq> ?i m" |
303 from C[of ?i] obtain y where y: "poly p y = 0" "\<forall>m\<le> Suc n. y \<noteq> ?i m" |
304 by blast |
304 by blast |
305 from y have "y = a \<or> poly q y = 0" |
305 from y have "y = a \<or> poly q y = 0" |
306 by (simp only: q poly_mult_eq_zero_disj poly_add) (simp add: algebra_simps) |
306 by (simp only: q poly_mult_eq_zero_disj poly_add) (simp add: algebra_simps) |
307 with i[rule_format, of y] y(1) y(2) have False apply auto |
307 with i[rule_format, of y] y(1) y(2) have False apply auto |
308 apply (erule_tac x="m" in allE) |
308 apply (erule_tac x="m" in allE) |
309 apply auto |
309 apply auto |
310 done} |
310 done} |
311 thus ?case by blast |
311 thus ?case by blast |
312 qed |
312 qed |
342 apply (rule_tac x="map (\<lambda>n. i n) [0 ..< Suc (length p)]" in exI) |
342 apply (rule_tac x="map (\<lambda>n. i n) [0 ..< Suc (length p)]" in exI) |
343 apply (auto simp add: image_iff) |
343 apply (auto simp add: image_iff) |
344 apply (erule_tac x="x" in allE, clarsimp) |
344 apply (erule_tac x="x" in allE, clarsimp) |
345 by (case_tac "n=length p", auto simp add: order_le_less) |
345 by (case_tac "n=length p", auto simp add: order_le_less) |
346 |
346 |
347 lemma (in ring_char_0) UNIV_ring_char_0_infinte: |
347 lemma (in ring_char_0) UNIV_ring_char_0_infinte: |
348 "\<not> (finite (UNIV:: 'a set))" |
348 "\<not> (finite (UNIV:: 'a set))" |
349 proof |
349 proof |
350 assume F: "finite (UNIV :: 'a set)" |
350 assume F: "finite (UNIV :: 'a set)" |
351 have "finite (UNIV :: nat set)" |
351 have "finite (UNIV :: nat set)" |
352 proof (rule finite_imageD) |
352 proof (rule finite_imageD) |
353 have "of_nat ` UNIV \<subseteq> UNIV" by simp |
353 have "of_nat ` UNIV \<subseteq> UNIV" by simp |
368 apply (rule ccontr) |
368 apply (rule ccontr) |
369 apply (clarify dest!: poly_roots_finite_lemma2) |
369 apply (clarify dest!: poly_roots_finite_lemma2) |
370 using finite_subset |
370 using finite_subset |
371 proof- |
371 proof- |
372 fix x i |
372 fix x i |
373 assume F: "\<not> finite {x. poly p x = (0\<Colon>'a)}" |
373 assume F: "\<not> finite {x. poly p x = (0\<Colon>'a)}" |
374 and P: "\<forall>x. poly p x = (0\<Colon>'a) \<longrightarrow> x \<in> set i" |
374 and P: "\<forall>x. poly p x = (0\<Colon>'a) \<longrightarrow> x \<in> set i" |
375 let ?M= "{x. poly p x = (0\<Colon>'a)}" |
375 let ?M= "{x. poly p x = (0\<Colon>'a)}" |
376 from P have "?M \<subseteq> set i" by auto |
376 from P have "?M \<subseteq> set i" by auto |
377 with finite_subset F show False by auto |
377 with finite_subset F show False by auto |
378 qed |
378 qed |
379 next |
379 next |
380 assume F: "finite {x. poly p x = (0\<Colon>'a)}" |
380 assume F: "finite {x. poly p x = (0\<Colon>'a)}" |
381 show "poly p \<noteq> poly []" using F UNIV_ring_char_0_infinte by auto |
381 show "poly p \<noteq> poly []" using F UNIV_ring_char_0_infinte by auto |
382 qed |
382 qed |
383 |
383 |
384 text{*Entirety and Cancellation for polynomials*} |
384 text{*Entirety and Cancellation for polynomials*} |
385 |
385 |
386 lemma (in idom_char_0) poly_entire_lemma2: |
386 lemma (in idom_char_0) poly_entire_lemma2: |
387 assumes p0: "poly p \<noteq> poly []" and q0: "poly q \<noteq> poly []" |
387 assumes p0: "poly p \<noteq> poly []" and q0: "poly q \<noteq> poly []" |
388 shows "poly (p***q) \<noteq> poly []" |
388 shows "poly (p***q) \<noteq> poly []" |
389 proof- |
389 proof- |
390 let ?S = "\<lambda>p. {x. poly p x = 0}" |
390 let ?S = "\<lambda>p. {x. poly p x = 0}" |
391 have "?S (p *** q) = ?S p \<union> ?S q" by (auto simp add: poly_mult) |
391 have "?S (p *** q) = ?S p \<union> ?S q" by (auto simp add: poly_mult) |
392 with p0 q0 show ?thesis unfolding poly_roots_finite by auto |
392 with p0 q0 show ?thesis unfolding poly_roots_finite by auto |
393 qed |
393 qed |
394 |
394 |
395 lemma (in idom_char_0) poly_entire: |
395 lemma (in idom_char_0) poly_entire: |
396 "poly (p *** q) = poly [] \<longleftrightarrow> poly p = poly [] \<or> poly q = poly []" |
396 "poly (p *** q) = poly [] \<longleftrightarrow> poly p = poly [] \<or> poly q = poly []" |
397 using poly_entire_lemma2[of p q] |
397 using poly_entire_lemma2[of p q] |
398 by (auto simp add: expand_fun_eq poly_mult) |
398 by (auto simp add: expand_fun_eq poly_mult) |
399 |
399 |
400 lemma (in idom_char_0) poly_entire_neg: "(poly (p *** q) \<noteq> poly []) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))" |
400 lemma (in idom_char_0) poly_entire_neg: "(poly (p *** q) \<noteq> poly []) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))" |
433 apply (rule_tac x = "minus one a" in exI) |
433 apply (rule_tac x = "minus one a" in exI) |
434 apply (unfold diff_minus) |
434 apply (unfold diff_minus) |
435 apply (subst add_commute) |
435 apply (subst add_commute) |
436 apply (subst add_assoc) |
436 apply (subst add_assoc) |
437 apply simp |
437 apply simp |
438 done |
438 done |
439 |
439 |
440 lemma (in recpower_idom) poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])" |
440 lemma (in recpower_idom) poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])" |
441 by auto |
441 by auto |
442 |
442 |
443 text{*A more constructive notion of polynomials being trivial*} |
443 text{*A more constructive notion of polynomials being trivial*} |
444 |
444 |
445 lemma (in idom_char_0) poly_zero_lemma': "poly (h # t) = poly [] ==> h = 0 & poly t = poly []" |
445 lemma (in idom_char_0) poly_zero_lemma': "poly (h # t) = poly [] ==> h = 0 & poly t = poly []" |
446 apply(simp add: fun_eq) |
446 apply(simp add: fun_eq) |
447 apply (case_tac "h = zero") |
447 apply (case_tac "h = zero") |
448 apply (drule_tac [2] x = zero in spec, auto) |
448 apply (drule_tac [2] x = zero in spec, auto) |
449 apply (cases "poly t = poly []", simp) |
449 apply (cases "poly t = poly []", simp) |
450 proof- |
450 proof- |
451 fix x |
451 fix x |
452 assume H: "\<forall>x. x = (0\<Colon>'a) \<or> poly t x = (0\<Colon>'a)" and pnz: "poly t \<noteq> poly []" |
452 assume H: "\<forall>x. x = (0\<Colon>'a) \<or> poly t x = (0\<Colon>'a)" and pnz: "poly t \<noteq> poly []" |
453 let ?S = "{x. poly t x = 0}" |
453 let ?S = "{x. poly t x = 0}" |
454 from H have "\<forall>x. x \<noteq>0 \<longrightarrow> poly t x = 0" by blast |
454 from H have "\<forall>x. x \<noteq>0 \<longrightarrow> poly t x = 0" by blast |
561 next |
561 next |
562 case (Suc n p) |
562 case (Suc n p) |
563 {assume p0: "poly p a = 0" |
563 {assume p0: "poly p a = 0" |
564 from Suc.prems have h: "length p = Suc n" "poly p \<noteq> poly []" by auto |
564 from Suc.prems have h: "length p = Suc n" "poly p \<noteq> poly []" by auto |
565 hence pN: "p \<noteq> []" by auto |
565 hence pN: "p \<noteq> []" by auto |
566 from p0[unfolded poly_linear_divides] pN obtain q where |
566 from p0[unfolded poly_linear_divides] pN obtain q where |
567 q: "p = [-a, 1] *** q" by blast |
567 q: "p = [-a, 1] *** q" by blast |
568 from q h p0 have qh: "length q = n" "poly q \<noteq> poly []" |
568 from q h p0 have qh: "length q = n" "poly q \<noteq> poly []" |
569 apply - |
569 apply - |
570 apply simp |
570 apply simp |
571 apply (simp only: fun_eq) |
571 apply (simp only: fun_eq) |
572 apply (rule ccontr) |
572 apply (rule ccontr) |
573 apply (simp add: fun_eq poly_add poly_cmult minus_mult_left[symmetric]) |
573 apply (simp add: fun_eq poly_add poly_cmult minus_mult_left[symmetric]) |
574 done |
574 done |
575 from Suc.hyps[OF qh] obtain m r where |
575 from Suc.hyps[OF qh] obtain m r where |
576 mr: "q = mulexp m [-a,1] r" "poly r a \<noteq> 0" by blast |
576 mr: "q = mulexp m [-a,1] r" "poly r a \<noteq> 0" by blast |
577 from mr q have "p = mulexp (Suc m) [-a,1] r \<and> poly r a \<noteq> 0" by simp |
577 from mr q have "p = mulexp (Suc m) [-a,1] r \<and> poly r a \<noteq> 0" by simp |
578 hence ?case by blast} |
578 hence ?case by blast} |
579 moreover |
579 moreover |
580 {assume p0: "poly p a \<noteq> 0" |
580 {assume p0: "poly p a \<noteq> 0" |
581 hence ?case using Suc.prems apply simp by (rule exI[where x="0::nat"], simp)} |
581 hence ?case using Suc.prems apply simp by (rule exI[where x="0::nat"], simp)} |
612 let ?mulexp = mulexp |
612 let ?mulexp = mulexp |
613 let ?pexp = pexp |
613 let ?pexp = pexp |
614 from lp p0 |
614 from lp p0 |
615 show ?thesis |
615 show ?thesis |
616 apply - |
616 apply - |
617 apply (drule poly_order_exists_lemma [where a=a], assumption, clarify) |
617 apply (drule poly_order_exists_lemma [where a=a], assumption, clarify) |
618 apply (rule_tac x = n in exI, safe) |
618 apply (rule_tac x = n in exI, safe) |
619 apply (unfold divides_def) |
619 apply (unfold divides_def) |
620 apply (rule_tac x = q in exI) |
620 apply (rule_tac x = q in exI) |
621 apply (induct_tac "n", simp) |
621 apply (induct_tac "n", simp) |
622 apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac) |
622 apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac) |
623 apply safe |
623 apply safe |
624 apply (subgoal_tac "?poly (?mulexp n [uminus a, one] q) \<noteq> ?poly (pmult (?pexp [uminus a, one] (Suc n)) qa)") |
624 apply (subgoal_tac "?poly (?mulexp n [uminus a, one] q) \<noteq> ?poly (pmult (?pexp [uminus a, one] (Suc n)) qa)") |
625 apply simp |
625 apply simp |
626 apply (induct_tac "n") |
626 apply (induct_tac "n") |
627 apply (simp del: pmult_Cons pexp_Suc) |
627 apply (simp del: pmult_Cons pexp_Suc) |
628 apply (erule_tac Q = "?poly q a = zero" in contrapos_np) |
628 apply (erule_tac Q = "?poly q a = zero" in contrapos_np) |
629 apply (simp add: poly_add poly_cmult minus_mult_left[symmetric]) |
629 apply (simp add: poly_add poly_cmult minus_mult_left[symmetric]) |
630 apply (rule pexp_Suc [THEN ssubst]) |
630 apply (rule pexp_Suc [THEN ssubst]) |
668 by (simp add: order del: pexp_Suc) |
668 by (simp add: order del: pexp_Suc) |
669 |
669 |
670 lemma (in recpower_idom_char_0) order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p; |
670 lemma (in recpower_idom_char_0) order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p; |
671 ~(([-a, 1] %^ (Suc n)) divides p) |
671 ~(([-a, 1] %^ (Suc n)) divides p) |
672 |] ==> (n = order a p)" |
672 |] ==> (n = order a p)" |
673 by (insert order [of a n p], auto) |
673 by (insert order [of a n p], auto) |
674 |
674 |
675 lemma (in recpower_idom_char_0) order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p & |
675 lemma (in recpower_idom_char_0) order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p & |
676 ~(([-a, 1] %^ (Suc n)) divides p)) |
676 ~(([-a, 1] %^ (Suc n)) divides p)) |
677 ==> (n = order a p)" |
677 ==> (n = order a p)" |
678 by (blast intro: order_unique) |
678 by (blast intro: order_unique) |
751 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))) ") |
751 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))) ") |
752 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
752 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
753 apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons) |
753 apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons) |
754 done |
754 done |
755 |
755 |
756 lemma (in recpower_idom_char_0) order_mult: |
756 lemma (in recpower_idom_char_0) order_mult: |
757 assumes pq0: "poly (p *** q) \<noteq> poly []" |
757 assumes pq0: "poly (p *** q) \<noteq> poly []" |
758 shows "order a (p *** q) = order a p + order a q" |
758 shows "order a (p *** q) = order a p + order a q" |
759 proof- |
759 proof- |
760 let ?order = order |
760 let ?order = order |
761 let ?divides = "op divides" |
761 let ?divides = "op divides" |
762 let ?poly = poly |
762 let ?poly = poly |
763 from pq0 |
763 from pq0 |
764 show ?thesis |
764 show ?thesis |
765 apply (cut_tac a = a and p = "pmult p q" and n = "?order a p + ?order a q" in order) |
765 apply (cut_tac a = a and p = "pmult p q" and n = "?order a p + ?order a q" in order) |
766 apply (auto simp add: poly_entire simp del: pmult_Cons) |
766 apply (auto simp add: poly_entire simp del: pmult_Cons) |
767 apply (drule_tac a = a in order2)+ |
767 apply (drule_tac a = a in order2)+ |
768 apply safe |
768 apply safe |
819 |
819 |
820 lemma (in semiring_0) lemma_degree_zero: |
820 lemma (in semiring_0) lemma_degree_zero: |
821 "list_all (%c. c = 0) p \<longleftrightarrow> pnormalize p = []" |
821 "list_all (%c. c = 0) p \<longleftrightarrow> pnormalize p = []" |
822 by (induct "p", auto) |
822 by (induct "p", auto) |
823 |
823 |
824 lemma (in idom_char_0) degree_zero: |
824 lemma (in idom_char_0) degree_zero: |
825 assumes pN: "poly p = poly []" shows"degree p = 0" |
825 assumes pN: "poly p = poly []" shows"degree p = 0" |
826 proof- |
826 proof- |
827 let ?pn = pnormalize |
827 let ?pn = pnormalize |
828 from pN |
828 from pN |
829 show ?thesis |
829 show ?thesis |
830 apply (simp add: degree_def) |
830 apply (simp add: degree_def) |
831 apply (case_tac "?pn p = []") |
831 apply (case_tac "?pn p = []") |
832 apply (auto simp add: poly_zero lemma_degree_zero ) |
832 apply (auto simp add: poly_zero lemma_degree_zero ) |
833 done |
833 done |
834 qed |
834 qed |
835 |
835 |
836 lemma (in semiring_0) pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0" by simp |
836 lemma (in semiring_0) pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0" by simp |
837 lemma (in semiring_0) pnormalize_pair: "y \<noteq> 0 \<longleftrightarrow> (pnormalize [x, y] = [x, y])" by simp |
837 lemma (in semiring_0) pnormalize_pair: "y \<noteq> 0 \<longleftrightarrow> (pnormalize [x, y] = [x, y])" by simp |
838 lemma (in semiring_0) pnormal_cons: "pnormal p \<Longrightarrow> pnormal (c#p)" |
838 lemma (in semiring_0) pnormal_cons: "pnormal p \<Longrightarrow> pnormal (c#p)" |
839 unfolding pnormal_def by simp |
839 unfolding pnormal_def by simp |
840 lemma (in semiring_0) pnormal_tail: "p\<noteq>[] \<Longrightarrow> pnormal (c#p) \<Longrightarrow> pnormal p" |
840 lemma (in semiring_0) pnormal_tail: "p\<noteq>[] \<Longrightarrow> pnormal (c#p) \<Longrightarrow> pnormal p" |
841 unfolding pnormal_def |
841 unfolding pnormal_def |
842 apply (cases "pnormalize p = []", auto) |
842 apply (cases "pnormalize p = []", auto) |
843 by (cases "c = 0", auto) |
843 by (cases "c = 0", auto) |
844 |
844 |
845 |
845 |
846 lemma (in semiring_0) pnormal_last_nonzero: "pnormal p ==> last p \<noteq> 0" |
846 lemma (in semiring_0) pnormal_last_nonzero: "pnormal p ==> last p \<noteq> 0" |
847 proof(induct p) |
847 proof(induct p) |
848 case Nil thus ?case by (simp add: pnormal_def) |
848 case Nil thus ?case by (simp add: pnormal_def) |
849 next |
849 next |
850 case (Cons a as) thus ?case |
850 case (Cons a as) thus ?case |
851 apply (simp add: pnormal_def) |
851 apply (simp add: pnormal_def) |
852 apply (cases "pnormalize as = []", simp_all) |
852 apply (cases "pnormalize as = []", simp_all) |
853 apply (cases "as = []", simp_all) |
853 apply (cases "as = []", simp_all) |
854 apply (cases "a=0", simp_all) |
854 apply (cases "a=0", simp_all) |
875 by (simp only: poly_minus poly_add algebra_simps) simp |
875 by (simp only: poly_minus poly_add algebra_simps) simp |
876 hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add:expand_fun_eq) |
876 hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add:expand_fun_eq) |
877 hence "c = d \<and> list_all (\<lambda>x. x=0) ((cs +++ -- ds))" |
877 hence "c = d \<and> list_all (\<lambda>x. x=0) ((cs +++ -- ds))" |
878 unfolding poly_zero by (simp add: poly_minus_def algebra_simps) |
878 unfolding poly_zero by (simp add: poly_minus_def algebra_simps) |
879 hence "c = d \<and> (\<forall>x. poly (cs +++ -- ds) x = 0)" |
879 hence "c = d \<and> (\<forall>x. poly (cs +++ -- ds) x = 0)" |
880 unfolding poly_zero[symmetric] by simp |
880 unfolding poly_zero[symmetric] by simp |
881 thus ?rhs by (simp add: poly_minus poly_add algebra_simps expand_fun_eq) |
881 thus ?rhs by (simp add: poly_minus poly_add algebra_simps expand_fun_eq) |
882 next |
882 next |
883 assume ?rhs then show ?lhs by(simp add:expand_fun_eq) |
883 assume ?rhs then show ?lhs by(simp add:expand_fun_eq) |
884 qed |
884 qed |
885 |
885 |
886 lemma (in idom_char_0) pnormalize_unique: "poly p = poly q \<Longrightarrow> pnormalize p = pnormalize q" |
886 lemma (in idom_char_0) pnormalize_unique: "poly p = poly q \<Longrightarrow> pnormalize p = pnormalize q" |
887 proof(induct q arbitrary: p) |
887 proof(induct q arbitrary: p) |
888 case Nil thus ?case by (simp only: poly_zero lemma_degree_zero) simp |
888 case Nil thus ?case by (simp only: poly_zero lemma_degree_zero) simp |
889 next |
889 next |
890 case (Cons c cs p) |
890 case (Cons c cs p) |
891 thus ?case |
891 thus ?case |
892 proof(induct p) |
892 proof(induct p) |
893 case Nil |
893 case Nil |
894 hence "poly [] = poly (c#cs)" by blast |
894 hence "poly [] = poly (c#cs)" by blast |
895 then have "poly (c#cs) = poly [] " by simp |
895 then have "poly (c#cs) = poly [] " by simp |
896 thus ?case by (simp only: poly_zero lemma_degree_zero) simp |
896 thus ?case by (simp only: poly_zero lemma_degree_zero) simp |
897 next |
897 next |
898 case (Cons d ds) |
898 case (Cons d ds) |
899 hence eq: "poly (d # ds) = poly (c # cs)" by blast |
899 hence eq: "poly (d # ds) = poly (c # cs)" by blast |
900 hence eq': "\<And>x. poly (d # ds) x = poly (c # cs) x" by simp |
900 hence eq': "\<And>x. poly (d # ds) x = poly (c # cs) x" by simp |
911 shows "degree p = degree q" |
911 shows "degree p = degree q" |
912 using pnormalize_unique[OF pq] unfolding degree_def by simp |
912 using pnormalize_unique[OF pq] unfolding degree_def by simp |
913 |
913 |
914 lemma (in semiring_0) pnormalize_length: "length (pnormalize p) \<le> length p" by (induct p, auto) |
914 lemma (in semiring_0) pnormalize_length: "length (pnormalize p) \<le> length p" by (induct p, auto) |
915 |
915 |
916 lemma (in semiring_0) last_linear_mul_lemma: |
916 lemma (in semiring_0) last_linear_mul_lemma: |
917 "last ((a %* p) +++ (x#(b %* p))) = (if p=[] then x else b*last p)" |
917 "last ((a %* p) +++ (x#(b %* p))) = (if p=[] then x else b*last p)" |
918 |
918 |
919 apply (induct p arbitrary: a x b, auto) |
919 apply (induct p arbitrary: a x b, auto) |
920 apply (subgoal_tac "padd (cmult aa p) (times b a # cmult b p) \<noteq> []", simp) |
920 apply (subgoal_tac "padd (cmult aa p) (times b a # cmult b p) \<noteq> []", simp) |
921 apply (induct_tac p, auto) |
921 apply (induct_tac p, auto) |
946 lemma (in idom_char_0) linear_mul_degree: assumes p: "poly p \<noteq> poly []" |
946 lemma (in idom_char_0) linear_mul_degree: assumes p: "poly p \<noteq> poly []" |
947 shows "degree ([a,1] *** p) = degree p + 1" |
947 shows "degree ([a,1] *** p) = degree p + 1" |
948 proof- |
948 proof- |
949 from p have pnz: "pnormalize p \<noteq> []" |
949 from p have pnz: "pnormalize p \<noteq> []" |
950 unfolding poly_zero lemma_degree_zero . |
950 unfolding poly_zero lemma_degree_zero . |
951 |
951 |
952 from last_linear_mul[OF pnz, of a] last_pnormalize[OF pnz] |
952 from last_linear_mul[OF pnz, of a] last_pnormalize[OF pnz] |
953 have l0: "last ([a, 1] *** pnormalize p) \<noteq> 0" by simp |
953 have l0: "last ([a, 1] *** pnormalize p) \<noteq> 0" by simp |
954 from last_pnormalize[OF pnz] last_linear_mul[OF pnz, of a] |
954 from last_pnormalize[OF pnz] last_linear_mul[OF pnz, of a] |
955 pnormal_degree[OF l0] pnormal_degree[OF last_pnormalize[OF pnz]] pnz |
955 pnormal_degree[OF l0] pnormal_degree[OF last_pnormalize[OF pnz]] pnz |
956 |
956 |
957 |
957 |
958 have th: "degree ([a,1] *** pnormalize p) = degree (pnormalize p) + 1" |
958 have th: "degree ([a,1] *** pnormalize p) = degree (pnormalize p) + 1" |
959 by (auto simp add: poly_length_mult) |
959 by (auto simp add: poly_length_mult) |
960 |
960 |
961 have eqs: "poly ([a,1] *** pnormalize p) = poly ([a,1] *** p)" |
961 have eqs: "poly ([a,1] *** pnormalize p) = poly ([a,1] *** p)" |
962 by (rule ext) (simp add: poly_mult poly_add poly_cmult) |
962 by (rule ext) (simp add: poly_mult poly_add poly_cmult) |
963 from degree_unique[OF eqs] th |
963 from degree_unique[OF eqs] th |
978 have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))" |
978 have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))" |
979 apply (rule ext, simp add: poly_mult poly_add poly_cmult) |
979 apply (rule ext, simp add: poly_mult poly_add poly_cmult) |
980 by (simp add: mult_ac add_ac right_distrib) |
980 by (simp add: mult_ac add_ac right_distrib) |
981 note deq = degree_unique[OF eq] |
981 note deq = degree_unique[OF eq] |
982 {assume p: "poly p = poly []" |
982 {assume p: "poly p = poly []" |
983 with eq have eq': "poly ([a,1] %^(Suc n) *** p) = poly []" |
983 with eq have eq': "poly ([a,1] %^(Suc n) *** p) = poly []" |
984 by - (rule ext,simp add: poly_mult poly_cmult poly_add) |
984 by - (rule ext,simp add: poly_mult poly_cmult poly_add) |
985 from degree_unique[OF eq'] p have ?case by (simp add: degree_def)} |
985 from degree_unique[OF eq'] p have ?case by (simp add: degree_def)} |
986 moreover |
986 moreover |
987 {assume p: "poly p \<noteq> poly []" |
987 {assume p: "poly p \<noteq> poly []" |
988 from p have ap: "poly ([a,1] *** p) \<noteq> poly []" |
988 from p have ap: "poly ([a,1] *** p) \<noteq> poly []" |
989 using poly_mult_not_eq_poly_Nil unfolding poly_entire by auto |
989 using poly_mult_not_eq_poly_Nil unfolding poly_entire by auto |
990 have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1]%^n *** ([a,1] *** p))" |
990 have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1]%^n *** ([a,1] *** p))" |
991 by (rule ext, simp add: poly_mult poly_add poly_exp poly_cmult algebra_simps) |
991 by (rule ext, simp add: poly_mult poly_add poly_exp poly_cmult algebra_simps) |
992 from ap have ap': "(poly ([a,1] *** p) = poly []) = False" by blast |
992 from ap have ap': "(poly ([a,1] *** p) = poly []) = False" by blast |
993 have th0: "degree ([a,1]%^n *** ([a,1] *** p)) = degree ([a,1] *** p) + n" |
993 have th0: "degree ([a,1]%^n *** ([a,1] *** p)) = degree ([a,1] *** p) + n" |
994 apply (simp only: Suc.hyps[of a "pmult [a,one] p"] ap') |
994 apply (simp only: Suc.hyps[of a "pmult [a,one] p"] ap') |
995 by simp |
995 by simp |
996 |
996 |
997 from degree_unique[OF eq] ap p th0 linear_mul_degree[OF p, of a] |
997 from degree_unique[OF eq] ap p th0 linear_mul_degree[OF p, of a] |
998 have ?case by (auto simp del: poly.simps)} |
998 have ?case by (auto simp del: poly.simps)} |
999 ultimately show ?case by blast |
999 ultimately show ?case by blast |
1000 qed |
1000 qed |
1001 |
1001 |
1002 lemma (in recpower_idom_char_0) order_degree: |
1002 lemma (in recpower_idom_char_0) order_degree: |
1003 assumes p0: "poly p \<noteq> poly []" |
1003 assumes p0: "poly p \<noteq> poly []" |
1004 shows "order a p \<le> degree p" |
1004 shows "order a p \<le> degree p" |
1005 proof- |
1005 proof- |
1006 from order2[OF p0, unfolded divides_def] |
1006 from order2[OF p0, unfolded divides_def] |
1007 obtain q where q: "poly p = poly ([- a, 1]%^ (order a p) *** q)" by blast |
1007 obtain q where q: "poly p = poly ([- a, 1]%^ (order a p) *** q)" by blast |
1008 {assume "poly q = poly []" |
1008 {assume "poly q = poly []" |
1009 with q p0 have False by (simp add: poly_mult poly_entire)} |
1009 with q p0 have False by (simp add: poly_mult poly_entire)} |
1010 with degree_unique[OF q, unfolded linear_pow_mul_degree] |
1010 with degree_unique[OF q, unfolded linear_pow_mul_degree] |
1011 show ?thesis by auto |
1011 show ?thesis by auto |
1012 qed |
1012 qed |
1013 |
1013 |
1014 text{*Tidier versions of finiteness of roots.*} |
1014 text{*Tidier versions of finiteness of roots.*} |
1015 |
1015 |