1 (* Title: ZF/AC/AC1_WO2.ML |
1 (* Title: ZF/AC/AC1_WO2.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Krzysztof Gr`abczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 The proof of AC1 ==> WO2 |
5 The proof of AC1 ==> WO2 |
6 *) |
6 *) |
7 |
7 |
8 open AC1_WO2; |
8 open AC1_WO2; |
9 |
9 |
10 val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==> \ |
10 val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==> \ |
11 \ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})"; |
11 \ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})"; |
12 by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1); |
12 by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1); |
13 by (resolve_tac [f_subsets_imp_UN_HH_eq_x] 1); |
13 by (rtac f_subsets_imp_UN_HH_eq_x 1); |
14 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2)); |
14 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2)); |
15 by (fast_tac (AC_cs addSDs [equals0D, prem RS apply_type]) 1); |
15 by (fast_tac (AC_cs addSDs [equals0D, prem RS apply_type]) 1); |
16 by (fast_tac (AC_cs addSIs [prem RS Pi_weaken_type]) 1); |
16 by (fast_tac (AC_cs addSIs [prem RS Pi_weaken_type]) 1); |
17 val lemma1 = uresult(); |
17 val lemma1 = uresult(); |
18 |
18 |
19 goalw thy [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2"; |
19 goalw thy [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2"; |
20 by (resolve_tac [allI] 1); |
20 by (rtac allI 1); |
21 by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); |
21 by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); |
22 by (fast_tac (AC_cs addSDs [lemma1] addSIs [Ord_Least]) 1); |
22 by (fast_tac (AC_cs addSDs [lemma1] addSIs [Ord_Least]) 1); |
23 qed "AC1_WO2"; |
23 qed "AC1_WO2"; |