replaced slightly odd locale congruent by plain definition
authorhaftmann
Mon Nov 29 22:32:06 2010 +0100 (2010-11-29)
changeset 4081619c492929756
parent 40815 6e2d17cc0d1d
child 40817 781da1e8808c
replaced slightly odd locale congruent by plain definition
src/HOL/Equiv_Relations.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
     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.20     apply (simp add: realrel_def)
    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]])