use new classes (linordered_)field_inverse_zero
authorhaftmann
Mon Apr 26 15:37:50 2010 +0200 (2010-04-26)
changeset 36409d323e7773aa8
parent 36350 bc7982c54e37
child 36410 fde7b064d5b2
use new classes (linordered_)field_inverse_zero
src/HOL/Big_Operators.thy
src/HOL/Complex.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy
src/HOL/Fields.thy
src/HOL/Groebner_Basis.thy
src/HOL/Int.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/Bit.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Multivariate_Analysis/Determinants.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/NSA.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:19 2010 +0200
     1.2 +++ b/src/HOL/Big_Operators.thy	Mon Apr 26 15:37:50 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_ring_inverse_zero}"
     1.8 +  fixes f :: "'b \<Rightarrow> 'a::field_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_ring_inverse_zero}"
    1.14 +  fixes f :: "'b \<Rightarrow> 'a::field_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
     2.1 --- a/src/HOL/Complex.thy	Mon Apr 26 11:34:19 2010 +0200
     2.2 +++ b/src/HOL/Complex.thy	Mon Apr 26 15:37:50 2010 +0200
     2.3 @@ -99,7 +99,7 @@
     2.4  
     2.5  subsection {* Multiplication and Division *}
     2.6  
     2.7 -instantiation complex :: "{field, division_ring_inverse_zero}"
     2.8 +instantiation complex :: field_inverse_zero
     2.9  begin
    2.10  
    2.11  definition
     3.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Apr 26 11:34:19 2010 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Apr 26 15:37:50 2010 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4    "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
     3.5  
     3.6    (* Semantics of terms tm *)
     3.7 -consts Itm :: "'a::{ring_char_0,division_ring_inverse_zero,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
     3.8 +consts Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
     3.9  primrec
    3.10    "Itm vs bs (CP c) = (Ipoly vs c)"
    3.11    "Itm vs bs (Bound n) = bs!n"
    3.12 @@ -270,7 +270,7 @@
    3.13  by (induct t arbitrary: i rule: tmmul.induct, auto simp add: Let_def)
    3.14  
    3.15  lemma tmmul_allpolys_npoly[simp]: 
    3.16 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    3.17 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.18    shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)" by (induct t rule: tmmul.induct, simp_all add: Let_def polymul_norm)
    3.19  
    3.20  definition tmneg :: "tm \<Rightarrow> tm" where
    3.21 @@ -296,7 +296,7 @@
    3.22  using tmneg_def by simp
    3.23  lemma [simp]: "isnpoly (C (-1,1))" unfolding isnpoly_def by simp
    3.24  lemma tmneg_allpolys_npoly[simp]: 
    3.25 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    3.26 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.27    shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)" 
    3.28    unfolding tmneg_def by auto
    3.29  
    3.30 @@ -310,7 +310,7 @@
    3.31  lemma tmsub_blt[simp]: "\<lbrakk>tmboundslt n t ; tmboundslt n s\<rbrakk> \<Longrightarrow> tmboundslt n (tmsub t s )"
    3.32  using tmsub_def by simp
    3.33  lemma tmsub_allpolys_npoly[simp]: 
    3.34 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    3.35 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.36    shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)" 
    3.37    unfolding tmsub_def by (simp add: isnpoly_def)
    3.38  
    3.39 @@ -324,8 +324,8 @@
    3.40    "simptm (CNP n c t) = (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"
    3.41  
    3.42  lemma polynate_stupid: 
    3.43 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    3.44 -  shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{ring_char_0,division_ring_inverse_zero, field})" 
    3.45 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.46 +  shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{field_char_0, field_inverse_zero})" 
    3.47  apply (subst polynate[symmetric])
    3.48  apply simp
    3.49  done
    3.50 @@ -345,7 +345,7 @@
    3.51  lemma [simp]: "isnpoly 0\<^sub>p" and [simp]: "isnpoly (C(1,1))" 
    3.52    by (simp_all add: isnpoly_def)
    3.53  lemma simptm_allpolys_npoly[simp]: 
    3.54 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    3.55 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.56    shows "allpolys isnpoly (simptm p)"
    3.57    by (induct p rule: simptm.induct, auto simp add: Let_def)
    3.58  
    3.59 @@ -387,7 +387,7 @@
    3.60  qed
    3.61  
    3.62  lemma split0_nb0: 
    3.63 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    3.64 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.65    shows "split0 t = (c',t') \<Longrightarrow>  tmbound 0 t'"
    3.66  proof-
    3.67    fix c' t'
    3.68 @@ -395,7 +395,7 @@
    3.69    with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'" by simp
    3.70  qed
    3.71  
    3.72 -lemma split0_nb0'[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    3.73 +lemma split0_nb0'[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.74    shows "tmbound0 (snd (split0 t))"
    3.75    using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"] by (simp add: tmbound0_tmbound_iff)
    3.76  
    3.77 @@ -418,7 +418,7 @@
    3.78  lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))"
    3.79  by (induct p rule: split0.induct, auto simp  add: isnpoly_def Let_def split_def split0_stupid)
    3.80  
    3.81 -lemma isnpoly_fst_split0:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    3.82 +lemma isnpoly_fst_split0:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    3.83    shows 
    3.84    "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
    3.85    by (induct p rule: split0.induct, 
    3.86 @@ -447,7 +447,7 @@
    3.87  by (induct p rule: fmsize.induct) simp_all
    3.88  
    3.89    (* Semantics of formulae (fm) *)
    3.90 -consts Ifm ::"'a::{division_ring_inverse_zero,linordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
    3.91 +consts Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
    3.92  primrec
    3.93    "Ifm vs bs T = True"
    3.94    "Ifm vs bs F = False"
    3.95 @@ -969,24 +969,24 @@
    3.96  definition "simpeq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then eq s else Eq (CNP 0 c s))"
    3.97  definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))"
    3.98  
    3.99 -lemma simplt_islin[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.100 +lemma simplt_islin[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.101    shows "islin (simplt t)"
   3.102    unfolding simplt_def 
   3.103    using split0_nb0'
   3.104  by (auto simp add: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly])
   3.105    
   3.106 -lemma simple_islin[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.107 +lemma simple_islin[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.108    shows "islin (simple t)"
   3.109    unfolding simple_def 
   3.110    using split0_nb0'
   3.111  by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)
   3.112 -lemma simpeq_islin[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.113 +lemma simpeq_islin[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.114    shows "islin (simpeq t)"
   3.115    unfolding simpeq_def 
   3.116    using split0_nb0'
   3.117  by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)
   3.118  
   3.119 -lemma simpneq_islin[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.120 +lemma simpneq_islin[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.121    shows "islin (simpneq t)"
   3.122    unfolding simpneq_def 
   3.123    using split0_nb0'
   3.124 @@ -994,7 +994,7 @@
   3.125  
   3.126  lemma really_stupid: "\<not> (\<forall>c1 s'. (c1, s') \<noteq> split0 s)"
   3.127    by (cases "split0 s", auto)
   3.128 -lemma split0_npoly:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.129 +lemma split0_npoly:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.130    and n: "allpolys isnpoly t"
   3.131    shows "isnpoly (fst (split0 t))" and "allpolys isnpoly (snd (split0 t))"
   3.132    using n
   3.133 @@ -1083,7 +1083,7 @@
   3.134    apply (case_tac poly, auto)
   3.135    done
   3.136  
   3.137 -lemma simplt_nb[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.138 +lemma simplt_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.139    shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
   3.140    using split0 [of "simptm t" vs bs]
   3.141  proof(simp add: simplt_def Let_def split_def)
   3.142 @@ -1100,7 +1100,7 @@
   3.143         fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def lt_nb)
   3.144  qed
   3.145  
   3.146 -lemma simple_nb[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.147 +lemma simple_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.148    shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
   3.149    using split0 [of "simptm t" vs bs]
   3.150  proof(simp add: simple_def Let_def split_def)
   3.151 @@ -1117,7 +1117,7 @@
   3.152         fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def le_nb)
   3.153  qed
   3.154  
   3.155 -lemma simpeq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.156 +lemma simpeq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.157    shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
   3.158    using split0 [of "simptm t" vs bs]
   3.159  proof(simp add: simpeq_def Let_def split_def)
   3.160 @@ -1134,7 +1134,7 @@
   3.161         fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simpeq_def Let_def split_def eq_nb)
   3.162  qed
   3.163  
   3.164 -lemma simpneq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.165 +lemma simpneq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.166    shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
   3.167    using split0 [of "simptm t" vs bs]
   3.168  proof(simp add: simpneq_def Let_def split_def)
   3.169 @@ -1267,7 +1267,7 @@
   3.170  lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p"
   3.171  by(induct p arbitrary: bs rule: simpfm.induct, auto)
   3.172  
   3.173 -lemma simpfm_bound0:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.174 +lemma simpfm_bound0:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.175    shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
   3.176  by (induct p rule: simpfm.induct, auto)
   3.177  
   3.178 @@ -1296,7 +1296,7 @@
   3.179  lemma disj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (disj p q)" by (simp add: disj_def)
   3.180  lemma conj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (conj p q)" by (simp add: conj_def)
   3.181  
   3.182 -lemma   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.183 +lemma   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.184    shows "qfree p \<Longrightarrow> islin (simpfm p)" 
   3.185    apply (induct p rule: simpfm.induct)
   3.186    apply (simp_all add: conj_lin disj_lin)
   3.187 @@ -2519,7 +2519,7 @@
   3.188  lemma remdps_set[simp]: "set (remdps xs) = set xs"
   3.189    by (induct xs rule: remdps.induct, auto)
   3.190  
   3.191 -lemma simpfm_lin:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   3.192 +lemma simpfm_lin:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.193    shows "qfree p \<Longrightarrow> islin (simpfm p)"
   3.194    by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)
   3.195  
   3.196 @@ -2747,12 +2747,12 @@
   3.197  using lp tnb
   3.198  by (induct p c t rule: msubstpos.induct, auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
   3.199  
   3.200 -lemma msubstneg_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t"
   3.201 +lemma msubstneg_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and lp: "islin p" and tnb: "tmbound0 t"
   3.202    shows "bound0 (msubstneg p c t)"
   3.203  using lp tnb
   3.204  by (induct p c t rule: msubstneg.induct, auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
   3.205  
   3.206 -lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t"
   3.207 +lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and lp: "islin p" and tnb: "tmbound0 t"
   3.208    shows "bound0 (msubst2 p c t)"
   3.209  using lp tnb
   3.210  by (simp add: msubst2_def msubstneg_nb msubstpos_nb conj_nb disj_nb lt_nb simpfm_bound0)
   3.211 @@ -3156,54 +3156,54 @@
   3.212  *} "Parametric QE for linear Arithmetic over fields, Version 2"
   3.213  
   3.214  
   3.215 -lemma "\<exists>(x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   3.216 -  apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "y::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   3.217 +lemma "\<exists>(x::'a::{linordered_field_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   3.218 +  apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "y::'a::{linordered_field_inverse_zero, number_ring}")
   3.219    apply (simp add: field_simps)
   3.220    apply (rule spec[where x=y])
   3.221 -  apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   3.222 +  apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "z::'a::{linordered_field_inverse_zero, number_ring}")
   3.223    by simp
   3.224  
   3.225  text{* Collins/Jones Problem *}
   3.226  (*
   3.227 -lemma "\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   3.228 +lemma "\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   3.229  proof-
   3.230 -  have "(\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   3.231 +  have "(\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   3.232  by (simp add: field_simps)
   3.233  have "?rhs"
   3.234  
   3.235 -  apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "a::'a::{linordered_field, division_ring_inverse_zero, number_ring}" "b::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   3.236 +  apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "a::'a::{linordered_field_inverse_zero, number_ring}" "b::'a::{linordered_field_inverse_zero, number_ring}")
   3.237    apply (simp add: field_simps)
   3.238  oops
   3.239  *)
   3.240  (*
   3.241 -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   3.242 -apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "t::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   3.243 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   3.244 +apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}")
   3.245  oops
   3.246  *)
   3.247  
   3.248 -lemma "\<exists>(x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   3.249 -  apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "y::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   3.250 +lemma "\<exists>(x::'a::{linordered_field_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   3.251 +  apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "y::'a::{linordered_field_inverse_zero, number_ring}")
   3.252    apply (simp add: field_simps)
   3.253    apply (rule spec[where x=y])
   3.254 -  apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   3.255 +  apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "z::'a::{linordered_field_inverse_zero, number_ring}")
   3.256    by simp
   3.257  
   3.258  text{* Collins/Jones Problem *}
   3.259  
   3.260  (*
   3.261 -lemma "\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   3.262 +lemma "\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   3.263  proof-
   3.264 -  have "(\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   3.265 +  have "(\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   3.266  by (simp add: field_simps)
   3.267  have "?rhs"
   3.268 -  apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "a::'a::{linordered_field, division_ring_inverse_zero, number_ring}" "b::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   3.269 +  apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "a::'a::{linordered_field_inverse_zero, number_ring}" "b::'a::{linordered_field_inverse_zero, number_ring}")
   3.270    apply simp
   3.271  oops
   3.272  *)
   3.273  
   3.274  (*
   3.275 -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   3.276 -apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "t::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   3.277 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   3.278 +apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}")
   3.279  apply (simp add: field_simps linorder_neq_iff[symmetric])
   3.280  apply ferrack
   3.281  oops
     4.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Apr 26 11:34:19 2010 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Apr 26 15:37:50 2010 +0200
     4.3 @@ -230,7 +230,7 @@
     4.4  
     4.5  subsection{* Semantics of the polynomial representation *}
     4.6  
     4.7 -consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{ring_char_0,power,division_ring_inverse_zero,field}"
     4.8 +consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}"
     4.9  primrec
    4.10    "Ipoly bs (C c) = INum c"
    4.11    "Ipoly bs (Bound n) = bs!n"
    4.12 @@ -241,7 +241,7 @@
    4.13    "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
    4.14    "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
    4.15  abbreviation
    4.16 -  Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_ring_inverse_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    4.17 +  Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    4.18    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
    4.19  
    4.20  lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" 
    4.21 @@ -394,7 +394,7 @@
    4.22  qed simp_all
    4.23  
    4.24  lemma polymul_properties:
    4.25 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    4.26 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    4.27    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1"
    4.28    shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" 
    4.29    and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)" 
    4.30 @@ -568,19 +568,19 @@
    4.31  by(induct p q rule: polymul.induct, auto simp add: field_simps)
    4.32  
    4.33  lemma polymul_normh: 
    4.34 -    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    4.35 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    4.36    shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
    4.37    using polymul_properties(1)  by blast
    4.38  lemma polymul_eq0_iff: 
    4.39 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    4.40 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    4.41    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p) "
    4.42    using polymul_properties(2)  by blast
    4.43  lemma polymul_degreen:  
    4.44 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    4.45 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    4.46    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 else degreen p m + degreen q m)"
    4.47    using polymul_properties(3) by blast
    4.48  lemma polymul_norm:   
    4.49 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    4.50 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    4.51    shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul (p,q))"
    4.52    using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
    4.53  
    4.54 @@ -591,7 +591,7 @@
    4.55    by (induct p arbitrary: n0, auto)
    4.56  
    4.57  lemma monic_eqI: assumes np: "isnpolyh p n0" 
    4.58 -  shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{ring_char_0,power,division_ring_inverse_zero,field})"
    4.59 +  shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
    4.60    unfolding monic_def Let_def
    4.61  proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
    4.62    let ?h = "headconst p"
    4.63 @@ -629,13 +629,13 @@
    4.64  
    4.65  lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub(p,q))"
    4.66    using polyadd_norm polyneg_norm by (simp add: polysub_def) 
    4.67 -lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    4.68 +lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    4.69    shows "isnpolyh p n0 \<Longrightarrow> polysub (p, p) = 0\<^sub>p"
    4.70  unfolding polysub_def split_def fst_conv snd_conv
    4.71  by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])
    4.72  
    4.73  lemma polysub_0: 
    4.74 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    4.75 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    4.76    shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
    4.77    unfolding polysub_def split_def fst_conv snd_conv
    4.78    apply (induct p q arbitrary: n0 n1 rule:polyadd.induct, simp_all add: Nsub0[simplified Nsub_def])
    4.79 @@ -657,7 +657,7 @@
    4.80    done
    4.81  
    4.82  text{* polypow is a power function and preserves normal forms *}
    4.83 -lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field, division_ring_inverse_zero, ring_char_0})) ^ n"
    4.84 +lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n"
    4.85  proof(induct n rule: polypow.induct)
    4.86    case 1 thus ?case by simp
    4.87  next
    4.88 @@ -688,7 +688,7 @@
    4.89  qed
    4.90  
    4.91  lemma polypow_normh: 
    4.92 -    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
    4.93 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    4.94    shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
    4.95  proof (induct k arbitrary: n rule: polypow.induct)
    4.96    case (2 k n)
    4.97 @@ -701,17 +701,17 @@
    4.98  qed auto 
    4.99  
   4.100  lemma polypow_norm:   
   4.101 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.102 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.103    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
   4.104    by (simp add: polypow_normh isnpoly_def)
   4.105  
   4.106  text{* Finally the whole normalization*}
   4.107  
   4.108 -lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field, division_ring_inverse_zero, ring_char_0})"
   4.109 +lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
   4.110  by (induct p rule:polynate.induct, auto)
   4.111  
   4.112  lemma polynate_norm[simp]: 
   4.113 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.114 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.115    shows "isnpoly (polynate p)"
   4.116    by (induct p rule: polynate.induct, simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm) (simp_all add: isnpoly_def)
   4.117  
   4.118 @@ -736,14 +736,14 @@
   4.119    shows "isnpolyh (funpow k f p) n"
   4.120    using f np by (induct k arbitrary: p, auto)
   4.121  
   4.122 -lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field, division_ring_inverse_zero, ring_char_0}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
   4.123 +lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
   4.124    by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
   4.125  
   4.126  lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
   4.127    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   4.128  
   4.129  lemma funpow_shift1_1: 
   4.130 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field, division_ring_inverse_zero, ring_char_0}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"
   4.131 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"
   4.132    by (simp add: funpow_shift1)
   4.133  
   4.134  lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
   4.135 @@ -751,7 +751,7 @@
   4.136  
   4.137  lemma behead:
   4.138    assumes np: "isnpolyh p n"
   4.139 -  shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field, division_ring_inverse_zero, ring_char_0})"
   4.140 +  shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})"
   4.141    using np
   4.142  proof (induct p arbitrary: n rule: behead.induct)
   4.143    case (1 c p n) hence pn: "isnpolyh p n" by simp
   4.144 @@ -981,7 +981,7 @@
   4.145    by (simp add: head_eq_headn0)
   4.146  
   4.147  lemma isnpolyh_zero_iff: 
   4.148 -  assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{ring_char_0,power,division_ring_inverse_zero,field})"
   4.149 +  assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, field_inverse_zero, power})"
   4.150    shows "p = 0\<^sub>p"
   4.151  using nq eq
   4.152  proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
   4.153 @@ -1033,7 +1033,7 @@
   4.154  
   4.155  lemma isnpolyh_unique:  
   4.156    assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"
   4.157 -  shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{ring_char_0,power,division_ring_inverse_zero,field})) \<longleftrightarrow>  p = q"
   4.158 +  shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0, field_inverse_zero, power})) \<longleftrightarrow>  p = q"
   4.159  proof(auto)
   4.160    assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
   4.161    hence "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp
   4.162 @@ -1046,50 +1046,50 @@
   4.163  
   4.164  text{* consequenses of unicity on the algorithms for polynomial normalization *}
   4.165  
   4.166 -lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.167 +lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.168    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
   4.169    using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
   4.170  
   4.171  lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
   4.172  lemma one_normh: "isnpolyh 1\<^sub>p n" by simp
   4.173  lemma polyadd_0[simp]: 
   4.174 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.175 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.176    and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
   4.177    using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] 
   4.178      isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
   4.179  
   4.180  lemma polymul_1[simp]: 
   4.181 -    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.182 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.183    and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
   4.184    using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 
   4.185      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
   4.186  lemma polymul_0[simp]: 
   4.187 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.188 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.189    and np: "isnpolyh p n0" shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
   4.190    using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] 
   4.191      isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
   4.192  
   4.193  lemma polymul_commute: 
   4.194 -    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.195 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.196    and np:"isnpolyh p n0" and nq: "isnpolyh q n1"
   4.197    shows "p *\<^sub>p q = q *\<^sub>p p"
   4.198 -using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{ring_char_0,power,division_ring_inverse_zero,field}"] by simp
   4.199 +using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{field_char_0, field_inverse_zero, power}"] by simp
   4.200  
   4.201  declare polyneg_polyneg[simp]
   4.202    
   4.203  lemma isnpolyh_polynate_id[simp]: 
   4.204 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.205 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.206    and np:"isnpolyh p n0" shows "polynate p = p"
   4.207 -  using isnpolyh_unique[where ?'a= "'a::{field, division_ring_inverse_zero, ring_char_0}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}"] by simp
   4.208 +  using isnpolyh_unique[where ?'a= "'a::{field_char_0, field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0, field_inverse_zero}"] by simp
   4.209  
   4.210  lemma polynate_idempotent[simp]: 
   4.211 -    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.212 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.213    shows "polynate (polynate p) = polynate p"
   4.214    using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
   4.215  
   4.216  lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
   4.217    unfolding poly_nate_def polypoly'_def ..
   4.218 -lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field, division_ring_inverse_zero, ring_char_0}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   4.219 +lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0, field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
   4.220    using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
   4.221    unfolding poly_nate_polypoly' by (auto intro: ext)
   4.222  
   4.223 @@ -1116,7 +1116,7 @@
   4.224  qed
   4.225  
   4.226  lemma degree_polysub_samehead: 
   4.227 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.228 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.229    and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" 
   4.230    and d: "degree p = degree q"
   4.231    shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
   4.232 @@ -1226,7 +1226,7 @@
   4.233  done
   4.234  
   4.235  lemma polymul_head_polyeq: 
   4.236 -   assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.237 +   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.238    shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
   4.239  proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
   4.240    case (2 a b c' n' p' n0 n1)
   4.241 @@ -1300,7 +1300,7 @@
   4.242    by (induct p arbitrary: n0 rule: polyneg.induct, auto)
   4.243  
   4.244  lemma degree_polymul:
   4.245 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.246 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.247    and np: "isnpolyh p n0" and nq: "isnpolyh q n1"
   4.248    shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
   4.249    using polymul_degreen[OF np nq, where m="0"]  degree_eq_degreen0 by simp
   4.250 @@ -1344,7 +1344,7 @@
   4.251  qed
   4.252  
   4.253  lemma polydivide_aux_properties:
   4.254 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.255 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.256    and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
   4.257    and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
   4.258    shows "polydivide_aux_dom (a,n,p,k,s) \<and> 
   4.259 @@ -1415,19 +1415,19 @@
   4.260              from polyadd_normh[OF polymul_normh[OF np 
   4.261                polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
   4.262              have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp 
   4.263 -            from asp have "\<forall> (bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = 
   4.264 +            from asp have "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = 
   4.265                Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
   4.266 -            hence " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = 
   4.267 +            hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = 
   4.268                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" 
   4.269                by (simp add: field_simps)
   4.270 -            hence " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   4.271 +            hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   4.272                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p) 
   4.273                + Ipoly bs p * Ipoly bs q + Ipoly bs r"
   4.274                by (auto simp only: funpow_shift1_1) 
   4.275 -            hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   4.276 +            hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   4.277                Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p) 
   4.278                + Ipoly bs q) + Ipoly bs r" by (simp add: field_simps)
   4.279 -            hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   4.280 +            hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   4.281                Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp
   4.282              with isnpolyh_unique[OF nakks' nqr']
   4.283              have "a ^\<^sub>p (k' - k) *\<^sub>p s = 
   4.284 @@ -1444,9 +1444,9 @@
   4.285              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   4.286            have dom: ?dths apply (rule polydivide_aux_real_domintros) 
   4.287              using ba dn' domsp by simp_all
   4.288 -          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}"]
   4.289 -          have " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs s = Ipoly bs ?p'" by simp
   4.290 -          hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
   4.291 +          from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0, field_inverse_zero}"]
   4.292 +          have " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp
   4.293 +          hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
   4.294              by (simp only: funpow_shift1_1) simp
   4.295            hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
   4.296            {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
   4.297 @@ -1501,7 +1501,7 @@
   4.298                and dr: "degree r = 0 \<or> degree r < degree p"
   4.299                and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto
   4.300              from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
   4.301 -            {fix bs:: "'a::{field, division_ring_inverse_zero, ring_char_0} list"
   4.302 +            {fix bs:: "'a::{field_char_0, field_inverse_zero} list"
   4.303                
   4.304              from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
   4.305              have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
   4.306 @@ -1511,7 +1511,7 @@
   4.307                by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
   4.308              hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
   4.309                by (simp add: field_simps)}
   4.310 -            hence ieq:"\<forall>(bs :: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   4.311 +            hence ieq:"\<forall>(bs :: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
   4.312                Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto 
   4.313              let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
   4.314              from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap ] nxdn]]
   4.315 @@ -1532,17 +1532,17 @@
   4.316              apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
   4.317            have dom: ?dths using sz ba dn' domsp 
   4.318              by - (rule polydivide_aux_real_domintros, simp_all)
   4.319 -          {fix bs :: "'a::{field, division_ring_inverse_zero, ring_char_0} list"
   4.320 +          {fix bs :: "'a::{field_char_0, field_inverse_zero} list"
   4.321              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
   4.322            have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
   4.323            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" 
   4.324              by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
   4.325            hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
   4.326          }
   4.327 -        hence hth: "\<forall> (bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
   4.328 +        hence hth: "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
   4.329            from hth
   4.330            have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" 
   4.331 -            using isnpolyh_unique[where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
   4.332 +            using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
   4.333                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
   4.334                simplified ap] by simp
   4.335            {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
   4.336 @@ -1566,7 +1566,7 @@
   4.337  qed
   4.338  
   4.339  lemma polydivide_properties: 
   4.340 -  assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.341 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.342    and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \<noteq> 0\<^sub>p"
   4.343    shows "(\<exists> k r. polydivide s p = (k,r) \<and> (\<exists>nr. isnpolyh r nr) \<and> (degree r = 0 \<or> degree r < degree p) 
   4.344    \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
   4.345 @@ -1698,11 +1698,11 @@
   4.346  definition "swapnorm n m t = polynate (swap n m t)"
   4.347  
   4.348  lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
   4.349 -  shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field, division_ring_inverse_zero, ring_char_0})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
   4.350 +  shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
   4.351    using swap[OF prems] swapnorm_def by simp
   4.352  
   4.353  lemma swapnorm_isnpoly[simp]: 
   4.354 -    assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
   4.355 +    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   4.356    shows "isnpoly (swapnorm n m p)"
   4.357    unfolding swapnorm_def by simp
   4.358  
     5.1 --- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Mon Apr 26 11:34:19 2010 +0200
     5.2 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy	Mon Apr 26 15:37:50 2010 +0200
     5.3 @@ -7,147 +7,147 @@
     5.4  begin
     5.5  
     5.6  lemma
     5.7 -  "\<exists>(y::'a::{linordered_field, division_ring_inverse_zero, number_ring}) <2. x + 3* y < 0 \<and> x - y >0"
     5.8 +  "\<exists>(y::'a::{linordered_field_inverse_zero, number_ring}) <2. x + 3* y < 0 \<and> x - y >0"
     5.9    by ferrack
    5.10  
    5.11 -lemma "~ (ALL x (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}). x < y --> 10*x < 11*y)"
    5.12 +lemma "~ (ALL x (y::'a::{linordered_field_inverse_zero, number_ring}). x < y --> 10*x < 11*y)"
    5.13    by ferrack
    5.14  
    5.15 -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
    5.16 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
    5.17    by ferrack
    5.18  
    5.19 -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x ~= y --> x < y"
    5.20 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. x ~= y --> x < y"
    5.21    by ferrack
    5.22  
    5.23 -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
    5.24 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
    5.25    by ferrack
    5.26  
    5.27 -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
    5.28 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
    5.29    by ferrack
    5.30  
    5.31 -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)"
    5.32 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX (y::'a::{linordered_field_inverse_zero, number_ring}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
    5.33    by ferrack
    5.34  
    5.35 -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)"
    5.36 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) < 0. (EX (y::'a::{linordered_field_inverse_zero, number_ring}) > 0. 7*x + y > 0 & x - y <= 9)"
    5.37    by ferrack
    5.38  
    5.39 -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
    5.40 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
    5.41    by ferrack
    5.42  
    5.43 -lemma "EX x. (ALL (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y < 2 -->  2*(y - x) \<le> 0 )"
    5.44 +lemma "EX x. (ALL (y::'a::{linordered_field_inverse_zero, number_ring}). y < 2 -->  2*(y - x) \<le> 0 )"
    5.45    by ferrack
    5.46  
    5.47 -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)"
    5.48 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
    5.49    by ferrack
    5.50  
    5.51 -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. x + y < z --> y >= z --> x < 0"
    5.52 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z. x + y < z --> y >= z --> x < 0"
    5.53    by ferrack
    5.54  
    5.55 -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"
    5.56 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
    5.57    by ferrack
    5.58  
    5.59 -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. abs (x + y) <= z --> (abs z = z)"
    5.60 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z. abs (x + y) <= z --> (abs z = z)"
    5.61    by ferrack
    5.62  
    5.63 -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"
    5.64 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
    5.65    by ferrack
    5.66  
    5.67 -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))"
    5.68 +lemma "ALL (x::'a::{linordered_field_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))"
    5.69    by ferrack
    5.70  
    5.71 -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)"
    5.72 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)"
    5.73    by ferrack
    5.74  
    5.75 -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)"
    5.76 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)"
    5.77    by ferrack
    5.78  
    5.79 -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX z>0. abs (x - y) <= z )"
    5.80 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX z>0. abs (x - y) <= z )"
    5.81    by ferrack
    5.82  
    5.83 -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    5.84 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    5.85    by ferrack
    5.86  
    5.87 -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
    5.88 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
    5.89    by ferrack
    5.90  
    5.91 -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    5.92 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    5.93    by ferrack
    5.94  
    5.95 -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))"
    5.96 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
    5.97    by ferrack
    5.98  
    5.99 -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))"
   5.100 +lemma "EX (x::'a::{linordered_field_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))"
   5.101    by ferrack
   5.102  
   5.103 -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))"
   5.104 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
   5.105    by ferrack
   5.106  
   5.107 -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) ))"
   5.108 +lemma "ALL (x::'a::{linordered_field_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) ))"
   5.109    by ferrack
   5.110  
   5.111 -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))"
   5.112 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
   5.113    by ferrack
   5.114  
   5.115 -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"
   5.116 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
   5.117    by ferrack
   5.118  
   5.119 -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"
   5.120 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
   5.121    by ferrack
   5.122  
   5.123 -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)"
   5.124 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
   5.125    by ferrack
   5.126  
   5.127 -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)"
   5.128 +lemma "EX (x::'a::{linordered_field_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)"
   5.129    by ferrack
   5.130  
   5.131 -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)"
   5.132 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
   5.133    by ferrack
   5.134  
   5.135 -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))"
   5.136 +lemma "~(ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
   5.137    by ferrack
   5.138  
   5.139 -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)"
   5.140 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
   5.141    by ferrack
   5.142  
   5.143 -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))"
   5.144 +lemma "ALL (x::'a::{linordered_field_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))"
   5.145    by ferrack
   5.146  
   5.147 -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)"
   5.148 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
   5.149    by ferrack
   5.150  
   5.151 -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))"
   5.152 +lemma "EX z. (ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
   5.153    by ferrack
   5.154  
   5.155 -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))"
   5.156 +lemma "EX z. (ALL (x::'a::{linordered_field_inverse_zero, number_ring}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
   5.157    by ferrack
   5.158  
   5.159 -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))"
   5.160 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
   5.161    by ferrack
   5.162  
   5.163 -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)))"
   5.164 +lemma "EX y. (ALL (x::'a::{linordered_field_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)))"
   5.165    by ferrack
   5.166  
   5.167 -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))"
   5.168 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
   5.169    by ferrack
   5.170  
   5.171 -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (ALL y < x. (EX z > (x+y).
   5.172 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). (ALL y < x. (EX z > (x+y).
   5.173    (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))"
   5.174    by ferrack
   5.175  
   5.176 -lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (ALL y. (EX z > y.
   5.177 +lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). (ALL y. (EX z > y.
   5.178    (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))"
   5.179    by ferrack
   5.180  
   5.181 -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)"
   5.182 +lemma "EX (x::'a::{linordered_field_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)"
   5.183    by ferrack
   5.184  
   5.185 -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)))"
   5.186 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
   5.187    by ferrack
   5.188  
   5.189 -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)))"
   5.190 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
   5.191    by ferrack
   5.192  
   5.193 -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)))"
   5.194 +lemma "ALL (x::'a::{linordered_field_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)))"
   5.195    by ferrack
   5.196  
   5.197  end
     6.1 --- a/src/HOL/Fields.thy	Mon Apr 26 11:34:19 2010 +0200
     6.2 +++ b/src/HOL/Fields.thy	Mon Apr 26 15:37:50 2010 +0200
     6.3 @@ -129,22 +129,20 @@
     6.4  subclass division_ring_inverse_zero proof
     6.5  qed (fact field_inverse_zero)
     6.6  
     6.7 -end
     6.8 -
     6.9  text{*This version builds in division by zero while also re-orienting
    6.10        the right-hand side.*}
    6.11  lemma inverse_mult_distrib [simp]:
    6.12 -     "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_ring_inverse_zero})"
    6.13 -  proof cases
    6.14 -    assume "a \<noteq> 0 & b \<noteq> 0" 
    6.15 -    thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
    6.16 -  next
    6.17 -    assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
    6.18 -    thus ?thesis by force
    6.19 -  qed
    6.20 +  "inverse (a * b) = inverse a * inverse b"
    6.21 +proof cases
    6.22 +  assume "a \<noteq> 0 & b \<noteq> 0" 
    6.23 +  thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
    6.24 +next
    6.25 +  assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
    6.26 +  thus ?thesis by force
    6.27 +qed
    6.28  
    6.29  lemma inverse_divide [simp]:
    6.30 -  "inverse (a/b) = b / (a::'a::{field,division_ring_inverse_zero})"
    6.31 +  "inverse (a / b) = b / a"
    6.32    by (simp add: divide_inverse mult_commute)
    6.33  
    6.34  
    6.35 @@ -155,86 +153,88 @@
    6.36  because the latter are covered by a simproc. *}
    6.37  
    6.38  lemma mult_divide_mult_cancel_left:
    6.39 -  "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_ring_inverse_zero})"
    6.40 +  "c \<noteq> 0 \<Longrightarrow> (c * a) / (c * b) = a / b"
    6.41  apply (cases "b = 0")
    6.42  apply simp_all
    6.43  done
    6.44  
    6.45  lemma mult_divide_mult_cancel_right:
    6.46 -  "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_ring_inverse_zero})"
    6.47 +  "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
    6.48  apply (cases "b = 0")
    6.49  apply simp_all
    6.50  done
    6.51  
    6.52 -lemma divide_divide_eq_right [simp,no_atp]:
    6.53 -  "a / (b/c) = (a*c) / (b::'a::{field,division_ring_inverse_zero})"
    6.54 -by (simp add: divide_inverse mult_ac)
    6.55 +lemma divide_divide_eq_right [simp, no_atp]:
    6.56 +  "a / (b / c) = (a * c) / b"
    6.57 +  by (simp add: divide_inverse mult_ac)
    6.58  
    6.59 -lemma divide_divide_eq_left [simp,no_atp]:
    6.60 -  "(a / b) / (c::'a::{field,division_ring_inverse_zero}) = a / (b*c)"
    6.61 -by (simp add: divide_inverse mult_assoc)
    6.62 +lemma divide_divide_eq_left [simp, no_atp]:
    6.63 +  "(a / b) / c = a / (b * c)"
    6.64 +  by (simp add: divide_inverse mult_assoc)
    6.65  
    6.66  
    6.67  text {*Special Cancellation Simprules for Division*}
    6.68  
    6.69 -lemma mult_divide_mult_cancel_left_if[simp,no_atp]:
    6.70 -fixes c :: "'a :: {field,division_ring_inverse_zero}"
    6.71 -shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
    6.72 -by (simp add: mult_divide_mult_cancel_left)
    6.73 +lemma mult_divide_mult_cancel_left_if [simp,no_atp]:
    6.74 +  shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
    6.75 +  by (simp add: mult_divide_mult_cancel_left)
    6.76  
    6.77  
    6.78  text {* Division and Unary Minus *}
    6.79  
    6.80 -lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_ring_inverse_zero})"
    6.81 -by (simp add: divide_inverse)
    6.82 +lemma minus_divide_right:
    6.83 +  "- (a / b) = a / - b"
    6.84 +  by (simp add: divide_inverse)
    6.85  
    6.86  lemma divide_minus_right [simp, no_atp]:
    6.87 -  "a / -(b::'a::{field,division_ring_inverse_zero}) = -(a / b)"
    6.88 -by (simp add: divide_inverse)
    6.89 +  "a / - b = - (a / b)"
    6.90 +  by (simp add: divide_inverse)
    6.91  
    6.92  lemma minus_divide_divide:
    6.93 -  "(-a)/(-b) = a / (b::'a::{field,division_ring_inverse_zero})"
    6.94 +  "(- a) / (- b) = a / b"
    6.95  apply (cases "b=0", simp) 
    6.96  apply (simp add: nonzero_minus_divide_divide) 
    6.97  done
    6.98  
    6.99  lemma eq_divide_eq:
   6.100 -  "((a::'a::{field,division_ring_inverse_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
   6.101 -by (simp add: nonzero_eq_divide_eq)
   6.102 +  "a = b / c \<longleftrightarrow> (if c \<noteq> 0 then a * c = b else a = 0)"
   6.103 +  by (simp add: nonzero_eq_divide_eq)
   6.104  
   6.105  lemma divide_eq_eq:
   6.106 -  "(b/c = (a::'a::{field,division_ring_inverse_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
   6.107 -by (force simp add: nonzero_divide_eq_eq)
   6.108 +  "b / c = a \<longleftrightarrow> (if c \<noteq> 0 then b = a * c else a = 0)"
   6.109 +  by (force simp add: nonzero_divide_eq_eq)
   6.110  
   6.111  lemma inverse_eq_1_iff [simp]:
   6.112 -  "(inverse x = 1) = (x = (1::'a::{field,division_ring_inverse_zero}))"
   6.113 -by (insert inverse_eq_iff_eq [of x 1], simp) 
   6.114 +  "inverse x = 1 \<longleftrightarrow> x = 1"
   6.115 +  by (insert inverse_eq_iff_eq [of x 1], simp) 
   6.116  
   6.117 -lemma divide_eq_0_iff [simp,no_atp]:
   6.118 -     "(a/b = 0) = (a=0 | b=(0::'a::{field,division_ring_inverse_zero}))"
   6.119 -by (simp add: divide_inverse)
   6.120 +lemma divide_eq_0_iff [simp, no_atp]:
   6.121 +  "a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   6.122 +  by (simp add: divide_inverse)
   6.123  
   6.124 -lemma divide_cancel_right [simp,no_atp]:
   6.125 -     "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_ring_inverse_zero}))"
   6.126 -apply (cases "c=0", simp)
   6.127 -apply (simp add: divide_inverse)
   6.128 -done
   6.129 +lemma divide_cancel_right [simp, no_atp]:
   6.130 +  "a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b"
   6.131 +  apply (cases "c=0", simp)
   6.132 +  apply (simp add: divide_inverse)
   6.133 +  done
   6.134  
   6.135 -lemma divide_cancel_left [simp,no_atp]:
   6.136 -     "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_ring_inverse_zero}))" 
   6.137 -apply (cases "c=0", simp)
   6.138 -apply (simp add: divide_inverse)
   6.139 -done
   6.140 +lemma divide_cancel_left [simp, no_atp]:
   6.141 +  "c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b" 
   6.142 +  apply (cases "c=0", simp)
   6.143 +  apply (simp add: divide_inverse)
   6.144 +  done
   6.145  
   6.146 -lemma divide_eq_1_iff [simp,no_atp]:
   6.147 -     "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_ring_inverse_zero}))"
   6.148 -apply (cases "b=0", simp)
   6.149 -apply (simp add: right_inverse_eq)
   6.150 -done
   6.151 +lemma divide_eq_1_iff [simp, no_atp]:
   6.152 +  "a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   6.153 +  apply (cases "b=0", simp)
   6.154 +  apply (simp add: right_inverse_eq)
   6.155 +  done
   6.156  
   6.157 -lemma one_eq_divide_iff [simp,no_atp]:
   6.158 -     "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_ring_inverse_zero}))"
   6.159 -by (simp add: eq_commute [of 1])
   6.160 +lemma one_eq_divide_iff [simp, no_atp]:
   6.161 +  "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   6.162 +  by (simp add: eq_commute [of 1])
   6.163 +
   6.164 +end
   6.165  
   6.166  
   6.167  text {* Ordered Fields *}
   6.168 @@ -650,39 +650,37 @@
   6.169  subclass field_inverse_zero proof
   6.170  qed (fact linordered_field_inverse_zero)
   6.171  
   6.172 -end
   6.173 -
   6.174  lemma le_divide_eq:
   6.175    "(a \<le> b/c) = 
   6.176     (if 0 < c then a*c \<le> b
   6.177               else if c < 0 then b \<le> a*c
   6.178 -             else  a \<le> (0::'a::{linordered_field,division_ring_inverse_zero}))"
   6.179 +             else  a \<le> 0)"
   6.180  apply (cases "c=0", simp) 
   6.181  apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) 
   6.182  done
   6.183  
   6.184  lemma inverse_positive_iff_positive [simp]:
   6.185 -  "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_ring_inverse_zero}))"
   6.186 +  "(0 < inverse a) = (0 < a)"
   6.187  apply (cases "a = 0", simp)
   6.188  apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
   6.189  done
   6.190  
   6.191  lemma inverse_negative_iff_negative [simp]:
   6.192 -  "(inverse a < 0) = (a < (0::'a::{linordered_field,division_ring_inverse_zero}))"
   6.193 +  "(inverse a < 0) = (a < 0)"
   6.194  apply (cases "a = 0", simp)
   6.195  apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
   6.196  done
   6.197  
   6.198  lemma inverse_nonnegative_iff_nonnegative [simp]:
   6.199 -  "(0 \<le> inverse a) = (0 \<le> (a::'a::{linordered_field,division_ring_inverse_zero}))"
   6.200 -by (simp add: linorder_not_less [symmetric])
   6.201 +  "0 \<le> inverse a \<longleftrightarrow> 0 \<le> a"
   6.202 +  by (simp add: not_less [symmetric])
   6.203  
   6.204  lemma inverse_nonpositive_iff_nonpositive [simp]:
   6.205 -  "(inverse a \<le> 0) = (a \<le> (0::'a::{linordered_field,division_ring_inverse_zero}))"
   6.206 -by (simp add: linorder_not_less [symmetric])
   6.207 +  "inverse a \<le> 0 \<longleftrightarrow> a \<le> 0"
   6.208 +  by (simp add: not_less [symmetric])
   6.209  
   6.210  lemma one_less_inverse_iff:
   6.211 -  "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_ring_inverse_zero}))"
   6.212 +  "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1"
   6.213  proof cases
   6.214    assume "0 < x"
   6.215      with inverse_less_iff_less [OF zero_less_one, of x]
   6.216 @@ -692,7 +690,7 @@
   6.217    have "~ (1 < inverse x)"
   6.218    proof
   6.219      assume "1 < inverse x"
   6.220 -    also with notless have "... \<le> 0" by (simp add: linorder_not_less)
   6.221 +    also with notless have "... \<le> 0" by simp
   6.222      also have "... < 1" by (rule zero_less_one) 
   6.223      finally show False by auto
   6.224    qed
   6.225 @@ -700,62 +698,69 @@
   6.226  qed
   6.227  
   6.228  lemma one_le_inverse_iff:
   6.229 -  "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{linordered_field,division_ring_inverse_zero}))"
   6.230 -by (force simp add: order_le_less one_less_inverse_iff)
   6.231 +  "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1"
   6.232 +proof (cases "x = 1")
   6.233 +  case True then show ?thesis by simp
   6.234 +next
   6.235 +  case False then have "inverse x \<noteq> 1" by simp
   6.236 +  then have "1 \<noteq> inverse x" by blast
   6.237 +  then have "1 \<le> inverse x \<longleftrightarrow> 1 < inverse x" by (simp add: le_less)
   6.238 +  with False show ?thesis by (auto simp add: one_less_inverse_iff)
   6.239 +qed
   6.240  
   6.241  lemma inverse_less_1_iff:
   6.242 -  "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{linordered_field,division_ring_inverse_zero}))"
   6.243 -by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) 
   6.244 +  "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x"
   6.245 +  by (simp add: not_le [symmetric] one_le_inverse_iff) 
   6.246  
   6.247  lemma inverse_le_1_iff:
   6.248 -  "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{linordered_field,division_ring_inverse_zero}))"
   6.249 -by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
   6.250 +  "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
   6.251 +  by (simp add: not_less [symmetric] one_less_inverse_iff) 
   6.252  
   6.253  lemma divide_le_eq:
   6.254    "(b/c \<le> a) = 
   6.255     (if 0 < c then b \<le> a*c
   6.256               else if c < 0 then a*c \<le> b
   6.257 -             else 0 \<le> (a::'a::{linordered_field,division_ring_inverse_zero}))"
   6.258 +             else 0 \<le> a)"
   6.259  apply (cases "c=0", simp) 
   6.260 -apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) 
   6.261 +apply (force simp add: pos_divide_le_eq neg_divide_le_eq) 
   6.262  done
   6.263  
   6.264  lemma less_divide_eq:
   6.265    "(a < b/c) = 
   6.266     (if 0 < c then a*c < b
   6.267               else if c < 0 then b < a*c
   6.268 -             else  a < (0::'a::{linordered_field,division_ring_inverse_zero}))"
   6.269 +             else  a < 0)"
   6.270  apply (cases "c=0", simp) 
   6.271 -apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) 
   6.272 +apply (force simp add: pos_less_divide_eq neg_less_divide_eq) 
   6.273  done
   6.274  
   6.275  lemma divide_less_eq:
   6.276    "(b/c < a) = 
   6.277     (if 0 < c then b < a*c
   6.278               else if c < 0 then a*c < b
   6.279 -             else 0 < (a::'a::{linordered_field,division_ring_inverse_zero}))"
   6.280 +             else 0 < a)"
   6.281  apply (cases "c=0", simp) 
   6.282 -apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
   6.283 +apply (force simp add: pos_divide_less_eq neg_divide_less_eq)
   6.284  done
   6.285  
   6.286  text {*Division and Signs*}
   6.287  
   6.288  lemma zero_less_divide_iff:
   6.289 -     "((0::'a::{linordered_field,division_ring_inverse_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
   6.290 +     "(0 < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
   6.291  by (simp add: divide_inverse zero_less_mult_iff)
   6.292  
   6.293  lemma divide_less_0_iff:
   6.294 -     "(a/b < (0::'a::{linordered_field,division_ring_inverse_zero})) = 
   6.295 +     "(a/b < 0) = 
   6.296        (0 < a & b < 0 | a < 0 & 0 < b)"
   6.297  by (simp add: divide_inverse mult_less_0_iff)
   6.298  
   6.299  lemma zero_le_divide_iff:
   6.300 -     "((0::'a::{linordered_field,division_ring_inverse_zero}) \<le> a/b) =
   6.301 +     "(0 \<le> a/b) =
   6.302        (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
   6.303  by (simp add: divide_inverse zero_le_mult_iff)
   6.304  
   6.305  lemma divide_le_0_iff:
   6.306 -     "(a/b \<le> (0::'a::{linordered_field,division_ring_inverse_zero})) =
   6.307 +     "(a/b \<le> 0) =
   6.308        (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
   6.309  by (simp add: divide_inverse mult_le_0_iff)
   6.310  
   6.311 @@ -764,13 +769,13 @@
   6.312  text{*Simplify expressions equated with 1*}
   6.313  
   6.314  lemma zero_eq_1_divide_iff [simp,no_atp]:
   6.315 -     "((0::'a::{linordered_field,division_ring_inverse_zero}) = 1/a) = (a = 0)"
   6.316 +     "(0 = 1/a) = (a = 0)"
   6.317  apply (cases "a=0", simp)
   6.318  apply (auto simp add: nonzero_eq_divide_eq)
   6.319  done
   6.320  
   6.321  lemma one_divide_eq_0_iff [simp,no_atp]:
   6.322 -     "(1/a = (0::'a::{linordered_field,division_ring_inverse_zero})) = (a = 0)"
   6.323 +     "(1/a = 0) = (a = 0)"
   6.324  apply (cases "a=0", simp)
   6.325  apply (insert zero_neq_one [THEN not_sym])
   6.326  apply (auto simp add: nonzero_divide_eq_eq)
   6.327 @@ -788,16 +793,16 @@
   6.328  declare divide_le_0_1_iff [simp,no_atp]
   6.329  
   6.330  lemma divide_right_mono:
   6.331 -     "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{linordered_field,division_ring_inverse_zero})"
   6.332 -by (force simp add: divide_strict_right_mono order_le_less)
   6.333 +     "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/c"
   6.334 +by (force simp add: divide_strict_right_mono le_less)
   6.335  
   6.336 -lemma divide_right_mono_neg: "(a::'a::{linordered_field,division_ring_inverse_zero}) <= b 
   6.337 +lemma divide_right_mono_neg: "a <= b 
   6.338      ==> c <= 0 ==> b / c <= a / c"
   6.339  apply (drule divide_right_mono [of _ _ "- c"])
   6.340  apply auto
   6.341  done
   6.342  
   6.343 -lemma divide_left_mono_neg: "(a::'a::{linordered_field,division_ring_inverse_zero}) <= b 
   6.344 +lemma divide_left_mono_neg: "a <= b 
   6.345      ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
   6.346    apply (drule divide_left_mono [of _ _ "- c"])
   6.347    apply (auto simp add: mult_commute)
   6.348 @@ -808,99 +813,84 @@
   6.349  text{*Simplify quotients that are compared with the value 1.*}
   6.350  
   6.351  lemma le_divide_eq_1 [no_atp]:
   6.352 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.353 -  shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
   6.354 +  "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
   6.355  by (auto simp add: le_divide_eq)
   6.356  
   6.357  lemma divide_le_eq_1 [no_atp]:
   6.358 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.359 -  shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
   6.360 +  "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
   6.361  by (auto simp add: divide_le_eq)
   6.362  
   6.363  lemma less_divide_eq_1 [no_atp]:
   6.364 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.365 -  shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
   6.366 +  "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
   6.367  by (auto simp add: less_divide_eq)
   6.368  
   6.369  lemma divide_less_eq_1 [no_atp]:
   6.370 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.371 -  shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
   6.372 +  "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
   6.373  by (auto simp add: divide_less_eq)
   6.374  
   6.375  
   6.376  text {*Conditional Simplification Rules: No Case Splits*}
   6.377  
   6.378  lemma le_divide_eq_1_pos [simp,no_atp]:
   6.379 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.380 -  shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
   6.381 +  "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
   6.382  by (auto simp add: le_divide_eq)
   6.383  
   6.384  lemma le_divide_eq_1_neg [simp,no_atp]:
   6.385 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.386 -  shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
   6.387 +  "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
   6.388  by (auto simp add: le_divide_eq)
   6.389  
   6.390  lemma divide_le_eq_1_pos [simp,no_atp]:
   6.391 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.392 -  shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
   6.393 +  "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
   6.394  by (auto simp add: divide_le_eq)
   6.395  
   6.396  lemma divide_le_eq_1_neg [simp,no_atp]:
   6.397 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.398 -  shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
   6.399 +  "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
   6.400  by (auto simp add: divide_le_eq)
   6.401  
   6.402  lemma less_divide_eq_1_pos [simp,no_atp]:
   6.403 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.404 -  shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
   6.405 +  "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
   6.406  by (auto simp add: less_divide_eq)
   6.407  
   6.408  lemma less_divide_eq_1_neg [simp,no_atp]:
   6.409 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.410 -  shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
   6.411 +  "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
   6.412  by (auto simp add: less_divide_eq)
   6.413  
   6.414  lemma divide_less_eq_1_pos [simp,no_atp]:
   6.415 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.416 -  shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
   6.417 +  "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
   6.418  by (auto simp add: divide_less_eq)
   6.419  
   6.420  lemma divide_less_eq_1_neg [simp,no_atp]:
   6.421 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.422 -  shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
   6.423 +  "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
   6.424  by (auto simp add: divide_less_eq)
   6.425  
   6.426  lemma eq_divide_eq_1 [simp,no_atp]:
   6.427 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.428 -  shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
   6.429 +  "(1 = b/a) = ((a \<noteq> 0 & a = b))"
   6.430  by (auto simp add: eq_divide_eq)
   6.431  
   6.432  lemma divide_eq_eq_1 [simp,no_atp]:
   6.433 -  fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
   6.434 -  shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
   6.435 +  "(b/a = 1) = ((a \<noteq> 0 & a = b))"
   6.436  by (auto simp add: divide_eq_eq)
   6.437  
   6.438  lemma abs_inverse [simp]:
   6.439 -     "\<bar>inverse (a::'a::{linordered_field,division_ring_inverse_zero})\<bar> = 
   6.440 +     "\<bar>inverse a\<bar> = 
   6.441        inverse \<bar>a\<bar>"
   6.442  apply (cases "a=0", simp) 
   6.443  apply (simp add: nonzero_abs_inverse) 
   6.444  done
   6.445  
   6.446  lemma abs_divide [simp]:
   6.447 -     "\<bar>a / (b::'a::{linordered_field,division_ring_inverse_zero})\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
   6.448 +     "\<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
   6.449  apply (cases "b=0", simp) 
   6.450  apply (simp add: nonzero_abs_divide) 
   6.451  done
   6.452  
   6.453 -lemma abs_div_pos: "(0::'a::{linordered_field,division_ring_inverse_zero}) < y ==> 
   6.454 +lemma abs_div_pos: "0 < y ==> 
   6.455      \<bar>x\<bar> / y = \<bar>x / y\<bar>"
   6.456    apply (subst abs_divide)
   6.457    apply (simp add: order_less_imp_le)
   6.458  done
   6.459  
   6.460  lemma field_le_mult_one_interval:
   6.461 -  fixes x :: "'a\<Colon>{linordered_field,division_ring_inverse_zero}"
   6.462    assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
   6.463    shows "x \<le> y"
   6.464  proof (cases "0 < x")
   6.465 @@ -916,6 +906,8 @@
   6.466    finally show ?thesis .
   6.467  qed
   6.468  
   6.469 +end
   6.470 +
   6.471  code_modulename SML
   6.472    Fields Arith
   6.473  
     7.1 --- a/src/HOL/Groebner_Basis.thy	Mon Apr 26 11:34:19 2010 +0200
     7.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Apr 26 15:37:50 2010 +0200
     7.3 @@ -473,21 +473,21 @@
     7.4  interpretation class_fieldgb:
     7.5    fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
     7.6  
     7.7 -lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
     7.8 -lemma divide_Numeral0: "(x::'a::{field,number_ring, division_ring_inverse_zero}) / Numeral0 = 0"
     7.9 +lemma divide_Numeral1: "(x::'a::{field, number_ring}) / Numeral1 = x" by simp
    7.10 +lemma divide_Numeral0: "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0"
    7.11    by simp
    7.12 -lemma mult_frac_frac: "((x::'a::{field,division_ring_inverse_zero}) / y) * (z / w) = (x*z) / (y*w)"
    7.13 +lemma mult_frac_frac: "((x::'a::field_inverse_zero) / y) * (z / w) = (x*z) / (y*w)"
    7.14    by simp
    7.15 -lemma mult_frac_num: "((x::'a::{field, division_ring_inverse_zero}) / y) * z  = (x*z) / y"
    7.16 +lemma mult_frac_num: "((x::'a::field_inverse_zero) / y) * z  = (x*z) / y"
    7.17    by simp
    7.18 -lemma mult_num_frac: "((x::'a::{field, division_ring_inverse_zero}) / y) * z  = (x*z) / y"
    7.19 +lemma mult_num_frac: "((x::'a::field_inverse_zero) / y) * z  = (x*z) / y"
    7.20    by simp
    7.21  
    7.22  lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
    7.23  
    7.24 -lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_ring_inverse_zero}) / y + z = (x + z*y) / y"
    7.25 +lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::field_inverse_zero) / y + z = (x + z*y) / y"
    7.26    by (simp add: add_divide_distrib)
    7.27 -lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_ring_inverse_zero}) / y = (x + z*y) / y"
    7.28 +lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::field_inverse_zero) / y = (x + z*y) / y"
    7.29    by (simp add: add_divide_distrib)
    7.30  
    7.31  ML {*
     8.1 --- a/src/HOL/Int.thy	Mon Apr 26 11:34:19 2010 +0200
     8.2 +++ b/src/HOL/Int.thy	Mon Apr 26 15:37:50 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_ring_inverse_zero,number_ring})"
     8.8 +     "x/-1 = -(x::'a::{field_inverse_zero, number_ring})"
     8.9  by simp
    8.10  
    8.11  lemma minus1_divide [simp]:
    8.12 -     "-1 / (x::'a::{field,division_ring_inverse_zero,number_ring}) = - (1/x)"
    8.13 +     "-1 / (x::'a::{field_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_ring_inverse_zero,number_ring}))"
    8.18 +     "(0 < r/2) = (0 < (r::'a::{linordered_field_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:19 2010 +0200
     9.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Mon Apr 26 15:37:50 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_ring_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
     9.8 +  shows "((INum x ::'a::{field_char_0, field_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,11 +217,11 @@
    9.13  qed
    9.14  
    9.15  
    9.16 -lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{ring_char_0, field,division_ring_inverse_zero})) = (x = 0\<^sub>N)"
    9.17 +lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_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 -lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::{field, ring_char_0}) / (of_int d) = 
    9.22 +lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) = 
    9.23      of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
    9.24  proof -
    9.25    assume "d ~= 0"
    9.26 @@ -238,14 +238,14 @@
    9.27  qed
    9.28  
    9.29  lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
    9.30 -    (of_int(n div d)::'a::{field, ring_char_0}) = of_int n / of_int d"
    9.31 +    (of_int(n div d)::'a::field_char_0) = of_int n / of_int d"
    9.32    apply (frule of_int_div_aux [of d n, where ?'a = 'a])
    9.33    apply simp
    9.34    apply (simp add: dvd_eq_mod_eq_0)
    9.35  done
    9.36  
    9.37  
    9.38 -lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{ring_char_0,field, division_ring_inverse_zero})"
    9.39 +lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
    9.40  proof-
    9.41    have "\<exists> a b. x = (a,b)" by auto
    9.42    then obtain a b where x[simp]: "x = (a,b)" by blast
    9.43 @@ -260,7 +260,7 @@
    9.44    ultimately show ?thesis by blast
    9.45  qed
    9.46  
    9.47 -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.48 +lemma INum_normNum_iff: "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
    9.49  proof -
    9.50    have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
    9.51      by (simp del: normNum)
    9.52 @@ -268,7 +268,7 @@
    9.53    finally show ?thesis by simp
    9.54  qed
    9.55  
    9.56 -lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {ring_char_0,division_ring_inverse_zero,field})"
    9.57 +lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})"
    9.58  proof-
    9.59  let ?z = "0:: 'a"
    9.60    have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
    9.61 @@ -300,7 +300,7 @@
    9.62    ultimately show ?thesis by blast
    9.63  qed
    9.64  
    9.65 -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {ring_char_0,division_ring_inverse_zero,field}) "
    9.66 +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero}) "
    9.67  proof-
    9.68    let ?z = "0::'a"
    9.69    have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
    9.70 @@ -323,16 +323,16 @@
    9.71  lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
    9.72    by (simp add: Nneg_def split_def INum_def)
    9.73  
    9.74 -lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {ring_char_0,division_ring_inverse_zero,field})"
    9.75 +lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
    9.76  by (simp add: Nsub_def split_def)
    9.77  
    9.78 -lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: {division_ring_inverse_zero,field}) / (INum x)"
    9.79 +lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
    9.80    by (simp add: Ninv_def INum_def split_def)
    9.81  
    9.82 -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.83 +lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" by (simp add: Ndiv_def)
    9.84  
    9.85  lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" 
    9.86 -  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})< 0) = 0>\<^sub>N x "
    9.87 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x "
    9.88  proof-
    9.89    have " \<exists> a b. x = (a,b)" by simp
    9.90    then obtain a b where x[simp]:"x = (a,b)" by blast
    9.91 @@ -345,7 +345,7 @@
    9.92  qed
    9.93  
    9.94  lemma Nle0_iff[simp]:assumes nx: "isnormNum x" 
    9.95 -  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \<le> 0) = 0\<ge>\<^sub>N x"
    9.96 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<le> 0) = 0\<ge>\<^sub>N x"
    9.97  proof-
    9.98    have " \<exists> a b. x = (a,b)" by simp
    9.99    then obtain a b where x[simp]:"x = (a,b)" by blast
   9.100 @@ -357,7 +357,7 @@
   9.101    ultimately show ?thesis by blast
   9.102  qed
   9.103  
   9.104 -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.105 +lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
   9.106  proof-
   9.107    have " \<exists> a b. x = (a,b)" by simp
   9.108    then obtain a b where x[simp]:"x = (a,b)" by blast
   9.109 @@ -369,7 +369,7 @@
   9.110    ultimately show ?thesis by blast
   9.111  qed
   9.112  lemma Nge0_iff[simp]:assumes nx: "isnormNum x" 
   9.113 -  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x"
   9.114 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
   9.115  proof-
   9.116    have " \<exists> a b. x = (a,b)" by simp
   9.117    then obtain a b where x[simp]:"x = (a,b)" by blast
   9.118 @@ -382,7 +382,7 @@
   9.119  qed
   9.120  
   9.121  lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   9.122 -  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) < INum y) = (x <\<^sub>N y)"
   9.123 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)"
   9.124  proof-
   9.125    let ?z = "0::'a"
   9.126    have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp
   9.127 @@ -391,7 +391,7 @@
   9.128  qed
   9.129  
   9.130  lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   9.131 -  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)"
   9.132 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)"
   9.133  proof-
   9.134    have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" using nx ny by simp
   9.135    also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
   9.136 @@ -399,7 +399,7 @@
   9.137  qed
   9.138  
   9.139  lemma Nadd_commute:
   9.140 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.141 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   9.142    shows "x +\<^sub>N y = y +\<^sub>N x"
   9.143  proof-
   9.144    have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
   9.145 @@ -408,7 +408,7 @@
   9.146  qed
   9.147  
   9.148  lemma [simp]:
   9.149 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.150 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   9.151    shows "(0, b) +\<^sub>N y = normNum y"
   9.152      and "(a, 0) +\<^sub>N y = normNum y" 
   9.153      and "x +\<^sub>N (0, b) = normNum x"
   9.154 @@ -420,7 +420,7 @@
   9.155    done
   9.156  
   9.157  lemma normNum_nilpotent_aux[simp]:
   9.158 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.159 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   9.160    assumes nx: "isnormNum x" 
   9.161    shows "normNum x = x"
   9.162  proof-
   9.163 @@ -432,7 +432,7 @@
   9.164  qed
   9.165  
   9.166  lemma normNum_nilpotent[simp]:
   9.167 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.168 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   9.169    shows "normNum (normNum x) = normNum x"
   9.170    by simp
   9.171  
   9.172 @@ -440,11 +440,11 @@
   9.173    by (simp_all add: normNum_def)
   9.174  
   9.175  lemma normNum_Nadd:
   9.176 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.177 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   9.178    shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
   9.179  
   9.180  lemma Nadd_normNum1[simp]:
   9.181 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.182 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   9.183    shows "normNum x +\<^sub>N y = x +\<^sub>N y"
   9.184  proof-
   9.185    have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
   9.186 @@ -454,7 +454,7 @@
   9.187  qed
   9.188  
   9.189  lemma Nadd_normNum2[simp]:
   9.190 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.191 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   9.192    shows "x +\<^sub>N normNum y = x +\<^sub>N y"
   9.193  proof-
   9.194    have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
   9.195 @@ -464,7 +464,7 @@
   9.196  qed
   9.197  
   9.198  lemma Nadd_assoc:
   9.199 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.200 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   9.201    shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
   9.202  proof-
   9.203    have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
   9.204 @@ -476,7 +476,7 @@
   9.205    by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute)
   9.206  
   9.207  lemma Nmul_assoc:
   9.208 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.209 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   9.210    assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
   9.211    shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
   9.212  proof-
   9.213 @@ -487,7 +487,7 @@
   9.214  qed
   9.215  
   9.216  lemma Nsub0:
   9.217 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.218 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   9.219    assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
   9.220  proof-
   9.221    { fix h :: 'a
   9.222 @@ -502,7 +502,7 @@
   9.223    by (simp_all add: Nmul_def Let_def split_def)
   9.224  
   9.225  lemma Nmul_eq0[simp]:
   9.226 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   9.227 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   9.228    assumes nx:"isnormNum x" and ny: "isnormNum y"
   9.229    shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
   9.230  proof-
    10.1 --- a/src/HOL/Library/Bit.thy	Mon Apr 26 11:34:19 2010 +0200
    10.2 +++ b/src/HOL/Library/Bit.thy	Mon Apr 26 15:37:50 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_ring_inverse_zero}"
    10.8 +instantiation bit :: field_inverse_zero
    10.9  begin
   10.10  
   10.11  definition plus_bit_def:
    11.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Mon Apr 26 11:34:19 2010 +0200
    11.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Apr 26 15:37:50 2010 +0200
    11.3 @@ -28,7 +28,7 @@
    11.4  
    11.5  text{* Definition of the basic elements 0 and 1 and the basic operations of addition, negation and multiplication *}
    11.6  
    11.7 -instantiation fps :: (zero)  zero
    11.8 +instantiation fps :: (zero) zero
    11.9  begin
   11.10  
   11.11  definition fps_zero_def:
   11.12 @@ -40,7 +40,7 @@
   11.13  lemma fps_zero_nth [simp]: "0 $ n = 0"
   11.14    unfolding fps_zero_def by simp
   11.15  
   11.16 -instantiation fps :: ("{one,zero}")  one
   11.17 +instantiation fps :: ("{one, zero}") one
   11.18  begin
   11.19  
   11.20  definition fps_one_def:
   11.21 @@ -2649,7 +2649,7 @@
   11.22  text{* The generalized binomial theorem as a  consequence of @{thm E_add_mult} *}
   11.23  
   11.24  lemma gbinomial_theorem: 
   11.25 -  "((a::'a::{field_char_0, division_ring_inverse_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
   11.26 +  "((a::'a::{field_char_0, field_inverse_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
   11.27  proof-
   11.28    from E_add_mult[of a b] 
   11.29    have "(E (a + b)) $ n = (E a * E b)$n" by simp
   11.30 @@ -3252,7 +3252,7 @@
   11.31  subsection {* Hypergeometric series *}
   11.32  
   11.33  
   11.34 -definition "F as bs (c::'a::{field_char_0, division_ring_inverse_zero}) = Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
   11.35 +definition "F as bs (c::'a::{field_char_0, field_inverse_zero}) = Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
   11.36  
   11.37  lemma F_nth[simp]: "F as bs c $ n =  (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n))"
   11.38    by (simp add: F_def)
   11.39 @@ -3321,9 +3321,9 @@
   11.40    by (simp add: fps_eq_iff fps_integral_def)
   11.41  
   11.42  lemma F_minus_nat: 
   11.43 -  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, division_ring_inverse_zero}) $ k = (if k <= n then pochhammer (- of_nat n) k * c ^ k /
   11.44 +  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, field_inverse_zero}) $ k = (if k <= n then pochhammer (- of_nat n) k * c ^ k /
   11.45      (pochhammer (- of_nat (n + m)) k * of_nat (fact k)) else 0)"
   11.46 -  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, division_ring_inverse_zero}) $ k = (if k <= m then pochhammer (- of_nat m) k * c ^ k /
   11.47 +  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, field_inverse_zero}) $ k = (if k <= m then pochhammer (- of_nat m) k * c ^ k /
   11.48      (pochhammer (- of_nat (m + n)) k * of_nat (fact k)) else 0)"
   11.49    by (auto simp add: pochhammer_eq_0_iff)
   11.50  
    12.1 --- a/src/HOL/Library/Fraction_Field.thy	Mon Apr 26 11:34:19 2010 +0200
    12.2 +++ b/src/HOL/Library/Fraction_Field.thy	Mon Apr 26 15:37:50 2010 +0200
    12.3 @@ -232,7 +232,7 @@
    12.4  thm mult_eq_0_iff
    12.5  end
    12.6  
    12.7 -instantiation fract :: (idom) field
    12.8 +instantiation fract :: (idom) field_inverse_zero
    12.9  begin
   12.10  
   12.11  definition
   12.12 @@ -263,16 +263,13 @@
   12.13  next
   12.14    fix q r :: "'a fract"
   12.15    show "q / r = q * inverse r" by (simp add: divide_fract_def)
   12.16 +next
   12.17 +  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
   12.18 +    (simp add: fract_collapse)
   12.19  qed
   12.20  
   12.21  end
   12.22  
   12.23 -instance fract :: (idom) division_ring_inverse_zero
   12.24 -proof
   12.25 -  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
   12.26 -    (simp add: fract_collapse)
   12.27 -qed
   12.28 -
   12.29  
   12.30  subsubsection {* The ordered field of fractions over an ordered idom *}
   12.31  
    13.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Mon Apr 26 11:34:19 2010 +0200
    13.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Mon Apr 26 15:37:50 2010 +0200
    13.3 @@ -55,7 +55,7 @@
    13.4  done
    13.5  
    13.6    (* FIXME: In Finite_Set there is a useless further assumption *)
    13.7 -lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: {division_ring_inverse_zero, field})"
    13.8 +lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)"
    13.9    apply (erule finite_induct)
   13.10    apply (simp)
   13.11    apply simp
    14.1 --- a/src/HOL/NSA/HyperDef.thy	Mon Apr 26 11:34:19 2010 +0200
    14.2 +++ b/src/HOL/NSA/HyperDef.thy	Mon Apr 26 15:37:50 2010 +0200
    14.3 @@ -140,12 +140,12 @@
    14.4  
    14.5  lemma of_hypreal_inverse [simp]:
    14.6    "\<And>x. of_hypreal (inverse x) =
    14.7 -   inverse (of_hypreal x :: 'a::{real_div_algebra,division_ring_inverse_zero} star)"
    14.8 +   inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring_inverse_zero} star)"
    14.9  by transfer (rule of_real_inverse)
   14.10  
   14.11  lemma of_hypreal_divide [simp]:
   14.12    "\<And>x y. of_hypreal (x / y) =
   14.13 -   (of_hypreal x / of_hypreal y :: 'a::{real_field,division_ring_inverse_zero} star)"
   14.14 +   (of_hypreal x / of_hypreal y :: 'a::{real_field, field_inverse_zero} star)"
   14.15  by transfer (rule of_real_divide)
   14.16  
   14.17  lemma of_hypreal_eq_iff [simp]:
   14.18 @@ -454,7 +454,7 @@
   14.19  by transfer (rule field_power_not_zero)
   14.20  
   14.21  lemma hyperpow_inverse:
   14.22 -  "\<And>r n. r \<noteq> (0::'a::{division_ring_inverse_zero,field} star)
   14.23 +  "\<And>r n. r \<noteq> (0::'a::field_inverse_zero star)
   14.24     \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
   14.25  by transfer (rule power_inverse)
   14.26    
    15.1 --- a/src/HOL/NSA/NSA.thy	Mon Apr 26 11:34:19 2010 +0200
    15.2 +++ b/src/HOL/NSA/NSA.thy	Mon Apr 26 15:37:50 2010 +0200
    15.3 @@ -145,12 +145,12 @@
    15.4  by transfer (rule nonzero_norm_inverse)
    15.5  
    15.6  lemma hnorm_inverse:
    15.7 -  "\<And>a::'a::{real_normed_div_algebra,division_ring_inverse_zero} star.
    15.8 +  "\<And>a::'a::{real_normed_div_algebra, division_ring_inverse_zero} star.
    15.9     hnorm (inverse a) = inverse (hnorm a)"
   15.10  by transfer (rule norm_inverse)
   15.11  
   15.12  lemma hnorm_divide:
   15.13 -  "\<And>a b::'a::{real_normed_field,division_ring_inverse_zero} star.
   15.14 +  "\<And>a b::'a::{real_normed_field, field_inverse_zero} star.
   15.15     hnorm (a / b) = hnorm a / hnorm b"
   15.16  by transfer (rule norm_divide)
   15.17  
    16.1 --- a/src/HOL/Power.thy	Mon Apr 26 11:34:19 2010 +0200
    16.2 +++ b/src/HOL/Power.thy	Mon Apr 26 15:37:50 2010 +0200
    16.3 @@ -392,27 +392,26 @@
    16.4    by (induct n)
    16.5      (auto simp add: no_zero_divisors elim: contrapos_pp)
    16.6  
    16.7 -lemma power_diff:
    16.8 -  fixes a :: "'a::field"
    16.9 +lemma (in field) power_diff:
   16.10    assumes nz: "a \<noteq> 0"
   16.11    shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
   16.12 -  by (induct m n rule: diff_induct) (simp_all add: nz)
   16.13 +  by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero)
   16.14  
   16.15  text{*Perhaps these should be simprules.*}
   16.16  lemma power_inverse:
   16.17 -  fixes a :: "'a::{division_ring,division_ring_inverse_zero,power}"
   16.18 -  shows "inverse (a ^ n) = (inverse a) ^ n"
   16.19 +  fixes a :: "'a::division_ring_inverse_zero"
   16.20 +  shows "inverse (a ^ n) = inverse a ^ n"
   16.21  apply (cases "a = 0")
   16.22  apply (simp add: power_0_left)
   16.23  apply (simp add: nonzero_power_inverse)
   16.24  done (* TODO: reorient or rename to inverse_power *)
   16.25  
   16.26  lemma power_one_over:
   16.27 -  "1 / (a::'a::{field,division_ring_inverse_zero, power}) ^ n =  (1 / a) ^ n"
   16.28 +  "1 / (a::'a::{field_inverse_zero, power}) ^ n =  (1 / a) ^ n"
   16.29    by (simp add: divide_inverse) (rule power_inverse)
   16.30  
   16.31  lemma power_divide:
   16.32 -  "(a / b) ^ n = (a::'a::{field,division_ring_inverse_zero}) ^ n / b ^ n"
   16.33 +  "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
   16.34  apply (cases "b = 0")
   16.35  apply (simp add: power_0_left)
   16.36  apply (rule nonzero_power_divide)
    17.1 --- a/src/HOL/Rat.thy	Mon Apr 26 11:34:19 2010 +0200
    17.2 +++ b/src/HOL/Rat.thy	Mon Apr 26 15:37:50 2010 +0200
    17.3 @@ -411,7 +411,7 @@
    17.4  
    17.5  subsubsection {* The field of rational numbers *}
    17.6  
    17.7 -instantiation rat :: field
    17.8 +instantiation rat :: field_inverse_zero
    17.9  begin
   17.10  
   17.11  definition
   17.12 @@ -440,13 +440,10 @@
   17.13  next
   17.14    fix q r :: rat
   17.15    show "q / r = q * inverse r" by (simp add: divide_rat_def)
   17.16 -qed
   17.17 +qed (simp add: rat_number_expand, simp add: rat_number_collapse)
   17.18  
   17.19  end
   17.20  
   17.21 -instance rat :: division_ring_inverse_zero proof
   17.22 -qed (simp add: rat_number_expand, simp add: rat_number_collapse)
   17.23 -
   17.24  
   17.25  subsubsection {* Various *}
   17.26  
   17.27 @@ -624,7 +621,7 @@
   17.28  
   17.29  end
   17.30  
   17.31 -instance rat :: linordered_field
   17.32 +instance rat :: linordered_field_inverse_zero
   17.33  proof
   17.34    fix q r s :: rat
   17.35    show "q \<le> r ==> s + q \<le> s + r"
   17.36 @@ -724,8 +721,7 @@
   17.37      by (cases "b = 0", simp, simp add: of_int_rat)
   17.38    moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
   17.39      unfolding Fract_of_int_quotient
   17.40 -    by (rule linorder_cases [of b 0])
   17.41 -       (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
   17.42 +    by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
   17.43    ultimately show ?thesis by simp
   17.44  qed
   17.45  
   17.46 @@ -818,7 +814,7 @@
   17.47  done
   17.48  
   17.49  lemma of_rat_inverse:
   17.50 -  "(of_rat (inverse a)::'a::{field_char_0,division_ring_inverse_zero}) =
   17.51 +  "(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) =
   17.52     inverse (of_rat a)"
   17.53  by (cases "a = 0", simp_all add: nonzero_of_rat_inverse)
   17.54  
   17.55 @@ -827,7 +823,7 @@
   17.56  by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse)
   17.57  
   17.58  lemma of_rat_divide:
   17.59 -  "(of_rat (a / b)::'a::{field_char_0,division_ring_inverse_zero})
   17.60 +  "(of_rat (a / b)::'a::{field_char_0, field_inverse_zero})
   17.61     = of_rat a / of_rat b"
   17.62  by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
   17.63  
   17.64 @@ -968,7 +964,7 @@
   17.65  done
   17.66  
   17.67  lemma Rats_inverse [simp]:
   17.68 -  fixes a :: "'a::{field_char_0,division_ring_inverse_zero}"
   17.69 +  fixes a :: "'a::{field_char_0, field_inverse_zero}"
   17.70    shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
   17.71  apply (auto simp add: Rats_def)
   17.72  apply (rule range_eqI)
   17.73 @@ -984,7 +980,7 @@
   17.74  done
   17.75  
   17.76  lemma Rats_divide [simp]:
   17.77 -  fixes a b :: "'a::{field_char_0,division_ring_inverse_zero}"
   17.78 +  fixes a b :: "'a::{field_char_0, field_inverse_zero}"
   17.79    shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
   17.80  apply (auto simp add: Rats_def)
   17.81  apply (rule range_eqI)
    18.1 --- a/src/HOL/RealDef.thy	Mon Apr 26 11:34:19 2010 +0200
    18.2 +++ b/src/HOL/RealDef.thy	Mon Apr 26 15:37:50 2010 +0200
    18.3 @@ -266,22 +266,15 @@
    18.4  
    18.5  subsection{*The Real Numbers form a Field*}
    18.6  
    18.7 -instance real :: field
    18.8 +lemma INVERSE_ZERO: "inverse 0 = (0::real)"
    18.9 +by (simp add: real_inverse_def)
   18.10 +
   18.11 +instance real :: field_inverse_zero
   18.12  proof
   18.13    fix x y z :: real
   18.14    show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
   18.15    show "x / y = x * inverse y" by (simp add: real_divide_def)
   18.16 -qed
   18.17 -
   18.18 -
   18.19 -text{*Inverse of zero!  Useful to simplify certain equations*}
   18.20 -
   18.21 -lemma INVERSE_ZERO: "inverse 0 = (0::real)"
   18.22 -by (simp add: real_inverse_def)
   18.23 -
   18.24 -instance real :: division_ring_inverse_zero
   18.25 -proof
   18.26 -  show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
   18.27 +  show "inverse 0 = (0::real)" by (fact INVERSE_ZERO)
   18.28  qed
   18.29  
   18.30  
   18.31 @@ -426,6 +419,9 @@
   18.32      by (simp only: real_sgn_def)
   18.33  qed
   18.34  
   18.35 +instance real :: linordered_field_inverse_zero proof
   18.36 +qed (fact INVERSE_ZERO)
   18.37 +
   18.38  text{*The function @{term real_of_preal} requires many proofs, but it seems
   18.39  to be essential for proving completeness of the reals from that of the
   18.40  positive reals.*}
    19.1 --- a/src/HOL/RealVector.thy	Mon Apr 26 11:34:19 2010 +0200
    19.2 +++ b/src/HOL/RealVector.thy	Mon Apr 26 15:37:50 2010 +0200
    19.3 @@ -207,7 +207,7 @@
    19.4  by (rule inverse_unique, simp)
    19.5  
    19.6  lemma inverse_scaleR_distrib:
    19.7 -  fixes x :: "'a::{real_div_algebra,division_ring_inverse_zero}"
    19.8 +  fixes x :: "'a::{real_div_algebra, division_ring_inverse_zero}"
    19.9    shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
   19.10  apply (case_tac "a = 0", simp)
   19.11  apply (case_tac "x = 0", simp)
   19.12 @@ -250,7 +250,7 @@
   19.13  
   19.14  lemma of_real_inverse [simp]:
   19.15    "of_real (inverse x) =
   19.16 -   inverse (of_real x :: 'a::{real_div_algebra,division_ring_inverse_zero})"
   19.17 +   inverse (of_real x :: 'a::{real_div_algebra, division_ring_inverse_zero})"
   19.18  by (simp add: of_real_def inverse_scaleR_distrib)
   19.19  
   19.20  lemma nonzero_of_real_divide:
   19.21 @@ -260,7 +260,7 @@
   19.22  
   19.23  lemma of_real_divide [simp]:
   19.24    "of_real (x / y) =
   19.25 -   (of_real x / of_real y :: 'a::{real_field,division_ring_inverse_zero})"
   19.26 +   (of_real x / of_real y :: 'a::{real_field, field_inverse_zero})"
   19.27  by (simp add: divide_inverse)
   19.28  
   19.29  lemma of_real_power [simp]:
   19.30 @@ -370,7 +370,7 @@
   19.31  done
   19.32  
   19.33  lemma Reals_inverse [simp]:
   19.34 -  fixes a :: "'a::{real_div_algebra,division_ring_inverse_zero}"
   19.35 +  fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}"
   19.36    shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
   19.37  apply (auto simp add: Reals_def)
   19.38  apply (rule range_eqI)
   19.39 @@ -386,7 +386,7 @@
   19.40  done
   19.41  
   19.42  lemma Reals_divide [simp]:
   19.43 -  fixes a b :: "'a::{real_field,division_ring_inverse_zero}"
   19.44 +  fixes a b :: "'a::{real_field, field_inverse_zero}"
   19.45    shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
   19.46  apply (auto simp add: Reals_def)
   19.47  apply (rule range_eqI)
   19.48 @@ -726,7 +726,7 @@
   19.49  done
   19.50  
   19.51  lemma norm_inverse:
   19.52 -  fixes a :: "'a::{real_normed_div_algebra,division_ring_inverse_zero}"
   19.53 +  fixes a :: "'a::{real_normed_div_algebra, division_ring_inverse_zero}"
   19.54    shows "norm (inverse a) = inverse (norm a)"
   19.55  apply (case_tac "a = 0", simp)
   19.56  apply (erule nonzero_norm_inverse)
   19.57 @@ -738,7 +738,7 @@
   19.58  by (simp add: divide_inverse norm_mult nonzero_norm_inverse)
   19.59  
   19.60  lemma norm_divide:
   19.61 -  fixes a b :: "'a::{real_normed_field,division_ring_inverse_zero}"
   19.62 +  fixes a b :: "'a::{real_normed_field, field_inverse_zero}"
   19.63    shows "norm (a / b) = norm a / norm b"
   19.64  by (simp add: divide_inverse norm_mult norm_inverse)
   19.65  
    20.1 --- a/src/HOL/Series.thy	Mon Apr 26 11:34:19 2010 +0200
    20.2 +++ b/src/HOL/Series.thy	Mon Apr 26 15:37:50 2010 +0200
    20.3 @@ -381,7 +381,7 @@
    20.4    shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
    20.5  by (rule geometric_sums [THEN sums_summable])
    20.6  
    20.7 -lemma half: "0 < 1 / (2::'a::{number_ring,division_ring_inverse_zero,linordered_field})"
    20.8 +lemma half: "0 < 1 / (2::'a::{number_ring,linordered_field_inverse_zero})"
    20.9    by arith 
   20.10  
   20.11  lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
    21.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Mon Apr 26 11:34:19 2010 +0200
    21.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Apr 26 15:37:50 2010 +0200
    21.3 @@ -332,8 +332,8 @@
    21.4  val field_combine_numerals =
    21.5    Arith_Data.prep_simproc @{theory}
    21.6      ("field_combine_numerals", 
    21.7 -     ["(i::'a::{number_ring,field,division_ring_inverse_zero}) + j",
    21.8 -      "(i::'a::{number_ring,field,division_ring_inverse_zero}) - j"], 
    21.9 +     ["(i::'a::{field_inverse_zero, number_ring}) + j",
   21.10 +      "(i::'a::{field_inverse_zero, number_ring}) - j"], 
   21.11       K FieldCombineNumerals.proc);
   21.12  
   21.13  (** Constant folding for multiplication in semirings **)
   21.14 @@ -442,9 +442,9 @@
   21.15        "(l::'a::{semiring_div,number_ring}) div (m * n)"],
   21.16       K DivCancelNumeralFactor.proc),
   21.17      ("divide_cancel_numeral_factor",
   21.18 -     ["((l::'a::{division_ring_inverse_zero,field,number_ring}) * m) / n",
   21.19 -      "(l::'a::{division_ring_inverse_zero,field,number_ring}) / (m * n)",
   21.20 -      "((number_of v)::'a::{division_ring_inverse_zero,field,number_ring}) / (number_of w)"],
   21.21 +     ["((l::'a::{field_inverse_zero,number_ring}) * m) / n",
   21.22 +      "(l::'a::{field_inverse_zero,number_ring}) / (m * n)",
   21.23 +      "((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)"],
   21.24       K DivideCancelNumeralFactor.proc)];
   21.25  
   21.26  val field_cancel_numeral_factors =
   21.27 @@ -454,9 +454,9 @@
   21.28        "(l::'a::{field,number_ring}) = m * n"],
   21.29       K EqCancelNumeralFactor.proc),
   21.30      ("field_cancel_numeral_factor",
   21.31 -     ["((l::'a::{division_ring_inverse_zero,field,number_ring}) * m) / n",
   21.32 -      "(l::'a::{division_ring_inverse_zero,field,number_ring}) / (m * n)",
   21.33 -      "((number_of v)::'a::{division_ring_inverse_zero,field,number_ring}) / (number_of w)"],
   21.34 +     ["((l::'a::{field_inverse_zero,number_ring}) * m) / n",
   21.35 +      "(l::'a::{field_inverse_zero,number_ring}) / (m * n)",
   21.36 +      "((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)"],
   21.37       K DivideCancelNumeralFactor.proc)]
   21.38  
   21.39  
   21.40 @@ -598,8 +598,8 @@
   21.41       ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
   21.42       K DvdCancelFactor.proc),
   21.43      ("divide_cancel_factor",
   21.44 -     ["((l::'a::{division_ring_inverse_zero,field}) * m) / n",
   21.45 -      "(l::'a::{division_ring_inverse_zero,field}) / (m * n)"],
   21.46 +     ["((l::'a::field_inverse_zero) * m) / n",
   21.47 +      "(l::'a::field_inverse_zero) / (m * n)"],
   21.48       K DivideCancelFactor.proc)];
   21.49  
   21.50  end;