src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 68442 477b3f7067c9 parent 67123 3fe40ff1b921
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 14 10:51:12 2018 +0200
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 14 15:45:53 2018 +0200
1.3 @@ -234,7 +234,7 @@
1.4
1.5  subsection \<open>Semantics of the polynomial representation\<close>
1.6
1.7 -primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
1.8 +primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,power}"
1.9    where
1.10      "Ipoly bs (C c) = INum c"
1.11    | "Ipoly bs (Bound n) = bs!n"
1.12 @@ -245,7 +245,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,power}"  ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
1.17 +abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,power}"  ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
1.18    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
1.19
1.20  lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i"
1.21 @@ -462,7 +462,7 @@
1.22  qed simp_all
1.23
1.24  lemma polymul_properties:
1.25 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.26 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
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 @@ -646,23 +646,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})"
1.35 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
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})"
1.41 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
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})"
1.47 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
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})"
1.54 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
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 @@ -675,7 +675,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, power})"
1.63 +    (Ipoly bs p ::'a::{field_char_0, power})"
1.64    unfolding monic_def Let_def
1.66    let ?h = "headconst p"
1.67 @@ -726,13 +726,13 @@
1.69
1.70  lemma polysub_same_0[simp]:
1.71 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.72 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
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})"
1.79 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
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 @@ -740,7 +740,7 @@
1.84
1.85  text \<open>polypow is a power function and preserves normal forms\<close>
1.86
1.87 -lemma polypow[simp]: "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
1.88 +lemma polypow[simp]: "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::field_char_0) ^ n"
1.89  proof (induct n rule: polypow.induct)
1.90    case 1
1.91    then show ?case by simp
1.92 @@ -777,7 +777,7 @@
1.93  qed
1.94
1.95  lemma polypow_normh:
1.96 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.97 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
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 @@ -796,17 +796,17 @@
1.102  qed
1.103
1.104  lemma polypow_norm:
1.105 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.106 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.107    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
1.108    by (simp add: polypow_normh isnpoly_def)
1.109
1.110  text \<open>Finally the whole normalization\<close>
1.111
1.112 -lemma polynate [simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
1.113 +lemma polynate [simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::field_char_0)"
1.114    by (induct p rule:polynate.induct) auto
1.115
1.116  lemma polynate_norm[simp]:
1.117 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.118 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.119    shows "isnpoly (polynate p)"
1.120    by (induct p rule: polynate.induct)
1.122 @@ -836,7 +836,7 @@
1.123    using assms by (induct k arbitrary: p) auto
1.124
1.125  lemma funpow_shift1:
1.126 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
1.127 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: field_char_0) =
1.128      Ipoly bs (Mul (Pw (Bound 0) n) p)"
1.129    by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
1.130
1.131 @@ -844,7 +844,7 @@
1.132    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
1.133
1.134  lemma funpow_shift1_1:
1.135 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
1.136 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: field_char_0) =
1.137      Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
1.139
1.140 @@ -854,7 +854,7 @@
1.142    assumes "isnpolyh p n"
1.144 -    (Ipoly bs p :: 'a :: {field_char_0,field})"
1.145 +    (Ipoly bs p :: 'a :: field_char_0)"
1.146    using assms
1.147  proof (induct p arbitrary: n rule: behead.induct)
1.148    case (1 c p n)
1.149 @@ -1120,7 +1120,7 @@
1.150
1.151  lemma isnpolyh_zero_iff:
1.152    assumes nq: "isnpolyh p n0"
1.153 -    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.154 +    and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, power})"
1.155    shows "p = 0\<^sub>p"
1.156    using nq eq
1.157  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
1.158 @@ -1197,7 +1197,7 @@
1.159  lemma isnpolyh_unique:
1.160    assumes np: "isnpolyh p n0"
1.161      and nq: "isnpolyh q n1"
1.162 -  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.163 +  shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,power})) \<longleftrightarrow> p = q"
1.164  proof auto
1.165    assume "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a) = \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
1.166    then have "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)"
1.167 @@ -1212,7 +1212,7 @@
1.168  text \<open>Consequences of unicity on the algorithms for polynomial normalization.\<close>
1.169
1.171 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.172 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.173      and np: "isnpolyh p n0"
1.174      and nq: "isnpolyh q n1"
1.175    shows "p +\<^sub>p q = q +\<^sub>p p"
1.176 @@ -1226,7 +1226,7 @@
1.177    by simp
1.178
1.180 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.181 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.182      and np: "isnpolyh p n0"
1.183    shows "p +\<^sub>p 0\<^sub>p = p"
1.184      and "0\<^sub>p +\<^sub>p p = p"
1.185 @@ -1234,7 +1234,7 @@
1.186      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
1.187
1.188  lemma polymul_1[simp]:
1.189 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.190 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.191      and np: "isnpolyh p n0"
1.192    shows "p *\<^sub>p (1)\<^sub>p = p"
1.193      and "(1)\<^sub>p *\<^sub>p p = p"
1.194 @@ -1242,7 +1242,7 @@
1.195      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
1.196
1.197  lemma polymul_0[simp]:
1.198 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.199 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.200      and np: "isnpolyh p n0"
1.201    shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p"
1.202      and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
1.203 @@ -1250,27 +1250,27 @@
1.204      isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
1.205
1.206  lemma polymul_commute:
1.207 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.208 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.209      and np: "isnpolyh p n0"
1.210      and nq: "isnpolyh q n1"
1.211    shows "p *\<^sub>p q = q *\<^sub>p p"
1.212    using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np],
1.213 -    where ?'a = "'a::{field_char_0,field, power}"]
1.214 +    where ?'a = "'a::{field_char_0, power}"]
1.215    by simp
1.216
1.217  declare polyneg_polyneg [simp]
1.218
1.219  lemma isnpolyh_polynate_id [simp]:
1.220 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.221 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.222      and np: "isnpolyh p n0"
1.223    shows "polynate p = p"
1.224 -  using isnpolyh_unique[where ?'a= "'a::{field_char_0,field}",
1.225 +  using isnpolyh_unique[where ?'a= "'a::field_char_0",
1.226        OF polynate_norm[of p, unfolded isnpoly_def] np]
1.227 -    polynate[where ?'a = "'a::{field_char_0,field}"]
1.228 +    polynate[where ?'a = "'a::field_char_0"]
1.229    by simp
1.230
1.231  lemma polynate_idempotent[simp]:
1.232 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.233 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.234    shows "polynate (polynate p) = polynate p"
1.235    using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
1.236
1.237 @@ -1278,7 +1278,7 @@
1.238    unfolding poly_nate_def polypoly'_def ..
1.239
1.240  lemma poly_nate_poly:
1.241 -  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
1.242 +  "poly (poly_nate bs p) = (\<lambda>x:: 'a ::field_char_0. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
1.243    using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
1.244    unfolding poly_nate_polypoly' by auto
1.245
1.246 @@ -1317,7 +1317,7 @@
1.247  qed
1.248
1.250 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.251 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.252      and np: "isnpolyh p n0"
1.253      and nq: "isnpolyh q n1"
1.255 @@ -1478,7 +1478,7 @@
1.256    done
1.257
1.259 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.260 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.261    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.262  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
1.263    case (2 c c' n' p' n0 n1)
1.264 @@ -1575,7 +1575,7 @@
1.265    by (induct p arbitrary: n0 rule: polyneg.induct) auto
1.266
1.267  lemma degree_polymul:
1.268 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.269 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.270      and np: "isnpolyh p n0"
1.271      and nq: "isnpolyh q n1"
1.272    shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
1.273 @@ -1591,7 +1591,7 @@
1.274  subsection \<open>Correctness of polynomial pseudo division\<close>
1.275
1.276  lemma polydivide_aux_properties:
1.277 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.278 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.279      and np: "isnpolyh p n0"
1.280      and ns: "isnpolyh s n1"
1.281      and ap: "head p = a"
1.282 @@ -1684,24 +1684,24 @@
1.283                polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
1.284              have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0"
1.285                by simp
1.286 -            from asp have "\<forall>bs :: 'a::{field_char_0,field} list.
1.287 +            from asp have "\<forall>bs :: 'a::field_char_0 list.
1.288                Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)"
1.289                by simp
1.290 -            then have "\<forall>bs :: 'a::{field_char_0,field} list.
1.291 +            then have "\<forall>bs :: 'a::field_char_0 list.
1.292                Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
1.293                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.295 -            then have "\<forall>bs :: 'a::{field_char_0,field} list.
1.296 +            then have "\<forall>bs :: 'a::field_char_0 list.
1.297                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.298                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) +
1.299                Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.300                by (auto simp only: funpow_shift1_1)
1.301 -            then have "\<forall>bs:: 'a::{field_char_0,field} list.
1.302 +            then have "\<forall>bs:: 'a::field_char_0 list.
1.303                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.304                Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) +
1.305                Ipoly bs q) + Ipoly bs r"
1.307 -            then have "\<forall>bs:: 'a::{field_char_0,field} list.
1.308 +            then have "\<forall>bs:: 'a::field_char_0 list.
1.309                Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.310                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.311                by simp
1.312 @@ -1720,10 +1720,10 @@
1.313            then show ?thesis by blast
1.314          next
1.315            case spz: 2
1.316 -          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field}"]
1.317 -          have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'"
1.318 +          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::field_char_0"]
1.319 +          have "\<forall>bs:: 'a::field_char_0 list. Ipoly bs s = Ipoly bs ?p'"
1.320              by simp
1.321 -          with np nxdn have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
1.322 +          with np nxdn have "\<forall>bs:: 'a::field_char_0 list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
1.323              by (simp only: funpow_shift1_1) simp
1.324            then have sp': "s = ?xdn *\<^sub>p p"
1.325              using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]]
1.326 @@ -1801,7 +1801,7 @@
1.327                by arith
1.328              have "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.329                  Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
1.330 -              for bs :: "'a::{field_char_0,field} list"
1.331 +              for bs :: "'a::field_char_0 list"
1.332              proof -
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 @@ -1815,7 +1815,7 @@
1.336                then show ?thesis
1.338              qed
1.339 -            then have ieq: "\<forall>bs :: 'a::{field_char_0,field} list.
1.340 +            then have ieq: "\<forall>bs :: 'a::field_char_0 list.
1.341                  Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.342                  Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)"
1.343                by auto
1.344 @@ -1837,10 +1837,10 @@
1.345            then show ?thesis by blast
1.346          next
1.347            case spz: 2
1.348 -          have hth: "\<forall>bs :: 'a::{field_char_0,field} list.
1.349 +          have hth: "\<forall>bs :: 'a::field_char_0 list.
1.350              Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
1.351            proof
1.352 -            fix bs :: "'a::{field_char_0,field} list"
1.353 +            fix bs :: "'a::field_char_0 list"
1.354              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
1.355              have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'"
1.356                by simp
1.357 @@ -1850,7 +1850,7 @@
1.358                by simp
1.359            qed
1.360            from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
1.361 -            using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.362 +            using isnpolyh_unique[where ?'a = "'a::field_char_0", OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.363                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
1.364                simplified ap]
1.365              by simp
1.366 @@ -1876,7 +1876,7 @@
1.367  qed
1.368
1.369  lemma polydivide_properties:
1.370 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.371 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.372      and np: "isnpolyh p n0"
1.373      and ns: "isnpolyh s n1"
1.374      and pnz: "p \<noteq> 0\<^sub>p"
1.375 @@ -2041,12 +2041,12 @@
1.376  lemma swapnorm:
1.377    assumes nbs: "n < length bs"
1.378      and mbs: "m < length bs"
1.379 -  shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field})) =
1.380 +  shows "((Ipoly bs (swapnorm n m t) :: 'a::field_char_0)) =
1.381      Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
1.382    using swap[OF assms] swapnorm_def by simp
1.383
1.384  lemma swapnorm_isnpoly [simp]:
1.385 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
1.386 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
1.387    shows "isnpoly (swapnorm n m p)"
1.388    unfolding swapnorm_def by simp
1.389
```