author krauss Sat, 25 Dec 2010 22:18:58 +0100 changeset 41404 aae9f912cca8 parent 41403 7eba049f7310 child 41405 05bd42fdaea8
dropped duplicate unused lemmas; spelling
```--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Dec 25 22:18:55 2010 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Dec 25 22:18:58 2010 +0100
@@ -321,7 +321,7 @@
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 *}

"\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow>
@@ -598,9 +598,8 @@
qed

-
+text{* polyneg is a negation and preserves normal forms *}

-text{* polyneg is a negation and preserves normal form *}
lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
by (induct p rule: polyneg.induct, auto)

@@ -615,7 +614,8 @@
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)"
lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub(p,q)) (min n0 n1)"
@@ -651,6 +651,7 @@
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
@@ -699,7 +700,7 @@
shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"

-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)
@@ -759,7 +760,7 @@
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')
@@ -841,8 +842,6 @@
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)

@@ -1038,7 +1037,7 @@
qed

-text{* consequenses of unicity on the algorithms for polynomial normalization *}
+text{* consequences of unicity on the algorithms for polynomial normalization *}