src/HOL/Real/RealDef.thy
 changeset 14497 76cdbeb0c9de parent 14484 ef8c7c5eb01b child 14658 b1293d0f8d5f
```--- 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)"

-lemma realrel_refl: "(x,x) \<in> realrel"
-apply (case_tac "x")
-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

-     "Abs_Real(realrel``{(x1,y1)}) + Abs_Real(realrel``{(x2,y2)}) =
-      Abs_Real(realrel``{(x1+x2, y1+y2)})"
-apply (subst equiv_realrel [THEN UN_equiv_class2])
-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)"
+  thus ?thesis
+                  UN_equiv_class2 [OF equiv_realrel])
+qed

lemma real_add_commute: "(z::real) + w = w + z"
-done

lemma real_add_assoc: "((z1::real) + z2) + z3 = z1 + (z2 + z3)"
-done

lemma real_add_zero_left: "(0::real) + z = z"
-done

instance real :: plus_ac0
by (intro_classes,
@@ -197,8 +192,7 @@
qed

lemma real_add_minus_left: "(-z) + z = (0::real)"
-done

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"
-done

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"
-done