author wenzelm Mon Mar 10 23:03:15 2014 +0100 (2014-03-10) changeset 56043 0b25c3d34b77 parent 56042 d3c35a300433 child 56044 f78b4c3e8e84
tuned proofs;
```     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.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.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.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