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