ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
authorlcp
Tue Aug 16 19:06:14 1994 +0200 (1994-08-16)
changeset 5359d62c7e08699
parent 534 cd8bec47e175
child 536 5fbfa997f1b0
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
src/ZF/EquivClass.ML
src/ZF/EquivClass.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/EquivClass.ML	Tue Aug 16 19:06:14 1994 +0200
     1.3 @@ -0,0 +1,268 @@
     1.4 +(*  Title: 	ZF/EquivClass.ML
     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 +For EquivClass.thy.  Equivalence relations in Zermelo-Fraenkel Set Theory 
    1.10 +*)
    1.11 +
    1.12 +val RSLIST = curry (op MRS);
    1.13 +
    1.14 +open EquivClass;
    1.15 +
    1.16 +(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***)
    1.17 +
    1.18 +(** first half: equiv(A,r) ==> converse(r) O r = r **)
    1.19 +
    1.20 +goalw EquivClass.thy [trans_def,sym_def]
    1.21 +    "!!r. [| sym(r); trans(r) |] ==> converse(r) O r <= r";
    1.22 +by (fast_tac (ZF_cs addSEs [converseD,compE]) 1);
    1.23 +val sym_trans_comp_subset = result();
    1.24 +
    1.25 +goalw EquivClass.thy [refl_def]
    1.26 +    "!!A r. [| refl(A,r); r <= A*A |] ==> r <= converse(r) O r";
    1.27 +by (fast_tac (ZF_cs addSIs [converseI] addIs [compI]) 1);
    1.28 +val refl_comp_subset = result();
    1.29 +
    1.30 +goalw EquivClass.thy [equiv_def]
    1.31 +    "!!A r. equiv(A,r) ==> converse(r) O r = r";
    1.32 +by (rtac equalityI 1);
    1.33 +by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1
    1.34 +     ORELSE etac conjE 1));
    1.35 +val equiv_comp_eq = result();
    1.36 +
    1.37 +(*second half*)
    1.38 +goalw EquivClass.thy [equiv_def,refl_def,sym_def,trans_def]
    1.39 +    "!!A r. [| converse(r) O r = r;  domain(r) = A |] ==> equiv(A,r)";
    1.40 +by (etac equalityE 1);
    1.41 +by (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r" 1);
    1.42 +by (safe_tac ZF_cs);
    1.43 +by (fast_tac (ZF_cs addSIs [converseI] addIs [compI]) 3);
    1.44 +by (ALLGOALS (fast_tac 
    1.45 +	      (ZF_cs addSIs [converseI] addIs [compI] addSEs [compE])));
    1.46 +by flexflex_tac;
    1.47 +val comp_equivI = result();
    1.48 +
    1.49 +(** Equivalence classes **)
    1.50 +
    1.51 +(*Lemma for the next result*)
    1.52 +goalw EquivClass.thy [trans_def,sym_def]
    1.53 +    "!!A r. [| sym(r);  trans(r);  <a,b>: r |] ==> r``{a} <= r``{b}";
    1.54 +by (fast_tac ZF_cs 1);
    1.55 +val equiv_class_subset = result();
    1.56 +
    1.57 +goalw EquivClass.thy [equiv_def]
    1.58 +    "!!A r. [| equiv(A,r);  <a,b>: r |] ==> r``{a} = r``{b}";
    1.59 +by (safe_tac (subset_cs addSIs [equalityI, equiv_class_subset]));
    1.60 +by (rewrite_goals_tac [sym_def]);
    1.61 +by (fast_tac ZF_cs 1);
    1.62 +val equiv_class_eq = result();
    1.63 +
    1.64 +val prems = goalw EquivClass.thy [equiv_def,refl_def]
    1.65 +    "[| equiv(A,r);  a: A |] ==> a: r``{a}";
    1.66 +by (cut_facts_tac prems 1);
    1.67 +by (fast_tac ZF_cs 1);
    1.68 +val equiv_class_self = result();
    1.69 +
    1.70 +(*Lemma for the next result*)
    1.71 +goalw EquivClass.thy [equiv_def,refl_def]
    1.72 +    "!!A r. [| equiv(A,r);  r``{b} <= r``{a};  b: A |] ==> <a,b>: r";
    1.73 +by (fast_tac ZF_cs 1);
    1.74 +val subset_equiv_class = result();
    1.75 +
    1.76 +val prems = goal EquivClass.thy
    1.77 +    "[| r``{a} = r``{b};  equiv(A,r);  b: A |] ==> <a,b>: r";
    1.78 +by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1));
    1.79 +val eq_equiv_class = result();
    1.80 +
    1.81 +(*thus r``{a} = r``{b} as well*)
    1.82 +goalw EquivClass.thy [equiv_def,trans_def,sym_def]
    1.83 +    "!!A r. [| equiv(A,r);  x: (r``{a} Int r``{b}) |] ==> <a,b>: r";
    1.84 +by (fast_tac ZF_cs 1);
    1.85 +val equiv_class_nondisjoint = result();
    1.86 +
    1.87 +goalw EquivClass.thy [equiv_def] "!!A r. equiv(A,r) ==> r <= A*A";
    1.88 +by (safe_tac ZF_cs);
    1.89 +val equiv_type = result();
    1.90 +
    1.91 +goal EquivClass.thy
    1.92 +    "!!A r. equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
    1.93 +by (fast_tac (ZF_cs addIs [eq_equiv_class, equiv_class_eq]
    1.94 +		    addDs [equiv_type]) 1);
    1.95 +val equiv_class_eq_iff = result();
    1.96 +
    1.97 +goal EquivClass.thy
    1.98 +    "!!A r. [| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
    1.99 +by (fast_tac (ZF_cs addIs [eq_equiv_class, equiv_class_eq]
   1.100 +		    addDs [equiv_type]) 1);
   1.101 +val eq_equiv_class_iff = result();
   1.102 +
   1.103 +(*** Quotients ***)
   1.104 +
   1.105 +(** Introduction/elimination rules -- needed? **)
   1.106 +
   1.107 +val prems = goalw EquivClass.thy [quotient_def] "x:A ==> r``{x}: A/r";
   1.108 +by (rtac RepFunI 1);
   1.109 +by (resolve_tac prems 1);
   1.110 +val quotientI = result();
   1.111 +
   1.112 +val major::prems = goalw EquivClass.thy [quotient_def]
   1.113 +    "[| X: A/r;  !!x. [| X = r``{x};  x:A |] ==> P |] 	\
   1.114 +\    ==> P";
   1.115 +by (rtac (major RS RepFunE) 1);
   1.116 +by (eresolve_tac prems 1);
   1.117 +by (assume_tac 1);
   1.118 +val quotientE = result();
   1.119 +
   1.120 +goalw EquivClass.thy [equiv_def,refl_def,quotient_def]
   1.121 +    "!!A r. equiv(A,r) ==> Union(A/r) = A";
   1.122 +by (fast_tac eq_cs 1);
   1.123 +val Union_quotient = result();
   1.124 +
   1.125 +goalw EquivClass.thy [quotient_def]
   1.126 +    "!!A r. [| equiv(A,r);  X: A/r;  Y: A/r |] ==> X=Y | (X Int Y <= 0)";
   1.127 +by (safe_tac (ZF_cs addSIs [equiv_class_eq]));
   1.128 +by (assume_tac 1);
   1.129 +by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
   1.130 +by (fast_tac ZF_cs 1);
   1.131 +val quotient_disj = result();
   1.132 +
   1.133 +(**** Defining unary operations upon equivalence classes ****)
   1.134 +
   1.135 +(** These proofs really require as local premises
   1.136 +     equiv(A,r);  congruent(r,b)
   1.137 +**)
   1.138 +
   1.139 +(*Conversion rule*)
   1.140 +val prems as [equivA,bcong,_] = goal EquivClass.thy
   1.141 +    "[| equiv(A,r);  congruent(r,b);  a: A |] ==> (UN x:r``{a}. b(x)) = b(a)";
   1.142 +by (cut_facts_tac prems 1);
   1.143 +by (rtac ([refl RS UN_cong, UN_constant] MRS trans) 1);
   1.144 +by (etac equiv_class_self 2);
   1.145 +by (assume_tac 2);
   1.146 +by (rewrite_goals_tac [equiv_def,sym_def,congruent_def]);
   1.147 +by (fast_tac ZF_cs 1);
   1.148 +val UN_equiv_class = result();
   1.149 +
   1.150 +(*Resolve th against the "local" premises*)
   1.151 +val localize = RSLIST [equivA,bcong];
   1.152 +
   1.153 +(*type checking of  UN x:r``{a}. b(x) *)
   1.154 +val _::_::prems = goalw EquivClass.thy [quotient_def]
   1.155 +    "[| equiv(A,r);  congruent(r,b);  X: A/r;	\
   1.156 +\	!!x.  x : A ==> b(x) : B |] 	\
   1.157 +\    ==> (UN x:X. b(x)) : B";
   1.158 +by (cut_facts_tac prems 1);
   1.159 +by (safe_tac ZF_cs);
   1.160 +by (rtac (localize UN_equiv_class RS ssubst) 1);
   1.161 +by (REPEAT (ares_tac prems 1));
   1.162 +val UN_equiv_class_type = result();
   1.163 +
   1.164 +(*Sufficient conditions for injectiveness.  Could weaken premises!
   1.165 +  major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
   1.166 +*)
   1.167 +val _::_::prems = goalw EquivClass.thy [quotient_def]
   1.168 +    "[| equiv(A,r);   congruent(r,b);  \
   1.169 +\       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;  \
   1.170 +\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] 	\
   1.171 +\    ==> X=Y";
   1.172 +by (cut_facts_tac prems 1);
   1.173 +by (safe_tac ZF_cs);
   1.174 +by (rtac (equivA RS equiv_class_eq) 1);
   1.175 +by (REPEAT (ares_tac prems 1));
   1.176 +by (etac box_equals 1);
   1.177 +by (REPEAT (ares_tac [localize UN_equiv_class] 1));
   1.178 +val UN_equiv_class_inject = result();
   1.179 +
   1.180 +
   1.181 +(**** Defining binary operations upon equivalence classes ****)
   1.182 +
   1.183 +
   1.184 +goalw EquivClass.thy [congruent_def,congruent2_def,equiv_def,refl_def]
   1.185 +    "!!A r. [| equiv(A,r);  congruent2(r,b);  a: A |] ==> congruent(r,b(a))";
   1.186 +by (fast_tac ZF_cs 1);
   1.187 +val congruent2_implies_congruent = result();
   1.188 +
   1.189 +val equivA::prems = goalw EquivClass.thy [congruent_def]
   1.190 +    "[| equiv(A,r);  congruent2(r,b);  a: A |] ==> \
   1.191 +\    congruent(r, %x1. UN x2:r``{a}. b(x1,x2))";
   1.192 +by (cut_facts_tac (equivA::prems) 1);
   1.193 +by (safe_tac ZF_cs);
   1.194 +by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
   1.195 +by (assume_tac 1);
   1.196 +by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
   1.197 +				 congruent2_implies_congruent]) 1);
   1.198 +by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
   1.199 +by (fast_tac ZF_cs 1);
   1.200 +val congruent2_implies_congruent_UN = result();
   1.201 +
   1.202 +val prems as equivA::_ = goal EquivClass.thy
   1.203 +    "[| equiv(A,r);  congruent2(r,b);  a1: A;  a2: A |]  \
   1.204 +\    ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
   1.205 +by (cut_facts_tac prems 1);
   1.206 +by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
   1.207 +				 congruent2_implies_congruent,
   1.208 +				 congruent2_implies_congruent_UN]) 1);
   1.209 +val UN_equiv_class2 = result();
   1.210 +
   1.211 +(*type checking*)
   1.212 +val prems = goalw EquivClass.thy [quotient_def]
   1.213 +    "[| equiv(A,r);  congruent2(r,b);  \
   1.214 +\       X1: A/r;  X2: A/r;	\
   1.215 +\	!!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B |]    \
   1.216 +\    ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B";
   1.217 +by (cut_facts_tac prems 1);
   1.218 +by (safe_tac ZF_cs);
   1.219 +by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
   1.220 +			     congruent2_implies_congruent_UN,
   1.221 +			     congruent2_implies_congruent, quotientI]) 1));
   1.222 +val UN_equiv_class_type2 = result();
   1.223 +
   1.224 +
   1.225 +(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
   1.226 +  than the direct proof*)
   1.227 +val prems = goalw EquivClass.thy [congruent2_def,equiv_def,refl_def]
   1.228 +    "[| equiv(A,r);	\
   1.229 +\       !! y z w. [| w: A;  <y,z> : r |] ==> b(y,w) = b(z,w);      \
   1.230 +\       !! y z w. [| w: A;  <y,z> : r |] ==> b(w,y) = b(w,z)       \
   1.231 +\    |] ==> congruent2(r,b)";
   1.232 +by (cut_facts_tac prems 1);
   1.233 +by (safe_tac ZF_cs);
   1.234 +by (rtac trans 1);
   1.235 +by (REPEAT (ares_tac prems 1
   1.236 +     ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
   1.237 +val congruent2I = result();
   1.238 +
   1.239 +val [equivA,commute,congt] = goal EquivClass.thy
   1.240 +    "[| equiv(A,r);	\
   1.241 +\       !! y z. [| y: A;  z: A |] ==> b(y,z) = b(z,y);        \
   1.242 +\       !! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)	\
   1.243 +\    |] ==> congruent2(r,b)";
   1.244 +by (resolve_tac [equivA RS congruent2I] 1);
   1.245 +by (rtac (commute RS trans) 1);
   1.246 +by (rtac (commute RS trans RS sym) 3);
   1.247 +by (rtac sym 5);
   1.248 +by (REPEAT (ares_tac [congt] 1
   1.249 +     ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1));
   1.250 +val congruent2_commuteI = result();
   1.251 +
   1.252 +(***OBSOLETE VERSION
   1.253 +(*Rules congruentI and congruentD would simplify use of rewriting below*)
   1.254 +val [equivA,ZinA,congt,commute] = goalw EquivClass.thy [quotient_def]
   1.255 +    "[| equiv(A,r);  Z: A/r;  \
   1.256 +\       !!w. [| w: A |] ==> congruent(r, %z.b(w,z));	\
   1.257 +\       !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)	\
   1.258 +\    |] ==> congruent(r, %w. UN z: Z. b(w,z))";
   1.259 +val congt' = rewrite_rule [congruent_def] congt;
   1.260 +by (cut_facts_tac [ZinA,congt] 1);
   1.261 +by (rewtac congruent_def);
   1.262 +by (safe_tac ZF_cs);
   1.263 +by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
   1.264 +by (assume_tac 1);
   1.265 +by (asm_simp_tac (ZF_ss addsimps [congt RS (equivA RS UN_equiv_class)]) 1);
   1.266 +by (rtac (commute RS trans) 1);
   1.267 +by (rtac (commute RS trans RS sym) 3);
   1.268 +by (rtac sym 5);
   1.269 +by (REPEAT (ares_tac [congt' RS spec RS spec RS mp] 1));
   1.270 +val congruent_commuteI = result();
   1.271 +***)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/ZF/EquivClass.thy	Tue Aug 16 19:06:14 1994 +0200
     2.3 @@ -0,0 +1,23 @@
     2.4 +(*  Title: 	ZF/EquivClass.thy
     2.5 +    ID:         $Id$
     2.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1994  University of Cambridge
     2.8 +
     2.9 +Equivalence relations in Zermelo-Fraenkel Set Theory 
    2.10 +*)
    2.11 +
    2.12 +EquivClass = Rel + Perm + 
    2.13 +consts
    2.14 +    "'/"        ::      "[i,i]=>i"  (infixl 90)  (*set of equiv classes*)
    2.15 +    congruent	::	"[i,i=>i]=>o"
    2.16 +    congruent2  ::      "[i,[i,i]=>i]=>o"
    2.17 +
    2.18 +rules
    2.19 +    quotient_def  "A/r == {r``{x} . x:A}"
    2.20 +    congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
    2.21 +
    2.22 +    congruent2_def
    2.23 +       "congruent2(r,b) == ALL y1 z1 y2 z2. \
    2.24 +\           <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
    2.25 +
    2.26 +end