src/ZF/AC.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46953 2b6e55924af3
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 484
diff changeset
     1
(*  Title:      ZF/AC.thy
2b8c2a7547ab expanded tabs
clasohm
parents: 484
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     3
    Copyright   1994  University of Cambridge
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     4
*)
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     5
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     6
header{*The Axiom of Choice*}
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     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
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
     9
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
    10
text{*This definition comes from Halmos (1960), page 59.*}
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    11
axiomatization where
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
    12
  AC: "[| a \<in> A;  !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    13
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    14
(*The same as AC, but no premise @{term"a \<in> A"}*)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    15
lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    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
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    18
(*The non-trivial case*)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    19
apply (blast intro: AC)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    20
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    21
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    22
(*Using dtac, this has the advantage of DELETING the universal quantifier*)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    23
lemma AC_ball_Pi: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)"
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    24
apply (rule AC_Pi)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13149
diff changeset
    25
apply (erule bspec, assumption)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    26
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    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
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    29
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13149
diff changeset
    30
apply (erule_tac [2] exI, blast)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    31
done
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 2469
diff changeset
    32
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    33
lemma AC_func:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    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
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    35
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    36
prefer 2 apply (blast dest: apply_type intro: Pi_type, blast)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    37
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    38
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    39
lemma non_empty_family: "[| 0 \<notin> A;  x \<in> A |] ==> \<exists>y. y \<in> x"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13149
diff changeset
    40
by (subgoal_tac "x \<noteq> 0", blast+)
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 2469
diff changeset
    41
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    42
lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->\<Union>(A). \<forall>x \<in> A. f`x \<in> x"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    43
apply (rule AC_func)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    44
apply (simp_all add: non_empty_family)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    45
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    46
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    47
lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> x"
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    48
apply (rule AC_func0 [THEN bexE])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    49
apply (rule_tac [2] bexI)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13149
diff changeset
    50
prefer 2 apply assumption
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13149
diff changeset
    51
apply (erule_tac [2] fun_weaken_type, blast+)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    52
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    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
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    55
apply (rule AC_Pi)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    56
apply (simp_all add: non_empty_family)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    57
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    58
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    59
end