src/ZF/AC.thy
 author wenzelm Tue Jul 31 19:40:22 2007 +0200 (2007-07-31) changeset 24091 109f19a13872 parent 16417 9bc16273c2d4 child 24893 b8ef7afe3a6b permissions -rw-r--r--
```     1 (*  Title:      ZF/AC.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1994  University of Cambridge
```
```     5
```
```     6 *)
```
```     7
```
```     8 header{*The Axiom of Choice*}
```
```     9
```
```    10 theory AC imports Main begin
```
```    11
```
```    12 text{*This definition comes from Halmos (1960), page 59.*}
```
```    13 axioms AC: "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
```
```    14
```
```    15 (*The same as AC, but no premise a \<in> A*)
```
```    16 lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
```
```    17 apply (case_tac "A=0")
```
```    18 apply (simp add: Pi_empty1)
```
```    19 (*The non-trivial case*)
```
```    20 apply (blast intro: AC)
```
```    21 done
```
```    22
```
```    23 (*Using dtac, this has the advantage of DELETING the universal quantifier*)
```
```    24 lemma AC_ball_Pi: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)"
```
```    25 apply (rule AC_Pi)
```
```    26 apply (erule bspec, assumption)
```
```    27 done
```
```    28
```
```    29 lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi> X \<in> Pow(C)-{0}. X)"
```
```    30 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
```
```    31 apply (erule_tac [2] exI, blast)
```
```    32 done
```
```    33
```
```    34 lemma AC_func:
```
```    35      "[| !!x. x \<in> A ==> (\<exists>y. y \<in> x) |] ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
```
```    36 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
```
```    37 prefer 2 apply (blast dest: apply_type intro: Pi_type, blast)
```
```    38 done
```
```    39
```
```    40 lemma non_empty_family: "[| 0 \<notin> A;  x \<in> A |] ==> \<exists>y. y \<in> x"
```
```    41 by (subgoal_tac "x \<noteq> 0", blast+)
```
```    42
```
```    43 lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
```
```    44 apply (rule AC_func)
```
```    45 apply (simp_all add: non_empty_family)
```
```    46 done
```
```    47
```
```    48 lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> x"
```
```    49 apply (rule AC_func0 [THEN bexE])
```
```    50 apply (rule_tac [2] bexI)
```
```    51 prefer 2 apply assumption
```
```    52 apply (erule_tac [2] fun_weaken_type, blast+)
```
```    53 done
```
```    54
```
```    55 lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi> x \<in> A. x)"
```
```    56 apply (rule AC_Pi)
```
```    57 apply (simp_all add: non_empty_family)
```
```    58 done
```
```    59
```
```    60 end
```