equal
deleted
inserted
replaced
319 by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib) |
319 by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib) |
320 |
320 |
321 lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))" |
321 lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))" |
322 using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp |
322 using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp |
323 |
323 |
324 text{* The degree of addition and other general lemmas needed for the normal form of polymul*} |
324 text{* The degree of addition and other general lemmas needed for the normal form of polymul *} |
325 |
325 |
326 lemma polyadd_different_degreen: |
326 lemma polyadd_different_degreen: |
327 "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> |
327 "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> |
328 degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)" |
328 degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)" |
329 proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct) |
329 proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct) |
596 with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast} |
596 with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast} |
597 thus "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast |
597 thus "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast |
598 qed |
598 qed |
599 |
599 |
600 |
600 |
601 |
601 text{* polyneg is a negation and preserves normal forms *} |
602 |
602 |
603 text{* polyneg is a negation and preserves normal form *} |
|
604 lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p" |
603 lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p" |
605 by (induct p rule: polyneg.induct, auto) |
604 by (induct p rule: polyneg.induct, auto) |
606 |
605 |
607 lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)" |
606 lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)" |
608 by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def) |
607 by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def) |
613 |
612 |
614 lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)" |
613 lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)" |
615 using isnpoly_def polyneg_normh by simp |
614 using isnpoly_def polyneg_normh by simp |
616 |
615 |
617 |
616 |
618 text{* polysub is a substraction and preserves normalform *} |
617 text{* polysub is a substraction and preserves normal forms *} |
|
618 |
619 lemma polysub[simp]: "Ipoly bs (polysub (p,q)) = (Ipoly bs p) - (Ipoly bs q)" |
619 lemma polysub[simp]: "Ipoly bs (polysub (p,q)) = (Ipoly bs p) - (Ipoly bs q)" |
620 by (simp add: polysub_def polyneg polyadd) |
620 by (simp add: polysub_def polyneg polyadd) |
621 lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub(p,q)) (min n0 n1)" |
621 lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub(p,q)) (min n0 n1)" |
622 by (simp add: polysub_def polyneg_normh polyadd_normh) |
622 by (simp add: polysub_def polyneg_normh polyadd_normh) |
623 |
623 |
649 apply (rule_tac x="Suc n" in exI, simp) |
649 apply (rule_tac x="Suc n" in exI, simp) |
650 apply clarsimp |
650 apply clarsimp |
651 done |
651 done |
652 |
652 |
653 text{* polypow is a power function and preserves normal forms *} |
653 text{* polypow is a power function and preserves normal forms *} |
|
654 |
654 lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n" |
655 lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n" |
655 proof(induct n rule: polypow.induct) |
656 proof(induct n rule: polypow.induct) |
656 case 1 thus ?case by simp |
657 case 1 thus ?case by simp |
657 next |
658 next |
658 case (2 n) |
659 case (2 n) |
697 lemma polypow_norm: |
698 lemma polypow_norm: |
698 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
699 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
699 shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)" |
700 shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)" |
700 by (simp add: polypow_normh isnpoly_def) |
701 by (simp add: polypow_normh isnpoly_def) |
701 |
702 |
702 text{* Finally the whole normalization*} |
703 text{* Finally the whole normalization *} |
703 |
704 |
704 lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})" |
705 lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})" |
705 by (induct p rule:polynate.induct, auto) |
706 by (induct p rule:polynate.induct, auto) |
706 |
707 |
707 lemma polynate_norm[simp]: |
708 lemma polynate_norm[simp]: |
757 |
758 |
758 lemma behead_isnpolyh: |
759 lemma behead_isnpolyh: |
759 assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n" |
760 assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n" |
760 using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono) |
761 using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono) |
761 |
762 |
762 subsection{* Miscilanious lemmas about indexes, decrementation, substitution etc ... *} |
763 subsection{* Miscellaneous lemmas about indexes, decrementation, substitution etc ... *} |
763 lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p" |
764 lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p" |
764 proof(induct p arbitrary: n rule: poly.induct, auto) |
765 proof(induct p arbitrary: n rule: poly.induct, auto) |
765 case (goal1 c n p n') |
766 case (goal1 c n p n') |
766 hence "n = Suc (n - 1)" by simp |
767 hence "n = Suc (n - 1)" by simp |
767 hence "isnpolyh p (Suc (n - 1))" using `isnpolyh p n` by simp |
768 hence "isnpolyh p (Suc (n - 1))" using `isnpolyh p n` by simp |
838 qed |
839 qed |
839 qed simp_all |
840 qed simp_all |
840 |
841 |
841 lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p" |
842 lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p" |
842 by (induct p rule: coefficients.induct, auto) |
843 by (induct p rule: coefficients.induct, auto) |
843 |
|
844 lemma length_exists: "\<exists>xs. length xs = n" by (rule exI[where x="replicate n x"], simp) |
|
845 |
844 |
846 lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p" |
845 lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p" |
847 unfolding wf_bs_def by (induct p, auto simp add: nth_append) |
846 unfolding wf_bs_def by (induct p, auto simp add: nth_append) |
848 |
847 |
849 lemma take_maxindex_wf: assumes wf: "wf_bs bs p" |
848 lemma take_maxindex_wf: assumes wf: "wf_bs bs p" |
1036 with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq] |
1035 with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq] |
1037 show "p = q" by blast |
1036 show "p = q" by blast |
1038 qed |
1037 qed |
1039 |
1038 |
1040 |
1039 |
1041 text{* consequenses of unicity on the algorithms for polynomial normalization *} |
1040 text{* consequences of unicity on the algorithms for polynomial normalization *} |
1042 |
1041 |
1043 lemma polyadd_commute: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
1042 lemma polyadd_commute: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
1044 and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p" |
1043 and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p" |
1045 using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp |
1044 using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp |
1046 |
1045 |
1523 |
1522 |
1524 subsection{* More about polypoly and pnormal etc *} |
1523 subsection{* More about polypoly and pnormal etc *} |
1525 |
1524 |
1526 definition "isnonconstant p = (\<not> isconstant p)" |
1525 definition "isnonconstant p = (\<not> isconstant p)" |
1527 |
1526 |
1528 lemma last_map: "xs \<noteq> [] ==> last (map f xs) = f (last xs)" by (induct xs, auto) |
|
1529 |
|
1530 lemma isnonconstant_pnormal_iff: assumes nc: "isnonconstant p" |
1527 lemma isnonconstant_pnormal_iff: assumes nc: "isnonconstant p" |
1531 shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0" |
1528 shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0" |
1532 proof |
1529 proof |
1533 let ?p = "polypoly bs p" |
1530 let ?p = "polypoly bs p" |
1534 assume H: "pnormal ?p" |
1531 assume H: "pnormal ?p" |