7 |
7 |
8 theory AC imports Main_ZF begin |
8 theory AC imports Main_ZF begin |
9 |
9 |
10 text{*This definition comes from Halmos (1960), page 59.*} |
10 text{*This definition comes from Halmos (1960), page 59.*} |
11 axiomatization where |
11 axiomatization where |
12 AC: "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)" |
12 AC: "[| a: A; !!x. x:A ==> (\<exists>y. y:B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)" |
13 |
13 |
14 (*The same as AC, but no premise a \<in> A*) |
14 (*The same as AC, but no premise @{term"a \<in> A"}*) |
15 lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)" |
15 lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)" |
16 apply (case_tac "A=0") |
16 apply (case_tac "A=0") |
17 apply (simp add: Pi_empty1) |
17 apply (simp add: Pi_empty1) |
18 (*The non-trivial case*) |
18 (*The non-trivial case*) |
19 apply (blast intro: AC) |
19 apply (blast intro: AC) |
29 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) |
29 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) |
30 apply (erule_tac [2] exI, blast) |
30 apply (erule_tac [2] exI, blast) |
31 done |
31 done |
32 |
32 |
33 lemma AC_func: |
33 lemma AC_func: |
34 "[| !!x. x \<in> A ==> (\<exists>y. y \<in> x) |] ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x" |
34 "[| !!x. x \<in> A ==> (\<exists>y. y \<in> x) |] ==> \<exists>f \<in> A->\<Union>(A). \<forall>x \<in> A. f`x \<in> x" |
35 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) |
35 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) |
36 prefer 2 apply (blast dest: apply_type intro: Pi_type, blast) |
36 prefer 2 apply (blast dest: apply_type intro: Pi_type, blast) |
37 done |
37 done |
38 |
38 |
39 lemma non_empty_family: "[| 0 \<notin> A; x \<in> A |] ==> \<exists>y. y \<in> x" |
39 lemma non_empty_family: "[| 0 \<notin> A; x \<in> A |] ==> \<exists>y. y \<in> x" |
40 by (subgoal_tac "x \<noteq> 0", blast+) |
40 by (subgoal_tac "x \<noteq> 0", blast+) |
41 |
41 |
42 lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x" |
42 lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->\<Union>(A). \<forall>x \<in> A. f`x \<in> x" |
43 apply (rule AC_func) |
43 apply (rule AC_func) |
44 apply (simp_all add: non_empty_family) |
44 apply (simp_all add: non_empty_family) |
45 done |
45 done |
46 |
46 |
47 lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> x" |
47 lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> x" |
48 apply (rule AC_func0 [THEN bexE]) |
48 apply (rule AC_func0 [THEN bexE]) |
49 apply (rule_tac [2] bexI) |
49 apply (rule_tac [2] bexI) |