440 lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p" |
440 lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p" |
441 by (rule poly_ext, simp) |
441 by (rule poly_ext, simp) |
442 |
442 |
443 lemma smult_add_right: |
443 lemma smult_add_right: |
444 "smult a (p + q) = smult a p + smult a q" |
444 "smult a (p + q) = smult a p + smult a q" |
445 by (rule poly_ext, simp add: ring_simps) |
445 by (rule poly_ext, simp add: algebra_simps) |
446 |
446 |
447 lemma smult_add_left: |
447 lemma smult_add_left: |
448 "smult (a + b) p = smult a p + smult b p" |
448 "smult (a + b) p = smult a p + smult b p" |
449 by (rule poly_ext, simp add: ring_simps) |
449 by (rule poly_ext, simp add: algebra_simps) |
450 |
450 |
451 lemma smult_minus_right [simp]: |
451 lemma smult_minus_right [simp]: |
452 "smult (a::'a::comm_ring) (- p) = - smult a p" |
452 "smult (a::'a::comm_ring) (- p) = - smult a p" |
453 by (rule poly_ext, simp) |
453 by (rule poly_ext, simp) |
454 |
454 |
456 "smult (- a::'a::comm_ring) p = - smult a p" |
456 "smult (- a::'a::comm_ring) p = - smult a p" |
457 by (rule poly_ext, simp) |
457 by (rule poly_ext, simp) |
458 |
458 |
459 lemma smult_diff_right: |
459 lemma smult_diff_right: |
460 "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q" |
460 "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q" |
461 by (rule poly_ext, simp add: ring_simps) |
461 by (rule poly_ext, simp add: algebra_simps) |
462 |
462 |
463 lemma smult_diff_left: |
463 lemma smult_diff_left: |
464 "smult (a - b::'a::comm_ring) p = smult a p - smult b p" |
464 "smult (a - b::'a::comm_ring) p = smult a p - smult b p" |
465 by (rule poly_ext, simp add: ring_simps) |
465 by (rule poly_ext, simp add: algebra_simps) |
466 |
466 |
467 lemmas smult_distribs = |
467 lemmas smult_distribs = |
468 smult_add_left smult_add_right |
468 smult_add_left smult_add_right |
469 smult_diff_left smult_diff_right |
469 smult_diff_left smult_diff_right |
470 |
470 |
515 lemma mult_poly_0_right: "p * (0::'a poly) = 0" |
515 lemma mult_poly_0_right: "p * (0::'a poly) = 0" |
516 by (induct p, simp add: mult_poly_0_left, simp) |
516 by (induct p, simp add: mult_poly_0_left, simp) |
517 |
517 |
518 lemma mult_pCons_right [simp]: |
518 lemma mult_pCons_right [simp]: |
519 "p * pCons a q = smult a p + pCons 0 (p * q)" |
519 "p * pCons a q = smult a p + pCons 0 (p * q)" |
520 by (induct p, simp add: mult_poly_0_left, simp add: ring_simps) |
520 by (induct p, simp add: mult_poly_0_left, simp add: algebra_simps) |
521 |
521 |
522 lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right |
522 lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right |
523 |
523 |
524 lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)" |
524 lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)" |
525 by (induct p, simp add: mult_poly_0, simp add: smult_add_right) |
525 by (induct p, simp add: mult_poly_0, simp add: smult_add_right) |
529 |
529 |
530 lemma mult_poly_add_left: |
530 lemma mult_poly_add_left: |
531 fixes p q r :: "'a poly" |
531 fixes p q r :: "'a poly" |
532 shows "(p + q) * r = p * r + q * r" |
532 shows "(p + q) * r = p * r + q * r" |
533 by (induct r, simp add: mult_poly_0, |
533 by (induct r, simp add: mult_poly_0, |
534 simp add: smult_distribs group_simps) |
534 simp add: smult_distribs algebra_simps) |
535 |
535 |
536 instance proof |
536 instance proof |
537 fix p q r :: "'a poly" |
537 fix p q r :: "'a poly" |
538 show 0: "0 * p = 0" |
538 show 0: "0 * p = 0" |
539 by (rule mult_poly_0_left) |
539 by (rule mult_poly_0_left) |
756 from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y" |
756 from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y" |
757 unfolding pdivmod_rel_def by simp_all |
757 unfolding pdivmod_rel_def by simp_all |
758 from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y" |
758 from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y" |
759 unfolding pdivmod_rel_def by simp_all |
759 unfolding pdivmod_rel_def by simp_all |
760 from q1 q2 have q3: "(q1 - q2) * y = r2 - r1" |
760 from q1 q2 have q3: "(q1 - q2) * y = r2 - r1" |
761 by (simp add: ring_simps) |
761 by (simp add: algebra_simps) |
762 from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y" |
762 from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y" |
763 by (auto intro: degree_diff_less) |
763 by (auto intro: degree_diff_less) |
764 |
764 |
765 show "q1 = q2 \<and> r1 = r2" |
765 show "q1 = q2 \<and> r1 = r2" |
766 proof (rule ccontr) |
766 proof (rule ccontr) |
892 shows "poly (monom a n) x = a * x ^ n" |
892 shows "poly (monom a n) x = a * x ^ n" |
893 by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac) |
893 by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac) |
894 |
894 |
895 lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x" |
895 lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x" |
896 apply (induct p arbitrary: q, simp) |
896 apply (induct p arbitrary: q, simp) |
897 apply (case_tac q, simp, simp add: ring_simps) |
897 apply (case_tac q, simp, simp add: algebra_simps) |
898 done |
898 done |
899 |
899 |
900 lemma poly_minus [simp]: |
900 lemma poly_minus [simp]: |
901 fixes x :: "'a::comm_ring" |
901 fixes x :: "'a::comm_ring" |
902 shows "poly (- p) x = - poly p x" |
902 shows "poly (- p) x = - poly p x" |
909 |
909 |
910 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)" |
910 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)" |
911 by (cases "finite A", induct set: finite, simp_all) |
911 by (cases "finite A", induct set: finite, simp_all) |
912 |
912 |
913 lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x" |
913 lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x" |
914 by (induct p, simp, simp add: ring_simps) |
914 by (induct p, simp, simp add: algebra_simps) |
915 |
915 |
916 lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x" |
916 lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x" |
917 by (induct p, simp_all, simp add: ring_simps) |
917 by (induct p, simp_all, simp add: algebra_simps) |
918 |
918 |
919 lemma poly_power [simp]: |
919 lemma poly_power [simp]: |
920 fixes p :: "'a::{comm_semiring_1,recpower} poly" |
920 fixes p :: "'a::{comm_semiring_1,recpower} poly" |
921 shows "poly (p ^ n) x = poly p x ^ n" |
921 shows "poly (p ^ n) x = poly p x ^ n" |
922 by (induct n, simp, simp add: power_Suc) |
922 by (induct n, simp, simp add: power_Suc) |
981 |
981 |
982 lemma synthetic_div_correct': |
982 lemma synthetic_div_correct': |
983 fixes c :: "'a::comm_ring_1" |
983 fixes c :: "'a::comm_ring_1" |
984 shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p" |
984 shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p" |
985 using synthetic_div_correct [of p c] |
985 using synthetic_div_correct [of p c] |
986 by (simp add: group_simps) |
986 by (simp add: algebra_simps) |
987 |
987 |
988 lemma poly_eq_0_iff_dvd: |
988 lemma poly_eq_0_iff_dvd: |
989 fixes c :: "'a::idom" |
989 fixes c :: "'a::idom" |
990 shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p" |
990 shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p" |
991 proof |
991 proof |