src/ZF/AC.thy
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58871 c399ae4b836f
child 60770 240563fbf41d
permissions -rw-r--r--
proper context for match_tac etc.;
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@58871
     6
section{*The Axiom of Choice*}
lcp@484
     7
krauss@26056
     8
theory AC imports Main_ZF begin
paulson@13134
     9
paulson@13328
    10
text{*This definition comes from Halmos (1960), page 59.*}
wenzelm@24893
    11
axiomatization where
paulson@46953
    12
  AC: "[| a \<in> A;  !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
paulson@13134
    13
paulson@46820
    14
(*The same as AC, but no premise @{term"a \<in> A"}*)
paulson@13134
    15
lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> 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: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)"
paulson@13134
    24
apply (rule AC_Pi)
paulson@13269
    25
apply (erule bspec, assumption)
paulson@13134
    26
done
paulson@13134
    27
skalberg@14171
    28
lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi> X \<in> 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 \<in> A ==> (\<exists>y. y \<in> x) |] ==> \<exists>f \<in> A->\<Union>(A). \<forall>x \<in> A. f`x \<in> 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 \<notin> A;  x \<in> A |] ==> \<exists>y. y \<in> x"
paulson@13269
    40
by (subgoal_tac "x \<noteq> 0", blast+)
paulson@6053
    41
paulson@46820
    42
lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->\<Union>(A). \<forall>x \<in> A. f`x \<in> 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: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> 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
skalberg@14171
    54
lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi> x \<in> 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