author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46953  2b6e55924af3 
child 58871  c399ae4b836f 
permissions  rwrr 
1478  1 
(* Title: ZF/AC.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

484  3 
Copyright 1994 University of Cambridge 
13328  4 
*) 
484  5 

13328  6 
header{*The Axiom of Choice*} 
484  7 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset

8 
theory AC imports Main_ZF begin 
13134  9 

13328  10 
text{*This definition comes from Halmos (1960), page 59.*} 
24893  11 
axiomatization where 
46953  12 
AC: "[ a \<in> A; !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) ] ==> \<exists>z. z \<in> Pi(A,B)" 
13134  13 

46820  14 
(*The same as AC, but no premise @{term"a \<in> A"}*) 
13134  15 
lemma AC_Pi: "[ !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) ] ==> \<exists>z. z \<in> Pi(A,B)" 
16 
apply (case_tac "A=0") 

13149
773657d466cb
better simplification of trivial existential equalities
paulson
parents:
13134
diff
changeset

17 
apply (simp add: Pi_empty1) 
13134  18 
(*The nontrivial case*) 
19 
apply (blast intro: AC) 

20 
done 

21 

22 
(*Using dtac, this has the advantage of DELETING the universal quantifier*) 

23 
lemma AC_ball_Pi: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)" 

24 
apply (rule AC_Pi) 

13269  25 
apply (erule bspec, assumption) 
13134  26 
done 
27 

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13328
diff
changeset

28 
lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi> X \<in> Pow(C){0}. X)" 
13134  29 
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) 
13269  30 
apply (erule_tac [2] exI, blast) 
13134  31 
done 
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
2469
diff
changeset

32 

13134  33 
lemma AC_func: 
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" 
13134  35 
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) 
46820  36 
prefer 2 apply (blast dest: apply_type intro: Pi_type, blast) 
13134  37 
done 
38 

39 
lemma non_empty_family: "[ 0 \<notin> A; x \<in> A ] ==> \<exists>y. y \<in> x" 

13269  40 
by (subgoal_tac "x \<noteq> 0", blast+) 
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
2469
diff
changeset

41 

46820  42 
lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A>\<Union>(A). \<forall>x \<in> A. f`x \<in> x" 
13134  43 
apply (rule AC_func) 
46820  44 
apply (simp_all add: non_empty_family) 
13134  45 
done 
46 

47 
lemma AC_func_Pow: "\<exists>f \<in> (Pow(C){0}) > C. \<forall>x \<in> Pow(C){0}. f`x \<in> x" 

48 
apply (rule AC_func0 [THEN bexE]) 

49 
apply (rule_tac [2] bexI) 

13269  50 
prefer 2 apply assumption 
51 
apply (erule_tac [2] fun_weaken_type, blast+) 

13134  52 
done 
53 

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13328
diff
changeset

54 
lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi> x \<in> A. x)" 
13134  55 
apply (rule AC_Pi) 
46820  56 
apply (simp_all add: non_empty_family) 
13134  57 
done 
58 

484  59 
end 