src/ZF/EquivClass.thy
author wenzelm
Sun Oct 07 15:49:25 2007 +0200 (2007-10-07)
changeset 24892 c663e675e177
parent 23146 0bc590051d95
child 24893 b8ef7afe3a6b
permissions -rw-r--r--
replaced some 'translations' by 'abbreviation';
     1 (*  Title:      ZF/EquivClass.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 *)
     7 
     8 header{*Equivalence Relations*}
     9 
    10 theory EquivClass imports Trancl Perm begin
    11 
    12 constdefs
    13 
    14   quotient   :: "[i,i]=>i"    (infixl "'/'/" 90)  (*set of equiv classes*)
    15       "A//r == {r``{x} . x:A}"
    16 
    17   congruent  :: "[i,i=>i]=>o"
    18       "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
    19 
    20   congruent2 :: "[i,i,[i,i]=>i]=>o"
    21       "congruent2(r1,r2,b) == ALL y1 z1 y2 z2.
    22            <y1,z1>:r1 --> <y2,z2>:r2 --> b(y1,y2) = b(z1,z2)"
    23 
    24 abbreviation
    25   RESPECTS ::"[i=>i, i] => o"  (infixr "respects" 80) where
    26   "f respects r == congruent(r,f)"
    27 
    28 abbreviation
    29   RESPECTS2 ::"[i=>i=>i, i] => o"  (infixr "respects2 " 80) where
    30   "f respects2 r == congruent2(r,r,f)"
    31     --{*Abbreviation for the common case where the relations are identical*}
    32 
    33 
    34 subsection{*Suppes, Theorem 70:
    35     @{term r} is an equiv relation iff @{term "converse(r) O r = r"}*}
    36 
    37 (** first half: equiv(A,r) ==> converse(r) O r = r **)
    38 
    39 lemma sym_trans_comp_subset:
    40     "[| sym(r); trans(r) |] ==> converse(r) O r <= r"
    41 by (unfold trans_def sym_def, blast)
    42 
    43 lemma refl_comp_subset:
    44     "[| refl(A,r); r <= A*A |] ==> r <= converse(r) O r"
    45 by (unfold refl_def, blast)
    46 
    47 lemma equiv_comp_eq:
    48     "equiv(A,r) ==> converse(r) O r = r"
    49 apply (unfold equiv_def)
    50 apply (blast del: subsetI intro!: sym_trans_comp_subset refl_comp_subset)
    51 done
    52 
    53 (*second half*)
    54 lemma comp_equivI:
    55     "[| converse(r) O r = r;  domain(r) = A |] ==> equiv(A,r)"
    56 apply (unfold equiv_def refl_def sym_def trans_def)
    57 apply (erule equalityE)
    58 apply (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r", blast+)
    59 done
    60 
    61 (** Equivalence classes **)
    62 
    63 (*Lemma for the next result*)
    64 lemma equiv_class_subset:
    65     "[| sym(r);  trans(r);  <a,b>: r |] ==> r``{a} <= r``{b}"
    66 by (unfold trans_def sym_def, blast)
    67 
    68 lemma equiv_class_eq:
    69     "[| equiv(A,r);  <a,b>: r |] ==> r``{a} = r``{b}"
    70 apply (unfold equiv_def)
    71 apply (safe del: subsetI intro!: equalityI equiv_class_subset)
    72 apply (unfold sym_def, blast)
    73 done
    74 
    75 lemma equiv_class_self:
    76     "[| equiv(A,r);  a: A |] ==> a: r``{a}"
    77 by (unfold equiv_def refl_def, blast)
    78 
    79 (*Lemma for the next result*)
    80 lemma subset_equiv_class:
    81     "[| equiv(A,r);  r``{b} <= r``{a};  b: A |] ==> <a,b>: r"
    82 by (unfold equiv_def refl_def, blast)
    83 
    84 lemma eq_equiv_class: "[| r``{a} = r``{b};  equiv(A,r);  b: A |] ==> <a,b>: r"
    85 by (assumption | rule equalityD2 subset_equiv_class)+
    86 
    87 (*thus r``{a} = r``{b} as well*)
    88 lemma equiv_class_nondisjoint:
    89     "[| equiv(A,r);  x: (r``{a} Int r``{b}) |] ==> <a,b>: r"
    90 by (unfold equiv_def trans_def sym_def, blast)
    91 
    92 lemma equiv_type: "equiv(A,r) ==> r <= A*A"
    93 by (unfold equiv_def, blast)
    94 
    95 lemma equiv_class_eq_iff:
    96      "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A"
    97 by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
    98 
    99 lemma eq_equiv_class_iff:
   100      "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r"
   101 by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
   102 
   103 (*** Quotients ***)
   104 
   105 (** Introduction/elimination rules -- needed? **)
   106 
   107 lemma quotientI [TC]: "x:A ==> r``{x}: A//r"
   108 apply (unfold quotient_def)
   109 apply (erule RepFunI)
   110 done
   111 
   112 lemma quotientE:
   113     "[| X: A//r;  !!x. [| X = r``{x};  x:A |] ==> P |] ==> P"
   114 by (unfold quotient_def, blast)
   115 
   116 lemma Union_quotient:
   117     "equiv(A,r) ==> Union(A//r) = A"
   118 by (unfold equiv_def refl_def quotient_def, blast)
   119 
   120 lemma quotient_disj:
   121     "[| equiv(A,r);  X: A//r;  Y: A//r |] ==> X=Y | (X Int Y <= 0)"
   122 apply (unfold quotient_def)
   123 apply (safe intro!: equiv_class_eq, assumption)
   124 apply (unfold equiv_def trans_def sym_def, blast)
   125 done
   126 
   127 subsection{*Defining Unary Operations upon Equivalence Classes*}
   128 
   129 (** Could have a locale with the premises equiv(A,r)  and  congruent(r,b)
   130 **)
   131 
   132 (*Conversion rule*)
   133 lemma UN_equiv_class:
   134     "[| equiv(A,r);  b respects r;  a: A |] ==> (UN x:r``{a}. b(x)) = b(a)"
   135 apply (subgoal_tac "\<forall>x \<in> r``{a}. b(x) = b(a)") 
   136  apply simp
   137  apply (blast intro: equiv_class_self)  
   138 apply (unfold equiv_def sym_def congruent_def, blast)
   139 done
   140 
   141 (*type checking of  UN x:r``{a}. b(x) *)
   142 lemma UN_equiv_class_type:
   143     "[| equiv(A,r);  b respects r;  X: A//r;  !!x.  x : A ==> b(x) : B |]
   144      ==> (UN x:X. b(x)) : B"
   145 apply (unfold quotient_def, safe)
   146 apply (simp (no_asm_simp) add: UN_equiv_class)
   147 done
   148 
   149 (*Sufficient conditions for injectiveness.  Could weaken premises!
   150   major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
   151 *)
   152 lemma UN_equiv_class_inject:
   153     "[| equiv(A,r);   b respects r;
   154         (UN x:X. b(x))=(UN y:Y. b(y));  X: A//r;  Y: A//r;
   155         !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |]
   156      ==> X=Y"
   157 apply (unfold quotient_def, safe)
   158 apply (rule equiv_class_eq, assumption)
   159 apply (simp add: UN_equiv_class [of A r b])  
   160 done
   161 
   162 
   163 subsection{*Defining Binary Operations upon Equivalence Classes*}
   164 
   165 lemma congruent2_implies_congruent:
   166     "[| equiv(A,r1);  congruent2(r1,r2,b);  a: A |] ==> congruent(r2,b(a))"
   167 by (unfold congruent_def congruent2_def equiv_def refl_def, blast)
   168 
   169 lemma congruent2_implies_congruent_UN:
   170     "[| equiv(A1,r1);  equiv(A2,r2);  congruent2(r1,r2,b);  a: A2 |] ==>
   171      congruent(r1, %x1. \<Union>x2 \<in> r2``{a}. b(x1,x2))"
   172 apply (unfold congruent_def, safe)
   173 apply (frule equiv_type [THEN subsetD], assumption)
   174 apply clarify 
   175 apply (simp add: UN_equiv_class congruent2_implies_congruent)
   176 apply (unfold congruent2_def equiv_def refl_def, blast)
   177 done
   178 
   179 lemma UN_equiv_class2:
   180     "[| equiv(A1,r1);  equiv(A2,r2);  congruent2(r1,r2,b);  a1: A1;  a2: A2 |]
   181      ==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. b(x1,x2)) = b(a1,a2)"
   182 by (simp add: UN_equiv_class congruent2_implies_congruent
   183               congruent2_implies_congruent_UN)
   184 
   185 (*type checking*)
   186 lemma UN_equiv_class_type2:
   187     "[| equiv(A,r);  b respects2 r;
   188         X1: A//r;  X2: A//r;
   189         !!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B
   190      |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B"
   191 apply (unfold quotient_def, safe)
   192 apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN 
   193                     congruent2_implies_congruent quotientI)
   194 done
   195 
   196 
   197 (*Suggested by John Harrison -- the two subproofs may be MUCH simpler
   198   than the direct proof*)
   199 lemma congruent2I:
   200     "[|  equiv(A1,r1);  equiv(A2,r2);  
   201         !! y z w. [| w \<in> A2;  <y,z> \<in> r1 |] ==> b(y,w) = b(z,w);
   202         !! y z w. [| w \<in> A1;  <y,z> \<in> r2 |] ==> b(w,y) = b(w,z)
   203      |] ==> congruent2(r1,r2,b)"
   204 apply (unfold congruent2_def equiv_def refl_def, safe)
   205 apply (blast intro: trans) 
   206 done
   207 
   208 lemma congruent2_commuteI:
   209  assumes equivA: "equiv(A,r)"
   210      and commute: "!! y z. [| y: A;  z: A |] ==> b(y,z) = b(z,y)"
   211      and congt:   "!! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)"
   212  shows "b respects2 r"
   213 apply (insert equivA [THEN equiv_type, THEN subsetD]) 
   214 apply (rule congruent2I [OF equivA equivA])
   215 apply (rule commute [THEN trans])
   216 apply (rule_tac [3] commute [THEN trans, symmetric])
   217 apply (rule_tac [5] sym) 
   218 apply (blast intro: congt)+
   219 done
   220 
   221 (*Obsolete?*)
   222 lemma congruent_commuteI:
   223     "[| equiv(A,r);  Z: A//r;
   224         !!w. [| w: A |] ==> congruent(r, %z. b(w,z));
   225         !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)
   226      |] ==> congruent(r, %w. UN z: Z. b(w,z))"
   227 apply (simp (no_asm) add: congruent_def)
   228 apply (safe elim!: quotientE)
   229 apply (frule equiv_type [THEN subsetD], assumption)
   230 apply (simp add: UN_equiv_class [of A r]) 
   231 apply (simp add: congruent_def) 
   232 done
   233 
   234 ML
   235 {*
   236 val sym_trans_comp_subset = thm "sym_trans_comp_subset";
   237 val refl_comp_subset = thm "refl_comp_subset";
   238 val equiv_comp_eq = thm "equiv_comp_eq";
   239 val comp_equivI = thm "comp_equivI";
   240 val equiv_class_subset = thm "equiv_class_subset";
   241 val equiv_class_eq = thm "equiv_class_eq";
   242 val equiv_class_self = thm "equiv_class_self";
   243 val subset_equiv_class = thm "subset_equiv_class";
   244 val eq_equiv_class = thm "eq_equiv_class";
   245 val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
   246 val equiv_type = thm "equiv_type";
   247 val equiv_class_eq_iff = thm "equiv_class_eq_iff";
   248 val eq_equiv_class_iff = thm "eq_equiv_class_iff";
   249 val quotientI = thm "quotientI";
   250 val quotientE = thm "quotientE";
   251 val Union_quotient = thm "Union_quotient";
   252 val quotient_disj = thm "quotient_disj";
   253 val UN_equiv_class = thm "UN_equiv_class";
   254 val UN_equiv_class_type = thm "UN_equiv_class_type";
   255 val UN_equiv_class_inject = thm "UN_equiv_class_inject";
   256 val congruent2_implies_congruent = thm "congruent2_implies_congruent";
   257 val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";
   258 val congruent_commuteI = thm "congruent_commuteI";
   259 val UN_equiv_class2 = thm "UN_equiv_class2";
   260 val UN_equiv_class_type2 = thm "UN_equiv_class_type2";
   261 val congruent2I = thm "congruent2I";
   262 val congruent2_commuteI = thm "congruent2_commuteI";
   263 val congruent_commuteI = thm "congruent_commuteI";
   264 *}
   265 
   266 end