src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
```     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.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.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.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.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.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.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.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.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.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.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.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.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.961 +  }
1.962 +  ultimately show ?case by blast
1.963  qed auto
1.964
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.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.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.993 -  thus ?case using 2 by (cases n') auto
1.994 +  then have "isnpolyh (head (CN c' n' p')) n1" "isnormNum c"
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.1001 -  thus ?case using 3 by (cases n) auto
1.1002 +  then have "isnpolyh (head (CN c n p)) n0" "isnormNum c'"
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.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.1050 -    {assume np: "n > 0"
1.1051 +    {
1.1052 +      assume np: "n > 0"
1.1053        with nn' head_isnpolyh_Suc'[OF np nth]
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.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"
```