author  paulson 
Tue, 04 Aug 1998 16:05:19 +0200  
changeset 5241  e5129172cb2b 
parent 5147  825877190618 
child 5470  855654b691db 
permissions  rwrr 
1461  1 
(* Title: ZF/AC/AC1_WO2.ML 
1123  2 
ID: $Id$ 
1461  3 
Author: Krzysztof Grabczewski 
1123  4 

5 
The proof of AC1 ==> WO2 

6 
*) 

7 

8 
open AC1_WO2; 

9 

2167  10 
(*Establishing the existence of a bijection  hence the need for uresult*) 
1123  11 
val [prem] = goal thy "f : (PROD X:Pow(x)  {0}. X) ==> \ 
1461  12 
\ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x){0}. {f`X}, x, i) = {x})"; 
1123  13 
by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1); 
1206  14 
by (rtac f_subsets_imp_UN_HH_eq_x 1); 
1123  15 
by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2)); 
5241  16 
by (fast_tac (claset() addSEs [equals0E] addSDs [prem RS apply_type]) 1); 
4091  17 
by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1); 
2167  18 
val lemma1 = uresult() > standard; 
1123  19 

5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset

20 
Goalw [AC1_def, WO2_def, eqpoll_def] "AC1 ==> WO2"; 
1206  21 
by (rtac allI 1); 
1123  22 
by (eres_inst_tac [("x","Pow(A){0}")] allE 1); 
4091  23 
by (fast_tac (claset() addSDs [lemma1] addSIs [Ord_Least]) 1); 
1196  24 
qed "AC1_WO2"; 