28 (* ********************************************************************** *) |
28 (* ********************************************************************** *) |
29 |
29 |
30 goalw thy [lepoll_def] "!!A. A~=0 ==> B lepoll A*B"; |
30 goalw thy [lepoll_def] "!!A. A~=0 ==> B lepoll A*B"; |
31 by (etac not_emptyE 1); |
31 by (etac not_emptyE 1); |
32 by (res_inst_tac [("x","lam z:B. <x,z>")] exI 1); |
32 by (res_inst_tac [("x","lam z:B. <x,z>")] exI 1); |
33 by (fast_tac (AC_cs addSIs [snd_conv, lam_injective]) 1); |
33 by (fast_tac (!claset addSIs [snd_conv, lam_injective]) 1); |
34 val lepoll_Sigma = result(); |
34 val lepoll_Sigma = result(); |
35 |
35 |
36 goal thy "!!A. 0~:A ==> ALL B:{cons(0,x*nat). x:A}. ~Finite(B)"; |
36 goal thy "!!A. 0~:A ==> ALL B:{cons(0,x*nat). x:A}. ~Finite(B)"; |
37 by (rtac ballI 1); |
37 by (rtac ballI 1); |
38 by (etac RepFunE 1); |
38 by (etac RepFunE 1); |
39 by (hyp_subst_tac 1); |
39 by (hyp_subst_tac 1); |
40 by (rtac notI 1); |
40 by (rtac notI 1); |
41 by (dresolve_tac [subset_consI RS subset_imp_lepoll RS lepoll_Finite] 1); |
41 by (dresolve_tac [subset_consI RS subset_imp_lepoll RS lepoll_Finite] 1); |
42 by (resolve_tac [lepoll_Sigma RS lepoll_Finite RS (nat_not_Finite RS notE)] 1 |
42 by (resolve_tac [lepoll_Sigma RS lepoll_Finite RS (nat_not_Finite RS notE)] 1 |
43 THEN (assume_tac 2)); |
43 THEN (assume_tac 2)); |
44 by (fast_tac AC_cs 1); |
44 by (Fast_tac 1); |
45 val cons_times_nat_not_Finite = result(); |
45 val cons_times_nat_not_Finite = result(); |
46 |
46 |
47 goal thy "!!A. [| Union(C)=A; a:A |] ==> EX B:C. a:B & B <= A"; |
47 goal thy "!!A. [| Union(C)=A; a:A |] ==> EX B:C. a:B & B <= A"; |
48 by (fast_tac ZF_cs 1); |
48 by (Fast_tac 1); |
49 val lemma1 = result(); |
49 val lemma1 = result(); |
50 |
50 |
51 goalw thy [pairwise_disjoint_def] |
51 goalw thy [pairwise_disjoint_def] |
52 "!!A. [| pairwise_disjoint(A); B:A; C:A; a:B; a:C |] ==> B=C"; |
52 "!!A. [| pairwise_disjoint(A); B:A; C:A; a:B; a:C |] ==> B=C"; |
53 by (dtac IntI 1 THEN (assume_tac 1)); |
53 by (dtac IntI 1 THEN (assume_tac 1)); |
54 by (dres_inst_tac [("A","B Int C")] not_emptyI 1); |
54 by (dres_inst_tac [("A","B Int C")] not_emptyI 1); |
55 by (fast_tac ZF_cs 1); |
55 by (Fast_tac 1); |
56 val lemma2 = result(); |
56 val lemma2 = result(); |
57 |
57 |
58 goalw thy [sets_of_size_between_def] |
58 goalw thy [sets_of_size_between_def] |
59 "!!A. ALL B:{cons(0, x*nat). x:A}. pairwise_disjoint(f`B) & \ |
59 "!!A. ALL B:{cons(0, x*nat). x:A}. pairwise_disjoint(f`B) & \ |
60 \ sets_of_size_between(f`B, 2, n) & Union(f`B)=B \ |
60 \ sets_of_size_between(f`B, 2, n) & Union(f`B)=B \ |
61 \ ==> ALL B:A. EX! u. u:f`cons(0, B*nat) & u <= cons(0, B*nat) & \ |
61 \ ==> ALL B:A. EX! u. u:f`cons(0, B*nat) & u <= cons(0, B*nat) & \ |
62 \ 0:u & 2 lepoll u & u lepoll n"; |
62 \ 0:u & 2 lepoll u & u lepoll n"; |
63 by (rtac ballI 1); |
63 by (rtac ballI 1); |
64 by (etac ballE 1); |
64 by (etac ballE 1); |
65 by (fast_tac ZF_cs 2); |
65 by (Fast_tac 2); |
66 by (REPEAT (etac conjE 1)); |
66 by (REPEAT (etac conjE 1)); |
67 by (dresolve_tac [consI1 RSN (2, lemma1)] 1); |
67 by (dresolve_tac [consI1 RSN (2, lemma1)] 1); |
68 by (etac bexE 1); |
68 by (etac bexE 1); |
69 by (rtac ex1I 1); |
69 by (rtac ex1I 1); |
70 by (fast_tac ZF_cs 1); |
70 by (Fast_tac 1); |
71 by (REPEAT (etac conjE 1)); |
71 by (REPEAT (etac conjE 1)); |
72 by (rtac lemma2 1 THEN (REPEAT (assume_tac 1))); |
72 by (rtac lemma2 1 THEN (REPEAT (assume_tac 1))); |
73 val lemma3 = result(); |
73 val lemma3 = result(); |
74 |
74 |
75 goalw thy [lepoll_def] "!!A. [| A lepoll i; Ord(i) |] ==> {P(a). a:A} lepoll i"; |
75 goalw thy [lepoll_def] "!!A. [| A lepoll i; Ord(i) |] ==> {P(a). a:A} lepoll i"; |
77 by (res_inst_tac |
77 by (res_inst_tac |
78 [("x", "lam x:RepFun(A, P). LEAST j. EX a:A. x=P(a) & f`a=j")] exI 1); |
78 [("x", "lam x:RepFun(A, P). LEAST j. EX a:A. x=P(a) & f`a=j")] exI 1); |
79 by (res_inst_tac [("d", "%y. P(converse(f)`y)")] lam_injective 1); |
79 by (res_inst_tac [("d", "%y. P(converse(f)`y)")] lam_injective 1); |
80 by (etac RepFunE 1); |
80 by (etac RepFunE 1); |
81 by (forward_tac [inj_is_fun RS apply_type] 1 THEN (assume_tac 1)); |
81 by (forward_tac [inj_is_fun RS apply_type] 1 THEN (assume_tac 1)); |
82 by (fast_tac (AC_cs addIs [LeastI2] |
82 by (fast_tac (!claset addIs [LeastI2] |
83 addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); |
83 addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); |
84 by (etac RepFunE 1); |
84 by (etac RepFunE 1); |
85 by (rtac LeastI2 1); |
85 by (rtac LeastI2 1); |
86 by (fast_tac AC_cs 1); |
86 by (Fast_tac 1); |
87 by (fast_tac (AC_cs addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); |
87 by (fast_tac (!claset addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); |
88 by (fast_tac (AC_cs addEs [sym, left_inverse RS ssubst]) 1); |
88 by (fast_tac (!claset addEs [sym, left_inverse RS ssubst]) 1); |
89 val lemma4 = result(); |
89 val lemma4 = result(); |
90 |
90 |
91 goal thy "!!A. [| n:nat; B:A; u(B) <= cons(0, B*nat); 0:u(B); 2 lepoll u(B); \ |
91 goal thy "!!A. [| n:nat; B:A; u(B) <= cons(0, B*nat); 0:u(B); 2 lepoll u(B); \ |
92 \ u(B) lepoll succ(n) |] \ |
92 \ u(B) lepoll succ(n) |] \ |
93 \ ==> (lam x:A. {fst(x). x:u(x)-{0}})`B ~= 0 & \ |
93 \ ==> (lam x:A. {fst(x). x:u(x)-{0}})`B ~= 0 & \ |
94 \ (lam x:A. {fst(x). x:u(x)-{0}})`B <= B & \ |
94 \ (lam x:A. {fst(x). x:u(x)-{0}})`B <= B & \ |
95 \ (lam x:A. {fst(x). x:u(x)-{0}})`B lepoll n"; |
95 \ (lam x:A. {fst(x). x:u(x)-{0}})`B lepoll n"; |
96 by (asm_simp_tac AC_ss 1); |
96 by (Asm_simp_tac 1); |
97 by (rtac conjI 1); |
97 by (rtac conjI 1); |
98 by (fast_tac (empty_cs addSDs [RepFun_eq_0_iff RS iffD1] |
98 by (fast_tac (empty_cs addSDs [RepFun_eq_0_iff RS iffD1] |
99 addDs [lepoll_Diff_sing] |
99 addDs [lepoll_Diff_sing] |
100 addEs [lepoll_trans RS succ_lepoll_natE, ssubst] |
100 addEs [lepoll_trans RS succ_lepoll_natE, ssubst] |
101 addSIs [notI, lepoll_refl, nat_0I]) 1); |
101 addSIs [notI, lepoll_refl, nat_0I]) 1); |
102 by (rtac conjI 1); |
102 by (rtac conjI 1); |
103 by (fast_tac (ZF_cs addSIs [fst_type] addSEs [consE]) 1); |
103 by (fast_tac (!claset addSIs [fst_type] addSEs [consE]) 1); |
104 by (fast_tac (ZF_cs addSEs [equalityE, |
104 by (fast_tac (!claset addSEs [equalityE, |
105 Diff_lepoll RS (nat_into_Ord RSN (2, lemma4))]) 1); |
105 Diff_lepoll RS (nat_into_Ord RSN (2, lemma4))]) 1); |
106 val lemma5 = result(); |
106 val lemma5 = result(); |
107 |
107 |
108 goal thy "!!A. [| EX f. ALL B:{cons(0, x*nat). x:A}. \ |
108 goal thy "!!A. [| EX f. ALL B:{cons(0, x*nat). x:A}. \ |
109 \ pairwise_disjoint(f`B) & \ |
109 \ pairwise_disjoint(f`B) & \ |
139 (* ********************************************************************** *) |
139 (* ********************************************************************** *) |
140 (* AC12 ==> AC15 *) |
140 (* AC12 ==> AC15 *) |
141 (* ********************************************************************** *) |
141 (* ********************************************************************** *) |
142 |
142 |
143 goalw thy AC_defs "!!Z. AC12 ==> AC15"; |
143 goalw thy AC_defs "!!Z. AC12 ==> AC15"; |
144 by (safe_tac ZF_cs); |
144 by (safe_tac (!claset)); |
145 by (etac allE 1); |
145 by (etac allE 1); |
146 by (etac impE 1); |
146 by (etac impE 1); |
147 by (etac cons_times_nat_not_Finite 1); |
147 by (etac cons_times_nat_not_Finite 1); |
148 by (fast_tac (ZF_cs addSIs [ex_fun_AC13_AC15]) 1); |
148 by (fast_tac (!claset addSIs [ex_fun_AC13_AC15]) 1); |
149 qed "AC12_AC15"; |
149 qed "AC12_AC15"; |
150 |
150 |
151 (* ********************************************************************** *) |
151 (* ********************************************************************** *) |
152 (* AC15 ==> WO6 *) |
152 (* AC15 ==> WO6 *) |
153 (* ********************************************************************** *) |
153 (* ********************************************************************** *) |
165 (* the following obviously equivalent theorem : *) |
165 (* the following obviously equivalent theorem : *) |
166 (* AC10(n) implies AC13(n) for (1 le n) *) |
166 (* AC10(n) implies AC13(n) for (1 le n) *) |
167 (* ********************************************************************** *) |
167 (* ********************************************************************** *) |
168 |
168 |
169 goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC10(n) |] ==> AC13(n)"; |
169 goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC10(n) |] ==> AC13(n)"; |
170 by (safe_tac ZF_cs); |
170 by (safe_tac (!claset)); |
171 by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE), |
171 by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE), |
172 ex_fun_AC13_AC15]) 1); |
172 ex_fun_AC13_AC15]) 1); |
173 qed "AC10_AC13"; |
173 qed "AC10_AC13"; |
174 |
174 |
175 (* ********************************************************************** *) |
175 (* ********************************************************************** *) |
185 by (etac allE 1); |
185 by (etac allE 1); |
186 by (rtac impI 1); |
186 by (rtac impI 1); |
187 by (mp_tac 1); |
187 by (mp_tac 1); |
188 by (etac exE 1); |
188 by (etac exE 1); |
189 by (res_inst_tac [("x","lam x:A. {f`x}")] exI 1); |
189 by (res_inst_tac [("x","lam x:A. {f`x}")] exI 1); |
190 by (asm_full_simp_tac (AC_ss addsimps |
190 by (asm_full_simp_tac (!simpset addsimps |
191 [singleton_eqpoll_1 RS eqpoll_imp_lepoll, |
191 [singleton_eqpoll_1 RS eqpoll_imp_lepoll, |
192 singletonI RS not_emptyI]) 1); |
192 singletonI RS not_emptyI]) 1); |
193 by (fast_tac (AC_cs addSEs [apply_type]) 1); |
193 by (fast_tac (!claset addSEs [apply_type]) 1); |
194 qed "AC1_AC13"; |
194 qed "AC1_AC13"; |
195 |
195 |
196 (* ********************************************************************** *) |
196 (* ********************************************************************** *) |
197 (* AC13(m) ==> AC13(n) for m <= n *) |
197 (* AC13(m) ==> AC13(n) for m <= n *) |
198 (* ********************************************************************** *) |
198 (* ********************************************************************** *) |
199 |
199 |
200 goalw thy AC_defs "!!m n. [| m:nat; n:nat; m le n; AC13(m) |] ==> AC13(n)"; |
200 goalw thy AC_defs "!!m n. [| m:nat; n:nat; m le n; AC13(m) |] ==> AC13(n)"; |
201 by (dtac nat_le_imp_lepoll 1 THEN REPEAT (assume_tac 1)); |
201 by (dtac nat_le_imp_lepoll 1 THEN REPEAT (assume_tac 1)); |
202 by (fast_tac (ZF_cs addSEs [lepoll_trans]) 1); |
202 by (fast_tac (!claset addSEs [lepoll_trans]) 1); |
203 qed "AC13_mono"; |
203 qed "AC13_mono"; |
204 |
204 |
205 (* ********************************************************************** *) |
205 (* ********************************************************************** *) |
206 (* The proofs necessary for both cases *) |
206 (* The proofs necessary for both cases *) |
207 (* ********************************************************************** *) |
207 (* ********************************************************************** *) |
229 (* ********************************************************************** *) |
229 (* ********************************************************************** *) |
230 (* AC13(1) ==> AC1 *) |
230 (* AC13(1) ==> AC1 *) |
231 (* ********************************************************************** *) |
231 (* ********************************************************************** *) |
232 |
232 |
233 goal thy "!!A. [| A~=0; A lepoll 1 |] ==> EX a. A={a}"; |
233 goal thy "!!A. [| A~=0; A lepoll 1 |] ==> EX a. A={a}"; |
234 by (fast_tac (AC_cs addSEs [not_emptyE, lepoll_1_is_sing]) 1); |
234 by (fast_tac (!claset addSEs [not_emptyE, lepoll_1_is_sing]) 1); |
235 val lemma_aux = result(); |
235 val lemma_aux = result(); |
236 |
236 |
237 goal thy "!!f. ALL B:A. f(B)~=0 & f(B)<=B & f(B) lepoll 1 \ |
237 goal thy "!!f. ALL B:A. f(B)~=0 & f(B)<=B & f(B) lepoll 1 \ |
238 \ ==> (lam x:A. THE y. f(x)={y}) : (PROD X:A. X)"; |
238 \ ==> (lam x:A. THE y. f(x)={y}) : (PROD X:A. X)"; |
239 by (rtac lam_type 1); |
239 by (rtac lam_type 1); |
240 by (dtac bspec 1 THEN (assume_tac 1)); |
240 by (dtac bspec 1 THEN (assume_tac 1)); |
241 by (REPEAT (etac conjE 1)); |
241 by (REPEAT (etac conjE 1)); |
242 by (eresolve_tac [lemma_aux RS exE] 1 THEN (assume_tac 1)); |
242 by (eresolve_tac [lemma_aux RS exE] 1 THEN (assume_tac 1)); |
243 by (asm_full_simp_tac (AC_ss addsimps [the_element]) 1); |
243 by (asm_full_simp_tac (!simpset addsimps [the_element]) 1); |
244 by (fast_tac (AC_cs addEs [ssubst]) 1); |
244 by (fast_tac (!claset addEs [ssubst]) 1); |
245 val lemma = result(); |
245 val lemma = result(); |
246 |
246 |
247 goalw thy AC_defs "!!Z. AC13(1) ==> AC1"; |
247 goalw thy AC_defs "!!Z. AC13(1) ==> AC1"; |
248 by (fast_tac (AC_cs addSEs [lemma]) 1); |
248 by (fast_tac (!claset addSEs [lemma]) 1); |
249 qed "AC13_AC1"; |
249 qed "AC13_AC1"; |
250 |
250 |
251 (* ********************************************************************** *) |
251 (* ********************************************************************** *) |
252 (* AC11 ==> AC14 *) |
252 (* AC11 ==> AC14 *) |
253 (* ********************************************************************** *) |
253 (* ********************************************************************** *) |
254 |
254 |
255 goalw thy [AC11_def, AC14_def] "!!Z. AC11 ==> AC14"; |
255 goalw thy [AC11_def, AC14_def] "!!Z. AC11 ==> AC14"; |
256 by (fast_tac (ZF_cs addSIs [AC10_AC13]) 1); |
256 by (fast_tac (!claset addSIs [AC10_AC13]) 1); |
257 qed "AC11_AC14"; |
257 qed "AC11_AC14"; |