src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 41807 ab5d2d81f9fb
parent 41763 8ce56536fda7
child 41816 7a55699805dc
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 18:29:47 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 23:47:19 2011 +0100
     1.3 @@ -253,53 +253,53 @@
     1.4        \<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)"
     1.5  proof(induct p q arbitrary: n0 n1 rule: polyadd.induct)
     1.6    case (2 a b c' n' p' n0 n1)
     1.7 -  from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
     1.8 -  from prems(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
     1.9 +  from 2 have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
    1.10 +  from 2(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
    1.11    with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
    1.12 -  with prems(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
    1.13 +  with 2(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
    1.14    from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
    1.15 -  thus ?case using prems th3 by simp
    1.16 +  thus ?case using 2 th3 by simp
    1.17  next
    1.18    case (3 c' n' p' a b n1 n0)
    1.19 -  from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
    1.20 -  from prems(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
    1.21 +  from 3 have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
    1.22 +  from 3(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
    1.23    with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
    1.24 -  with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
    1.25 +  with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
    1.26    from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
    1.27 -  thus ?case using prems th3 by simp
    1.28 +  thus ?case using 3 th3 by simp
    1.29  next
    1.30    case (4 c n p c' n' p' n0 n1)
    1.31    hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all
    1.32 -  from prems have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all 
    1.33 -  from prems have ngen0: "n \<ge> n0" by simp
    1.34 -  from prems have n'gen1: "n' \<ge> n1" by simp 
    1.35 +  from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all 
    1.36 +  from 4 have ngen0: "n \<ge> n0" by simp
    1.37 +  from 4 have n'gen1: "n' \<ge> n1" by simp 
    1.38    have "n < n' \<or> n' < n \<or> n = n'" by auto
    1.39    moreover {assume eq: "n = n'"
    1.40 -    with prems(2)[OF nc nc'] 
    1.41 +    with 4(2)[OF nc nc'] 
    1.42      have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto
    1.43      hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
    1.44        using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
    1.45 -    from eq prems(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
    1.46 +    from eq 4(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
    1.47      have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp
    1.48 -    from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
    1.49 +    from minle npp' ncc'n01 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
    1.50    moreover {assume lt: "n < n'"
    1.51      have "min n0 n1 \<le> n0" by simp
    1.52 -    with prems have th1:"min n0 n1 \<le> n" by auto 
    1.53 -    from prems have th21: "isnpolyh c (Suc n)" by simp
    1.54 -    from prems have th22: "isnpolyh (CN c' n' p') n'" by simp
    1.55 +    with 4 have th1:"min n0 n1 \<le> n" by auto 
    1.56 +    from 4 have th21: "isnpolyh c (Suc n)" by simp
    1.57 +    from 4 have th22: "isnpolyh (CN c' n' p') n'" by simp
    1.58      from lt have th23: "min (Suc n) n' = Suc n" by arith
    1.59 -    from prems(4)[OF th21 th22]
    1.60 +    from 4(4)[OF th21 th22]
    1.61      have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp
    1.62 -    with prems th1 have ?case by simp } 
    1.63 +    with 4 lt th1 have ?case by simp }
    1.64    moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp
    1.65      have "min n0 n1 \<le> n1"  by simp
    1.66 -    with prems have th1:"min n0 n1 \<le> n'" by auto
    1.67 -    from prems have th21: "isnpolyh c' (Suc n')" by simp_all
    1.68 -    from prems have th22: "isnpolyh (CN c n p) n" by simp
    1.69 +    with 4 have th1:"min n0 n1 \<le> n'" by auto
    1.70 +    from 4 have th21: "isnpolyh c' (Suc n')" by simp_all
    1.71 +    from 4 have th22: "isnpolyh (CN c n p) n" by simp
    1.72      from gt have th23: "min n (Suc n') = Suc n'" by arith
    1.73 -    from prems(3)[OF th22 th21]
    1.74 +    from 4(3)[OF th22 th21]
    1.75      have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp
    1.76 -    with prems th1 have ?case by simp}
    1.77 +    with 4 gt th1 have ?case by simp}
    1.78        ultimately show ?case by blast
    1.79  qed auto
    1.80  
    1.81 @@ -370,14 +370,15 @@
    1.82    \<Longrightarrow> degreen p m = degreen q m"
    1.83  proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
    1.84    case (4 c n p c' n' p' m n0 n1 x) 
    1.85 -  {assume nn': "n' < n" hence ?case using prems by simp}
    1.86 +  {assume nn': "n' < n" hence ?case using 4 by simp}
    1.87    moreover 
    1.88    {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
    1.89 -    moreover {assume "n < n'" with prems have ?case by simp }
    1.90 -    moreover {assume eq: "n = n'" hence ?case using prems 
    1.91 +    moreover {assume "n < n'" with 4 have ?case by simp }
    1.92 +    moreover {assume eq: "n = n'" hence ?case using 4 
    1.93          apply (cases "p +\<^sub>p p' = 0\<^sub>p")
    1.94          apply (auto simp add: Let_def)
    1.95 -        by blast
    1.96 +        apply blast
    1.97 +        done
    1.98        }
    1.99      ultimately have ?case by blast}
   1.100    ultimately show ?case by blast
   1.101 @@ -664,13 +665,13 @@
   1.102  qed
   1.103  
   1.104  lemma polypow_normh: 
   1.105 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.106 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.107    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
   1.108  proof (induct k arbitrary: n rule: polypow.induct)
   1.109    case (2 k n)
   1.110    let ?q = "polypow (Suc k div 2) p"
   1.111    let ?d = "polymul (?q,?q)"
   1.112 -  from prems have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
   1.113 +  from 2 have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
   1.114    from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp
   1.115    from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul(p,?d)) n" by simp
   1.116    from dn on show ?case by (simp add: Let_def)
   1.117 @@ -695,7 +696,7 @@
   1.118  
   1.119  
   1.120  lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
   1.121 -by (simp add: shift1_def polymul)
   1.122 +  by (simp add: shift1_def)
   1.123  
   1.124  lemma shift1_isnpoly: 
   1.125    assumes pn: "isnpoly p" and pnz: "p \<noteq> 0\<^sub>p" shows "isnpoly (shift1 p) "
   1.126 @@ -713,7 +714,7 @@
   1.127    using f np by (induct k arbitrary: p, auto)
   1.128  
   1.129  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.130 -  by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
   1.131 +  by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
   1.132  
   1.133  lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
   1.134    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   1.135 @@ -731,10 +732,10 @@
   1.136    using np
   1.137  proof (induct p arbitrary: n rule: behead.induct)
   1.138    case (1 c p n) hence pn: "isnpolyh p n" by simp
   1.139 -  from prems(2)[OF pn] 
   1.140 +  from 1(1)[OF pn] 
   1.141    have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . 
   1.142    then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
   1.143 -    by (simp_all add: th[symmetric] field_simps power_Suc)
   1.144 +    by (simp_all add: th[symmetric] field_simps)
   1.145  qed (auto simp add: Let_def)
   1.146  
   1.147  lemma behead_isnpolyh:
   1.148 @@ -747,7 +748,7 @@
   1.149    case (goal1 c n p n')
   1.150    hence "n = Suc (n - 1)" by simp
   1.151    hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
   1.152 -  with prems(2) show ?case by simp
   1.153 +  with goal1(2) show ?case by simp
   1.154  qed
   1.155  
   1.156  lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p"
   1.157 @@ -838,7 +839,7 @@
   1.158  qed
   1.159  
   1.160  lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1"
   1.161 -  by (induct p, auto)
   1.162 +  by (induct p) auto
   1.163  
   1.164  lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
   1.165    unfolding wf_bs_def by simp
   1.166 @@ -1033,7 +1034,7 @@
   1.167      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
   1.168  
   1.169  lemma polymul_1[simp]: 
   1.170 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.171 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.172    and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
   1.173    using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 
   1.174      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
   1.175 @@ -1101,17 +1102,17 @@
   1.176  next
   1.177    case (2 a b c' n' p') 
   1.178    let ?c = "(a,b)"
   1.179 -  from prems have "degree (C ?c) = degree (CN c' n' p')" by simp
   1.180 +  from 2 have "degree (C ?c) = degree (CN c' n' p')" by simp
   1.181    hence nz:"n' > 0" by (cases n', auto)
   1.182    hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
   1.183 -  with prems show ?case by simp
   1.184 +  with 2 show ?case by simp
   1.185  next
   1.186    case (3 c n p a' b') 
   1.187    let ?c' = "(a',b')"
   1.188 -  from prems have "degree (C ?c') = degree (CN c n p)" by simp
   1.189 +  from 3 have "degree (C ?c') = degree (CN c n p)" by simp
   1.190    hence nz:"n > 0" by (cases n, auto)
   1.191    hence "head (CN c n p) = CN c n p" by (cases n, auto)
   1.192 -  with prems show ?case by simp
   1.193 +  with 3 show ?case by simp
   1.194  next
   1.195    case (4 c n p c' n' p')
   1.196    hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" 
   1.197 @@ -1126,36 +1127,40 @@
   1.198    moreover
   1.199    {assume nn': "n = n'"
   1.200      have "n = 0 \<or> n >0" by arith
   1.201 -    moreover {assume nz: "n = 0" hence ?case using prems by (auto simp add: Let_def degcmc')}
   1.202 +    moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')}
   1.203      moreover {assume nz: "n > 0"
   1.204 -      with nn' H(3) have  cc':"c = c'" and pp': "p = p'" by (cases n, auto)+
   1.205 -      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 split_def fst_conv snd_conv] using nn' prems by (simp add: Let_def)}
   1.206 +      with nn' H(3) have  cc': "c = c'" and pp': "p = p'" by (cases n, auto)+
   1.207 +      hence ?case
   1.208 +        using polysub_same_0 [OF p'nh, simplified polysub_def split_def fst_conv snd_conv]
   1.209 +          polysub_same_0 [OF c'nh, simplified polysub_def split_def fst_conv snd_conv]
   1.210 +        using 4 nn' by (simp add: Let_def) }
   1.211      ultimately have ?case by blast}
   1.212    moreover
   1.213    {assume nn': "n < n'" hence n'p: "n' > 0" by simp 
   1.214      hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n', simp_all)
   1.215 -    have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" using prems by (cases n', simp_all)
   1.216 -    hence "n > 0" by (cases n, simp_all)
   1.217 -    hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto)
   1.218 -    from H(3) headcnp headcnp' nn' have ?case by auto}
   1.219 +    have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')"
   1.220 +      using 4 nn' by (cases n', simp_all)
   1.221 +    hence "n > 0" by (cases n) simp_all
   1.222 +    hence headcnp: "head (CN c n p) = CN c n p" by (cases n) auto
   1.223 +    from H(3) headcnp headcnp' nn' have ?case by auto }
   1.224    moreover
   1.225    {assume nn': "n > n'"  hence np: "n > 0" by simp 
   1.226 -    hence headcnp:"head (CN c n p) = CN c n p"  by (cases n, simp_all)
   1.227 -    from prems have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
   1.228 -    from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all)
   1.229 +    hence headcnp: "head (CN c n p) = CN c n p" by (cases n) simp_all
   1.230 +    from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
   1.231 +    from np have degcnp: "degree (CN c n p) = 0" by (cases n) simp_all
   1.232      with degcnpeq have "n' > 0" by (cases n', simp_all)
   1.233 -    hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
   1.234 -    from H(3) headcnp headcnp' nn' have ?case by auto}
   1.235 +    hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n') auto
   1.236 +    from H(3) headcnp headcnp' nn' have ?case by auto }
   1.237    ultimately show ?case  by blast
   1.238  qed auto 
   1.239   
   1.240  lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p"
   1.241 -by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def)
   1.242 +  by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def)
   1.243  
   1.244  lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
   1.245  proof(induct k arbitrary: n0 p)
   1.246    case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
   1.247 -  with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
   1.248 +  with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
   1.249      and "head (shift1 p) = head p" by (simp_all add: shift1_head) 
   1.250    thus ?case by (simp add: funpow_swap1)
   1.251  qed auto  
   1.252 @@ -1194,19 +1199,20 @@
   1.253  apply (metis head_nz)
   1.254  apply (metis head_nz)
   1.255  apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
   1.256 -by (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
   1.257 +apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
   1.258 +done
   1.259  
   1.260  lemma polymul_head_polyeq: 
   1.261 -   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.262 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.263    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.264  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   1.265    case (2 a b c' n' p' n0 n1)
   1.266    hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum (a,b)"  by (simp_all add: head_isnpolyh)
   1.267 -  thus ?case using prems by (cases n', auto) 
   1.268 +  thus ?case using 2 by (cases n') auto
   1.269  next 
   1.270    case (3 c n p a' b' n0 n1) 
   1.271    hence "isnpolyh (head (CN c n p)) n0" "isnormNum (a',b')"  by (simp_all add: head_isnpolyh)
   1.272 -  thus ?case using prems by (cases n, auto)
   1.273 +  thus ?case using 3 by (cases n) auto
   1.274  next
   1.275    case (4 c n p c' n' p' n0 n1)
   1.276    hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
   1.277 @@ -1215,15 +1221,14 @@
   1.278    have "n < n' \<or> n' < n \<or> n = n'" by arith
   1.279    moreover 
   1.280    {assume nn': "n < n'" hence ?case 
   1.281 -      thm prems
   1.282 -      using norm 
   1.283 -    prems(6)[rule_format, OF nn' norm(1,6)]
   1.284 -    prems(7)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
   1.285 +    using norm 
   1.286 +    4(5)[rule_format, OF nn' norm(1,6)]
   1.287 +    4(6)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all) }
   1.288    moreover {assume nn': "n'< n"
   1.289      hence stupid: "n' < n \<and> \<not> n < n'" by simp
   1.290 -    hence ?case using norm prems(4) [rule_format, OF stupid norm(5,3)]
   1.291 -      prems(5)[rule_format, OF stupid norm(5,4)] 
   1.292 -      by (simp,cases n',simp,cases n,auto)}
   1.293 +    hence ?case using norm 4(3) [rule_format, OF stupid norm(5,3)]
   1.294 +      4(4)[rule_format, OF stupid norm(5,4)] 
   1.295 +      by (simp,cases n',simp,cases n,auto) }
   1.296    moreover {assume nn': "n' = n"
   1.297      hence stupid: "\<not> n' < n \<and> \<not> n < n'" by simp
   1.298      from nn' polymul_normh[OF norm(5,4)] 
   1.299 @@ -1247,8 +1252,8 @@
   1.300      have dth:"degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
   1.301      hence dth':"degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp
   1.302      from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
   1.303 -    have ?case   using norm prems(2)[rule_format, OF stupid norm(5,3)]
   1.304 -        prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
   1.305 +    have ?case using norm 4(1)[rule_format, OF stupid norm(5,3)]
   1.306 +        4(2)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
   1.307      ultimately have ?case by (cases n) auto} 
   1.308    ultimately show ?case by blast
   1.309  qed simp_all
   1.310 @@ -1603,12 +1608,13 @@
   1.311  
   1.312  definition "swapnorm n m t = polynate (swap n m t)"
   1.313  
   1.314 -lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
   1.315 +lemma swapnorm:
   1.316 +  assumes nbs: "n < length bs" and mbs: "m < length bs"
   1.317    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.318 -  using swap[OF prems] swapnorm_def by simp
   1.319 +  using swap[OF assms] swapnorm_def by simp
   1.320  
   1.321  lemma swapnorm_isnpoly[simp]: 
   1.322 -    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.323 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.324    shows "isnpoly (swapnorm n m p)"
   1.325    unfolding swapnorm_def by simp
   1.326  
   1.327 @@ -1625,9 +1631,9 @@
   1.328    "isweaknpoly p = False"       
   1.329  
   1.330  lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p" 
   1.331 -  by (induct p arbitrary: n0, auto)
   1.332 +  by (induct p arbitrary: n0) auto
   1.333  
   1.334  lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)" 
   1.335 -  by (induct p, auto)
   1.336 +  by (induct p) auto
   1.337  
   1.338  end
   1.339 \ No newline at end of file