replaced slightly odd locale congruent2 by plain definition
authorhaftmann
Mon Nov 29 22:41:17 2010 +0100 (2010-11-29)
changeset 40817781da1e8808c
parent 40816 19c492929756
child 40818 b117df72e56b
replaced slightly odd locale congruent2 by plain definition
src/HOL/Equiv_Relations.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Equiv_Relations.thy	Mon Nov 29 22:32:06 2010 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Nov 29 22:41:17 2010 +0100
     1.3 @@ -164,16 +164,16 @@
     1.4  
     1.5  text{*A congruence-preserving function*}
     1.6  
     1.7 -definition congruent where
     1.8 -  "congruent r f \<longleftrightarrow> (\<forall>y z. (y, z) \<in> r \<longrightarrow> f y = f z)"
     1.9 +definition congruent :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"  where
    1.10 +  "congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)"
    1.11  
    1.12  lemma congruentI:
    1.13    "(\<And>y z. (y, z) \<in> r \<Longrightarrow> f y = f z) \<Longrightarrow> congruent r f"
    1.14 -  by (simp add: congruent_def)
    1.15 +  by (auto simp add: congruent_def)
    1.16  
    1.17  lemma congruentD:
    1.18    "congruent r f \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> f y = f z"
    1.19 -  by (simp add: congruent_def)
    1.20 +  by (auto simp add: congruent_def)
    1.21  
    1.22  abbreviation
    1.23    RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"
    1.24 @@ -228,10 +228,18 @@
    1.25  subsection {* Defining binary operations upon equivalence classes *}
    1.26  
    1.27  text{*A congruence-preserving function of two arguments*}
    1.28 -locale congruent2 =
    1.29 -  fixes r1 and r2 and f
    1.30 -  assumes congruent2:
    1.31 -    "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
    1.32 +
    1.33 +definition congruent2 :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<times> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
    1.34 +  "congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)"
    1.35 +
    1.36 +lemma congruent2I':
    1.37 +  assumes "\<And>y1 z1 y2 z2. (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
    1.38 +  shows "congruent2 r1 r2 f"
    1.39 +  using assms by (auto simp add: congruent2_def)
    1.40 +
    1.41 +lemma congruent2D:
    1.42 +  "congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
    1.43 +  using assms by (auto simp add: congruent2_def)
    1.44  
    1.45  text{*Abbreviation for the common case where the relations are identical*}
    1.46  abbreviation
     2.1 --- a/src/HOL/RealDef.thy	Mon Nov 29 22:32:06 2010 +0100
     2.2 +++ b/src/HOL/RealDef.thy	Mon Nov 29 22:41:17 2010 +0100
     2.3 @@ -377,7 +377,7 @@
     2.4    apply (subst real_case_1 [OF _ Y])
     2.5     apply (rule congruent2_implies_congruent [OF equiv_realrel f])
     2.6     apply (simp add: realrel_def)
     2.7 -  apply (erule congruent2.congruent2 [OF f])
     2.8 +  apply (erule congruent2D [OF f])
     2.9    apply (rule refl_onD [OF refl_realrel])
    2.10    apply (simp add: Y)
    2.11    apply (rule real_case_1 [OF _ Y])