src/HOL/Equiv_Relations.thy
 changeset 40816 19c492929756 parent 40815 6e2d17cc0d1d child 40817 781da1e8808c
```     1.1 --- a/src/HOL/Equiv_Relations.thy	Mon Nov 29 13:44:54 2010 +0100
1.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Nov 29 22:32:06 2010 +0100
1.3 @@ -163,9 +163,17 @@
1.4  subsection {* Defining unary operations upon equivalence classes *}
1.5
1.6  text{*A congruence-preserving function*}
1.7 -locale congruent =
1.8 -  fixes r and f
1.9 -  assumes congruent: "(y,z) \<in> r ==> f y = f z"
1.10 +
1.11 +definition congruent where
1.12 +  "congruent r f \<longleftrightarrow> (\<forall>y z. (y, z) \<in> r \<longrightarrow> f y = f z)"
1.13 +
1.14 +lemma congruentI:
1.15 +  "(\<And>y z. (y, z) \<in> r \<Longrightarrow> f y = f z) \<Longrightarrow> congruent r f"
1.16 +  by (simp add: congruent_def)
1.17 +
1.18 +lemma congruentD:
1.19 +  "congruent r f \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> f y = f z"
1.20 +  by (simp add: congruent_def)
1.21
1.22  abbreviation
1.23    RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"
```