new "respects" syntax for quotienting
authorpaulson
Wed Sep 01 15:04:01 2004 +0200 (2004-09-01)
changeset 151692b5da07a0b89
parent 15168 33a08cfc3ae5
child 15170 e7d4d3314f4c
new "respects" syntax for quotienting
src/HOL/Complex/CStar.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/NatStar.thy
src/HOL/Hyperreal/Star.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Integ/Equiv.thy
src/HOL/Integ/IntDef.thy
src/HOL/Real/RealDef.thy
     1.1 --- a/src/HOL/Complex/CStar.thy	Wed Sep 01 15:03:41 2004 +0200
     1.2 +++ b/src/HOL/Complex/CStar.thy	Wed Sep 01 15:04:01 2004 +0200
     1.3 @@ -206,9 +206,8 @@
     1.4  by (simp add: starfunCR_n_def starfunCR_def)
     1.5  
     1.6  lemma starfunC_congruent:
     1.7 -      "congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})"
     1.8 -apply (auto simp add: hcomplexrel_iff congruent_def, ultra)
     1.9 -done
    1.10 +      "(%X. hcomplexrel``{%n. f (X n)}) respects hcomplexrel"
    1.11 +by (auto simp add: hcomplexrel_iff congruent_def, ultra)
    1.12  
    1.13  (* f::complex => complex *)
    1.14  lemma starfunC:
    1.15 @@ -508,7 +507,7 @@
    1.16  subsection{*Internal Functions - Some Redundancy With *Fc* Now*}
    1.17  
    1.18  lemma starfunC_n_congruent:
    1.19 -      "congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})"
    1.20 +      "(%X. hcomplexrel``{%n. f n (X n)}) respects hcomplexrel"
    1.21  by (auto simp add: congruent_def hcomplexrel_iff, ultra)
    1.22  
    1.23  lemma starfunC_n:
     2.1 --- a/src/HOL/Complex/NSComplex.thy	Wed Sep 01 15:03:41 2004 +0200
     2.2 +++ b/src/HOL/Complex/NSComplex.thy	Wed Sep 01 15:04:01 2004 +0200
     2.3 @@ -283,7 +283,7 @@
     2.4  subsection{*Additive Inverse on Nonstandard Complex Numbers*}
     2.5  
     2.6  lemma hcomplex_minus_congruent:
     2.7 -     "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
     2.8 +     "(%X. hcomplexrel `` {%n. - (X n)}) respects hcomplexrel"
     2.9  by (simp add: congruent_def)
    2.10  
    2.11  lemma hcomplex_minus:
     3.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Wed Sep 01 15:03:41 2004 +0200
     3.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Sep 01 15:04:01 2004 +0200
     3.3 @@ -342,8 +342,7 @@
     3.4  
     3.5  subsection{*Additive inverse on @{typ hypreal}*}
     3.6  
     3.7 -lemma hypreal_minus_congruent: 
     3.8 -  "congruent hyprel (%X. hyprel``{%n. - (X n)})"
     3.9 +lemma hypreal_minus_congruent: "(%X. hyprel``{%n. - (X n)}) respects hyprel"
    3.10  by (force simp add: congruent_def)
    3.11  
    3.12  lemma hypreal_minus: 
    3.13 @@ -397,7 +396,7 @@
    3.14  subsection{*Multiplicative Inverse on @{typ hypreal} *}
    3.15  
    3.16  lemma hypreal_inverse_congruent: 
    3.17 -  "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})"
    3.18 +  "(%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)}) respects hyprel"
    3.19  by (auto simp add: congruent_def, ultra)
    3.20  
    3.21  lemma hypreal_inverse: 
     4.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Wed Sep 01 15:03:41 2004 +0200
     4.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Wed Sep 01 15:04:01 2004 +0200
     4.3 @@ -136,7 +136,7 @@
     4.4  subsection{*Hypernat Addition*}
     4.5  
     4.6  lemma hypnat_add_congruent2:
     4.7 -     "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
     4.8 +     "(%X Y. hypnatrel``{%n. X n + Y n}) respects2 hypnatrel"
     4.9  by (simp add: congruent2_def, auto, ultra)
    4.10  
    4.11  lemma hypnat_add:
    4.12 @@ -170,7 +170,7 @@
    4.13  
    4.14  
    4.15  lemma hypnat_minus_congruent2:
    4.16 -    "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
    4.17 +    "(%X Y. hypnatrel``{%n. X n - Y n}) respects2 hypnatrel"
    4.18  by (simp add: congruent2_def, auto, ultra)
    4.19  
    4.20  lemma hypnat_minus:
    4.21 @@ -238,7 +238,7 @@
    4.22  subsection{*Hyperreal Multiplication*}
    4.23  
    4.24  lemma hypnat_mult_congruent2:
    4.25 -    "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
    4.26 +    "(%X Y. hypnatrel``{%n. X n * Y n}) respects2 hypnatrel"
    4.27  by (simp add: congruent2_def, auto, ultra)
    4.28  
    4.29  lemma hypnat_mult:
     5.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Wed Sep 01 15:03:41 2004 +0200
     5.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Wed Sep 01 15:04:01 2004 +0200
     5.3 @@ -114,12 +114,8 @@
     5.4  
     5.5  subsection{*Powers with Hypernatural Exponents*}
     5.6  
     5.7 -lemma hyperpow_congruent:
     5.8 -     "congruent hyprel
     5.9 -     (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"
    5.10 -apply (unfold congruent_def)
    5.11 -apply (auto intro!: ext, fuf+)
    5.12 -done
    5.13 +lemma hyperpow_congruent: "(%X Y. hyprel``{%n. (X n ^ Y n)}) respects hyprel"
    5.14 +by (auto simp add: congruent_def intro!: ext, fuf+)
    5.15  
    5.16  lemma hyperpow:
    5.17    "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
     6.1 --- a/src/HOL/Hyperreal/NatStar.thy	Wed Sep 01 15:03:41 2004 +0200
     6.2 +++ b/src/HOL/Hyperreal/NatStar.thy	Wed Sep 01 15:04:01 2004 +0200
     6.3 @@ -185,8 +185,7 @@
     6.4  lemma starfunNat2_n_starfunNat2: "\<forall>n. (F n = f) ==> *fNat2n* F = *fNat2* f"
     6.5  by (simp add: starfunNat2_n_def starfunNat2_def)
     6.6  
     6.7 -lemma starfunNat_congruent:
     6.8 -      "congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})"
     6.9 +lemma starfunNat_congruent: "(%X. hypnatrel``{%n. f (X n)}) respects hypnatrel"
    6.10  apply (simp add: congruent_def, safe)
    6.11  apply (ultra+)
    6.12  done
    6.13 @@ -396,10 +395,8 @@
    6.14  text{*Internal functions - some redundancy with *fNat* now*}
    6.15  
    6.16  lemma starfunNat_n_congruent:
    6.17 -      "congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})"
    6.18 -apply (simp add: congruent_def, safe)
    6.19 -apply (ultra+)
    6.20 -done
    6.21 +      "(%X. hypnatrel``{%n. f n (X n)}) respects hypnatrel"
    6.22 +by (auto simp add: congruent_def, ultra+)
    6.23  
    6.24  lemma starfunNat_n:
    6.25       "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
     7.1 --- a/src/HOL/Hyperreal/Star.thy	Wed Sep 01 15:03:41 2004 +0200
     7.2 +++ b/src/HOL/Hyperreal/Star.thy	Wed Sep 01 15:04:01 2004 +0200
     7.3 @@ -53,9 +53,7 @@
     7.4  apply (blast intro: LeastI)
     7.5  done
     7.6  
     7.7 -(*------------------------------------------------------------
     7.8 -    Properties of the *-transform applied to sets of reals
     7.9 - ------------------------------------------------------------*)
    7.10 +subsection{*Properties of the Star-transform Applied to Sets of Reals*}
    7.11  
    7.12  lemma STAR_real_set: "*s*(UNIV::real set) = (UNIV::hypreal set)"
    7.13  by (simp add: starset_def)
    7.14 @@ -148,10 +146,8 @@
    7.15  lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
    7.16  by (blast dest: STAR_subset)
    7.17  
    7.18 -(*------------------------------------------------------------------
    7.19 -   Nonstandard extension of a set (defined using a constant
    7.20 -   sequence) as a special case of an internal set
    7.21 - -----------------------------------------------------------------*)
    7.22 +text{*Nonstandard extension of a set (defined using a constant
    7.23 +   sequence) as a special case of an internal set*}
    7.24  
    7.25  lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
    7.26  by (simp add: starset_n_def starset_def)
    7.27 @@ -197,11 +193,9 @@
    7.28  apply (auto, ultra)
    7.29  done
    7.30  
    7.31 -(*-----------------------------------------------------------------------
    7.32 -    Nonstandard extension of functions- congruence
    7.33 - -----------------------------------------------------------------------*)
    7.34 +text{*Nonstandard extension of functions*}
    7.35  
    7.36 -lemma starfun_congruent: "congruent hyprel (%X. hyprel``{%n. f (X n)})"
    7.37 +lemma starfun_congruent: "(%X. hyprel``{%n. f (X n)}) respects hyprel"
    7.38  by (simp add: congruent_def, auto, ultra)
    7.39  
    7.40  lemma starfun:
    7.41 @@ -272,9 +266,7 @@
    7.42  apply (simp (no_asm) add: starfun_o2)
    7.43  done
    7.44  
    7.45 -(*--------------------------------------
    7.46 -  NS extension of constant function
    7.47 - --------------------------------------*)
    7.48 +text{*NS extension of constant function*}
    7.49  lemma starfun_const_fun: "( *f* (%x. k)) xa = hypreal_of_real  k"
    7.50  apply (cases xa)
    7.51  apply (auto simp add: starfun hypreal_of_real_def)
    7.52 @@ -282,9 +274,7 @@
    7.53  
    7.54  declare starfun_const_fun [simp]
    7.55  
    7.56 -(*----------------------------------------------------
    7.57 -   the NS extension of the identity function
    7.58 - ----------------------------------------------------*)
    7.59 +text{*the NS extension of the identity function*}
    7.60  
    7.61  lemma starfun_Idfun_approx: "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real  a"
    7.62  apply (cases x)
    7.63 @@ -297,9 +287,7 @@
    7.64  done
    7.65  declare starfun_Id [simp]
    7.66  
    7.67 -(*----------------------------------------------------------------------
    7.68 -      the *-function is a (nonstandard) extension of the function
    7.69 - ----------------------------------------------------------------------*)
    7.70 +text{*The Star-function is a (nonstandard) extension of the function*}
    7.71  
    7.72  lemma is_starext_starfun: "is_starext ( *f* f) f"
    7.73  apply (simp add: is_starext_def, auto)
    7.74 @@ -308,9 +296,7 @@
    7.75  apply (auto intro!: bexI simp add: starfun)
    7.76  done
    7.77  
    7.78 -(*----------------------------------------------------------------------
    7.79 -     Any nonstandard extension is in fact the *-function
    7.80 - ----------------------------------------------------------------------*)
    7.81 +text{*Any nonstandard extension is in fact the Star-function*}
    7.82  
    7.83  lemma is_starfun_starext: "is_starext F f ==> F = *f* f"
    7.84  apply (simp add: is_starext_def)
    7.85 @@ -324,11 +310,9 @@
    7.86  lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)"
    7.87  by (blast intro: is_starfun_starext is_starext_starfun)
    7.88  
    7.89 -(*--------------------------------------------------------
    7.90 -   extented function has same solution as its standard
    7.91 +text{*extented function has same solution as its standard
    7.92     version for real arguments. i.e they are the same
    7.93 -   for all real arguments
    7.94 - -------------------------------------------------------*)
    7.95 +   for all real arguments*}
    7.96  lemma starfun_eq: "( *f* f) (hypreal_of_real a) = hypreal_of_real (f a)"
    7.97  by (auto simp add: starfun hypreal_of_real_def)
    7.98  
    7.99 @@ -360,10 +344,8 @@
   7.100  apply (auto intro: approx_add)
   7.101  done
   7.102  
   7.103 -(*----------------------------------------------------
   7.104 -    Examples: hrabs is nonstandard extension of rabs
   7.105 -              inverse is nonstandard extension of inverse
   7.106 - ---------------------------------------------------*)
   7.107 +text{*Examples: hrabs is nonstandard extension of rabs
   7.108 +              inverse is nonstandard extension of inverse*}
   7.109  
   7.110  (* can be proved easily using theorem "starfun" and *)
   7.111  (* properties of ultrafilter as for inverse below we  *)
   7.112 @@ -393,10 +375,8 @@
   7.113  apply (auto intro: FreeUltrafilterNat_subset dest!: FreeUltrafilterNat_Compl_mem simp add: starfun hypreal_inverse hypreal_zero_def)
   7.114  done
   7.115  
   7.116 -(*-------------------------------------------------------------
   7.117 -    General lemma/theorem needed for proofs in elementary
   7.118 -    topology of the reals
   7.119 - ------------------------------------------------------------*)
   7.120 +text{*General lemma/theorem needed for proofs in elementary
   7.121 +    topology of the reals*}
   7.122  lemma starfun_mem_starset:
   7.123        "( *f* f) x : *s* A ==> x : *s* {x. f x  \<in> A}"
   7.124  apply (simp add: starset_def)
   7.125 @@ -407,22 +387,18 @@
   7.126  apply (auto, ultra)
   7.127  done
   7.128  
   7.129 -(*------------------------------------------------------------
   7.130 -   Alternative definition for hrabs with rabs function
   7.131 +text{*Alternative definition for hrabs with rabs function
   7.132     applied entrywise to equivalence class representative.
   7.133 -   This is easily proved using starfun and ns extension thm
   7.134 - ------------------------------------------------------------*)
   7.135 +   This is easily proved using starfun and ns extension thm*}
   7.136  lemma hypreal_hrabs: "abs (Abs_hypreal (hyprel `` {X})) =
   7.137                    Abs_hypreal(hyprel `` {%n. abs (X n)})"
   7.138  apply (simp (no_asm) add: starfun_rabs_hrabs [symmetric] starfun)
   7.139  done
   7.140  
   7.141 -(*----------------------------------------------------------------
   7.142 -   nonstandard extension of set through nonstandard extension
   7.143 +text{*nonstandard extension of set through nonstandard extension
   7.144     of rabs function i.e hrabs. A more general result should be
   7.145     where we replace rabs by some arbitrary function f and hrabs
   7.146 -   by its NS extenson ( *f* f). See second NS set extension below.
   7.147 - ----------------------------------------------------------------*)
   7.148 +   by its NS extenson. See second NS set extension below.*}
   7.149  lemma STAR_rabs_add_minus:
   7.150     "*s* {x. abs (x + - y) < r} =
   7.151       {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
   7.152 @@ -439,11 +415,9 @@
   7.153  apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less starfun, ultra)
   7.154  done
   7.155  
   7.156 -(*-------------------------------------------------------------------
   7.157 -   Another characterization of Infinitesimal and one of @= relation.
   7.158 +text{*Another characterization of Infinitesimal and one of @= relation.
   7.159     In this theory since hypreal_hrabs proved here. (To Check:) Maybe
   7.160 -   move both if possible?
   7.161 - -------------------------------------------------------------------*)
   7.162 +   move both if possible?*}
   7.163  lemma Infinitesimal_FreeUltrafilterNat_iff2:
   7.164       "(x \<in> Infinitesimal) =
   7.165        (\<exists>X \<in> Rep_hypreal(x).
     8.1 --- a/src/HOL/Induct/QuoDataType.thy	Wed Sep 01 15:03:41 2004 +0200
     8.2 +++ b/src/HOL/Induct/QuoDataType.thy	Wed Sep 01 15:04:01 2004 +0200
     8.3 @@ -166,7 +166,7 @@
     8.4  
     8.5  
     8.6  text{*All equivalence classes belong to set of representatives*}
     8.7 -lemma msgrel_in_integ [simp]: "msgrel``{U} \<in> Msg"
     8.8 +lemma [simp]: "msgrel``{U} \<in> Msg"
     8.9  by (auto simp add: Msg_def quotient_def intro: msgrel_refl)
    8.10  
    8.11  lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"
    8.12 @@ -185,7 +185,7 @@
    8.13  lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) = 
    8.14                Abs_Msg (msgrel``{MPAIR U V})"
    8.15  proof -
    8.16 -  have "congruent2 msgrel msgrel (\<lambda>U V. msgrel `` {MPAIR U V})"
    8.17 +  have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"
    8.18      by (simp add: congruent2_def msgrel.MPAIR)
    8.19    thus ?thesis
    8.20      by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
    8.21 @@ -193,7 +193,7 @@
    8.22  
    8.23  lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
    8.24  proof -
    8.25 -  have "congruent msgrel (\<lambda>U. msgrel `` {CRYPT K U})"
    8.26 +  have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"
    8.27      by (simp add: congruent_def msgrel.CRYPT)
    8.28    thus ?thesis
    8.29      by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
    8.30 @@ -202,7 +202,7 @@
    8.31  lemma Decrypt:
    8.32       "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
    8.33  proof -
    8.34 -  have "congruent msgrel (\<lambda>U. msgrel `` {DECRYPT K U})"
    8.35 +  have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"
    8.36      by (simp add: congruent_def msgrel.DECRYPT)
    8.37    thus ?thesis
    8.38      by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
    8.39 @@ -230,7 +230,7 @@
    8.40    nonces :: "msg \<Rightarrow> nat set"
    8.41     "nonces X == \<Union>U \<in> Rep_Msg X. freenonces U"
    8.42  
    8.43 -lemma nonces_congruent: "congruent msgrel freenonces"
    8.44 +lemma nonces_congruent: "freenonces respects msgrel"
    8.45  by (simp add: congruent_def msgrel_imp_eq_freenonces) 
    8.46  
    8.47  
    8.48 @@ -265,7 +265,7 @@
    8.49    left :: "msg \<Rightarrow> msg"
    8.50     "left X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
    8.51  
    8.52 -lemma left_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeleft U})"
    8.53 +lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
    8.54  by (simp add: congruent_def msgrel_imp_eqv_freeleft) 
    8.55  
    8.56  text{*Now prove the four equations for @{term left}*}
    8.57 @@ -299,7 +299,7 @@
    8.58    right :: "msg \<Rightarrow> msg"
    8.59     "right X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
    8.60  
    8.61 -lemma right_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeright U})"
    8.62 +lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
    8.63  by (simp add: congruent_def msgrel_imp_eqv_freeright) 
    8.64  
    8.65  text{*Now prove the four equations for @{term right}*}
    8.66 @@ -433,7 +433,7 @@
    8.67    discrim :: "msg \<Rightarrow> int"
    8.68     "discrim X == contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
    8.69  
    8.70 -lemma discrim_congruent: "congruent msgrel (\<lambda>U. {freediscrim U})"
    8.71 +lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
    8.72  by (simp add: congruent_def msgrel_imp_eq_freediscrim) 
    8.73  
    8.74  text{*Now prove the four equations for @{term discrim}*}
     9.1 --- a/src/HOL/Integ/Equiv.thy	Wed Sep 01 15:03:41 2004 +0200
     9.2 +++ b/src/HOL/Integ/Equiv.thy	Wed Sep 01 15:04:01 2004 +0200
     9.3 @@ -151,12 +151,19 @@
     9.4    fixes r and f
     9.5    assumes congruent: "(y,z) \<in> r ==> f y = f z"
     9.6  
     9.7 +syntax
     9.8 +  RESPECTS ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects" 80)
     9.9 +
    9.10 +translations
    9.11 +  "f respects r" == "congruent r f"
    9.12 +
    9.13 +
    9.14  lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
    9.15    -- {* lemma required to prove @{text UN_equiv_class} *}
    9.16    by auto
    9.17  
    9.18  lemma UN_equiv_class:
    9.19 -  "equiv A r ==> congruent r f ==> a \<in> A
    9.20 +  "equiv A r ==> f respects r ==> a \<in> A
    9.21      ==> (\<Union>x \<in> r``{a}. f x) = f a"
    9.22    -- {* Conversion rule *}
    9.23    apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)
    9.24 @@ -165,7 +172,7 @@
    9.25    done
    9.26  
    9.27  lemma UN_equiv_class_type:
    9.28 -  "equiv A r ==> congruent r f ==> X \<in> A//r ==>
    9.29 +  "equiv A r ==> f respects r ==> X \<in> A//r ==>
    9.30      (!!x. x \<in> A ==> f x \<in> B) ==> (\<Union>x \<in> X. f x) \<in> B"
    9.31    apply (unfold quotient_def)
    9.32    apply clarify
    9.33 @@ -180,7 +187,7 @@
    9.34  *}
    9.35  
    9.36  lemma UN_equiv_class_inject:
    9.37 -  "equiv A r ==> congruent r f ==>
    9.38 +  "equiv A r ==> f respects r ==>
    9.39      (\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) ==> X \<in> A//r ==> Y \<in> A//r
    9.40      ==> (!!x y. x \<in> A ==> y \<in> A ==> f x = f y ==> (x, y) \<in> r)
    9.41      ==> X = Y"
    9.42 @@ -203,6 +210,13 @@
    9.43    assumes congruent2:
    9.44      "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
    9.45  
    9.46 +text{*Abbreviation for the common case where the relations are identical*}
    9.47 +syntax
    9.48 +  RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects2 " 80)
    9.49 +
    9.50 +translations
    9.51 +  "f respects2 r" => "congruent2 r r f"
    9.52 +
    9.53  lemma congruent2_implies_congruent:
    9.54      "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
    9.55    by (unfold congruent_def congruent2_def equiv_def refl_def) blast
    9.56 @@ -258,7 +272,7 @@
    9.57    assumes equivA: "equiv A r"
    9.58      and commute: "!!y z. y \<in> A ==> z \<in> A ==> f y z = f z y"
    9.59      and congt: "!!y z w. w \<in> A ==> (y,z) \<in> r ==> f w y = f w z"
    9.60 -  shows "congruent2 r r f"
    9.61 +  shows "f respects2 r"
    9.62    apply (rule congruent2I [OF equivA equivA])
    9.63     apply (rule commute [THEN trans])
    9.64       apply (rule_tac [3] commute [THEN trans, symmetric])
    9.65 @@ -270,7 +284,7 @@
    9.66  
    9.67  subsection {* Cardinality results *}
    9.68  
    9.69 -text {* (suggested by Florian Kammüller) *}
    9.70 +text {*Suggested by Florian Kammüller*}
    9.71  
    9.72  lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
    9.73    -- {* recall @{thm equiv_type} *}
    10.1 --- a/src/HOL/Integ/IntDef.thy	Wed Sep 01 15:03:41 2004 +0200
    10.2 +++ b/src/HOL/Integ/IntDef.thy	Wed Sep 01 15:04:01 2004 +0200
    10.3 @@ -110,7 +110,7 @@
    10.4  
    10.5  lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
    10.6  proof -
    10.7 -  have "congruent intrel (\<lambda>(x,y). intrel``{(y,x)})"
    10.8 +  have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
    10.9      by (simp add: congruent_def) 
   10.10    thus ?thesis
   10.11      by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
   10.12 @@ -129,8 +129,8 @@
   10.13       "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
   10.14        Abs_Integ (intrel``{(x+u, y+v)})"
   10.15  proof -
   10.16 -  have "congruent2 intrel intrel
   10.17 -        (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)"
   10.18 +  have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
   10.19 +        respects2 intrel"
   10.20      by (simp add: congruent2_def)
   10.21    thus ?thesis
   10.22      by (simp add: add_int_def UN_UN_split_split_eq
   10.23 @@ -183,9 +183,8 @@
   10.24  
   10.25  text{*Congruence property for multiplication*}
   10.26  lemma mult_congruent2:
   10.27 -     "congruent2 intrel intrel
   10.28 -        (%p1 p2. (%(x,y). (%(u,v).
   10.29 -                    intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)"
   10.30 +     "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
   10.31 +      respects2 intrel"
   10.32  apply (rule equiv_intrel [THEN congruent2_commuteI])
   10.33   apply (force simp add: mult_ac, clarify) 
   10.34  apply (simp add: congruent_def mult_ac)  
   10.35 @@ -393,7 +392,7 @@
   10.36  
   10.37  lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
   10.38  proof -
   10.39 -  have "congruent intrel (\<lambda>(x,y). {x-y})"
   10.40 +  have "(\<lambda>(x,y). {x-y}) respects intrel"
   10.41      by (simp add: congruent_def, arith) 
   10.42    thus ?thesis
   10.43      by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
   10.44 @@ -695,7 +694,7 @@
   10.45  
   10.46  lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
   10.47  proof -
   10.48 -  have "congruent intrel (\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) })"
   10.49 +  have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
   10.50      by (simp add: congruent_def compare_rls of_nat_add [symmetric]
   10.51              del: of_nat_add) 
   10.52    thus ?thesis
    11.1 --- a/src/HOL/Real/RealDef.thy	Wed Sep 01 15:03:41 2004 +0200
    11.2 +++ b/src/HOL/Real/RealDef.thy	Wed Sep 01 15:04:01 2004 +0200
    11.3 @@ -154,8 +154,8 @@
    11.4       "Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) =
    11.5        Abs_Real (realrel``{(x+u, y+v)})"
    11.6  proof -
    11.7 -  have "congruent2 realrel realrel
    11.8 -        (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)"
    11.9 +  have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)
   11.10 +        respects2 realrel"
   11.11      by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
   11.12    thus ?thesis
   11.13      by (simp add: real_add_def UN_UN_split_split_eq
   11.14 @@ -181,7 +181,7 @@
   11.15  
   11.16  lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
   11.17  proof -
   11.18 -  have "congruent realrel (\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})})"
   11.19 +  have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
   11.20      by (simp add: congruent_def preal_add_commute) 
   11.21    thus ?thesis
   11.22      by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
   11.23 @@ -203,9 +203,10 @@
   11.24  done
   11.25  
   11.26  lemma real_mult_congruent2:
   11.27 -    "congruent2 realrel realrel (%p1 p2.
   11.28 +    "(%p1 p2.
   11.29          (%(x1,y1). (%(x2,y2). 
   11.30 -          { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)"
   11.31 +          { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)
   11.32 +     respects2 realrel"
   11.33  apply (rule congruent2_commuteI [OF equiv_realrel], clarify)
   11.34  apply (simp add: preal_mult_commute preal_add_commute)
   11.35  apply (auto simp add: real_mult_congruent2_lemma)