|
1 (* Title: ZF/AC/AC10_AC15.ML |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Grabczewski |
|
4 |
|
5 The proofs needed to state that AC10, ..., AC15 are equivalent to the rest. |
|
6 We need the following: |
|
7 |
|
8 WO1 ==> AC10(n) ==> AC11 ==> AC12 ==> AC15 ==> WO6 |
|
9 |
|
10 In order to add the formulations AC13 and AC14 we need: |
|
11 |
|
12 AC10(succ(n)) ==> AC13(n) ==> AC14 ==> AC15 |
|
13 |
|
14 or |
|
15 |
|
16 AC1 ==> AC13(1); AC13(m) ==> AC13(n); AC13(n) ==> AC14 ==> AC15 |
|
17 |
|
18 So we don't have to prove all impllications of both cases. |
|
19 Moreover we don't need to prove that AC13(1) ==> AC1, AC11 ==> AC14 as |
|
20 Rubin & Rubin do. |
|
21 *) |
|
22 |
|
23 (* ********************************************************************** *) |
|
24 (* Lemmas used in the proofs in which the conclusion is AC13, AC14 *) |
|
25 (* or AC15 *) |
|
26 (* - cons_times_nat_not_Finite *) |
|
27 (* - ex_fun_AC13_AC15 *) |
|
28 (* ********************************************************************** *) |
|
29 |
|
30 (* Change to ZF/Cardinal.ML *) |
|
31 |
|
32 goalw Cardinal.thy [succ_def] |
|
33 "!!A. succ(n) lepoll A ==> n lepoll A - {a}"; |
|
34 by (rtac cons_lepoll_consD 1); |
|
35 by (rtac mem_not_refl 2); |
|
36 by (fast_tac AC_cs 2); |
|
37 by (fast_tac (AC_cs addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1); |
|
38 val lepoll_diff_sing = result(); |
|
39 (* qed "lepoll_diff_sing"; *) |
|
40 |
|
41 goalw thy [Finite_def] "~Finite(nat)"; |
|
42 by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll] |
|
43 addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); |
|
44 val nat_not_Finite = result(); |
|
45 |
|
46 goalw thy [lepoll_def] "!!A. A~=0 ==> B lepoll A*B"; |
|
47 by (eresolve_tac [not_emptyE] 1); |
|
48 by (res_inst_tac [("x","lam z:B. <x,z>")] exI 1); |
|
49 by (fast_tac (AC_cs addSIs [snd_conv, lam_injective]) 1); |
|
50 val lepoll_Sigma = result(); |
|
51 |
|
52 goal thy "!!A. 0~:A ==> ALL B:{cons(0,x*nat). x:A}. ~Finite(B)"; |
|
53 by (resolve_tac [ballI] 1); |
|
54 by (eresolve_tac [RepFunE] 1); |
|
55 by (hyp_subst_tac 1); |
|
56 by (resolve_tac [notI] 1); |
|
57 by (dresolve_tac [subset_consI RS subset_imp_lepoll RS lepoll_Finite] 1); |
|
58 by (resolve_tac [lepoll_Sigma RS lepoll_Finite RS (nat_not_Finite RS notE)] 1 |
|
59 THEN (atac 2)); |
|
60 by (fast_tac AC_cs 1); |
|
61 val cons_times_nat_not_Finite = result(); |
|
62 |
|
63 goal thy "!!A. [| Union(C)=A; a:A |] ==> EX B:C. a:B & B <= A"; |
|
64 by (fast_tac ZF_cs 1); |
|
65 val lemma1 = result(); |
|
66 |
|
67 goalw thy [pairwise_disjoint_def] |
|
68 "!!A. [| pairwise_disjoint(A); B:A; C:A; a:B; a:C |] ==> B=C"; |
|
69 by (dresolve_tac [IntI] 1 THEN (atac 1)); |
|
70 by (dres_inst_tac [("A","B Int C")] not_emptyI 1); |
|
71 by (fast_tac ZF_cs 1); |
|
72 val lemma2 = result(); |
|
73 |
|
74 goalw thy [sets_of_size_between_def] |
|
75 "!!A. ALL B:{cons(0, x*nat). x:A}. pairwise_disjoint(f`B) & \ |
|
76 \ sets_of_size_between(f`B, 2, n) & Union(f`B)=B \ |
|
77 \ ==> ALL B:A. EX! u. u:f`cons(0, B*nat) & u <= cons(0, B*nat) & \ |
|
78 \ 0:u & 2 lepoll u & u lepoll n"; |
|
79 by (resolve_tac [ballI] 1); |
|
80 by (eresolve_tac [ballE] 1); |
|
81 by (fast_tac ZF_cs 2); |
|
82 by (REPEAT (eresolve_tac [conjE] 1)); |
|
83 by (dresolve_tac [consI1 RSN (2, lemma1)] 1); |
|
84 by (eresolve_tac [bexE] 1); |
|
85 by (resolve_tac [ex1I] 1); |
|
86 by (fast_tac ZF_cs 1); |
|
87 by (REPEAT (eresolve_tac [conjE] 1)); |
|
88 by (resolve_tac [lemma2] 1 THEN (REPEAT (atac 1))); |
|
89 val lemma3 = result(); |
|
90 |
|
91 goalw thy [lepoll_def] "!!A. [| A lepoll i; Ord(i) |] ==> {P(a). a:A} lepoll i"; |
|
92 by (eresolve_tac [exE] 1); |
|
93 by (res_inst_tac |
|
94 [("x", "lam x:RepFun(A, P). LEAST j. EX a:A. x=P(a) & f`a=j")] exI 1); |
|
95 by (res_inst_tac [("d", "%y. P(converse(f)`y)")] lam_injective 1); |
|
96 by (eresolve_tac [RepFunE] 1); |
|
97 by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1)); |
|
98 by (fast_tac (AC_cs addIs [LeastI2] |
|
99 addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); |
|
100 by (eresolve_tac [RepFunE] 1); |
|
101 by (resolve_tac [LeastI2] 1); |
|
102 by (fast_tac AC_cs 1); |
|
103 by (fast_tac (AC_cs addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); |
|
104 by (fast_tac (AC_cs addEs [sym, left_inverse RS ssubst]) 1); |
|
105 val lemma4 = result(); |
|
106 |
|
107 goal thy "!!A. [| n:nat; B:A; u(B) <= cons(0, B*nat); 0:u(B); 2 lepoll u(B); \ |
|
108 \ u(B) lepoll succ(n) |] \ |
|
109 \ ==> (lam x:A. {fst(x). x:u(x)-{0}})`B ~= 0 & \ |
|
110 \ (lam x:A. {fst(x). x:u(x)-{0}})`B <= B & \ |
|
111 \ (lam x:A. {fst(x). x:u(x)-{0}})`B lepoll n"; |
|
112 by (asm_simp_tac AC_ss 1); |
|
113 by (resolve_tac [conjI] 1); |
|
114 by (fast_tac (empty_cs addSDs [RepFun_eq_0_iff RS iffD1] |
|
115 addDs [lepoll_diff_sing] |
|
116 addEs [lepoll_trans RS succ_lepoll_natE, ssubst] |
|
117 addSIs [notI, lepoll_refl, nat_0I]) 1); |
|
118 by (resolve_tac [conjI] 1); |
|
119 by (fast_tac (ZF_cs addSIs [fst_type] addSEs [consE]) 1); |
|
120 by (fast_tac (ZF_cs addSEs [equalityE, |
|
121 Diff_lepoll RS (nat_into_Ord RSN (2, lemma4))]) 1); |
|
122 val lemma5 = result(); |
|
123 |
|
124 goal thy "!!A. [| EX f. ALL B:{cons(0, x*nat). x:A}. \ |
|
125 \ pairwise_disjoint(f`B) & \ |
|
126 \ sets_of_size_between(f`B, 2, succ(n)) & \ |
|
127 \ Union(f`B)=B; n:nat |] \ |
|
128 \ ==> EX f. ALL B:A. f`B ~= 0 & f`B <= B & f`B lepoll n"; |
|
129 by (etac exE 1); |
|
130 by (dtac lemma3 1); |
|
131 by (fast_tac (empty_cs addSDs [bspec, theI] |
|
132 addSEs [conjE] |
|
133 addSIs [exI, ballI, lemma5]) 1); |
|
134 val ex_fun_AC13_AC15 = result(); |
|
135 |
|
136 (* ********************************************************************** *) |
|
137 (* The target proofs *) |
|
138 (* ********************************************************************** *) |
|
139 |
|
140 (* ********************************************************************** *) |
|
141 (* AC10(n) ==> AC11 *) |
|
142 (* ********************************************************************** *) |
|
143 |
|
144 goalw thy AC_defs "!!Z. [| n:nat; 1 le n; AC10(n) |] ==> AC11"; |
|
145 by (resolve_tac [bexI] 1 THEN (assume_tac 2)); |
|
146 by (fast_tac ZF_cs 1); |
|
147 result(); |
|
148 |
|
149 (* ********************************************************************** *) |
|
150 (* AC11 ==> AC12 *) |
|
151 (* ********************************************************************** *) |
|
152 |
|
153 goalw thy AC_defs "!! Z. AC11 ==> AC12"; |
|
154 by (fast_tac (FOL_cs addSEs [bexE] addIs [bexI]) 1); |
|
155 result(); |
|
156 |
|
157 (* ********************************************************************** *) |
|
158 (* AC12 ==> AC15 *) |
|
159 (* ********************************************************************** *) |
|
160 |
|
161 goalw thy AC_defs "!!Z. AC12 ==> AC15"; |
|
162 by (safe_tac ZF_cs); |
|
163 by (eresolve_tac [allE] 1); |
|
164 by (eresolve_tac [impE] 1); |
|
165 by (eresolve_tac [cons_times_nat_not_Finite] 1); |
|
166 by (fast_tac (ZF_cs addSIs [ex_fun_AC13_AC15]) 1); |
|
167 result(); |
|
168 |
|
169 (* ********************************************************************** *) |
|
170 (* AC15 ==> WO6 *) |
|
171 (* ********************************************************************** *) |
|
172 |
|
173 (* in a separate file *) |
|
174 |
|
175 (* ********************************************************************** *) |
|
176 (* The proof needed in the first case, not in the second *) |
|
177 (* ********************************************************************** *) |
|
178 |
|
179 (* ********************************************************************** *) |
|
180 (* AC10(n) ==> AC13(n-1) if 2 le n *) |
|
181 (* *) |
|
182 (* Because of the change to the formal definition of AC10(n) we prove *) |
|
183 (* the following obviously equivalent theorem : *) |
|
184 (* AC10(n) implies AC13(n) for (1 le n) *) |
|
185 (* ********************************************************************** *) |
|
186 |
|
187 goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC10(n) |] ==> AC13(n)"; |
|
188 by (safe_tac ZF_cs); |
|
189 by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE), |
|
190 ex_fun_AC13_AC15]) 1); |
|
191 val AC10_imp_AC13 = result(); |
|
192 |
|
193 (* ********************************************************************** *) |
|
194 (* The proofs needed in the second case, not in the first *) |
|
195 (* ********************************************************************** *) |
|
196 |
|
197 (* ********************************************************************** *) |
|
198 (* AC1 ==> AC13(1) *) |
|
199 (* ********************************************************************** *) |
|
200 |
|
201 goalw thy AC_defs "!!Z. AC1 ==> AC13(1)"; |
|
202 by (resolve_tac [allI] 1); |
|
203 by (eresolve_tac [allE] 1); |
|
204 by (resolve_tac [impI] 1); |
|
205 by (mp_tac 1); |
|
206 by (eresolve_tac [exE] 1); |
|
207 by (res_inst_tac [("x","lam x:A. {f`x}")] exI 1); |
|
208 by (asm_full_simp_tac (AC_ss addsimps |
|
209 [singleton_eqpoll_1 RS eqpoll_imp_lepoll, |
|
210 singletonI RS not_emptyI]) 1); |
|
211 by (fast_tac (AC_cs addSEs [singletonE, apply_type]) 1); |
|
212 result(); |
|
213 |
|
214 (* ********************************************************************** *) |
|
215 (* AC13(m) ==> AC13(n) for m <= n *) |
|
216 (* ********************************************************************** *) |
|
217 |
|
218 goalw thy AC_defs "!!m n. [| m:nat; n:nat; m le n; AC13(m) |] ==> AC13(n)"; |
|
219 by (dresolve_tac [nat_le_imp_lepoll] 1 THEN REPEAT (atac 1)); |
|
220 by (fast_tac (ZF_cs addSEs [lepoll_trans]) 1); |
|
221 result(); |
|
222 |
|
223 (* ********************************************************************** *) |
|
224 (* The proofs necessary for both cases *) |
|
225 (* ********************************************************************** *) |
|
226 |
|
227 (* ********************************************************************** *) |
|
228 (* AC13(n) ==> AC14 if 1 <= n *) |
|
229 (* ********************************************************************** *) |
|
230 |
|
231 goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC13(n) |] ==> AC14"; |
|
232 by (fast_tac (FOL_cs addIs [bexI]) 1); |
|
233 result(); |
|
234 |
|
235 (* ********************************************************************** *) |
|
236 (* AC14 ==> AC15 *) |
|
237 (* ********************************************************************** *) |
|
238 |
|
239 goalw thy AC_defs "!!Z. AC14 ==> AC15"; |
|
240 by (fast_tac ZF_cs 1); |
|
241 result(); |
|
242 |
|
243 (* ********************************************************************** *) |
|
244 (* The redundant proofs; however cited by Rubin & Rubin *) |
|
245 (* ********************************************************************** *) |
|
246 |
|
247 (* ********************************************************************** *) |
|
248 (* AC13(1) ==> AC1 *) |
|
249 (* ********************************************************************** *) |
|
250 |
|
251 goal thy "!!A. [| A~=0; A lepoll 1 |] ==> EX a. A={a}"; |
|
252 by (fast_tac (AC_cs addSEs [not_emptyE, lepoll_1_is_sing]) 1); |
|
253 val lemma_aux = result(); |
|
254 |
|
255 goal thy "!!f. ALL B:A. f(B)~=0 & f(B)<=B & f(B) lepoll 1 \ |
|
256 \ ==> (lam x:A. THE y. f(x)={y}) : (PROD X:A. X)"; |
|
257 by (resolve_tac [lam_type] 1); |
|
258 by (dresolve_tac [bspec] 1 THEN (atac 1)); |
|
259 by (REPEAT (eresolve_tac [conjE] 1)); |
|
260 by (eresolve_tac [lemma_aux RS exE] 1 THEN (atac 1)); |
|
261 by (asm_full_simp_tac (AC_ss addsimps [the_element]) 1); |
|
262 by (fast_tac (AC_cs addEs [ssubst]) 1); |
|
263 val lemma = result(); |
|
264 |
|
265 goalw thy AC_defs "!!Z. AC13(1) ==> AC1"; |
|
266 by (fast_tac (AC_cs addSEs [lemma]) 1); |
|
267 result(); |
|
268 |
|
269 (* ********************************************************************** *) |
|
270 (* AC11 ==> AC14 *) |
|
271 (* ********************************************************************** *) |
|
272 |
|
273 goalw thy [AC11_def, AC14_def] "!!Z. AC11 ==> AC14"; |
|
274 by (fast_tac (ZF_cs addSIs [AC10_imp_AC13]) 1); |
|
275 result(); |