484

1 
(* Title: ZF/AC.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
For AC.thy. The Axiom of Choice


7 
*)


8 


9 
open AC;


10 


11 
(*The same as AC, but no premise a:A*)


12 
val [nonempty] = goal AC.thy


13 
"[ !!x. x:A ==> (EX y. y:B(x)) ] ==> EX z. z : Pi(A,B)";


14 
by (excluded_middle_tac "A=0" 1);


15 
by (asm_simp_tac (ZF_ss addsimps [Pi_empty1]) 2 THEN fast_tac ZF_cs 2);


16 
(*The nontrivial case*)


17 
by (safe_tac eq_cs);


18 
by (fast_tac (ZF_cs addSIs [AC, nonempty]) 1);


19 
val AC_Pi = result();


20 


21 
(*Using dtac, this has the advantage of DELETING the universal quantifier*)


22 
goal AC.thy "!!A B. ALL x:A. EX y. y:B(x) ==> EX y. y : Pi(A,B)";


23 
by (resolve_tac [AC_Pi] 1);


24 
by (eresolve_tac [bspec] 1);


25 
by (assume_tac 1);


26 
val AC_ball_Pi = result();


27 


28 
goal AC.thy "EX f. f: (PROD X: Pow(C){0}. X)";


29 
by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);


30 
by (etac exI 2);


31 
by (fast_tac eq_cs 1);


32 
val AC_Pi_Pow = result();


33 


34 
val [nonempty] = goal AC.thy


35 
"[ !!x. x:A ==> (EX y. y:x) \


36 
\ ] ==> EX f: A>Union(A). ALL x:A. f`x : x";


37 
by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);


38 
by (etac nonempty 1);


39 
by (fast_tac (ZF_cs addDs [apply_type] addIs [Pi_type]) 1);


40 
val AC_func = result();


41 


42 
goal AC.thy "!!x A. [ 0 ~: A; x: A ] ==> EX y. y:x";


43 
by (resolve_tac [exCI] 1);


44 
by (eresolve_tac [notE] 1);


45 
by (resolve_tac [equals0I RS subst] 1);


46 
by (eresolve_tac [spec RS notE] 1 THEN REPEAT (assume_tac 1));


47 
val non_empty_family = result();


48 


49 
goal AC.thy "!!A. 0 ~: A ==> EX f: A>Union(A). ALL x:A. f`x : x";


50 
by (rtac AC_func 1);


51 
by (REPEAT (ares_tac [non_empty_family] 1));


52 
val AC_func0 = result();


53 


54 
goal AC.thy "EX f: (Pow(C){0}) > C. ALL x:(Pow(C){0}). f`x : x";


55 
by (resolve_tac [AC_func0 RS bexE] 1);


56 
by (rtac bexI 2);


57 
by (assume_tac 2);


58 
by (eresolve_tac [fun_weaken_type] 2);


59 
by (ALLGOALS (fast_tac ZF_cs));


60 
val AC_func_Pow = result();


61 
