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 The Axiom of Choice |
|
7 *) |
|
8 |
|
9 (*The same as AC, but no premise a \\<in> A*) |
|
10 val [nonempty] = goal (the_context ()) |
|
11 "[| !!x. x \\<in> A ==> (\\<exists>y. y \\<in> B(x)) |] ==> \\<exists>z. z \\<in> Pi(A,B)"; |
|
12 by (excluded_middle_tac "A=0" 1); |
|
13 by (asm_simp_tac (simpset() addsimps [Pi_empty1]) 2 THEN Blast_tac 2); |
|
14 (*The non-trivial case*) |
|
15 by (blast_tac (claset() addIs [AC, nonempty]) 1); |
|
16 qed "AC_Pi"; |
|
17 |
|
18 (*Using dtac, this has the advantage of DELETING the universal quantifier*) |
|
19 Goal "\\<forall>x \\<in> A. \\<exists>y. y \\<in> B(x) ==> \\<exists>y. y \\<in> Pi(A,B)"; |
|
20 by (rtac AC_Pi 1); |
|
21 by (etac bspec 1); |
|
22 by (assume_tac 1); |
|
23 qed "AC_ball_Pi"; |
|
24 |
|
25 Goal "\\<exists>f. f \\<in> (\\<Pi>X \\<in> Pow(C)-{0}. X)"; |
|
26 by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1); |
|
27 by (etac exI 2); |
|
28 by (Blast_tac 1); |
|
29 qed "AC_Pi_Pow"; |
|
30 |
|
31 val [nonempty] = goal (the_context ()) |
|
32 "[| !!x. x \\<in> A ==> (\\<exists>y. y \\<in> x) \ |
|
33 \ |] ==> \\<exists>f \\<in> A->Union(A). \\<forall>x \\<in> A. f`x \\<in> x"; |
|
34 by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1); |
|
35 by (etac nonempty 1); |
|
36 by (blast_tac (claset() addDs [apply_type] addIs [Pi_type]) 1); |
|
37 qed "AC_func"; |
|
38 |
|
39 Goal "[| 0 \\<notin> A; x \\<in> A |] ==> \\<exists>y. y \\<in> x"; |
|
40 by (subgoal_tac "x \\<noteq> 0" 1); |
|
41 by (ALLGOALS Blast_tac); |
|
42 qed "non_empty_family"; |
|
43 |
|
44 Goal "0 \\<notin> A ==> \\<exists>f \\<in> A->Union(A). \\<forall>x \\<in> A. f`x \\<in> x"; |
|
45 by (rtac AC_func 1); |
|
46 by (REPEAT (ares_tac [non_empty_family] 1)); |
|
47 qed "AC_func0"; |
|
48 |
|
49 Goal "\\<exists>f \\<in> (Pow(C)-{0}) -> C. \\<forall>x \\<in> Pow(C)-{0}. f`x \\<in> x"; |
|
50 by (resolve_tac [AC_func0 RS bexE] 1); |
|
51 by (rtac bexI 2); |
|
52 by (assume_tac 2); |
|
53 by (etac fun_weaken_type 2); |
|
54 by (ALLGOALS Blast_tac); |
|
55 qed "AC_func_Pow"; |
|
56 |
|
57 Goal "0 \\<notin> A ==> \\<exists>f. f \\<in> (\\<Pi>x \\<in> A. x)"; |
|
58 by (rtac AC_Pi 1); |
|
59 by (REPEAT (ares_tac [non_empty_family] 1)); |
|
60 qed "AC_Pi0"; |
|
61 |
|
62 (*Used in Zorn.ML*) |
|
63 Goal "[| ch \\<in> (\\<Pi>X \\<in> Pow(S) - {0}. X); X \\<subseteq> S; X\\<noteq>S |] ==> ch ` (S-X) \\<in> S-X"; |
|
64 by (etac apply_type 1); |
|
65 by (blast_tac (claset() addSEs [equalityE]) 1); |
|
66 qed "choice_Diff"; |
|
67 |
|