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*)

741

17 
by (fast_tac (eq_cs addSIs [AC, nonempty]) 1);

484

18 
val AC_Pi = result();


19 


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


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


22 
by (resolve_tac [AC_Pi] 1);


23 
by (eresolve_tac [bspec] 1);


24 
by (assume_tac 1);


25 
val AC_ball_Pi = result();


26 


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


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


29 
by (etac exI 2);


30 
by (fast_tac eq_cs 1);


31 
val AC_Pi_Pow = result();


32 


33 
val [nonempty] = goal AC.thy


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


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


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


37 
by (etac nonempty 1);


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


39 
val AC_func = result();


40 

741

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


42 
by (subgoal_tac "x ~= 0" 1);


43 
by (ALLGOALS (fast_tac eq_cs));

484

44 
val non_empty_family = result();


45 


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


47 
by (rtac AC_func 1);


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


49 
val AC_func0 = result();


50 


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


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


53 
by (rtac bexI 2);


54 
by (assume_tac 2);


55 
by (eresolve_tac [fun_weaken_type] 2);


56 
by (ALLGOALS (fast_tac ZF_cs));


57 
val AC_func_Pow = result();


58 
