src/HOL/Equiv_Relations.thy
changeset 30198 922f944f03b2
parent 29655 ac31940cfb69
child 35216 7641e8d831d2
     1.1 --- a/src/HOL/Equiv_Relations.thy	Mon Mar 02 08:26:03 2009 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Mar 02 16:53:55 2009 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  locale equiv =
     1.6    fixes A and r
     1.7 -  assumes refl: "refl A r"
     1.8 +  assumes refl_on: "refl_on A r"
     1.9      and sym: "sym r"
    1.10      and trans: "trans r"
    1.11  
    1.12 @@ -27,21 +27,21 @@
    1.13      "sym r ==> trans r ==> r\<inverse> O r \<subseteq> r"
    1.14    by (unfold trans_def sym_def converse_def) blast
    1.15  
    1.16 -lemma refl_comp_subset: "refl A r ==> r \<subseteq> r\<inverse> O r"
    1.17 -  by (unfold refl_def) blast
    1.18 +lemma refl_on_comp_subset: "refl_on A r ==> r \<subseteq> r\<inverse> O r"
    1.19 +  by (unfold refl_on_def) blast
    1.20  
    1.21  lemma equiv_comp_eq: "equiv A r ==> r\<inverse> O r = r"
    1.22    apply (unfold equiv_def)
    1.23    apply clarify
    1.24    apply (rule equalityI)
    1.25 -   apply (iprover intro: sym_trans_comp_subset refl_comp_subset)+
    1.26 +   apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+
    1.27    done
    1.28  
    1.29  text {* Second half. *}
    1.30  
    1.31  lemma comp_equivI:
    1.32      "r\<inverse> O r = r ==> Domain r = A ==> equiv A r"
    1.33 -  apply (unfold equiv_def refl_def sym_def trans_def)
    1.34 +  apply (unfold equiv_def refl_on_def sym_def trans_def)
    1.35    apply (erule equalityE)
    1.36    apply (subgoal_tac "\<forall>x y. (x, y) \<in> r --> (y, x) \<in> r")
    1.37     apply fast
    1.38 @@ -63,12 +63,12 @@
    1.39    done
    1.40  
    1.41  lemma equiv_class_self: "equiv A r ==> a \<in> A ==> a \<in> r``{a}"
    1.42 -  by (unfold equiv_def refl_def) blast
    1.43 +  by (unfold equiv_def refl_on_def) blast
    1.44  
    1.45  lemma subset_equiv_class:
    1.46      "equiv A r ==> r``{b} \<subseteq> r``{a} ==> b \<in> A ==> (a,b) \<in> r"
    1.47    -- {* lemma for the next result *}
    1.48 -  by (unfold equiv_def refl_def) blast
    1.49 +  by (unfold equiv_def refl_on_def) blast
    1.50  
    1.51  lemma eq_equiv_class:
    1.52      "r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r"
    1.53 @@ -79,7 +79,7 @@
    1.54    by (unfold equiv_def trans_def sym_def) blast
    1.55  
    1.56  lemma equiv_type: "equiv A r ==> r \<subseteq> A \<times> A"
    1.57 -  by (unfold equiv_def refl_def) blast
    1.58 +  by (unfold equiv_def refl_on_def) blast
    1.59  
    1.60  theorem equiv_class_eq_iff:
    1.61    "equiv A r ==> ((x, y) \<in> r) = (r``{x} = r``{y} & x \<in> A & y \<in> A)"
    1.62 @@ -103,7 +103,7 @@
    1.63    by (unfold quotient_def) blast
    1.64  
    1.65  lemma Union_quotient: "equiv A r ==> Union (A//r) = A"
    1.66 -  by (unfold equiv_def refl_def quotient_def) blast
    1.67 +  by (unfold equiv_def refl_on_def quotient_def) blast
    1.68  
    1.69  lemma quotient_disj:
    1.70    "equiv A r ==> X \<in> A//r ==> Y \<in> A//r ==> X = Y | (X \<inter> Y = {})"
    1.71 @@ -228,7 +228,7 @@
    1.72  
    1.73  lemma congruent2_implies_congruent:
    1.74      "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
    1.75 -  by (unfold congruent_def congruent2_def equiv_def refl_def) blast
    1.76 +  by (unfold congruent_def congruent2_def equiv_def refl_on_def) blast
    1.77  
    1.78  lemma congruent2_implies_congruent_UN:
    1.79    "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \<in> A2 ==>
    1.80 @@ -237,7 +237,7 @@
    1.81    apply clarify
    1.82    apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)
    1.83    apply (simp add: UN_equiv_class congruent2_implies_congruent)
    1.84 -  apply (unfold congruent2_def equiv_def refl_def)
    1.85 +  apply (unfold congruent2_def equiv_def refl_on_def)
    1.86    apply (blast del: equalityI)
    1.87    done
    1.88  
    1.89 @@ -272,7 +272,7 @@
    1.90      ==> congruent2 r1 r2 f"
    1.91    -- {* Suggested by John Harrison -- the two subproofs may be *}
    1.92    -- {* \emph{much} simpler than the direct proof. *}
    1.93 -  apply (unfold congruent2_def equiv_def refl_def)
    1.94 +  apply (unfold congruent2_def equiv_def refl_on_def)
    1.95    apply clarify
    1.96    apply (blast intro: trans)
    1.97    done