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 (resolve_tac [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 |
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 (eresolve_tac [swap] 1); |
30 by (etac swap 1); |
31 by (resolve_tac [allI] 1); |
31 by (rtac allI 1); |
32 by (eresolve_tac [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 (resolve_tac [ballI] 1); |
34 by (rtac ballI 1); |
35 by (eresolve_tac [swap] 1); |
35 by (etac swap 1); |
36 by (resolve_tac [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 (eresolve_tac [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 (eresolve_tac [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); |
50 by (eresolve_tac [notE] 1); |
50 by (etac notE 1); |
51 by (resolve_tac [Pi_type] 1 THEN (assume_tac 1)); |
51 by (rtac Pi_type 1 THEN (assume_tac 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) \ |
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 (resolve_tac [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 (eresolve_tac [lemma1] 2 THEN (assume_tac 2)); |
81 by (etac lemma1 2 THEN (assume_tac 2)); |
82 by (dresolve_tac [lemma2] 1); |
82 by (dtac lemma2 1); |
83 by (eresolve_tac [allE] 1); |
83 by (etac allE 1); |
84 by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); |
84 by (dtac bspec 1 THEN (assume_tac 1)); |
85 by (dresolve_tac [lemma4] 1); |
85 by (dtac lemma4 1); |
86 by (eresolve_tac [bexE] 1); |
86 by (etac bexE 1); |
87 by (dresolve_tac [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 (dresolve_tac [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"; |