125 qed |
125 qed |
126 |
126 |
127 lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)" |
127 lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)" |
128 apply (induct a) |
128 apply (induct a) |
129 apply (simp, clarify) |
129 apply (simp, clarify) |
130 apply (case_tac b, simp_all add: add_ac) |
130 apply (case_tac b, simp_all add: ac_simps) |
131 done |
131 done |
132 |
132 |
133 lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)" |
133 lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)" |
134 apply (induct p arbitrary: q) |
134 apply (induct p arbitrary: q) |
135 apply simp |
135 apply simp |
150 case Nil |
150 case Nil |
151 thus ?case by simp |
151 thus ?case by simp |
152 next |
152 next |
153 case (Cons a as p2) |
153 case (Cons a as p2) |
154 thus ?case |
154 thus ?case |
155 by (cases p2) (simp_all add: add_ac distrib_left) |
155 by (cases p2) (simp_all add: ac_simps distrib_left) |
156 qed |
156 qed |
157 |
157 |
158 lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x" |
158 lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x" |
159 apply (induct p) |
159 apply (induct p) |
160 apply (case_tac [2] "x = zero") |
160 apply (case_tac [2] "x = zero") |
161 apply (auto simp add: distrib_left mult_ac) |
161 apply (auto simp add: distrib_left ac_simps) |
162 done |
162 done |
163 |
163 |
164 lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c*poly p x" |
164 lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c*poly p x" |
165 by (induct p) (auto simp add: distrib_left mult_ac) |
165 by (induct p) (auto simp add: distrib_left ac_simps) |
166 |
166 |
167 lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)" |
167 lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)" |
168 apply (simp add: poly_minus_def) |
168 apply (simp add: poly_minus_def) |
169 apply (auto simp add: poly_cmult) |
169 apply (auto simp add: poly_cmult) |
170 done |
170 done |
503 apply clarsimp |
503 apply clarsimp |
504 |
504 |
505 apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric]) |
505 apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric]) |
506 apply (rule_tac x = "pmult qa q" in exI) |
506 apply (rule_tac x = "pmult qa q" in exI) |
507 apply (rule_tac [2] x = "pmult p qa" in exI) |
507 apply (rule_tac [2] x = "pmult p qa" in exI) |
508 apply (auto simp add: poly_add poly_mult poly_cmult mult_ac) |
508 apply (auto simp add: poly_add poly_mult poly_cmult ac_simps) |
509 done |
509 done |
510 |
510 |
511 lemma (in comm_semiring_1) poly_divides_refl[simp]: "p divides p" |
511 lemma (in comm_semiring_1) poly_divides_refl[simp]: "p divides p" |
512 apply (simp add: divides_def) |
512 apply (simp add: divides_def) |
513 apply (rule_tac x = "[one]" in exI) |
513 apply (rule_tac x = "[one]" in exI) |
524 apply (auto simp add: le_iff_add) |
524 apply (auto simp add: le_iff_add) |
525 apply (induct_tac k) |
525 apply (induct_tac k) |
526 apply (rule_tac [2] poly_divides_trans) |
526 apply (rule_tac [2] poly_divides_trans) |
527 apply (auto simp add: divides_def) |
527 apply (auto simp add: divides_def) |
528 apply (rule_tac x = p in exI) |
528 apply (rule_tac x = p in exI) |
529 apply (auto simp add: poly_mult fun_eq mult_ac) |
529 apply (auto simp add: poly_mult fun_eq ac_simps) |
530 done |
530 done |
531 |
531 |
532 lemma (in comm_semiring_1) poly_exp_divides: |
532 lemma (in comm_semiring_1) poly_exp_divides: |
533 "(p %^ n) divides q \<Longrightarrow> m \<le> n \<Longrightarrow> (p %^ m) divides q" |
533 "(p %^ n) divides q \<Longrightarrow> m \<le> n \<Longrightarrow> (p %^ m) divides q" |
534 by (blast intro: poly_divides_exp poly_divides_trans) |
534 by (blast intro: poly_divides_exp poly_divides_trans) |
548 done |
548 done |
549 |
549 |
550 lemma (in comm_ring_1) poly_divides_diff2: |
550 lemma (in comm_ring_1) poly_divides_diff2: |
551 "p divides r \<Longrightarrow> p divides (q +++ r) \<Longrightarrow> p divides q" |
551 "p divides r \<Longrightarrow> p divides (q +++ r) \<Longrightarrow> p divides q" |
552 apply (erule poly_divides_diff) |
552 apply (erule poly_divides_diff) |
553 apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac) |
553 apply (auto simp add: poly_add fun_eq poly_mult divides_def ac_simps) |
554 done |
554 done |
555 |
555 |
556 lemma (in semiring_0) poly_divides_zero: "poly p = poly [] \<Longrightarrow> q divides p" |
556 lemma (in semiring_0) poly_divides_zero: "poly p = poly [] \<Longrightarrow> q divides p" |
557 apply (simp add: divides_def) |
557 apply (simp add: divides_def) |
558 apply (rule exI[where x="[]"]) |
558 apply (rule exI[where x="[]"]) |
606 qed |
606 qed |
607 qed |
607 qed |
608 |
608 |
609 |
609 |
610 lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x" |
610 lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x" |
611 by (induct n) (auto simp add: poly_mult mult_ac) |
611 by (induct n) (auto simp add: poly_mult ac_simps) |
612 |
612 |
613 lemma (in comm_semiring_1) divides_left_mult: |
613 lemma (in comm_semiring_1) divides_left_mult: |
614 assumes d:"(p***q) divides r" shows "p divides r \<and> q divides r" |
614 assumes d:"(p***q) divides r" shows "p divides r \<and> q divides r" |
615 proof- |
615 proof- |
616 from d obtain t where r:"poly r = poly (p***q *** t)" |
616 from d obtain t where r:"poly r = poly (p***q *** t)" |
617 unfolding divides_def by blast |
617 unfolding divides_def by blast |
618 hence "poly r = poly (p *** (q *** t))" |
618 hence "poly r = poly (p *** (q *** t))" |
619 "poly r = poly (q *** (p***t))" by(auto simp add: fun_eq poly_mult mult_ac) |
619 "poly r = poly (q *** (p***t))" by(auto simp add: fun_eq poly_mult ac_simps) |
620 thus ?thesis unfolding divides_def by blast |
620 thus ?thesis unfolding divides_def by blast |
621 qed |
621 qed |
622 |
622 |
623 |
623 |
624 (* FIXME: Tidy up *) |
624 (* FIXME: Tidy up *) |
740 apply (unfold divides_def) |
740 apply (unfold divides_def) |
741 apply (drule order2 [where a = a]) |
741 apply (drule order2 [where a = a]) |
742 apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe) |
742 apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe) |
743 apply (rule_tac x = q in exI, safe) |
743 apply (rule_tac x = q in exI, safe) |
744 apply (drule_tac x = qa in spec) |
744 apply (drule_tac x = qa in spec) |
745 apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons) |
745 apply (auto simp add: poly_mult fun_eq poly_exp ac_simps simp del: pmult_Cons) |
746 done |
746 done |
747 |
747 |
748 text{*Important composition properties of orders.*} |
748 text{*Important composition properties of orders.*} |
749 lemma order_mult: |
749 lemma order_mult: |
750 "poly (p *** q) \<noteq> poly [] \<Longrightarrow> |
750 "poly (p *** q) \<noteq> poly [] \<Longrightarrow> |
753 apply (auto simp add: poly_entire simp del: pmult_Cons) |
753 apply (auto simp add: poly_entire simp del: pmult_Cons) |
754 apply (drule_tac a = a in order2)+ |
754 apply (drule_tac a = a in order2)+ |
755 apply safe |
755 apply safe |
756 apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe) |
756 apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe) |
757 apply (rule_tac x = "qa *** qaa" in exI) |
757 apply (rule_tac x = "qa *** qaa" in exI) |
758 apply (simp add: poly_mult mult_ac del: pmult_Cons) |
758 apply (simp add: poly_mult ac_simps del: pmult_Cons) |
759 apply (drule_tac a = a in order_decomp)+ |
759 apply (drule_tac a = a in order_decomp)+ |
760 apply safe |
760 apply safe |
761 apply (subgoal_tac "[-a,1] divides (qa *** qaa) ") |
761 apply (subgoal_tac "[-a,1] divides (qa *** qaa) ") |
762 apply (simp add: poly_primes del: pmult_Cons) |
762 apply (simp add: poly_primes del: pmult_Cons) |
763 apply (auto simp add: divides_def simp del: pmult_Cons) |
763 apply (auto simp add: divides_def simp del: pmult_Cons) |
764 apply (rule_tac x = qb in exI) |
764 apply (rule_tac x = qb in exI) |
765 apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))") |
765 apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))") |
766 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
766 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
767 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))) ") |
767 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))) ") |
768 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
768 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
769 apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons) |
769 apply (simp add: fun_eq poly_exp_add poly_mult ac_simps del: pmult_Cons) |
770 done |
770 done |
771 |
771 |
772 lemma (in idom_char_0) order_mult: |
772 lemma (in idom_char_0) order_mult: |
773 assumes "poly (p *** q) \<noteq> poly []" |
773 assumes "poly (p *** q) \<noteq> poly []" |
774 shows "order a (p *** q) = order a p + order a q" |
774 shows "order a (p *** q) = order a p + order a q" |
777 apply (auto simp add: poly_entire simp del: pmult_Cons) |
777 apply (auto simp add: poly_entire simp del: pmult_Cons) |
778 apply (drule_tac a = a in order2)+ |
778 apply (drule_tac a = a in order2)+ |
779 apply safe |
779 apply safe |
780 apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe) |
780 apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe) |
781 apply (rule_tac x = "pmult qa qaa" in exI) |
781 apply (rule_tac x = "pmult qa qaa" in exI) |
782 apply (simp add: poly_mult mult_ac del: pmult_Cons) |
782 apply (simp add: poly_mult ac_simps del: pmult_Cons) |
783 apply (drule_tac a = a in order_decomp)+ |
783 apply (drule_tac a = a in order_decomp)+ |
784 apply safe |
784 apply safe |
785 apply (subgoal_tac "[uminus a, one] divides pmult qa qaa") |
785 apply (subgoal_tac "[uminus a, one] divides pmult qa qaa") |
786 apply (simp add: poly_primes del: pmult_Cons) |
786 apply (simp add: poly_primes del: pmult_Cons) |
787 apply (auto simp add: divides_def simp del: pmult_Cons) |
787 apply (auto simp add: divides_def simp del: pmult_Cons) |
792 apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a q)) |
792 apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a q)) |
793 (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa))) = |
793 (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa))) = |
794 poly (pmult (pexp [uminus a, one] (order a q)) |
794 poly (pmult (pexp [uminus a, one] (order a q)) |
795 (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb)))") |
795 (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb)))") |
796 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
796 apply (drule poly_mult_left_cancel [THEN iffD1], force) |
797 apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons) |
797 apply (simp add: fun_eq poly_exp_add poly_mult ac_simps del: pmult_Cons) |
798 done |
798 done |
799 |
799 |
800 lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] \<Longrightarrow> poly p a = 0 \<longleftrightarrow> order a p \<noteq> 0" |
800 lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] \<Longrightarrow> poly p a = 0 \<longleftrightarrow> order a p \<noteq> 0" |
801 by (rule order_root [THEN ssubst]) auto |
801 by (rule order_root [THEN ssubst]) auto |
802 |
802 |
986 next |
986 next |
987 case (Suc n a p) |
987 case (Suc n a p) |
988 have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))" |
988 have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))" |
989 apply (rule ext) |
989 apply (rule ext) |
990 apply (simp add: poly_mult poly_add poly_cmult) |
990 apply (simp add: poly_mult poly_add poly_cmult) |
991 apply (simp add: mult_ac add_ac distrib_left) |
991 apply (simp add: ac_simps ac_simps distrib_left) |
992 done |
992 done |
993 note deq = degree_unique[OF eq] |
993 note deq = degree_unique[OF eq] |
994 show ?case |
994 show ?case |
995 proof (cases "poly p = poly []") |
995 proof (cases "poly p = poly []") |
996 case True |
996 case True |