# HG changeset patch
# User paulson
# Date 1080638714 -7200
# Node ID 76cdbeb0c9def40b3d497da6a02793d36df9cc43
# Parent  aba569f1b1e0ef369ba17fab90d8477f94911132
tidied

diff -r aba569f1b1e0 -r 76cdbeb0c9de src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Tue Mar 30 11:18:12 2004 +0200
+++ b/src/HOL/Real/RealDef.thy	Tue Mar 30 11:25:14 2004 +0200
@@ -107,22 +107,19 @@
 lemma realrel_iff [simp]: "(((x1,y1),(x2,y2)) \<in> realrel) = (x1 + y2 = x2 + y1)"
 by (simp add: realrel_def)
 
-lemma realrel_refl: "(x,x) \<in> realrel"
-apply (case_tac "x")
-apply (simp add: realrel_def)
-done
-
 lemma equiv_realrel: "equiv UNIV realrel"
 apply (auto simp add: equiv_def refl_def sym_def trans_def realrel_def)
 apply (blast dest: preal_trans_lemma) 
 done
 
-(* (realrel `` {x} = realrel `` {y}) = ((x,y) \<in> realrel) *)
+text{*Reduces equality of equivalence classes to the @{term realrel} relation:
+  @{term "(realrel `` {x} = realrel `` {y}) = ((x,y) \<in> realrel)"} *}
 lemmas equiv_realrel_iff = 
        eq_equiv_class_iff [OF equiv_realrel UNIV_I UNIV_I]
 
 declare equiv_realrel_iff [simp]
 
+
 lemma realrel_in_real [simp]: "realrel``{(x,y)}: Real"
 by (simp add: Real_def realrel_def quotient_def, blast)
 
@@ -136,8 +133,6 @@
 declare Abs_Real_inverse [simp]
 
 
-lemmas eq_realrelD = equiv_realrel [THEN [2] eq_equiv_class]
-
 text{*Case analysis on the representation of a real number as an equivalence
       class of pairs of positive reals.*}
 lemma eq_Abs_Real [case_names Abs_Real, cases type: real]: 
@@ -160,25 +155,25 @@
 done
 
 lemma real_add:
-     "Abs_Real(realrel``{(x1,y1)}) + Abs_Real(realrel``{(x2,y2)}) =
-      Abs_Real(realrel``{(x1+x2, y1+y2)})"
-apply (simp add: real_add_def UN_UN_split_split_eq)
-apply (subst equiv_realrel [THEN UN_equiv_class2])
-apply (auto simp add: congruent2_def)
-apply (blast intro: real_add_congruent2_lemma) 
-done
+     "Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) =
+      Abs_Real (realrel``{(x+u, y+v)})"
+proof -
+  have "congruent2 realrel
+        (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)"
+    by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
+  thus ?thesis
+    by (simp add: real_add_def UN_UN_split_split_eq
+                  UN_equiv_class2 [OF equiv_realrel])
+qed
 
 lemma real_add_commute: "(z::real) + w = w + z"
-apply (cases z, cases w, simp add: real_add preal_add_ac)
-done
+by (cases z, cases w, simp add: real_add preal_add_ac)
 
 lemma real_add_assoc: "((z1::real) + z2) + z3 = z1 + (z2 + z3)"
-apply (cases z1, cases z2, cases z3, simp add: real_add preal_add_assoc)
-done
+by (cases z1, cases z2, cases z3, simp add: real_add preal_add_assoc)
 
 lemma real_add_zero_left: "(0::real) + z = z"
-apply (cases z, simp add: real_add real_zero_def preal_add_ac)
-done
+by (cases z, simp add: real_add real_zero_def preal_add_ac)
 
 instance real :: plus_ac0
   by (intro_classes,
@@ -197,8 +192,7 @@
 qed
 
 lemma real_add_minus_left: "(-z) + z = (0::real)"
-apply (cases z, simp add: real_minus real_add real_zero_def preal_add_commute)
-done
+by (cases z, simp add: real_minus real_add real_zero_def preal_add_commute)
 
 
 subsection{*Congruence property for multiplication*}
@@ -228,8 +222,7 @@
               UN_equiv_class2 [OF equiv_realrel real_mult_congruent2])
 
 lemma real_mult_commute: "(z::real) * w = w * z"
-apply (cases z, cases w, simp add: real_mult preal_add_ac preal_mult_ac)
-done
+by (cases z, cases w, simp add: real_mult preal_add_ac preal_mult_ac)
 
 lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)"
 apply (cases z1, cases z2, cases z3)
@@ -260,8 +253,7 @@
 subsection{*existence of inverse*}
 
 lemma real_zero_iff: "Abs_Real (realrel `` {(x, x)}) = 0"
-apply (simp add: real_zero_def preal_add_commute)
-done
+by (simp add: real_zero_def preal_add_commute)
 
 text{*Instead of using an existential quantifier and constructing the inverse
 within the proof, we could define the inverse explicitly.*}
@@ -367,8 +359,7 @@
 done
 
 lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
-apply (cases z, cases w, simp add: real_le order_antisym) 
-done
+by (cases z, cases w, simp add: real_le order_antisym)
 
 lemma real_trans_lemma:
   assumes "x + v \<le> u + y"
diff -r aba569f1b1e0 -r 76cdbeb0c9de src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Tue Mar 30 11:18:12 2004 +0200
+++ b/src/HOL/Real/real_arith.ML	Tue Mar 30 11:25:14 2004 +0200
@@ -18,19 +18,11 @@
 val real_diff_def = thm "real_diff_def";
 val real_divide_def = thm "real_divide_def";
 
-val realrel_iff = thm"realrel_iff";
-val realrel_refl = thm"realrel_refl";
-val equiv_realrel = thm"equiv_realrel";
-val equiv_realrel_iff = thm"equiv_realrel_iff";
 val realrel_in_real = thm"realrel_in_real";
-val eq_realrelD = thm"eq_realrelD";
-val real_minus = thm"real_minus";
-val real_add = thm"real_add";
 val real_add_commute = thm"real_add_commute";
 val real_add_assoc = thm"real_add_assoc";
 val real_add_zero_left = thm"real_add_zero_left";
 
-val real_mult = thm"real_mult";
 val real_mult_commute = thm"real_mult_commute";
 val real_mult_assoc = thm"real_mult_assoc";
 val real_mult_1 = thm"real_mult_1";