# HG changeset patch
# User paulson
# Date 1094043841 -7200
# Node ID 2b5da07a0b89ba241e057814e52affc22f8fdbd2
# Parent  33a08cfc3ae5639086167af0ef184ce751a41205
new "respects" syntax for quotienting

diff -r 33a08cfc3ae5 -r 2b5da07a0b89 src/HOL/Complex/CStar.thy
--- a/src/HOL/Complex/CStar.thy	Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Complex/CStar.thy	Wed Sep 01 15:04:01 2004 +0200
@@ -206,9 +206,8 @@
 by (simp add: starfunCR_n_def starfunCR_def)
 
 lemma starfunC_congruent:
-      "congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})"
-apply (auto simp add: hcomplexrel_iff congruent_def, ultra)
-done
+      "(%X. hcomplexrel``{%n. f (X n)}) respects hcomplexrel"
+by (auto simp add: hcomplexrel_iff congruent_def, ultra)
 
 (* f::complex => complex *)
 lemma starfunC:
@@ -508,7 +507,7 @@
 subsection{*Internal Functions - Some Redundancy With *Fc* Now*}
 
 lemma starfunC_n_congruent:
-      "congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})"
+      "(%X. hcomplexrel``{%n. f n (X n)}) respects hcomplexrel"
 by (auto simp add: congruent_def hcomplexrel_iff, ultra)
 
 lemma starfunC_n:
diff -r 33a08cfc3ae5 -r 2b5da07a0b89 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Wed Sep 01 15:04:01 2004 +0200
@@ -283,7 +283,7 @@
 subsection{*Additive Inverse on Nonstandard Complex Numbers*}
 
 lemma hcomplex_minus_congruent:
-     "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
+     "(%X. hcomplexrel `` {%n. - (X n)}) respects hcomplexrel"
 by (simp add: congruent_def)
 
 lemma hcomplex_minus:
diff -r 33a08cfc3ae5 -r 2b5da07a0b89 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Sep 01 15:04:01 2004 +0200
@@ -342,8 +342,7 @@
 
 subsection{*Additive inverse on @{typ hypreal}*}
 
-lemma hypreal_minus_congruent: 
-  "congruent hyprel (%X. hyprel``{%n. - (X n)})"
+lemma hypreal_minus_congruent: "(%X. hyprel``{%n. - (X n)}) respects hyprel"
 by (force simp add: congruent_def)
 
 lemma hypreal_minus: 
@@ -397,7 +396,7 @@
 subsection{*Multiplicative Inverse on @{typ hypreal} *}
 
 lemma hypreal_inverse_congruent: 
-  "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})"
+  "(%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)}) respects hyprel"
 by (auto simp add: congruent_def, ultra)
 
 lemma hypreal_inverse: 
diff -r 33a08cfc3ae5 -r 2b5da07a0b89 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Wed Sep 01 15:04:01 2004 +0200
@@ -136,7 +136,7 @@
 subsection{*Hypernat Addition*}
 
 lemma hypnat_add_congruent2:
-     "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
+     "(%X Y. hypnatrel``{%n. X n + Y n}) respects2 hypnatrel"
 by (simp add: congruent2_def, auto, ultra)
 
 lemma hypnat_add:
@@ -170,7 +170,7 @@
 
 
 lemma hypnat_minus_congruent2:
-    "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
+    "(%X Y. hypnatrel``{%n. X n - Y n}) respects2 hypnatrel"
 by (simp add: congruent2_def, auto, ultra)
 
 lemma hypnat_minus:
@@ -238,7 +238,7 @@
 subsection{*Hyperreal Multiplication*}
 
 lemma hypnat_mult_congruent2:
-    "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
+    "(%X Y. hypnatrel``{%n. X n * Y n}) respects2 hypnatrel"
 by (simp add: congruent2_def, auto, ultra)
 
 lemma hypnat_mult:
diff -r 33a08cfc3ae5 -r 2b5da07a0b89 src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy	Wed Sep 01 15:04:01 2004 +0200
@@ -114,12 +114,8 @@
 
 subsection{*Powers with Hypernatural Exponents*}
 
-lemma hyperpow_congruent:
-     "congruent hyprel
-     (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"
-apply (unfold congruent_def)
-apply (auto intro!: ext, fuf+)
-done
+lemma hyperpow_congruent: "(%X Y. hyprel``{%n. (X n ^ Y n)}) respects hyprel"
+by (auto simp add: congruent_def intro!: ext, fuf+)
 
 lemma hyperpow:
   "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
diff -r 33a08cfc3ae5 -r 2b5da07a0b89 src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Wed Sep 01 15:04:01 2004 +0200
@@ -185,8 +185,7 @@
 lemma starfunNat2_n_starfunNat2: "\<forall>n. (F n = f) ==> *fNat2n* F = *fNat2* f"
 by (simp add: starfunNat2_n_def starfunNat2_def)
 
-lemma starfunNat_congruent:
-      "congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})"
+lemma starfunNat_congruent: "(%X. hypnatrel``{%n. f (X n)}) respects hypnatrel"
 apply (simp add: congruent_def, safe)
 apply (ultra+)
 done
@@ -396,10 +395,8 @@
 text{*Internal functions - some redundancy with *fNat* now*}
 
 lemma starfunNat_n_congruent:
-      "congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})"
-apply (simp add: congruent_def, safe)
-apply (ultra+)
-done
+      "(%X. hypnatrel``{%n. f n (X n)}) respects hypnatrel"
+by (auto simp add: congruent_def, ultra+)
 
 lemma starfunNat_n:
      "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
diff -r 33a08cfc3ae5 -r 2b5da07a0b89 src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Wed Sep 01 15:04:01 2004 +0200
@@ -53,9 +53,7 @@
 apply (blast intro: LeastI)
 done
 
-(*------------------------------------------------------------
-    Properties of the *-transform applied to sets of reals
- ------------------------------------------------------------*)
+subsection{*Properties of the Star-transform Applied to Sets of Reals*}
 
 lemma STAR_real_set: "*s*(UNIV::real set) = (UNIV::hypreal set)"
 by (simp add: starset_def)
@@ -148,10 +146,8 @@
 lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
 by (blast dest: STAR_subset)
 
-(*------------------------------------------------------------------
-   Nonstandard extension of a set (defined using a constant
-   sequence) as a special case of an internal set
- -----------------------------------------------------------------*)
+text{*Nonstandard extension of a set (defined using a constant
+   sequence) as a special case of an internal set*}
 
 lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
 by (simp add: starset_n_def starset_def)
@@ -197,11 +193,9 @@
 apply (auto, ultra)
 done
 
-(*-----------------------------------------------------------------------
-    Nonstandard extension of functions- congruence
- -----------------------------------------------------------------------*)
+text{*Nonstandard extension of functions*}
 
-lemma starfun_congruent: "congruent hyprel (%X. hyprel``{%n. f (X n)})"
+lemma starfun_congruent: "(%X. hyprel``{%n. f (X n)}) respects hyprel"
 by (simp add: congruent_def, auto, ultra)
 
 lemma starfun:
@@ -272,9 +266,7 @@
 apply (simp (no_asm) add: starfun_o2)
 done
 
-(*--------------------------------------
-  NS extension of constant function
- --------------------------------------*)
+text{*NS extension of constant function*}
 lemma starfun_const_fun: "( *f* (%x. k)) xa = hypreal_of_real  k"
 apply (cases xa)
 apply (auto simp add: starfun hypreal_of_real_def)
@@ -282,9 +274,7 @@
 
 declare starfun_const_fun [simp]
 
-(*----------------------------------------------------
-   the NS extension of the identity function
- ----------------------------------------------------*)
+text{*the NS extension of the identity function*}
 
 lemma starfun_Idfun_approx: "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real  a"
 apply (cases x)
@@ -297,9 +287,7 @@
 done
 declare starfun_Id [simp]
 
-(*----------------------------------------------------------------------
-      the *-function is a (nonstandard) extension of the function
- ----------------------------------------------------------------------*)
+text{*The Star-function is a (nonstandard) extension of the function*}
 
 lemma is_starext_starfun: "is_starext ( *f* f) f"
 apply (simp add: is_starext_def, auto)
@@ -308,9 +296,7 @@
 apply (auto intro!: bexI simp add: starfun)
 done
 
-(*----------------------------------------------------------------------
-     Any nonstandard extension is in fact the *-function
- ----------------------------------------------------------------------*)
+text{*Any nonstandard extension is in fact the Star-function*}
 
 lemma is_starfun_starext: "is_starext F f ==> F = *f* f"
 apply (simp add: is_starext_def)
@@ -324,11 +310,9 @@
 lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)"
 by (blast intro: is_starfun_starext is_starext_starfun)
 
-(*--------------------------------------------------------
-   extented function has same solution as its standard
+text{*extented function has same solution as its standard
    version for real arguments. i.e they are the same
-   for all real arguments
- -------------------------------------------------------*)
+   for all real arguments*}
 lemma starfun_eq: "( *f* f) (hypreal_of_real a) = hypreal_of_real (f a)"
 by (auto simp add: starfun hypreal_of_real_def)
 
@@ -360,10 +344,8 @@
 apply (auto intro: approx_add)
 done
 
-(*----------------------------------------------------
-    Examples: hrabs is nonstandard extension of rabs
-              inverse is nonstandard extension of inverse
- ---------------------------------------------------*)
+text{*Examples: hrabs is nonstandard extension of rabs
+              inverse is nonstandard extension of inverse*}
 
 (* can be proved easily using theorem "starfun" and *)
 (* properties of ultrafilter as for inverse below we  *)
@@ -393,10 +375,8 @@
 apply (auto intro: FreeUltrafilterNat_subset dest!: FreeUltrafilterNat_Compl_mem simp add: starfun hypreal_inverse hypreal_zero_def)
 done
 
-(*-------------------------------------------------------------
-    General lemma/theorem needed for proofs in elementary
-    topology of the reals
- ------------------------------------------------------------*)
+text{*General lemma/theorem needed for proofs in elementary
+    topology of the reals*}
 lemma starfun_mem_starset:
       "( *f* f) x : *s* A ==> x : *s* {x. f x  \<in> A}"
 apply (simp add: starset_def)
@@ -407,22 +387,18 @@
 apply (auto, ultra)
 done
 
-(*------------------------------------------------------------
-   Alternative definition for hrabs with rabs function
+text{*Alternative definition for hrabs with rabs function
    applied entrywise to equivalence class representative.
-   This is easily proved using starfun and ns extension thm
- ------------------------------------------------------------*)
+   This is easily proved using starfun and ns extension thm*}
 lemma hypreal_hrabs: "abs (Abs_hypreal (hyprel `` {X})) =
                   Abs_hypreal(hyprel `` {%n. abs (X n)})"
 apply (simp (no_asm) add: starfun_rabs_hrabs [symmetric] starfun)
 done
 
-(*----------------------------------------------------------------
-   nonstandard extension of set through nonstandard extension
+text{*nonstandard extension of set through nonstandard extension
    of rabs function i.e hrabs. A more general result should be
    where we replace rabs by some arbitrary function f and hrabs
-   by its NS extenson ( *f* f). See second NS set extension below.
- ----------------------------------------------------------------*)
+   by its NS extenson. See second NS set extension below.*}
 lemma STAR_rabs_add_minus:
    "*s* {x. abs (x + - y) < r} =
      {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
@@ -439,11 +415,9 @@
 apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less starfun, ultra)
 done
 
-(*-------------------------------------------------------------------
-   Another characterization of Infinitesimal and one of @= relation.
+text{*Another characterization of Infinitesimal and one of @= relation.
    In this theory since hypreal_hrabs proved here. (To Check:) Maybe
-   move both if possible?
- -------------------------------------------------------------------*)
+   move both if possible?*}
 lemma Infinitesimal_FreeUltrafilterNat_iff2:
      "(x \<in> Infinitesimal) =
       (\<exists>X \<in> Rep_hypreal(x).
diff -r 33a08cfc3ae5 -r 2b5da07a0b89 src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Induct/QuoDataType.thy	Wed Sep 01 15:04:01 2004 +0200
@@ -166,7 +166,7 @@
 
 
 text{*All equivalence classes belong to set of representatives*}
-lemma msgrel_in_integ [simp]: "msgrel``{U} \<in> Msg"
+lemma [simp]: "msgrel``{U} \<in> Msg"
 by (auto simp add: Msg_def quotient_def intro: msgrel_refl)
 
 lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"
@@ -185,7 +185,7 @@
 lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) = 
               Abs_Msg (msgrel``{MPAIR U V})"
 proof -
-  have "congruent2 msgrel msgrel (\<lambda>U V. msgrel `` {MPAIR U V})"
+  have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"
     by (simp add: congruent2_def msgrel.MPAIR)
   thus ?thesis
     by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
@@ -193,7 +193,7 @@
 
 lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
 proof -
-  have "congruent msgrel (\<lambda>U. msgrel `` {CRYPT K U})"
+  have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"
     by (simp add: congruent_def msgrel.CRYPT)
   thus ?thesis
     by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
@@ -202,7 +202,7 @@
 lemma Decrypt:
      "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
 proof -
-  have "congruent msgrel (\<lambda>U. msgrel `` {DECRYPT K U})"
+  have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"
     by (simp add: congruent_def msgrel.DECRYPT)
   thus ?thesis
     by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
@@ -230,7 +230,7 @@
   nonces :: "msg \<Rightarrow> nat set"
    "nonces X == \<Union>U \<in> Rep_Msg X. freenonces U"
 
-lemma nonces_congruent: "congruent msgrel freenonces"
+lemma nonces_congruent: "freenonces respects msgrel"
 by (simp add: congruent_def msgrel_imp_eq_freenonces) 
 
 
@@ -265,7 +265,7 @@
   left :: "msg \<Rightarrow> msg"
    "left X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
 
-lemma left_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeleft U})"
+lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
 by (simp add: congruent_def msgrel_imp_eqv_freeleft) 
 
 text{*Now prove the four equations for @{term left}*}
@@ -299,7 +299,7 @@
   right :: "msg \<Rightarrow> msg"
    "right X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
 
-lemma right_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeright U})"
+lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
 by (simp add: congruent_def msgrel_imp_eqv_freeright) 
 
 text{*Now prove the four equations for @{term right}*}
@@ -433,7 +433,7 @@
   discrim :: "msg \<Rightarrow> int"
    "discrim X == contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
 
-lemma discrim_congruent: "congruent msgrel (\<lambda>U. {freediscrim U})"
+lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
 by (simp add: congruent_def msgrel_imp_eq_freediscrim) 
 
 text{*Now prove the four equations for @{term discrim}*}
diff -r 33a08cfc3ae5 -r 2b5da07a0b89 src/HOL/Integ/Equiv.thy
--- a/src/HOL/Integ/Equiv.thy	Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Integ/Equiv.thy	Wed Sep 01 15:04:01 2004 +0200
@@ -151,12 +151,19 @@
   fixes r and f
   assumes congruent: "(y,z) \<in> r ==> f y = f z"
 
+syntax
+  RESPECTS ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects" 80)
+
+translations
+  "f respects r" == "congruent r f"
+
+
 lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
   -- {* lemma required to prove @{text UN_equiv_class} *}
   by auto
 
 lemma UN_equiv_class:
-  "equiv A r ==> congruent r f ==> a \<in> A
+  "equiv A r ==> f respects r ==> a \<in> A
     ==> (\<Union>x \<in> r``{a}. f x) = f a"
   -- {* Conversion rule *}
   apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)
@@ -165,7 +172,7 @@
   done
 
 lemma UN_equiv_class_type:
-  "equiv A r ==> congruent r f ==> X \<in> A//r ==>
+  "equiv A r ==> f respects r ==> X \<in> A//r ==>
     (!!x. x \<in> A ==> f x \<in> B) ==> (\<Union>x \<in> X. f x) \<in> B"
   apply (unfold quotient_def)
   apply clarify
@@ -180,7 +187,7 @@
 *}
 
 lemma UN_equiv_class_inject:
-  "equiv A r ==> congruent r f ==>
+  "equiv A r ==> f respects r ==>
     (\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) ==> X \<in> A//r ==> Y \<in> A//r
     ==> (!!x y. x \<in> A ==> y \<in> A ==> f x = f y ==> (x, y) \<in> r)
     ==> X = Y"
@@ -203,6 +210,13 @@
   assumes congruent2:
     "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
 
+text{*Abbreviation for the common case where the relations are identical*}
+syntax
+  RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects2 " 80)
+
+translations
+  "f respects2 r" => "congruent2 r r f"
+
 lemma congruent2_implies_congruent:
     "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
   by (unfold congruent_def congruent2_def equiv_def refl_def) blast
@@ -258,7 +272,7 @@
   assumes equivA: "equiv A r"
     and commute: "!!y z. y \<in> A ==> z \<in> A ==> f y z = f z y"
     and congt: "!!y z w. w \<in> A ==> (y,z) \<in> r ==> f w y = f w z"
-  shows "congruent2 r r f"
+  shows "f respects2 r"
   apply (rule congruent2I [OF equivA equivA])
    apply (rule commute [THEN trans])
      apply (rule_tac [3] commute [THEN trans, symmetric])
@@ -270,7 +284,7 @@
 
 subsection {* Cardinality results *}
 
-text {* (suggested by Florian Kammüller) *}
+text {*Suggested by Florian Kammüller*}
 
 lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
   -- {* recall @{thm equiv_type} *}
diff -r 33a08cfc3ae5 -r 2b5da07a0b89 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Sep 01 15:04:01 2004 +0200
@@ -110,7 +110,7 @@
 
 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
 proof -
-  have "congruent intrel (\<lambda>(x,y). intrel``{(y,x)})"
+  have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
     by (simp add: congruent_def) 
   thus ?thesis
     by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
@@ -129,8 +129,8 @@
      "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
       Abs_Integ (intrel``{(x+u, y+v)})"
 proof -
-  have "congruent2 intrel intrel
-        (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)"
+  have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
+        respects2 intrel"
     by (simp add: congruent2_def)
   thus ?thesis
     by (simp add: add_int_def UN_UN_split_split_eq
@@ -183,9 +183,8 @@
 
 text{*Congruence property for multiplication*}
 lemma mult_congruent2:
-     "congruent2 intrel intrel
-        (%p1 p2. (%(x,y). (%(u,v).
-                    intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)"
+     "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
+      respects2 intrel"
 apply (rule equiv_intrel [THEN congruent2_commuteI])
  apply (force simp add: mult_ac, clarify) 
 apply (simp add: congruent_def mult_ac)  
@@ -393,7 +392,7 @@
 
 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
 proof -
-  have "congruent intrel (\<lambda>(x,y). {x-y})"
+  have "(\<lambda>(x,y). {x-y}) respects intrel"
     by (simp add: congruent_def, arith) 
   thus ?thesis
     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
@@ -695,7 +694,7 @@
 
 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
 proof -
-  have "congruent intrel (\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) })"
+  have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
     by (simp add: congruent_def compare_rls of_nat_add [symmetric]
             del: of_nat_add) 
   thus ?thesis
diff -r 33a08cfc3ae5 -r 2b5da07a0b89 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed Sep 01 15:04:01 2004 +0200
@@ -154,8 +154,8 @@
      "Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) =
       Abs_Real (realrel``{(x+u, y+v)})"
 proof -
-  have "congruent2 realrel realrel
-        (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)"
+  have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)
+        respects2 realrel"
     by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
   thus ?thesis
     by (simp add: real_add_def UN_UN_split_split_eq
@@ -181,7 +181,7 @@
 
 lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
 proof -
-  have "congruent realrel (\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})})"
+  have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
     by (simp add: congruent_def preal_add_commute) 
   thus ?thesis
     by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
@@ -203,9 +203,10 @@
 done
 
 lemma real_mult_congruent2:
-    "congruent2 realrel realrel (%p1 p2.
+    "(%p1 p2.
         (%(x1,y1). (%(x2,y2). 
-          { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)"
+          { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)
+     respects2 realrel"
 apply (rule congruent2_commuteI [OF equiv_realrel], clarify)
 apply (simp add: preal_mult_commute preal_add_commute)
 apply (auto simp add: real_mult_congruent2_lemma)