src/ZF/AC.thy
author paulson
Wed May 15 10:42:32 2002 +0200 (2002-05-15)
changeset 13149 773657d466cb
parent 13134 bf37a3049251
child 13269 3ba9be497c33
permissions -rw-r--r--
better simplification of trivial existential equalities
clasohm@1478
     1
(*  Title:      ZF/AC.thy
lcp@484
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@484
     4
    Copyright   1994  University of Cambridge
lcp@484
     5
lcp@484
     6
The Axiom of Choice
lcp@484
     7
lcp@484
     8
This definition comes from Halmos (1960), page 59.
lcp@484
     9
*)
lcp@484
    10
paulson@13134
    11
theory AC = Main:
paulson@13134
    12
paulson@13134
    13
axioms AC: "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
paulson@13134
    14
paulson@13134
    15
(*The same as AC, but no premise a \<in> A*)
paulson@13134
    16
lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
paulson@13134
    17
apply (case_tac "A=0")
paulson@13149
    18
apply (simp add: Pi_empty1)
paulson@13134
    19
(*The non-trivial case*)
paulson@13134
    20
apply (blast intro: AC)
paulson@13134
    21
done
paulson@13134
    22
paulson@13134
    23
(*Using dtac, this has the advantage of DELETING the universal quantifier*)
paulson@13134
    24
lemma AC_ball_Pi: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)"
paulson@13134
    25
apply (rule AC_Pi)
paulson@13134
    26
apply (erule bspec)
paulson@13134
    27
apply assumption
paulson@13134
    28
done
paulson@13134
    29
paulson@13134
    30
lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi>X \<in> Pow(C)-{0}. X)"
paulson@13134
    31
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
paulson@13134
    32
apply (erule_tac [2] exI)
paulson@13134
    33
apply blast
paulson@13134
    34
done
paulson@6053
    35
paulson@13134
    36
lemma AC_func:
paulson@13134
    37
     "[| !!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
    38
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
paulson@13134
    39
prefer 2 apply (blast dest: apply_type intro: Pi_type)
paulson@13134
    40
apply (blast intro: elim:); 
paulson@13134
    41
done
paulson@13134
    42
paulson@13134
    43
lemma non_empty_family: "[| 0 \<notin> A;  x \<in> A |] ==> \<exists>y. y \<in> x"
paulson@13134
    44
apply (subgoal_tac "x \<noteq> 0")
paulson@13134
    45
apply blast+
paulson@13134
    46
done
paulson@6053
    47
paulson@13134
    48
lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
paulson@13134
    49
apply (rule AC_func)
paulson@13134
    50
apply (simp_all add: non_empty_family) 
paulson@13134
    51
done
paulson@13134
    52
paulson@13134
    53
lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> x"
paulson@13134
    54
apply (rule AC_func0 [THEN bexE])
paulson@13134
    55
apply (rule_tac [2] bexI)
paulson@13134
    56
prefer 2 apply (assumption)
paulson@13134
    57
apply (erule_tac [2] fun_weaken_type)
paulson@13134
    58
apply blast+
paulson@13134
    59
done
paulson@13134
    60
paulson@13134
    61
lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi>x \<in> A. x)"
paulson@13134
    62
apply (rule AC_Pi)
paulson@13134
    63
apply (simp_all add: non_empty_family) 
paulson@13134
    64
done
paulson@13134
    65
lcp@484
    66
end