--- a/src/HOL/Equiv_Relations.thy Mon Nov 29 13:44:54 2010 +0100
+++ b/src/HOL/Equiv_Relations.thy Mon Nov 29 22:32:06 2010 +0100
@@ -163,9 +163,17 @@
subsection {* Defining unary operations upon equivalence classes *}
text{*A congruence-preserving function*}
-locale congruent =
- fixes r and f
- assumes congruent: "(y,z) \<in> r ==> f y = f z"
+
+definition congruent where
+ "congruent r f \<longleftrightarrow> (\<forall>y z. (y, z) \<in> r \<longrightarrow> f y = f z)"
+
+lemma congruentI:
+ "(\<And>y z. (y, z) \<in> r \<Longrightarrow> f y = f z) \<Longrightarrow> congruent r f"
+ by (simp add: congruent_def)
+
+lemma congruentD:
+ "congruent r f \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> f y = f z"
+ by (simp add: congruent_def)
abbreviation
RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"
--- a/src/HOL/Rat.thy Mon Nov 29 13:44:54 2010 +0100
+++ b/src/HOL/Rat.thy Mon Nov 29 22:32:06 2010 +0100
@@ -781,7 +781,7 @@
lemma of_rat_congruent:
"(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel"
-apply (rule congruent.intro)
+apply (rule congruentI)
apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
apply (simp only: of_int_mult [symmetric])
done
--- a/src/HOL/RealDef.thy Mon Nov 29 13:44:54 2010 +0100
+++ b/src/HOL/RealDef.thy Mon Nov 29 22:32:06 2010 +0100
@@ -358,7 +358,7 @@
apply (simp add: quotientI X)
apply (rule the_equality)
apply clarsimp
- apply (erule congruent.congruent [OF f])
+ apply (erule congruentD [OF f])
apply (erule bspec)
apply simp
apply (rule refl_onD [OF refl_realrel])
@@ -370,7 +370,7 @@
assumes X: "cauchy X" and Y: "cauchy Y"
shows "real_case (\<lambda>X. real_case (\<lambda>Y. f X Y) (Real Y)) (Real X) = f X Y"
apply (subst real_case_1 [OF _ X])
- apply (rule congruent.intro)
+ apply (rule congruentI)
apply (subst real_case_1 [OF _ Y])
apply (rule congruent2_implies_congruent [OF equiv_realrel f])
apply (simp add: realrel_def)
@@ -416,7 +416,7 @@
lemma minus_respects_realrel:
"(\<lambda>X. Real (\<lambda>n. - X n)) respects realrel"
-proof (rule congruent.intro)
+proof (rule congruentI)
fix X Y assume "(X, Y) \<in> realrel"
hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
unfolding realrel_def by simp_all
@@ -492,7 +492,7 @@
lemma inverse_respects_realrel:
"(\<lambda>X. if vanishes X then c else Real (\<lambda>n. inverse (X n))) respects realrel"
(is "?inv respects realrel")
-proof (rule congruent.intro)
+proof (rule congruentI)
fix X Y assume "(X, Y) \<in> realrel"
hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
unfolding realrel_def by simp_all
@@ -622,7 +622,7 @@
assumes sym: "sym r"
assumes P: "\<And>x y. (x, y) \<in> r \<Longrightarrow> P x \<Longrightarrow> P y"
shows "P respects r"
-apply (rule congruent.intro)
+apply (rule congruentI)
apply (rule iffI)
apply (erule (1) P)
apply (erule (1) P [OF symD [OF sym]])