Quelle AC.thy Sprache: Isabelle

(*  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

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.