1461
|
1 |
(* Title: ZF/AC/AC15_WO6.ML
|
1123
|
2 |
ID: $Id$
|
1461
|
3 |
Author: Krzysztof Grabczewski
|
1123
|
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))";
|
2496
|
11 |
by (fast_tac (!claset addSIs [ltI] addSDs [ltD]) 1);
|
3731
|
12 |
qed "OUN_eq_UN";
|
1123
|
13 |
|
|
14 |
val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==> \
|
1461
|
15 |
\ (UN i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A";
|
2469
|
16 |
by (simp_tac (!simpset addsimps [Ord_Least RS OUN_eq_UN]) 1);
|
1205
|
17 |
by (rtac equalityI 1);
|
2469
|
18 |
by (fast_tac (!claset addSDs [less_Least_subset_x]) 1);
|
|
19 |
by (fast_tac (!claset addSDs [prem RS bspec]
|
1461
|
20 |
addSIs [f_subsets_imp_UN_HH_eq_x RS (Diff_eq_0_iff RS iffD1)]) 1);
|
1123
|
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 ==> \
|
1461
|
24 |
\ ALL x<LEAST x. HH(f,A,x)={A}. HH(f,A,x) lepoll m";
|
1205
|
25 |
by (rtac oallI 1);
|
1123
|
26 |
by (dresolve_tac [ltD RS less_Least_subset_x] 1);
|
|
27 |
by (forward_tac [HH_subset_imp_eq] 1);
|
1205
|
28 |
by (etac ssubst 1);
|
2469
|
29 |
by (fast_tac (!claset addIs [prem RS ballE]
|
1461
|
30 |
addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
|
1123
|
31 |
val lemma2 = result();
|
|
32 |
|
|
33 |
goalw thy [AC15_def, WO6_def] "!!Z. AC15 ==> WO6";
|
1205
|
34 |
by (rtac allI 1);
|
1123
|
35 |
by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
|
1205
|
36 |
by (etac impE 1);
|
2469
|
37 |
by (Fast_tac 1);
|
1123
|
38 |
by (REPEAT (eresolve_tac [bexE,conjE,exE] 1));
|
1205
|
39 |
by (rtac bexI 1 THEN (assume_tac 2));
|
|
40 |
by (rtac conjI 1 THEN (assume_tac 1));
|
1123
|
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);
|
2469
|
43 |
by (Asm_full_simp_tac 1);
|
|
44 |
by (fast_tac (!claset addSIs [Ord_Least, lam_type RS domain_of_fun]
|
1461
|
45 |
addSEs [less_Least_subset_x, lemma1, lemma2]) 1);
|
1196
|
46 |
qed "AC15_WO6";
|