src/ZF/AC.thy
 author wenzelm Mon Dec 04 22:54:31 2017 +0100 (20 months ago) changeset 67131 85d10959c2e4 parent 65449 c82e63b11b8b permissions -rw-r--r--
tuned signature;
 clasohm@1478 1 (* Title: ZF/AC.thy clasohm@1478 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory lcp@484 3 Copyright 1994 University of Cambridge paulson@13328 4 *) lcp@484 5 wenzelm@60770 6 section\The Axiom of Choice\ lcp@484 7 wenzelm@65449 8 theory AC imports ZF begin paulson@13134 9 wenzelm@60770 10 text\This definition comes from Halmos (1960), page 59.\ wenzelm@24893 11 axiomatization where paulson@46953 12 AC: "[| a \ A; !!x. x \ A ==> (\y. y \ B(x)) |] ==> \z. z \ Pi(A,B)" paulson@13134 13 paulson@46820 14 (*The same as AC, but no premise @{term"a \ A"}*) paulson@13134 15 lemma AC_Pi: "[| !!x. x \ A ==> (\y. y \ B(x)) |] ==> \z. z \ Pi(A,B)" paulson@13134 16 apply (case_tac "A=0") paulson@13149 17 apply (simp add: Pi_empty1) paulson@13134 18 (*The non-trivial case*) paulson@13134 19 apply (blast intro: AC) paulson@13134 20 done paulson@13134 21 paulson@13134 22 (*Using dtac, this has the advantage of DELETING the universal quantifier*) paulson@13134 23 lemma AC_ball_Pi: "\x \ A. \y. y \ B(x) ==> \y. y \ Pi(A,B)" paulson@13134 24 apply (rule AC_Pi) paulson@13269 25 apply (erule bspec, assumption) paulson@13134 26 done paulson@13134 27 wenzelm@61980 28 lemma AC_Pi_Pow: "\f. f \ (\X \ Pow(C)-{0}. X)" paulson@13134 29 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) paulson@13269 30 apply (erule_tac [2] exI, blast) paulson@13134 31 done paulson@6053 32 paulson@13134 33 lemma AC_func: paulson@46820 34 "[| !!x. x \ A ==> (\y. y \ x) |] ==> \f \ A->\(A). \x \ A. f`x \ x" paulson@13134 35 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) paulson@46820 36 prefer 2 apply (blast dest: apply_type intro: Pi_type, blast) paulson@13134 37 done paulson@13134 38 paulson@13134 39 lemma non_empty_family: "[| 0 \ A; x \ A |] ==> \y. y \ x" paulson@13269 40 by (subgoal_tac "x \ 0", blast+) paulson@6053 41 paulson@46820 42 lemma AC_func0: "0 \ A ==> \f \ A->\(A). \x \ A. f`x \ x" paulson@13134 43 apply (rule AC_func) paulson@46820 44 apply (simp_all add: non_empty_family) paulson@13134 45 done paulson@13134 46 paulson@13134 47 lemma AC_func_Pow: "\f \ (Pow(C)-{0}) -> C. \x \ Pow(C)-{0}. f`x \ x" paulson@13134 48 apply (rule AC_func0 [THEN bexE]) paulson@13134 49 apply (rule_tac [2] bexI) paulson@13269 50 prefer 2 apply assumption paulson@13269 51 apply (erule_tac [2] fun_weaken_type, blast+) paulson@13134 52 done paulson@13134 53 wenzelm@61980 54 lemma AC_Pi0: "0 \ A ==> \f. f \ (\x \ A. x)" paulson@13134 55 apply (rule AC_Pi) paulson@46820 56 apply (simp_all add: non_empty_family) paulson@13134 57 done paulson@13134 58 lcp@484 59 end