author | wenzelm |
Fri, 03 Aug 2007 16:28:22 +0200 | |
changeset 24143 | 90a9a6fe0d01 |
parent 16417 | 9bc16273c2d4 |
child 24893 | b8ef7afe3a6b |
permissions | -rw-r--r-- |
(* Title: ZF/AC.thy ID: $Id$ 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 \<in> A*) lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> 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: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)" apply (rule AC_Pi) apply (erule bspec, assumption) done lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi> X \<in> 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 \<in> A ==> (\<exists>y. y \<in> x) |] ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> 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 \<notin> A; x \<in> A |] ==> \<exists>y. y \<in> x" by (subgoal_tac "x \<noteq> 0", blast+) lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x" apply (rule AC_func) apply (simp_all add: non_empty_family) done lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> 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 \<notin> A ==> \<exists>f. f \<in> (\<Pi> x \<in> A. x)" apply (rule AC_Pi) apply (simp_all add: non_empty_family) done end