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"