1 (* Title: ZF/AC/DC.ML |
1 (* Title: ZF/AC/DC.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Krzysztof Grabczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 The proofs concerning the Axiom of Dependent Choice |
5 The proofs concerning the Axiom of Dependent Choice |
6 *) |
6 *) |
7 |
7 |
8 open DC; |
8 open DC; |
9 |
9 |
10 (* ********************************************************************** *) |
10 (* ********************************************************************** *) |
11 (* DC ==> DC(omega) *) |
11 (* DC ==> DC(omega) *) |
12 (* *) |
12 (* *) |
13 (* The scheme of the proof: *) |
13 (* The scheme of the proof: *) |
14 (* *) |
14 (* *) |
15 (* Assume DC. Let R and x satisfy the premise of DC(omega). *) |
15 (* Assume DC. Let R and x satisfy the premise of DC(omega). *) |
16 (* *) |
16 (* *) |
17 (* Define XX and RR as follows: *) |
17 (* Define XX and RR as follows: *) |
18 (* *) |
18 (* *) |
19 (* XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) *) |
19 (* XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) *) |
20 (* f RR g iff domain(g)=succ(domain(f)) & *) |
20 (* f RR g iff domain(g)=succ(domain(f)) & *) |
21 (* restrict(g, domain(f)) = f *) |
21 (* restrict(g, domain(f)) = f *) |
22 (* *) |
22 (* *) |
23 (* Then RR satisfies the hypotheses of DC. *) |
23 (* Then RR satisfies the hypotheses of DC. *) |
24 (* So applying DC: *) |
24 (* So applying DC: *) |
25 (* *) |
25 (* *) |
26 (* EX f:nat->XX. ALL n:nat. f`n RR f`succ(n) *) |
26 (* EX f:nat->XX. ALL n:nat. f`n RR f`succ(n) *) |
27 (* *) |
27 (* *) |
28 (* Thence *) |
28 (* Thence *) |
29 (* *) |
29 (* *) |
30 (* ff = {<n, f`succ(n)`n>. n:nat} *) |
30 (* ff = {<n, f`succ(n)`n>. n:nat} *) |
31 (* *) |
31 (* *) |
32 (* is the desired function. *) |
32 (* is the desired function. *) |
33 (* *) |
33 (* *) |
34 (* ********************************************************************** *) |
34 (* ********************************************************************** *) |
35 |
35 |
36 goal thy "{z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
36 goal thy "{z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
37 \ & restrict(snd(z), domain(fst(z))) = fst(z)} <= XX*XX"; |
37 \ & restrict(snd(z), domain(fst(z))) = fst(z)} <= XX*XX"; |
38 by (fast_tac AC_cs 1); |
38 by (fast_tac AC_cs 1); |
39 val lemma1_1 = result(); |
39 val lemma1_1 = result(); |
40 |
40 |
41 goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
41 goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
42 \ ==> {z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
42 \ ==> {z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
43 \ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
43 \ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
44 \ domain(snd(z))=succ(domain(fst(z))) \ |
44 \ domain(snd(z))=succ(domain(fst(z))) \ |
45 \ & restrict(snd(z), domain(fst(z))) = fst(z)} ~= 0"; |
45 \ & restrict(snd(z), domain(fst(z))) = fst(z)} ~= 0"; |
46 by (etac ballE 1); |
46 by (etac ballE 1); |
47 by (eresolve_tac [empty_subsetI RS PowI RSN (2, notE)] 2); |
47 by (eresolve_tac [empty_subsetI RS PowI RSN (2, notE)] 2); |
48 by (eresolve_tac [nat_0I RS n_lesspoll_nat RSN (2, impE)] 1); |
48 by (eresolve_tac [nat_0I RS n_lesspoll_nat RSN (2, impE)] 1); |
49 by (etac bexE 1); |
49 by (etac bexE 1); |
50 by (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1); |
50 by (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1); |
51 by (rtac CollectI 1); |
51 by (rtac CollectI 1); |
52 by (rtac SigmaI 1); |
52 by (rtac SigmaI 1); |
53 by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, empty_fun]) 1); |
53 by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, empty_fun]) 1); |
54 by (fast_tac (AC_cs addSIs [nat_1I RS UN_I, singleton_fun RS Pi_type] |
54 by (fast_tac (AC_cs addSIs [nat_1I RS UN_I, singleton_fun RS Pi_type] |
55 addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, |
55 addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, |
56 apply_singleton_eq, image_0])) 1); |
56 apply_singleton_eq, image_0])) 1); |
57 by (asm_full_simp_tac (AC_ss addsimps [domain_0, restrict_0, domain_sing, |
57 by (asm_full_simp_tac (AC_ss addsimps [domain_0, restrict_0, domain_sing, |
58 [lepoll_refl, succI1] MRS lepoll_1_is_sing]) 1); |
58 [lepoll_refl, succI1] MRS lepoll_1_is_sing]) 1); |
59 val lemma1_2 = result(); |
59 val lemma1_2 = result(); |
60 |
60 |
61 goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
61 goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
62 \ ==> range({z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
62 \ ==> range({z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
63 \ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
63 \ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
64 \ domain(snd(z))=succ(domain(fst(z))) \ |
64 \ domain(snd(z))=succ(domain(fst(z))) \ |
65 \ & restrict(snd(z), domain(fst(z))) = fst(z)}) \ |
65 \ & restrict(snd(z), domain(fst(z))) = fst(z)}) \ |
66 \ <= domain({z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
66 \ <= domain({z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \ |
67 \ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
67 \ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \ |
68 \ domain(snd(z))=succ(domain(fst(z))) \ |
68 \ domain(snd(z))=succ(domain(fst(z))) \ |
69 \ & restrict(snd(z), domain(fst(z))) = fst(z)})"; |
69 \ & restrict(snd(z), domain(fst(z))) = fst(z)})"; |
70 by (rtac range_subset_domain 1); |
70 by (rtac range_subset_domain 1); |
71 by (rtac subsetI 2); |
71 by (rtac subsetI 2); |
72 by (etac CollectD1 2); |
72 by (etac CollectD1 2); |
73 by (etac UN_E 1); |
73 by (etac UN_E 1); |
74 by (etac CollectE 1); |
74 by (etac CollectE 1); |
75 by (dresolve_tac [fun_is_rel RS image_subset RS PowI RSN (2, bspec)] 1 |
75 by (dresolve_tac [fun_is_rel RS image_subset RS PowI RSN (2, bspec)] 1 |
76 THEN (assume_tac 1)); |
76 THEN (assume_tac 1)); |
77 by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)] |
77 by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)] |
78 MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1 |
78 MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1 |
79 THEN REPEAT (assume_tac 1)); |
79 THEN REPEAT (assume_tac 1)); |
80 by (etac bexE 1); |
80 by (etac bexE 1); |
81 by (res_inst_tac [("x","cons(<n,x>, g)")] exI 1); |
81 by (res_inst_tac [("x","cons(<n,x>, g)")] exI 1); |
82 by (rtac CollectI 1); |
82 by (rtac CollectI 1); |
83 by (rtac SigmaI 1); |
83 by (rtac SigmaI 1); |
84 by (fast_tac AC_cs 1); |
84 by (fast_tac AC_cs 1); |
85 by (rtac UN_I 1); |
85 by (rtac UN_I 1); |
86 by (etac nat_succI 1); |
86 by (etac nat_succI 1); |
87 by (rtac CollectI 1); |
87 by (rtac CollectI 1); |
88 by (etac cons_fun_type2 1 THEN (assume_tac 1)); |
88 by (etac cons_fun_type2 1 THEN (assume_tac 1)); |
89 by (fast_tac (AC_cs addSEs [succE] addss (AC_ss |
89 by (fast_tac (AC_cs addSEs [succE] addss (AC_ss |
90 addsimps [cons_image_n, cons_val_n, cons_image_k, cons_val_k])) 1); |
90 addsimps [cons_image_n, cons_val_n, cons_image_k, cons_val_k])) 1); |
91 by (asm_full_simp_tac (AC_ss |
91 by (asm_full_simp_tac (AC_ss |
92 addsimps [domain_cons, domain_of_fun, succ_def, restrict_cons_eq]) 1); |
92 addsimps [domain_cons, domain_of_fun, succ_def, restrict_cons_eq]) 1); |
93 val lemma1_3 = result(); |
93 val lemma1_3 = result(); |
94 |
94 |
95 goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
95 goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \ |
96 \ RR = {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
96 \ RR = {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ |
97 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
97 \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ |
98 \ ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
98 \ ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \ |
99 \ |] ==> RR <= XX*XX & RR ~= 0 & range(RR) <= domain(RR)"; |
99 \ |] ==> RR <= XX*XX & RR ~= 0 & range(RR) <= domain(RR)"; |
100 by (fast_tac (AC_cs addSIs [lemma1_1] addSEs [lemma1_2, lemma1_3]) 1); |
100 by (fast_tac (AC_cs addSIs [lemma1_1] addSEs [lemma1_2, lemma1_3]) 1); |
101 val lemma1 = result(); |
101 val lemma1 = result(); |
102 |
102 |
103 goal thy "!!f. [| <f,g> : {z:XX*XX. \ |
103 goal thy "!!f. [| <f,g> : {z:XX*XX. \ |
104 \ domain(snd(z))=succ(domain(fst(z))) & Q(z)}; \ |
104 \ domain(snd(z))=succ(domain(fst(z))) & Q(z)}; \ |
105 \ XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); f:k->X \ |
105 \ XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); f:k->X \ |
106 \ |] ==> g:succ(k)->X"; |
106 \ |] ==> g:succ(k)->X"; |
107 by (etac CollectE 1); |
107 by (etac CollectE 1); |
108 by (dtac SigmaD2 1); |
108 by (dtac SigmaD2 1); |
109 by (hyp_subst_tac 1); |
109 by (hyp_subst_tac 1); |
110 by (etac UN_E 1); |
110 by (etac UN_E 1); |
111 by (etac CollectE 1); |
111 by (etac CollectE 1); |
283 by (assume_tac 2); |
283 by (assume_tac 2); |
284 by (fast_tac AC_cs 1); |
284 by (fast_tac AC_cs 1); |
285 val Finite_Fin = result(); |
285 val Finite_Fin = result(); |
286 |
286 |
287 goal thy "!!x. x: X ==> {<0,x>}: (UN n:nat. \ |
287 goal thy "!!x. x: X ==> {<0,x>}: (UN n:nat. \ |
288 \ {f:succ(n)->X. ALL k:n. <f`k, f`succ(k)> : R})"; |
288 \ {f:succ(n)->X. ALL k:n. <f`k, f`succ(k)> : R})"; |
289 by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, singleton_fun RS Pi_type] |
289 by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, singleton_fun RS Pi_type] |
290 addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, |
290 addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, |
291 apply_singleton_eq])) 1); |
291 apply_singleton_eq])) 1); |
292 val singleton_in_funs = result(); |
292 val singleton_in_funs = result(); |
293 |
293 |
294 goal thy |
294 goal thy |
295 "!!X. [| XX = (UN n:nat. \ |
295 "!!X. [| XX = (UN n:nat. \ |
296 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
296 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
297 \ RR = {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
297 \ RR = {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
298 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \ |
298 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \ |
299 \ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \ |
299 \ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \ |
300 \ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \ |
300 \ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \ |
301 \ range(R) <= domain(R); x:domain(R) \ |
301 \ range(R) <= domain(R); x:domain(R) \ |
302 \ |] ==> RR <= Pow(XX)*XX & \ |
302 \ |] ==> RR <= Pow(XX)*XX & \ |
303 \ (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))"; |
303 \ (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))"; |
304 by (rtac conjI 1); |
304 by (rtac conjI 1); |
305 by (fast_tac (FOL_cs addSEs [FinD RS PowI, SigmaE, CollectE] |
305 by (fast_tac (FOL_cs addSEs [FinD RS PowI, SigmaE, CollectE] |
306 addSIs [subsetI, SigmaI]) 1); |
306 addSIs [subsetI, SigmaI]) 1); |
307 by (rtac ballI 1); |
307 by (rtac ballI 1); |
308 by (rtac impI 1); |
308 by (rtac impI 1); |
309 by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1 |
309 by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1 |
310 THEN (assume_tac 1)); |
310 THEN (assume_tac 1)); |
311 by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f)) \ |
311 by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f)) \ |
312 \ & (ALL f:Y. restrict(g, domain(f)) = f)" 1); |
312 \ & (ALL f:Y. restrict(g, domain(f)) = f)" 1); |
313 by (fast_tac (AC_cs addss AC_ss) 2); |
313 by (fast_tac (AC_cs addss AC_ss) 2); |
314 by (fast_tac (FOL_cs addSEs [CollectE, singleton_in_funs] |
314 by (fast_tac (FOL_cs addSEs [CollectE, singleton_in_funs] |
315 addSIs [SigmaI] addIs [bexI] addss AC_ss) 1); |
315 addSIs [SigmaI] addIs [bexI] addss AC_ss) 1); |
316 val lemma1 = result(); |
316 val lemma1 = result(); |
317 |
317 |
318 goal thy "!!f. [| f:nat->X; n:nat |] ==> \ |
318 goal thy "!!f. [| f:nat->X; n:nat |] ==> \ |
319 \ (UN x:f``succ(n). P(x)) = P(f`n) Un (UN x:f``n. P(x))"; |
319 \ (UN x:f``succ(n). P(x)) = P(f`n) Un (UN x:f``n. P(x))"; |
320 by (asm_full_simp_tac (AC_ss |
320 by (asm_full_simp_tac (AC_ss |
321 addsimps [Ord_nat RSN (2, OrdmemD) RSN (2, image_fun), |
321 addsimps [Ord_nat RSN (2, OrdmemD) RSN (2, image_fun), |
322 [nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
322 [nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
323 val UN_image_succ_eq = result(); |
323 val UN_image_succ_eq = result(); |
324 |
324 |
325 goal thy "!!f. [| (UN x:f``n. P(x)) = y; P(f`n) = succ(y); \ |
325 goal thy "!!f. [| (UN x:f``n. P(x)) = y; P(f`n) = succ(y); \ |
326 \ f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)"; |
326 \ f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)"; |
327 by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq]) 1); |
327 by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq]) 1); |
328 by (fast_tac (AC_cs addSIs [equalityI]) 1); |
328 by (fast_tac (AC_cs addSIs [equalityI]) 1); |
329 val UN_image_succ_eq_succ = result(); |
329 val UN_image_succ_eq_succ = result(); |
330 |
330 |
331 goal thy "!!f. [| f: (UN n:nat. {g:succ(n) -> D. P(g, n)}); \ |
331 goal thy "!!f. [| f: (UN n:nat. {g:succ(n) -> D. P(g, n)}); \ |
332 \ domain(f)=succ(x); x=y |] ==> f`y : D"; |
332 \ domain(f)=succ(x); x=y |] ==> f`y : D"; |
333 by (fast_tac (AC_cs addEs [apply_type] |
333 by (fast_tac (AC_cs addEs [apply_type] |
334 addSDs [[sym, domain_of_fun] MRS trans]) 1); |
334 addSDs [[sym, domain_of_fun] MRS trans]) 1); |
335 val apply_UN_type = result(); |
335 val apply_UN_type = result(); |
336 |
336 |
337 goal thy "!!f. [| f : nat -> X; n:nat |] ==> f``succ(n) = cons(f`n, f``n)"; |
337 goal thy "!!f. [| f : nat -> X; n:nat |] ==> f``succ(n) = cons(f`n, f``n)"; |
338 by (asm_full_simp_tac (AC_ss |
338 by (asm_full_simp_tac (AC_ss |
339 addsimps [nat_succI, Ord_nat RSN (2, OrdmemD), image_fun]) 1); |
339 addsimps [nat_succI, Ord_nat RSN (2, OrdmemD), image_fun]) 1); |
340 val image_fun_succ = result(); |
340 val image_fun_succ = result(); |
341 |
341 |
342 goal thy "!!f. [| domain(f`n) = succ(u); f : nat -> (UN n:nat. \ |
342 goal thy "!!f. [| domain(f`n) = succ(u); f : nat -> (UN n:nat. \ |
343 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
343 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
344 \ u=k; n:nat \ |
344 \ u=k; n:nat \ |
345 \ |] ==> f`n : succ(k) -> domain(R)"; |
345 \ |] ==> f`n : succ(k) -> domain(R)"; |
346 by (dtac apply_type 1 THEN (assume_tac 1)); |
346 by (dtac apply_type 1 THEN (assume_tac 1)); |
347 by (fast_tac (AC_cs addEs [UN_E, domain_eq_imp_fun_type]) 1); |
347 by (fast_tac (AC_cs addEs [UN_E, domain_eq_imp_fun_type]) 1); |
348 val f_n_type = result(); |
348 val f_n_type = result(); |
349 |
349 |
350 goal thy "!!f. [| f : nat -> (UN n:nat. \ |
350 goal thy "!!f. [| f : nat -> (UN n:nat. \ |
351 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
351 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
352 \ domain(f`n) = succ(k); n:nat \ |
352 \ domain(f`n) = succ(k); n:nat \ |
353 \ |] ==> ALL i:k. <f`n`i, f`n`succ(i)> : R"; |
353 \ |] ==> ALL i:k. <f`n`i, f`n`succ(i)> : R"; |
354 by (dtac apply_type 1 THEN (assume_tac 1)); |
354 by (dtac apply_type 1 THEN (assume_tac 1)); |
355 by (etac UN_E 1); |
355 by (etac UN_E 1); |
356 by (etac CollectE 1); |
356 by (etac CollectE 1); |
357 by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); |
357 by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); |
358 by (dtac succ_eqD 1); |
358 by (dtac succ_eqD 1); |
359 by (asm_full_simp_tac AC_ss 1); |
359 by (asm_full_simp_tac AC_ss 1); |
360 val f_n_pairs_in_R = result(); |
360 val f_n_pairs_in_R = result(); |
361 |
361 |
362 goalw thy [restrict_def] |
362 goalw thy [restrict_def] |
363 "!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \ |
363 "!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \ |
364 \ |] ==> restrict(cons(<n, y>, f), domain(x)) = x"; |
364 \ |] ==> restrict(cons(<n, y>, f), domain(x)) = x"; |
365 by (eresolve_tac [sym RS trans RS sym] 1); |
365 by (eresolve_tac [sym RS trans RS sym] 1); |
366 by (rtac fun_extension 1); |
366 by (rtac fun_extension 1); |
367 by (fast_tac (AC_cs addSIs [lam_type]) 1); |
367 by (fast_tac (AC_cs addSIs [lam_type]) 1); |
368 by (fast_tac (AC_cs addSIs [lam_type]) 1); |
368 by (fast_tac (AC_cs addSIs [lam_type]) 1); |
369 by (asm_full_simp_tac (AC_ss addsimps [subsetD RS cons_val_k]) 1); |
369 by (asm_full_simp_tac (AC_ss addsimps [subsetD RS cons_val_k]) 1); |
370 val restrict_cons_eq_restrict = result(); |
370 val restrict_cons_eq_restrict = result(); |
371 |
371 |
372 goal thy "!!f. [| ALL x:f``n. restrict(f`n, domain(x))=x; \ |
372 goal thy "!!f. [| ALL x:f``n. restrict(f`n, domain(x))=x; \ |
373 \ f : nat -> (UN n:nat. \ |
373 \ f : nat -> (UN n:nat. \ |
374 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
374 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
375 \ n:nat; domain(f`n) = succ(n); \ |
375 \ n:nat; domain(f`n) = succ(n); \ |
376 \ (UN x:f``n. domain(x)) <= n |] \ |
376 \ (UN x:f``n. domain(x)) <= n |] \ |
377 \ ==> ALL x:f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x))=x"; |
377 \ ==> ALL x:f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x))=x"; |
378 by (rtac ballI 1); |
378 by (rtac ballI 1); |
379 by (asm_full_simp_tac (AC_ss addsimps [image_fun_succ]) 1); |
379 by (asm_full_simp_tac (AC_ss addsimps [image_fun_succ]) 1); |
380 by (dtac f_n_type 1 THEN REPEAT (ares_tac [refl] 1)); |
380 by (dtac f_n_type 1 THEN REPEAT (ares_tac [refl] 1)); |
381 by (etac consE 1); |
381 by (etac consE 1); |
382 by (asm_full_simp_tac (AC_ss addsimps [domain_of_fun, restrict_cons_eq]) 1); |
382 by (asm_full_simp_tac (AC_ss addsimps [domain_of_fun, restrict_cons_eq]) 1); |
383 by (dtac bspec 1 THEN (assume_tac 1)); |
383 by (dtac bspec 1 THEN (assume_tac 1)); |
384 by (fast_tac (AC_cs addSEs [restrict_cons_eq_restrict]) 1); |
384 by (fast_tac (AC_cs addSEs [restrict_cons_eq_restrict]) 1); |
385 val all_in_image_restrict_eq = result(); |
385 val all_in_image_restrict_eq = result(); |
386 |
386 |
387 goal thy "!!X. [| ALL b<nat. <f``b, f`b> : \ |
387 goal thy "!!X. [| ALL b<nat. <f``b, f`b> : \ |
388 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
388 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
389 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \ |
389 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \ |
390 \ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \ |
390 \ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \ |
391 \ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \ |
391 \ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \ |
392 \ XX = (UN n:nat. \ |
392 \ XX = (UN n:nat. \ |
393 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
393 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
394 \ f: nat -> XX; range(R) <= domain(R); x:domain(R) \ |
394 \ f: nat -> XX; range(R) <= domain(R); x:domain(R) \ |
395 \ |] ==> ALL b<nat. <f``b, f`b> : \ |
395 \ |] ==> ALL b<nat. <f``b, f`b> : \ |
396 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
396 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
397 \ & (UN f:fst(z). domain(f)) = b \ |
397 \ & (UN f:fst(z). domain(f)) = b \ |
398 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}"; |
398 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}"; |
399 by (rtac oallI 1); |
399 by (rtac oallI 1); |
400 by (dtac ltD 1); |
400 by (dtac ltD 1); |
401 by (etac nat_induct 1); |
401 by (etac nat_induct 1); |
402 by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); |
402 by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); |
403 by (fast_tac (FOL_cs addss |
403 by (fast_tac (FOL_cs addss |
404 (ZF_ss addsimps [image_0, singleton_fun RS domain_of_fun, |
404 (ZF_ss addsimps [image_0, singleton_fun RS domain_of_fun, |
405 [lepoll_refl, succI1] MRS lepoll_1_is_sing, singleton_in_funs])) 1); |
405 [lepoll_refl, succI1] MRS lepoll_1_is_sing, singleton_in_funs])) 1); |
406 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
406 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
407 THEN (assume_tac 1)); |
407 THEN (assume_tac 1)); |
408 by (REPEAT (eresolve_tac [conjE, CollectE, disjE] 1)); |
408 by (REPEAT (eresolve_tac [conjE, CollectE, disjE] 1)); |
409 by (fast_tac (FOL_cs addSEs [trans, subst_context] |
409 by (fast_tac (FOL_cs addSEs [trans, subst_context] |
410 addSIs [UN_image_succ_eq_succ] addss AC_ss) 1); |
410 addSIs [UN_image_succ_eq_succ] addss AC_ss) 1); |
411 by (etac conjE 1); |
411 by (etac conjE 1); |
412 by (etac notE 1); |
412 by (etac notE 1); |
413 by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq_succ]) 1); |
413 by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq_succ]) 1); |
414 by (etac conjE 1); |
414 by (etac conjE 1); |
415 by (dtac apply_UN_type 1 THEN REPEAT (assume_tac 1)); |
415 by (dtac apply_UN_type 1 THEN REPEAT (assume_tac 1)); |
416 by (etac domainE 1); |
416 by (etac domainE 1); |
417 by (etac domainE 1); |
417 by (etac domainE 1); |
418 by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1)); |
418 by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1)); |
419 by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1); |
419 by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1); |
420 by (fast_tac (FOL_cs |
420 by (fast_tac (FOL_cs |
421 addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ, |
421 addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ, |
422 subst_context, all_in_image_restrict_eq, trans, equalityD1]) 1); |
422 subst_context, all_in_image_restrict_eq, trans, equalityD1]) 1); |
423 by (rtac UN_I 1); |
423 by (rtac UN_I 1); |
424 by (etac nat_succI 1); |
424 by (etac nat_succI 1); |
425 by (rtac CollectI 1); |
425 by (rtac CollectI 1); |
426 by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 1 |
426 by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 1 |
427 THEN REPEAT (assume_tac 1)); |
427 THEN REPEAT (assume_tac 1)); |
428 by (rtac ballI 1); |
428 by (rtac ballI 1); |
429 by (etac succE 1); |
429 by (etac succE 1); |
430 by (asm_full_simp_tac (AC_ss addsimps [cons_val_n, cons_val_k]) 1); |
430 by (asm_full_simp_tac (AC_ss addsimps [cons_val_n, cons_val_k]) 1); |
431 by (dresolve_tac [domain_of_fun RSN (2, f_n_pairs_in_R)] 1 |
431 by (dresolve_tac [domain_of_fun RSN (2, f_n_pairs_in_R)] 1 |
432 THEN REPEAT (assume_tac 1)); |
432 THEN REPEAT (assume_tac 1)); |
433 by (dtac bspec 1 THEN (assume_tac 1)); |
433 by (dtac bspec 1 THEN (assume_tac 1)); |
434 by (asm_full_simp_tac (AC_ss |
434 by (asm_full_simp_tac (AC_ss |
435 addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 1); |
435 addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 1); |
436 val simplify_recursion = result(); |
436 val simplify_recursion = result(); |
437 |
437 |
438 goal thy "!!X. [| XX = (UN n:nat. \ |
438 goal thy "!!X. [| XX = (UN n:nat. \ |
439 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
439 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
440 \ ALL b<nat. <f``b, f`b> : \ |
440 \ ALL b<nat. <f``b, f`b> : \ |
441 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
441 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
442 \ & (UN f:fst(z). domain(f)) = b \ |
442 \ & (UN f:fst(z). domain(f)) = b \ |
443 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ |
443 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ |
444 \ f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat \ |
444 \ f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat \ |
445 \ |] ==> f`n : succ(n) -> domain(R) \ |
445 \ |] ==> f`n : succ(n) -> domain(R) \ |
446 \ & (ALL i:n. <f`n`i, f`n`succ(i)>:R)"; |
446 \ & (ALL i:n. <f`n`i, f`n`succ(i)>:R)"; |
447 by (dtac ospec 1); |
447 by (dtac ospec 1); |
448 by (eresolve_tac [Ord_nat RSN (2, ltI)] 1); |
448 by (eresolve_tac [Ord_nat RSN (2, ltI)] 1); |
449 by (etac CollectE 1); |
449 by (etac CollectE 1); |
450 by (asm_full_simp_tac AC_ss 1); |
450 by (asm_full_simp_tac AC_ss 1); |
451 by (rtac conjI 1); |
451 by (rtac conjI 1); |
452 by (fast_tac (AC_cs |
452 by (fast_tac (AC_cs |
453 addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1); |
453 addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1); |
454 by (fast_tac (FOL_cs |
454 by (fast_tac (FOL_cs |
455 addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 1); |
455 addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 1); |
456 val lemma2 = result(); |
456 val lemma2 = result(); |
457 |
457 |
458 goal thy "!!n. [| XX = (UN n:nat. \ |
458 goal thy "!!n. [| XX = (UN n:nat. \ |
459 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
459 \ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \ |
460 \ ALL b<nat. <f``b, f`b> : \ |
460 \ ALL b<nat. <f``b, f`b> : \ |
461 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
461 \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ |
462 \ & (UN f:fst(z). domain(f)) = b \ |
462 \ & (UN f:fst(z). domain(f)) = b \ |
463 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ |
463 \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ |
464 \ f : nat -> XX; n:nat; range(R) <= domain(R); x:domain(R) \ |
464 \ f : nat -> XX; n:nat; range(R) <= domain(R); x:domain(R) \ |
465 \ |] ==> f`n`n = f`succ(n)`n"; |
465 \ |] ==> f`n`n = f`succ(n)`n"; |
466 by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1 |
466 by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1 |
467 THEN REPEAT (assume_tac 1)); |
467 THEN REPEAT (assume_tac 1)); |
468 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
468 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
469 THEN (assume_tac 1)); |
469 THEN (assume_tac 1)); |
470 by (asm_full_simp_tac AC_ss 1); |
470 by (asm_full_simp_tac AC_ss 1); |
471 by (REPEAT (etac conjE 1)); |
471 by (REPEAT (etac conjE 1)); |
472 by (etac ballE 1); |
472 by (etac ballE 1); |
473 by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1); |
473 by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1); |
474 by (fast_tac (AC_cs addSEs [ssubst]) 1); |
474 by (fast_tac (AC_cs addSEs [ssubst]) 1); |
475 by (asm_full_simp_tac (AC_ss |
475 by (asm_full_simp_tac (AC_ss |
476 addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
476 addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
477 val lemma3 = result(); |
477 val lemma3 = result(); |
478 |
478 |
479 goalw thy [DC_def, DC0_def] "!!Z. DC(nat) ==> DC0"; |
479 goalw thy [DC_def, DC0_def] "!!Z. DC(nat) ==> DC0"; |
480 by (REPEAT (resolve_tac [allI, impI] 1)); |
480 by (REPEAT (resolve_tac [allI, impI] 1)); |
481 by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1)); |
481 by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1)); |
482 by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 |
482 by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 |
483 THEN REPEAT (assume_tac 1)); |
483 THEN REPEAT (assume_tac 1)); |
484 by (etac bexE 1); |
484 by (etac bexE 1); |
485 by (dresolve_tac [refl RSN (2, simplify_recursion)] 1 |
485 by (dresolve_tac [refl RSN (2, simplify_recursion)] 1 |
486 THEN REPEAT (assume_tac 1)); |
486 THEN REPEAT (assume_tac 1)); |
487 by (res_inst_tac [("x","lam n:nat. f`n`n")] bexI 1); |
487 by (res_inst_tac [("x","lam n:nat. f`n`n")] bexI 1); |
488 by (rtac lam_type 2); |
488 by (rtac lam_type 2); |
489 by (eresolve_tac [[refl RS lemma2 RS conjunct1, succI1] MRS apply_type] 2 |
489 by (eresolve_tac [[refl RS lemma2 RS conjunct1, succI1] MRS apply_type] 2 |
490 THEN REPEAT (assume_tac 2)); |
490 THEN REPEAT (assume_tac 2)); |
491 by (rtac ballI 1); |
491 by (rtac ballI 1); |
492 by (forward_tac [refl RS (nat_succI RSN (6, lemma2)) RS conjunct2] 1 |
492 by (forward_tac [refl RS (nat_succI RSN (6, lemma2)) RS conjunct2] 1 |
493 THEN REPEAT (assume_tac 1)); |
493 THEN REPEAT (assume_tac 1)); |
494 by (dresolve_tac [refl RS lemma3] 1 THEN REPEAT (assume_tac 1)); |
494 by (dresolve_tac [refl RS lemma3] 1 THEN REPEAT (assume_tac 1)); |
495 by (asm_full_simp_tac (AC_ss addsimps [nat_succI]) 1); |
495 by (asm_full_simp_tac (AC_ss addsimps [nat_succI]) 1); |
496 qed "DC_nat_DC0"; |
496 qed "DC_nat_DC0"; |
497 |
497 |
498 (* ********************************************************************** *) |
498 (* ********************************************************************** *) |
499 (* ALL K. Card(K) --> DC(K) ==> WO3 *) |
499 (* ALL K. Card(K) --> DC(K) ==> WO3 *) |
500 (* ********************************************************************** *) |
500 (* ********************************************************************** *) |
501 |
501 |
502 goalw thy [lesspoll_def] |
502 goalw thy [lesspoll_def] |
503 "!!A. [| ~ A lesspoll B; C lesspoll B |] ==> A - C ~= 0"; |
503 "!!A. [| ~ A lesspoll B; C lesspoll B |] ==> A - C ~= 0"; |
504 by (fast_tac (AC_cs addSDs [Diff_eq_0_iff RS iffD1 RS subset_imp_lepoll] |
504 by (fast_tac (AC_cs addSDs [Diff_eq_0_iff RS iffD1 RS subset_imp_lepoll] |
505 addSIs [eqpollI] addEs [notE] addSEs [eqpollE, lepoll_trans]) 1); |
505 addSIs [eqpollI] addEs [notE] addSEs [eqpollE, lepoll_trans]) 1); |
506 val lemma1 = result(); |
506 val lemma1 = result(); |
507 |
507 |
508 val [f_type, Ord_a, not_eq] = goalw thy [inj_def] |
508 val [f_type, Ord_a, not_eq] = goalw thy [inj_def] |
509 "[| f:a->X; Ord(a); (!!b c. [| b<c; c:a |] ==> f`b~=f`c) \ |
509 "[| f:a->X; Ord(a); (!!b c. [| b<c; c:a |] ==> f`b~=f`c) \ |
510 \ |] ==> f:inj(a, X)"; |
510 \ |] ==> f:inj(a, X)"; |
511 by (resolve_tac [f_type RS CollectI] 1); |
511 by (resolve_tac [f_type RS CollectI] 1); |
512 by (REPEAT (resolve_tac [ballI,impI] 1)); |
512 by (REPEAT (resolve_tac [ballI,impI] 1)); |
513 by (resolve_tac [Ord_a RS Ord_in_Ord RS Ord_linear_lt] 1 |
513 by (resolve_tac [Ord_a RS Ord_in_Ord RS Ord_linear_lt] 1 |
514 THEN (assume_tac 1)); |
514 THEN (assume_tac 1)); |
515 by (eres_inst_tac [("j","x")] (Ord_a RS Ord_in_Ord) 1); |
515 by (eres_inst_tac [("j","x")] (Ord_a RS Ord_in_Ord) 1); |
516 by (REPEAT (fast_tac (AC_cs addDs [not_eq, not_eq RS not_sym]) 1)); |
516 by (REPEAT (fast_tac (AC_cs addDs [not_eq, not_eq RS not_sym]) 1)); |
517 val fun_Ord_inj = result(); |
517 val fun_Ord_inj = result(); |
518 |
518 |
519 goal thy "!!a. [| f:X->Y; A<=X; a:A |] ==> f`a : f``A"; |
519 goal thy "!!a. [| f:X->Y; A<=X; a:A |] ==> f`a : f``A"; |
520 by (fast_tac (AC_cs addSEs [image_fun RS ssubst]) 1); |
520 by (fast_tac (AC_cs addSEs [image_fun RS ssubst]) 1); |
521 val value_in_image = result(); |
521 val value_in_image = result(); |
522 |
522 |
523 goalw thy [DC_def, WO3_def] |
523 goalw thy [DC_def, WO3_def] |
524 "!!Z. ALL K. Card(K) --> DC(K) ==> WO3"; |
524 "!!Z. ALL K. Card(K) --> DC(K) ==> WO3"; |
525 by (rtac allI 1); |
525 by (rtac allI 1); |
526 by (excluded_middle_tac "A lesspoll Hartog(A)" 1); |
526 by (excluded_middle_tac "A lesspoll Hartog(A)" 1); |
527 by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll] |
527 by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll] |
528 addSIs [Ord_Hartog, leI RS le_imp_subset]) 2); |
528 addSIs [Ord_Hartog, leI RS le_imp_subset]) 2); |
529 by (REPEAT (eresolve_tac [allE, impE] 1)); |
529 by (REPEAT (eresolve_tac [allE, impE] 1)); |
530 by (rtac Card_Hartog 1); |
530 by (rtac Card_Hartog 1); |
531 by (eres_inst_tac [("x","A")] allE 1); |
531 by (eres_inst_tac [("x","A")] allE 1); |
532 by (eres_inst_tac [("x","{z:Pow(A)*A . fst(z) \ |
532 by (eres_inst_tac [("x","{z:Pow(A)*A . fst(z) \ |
533 \ lesspoll Hartog(A) & snd(z) ~: fst(z)}")] allE 1); |
533 \ lesspoll Hartog(A) & snd(z) ~: fst(z)}")] allE 1); |
534 by (asm_full_simp_tac AC_ss 1); |
534 by (asm_full_simp_tac AC_ss 1); |
535 by (etac impE 1); |
535 by (etac impE 1); |
536 by (fast_tac (AC_cs addEs [lemma1 RS not_emptyE]) 1); |
536 by (fast_tac (AC_cs addEs [lemma1 RS not_emptyE]) 1); |
537 by (etac bexE 1); |
537 by (etac bexE 1); |
538 by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2)) |
538 by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2)) |
539 RS (HartogI RS notE)] 1); |
539 RS (HartogI RS notE)] 1); |
540 by (resolve_tac [Ord_Hartog RSN (2, fun_Ord_inj)] 1 THEN (assume_tac 1)); |
540 by (resolve_tac [Ord_Hartog RSN (2, fun_Ord_inj)] 1 THEN (assume_tac 1)); |
541 by (dresolve_tac [Ord_Hartog RSN (2, OrdmemD) RSN (2, |
541 by (dresolve_tac [Ord_Hartog RSN (2, OrdmemD) RSN (2, |
542 ltD RSN (3, value_in_image))] 1 |
542 ltD RSN (3, value_in_image))] 1 |
543 THEN REPEAT (assume_tac 1)); |
543 THEN REPEAT (assume_tac 1)); |
544 by (fast_tac (AC_cs addSDs [Ord_Hartog RSN (2, ltI) RSN (2, ospec)] |
544 by (fast_tac (AC_cs addSDs [Ord_Hartog RSN (2, ltI) RSN (2, ospec)] |
545 addEs [subst]) 1); |
545 addEs [subst]) 1); |
546 qed "DC_WO3"; |
546 qed "DC_WO3"; |
547 |
547 |
548 (* ********************************************************************** *) |
548 (* ********************************************************************** *) |
549 (* WO1 ==> ALL K. Card(K) --> DC(K) *) |
549 (* WO1 ==> ALL K. Card(K) --> DC(K) *) |
550 (* ********************************************************************** *) |
550 (* ********************************************************************** *) |
551 |
551 |
552 goal thy |
552 goal thy |
553 "!!a. [| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b"; |
553 "!!a. [| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b"; |
554 by (rtac images_eq 1); |
554 by (rtac images_eq 1); |
555 by (REPEAT (fast_tac (AC_cs addSEs [RepFunI, OrdmemD] |
555 by (REPEAT (fast_tac (AC_cs addSEs [RepFunI, OrdmemD] |
556 addSIs [lam_type]) 2)); |
556 addSIs [lam_type]) 2)); |
557 by (rtac ballI 1); |
557 by (rtac ballI 1); |
558 by (dresolve_tac [OrdmemD RS subsetD] 1 |
558 by (dresolve_tac [OrdmemD RS subsetD] 1 |
559 THEN REPEAT (assume_tac 1)); |
559 THEN REPEAT (assume_tac 1)); |
560 by (asm_full_simp_tac AC_ss 1); |
560 by (asm_full_simp_tac AC_ss 1); |
561 val lam_images_eq = result(); |
561 val lam_images_eq = result(); |
562 |
562 |
563 goalw thy [lesspoll_def] "!!K. [| Card(K); b:K |] ==> b lesspoll K"; |
563 goalw thy [lesspoll_def] "!!K. [| Card(K); b:K |] ==> b lesspoll K"; |
564 by (asm_full_simp_tac (AC_ss addsimps [Card_iff_initial]) 1); |
564 by (asm_full_simp_tac (AC_ss addsimps [Card_iff_initial]) 1); |