src/ZF/EquivClass.thy
changeset 23146 0bc590051d95
child 24892 c663e675e177
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/EquivClass.thy	Thu May 31 12:06:31 2007 +0200
     1.3 @@ -0,0 +1,265 @@
     1.4 +(*  Title:      ZF/EquivClass.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1994  University of Cambridge
     1.8 +
     1.9 +*)
    1.10 +
    1.11 +header{*Equivalence Relations*}
    1.12 +
    1.13 +theory EquivClass imports Trancl Perm begin
    1.14 +
    1.15 +constdefs
    1.16 +
    1.17 +  quotient   :: "[i,i]=>i"    (infixl "'/'/" 90)  (*set of equiv classes*)
    1.18 +      "A//r == {r``{x} . x:A}"
    1.19 +
    1.20 +  congruent  :: "[i,i=>i]=>o"
    1.21 +      "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
    1.22 +
    1.23 +  congruent2 :: "[i,i,[i,i]=>i]=>o"
    1.24 +      "congruent2(r1,r2,b) == ALL y1 z1 y2 z2.
    1.25 +           <y1,z1>:r1 --> <y2,z2>:r2 --> b(y1,y2) = b(z1,z2)"
    1.26 +
    1.27 +syntax
    1.28 +  RESPECTS ::"[i=>i, i] => o"  (infixr "respects" 80)
    1.29 +  RESPECTS2 ::"[i=>i, i] => o"  (infixr "respects2 " 80)
    1.30 +    --{*Abbreviation for the common case where the relations are identical*}
    1.31 +
    1.32 +translations
    1.33 +  "f respects r" == "congruent(r,f)"
    1.34 +  "f respects2 r" => "congruent2(r,r,f)"
    1.35 +
    1.36 +subsection{*Suppes, Theorem 70:
    1.37 +    @{term r} is an equiv relation iff @{term "converse(r) O r = r"}*}
    1.38 +
    1.39 +(** first half: equiv(A,r) ==> converse(r) O r = r **)
    1.40 +
    1.41 +lemma sym_trans_comp_subset:
    1.42 +    "[| sym(r); trans(r) |] ==> converse(r) O r <= r"
    1.43 +by (unfold trans_def sym_def, blast)
    1.44 +
    1.45 +lemma refl_comp_subset:
    1.46 +    "[| refl(A,r); r <= A*A |] ==> r <= converse(r) O r"
    1.47 +by (unfold refl_def, blast)
    1.48 +
    1.49 +lemma equiv_comp_eq:
    1.50 +    "equiv(A,r) ==> converse(r) O r = r"
    1.51 +apply (unfold equiv_def)
    1.52 +apply (blast del: subsetI intro!: sym_trans_comp_subset refl_comp_subset)
    1.53 +done
    1.54 +
    1.55 +(*second half*)
    1.56 +lemma comp_equivI:
    1.57 +    "[| converse(r) O r = r;  domain(r) = A |] ==> equiv(A,r)"
    1.58 +apply (unfold equiv_def refl_def sym_def trans_def)
    1.59 +apply (erule equalityE)
    1.60 +apply (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r", blast+)
    1.61 +done
    1.62 +
    1.63 +(** Equivalence classes **)
    1.64 +
    1.65 +(*Lemma for the next result*)
    1.66 +lemma equiv_class_subset:
    1.67 +    "[| sym(r);  trans(r);  <a,b>: r |] ==> r``{a} <= r``{b}"
    1.68 +by (unfold trans_def sym_def, blast)
    1.69 +
    1.70 +lemma equiv_class_eq:
    1.71 +    "[| equiv(A,r);  <a,b>: r |] ==> r``{a} = r``{b}"
    1.72 +apply (unfold equiv_def)
    1.73 +apply (safe del: subsetI intro!: equalityI equiv_class_subset)
    1.74 +apply (unfold sym_def, blast)
    1.75 +done
    1.76 +
    1.77 +lemma equiv_class_self:
    1.78 +    "[| equiv(A,r);  a: A |] ==> a: r``{a}"
    1.79 +by (unfold equiv_def refl_def, blast)
    1.80 +
    1.81 +(*Lemma for the next result*)
    1.82 +lemma subset_equiv_class:
    1.83 +    "[| equiv(A,r);  r``{b} <= r``{a};  b: A |] ==> <a,b>: r"
    1.84 +by (unfold equiv_def refl_def, blast)
    1.85 +
    1.86 +lemma eq_equiv_class: "[| r``{a} = r``{b};  equiv(A,r);  b: A |] ==> <a,b>: r"
    1.87 +by (assumption | rule equalityD2 subset_equiv_class)+
    1.88 +
    1.89 +(*thus r``{a} = r``{b} as well*)
    1.90 +lemma equiv_class_nondisjoint:
    1.91 +    "[| equiv(A,r);  x: (r``{a} Int r``{b}) |] ==> <a,b>: r"
    1.92 +by (unfold equiv_def trans_def sym_def, blast)
    1.93 +
    1.94 +lemma equiv_type: "equiv(A,r) ==> r <= A*A"
    1.95 +by (unfold equiv_def, blast)
    1.96 +
    1.97 +lemma equiv_class_eq_iff:
    1.98 +     "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A"
    1.99 +by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
   1.100 +
   1.101 +lemma eq_equiv_class_iff:
   1.102 +     "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r"
   1.103 +by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
   1.104 +
   1.105 +(*** Quotients ***)
   1.106 +
   1.107 +(** Introduction/elimination rules -- needed? **)
   1.108 +
   1.109 +lemma quotientI [TC]: "x:A ==> r``{x}: A//r"
   1.110 +apply (unfold quotient_def)
   1.111 +apply (erule RepFunI)
   1.112 +done
   1.113 +
   1.114 +lemma quotientE:
   1.115 +    "[| X: A//r;  !!x. [| X = r``{x};  x:A |] ==> P |] ==> P"
   1.116 +by (unfold quotient_def, blast)
   1.117 +
   1.118 +lemma Union_quotient:
   1.119 +    "equiv(A,r) ==> Union(A//r) = A"
   1.120 +by (unfold equiv_def refl_def quotient_def, blast)
   1.121 +
   1.122 +lemma quotient_disj:
   1.123 +    "[| equiv(A,r);  X: A//r;  Y: A//r |] ==> X=Y | (X Int Y <= 0)"
   1.124 +apply (unfold quotient_def)
   1.125 +apply (safe intro!: equiv_class_eq, assumption)
   1.126 +apply (unfold equiv_def trans_def sym_def, blast)
   1.127 +done
   1.128 +
   1.129 +subsection{*Defining Unary Operations upon Equivalence Classes*}
   1.130 +
   1.131 +(** Could have a locale with the premises equiv(A,r)  and  congruent(r,b)
   1.132 +**)
   1.133 +
   1.134 +(*Conversion rule*)
   1.135 +lemma UN_equiv_class:
   1.136 +    "[| equiv(A,r);  b respects r;  a: A |] ==> (UN x:r``{a}. b(x)) = b(a)"
   1.137 +apply (subgoal_tac "\<forall>x \<in> r``{a}. b(x) = b(a)") 
   1.138 + apply simp
   1.139 + apply (blast intro: equiv_class_self)  
   1.140 +apply (unfold equiv_def sym_def congruent_def, blast)
   1.141 +done
   1.142 +
   1.143 +(*type checking of  UN x:r``{a}. b(x) *)
   1.144 +lemma UN_equiv_class_type:
   1.145 +    "[| equiv(A,r);  b respects r;  X: A//r;  !!x.  x : A ==> b(x) : B |]
   1.146 +     ==> (UN x:X. b(x)) : B"
   1.147 +apply (unfold quotient_def, safe)
   1.148 +apply (simp (no_asm_simp) add: UN_equiv_class)
   1.149 +done
   1.150 +
   1.151 +(*Sufficient conditions for injectiveness.  Could weaken premises!
   1.152 +  major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
   1.153 +*)
   1.154 +lemma UN_equiv_class_inject:
   1.155 +    "[| equiv(A,r);   b respects r;
   1.156 +        (UN x:X. b(x))=(UN y:Y. b(y));  X: A//r;  Y: A//r;
   1.157 +        !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |]
   1.158 +     ==> X=Y"
   1.159 +apply (unfold quotient_def, safe)
   1.160 +apply (rule equiv_class_eq, assumption)
   1.161 +apply (simp add: UN_equiv_class [of A r b])  
   1.162 +done
   1.163 +
   1.164 +
   1.165 +subsection{*Defining Binary Operations upon Equivalence Classes*}
   1.166 +
   1.167 +lemma congruent2_implies_congruent:
   1.168 +    "[| equiv(A,r1);  congruent2(r1,r2,b);  a: A |] ==> congruent(r2,b(a))"
   1.169 +by (unfold congruent_def congruent2_def equiv_def refl_def, blast)
   1.170 +
   1.171 +lemma congruent2_implies_congruent_UN:
   1.172 +    "[| equiv(A1,r1);  equiv(A2,r2);  congruent2(r1,r2,b);  a: A2 |] ==>
   1.173 +     congruent(r1, %x1. \<Union>x2 \<in> r2``{a}. b(x1,x2))"
   1.174 +apply (unfold congruent_def, safe)
   1.175 +apply (frule equiv_type [THEN subsetD], assumption)
   1.176 +apply clarify 
   1.177 +apply (simp add: UN_equiv_class congruent2_implies_congruent)
   1.178 +apply (unfold congruent2_def equiv_def refl_def, blast)
   1.179 +done
   1.180 +
   1.181 +lemma UN_equiv_class2:
   1.182 +    "[| equiv(A1,r1);  equiv(A2,r2);  congruent2(r1,r2,b);  a1: A1;  a2: A2 |]
   1.183 +     ==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. b(x1,x2)) = b(a1,a2)"
   1.184 +by (simp add: UN_equiv_class congruent2_implies_congruent
   1.185 +              congruent2_implies_congruent_UN)
   1.186 +
   1.187 +(*type checking*)
   1.188 +lemma UN_equiv_class_type2:
   1.189 +    "[| equiv(A,r);  b respects2 r;
   1.190 +        X1: A//r;  X2: A//r;
   1.191 +        !!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B
   1.192 +     |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B"
   1.193 +apply (unfold quotient_def, safe)
   1.194 +apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN 
   1.195 +                    congruent2_implies_congruent quotientI)
   1.196 +done
   1.197 +
   1.198 +
   1.199 +(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
   1.200 +  than the direct proof*)
   1.201 +lemma congruent2I:
   1.202 +    "[|  equiv(A1,r1);  equiv(A2,r2);  
   1.203 +        !! y z w. [| w \<in> A2;  <y,z> \<in> r1 |] ==> b(y,w) = b(z,w);
   1.204 +        !! y z w. [| w \<in> A1;  <y,z> \<in> r2 |] ==> b(w,y) = b(w,z)
   1.205 +     |] ==> congruent2(r1,r2,b)"
   1.206 +apply (unfold congruent2_def equiv_def refl_def, safe)
   1.207 +apply (blast intro: trans) 
   1.208 +done
   1.209 +
   1.210 +lemma congruent2_commuteI:
   1.211 + assumes equivA: "equiv(A,r)"
   1.212 +     and commute: "!! y z. [| y: A;  z: A |] ==> b(y,z) = b(z,y)"
   1.213 +     and congt:   "!! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)"
   1.214 + shows "b respects2 r"
   1.215 +apply (insert equivA [THEN equiv_type, THEN subsetD]) 
   1.216 +apply (rule congruent2I [OF equivA equivA])
   1.217 +apply (rule commute [THEN trans])
   1.218 +apply (rule_tac [3] commute [THEN trans, symmetric])
   1.219 +apply (rule_tac [5] sym) 
   1.220 +apply (blast intro: congt)+
   1.221 +done
   1.222 +
   1.223 +(*Obsolete?*)
   1.224 +lemma congruent_commuteI:
   1.225 +    "[| equiv(A,r);  Z: A//r;
   1.226 +        !!w. [| w: A |] ==> congruent(r, %z. b(w,z));
   1.227 +        !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)
   1.228 +     |] ==> congruent(r, %w. UN z: Z. b(w,z))"
   1.229 +apply (simp (no_asm) add: congruent_def)
   1.230 +apply (safe elim!: quotientE)
   1.231 +apply (frule equiv_type [THEN subsetD], assumption)
   1.232 +apply (simp add: UN_equiv_class [of A r]) 
   1.233 +apply (simp add: congruent_def) 
   1.234 +done
   1.235 +
   1.236 +ML
   1.237 +{*
   1.238 +val sym_trans_comp_subset = thm "sym_trans_comp_subset";
   1.239 +val refl_comp_subset = thm "refl_comp_subset";
   1.240 +val equiv_comp_eq = thm "equiv_comp_eq";
   1.241 +val comp_equivI = thm "comp_equivI";
   1.242 +val equiv_class_subset = thm "equiv_class_subset";
   1.243 +val equiv_class_eq = thm "equiv_class_eq";
   1.244 +val equiv_class_self = thm "equiv_class_self";
   1.245 +val subset_equiv_class = thm "subset_equiv_class";
   1.246 +val eq_equiv_class = thm "eq_equiv_class";
   1.247 +val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
   1.248 +val equiv_type = thm "equiv_type";
   1.249 +val equiv_class_eq_iff = thm "equiv_class_eq_iff";
   1.250 +val eq_equiv_class_iff = thm "eq_equiv_class_iff";
   1.251 +val quotientI = thm "quotientI";
   1.252 +val quotientE = thm "quotientE";
   1.253 +val Union_quotient = thm "Union_quotient";
   1.254 +val quotient_disj = thm "quotient_disj";
   1.255 +val UN_equiv_class = thm "UN_equiv_class";
   1.256 +val UN_equiv_class_type = thm "UN_equiv_class_type";
   1.257 +val UN_equiv_class_inject = thm "UN_equiv_class_inject";
   1.258 +val congruent2_implies_congruent = thm "congruent2_implies_congruent";
   1.259 +val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";
   1.260 +val congruent_commuteI = thm "congruent_commuteI";
   1.261 +val UN_equiv_class2 = thm "UN_equiv_class2";
   1.262 +val UN_equiv_class_type2 = thm "UN_equiv_class_type2";
   1.263 +val congruent2I = thm "congruent2I";
   1.264 +val congruent2_commuteI = thm "congruent2_commuteI";
   1.265 +val congruent_commuteI = thm "congruent_commuteI";
   1.266 +*}
   1.267 +
   1.268 +end