author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2469  b50b8c0eec01 
permissions  rwrr 
1461  1 
(* Title: ZF/AC.ML 
484  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
484  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*) 

1074
d60f203eeddf
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
760
diff
changeset

17 
by (fast_tac (eq_cs addIs [AC, nonempty]) 1); 
760  18 
qed "AC_Pi"; 
484  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)"; 

1461  22 
by (rtac AC_Pi 1); 
23 
by (etac bspec 1); 

484  24 
by (assume_tac 1); 
760  25 
qed "AC_ball_Pi"; 
484  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); 

760  31 
qed "AC_Pi_Pow"; 
484  32 

33 
val [nonempty] = goal AC.thy 

1461  34 
"[ !!x. x:A ==> (EX y. y:x) \ 
484  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); 

760  39 
qed "AC_func"; 
484  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)); 

760  44 
qed "non_empty_family"; 
484  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)); 

760  49 
qed "AC_func0"; 
484  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); 

1461  55 
by (etac fun_weaken_type 2); 
484  56 
by (ALLGOALS (fast_tac ZF_cs)); 
760  57 
qed "AC_func_Pow"; 
484  58 

1074
d60f203eeddf
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
760
diff
changeset

59 
goal AC.thy "!!A. 0 ~: A ==> EX f. f: (PROD x:A. x)"; 
d60f203eeddf
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
760
diff
changeset

60 
by (rtac AC_Pi 1); 
d60f203eeddf
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
760
diff
changeset

61 
by (REPEAT (ares_tac [non_empty_family] 1)); 
d60f203eeddf
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
760
diff
changeset

62 
qed "AC_Pi0"; 
d60f203eeddf
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
760
diff
changeset

63 