tuned specifications and proofs;
authorwenzelm
Mon Jul 15 11:29:19 2013 +0200 (2013-07-15)
changeset 526581e7896c7f781
parent 52657 42c14dba1daa
child 52659 58b87aa4dc3b
tuned specifications and proofs;
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
     1.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Mon Jul 15 10:42:12 2013 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Mon Jul 15 11:29:19 2013 +0200
     1.3 @@ -271,7 +271,7 @@
     1.4        with 1 have "\<And>P. Ipol ls (pow l P) = Ipol ls P ^ l" by simp
     1.5        moreover
     1.6        note Suc `even l` even_nat_plus_one_div_two
     1.7 -      ultimately show ?thesis by (auto simp add: mul_ci power_Suc even_pow)
     1.8 +      ultimately show ?thesis by (auto simp add: mul_ci even_pow)
     1.9      next
    1.10        assume "odd l"
    1.11        {
    1.12 @@ -286,7 +286,7 @@
    1.13            have two_times: "2 * (w div 2) = w"
    1.14              by (simp only: numerals even_nat_div_two_times_two [OF `even w`])
    1.15            have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)"
    1.16 -            by (simp add: power_Suc)
    1.17 +            by simp
    1.18            then have "Ipol ls P * Ipol ls P = Ipol ls P ^ 2"
    1.19              by (simp add: numerals)
    1.20            with Suc show ?thesis
     2.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Jul 15 10:42:12 2013 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Jul 15 11:29:19 2013 +0200
     2.3 @@ -8,8 +8,6 @@
     2.4  imports Complex_Main "~~/src/HOL/Library/Abstract_Rat" Polynomial_List
     2.5  begin
     2.6  
     2.7 -  (* Implementation *)
     2.8 -
     2.9  subsection{* Datatype of polynomial expressions *} 
    2.10  
    2.11  datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly
    2.12 @@ -18,8 +16,11 @@
    2.13  abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
    2.14  abbreviation poly_p :: "int \<Rightarrow> poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \<equiv> C (i)\<^sub>N"
    2.15  
    2.16 +
    2.17  subsection{* Boundedness, substitution and all that *}
    2.18 -primrec polysize:: "poly \<Rightarrow> nat" where
    2.19 +
    2.20 +primrec polysize:: "poly \<Rightarrow> nat"
    2.21 +where
    2.22    "polysize (C c) = 1"
    2.23  | "polysize (Bound n) = 1"
    2.24  | "polysize (Neg p) = 1 + polysize p"
    2.25 @@ -29,7 +30,8 @@
    2.26  | "polysize (Pw p n) = 1 + polysize p"
    2.27  | "polysize (CN c n p) = 4 + polysize c + polysize p"
    2.28  
    2.29 -primrec polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) where
    2.30 +primrec polybound0:: "poly \<Rightarrow> bool" -- {* a poly is INDEPENDENT of Bound 0 *}
    2.31 +where
    2.32    "polybound0 (C c) = True"
    2.33  | "polybound0 (Bound n) = (n>0)"
    2.34  | "polybound0 (Neg a) = polybound0 a"
    2.35 @@ -39,7 +41,8 @@
    2.36  | "polybound0 (Pw p n) = (polybound0 p)"
    2.37  | "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
    2.38  
    2.39 -primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *) where
    2.40 +primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" -- {* substitute a poly into a poly for Bound 0 *}
    2.41 +where
    2.42    "polysubst0 t (C c) = (C c)"
    2.43  | "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
    2.44  | "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
    2.45 @@ -61,6 +64,7 @@
    2.46  | "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)"
    2.47  | "decrpoly a = a"
    2.48  
    2.49 +
    2.50  subsection{* Degrees and heads and coefficients *}
    2.51  
    2.52  fun degree:: "poly \<Rightarrow> nat"
    2.53 @@ -104,9 +108,9 @@
    2.54    "headconst (CN c n p) = headconst p"
    2.55  | "headconst (C n) = n"
    2.56  
    2.57 +
    2.58  subsection{* Operations for normalization *}
    2.59  
    2.60 -
    2.61  declare if_cong[fundef_cong del]
    2.62  declare let_cong[fundef_cong del]
    2.63  
    2.64 @@ -131,8 +135,7 @@
    2.65  | "polyneg a = Neg a"
    2.66  
    2.67  definition polysub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
    2.68 -where
    2.69 -  "p -\<^sub>p q = polyadd p (polyneg q)"
    2.70 +  where "p -\<^sub>p q = polyadd p (polyneg q)"
    2.71  
    2.72  fun polymul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
    2.73  where
    2.74 @@ -173,7 +176,8 @@
    2.75  by pat_completeness auto
    2.76  termination by (relation "measure polysize") auto
    2.77  
    2.78 -fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly" where
    2.79 +fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly"
    2.80 +where
    2.81    "poly_cmul y (C x) = C (y *\<^sub>N x)"
    2.82  | "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)"
    2.83  | "poly_cmul y p = C y *\<^sub>p p"
    2.84 @@ -181,35 +185,39 @@
    2.85  definition monic :: "poly \<Rightarrow> (poly \<times> bool)" where
    2.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))"
    2.87  
    2.88 +
    2.89  subsection{* Pseudo-division *}
    2.90  
    2.91 -definition shift1 :: "poly \<Rightarrow> poly" where
    2.92 -  "shift1 p \<equiv> CN 0\<^sub>p 0 p"
    2.93 +definition shift1 :: "poly \<Rightarrow> poly"
    2.94 +  where "shift1 p \<equiv> CN 0\<^sub>p 0 p"
    2.95  
    2.96 -abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    2.97 -  "funpow \<equiv> compow"
    2.98 +abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
    2.99 +  where "funpow \<equiv> compow"
   2.100  
   2.101  partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly"
   2.102 -  where
   2.103 +where
   2.104    "polydivide_aux a n p k s = 
   2.105 -  (if s = 0\<^sub>p then (k,s)
   2.106 -  else (let b = head s; m = degree s in
   2.107 -  (if m < n then (k,s) else 
   2.108 -  (let p'= funpow (m - n) shift1 p in 
   2.109 -  (if a = b then polydivide_aux a n p k (s -\<^sub>p p') 
   2.110 -  else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
   2.111 +    (if s = 0\<^sub>p then (k,s)
   2.112 +    else (let b = head s; m = degree s in
   2.113 +    (if m < n then (k,s) else 
   2.114 +    (let p'= funpow (m - n) shift1 p in 
   2.115 +    (if a = b then polydivide_aux a n p k (s -\<^sub>p p') 
   2.116 +    else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
   2.117  
   2.118 -definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
   2.119 -  "polydivide s p \<equiv> polydivide_aux (head p) (degree p) p 0 s"
   2.120 +definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)"
   2.121 +  where "polydivide s p \<equiv> polydivide_aux (head p) (degree p) p 0 s"
   2.122  
   2.123 -fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where
   2.124 +fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly"
   2.125 +where
   2.126    "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"
   2.127  | "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p"
   2.128  
   2.129 -fun poly_deriv :: "poly \<Rightarrow> poly" where
   2.130 +fun poly_deriv :: "poly \<Rightarrow> poly"
   2.131 +where
   2.132    "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
   2.133  | "poly_deriv p = 0\<^sub>p"
   2.134  
   2.135 +
   2.136  subsection{* Semantics of the polynomial representation *}
   2.137  
   2.138  primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
   2.139 @@ -233,6 +241,7 @@
   2.140  
   2.141  lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat
   2.142  
   2.143 +
   2.144  subsection {* Normal form and normalization *}
   2.145  
   2.146  fun isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
   2.147 @@ -242,10 +251,10 @@
   2.148  | "isnpolyh p = (\<lambda>k. False)"
   2.149  
   2.150  lemma isnpolyh_mono: "\<lbrakk>n' \<le> n ; isnpolyh p n\<rbrakk> \<Longrightarrow> isnpolyh p n'"
   2.151 -by (induct p rule: isnpolyh.induct, auto)
   2.152 +  by (induct p rule: isnpolyh.induct) auto
   2.153  
   2.154 -definition isnpoly :: "poly \<Rightarrow> bool" where
   2.155 -  "isnpoly p \<equiv> isnpolyh p 0"
   2.156 +definition isnpoly :: "poly \<Rightarrow> bool"
   2.157 +  where "isnpoly p \<equiv> isnpolyh p 0"
   2.158  
   2.159  text{* polyadd preserves normal forms *}
   2.160  
   2.161 @@ -304,7 +313,8 @@
   2.162  qed auto
   2.163  
   2.164  lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
   2.165 -by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
   2.166 +  by (induct p q rule: polyadd.induct)
   2.167 +    (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
   2.168  
   2.169  lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd p q)"
   2.170    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
   2.171 @@ -332,14 +342,14 @@
   2.172  qed auto
   2.173  
   2.174  lemma headnz[simp]: "\<lbrakk>isnpolyh p n ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> headn p m \<noteq> 0\<^sub>p"
   2.175 -  by (induct p arbitrary: n rule: headn.induct, auto)
   2.176 +  by (induct p arbitrary: n rule: headn.induct) auto
   2.177  lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> degree p = 0"
   2.178 -  by (induct p arbitrary: n rule: degree.induct, auto)
   2.179 +  by (induct p arbitrary: n rule: degree.induct) auto
   2.180  lemma degreen_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> degreen p m = 0"
   2.181 -  by (induct p arbitrary: n rule: degreen.induct, auto)
   2.182 +  by (induct p arbitrary: n rule: degreen.induct) auto
   2.183  
   2.184  lemma degree_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> degree p = 0"
   2.185 -  by (induct p arbitrary: n rule: degree.induct, auto)
   2.186 +  by (induct p arbitrary: n rule: degree.induct) auto
   2.187  
   2.188  lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degree c = 0"
   2.189    using degree_isnpolyh_Suc by auto
   2.190 @@ -352,9 +362,9 @@
   2.191    shows "degreen (p +\<^sub>p q) m \<le> max (degreen p m) (degreen q m)"
   2.192    using np nq m
   2.193  proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct)
   2.194 -  case (2 c c' n' p' n0 n1) thus ?case  by (cases n', simp_all)
   2.195 +  case (2 c c' n' p' n0 n1) thus ?case  by (cases n') simp_all
   2.196  next
   2.197 -  case (3 c n p c' n0 n1) thus ?case by (cases n, auto)
   2.198 +  case (3 c n p c' n0 n1) thus ?case by (cases n) auto
   2.199  next
   2.200    case (4 c n p c' n' p' n0 n1 m) 
   2.201    have "n' = n \<or> n < n' \<or> n' < n" by arith
   2.202 @@ -377,7 +387,8 @@
   2.203      moreover {assume eq: "n = n'" hence ?case using 4 
   2.204          apply (cases "p +\<^sub>p p' = 0\<^sub>p")
   2.205          apply (auto simp add: Let_def)
   2.206 -        by blast
   2.207 +        apply blast
   2.208 +        done
   2.209        }
   2.210      ultimately have ?case by blast}
   2.211    ultimately show ?case by blast
   2.212 @@ -385,13 +396,14 @@
   2.213  
   2.214  lemma polymul_properties:
   2.215    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.216 -  and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1"
   2.217 +    and np: "isnpolyh p n0"
   2.218 +    and nq: "isnpolyh q n1"
   2.219 +    and m: "m \<le> min n0 n1"
   2.220    shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" 
   2.221 -  and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)" 
   2.222 -  and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 
   2.223 -                             else degreen p m + degreen q m)"
   2.224 +    and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)" 
   2.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)"
   2.226    using np nq m
   2.227 -proof(induct p q arbitrary: n0 n1 m rule: polymul.induct)
   2.228 +proof (induct p q arbitrary: n0 n1 m rule: polymul.induct)
   2.229    case (2 c c' n' p') 
   2.230    { case (1 n0 n1) 
   2.231      with "2.hyps"(4-6)[of n' n' n']
   2.232 @@ -430,7 +442,7 @@
   2.233          with "4.hyps"(16-17)[OF cnp np', of "n'"]
   2.234            "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp'
   2.235          have ?case
   2.236 -          by (cases "Suc n' = n", simp_all add: min_def)
   2.237 +          by (cases "Suc n' = n") (simp_all add: min_def)
   2.238        } moreover {
   2.239          assume "n' = n"
   2.240          with "4.hyps"(16-17)[OF cnp np', of n]
   2.241 @@ -525,35 +537,41 @@
   2.242  qed auto
   2.243  
   2.244  lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)"
   2.245 -by(induct p q rule: polymul.induct, auto simp add: field_simps)
   2.246 +  by (induct p q rule: polymul.induct) (auto simp add: field_simps)
   2.247  
   2.248  lemma polymul_normh: 
   2.249 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.250 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.251    shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
   2.252    using polymul_properties(1)  by blast
   2.253 +
   2.254  lemma polymul_eq0_iff: 
   2.255    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.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) "
   2.257    using polymul_properties(2)  by blast
   2.258 -lemma polymul_degreen:  
   2.259 +
   2.260 +lemma polymul_degreen:  (* FIXME duplicate? *)
   2.261    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.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)"
   2.263 +  shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow>
   2.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)"
   2.265    using polymul_properties(3) by blast
   2.266 +
   2.267  lemma polymul_norm:   
   2.268    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.269    shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul p q)"
   2.270    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
   2.271  
   2.272  lemma headconst_zero: "isnpolyh p n0 \<Longrightarrow> headconst p = 0\<^sub>N \<longleftrightarrow> p = 0\<^sub>p"
   2.273 -  by (induct p arbitrary: n0 rule: headconst.induct, auto)
   2.274 +  by (induct p arbitrary: n0 rule: headconst.induct) auto
   2.275  
   2.276  lemma headconst_isnormNum: "isnpolyh p n0 \<Longrightarrow> isnormNum (headconst p)"
   2.277 -  by (induct p arbitrary: n0, auto)
   2.278 +  by (induct p arbitrary: n0) auto
   2.279  
   2.280 -lemma monic_eqI: assumes np: "isnpolyh p n0" 
   2.281 -  shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
   2.282 +lemma monic_eqI:
   2.283 +  assumes np: "isnpolyh p n0" 
   2.284 +  shows "INum (headconst p) * Ipoly bs (fst (monic p)) =
   2.285 +    (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
   2.286    unfolding monic_def Let_def
   2.287 -proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
   2.288 +proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
   2.289    let ?h = "headconst p"
   2.290    assume pz: "p \<noteq> 0\<^sub>p"
   2.291    {assume hz: "INum ?h = (0::'a)"
   2.292 @@ -567,14 +585,14 @@
   2.293  text{* polyneg is a negation and preserves normal forms *}
   2.294  
   2.295  lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
   2.296 -by (induct p rule: polyneg.induct, auto)
   2.297 +  by (induct p rule: polyneg.induct) auto
   2.298  
   2.299  lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)"
   2.300 -  by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def)
   2.301 +  by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: Nneg_def)
   2.302  lemma polyneg_polyneg: "isnpolyh p n0 \<Longrightarrow> ~\<^sub>p (~\<^sub>p p) = p"
   2.303 -  by (induct p arbitrary: n0 rule: polyneg.induct, auto)
   2.304 +  by (induct p arbitrary: n0 rule: polyneg.induct) auto
   2.305  lemma polyneg_normh: "\<And>n. isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n "
   2.306 -by (induct p rule: polyneg.induct, auto simp add: polyneg0)
   2.307 +  by (induct p rule: polyneg.induct) (auto simp add: polyneg0)
   2.308  
   2.309  lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)"
   2.310    using isnpoly_def polyneg_normh by simp
   2.311 @@ -583,29 +601,31 @@
   2.312  text{* polysub is a substraction and preserves normal forms *}
   2.313  
   2.314  lemma polysub[simp]: "Ipoly bs (polysub p q) = (Ipoly bs p) - (Ipoly bs q)"
   2.315 -by (simp add: polysub_def polyneg polyadd)
   2.316 +  by (simp add: polysub_def)
   2.317  lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub p q) (min n0 n1)"
   2.318 -by (simp add: polysub_def polyneg_normh polyadd_normh)
   2.319 +  by (simp add: polysub_def polyneg_normh polyadd_normh)
   2.320  
   2.321  lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub p q)"
   2.322    using polyadd_norm polyneg_norm by (simp add: polysub_def) 
   2.323 -lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.324 +lemma polysub_same_0[simp]:
   2.325 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.326    shows "isnpolyh p n0 \<Longrightarrow> polysub p p = 0\<^sub>p"
   2.327 -unfolding polysub_def split_def fst_conv snd_conv
   2.328 -by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])
   2.329 +  unfolding polysub_def split_def fst_conv snd_conv
   2.330 +  by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def])
   2.331  
   2.332  lemma polysub_0: 
   2.333    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.334    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
   2.335    unfolding polysub_def split_def fst_conv snd_conv
   2.336    by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
   2.337 -  (auto simp: Nsub0[simplified Nsub_def] Let_def)
   2.338 +    (auto simp: Nsub0[simplified Nsub_def] Let_def)
   2.339  
   2.340  text{* polypow is a power function and preserves normal forms *}
   2.341  
   2.342  lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n"
   2.343 -proof(induct n rule: polypow.induct)
   2.344 -  case 1 thus ?case by simp
   2.345 +proof (induct n rule: polypow.induct)
   2.346 +  case 1
   2.347 +  thus ?case by simp
   2.348  next
   2.349    case (2 n)
   2.350    let ?q = "polypow ((Suc n) div 2) p"
   2.351 @@ -613,19 +633,21 @@
   2.352    have "odd (Suc n) \<or> even (Suc n)" by simp
   2.353    moreover 
   2.354    {assume odd: "odd (Suc n)"
   2.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
   2.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"
   2.357 +      by arith
   2.358      from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" by (simp add: Let_def)
   2.359      also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)"
   2.360        using "2.hyps" by simp
   2.361      also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
   2.362 -      apply (simp only: power_add power_one_right) by simp
   2.363 +      by (simp only: power_add power_one_right) simp
   2.364      also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat)))))"
   2.365        by (simp only: th)
   2.366      finally have ?case 
   2.367      using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp  }
   2.368    moreover 
   2.369    {assume even: "even (Suc n)"
   2.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
   2.371 +    have th: "(Suc (Suc (0\<Colon>nat))) * (Suc n div Suc (Suc (0\<Colon>nat))) = Suc n div 2 + Suc n div 2"
   2.372 +      by arith
   2.373      from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def)
   2.374      also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"
   2.375        using "2.hyps" apply (simp only: power_add) by simp
   2.376 @@ -634,7 +656,7 @@
   2.377  qed
   2.378  
   2.379  lemma polypow_normh: 
   2.380 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.381 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.382    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
   2.383  proof (induct k arbitrary: n rule: polypow.induct)
   2.384    case (2 k n)
   2.385 @@ -653,23 +675,28 @@
   2.386  
   2.387  text{* Finally the whole normalization *}
   2.388  
   2.389 -lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
   2.390 -by (induct p rule:polynate.induct, auto)
   2.391 +lemma polynate [simp]:
   2.392 +  "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
   2.393 +  by (induct p rule:polynate.induct) auto
   2.394  
   2.395  lemma polynate_norm[simp]: 
   2.396    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.397    shows "isnpoly (polynate p)"
   2.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)
   2.399 +  by (induct p rule: polynate.induct)
   2.400 +     (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
   2.401 +      simp_all add: isnpoly_def)
   2.402  
   2.403  text{* shift1 *}
   2.404  
   2.405  
   2.406  lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
   2.407 -by (simp add: shift1_def polymul)
   2.408 +  by (simp add: shift1_def)
   2.409  
   2.410  lemma shift1_isnpoly: 
   2.411 -  assumes pn: "isnpoly p" and pnz: "p \<noteq> 0\<^sub>p" shows "isnpoly (shift1 p) "
   2.412 -  using pn pnz by (simp add: shift1_def isnpoly_def )
   2.413 +  assumes pn: "isnpoly p"
   2.414 +    and pnz: "p \<noteq> 0\<^sub>p"
   2.415 +  shows "isnpoly (shift1 p) "
   2.416 +  using pn pnz by (simp add: shift1_def isnpoly_def)
   2.417  
   2.418  lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p"
   2.419    by (simp add: shift1_def)
   2.420 @@ -678,18 +705,22 @@
   2.421    by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
   2.422  
   2.423  lemma funpow_isnpolyh: 
   2.424 -  assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n"
   2.425 +  assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
   2.426 +    and np: "isnpolyh p n"
   2.427    shows "isnpolyh (funpow k f p) n"
   2.428 -  using f np by (induct k arbitrary: p, auto)
   2.429 +  using f np by (induct k arbitrary: p) auto
   2.430  
   2.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)"
   2.432 -  by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
   2.433 +lemma funpow_shift1:
   2.434 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) =
   2.435 +    Ipoly bs (Mul (Pw (Bound 0) n) p)"
   2.436 +  by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
   2.437  
   2.438  lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
   2.439    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   2.440  
   2.441  lemma funpow_shift1_1: 
   2.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)"
   2.443 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) =
   2.444 +    Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
   2.445    by (simp add: funpow_shift1)
   2.446  
   2.447  lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
   2.448 @@ -697,23 +728,29 @@
   2.449  
   2.450  lemma behead:
   2.451    assumes np: "isnpolyh p n"
   2.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})"
   2.453 +  shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
   2.454 +    (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})"
   2.455    using np
   2.456  proof (induct p arbitrary: n rule: behead.induct)
   2.457    case (1 c p n) hence pn: "isnpolyh p n" by simp
   2.458    from 1(1)[OF pn] 
   2.459    have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . 
   2.460 -  then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
   2.461 -    by (simp_all add: th[symmetric] field_simps power_Suc)
   2.462 +  then show ?case using "1.hyps"
   2.463 +    apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
   2.464 +    apply (simp_all add: th[symmetric] field_simps)
   2.465 +    done
   2.466  qed (auto simp add: Let_def)
   2.467  
   2.468  lemma behead_isnpolyh:
   2.469 -  assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n"
   2.470 -  using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono)
   2.471 +  assumes np: "isnpolyh p n"
   2.472 +  shows "isnpolyh (behead p) n"
   2.473 +  using np by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono)
   2.474 +
   2.475  
   2.476  subsection{* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
   2.477 +
   2.478  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
   2.479 -proof(induct p arbitrary: n rule: poly.induct, auto)
   2.480 +proof (induct p arbitrary: n rule: poly.induct, auto)
   2.481    case (goal1 c n p n')
   2.482    hence "n = Suc (n - 1)" by simp
   2.483    hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
   2.484 @@ -721,27 +758,29 @@
   2.485  qed
   2.486  
   2.487  lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p"
   2.488 -by (induct p arbitrary: n0 rule: isconstant.induct, auto simp add: isnpolyh_polybound0)
   2.489 +  by (induct p arbitrary: n0 rule: isconstant.induct) (auto simp add: isnpolyh_polybound0)
   2.490  
   2.491 -lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p" by (induct p, auto)
   2.492 +lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p"
   2.493 +  by (induct p) auto
   2.494  
   2.495  lemma decrpoly_normh: "isnpolyh p n0 \<Longrightarrow> polybound0 p \<Longrightarrow> isnpolyh (decrpoly p) (n0 - 1)"
   2.496 -  apply (induct p arbitrary: n0, auto)
   2.497 +  apply (induct p arbitrary: n0)
   2.498 +  apply auto
   2.499    apply (atomize)
   2.500    apply (erule_tac x = "Suc nat" in allE)
   2.501    apply auto
   2.502    done
   2.503  
   2.504  lemma head_polybound0: "isnpolyh p n0 \<Longrightarrow> polybound0 (head p)"
   2.505 - by (induct p  arbitrary: n0 rule: head.induct, auto intro: isnpolyh_polybound0)
   2.506 +  by (induct p  arbitrary: n0 rule: head.induct) (auto intro: isnpolyh_polybound0)
   2.507  
   2.508  lemma polybound0_I:
   2.509    assumes nb: "polybound0 a"
   2.510    shows "Ipoly (b#bs) a = Ipoly (b'#bs) a"
   2.511 -using nb
   2.512 -by (induct a rule: poly.induct) auto 
   2.513 -lemma polysubst0_I:
   2.514 -  shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
   2.515 +  using nb
   2.516 +  by (induct a rule: poly.induct) auto 
   2.517 +
   2.518 +lemma polysubst0_I: "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
   2.519    by (induct t) simp_all
   2.520  
   2.521  lemma polysubst0_I':
   2.522 @@ -749,16 +788,18 @@
   2.523    shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b'#bs) a)#bs) t"
   2.524    by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"])
   2.525  
   2.526 -lemma decrpoly: assumes nb: "polybound0 t"
   2.527 +lemma decrpoly:
   2.528 +  assumes nb: "polybound0 t"
   2.529    shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)"
   2.530 -  using nb by (induct t rule: decrpoly.induct, simp_all)
   2.531 +  using nb by (induct t rule: decrpoly.induct) simp_all
   2.532  
   2.533 -lemma polysubst0_polybound0: assumes nb: "polybound0 t"
   2.534 +lemma polysubst0_polybound0:
   2.535 +  assumes nb: "polybound0 t"
   2.536    shows "polybound0 (polysubst0 t a)"
   2.537 -using nb by (induct a rule: poly.induct, auto)
   2.538 +  using nb by (induct a rule: poly.induct) auto
   2.539  
   2.540  lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
   2.541 -  by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0)
   2.542 +  by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0)
   2.543  
   2.544  primrec maxindex :: "poly \<Rightarrow> nat" where
   2.545    "maxindex (Bound n) = n + 1"
   2.546 @@ -770,11 +811,11 @@
   2.547  | "maxindex (Pw p n) = maxindex p"
   2.548  | "maxindex (C x) = 0"
   2.549  
   2.550 -definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool" where
   2.551 -  "wf_bs bs p = (length bs \<ge> maxindex p)"
   2.552 +definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool"
   2.553 +  where "wf_bs bs p = (length bs \<ge> maxindex p)"
   2.554  
   2.555  lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall> c \<in> set (coefficients p). wf_bs bs c"
   2.556 -proof(induct p rule: coefficients.induct)
   2.557 +proof (induct p rule: coefficients.induct)
   2.558    case (1 c p) 
   2.559    show ?case 
   2.560    proof
   2.561 @@ -791,12 +832,13 @@
   2.562  qed simp_all
   2.563  
   2.564  lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"
   2.565 -by (induct p rule: coefficients.induct, auto)
   2.566 +  by (induct p rule: coefficients.induct) auto
   2.567  
   2.568  lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p"
   2.569 -  unfolding wf_bs_def by (induct p, auto simp add: nth_append)
   2.570 +  unfolding wf_bs_def by (induct p) (auto simp add: nth_append)
   2.571  
   2.572 -lemma take_maxindex_wf: assumes wf: "wf_bs bs p" 
   2.573 +lemma take_maxindex_wf:
   2.574 +  assumes wf: "wf_bs bs p" 
   2.575    shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p"
   2.576  proof-
   2.577    let ?ip = "maxindex p"
   2.578 @@ -808,7 +850,7 @@
   2.579  qed
   2.580  
   2.581  lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1"
   2.582 -  by (induct p, auto)
   2.583 +  by (induct p) auto
   2.584  
   2.585  lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
   2.586    unfolding wf_bs_def by simp
   2.587 @@ -819,22 +861,28 @@
   2.588  
   2.589  
   2.590  lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"
   2.591 -by(induct p rule: coefficients.induct, auto simp add: wf_bs_def)
   2.592 +  by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def)
   2.593  lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"
   2.594 -  by (induct p rule: coefficients.induct, simp_all)
   2.595 +  by (induct p rule: coefficients.induct) simp_all
   2.596  
   2.597  
   2.598  lemma coefficients_head: "last (coefficients p) = head p"
   2.599 -  by (induct p rule: coefficients.induct, auto)
   2.600 +  by (induct p rule: coefficients.induct) auto
   2.601  
   2.602  lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p"
   2.603 -  unfolding wf_bs_def by (induct p rule: decrpoly.induct, auto)
   2.604 +  unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto
   2.605  
   2.606  lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists> ys. length (xs @ ys) = n"
   2.607    apply (rule exI[where x="replicate (n - length xs) z"])
   2.608 -  by simp
   2.609 +  apply simp
   2.610 +  done
   2.611 +
   2.612  lemma isnpolyh_Suc_const:"isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
   2.613 -by (cases p, auto) (case_tac "nat", simp_all)
   2.614 +  apply (cases p)
   2.615 +  apply auto
   2.616 +  apply (case_tac "nat")
   2.617 +  apply simp_all
   2.618 +  done
   2.619  
   2.620  lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)"
   2.621    unfolding wf_bs_def 
   2.622 @@ -852,11 +900,12 @@
   2.623    done
   2.624  
   2.625  lemma wf_bs_polyneg: "wf_bs bs p \<Longrightarrow> wf_bs bs (~\<^sub>p p)"
   2.626 -  unfolding wf_bs_def by (induct p rule: polyneg.induct, auto)
   2.627 +  unfolding wf_bs_def by (induct p rule: polyneg.induct) auto
   2.628  
   2.629  lemma wf_bs_polysub: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p -\<^sub>p q)"
   2.630    unfolding polysub_def split_def fst_conv snd_conv using wf_bs_polyadd wf_bs_polyneg by blast
   2.631  
   2.632 +
   2.633  subsection{* Canonicity of polynomial representation, see lemma isnpolyh_unique*}
   2.634  
   2.635  definition "polypoly bs p = map (Ipoly bs) (coefficients p)"
   2.636 @@ -874,8 +923,8 @@
   2.637  
   2.638  lemma coefficients_isconst:
   2.639    "isnpolyh p n \<Longrightarrow> \<forall>q\<in>set (coefficients p). isconstant q"
   2.640 -  by (induct p arbitrary: n rule: coefficients.induct, 
   2.641 -    auto simp add: isnpolyh_Suc_const)
   2.642 +  by (induct p arbitrary: n rule: coefficients.induct) 
   2.643 +    (auto simp add: isnpolyh_Suc_const)
   2.644  
   2.645  lemma polypoly_polypoly':
   2.646    assumes np: "isnpolyh p n0"
   2.647 @@ -896,12 +945,14 @@
   2.648  qed
   2.649  
   2.650  lemma polypoly_poly:
   2.651 -  assumes np: "isnpolyh p n0" shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x"
   2.652 +  assumes np: "isnpolyh p n0"
   2.653 +  shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x"
   2.654    using np 
   2.655 -by (induct p arbitrary: n0 bs rule: coefficients.induct, auto simp add: polypoly_def)
   2.656 +  by (induct p arbitrary: n0 bs rule: coefficients.induct) (auto simp add: polypoly_def)
   2.657  
   2.658  lemma polypoly'_poly: 
   2.659 -  assumes np: "isnpolyh p n0" shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x"
   2.660 +  assumes np: "isnpolyh p n0"
   2.661 +  shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x"
   2.662    using polypoly_poly[OF np, simplified polypoly_polypoly'[OF np]] .
   2.663  
   2.664  
   2.665 @@ -909,29 +960,34 @@
   2.666    assumes np: "isnpolyh p n0" and nb: "polybound0 p"
   2.667    shows "polypoly bs p = [Ipoly bs p]"
   2.668    using np nb unfolding polypoly_def 
   2.669 -  by (cases p, auto, case_tac nat, auto)
   2.670 +  apply (cases p)
   2.671 +  apply auto
   2.672 +  apply (case_tac nat)
   2.673 +  apply auto
   2.674 +  done
   2.675  
   2.676  lemma head_isnpolyh: "isnpolyh p n0 \<Longrightarrow> isnpolyh (head p) n0" 
   2.677 -  by (induct p rule: head.induct, auto)
   2.678 +  by (induct p rule: head.induct) auto
   2.679  
   2.680  lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)"
   2.681 -  by (cases p,auto)
   2.682 +  by (cases p) auto
   2.683  
   2.684  lemma head_eq_headn0: "head p = headn p 0"
   2.685 -  by (induct p rule: head.induct, simp_all)
   2.686 +  by (induct p rule: head.induct) simp_all
   2.687  
   2.688  lemma head_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (head p = 0\<^sub>p) = (p = 0\<^sub>p)"
   2.689    by (simp add: head_eq_headn0)
   2.690  
   2.691  lemma isnpolyh_zero_iff: 
   2.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})"
   2.693 +  assumes nq: "isnpolyh p n0"
   2.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})"
   2.695    shows "p = 0\<^sub>p"
   2.696 -using nq eq
   2.697 +  using nq eq
   2.698  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
   2.699    case less
   2.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)`
   2.701    {assume nz: "maxindex p = 0"
   2.702 -    then obtain c where "p = C c" using np by (cases p, auto)
   2.703 +    then obtain c where "p = C c" using np by (cases p) auto
   2.704      with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp}
   2.705    moreover
   2.706    {assume nz: "maxindex p \<noteq> 0"
   2.707 @@ -958,7 +1014,7 @@
   2.708        hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp
   2.709        with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]
   2.710        have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
   2.711 -      hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) 
   2.712 +      hence "poly (polypoly' (?ts @ xs) p) = poly []" by auto
   2.713        hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
   2.714          using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
   2.715        with coefficients_head[of p, symmetric]
   2.716 @@ -975,7 +1031,8 @@
   2.717  qed
   2.718  
   2.719  lemma isnpolyh_unique:  
   2.720 -  assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"
   2.721 +  assumes np:"isnpolyh p n0"
   2.722 +    and nq: "isnpolyh q n1"
   2.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"
   2.724  proof(auto)
   2.725    assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
   2.726 @@ -989,69 +1046,91 @@
   2.727  
   2.728  text{* consequences of unicity on the algorithms for polynomial normalization *}
   2.729  
   2.730 -lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.731 -  and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
   2.732 +lemma polyadd_commute:
   2.733 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.734 +    and np: "isnpolyh p n0"
   2.735 +    and nq: "isnpolyh q n1"
   2.736 +  shows "p +\<^sub>p q = q +\<^sub>p p"
   2.737    using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
   2.738  
   2.739  lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
   2.740  lemma one_normh: "isnpolyh (1)\<^sub>p n" by simp
   2.741 +
   2.742  lemma polyadd_0[simp]: 
   2.743    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.744 -  and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
   2.745 +    and np: "isnpolyh p n0"
   2.746 +  shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
   2.747    using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] 
   2.748      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
   2.749  
   2.750  lemma polymul_1[simp]: 
   2.751 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.752 -  and np: "isnpolyh p n0" shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p"
   2.753 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.754 +    and np: "isnpolyh p n0"
   2.755 +  shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p"
   2.756    using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 
   2.757      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
   2.758 +
   2.759  lemma polymul_0[simp]: 
   2.760    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.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"
   2.762 +    and np: "isnpolyh p n0"
   2.763 +  shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
   2.764    using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] 
   2.765      isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
   2.766  
   2.767  lemma polymul_commute: 
   2.768 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.769 -  and np:"isnpolyh p n0" and nq: "isnpolyh q n1"
   2.770 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.771 +    and np:"isnpolyh p n0"
   2.772 +    and nq: "isnpolyh q n1"
   2.773    shows "p *\<^sub>p q = q *\<^sub>p p"
   2.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
   2.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}"]
   2.776 +  by simp
   2.777  
   2.778 -declare polyneg_polyneg[simp]
   2.779 +declare polyneg_polyneg [simp]
   2.780    
   2.781 -lemma isnpolyh_polynate_id[simp]: 
   2.782 +lemma isnpolyh_polynate_id [simp]: 
   2.783    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.784 -  and np:"isnpolyh p n0" shows "polynate p = p"
   2.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
   2.786 +    and np:"isnpolyh p n0"
   2.787 +  shows "polynate p = p"
   2.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}"]
   2.789 +  by simp
   2.790  
   2.791  lemma polynate_idempotent[simp]: 
   2.792 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.793 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.794    shows "polynate (polynate p) = polynate p"
   2.795    using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
   2.796  
   2.797  lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
   2.798    unfolding poly_nate_def polypoly'_def ..
   2.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>)"
   2.800 +
   2.801 +lemma poly_nate_poly:
   2.802 +  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0, field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   2.803    using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
   2.804 -  unfolding poly_nate_polypoly' by (auto intro: ext)
   2.805 +  unfolding poly_nate_polypoly' by auto
   2.806 +
   2.807  
   2.808  subsection{* heads, degrees and all that *}
   2.809 +
   2.810  lemma degree_eq_degreen0: "degree p = degreen p 0"
   2.811 -  by (induct p rule: degree.induct, simp_all)
   2.812 +  by (induct p rule: degree.induct) simp_all
   2.813  
   2.814 -lemma degree_polyneg: assumes n: "isnpolyh p n"
   2.815 +lemma degree_polyneg:
   2.816 +  assumes n: "isnpolyh p n"
   2.817    shows "degree (polyneg p) = degree p"
   2.818 -  using n
   2.819 -  by (induct p arbitrary: n rule: polyneg.induct, simp_all) (case_tac na, auto)
   2.820 +  apply (induct p arbitrary: n rule: polyneg.induct)
   2.821 +  using n apply simp_all
   2.822 +  apply (case_tac na)
   2.823 +  apply auto
   2.824 +  done
   2.825  
   2.826  lemma degree_polyadd:
   2.827    assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
   2.828    shows "degree (p +\<^sub>p q) \<le> max (degree p) (degree q)"
   2.829 -using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp
   2.830 +  using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp
   2.831  
   2.832  
   2.833 -lemma degree_polysub: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
   2.834 +lemma degree_polysub:
   2.835 +  assumes np: "isnpolyh p n0"
   2.836 +    and nq: "isnpolyh q n1"
   2.837    shows "degree (p -\<^sub>p q) \<le> max (degree p) (degree q)"
   2.838  proof-
   2.839    from nq have nq': "isnpolyh (~\<^sub>p q) n1" using polyneg_normh by simp
   2.840 @@ -1060,24 +1139,25 @@
   2.841  
   2.842  lemma degree_polysub_samehead: 
   2.843    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.844 -  and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" 
   2.845 -  and d: "degree p = degree q"
   2.846 +    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" 
   2.847 +    and d: "degree p = degree q"
   2.848    shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
   2.849 -unfolding polysub_def split_def fst_conv snd_conv
   2.850 -using np nq h d
   2.851 -proof(induct p q rule:polyadd.induct)
   2.852 -  case (1 c c') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) 
   2.853 +  unfolding polysub_def split_def fst_conv snd_conv
   2.854 +  using np nq h d
   2.855 +proof (induct p q rule: polyadd.induct)
   2.856 +  case (1 c c')
   2.857 +  thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) 
   2.858  next
   2.859    case (2 c c' n' p') 
   2.860    from 2 have "degree (C c) = degree (CN c' n' p')" by simp
   2.861 -  hence nz:"n' > 0" by (cases n', auto)
   2.862 -  hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
   2.863 +  hence nz:"n' > 0" by (cases n') auto
   2.864 +  hence "head (CN c' n' p') = CN c' n' p'" by (cases n') auto
   2.865    with 2 show ?case by simp
   2.866  next
   2.867    case (3 c n p c') 
   2.868    hence "degree (C c') = degree (CN c n p)" by simp
   2.869 -  hence nz:"n > 0" by (cases n, auto)
   2.870 -  hence "head (CN c n p) = CN c n p" by (cases n, auto)
   2.871 +  hence nz:"n > 0" by (cases n) auto
   2.872 +  hence "head (CN c n p) = CN c n p" by (cases n) auto
   2.873    with 3 show ?case by simp
   2.874  next
   2.875    case (4 c n p c' n' p')
   2.876 @@ -1096,36 +1176,43 @@
   2.877      moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')}
   2.878      moreover {assume nz: "n > 0"
   2.879        with nn' H(3) have  cc':"c = c'" and pp': "p = p'" by (cases n, auto)+
   2.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)}
   2.881 +      hence ?case
   2.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]
   2.883 +        using nn' 4 by (simp add: Let_def)}
   2.884      ultimately have ?case by blast}
   2.885    moreover
   2.886    {assume nn': "n < n'" hence n'p: "n' > 0" by simp 
   2.887 -    hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n', simp_all)
   2.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)
   2.889 -    hence "n > 0" by (cases n, simp_all)
   2.890 -    hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto)
   2.891 +    hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n') simp_all
   2.892 +    have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')"
   2.893 +      using 4 nn' by (cases n', simp_all)
   2.894 +    hence "n > 0" by (cases n) simp_all
   2.895 +    hence headcnp: "head (CN c n p) = CN c n p" by (cases n) auto
   2.896      from H(3) headcnp headcnp' nn' have ?case by auto}
   2.897    moreover
   2.898    {assume nn': "n > n'"  hence np: "n > 0" by simp 
   2.899 -    hence headcnp:"head (CN c n p) = CN c n p"  by (cases n, simp_all)
   2.900 +    hence headcnp:"head (CN c n p) = CN c n p"  by (cases n) simp_all
   2.901      from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
   2.902 -    from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all)
   2.903 -    with degcnpeq have "n' > 0" by (cases n', simp_all)
   2.904 -    hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
   2.905 +    from np have degcnp: "degree (CN c n p) = 0" by (cases n) simp_all
   2.906 +    with degcnpeq have "n' > 0" by (cases n') simp_all
   2.907 +    hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n') auto
   2.908      from H(3) headcnp headcnp' nn' have ?case by auto}
   2.909    ultimately show ?case  by blast
   2.910  qed auto
   2.911   
   2.912  lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p"
   2.913 -by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def)
   2.914 +  by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def)
   2.915  
   2.916  lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
   2.917 -proof(induct k arbitrary: n0 p)
   2.918 -  case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
   2.919 +proof (induct k arbitrary: n0 p)
   2.920 +  case 0
   2.921 +  thus ?case by auto
   2.922 +next
   2.923 +  case (Suc k n0 p)
   2.924 +  hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
   2.925    with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
   2.926      and "head (shift1 p) = head p" by (simp_all add: shift1_head) 
   2.927    thus ?case by (simp add: funpow_swap1)
   2.928 -qed auto  
   2.929 +qed
   2.930  
   2.931  lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
   2.932    by (simp add: shift1_def)
   2.933 @@ -1133,47 +1220,52 @@
   2.934    by (induct k arbitrary: p) (auto simp add: shift1_degree)
   2.935  
   2.936  lemma funpow_shift1_nz: "p \<noteq> 0\<^sub>p \<Longrightarrow> funpow n shift1 p \<noteq> 0\<^sub>p"
   2.937 -  by (induct n arbitrary: p) (simp_all add: funpow.simps)
   2.938 +  by (induct n arbitrary: p) simp_all
   2.939  
   2.940  lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> head p = p"
   2.941 -  by (induct p arbitrary: n rule: degree.induct, auto)
   2.942 +  by (induct p arbitrary: n rule: degree.induct) auto
   2.943  lemma headn_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> headn p m = p"
   2.944 -  by (induct p arbitrary: n rule: degreen.induct, auto)
   2.945 +  by (induct p arbitrary: n rule: degreen.induct) auto
   2.946  lemma head_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> head p = p"
   2.947 -  by (induct p arbitrary: n rule: degree.induct, auto)
   2.948 +  by (induct p arbitrary: n rule: degree.induct) auto
   2.949  lemma head_head[simp]: "isnpolyh p n0 \<Longrightarrow> head (head p) = head p"
   2.950 -  by (induct p rule: head.induct, auto)
   2.951 +  by (induct p rule: head.induct) auto
   2.952  
   2.953  lemma polyadd_eq_const_degree: 
   2.954 -  "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\<rbrakk> \<Longrightarrow> degree p = degree q" 
   2.955 +  "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> polyadd p q = C c \<Longrightarrow> degree p = degree q"
   2.956    using polyadd_eq_const_degreen degree_eq_degreen0 by simp
   2.957  
   2.958 -lemma polyadd_head: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
   2.959 -  and deg: "degree p \<noteq> degree q"
   2.960 +lemma polyadd_head:
   2.961 +  assumes np: "isnpolyh p n0"
   2.962 +    and nq: "isnpolyh q n1"
   2.963 +    and deg: "degree p \<noteq> degree q"
   2.964    shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)"
   2.965 -using np nq deg
   2.966 -apply(induct p q arbitrary: n0 n1 rule: polyadd.induct,simp_all)
   2.967 -apply (case_tac n', simp, simp)
   2.968 -apply (case_tac n, simp, simp)
   2.969 -apply (case_tac n, case_tac n', simp add: Let_def)
   2.970 -apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
   2.971 -apply (auto simp add: polyadd_eq_const_degree)
   2.972 -apply (metis head_nz)
   2.973 -apply (metis head_nz)
   2.974 -apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
   2.975 -by (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
   2.976 +  using np nq deg
   2.977 +  apply (induct p q arbitrary: n0 n1 rule: polyadd.induct)
   2.978 +  using np
   2.979 +  apply simp_all
   2.980 +  apply (case_tac n', simp, simp)
   2.981 +  apply (case_tac n, simp, simp)
   2.982 +  apply (case_tac n, case_tac n', simp add: Let_def)
   2.983 +  apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
   2.984 +  apply (auto simp add: polyadd_eq_const_degree)
   2.985 +  apply (metis head_nz)
   2.986 +  apply (metis head_nz)
   2.987 +  apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
   2.988 +  apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
   2.989 +  done
   2.990  
   2.991  lemma polymul_head_polyeq: 
   2.992 -   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.993 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   2.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"
   2.995  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   2.996    case (2 c c' n' p' n0 n1)
   2.997    hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum c"  by (simp_all add: head_isnpolyh)
   2.998 -  thus ?case using 2 by (cases n', auto) 
   2.999 +  thus ?case using 2 by (cases n') auto
  2.1000  next 
  2.1001    case (3 c n p c' n0 n1) 
  2.1002    hence "isnpolyh (head (CN c n p)) n0" "isnormNum c'"  by (simp_all add: head_isnpolyh)
  2.1003 -  thus ?case using 3 by (cases n, auto)
  2.1004 +  thus ?case using 3 by (cases n) auto
  2.1005  next
  2.1006    case (4 c n p c' n' p' n0 n1)
  2.1007    hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
  2.1008 @@ -1182,13 +1274,22 @@
  2.1009    have "n < n' \<or> n' < n \<or> n = n'" by arith
  2.1010    moreover 
  2.1011    {assume nn': "n < n'" hence ?case 
  2.1012 -      using norm 
  2.1013 -    "4.hyps"(2)[OF norm(1,6)]
  2.1014 -    "4.hyps"(1)[OF norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
  2.1015 +      using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)]
  2.1016 +      apply simp
  2.1017 +      apply (cases n)
  2.1018 +      apply simp
  2.1019 +      apply (cases n')
  2.1020 +      apply simp_all
  2.1021 +      done }
  2.1022    moreover {assume nn': "n'< n"
  2.1023 -    hence ?case using norm "4.hyps"(6) [OF norm(5,3)]
  2.1024 -      "4.hyps"(5)[OF norm(5,4)] 
  2.1025 -      by (simp,cases n',simp,cases n,auto)}
  2.1026 +    hence ?case
  2.1027 +      using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] 
  2.1028 +      apply simp
  2.1029 +      apply (cases n')
  2.1030 +      apply simp
  2.1031 +      apply (cases n)
  2.1032 +      apply auto
  2.1033 +      done }
  2.1034    moreover {assume nn': "n' = n"
  2.1035      from nn' polymul_normh[OF norm(5,4)] 
  2.1036      have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)
  2.1037 @@ -1218,44 +1319,50 @@
  2.1038  qed simp_all
  2.1039  
  2.1040  lemma degree_coefficients: "degree p = length (coefficients p) - 1"
  2.1041 -  by(induct p rule: degree.induct, auto)
  2.1042 +  by (induct p rule: degree.induct) auto
  2.1043  
  2.1044  lemma degree_head[simp]: "degree (head p) = 0"
  2.1045 -  by (induct p rule: head.induct, auto)
  2.1046 +  by (induct p rule: head.induct) auto
  2.1047  
  2.1048  lemma degree_CN: "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<le> 1 + degree p"
  2.1049 -  by (cases n, simp_all)
  2.1050 +  by (cases n) simp_all
  2.1051  lemma degree_CN': "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<ge>  degree p"
  2.1052 -  by (cases n, simp_all)
  2.1053 +  by (cases n) simp_all
  2.1054  
  2.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)"
  2.1056 +lemma polyadd_different_degree:
  2.1057 +  "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degree p \<noteq> degree q\<rbrakk> \<Longrightarrow>
  2.1058 +    degree (polyadd p q) = max (degree p) (degree q)"
  2.1059    using polyadd_different_degreen degree_eq_degreen0 by simp
  2.1060  
  2.1061  lemma degreen_polyneg: "isnpolyh p n0 \<Longrightarrow> degreen (~\<^sub>p p) m = degreen p m"
  2.1062 -  by (induct p arbitrary: n0 rule: polyneg.induct, auto)
  2.1063 +  by (induct p arbitrary: n0 rule: polyneg.induct) auto
  2.1064  
  2.1065  lemma degree_polymul:
  2.1066    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  2.1067 -  and np: "isnpolyh p n0" and nq: "isnpolyh q n1"
  2.1068 +    and np: "isnpolyh p n0"
  2.1069 +    and nq: "isnpolyh q n1"
  2.1070    shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
  2.1071    using polymul_degreen[OF np nq, where m="0"]  degree_eq_degreen0 by simp
  2.1072  
  2.1073  lemma polyneg_degree: "isnpolyh p n \<Longrightarrow> degree (polyneg p) = degree p"
  2.1074 -  by (induct p arbitrary: n rule: degree.induct, auto)
  2.1075 +  by (induct p arbitrary: n rule: degree.induct) auto
  2.1076  
  2.1077  lemma polyneg_head: "isnpolyh p n \<Longrightarrow> head(polyneg p) = polyneg (head p)"
  2.1078 -  by (induct p arbitrary: n rule: degree.induct, auto)
  2.1079 +  by (induct p arbitrary: n rule: degree.induct) auto
  2.1080 +
  2.1081  
  2.1082  subsection {* Correctness of polynomial pseudo division *}
  2.1083  
  2.1084  lemma polydivide_aux_properties:
  2.1085    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  2.1086 -  and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
  2.1087 -  and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
  2.1088 +    and np: "isnpolyh p n0"
  2.1089 +    and ns: "isnpolyh s n1"
  2.1090 +    and ap: "head p = a"
  2.1091 +    and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
  2.1092    shows "(polydivide_aux a n p k s = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p) 
  2.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)))"
  2.1094    using ns
  2.1095 -proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
  2.1096 +proof (induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
  2.1097    case less
  2.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)"
  2.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) 
  2.1100 @@ -1272,12 +1379,20 @@
  2.1101    from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
  2.1102    from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap 
  2.1103    have nakk':"isnpolyh ?akk' 0" by blast
  2.1104 -  {assume sz: "s = 0\<^sub>p"
  2.1105 -   hence ?ths using np polydivide_aux.simps apply clarsimp by (rule exI[where x="0\<^sub>p"], simp) }
  2.1106 +  { assume sz: "s = 0\<^sub>p"
  2.1107 +    hence ?ths using np polydivide_aux.simps
  2.1108 +      apply clarsimp
  2.1109 +      apply (rule exI[where x="0\<^sub>p"])
  2.1110 +      apply simp
  2.1111 +      done }
  2.1112    moreover
  2.1113    {assume sz: "s \<noteq> 0\<^sub>p"
  2.1114      {assume dn: "degree s < n"
  2.1115 -      hence "?ths" using ns ndp np polydivide_aux.simps by auto (rule exI[where x="0\<^sub>p"],simp) }
  2.1116 +      hence "?ths" using ns ndp np polydivide_aux.simps
  2.1117 +        apply auto
  2.1118 +        apply (rule exI[where x="0\<^sub>p"])
  2.1119 +        apply simp
  2.1120 +        done }
  2.1121      moreover 
  2.1122      {assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> n" by arith
  2.1123        have degsp': "degree s = degree ?p'" 
  2.1124 @@ -1332,9 +1447,14 @@
  2.1125          {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
  2.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}"]
  2.1127            have " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp
  2.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
  2.1129 -            by (simp only: funpow_shift1_1) simp
  2.1130 -          hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
  2.1131 +          hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
  2.1132 +            using np nxdn
  2.1133 +            apply simp
  2.1134 +            apply (simp only: funpow_shift1_1)
  2.1135 +            apply simp
  2.1136 +            done
  2.1137 +          hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
  2.1138 +            by blast
  2.1139            {assume h1: "polydivide_aux a n p k s = (k',r)"
  2.1140              from polydivide_aux.simps sz dn' ba
  2.1141              have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
  2.1142 @@ -1385,12 +1505,16 @@
  2.1143              {fix bs:: "'a::{field_char_0, field_inverse_zero} list"
  2.1144                
  2.1145              from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
  2.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
  2.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"
  2.1148 -              by (simp add: field_simps power_Suc)
  2.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"
  2.1150 -              by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
  2.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"
  2.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)"
  2.1153 +              by simp
  2.1154 +            hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s =
  2.1155 +              Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r"
  2.1156 +              by (simp add: field_simps)
  2.1157 +            hence "Ipoly bs a ^ (k' - k)  * Ipoly bs s =
  2.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"
  2.1159 +              by (simp add: kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
  2.1160 +            hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
  2.1161 +              Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
  2.1162                by (simp add: field_simps)}
  2.1163              hence ieq:"\<forall>(bs :: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
  2.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 
  2.1165 @@ -1415,7 +1539,8 @@
  2.1166              by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
  2.1167            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
  2.1168          }
  2.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))" ..
  2.1170 +        hence hth: "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) =
  2.1171 +            Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
  2.1172            from hth
  2.1173            have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" 
  2.1174              using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
  2.1175 @@ -1426,17 +1551,20 @@
  2.1176            have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
  2.1177            with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
  2.1178              polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
  2.1179 -          have ?ths apply (clarsimp simp add: Let_def)
  2.1180 -            apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
  2.1181 +          have ?ths
  2.1182 +            apply (clarsimp simp add: Let_def)
  2.1183 +            apply (rule exI[where x="?b *\<^sub>p ?xdn"])
  2.1184 +            apply simp
  2.1185              apply (rule exI[where x="0"], simp)
  2.1186 -            done}
  2.1187 -        hence ?ths by blast}
  2.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"]
  2.1189 -          head_nz[OF np] pnz sz ap[symmetric]
  2.1190 +            done }
  2.1191 +        hence ?ths by blast }
  2.1192 +        ultimately have ?ths
  2.1193 +          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"]
  2.1194 +            head_nz[OF np] pnz sz ap[symmetric]
  2.1195            by (simp add: degree_eq_degreen0[symmetric]) blast }
  2.1196        ultimately have ?ths by blast
  2.1197      }
  2.1198 -    ultimately have ?ths by blast}
  2.1199 +    ultimately have ?ths by blast }
  2.1200    ultimately show ?ths by blast
  2.1201  qed
  2.1202  
  2.1203 @@ -1462,16 +1590,18 @@
  2.1204      done
  2.1205  qed
  2.1206  
  2.1207 +
  2.1208  subsection{* More about polypoly and pnormal etc *}
  2.1209  
  2.1210  definition "isnonconstant p = (\<not> isconstant p)"
  2.1211  
  2.1212 -lemma isnonconstant_pnormal_iff: assumes nc: "isnonconstant p" 
  2.1213 +lemma isnonconstant_pnormal_iff:
  2.1214 +  assumes nc: "isnonconstant p" 
  2.1215    shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0" 
  2.1216  proof
  2.1217    let ?p = "polypoly bs p"  
  2.1218    assume H: "pnormal ?p"
  2.1219 -  have csz: "coefficients p \<noteq> []" using nc by (cases p, auto)
  2.1220 +  have csz: "coefficients p \<noteq> []" using nc by (cases p) auto
  2.1221    
  2.1222    from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"]  
  2.1223      pnormal_last_nonzero[OF H]
  2.1224 @@ -1479,7 +1609,7 @@
  2.1225  next
  2.1226    assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
  2.1227    let ?p = "polypoly bs p"
  2.1228 -  have csz: "coefficients p \<noteq> []" using nc by (cases p, auto)
  2.1229 +  have csz: "coefficients p \<noteq> []" using nc by (cases p) auto
  2.1230    hence pz: "?p \<noteq> []" by (simp add: polypoly_def) 
  2.1231    hence lg: "length ?p > 0" by simp
  2.1232    from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] 
  2.1233 @@ -1489,10 +1619,14 @@
  2.1234  
  2.1235  lemma isnonconstant_coefficients_length: "isnonconstant p \<Longrightarrow> length (coefficients p) > 1"
  2.1236    unfolding isnonconstant_def
  2.1237 -  apply (cases p, simp_all)
  2.1238 -  apply (case_tac nat, auto)
  2.1239 +  apply (cases p)
  2.1240 +  apply simp_all
  2.1241 +  apply (case_tac nat)
  2.1242 +  apply auto
  2.1243    done
  2.1244 -lemma isnonconstant_nonconstant: assumes inc: "isnonconstant p"
  2.1245 +
  2.1246 +lemma isnonconstant_nonconstant:
  2.1247 +  assumes inc: "isnonconstant p"
  2.1248    shows "nonconstant (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
  2.1249  proof
  2.1250    let ?p = "polypoly bs p"
  2.1251 @@ -1511,12 +1645,14 @@
  2.1252  qed
  2.1253  
  2.1254  lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
  2.1255 -  unfolding pnormal_def
  2.1256 - apply (induct p)
  2.1257 - apply (simp_all, case_tac "p=[]", simp_all)
  2.1258 - done
  2.1259 +  apply (induct p)
  2.1260 +  apply (simp_all add: pnormal_def)
  2.1261 +  apply (case_tac "p = []")
  2.1262 +  apply simp_all
  2.1263 +  done
  2.1264  
  2.1265 -lemma degree_degree: assumes inc: "isnonconstant p"
  2.1266 +lemma degree_degree:
  2.1267 +  assumes inc: "isnonconstant p"
  2.1268    shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
  2.1269  proof
  2.1270    let  ?p = "polypoly bs p"
  2.1271 @@ -1538,7 +1674,9 @@
  2.1272      unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto
  2.1273  qed
  2.1274  
  2.1275 +
  2.1276  section{* Swaps ; Division by a certain variable *}
  2.1277 +
  2.1278  primrec swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" where
  2.1279    "swap n m (C x) = C x"
  2.1280  | "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
  2.1281 @@ -1550,37 +1688,47 @@
  2.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)
  2.1283    (swap n m p)"
  2.1284  
  2.1285 -lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs"
  2.1286 +lemma swap:
  2.1287 +  assumes nbs: "n < length bs"
  2.1288 +    and mbs: "m < length bs"
  2.1289    shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
  2.1290  proof (induct t)
  2.1291 -  case (Bound k) thus ?case using nbs mbs by simp 
  2.1292 +  case (Bound k)
  2.1293 +  thus ?case using nbs mbs by simp 
  2.1294  next
  2.1295 -  case (CN c k p) thus ?case using nbs mbs by simp 
  2.1296 +  case (CN c k p)
  2.1297 +  thus ?case using nbs mbs by simp 
  2.1298  qed simp_all
  2.1299 -lemma swap_swap_id[simp]: "swap n m (swap m n t) = t"
  2.1300 -  by (induct t,simp_all)
  2.1301  
  2.1302 -lemma swap_commute: "swap n m p = swap m n p" by (induct p, simp_all)
  2.1303 +lemma swap_swap_id [simp]: "swap n m (swap m n t) = t"
  2.1304 +  by (induct t) simp_all
  2.1305 +
  2.1306 +lemma swap_commute: "swap n m p = swap m n p"
  2.1307 +  by (induct p) simp_all
  2.1308  
  2.1309  lemma swap_same_id[simp]: "swap n n t = t"
  2.1310 -  by (induct t, simp_all)
  2.1311 +  by (induct t) simp_all
  2.1312  
  2.1313  definition "swapnorm n m t = polynate (swap n m t)"
  2.1314  
  2.1315 -lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
  2.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"
  2.1317 +lemma swapnorm:
  2.1318 +  assumes nbs: "n < length bs"
  2.1319 +    and mbs: "m < length bs"
  2.1320 +  shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) =
  2.1321 +    Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
  2.1322    using swap[OF assms] swapnorm_def by simp
  2.1323  
  2.1324 -lemma swapnorm_isnpoly[simp]: 
  2.1325 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  2.1326 +lemma swapnorm_isnpoly [simp]:
  2.1327 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  2.1328    shows "isnpoly (swapnorm n m p)"
  2.1329    unfolding swapnorm_def by simp
  2.1330  
  2.1331  definition "polydivideby n s p = 
  2.1332 -    (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp
  2.1333 -     in (k,swapnorm 0 n h,swapnorm 0 n r))"
  2.1334 +  (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp
  2.1335 +   in (k,swapnorm 0 n h,swapnorm 0 n r))"
  2.1336  
  2.1337 -lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)" by (induct p, simp_all)
  2.1338 +lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)"
  2.1339 +  by (induct p) simp_all
  2.1340  
  2.1341  fun isweaknpoly :: "poly \<Rightarrow> bool"
  2.1342  where
  2.1343 @@ -1589,9 +1737,9 @@
  2.1344  | "isweaknpoly p = False"
  2.1345  
  2.1346  lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p" 
  2.1347 -  by (induct p arbitrary: n0, auto)
  2.1348 +  by (induct p arbitrary: n0) auto
  2.1349  
  2.1350  lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)" 
  2.1351 -  by (induct p, auto)
  2.1352 +  by (induct p) auto
  2.1353  
  2.1354  end
  2.1355 \ No newline at end of file