src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 36409 d323e7773aa8 parent 36349 39be26d1bc28 child 39246 9e58f0499f57
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Apr 26 11:34:19 2010 +0200
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Apr 26 15:37:50 2010 +0200
1.3 @@ -230,7 +230,7 @@
1.4
1.5  subsection{* Semantics of the polynomial representation *}
1.6
1.7 -consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{ring_char_0,power,division_ring_inverse_zero,field}"
1.8 +consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}"
1.9  primrec
1.10    "Ipoly bs (C c) = INum c"
1.11    "Ipoly bs (Bound n) = bs!n"
1.12 @@ -241,7 +241,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  abbreviation
1.16 -  Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_ring_inverse_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
1.17 +  Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, 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 @@ -394,7 +394,7 @@
1.22  qed simp_all
1.23
1.24  lemma polymul_properties:
1.25 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.26 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.27    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1"
1.28    shows "isnpolyh (p *\<^sub>p q) (min n0 n1)"
1.29    and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)"
1.30 @@ -568,19 +568,19 @@
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, division_ring_inverse_zero, ring_char_0})"
1.35 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.36    shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
1.37    using polymul_properties(1)  by blast
1.38  lemma polymul_eq0_iff:
1.39 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.40 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.41    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.42    using polymul_properties(2)  by blast
1.43  lemma polymul_degreen:
1.44 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.45 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.46    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> 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.47    using polymul_properties(3) by blast
1.48  lemma polymul_norm:
1.49 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.50 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.51    shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul (p,q))"
1.52    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
1.53
1.54 @@ -591,7 +591,7 @@
1.55    by (induct p arbitrary: n0, auto)
1.56
1.57  lemma monic_eqI: assumes np: "isnpolyh p n0"
1.58 -  shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{ring_char_0,power,division_ring_inverse_zero,field})"
1.59 +  shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
1.60    unfolding monic_def Let_def
1.62    let ?h = "headconst p"
1.63 @@ -629,13 +629,13 @@
1.64
1.65  lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub(p,q))"
1.67 -lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.68 +lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.69    shows "isnpolyh p n0 \<Longrightarrow> polysub (p, p) = 0\<^sub>p"
1.70  unfolding polysub_def split_def fst_conv snd_conv
1.71  by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])
1.72
1.73  lemma polysub_0:
1.74 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.75 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.76    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
1.77    unfolding polysub_def split_def fst_conv snd_conv
1.78    apply (induct p q arbitrary: n0 n1 rule:polyadd.induct, simp_all add: Nsub0[simplified Nsub_def])
1.79 @@ -657,7 +657,7 @@
1.80    done
1.81
1.82  text{* polypow is a power function and preserves normal forms *}
1.83 -lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field, division_ring_inverse_zero, ring_char_0})) ^ n"
1.84 +lemma polypow[simp]: "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 thus ?case by simp
1.87  next
1.88 @@ -688,7 +688,7 @@
1.89  qed
1.90
1.91  lemma polypow_normh:
1.92 -    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.93 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.94    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
1.95  proof (induct k arbitrary: n rule: polypow.induct)
1.96    case (2 k n)
1.97 @@ -701,17 +701,17 @@
1.98  qed auto
1.99
1.100  lemma polypow_norm:
1.101 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.102 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.103    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
1.104    by (simp add: polypow_normh isnpoly_def)
1.105
1.106  text{* Finally the whole normalization*}
1.107
1.108 -lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field, division_ring_inverse_zero, ring_char_0})"
1.109 +lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
1.110  by (induct p rule:polynate.induct, auto)
1.111
1.112  lemma polynate_norm[simp]:
1.113 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.114 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.115    shows "isnpoly (polynate p)"
1.117
1.118 @@ -736,14 +736,14 @@
1.119    shows "isnpolyh (funpow k f p) n"
1.120    using f np by (induct k arbitrary: p, auto)
1.121
1.122 -lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field, division_ring_inverse_zero, ring_char_0}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
1.123 +lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
1.124    by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
1.125
1.126  lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
1.127    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
1.128
1.129  lemma funpow_shift1_1:
1.130 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field, division_ring_inverse_zero, ring_char_0}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"
1.131 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"
1.133
1.134  lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
1.135 @@ -751,7 +751,7 @@
1.136
1.138    assumes np: "isnpolyh p n"
1.139 -  shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field, division_ring_inverse_zero, ring_char_0})"
1.140 +  shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})"
1.141    using np
1.142  proof (induct p arbitrary: n rule: behead.induct)
1.143    case (1 c p n) hence pn: "isnpolyh p n" by simp
1.144 @@ -981,7 +981,7 @@
1.146
1.147  lemma isnpolyh_zero_iff:
1.148 -  assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{ring_char_0,power,division_ring_inverse_zero,field})"
1.149 +  assumes nq: "isnpolyh p n0" 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.150    shows "p = 0\<^sub>p"
1.151  using nq eq
1.152  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
1.153 @@ -1033,7 +1033,7 @@
1.154
1.155  lemma isnpolyh_unique:
1.156    assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"
1.157 -  shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{ring_char_0,power,division_ring_inverse_zero,field})) \<longleftrightarrow>  p = q"
1.158 +  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.159  proof(auto)
1.160    assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
1.161    hence "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp
1.162 @@ -1046,50 +1046,50 @@
1.163
1.164  text{* consequenses of unicity on the algorithms for polynomial normalization *}
1.165
1.166 -lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.167 +lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.168    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
1.170
1.171  lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
1.172  lemma one_normh: "isnpolyh 1\<^sub>p n" by simp
1.174 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.175 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.176    and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
1.177    using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np]
1.178      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
1.179
1.180  lemma polymul_1[simp]:
1.181 -    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.182 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.183    and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
1.184    using isnpolyh_unique[OF polymul_normh[OF np one_normh] np]
1.185      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
1.186  lemma polymul_0[simp]:
1.187 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.188 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.189    and np: "isnpolyh p n0" shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
1.190    using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh]
1.191      isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
1.192
1.193  lemma polymul_commute:
1.194 -    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.195 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.196    and np:"isnpolyh p n0" and nq: "isnpolyh q n1"
1.197    shows "p *\<^sub>p q = q *\<^sub>p p"
1.198 -using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{ring_char_0,power,division_ring_inverse_zero,field}"] by simp
1.199 +using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{field_char_0, field_inverse_zero, power}"] by simp
1.200
1.201  declare polyneg_polyneg[simp]
1.202
1.203  lemma isnpolyh_polynate_id[simp]:
1.204 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.205 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.206    and np:"isnpolyh p n0" shows "polynate p = p"
1.207 -  using isnpolyh_unique[where ?'a= "'a::{field, division_ring_inverse_zero, ring_char_0}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}"] by simp
1.208 +  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}"] by simp
1.209
1.210  lemma polynate_idempotent[simp]:
1.211 -    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.212 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.213    shows "polynate (polynate p) = polynate p"
1.214    using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
1.215
1.216  lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
1.217    unfolding poly_nate_def polypoly'_def ..
1.218 -lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field, division_ring_inverse_zero, ring_char_0}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
1.219 +lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0, field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
1.220    using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
1.221    unfolding poly_nate_polypoly' by (auto intro: ext)
1.222
1.223 @@ -1116,7 +1116,7 @@
1.224  qed
1.225
1.227 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.228 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.229    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q"
1.230    and d: "degree p = degree q"
1.231    shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
1.232 @@ -1226,7 +1226,7 @@
1.233  done
1.234
1.236 -   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.237 +   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.238    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.239  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
1.240    case (2 a b c' n' p' n0 n1)
1.241 @@ -1300,7 +1300,7 @@
1.242    by (induct p arbitrary: n0 rule: polyneg.induct, auto)
1.243
1.244  lemma degree_polymul:
1.245 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.246 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.247    and np: "isnpolyh p n0" and nq: "isnpolyh q n1"
1.248    shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
1.249    using polymul_degreen[OF np nq, where m="0"]  degree_eq_degreen0 by simp
1.250 @@ -1344,7 +1344,7 @@
1.251  qed
1.252
1.253  lemma polydivide_aux_properties:
1.254 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.255 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.256    and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
1.257    and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
1.258    shows "polydivide_aux_dom (a,n,p,k,s) \<and>
1.259 @@ -1415,19 +1415,19 @@
1.261                polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
1.262              have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp
1.263 -            from asp have "\<forall> (bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) =
1.264 +            from asp have "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) =
1.265                Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
1.266 -            hence " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
1.267 +            hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
1.268                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.270 -            hence " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.271 +            hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.272                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p)
1.273                + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.274                by (auto simp only: funpow_shift1_1)
1.275 -            hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.276 +            hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.277                Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p)
1.278                + Ipoly bs q) + Ipoly bs r" by (simp add: field_simps)
1.279 -            hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.280 +            hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.281                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)" by simp
1.282              with isnpolyh_unique[OF nakks' nqr']
1.283              have "a ^\<^sub>p (k' - k) *\<^sub>p s =
1.284 @@ -1444,9 +1444,9 @@
1.285              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
1.286            have dom: ?dths apply (rule polydivide_aux_real_domintros)
1.287              using ba dn' domsp by simp_all
1.288 -          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}"]
1.289 -          have " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs s = Ipoly bs ?p'" by simp
1.290 -          hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
1.291 +          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.292 +          have " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp
1.293 +          hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
1.294              by (simp only: funpow_shift1_1) simp
1.295            hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
1.296            {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
1.297 @@ -1501,7 +1501,7 @@
1.298                and dr: "degree r = 0 \<or> degree r < degree p"
1.299                and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto
1.300              from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
1.301 -            {fix bs:: "'a::{field, division_ring_inverse_zero, ring_char_0} list"
1.302 +            {fix bs:: "'a::{field_char_0, field_inverse_zero} list"
1.303
1.304              from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
1.305              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)" by simp
1.306 @@ -1511,7 +1511,7 @@
1.307                by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
1.308              hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
1.310 -            hence ieq:"\<forall>(bs :: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.311 +            hence ieq:"\<forall>(bs :: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.312                Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto
1.313              let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
1.314              from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap ] nxdn]]
1.315 @@ -1532,17 +1532,17 @@
1.316              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
1.317            have dom: ?dths using sz ba dn' domsp
1.318              by - (rule polydivide_aux_real_domintros, simp_all)
1.319 -          {fix bs :: "'a::{field, division_ring_inverse_zero, ring_char_0} list"
1.320 +          {fix bs :: "'a::{field_char_0, field_inverse_zero} list"
1.321              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
1.322            have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
1.323            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p"
1.324              by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
1.325            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
1.326          }
1.327 -        hence hth: "\<forall> (bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
1.328 +        hence hth: "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
1.329            from hth
1.330            have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
1.331 -            using isnpolyh_unique[where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.332 +            using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.333                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
1.334                simplified ap] by simp
1.335            {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
1.336 @@ -1566,7 +1566,7 @@
1.337  qed
1.338
1.339  lemma polydivide_properties:
1.340 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.341 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.342    and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \<noteq> 0\<^sub>p"
1.343    shows "(\<exists> k r. polydivide s p = (k,r) \<and> (\<exists>nr. isnpolyh r nr) \<and> (degree r = 0 \<or> degree r < degree p)
1.344    \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
1.345 @@ -1698,11 +1698,11 @@
1.346  definition "swapnorm n m t = polynate (swap n m t)"
1.347
1.348  lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
1.349 -  shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field, division_ring_inverse_zero, ring_char_0})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
1.350 +  shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
1.351    using swap[OF prems] swapnorm_def by simp
1.352
1.353  lemma swapnorm_isnpoly[simp]:
1.354 -    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
1.355 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.356    shows "isnpoly (swapnorm n m p)"
1.357    unfolding swapnorm_def by simp
1.358
```