src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 52658 1e7896c7f781 parent 50282 fe4d4bb9f4c2 child 52803 bcaa5bbf7e6b
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Jul 15 10:42:12 2013 +0200
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Jul 15 11:29:19 2013 +0200
1.3 @@ -8,8 +8,6 @@
1.4  imports Complex_Main "~~/src/HOL/Library/Abstract_Rat" Polynomial_List
1.5  begin
1.6
1.7 -  (* Implementation *)
1.8 -
1.9  subsection{* Datatype of polynomial expressions *}
1.10
1.11  datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly
1.12 @@ -18,8 +16,11 @@
1.13  abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
1.14  abbreviation poly_p :: "int \<Rightarrow> poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \<equiv> C (i)\<^sub>N"
1.15
1.16 +
1.17  subsection{* Boundedness, substitution and all that *}
1.18 -primrec polysize:: "poly \<Rightarrow> nat" where
1.19 +
1.20 +primrec polysize:: "poly \<Rightarrow> nat"
1.21 +where
1.22    "polysize (C c) = 1"
1.23  | "polysize (Bound n) = 1"
1.24  | "polysize (Neg p) = 1 + polysize p"
1.25 @@ -29,7 +30,8 @@
1.26  | "polysize (Pw p n) = 1 + polysize p"
1.27  | "polysize (CN c n p) = 4 + polysize c + polysize p"
1.28
1.29 -primrec polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) where
1.30 +primrec polybound0:: "poly \<Rightarrow> bool" -- {* a poly is INDEPENDENT of Bound 0 *}
1.31 +where
1.32    "polybound0 (C c) = True"
1.33  | "polybound0 (Bound n) = (n>0)"
1.34  | "polybound0 (Neg a) = polybound0 a"
1.35 @@ -39,7 +41,8 @@
1.36  | "polybound0 (Pw p n) = (polybound0 p)"
1.37  | "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
1.38
1.39 -primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *) where
1.40 +primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" -- {* substitute a poly into a poly for Bound 0 *}
1.41 +where
1.42    "polysubst0 t (C c) = (C c)"
1.43  | "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
1.44  | "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
1.45 @@ -61,6 +64,7 @@
1.46  | "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)"
1.47  | "decrpoly a = a"
1.48
1.49 +
1.50  subsection{* Degrees and heads and coefficients *}
1.51
1.52  fun degree:: "poly \<Rightarrow> nat"
1.53 @@ -104,9 +108,9 @@
1.55  | "headconst (C n) = n"
1.56
1.57 +
1.58  subsection{* Operations for normalization *}
1.59
1.60 -
1.61  declare if_cong[fundef_cong del]
1.62  declare let_cong[fundef_cong del]
1.63
1.64 @@ -131,8 +135,7 @@
1.65  | "polyneg a = Neg a"
1.66
1.67  definition polysub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
1.68 -where
1.69 -  "p -\<^sub>p q = polyadd p (polyneg q)"
1.70 +  where "p -\<^sub>p q = polyadd p (polyneg q)"
1.71
1.72  fun polymul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
1.73  where
1.74 @@ -173,7 +176,8 @@
1.75  by pat_completeness auto
1.76  termination by (relation "measure polysize") auto
1.77
1.78 -fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly" where
1.79 +fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly"
1.80 +where
1.81    "poly_cmul y (C x) = C (y *\<^sub>N x)"
1.82  | "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)"
1.83  | "poly_cmul y p = C y *\<^sub>p p"
1.84 @@ -181,35 +185,39 @@
1.85  definition monic :: "poly \<Rightarrow> (poly \<times> bool)" where
1.86    "monic p \<equiv> (let h = headconst p in if h = 0\<^sub>N then (p,False) else ((C (Ninv h)) *\<^sub>p p, 0>\<^sub>N h))"
1.87
1.88 +
1.89  subsection{* Pseudo-division *}
1.90
1.91 -definition shift1 :: "poly \<Rightarrow> poly" where
1.92 -  "shift1 p \<equiv> CN 0\<^sub>p 0 p"
1.93 +definition shift1 :: "poly \<Rightarrow> poly"
1.94 +  where "shift1 p \<equiv> CN 0\<^sub>p 0 p"
1.95
1.96 -abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where
1.97 -  "funpow \<equiv> compow"
1.98 +abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
1.99 +  where "funpow \<equiv> compow"
1.100
1.101  partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly"
1.102 -  where
1.103 +where
1.104    "polydivide_aux a n p k s =
1.105 -  (if s = 0\<^sub>p then (k,s)
1.106 -  else (let b = head s; m = degree s in
1.107 -  (if m < n then (k,s) else
1.108 -  (let p'= funpow (m - n) shift1 p in
1.109 -  (if a = b then polydivide_aux a n p k (s -\<^sub>p p')
1.110 -  else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
1.111 +    (if s = 0\<^sub>p then (k,s)
1.112 +    else (let b = head s; m = degree s in
1.113 +    (if m < n then (k,s) else
1.114 +    (let p'= funpow (m - n) shift1 p in
1.115 +    (if a = b then polydivide_aux a n p k (s -\<^sub>p p')
1.116 +    else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
1.117
1.118 -definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
1.119 -  "polydivide s p \<equiv> polydivide_aux (head p) (degree p) p 0 s"
1.120 +definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)"
1.121 +  where "polydivide s p \<equiv> polydivide_aux (head p) (degree p) p 0 s"
1.122
1.123 -fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where
1.124 +fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly"
1.125 +where
1.126    "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"
1.127  | "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p"
1.128
1.129 -fun poly_deriv :: "poly \<Rightarrow> poly" where
1.130 +fun poly_deriv :: "poly \<Rightarrow> poly"
1.131 +where
1.132    "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
1.133  | "poly_deriv p = 0\<^sub>p"
1.134
1.135 +
1.136  subsection{* Semantics of the polynomial representation *}
1.137
1.138  primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
1.139 @@ -233,6 +241,7 @@
1.140
1.141  lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat
1.142
1.143 +
1.144  subsection {* Normal form and normalization *}
1.145
1.146  fun isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
1.147 @@ -242,10 +251,10 @@
1.148  | "isnpolyh p = (\<lambda>k. False)"
1.149
1.150  lemma isnpolyh_mono: "\<lbrakk>n' \<le> n ; isnpolyh p n\<rbrakk> \<Longrightarrow> isnpolyh p n'"
1.151 -by (induct p rule: isnpolyh.induct, auto)
1.152 +  by (induct p rule: isnpolyh.induct) auto
1.153
1.154 -definition isnpoly :: "poly \<Rightarrow> bool" where
1.155 -  "isnpoly p \<equiv> isnpolyh p 0"
1.156 +definition isnpoly :: "poly \<Rightarrow> bool"
1.157 +  where "isnpoly p \<equiv> isnpolyh p 0"
1.158
1.159  text{* polyadd preserves normal forms *}
1.160
1.161 @@ -304,7 +313,8 @@
1.162  qed auto
1.163
1.164  lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
1.165 -by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
1.166 +  by (induct p q rule: polyadd.induct)
1.167 +    (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
1.168
1.169  lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd p q)"
1.170    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
1.171 @@ -332,14 +342,14 @@
1.172  qed auto
1.173
1.174  lemma headnz[simp]: "\<lbrakk>isnpolyh p n ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> headn p m \<noteq> 0\<^sub>p"
1.175 -  by (induct p arbitrary: n rule: headn.induct, auto)
1.176 +  by (induct p arbitrary: n rule: headn.induct) auto
1.177  lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> degree p = 0"
1.178 -  by (induct p arbitrary: n rule: degree.induct, auto)
1.179 +  by (induct p arbitrary: n rule: degree.induct) auto
1.180  lemma degreen_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> degreen p m = 0"
1.181 -  by (induct p arbitrary: n rule: degreen.induct, auto)
1.182 +  by (induct p arbitrary: n rule: degreen.induct) auto
1.183
1.184  lemma degree_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> degree p = 0"
1.185 -  by (induct p arbitrary: n rule: degree.induct, auto)
1.186 +  by (induct p arbitrary: n rule: degree.induct) auto
1.187
1.188  lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degree c = 0"
1.189    using degree_isnpolyh_Suc by auto
1.190 @@ -352,9 +362,9 @@
1.191    shows "degreen (p +\<^sub>p q) m \<le> max (degreen p m) (degreen q m)"
1.192    using np nq m
1.193  proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct)
1.194 -  case (2 c c' n' p' n0 n1) thus ?case  by (cases n', simp_all)
1.195 +  case (2 c c' n' p' n0 n1) thus ?case  by (cases n') simp_all
1.196  next
1.197 -  case (3 c n p c' n0 n1) thus ?case by (cases n, auto)
1.198 +  case (3 c n p c' n0 n1) thus ?case by (cases n) auto
1.199  next
1.200    case (4 c n p c' n' p' n0 n1 m)
1.201    have "n' = n \<or> n < n' \<or> n' < n" by arith
1.202 @@ -377,7 +387,8 @@
1.203      moreover {assume eq: "n = n'" hence ?case using 4
1.204          apply (cases "p +\<^sub>p p' = 0\<^sub>p")
1.205          apply (auto simp add: Let_def)
1.206 -        by blast
1.207 +        apply blast
1.208 +        done
1.209        }
1.210      ultimately have ?case by blast}
1.211    ultimately show ?case by blast
1.212 @@ -385,13 +396,14 @@
1.213
1.214  lemma polymul_properties:
1.215    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.216 -  and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1"
1.217 +    and np: "isnpolyh p n0"
1.218 +    and nq: "isnpolyh q n1"
1.219 +    and m: "m \<le> min n0 n1"
1.220    shows "isnpolyh (p *\<^sub>p q) (min n0 n1)"
1.221 -  and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)"
1.222 -  and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0
1.223 -                             else degreen p m + degreen q m)"
1.224 +    and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)"
1.225 +    and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 else degreen p m + degreen q m)"
1.226    using np nq m
1.227 -proof(induct p q arbitrary: n0 n1 m rule: polymul.induct)
1.228 +proof (induct p q arbitrary: n0 n1 m rule: polymul.induct)
1.229    case (2 c c' n' p')
1.230    { case (1 n0 n1)
1.231      with "2.hyps"(4-6)[of n' n' n']
1.232 @@ -430,7 +442,7 @@
1.233          with "4.hyps"(16-17)[OF cnp np', of "n'"]
1.234            "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp'
1.235          have ?case
1.236 -          by (cases "Suc n' = n", simp_all add: min_def)
1.237 +          by (cases "Suc n' = n") (simp_all add: min_def)
1.238        } moreover {
1.239          assume "n' = n"
1.240          with "4.hyps"(16-17)[OF cnp np', of n]
1.241 @@ -525,35 +537,41 @@
1.242  qed auto
1.243
1.244  lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)"
1.245 -by(induct p q rule: polymul.induct, auto simp add: field_simps)
1.246 +  by (induct p q rule: polymul.induct) (auto simp add: field_simps)
1.247
1.248  lemma polymul_normh:
1.249 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.250 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.251    shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
1.252    using polymul_properties(1)  by blast
1.253 +
1.254  lemma polymul_eq0_iff:
1.255    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.256    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p) "
1.257    using polymul_properties(2)  by blast
1.258 -lemma polymul_degreen:
1.259 +
1.260 +lemma polymul_degreen:  (* FIXME duplicate? *)
1.261    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.262 -  shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 else degreen p m + degreen q m)"
1.263 +  shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow>
1.264 +    degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 else degreen p m + degreen q m)"
1.265    using polymul_properties(3) by blast
1.266 +
1.267  lemma polymul_norm:
1.268    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.269    shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul p q)"
1.270    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
1.271
1.272  lemma headconst_zero: "isnpolyh p n0 \<Longrightarrow> headconst p = 0\<^sub>N \<longleftrightarrow> p = 0\<^sub>p"
1.273 -  by (induct p arbitrary: n0 rule: headconst.induct, auto)
1.274 +  by (induct p arbitrary: n0 rule: headconst.induct) auto
1.275
1.277 -  by (induct p arbitrary: n0, auto)
1.278 +  by (induct p arbitrary: n0) auto
1.279
1.280 -lemma monic_eqI: assumes np: "isnpolyh p n0"
1.281 -  shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
1.282 +lemma monic_eqI:
1.283 +  assumes np: "isnpolyh p n0"
1.284 +  shows "INum (headconst p) * Ipoly bs (fst (monic p)) =
1.285 +    (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
1.286    unfolding monic_def Let_def
1.289    let ?h = "headconst p"
1.290    assume pz: "p \<noteq> 0\<^sub>p"
1.291    {assume hz: "INum ?h = (0::'a)"
1.292 @@ -567,14 +585,14 @@
1.293  text{* polyneg is a negation and preserves normal forms *}
1.294
1.295  lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
1.296 -by (induct p rule: polyneg.induct, auto)
1.297 +  by (induct p rule: polyneg.induct) auto
1.298
1.299  lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)"
1.300 -  by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def)
1.301 +  by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: Nneg_def)
1.302  lemma polyneg_polyneg: "isnpolyh p n0 \<Longrightarrow> ~\<^sub>p (~\<^sub>p p) = p"
1.303 -  by (induct p arbitrary: n0 rule: polyneg.induct, auto)
1.304 +  by (induct p arbitrary: n0 rule: polyneg.induct) auto
1.305  lemma polyneg_normh: "\<And>n. isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n "
1.306 -by (induct p rule: polyneg.induct, auto simp add: polyneg0)
1.307 +  by (induct p rule: polyneg.induct) (auto simp add: polyneg0)
1.308
1.309  lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)"
1.310    using isnpoly_def polyneg_normh by simp
1.311 @@ -583,29 +601,31 @@
1.312  text{* polysub is a substraction and preserves normal forms *}
1.313
1.314  lemma polysub[simp]: "Ipoly bs (polysub p q) = (Ipoly bs p) - (Ipoly bs q)"
1.316 +  by (simp add: polysub_def)
1.317  lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub p q) (min n0 n1)"
1.320
1.321  lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub p q)"
1.323 -lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.324 +lemma polysub_same_0[simp]:
1.325 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.326    shows "isnpolyh p n0 \<Longrightarrow> polysub p p = 0\<^sub>p"
1.327 -unfolding polysub_def split_def fst_conv snd_conv
1.328 -by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])
1.329 +  unfolding polysub_def split_def fst_conv snd_conv
1.330 +  by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def])
1.331
1.332  lemma polysub_0:
1.333    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.334    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
1.335    unfolding polysub_def split_def fst_conv snd_conv
1.336    by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
1.337 -  (auto simp: Nsub0[simplified Nsub_def] Let_def)
1.338 +    (auto simp: Nsub0[simplified Nsub_def] Let_def)
1.339
1.340  text{* polypow is a power function and preserves normal forms *}
1.341
1.342  lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n"
1.343 -proof(induct n rule: polypow.induct)
1.344 -  case 1 thus ?case by simp
1.345 +proof (induct n rule: polypow.induct)
1.346 +  case 1
1.347 +  thus ?case by simp
1.348  next
1.349    case (2 n)
1.350    let ?q = "polypow ((Suc n) div 2) p"
1.351 @@ -613,19 +633,21 @@
1.352    have "odd (Suc n) \<or> even (Suc n)" by simp
1.353    moreover
1.354    {assume odd: "odd (Suc n)"
1.355 -    have th: "(Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat))))) = Suc n div 2 + Suc n div 2 + 1" by arith
1.356 +    have th: "(Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat))))) = Suc n div 2 + Suc n div 2 + 1"
1.357 +      by arith
1.358      from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" by (simp add: Let_def)
1.359      also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)"
1.360        using "2.hyps" by simp
1.361      also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
1.362 -      apply (simp only: power_add power_one_right) by simp
1.363 +      by (simp only: power_add power_one_right) simp
1.364      also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat)))))"
1.365        by (simp only: th)
1.366      finally have ?case
1.367      using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp  }
1.368    moreover
1.369    {assume even: "even (Suc n)"
1.370 -    have th: "(Suc (Suc (0\<Colon>nat))) * (Suc n div Suc (Suc (0\<Colon>nat))) = Suc n div 2 + Suc n div 2" by arith
1.371 +    have th: "(Suc (Suc (0\<Colon>nat))) * (Suc n div Suc (Suc (0\<Colon>nat))) = Suc n div 2 + Suc n div 2"
1.372 +      by arith
1.373      from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def)
1.374      also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"
1.375        using "2.hyps" apply (simp only: power_add) by simp
1.376 @@ -634,7 +656,7 @@
1.377  qed
1.378
1.379  lemma polypow_normh:
1.380 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.381 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.382    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
1.383  proof (induct k arbitrary: n rule: polypow.induct)
1.384    case (2 k n)
1.385 @@ -653,23 +675,28 @@
1.386
1.387  text{* Finally the whole normalization *}
1.388
1.389 -lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
1.390 -by (induct p rule:polynate.induct, auto)
1.391 +lemma polynate [simp]:
1.392 +  "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
1.393 +  by (induct p rule:polynate.induct) auto
1.394
1.395  lemma polynate_norm[simp]:
1.396    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.397    shows "isnpoly (polynate p)"
1.398 -  by (induct p rule: polynate.induct, simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm) (simp_all add: isnpoly_def)
1.399 +  by (induct p rule: polynate.induct)
1.402
1.403  text{* shift1 *}
1.404
1.405
1.406  lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
1.407 -by (simp add: shift1_def polymul)
1.408 +  by (simp add: shift1_def)
1.409
1.410  lemma shift1_isnpoly:
1.411 -  assumes pn: "isnpoly p" and pnz: "p \<noteq> 0\<^sub>p" shows "isnpoly (shift1 p) "
1.412 -  using pn pnz by (simp add: shift1_def isnpoly_def )
1.413 +  assumes pn: "isnpoly p"
1.414 +    and pnz: "p \<noteq> 0\<^sub>p"
1.415 +  shows "isnpoly (shift1 p) "
1.416 +  using pn pnz by (simp add: shift1_def isnpoly_def)
1.417
1.418  lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p"
1.420 @@ -678,18 +705,22 @@
1.421    by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
1.422
1.423  lemma funpow_isnpolyh:
1.424 -  assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n"
1.425 +  assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
1.426 +    and np: "isnpolyh p n"
1.427    shows "isnpolyh (funpow k f p) n"
1.428 -  using f np by (induct k arbitrary: p, auto)
1.429 +  using f np by (induct k arbitrary: p) auto
1.430
1.431 -lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
1.432 -  by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
1.433 +lemma funpow_shift1:
1.434 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) =
1.435 +    Ipoly bs (Mul (Pw (Bound 0) n) p)"
1.436 +  by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
1.437
1.438  lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
1.439    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
1.440
1.441  lemma funpow_shift1_1:
1.442 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
1.443 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) =
1.444 +    Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
1.446
1.447  lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
1.448 @@ -697,23 +728,29 @@
1.449
1.451    assumes np: "isnpolyh p n"
1.452 -  shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})"
1.453 +  shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
1.454 +    (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})"
1.455    using np
1.456  proof (induct p arbitrary: n rule: behead.induct)
1.457    case (1 c p n) hence pn: "isnpolyh p n" by simp
1.458    from 1(1)[OF pn]
1.459    have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" .
1.460 -  then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
1.461 -    by (simp_all add: th[symmetric] field_simps power_Suc)
1.462 +  then show ?case using "1.hyps"
1.464 +    apply (simp_all add: th[symmetric] field_simps)
1.465 +    done
1.466  qed (auto simp add: Let_def)
1.467
1.469 -  assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n"
1.470 -  using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono)
1.471 +  assumes np: "isnpolyh p n"
1.472 +  shows "isnpolyh (behead p) n"
1.473 +  using np by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)
1.474 +
1.475
1.476  subsection{* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
1.477 +
1.478  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
1.479 -proof(induct p arbitrary: n rule: poly.induct, auto)
1.480 +proof (induct p arbitrary: n rule: poly.induct, auto)
1.481    case (goal1 c n p n')
1.482    hence "n = Suc (n - 1)" by simp
1.483    hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
1.484 @@ -721,27 +758,29 @@
1.485  qed
1.486
1.487  lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p"
1.488 -by (induct p arbitrary: n0 rule: isconstant.induct, auto simp add: isnpolyh_polybound0)
1.489 +  by (induct p arbitrary: n0 rule: isconstant.induct) (auto simp add: isnpolyh_polybound0)
1.490
1.491 -lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p" by (induct p, auto)
1.492 +lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p"
1.493 +  by (induct p) auto
1.494
1.495  lemma decrpoly_normh: "isnpolyh p n0 \<Longrightarrow> polybound0 p \<Longrightarrow> isnpolyh (decrpoly p) (n0 - 1)"
1.496 -  apply (induct p arbitrary: n0, auto)
1.497 +  apply (induct p arbitrary: n0)
1.498 +  apply auto
1.499    apply (atomize)
1.500    apply (erule_tac x = "Suc nat" in allE)
1.501    apply auto
1.502    done
1.503
1.505 - by (induct p  arbitrary: n0 rule: head.induct, auto intro: isnpolyh_polybound0)
1.506 +  by (induct p  arbitrary: n0 rule: head.induct) (auto intro: isnpolyh_polybound0)
1.507
1.508  lemma polybound0_I:
1.509    assumes nb: "polybound0 a"
1.510    shows "Ipoly (b#bs) a = Ipoly (b'#bs) a"
1.511 -using nb
1.512 -by (induct a rule: poly.induct) auto
1.513 -lemma polysubst0_I:
1.514 -  shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
1.515 +  using nb
1.516 +  by (induct a rule: poly.induct) auto
1.517 +
1.518 +lemma polysubst0_I: "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
1.519    by (induct t) simp_all
1.520
1.521  lemma polysubst0_I':
1.522 @@ -749,16 +788,18 @@
1.523    shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b'#bs) a)#bs) t"
1.524    by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"])
1.525
1.526 -lemma decrpoly: assumes nb: "polybound0 t"
1.527 +lemma decrpoly:
1.528 +  assumes nb: "polybound0 t"
1.529    shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)"
1.530 -  using nb by (induct t rule: decrpoly.induct, simp_all)
1.531 +  using nb by (induct t rule: decrpoly.induct) simp_all
1.532
1.533 -lemma polysubst0_polybound0: assumes nb: "polybound0 t"
1.534 +lemma polysubst0_polybound0:
1.535 +  assumes nb: "polybound0 t"
1.536    shows "polybound0 (polysubst0 t a)"
1.537 -using nb by (induct a rule: poly.induct, auto)
1.538 +  using nb by (induct a rule: poly.induct) auto
1.539
1.540  lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
1.541 -  by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0)
1.542 +  by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0)
1.543
1.544  primrec maxindex :: "poly \<Rightarrow> nat" where
1.545    "maxindex (Bound n) = n + 1"
1.546 @@ -770,11 +811,11 @@
1.547  | "maxindex (Pw p n) = maxindex p"
1.548  | "maxindex (C x) = 0"
1.549
1.550 -definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool" where
1.551 -  "wf_bs bs p = (length bs \<ge> maxindex p)"
1.552 +definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool"
1.553 +  where "wf_bs bs p = (length bs \<ge> maxindex p)"
1.554
1.555  lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall> c \<in> set (coefficients p). wf_bs bs c"
1.556 -proof(induct p rule: coefficients.induct)
1.557 +proof (induct p rule: coefficients.induct)
1.558    case (1 c p)
1.559    show ?case
1.560    proof
1.561 @@ -791,12 +832,13 @@
1.562  qed simp_all
1.563
1.564  lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"
1.565 -by (induct p rule: coefficients.induct, auto)
1.566 +  by (induct p rule: coefficients.induct) auto
1.567
1.568  lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p"
1.569 -  unfolding wf_bs_def by (induct p, auto simp add: nth_append)
1.570 +  unfolding wf_bs_def by (induct p) (auto simp add: nth_append)
1.571
1.572 -lemma take_maxindex_wf: assumes wf: "wf_bs bs p"
1.573 +lemma take_maxindex_wf:
1.574 +  assumes wf: "wf_bs bs p"
1.575    shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p"
1.576  proof-
1.577    let ?ip = "maxindex p"
1.578 @@ -808,7 +850,7 @@
1.579  qed
1.580
1.581  lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1"
1.582 -  by (induct p, auto)
1.583 +  by (induct p) auto
1.584
1.585  lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
1.586    unfolding wf_bs_def by simp
1.587 @@ -819,22 +861,28 @@
1.588
1.589
1.590  lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"
1.591 -by(induct p rule: coefficients.induct, auto simp add: wf_bs_def)
1.592 +  by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def)
1.593  lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"
1.594 -  by (induct p rule: coefficients.induct, simp_all)
1.595 +  by (induct p rule: coefficients.induct) simp_all
1.596
1.597
1.599 -  by (induct p rule: coefficients.induct, auto)
1.600 +  by (induct p rule: coefficients.induct) auto
1.601
1.602  lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p"
1.603 -  unfolding wf_bs_def by (induct p rule: decrpoly.induct, auto)
1.604 +  unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto
1.605
1.606  lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists> ys. length (xs @ ys) = n"
1.607    apply (rule exI[where x="replicate (n - length xs) z"])
1.608 -  by simp
1.609 +  apply simp
1.610 +  done
1.611 +
1.612  lemma isnpolyh_Suc_const:"isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
1.613 -by (cases p, auto) (case_tac "nat", simp_all)
1.614 +  apply (cases p)
1.615 +  apply auto
1.616 +  apply (case_tac "nat")
1.617 +  apply simp_all
1.618 +  done
1.619
1.620  lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)"
1.621    unfolding wf_bs_def
1.622 @@ -852,11 +900,12 @@
1.623    done
1.624
1.625  lemma wf_bs_polyneg: "wf_bs bs p \<Longrightarrow> wf_bs bs (~\<^sub>p p)"
1.626 -  unfolding wf_bs_def by (induct p rule: polyneg.induct, auto)
1.627 +  unfolding wf_bs_def by (induct p rule: polyneg.induct) auto
1.628
1.629  lemma wf_bs_polysub: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p -\<^sub>p q)"
1.630    unfolding polysub_def split_def fst_conv snd_conv using wf_bs_polyadd wf_bs_polyneg by blast
1.631
1.632 +
1.633  subsection{* Canonicity of polynomial representation, see lemma isnpolyh_unique*}
1.634
1.635  definition "polypoly bs p = map (Ipoly bs) (coefficients p)"
1.636 @@ -874,8 +923,8 @@
1.637
1.638  lemma coefficients_isconst:
1.639    "isnpolyh p n \<Longrightarrow> \<forall>q\<in>set (coefficients p). isconstant q"
1.640 -  by (induct p arbitrary: n rule: coefficients.induct,
1.641 -    auto simp add: isnpolyh_Suc_const)
1.642 +  by (induct p arbitrary: n rule: coefficients.induct)
1.643 +    (auto simp add: isnpolyh_Suc_const)
1.644
1.645  lemma polypoly_polypoly':
1.646    assumes np: "isnpolyh p n0"
1.647 @@ -896,12 +945,14 @@
1.648  qed
1.649
1.650  lemma polypoly_poly:
1.651 -  assumes np: "isnpolyh p n0" shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x"
1.652 +  assumes np: "isnpolyh p n0"
1.653 +  shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x"
1.654    using np
1.655 -by (induct p arbitrary: n0 bs rule: coefficients.induct, auto simp add: polypoly_def)
1.656 +  by (induct p arbitrary: n0 bs rule: coefficients.induct) (auto simp add: polypoly_def)
1.657
1.658  lemma polypoly'_poly:
1.659 -  assumes np: "isnpolyh p n0" shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x"
1.660 +  assumes np: "isnpolyh p n0"
1.661 +  shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x"
1.662    using polypoly_poly[OF np, simplified polypoly_polypoly'[OF np]] .
1.663
1.664
1.665 @@ -909,29 +960,34 @@
1.666    assumes np: "isnpolyh p n0" and nb: "polybound0 p"
1.667    shows "polypoly bs p = [Ipoly bs p]"
1.668    using np nb unfolding polypoly_def
1.669 -  by (cases p, auto, case_tac nat, auto)
1.670 +  apply (cases p)
1.671 +  apply auto
1.672 +  apply (case_tac nat)
1.673 +  apply auto
1.674 +  done
1.675
1.677 -  by (induct p rule: head.induct, auto)
1.678 +  by (induct p rule: head.induct) auto
1.679
1.680  lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)"
1.681 -  by (cases p,auto)
1.682 +  by (cases p) auto
1.683
1.685 -  by (induct p rule: head.induct, simp_all)
1.686 +  by (induct p rule: head.induct) simp_all
1.687
1.688  lemma head_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (head p = 0\<^sub>p) = (p = 0\<^sub>p)"
1.690
1.691  lemma isnpolyh_zero_iff:
1.692 -  assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, field_inverse_zero, power})"
1.693 +  assumes nq: "isnpolyh p n0"
1.694 +    and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, field_inverse_zero, power})"
1.695    shows "p = 0\<^sub>p"
1.696 -using nq eq
1.697 +  using nq eq
1.698  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
1.699    case less
1.700    note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)`
1.701    {assume nz: "maxindex p = 0"
1.702 -    then obtain c where "p = C c" using np by (cases p, auto)
1.703 +    then obtain c where "p = C c" using np by (cases p) auto
1.704      with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp}
1.705    moreover
1.706    {assume nz: "maxindex p \<noteq> 0"
1.707 @@ -958,7 +1014,7 @@
1.708        hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp
1.709        with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]
1.710        have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
1.711 -      hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext)
1.712 +      hence "poly (polypoly' (?ts @ xs) p) = poly []" by auto
1.713        hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
1.714          using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
1.716 @@ -975,7 +1031,8 @@
1.717  qed
1.718
1.719  lemma isnpolyh_unique:
1.720 -  assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"
1.721 +  assumes np:"isnpolyh p n0"
1.722 +    and nq: "isnpolyh q n1"
1.723    shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0, field_inverse_zero, power})) \<longleftrightarrow>  p = q"
1.724  proof(auto)
1.725    assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
1.726 @@ -989,69 +1046,91 @@
1.727
1.728  text{* consequences of unicity on the algorithms for polynomial normalization *}
1.729
1.730 -lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.731 -  and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
1.733 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.734 +    and np: "isnpolyh p n0"
1.735 +    and nq: "isnpolyh q n1"
1.736 +  shows "p +\<^sub>p q = q +\<^sub>p p"
1.738
1.739  lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
1.740  lemma one_normh: "isnpolyh (1)\<^sub>p n" by simp
1.741 +
1.743    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.744 -  and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
1.745 +    and np: "isnpolyh p n0"
1.746 +  shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
1.747    using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np]
1.748      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
1.749
1.750  lemma polymul_1[simp]:
1.751 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.752 -  and np: "isnpolyh p n0" shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p"
1.753 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.754 +    and np: "isnpolyh p n0"
1.755 +  shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p"
1.756    using isnpolyh_unique[OF polymul_normh[OF np one_normh] np]
1.757      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
1.758 +
1.759  lemma polymul_0[simp]:
1.760    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.761 -  and np: "isnpolyh p n0" shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
1.762 +    and np: "isnpolyh p n0"
1.763 +  shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
1.764    using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh]
1.765      isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
1.766
1.767  lemma polymul_commute:
1.768 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.769 -  and np:"isnpolyh p n0" and nq: "isnpolyh q n1"
1.770 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.771 +    and np:"isnpolyh p n0"
1.772 +    and nq: "isnpolyh q n1"
1.773    shows "p *\<^sub>p q = q *\<^sub>p p"
1.774 -using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{field_char_0, field_inverse_zero, power}"] by simp
1.775 +  using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{field_char_0, field_inverse_zero, power}"]
1.776 +  by simp
1.777
1.778 -declare polyneg_polyneg[simp]
1.779 +declare polyneg_polyneg [simp]
1.780
1.781 -lemma isnpolyh_polynate_id[simp]:
1.782 +lemma isnpolyh_polynate_id [simp]:
1.783    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.784 -  and np:"isnpolyh p n0" shows "polynate p = p"
1.785 -  using isnpolyh_unique[where ?'a= "'a::{field_char_0, field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0, field_inverse_zero}"] by simp
1.786 +    and np:"isnpolyh p n0"
1.787 +  shows "polynate p = p"
1.788 +  using isnpolyh_unique[where ?'a= "'a::{field_char_0, field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0, field_inverse_zero}"]
1.789 +  by simp
1.790
1.791  lemma polynate_idempotent[simp]:
1.792 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.793 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.794    shows "polynate (polynate p) = polynate p"
1.795    using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
1.796
1.797  lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
1.798    unfolding poly_nate_def polypoly'_def ..
1.799 -lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0, field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
1.800 +
1.801 +lemma poly_nate_poly:
1.802 +  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0, field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
1.803    using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
1.804 -  unfolding poly_nate_polypoly' by (auto intro: ext)
1.805 +  unfolding poly_nate_polypoly' by auto
1.806 +
1.807
1.808  subsection{* heads, degrees and all that *}
1.809 +
1.810  lemma degree_eq_degreen0: "degree p = degreen p 0"
1.811 -  by (induct p rule: degree.induct, simp_all)
1.812 +  by (induct p rule: degree.induct) simp_all
1.813
1.814 -lemma degree_polyneg: assumes n: "isnpolyh p n"
1.815 +lemma degree_polyneg:
1.816 +  assumes n: "isnpolyh p n"
1.817    shows "degree (polyneg p) = degree p"
1.818 -  using n
1.819 -  by (induct p arbitrary: n rule: polyneg.induct, simp_all) (case_tac na, auto)
1.820 +  apply (induct p arbitrary: n rule: polyneg.induct)
1.821 +  using n apply simp_all
1.822 +  apply (case_tac na)
1.823 +  apply auto
1.824 +  done
1.825
1.827    assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
1.828    shows "degree (p +\<^sub>p q) \<le> max (degree p) (degree q)"
1.829 -using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp
1.830 +  using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp
1.831
1.832
1.833 -lemma degree_polysub: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
1.834 +lemma degree_polysub:
1.835 +  assumes np: "isnpolyh p n0"
1.836 +    and nq: "isnpolyh q n1"
1.837    shows "degree (p -\<^sub>p q) \<le> max (degree p) (degree q)"
1.838  proof-
1.839    from nq have nq': "isnpolyh (~\<^sub>p q) n1" using polyneg_normh by simp
1.840 @@ -1060,24 +1139,25 @@
1.841
1.843    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.844 -  and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q"
1.845 -  and d: "degree p = degree q"
1.846 +    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q"
1.847 +    and d: "degree p = degree q"
1.848    shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
1.849 -unfolding polysub_def split_def fst_conv snd_conv
1.850 -using np nq h d
1.852 -  case (1 c c') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def])
1.853 +  unfolding polysub_def split_def fst_conv snd_conv
1.854 +  using np nq h d
1.855 +proof (induct p q rule: polyadd.induct)
1.856 +  case (1 c c')
1.857 +  thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def])
1.858  next
1.859    case (2 c c' n' p')
1.860    from 2 have "degree (C c) = degree (CN c' n' p')" by simp
1.861 -  hence nz:"n' > 0" by (cases n', auto)
1.862 -  hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
1.863 +  hence nz:"n' > 0" by (cases n') auto
1.864 +  hence "head (CN c' n' p') = CN c' n' p'" by (cases n') auto
1.865    with 2 show ?case by simp
1.866  next
1.867    case (3 c n p c')
1.868    hence "degree (C c') = degree (CN c n p)" by simp
1.869 -  hence nz:"n > 0" by (cases n, auto)
1.870 -  hence "head (CN c n p) = CN c n p" by (cases n, auto)
1.871 +  hence nz:"n > 0" by (cases n) auto
1.872 +  hence "head (CN c n p) = CN c n p" by (cases n) auto
1.873    with 3 show ?case by simp
1.874  next
1.875    case (4 c n p c' n' p')
1.876 @@ -1096,36 +1176,43 @@
1.877      moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')}
1.878      moreover {assume nz: "n > 0"
1.879        with nn' H(3) have  cc':"c = c'" and pp': "p = p'" by (cases n, auto)+
1.880 -      hence ?case using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] polysub_same_0[OF c'nh, simplified polysub_def] using nn' 4 by (simp add: Let_def)}
1.881 +      hence ?case
1.882 +        using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] polysub_same_0[OF c'nh, simplified polysub_def]
1.883 +        using nn' 4 by (simp add: Let_def)}
1.884      ultimately have ?case by blast}
1.885    moreover
1.886    {assume nn': "n < n'" hence n'p: "n' > 0" by simp
1.887 -    hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n', simp_all)
1.888 -    have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" using 4 nn' by (cases n', simp_all)
1.889 -    hence "n > 0" by (cases n, simp_all)
1.890 -    hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto)
1.891 +    hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n') simp_all
1.892 +    have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')"
1.893 +      using 4 nn' by (cases n', simp_all)
1.894 +    hence "n > 0" by (cases n) simp_all
1.895 +    hence headcnp: "head (CN c n p) = CN c n p" by (cases n) auto
1.897    moreover
1.898    {assume nn': "n > n'"  hence np: "n > 0" by simp
1.899 -    hence headcnp:"head (CN c n p) = CN c n p"  by (cases n, simp_all)
1.900 +    hence headcnp:"head (CN c n p) = CN c n p"  by (cases n) simp_all
1.901      from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
1.902 -    from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all)
1.903 -    with degcnpeq have "n' > 0" by (cases n', simp_all)
1.904 -    hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
1.905 +    from np have degcnp: "degree (CN c n p) = 0" by (cases n) simp_all
1.906 +    with degcnpeq have "n' > 0" by (cases n') simp_all
1.907 +    hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n') auto
1.909    ultimately show ?case  by blast
1.910  qed auto
1.911
1.914 +  by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def)
1.915
1.916  lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
1.917 -proof(induct k arbitrary: n0 p)
1.918 -  case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
1.919 +proof (induct k arbitrary: n0 p)
1.920 +  case 0
1.921 +  thus ?case by auto
1.922 +next
1.923 +  case (Suc k n0 p)
1.924 +  hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
1.925    with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
1.927    thus ?case by (simp add: funpow_swap1)
1.928 -qed auto
1.929 +qed
1.930
1.931  lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
1.933 @@ -1133,47 +1220,52 @@
1.934    by (induct k arbitrary: p) (auto simp add: shift1_degree)
1.935
1.936  lemma funpow_shift1_nz: "p \<noteq> 0\<^sub>p \<Longrightarrow> funpow n shift1 p \<noteq> 0\<^sub>p"
1.937 -  by (induct n arbitrary: p) (simp_all add: funpow.simps)
1.938 +  by (induct n arbitrary: p) simp_all
1.939
1.940  lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> head p = p"
1.941 -  by (induct p arbitrary: n rule: degree.induct, auto)
1.942 +  by (induct p arbitrary: n rule: degree.induct) auto
1.943  lemma headn_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> headn p m = p"
1.944 -  by (induct p arbitrary: n rule: degreen.induct, auto)
1.945 +  by (induct p arbitrary: n rule: degreen.induct) auto
1.946  lemma head_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> head p = p"
1.947 -  by (induct p arbitrary: n rule: degree.induct, auto)
1.948 +  by (induct p arbitrary: n rule: degree.induct) auto
1.950 -  by (induct p rule: head.induct, auto)
1.951 +  by (induct p rule: head.induct) auto
1.952
1.954 -  "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\<rbrakk> \<Longrightarrow> degree p = degree q"
1.955 +  "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> polyadd p q = C c \<Longrightarrow> degree p = degree q"
1.956    using polyadd_eq_const_degreen degree_eq_degreen0 by simp
1.957
1.958 -lemma polyadd_head: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
1.959 -  and deg: "degree p \<noteq> degree q"
1.961 +  assumes np: "isnpolyh p n0"
1.962 +    and nq: "isnpolyh q n1"
1.963 +    and deg: "degree p \<noteq> degree q"
1.964    shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)"
1.965 -using np nq deg
1.966 -apply(induct p q arbitrary: n0 n1 rule: polyadd.induct,simp_all)
1.967 -apply (case_tac n', simp, simp)
1.968 -apply (case_tac n, simp, simp)
1.969 -apply (case_tac n, case_tac n', simp add: Let_def)
1.970 -apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
1.974 -apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
1.975 -by (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
1.976 +  using np nq deg
1.977 +  apply (induct p q arbitrary: n0 n1 rule: polyadd.induct)
1.978 +  using np
1.979 +  apply simp_all
1.980 +  apply (case_tac n', simp, simp)
1.981 +  apply (case_tac n, simp, simp)
1.982 +  apply (case_tac n, case_tac n', simp add: Let_def)
1.983 +  apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
1.987 +  apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
1.988 +  apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
1.989 +  done
1.990
1.992 -   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.993 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.994    shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
1.995  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
1.996    case (2 c c' n' p' n0 n1)
1.998 -  thus ?case using 2 by (cases n', auto)
1.999 +  thus ?case using 2 by (cases n') auto
1.1000  next
1.1001    case (3 c n p c' n0 n1)
1.1003 -  thus ?case using 3 by (cases n, auto)
1.1004 +  thus ?case using 3 by (cases n) auto
1.1005  next
1.1006    case (4 c n p c' n' p' n0 n1)
1.1007    hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
1.1008 @@ -1182,13 +1274,22 @@
1.1009    have "n < n' \<or> n' < n \<or> n = n'" by arith
1.1010    moreover
1.1011    {assume nn': "n < n'" hence ?case
1.1012 -      using norm
1.1013 -    "4.hyps"(2)[OF norm(1,6)]
1.1014 -    "4.hyps"(1)[OF norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
1.1015 +      using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)]
1.1016 +      apply simp
1.1017 +      apply (cases n)
1.1018 +      apply simp
1.1019 +      apply (cases n')
1.1020 +      apply simp_all
1.1021 +      done }
1.1022    moreover {assume nn': "n'< n"
1.1023 -    hence ?case using norm "4.hyps"(6) [OF norm(5,3)]
1.1024 -      "4.hyps"(5)[OF norm(5,4)]
1.1025 -      by (simp,cases n',simp,cases n,auto)}
1.1026 +    hence ?case
1.1027 +      using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)]
1.1028 +      apply simp
1.1029 +      apply (cases n')
1.1030 +      apply simp
1.1031 +      apply (cases n)
1.1032 +      apply auto
1.1033 +      done }
1.1034    moreover {assume nn': "n' = n"
1.1035      from nn' polymul_normh[OF norm(5,4)]
1.1036      have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)
1.1037 @@ -1218,44 +1319,50 @@
1.1038  qed simp_all
1.1039
1.1040  lemma degree_coefficients: "degree p = length (coefficients p) - 1"
1.1041 -  by(induct p rule: degree.induct, auto)
1.1042 +  by (induct p rule: degree.induct) auto
1.1043
1.1045 -  by (induct p rule: head.induct, auto)
1.1046 +  by (induct p rule: head.induct) auto
1.1047
1.1048  lemma degree_CN: "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<le> 1 + degree p"
1.1049 -  by (cases n, simp_all)
1.1050 +  by (cases n) simp_all
1.1051  lemma degree_CN': "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<ge>  degree p"
1.1052 -  by (cases n, simp_all)
1.1053 +  by (cases n) simp_all
1.1054
1.1055 -lemma polyadd_different_degree: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degree p \<noteq> degree q\<rbrakk> \<Longrightarrow> degree (polyadd p q) = max (degree p) (degree q)"
1.1057 +  "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degree p \<noteq> degree q\<rbrakk> \<Longrightarrow>
1.1058 +    degree (polyadd p q) = max (degree p) (degree q)"
1.1059    using polyadd_different_degreen degree_eq_degreen0 by simp
1.1060
1.1061  lemma degreen_polyneg: "isnpolyh p n0 \<Longrightarrow> degreen (~\<^sub>p p) m = degreen p m"
1.1062 -  by (induct p arbitrary: n0 rule: polyneg.induct, auto)
1.1063 +  by (induct p arbitrary: n0 rule: polyneg.induct) auto
1.1064
1.1065  lemma degree_polymul:
1.1066    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.1067 -  and np: "isnpolyh p n0" and nq: "isnpolyh q n1"
1.1068 +    and np: "isnpolyh p n0"
1.1069 +    and nq: "isnpolyh q n1"
1.1070    shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
1.1071    using polymul_degreen[OF np nq, where m="0"]  degree_eq_degreen0 by simp
1.1072
1.1073  lemma polyneg_degree: "isnpolyh p n \<Longrightarrow> degree (polyneg p) = degree p"
1.1074 -  by (induct p arbitrary: n rule: degree.induct, auto)
1.1075 +  by (induct p arbitrary: n rule: degree.induct) auto
1.1076
1.1078 -  by (induct p arbitrary: n rule: degree.induct, auto)
1.1079 +  by (induct p arbitrary: n rule: degree.induct) auto
1.1080 +
1.1081
1.1082  subsection {* Correctness of polynomial pseudo division *}
1.1083
1.1084  lemma polydivide_aux_properties:
1.1085    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.1086 -  and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
1.1087 -  and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
1.1088 +    and np: "isnpolyh p n0"
1.1089 +    and ns: "isnpolyh s n1"
1.1090 +    and ap: "head p = a"
1.1091 +    and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
1.1092    shows "(polydivide_aux a n p k s = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p)
1.1093            \<and> (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
1.1094    using ns
1.1095 -proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
1.1096 +proof (induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
1.1097    case less
1.1098    let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
1.1099    let ?ths = "polydivide_aux a n p k s = (k', r) \<longrightarrow>  k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p)
1.1100 @@ -1272,12 +1379,20 @@
1.1101    from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
1.1102    from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap
1.1103    have nakk':"isnpolyh ?akk' 0" by blast
1.1104 -  {assume sz: "s = 0\<^sub>p"
1.1105 -   hence ?ths using np polydivide_aux.simps apply clarsimp by (rule exI[where x="0\<^sub>p"], simp) }
1.1106 +  { assume sz: "s = 0\<^sub>p"
1.1107 +    hence ?ths using np polydivide_aux.simps
1.1108 +      apply clarsimp
1.1109 +      apply (rule exI[where x="0\<^sub>p"])
1.1110 +      apply simp
1.1111 +      done }
1.1112    moreover
1.1113    {assume sz: "s \<noteq> 0\<^sub>p"
1.1114      {assume dn: "degree s < n"
1.1115 -      hence "?ths" using ns ndp np polydivide_aux.simps by auto (rule exI[where x="0\<^sub>p"],simp) }
1.1116 +      hence "?ths" using ns ndp np polydivide_aux.simps
1.1117 +        apply auto
1.1118 +        apply (rule exI[where x="0\<^sub>p"])
1.1119 +        apply simp
1.1120 +        done }
1.1121      moreover
1.1122      {assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> n" by arith
1.1123        have degsp': "degree s = degree ?p'"
1.1124 @@ -1332,9 +1447,14 @@
1.1125          {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
1.1126            from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0, field_inverse_zero}"]
1.1127            have " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp
1.1128 -          hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
1.1129 -            by (simp only: funpow_shift1_1) simp
1.1130 -          hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
1.1131 +          hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
1.1132 +            using np nxdn
1.1133 +            apply simp
1.1134 +            apply (simp only: funpow_shift1_1)
1.1135 +            apply simp
1.1136 +            done
1.1137 +          hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
1.1138 +            by blast
1.1139            {assume h1: "polydivide_aux a n p k s = (k',r)"
1.1140              from polydivide_aux.simps sz dn' ba
1.1141              have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
1.1142 @@ -1385,12 +1505,16 @@
1.1143              {fix bs:: "'a::{field_char_0, field_inverse_zero} list"
1.1144
1.1145              from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
1.1146 -            have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
1.1147 -            hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r"
1.1148 -              by (simp add: field_simps power_Suc)
1.1149 -            hence "Ipoly bs a ^ (k' - k)  * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r"
1.1150 -              by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
1.1151 -            hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
1.1152 +            have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)"
1.1153 +              by simp
1.1154 +            hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s =
1.1155 +              Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r"
1.1156 +              by (simp add: field_simps)
1.1157 +            hence "Ipoly bs a ^ (k' - k)  * Ipoly bs s =
1.1158 +              Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r"
1.1159 +              by (simp add: kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
1.1160 +            hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.1161 +              Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
1.1163              hence ieq:"\<forall>(bs :: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.1164                Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto
1.1165 @@ -1415,7 +1539,8 @@
1.1166              by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
1.1167            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
1.1168          }
1.1169 -        hence hth: "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
1.1170 +        hence hth: "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) =
1.1171 +            Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
1.1172            from hth
1.1173            have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
1.1174              using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.1175 @@ -1426,17 +1551,20 @@
1.1176            have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
1.1177            with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
1.1178              polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
1.1179 -          have ?ths apply (clarsimp simp add: Let_def)
1.1180 -            apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
1.1181 +          have ?ths
1.1182 +            apply (clarsimp simp add: Let_def)
1.1183 +            apply (rule exI[where x="?b *\<^sub>p ?xdn"])
1.1184 +            apply simp
1.1185              apply (rule exI[where x="0"], simp)
1.1186 -            done}
1.1187 -        hence ?ths by blast}
1.1188 -        ultimately have ?ths using  degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth] polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
1.1189 -          head_nz[OF np] pnz sz ap[symmetric]
1.1190 +            done }
1.1191 +        hence ?ths by blast }
1.1192 +        ultimately have ?ths
1.1194 +            head_nz[OF np] pnz sz ap[symmetric]
1.1195            by (simp add: degree_eq_degreen0[symmetric]) blast }
1.1196        ultimately have ?ths by blast
1.1197      }
1.1198 -    ultimately have ?ths by blast}
1.1199 +    ultimately have ?ths by blast }
1.1200    ultimately show ?ths by blast
1.1201  qed
1.1202
1.1203 @@ -1462,16 +1590,18 @@
1.1204      done
1.1205  qed
1.1206
1.1207 +
1.1208  subsection{* More about polypoly and pnormal etc *}
1.1209
1.1210  definition "isnonconstant p = (\<not> isconstant p)"
1.1211
1.1212 -lemma isnonconstant_pnormal_iff: assumes nc: "isnonconstant p"
1.1213 +lemma isnonconstant_pnormal_iff:
1.1214 +  assumes nc: "isnonconstant p"
1.1215    shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
1.1216  proof
1.1217    let ?p = "polypoly bs p"
1.1218    assume H: "pnormal ?p"
1.1219 -  have csz: "coefficients p \<noteq> []" using nc by (cases p, auto)
1.1220 +  have csz: "coefficients p \<noteq> []" using nc by (cases p) auto
1.1221
1.1222    from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"]
1.1223      pnormal_last_nonzero[OF H]
1.1224 @@ -1479,7 +1609,7 @@
1.1225  next
1.1226    assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.1227    let ?p = "polypoly bs p"
1.1228 -  have csz: "coefficients p \<noteq> []" using nc by (cases p, auto)
1.1229 +  have csz: "coefficients p \<noteq> []" using nc by (cases p) auto
1.1230    hence pz: "?p \<noteq> []" by (simp add: polypoly_def)
1.1231    hence lg: "length ?p > 0" by simp
1.1232    from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"]
1.1233 @@ -1489,10 +1619,14 @@
1.1234
1.1235  lemma isnonconstant_coefficients_length: "isnonconstant p \<Longrightarrow> length (coefficients p) > 1"
1.1236    unfolding isnonconstant_def
1.1237 -  apply (cases p, simp_all)
1.1238 -  apply (case_tac nat, auto)
1.1239 +  apply (cases p)
1.1240 +  apply simp_all
1.1241 +  apply (case_tac nat)
1.1242 +  apply auto
1.1243    done
1.1244 -lemma isnonconstant_nonconstant: assumes inc: "isnonconstant p"
1.1245 +
1.1246 +lemma isnonconstant_nonconstant:
1.1247 +  assumes inc: "isnonconstant p"
1.1248    shows "nonconstant (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
1.1249  proof
1.1250    let ?p = "polypoly bs p"
1.1251 @@ -1511,12 +1645,14 @@
1.1252  qed
1.1253
1.1254  lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
1.1255 -  unfolding pnormal_def
1.1256 - apply (induct p)
1.1257 - apply (simp_all, case_tac "p=[]", simp_all)
1.1258 - done
1.1259 +  apply (induct p)
1.1260 +  apply (simp_all add: pnormal_def)
1.1261 +  apply (case_tac "p = []")
1.1262 +  apply simp_all
1.1263 +  done
1.1264
1.1265 -lemma degree_degree: assumes inc: "isnonconstant p"
1.1266 +lemma degree_degree:
1.1267 +  assumes inc: "isnonconstant p"
1.1268    shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
1.1269  proof
1.1270    let  ?p = "polypoly bs p"
1.1271 @@ -1538,7 +1674,9 @@
1.1272      unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto
1.1273  qed
1.1274
1.1275 +
1.1276  section{* Swaps ; Division by a certain variable *}
1.1277 +
1.1278  primrec swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" where
1.1279    "swap n m (C x) = C x"
1.1280  | "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
1.1281 @@ -1550,37 +1688,47 @@
1.1282  | "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k)
1.1283    (swap n m p)"
1.1284
1.1285 -lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs"
1.1286 +lemma swap:
1.1287 +  assumes nbs: "n < length bs"
1.1288 +    and mbs: "m < length bs"
1.1289    shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
1.1290  proof (induct t)
1.1291 -  case (Bound k) thus ?case using nbs mbs by simp
1.1292 +  case (Bound k)
1.1293 +  thus ?case using nbs mbs by simp
1.1294  next
1.1295 -  case (CN c k p) thus ?case using nbs mbs by simp
1.1296 +  case (CN c k p)
1.1297 +  thus ?case using nbs mbs by simp
1.1298  qed simp_all
1.1299 -lemma swap_swap_id[simp]: "swap n m (swap m n t) = t"
1.1300 -  by (induct t,simp_all)
1.1301
1.1302 -lemma swap_commute: "swap n m p = swap m n p" by (induct p, simp_all)
1.1303 +lemma swap_swap_id [simp]: "swap n m (swap m n t) = t"
1.1304 +  by (induct t) simp_all
1.1305 +
1.1306 +lemma swap_commute: "swap n m p = swap m n p"
1.1307 +  by (induct p) simp_all
1.1308
1.1309  lemma swap_same_id[simp]: "swap n n t = t"
1.1310 -  by (induct t, simp_all)
1.1311 +  by (induct t) simp_all
1.1312
1.1313  definition "swapnorm n m t = polynate (swap n m t)"
1.1314
1.1315 -lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
1.1316 -  shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
1.1317 +lemma swapnorm:
1.1318 +  assumes nbs: "n < length bs"
1.1319 +    and mbs: "m < length bs"
1.1320 +  shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) =
1.1321 +    Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
1.1322    using swap[OF assms] swapnorm_def by simp
1.1323
1.1324 -lemma swapnorm_isnpoly[simp]:
1.1325 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.1326 +lemma swapnorm_isnpoly [simp]:
1.1327 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.1328    shows "isnpoly (swapnorm n m p)"
1.1329    unfolding swapnorm_def by simp
1.1330
1.1331  definition "polydivideby n s p =
1.1332 -    (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp
1.1333 -     in (k,swapnorm 0 n h,swapnorm 0 n r))"
1.1334 +  (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp
1.1335 +   in (k,swapnorm 0 n h,swapnorm 0 n r))"
1.1336
1.1337 -lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)" by (induct p, simp_all)
1.1338 +lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)"
1.1339 +  by (induct p) simp_all
1.1340
1.1341  fun isweaknpoly :: "poly \<Rightarrow> bool"
1.1342  where
1.1343 @@ -1589,9 +1737,9 @@
1.1344  | "isweaknpoly p = False"
1.1345
1.1346  lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p"
1.1347 -  by (induct p arbitrary: n0, auto)
1.1348 +  by (induct p arbitrary: n0) auto
1.1349
1.1350  lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)"
1.1351 -  by (induct p, auto)
1.1352 +  by (induct p) auto
1.1353
1.1354  end
1.1355 \ No newline at end of file
```