author haftmann Mon Nov 29 22:32:06 2010 +0100 (2010-11-29) changeset 40816 19c492929756 parent 40815 6e2d17cc0d1d child 40817 781da1e8808c
replaced slightly odd locale congruent by plain definition
 src/HOL/Equiv_Relations.thy file | annotate | diff | revisions src/HOL/Rat.thy file | annotate | diff | revisions src/HOL/RealDef.thy file | annotate | diff | revisions
```     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"
```
```     2.1 --- a/src/HOL/Rat.thy	Mon Nov 29 13:44:54 2010 +0100
2.2 +++ b/src/HOL/Rat.thy	Mon Nov 29 22:32:06 2010 +0100
2.3 @@ -781,7 +781,7 @@
2.4
2.5  lemma of_rat_congruent:
2.6    "(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel"
2.7 -apply (rule congruent.intro)
2.8 +apply (rule congruentI)
2.9  apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
2.10  apply (simp only: of_int_mult [symmetric])
2.11  done
```
```     3.1 --- a/src/HOL/RealDef.thy	Mon Nov 29 13:44:54 2010 +0100
3.2 +++ b/src/HOL/RealDef.thy	Mon Nov 29 22:32:06 2010 +0100
3.3 @@ -358,7 +358,7 @@
3.4    apply (simp add: quotientI X)
3.5    apply (rule the_equality)
3.6    apply clarsimp
3.7 -  apply (erule congruent.congruent [OF f])
3.8 +  apply (erule congruentD [OF f])
3.9    apply (erule bspec)
3.10    apply simp
3.11    apply (rule refl_onD [OF refl_realrel])
3.12 @@ -370,7 +370,7 @@
3.13    assumes X: "cauchy X" and Y: "cauchy Y"
3.14    shows "real_case (\<lambda>X. real_case (\<lambda>Y. f X Y) (Real Y)) (Real X) = f X Y"
3.15   apply (subst real_case_1 [OF _ X])
3.16 -  apply (rule congruent.intro)
3.17 +  apply (rule congruentI)
3.18    apply (subst real_case_1 [OF _ Y])
3.19     apply (rule congruent2_implies_congruent [OF equiv_realrel f])
3.21 @@ -416,7 +416,7 @@
3.22
3.23  lemma minus_respects_realrel:
3.24    "(\<lambda>X. Real (\<lambda>n. - X n)) respects realrel"
3.25 -proof (rule congruent.intro)
3.26 +proof (rule congruentI)
3.27    fix X Y assume "(X, Y) \<in> realrel"
3.28    hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
3.29      unfolding realrel_def by simp_all
3.30 @@ -492,7 +492,7 @@
3.31  lemma inverse_respects_realrel:
3.32    "(\<lambda>X. if vanishes X then c else Real (\<lambda>n. inverse (X n))) respects realrel"
3.33      (is "?inv respects realrel")
3.34 -proof (rule congruent.intro)
3.35 +proof (rule congruentI)
3.36    fix X Y assume "(X, Y) \<in> realrel"
3.37    hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
3.38      unfolding realrel_def by simp_all
3.39 @@ -622,7 +622,7 @@
3.40    assumes sym: "sym r"
3.41    assumes P: "\<And>x y. (x, y) \<in> r \<Longrightarrow> P x \<Longrightarrow> P y"
3.42    shows "P respects r"
3.43 -apply (rule congruent.intro)
3.44 +apply (rule congruentI)
3.45  apply (rule iffI)
3.46  apply (erule (1) P)
3.47  apply (erule (1) P [OF symD [OF sym]])
```