author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1609  5324067d993f 
permissions  rwrr 
1461  1 
(* Title: ZF/Cardinal_AC.ML 
484  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
484  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); 

1461  17 
by (etac well_ord_cardinal_eqpoll 1); 
760  18 
qed "cardinal_eqpoll"; 
484  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); 

1461  25 
by (rtac well_ord_cardinal_eqE 1); 
484  26 
by (REPEAT_SOME assume_tac); 
760  27 
qed "cardinal_eqE"; 
484  28 

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

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

1461  31 
by (etac well_ord_lepoll_imp_Card_le 1); 
484  32 
by (assume_tac 1); 
766  33 
qed "lepoll_imp_Card_le"; 
484  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); 

1461  39 
by (rtac well_ord_cadd_assoc 1); 
484  40 
by (REPEAT_SOME assume_tac); 
760  41 
qed "cadd_assoc"; 
484  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); 

1461  47 
by (rtac well_ord_cmult_assoc 1); 
484  48 
by (REPEAT_SOME assume_tac); 
760  49 
qed "cmult_assoc"; 
484  50 

847  51 
goal Cardinal_AC.thy "(i + j) * k = (i * k) + (j * k)"; 
52 
by (resolve_tac [AC_well_ord RS exE] 1); 

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

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

1461  55 
by (rtac well_ord_cadd_cmult_distrib 1); 
847  56 
by (REPEAT_SOME assume_tac); 
57 
qed "cadd_cmult_distrib"; 

58 

484  59 
goal Cardinal_AC.thy "!!A. InfCard(A) ==> A*A eqpoll A"; 
60 
by (resolve_tac [AC_well_ord RS exE] 1); 

1461  61 
by (etac well_ord_InfCard_square_eq 1); 
484  62 
by (assume_tac 1); 
760  63 
qed "InfCard_square_eq"; 
484  64 

65 

66 
(*** Other applications of AC ***) 

67 

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

69 
by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS 

1461  70 
lepoll_trans] 1); 
484  71 
by (eresolve_tac [le_imp_subset RS subset_imp_lepoll RS lepoll_trans] 1); 
72 
by (resolve_tac [cardinal_eqpoll RS eqpoll_imp_lepoll] 1); 

766  73 
qed "Card_le_imp_lepoll"; 
484  74 

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

76 
by (eresolve_tac [Card_cardinal_eq RS subst] 1 THEN 

77 
rtac iffI 1 THEN 

766  78 
DEPTH_SOLVE (eresolve_tac [Card_le_imp_lepoll,lepoll_imp_Card_le] 1)); 
760  79 
qed "le_Card_iff"; 
484  80 

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

82 
by (etac CollectE 1); 

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

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

1461  85 
by (rtac exI 1); 
484  86 
by (rtac f_imp_injective 1); 
1461  87 
by (rtac Pi_type 1 THEN assume_tac 1); 
683
8fe0fbd76887
Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE
lcp
parents:
517
diff
changeset

88 
by (fast_tac (ZF_cs addDs [apply_type] addDs [Pi_memberD]) 1); 
484  89 
by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1); 
760  90 
qed "surj_implies_inj"; 
484  91 

92 
(*Kunen's Lemma 10.20*) 

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

1461  94 
by (rtac lepoll_imp_Card_le 1); 
484  95 
by (eresolve_tac [surj_implies_inj RS exE] 1); 
96 
by (rewtac lepoll_def); 

1461  97 
by (etac exI 1); 
760  98 
qed "surj_implies_cardinal_le"; 
484  99 

100 
(*Kunen's Lemma 10.21*) 

101 
goal Cardinal_AC.thy 

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

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

1461  104 
by (rtac lepoll_trans 1); 
484  105 
by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2); 
106 
by (asm_simp_tac (ZF_ss addsimps [InfCard_is_Card, Card_cardinal_eq]) 2); 

1461  107 
by (rewtac lepoll_def); 
484  108 
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); 
109 
by (etac (AC_ball_Pi RS exE) 1); 

1461  110 
by (rtac exI 1); 
484  111 
(*Lemma needed in both subgoals, for a fixed z*) 
112 
by (subgoal_tac 

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

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

115 
addSEs [LeastI, Ord_in_Ord]) 2); 

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

1461  117 
("d", "%<i,j>. converse(f`i) ` j")] 
118 
lam_injective 1); 

484  119 
(*Instantiate the lemma proved above*) 
120 
by (ALLGOALS ball_tac); 

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

122 
addDs [apply_type]) 1); 

1461  123 
by (dtac apply_type 1); 
124 
by (etac conjunct2 1); 

484  125 
by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1); 
760  126 
qed "cardinal_UN_le"; 
484  127 

488  128 
(*The same again, using csucc*) 
484  129 
goal Cardinal_AC.thy 
130 
"!!K. [ InfCard(K); ALL i:K. X(i) < csucc(K) ] ==> \ 

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

132 
by (asm_full_simp_tac 

133 
(ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le, 

1461  134 
InfCard_is_Card, Card_cardinal]) 1); 
760  135 
qed "cardinal_UN_lt_csucc"; 
488  136 

785  137 
(*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i), 
138 
the least ordinal j such that i:Vfrom(A,j). *) 

488  139 
goal Cardinal_AC.thy 
140 
"!!K. [ InfCard(K); ALL i:K. j(i) < csucc(K) ] ==> \ 

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

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

143 
by (assume_tac 1); 

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

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

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

760  147 
qed "cardinal_UN_Ord_lt_csucc"; 
488  148 

517  149 

785  150 
(** Main result for infinitebranching datatypes. As above, but the index 
151 
set need not be a cardinal. Surprisingly complicated proof! 

152 
**) 

153 

517  154 
(*Saves checking Ord(j) below*) 
155 
goal Ordinal.thy "!!i j. [ i <= j; j<k; Ord(i) ] ==> i<k"; 

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

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

760  158 
qed "lt_subset_trans"; 
517  159 

785  160 
(*Work backwards along the injection from W into K, given that W~=0.*) 
161 
goal Perm.thy 

1461  162 
"!!A. [ f: inj(A,B); a:A ] ==> \ 
785  163 
\ (UN x:A. C(x)) <= (UN y:B. C(if(y: range(f), converse(f)`y, a)))"; 
1461  164 
by (rtac UN_least 1); 
785  165 
by (res_inst_tac [("x1", "f`x")] (UN_upper RSN (2,subset_trans)) 1); 
166 
by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2); 

167 
by (asm_simp_tac 

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

169 
val inj_UN_subset = result(); 

170 

171 
(*Simpler to require W=K; we'd have a bijection; but the theorem would 

172 
be weaker.*) 

516  173 
goal Cardinal_AC.thy 
517  174 
"!!K. [ InfCard(K); W le K; ALL w:W. j(w) < csucc(K) ] ==> \ 
175 
\ (UN w:W. j(w)) < csucc(K)"; 

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

1461  177 
by (asm_simp_tac (*solve the easy 0 case*) 
517  178 
(ZF_ss addsimps [UN_0, InfCard_is_Card, Card_is_Ord RS Card_csucc, 
1461  179 
Card_is_Ord, Ord_0_lt_csucc]) 2); 
516  180 
by (asm_full_simp_tac 
181 
(ZF_ss addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1); 

517  182 
by (safe_tac eq_cs); 
785  183 
by (swap_res_tac [[inj_UN_subset, cardinal_UN_Ord_lt_csucc] 
1461  184 
MRS lt_subset_trans] 1); 
785  185 
by (REPEAT (assume_tac 1)); 
517  186 
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 2); 
187 
by (asm_simp_tac (ZF_ss addsimps [inj_converse_fun RS apply_type] 

1461  188 
setloop split_tac [expand_if]) 1); 
760  189 
qed "le_UN_Ord_lt_csucc"; 
516  190 