author | paulson |
Thu, 07 Jan 1999 18:30:55 +0100 | |
changeset 6070 | 032babd0120b |
parent 5147 | 825877190618 |
child 7499 | 23e090051cb8 |
permissions | -rw-r--r-- |
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 |
||
5137 | 10 |
Goal "Ord(x) ==> (UN a<x. F(a)) = (UN a:x. F(a))"; |
4091 | 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"; |
4091 | 16 |
by (simp_tac (simpset() addsimps [Ord_Least RS OUN_eq_UN]) 1); |
1205 | 17 |
by (rtac equalityI 1); |
4091 | 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); |
4091 | 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 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
33 |
Goalw [AC15_def, WO6_def] "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); |
4091 | 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"; |