src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 36349 39be26d1bc28
parent 35416 d8d7d1b785af
child 36409 d323e7773aa8
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Apr 26 11:34:15 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Apr 26 11:34:17 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_by_zero,field}"
     1.8 +consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{ring_char_0,power,division_ring_inverse_zero,field}"
     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_by_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    1.17 +  Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_ring_inverse_zero,field}" ("\<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 @@ -322,7 +322,7 @@
    1.22  qed auto
    1.23  
    1.24  lemma polyadd[simp]: "Ipoly bs (polyadd (p,q)) = (Ipoly bs p) + (Ipoly bs q)"
    1.25 -by (induct p q rule: polyadd.induct, auto simp add: Let_def ring_simps right_distrib[symmetric] simp del: right_distrib)
    1.26 +by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
    1.27  
    1.28  lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))"
    1.29    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
    1.30 @@ -394,7 +394,7 @@
    1.31  qed simp_all
    1.32  
    1.33  lemma polymul_properties:
    1.34 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.35 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    1.36    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1"
    1.37    shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" 
    1.38    and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)" 
    1.39 @@ -565,22 +565,22 @@
    1.40  qed auto
    1.41  
    1.42  lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)"
    1.43 -by(induct p q rule: polymul.induct, auto simp add: ring_simps)
    1.44 +by(induct p q rule: polymul.induct, auto simp add: field_simps)
    1.45  
    1.46  lemma polymul_normh: 
    1.47 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.48 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    1.49    shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
    1.50    using polymul_properties(1)  by blast
    1.51  lemma polymul_eq0_iff: 
    1.52 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.53 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    1.54    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.55    using polymul_properties(2)  by blast
    1.56  lemma polymul_degreen:  
    1.57 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.58 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    1.59    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.60    using polymul_properties(3) by blast
    1.61  lemma polymul_norm:   
    1.62 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.63 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    1.64    shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul (p,q))"
    1.65    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
    1.66  
    1.67 @@ -591,7 +591,7 @@
    1.68    by (induct p arbitrary: n0, auto)
    1.69  
    1.70  lemma monic_eqI: assumes np: "isnpolyh p n0" 
    1.71 -  shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{ring_char_0,power,division_by_zero,field})"
    1.72 +  shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{ring_char_0,power,division_ring_inverse_zero,field})"
    1.73    unfolding monic_def Let_def
    1.74  proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
    1.75    let ?h = "headconst p"
    1.76 @@ -629,13 +629,13 @@
    1.77  
    1.78  lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub(p,q))"
    1.79    using polyadd_norm polyneg_norm by (simp add: polysub_def) 
    1.80 -lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.81 +lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    1.82    shows "isnpolyh p n0 \<Longrightarrow> polysub (p, p) = 0\<^sub>p"
    1.83  unfolding polysub_def split_def fst_conv snd_conv
    1.84  by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])
    1.85  
    1.86  lemma polysub_0: 
    1.87 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    1.88 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    1.89    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
    1.90    unfolding polysub_def split_def fst_conv snd_conv
    1.91    apply (induct p q arbitrary: n0 n1 rule:polyadd.induct, simp_all add: Nsub0[simplified Nsub_def])
    1.92 @@ -657,7 +657,7 @@
    1.93    done
    1.94  
    1.95  text{* polypow is a power function and preserves normal forms *}
    1.96 -lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{ring_char_0,division_by_zero,field})) ^ n"
    1.97 +lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field, division_ring_inverse_zero, ring_char_0})) ^ n"
    1.98  proof(induct n rule: polypow.induct)
    1.99    case 1 thus ?case by simp
   1.100  next
   1.101 @@ -688,7 +688,7 @@
   1.102  qed
   1.103  
   1.104  lemma polypow_normh: 
   1.105 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.106 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.107    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
   1.108  proof (induct k arbitrary: n rule: polypow.induct)
   1.109    case (2 k n)
   1.110 @@ -701,17 +701,17 @@
   1.111  qed auto 
   1.112  
   1.113  lemma polypow_norm:   
   1.114 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.115 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.116    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
   1.117    by (simp add: polypow_normh isnpoly_def)
   1.118  
   1.119  text{* Finally the whole normalization*}
   1.120  
   1.121 -lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{ring_char_0,division_by_zero,field})"
   1.122 +lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field, division_ring_inverse_zero, ring_char_0})"
   1.123  by (induct p rule:polynate.induct, auto)
   1.124  
   1.125  lemma polynate_norm[simp]: 
   1.126 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.127 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.128    shows "isnpoly (polynate p)"
   1.129    by (induct p rule: polynate.induct, simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm) (simp_all add: isnpoly_def)
   1.130  
   1.131 @@ -736,29 +736,29 @@
   1.132    shows "isnpolyh (funpow k f p) n"
   1.133    using f np by (induct k arbitrary: p, auto)
   1.134  
   1.135 -lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {ring_char_0,division_by_zero,field}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
   1.136 +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.137    by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
   1.138  
   1.139  lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
   1.140    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   1.141  
   1.142  lemma funpow_shift1_1: 
   1.143 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {ring_char_0,division_by_zero,field}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"
   1.144 +  "(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.145    by (simp add: funpow_shift1)
   1.146  
   1.147  lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
   1.148 -by (induct p  arbitrary: n0 rule: poly_cmul.induct, auto simp add: ring_simps)
   1.149 +by (induct p  arbitrary: n0 rule: poly_cmul.induct, auto simp add: field_simps)
   1.150  
   1.151  lemma behead:
   1.152    assumes np: "isnpolyh p n"
   1.153 -  shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {ring_char_0,division_by_zero,field})"
   1.154 +  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.155    using np
   1.156  proof (induct p arbitrary: n rule: behead.induct)
   1.157    case (1 c p n) hence pn: "isnpolyh p n" by simp
   1.158    from prems(2)[OF pn] 
   1.159    have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . 
   1.160    then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
   1.161 -    by (simp_all add: th[symmetric] ring_simps power_Suc)
   1.162 +    by (simp_all add: th[symmetric] field_simps power_Suc)
   1.163  qed (auto simp add: Let_def)
   1.164  
   1.165  lemma behead_isnpolyh:
   1.166 @@ -981,7 +981,7 @@
   1.167    by (simp add: head_eq_headn0)
   1.168  
   1.169  lemma isnpolyh_zero_iff: 
   1.170 -  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_by_zero,field})"
   1.171 +  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.172    shows "p = 0\<^sub>p"
   1.173  using nq eq
   1.174  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
   1.175 @@ -1033,7 +1033,7 @@
   1.176  
   1.177  lemma isnpolyh_unique:  
   1.178    assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"
   1.179 -  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_by_zero,field})) \<longleftrightarrow>  p = q"
   1.180 +  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.181  proof(auto)
   1.182    assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
   1.183    hence "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp
   1.184 @@ -1046,50 +1046,50 @@
   1.185  
   1.186  text{* consequenses of unicity on the algorithms for polynomial normalization *}
   1.187  
   1.188 -lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.189 +lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.190    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
   1.191    using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
   1.192  
   1.193  lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
   1.194  lemma one_normh: "isnpolyh 1\<^sub>p n" by simp
   1.195  lemma polyadd_0[simp]: 
   1.196 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.197 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.198    and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
   1.199    using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] 
   1.200      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
   1.201  
   1.202  lemma polymul_1[simp]: 
   1.203 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.204 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.205    and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
   1.206    using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 
   1.207      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
   1.208  lemma polymul_0[simp]: 
   1.209 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.210 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.211    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.212    using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] 
   1.213      isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
   1.214  
   1.215  lemma polymul_commute: 
   1.216 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.217 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.218    and np:"isnpolyh p n0" and nq: "isnpolyh q n1"
   1.219    shows "p *\<^sub>p q = q *\<^sub>p p"
   1.220 -using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{ring_char_0,power,division_by_zero,field}"] by simp
   1.221 +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.222  
   1.223  declare polyneg_polyneg[simp]
   1.224    
   1.225  lemma isnpolyh_polynate_id[simp]: 
   1.226 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.227 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.228    and np:"isnpolyh p n0" shows "polynate p = p"
   1.229 -  using isnpolyh_unique[where ?'a= "'a::{ring_char_0,division_by_zero,field}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{ring_char_0,division_by_zero,field}"] by simp
   1.230 +  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.231  
   1.232  lemma polynate_idempotent[simp]: 
   1.233 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.234 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   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  lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
   1.239    unfolding poly_nate_def polypoly'_def ..
   1.240 -lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{ring_char_0,division_by_zero,field}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   1.241 +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.242    using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
   1.243    unfolding poly_nate_polypoly' by (auto intro: ext)
   1.244  
   1.245 @@ -1116,7 +1116,7 @@
   1.246  qed
   1.247  
   1.248  lemma degree_polysub_samehead: 
   1.249 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.250 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.251    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" 
   1.252    and d: "degree p = degree q"
   1.253    shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
   1.254 @@ -1226,7 +1226,7 @@
   1.255  done
   1.256  
   1.257  lemma polymul_head_polyeq: 
   1.258 -   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.259 +   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.260    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.261  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   1.262    case (2 a b c' n' p' n0 n1)
   1.263 @@ -1300,7 +1300,7 @@
   1.264    by (induct p arbitrary: n0 rule: polyneg.induct, auto)
   1.265  
   1.266  lemma degree_polymul:
   1.267 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.268 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.269    and np: "isnpolyh p n0" and nq: "isnpolyh q n1"
   1.270    shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
   1.271    using polymul_degreen[OF np nq, where m="0"]  degree_eq_degreen0 by simp
   1.272 @@ -1344,7 +1344,7 @@
   1.273  qed
   1.274  
   1.275  lemma polydivide_aux_properties:
   1.276 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.277 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.278    and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
   1.279    and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
   1.280    shows "polydivide_aux_dom (a,n,p,k,s) \<and> 
   1.281 @@ -1415,19 +1415,19 @@
   1.282              from polyadd_normh[OF polymul_normh[OF np 
   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" by simp 
   1.285 -            from asp have "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = 
   1.286 +            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.287                Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
   1.288 -            hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = 
   1.289 +            hence " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = 
   1.290                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" 
   1.291 -              by (simp add: ring_simps)
   1.292 -            hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   1.293 +              by (simp add: field_simps)
   1.294 +            hence " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   1.295                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p) 
   1.296                + Ipoly bs p * Ipoly bs q + Ipoly bs r"
   1.297                by (auto simp only: funpow_shift1_1) 
   1.298 -            hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   1.299 +            hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   1.300                Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p) 
   1.301 -              + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
   1.302 -            hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   1.303 +              + Ipoly bs q) + Ipoly bs r" by (simp add: field_simps)
   1.304 +            hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   1.305                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.306              with isnpolyh_unique[OF nakks' nqr']
   1.307              have "a ^\<^sub>p (k' - k) *\<^sub>p s = 
   1.308 @@ -1444,9 +1444,9 @@
   1.309              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   1.310            have dom: ?dths apply (rule polydivide_aux_real_domintros) 
   1.311              using ba dn' domsp by simp_all
   1.312 -          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{ring_char_0,division_by_zero,field}"]
   1.313 -          have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
   1.314 -          hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
   1.315 +          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.316 +          have " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs s = Ipoly bs ?p'" by simp
   1.317 +          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.318              by (simp only: funpow_shift1_1) simp
   1.319            hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
   1.320            {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
   1.321 @@ -1501,17 +1501,17 @@
   1.322                and dr: "degree r = 0 \<or> degree r < degree p"
   1.323                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.324              from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
   1.325 -            {fix bs:: "'a::{ring_char_0,division_by_zero,field} list"
   1.326 +            {fix bs:: "'a::{field, division_ring_inverse_zero, ring_char_0} list"
   1.327                
   1.328              from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
   1.329              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.330              hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r"
   1.331 -              by (simp add: ring_simps power_Suc)
   1.332 +              by (simp add: field_simps power_Suc)
   1.333              hence "Ipoly bs a ^ (k' - k)  * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r"
   1.334                by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
   1.335              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.336 -              by (simp add: ring_simps)}
   1.337 -            hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   1.338 +              by (simp add: field_simps)}
   1.339 +            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.340                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.341              let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
   1.342              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.343 @@ -1532,17 +1532,17 @@
   1.344              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   1.345            have dom: ?dths using sz ba dn' domsp 
   1.346              by - (rule polydivide_aux_real_domintros, simp_all)
   1.347 -          {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
   1.348 +          {fix bs :: "'a::{field, division_ring_inverse_zero, ring_char_0} list"
   1.349              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
   1.350            have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
   1.351            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" 
   1.352              by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
   1.353            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
   1.354          }
   1.355 -        hence hth: "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
   1.356 +        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.357            from hth
   1.358            have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" 
   1.359 -            using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
   1.360 +            using isnpolyh_unique[where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
   1.361                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
   1.362                simplified ap] by simp
   1.363            {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
   1.364 @@ -1566,7 +1566,7 @@
   1.365  qed
   1.366  
   1.367  lemma polydivide_properties: 
   1.368 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.369 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.370    and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \<noteq> 0\<^sub>p"
   1.371    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.372    \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
   1.373 @@ -1698,11 +1698,11 @@
   1.374  definition "swapnorm n m t = polynate (swap n m t)"
   1.375  
   1.376  lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
   1.377 -  shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{ring_char_0,division_by_zero,field})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
   1.378 +  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.379    using swap[OF prems] swapnorm_def by simp
   1.380  
   1.381  lemma swapnorm_isnpoly[simp]: 
   1.382 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   1.383 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   1.384    shows "isnpoly (swapnorm n m p)"
   1.385    unfolding swapnorm_def by simp
   1.386