(* Title: ZF/AC.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)
section\<open>The Axiom of Choice\<close>
theory AC imports ZF begin
text\<open>This definition comes from Halmos (1960), page 59.\<close>
axiomatization where
AC: "[| a \ A; !!x. x \ A ==> (\y. y \ B(x)) |] ==> \z. z \ Pi(A,B)"
(*The same as AC, but no premise @{term"a \<in> A"}*)
lemma AC_Pi: "[| !!x. x \ A ==> (\y. y \ B(x)) |] ==> \z. z \ Pi(A,B)"
apply (case_tac "A=0")
apply (simp add: Pi_empty1)
(*The non-trivial case*)
apply (blast intro: AC)
done
(*Using dtac, this has the advantage of DELETING the universal quantifier*)
lemma AC_ball_Pi: "\x \ A. \y. y \ B(x) ==> \y. y \ Pi(A,B)"
apply (rule AC_Pi)
apply (erule bspec, assumption)
done
lemma AC_Pi_Pow: "\f. f \ (\X \ Pow(C)-{0}. X)"
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
apply (erule_tac [2] exI, blast)
done
lemma AC_func:
"[| !!x. x \ A ==> (\y. y \ x) |] ==> \f \ A->\(A). \x \ A. f`x \ x"
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
prefer 2 apply (blast dest: apply_type intro: Pi_type, blast)
done
lemma non_empty_family: "[| 0 \ A; x \ A |] ==> \y. y \ x"
by (subgoal_tac "x \ 0", blast+)
lemma AC_func0: "0 \ A ==> \f \ A->\(A). \x \ A. f`x \ x"
apply (rule AC_func)
apply (simp_all add: non_empty_family)
done
lemma AC_func_Pow: "\f \ (Pow(C)-{0}) -> C. \x \ Pow(C)-{0}. f`x \ x"
apply (rule AC_func0 [THEN bexE])
apply (rule_tac [2] bexI)
prefer 2 apply assumption
apply (erule_tac [2] fun_weaken_type, blast+)
done
lemma AC_Pi0: "0 \ A ==> \f. f \ (\x \ A. x)"
apply (rule AC_Pi)
apply (simp_all add: non_empty_family)
done
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|