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); |
35 by (etac swap 1); |
35 by (etac swap 1); |
36 by (rtac impI 1); |
36 by (rtac impI 1); |
37 by (fast_tac (!claset addSIs [restrict_type]) 1); |
37 by (fast_tac (claset() addSIs [restrict_type]) 1); |
38 qed "not_AC1_imp_ex"; |
38 qed "not_AC1_imp_ex"; |
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}). \ |
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 (!claset addSIs [lam_type] addSDs [Diff_eq_0_iff RS iffD1]) 1); |
59 by (fast_tac (claset() addSIs [lam_type] addSDs [Diff_eq_0_iff RS iffD1]) 1); |
60 val lemma2 = result(); |
60 val lemma2 = result(); |
61 |
61 |
62 goal thy "!!f. [| f`Z : Z; Z:Pow(x)-{0} |] ==> \ |
62 goal thy "!!f. [| f`Z : Z; Z:Pow(x)-{0} |] ==> \ |
63 \ (lam X:Pow(x)-{0}. {f`X})`Z : Pow(Z)-{0}"; |
63 \ (lam X:Pow(x)-{0}. {f`X})`Z : Pow(Z)-{0}"; |
64 by (Asm_full_simp_tac 1); |
64 by (Asm_full_simp_tac 1); |
65 by (fast_tac (!claset addSDs [equals0D]) 1); |
65 by (fast_tac (claset() addSDs [equals0D]) 1); |
66 val lemma3 = result(); |
66 val lemma3 = result(); |
67 |
67 |
68 goal thy "!!z. EX f:F. f`((lam f:F. Q(f))`f) : (lam f:F. Q(f))`f \ |
68 goal thy "!!z. EX f:F. f`((lam f:F. Q(f))`f) : (lam f:F. Q(f))`f \ |
69 \ ==> EX f:F. f`Q(f) : Q(f)"; |
69 \ ==> EX f:F. f`Q(f) : Q(f)"; |
70 by (Asm_full_simp_tac 1); |
70 by (Asm_full_simp_tac 1); |
85 by (etac bexE 1); |
85 by (etac bexE 1); |
86 by (dtac apply_type 1 THEN (assume_tac 1)); |
86 by (dtac apply_type 1 THEN (assume_tac 1)); |
87 by (dresolve_tac [beta RS sym RSN (2, subst_elem)] 1); |
87 by (dresolve_tac [beta RS sym RSN (2, subst_elem)] 1); |
88 by (assume_tac 1); |
88 by (assume_tac 1); |
89 by (dtac lemma3 1 THEN (assume_tac 1)); |
89 by (dtac lemma3 1 THEN (assume_tac 1)); |
90 by (fast_tac (!claset addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem), |
90 by (fast_tac (claset() addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem), |
91 f_subset_imp_HH_subset] addSEs [mem_irrefl]) 1); |
91 f_subset_imp_HH_subset] addSEs [mem_irrefl]) 1); |
92 qed "AC17_AC1"; |
92 qed "AC17_AC1"; |