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.54    "headconst (CN c n p) = headconst p"
    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.276  lemma headconst_isnormNum: "isnpolyh p n0 \<Longrightarrow> isnormNum (headconst p)"
   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.287 -proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
   1.288 +proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
   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.315 -by (simp add: polysub_def polyneg polyadd)
   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.318 -by (simp add: polysub_def polyneg_normh polyadd_normh)
   1.319 +  by (simp add: polysub_def polyneg_normh polyadd_normh)
   1.320  
   1.321  lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub p q)"
   1.322    using polyadd_norm polyneg_norm by (simp add: polysub_def) 
   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.400 +     (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
   1.401 +      simp_all add: isnpoly_def)
   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.419    by (simp add: shift1_def)
   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.445    by (simp add: funpow_shift1)
   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.450  lemma behead:
   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.463 +    apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
   1.464 +    apply (simp_all add: th[symmetric] field_simps)
   1.465 +    done
   1.466  qed (auto simp add: Let_def)
   1.467  
   1.468  lemma behead_isnpolyh:
   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.504  lemma head_polybound0: "isnpolyh p n0 \<Longrightarrow> polybound0 (head p)"
   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.598  lemma coefficients_head: "last (coefficients p) = head p"
   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.676  lemma head_isnpolyh: "isnpolyh p n0 \<Longrightarrow> isnpolyh (head p) n0" 
   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.684  lemma head_eq_headn0: "head p = headn p 0"
   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.689    by (simp add: head_eq_headn0)
   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.715        with coefficients_head[of p, symmetric]
   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.732 +lemma polyadd_commute:
   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.737    using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
   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.742  lemma polyadd_0[simp]: 
   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.826  lemma degree_polyadd:
   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.842  lemma degree_polysub_samehead: 
   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.851 -proof(induct p q rule:polyadd.induct)
   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.896      from H(3) headcnp headcnp' nn' have ?case by 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.908      from H(3) headcnp headcnp' nn' have ?case by auto}
   1.909    ultimately show ?case  by blast
   1.910  qed auto
   1.911   
   1.912  lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p"
   1.913 -by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def)
   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.926      and "head (shift1 p) = head p" by (simp_all add: shift1_head) 
   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.932    by (simp add: shift1_def)
   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.949  lemma head_head[simp]: "isnpolyh p n0 \<Longrightarrow> head (head p) = head p"
   1.950 -  by (induct p rule: head.induct, auto)
   1.951 +  by (induct p rule: head.induct) auto
   1.952  
   1.953  lemma polyadd_eq_const_degree: 
   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.960 +lemma polyadd_head:
   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.971 -apply (auto simp add: polyadd_eq_const_degree)
   1.972 -apply (metis head_nz)
   1.973 -apply (metis head_nz)
   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.984 +  apply (auto simp add: polyadd_eq_const_degree)
   1.985 +  apply (metis head_nz)
   1.986 +  apply (metis head_nz)
   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.991  lemma polymul_head_polyeq: 
   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.997    hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum c"  by (simp_all add: head_isnpolyh)
   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.1002    hence "isnpolyh (head (CN c n p)) n0" "isnormNum c'"  by (simp_all add: head_isnpolyh)
  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.1044  lemma degree_head[simp]: "degree (head p) = 0"
  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.1056 +lemma polyadd_different_degree:
  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.1077  lemma polyneg_head: "isnpolyh p n \<Longrightarrow> head(polyneg p) = polyneg (head p)"
  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.1162                by (simp add: field_simps)}
  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.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"]
  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