484

1 
(* Title: ZF/Cardinal_AC.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
Cardinal arithmetic WITH the Axiom of Choice

517

7 


8 
These results help justify infinitebranching datatypes

484

9 
*)


10 


11 
open Cardinal_AC;


12 


13 
(*** Strengthened versions of existing theorems about cardinals ***)


14 


15 
goal Cardinal_AC.thy "A eqpoll A";


16 
by (resolve_tac [AC_well_ord RS exE] 1);


17 
by (eresolve_tac [well_ord_cardinal_eqpoll] 1);


18 
val cardinal_eqpoll = result();


19 


20 
val cardinal_idem = cardinal_eqpoll RS cardinal_cong;


21 


22 
goal Cardinal_AC.thy "!!X Y. X = Y ==> X eqpoll Y";


23 
by (resolve_tac [AC_well_ord RS exE] 1);


24 
by (resolve_tac [AC_well_ord RS exE] 1);


25 
by (resolve_tac [well_ord_cardinal_eqE] 1);


26 
by (REPEAT_SOME assume_tac);


27 
val cardinal_eqE = result();


28 


29 
goal Cardinal_AC.thy "!!A B. A lepoll B ==> A le B";


30 
by (resolve_tac [AC_well_ord RS exE] 1);


31 
by (eresolve_tac [well_ord_lepoll_imp_le] 1);


32 
by (assume_tac 1);


33 
val lepoll_imp_le = result();


34 


35 
goal Cardinal_AC.thy "(i + j) + k = i + (j + k)";


36 
by (resolve_tac [AC_well_ord RS exE] 1);


37 
by (resolve_tac [AC_well_ord RS exE] 1);


38 
by (resolve_tac [AC_well_ord RS exE] 1);


39 
by (resolve_tac [well_ord_cadd_assoc] 1);


40 
by (REPEAT_SOME assume_tac);


41 
val cadd_assoc = result();


42 


43 
goal Cardinal_AC.thy "(i * j) * k = i * (j * k)";


44 
by (resolve_tac [AC_well_ord RS exE] 1);


45 
by (resolve_tac [AC_well_ord RS exE] 1);


46 
by (resolve_tac [AC_well_ord RS exE] 1);


47 
by (resolve_tac [well_ord_cmult_assoc] 1);


48 
by (REPEAT_SOME assume_tac);


49 
val cmult_assoc = result();


50 


51 
goal Cardinal_AC.thy "!!A. InfCard(A) ==> A*A eqpoll A";


52 
by (resolve_tac [AC_well_ord RS exE] 1);


53 
by (eresolve_tac [well_ord_InfCard_square_eq] 1);


54 
by (assume_tac 1);


55 
val InfCard_square_eq = result();


56 


57 


58 
(*** Other applications of AC ***)


59 


60 
goal Cardinal_AC.thy "!!A B. A le B ==> A lepoll B";


61 
by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS


62 
lepoll_trans] 1);


63 
by (eresolve_tac [le_imp_subset RS subset_imp_lepoll RS lepoll_trans] 1);


64 
by (resolve_tac [cardinal_eqpoll RS eqpoll_imp_lepoll] 1);


65 
val le_imp_lepoll = result();


66 


67 
goal Cardinal_AC.thy "!!A K. Card(K) ==> A le K <> A lepoll K";


68 
by (eresolve_tac [Card_cardinal_eq RS subst] 1 THEN


69 
rtac iffI 1 THEN


70 
DEPTH_SOLVE (eresolve_tac [le_imp_lepoll,lepoll_imp_le] 1));


71 
val le_Card_iff = result();


72 


73 
goalw Cardinal_AC.thy [surj_def] "!!f. f: surj(X,Y) ==> EX g. g: inj(Y,X)";


74 
by (etac CollectE 1);


75 
by (res_inst_tac [("A1", "Y"), ("B1", "%y. f``{y}")] (AC_Pi RS exE) 1);


76 
by (fast_tac (ZF_cs addSEs [apply_Pair]) 1);


77 
by (resolve_tac [exI] 1);


78 
by (rtac f_imp_injective 1);


79 
by (resolve_tac [Pi_type] 1 THEN assume_tac 1);


80 
by (fast_tac (ZF_cs addDs [apply_type] addEs [memberPiE]) 1);


81 
by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1);


82 
val surj_implies_inj = result();


83 


84 
(*Kunen's Lemma 10.20*)


85 
goal Cardinal_AC.thy "!!f. f: surj(X,Y) ==> Y le X";


86 
by (resolve_tac [lepoll_imp_le] 1);


87 
by (eresolve_tac [surj_implies_inj RS exE] 1);


88 
by (rewtac lepoll_def);


89 
by (eresolve_tac [exI] 1);


90 
val surj_implies_cardinal_le = result();


91 


92 
(*Kunen's Lemma 10.21*)


93 
goal Cardinal_AC.thy


94 
"!!K. [ InfCard(K); ALL i:K. X(i) le K ] ==> UN i:K. X(i) le K";


95 
by (asm_full_simp_tac (ZF_ss addsimps [InfCard_is_Card, le_Card_iff]) 1);


96 
by (resolve_tac [lepoll_trans] 1);


97 
by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2);


98 
by (asm_simp_tac (ZF_ss addsimps [InfCard_is_Card, Card_cardinal_eq]) 2);


99 
by (rewrite_goals_tac [lepoll_def]);


100 
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);


101 
by (etac (AC_ball_Pi RS exE) 1);


102 
by (resolve_tac [exI] 1);


103 
(*Lemma needed in both subgoals, for a fixed z*)


104 
by (subgoal_tac


105 
"ALL z: (UN i:K. X(i)). z: X(LEAST i. z:X(i)) & (LEAST i. z:X(i)) : K" 1);


106 
by (fast_tac (ZF_cs addSIs [Least_le RS lt_trans1 RS ltD, ltI]


107 
addSEs [LeastI, Ord_in_Ord]) 2);


108 
by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"),


109 
("d", "split(%i j. converse(f`i) ` j)")]


110 
lam_injective 1);


111 
(*Instantiate the lemma proved above*)


112 
by (ALLGOALS ball_tac);


113 
by (fast_tac (ZF_cs addEs [inj_is_fun RS apply_type]


114 
addDs [apply_type]) 1);


115 
by (dresolve_tac [apply_type] 1);


116 
by (eresolve_tac [conjunct2] 1);


117 
by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1);


118 
val cardinal_UN_le = result();


119 

488

120 
(*The same again, using csucc*)

484

121 
goal Cardinal_AC.thy


122 
"!!K. [ InfCard(K); ALL i:K. X(i) < csucc(K) ] ==> \


123 
\ UN i:K. X(i) < csucc(K)";


124 
by (asm_full_simp_tac


125 
(ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le,


126 
InfCard_is_Card, Card_cardinal]) 1);


127 
val cardinal_UN_lt_csucc = result();

488

128 


129 
(*The same again, for a union of ordinals*)


130 
goal Cardinal_AC.thy


131 
"!!K. [ InfCard(K); ALL i:K. j(i) < csucc(K) ] ==> \


132 
\ (UN i:K. j(i)) < csucc(K)";


133 
by (resolve_tac [cardinal_UN_lt_csucc RS Card_lt_imp_lt] 1);


134 
by (assume_tac 1);


135 
by (fast_tac (ZF_cs addIs [Ord_cardinal_le RS lt_trans1] addEs [ltE]) 1);


136 
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 1);


137 
by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1);


138 
val cardinal_UN_Ord_lt_csucc = result();


139 

517

140 


141 
(*Saves checking Ord(j) below*)


142 
goal Ordinal.thy "!!i j. [ i <= j; j<k; Ord(i) ] ==> i<k";


143 
by (resolve_tac [subset_imp_le RS lt_trans1] 1);


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


145 
val lt_subset_trans = result();


146 

516

147 
goal Cardinal_AC.thy

517

148 
"!!K. [ InfCard(K); W le K; ALL w:W. j(w) < csucc(K) ] ==> \


149 
\ (UN w:W. j(w)) < csucc(K)";


150 
by (excluded_middle_tac "W=0" 1);


151 
by (asm_simp_tac


152 
(ZF_ss addsimps [UN_0, InfCard_is_Card, Card_is_Ord RS Card_csucc,


153 
Card_is_Ord, Ord_0_lt_csucc]) 2);

516

154 
by (asm_full_simp_tac


155 
(ZF_ss addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1);

517

156 
by (safe_tac eq_cs);


157 
by (eresolve_tac [notE] 1);


158 
by (res_inst_tac [("j1", "%i. j(if(i: range(f), converse(f)`i, x))")]


159 
(cardinal_UN_Ord_lt_csucc RSN (2,lt_subset_trans)) 1);

516

160 
by (assume_tac 2);

517

161 
by (resolve_tac [UN_least] 1);


162 
by (res_inst_tac [("x1", "f`xa")] (UN_upper RSN (2,subset_trans)) 1);


163 
by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2);


164 
by (asm_simp_tac


165 
(ZF_ss addsimps [inj_is_fun RS apply_rangeI, left_inverse]) 1);


166 
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 2);


167 
by (asm_simp_tac (ZF_ss addsimps [inj_converse_fun RS apply_type]


168 
setloop split_tac [expand_if]) 1);


169 
val le_UN_Ord_lt_csucc = result();

516

170 
