src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 59867 58043346ca64
parent 58889 5b7a9633cfa8
child 60533 1e7ccd864b62
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Mar 31 16:49:41 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Mar 31 21:54:32 2015 +0200
     1.3 @@ -235,7 +235,7 @@
     1.4  
     1.5  subsection{* Semantics of the polynomial representation *}
     1.6  
     1.7 -primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field_inverse_zero,power}"
     1.8 +primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
     1.9  where
    1.10    "Ipoly bs (C c) = INum c"
    1.11  | "Ipoly bs (Bound n) = bs!n"
    1.12 @@ -246,7 +246,7 @@
    1.13  | "Ipoly bs (Pw t n) = Ipoly bs t ^ n"
    1.14  | "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p"
    1.15  
    1.16 -abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field_inverse_zero,power}"
    1.17 +abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}"
    1.18      ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    1.19    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
    1.20  
    1.21 @@ -481,7 +481,7 @@
    1.22  qed simp_all
    1.23  
    1.24  lemma polymul_properties:
    1.25 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    1.26 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.27      and np: "isnpolyh p n0"
    1.28      and nq: "isnpolyh q n1"
    1.29      and m: "m \<le> min n0 n1"
    1.30 @@ -670,23 +670,23 @@
    1.31    by (induct p q rule: polymul.induct) (auto simp add: field_simps)
    1.32  
    1.33  lemma polymul_normh:
    1.34 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    1.35 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.36    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
    1.37    using polymul_properties(1) by blast
    1.38  
    1.39  lemma polymul_eq0_iff:
    1.40 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    1.41 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.42    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.43    using polymul_properties(2) by blast
    1.44  
    1.45  lemma polymul_degreen:
    1.46 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    1.47 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.48    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow>
    1.49      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.50    by (fact polymul_properties(3))
    1.51  
    1.52  lemma polymul_norm:
    1.53 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    1.54 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.55    shows "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polymul p q)"
    1.56    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
    1.57  
    1.58 @@ -699,7 +699,7 @@
    1.59  lemma monic_eqI:
    1.60    assumes np: "isnpolyh p n0"
    1.61    shows "INum (headconst p) * Ipoly bs (fst (monic p)) =
    1.62 -    (Ipoly bs p ::'a::{field_char_0,field_inverse_zero, power})"
    1.63 +    (Ipoly bs p ::'a::{field_char_0,field, power})"
    1.64    unfolding monic_def Let_def
    1.65  proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
    1.66    let ?h = "headconst p"
    1.67 @@ -750,13 +750,13 @@
    1.68    using polyadd_norm polyneg_norm by (simp add: polysub_def)
    1.69  
    1.70  lemma polysub_same_0[simp]:
    1.71 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    1.72 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.73    shows "isnpolyh p n0 \<Longrightarrow> polysub p p = 0\<^sub>p"
    1.74    unfolding polysub_def split_def fst_conv snd_conv
    1.75    by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def])
    1.76  
    1.77  lemma polysub_0:
    1.78 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    1.79 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.80    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p -\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = q"
    1.81    unfolding polysub_def split_def fst_conv snd_conv
    1.82    by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
    1.83 @@ -765,7 +765,7 @@
    1.84  text{* polypow is a power function and preserves normal forms *}
    1.85  
    1.86  lemma polypow[simp]:
    1.87 -  "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n"
    1.88 +  "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
    1.89  proof (induct n rule: polypow.induct)
    1.90    case 1
    1.91    then show ?case
    1.92 @@ -806,7 +806,7 @@
    1.93  qed
    1.94  
    1.95  lemma polypow_normh:
    1.96 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
    1.97 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.98    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
    1.99  proof (induct k arbitrary: n rule: polypow.induct)
   1.100    case 1
   1.101 @@ -826,18 +826,18 @@
   1.102  qed
   1.103  
   1.104  lemma polypow_norm:
   1.105 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.106 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.107    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
   1.108    by (simp add: polypow_normh isnpoly_def)
   1.109  
   1.110  text{* Finally the whole normalization *}
   1.111  
   1.112  lemma polynate [simp]:
   1.113 -  "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field_inverse_zero})"
   1.114 +  "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
   1.115    by (induct p rule:polynate.induct) auto
   1.116  
   1.117  lemma polynate_norm[simp]:
   1.118 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.119 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.120    shows "isnpoly (polynate p)"
   1.121    by (induct p rule: polynate.induct)
   1.122       (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
   1.123 @@ -868,7 +868,7 @@
   1.124    using assms by (induct k arbitrary: p) auto
   1.125  
   1.126  lemma funpow_shift1:
   1.127 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
   1.128 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
   1.129      Ipoly bs (Mul (Pw (Bound 0) n) p)"
   1.130    by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
   1.131  
   1.132 @@ -876,7 +876,7 @@
   1.133    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   1.134  
   1.135  lemma funpow_shift1_1:
   1.136 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
   1.137 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
   1.138      Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
   1.139    by (simp add: funpow_shift1)
   1.140  
   1.141 @@ -886,7 +886,7 @@
   1.142  lemma behead:
   1.143    assumes "isnpolyh p n"
   1.144    shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
   1.145 -    (Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})"
   1.146 +    (Ipoly bs p :: 'a :: {field_char_0,field})"
   1.147    using assms
   1.148  proof (induct p arbitrary: n rule: behead.induct)
   1.149    case (1 c p n)
   1.150 @@ -1160,7 +1160,7 @@
   1.151  
   1.152  lemma isnpolyh_zero_iff:
   1.153    assumes nq: "isnpolyh p n0"
   1.154 -    and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field_inverse_zero, power})"
   1.155 +    and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field, power})"
   1.156    shows "p = 0\<^sub>p"
   1.157    using nq eq
   1.158  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
   1.159 @@ -1242,7 +1242,7 @@
   1.160  lemma isnpolyh_unique:
   1.161    assumes np: "isnpolyh p n0"
   1.162      and nq: "isnpolyh q n1"
   1.163 -  shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field_inverse_zero,power})) \<longleftrightarrow> p = q"
   1.164 +  shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field,power})) \<longleftrightarrow> p = q"
   1.165  proof auto
   1.166    assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a) = \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
   1.167    then have "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)"
   1.168 @@ -1257,7 +1257,7 @@
   1.169  text{* consequences of unicity on the algorithms for polynomial normalization *}
   1.170  
   1.171  lemma polyadd_commute:
   1.172 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.173 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.174      and np: "isnpolyh p n0"
   1.175      and nq: "isnpolyh q n1"
   1.176    shows "p +\<^sub>p q = q +\<^sub>p p"
   1.177 @@ -1271,7 +1271,7 @@
   1.178    by simp
   1.179  
   1.180  lemma polyadd_0[simp]:
   1.181 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.182 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.183      and np: "isnpolyh p n0"
   1.184    shows "p +\<^sub>p 0\<^sub>p = p"
   1.185      and "0\<^sub>p +\<^sub>p p = p"
   1.186 @@ -1279,7 +1279,7 @@
   1.187      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
   1.188  
   1.189  lemma polymul_1[simp]:
   1.190 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.191 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.192      and np: "isnpolyh p n0"
   1.193    shows "p *\<^sub>p (1)\<^sub>p = p"
   1.194      and "(1)\<^sub>p *\<^sub>p p = p"
   1.195 @@ -1287,7 +1287,7 @@
   1.196      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
   1.197  
   1.198  lemma polymul_0[simp]:
   1.199 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.200 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.201      and np: "isnpolyh p n0"
   1.202    shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p"
   1.203      and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
   1.204 @@ -1295,27 +1295,27 @@
   1.205      isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
   1.206  
   1.207  lemma polymul_commute:
   1.208 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.209 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.210      and np: "isnpolyh p n0"
   1.211      and nq: "isnpolyh q n1"
   1.212    shows "p *\<^sub>p q = q *\<^sub>p p"
   1.213    using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np],
   1.214 -    where ?'a = "'a::{field_char_0,field_inverse_zero, power}"]
   1.215 +    where ?'a = "'a::{field_char_0,field, power}"]
   1.216    by simp
   1.217  
   1.218  declare polyneg_polyneg [simp]
   1.219  
   1.220  lemma isnpolyh_polynate_id [simp]:
   1.221 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.222 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.223      and np: "isnpolyh p n0"
   1.224    shows "polynate p = p"
   1.225 -  using isnpolyh_unique[where ?'a= "'a::{field_char_0,field_inverse_zero}",
   1.226 +  using isnpolyh_unique[where ?'a= "'a::{field_char_0,field}",
   1.227        OF polynate_norm[of p, unfolded isnpoly_def] np]
   1.228 -    polynate[where ?'a = "'a::{field_char_0,field_inverse_zero}"]
   1.229 +    polynate[where ?'a = "'a::{field_char_0,field}"]
   1.230    by simp
   1.231  
   1.232  lemma polynate_idempotent[simp]:
   1.233 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.234 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.235    shows "polynate (polynate p) = polynate p"
   1.236    using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
   1.237  
   1.238 @@ -1323,7 +1323,7 @@
   1.239    unfolding poly_nate_def polypoly'_def ..
   1.240  
   1.241  lemma poly_nate_poly:
   1.242 -  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   1.243 +  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   1.244    using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
   1.245    unfolding poly_nate_polypoly' by auto
   1.246  
   1.247 @@ -1362,7 +1362,7 @@
   1.248  qed
   1.249  
   1.250  lemma degree_polysub_samehead:
   1.251 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.252 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.253      and np: "isnpolyh p n0"
   1.254      and nq: "isnpolyh q n1"
   1.255      and h: "head p = head q"
   1.256 @@ -1531,7 +1531,7 @@
   1.257    done
   1.258  
   1.259  lemma polymul_head_polyeq:
   1.260 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.261 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.262    shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> q \<noteq> 0\<^sub>p \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
   1.263  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   1.264    case (2 c c' n' p' n0 n1)
   1.265 @@ -1634,7 +1634,7 @@
   1.266    by (induct p arbitrary: n0 rule: polyneg.induct) auto
   1.267  
   1.268  lemma degree_polymul:
   1.269 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.270 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.271      and np: "isnpolyh p n0"
   1.272      and nq: "isnpolyh q n1"
   1.273    shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
   1.274 @@ -1650,7 +1650,7 @@
   1.275  subsection {* Correctness of polynomial pseudo division *}
   1.276  
   1.277  lemma polydivide_aux_properties:
   1.278 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.279 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.280      and np: "isnpolyh p n0"
   1.281      and ns: "isnpolyh s n1"
   1.282      and ap: "head p = a"
   1.283 @@ -1745,24 +1745,24 @@
   1.284                polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
   1.285              have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0"
   1.286                by simp
   1.287 -            from asp have "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
   1.288 +            from asp have "\<forall>bs :: 'a::{field_char_0,field} list.
   1.289                Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)"
   1.290                by simp
   1.291 -            then have "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
   1.292 +            then have "\<forall>bs :: 'a::{field_char_0,field} list.
   1.293                Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
   1.294                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
   1.295                by (simp add: field_simps)
   1.296 -            then have "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
   1.297 +            then have "\<forall>bs :: 'a::{field_char_0,field} list.
   1.298                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.299                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) +
   1.300                Ipoly bs p * Ipoly bs q + Ipoly bs r"
   1.301                by (auto simp only: funpow_shift1_1)
   1.302 -            then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list.
   1.303 +            then have "\<forall>bs:: 'a::{field_char_0,field} list.
   1.304                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.305                Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) +
   1.306                Ipoly bs q) + Ipoly bs r"
   1.307                by (simp add: field_simps)
   1.308 -            then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list.
   1.309 +            then have "\<forall>bs:: 'a::{field_char_0,field} list.
   1.310                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.311                Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r)"
   1.312                by simp
   1.313 @@ -1784,10 +1784,10 @@
   1.314          moreover
   1.315          {
   1.316            assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
   1.317 -          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field_inverse_zero}"]
   1.318 -          have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs ?p'"
   1.319 +          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field}"]
   1.320 +          have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'"
   1.321              by simp
   1.322 -          then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
   1.323 +          then have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
   1.324              using np nxdn
   1.325              apply simp
   1.326              apply (simp only: funpow_shift1_1)
   1.327 @@ -1861,7 +1861,7 @@
   1.328              from kk' have kk'': "Suc (k' - Suc k) = k' - k"
   1.329                by arith
   1.330              {
   1.331 -              fix bs :: "'a::{field_char_0,field_inverse_zero} list"
   1.332 +              fix bs :: "'a::{field_char_0,field} list"
   1.333                from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
   1.334                have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)"
   1.335                  by simp
   1.336 @@ -1875,7 +1875,7 @@
   1.337                  Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
   1.338                  by (simp add: field_simps)
   1.339              }
   1.340 -            then have ieq:"\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
   1.341 +            then have ieq:"\<forall>bs :: 'a::{field_char_0,field} list.
   1.342                  Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
   1.343                  Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
   1.344                by auto
   1.345 @@ -1900,7 +1900,7 @@
   1.346          {
   1.347            assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
   1.348            {
   1.349 -            fix bs :: "'a::{field_char_0,field_inverse_zero} list"
   1.350 +            fix bs :: "'a::{field_char_0,field} list"
   1.351              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
   1.352              have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'"
   1.353                by simp
   1.354 @@ -1909,10 +1909,10 @@
   1.355              then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
   1.356                by simp
   1.357            }
   1.358 -          then have hth: "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
   1.359 +          then have hth: "\<forall>bs :: 'a::{field_char_0,field} list.
   1.360              Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
   1.361            from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
   1.362 -            using isnpolyh_unique[where ?'a = "'a::{field_char_0,field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
   1.363 +            using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
   1.364                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
   1.365                simplified ap]
   1.366              by simp
   1.367 @@ -1945,7 +1945,7 @@
   1.368  qed
   1.369  
   1.370  lemma polydivide_properties:
   1.371 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.372 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.373      and np: "isnpolyh p n0"
   1.374      and ns: "isnpolyh s n1"
   1.375      and pnz: "p \<noteq> 0\<^sub>p"
   1.376 @@ -2112,12 +2112,12 @@
   1.377  lemma swapnorm:
   1.378    assumes nbs: "n < length bs"
   1.379      and mbs: "m < length bs"
   1.380 -  shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field_inverse_zero})) =
   1.381 +  shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field})) =
   1.382      Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
   1.383    using swap[OF assms] swapnorm_def by simp
   1.384  
   1.385  lemma swapnorm_isnpoly [simp]:
   1.386 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
   1.387 +  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.388    shows "isnpoly (swapnorm n m p)"
   1.389    unfolding swapnorm_def by simp
   1.390