author | paulson |
Thu, 21 Mar 1996 13:02:26 +0100 | |
changeset 1601 | 0ef6ea27ab15 |
parent 1461 | 6bcb44e4d6e5 |
child 1609 | 5324067d993f |
permissions | -rw-r--r-- |
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 infinite-branching 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 infinite-branching 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 |