--- 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
--- 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"
--- 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 *}
--- 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.*}