1 (* Title: ZF/AC/AC17_AC1.ML |
1 (* Title: ZF/AC/AC17_AC1.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Krzysztof Grabczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 The proof of AC1 ==> AC17 |
5 The proof of AC1 ==> AC17 |
6 *) |
6 *) |
7 |
7 |
8 open AC17_AC1; |
8 open AC17_AC1; |
9 |
9 |
10 (* *********************************************************************** *) |
10 (* *********************************************************************** *) |
11 (* more properties of HH *) |
11 (* more properties of HH *) |
12 (* *********************************************************************** *) |
12 (* *********************************************************************** *) |
13 |
13 |
14 goal thy "!!f. [| x - (UN j:LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x}. \ |
14 goal thy "!!f. [| x - (UN j:LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x}. \ |
15 \ HH(lam X:Pow(x)-{0}. {f`X}, x, j)) = 0; \ |
15 \ HH(lam X:Pow(x)-{0}. {f`X}, x, j)) = 0; \ |
16 \ f : Pow(x)-{0} -> x |] \ |
16 \ f : Pow(x)-{0} -> x |] \ |
17 \ ==> EX r. well_ord(x,r)"; |
17 \ ==> EX r. well_ord(x,r)"; |
18 by (rtac exI 1); |
18 by (rtac exI 1); |
19 by (eresolve_tac [[bij_Least_HH_x RS bij_converse_bij RS bij_is_inj, |
19 by (eresolve_tac [[bij_Least_HH_x RS bij_converse_bij RS bij_is_inj, |
20 Ord_Least RS well_ord_Memrel] MRS well_ord_rvimage] 1); |
20 Ord_Least RS well_ord_Memrel] MRS well_ord_rvimage] 1); |
21 by (assume_tac 1); |
21 by (assume_tac 1); |
22 val UN_eq_imp_well_ord = result(); |
22 val UN_eq_imp_well_ord = result(); |
23 |
23 |
24 (* *********************************************************************** *) |
24 (* *********************************************************************** *) |
25 (* theorems closer to the proof *) |
25 (* theorems closer to the proof *) |
26 (* *********************************************************************** *) |
26 (* *********************************************************************** *) |
27 |
27 |
28 goalw thy AC_defs "!!Z. ~AC1 ==> \ |
28 goalw thy AC_defs "!!Z. ~AC1 ==> \ |
29 \ EX A. ALL f:Pow(A)-{0} -> A. EX u:Pow(A)-{0}. f`u ~: u"; |
29 \ EX A. ALL f:Pow(A)-{0} -> A. EX u:Pow(A)-{0}. f`u ~: u"; |
30 by (etac swap 1); |
30 by (etac swap 1); |
31 by (rtac allI 1); |
31 by (rtac allI 1); |
32 by (etac swap 1); |
32 by (etac swap 1); |
33 by (res_inst_tac [("x","Union(A)")] exI 1); |
33 by (res_inst_tac [("x","Union(A)")] exI 1); |
34 by (rtac ballI 1); |
34 by (rtac ballI 1); |
36 by (rtac impI 1); |
36 by (rtac impI 1); |
37 by (fast_tac (AC_cs addSIs [restrict_type]) 1); |
37 by (fast_tac (AC_cs addSIs [restrict_type]) 1); |
38 val not_AC1_imp_ex = result(); |
38 val not_AC1_imp_ex = result(); |
39 |
39 |
40 goal thy "!!x. [| ALL f:Pow(x) - {0} -> x. EX u: Pow(x) - {0}. f`u~:u; \ |
40 goal thy "!!x. [| ALL f:Pow(x) - {0} -> x. EX u: Pow(x) - {0}. f`u~:u; \ |
41 \ EX f: Pow(x)-{0}->x. \ |
41 \ EX f: Pow(x)-{0}->x. \ |
42 \ x - (UN a:(LEAST i. HH(lam X:Pow(x)-{0}. {f`X},x,i)={x}). \ |
42 \ x - (UN a:(LEAST i. HH(lam X:Pow(x)-{0}. {f`X},x,i)={x}). \ |
43 \ HH(lam X:Pow(x)-{0}. {f`X},x,a)) = 0 |] \ |
43 \ HH(lam X:Pow(x)-{0}. {f`X},x,a)) = 0 |] \ |
44 \ ==> P"; |
44 \ ==> P"; |
45 by (etac bexE 1); |
45 by (etac bexE 1); |
46 by (eresolve_tac [UN_eq_imp_well_ord RS exE] 1 THEN (assume_tac 1)); |
46 by (eresolve_tac [UN_eq_imp_well_ord RS exE] 1 THEN (assume_tac 1)); |
47 by (eresolve_tac [ex_choice_fun_Pow RS exE] 1); |
47 by (eresolve_tac [ex_choice_fun_Pow RS exE] 1); |
48 by (etac ballE 1); |
48 by (etac ballE 1); |
49 by (fast_tac (FOL_cs addEs [bexE, notE, apply_type]) 1); |
49 by (fast_tac (FOL_cs addEs [bexE, notE, apply_type]) 1); |
52 by (resolve_tac [apply_type RSN (2, subsetD)] 1 THEN TRYALL assume_tac); |
52 by (resolve_tac [apply_type RSN (2, subsetD)] 1 THEN TRYALL assume_tac); |
53 by (fast_tac AC_cs 1); |
53 by (fast_tac AC_cs 1); |
54 val lemma1 = result(); |
54 val lemma1 = result(); |
55 |
55 |
56 goal thy "!!x. ~ (EX f: Pow(x)-{0}->x. x - F(f) = 0) \ |
56 goal thy "!!x. ~ (EX f: Pow(x)-{0}->x. x - F(f) = 0) \ |
57 \ ==> (lam f: Pow(x)-{0}->x. x - F(f)) \ |
57 \ ==> (lam f: Pow(x)-{0}->x. x - F(f)) \ |
58 \ : (Pow(x) -{0} -> x) -> Pow(x) - {0}"; |
58 \ : (Pow(x) -{0} -> x) -> Pow(x) - {0}"; |
59 by (fast_tac (AC_cs addSIs [lam_type] addIs [equalityI] |
59 by (fast_tac (AC_cs addSIs [lam_type] addIs [equalityI] |
60 addSDs [Diff_eq_0_iff RS iffD1]) 1); |
60 addSDs [Diff_eq_0_iff RS iffD1]) 1); |
61 val lemma2 = result(); |
61 val lemma2 = result(); |
62 |
62 |
63 goal thy "!!f. [| f`Z : Z; Z:Pow(x)-{0} |] ==> \ |
63 goal thy "!!f. [| f`Z : Z; Z:Pow(x)-{0} |] ==> \ |
64 \ (lam X:Pow(x)-{0}. {f`X})`Z : Pow(Z)-{0}"; |
64 \ (lam X:Pow(x)-{0}. {f`X})`Z : Pow(Z)-{0}"; |
65 by (asm_full_simp_tac AC_ss 1); |
65 by (asm_full_simp_tac AC_ss 1); |
66 by (fast_tac (AC_cs addSDs [equals0D]) 1); |
66 by (fast_tac (AC_cs addSDs [equals0D]) 1); |
67 val lemma3 = result(); |
67 val lemma3 = result(); |
68 |
68 |
69 goal thy "!!z. EX f:F. f`((lam f:F. Q(f))`f) : (lam f:F. Q(f))`f \ |
69 goal thy "!!z. EX f:F. f`((lam f:F. Q(f))`f) : (lam f:F. Q(f))`f \ |
70 \ ==> EX f:F. f`Q(f) : Q(f)"; |
70 \ ==> EX f:F. f`Q(f) : Q(f)"; |
71 by (asm_full_simp_tac AC_ss 1); |
71 by (asm_full_simp_tac AC_ss 1); |
72 val lemma4 = result(); |
72 val lemma4 = result(); |
73 |
73 |
74 goalw thy [AC17_def] "!!Z. AC17 ==> AC1"; |
74 goalw thy [AC17_def] "!!Z. AC17 ==> AC1"; |
75 by (rtac classical 1); |
75 by (rtac classical 1); |
76 by (eresolve_tac [not_AC1_imp_ex RS exE] 1); |
76 by (eresolve_tac [not_AC1_imp_ex RS exE] 1); |
77 by (excluded_middle_tac |
77 by (excluded_middle_tac |
78 "EX f: Pow(x)-{0}->x. \ |
78 "EX f: Pow(x)-{0}->x. \ |
79 \ x - (UN a:(LEAST i. HH(lam X:Pow(x)-{0}. {f`X},x,i)={x}). \ |
79 \ x - (UN a:(LEAST i. HH(lam X:Pow(x)-{0}. {f`X},x,i)={x}). \ |
80 \ HH(lam X:Pow(x)-{0}. {f`X},x,a)) = 0" 1); |
80 \ HH(lam X:Pow(x)-{0}. {f`X},x,a)) = 0" 1); |
81 by (etac lemma1 2 THEN (assume_tac 2)); |
81 by (etac lemma1 2 THEN (assume_tac 2)); |
82 by (dtac lemma2 1); |
82 by (dtac lemma2 1); |
83 by (etac allE 1); |
83 by (etac allE 1); |
84 by (dtac bspec 1 THEN (assume_tac 1)); |
84 by (dtac bspec 1 THEN (assume_tac 1)); |
85 by (dtac lemma4 1); |
85 by (dtac lemma4 1); |
87 by (dtac apply_type 1 THEN (assume_tac 1)); |
87 by (dtac apply_type 1 THEN (assume_tac 1)); |
88 by (dresolve_tac [beta RS sym RSN (2, subst_elem)] 1); |
88 by (dresolve_tac [beta RS sym RSN (2, subst_elem)] 1); |
89 by (assume_tac 1); |
89 by (assume_tac 1); |
90 by (dtac lemma3 1 THEN (assume_tac 1)); |
90 by (dtac lemma3 1 THEN (assume_tac 1)); |
91 by (fast_tac (AC_cs addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem), |
91 by (fast_tac (AC_cs addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem), |
92 f_subset_imp_HH_subset] addSEs [mem_irrefl]) 1); |
92 f_subset_imp_HH_subset] addSEs [mem_irrefl]) 1); |
93 qed "AC17_AC1"; |
93 qed "AC17_AC1"; |