src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 56009 dda076a32aea
parent 56000 899ad5a3ad00
child 56043 0b25c3d34b77
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Mar 09 17:43:40 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Mar 09 18:43:38 2014 +0100
     1.3 @@ -188,7 +188,7 @@
     1.4  | "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)"
     1.5  | "poly_cmul y p = C y *\<^sub>p p"
     1.6  
     1.7 -definition monic :: "poly \<Rightarrow> (poly \<times> bool)"
     1.8 +definition monic :: "poly \<Rightarrow> poly \<times> bool"
     1.9  where
    1.10    "monic p =
    1.11      (let h = headconst p
    1.12 @@ -200,7 +200,7 @@
    1.13  definition shift1 :: "poly \<Rightarrow> poly"
    1.14    where "shift1 p = CN 0\<^sub>p 0 p"
    1.15  
    1.16 -abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
    1.17 +abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
    1.18    where "funpow \<equiv> compow"
    1.19  
    1.20  partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly"
    1.21 @@ -250,7 +250,7 @@
    1.22      ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    1.23    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
    1.24  
    1.25 -lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i"
    1.26 +lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i"
    1.27    by (simp add: INum_def)
    1.28  
    1.29  lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j"
    1.30 @@ -278,56 +278,98 @@
    1.31  lemma polyadd_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)"
    1.32  proof (induct p q arbitrary: n0 n1 rule: polyadd.induct)
    1.33    case (2 ab c' n' p' n0 n1)
    1.34 -  from 2 have  th1: "isnpolyh (C ab) (Suc n')" by simp
    1.35 -  from 2(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
    1.36 -  with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
    1.37 -  with 2(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')" by simp
    1.38 -  from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp
    1.39 -  thus ?case using 2 th3 by simp
    1.40 +  from 2 have  th1: "isnpolyh (C ab) (Suc n')"
    1.41 +    by simp
    1.42 +  from 2(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1"
    1.43 +    by simp_all
    1.44 +  with isnpolyh_mono have cp: "isnpolyh c' (Suc n')"
    1.45 +    by simp
    1.46 +  with 2(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')"
    1.47 +    by simp
    1.48 +  from nplen1 have n01len1: "min n0 n1 \<le> n'"
    1.49 +    by simp
    1.50 +  then show ?case using 2 th3
    1.51 +    by simp
    1.52  next
    1.53    case (3 c' n' p' ab n1 n0)
    1.54 -  from 3 have  th1: "isnpolyh (C ab) (Suc n')" by simp
    1.55 -  from 3(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
    1.56 -  with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
    1.57 -  with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')" by simp
    1.58 -  from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp
    1.59 -  thus ?case using 3 th3 by simp
    1.60 +  from 3 have  th1: "isnpolyh (C ab) (Suc n')"
    1.61 +    by simp
    1.62 +  from 3(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1"
    1.63 +    by simp_all
    1.64 +  with isnpolyh_mono have cp: "isnpolyh c' (Suc n')"
    1.65 +    by simp
    1.66 +  with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')"
    1.67 +    by simp
    1.68 +  from nplen1 have n01len1: "min n0 n1 \<le> n'"
    1.69 +    by simp
    1.70 +  then show ?case using 3 th3
    1.71 +    by simp
    1.72  next
    1.73    case (4 c n p c' n' p' n0 n1)
    1.74 -  hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all
    1.75 -  from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all
    1.76 -  from 4 have ngen0: "n \<ge> n0" by simp
    1.77 -  from 4 have n'gen1: "n' \<ge> n1" by simp
    1.78 -  have "n < n' \<or> n' < n \<or> n = n'" by auto
    1.79 -  moreover {
    1.80 +  then have nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n"
    1.81 +    by simp_all
    1.82 +  from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'"
    1.83 +    by simp_all
    1.84 +  from 4 have ngen0: "n \<ge> n0"
    1.85 +    by simp
    1.86 +  from 4 have n'gen1: "n' \<ge> n1"
    1.87 +    by simp
    1.88 +  have "n < n' \<or> n' < n \<or> n = n'"
    1.89 +    by auto
    1.90 +  moreover
    1.91 +  {
    1.92      assume eq: "n = n'"
    1.93      with "4.hyps"(3)[OF nc nc']
    1.94 -    have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto
    1.95 -    hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
    1.96 -      using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
    1.97 -    from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
    1.98 -    have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp
    1.99 -    from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def) }
   1.100 -  moreover {
   1.101 +    have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)"
   1.102 +      by auto
   1.103 +    then have ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
   1.104 +      using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1
   1.105 +      by auto
   1.106 +    from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n"
   1.107 +      by simp
   1.108 +    have minle: "min n0 n1 \<le> n'"
   1.109 +      using ngen0 n'gen1 eq by simp
   1.110 +    from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case
   1.111 +      by (simp add: Let_def)
   1.112 +  }
   1.113 +  moreover
   1.114 +  {
   1.115      assume lt: "n < n'"
   1.116 -    have "min n0 n1 \<le> n0" by simp
   1.117 -    with 4 lt have th1:"min n0 n1 \<le> n" by auto
   1.118 -    from 4 have th21: "isnpolyh c (Suc n)" by simp
   1.119 -    from 4 have th22: "isnpolyh (CN c' n' p') n'" by simp
   1.120 -    from lt have th23: "min (Suc n) n' = Suc n" by arith
   1.121 -    from "4.hyps"(1)[OF th21 th22]
   1.122 -    have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)" using th23 by simp
   1.123 -    with 4 lt th1 have ?case by simp }
   1.124 -  moreover {
   1.125 -    assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp
   1.126 -    have "min n0 n1 \<le> n1"  by simp
   1.127 -    with 4 gt have th1:"min n0 n1 \<le> n'" by auto
   1.128 -    from 4 have th21: "isnpolyh c' (Suc n')" by simp_all
   1.129 -    from 4 have th22: "isnpolyh (CN c n p) n" by simp
   1.130 -    from gt have th23: "min n (Suc n') = Suc n'" by arith
   1.131 -    from "4.hyps"(2)[OF th22 th21]
   1.132 -    have "isnpolyh (polyadd (CN c n p) c') (Suc n')" using th23 by simp
   1.133 -    with 4 gt th1 have ?case by simp }
   1.134 +    have "min n0 n1 \<le> n0"
   1.135 +      by simp
   1.136 +    with 4 lt have th1:"min n0 n1 \<le> n"
   1.137 +      by auto
   1.138 +    from 4 have th21: "isnpolyh c (Suc n)"
   1.139 +      by simp
   1.140 +    from 4 have th22: "isnpolyh (CN c' n' p') n'"
   1.141 +      by simp
   1.142 +    from lt have th23: "min (Suc n) n' = Suc n"
   1.143 +      by arith
   1.144 +    from "4.hyps"(1)[OF th21 th22] have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)"
   1.145 +      using th23 by simp
   1.146 +    with 4 lt th1 have ?case
   1.147 +      by simp
   1.148 +  }
   1.149 +  moreover
   1.150 +  {
   1.151 +    assume gt: "n' < n"
   1.152 +    then have gt': "n' < n \<and> \<not> n < n'"
   1.153 +      by simp
   1.154 +    have "min n0 n1 \<le> n1"
   1.155 +      by simp
   1.156 +    with 4 gt have th1: "min n0 n1 \<le> n'"
   1.157 +      by auto
   1.158 +    from 4 have th21: "isnpolyh c' (Suc n')"
   1.159 +      by simp_all
   1.160 +    from 4 have th22: "isnpolyh (CN c n p) n"
   1.161 +      by simp
   1.162 +    from gt have th23: "min n (Suc n') = Suc n'"
   1.163 +      by arith
   1.164 +    from "4.hyps"(2)[OF th22 th21] have "isnpolyh (polyadd (CN c n p) c') (Suc n')"
   1.165 +      using th23 by simp
   1.166 +    with 4 gt th1 have ?case
   1.167 +      by simp
   1.168 +  }
   1.169    ultimately show ?case by blast
   1.170  qed auto
   1.171  
   1.172 @@ -335,18 +377,22 @@
   1.173    by (induct p q rule: polyadd.induct)
   1.174      (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
   1.175  
   1.176 -lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd p q)"
   1.177 +lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)"
   1.178    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
   1.179  
   1.180  text{* The degree of addition and other general lemmas needed for the normal form of polymul *}
   1.181  
   1.182  lemma polyadd_different_degreen:
   1.183 -  "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow>
   1.184 -  degreen (polyadd p q) m = max (degreen p m) (degreen q m)"
   1.185 +  assumes "isnpolyh p n0"
   1.186 +    and "isnpolyh q n1"
   1.187 +    and "degreen p m \<noteq> degreen q m"
   1.188 +    and "m \<le> min n0 n1"
   1.189 +  shows "degreen (polyadd p q) m = max (degreen p m) (degreen q m)"
   1.190 +  using assms
   1.191  proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
   1.192    case (4 c n p c' n' p' m n0 n1)
   1.193    have "n' = n \<or> n < n' \<or> n' < n" by arith
   1.194 -  thus ?case
   1.195 +  then show ?case
   1.196    proof (elim disjE)
   1.197      assume [simp]: "n' = n"
   1.198      from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
   1.199 @@ -360,10 +406,12 @@
   1.200    qed
   1.201  qed auto
   1.202  
   1.203 -lemma headnz[simp]: "\<lbrakk>isnpolyh p n ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> headn p m \<noteq> 0\<^sub>p"
   1.204 +lemma headnz[simp]: "isnpolyh p n \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> headn p m \<noteq> 0\<^sub>p"
   1.205    by (induct p arbitrary: n rule: headn.induct) auto
   1.206 +
   1.207  lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> degree p = 0"
   1.208    by (induct p arbitrary: n rule: degree.induct) auto
   1.209 +
   1.210  lemma degreen_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> degreen p m = 0"
   1.211    by (induct p arbitrary: n rule: degreen.induct) auto
   1.212  
   1.213 @@ -372,24 +420,29 @@
   1.214  
   1.215  lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degree c = 0"
   1.216    using degree_isnpolyh_Suc by auto
   1.217 +
   1.218  lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degreen c n = 0"
   1.219    using degreen_0 by auto
   1.220  
   1.221  
   1.222  lemma degreen_polyadd:
   1.223 -  assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> max n0 n1"
   1.224 +  assumes np: "isnpolyh p n0"
   1.225 +    and nq: "isnpolyh q n1"
   1.226 +    and m: "m \<le> max n0 n1"
   1.227    shows "degreen (p +\<^sub>p q) m \<le> max (degreen p m) (degreen q m)"
   1.228    using np nq m
   1.229  proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct)
   1.230    case (2 c c' n' p' n0 n1)
   1.231 -  thus ?case  by (cases n') simp_all
   1.232 +  then show ?case
   1.233 +    by (cases n') simp_all
   1.234  next
   1.235    case (3 c n p c' n0 n1)
   1.236 -  thus ?case by (cases n) auto
   1.237 +  then show ?case
   1.238 +    by (cases n) auto
   1.239  next
   1.240    case (4 c n p c' n' p' n0 n1 m)
   1.241    have "n' = n \<or> n < n' \<or> n' < n" by arith
   1.242 -  thus ?case
   1.243 +  then show ?case
   1.244    proof (elim disjE)
   1.245      assume [simp]: "n' = n"
   1.246      from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
   1.247 @@ -397,21 +450,34 @@
   1.248    qed simp_all
   1.249  qed auto
   1.250  
   1.251 -lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\<rbrakk>
   1.252 -  \<Longrightarrow> degreen p m = degreen q m"
   1.253 +lemma polyadd_eq_const_degreen:
   1.254 +  assumes "isnpolyh p n0"
   1.255 +    and "isnpolyh q n1"
   1.256 +    and "polyadd p q = C c"
   1.257 +  shows "degreen p m = degreen q m"
   1.258 +  using assms
   1.259  proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
   1.260    case (4 c n p c' n' p' m n0 n1 x)
   1.261 -  { assume nn': "n' < n" hence ?case using 4 by simp }
   1.262 +  {
   1.263 +    assume nn': "n' < n"
   1.264 +    then have ?case using 4 by simp
   1.265 +  }
   1.266    moreover
   1.267 -  { assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
   1.268 +  {
   1.269 +    assume nn': "\<not> n' < n"
   1.270 +    then have "n < n' \<or> n = n'" by arith
   1.271      moreover { assume "n < n'" with 4 have ?case by simp }
   1.272 -    moreover { assume eq: "n = n'" hence ?case using 4
   1.273 +    moreover
   1.274 +    {
   1.275 +      assume eq: "n = n'"
   1.276 +      then have ?case using 4
   1.277          apply (cases "p +\<^sub>p p' = 0\<^sub>p")
   1.278          apply (auto simp add: Let_def)
   1.279          apply blast
   1.280          done
   1.281      }
   1.282 -    ultimately have ?case by blast }
   1.283 +    ultimately have ?case by blast
   1.284 +  }
   1.285    ultimately show ?case by blast
   1.286  qed simp_all
   1.287  
   1.288 @@ -421,165 +487,201 @@
   1.289      and nq: "isnpolyh q n1"
   1.290      and m: "m \<le> min n0 n1"
   1.291    shows "isnpolyh (p *\<^sub>p q) (min n0 n1)"
   1.292 -    and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)"
   1.293 -    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.294 +    and "p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p"
   1.295 +    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.296    using np nq m
   1.297  proof (induct p q arbitrary: n0 n1 m rule: polymul.induct)
   1.298    case (2 c c' n' p')
   1.299 -  { case (1 n0 n1)
   1.300 -    with "2.hyps"(4-6)[of n' n' n']
   1.301 -      and "2.hyps"(1-3)[of "Suc n'" "Suc n'" n']
   1.302 +  {
   1.303 +    case (1 n0 n1)
   1.304 +    with "2.hyps"(4-6)[of n' n' n'] and "2.hyps"(1-3)[of "Suc n'" "Suc n'" n']
   1.305      show ?case by (auto simp add: min_def)
   1.306    next
   1.307 -    case (2 n0 n1) thus ?case by auto
   1.308 +    case (2 n0 n1)
   1.309 +    then show ?case by auto
   1.310    next
   1.311 -    case (3 n0 n1) thus ?case  using "2.hyps" by auto }
   1.312 +    case (3 n0 n1)
   1.313 +    then show ?case  using "2.hyps" by auto
   1.314 +  }
   1.315  next
   1.316    case (3 c n p c')
   1.317 -  { case (1 n0 n1)
   1.318 -    with "3.hyps"(4-6)[of n n n]
   1.319 -      "3.hyps"(1-3)[of "Suc n" "Suc n" n]
   1.320 +  {
   1.321 +    case (1 n0 n1)
   1.322 +    with "3.hyps"(4-6)[of n n n] and "3.hyps"(1-3)[of "Suc n" "Suc n" n]
   1.323      show ?case by (auto simp add: min_def)
   1.324    next
   1.325 -    case (2 n0 n1) thus ?case by auto
   1.326 +    case (2 n0 n1)
   1.327 +    then show ?case by auto
   1.328    next
   1.329 -    case (3 n0 n1) thus ?case  using "3.hyps" by auto }
   1.330 +    case (3 n0 n1)
   1.331 +    then show ?case  using "3.hyps" by auto
   1.332 +  }
   1.333  next
   1.334    case (4 c n p c' n' p')
   1.335    let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'"
   1.336 +  {
   1.337 +    case (1 n0 n1)
   1.338 +    then have cnp: "isnpolyh ?cnp n"
   1.339 +      and cnp': "isnpolyh ?cnp' n'"
   1.340 +      and np: "isnpolyh p n"
   1.341 +      and nc: "isnpolyh c (Suc n)"
   1.342 +      and np': "isnpolyh p' n'"
   1.343 +      and nc': "isnpolyh c' (Suc n')"
   1.344 +      and nn0: "n \<ge> n0"
   1.345 +      and nn1: "n' \<ge> n1"
   1.346 +      by simp_all
   1.347      {
   1.348 -      case (1 n0 n1)
   1.349 -      hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'"
   1.350 -        and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)"
   1.351 -        and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
   1.352 -        and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
   1.353 -        by simp_all
   1.354 -      { assume "n < n'"
   1.355 -        with "4.hyps"(4-5)[OF np cnp', of n]
   1.356 -          "4.hyps"(1)[OF nc cnp', of n] nn0 cnp
   1.357 -        have ?case by (simp add: min_def)
   1.358 -      } moreover {
   1.359 -        assume "n' < n"
   1.360 -        with "4.hyps"(16-17)[OF cnp np', of "n'"]
   1.361 -          "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp'
   1.362 -        have ?case
   1.363 -          by (cases "Suc n' = n") (simp_all add: min_def)
   1.364 -      } moreover {
   1.365 -        assume "n' = n"
   1.366 -        with "4.hyps"(16-17)[OF cnp np', of n]
   1.367 -          "4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0
   1.368 -        have ?case
   1.369 -          apply (auto intro!: polyadd_normh)
   1.370 -          apply (simp_all add: min_def isnpolyh_mono[OF nn0])
   1.371 -          done
   1.372 +      assume "n < n'"
   1.373 +      with "4.hyps"(4-5)[OF np cnp', of n] and "4.hyps"(1)[OF nc cnp', of n] nn0 cnp
   1.374 +      have ?case by (simp add: min_def)
   1.375 +    } moreover {
   1.376 +      assume "n' < n"
   1.377 +      with "4.hyps"(16-17)[OF cnp np', of "n'"] and "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp'
   1.378 +      have ?case by (cases "Suc n' = n") (simp_all add: min_def)
   1.379 +    } moreover {
   1.380 +      assume "n' = n"
   1.381 +      with "4.hyps"(16-17)[OF cnp np', of n] and "4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0
   1.382 +      have ?case
   1.383 +        apply (auto intro!: polyadd_normh)
   1.384 +        apply (simp_all add: min_def isnpolyh_mono[OF nn0])
   1.385 +        done
   1.386 +    }
   1.387 +    ultimately show ?case by arith
   1.388 +  next
   1.389 +    fix n0 n1 m
   1.390 +    assume np: "isnpolyh ?cnp n0"
   1.391 +    assume np':"isnpolyh ?cnp' n1"
   1.392 +    assume m: "m \<le> min n0 n1"
   1.393 +    let ?d = "degreen (?cnp *\<^sub>p ?cnp') m"
   1.394 +    let ?d1 = "degreen ?cnp m"
   1.395 +    let ?d2 = "degreen ?cnp' m"
   1.396 +    let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0  else ?d1 + ?d2)"
   1.397 +    have "n'<n \<or> n < n' \<or> n' = n" by auto
   1.398 +    moreover
   1.399 +    {
   1.400 +      assume "n' < n \<or> n < n'"
   1.401 +      with "4.hyps"(3,6,18) np np' m have ?eq
   1.402 +        by auto
   1.403 +    }
   1.404 +    moreover
   1.405 +    {
   1.406 +      assume nn': "n' = n"
   1.407 +      then have nn: "\<not> n' < n \<and> \<not> n < n'" by arith
   1.408 +      from "4.hyps"(16,18)[of n n' n]
   1.409 +        "4.hyps"(13,14)[of n "Suc n'" n]
   1.410 +        np np' nn'
   1.411 +      have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   1.412 +        "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   1.413 +        "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
   1.414 +        "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
   1.415 +      {
   1.416 +        assume mn: "m = n"
   1.417 +        from "4.hyps"(17,18)[OF norm(1,4), of n]
   1.418 +          "4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn
   1.419 +        have degs:
   1.420 +          "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else ?d1 + degreen c' n)"
   1.421 +          "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n"
   1.422 +          by (simp_all add: min_def)
   1.423 +        from degs norm have th1: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
   1.424 +          by simp
   1.425 +        then have neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
   1.426 +          by simp
   1.427 +        have nmin: "n \<le> min n n"
   1.428 +          by (simp add: min_def)
   1.429 +        from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
   1.430 +        have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n =
   1.431 +            degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   1.432 +          by simp
   1.433 +        from "4.hyps"(16-18)[OF norm(1,4), of n]
   1.434 +          "4.hyps"(13-15)[OF norm(1,2), of n]
   1.435 +          mn norm m nn' deg
   1.436 +        have ?eq by simp
   1.437        }
   1.438 -      ultimately show ?case by arith
   1.439 -    next
   1.440 -      fix n0 n1 m
   1.441 -      assume np: "isnpolyh ?cnp n0" and np':"isnpolyh ?cnp' n1"
   1.442 -      and m: "m \<le> min n0 n1"
   1.443 -      let ?d = "degreen (?cnp *\<^sub>p ?cnp') m"
   1.444 -      let ?d1 = "degreen ?cnp m"
   1.445 -      let ?d2 = "degreen ?cnp' m"
   1.446 -      let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0  else ?d1 + ?d2)"
   1.447 -      have "n'<n \<or> n < n' \<or> n' = n" by auto
   1.448 -      moreover
   1.449 -      {assume "n' < n \<or> n < n'"
   1.450 -        with "4.hyps"(3,6,18) np np' m
   1.451 -        have ?eq by auto }
   1.452        moreover
   1.453 -      { assume nn': "n' = n"
   1.454 -        hence nn: "\<not> n' < n \<and> \<not> n < n'" by arith
   1.455 -        from "4.hyps"(16,18)[of n n' n]
   1.456 -          "4.hyps"(13,14)[of n "Suc n'" n]
   1.457 -          np np' nn'
   1.458 -        have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   1.459 -          "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   1.460 -          "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
   1.461 -          "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
   1.462 -        { assume mn: "m = n"
   1.463 -          from "4.hyps"(17,18)[OF norm(1,4), of n]
   1.464 -            "4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn
   1.465 -          have degs:  "degreen (?cnp *\<^sub>p c') n =
   1.466 -            (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
   1.467 -            "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
   1.468 -          from degs norm
   1.469 -          have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
   1.470 -          hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
   1.471 -            by simp
   1.472 -          have nmin: "n \<le> min n n" by (simp add: min_def)
   1.473 -          from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
   1.474 -          have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n = degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
   1.475 -          from "4.hyps"(16-18)[OF norm(1,4), of n]
   1.476 -            "4.hyps"(13-15)[OF norm(1,2), of n]
   1.477 -            mn norm m nn' deg
   1.478 -          have ?eq by simp }
   1.479 -        moreover
   1.480 -        { assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
   1.481 -          from nn' m np have max1: "m \<le> max n n"  by simp
   1.482 -          hence min1: "m \<le> min n n" by simp
   1.483 -          hence min2: "m \<le> min n (Suc n)" by simp
   1.484 -          from "4.hyps"(16-18)[OF norm(1,4) min1]
   1.485 -            "4.hyps"(13-15)[OF norm(1,2) min2]
   1.486 -            degreen_polyadd[OF norm(3,6) max1]
   1.487 -
   1.488 -          have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m
   1.489 -            \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
   1.490 -            using mn nn' np np' by simp
   1.491 -          with "4.hyps"(16-18)[OF norm(1,4) min1]
   1.492 -            "4.hyps"(13-15)[OF norm(1,2) min2]
   1.493 -            degreen_0[OF norm(3) mn']
   1.494 -          have ?eq using nn' mn np np' by clarsimp }
   1.495 -        ultimately have ?eq by blast }
   1.496 -      ultimately show ?eq by blast }
   1.497 -    { case (2 n0 n1)
   1.498 -      hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1"
   1.499 -        and m: "m \<le> min n0 n1" by simp_all
   1.500 -      hence mn: "m \<le> n" by simp
   1.501 -      let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
   1.502 -      {assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
   1.503 -        hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
   1.504 -        from "4.hyps"(16-18) [of n n n]
   1.505 -          "4.hyps"(13-15)[of n "Suc n" n]
   1.506 -          np np' C(2) mn
   1.507 -        have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   1.508 -          "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   1.509 -          "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
   1.510 -          "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"
   1.511 -          "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
   1.512 -            "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
   1.513 -          by (simp_all add: min_def)
   1.514 -
   1.515 -          from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
   1.516 -          have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
   1.517 -            using norm by simp
   1.518 -        from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"]  degneq
   1.519 -        have "False" by simp }
   1.520 -      thus ?case using "4.hyps" by clarsimp }
   1.521 +      {
   1.522 +        assume mn: "m \<noteq> n"
   1.523 +        then have mn': "m < n"
   1.524 +          using m np by auto
   1.525 +        from nn' m np have max1: "m \<le> max n n"
   1.526 +          by simp
   1.527 +        then have min1: "m \<le> min n n"
   1.528 +          by simp
   1.529 +        then have min2: "m \<le> min n (Suc n)"
   1.530 +          by simp
   1.531 +        from "4.hyps"(16-18)[OF norm(1,4) min1]
   1.532 +          "4.hyps"(13-15)[OF norm(1,2) min2]
   1.533 +          degreen_polyadd[OF norm(3,6) max1]
   1.534 +        have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m \<le>
   1.535 +            max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
   1.536 +          using mn nn' np np' by simp
   1.537 +        with "4.hyps"(16-18)[OF norm(1,4) min1]
   1.538 +          "4.hyps"(13-15)[OF norm(1,2) min2]
   1.539 +          degreen_0[OF norm(3) mn']
   1.540 +        have ?eq using nn' mn np np' by clarsimp
   1.541 +      }
   1.542 +      ultimately have ?eq by blast
   1.543 +    }
   1.544 +    ultimately show ?eq by blast
   1.545 +  }
   1.546 +  {
   1.547 +    case (2 n0 n1)
   1.548 +    then have np: "isnpolyh ?cnp n0"
   1.549 +      and np': "isnpolyh ?cnp' n1"
   1.550 +      and m: "m \<le> min n0 n1" by simp_all
   1.551 +    then have mn: "m \<le> n" by simp
   1.552 +    let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
   1.553 +    {
   1.554 +      assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
   1.555 +      then have nn: "\<not> n' < n \<and> \<not> n < n'"
   1.556 +        by simp
   1.557 +      from "4.hyps"(16-18) [of n n n]
   1.558 +        "4.hyps"(13-15)[of n "Suc n" n]
   1.559 +        np np' C(2) mn
   1.560 +      have norm:
   1.561 +        "isnpolyh ?cnp n"
   1.562 +        "isnpolyh c' (Suc n)"
   1.563 +        "isnpolyh (?cnp *\<^sub>p c') n"
   1.564 +        "isnpolyh p' n"
   1.565 +        "isnpolyh (?cnp *\<^sub>p p') n"
   1.566 +        "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   1.567 +        "?cnp *\<^sub>p c' = 0\<^sub>p \<longleftrightarrow> c' = 0\<^sub>p"
   1.568 +        "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"
   1.569 +        "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
   1.570 +        "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
   1.571 +        by (simp_all add: min_def)
   1.572 +      from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   1.573 +        by simp
   1.574 +      have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
   1.575 +        using norm by simp
   1.576 +      from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq
   1.577 +      have False by simp
   1.578 +    }
   1.579 +    then show ?case using "4.hyps" by clarsimp
   1.580 +  }
   1.581  qed auto
   1.582  
   1.583 -lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)"
   1.584 +lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = Ipoly bs p * Ipoly bs q"
   1.585    by (induct p q rule: polymul.induct) (auto simp add: field_simps)
   1.586  
   1.587  lemma polymul_normh:
   1.588    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.589 -  shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
   1.590 +  shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
   1.591    using polymul_properties(1) by blast
   1.592  
   1.593  lemma polymul_eq0_iff:
   1.594    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.595 -  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.596 +  shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p"
   1.597    using polymul_properties(2) by blast
   1.598  
   1.599  lemma polymul_degreen:  (* FIXME duplicate? *)
   1.600    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.601 -  shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow>
   1.602 -    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.603 +  shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow>
   1.604 +    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.605    using polymul_properties(3) by blast
   1.606  
   1.607  lemma polymul_norm:
   1.608    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.609 -  shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul p q)"
   1.610 +  shows "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polymul p q)"
   1.611    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
   1.612  
   1.613  lemma headconst_zero: "isnpolyh p n0 \<Longrightarrow> headconst p = 0\<^sub>N \<longleftrightarrow> p = 0\<^sub>p"
   1.614 @@ -601,7 +703,7 @@
   1.615      from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all
   1.616      from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp
   1.617      with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast}
   1.618 -  thus "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast
   1.619 +  then show "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast
   1.620  qed
   1.621  
   1.622  
   1.623 @@ -610,12 +712,14 @@
   1.624  lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
   1.625    by (induct p rule: polyneg.induct) auto
   1.626  
   1.627 -lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)"
   1.628 +lemma polyneg0: "isnpolyh p n \<Longrightarrow> (~\<^sub>p p) = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p"
   1.629    by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: Nneg_def)
   1.630 +
   1.631  lemma polyneg_polyneg: "isnpolyh p n0 \<Longrightarrow> ~\<^sub>p (~\<^sub>p p) = p"
   1.632    by (induct p arbitrary: n0 rule: polyneg.induct) auto
   1.633 -lemma polyneg_normh: "\<And>n. isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n "
   1.634 -  by (induct p rule: polyneg.induct) (auto simp add: polyneg0)
   1.635 +
   1.636 +lemma polyneg_normh: "isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n"
   1.637 +  by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: polyneg0)
   1.638  
   1.639  lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)"
   1.640    using isnpoly_def polyneg_normh by simp
   1.641 @@ -623,14 +727,15 @@
   1.642  
   1.643  text{* polysub is a substraction and preserves normal forms *}
   1.644  
   1.645 -lemma polysub[simp]: "Ipoly bs (polysub p q) = (Ipoly bs p) - (Ipoly bs q)"
   1.646 +lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p - Ipoly bs q"
   1.647    by (simp add: polysub_def)
   1.648 -lemma polysub_normh:
   1.649 -  "\<And>n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub p q) (min n0 n1)"
   1.650 +
   1.651 +lemma polysub_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polysub p q) (min n0 n1)"
   1.652    by (simp add: polysub_def polyneg_normh polyadd_normh)
   1.653  
   1.654 -lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub p q)"
   1.655 +lemma polysub_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polysub p q)"
   1.656    using polyadd_norm polyneg_norm by (simp add: polysub_def)
   1.657 +
   1.658  lemma polysub_same_0[simp]:
   1.659    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.660    shows "isnpolyh p n0 \<Longrightarrow> polysub p p = 0\<^sub>p"
   1.661 @@ -639,17 +744,18 @@
   1.662  
   1.663  lemma polysub_0:
   1.664    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.665 -  shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
   1.666 +  shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p -\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = q"
   1.667    unfolding polysub_def split_def fst_conv snd_conv
   1.668    by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
   1.669      (auto simp: Nsub0[simplified Nsub_def] Let_def)
   1.670  
   1.671  text{* polypow is a power function and preserves normal forms *}
   1.672  
   1.673 -lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0,field_inverse_zero})) ^ n"
   1.674 +lemma polypow[simp]:
   1.675 +  "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n"
   1.676  proof (induct n rule: polypow.induct)
   1.677    case 1
   1.678 -  thus ?case by simp
   1.679 +  then show ?case by simp
   1.680  next
   1.681    case (2 n)
   1.682    let ?q = "polypow ((Suc n) div 2) p"
   1.683 @@ -756,7 +862,8 @@
   1.684      (Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})"
   1.685    using np
   1.686  proof (induct p arbitrary: n rule: behead.induct)
   1.687 -  case (1 c p n) hence pn: "isnpolyh p n" by simp
   1.688 +  case (1 c p n)
   1.689 +  then have pn: "isnpolyh p n" by simp
   1.690    from 1(1)[OF pn]
   1.691    have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" .
   1.692    then show ?case using "1.hyps"
   1.693 @@ -776,9 +883,12 @@
   1.694  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
   1.695  proof (induct p arbitrary: n rule: poly.induct, auto)
   1.696    case (goal1 c n p n')
   1.697 -  hence "n = Suc (n - 1)" by simp
   1.698 -  hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
   1.699 -  with goal1(2) show ?case by simp
   1.700 +  then have "n = Suc (n - 1)"
   1.701 +    by simp
   1.702 +  then have "isnpolyh p (Suc (n - 1))"
   1.703 +    using `isnpolyh p n` by simp
   1.704 +  with goal1(2) show ?case
   1.705 +    by simp
   1.706  qed
   1.707  
   1.708  lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p"
   1.709 @@ -800,16 +910,16 @@
   1.710  
   1.711  lemma polybound0_I:
   1.712    assumes nb: "polybound0 a"
   1.713 -  shows "Ipoly (b#bs) a = Ipoly (b'#bs) a"
   1.714 +  shows "Ipoly (b # bs) a = Ipoly (b' # bs) a"
   1.715    using nb
   1.716    by (induct a rule: poly.induct) auto
   1.717  
   1.718 -lemma polysubst0_I: "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
   1.719 +lemma polysubst0_I: "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b # bs) a) # bs) t"
   1.720    by (induct t) simp_all
   1.721  
   1.722  lemma polysubst0_I':
   1.723    assumes nb: "polybound0 a"
   1.724 -  shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b'#bs) a)#bs) t"
   1.725 +  shows "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b' # bs) a) # bs) t"
   1.726    by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"])
   1.727  
   1.728  lemma decrpoly:
   1.729 @@ -843,19 +953,30 @@
   1.730    case (1 c p)
   1.731    show ?case
   1.732    proof
   1.733 -    fix x assume xc: "x \<in> set (coefficients (CN c 0 p))"
   1.734 -    hence "x = c \<or> x \<in> set (coefficients p)" by simp
   1.735 -    moreover
   1.736 -    {assume "x = c" hence "wf_bs bs x" using "1.prems"  unfolding wf_bs_def by simp}
   1.737 +    fix x
   1.738 +    assume xc: "x \<in> set (coefficients (CN c 0 p))"
   1.739 +    then have "x = c \<or> x \<in> set (coefficients p)"
   1.740 +      by simp
   1.741      moreover
   1.742 -    {assume H: "x \<in> set (coefficients p)"
   1.743 -      from "1.prems" have "wf_bs bs p" unfolding wf_bs_def by simp
   1.744 -      with "1.hyps" H have "wf_bs bs x" by blast }
   1.745 -    ultimately  show "wf_bs bs x" by blast
   1.746 +    {
   1.747 +      assume "x = c"
   1.748 +      then have "wf_bs bs x"
   1.749 +        using "1.prems"  unfolding wf_bs_def by simp
   1.750 +    }
   1.751 +    moreover
   1.752 +    {
   1.753 +      assume H: "x \<in> set (coefficients p)"
   1.754 +      from "1.prems" have "wf_bs bs p"
   1.755 +        unfolding wf_bs_def by simp
   1.756 +      with "1.hyps" H have "wf_bs bs x"
   1.757 +        by blast
   1.758 +    }
   1.759 +    ultimately  show "wf_bs bs x"
   1.760 +      by blast
   1.761    qed
   1.762  qed simp_all
   1.763  
   1.764 -lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"
   1.765 +lemma maxindex_coefficients: "\<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"
   1.766    by (induct p rule: coefficients.induct) auto
   1.767  
   1.768  lemma wf_bs_I: "wf_bs bs p \<Longrightarrow> Ipoly (bs @ bs') p = Ipoly bs p"
   1.769 @@ -864,13 +985,17 @@
   1.770  lemma take_maxindex_wf:
   1.771    assumes wf: "wf_bs bs p"
   1.772    shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p"
   1.773 -proof-
   1.774 +proof -
   1.775    let ?ip = "maxindex p"
   1.776    let ?tbs = "take ?ip bs"
   1.777 -  from wf have "length ?tbs = ?ip" unfolding wf_bs_def by simp
   1.778 -  hence wf': "wf_bs ?tbs p" unfolding wf_bs_def by  simp
   1.779 -  have eq: "bs = ?tbs @ (drop ?ip bs)" by simp
   1.780 -  from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis using eq by simp
   1.781 +  from wf have "length ?tbs = ?ip"
   1.782 +    unfolding wf_bs_def by simp
   1.783 +  then have wf': "wf_bs ?tbs p"
   1.784 +    unfolding wf_bs_def by  simp
   1.785 +  have eq: "bs = ?tbs @ (drop ?ip bs)"
   1.786 +    by simp
   1.787 +  from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis
   1.788 +    using eq by simp
   1.789  qed
   1.790  
   1.791  lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1"
   1.792 @@ -939,10 +1064,12 @@
   1.793  lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall> q \<in> set (coefficients p). isnpolyh q n0"
   1.794  proof (induct p arbitrary: n0 rule: coefficients.induct)
   1.795    case (1 c p n0)
   1.796 -  have cp: "isnpolyh (CN c 0 p) n0" by fact
   1.797 -  hence norm: "isnpolyh c 0" "isnpolyh p 0" "p \<noteq> 0\<^sub>p" "n0 = 0"
   1.798 +  have cp: "isnpolyh (CN c 0 p) n0"
   1.799 +    by fact
   1.800 +  then have norm: "isnpolyh c 0" "isnpolyh p 0" "p \<noteq> 0\<^sub>p" "n0 = 0"
   1.801      by (auto simp add: isnpolyh_mono[where n'=0])
   1.802 -  from "1.hyps"[OF norm(2)] norm(1) norm(4)  show ?case by simp
   1.803 +  from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case
   1.804 +    by simp
   1.805  qed auto
   1.806  
   1.807  lemma coefficients_isconst:
   1.808 @@ -960,12 +1087,11 @@
   1.809      from q cn_norm have th: "isnpolyh q n0" by blast
   1.810      from coefficients_isconst[OF np] q have "isconstant q" by blast
   1.811      with isconstant_polybound0[OF th] have "polybound0 q" by blast}
   1.812 -  hence "\<forall>q \<in> ?cf. polybound0 q" ..
   1.813 -  hence "\<forall>q \<in> ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)"
   1.814 +  then have "\<forall>q \<in> ?cf. polybound0 q" ..
   1.815 +  then have "\<forall>q \<in> ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)"
   1.816      using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs]
   1.817      by auto
   1.818 -
   1.819 -  thus ?thesis unfolding polypoly_def polypoly'_def by simp
   1.820 +  then show ?thesis unfolding polypoly_def polypoly'_def by simp
   1.821  qed
   1.822  
   1.823  lemma polypoly_poly:
   1.824 @@ -1207,57 +1333,102 @@
   1.825    using np nq h d
   1.826  proof (induct p q rule: polyadd.induct)
   1.827    case (1 c c')
   1.828 -  thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def])
   1.829 +  then show ?case
   1.830 +    by (simp add: Nsub_def Nsub0[simplified Nsub_def])
   1.831  next
   1.832    case (2 c c' n' p')
   1.833 -  from 2 have "degree (C c) = degree (CN c' n' p')" by simp
   1.834 -  hence nz:"n' > 0" by (cases n') auto
   1.835 -  hence "head (CN c' n' p') = CN c' n' p'" by (cases n') auto
   1.836 -  with 2 show ?case by simp
   1.837 +  from 2 have "degree (C c) = degree (CN c' n' p')"
   1.838 +    by simp
   1.839 +  then have nz: "n' > 0"
   1.840 +    by (cases n') auto
   1.841 +  then have "head (CN c' n' p') = CN c' n' p'"
   1.842 +    by (cases n') auto
   1.843 +  with 2 show ?case
   1.844 +    by simp
   1.845  next
   1.846    case (3 c n p c')
   1.847 -  hence "degree (C c') = degree (CN c n p)" by simp
   1.848 -  hence nz:"n > 0" by (cases n) auto
   1.849 -  hence "head (CN c n p) = CN c n p" by (cases n) auto
   1.850 +  then have "degree (C c') = degree (CN c n p)"
   1.851 +    by simp
   1.852 +  then have nz: "n > 0"
   1.853 +    by (cases n) auto
   1.854 +  then have "head (CN c n p) = CN c n p"
   1.855 +    by (cases n) auto
   1.856    with 3 show ?case by simp
   1.857  next
   1.858    case (4 c n p c' n' p')
   1.859 -  hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1"
   1.860 -    "head (CN c n p) = head (CN c' n' p')" "degree (CN c n p) = degree (CN c' n' p')" by simp+
   1.861 -  hence degc: "degree c = 0" and degc': "degree c' = 0" by simp_all
   1.862 -  hence degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0"
   1.863 +  then have H:
   1.864 +    "isnpolyh (CN c n p) n0"
   1.865 +    "isnpolyh (CN c' n' p') n1"
   1.866 +    "head (CN c n p) = head (CN c' n' p')"
   1.867 +    "degree (CN c n p) = degree (CN c' n' p')"
   1.868 +    by simp_all
   1.869 +  then have degc: "degree c = 0" and degc': "degree c' = 0"
   1.870 +    by simp_all
   1.871 +  then have degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0"
   1.872      using H(1-2) degree_polyneg by auto
   1.873 -  from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')"  by simp+
   1.874 -  from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' have degcmc': "degree (c +\<^sub>p  ~\<^sub>pc') = 0"  by simp
   1.875 -  from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" by auto
   1.876 -  have "n = n' \<or> n < n' \<or> n > n'" by arith
   1.877 +  from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')"
   1.878 +    by simp_all
   1.879 +  from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc'
   1.880 +  have degcmc': "degree (c +\<^sub>p  ~\<^sub>pc') = 0"
   1.881 +    by simp
   1.882 +  from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'"
   1.883 +    by auto
   1.884 +  have "n = n' \<or> n < n' \<or> n > n'"
   1.885 +    by arith
   1.886    moreover
   1.887 -  {assume nn': "n = n'"
   1.888 -    have "n = 0 \<or> n >0" by arith
   1.889 -    moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')}
   1.890 -    moreover {assume nz: "n > 0"
   1.891 -      with nn' H(3) have  cc':"c = c'" and pp': "p = p'" by (cases n, auto)+
   1.892 -      hence ?case
   1.893 -        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.894 -        using nn' 4 by (simp add: Let_def) }
   1.895 -    ultimately have ?case by blast}
   1.896 +  {
   1.897 +    assume nn': "n = n'"
   1.898 +    have "n = 0 \<or> n > 0" by arith
   1.899 +    moreover {
   1.900 +      assume nz: "n = 0"
   1.901 +      then have ?case using 4 nn'
   1.902 +        by (auto simp add: Let_def degcmc')
   1.903 +    }
   1.904 +    moreover {
   1.905 +      assume nz: "n > 0"
   1.906 +      with nn' H(3) have  cc': "c = c'" and pp': "p = p'"
   1.907 +        by (cases n, auto)+
   1.908 +      then have ?case
   1.909 +        using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv]
   1.910 +        using polysub_same_0[OF c'nh, simplified polysub_def]
   1.911 +        using nn' 4 by (simp add: Let_def)
   1.912 +    }
   1.913 +    ultimately have ?case by blast
   1.914 +  }
   1.915    moreover
   1.916 -  {assume nn': "n < n'" hence n'p: "n' > 0" by simp
   1.917 -    hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n') simp_all
   1.918 -    have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')"
   1.919 +  {
   1.920 +    assume nn': "n < n'"
   1.921 +    then have n'p: "n' > 0"
   1.922 +      by simp
   1.923 +    then have headcnp':"head (CN c' n' p') = CN c' n' p'"
   1.924 +      by (cases n') simp_all
   1.925 +    have degcnp': "degree (CN c' n' p') = 0"
   1.926 +      and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')"
   1.927        using 4 nn' by (cases n', simp_all)
   1.928 -    hence "n > 0" by (cases n) simp_all
   1.929 -    hence headcnp: "head (CN c n p) = CN c n p" by (cases n) auto
   1.930 -    from H(3) headcnp headcnp' nn' have ?case by auto}
   1.931 +    then have "n > 0"
   1.932 +      by (cases n) simp_all
   1.933 +    then have headcnp: "head (CN c n p) = CN c n p"
   1.934 +      by (cases n) auto
   1.935 +    from H(3) headcnp headcnp' nn' have ?case
   1.936 +      by auto
   1.937 +  }
   1.938    moreover
   1.939 -  {assume nn': "n > n'"  hence np: "n > 0" by simp
   1.940 -    hence headcnp:"head (CN c n p) = CN c n p"  by (cases n) simp_all
   1.941 -    from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
   1.942 -    from np have degcnp: "degree (CN c n p) = 0" by (cases n) simp_all
   1.943 -    with degcnpeq have "n' > 0" by (cases n') simp_all
   1.944 -    hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n') auto
   1.945 -    from H(3) headcnp headcnp' nn' have ?case by auto}
   1.946 -  ultimately show ?case  by blast
   1.947 +  {
   1.948 +    assume nn': "n > n'"
   1.949 +    then have np: "n > 0" by simp
   1.950 +    then have headcnp:"head (CN c n p) = CN c n p"
   1.951 +      by (cases n) simp_all
   1.952 +    from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)"
   1.953 +      by simp
   1.954 +    from np have degcnp: "degree (CN c n p) = 0"
   1.955 +      by (cases n) simp_all
   1.956 +    with degcnpeq have "n' > 0"
   1.957 +      by (cases n') simp_all
   1.958 +    then have headcnp': "head (CN c' n' p') = CN c' n' p'"
   1.959 +      by (cases n') auto
   1.960 +    from H(3) headcnp headcnp' nn' have ?case by auto
   1.961 +  }
   1.962 +  ultimately show ?case by blast
   1.963  qed auto
   1.964  
   1.965  lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p"
   1.966 @@ -1266,17 +1437,18 @@
   1.967  lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
   1.968  proof (induct k arbitrary: n0 p)
   1.969    case 0
   1.970 -  thus ?case by auto
   1.971 +  then show ?case by auto
   1.972  next
   1.973    case (Suc k n0 p)
   1.974 -  hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
   1.975 +  then have "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
   1.976    with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
   1.977      and "head (shift1 p) = head p" by (simp_all add: shift1_head)
   1.978 -  thus ?case by (simp add: funpow_swap1)
   1.979 +  then show ?case by (simp add: funpow_swap1)
   1.980  qed
   1.981  
   1.982  lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
   1.983    by (simp add: shift1_def)
   1.984 +
   1.985  lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p "
   1.986    by (induct k arbitrary: p) (auto simp add: shift1_degree)
   1.987  
   1.988 @@ -1319,12 +1491,16 @@
   1.989    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.990  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   1.991    case (2 c c' n' p' n0 n1)
   1.992 -  hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum c"  by (simp_all add: head_isnpolyh)
   1.993 -  thus ?case using 2 by (cases n') auto
   1.994 +  then have "isnpolyh (head (CN c' n' p')) n1" "isnormNum c"
   1.995 +    by (simp_all add: head_isnpolyh)
   1.996 +  then show ?case
   1.997 +    using 2 by (cases n') auto
   1.998  next
   1.999    case (3 c n p c' n0 n1)
  1.1000 -  hence "isnpolyh (head (CN c n p)) n0" "isnormNum c'"  by (simp_all add: head_isnpolyh)
  1.1001 -  thus ?case using 3 by (cases n) auto
  1.1002 +  then have "isnpolyh (head (CN c n p)) n0" "isnormNum c'"
  1.1003 +    by (simp_all add: head_isnpolyh)
  1.1004 +  then show ?case using 3
  1.1005 +    by (cases n) auto
  1.1006  next
  1.1007    case (4 c n p c' n' p' n0 n1)
  1.1008    hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
  1.1009 @@ -1332,24 +1508,30 @@
  1.1010      by simp_all
  1.1011    have "n < n' \<or> n' < n \<or> n = n'" by arith
  1.1012    moreover
  1.1013 -  {assume nn': "n < n'" hence ?case
  1.1014 +  {
  1.1015 +    assume nn': "n < n'"
  1.1016 +    then have ?case
  1.1017        using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)]
  1.1018        apply simp
  1.1019        apply (cases n)
  1.1020        apply simp
  1.1021        apply (cases n')
  1.1022        apply simp_all
  1.1023 -      done }
  1.1024 -  moreover {assume nn': "n'< n"
  1.1025 -    hence ?case
  1.1026 +      done
  1.1027 +  }
  1.1028 +  moreover {
  1.1029 +    assume nn': "n'< n"
  1.1030 +    then have ?case
  1.1031        using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)]
  1.1032        apply simp
  1.1033        apply (cases n')
  1.1034        apply simp
  1.1035        apply (cases n)
  1.1036        apply auto
  1.1037 -      done }
  1.1038 -  moreover {assume nn': "n' = n"
  1.1039 +      done
  1.1040 +  }
  1.1041 +  moreover {
  1.1042 +    assume nn': "n' = n"
  1.1043      from nn' polymul_normh[OF norm(5,4)]
  1.1044      have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)
  1.1045      from nn' polymul_normh[OF norm(5,3)] norm
  1.1046 @@ -1359,12 +1541,15 @@
  1.1047      from polyadd_normh[OF ncnpc' ncnpp0']
  1.1048      have nth: "isnpolyh ((CN c n p *\<^sub>p c') +\<^sub>p (CN 0\<^sub>p n (CN c n p *\<^sub>p p'))) n"
  1.1049        by (simp add: min_def)
  1.1050 -    {assume np: "n > 0"
  1.1051 +    {
  1.1052 +      assume np: "n > 0"
  1.1053        with nn' head_isnpolyh_Suc'[OF np nth]
  1.1054          head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
  1.1055 -      have ?case by simp}
  1.1056 +      have ?case by simp
  1.1057 +    }
  1.1058      moreover
  1.1059 -    { assume nz: "n = 0"
  1.1060 +    {
  1.1061 +      assume nz: "n = 0"
  1.1062        from polymul_degreen[OF norm(5,4), where m="0"]
  1.1063          polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
  1.1064        norm(5,6) degree_npolyhCN[OF norm(6)]
  1.1065 @@ -1372,8 +1557,10 @@
  1.1066      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.1067      from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
  1.1068      have ?case   using norm "4.hyps"(6)[OF norm(5,3)]
  1.1069 -        "4.hyps"(5)[OF norm(5,4)] nn' nz by simp }
  1.1070 -    ultimately have ?case by (cases n) auto}
  1.1071 +        "4.hyps"(5)[OF norm(5,4)] nn' nz by simp
  1.1072 +    }
  1.1073 +    ultimately have ?case by (cases n) auto
  1.1074 +  }
  1.1075    ultimately show ?case by blast
  1.1076  qed simp_all
  1.1077  
  1.1078 @@ -1744,10 +1931,16 @@
  1.1079    assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
  1.1080    from isnonconstant_pnormal_iff[OF inc, of bs] h
  1.1081    have pn: "pnormal ?p" by blast
  1.1082 -  { fix x assume H: "?p = [x]"
  1.1083 -    from H have "length (coefficients p) = 1" unfolding polypoly_def by auto
  1.1084 -    with isnonconstant_coefficients_length[OF inc] have False by arith }
  1.1085 -  thus "nonconstant ?p" using pn unfolding nonconstant_def by blast
  1.1086 +  {
  1.1087 +    fix x
  1.1088 +    assume H: "?p = [x]"
  1.1089 +    from H have "length (coefficients p) = 1"
  1.1090 +      unfolding polypoly_def by auto
  1.1091 +    with isnonconstant_coefficients_length[OF inc]
  1.1092 +      have False by arith
  1.1093 +  }
  1.1094 +  then show "nonconstant ?p"
  1.1095 +    using pn unfolding nonconstant_def by blast
  1.1096  qed
  1.1097  
  1.1098  lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
  1.1099 @@ -1800,10 +1993,10 @@
  1.1100    shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
  1.1101  proof (induct t)
  1.1102    case (Bound k)
  1.1103 -  thus ?case using nbs mbs by simp
  1.1104 +  then show ?case using nbs mbs by simp
  1.1105  next
  1.1106    case (CN c k p)
  1.1107 -  thus ?case using nbs mbs by simp
  1.1108 +  then show ?case using nbs mbs by simp
  1.1109  qed simp_all
  1.1110  
  1.1111  lemma swap_swap_id [simp]: "swap n m (swap m n t) = t"