# HG changeset patch
# User haftmann
# Date 1272354576 -7200
# Node ID a19ba9bbc8dcd3cf59d854e44226d2d9c663518e
# Parent  942438a0fa84c700b6fe1f356a683267b64f96ef
tuned class linordered_field_inverse_zero

diff -r 942438a0fa84 -r a19ba9bbc8dc src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Tue Apr 27 08:18:25 2010 +0200
+++ b/src/HOL/Fields.thy	Tue Apr 27 09:49:36 2010 +0200
@@ -643,13 +643,9 @@
 
 end
 
-class linordered_field_inverse_zero = linordered_field +
-  assumes linordered_field_inverse_zero: "inverse 0 = 0"
+class linordered_field_inverse_zero = linordered_field + field_inverse_zero
 begin
 
-subclass field_inverse_zero proof
-qed (fact linordered_field_inverse_zero)
-
 lemma le_divide_eq:
   "(a \<le> b/c) = 
    (if 0 < c then a*c \<le> b
diff -r 942438a0fa84 -r a19ba9bbc8dc src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Tue Apr 27 08:18:25 2010 +0200
+++ b/src/HOL/Library/Fraction_Field.thy	Tue Apr 27 09:49:36 2010 +0200
@@ -431,7 +431,7 @@
 
 end
 
-instance fract :: (linordered_idom) linordered_field
+instance fract :: (linordered_idom) linordered_field_inverse_zero
 proof
   fix q r s :: "'a fract"
   show "q \<le> r ==> s + q \<le> s + r"
diff -r 942438a0fa84 -r a19ba9bbc8dc src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Tue Apr 27 08:18:25 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy	Tue Apr 27 09:49:36 2010 +0200
@@ -950,10 +950,7 @@
 
 instance star :: (linordered_idom) linordered_idom ..
 instance star :: (linordered_field) linordered_field ..
-instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero 
-apply intro_classes
-apply (rule inverse_zero)
-done
+instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero ..
 
 
 subsection {* Power *}
diff -r 942438a0fa84 -r a19ba9bbc8dc src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Tue Apr 27 08:18:25 2010 +0200
+++ b/src/HOL/RealDef.thy	Tue Apr 27 09:49:36 2010 +0200
@@ -266,17 +266,17 @@
 
 subsection{*The Real Numbers form a Field*}
 
-lemma INVERSE_ZERO: "inverse 0 = (0::real)"
-by (simp add: real_inverse_def)
-
 instance real :: field_inverse_zero
 proof
   fix x y z :: real
   show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
   show "x / y = x * inverse y" by (simp add: real_divide_def)
-  show "inverse 0 = (0::real)" by (fact INVERSE_ZERO)
+  show "inverse 0 = (0::real)" by (simp add: real_inverse_def)
 qed
 
+lemma INVERSE_ZERO: "inverse 0 = (0::real)"
+  by (fact inverse_zero)
+
 
 subsection{*The @{text "\<le>"} Ordering*}
 
@@ -409,7 +409,7 @@
 
 subsection{*The Reals Form an Ordered Field*}
 
-instance real :: linordered_field
+instance real :: linordered_field_inverse_zero
 proof
   fix x y z :: real
   show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
@@ -419,9 +419,6 @@
     by (simp only: real_sgn_def)
 qed
 
-instance real :: linordered_field_inverse_zero proof
-qed (fact INVERSE_ZERO)
-
 text{*The function @{term real_of_preal} requires many proofs, but it seems
 to be essential for proving completeness of the reals from that of the
 positive reals.*}