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 

435

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


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


63 
val subset_Int_iff2 = result();


64 

0

65 
(** Binary Union **)


66 


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


68 
by (fast_tac eq_cs 1);


69 
val Un_0 = result();


70 


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


72 
by (fast_tac eq_cs 1);


73 
val Un_cons = result();


74 


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


76 
by (fast_tac eq_cs 1);


77 
val Un_absorb = result();


78 


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


80 
by (fast_tac eq_cs 1);


81 
val Un_commute = result();


82 


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


84 
by (fast_tac eq_cs 1);


85 
val Un_assoc = result();


86 


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


88 
by (fast_tac eq_cs 1);


89 
val Un_Int_distrib = result();


90 


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


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


93 
val subset_Un_iff = result();


94 

435

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


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


97 
val subset_Un_iff2 = result();


98 

0

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


100 


101 
goal ZF.thy "AA = 0";


102 
by (fast_tac eq_cs 1);


103 
val Diff_cancel = result();


104 


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


106 
by (fast_tac eq_cs 1);


107 
val empty_Diff = result();


108 


109 
goal ZF.thy "A0 = A";


110 
by (fast_tac eq_cs 1);


111 
val Diff_0 = result();


112 


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


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


115 
by (fast_tac eq_cs 1);


116 
val Diff_cons = result();


117 


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


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


120 
by (fast_tac eq_cs 1);


121 
val Diff_cons2 = result();


122 


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


124 
by (fast_tac eq_cs 1);


125 
val Diff_disjoint = result();


126 


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


128 
by (fast_tac eq_cs 1);


129 
val Diff_partition = result();


130 

268

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

0

132 
by (fast_tac eq_cs 1);


133 
val double_complement = result();


134 

268

135 
goal ZF.thy "(A Un B)  (BA) = A";


136 
by (fast_tac eq_cs 1);


137 
val double_complement_Un = result();


138 

0

139 
goal ZF.thy


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


141 
by (fast_tac eq_cs 1);


142 
val Un_Int_crazy = result();


143 


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


145 
by (fast_tac eq_cs 1);


146 
val Diff_Un = result();


147 


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


149 
by (fast_tac eq_cs 1);


150 
val Diff_Int = result();


151 


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


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


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


155 
val Un_Int_assoc_iff = result();


156 


157 


158 
(** Big Union and Intersection **)


159 


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


161 
by (fast_tac eq_cs 1);


162 
val Union_0 = result();


163 


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


165 
by (fast_tac eq_cs 1);


166 
val Union_cons = result();


167 


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


169 
by (fast_tac eq_cs 1);


170 
val Union_Un_distrib = result();


171 

435

172 
goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)";


173 
by (fast_tac ZF_cs 1);


174 
val Union_Int_subset = result();


175 

0

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


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


178 
val Union_disjoint = result();


179 


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


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


182 
by (fast_tac eq_cs 1);


183 
val Inter_Un_distrib = result();


184 


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


186 
by (fast_tac eq_cs 1);


187 
val Union_singleton = result();


188 


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


190 
by (fast_tac eq_cs 1);


191 
val Inter_singleton = result();


192 


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


194 


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


196 
by (fast_tac eq_cs 1);


197 
val Union_eq_UN = result();


198 


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


200 
by (fast_tac eq_cs 1);


201 
val Inter_eq_INT = result();


202 

517

203 
goal ZF.thy "(UN i:0. A(i)) = 0";


204 
by (fast_tac eq_cs 1);


205 
val UN_0 = result();


206 

0

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


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


209 
by (fast_tac eq_cs 1);


210 
val Int_UN_distrib = result();


211 


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


213 
by (fast_tac eq_cs 1);


214 
val Un_INT_distrib = result();


215 


216 
goal ZF.thy


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


218 
by (fast_tac eq_cs 1);


219 
val Int_UN_distrib2 = result();


220 


221 
goal ZF.thy


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


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


224 
by (fast_tac eq_cs 1);


225 
val Un_INT_distrib2 = result();


226 

435

227 
goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c";


228 
by (fast_tac eq_cs 1);


229 
val UN_constant = result();

0

230 

435

231 
goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c";


232 
by (fast_tac eq_cs 1);


233 
val INT_constant = result();

0

234 


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


236 
Union of a family of unions **)


237 

192

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

0

239 
by (fast_tac eq_cs 1);


240 
val UN_Un_distrib = result();


241 


242 
goal ZF.thy


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

192

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

0

245 
by (fast_tac eq_cs 1);


246 
val INT_Int_distrib = result();


247 


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


249 


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


251 
by (fast_tac eq_cs 1);


252 
val Diff_UN = result();


253 


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


255 
by (fast_tac eq_cs 1);


256 
val Diff_INT = result();


257 


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


259 

182

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


261 
by (fast_tac eq_cs 1);


262 
val SUM_UN_distrib1 = result();


263 

192

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

182

265 
by (fast_tac eq_cs 1);


266 
val SUM_UN_distrib2 = result();


267 

192

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

0

269 
by (fast_tac eq_cs 1);


270 
val SUM_Un_distrib1 = result();


271 

192

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

0

273 
by (fast_tac eq_cs 1);


274 
val SUM_Un_distrib2 = result();


275 

192

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

0

277 
by (fast_tac eq_cs 1);


278 
val SUM_Int_distrib1 = result();


279 


280 
goal ZF.thy

192

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

0

282 
by (fast_tac eq_cs 1);


283 
val SUM_Int_distrib2 = result();


284 

192

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


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


287 
by (fast_tac eq_cs 1);


288 
val SUM_eq_UN = result();


289 

0

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


291 


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


293 
by (fast_tac eq_cs 1);


294 
val domain_Un_eq = result();


295 


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


297 
by (fast_tac eq_cs 1);


298 
val domain_Int_subset = result();


299 


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


301 
by (fast_tac eq_cs 1);


302 
val domain_diff_subset = result();


303 


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


305 
by (fast_tac eq_cs 1);


306 
val range_Un_eq = result();


307 


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

435

309 
by (fast_tac ZF_cs 1);

0

310 
val range_Int_subset = result();


311 


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


313 
by (fast_tac eq_cs 1);


314 
val range_diff_subset = result();


315 


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


317 
by (fast_tac eq_cs 1);


318 
val field_Un_eq = result();


319 


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


321 
by (fast_tac eq_cs 1);


322 
val field_Int_subset = result();


323 


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


325 
by (fast_tac eq_cs 1);


326 
val field_diff_subset = result();


327 


328 

435

329 
(** Image **)


330 


331 
goal ZF.thy "r``0 = 0";


332 
by (fast_tac eq_cs 1);


333 
val image_empty = result();


334 


335 
goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)";


336 
by (fast_tac eq_cs 1);


337 
val image_Un = result();


338 


339 
goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)";


340 
by (fast_tac ZF_cs 1);


341 
val image_Int_subset = result();


342 


343 
goal ZF.thy "(r Int A*A)``B <= (r``B) Int A";


344 
by (fast_tac ZF_cs 1);


345 
val image_Int_square_subset = result();


346 


347 
goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";


348 
by (fast_tac eq_cs 1);


349 
val image_Int_square = result();


350 


351 


352 
(** Inverse Image **)


353 


354 
goal ZF.thy "r``0 = 0";


355 
by (fast_tac eq_cs 1);


356 
val vimage_empty = result();


357 


358 
goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)";


359 
by (fast_tac eq_cs 1);


360 
val vimage_Un = result();


361 


362 
goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)";


363 
by (fast_tac ZF_cs 1);


364 
val vimage_Int_subset = result();


365 


366 
goal ZF.thy "(r Int A*A)``B <= (r``B) Int A";


367 
by (fast_tac ZF_cs 1);


368 
val vimage_Int_square_subset = result();


369 


370 
goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";


371 
by (fast_tac eq_cs 1);


372 
val vimage_Int_square = result();


373 


374 

0

375 
(** Converse **)


376 


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


378 
by (fast_tac eq_cs 1);


379 
val converse_Un = result();


380 


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


382 
by (fast_tac eq_cs 1);


383 
val converse_Int = result();


384 


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


386 
by (fast_tac eq_cs 1);


387 
val converse_diff = result();


388 

198

389 
(** Pow **)


390 


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


392 
by (fast_tac upair_cs 1);


393 
val Un_Pow_subset = result();


394 


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


396 
by (fast_tac upair_cs 1);


397 
val UN_Pow_subset = result();


398 


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


400 
by (fast_tac upair_cs 1);


401 
val subset_Pow_Union = result();


402 


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


404 
by (fast_tac eq_cs 1);


405 
val Union_Pow_eq = result();


406 


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


408 
by (fast_tac eq_cs 1);


409 
val Int_Pow_eq = result();


410 


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


412 
by (fast_tac eq_cs 1);


413 
val INT_Pow_subset = result();

435

414 
