src/HOL/Real/RealDef.thy
 changeset 14738 83f1a514dcb4 parent 14691 e1eedc8cad37 child 14754 a080eeeaec14
```--- a/src/HOL/Real/RealDef.thy	Tue May 11 14:00:02 2004 +0200
+++ b/src/HOL/Real/RealDef.thy	Tue May 11 20:11:08 2004 +0200
@@ -169,7 +169,7 @@
lemma real_add_zero_left: "(0::real) + z = z"

-instance real :: plus_ac0
by (intro_classes,
(assumption |
@@ -281,9 +281,6 @@
instance real :: field
proof
fix x y z :: real
-  show "(x + y) + z = x + (y + z)" by (rule real_add_assoc)
-  show "x + y = y + x" by (rule real_add_commute)
-  show "0 + x = x" by simp
show "- x + x = 0" by (rule real_add_minus_left)
show "x - y = x + (-y)" by (simp add: real_diff_def)
show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
@@ -312,7 +309,7 @@
minus_mult_left [symmetric, simp]

lemma real_mult_1_right: "z * (1::real) = z"
-  by (rule Ring_and_Field.mult_1_right)
+  by (rule OrderedGroup.mult_1_right)

subsection{*The @{text "\<le>"} Ordering*}
@@ -554,11 +551,11 @@
by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])

lemma real_add_less_le_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::real)"

"!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"

lemma real_le_square [simp]: "(0::real) \<le> x*x"
by (rule Ring_and_Field.zero_le_square)
@@ -597,7 +594,7 @@

text{*FIXME: delete or at least combine the next two lemmas*}
lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
-apply (drule Ring_and_Field.equals_zero_I [THEN sym])
+apply (drule OrderedGroup.equals_zero_I [THEN sym])
apply (cut_tac x = y in real_le_square)
apply (auto, drule order_antisym, auto)
done
@@ -848,7 +845,7 @@

lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"