author | obua |
Thu, 16 Feb 2006 04:17:19 +0100 | |
changeset 19067 | c0321d7d6b3d |
parent 16417 | 9bc16273c2d4 |
child 24893 | b8ef7afe3a6b |
permissions | -rw-r--r-- |
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 |
||
13328 | 6 |
*) |
484 | 7 |
|
13328 | 8 |
header{*The Axiom of Choice*} |
484 | 9 |
|
16417 | 10 |
theory AC imports Main begin |
13134 | 11 |
|
13328 | 12 |
text{*This definition comes from Halmos (1960), page 59.*} |
13134 | 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 non-trivial 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) |
|
13269 | 26 |
apply (erule bspec, assumption) |
13134 | 27 |
done |
28 |
||
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13328
diff
changeset
|
29 |
lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi> X \<in> Pow(C)-{0}. X)" |
13134 | 30 |
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) |
13269 | 31 |
apply (erule_tac [2] exI, blast) |
13134 | 32 |
done |
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
2469
diff
changeset
|
33 |
|
13134 | 34 |
lemma AC_func: |
35 |
"[| !!x. x \<in> A ==> (\<exists>y. y \<in> x) |] ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x" |
|
36 |
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE]) |
|
13269 | 37 |
prefer 2 apply (blast dest: apply_type intro: Pi_type, blast) |
13134 | 38 |
done |
39 |
||
40 |
lemma non_empty_family: "[| 0 \<notin> A; x \<in> A |] ==> \<exists>y. y \<in> x" |
|
13269 | 41 |
by (subgoal_tac "x \<noteq> 0", blast+) |
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
2469
diff
changeset
|
42 |
|
13134 | 43 |
lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x" |
44 |
apply (rule AC_func) |
|
45 |
apply (simp_all add: non_empty_family) |
|
46 |
done |
|
47 |
||
48 |
lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> x" |
|
49 |
apply (rule AC_func0 [THEN bexE]) |
|
50 |
apply (rule_tac [2] bexI) |
|
13269 | 51 |
prefer 2 apply assumption |
52 |
apply (erule_tac [2] fun_weaken_type, blast+) |
|
13134 | 53 |
done |
54 |
||
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13328
diff
changeset
|
55 |
lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi> x \<in> A. x)" |
13134 | 56 |
apply (rule AC_Pi) |
57 |
apply (simp_all add: non_empty_family) |
|
58 |
done |
|
59 |
||
484 | 60 |
end |