author  paulson 
Wed, 15 May 2002 10:42:32 +0200  
changeset 13149  773657d466cb 
parent 13134  bf37a3049251 
child 13269  3ba9be497c33 
permissions  rwrr 
1478  1 
(* Title: ZF/AC.thy 
484  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
484  4 
Copyright 1994 University of Cambridge 
5 

6 
The Axiom of Choice 

7 

8 
This definition comes from Halmos (1960), page 59. 

9 
*) 

10 

13134  11 
theory AC = Main: 
12 

13 
axioms AC: "[ a: A; !!x. x:A ==> (EX y. y:B(x)) ] ==> EX z. z : Pi(A,B)" 

14 

15 
(*The same as AC, but no premise a \<in> A*) 

16 
lemma AC_Pi: "[ !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) ] ==> \<exists>z. z \<in> Pi(A,B)" 

17 
apply (case_tac "A=0") 

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

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

21 
done 

22 

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

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

25 
apply (rule AC_Pi) 

26 
apply (erule bspec) 

27 
apply assumption 

28 
done 

29 

30 
lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi>X \<in> Pow(C){0}. X)" 

31 
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) 

32 
apply (erule_tac [2] exI) 

33 
apply blast 

34 
done 

6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
2469
diff
changeset

35 

13134  36 
lemma AC_func: 
37 
"[ !!x. x \<in> A ==> (\<exists>y. y \<in> x) ] ==> \<exists>f \<in> A>Union(A). \<forall>x \<in> A. f`x \<in> x" 

38 
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) 

39 
prefer 2 apply (blast dest: apply_type intro: Pi_type) 

40 
apply (blast intro: elim:); 

41 
done 

42 

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

44 
apply (subgoal_tac "x \<noteq> 0") 

45 
apply blast+ 

46 
done 

6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
2469
diff
changeset

47 

13134  48 
lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A>Union(A). \<forall>x \<in> A. f`x \<in> x" 
49 
apply (rule AC_func) 

50 
apply (simp_all add: non_empty_family) 

51 
done 

52 

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

54 
apply (rule AC_func0 [THEN bexE]) 

55 
apply (rule_tac [2] bexI) 

56 
prefer 2 apply (assumption) 

57 
apply (erule_tac [2] fun_weaken_type) 

58 
apply blast+ 

59 
done 

60 

61 
lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi>x \<in> A. x)" 

62 
apply (rule AC_Pi) 

63 
apply (simp_all add: non_empty_family) 

64 
done 

65 

484  66 
end 