src/ZF/ex/equiv.ML
 changeset 0 a5a9c433f639 child 7 268f93ab3bc4
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/ZF/ex/equiv.ML	Thu Sep 16 12:20:38 1993 +0200
1.3 @@ -0,0 +1,268 @@
1.4 +(*  Title: 	ZF/ex/equiv.ML
1.5 +    ID:         \$Id\$
1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 +    Copyright   1993  University of Cambridge
1.8 +
1.9 +For equiv.thy.  Equivalence relations in Zermelo-Fraenkel Set Theory
1.10 +*)
1.11 +
1.12 +val RSLIST = curry (op MRS);
1.13 +
1.14 +open Equiv;
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 Equiv.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 Equiv.thy [refl_def]
1.26 +    "!!A r. refl(A,r) ==> r <= converse(r) O r";
1.28 +val refl_comp_subset = result();
1.29 +
1.30 +goalw Equiv.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 Equiv.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.44 +by (ALLGOALS (fast_tac
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 Equiv.thy [equiv_def,trans_def,sym_def]
1.53 +    "!!A r. [| equiv(A,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 +goal Equiv.thy "!!A r. [| equiv(A,r);  <a,b>: r |] ==> r``{a} = r``{b}";
1.58 +by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
1.59 +by (rewrite_goals_tac [equiv_def,sym_def]);
1.60 +by (fast_tac ZF_cs 1);
1.61 +val equiv_class_eq = result();
1.62 +
1.63 +val prems = goalw Equiv.thy [equiv_def,refl_def]
1.64 +    "[| equiv(A,r);  a: A |] ==> a: r``{a}";
1.65 +by (cut_facts_tac prems 1);
1.66 +by (fast_tac ZF_cs 1);
1.67 +val equiv_class_self = result();
1.68 +
1.69 +(*Lemma for the next result*)
1.70 +goalw Equiv.thy [equiv_def,refl_def]
1.71 +    "!!A r. [| equiv(A,r);  r``{b} <= r``{a};  b: A |] ==> <a,b>: r";
1.72 +by (fast_tac ZF_cs 1);
1.73 +val subset_equiv_class = result();
1.74 +
1.75 +val prems = goal Equiv.thy
1.76 +    "[| r``{a} = r``{b};  equiv(A,r);  b: A |] ==> <a,b>: r";
1.77 +by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1));
1.78 +val eq_equiv_class = result();
1.79 +
1.80 +(*thus r``{a} = r``{b} as well*)
1.81 +goalw Equiv.thy [equiv_def,trans_def,sym_def]
1.82 +    "!!A r. [| equiv(A,r);  x: (r``{a} Int r``{b}) |] ==> <a,b>: r";
1.83 +by (fast_tac ZF_cs 1);
1.84 +val equiv_class_nondisjoint = result();
1.85 +
1.86 +val [major] = goalw Equiv.thy [equiv_def,refl_def]
1.87 +    "equiv(A,r) ==> r <= A*A";
1.88 +by (rtac (major RS conjunct1 RS conjunct1) 1);
1.89 +val equiv_type = result();
1.90 +
1.91 +goal Equiv.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.95 +val equiv_class_eq_iff = result();
1.96 +
1.97 +goal Equiv.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.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 Equiv.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 Equiv.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 Equiv.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 Equiv.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 Equiv.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 UN_singleton 1);
1.144 +by (etac equiv_class_self 1);
1.145 +by (assume_tac 1);
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 Equiv.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 Equiv.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 Equiv.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 Equiv.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 addrews [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 Equiv.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 addrews [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 Equiv.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 Equiv.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 Equiv.thy
1.240 +    "[| equiv(A,r);	\
1.241 +\       !! y z w. [| 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 Equiv.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 addrews [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 +***)
```