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