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 |
|
7 |
|
8 These results help justify infinite-branching datatypes |
|
9 *) |
|
10 |
|
11 (*** Strengthened versions of existing theorems about cardinals ***) |
|
12 |
|
13 Goal "|A| eqpoll A"; |
|
14 by (resolve_tac [AC_well_ord RS exE] 1); |
|
15 by (etac well_ord_cardinal_eqpoll 1); |
|
16 qed "cardinal_eqpoll"; |
|
17 |
|
18 bind_thm ("cardinal_idem", cardinal_eqpoll RS cardinal_cong); |
|
19 |
|
20 Goal "|X| = |Y| ==> X eqpoll Y"; |
|
21 by (resolve_tac [AC_well_ord RS exE] 1); |
|
22 by (resolve_tac [AC_well_ord RS exE] 1); |
|
23 by (rtac well_ord_cardinal_eqE 1); |
|
24 by (REPEAT_SOME assume_tac); |
|
25 qed "cardinal_eqE"; |
|
26 |
|
27 Goal "|X| = |Y| <-> X eqpoll Y"; |
|
28 by (blast_tac (claset() addIs [cardinal_cong, cardinal_eqE]) 1); |
|
29 qed "cardinal_eqpoll_iff"; |
|
30 |
|
31 Goal "[| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] ==> \ |
|
32 \ |A Un C| = |B Un D|"; |
|
33 by (asm_full_simp_tac (simpset() addsimps [cardinal_eqpoll_iff, |
|
34 eqpoll_disjoint_Un]) 1); |
|
35 qed "cardinal_disjoint_Un"; |
|
36 |
|
37 Goal "A lepoll B ==> |A| le |B|"; |
|
38 by (resolve_tac [AC_well_ord RS exE] 1); |
|
39 by (etac well_ord_lepoll_imp_Card_le 1); |
|
40 by (assume_tac 1); |
|
41 qed "lepoll_imp_Card_le"; |
|
42 |
|
43 Goal "(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 (rtac well_ord_cadd_assoc 1); |
|
48 by (REPEAT_SOME assume_tac); |
|
49 qed "cadd_assoc"; |
|
50 |
|
51 Goal "(i |*| j) |*| k = i |*| (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); |
|
55 by (rtac well_ord_cmult_assoc 1); |
|
56 by (REPEAT_SOME assume_tac); |
|
57 qed "cmult_assoc"; |
|
58 |
|
59 Goal "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)"; |
|
60 by (resolve_tac [AC_well_ord RS exE] 1); |
|
61 by (resolve_tac [AC_well_ord RS exE] 1); |
|
62 by (resolve_tac [AC_well_ord RS exE] 1); |
|
63 by (rtac well_ord_cadd_cmult_distrib 1); |
|
64 by (REPEAT_SOME assume_tac); |
|
65 qed "cadd_cmult_distrib"; |
|
66 |
|
67 Goal "InfCard(|A|) ==> A*A eqpoll A"; |
|
68 by (resolve_tac [AC_well_ord RS exE] 1); |
|
69 by (etac well_ord_InfCard_square_eq 1); |
|
70 by (assume_tac 1); |
|
71 qed "InfCard_square_eq"; |
|
72 |
|
73 |
|
74 (*** Other applications of AC ***) |
|
75 |
|
76 Goal "|A| le |B| ==> A lepoll B"; |
|
77 by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS |
|
78 lepoll_trans] 1); |
|
79 by (eresolve_tac [le_imp_subset RS subset_imp_lepoll RS lepoll_trans] 1); |
|
80 by (resolve_tac [cardinal_eqpoll RS eqpoll_imp_lepoll] 1); |
|
81 qed "Card_le_imp_lepoll"; |
|
82 |
|
83 Goal "Card(K) ==> |A| le K <-> A lepoll K"; |
|
84 by (eresolve_tac [Card_cardinal_eq RS subst] 1 THEN |
|
85 rtac iffI 1 THEN |
|
86 DEPTH_SOLVE (eresolve_tac [Card_le_imp_lepoll,lepoll_imp_Card_le] 1)); |
|
87 qed "le_Card_iff"; |
|
88 |
|
89 Goalw [surj_def] "f: surj(X,Y) ==> EX g. g: inj(Y,X)"; |
|
90 by (etac CollectE 1); |
|
91 by (res_inst_tac [("A1", "Y"), ("B1", "%y. f-``{y}")] (AC_Pi RS exE) 1); |
|
92 by (fast_tac (claset() addSEs [apply_Pair]) 1); |
|
93 by (blast_tac (claset() addDs [apply_type, Pi_memberD] |
|
94 addIs [apply_equality, Pi_type, f_imp_injective]) 1); |
|
95 qed "surj_implies_inj"; |
|
96 |
|
97 (*Kunen's Lemma 10.20*) |
|
98 Goal "f: surj(X,Y) ==> |Y| le |X|"; |
|
99 by (rtac lepoll_imp_Card_le 1); |
|
100 by (eresolve_tac [surj_implies_inj RS exE] 1); |
|
101 by (rewtac lepoll_def); |
|
102 by (etac exI 1); |
|
103 qed "surj_implies_cardinal_le"; |
|
104 |
|
105 (*Kunen's Lemma 10.21*) |
|
106 Goal "[| InfCard(K); ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K"; |
|
107 by (asm_full_simp_tac (simpset() addsimps [InfCard_is_Card, le_Card_iff]) 1); |
|
108 by (rtac lepoll_trans 1); |
|
109 by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2); |
|
110 by (asm_simp_tac (simpset() addsimps [InfCard_is_Card, Card_cardinal_eq]) 2); |
|
111 by (rewtac lepoll_def); |
|
112 by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); |
|
113 by (etac (AC_ball_Pi RS exE) 1); |
|
114 by (rtac exI 1); |
|
115 (*Lemma needed in both subgoals, for a fixed z*) |
|
116 by (subgoal_tac |
|
117 "ALL z: (UN i:K. X(i)). z: X(LEAST i. z:X(i)) & (LEAST i. z:X(i)) : K" 1); |
|
118 by (fast_tac (claset() addSIs [Least_le RS lt_trans1 RS ltD, ltI] |
|
119 addSEs [LeastI, Ord_in_Ord]) 2); |
|
120 by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"), |
|
121 ("d", "%<i,j>. converse(f`i) ` j")] |
|
122 lam_injective 1); |
|
123 (*Instantiate the lemma proved above*) |
|
124 by (ALLGOALS ball_tac); |
|
125 by (blast_tac (claset() addIs [inj_is_fun RS apply_type] |
|
126 addDs [apply_type]) 1); |
|
127 by Auto_tac; |
|
128 qed "cardinal_UN_le"; |
|
129 |
|
130 |
|
131 |
|
132 (*The same again, using csucc*) |
|
133 Goal "[| InfCard(K); ALL i:K. |X(i)| < csucc(K) |] ==> \ |
|
134 \ |UN i:K. X(i)| < csucc(K)"; |
|
135 by (asm_full_simp_tac |
|
136 (simpset() addsimps [Card_lt_csucc_iff, cardinal_UN_le, |
|
137 InfCard_is_Card, Card_cardinal]) 1); |
|
138 qed "cardinal_UN_lt_csucc"; |
|
139 |
|
140 (*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i), |
|
141 the least ordinal j such that i:Vfrom(A,j). *) |
|
142 Goal "[| InfCard(K); ALL i:K. j(i) < csucc(K) |] ==> \ |
|
143 \ (UN i:K. j(i)) < csucc(K)"; |
|
144 by (resolve_tac [cardinal_UN_lt_csucc RS Card_lt_imp_lt] 1); |
|
145 by (assume_tac 1); |
|
146 by (blast_tac (claset() addIs [Ord_cardinal_le RS lt_trans1] addEs [ltE]) 1); |
|
147 by (blast_tac (claset() addSIs [Ord_UN] addEs [ltE]) 1); |
|
148 by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1); |
|
149 qed "cardinal_UN_Ord_lt_csucc"; |
|
150 |
|
151 |
|
152 (** Main result for infinite-branching datatypes. As above, but the index |
|
153 set need not be a cardinal. Surprisingly complicated proof! |
|
154 **) |
|
155 |
|
156 (*Work backwards along the injection from W into K, given that W~=0.*) |
|
157 Goal "[| f: inj(A,B); a:A |] ==> \ |
|
158 \ (UN x:A. C(x)) <= (UN y:B. C(if y: range(f) then converse(f)`y else a))"; |
|
159 by (rtac UN_least 1); |
|
160 by (res_inst_tac [("x1", "f`x")] (UN_upper RSN (2,subset_trans)) 1); |
|
161 by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2); |
|
162 by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_rangeI]) 1); |
|
163 qed "inj_UN_subset"; |
|
164 |
|
165 (*Simpler to require |W|=K; we'd have a bijection; but the theorem would |
|
166 be weaker.*) |
|
167 Goal "[| InfCard(K); |W| le K; ALL w:W. j(w) < csucc(K) |] ==> \ |
|
168 \ (UN w:W. j(w)) < csucc(K)"; |
|
169 by (excluded_middle_tac "W=0" 1); |
|
170 by (asm_simp_tac (*solve the easy 0 case*) |
|
171 (simpset() addsimps [UN_0, InfCard_is_Card, Card_is_Ord RS Card_csucc, |
|
172 Card_is_Ord, Ord_0_lt_csucc]) 2); |
|
173 by (asm_full_simp_tac |
|
174 (simpset() addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1); |
|
175 by (safe_tac (claset() addSIs [equalityI])); |
|
176 by (swap_res_tac [[inj_UN_subset, cardinal_UN_Ord_lt_csucc] |
|
177 MRS lt_subset_trans] 1); |
|
178 by (REPEAT (assume_tac 1)); |
|
179 by (blast_tac (claset() addSIs [Ord_UN] addEs [ltE]) 2); |
|
180 by (asm_simp_tac (simpset() addsimps [inj_converse_fun RS apply_type]) 1); |
|
181 qed "le_UN_Ord_lt_csucc"; |
|
182 |
|