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