author | clasohm |
Wed, 07 Dec 1994 13:12:04 +0100 | |
changeset 760 | f0200e91b272 |
parent 754 | 521a6f3ff279 |
child 766 | f811d04fa4dd |
permissions | -rw-r--r-- |
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 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); |
|
17 |
by (eresolve_tac [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); |
|
25 |
by (resolve_tac [well_ord_cardinal_eqE] 1); |
|
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); |
|
31 |
by (eresolve_tac [well_ord_lepoll_imp_le] 1); |
|
32 |
by (assume_tac 1); |
|
760 | 33 |
qed "lepoll_imp_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); |
|
39 |
by (resolve_tac [well_ord_cadd_assoc] 1); |
|
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); |
|
47 |
by (resolve_tac [well_ord_cmult_assoc] 1); |
|
48 |
by (REPEAT_SOME assume_tac); |
|
760 | 49 |
qed "cmult_assoc"; |
484 | 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); |
|
760 | 55 |
qed "InfCard_square_eq"; |
484 | 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); |
|
760 | 65 |
qed "le_imp_lepoll"; |
484 | 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)); |
|
760 | 71 |
qed "le_Card_iff"; |
484 | 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); |
|
683
8fe0fbd76887
Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE
lcp
parents:
517
diff
changeset
|
80 |
by (fast_tac (ZF_cs addDs [apply_type] addDs [Pi_memberD]) 1); |
484 | 81 |
by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1); |
760 | 82 |
qed "surj_implies_inj"; |
484 | 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); |
|
760 | 90 |
qed "surj_implies_cardinal_le"; |
484 | 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); |
|
760 | 118 |
qed "cardinal_UN_le"; |
484 | 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); |
|
760 | 127 |
qed "cardinal_UN_lt_csucc"; |
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); |
|
760 | 138 |
qed "cardinal_UN_Ord_lt_csucc"; |
488 | 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)); |
|
760 | 145 |
qed "lt_subset_trans"; |
517 | 146 |
|
754 | 147 |
(*The same yet again, but the index set need not be a cardinal. |
148 |
Surprisingly complicated proof!*) |
|
516 | 149 |
goal Cardinal_AC.thy |
517 | 150 |
"!!K. [| InfCard(K); |W| le K; ALL w:W. j(w) < csucc(K) |] ==> \ |
151 |
\ (UN w:W. j(w)) < csucc(K)"; |
|
152 |
by (excluded_middle_tac "W=0" 1); |
|
153 |
by (asm_simp_tac |
|
154 |
(ZF_ss addsimps [UN_0, InfCard_is_Card, Card_is_Ord RS Card_csucc, |
|
155 |
Card_is_Ord, Ord_0_lt_csucc]) 2); |
|
516 | 156 |
by (asm_full_simp_tac |
157 |
(ZF_ss addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1); |
|
517 | 158 |
by (safe_tac eq_cs); |
159 |
by (eresolve_tac [notE] 1); |
|
160 |
by (res_inst_tac [("j1", "%i. j(if(i: range(f), converse(f)`i, x))")] |
|
161 |
(cardinal_UN_Ord_lt_csucc RSN (2,lt_subset_trans)) 1); |
|
516 | 162 |
by (assume_tac 2); |
517 | 163 |
by (resolve_tac [UN_least] 1); |
164 |
by (res_inst_tac [("x1", "f`xa")] (UN_upper RSN (2,subset_trans)) 1); |
|
165 |
by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2); |
|
166 |
by (asm_simp_tac |
|
167 |
(ZF_ss addsimps [inj_is_fun RS apply_rangeI, left_inverse]) 1); |
|
168 |
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 2); |
|
169 |
by (asm_simp_tac (ZF_ss addsimps [inj_converse_fun RS apply_type] |
|
170 |
setloop split_tac [expand_if]) 1); |
|
760 | 171 |
qed "le_UN_Ord_lt_csucc"; |
516 | 172 |