src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 41404 aae9f912cca8
parent 41403 7eba049f7310
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Dec 25 22:18:55 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Dec 25 22:18:58 2010 +0100
     1.3 @@ -321,7 +321,7 @@
     1.4  lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))"
     1.5    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
     1.6  
     1.7 -text{* The degree of addition and other general lemmas needed for the normal form of polymul*}
     1.8 +text{* The degree of addition and other general lemmas needed for the normal form of polymul *}
     1.9  
    1.10  lemma polyadd_different_degreen: 
    1.11    "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> 
    1.12 @@ -598,9 +598,8 @@
    1.13  qed
    1.14  
    1.15  
    1.16 - 
    1.17 +text{* polyneg is a negation and preserves normal forms *}
    1.18  
    1.19 -text{* polyneg is a negation and preserves normal form *}
    1.20  lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
    1.21  by (induct p rule: polyneg.induct, auto)
    1.22  
    1.23 @@ -615,7 +614,8 @@
    1.24    using isnpoly_def polyneg_normh by simp
    1.25  
    1.26  
    1.27 -text{* polysub is a substraction and preserves normalform *}
    1.28 +text{* polysub is a substraction and preserves normal forms *}
    1.29 +
    1.30  lemma polysub[simp]: "Ipoly bs (polysub (p,q)) = (Ipoly bs p) - (Ipoly bs q)"
    1.31  by (simp add: polysub_def polyneg polyadd)
    1.32  lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub(p,q)) (min n0 n1)"
    1.33 @@ -651,6 +651,7 @@
    1.34    done
    1.35  
    1.36  text{* polypow is a power function and preserves normal forms *}
    1.37 +
    1.38  lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n"
    1.39  proof(induct n rule: polypow.induct)
    1.40    case 1 thus ?case by simp
    1.41 @@ -699,7 +700,7 @@
    1.42    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
    1.43    by (simp add: polypow_normh isnpoly_def)
    1.44  
    1.45 -text{* Finally the whole normalization*}
    1.46 +text{* Finally the whole normalization *}
    1.47  
    1.48  lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
    1.49  by (induct p rule:polynate.induct, auto)
    1.50 @@ -759,7 +760,7 @@
    1.51    assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n"
    1.52    using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono)
    1.53  
    1.54 -subsection{* Miscilanious lemmas about indexes, decrementation, substitution  etc ... *}
    1.55 +subsection{* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
    1.56  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
    1.57  proof(induct p arbitrary: n rule: poly.induct, auto)
    1.58    case (goal1 c n p n')
    1.59 @@ -841,8 +842,6 @@
    1.60  lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"
    1.61  by (induct p rule: coefficients.induct, auto)
    1.62  
    1.63 -lemma length_exists: "\<exists>xs. length xs = n" by (rule exI[where x="replicate n x"], simp)
    1.64 -
    1.65  lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p"
    1.66    unfolding wf_bs_def by (induct p, auto simp add: nth_append)
    1.67  
    1.68 @@ -1038,7 +1037,7 @@
    1.69  qed
    1.70  
    1.71  
    1.72 -text{* consequenses of unicity on the algorithms for polynomial normalization *}
    1.73 +text{* consequences of unicity on the algorithms for polynomial normalization *}
    1.74  
    1.75  lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.76    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
    1.77 @@ -1525,8 +1524,6 @@
    1.78  
    1.79  definition "isnonconstant p = (\<not> isconstant p)"
    1.80  
    1.81 -lemma last_map: "xs \<noteq> [] ==> last (map f xs) = f (last xs)" by (induct xs, auto)
    1.82 -
    1.83  lemma isnonconstant_pnormal_iff: assumes nc: "isnonconstant p" 
    1.84    shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0" 
    1.85  proof