class division_ring_inverse_zero
authorhaftmann
Mon Apr 26 11:34:17 2010 +0200 (2010-04-26)
changeset 3634939be26d1bc28
parent 36348 89c54f51f55a
child 36350 bc7982c54e37
class division_ring_inverse_zero
src/HOL/Big_Operators.thy
src/HOL/Complex.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy
src/HOL/Groebner_Basis.thy
src/HOL/Import/HOL/real.imp
src/HOL/Import/HOL/realax.imp
src/HOL/Int.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/Bit.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/StarDef.thy
src/HOL/Power.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
src/HOL/RealVector.thy
src/HOL/Series.thy
src/HOL/Tools/numeral_simprocs.ML
     1.1 --- a/src/HOL/Big_Operators.thy	Mon Apr 26 11:34:15 2010 +0200
     1.2 +++ b/src/HOL/Big_Operators.thy	Mon Apr 26 11:34:17 2010 +0200
     1.3 @@ -1033,12 +1033,12 @@
     1.4    by (erule finite_induct) (auto simp add: insert_Diff_if)
     1.5  
     1.6  lemma setprod_inversef: 
     1.7 -  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
     1.8 +  fixes f :: "'b \<Rightarrow> 'a::{field,division_ring_inverse_zero}"
     1.9    shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
    1.10  by (erule finite_induct) auto
    1.11  
    1.12  lemma setprod_dividef:
    1.13 -  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
    1.14 +  fixes f :: "'b \<Rightarrow> 'a::{field,division_ring_inverse_zero}"
    1.15    shows "finite A
    1.16      ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
    1.17  apply (subgoal_tac
    1.18 @@ -1140,7 +1140,7 @@
    1.19        using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
    1.20        by simp
    1.21      then have ?thesis using a cA
    1.22 -      by (simp add: fA1 ring_simps cong add: setprod_cong cong del: if_weak_cong)}
    1.23 +      by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
    1.24    ultimately show ?thesis by blast
    1.25  qed
    1.26  
     2.1 --- a/src/HOL/Complex.thy	Mon Apr 26 11:34:15 2010 +0200
     2.2 +++ b/src/HOL/Complex.thy	Mon Apr 26 11:34:17 2010 +0200
     2.3 @@ -99,7 +99,7 @@
     2.4  
     2.5  subsection {* Multiplication and Division *}
     2.6  
     2.7 -instantiation complex :: "{field, division_by_zero}"
     2.8 +instantiation complex :: "{field, division_ring_inverse_zero}"
     2.9  begin
    2.10  
    2.11  definition
     3.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Apr 26 11:34:15 2010 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Apr 26 11:34:17 2010 +0200
     3.3 @@ -230,7 +230,7 @@
     3.4  
     3.5  subsection{* Semantics of the polynomial representation *}
     3.6  
     3.7 -consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{ring_char_0,power,division_by_zero,field}"
     3.8 +consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{ring_char_0,power,division_ring_inverse_zero,field}"
     3.9  primrec
    3.10    "Ipoly bs (C c) = INum c"
    3.11    "Ipoly bs (Bound n) = bs!n"
    3.12 @@ -241,7 +241,7 @@
    3.13    "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
    3.14    "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
    3.15  abbreviation
    3.16 -  Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_by_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    3.17 +  Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_ring_inverse_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    3.18    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
    3.19  
    3.20  lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" 
    3.21 @@ -322,7 +322,7 @@
    3.22  qed auto
    3.23  
    3.24  lemma polyadd[simp]: "Ipoly bs (polyadd (p,q)) = (Ipoly bs p) + (Ipoly bs q)"
    3.25 -by (induct p q rule: polyadd.induct, auto simp add: Let_def ring_simps right_distrib[symmetric] simp del: right_distrib)
    3.26 +by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
    3.27  
    3.28  lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))"
    3.29    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
    3.30 @@ -394,7 +394,7 @@
    3.31  qed simp_all
    3.32  
    3.33  lemma polymul_properties:
    3.34 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    3.35 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    3.36    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1"
    3.37    shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" 
    3.38    and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)" 
    3.39 @@ -565,22 +565,22 @@
    3.40  qed auto
    3.41  
    3.42  lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)"
    3.43 -by(induct p q rule: polymul.induct, auto simp add: ring_simps)
    3.44 +by(induct p q rule: polymul.induct, auto simp add: field_simps)
    3.45  
    3.46  lemma polymul_normh: 
    3.47 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    3.48 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    3.49    shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
    3.50    using polymul_properties(1)  by blast
    3.51  lemma polymul_eq0_iff: 
    3.52 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    3.53 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    3.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) "
    3.55    using polymul_properties(2)  by blast
    3.56  lemma polymul_degreen:  
    3.57 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    3.58 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    3.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)"
    3.60    using polymul_properties(3) by blast
    3.61  lemma polymul_norm:   
    3.62 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    3.63 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    3.64    shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul (p,q))"
    3.65    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
    3.66  
    3.67 @@ -591,7 +591,7 @@
    3.68    by (induct p arbitrary: n0, auto)
    3.69  
    3.70  lemma monic_eqI: assumes np: "isnpolyh p n0" 
    3.71 -  shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{ring_char_0,power,division_by_zero,field})"
    3.72 +  shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{ring_char_0,power,division_ring_inverse_zero,field})"
    3.73    unfolding monic_def Let_def
    3.74  proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
    3.75    let ?h = "headconst p"
    3.76 @@ -629,13 +629,13 @@
    3.77  
    3.78  lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub(p,q))"
    3.79    using polyadd_norm polyneg_norm by (simp add: polysub_def) 
    3.80 -lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    3.81 +lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    3.82    shows "isnpolyh p n0 \<Longrightarrow> polysub (p, p) = 0\<^sub>p"
    3.83  unfolding polysub_def split_def fst_conv snd_conv
    3.84  by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])
    3.85  
    3.86  lemma polysub_0: 
    3.87 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
    3.88 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    3.89    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
    3.90    unfolding polysub_def split_def fst_conv snd_conv
    3.91    apply (induct p q arbitrary: n0 n1 rule:polyadd.induct, simp_all add: Nsub0[simplified Nsub_def])
    3.92 @@ -657,7 +657,7 @@
    3.93    done
    3.94  
    3.95  text{* polypow is a power function and preserves normal forms *}
    3.96 -lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{ring_char_0,division_by_zero,field})) ^ n"
    3.97 +lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field, division_ring_inverse_zero, ring_char_0})) ^ n"
    3.98  proof(induct n rule: polypow.induct)
    3.99    case 1 thus ?case by simp
   3.100  next
   3.101 @@ -688,7 +688,7 @@
   3.102  qed
   3.103  
   3.104  lemma polypow_normh: 
   3.105 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.106 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.107    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
   3.108  proof (induct k arbitrary: n rule: polypow.induct)
   3.109    case (2 k n)
   3.110 @@ -701,17 +701,17 @@
   3.111  qed auto 
   3.112  
   3.113  lemma polypow_norm:   
   3.114 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.115 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.116    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
   3.117    by (simp add: polypow_normh isnpoly_def)
   3.118  
   3.119  text{* Finally the whole normalization*}
   3.120  
   3.121 -lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{ring_char_0,division_by_zero,field})"
   3.122 +lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field, division_ring_inverse_zero, ring_char_0})"
   3.123  by (induct p rule:polynate.induct, auto)
   3.124  
   3.125  lemma polynate_norm[simp]: 
   3.126 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.127 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.128    shows "isnpoly (polynate p)"
   3.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)
   3.130  
   3.131 @@ -736,29 +736,29 @@
   3.132    shows "isnpolyh (funpow k f p) n"
   3.133    using f np by (induct k arbitrary: p, auto)
   3.134  
   3.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)"
   3.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)"
   3.137    by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
   3.138  
   3.139  lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
   3.140    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   3.141  
   3.142  lemma funpow_shift1_1: 
   3.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)"
   3.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)"
   3.145    by (simp add: funpow_shift1)
   3.146  
   3.147  lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
   3.148 -by (induct p  arbitrary: n0 rule: poly_cmul.induct, auto simp add: ring_simps)
   3.149 +by (induct p  arbitrary: n0 rule: poly_cmul.induct, auto simp add: field_simps)
   3.150  
   3.151  lemma behead:
   3.152    assumes np: "isnpolyh p n"
   3.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})"
   3.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})"
   3.155    using np
   3.156  proof (induct p arbitrary: n rule: behead.induct)
   3.157    case (1 c p n) hence pn: "isnpolyh p n" by simp
   3.158    from prems(2)[OF pn] 
   3.159    have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . 
   3.160    then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
   3.161 -    by (simp_all add: th[symmetric] ring_simps power_Suc)
   3.162 +    by (simp_all add: th[symmetric] field_simps power_Suc)
   3.163  qed (auto simp add: Let_def)
   3.164  
   3.165  lemma behead_isnpolyh:
   3.166 @@ -981,7 +981,7 @@
   3.167    by (simp add: head_eq_headn0)
   3.168  
   3.169  lemma isnpolyh_zero_iff: 
   3.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})"
   3.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})"
   3.172    shows "p = 0\<^sub>p"
   3.173  using nq eq
   3.174  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
   3.175 @@ -1033,7 +1033,7 @@
   3.176  
   3.177  lemma isnpolyh_unique:  
   3.178    assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"
   3.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"
   3.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"
   3.181  proof(auto)
   3.182    assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
   3.183    hence "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp
   3.184 @@ -1046,50 +1046,50 @@
   3.185  
   3.186  text{* consequenses of unicity on the algorithms for polynomial normalization *}
   3.187  
   3.188 -lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.189 +lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.190    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
   3.191    using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
   3.192  
   3.193  lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
   3.194  lemma one_normh: "isnpolyh 1\<^sub>p n" by simp
   3.195  lemma polyadd_0[simp]: 
   3.196 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.197 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.198    and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
   3.199    using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] 
   3.200      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
   3.201  
   3.202  lemma polymul_1[simp]: 
   3.203 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.204 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.205    and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
   3.206    using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 
   3.207      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
   3.208  lemma polymul_0[simp]: 
   3.209 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.210 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.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"
   3.212    using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] 
   3.213      isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
   3.214  
   3.215  lemma polymul_commute: 
   3.216 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.217 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.218    and np:"isnpolyh p n0" and nq: "isnpolyh q n1"
   3.219    shows "p *\<^sub>p q = q *\<^sub>p p"
   3.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
   3.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
   3.222  
   3.223  declare polyneg_polyneg[simp]
   3.224    
   3.225  lemma isnpolyh_polynate_id[simp]: 
   3.226 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.227 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.228    and np:"isnpolyh p n0" shows "polynate p = p"
   3.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
   3.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
   3.231  
   3.232  lemma polynate_idempotent[simp]: 
   3.233 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.234 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.235    shows "polynate (polynate p) = polynate p"
   3.236    using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
   3.237  
   3.238  lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
   3.239    unfolding poly_nate_def polypoly'_def ..
   3.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>)"
   3.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>)"
   3.242    using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
   3.243    unfolding poly_nate_polypoly' by (auto intro: ext)
   3.244  
   3.245 @@ -1116,7 +1116,7 @@
   3.246  qed
   3.247  
   3.248  lemma degree_polysub_samehead: 
   3.249 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.250 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.251    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" 
   3.252    and d: "degree p = degree q"
   3.253    shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
   3.254 @@ -1226,7 +1226,7 @@
   3.255  done
   3.256  
   3.257  lemma polymul_head_polyeq: 
   3.258 -   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.259 +   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.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"
   3.261  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   3.262    case (2 a b c' n' p' n0 n1)
   3.263 @@ -1300,7 +1300,7 @@
   3.264    by (induct p arbitrary: n0 rule: polyneg.induct, auto)
   3.265  
   3.266  lemma degree_polymul:
   3.267 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.268 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.269    and np: "isnpolyh p n0" and nq: "isnpolyh q n1"
   3.270    shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
   3.271    using polymul_degreen[OF np nq, where m="0"]  degree_eq_degreen0 by simp
   3.272 @@ -1344,7 +1344,7 @@
   3.273  qed
   3.274  
   3.275  lemma polydivide_aux_properties:
   3.276 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.277 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.278    and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
   3.279    and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
   3.280    shows "polydivide_aux_dom (a,n,p,k,s) \<and> 
   3.281 @@ -1415,19 +1415,19 @@
   3.282              from polyadd_normh[OF polymul_normh[OF np 
   3.283                polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
   3.284              have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp 
   3.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')) = 
   3.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')) = 
   3.287                Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
   3.288 -            hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = 
   3.289 +            hence " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = 
   3.290                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" 
   3.291 -              by (simp add: ring_simps)
   3.292 -            hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.293 +              by (simp add: field_simps)
   3.294 +            hence " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.295                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p) 
   3.296                + Ipoly bs p * Ipoly bs q + Ipoly bs r"
   3.297                by (auto simp only: funpow_shift1_1) 
   3.298 -            hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.299 +            hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.300                Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p) 
   3.301 -              + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
   3.302 -            hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.303 +              + Ipoly bs q) + Ipoly bs r" by (simp add: field_simps)
   3.304 +            hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.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
   3.306              with isnpolyh_unique[OF nakks' nqr']
   3.307              have "a ^\<^sub>p (k' - k) *\<^sub>p s = 
   3.308 @@ -1444,9 +1444,9 @@
   3.309              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   3.310            have dom: ?dths apply (rule polydivide_aux_real_domintros) 
   3.311              using ba dn' domsp by simp_all
   3.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}"]
   3.313 -          have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
   3.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
   3.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}"]
   3.316 +          have " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs s = Ipoly bs ?p'" by simp
   3.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
   3.318              by (simp only: funpow_shift1_1) simp
   3.319            hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
   3.320            {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
   3.321 @@ -1501,17 +1501,17 @@
   3.322                and dr: "degree r = 0 \<or> degree r < degree p"
   3.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
   3.324              from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
   3.325 -            {fix bs:: "'a::{ring_char_0,division_by_zero,field} list"
   3.326 +            {fix bs:: "'a::{field, division_ring_inverse_zero, ring_char_0} list"
   3.327                
   3.328              from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
   3.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
   3.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"
   3.331 -              by (simp add: ring_simps power_Suc)
   3.332 +              by (simp add: field_simps power_Suc)
   3.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"
   3.334                by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
   3.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"
   3.336 -              by (simp add: ring_simps)}
   3.337 -            hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   3.338 +              by (simp add: field_simps)}
   3.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) = 
   3.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 
   3.341              let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
   3.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]]
   3.343 @@ -1532,17 +1532,17 @@
   3.344              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   3.345            have dom: ?dths using sz ba dn' domsp 
   3.346              by - (rule polydivide_aux_real_domintros, simp_all)
   3.347 -          {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
   3.348 +          {fix bs :: "'a::{field, division_ring_inverse_zero, ring_char_0} list"
   3.349              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
   3.350            have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
   3.351            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" 
   3.352              by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
   3.353            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
   3.354          }
   3.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))" ..
   3.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))" ..
   3.357            from hth
   3.358            have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" 
   3.359 -            using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
   3.360 +            using isnpolyh_unique[where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
   3.361                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
   3.362                simplified ap] by simp
   3.363            {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
   3.364 @@ -1566,7 +1566,7 @@
   3.365  qed
   3.366  
   3.367  lemma polydivide_properties: 
   3.368 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.369 +  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.370    and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \<noteq> 0\<^sub>p"
   3.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) 
   3.372    \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
   3.373 @@ -1698,11 +1698,11 @@
   3.374  definition "swapnorm n m t = polynate (swap n m t)"
   3.375  
   3.376  lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
   3.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"
   3.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"
   3.379    using swap[OF prems] swapnorm_def by simp
   3.380  
   3.381  lemma swapnorm_isnpoly[simp]: 
   3.382 -    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   3.383 +    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   3.384    shows "isnpoly (swapnorm n m p)"
   3.385    unfolding swapnorm_def by simp
   3.386  
     4.1 --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Mon Apr 26 11:34:15 2010 +0200
     4.2 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Mon Apr 26 11:34:17 2010 +0200
     4.3 @@ -7,147 +7,147 @@
     4.4  begin
     4.5  
     4.6  lemma
     4.7 -  "\<exists>(y::'a::{linordered_field,number_ring, division_by_zero}) <2. x + 3* y < 0 \<and> x - y >0"
     4.8 +  "\<exists>(y::'a::{linordered_field, division_ring_inverse_zero, number_ring}) <2. x + 3* y < 0 \<and> x - y >0"
     4.9    by ferrack
    4.10  
    4.11 -lemma "~ (ALL x (y::'a::{linordered_field,number_ring, division_by_zero}). x < y --> 10*x < 11*y)"
    4.12 +lemma "~ (ALL x (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}). x < y --> 10*x < 11*y)"
    4.13    by ferrack
    4.14  
    4.15 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
    4.16 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
    4.17    by ferrack
    4.18  
    4.19 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y. x ~= y --> x < y"
    4.20 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x ~= y --> x < y"
    4.21    by ferrack
    4.22  
    4.23 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
    4.24 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
    4.25    by ferrack
    4.26  
    4.27 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
    4.28 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
    4.29    by ferrack
    4.30  
    4.31 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX (y::'a::{linordered_field,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
    4.32 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
    4.33    by ferrack
    4.34  
    4.35 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) < 0. (EX (y::'a::{linordered_field,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)"
    4.36 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) < 0. (EX (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}) > 0. 7*x + y > 0 & x - y <= 9)"
    4.37    by ferrack
    4.38  
    4.39 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
    4.40 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
    4.41    by ferrack
    4.42  
    4.43 -lemma "EX x. (ALL (y::'a::{linordered_field,number_ring, division_by_zero}). y < 2 -->  2*(y - x) \<le> 0 )"
    4.44 +lemma "EX x. (ALL (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y < 2 -->  2*(y - x) \<le> 0 )"
    4.45    by ferrack
    4.46  
    4.47 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
    4.48 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
    4.49    by ferrack
    4.50  
    4.51 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0"
    4.52 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. x + y < z --> y >= z --> x < 0"
    4.53    by ferrack
    4.54  
    4.55 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
    4.56 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
    4.57    by ferrack
    4.58  
    4.59 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)"
    4.60 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. abs (x + y) <= z --> (abs z = z)"
    4.61    by ferrack
    4.62  
    4.63 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
    4.64 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
    4.65    by ferrack
    4.66  
    4.67 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
    4.68 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
    4.69    by ferrack
    4.70  
    4.71 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
    4.72 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)"
    4.73    by ferrack
    4.74  
    4.75 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)"
    4.76 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)"
    4.77    by ferrack
    4.78  
    4.79 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )"
    4.80 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX z>0. abs (x - y) <= z )"
    4.81    by ferrack
    4.82  
    4.83 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    4.84 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    4.85    by ferrack
    4.86  
    4.87 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
    4.88 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
    4.89    by ferrack
    4.90  
    4.91 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    4.92 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    4.93    by ferrack
    4.94  
    4.95 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
    4.96 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
    4.97    by ferrack
    4.98  
    4.99 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
   4.100 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
   4.101    by ferrack
   4.102  
   4.103 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
   4.104 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
   4.105    by ferrack
   4.106  
   4.107 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
   4.108 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
   4.109    by ferrack
   4.110  
   4.111 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
   4.112 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
   4.113    by ferrack
   4.114  
   4.115 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
   4.116 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
   4.117    by ferrack
   4.118  
   4.119 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
   4.120 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
   4.121    by ferrack
   4.122  
   4.123 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
   4.124 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
   4.125    by ferrack
   4.126  
   4.127 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   4.128 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   4.129    by ferrack
   4.130  
   4.131 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
   4.132 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
   4.133    by ferrack
   4.134  
   4.135 -lemma "~(ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
   4.136 +lemma "~(ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
   4.137    by ferrack
   4.138  
   4.139 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
   4.140 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
   4.141    by ferrack
   4.142  
   4.143 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
   4.144 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
   4.145    by ferrack
   4.146  
   4.147 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
   4.148 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
   4.149    by ferrack
   4.150  
   4.151 -lemma "EX z. (ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
   4.152 +lemma "EX z. (ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
   4.153    by ferrack
   4.154  
   4.155 -lemma "EX z. (ALL (x::'a::{linordered_field,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
   4.156 +lemma "EX z. (ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
   4.157    by ferrack
   4.158  
   4.159 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
   4.160 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
   4.161    by ferrack
   4.162  
   4.163 -lemma "EX y. (ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
   4.164 +lemma "EX y. (ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
   4.165    by ferrack
   4.166  
   4.167 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
   4.168 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
   4.169    by ferrack
   4.170  
   4.171 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y).
   4.172 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (ALL y < x. (EX z > (x+y).
   4.173    (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))"
   4.174    by ferrack
   4.175  
   4.176 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}). (ALL y. (EX z > y.
   4.177 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (ALL y. (EX z > y.
   4.178    (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))"
   4.179    by ferrack
   4.180  
   4.181 -lemma "EX (x::'a::{linordered_field,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   4.182 +lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   4.183    by ferrack
   4.184  
   4.185 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
   4.186 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
   4.187    by ferrack
   4.188  
   4.189 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
   4.190 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
   4.191    by ferrack
   4.192  
   4.193 -lemma "ALL (x::'a::{linordered_field,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
   4.194 +lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
   4.195    by ferrack
   4.196  
   4.197  end
     5.1 --- a/src/HOL/Groebner_Basis.thy	Mon Apr 26 11:34:15 2010 +0200
     5.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Apr 26 11:34:17 2010 +0200
     5.3 @@ -474,20 +474,20 @@
     5.4    fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
     5.5  
     5.6  lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
     5.7 -lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
     5.8 +lemma divide_Numeral0: "(x::'a::{field,number_ring, division_ring_inverse_zero}) / Numeral0 = 0"
     5.9    by simp
    5.10 -lemma mult_frac_frac: "((x::'a::{field,division_by_zero}) / y) * (z / w) = (x*z) / (y*w)"
    5.11 +lemma mult_frac_frac: "((x::'a::{field,division_ring_inverse_zero}) / y) * (z / w) = (x*z) / (y*w)"
    5.12    by simp
    5.13 -lemma mult_frac_num: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
    5.14 +lemma mult_frac_num: "((x::'a::{field, division_ring_inverse_zero}) / y) * z  = (x*z) / y"
    5.15    by simp
    5.16 -lemma mult_num_frac: "((x::'a::{field, division_by_zero}) / y) * z  = (x*z) / y"
    5.17 +lemma mult_num_frac: "((x::'a::{field, division_ring_inverse_zero}) / y) * z  = (x*z) / y"
    5.18    by simp
    5.19  
    5.20  lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
    5.21  
    5.22 -lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_by_zero}) / y + z = (x + z*y) / y"
    5.23 +lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_ring_inverse_zero}) / y + z = (x + z*y) / y"
    5.24    by (simp add: add_divide_distrib)
    5.25 -lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
    5.26 +lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_ring_inverse_zero}) / y = (x + z*y) / y"
    5.27    by (simp add: add_divide_distrib)
    5.28  
    5.29  ML {*
     6.1 --- a/src/HOL/Import/HOL/real.imp	Mon Apr 26 11:34:15 2010 +0200
     6.2 +++ b/src/HOL/Import/HOL/real.imp	Mon Apr 26 11:34:17 2010 +0200
     6.3 @@ -251,7 +251,7 @@
     6.4    "REAL_INV_INV" > "Rings.inverse_inverse_eq"
     6.5    "REAL_INV_EQ_0" > "Rings.inverse_nonzero_iff_nonzero"
     6.6    "REAL_INV_1OVER" > "Rings.inverse_eq_divide"
     6.7 -  "REAL_INV_0" > "Rings.division_by_zero_class.inverse_zero"
     6.8 +  "REAL_INV_0" > "Rings.division_ring_inverse_zero_class.inverse_zero"
     6.9    "REAL_INVINV" > "Rings.nonzero_inverse_inverse_eq"
    6.10    "REAL_INV1" > "Rings.inverse_1"
    6.11    "REAL_INJ" > "RealDef.real_of_nat_inject"
     7.1 --- a/src/HOL/Import/HOL/realax.imp	Mon Apr 26 11:34:15 2010 +0200
     7.2 +++ b/src/HOL/Import/HOL/realax.imp	Mon Apr 26 11:34:17 2010 +0200
     7.3 @@ -101,7 +101,7 @@
     7.4    "REAL_LT_MUL" > "Rings.mult_pos_pos"
     7.5    "REAL_LT_IADD" > "Groups.add_strict_left_mono"
     7.6    "REAL_LDISTRIB" > "Rings.ring_eq_simps_2"
     7.7 -  "REAL_INV_0" > "Rings.division_by_zero_class.inverse_zero"
     7.8 +  "REAL_INV_0" > "Rings.division_ring_inverse_zero_class.inverse_zero"
     7.9    "REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
    7.10    "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
    7.11    "REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident"
     8.1 --- a/src/HOL/Int.thy	Mon Apr 26 11:34:15 2010 +0200
     8.2 +++ b/src/HOL/Int.thy	Mon Apr 26 11:34:17 2010 +0200
     8.3 @@ -1995,15 +1995,15 @@
     8.4  text{*Division By @{text "-1"}*}
     8.5  
     8.6  lemma divide_minus1 [simp]:
     8.7 -     "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
     8.8 +     "x/-1 = -(x::'a::{field,division_ring_inverse_zero,number_ring})"
     8.9  by simp
    8.10  
    8.11  lemma minus1_divide [simp]:
    8.12 -     "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
    8.13 +     "-1 / (x::'a::{field,division_ring_inverse_zero,number_ring}) = - (1/x)"
    8.14  by (simp add: divide_inverse)
    8.15  
    8.16  lemma half_gt_zero_iff:
    8.17 -     "(0 < r/2) = (0 < (r::'a::{linordered_field,division_by_zero,number_ring}))"
    8.18 +     "(0 < r/2) = (0 < (r::'a::{linordered_field,division_ring_inverse_zero,number_ring}))"
    8.19  by auto
    8.20  
    8.21  lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
     9.1 --- a/src/HOL/Library/Abstract_Rat.thy	Mon Apr 26 11:34:15 2010 +0200
     9.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Mon Apr 26 11:34:17 2010 +0200
     9.3 @@ -184,7 +184,7 @@
     9.4  
     9.5  lemma isnormNum_unique[simp]: 
     9.6    assumes na: "isnormNum x" and nb: "isnormNum y" 
     9.7 -  shows "((INum x ::'a::{ring_char_0,field, division_by_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
     9.8 +  shows "((INum x ::'a::{ring_char_0,field, division_ring_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
     9.9  proof
    9.10    have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
    9.11    then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
    9.12 @@ -217,7 +217,7 @@
    9.13  qed
    9.14  
    9.15  
    9.16 -lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{ring_char_0, field,division_by_zero})) = (x = 0\<^sub>N)"
    9.17 +lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{ring_char_0, field,division_ring_inverse_zero})) = (x = 0\<^sub>N)"
    9.18    unfolding INum_int(2)[symmetric]
    9.19    by (rule isnormNum_unique, simp_all)
    9.20  
    9.21 @@ -245,7 +245,7 @@
    9.22  done
    9.23  
    9.24  
    9.25 -lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{ring_char_0,field, division_by_zero})"
    9.26 +lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{ring_char_0,field, division_ring_inverse_zero})"
    9.27  proof-
    9.28    have "\<exists> a b. x = (a,b)" by auto
    9.29    then obtain a b where x[simp]: "x = (a,b)" by blast
    9.30 @@ -260,7 +260,7 @@
    9.31    ultimately show ?thesis by blast
    9.32  qed
    9.33  
    9.34 -lemma INum_normNum_iff: "(INum x ::'a::{field, division_by_zero, ring_char_0}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
    9.35 +lemma INum_normNum_iff: "(INum x ::'a::{field, division_ring_inverse_zero, ring_char_0}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
    9.36  proof -
    9.37    have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
    9.38      by (simp del: normNum)
    9.39 @@ -268,7 +268,7 @@
    9.40    finally show ?thesis by simp
    9.41  qed
    9.42  
    9.43 -lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {ring_char_0,division_by_zero,field})"
    9.44 +lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {ring_char_0,division_ring_inverse_zero,field})"
    9.45  proof-
    9.46  let ?z = "0:: 'a"
    9.47    have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
    9.48 @@ -300,7 +300,7 @@
    9.49    ultimately show ?thesis by blast
    9.50  qed
    9.51  
    9.52 -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {ring_char_0,division_by_zero,field}) "
    9.53 +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {ring_char_0,division_ring_inverse_zero,field}) "
    9.54  proof-
    9.55    let ?z = "0::'a"
    9.56    have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
    9.57 @@ -323,16 +323,16 @@
    9.58  lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
    9.59    by (simp add: Nneg_def split_def INum_def)
    9.60  
    9.61 -lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {ring_char_0,division_by_zero,field})"
    9.62 +lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {ring_char_0,division_ring_inverse_zero,field})"
    9.63  by (simp add: Nsub_def split_def)
    9.64  
    9.65 -lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: {division_by_zero,field}) / (INum x)"
    9.66 +lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: {division_ring_inverse_zero,field}) / (INum x)"
    9.67    by (simp add: Ninv_def INum_def split_def)
    9.68  
    9.69 -lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {ring_char_0, division_by_zero,field})" by (simp add: Ndiv_def)
    9.70 +lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {ring_char_0, division_ring_inverse_zero,field})" by (simp add: Ndiv_def)
    9.71  
    9.72  lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" 
    9.73 -  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field})< 0) = 0>\<^sub>N x "
    9.74 +  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})< 0) = 0>\<^sub>N x "
    9.75  proof-
    9.76    have " \<exists> a b. x = (a,b)" by simp
    9.77    then obtain a b where x[simp]:"x = (a,b)" by blast
    9.78 @@ -345,7 +345,7 @@
    9.79  qed
    9.80  
    9.81  lemma Nle0_iff[simp]:assumes nx: "isnormNum x" 
    9.82 -  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) \<le> 0) = 0\<ge>\<^sub>N x"
    9.83 +  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \<le> 0) = 0\<ge>\<^sub>N x"
    9.84  proof-
    9.85    have " \<exists> a b. x = (a,b)" by simp
    9.86    then obtain a b where x[simp]:"x = (a,b)" by blast
    9.87 @@ -357,7 +357,7 @@
    9.88    ultimately show ?thesis by blast
    9.89  qed
    9.90  
    9.91 -lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field})> 0) = 0<\<^sub>N x"
    9.92 +lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})> 0) = 0<\<^sub>N x"
    9.93  proof-
    9.94    have " \<exists> a b. x = (a,b)" by simp
    9.95    then obtain a b where x[simp]:"x = (a,b)" by blast
    9.96 @@ -369,7 +369,7 @@
    9.97    ultimately show ?thesis by blast
    9.98  qed
    9.99  lemma Nge0_iff[simp]:assumes nx: "isnormNum x" 
   9.100 -  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x"
   9.101 +  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x"
   9.102  proof-
   9.103    have " \<exists> a b. x = (a,b)" by simp
   9.104    then obtain a b where x[simp]:"x = (a,b)" by blast
   9.105 @@ -382,7 +382,7 @@
   9.106  qed
   9.107  
   9.108  lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   9.109 -  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) < INum y) = (x <\<^sub>N y)"
   9.110 +  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) < INum y) = (x <\<^sub>N y)"
   9.111  proof-
   9.112    let ?z = "0::'a"
   9.113    have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp
   9.114 @@ -391,7 +391,7 @@
   9.115  qed
   9.116  
   9.117  lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   9.118 -  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)"
   9.119 +  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)"
   9.120  proof-
   9.121    have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" using nx ny by simp
   9.122    also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
   9.123 @@ -399,7 +399,7 @@
   9.124  qed
   9.125  
   9.126  lemma Nadd_commute:
   9.127 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   9.128 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.129    shows "x +\<^sub>N y = y +\<^sub>N x"
   9.130  proof-
   9.131    have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
   9.132 @@ -408,7 +408,7 @@
   9.133  qed
   9.134  
   9.135  lemma [simp]:
   9.136 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   9.137 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.138    shows "(0, b) +\<^sub>N y = normNum y"
   9.139      and "(a, 0) +\<^sub>N y = normNum y" 
   9.140      and "x +\<^sub>N (0, b) = normNum x"
   9.141 @@ -420,7 +420,7 @@
   9.142    done
   9.143  
   9.144  lemma normNum_nilpotent_aux[simp]:
   9.145 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   9.146 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.147    assumes nx: "isnormNum x" 
   9.148    shows "normNum x = x"
   9.149  proof-
   9.150 @@ -432,7 +432,7 @@
   9.151  qed
   9.152  
   9.153  lemma normNum_nilpotent[simp]:
   9.154 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   9.155 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.156    shows "normNum (normNum x) = normNum x"
   9.157    by simp
   9.158  
   9.159 @@ -440,11 +440,11 @@
   9.160    by (simp_all add: normNum_def)
   9.161  
   9.162  lemma normNum_Nadd:
   9.163 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   9.164 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.165    shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
   9.166  
   9.167  lemma Nadd_normNum1[simp]:
   9.168 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   9.169 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.170    shows "normNum x +\<^sub>N y = x +\<^sub>N y"
   9.171  proof-
   9.172    have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
   9.173 @@ -454,7 +454,7 @@
   9.174  qed
   9.175  
   9.176  lemma Nadd_normNum2[simp]:
   9.177 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   9.178 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.179    shows "x +\<^sub>N normNum y = x +\<^sub>N y"
   9.180  proof-
   9.181    have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
   9.182 @@ -464,7 +464,7 @@
   9.183  qed
   9.184  
   9.185  lemma Nadd_assoc:
   9.186 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   9.187 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.188    shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
   9.189  proof-
   9.190    have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
   9.191 @@ -476,7 +476,7 @@
   9.192    by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute)
   9.193  
   9.194  lemma Nmul_assoc:
   9.195 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   9.196 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.197    assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
   9.198    shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
   9.199  proof-
   9.200 @@ -487,7 +487,7 @@
   9.201  qed
   9.202  
   9.203  lemma Nsub0:
   9.204 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   9.205 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.206    assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
   9.207  proof-
   9.208    { fix h :: 'a
   9.209 @@ -502,7 +502,7 @@
   9.210    by (simp_all add: Nmul_def Let_def split_def)
   9.211  
   9.212  lemma Nmul_eq0[simp]:
   9.213 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   9.214 +  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.215    assumes nx:"isnormNum x" and ny: "isnormNum y"
   9.216    shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
   9.217  proof-
    10.1 --- a/src/HOL/Library/Bit.thy	Mon Apr 26 11:34:15 2010 +0200
    10.2 +++ b/src/HOL/Library/Bit.thy	Mon Apr 26 11:34:17 2010 +0200
    10.3 @@ -49,7 +49,7 @@
    10.4  
    10.5  subsection {* Type @{typ bit} forms a field *}
    10.6  
    10.7 -instantiation bit :: "{field, division_by_zero}"
    10.8 +instantiation bit :: "{field, division_ring_inverse_zero}"
    10.9  begin
   10.10  
   10.11  definition plus_bit_def:
    11.1 --- a/src/HOL/NSA/NSA.thy	Mon Apr 26 11:34:15 2010 +0200
    11.2 +++ b/src/HOL/NSA/NSA.thy	Mon Apr 26 11:34:17 2010 +0200
    11.3 @@ -145,12 +145,12 @@
    11.4  by transfer (rule nonzero_norm_inverse)
    11.5  
    11.6  lemma hnorm_inverse:
    11.7 -  "\<And>a::'a::{real_normed_div_algebra,division_by_zero} star.
    11.8 +  "\<And>a::'a::{real_normed_div_algebra,division_ring_inverse_zero} star.
    11.9     hnorm (inverse a) = inverse (hnorm a)"
   11.10  by transfer (rule norm_inverse)
   11.11  
   11.12  lemma hnorm_divide:
   11.13 -  "\<And>a b::'a::{real_normed_field,division_by_zero} star.
   11.14 +  "\<And>a b::'a::{real_normed_field,division_ring_inverse_zero} star.
   11.15     hnorm (a / b) = hnorm a / hnorm b"
   11.16  by transfer (rule norm_divide)
   11.17  
    12.1 --- a/src/HOL/NSA/StarDef.thy	Mon Apr 26 11:34:15 2010 +0200
    12.2 +++ b/src/HOL/NSA/StarDef.thy	Mon Apr 26 11:34:17 2010 +0200
    12.3 @@ -902,7 +902,7 @@
    12.4  apply (transfer, rule divide_inverse)
    12.5  done
    12.6  
    12.7 -instance star :: (division_by_zero) division_by_zero
    12.8 +instance star :: (division_ring_inverse_zero) division_ring_inverse_zero
    12.9  by (intro_classes, transfer, rule inverse_zero)
   12.10  
   12.11  instance star :: (ordered_semiring) ordered_semiring
    13.1 --- a/src/HOL/Power.thy	Mon Apr 26 11:34:15 2010 +0200
    13.2 +++ b/src/HOL/Power.thy	Mon Apr 26 11:34:17 2010 +0200
    13.3 @@ -400,7 +400,7 @@
    13.4  
    13.5  text{*Perhaps these should be simprules.*}
    13.6  lemma power_inverse:
    13.7 -  fixes a :: "'a::{division_ring,division_by_zero,power}"
    13.8 +  fixes a :: "'a::{division_ring,division_ring_inverse_zero,power}"
    13.9    shows "inverse (a ^ n) = (inverse a) ^ n"
   13.10  apply (cases "a = 0")
   13.11  apply (simp add: power_0_left)
   13.12 @@ -408,11 +408,11 @@
   13.13  done (* TODO: reorient or rename to inverse_power *)
   13.14  
   13.15  lemma power_one_over:
   13.16 -  "1 / (a::'a::{field,division_by_zero, power}) ^ n =  (1 / a) ^ n"
   13.17 +  "1 / (a::'a::{field,division_ring_inverse_zero, power}) ^ n =  (1 / a) ^ n"
   13.18    by (simp add: divide_inverse) (rule power_inverse)
   13.19  
   13.20  lemma power_divide:
   13.21 -  "(a / b) ^ n = (a::'a::{field,division_by_zero}) ^ n / b ^ n"
   13.22 +  "(a / b) ^ n = (a::'a::{field,division_ring_inverse_zero}) ^ n / b ^ n"
   13.23  apply (cases "b = 0")
   13.24  apply (simp add: power_0_left)
   13.25  apply (rule nonzero_power_divide)
    14.1 --- a/src/HOL/Rat.thy	Mon Apr 26 11:34:15 2010 +0200
    14.2 +++ b/src/HOL/Rat.thy	Mon Apr 26 11:34:17 2010 +0200
    14.3 @@ -444,7 +444,7 @@
    14.4  
    14.5  end
    14.6  
    14.7 -instance rat :: division_by_zero proof
    14.8 +instance rat :: division_ring_inverse_zero proof
    14.9  qed (simp add: rat_number_expand, simp add: rat_number_collapse)
   14.10  
   14.11  
   14.12 @@ -818,7 +818,7 @@
   14.13  done
   14.14  
   14.15  lemma of_rat_inverse:
   14.16 -  "(of_rat (inverse a)::'a::{field_char_0,division_by_zero}) =
   14.17 +  "(of_rat (inverse a)::'a::{field_char_0,division_ring_inverse_zero}) =
   14.18     inverse (of_rat a)"
   14.19  by (cases "a = 0", simp_all add: nonzero_of_rat_inverse)
   14.20  
   14.21 @@ -827,7 +827,7 @@
   14.22  by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse)
   14.23  
   14.24  lemma of_rat_divide:
   14.25 -  "(of_rat (a / b)::'a::{field_char_0,division_by_zero})
   14.26 +  "(of_rat (a / b)::'a::{field_char_0,division_ring_inverse_zero})
   14.27     = of_rat a / of_rat b"
   14.28  by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
   14.29  
   14.30 @@ -968,7 +968,7 @@
   14.31  done
   14.32  
   14.33  lemma Rats_inverse [simp]:
   14.34 -  fixes a :: "'a::{field_char_0,division_by_zero}"
   14.35 +  fixes a :: "'a::{field_char_0,division_ring_inverse_zero}"
   14.36    shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
   14.37  apply (auto simp add: Rats_def)
   14.38  apply (rule range_eqI)
   14.39 @@ -984,7 +984,7 @@
   14.40  done
   14.41  
   14.42  lemma Rats_divide [simp]:
   14.43 -  fixes a b :: "'a::{field_char_0,division_by_zero}"
   14.44 +  fixes a b :: "'a::{field_char_0,division_ring_inverse_zero}"
   14.45    shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
   14.46  apply (auto simp add: Rats_def)
   14.47  apply (rule range_eqI)
    15.1 --- a/src/HOL/RealDef.thy	Mon Apr 26 11:34:15 2010 +0200
    15.2 +++ b/src/HOL/RealDef.thy	Mon Apr 26 11:34:17 2010 +0200
    15.3 @@ -279,7 +279,7 @@
    15.4  lemma INVERSE_ZERO: "inverse 0 = (0::real)"
    15.5  by (simp add: real_inverse_def)
    15.6  
    15.7 -instance real :: division_by_zero
    15.8 +instance real :: division_ring_inverse_zero
    15.9  proof
   15.10    show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
   15.11  qed
    16.1 --- a/src/HOL/RealVector.thy	Mon Apr 26 11:34:15 2010 +0200
    16.2 +++ b/src/HOL/RealVector.thy	Mon Apr 26 11:34:17 2010 +0200
    16.3 @@ -207,7 +207,7 @@
    16.4  by (rule inverse_unique, simp)
    16.5  
    16.6  lemma inverse_scaleR_distrib:
    16.7 -  fixes x :: "'a::{real_div_algebra,division_by_zero}"
    16.8 +  fixes x :: "'a::{real_div_algebra,division_ring_inverse_zero}"
    16.9    shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
   16.10  apply (case_tac "a = 0", simp)
   16.11  apply (case_tac "x = 0", simp)
   16.12 @@ -250,7 +250,7 @@
   16.13  
   16.14  lemma of_real_inverse [simp]:
   16.15    "of_real (inverse x) =
   16.16 -   inverse (of_real x :: 'a::{real_div_algebra,division_by_zero})"
   16.17 +   inverse (of_real x :: 'a::{real_div_algebra,division_ring_inverse_zero})"
   16.18  by (simp add: of_real_def inverse_scaleR_distrib)
   16.19  
   16.20  lemma nonzero_of_real_divide:
   16.21 @@ -260,7 +260,7 @@
   16.22  
   16.23  lemma of_real_divide [simp]:
   16.24    "of_real (x / y) =
   16.25 -   (of_real x / of_real y :: 'a::{real_field,division_by_zero})"
   16.26 +   (of_real x / of_real y :: 'a::{real_field,division_ring_inverse_zero})"
   16.27  by (simp add: divide_inverse)
   16.28  
   16.29  lemma of_real_power [simp]:
   16.30 @@ -370,7 +370,7 @@
   16.31  done
   16.32  
   16.33  lemma Reals_inverse [simp]:
   16.34 -  fixes a :: "'a::{real_div_algebra,division_by_zero}"
   16.35 +  fixes a :: "'a::{real_div_algebra,division_ring_inverse_zero}"
   16.36    shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
   16.37  apply (auto simp add: Reals_def)
   16.38  apply (rule range_eqI)
   16.39 @@ -386,7 +386,7 @@
   16.40  done
   16.41  
   16.42  lemma Reals_divide [simp]:
   16.43 -  fixes a b :: "'a::{real_field,division_by_zero}"
   16.44 +  fixes a b :: "'a::{real_field,division_ring_inverse_zero}"
   16.45    shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
   16.46  apply (auto simp add: Reals_def)
   16.47  apply (rule range_eqI)
   16.48 @@ -726,7 +726,7 @@
   16.49  done
   16.50  
   16.51  lemma norm_inverse:
   16.52 -  fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
   16.53 +  fixes a :: "'a::{real_normed_div_algebra,division_ring_inverse_zero}"
   16.54    shows "norm (inverse a) = inverse (norm a)"
   16.55  apply (case_tac "a = 0", simp)
   16.56  apply (erule nonzero_norm_inverse)
   16.57 @@ -738,7 +738,7 @@
   16.58  by (simp add: divide_inverse norm_mult nonzero_norm_inverse)
   16.59  
   16.60  lemma norm_divide:
   16.61 -  fixes a b :: "'a::{real_normed_field,division_by_zero}"
   16.62 +  fixes a b :: "'a::{real_normed_field,division_ring_inverse_zero}"
   16.63    shows "norm (a / b) = norm a / norm b"
   16.64  by (simp add: divide_inverse norm_mult norm_inverse)
   16.65  
    17.1 --- a/src/HOL/Series.thy	Mon Apr 26 11:34:15 2010 +0200
    17.2 +++ b/src/HOL/Series.thy	Mon Apr 26 11:34:17 2010 +0200
    17.3 @@ -381,7 +381,7 @@
    17.4    shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
    17.5  by (rule geometric_sums [THEN sums_summable])
    17.6  
    17.7 -lemma half: "0 < 1 / (2::'a::{number_ring,division_by_zero,linordered_field})"
    17.8 +lemma half: "0 < 1 / (2::'a::{number_ring,division_ring_inverse_zero,linordered_field})"
    17.9    by arith 
   17.10  
   17.11  lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
    18.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Mon Apr 26 11:34:15 2010 +0200
    18.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Apr 26 11:34:17 2010 +0200
    18.3 @@ -332,8 +332,8 @@
    18.4  val field_combine_numerals =
    18.5    Arith_Data.prep_simproc @{theory}
    18.6      ("field_combine_numerals", 
    18.7 -     ["(i::'a::{number_ring,field,division_by_zero}) + j",
    18.8 -      "(i::'a::{number_ring,field,division_by_zero}) - j"], 
    18.9 +     ["(i::'a::{number_ring,field,division_ring_inverse_zero}) + j",
   18.10 +      "(i::'a::{number_ring,field,division_ring_inverse_zero}) - j"], 
   18.11       K FieldCombineNumerals.proc);
   18.12  
   18.13  (** Constant folding for multiplication in semirings **)
   18.14 @@ -442,9 +442,9 @@
   18.15        "(l::'a::{semiring_div,number_ring}) div (m * n)"],
   18.16       K DivCancelNumeralFactor.proc),
   18.17      ("divide_cancel_numeral_factor",
   18.18 -     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
   18.19 -      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
   18.20 -      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
   18.21 +     ["((l::'a::{division_ring_inverse_zero,field,number_ring}) * m) / n",
   18.22 +      "(l::'a::{division_ring_inverse_zero,field,number_ring}) / (m * n)",
   18.23 +      "((number_of v)::'a::{division_ring_inverse_zero,field,number_ring}) / (number_of w)"],
   18.24       K DivideCancelNumeralFactor.proc)];
   18.25  
   18.26  val field_cancel_numeral_factors =
   18.27 @@ -454,9 +454,9 @@
   18.28        "(l::'a::{field,number_ring}) = m * n"],
   18.29       K EqCancelNumeralFactor.proc),
   18.30      ("field_cancel_numeral_factor",
   18.31 -     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
   18.32 -      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
   18.33 -      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
   18.34 +     ["((l::'a::{division_ring_inverse_zero,field,number_ring}) * m) / n",
   18.35 +      "(l::'a::{division_ring_inverse_zero,field,number_ring}) / (m * n)",
   18.36 +      "((number_of v)::'a::{division_ring_inverse_zero,field,number_ring}) / (number_of w)"],
   18.37       K DivideCancelNumeralFactor.proc)]
   18.38  
   18.39  
   18.40 @@ -598,8 +598,8 @@
   18.41       ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
   18.42       K DvdCancelFactor.proc),
   18.43      ("divide_cancel_factor",
   18.44 -     ["((l::'a::{division_by_zero,field}) * m) / n",
   18.45 -      "(l::'a::{division_by_zero,field}) / (m * n)"],
   18.46 +     ["((l::'a::{division_ring_inverse_zero,field}) * m) / n",
   18.47 +      "(l::'a::{division_ring_inverse_zero,field}) / (m * n)"],
   18.48       K DivideCancelFactor.proc)];
   18.49  
   18.50  end;