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 


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


221 
by (fast_tac eq_cs 1);


222 
val UN_Un_distrib = result();


223 


224 
goal ZF.thy


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


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


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 


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


243 
by (fast_tac eq_cs 1);


244 
val SUM_Un_distrib1 = result();


245 


246 
goal ZF.thy


247 
"(SUM i:I. A(x) Un B(x)) = (SUM i:I. A(x)) Un (SUM i:I. B(x))";


248 
by (fast_tac eq_cs 1);


249 
val SUM_Un_distrib2 = result();


250 


251 
goal ZF.thy "(SUM x:A Int B. C(x)) = (SUM x:A. C(x)) Int (SUM x:B. C(x))";


252 
by (fast_tac eq_cs 1);


253 
val SUM_Int_distrib1 = result();


254 


255 
goal ZF.thy


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


257 
by (fast_tac eq_cs 1);


258 
val SUM_Int_distrib2 = result();


259 


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


261 


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


263 
by (fast_tac eq_cs 1);


264 
val domain_Un_eq = result();


265 


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


267 
by (fast_tac eq_cs 1);


268 
val domain_Int_subset = result();


269 


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


271 
by (fast_tac eq_cs 1);


272 
val domain_diff_subset = result();


273 


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


275 
by (fast_tac eq_cs 1);


276 
val range_Un_eq = result();


277 


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


279 
by (fast_tac eq_cs 1);


280 
val range_Int_subset = result();


281 


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


283 
by (fast_tac eq_cs 1);


284 
val range_diff_subset = result();


285 


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


287 
by (fast_tac eq_cs 1);


288 
val field_Un_eq = result();


289 


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


291 
by (fast_tac eq_cs 1);


292 
val field_Int_subset = result();


293 


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


295 
by (fast_tac eq_cs 1);


296 
val field_diff_subset = result();


297 


298 


299 
(** Converse **)


300 


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


302 
by (fast_tac eq_cs 1);


303 
val converse_Un = result();


304 


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


306 
by (fast_tac eq_cs 1);


307 
val converse_Int = result();


308 


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


310 
by (fast_tac eq_cs 1);


311 
val converse_diff = result();


312 
