(* Title: ZF/AC.thy ID: $Id: AC.thy,v 1.10 2005/06/17 14:15:09 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge *) header{*The Axiom of Choice*} theory AC imports Main begin text{*This definition comes from Halmos (1960), page 59.*} axioms AC: "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)" (*The same as AC, but no premise a ∈ A*) lemma AC_Pi: "[| !!x. x ∈ A ==> (∃y. y ∈ B(x)) |] ==> ∃z. z ∈ Pi(A,B)" apply (case_tac "A=0") apply (simp add: Pi_empty1) (*The non-trivial case*) apply (blast intro: AC) done (*Using dtac, this has the advantage of DELETING the universal quantifier*) lemma AC_ball_Pi: "∀x ∈ A. ∃y. y ∈ B(x) ==> ∃y. y ∈ Pi(A,B)" apply (rule AC_Pi) apply (erule bspec, assumption) done lemma AC_Pi_Pow: "∃f. f ∈ (Π X ∈ Pow(C)-{0}. X)" apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) apply (erule_tac [2] exI, blast) done lemma AC_func: "[| !!x. x ∈ A ==> (∃y. y ∈ x) |] ==> ∃f ∈ A->Union(A). ∀x ∈ A. f`x ∈ x" apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) prefer 2 apply (blast dest: apply_type intro: Pi_type, blast) done lemma non_empty_family: "[| 0 ∉ A; x ∈ A |] ==> ∃y. y ∈ x" by (subgoal_tac "x ≠ 0", blast+) lemma AC_func0: "0 ∉ A ==> ∃f ∈ A->Union(A). ∀x ∈ A. f`x ∈ x" apply (rule AC_func) apply (simp_all add: non_empty_family) done lemma AC_func_Pow: "∃f ∈ (Pow(C)-{0}) -> C. ∀x ∈ Pow(C)-{0}. f`x ∈ x" apply (rule AC_func0 [THEN bexE]) apply (rule_tac [2] bexI) prefer 2 apply assumption apply (erule_tac [2] fun_weaken_type, blast+) done lemma AC_Pi0: "0 ∉ A ==> ∃f. f ∈ (Π x ∈ A. x)" apply (rule AC_Pi) apply (simp_all add: non_empty_family) done end
lemma AC_Pi:
(!!x. x ∈ A ==> ∃y. y ∈ B(x)) ==> ∃z. z ∈ Pi(A, B)
lemma AC_ball_Pi:
∀x∈A. ∃y. y ∈ B(x) ==> ∃y. y ∈ Pi(A, B)
lemma AC_Pi_Pow:
∃f. f ∈ (ΠX∈Pow(C) - {0}. X)
lemma AC_func:
(!!x. x ∈ A ==> ∃y. y ∈ x) ==> ∃f∈A -> \<Union>A. ∀x∈A. f ` x ∈ x
lemma non_empty_family:
[| 0 ∉ A; x ∈ A |] ==> ∃y. y ∈ x
lemma AC_func0:
0 ∉ A ==> ∃f∈A -> \<Union>A. ∀x∈A. f ` x ∈ x
lemma AC_func_Pow:
∃f∈Pow(C) - {0} -> C. ∀x∈Pow(C) - {0}. f ` x ∈ x
lemma AC_Pi0:
0 ∉ A ==> ∃f. f ∈ (Πx∈A. x)