author haftmann Mon Nov 29 22:41:17 2010 +0100 (2010-11-29) changeset 40817 781da1e8808c parent 40816 19c492929756 child 40818 b117df72e56b
replaced slightly odd locale congruent2 by plain definition
 src/HOL/Equiv_Relations.thy file | annotate | diff | revisions src/HOL/RealDef.thy file | annotate | diff | revisions
```     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.7 -  apply (erule congruent2.congruent2 [OF f])
2.8 +  apply (erule congruent2D [OF f])
2.9    apply (rule refl_onD [OF refl_realrel])