0

1 
(* Title: ZF/equalities


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Set Theory examples: Union, Intersection, Inclusion, etc.


7 
(Thanks also to Philippe de Groote.)


8 
*)


9 


10 
(** Finite Sets **)


11 


12 
goal ZF.thy "cons(a, cons(b, C)) = cons(b, cons(a, C))";


13 
by (fast_tac eq_cs 1);


14 
val cons_commute = result();


15 


16 
goal ZF.thy "!!B. a: B ==> cons(a,B) = B";


17 
by (fast_tac eq_cs 1);


18 
val cons_absorb = result();


19 


20 
goal ZF.thy "!!B. a: B ==> cons(a, B{a}) = B";


21 
by (fast_tac eq_cs 1);


22 
val cons_Diff = result();


23 


24 
goal ZF.thy "!!C. [ a: C; ALL y:C. y=b ] ==> C = {b}";


25 
by (fast_tac eq_cs 1);


26 
val equal_singleton_lemma = result();


27 
val equal_singleton = ballI RSN (2,equal_singleton_lemma);


28 


29 


30 
(** Binary Intersection **)


31 


32 
goal ZF.thy "0 Int A = 0";


33 
by (fast_tac eq_cs 1);


34 
val Int_0 = result();


35 


36 
(*NOT an equality, but it seems to belong here...*)


37 
goal ZF.thy "cons(a,B) Int C <= cons(a, B Int C)";


38 
by (fast_tac eq_cs 1);


39 
val Int_cons = result();


40 


41 
goal ZF.thy "A Int A = A";


42 
by (fast_tac eq_cs 1);


43 
val Int_absorb = result();


44 


45 
goal ZF.thy "A Int B = B Int A";


46 
by (fast_tac eq_cs 1);


47 
val Int_commute = result();


48 


49 
goal ZF.thy "(A Int B) Int C = A Int (B Int C)";


50 
by (fast_tac eq_cs 1);


51 
val Int_assoc = result();


52 


53 
goal ZF.thy "(A Un B) Int C = (A Int C) Un (B Int C)";


54 
by (fast_tac eq_cs 1);


55 
val Int_Un_distrib = result();


56 


57 
goal ZF.thy "A<=B <> A Int B = A";


58 
by (fast_tac (eq_cs addSEs [equalityE]) 1);


59 
val subset_Int_iff = result();


60 


61 
(** Binary Union **)


62 


63 
goal ZF.thy "0 Un A = A";


64 
by (fast_tac eq_cs 1);


65 
val Un_0 = result();


66 


67 
goal ZF.thy "cons(a,B) Un C = cons(a, B Un C)";


68 
by (fast_tac eq_cs 1);


69 
val Un_cons = result();


70 


71 
goal ZF.thy "A Un A = A";


72 
by (fast_tac eq_cs 1);


73 
val Un_absorb = result();


74 


75 
goal ZF.thy "A Un B = B Un A";


76 
by (fast_tac eq_cs 1);


77 
val Un_commute = result();


78 


79 
goal ZF.thy "(A Un B) Un C = A Un (B Un C)";


80 
by (fast_tac eq_cs 1);


81 
val Un_assoc = result();


82 


83 
goal ZF.thy "(A Int B) Un C = (A Un C) Int (B Un C)";


84 
by (fast_tac eq_cs 1);


85 
val Un_Int_distrib = result();


86 


87 
goal ZF.thy "A<=B <> A Un B = B";


88 
by (fast_tac (eq_cs addSEs [equalityE]) 1);


89 
val subset_Un_iff = result();


90 


91 
(** Simple properties of Diff  set difference **)


92 


93 
goal ZF.thy "AA = 0";


94 
by (fast_tac eq_cs 1);


95 
val Diff_cancel = result();


96 


97 
goal ZF.thy "0A = 0";


98 
by (fast_tac eq_cs 1);


99 
val empty_Diff = result();


100 


101 
goal ZF.thy "A0 = A";


102 
by (fast_tac eq_cs 1);


103 
val Diff_0 = result();


104 


105 
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)


106 
goal ZF.thy "A  cons(a,B) = A  B  {a}";


107 
by (fast_tac eq_cs 1);


108 
val Diff_cons = result();


109 


110 
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)


111 
goal ZF.thy "A  cons(a,B) = A  {a}  B";


112 
by (fast_tac eq_cs 1);


113 
val Diff_cons2 = result();


114 


115 
goal ZF.thy "A Int (BA) = 0";


116 
by (fast_tac eq_cs 1);


117 
val Diff_disjoint = result();


118 


119 
goal ZF.thy "!!A B. A<=B ==> A Un (BA) = B";


120 
by (fast_tac eq_cs 1);


121 
val Diff_partition = result();


122 


123 
goal ZF.thy "!!A B. [ A<=B; B<= C ] ==> (B  (CA)) = A";


124 
by (fast_tac eq_cs 1);


125 
val double_complement = result();


126 


127 
goal ZF.thy


128 
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";


129 
by (fast_tac eq_cs 1);


130 
val Un_Int_crazy = result();


131 


132 
goal ZF.thy "A  (B Un C) = (AB) Int (AC)";


133 
by (fast_tac eq_cs 1);


134 
val Diff_Un = result();


135 


136 
goal ZF.thy "A  (B Int C) = (AB) Un (AC)";


137 
by (fast_tac eq_cs 1);


138 
val Diff_Int = result();


139 


140 
(*Halmos, Naive Set Theory, page 16.*)


141 
goal ZF.thy "(A Int B) Un C = A Int (B Un C) <> C<=A";


142 
by (fast_tac (eq_cs addSEs [equalityE]) 1);


143 
val Un_Int_assoc_iff = result();


144 


145 


146 
(** Big Union and Intersection **)


147 


148 
goal ZF.thy "Union(0) = 0";


149 
by (fast_tac eq_cs 1);


150 
val Union_0 = result();


151 


152 
goal ZF.thy "Union(cons(a,B)) = a Un Union(B)";


153 
by (fast_tac eq_cs 1);


154 
val Union_cons = result();


155 


156 
goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)";


157 
by (fast_tac eq_cs 1);


158 
val Union_Un_distrib = result();


159 


160 
goal ZF.thy "Union(C) Int A = 0 <> (ALL B:C. B Int A = 0)";


161 
by (fast_tac (eq_cs addSEs [equalityE]) 1);


162 
val Union_disjoint = result();


163 


164 
(* A good challenge: Inter is illbehaved on the empty set *)


165 
goal ZF.thy "!!A B. [ a:A; b:B ] ==> Inter(A Un B) = Inter(A) Int Inter(B)";


166 
by (fast_tac eq_cs 1);


167 
val Inter_Un_distrib = result();


168 


169 
goal ZF.thy "Union({b}) = b";


170 
by (fast_tac eq_cs 1);


171 
val Union_singleton = result();


172 


173 
goal ZF.thy "Inter({b}) = b";


174 
by (fast_tac eq_cs 1);


175 
val Inter_singleton = result();


176 


177 
(** Unions and Intersections of Families **)


178 


179 
goal ZF.thy "Union(A) = (UN x:A. x)";


180 
by (fast_tac eq_cs 1);


181 
val Union_eq_UN = result();


182 


183 
goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)";


184 
by (fast_tac eq_cs 1);


185 
val Inter_eq_INT = result();


186 


187 
(*Halmos, Naive Set Theory, page 35.*)


188 
goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";


189 
by (fast_tac eq_cs 1);


190 
val Int_UN_distrib = result();


191 


192 
goal ZF.thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";


193 
by (fast_tac eq_cs 1);


194 
val Un_INT_distrib = result();


195 


196 
goal ZF.thy


197 
"(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";


198 
by (fast_tac eq_cs 1);


199 
val Int_UN_distrib2 = result();


200 


201 
goal ZF.thy


202 
"!!I J. [ i:I; j:J ] ==> \


203 
\ (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";


204 
by (fast_tac eq_cs 1);


205 
val Un_INT_distrib2 = result();


206 


207 
goal ZF.thy "!!A. [ a: A; ALL y:A. b(y)=b(a) ] ==> (UN y:A. b(y)) = b(a)";


208 
by (fast_tac (eq_cs addSEs [equalityE]) 1);


209 
val UN_singleton_lemma = result();


210 
val UN_singleton = ballI RSN (2,UN_singleton_lemma);


211 


212 
goal ZF.thy "!!A. [ a: A; ALL y:A. b(y)=b(a) ] ==> (INT y:A. b(y)) = b(a)";


213 
by (fast_tac (eq_cs addSEs [equalityE]) 1);


214 
val INT_singleton_lemma = result();


215 
val INT_singleton = ballI RSN (2,INT_singleton_lemma);


216 


217 
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:


218 
Union of a family of unions **)


219 

192

220 
goal ZF.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))";

0

221 
by (fast_tac eq_cs 1);


222 
val UN_Un_distrib = result();


223 


224 
goal ZF.thy


225 
"!!A B. i:I ==> \

192

226 
\ (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";

0

227 
by (fast_tac eq_cs 1);


228 
val INT_Int_distrib = result();


229 


230 
(** Devlin, page 12, exercise 5: Complements **)


231 


232 
goal ZF.thy "!!A B. i:I ==> B  (UN i:I. A(i)) = (INT i:I. B  A(i))";


233 
by (fast_tac eq_cs 1);


234 
val Diff_UN = result();


235 


236 
goal ZF.thy "!!A B. i:I ==> B  (INT i:I. A(i)) = (UN i:I. B  A(i))";


237 
by (fast_tac eq_cs 1);


238 
val Diff_INT = result();


239 


240 
(** Unions and Intersections with General Sum **)


241 

182

242 
goal ZF.thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";


243 
by (fast_tac eq_cs 1);


244 
val SUM_UN_distrib1 = result();


245 

192

246 
goal ZF.thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";

182

247 
by (fast_tac eq_cs 1);


248 
val SUM_UN_distrib2 = result();


249 

192

250 
goal ZF.thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";

0

251 
by (fast_tac eq_cs 1);


252 
val SUM_Un_distrib1 = result();


253 

192

254 
goal ZF.thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";

0

255 
by (fast_tac eq_cs 1);


256 
val SUM_Un_distrib2 = result();


257 

192

258 
goal ZF.thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";

0

259 
by (fast_tac eq_cs 1);


260 
val SUM_Int_distrib1 = result();


261 


262 
goal ZF.thy

192

263 
"(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";

0

264 
by (fast_tac eq_cs 1);


265 
val SUM_Int_distrib2 = result();


266 

192

267 
(*Cf Aczel, NonWellFounded Sets, page 115*)


268 
goal ZF.thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";


269 
by (fast_tac eq_cs 1);


270 
val SUM_eq_UN = result();


271 

0

272 
(** Domain, Range and Field **)


273 


274 
goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";


275 
by (fast_tac eq_cs 1);


276 
val domain_Un_eq = result();


277 


278 
goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)";


279 
by (fast_tac eq_cs 1);


280 
val domain_Int_subset = result();


281 


282 
goal ZF.thy "domain(A)  domain(B) <= domain(A  B)";


283 
by (fast_tac eq_cs 1);


284 
val domain_diff_subset = result();


285 


286 
goal ZF.thy "range(A Un B) = range(A) Un range(B)";


287 
by (fast_tac eq_cs 1);


288 
val range_Un_eq = result();


289 


290 
goal ZF.thy "range(A Int B) <= range(A) Int range(B)";


291 
by (fast_tac eq_cs 1);


292 
val range_Int_subset = result();


293 


294 
goal ZF.thy "range(A)  range(B) <= range(A  B)";


295 
by (fast_tac eq_cs 1);


296 
val range_diff_subset = result();


297 


298 
goal ZF.thy "field(A Un B) = field(A) Un field(B)";


299 
by (fast_tac eq_cs 1);


300 
val field_Un_eq = result();


301 


302 
goal ZF.thy "field(A Int B) <= field(A) Int field(B)";


303 
by (fast_tac eq_cs 1);


304 
val field_Int_subset = result();


305 


306 
goal ZF.thy "field(A)  field(B) <= field(A  B)";


307 
by (fast_tac eq_cs 1);


308 
val field_diff_subset = result();


309 


310 


311 
(** Converse **)


312 


313 
goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)";


314 
by (fast_tac eq_cs 1);


315 
val converse_Un = result();


316 


317 
goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)";


318 
by (fast_tac eq_cs 1);


319 
val converse_Int = result();


320 


321 
goal ZF.thy "converse(A)  converse(B) = converse(A  B)";


322 
by (fast_tac eq_cs 1);


323 
val converse_diff = result();


324 

198

325 
(** Pow **)


326 


327 
goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";


328 
by (fast_tac upair_cs 1);


329 
val Un_Pow_subset = result();


330 


331 
goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";


332 
by (fast_tac upair_cs 1);


333 
val UN_Pow_subset = result();


334 


335 
goal ZF.thy "A <= Pow(Union(A))";


336 
by (fast_tac upair_cs 1);


337 
val subset_Pow_Union = result();


338 


339 
goal ZF.thy "Union(Pow(A)) = A";


340 
by (fast_tac eq_cs 1);


341 
val Union_Pow_eq = result();


342 


343 
goal ZF.thy "Pow(A) Int Pow(B) = Pow(A Int B)";


344 
by (fast_tac eq_cs 1);


345 
val Int_Pow_eq = result();


346 


347 
goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";


348 
by (fast_tac eq_cs 1);


349 
val INT_Pow_subset = result();
