Theory AC

Up to index of Isabelle/ZF

theory AC
imports Main_ZF
`(*  Title:      ZF/AC.thy    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1994  University of Cambridge*)header{*The Axiom of Choice*}theory AC imports Main_ZF begintext{*This definition comes from Halmos (1960), page 59.*}axiomatization where  AC: "[| a ∈ A;  !!x. x ∈ A ==> (∃y. y ∈ B(x)) |] ==> ∃z. z ∈ Pi(A,B)"(*The same as AC, but no premise @{term"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)donelemma 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)donelemma 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)donelemma 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)donelemma 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 assumptionapply (erule_tac [2] fun_weaken_type, blast+)donelemma AC_Pi0: "0 ∉ A ==> ∃f. f ∈ (Π x ∈ A. x)"apply (rule AC_Pi)apply (simp_all add: non_empty_family)doneend`