435

1 
(* Title: ZF/Cardinal.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
Cardinals in ZermeloFraenkel Set Theory


7 


8 
This theory does NOT assume the Axiom of Choice


9 
*)


10 


11 
open Cardinal;


12 


13 
(*** The SchroederBernstein Theorem  see Davey & Priestly, page 106 ***)


14 


15 
(** Lemma: Banach's Decomposition Theorem **)


16 


17 
goal Cardinal.thy "bnd_mono(X, %W. X  g``(Y  f``W))";


18 
by (rtac bnd_monoI 1);


19 
by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1));


20 
val decomp_bnd_mono = result();


21 


22 
val [gfun] = goal Cardinal.thy


23 
"g: Y>X ==> \


24 
\ g``(Y  f`` lfp(X, %W. X  g``(Y  f``W))) = \


25 
\ X  lfp(X, %W. X  g``(Y  f``W)) ";


26 
by (res_inst_tac [("P", "%u. ?v = Xu")]


27 
(decomp_bnd_mono RS lfp_Tarski RS ssubst) 1);


28 
by (simp_tac (ZF_ss addsimps [subset_refl, double_complement,


29 
gfun RS fun_is_rel RS image_subset]) 1);


30 
val Banach_last_equation = result();


31 


32 
val prems = goal Cardinal.thy


33 
"[ f: X>Y; g: Y>X ] ==> \


34 
\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \


35 
\ (YA Int YB = 0) & (YA Un YB = Y) & \


36 
\ f``XA=YA & g``YB=XB";


37 
by (REPEAT


38 
(FIRSTGOAL


39 
(resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition])));


40 
by (rtac Banach_last_equation 3);


41 
by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1));


42 
val decomposition = result();


43 


44 
val prems = goal Cardinal.thy


45 
"[ f: inj(X,Y); g: inj(Y,X) ] ==> EX h. h: bij(X,Y)";


46 
by (cut_facts_tac prems 1);


47 
by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1);


48 
by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un]


49 
addIs [bij_converse_bij]) 1);


50 
(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"


51 
is forced by the context!! *)


52 
val schroeder_bernstein = result();


53 


54 


55 
(** Equipollence is an equivalence relation **)


56 


57 
goalw Cardinal.thy [eqpoll_def] "X eqpoll X";

437

58 
by (rtac exI 1);


59 
by (rtac id_bij 1);

435

60 
val eqpoll_refl = result();


61 


62 
goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X";


63 
by (fast_tac (ZF_cs addIs [bij_converse_bij]) 1);


64 
val eqpoll_sym = result();


65 


66 
goalw Cardinal.thy [eqpoll_def]


67 
"!!X Y. [ X eqpoll Y; Y eqpoll Z ] ==> X eqpoll Z";


68 
by (fast_tac (ZF_cs addIs [comp_bij]) 1);


69 
val eqpoll_trans = result();


70 


71 
(** Lepollence is a partial ordering **)


72 


73 
goalw Cardinal.thy [lepoll_def] "!!X Y. X<=Y ==> X lepoll Y";

437

74 
by (rtac exI 1);


75 
by (etac id_subset_inj 1);

435

76 
val subset_imp_lepoll = result();


77 


78 
val lepoll_refl = subset_refl RS subset_imp_lepoll;


79 


80 
goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def]


81 
"!!X Y. X eqpoll Y ==> X lepoll Y";


82 
by (fast_tac ZF_cs 1);


83 
val eqpoll_imp_lepoll = result();


84 


85 
goalw Cardinal.thy [lepoll_def]


86 
"!!X Y. [ X lepoll Y; Y lepoll Z ] ==> X lepoll Z";


87 
by (fast_tac (ZF_cs addIs [comp_inj]) 1);


88 
val lepoll_trans = result();


89 


90 
(*Asymmetry law*)


91 
goalw Cardinal.thy [lepoll_def,eqpoll_def]


92 
"!!X Y. [ X lepoll Y; Y lepoll X ] ==> X eqpoll Y";


93 
by (REPEAT (etac exE 1));


94 
by (rtac schroeder_bernstein 1);


95 
by (REPEAT (assume_tac 1));


96 
val eqpollI = result();


97 


98 
val [major,minor] = goal Cardinal.thy


99 
"[ X eqpoll Y; [ X lepoll Y; Y lepoll X ] ==> P ] ==> P";

437

100 
by (rtac minor 1);

435

101 
by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1));


102 
val eqpollE = result();


103 


104 
goal Cardinal.thy "X eqpoll Y <> X lepoll Y & Y lepoll X";


105 
by (fast_tac (ZF_cs addIs [eqpollI] addSEs [eqpollE]) 1);


106 
val eqpoll_iff = result();


107 


108 


109 
(** LEAST  the least number operator [from HOL/Univ.ML] **)


110 


111 
val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def]


112 
"[ P(i); Ord(i); !!x. x<i ==> ~P(x) ] ==> (LEAST x.P(x)) = i";


113 
by (rtac the_equality 1);


114 
by (fast_tac (ZF_cs addSIs [premP,premOrd,premNot]) 1);


115 
by (REPEAT (etac conjE 1));

437

116 
by (etac (premOrd RS Ord_linear_lt) 1);

435

117 
by (ALLGOALS (fast_tac (ZF_cs addSIs [premP] addSDs [premNot])));


118 
val Least_equality = result();


119 


120 
goal Cardinal.thy "!!i. [ P(i); Ord(i) ] ==> P(LEAST x.P(x))";


121 
by (etac rev_mp 1);


122 
by (trans_ind_tac "i" [] 1);


123 
by (rtac impI 1);


124 
by (rtac classical 1);


125 
by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);


126 
by (assume_tac 2);


127 
by (fast_tac (ZF_cs addSEs [ltE]) 1);


128 
val LeastI = result();


129 


130 
(*Proof is almost identical to the one above!*)


131 
goal Cardinal.thy "!!i. [ P(i); Ord(i) ] ==> (LEAST x.P(x)) le i";


132 
by (etac rev_mp 1);


133 
by (trans_ind_tac "i" [] 1);


134 
by (rtac impI 1);


135 
by (rtac classical 1);


136 
by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);


137 
by (etac le_refl 2);


138 
by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1);


139 
val Least_le = result();


140 


141 
(*LEAST really is the smallest*)


142 
goal Cardinal.thy "!!i. [ P(i); i < (LEAST x.P(x)) ] ==> Q";

437

143 
by (rtac (Least_le RSN (2,lt_trans2) RS lt_irrefl) 1);

435

144 
by (REPEAT (eresolve_tac [asm_rl, ltE] 1));


145 
val less_LeastE = result();


146 

437

147 
(*If there is no such P then LEAST is vacuously 0*)


148 
goalw Cardinal.thy [Least_def]


149 
"!!P. [ ~ (EX i. Ord(i) & P(i)) ] ==> (LEAST x.P(x)) = 0";


150 
by (rtac the_0 1);


151 
by (fast_tac ZF_cs 1);


152 
val Least_0 = result();


153 

435

154 
goal Cardinal.thy "Ord(LEAST x.P(x))";

437

155 
by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1);

435

156 
by (safe_tac ZF_cs);

437

157 
by (rtac (Least_le RS ltE) 2);

435

158 
by (REPEAT_SOME assume_tac);

437

159 
by (etac (Least_0 RS ssubst) 1);


160 
by (rtac Ord_0 1);

435

161 
val Ord_Least = result();


162 


163 


164 
(** Basic properties of cardinals **)


165 


166 
(*Not needed for simplification, but helpful below*)


167 
val prems = goal Cardinal.thy


168 
"[ !!y. P(y) <> Q(y) ] ==> (LEAST x.P(x)) = (LEAST x.Q(x))";


169 
by (simp_tac (FOL_ss addsimps prems) 1);


170 
val Least_cong = result();


171 


172 
(*Need AC to prove X lepoll Y ==> X le Y ; see well_ord_lepoll_imp_le *)


173 
goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> X = Y";

437

174 
by (rtac Least_cong 1);

435

175 
by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1);


176 
val cardinal_cong = result();


177 


178 
(*Under AC, the premise becomes trivial; one consequence is A = A*)


179 
goalw Cardinal.thy [eqpoll_def, cardinal_def]


180 
"!!A. well_ord(A,r) ==> A eqpoll A";

437

181 
by (rtac LeastI 1);


182 
by (etac Ord_ordertype 2);


183 
by (rtac exI 1);


184 
by (etac (ordertype_bij RS bij_converse_bij) 1);

435

185 
val well_ord_cardinal_eqpoll = result();


186 


187 
val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll


188 
> standard;


189 


190 
goal Cardinal.thy


191 
"!!X Y. [ well_ord(X,r); well_ord(Y,s); X = Y ] ==> X eqpoll Y";

437

192 
by (rtac (eqpoll_sym RS eqpoll_trans) 1);


193 
by (etac well_ord_cardinal_eqpoll 1);

435

194 
by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1);


195 
val well_ord_cardinal_eqE = result();


196 


197 


198 
(** Observations from Kunen, page 28 **)


199 


200 
goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> i le i";

437

201 
by (etac (eqpoll_refl RS Least_le) 1);

435

202 
val Ord_cardinal_le = result();


203 


204 
goalw Cardinal.thy [Card_def] "!!i. Card(i) ==> i = i";

437

205 
by (etac sym 1);

435

206 
val Card_cardinal_eq = result();


207 


208 
val prems = goalw Cardinal.thy [Card_def,cardinal_def]


209 
"[ Ord(i); !!j. j<i ==> ~(j eqpoll i) ] ==> Card(i)";

437

210 
by (rtac (Least_equality RS ssubst) 1);

435

211 
by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1));


212 
val CardI = result();


213 


214 
goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)";

437

215 
by (etac ssubst 1);


216 
by (rtac Ord_Least 1);

435

217 
val Card_is_Ord = result();


218 

437

219 
goalw Cardinal.thy [cardinal_def] "Ord( A )";


220 
by (rtac Ord_Least 1);

435

221 
val Ord_cardinal = result();


222 

437

223 
goal Cardinal.thy "Card(0)";


224 
by (rtac (Ord_0 RS CardI) 1);


225 
by (fast_tac (ZF_cs addSEs [ltE]) 1);


226 
val Card_0 = result();


227 


228 
goalw Cardinal.thy [cardinal_def] "Card( A )";


229 
by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1);


230 
by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1);


231 
by (rtac (Ord_Least RS CardI) 1);


232 
by (safe_tac ZF_cs);


233 
by (rtac less_LeastE 1);


234 
by (assume_tac 2);


235 
by (etac eqpoll_trans 1);


236 
by (REPEAT (ares_tac [LeastI] 1));


237 
val Card_cardinal = result();


238 

435

239 
(*Kunen's Lemma 10.5*)


240 
goal Cardinal.thy "!!i j. [ i le j; j le i ] ==> j = i";

437

241 
by (rtac (eqpollI RS cardinal_cong) 1);


242 
by (etac (le_imp_subset RS subset_imp_lepoll) 1);


243 
by (rtac lepoll_trans 1);


244 
by (etac (le_imp_subset RS subset_imp_lepoll) 2);


245 
by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1);


246 
by (rtac Ord_cardinal_eqpoll 1);

435

247 
by (REPEAT (eresolve_tac [ltE, Ord_succD] 1));


248 
val cardinal_eq_lemma = result();


249 


250 
goal Cardinal.thy "!!i j. i le j ==> i le j";


251 
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);


252 
by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));

437

253 
by (rtac cardinal_eq_lemma 1);


254 
by (assume_tac 2);


255 
by (etac le_trans 1);


256 
by (etac ltE 1);


257 
by (etac Ord_cardinal_le 1);

435

258 
val cardinal_mono = result();


259 


260 
(*Since we have succ(nat) le nat, the converse of cardinal_mono fails!*)


261 
goal Cardinal.thy "!!i j. [ i < j; Ord(i); Ord(j) ] ==> i < j";

437

262 
by (rtac Ord_linear2 1);

435

263 
by (REPEAT_SOME assume_tac);

437

264 
by (etac (lt_trans2 RS lt_irrefl) 1);


265 
by (etac cardinal_mono 1);

435

266 
val cardinal_lt_imp_lt = result();


267 


268 
goal Cardinal.thy "!!i j. [ i < k; Ord(i); Card(k) ] ==> i < k";


269 
by (asm_simp_tac (ZF_ss addsimps


270 
[cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1);


271 
val Card_lt_imp_lt = result();


272 


273 


274 
(** The swap operator [NOT USED] **)


275 


276 
goalw Cardinal.thy [swap_def]


277 
"!!A. [ x:A; y:A ] ==> swap(A,x,y) : A>A";


278 
by (REPEAT (ares_tac [lam_type,if_type] 1));


279 
val swap_type = result();


280 


281 
goalw Cardinal.thy [swap_def]


282 
"!!A. [ x:A; y:A; z:A ] ==> swap(A,x,y)`(swap(A,x,y)`z) = z";


283 
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);


284 
val swap_swap_identity = result();


285 


286 
goal Cardinal.thy "!!A. [ x:A; y:A ] ==> swap(A,x,y) : bij(A,A)";

437

287 
by (rtac nilpotent_imp_bijective 1);

435

288 
by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2,


289 
ballI, swap_swap_identity] 1));


290 
val swap_bij = result();


291 


292 
(*** The finite cardinals ***)


293 


294 
(*Lemma suggested by Mike Fourman*)


295 
val [prem] = goalw Cardinal.thy [inj_def]


296 
"f: inj(succ(m), succ(n)) ==> (lam x:m. if(f`x=n, f`m, f`x)) : inj(m,n)";

437

297 
by (rtac CollectI 1);

435

298 
(*Proving it's in the function space m>n*)


299 
by (cut_facts_tac [prem] 1);

437

300 
by (rtac (if_type RS lam_type) 1);


301 
by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS succE]) 1);


302 
by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS succE]) 1);

435

303 
(*Proving it's injective*)


304 
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);


305 
(*Adding prem earlier would cause the simplifier to loop*)


306 
by (cut_facts_tac [prem] 1);

437

307 
by (fast_tac (ZF_cs addSEs [mem_irrefl]) 1);

435

308 
val inj_succ_succD = result();


309 


310 
val [prem] = goalw Cardinal.thy [lepoll_def]


311 
"m:nat ==> ALL n: nat. m lepoll n > m le n";


312 
by (nat_ind_tac "m" [prem] 1);


313 
by (fast_tac (ZF_cs addSIs [nat_0_le]) 1);

437

314 
by (rtac ballI 1);

435

315 
by (eres_inst_tac [("n","n")] natE 1);


316 
by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1);


317 
by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1);


318 
val nat_lepoll_imp_le_lemma = result();


319 
val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp > standard;


320 


321 
goal Cardinal.thy


322 
"!!m n. [ m:nat; n: nat ] ==> m eqpoll n <> m = n";

437

323 
by (rtac iffI 1);

435

324 
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2);

437

325 
by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_anti_sym]


326 
addSEs [eqpollE]) 1);

435

327 
val nat_eqpoll_iff = result();


328 


329 
goalw Cardinal.thy [Card_def,cardinal_def]


330 
"!!n. n: nat ==> Card(n)";

437

331 
by (rtac (Least_equality RS ssubst) 1);

435

332 
by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl]));


333 
by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1);

437

334 
by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1);

435

335 
val nat_into_Card = result();


336 


337 
(*Part of Kunen's Lemma 10.6*)


338 
goal Cardinal.thy "!!n. [ succ(n) lepoll n; n:nat ] ==> P";

437

339 
by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1);

435

340 
by (REPEAT (ares_tac [nat_succI] 1));


341 
val succ_lepoll_natE = result();


342 


343 


344 
(*** The first infinite cardinal: Omega, or nat ***)


345 


346 
(*This implies Kunen's Lemma 10.6*)


347 
goal Cardinal.thy "!!n. [ n<i; n:nat ] ==> ~ i lepoll n";

437

348 
by (rtac notI 1);

435

349 
by (rtac succ_lepoll_natE 1 THEN assume_tac 2);


350 
by (rtac lepoll_trans 1 THEN assume_tac 2);

437

351 
by (etac ltE 1);

435

352 
by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1));


353 
val lt_not_lepoll = result();


354 


355 
goal Cardinal.thy "!!i n. [ Ord(i); n:nat ] ==> i eqpoll n <> i=n";

437

356 
by (rtac iffI 1);

435

357 
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2);


358 
by (rtac Ord_linear_lt 1);


359 
by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord]));


360 
by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN


361 
REPEAT (assume_tac 1));


362 
by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1)));

437

363 
by (etac eqpoll_imp_lepoll 1);

435

364 
val Ord_nat_eqpoll_iff = result();


365 

437

366 
goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)";


367 
by (rtac (Least_equality RS ssubst) 1);


368 
by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl]));


369 
by (etac ltE 1);


370 
by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1);


371 
val Card_nat = result();

435

372 

437

373 
(*Allows showing that i is a limit cardinal*)


374 
goal Cardinal.thy "!!i. nat le i ==> nat le i";


375 
by (rtac (Card_nat RS Card_cardinal_eq RS subst) 1);


376 
by (etac cardinal_mono 1);


377 
val nat_le_cardinal = result();


378 
