src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy

 by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
 
 lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))"
   using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
 
-text{* The degree of addition and other general lemmas needed for the normal form of polymul*}
+text{* The degree of addition and other general lemmas needed for the normal form of polymul *}
 
 lemma polyadd_different_degreen: 
   "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> 
   degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)"
 proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)

     with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast}
   thus "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast
 qed
 
 
- 
-
-text{* polyneg is a negation and preserves normal form *}
+text{* polyneg is a negation and preserves normal forms *}
+
 lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
 by (induct p rule: polyneg.induct, auto)
 
 lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)"
   by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def)

 
 lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)"
   using isnpoly_def polyneg_normh by simp
 
 
-text{* polysub is a substraction and preserves normalform *}
+text{* polysub is a substraction and preserves normal forms *}
+
 lemma polysub[simp]: "Ipoly bs (polysub (p,q)) = (Ipoly bs p) - (Ipoly bs q)"
 by (simp add: polysub_def polyneg polyadd)
 lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub(p,q)) (min n0 n1)"
 by (simp add: polysub_def polyneg_normh polyadd_normh)
 

   apply (rule_tac x="Suc n" in exI, simp)
   apply clarsimp
   done
 
 text{* polypow is a power function and preserves normal forms *}
+
 lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n"
 proof(induct n rule: polypow.induct)
   case 1 thus ?case by simp
 next
   case (2 n)

 lemma polypow_norm:   
   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
   by (simp add: polypow_normh isnpoly_def)
 
-text{* Finally the whole normalization*}
+text{* Finally the whole normalization *}
 
 lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
 by (induct p rule:polynate.induct, auto)
 
 lemma polynate_norm[simp]: 

 
 lemma behead_isnpolyh:
   assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n"
   using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono)
 
-subsection{* Miscilanious lemmas about indexes, decrementation, substitution  etc ... *}
+subsection{* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
 lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
 proof(induct p arbitrary: n rule: poly.induct, auto)
   case (goal1 c n p n')
   hence "n = Suc (n - 1)" by simp
   hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp

   qed
 qed simp_all
 
 lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"
 by (induct p rule: coefficients.induct, auto)
-
-lemma length_exists: "\<exists>xs. length xs = n" by (rule exI[where x="replicate n x"], simp)
 
 lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p"
   unfolding wf_bs_def by (induct p, auto simp add: nth_append)
 
 lemma take_maxindex_wf: assumes wf: "wf_bs bs p" 

   with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq]
   show "p = q" by blast
 qed
 
 
-text{* consequenses of unicity on the algorithms for polynomial normalization *}
+text{* consequences of unicity on the algorithms for polynomial normalization *}
 
 lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
   using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
 

 
 subsection{* More about polypoly and pnormal etc *}
 
 definition "isnonconstant p = (\<not> isconstant p)"
 
-lemma last_map: "xs \<noteq> [] ==> last (map f xs) = f (last xs)" by (induct xs, auto)
-
 lemma isnonconstant_pnormal_iff: assumes nc: "isnonconstant p" 
   shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0" 
 proof
   let ?p = "polypoly bs p"  
   assume H: "pnormal ?p"