# HG changeset patch
# User haftmann
# Date 1291066326 -3600
# Node ID 19c4929297560dcbad2e61540ae986c6ef927e8e
# Parent  6e2d17cc0d1defd386e563fe4f08e81df80ea043
replaced slightly odd locale congruent by plain definition

diff -r 6e2d17cc0d1d -r 19c492929756 src/HOL/Equiv_Relations.thy
--- 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"
diff -r 6e2d17cc0d1d -r 19c492929756 src/HOL/Rat.thy
--- 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
diff -r 6e2d17cc0d1d -r 19c492929756 src/HOL/RealDef.thy
--- 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]])