src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 56043 0b25c3d34b77
parent 56009 dda076a32aea
child 56066 cce36efe32eb
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Mar 10 22:40:48 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Mar 10 23:03:15 2014 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  subsection{* Datatype of polynomial expressions *}
     1.6  
     1.7 -datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly
     1.8 +datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly
     1.9    | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
    1.10  
    1.11  abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
    1.12 @@ -142,7 +142,7 @@
    1.13  
    1.14  fun polymul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
    1.15  where
    1.16 -  "polymul (C c) (C c') = C (c*\<^sub>Nc')"
    1.17 +  "polymul (C c) (C c') = C (c *\<^sub>N c')"
    1.18  | "polymul (C c) (CN c' n' p') =
    1.19      (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))"
    1.20  | "polymul (CN c n p) (C c') =
    1.21 @@ -556,7 +556,7 @@
    1.22      let ?d1 = "degreen ?cnp m"
    1.23      let ?d2 = "degreen ?cnp' m"
    1.24      let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0  else ?d1 + ?d2)"
    1.25 -    have "n'<n \<or> n < n' \<or> n' = n" by auto
    1.26 +    have "n' < n \<or> n < n' \<or> n' = n" by auto
    1.27      moreover
    1.28      {
    1.29        assume "n' < n \<or> n < n'"
    1.30 @@ -570,10 +570,16 @@
    1.31        from "4.hyps"(16,18)[of n n' n]
    1.32          "4.hyps"(13,14)[of n "Suc n'" n]
    1.33          np np' nn'
    1.34 -      have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
    1.35 -        "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
    1.36 -        "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
    1.37 -        "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
    1.38 +      have norm:
    1.39 +        "isnpolyh ?cnp n"
    1.40 +        "isnpolyh c' (Suc n)"
    1.41 +        "isnpolyh (?cnp *\<^sub>p c') n"
    1.42 +        "isnpolyh p' n"
    1.43 +        "isnpolyh (?cnp *\<^sub>p p') n"
    1.44 +        "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
    1.45 +        "?cnp *\<^sub>p c' = 0\<^sub>p \<longleftrightarrow> c' = 0\<^sub>p"
    1.46 +        "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"
    1.47 +        by (auto simp add: min_def)
    1.48        {
    1.49          assume mn: "m = n"
    1.50          from "4.hyps"(17,18)[OF norm(1,4), of n]
    1.51 @@ -627,7 +633,8 @@
    1.52      case (2 n0 n1)
    1.53      then have np: "isnpolyh ?cnp n0"
    1.54        and np': "isnpolyh ?cnp' n1"
    1.55 -      and m: "m \<le> min n0 n1" by simp_all
    1.56 +      and m: "m \<le> min n0 n1"
    1.57 +      by simp_all
    1.58      then have mn: "m \<le> n" by simp
    1.59      let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
    1.60      {
    1.61 @@ -700,10 +707,17 @@
    1.62    assume pz: "p \<noteq> 0\<^sub>p"
    1.63    {
    1.64      assume hz: "INum ?h = (0::'a)"
    1.65 -    from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all
    1.66 -    from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp
    1.67 -    with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast}
    1.68 -  then show "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast
    1.69 +    from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N"
    1.70 +      by simp_all
    1.71 +    from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N"
    1.72 +      by simp
    1.73 +    with headconst_zero[OF np] have "p = 0\<^sub>p"
    1.74 +      by blast
    1.75 +    with pz have False
    1.76 +      by blast
    1.77 +  }
    1.78 +  then show "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0"
    1.79 +    by blast
    1.80  qed
    1.81  
    1.82  
    1.83 @@ -755,33 +769,42 @@
    1.84    "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n"
    1.85  proof (induct n rule: polypow.induct)
    1.86    case 1
    1.87 -  then show ?case by simp
    1.88 +  then show ?case
    1.89 +    by simp
    1.90  next
    1.91    case (2 n)
    1.92    let ?q = "polypow ((Suc n) div 2) p"
    1.93    let ?d = "polymul ?q ?q"
    1.94 -  have "odd (Suc n) \<or> even (Suc n)" by simp
    1.95 +  have "odd (Suc n) \<or> even (Suc n)"
    1.96 +    by simp
    1.97    moreover
    1.98 -  { assume odd: "odd (Suc n)"
    1.99 +  {
   1.100 +    assume odd: "odd (Suc n)"
   1.101      have th: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1"
   1.102        by arith
   1.103 -    from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" by (simp add: Let_def)
   1.104 -    also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)"
   1.105 +    from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)"
   1.106 +      by (simp add: Let_def)
   1.107 +    also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2) * (Ipoly bs p)^(Suc n div 2)"
   1.108        using "2.hyps" by simp
   1.109      also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
   1.110        by (simp only: power_add power_one_right) simp
   1.111      also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
   1.112        by (simp only: th)
   1.113      finally have ?case
   1.114 -    using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp  }
   1.115 +    using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp
   1.116 +  }
   1.117    moreover
   1.118 -  { assume even: "even (Suc n)"
   1.119 +  {
   1.120 +    assume even: "even (Suc n)"
   1.121      have th: "(Suc (Suc 0)) * (Suc n div Suc (Suc 0)) = Suc n div 2 + Suc n div 2"
   1.122        by arith
   1.123 -    from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def)
   1.124 +    from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d"
   1.125 +      by (simp add: Let_def)
   1.126      also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"
   1.127 -      using "2.hyps" apply (simp only: power_add) by simp
   1.128 -    finally have ?case using even_nat_div_two_times_two[OF even] by (simp only: th)}
   1.129 +      using "2.hyps" by (simp only: power_add) simp
   1.130 +    finally have ?case using even_nat_div_two_times_two[OF even]
   1.131 +      by (simp only: th)
   1.132 +  }
   1.133    ultimately show ?case by blast
   1.134  qed
   1.135  
   1.136 @@ -789,14 +812,21 @@
   1.137    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.138    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
   1.139  proof (induct k arbitrary: n rule: polypow.induct)
   1.140 +  case 1
   1.141 +  then show ?case by auto
   1.142 +next
   1.143    case (2 k n)
   1.144    let ?q = "polypow (Suc k div 2) p"
   1.145    let ?d = "polymul ?q ?q"
   1.146 -  from 2 have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
   1.147 -  from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp
   1.148 -  from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n" by simp
   1.149 -  from dn on show ?case by (simp add: Let_def)
   1.150 -qed auto
   1.151 +  from 2 have th1: "isnpolyh ?q n" and th2: "isnpolyh p n"
   1.152 +    by blast+
   1.153 +  from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n"
   1.154 +    by simp
   1.155 +  from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n"
   1.156 +    by simp
   1.157 +  from dn on show ?case
   1.158 +    by (simp add: Let_def)
   1.159 +qed
   1.160  
   1.161  lemma polypow_norm:
   1.162    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.163 @@ -830,12 +860,12 @@
   1.164  
   1.165  lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p"
   1.166    by (simp add: shift1_def)
   1.167 -lemma funpow_shift1_isnpoly:
   1.168 -  "\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)"
   1.169 +
   1.170 +lemma funpow_shift1_isnpoly: "isnpoly p \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> isnpoly (funpow n shift1 p)"
   1.171    by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
   1.172  
   1.173  lemma funpow_isnpolyh:
   1.174 -  assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
   1.175 +  assumes f: "\<And>p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n"
   1.176      and np: "isnpolyh p n"
   1.177    shows "isnpolyh (funpow k f p) n"
   1.178    using f np by (induct k arbitrary: p) auto
   1.179 @@ -845,7 +875,7 @@
   1.180      Ipoly bs (Mul (Pw (Bound 0) n) p)"
   1.181    by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
   1.182  
   1.183 -lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
   1.184 +lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
   1.185    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   1.186  
   1.187  lemma funpow_shift1_1:
   1.188 @@ -900,7 +930,7 @@
   1.189  lemma decrpoly_normh: "isnpolyh p n0 \<Longrightarrow> polybound0 p \<Longrightarrow> isnpolyh (decrpoly p) (n0 - 1)"
   1.190    apply (induct p arbitrary: n0)
   1.191    apply auto
   1.192 -  apply (atomize)
   1.193 +  apply atomize
   1.194    apply (erule_tac x = "Suc nat" in allE)
   1.195    apply auto
   1.196    done
   1.197 @@ -924,7 +954,7 @@
   1.198  
   1.199  lemma decrpoly:
   1.200    assumes nb: "polybound0 t"
   1.201 -  shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)"
   1.202 +  shows "Ipoly (x # bs) t = Ipoly bs (decrpoly t)"
   1.203    using nb by (induct t rule: decrpoly.induct) simp_all
   1.204  
   1.205  lemma polysubst0_polybound0:
   1.206 @@ -935,7 +965,8 @@
   1.207  lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
   1.208    by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0)
   1.209  
   1.210 -primrec maxindex :: "poly \<Rightarrow> nat" where
   1.211 +primrec maxindex :: "poly \<Rightarrow> nat"
   1.212 +where
   1.213    "maxindex (Bound n) = n + 1"
   1.214  | "maxindex (CN c n p) = max  (n + 1) (max (maxindex c) (maxindex p))"
   1.215  | "maxindex (Add p q) = max (maxindex p) (maxindex q)"
   1.216 @@ -948,7 +979,7 @@
   1.217  definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool"
   1.218    where "wf_bs bs p \<longleftrightarrow> length bs \<ge> maxindex p"
   1.219  
   1.220 -lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall> c \<in> set (coefficients p). wf_bs bs c"
   1.221 +lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall>c \<in> set (coefficients p). wf_bs bs c"
   1.222  proof (induct p rule: coefficients.induct)
   1.223    case (1 c p)
   1.224    show ?case
   1.225 @@ -961,7 +992,7 @@
   1.226      {
   1.227        assume "x = c"
   1.228        then have "wf_bs bs x"
   1.229 -        using "1.prems"  unfolding wf_bs_def by simp
   1.230 +        using "1.prems" unfolding wf_bs_def by simp
   1.231      }
   1.232      moreover
   1.233      {
   1.234 @@ -976,7 +1007,7 @@
   1.235    qed
   1.236  qed simp_all
   1.237  
   1.238 -lemma maxindex_coefficients: "\<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"
   1.239 +lemma maxindex_coefficients: "\<forall>c \<in> set (coefficients p). maxindex c \<le> maxindex p"
   1.240    by (induct p rule: coefficients.induct) auto
   1.241  
   1.242  lemma wf_bs_I: "wf_bs bs p \<Longrightarrow> Ipoly (bs @ bs') p = Ipoly bs p"
   1.243 @@ -992,7 +1023,7 @@
   1.244      unfolding wf_bs_def by simp
   1.245    then have wf': "wf_bs ?tbs p"
   1.246      unfolding wf_bs_def by  simp
   1.247 -  have eq: "bs = ?tbs @ (drop ?ip bs)"
   1.248 +  have eq: "bs = ?tbs @ drop ?ip bs"
   1.249      by simp
   1.250    from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis
   1.251      using eq by simp
   1.252 @@ -1007,26 +1038,24 @@
   1.253  lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p"
   1.254    unfolding wf_bs_def by simp
   1.255  
   1.256 -
   1.257 -
   1.258  lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"
   1.259    by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def)
   1.260 +
   1.261  lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"
   1.262    by (induct p rule: coefficients.induct) simp_all
   1.263  
   1.264 -
   1.265  lemma coefficients_head: "last (coefficients p) = head p"
   1.266    by (induct p rule: coefficients.induct) auto
   1.267  
   1.268  lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p"
   1.269    unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto
   1.270  
   1.271 -lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists> ys. length (xs @ ys) = n"
   1.272 +lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists>ys. length (xs @ ys) = n"
   1.273    apply (rule exI[where x="replicate (n - length xs) z"])
   1.274    apply simp
   1.275    done
   1.276  
   1.277 -lemma isnpolyh_Suc_const:"isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
   1.278 +lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
   1.279    apply (cases p)
   1.280    apply auto
   1.281    apply (case_tac "nat")
   1.282 @@ -1052,16 +1081,17 @@
   1.283    unfolding wf_bs_def by (induct p rule: polyneg.induct) auto
   1.284  
   1.285  lemma wf_bs_polysub: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p -\<^sub>p q)"
   1.286 -  unfolding polysub_def split_def fst_conv snd_conv using wf_bs_polyadd wf_bs_polyneg by blast
   1.287 +  unfolding polysub_def split_def fst_conv snd_conv
   1.288 +  using wf_bs_polyadd wf_bs_polyneg by blast
   1.289  
   1.290  
   1.291 -subsection{* Canonicity of polynomial representation, see lemma isnpolyh_unique*}
   1.292 +subsection {* Canonicity of polynomial representation, see lemma isnpolyh_unique *}
   1.293  
   1.294  definition "polypoly bs p = map (Ipoly bs) (coefficients p)"
   1.295 -definition "polypoly' bs p = map ((Ipoly bs o decrpoly)) (coefficients p)"
   1.296 -definition "poly_nate bs p = map ((Ipoly bs o decrpoly)) (coefficients (polynate p))"
   1.297 +definition "polypoly' bs p = map (Ipoly bs \<circ> decrpoly) (coefficients p)"
   1.298 +definition "poly_nate bs p = map (Ipoly bs \<circ> decrpoly) (coefficients (polynate p))"
   1.299  
   1.300 -lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall> q \<in> set (coefficients p). isnpolyh q n0"
   1.301 +lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall>q \<in> set (coefficients p). isnpolyh q n0"
   1.302  proof (induct p arbitrary: n0 rule: coefficients.induct)
   1.303    case (1 c p n0)
   1.304    have cp: "isnpolyh (CN c 0 p) n0"
   1.305 @@ -1072,44 +1102,51 @@
   1.306      by simp
   1.307  qed auto
   1.308  
   1.309 -lemma coefficients_isconst:
   1.310 -  "isnpolyh p n \<Longrightarrow> \<forall>q\<in>set (coefficients p). isconstant q"
   1.311 -  by (induct p arbitrary: n rule: coefficients.induct)
   1.312 -    (auto simp add: isnpolyh_Suc_const)
   1.313 +lemma coefficients_isconst: "isnpolyh p n \<Longrightarrow> \<forall>q \<in> set (coefficients p). isconstant q"
   1.314 +  by (induct p arbitrary: n rule: coefficients.induct) (auto simp add: isnpolyh_Suc_const)
   1.315  
   1.316  lemma polypoly_polypoly':
   1.317    assumes np: "isnpolyh p n0"
   1.318 -  shows "polypoly (x#bs) p = polypoly' bs p"
   1.319 -proof-
   1.320 +  shows "polypoly (x # bs) p = polypoly' bs p"
   1.321 +proof -
   1.322    let ?cf = "set (coefficients p)"
   1.323    from coefficients_normh[OF np] have cn_norm: "\<forall> q\<in> ?cf. isnpolyh q n0" .
   1.324 -  {fix q assume q: "q \<in> ?cf"
   1.325 -    from q cn_norm have th: "isnpolyh q n0" by blast
   1.326 -    from coefficients_isconst[OF np] q have "isconstant q" by blast
   1.327 -    with isconstant_polybound0[OF th] have "polybound0 q" by blast}
   1.328 +  {
   1.329 +    fix q
   1.330 +    assume q: "q \<in> ?cf"
   1.331 +    from q cn_norm have th: "isnpolyh q n0"
   1.332 +      by blast
   1.333 +    from coefficients_isconst[OF np] q have "isconstant q"
   1.334 +      by blast
   1.335 +    with isconstant_polybound0[OF th] have "polybound0 q"
   1.336 +      by blast
   1.337 +  }
   1.338    then have "\<forall>q \<in> ?cf. polybound0 q" ..
   1.339 -  then have "\<forall>q \<in> ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)"
   1.340 +  then have "\<forall>q \<in> ?cf. Ipoly (x # bs) q = Ipoly bs (decrpoly q)"
   1.341      using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs]
   1.342      by auto
   1.343 -  then show ?thesis unfolding polypoly_def polypoly'_def by simp
   1.344 +  then show ?thesis
   1.345 +    unfolding polypoly_def polypoly'_def by simp
   1.346  qed
   1.347  
   1.348  lemma polypoly_poly:
   1.349 -  assumes np: "isnpolyh p n0"
   1.350 -  shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x"
   1.351 -  using np
   1.352 +  assumes "isnpolyh p n0"
   1.353 +  shows "Ipoly (x # bs) p = poly (polypoly (x # bs) p) x"
   1.354 +  using assms
   1.355    by (induct p arbitrary: n0 bs rule: coefficients.induct) (auto simp add: polypoly_def)
   1.356  
   1.357  lemma polypoly'_poly:
   1.358 -  assumes np: "isnpolyh p n0"
   1.359 +  assumes "isnpolyh p n0"
   1.360    shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x"
   1.361 -  using polypoly_poly[OF np, simplified polypoly_polypoly'[OF np]] .
   1.362 +  using polypoly_poly[OF assms, simplified polypoly_polypoly'[OF assms]] .
   1.363  
   1.364  
   1.365  lemma polypoly_poly_polybound0:
   1.366 -  assumes np: "isnpolyh p n0" and nb: "polybound0 p"
   1.367 +  assumes "isnpolyh p n0"
   1.368 +    and "polybound0 p"
   1.369    shows "polypoly bs p = [Ipoly bs p]"
   1.370 -  using np nb unfolding polypoly_def
   1.371 +  using assms
   1.372 +  unfolding polypoly_def
   1.373    apply (cases p)
   1.374    apply auto
   1.375    apply (case_tac nat)
   1.376 @@ -1119,13 +1156,13 @@
   1.377  lemma head_isnpolyh: "isnpolyh p n0 \<Longrightarrow> isnpolyh (head p) n0"
   1.378    by (induct p rule: head.induct) auto
   1.379  
   1.380 -lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)"
   1.381 +lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> headn p m = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p"
   1.382    by (cases p) auto
   1.383  
   1.384  lemma head_eq_headn0: "head p = headn p 0"
   1.385    by (induct p rule: head.induct) simp_all
   1.386  
   1.387 -lemma head_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (head p = 0\<^sub>p) = (p = 0\<^sub>p)"
   1.388 +lemma head_nz[simp]: "isnpolyh p n0 \<Longrightarrow> head p = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p"
   1.389    by (simp add: head_eq_headn0)
   1.390  
   1.391  lemma isnpolyh_zero_iff:
   1.392 @@ -1269,7 +1306,8 @@
   1.393      and np: "isnpolyh p n0"
   1.394      and nq: "isnpolyh q n1"
   1.395    shows "p *\<^sub>p q = q *\<^sub>p p"
   1.396 -  using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a::{field_char_0,field_inverse_zero, power}"]
   1.397 +  using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np],
   1.398 +    where ?'a = "'a::{field_char_0,field_inverse_zero, power}"]
   1.399    by simp
   1.400  
   1.401  declare polyneg_polyneg [simp]
   1.402 @@ -1278,7 +1316,9 @@
   1.403    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.404      and np: "isnpolyh p n0"
   1.405    shows "polynate p = p"
   1.406 -  using isnpolyh_unique[where ?'a= "'a::{field_char_0,field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0,field_inverse_zero}"]
   1.407 +  using isnpolyh_unique[where ?'a= "'a::{field_char_0,field_inverse_zero}",
   1.408 +      OF polynate_norm[of p, unfolded isnpoly_def] np]
   1.409 +    polynate[where ?'a = "'a::{field_char_0,field_inverse_zero}"]
   1.410    by simp
   1.411  
   1.412  lemma polynate_idempotent[simp]:
   1.413 @@ -1301,16 +1341,18 @@
   1.414    by (induct p rule: degree.induct) simp_all
   1.415  
   1.416  lemma degree_polyneg:
   1.417 -  assumes n: "isnpolyh p n"
   1.418 +  assumes "isnpolyh p n"
   1.419    shows "degree (polyneg p) = degree p"
   1.420 -  apply (induct p arbitrary: n rule: polyneg.induct)
   1.421 -  using n apply simp_all
   1.422 +  apply (induct p rule: polyneg.induct)
   1.423 +  using assms
   1.424 +  apply simp_all
   1.425    apply (case_tac na)
   1.426    apply auto
   1.427    done
   1.428  
   1.429  lemma degree_polyadd:
   1.430 -  assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
   1.431 +  assumes np: "isnpolyh p n0"
   1.432 +    and nq: "isnpolyh q n1"
   1.433    shows "degree (p +\<^sub>p q) \<le> max (degree p) (degree q)"
   1.434    using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp
   1.435  
   1.436 @@ -1320,13 +1362,17 @@
   1.437      and nq: "isnpolyh q n1"
   1.438    shows "degree (p -\<^sub>p q) \<le> max (degree p) (degree q)"
   1.439  proof-
   1.440 -  from nq have nq': "isnpolyh (~\<^sub>p q) n1" using polyneg_normh by simp
   1.441 -  from degree_polyadd[OF np nq'] show ?thesis by (simp add: polysub_def degree_polyneg[OF nq])
   1.442 +  from nq have nq': "isnpolyh (~\<^sub>p q) n1"
   1.443 +    using polyneg_normh by simp
   1.444 +  from degree_polyadd[OF np nq'] show ?thesis
   1.445 +    by (simp add: polysub_def degree_polyneg[OF nq])
   1.446  qed
   1.447  
   1.448  lemma degree_polysub_samehead:
   1.449    assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.450 -    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q"
   1.451 +    and np: "isnpolyh p n0"
   1.452 +    and nq: "isnpolyh q n1"
   1.453 +    and h: "head p = head q"
   1.454      and d: "degree p = degree q"
   1.455    shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
   1.456    unfolding polysub_def split_def fst_conv snd_conv