|
1 (* Title: ZF/AC/AC15_WO6.ML |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Gr`abczewski |
|
4 |
|
5 The proof of AC1 ==> WO2 |
|
6 *) |
|
7 |
|
8 open AC15_WO6; |
|
9 |
|
10 goal thy "!!x. Ord(x) ==> (UN a<x. F(a)) = (UN a:x. F(a))"; |
|
11 by (fast_tac (AC_cs addSIs [equalityI, ltI] addSDs [ltD]) 1); |
|
12 val OUN_eq_UN = result(); |
|
13 |
|
14 val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==> \ |
|
15 \ (UN i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A"; |
|
16 by (simp_tac (AC_ss addsimps [Ord_Least RS OUN_eq_UN]) 1); |
|
17 by (resolve_tac [equalityI] 1); |
|
18 by (fast_tac (AC_cs addSDs [less_Least_subset_x]) 1); |
|
19 by (fast_tac (AC_cs addSDs [prem RS bspec] |
|
20 addSIs [f_subsets_imp_UN_HH_eq_x RS (Diff_eq_0_iff RS iffD1)]) 1); |
|
21 val lemma1 = result(); |
|
22 |
|
23 val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==> \ |
|
24 \ ALL x<LEAST x. HH(f,A,x)={A}. HH(f,A,x) lepoll m"; |
|
25 by (resolve_tac [oallI] 1); |
|
26 by (dresolve_tac [ltD RS less_Least_subset_x] 1); |
|
27 by (forward_tac [HH_subset_imp_eq] 1); |
|
28 by (eresolve_tac [ssubst] 1); |
|
29 by (fast_tac (AC_cs addIs [prem RS ballE] |
|
30 addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1); |
|
31 val lemma2 = result(); |
|
32 |
|
33 goalw thy [AC15_def, WO6_def] "!!Z. AC15 ==> WO6"; |
|
34 by (resolve_tac [allI] 1); |
|
35 by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); |
|
36 by (eresolve_tac [impE] 1); |
|
37 by (fast_tac ZF_cs 1); |
|
38 by (REPEAT (eresolve_tac [bexE,conjE,exE] 1)); |
|
39 by (resolve_tac [bexI] 1 THEN (assume_tac 2)); |
|
40 by (resolve_tac [conjI] 1 THEN (assume_tac 1)); |
|
41 by (res_inst_tac [("x","LEAST i. HH(f,A,i)={A}")] exI 1); |
|
42 by (res_inst_tac [("x","lam j: (LEAST i. HH(f,A,i)={A}). HH(f,A,j)")] exI 1); |
|
43 by (asm_full_simp_tac AC_ss 1); |
|
44 by (fast_tac (AC_cs addSIs [Ord_Least, lam_type RS domain_of_fun] |
|
45 addSEs [less_Least_subset_x, lemma1, lemma2]) 1); |
|
46 result(); |