Theory AC

(*  Title:      ZF/AC.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge
*)

sectionThe Axiom of Choice

theory AC imports ZF begin

textThis 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)
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->(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->(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