Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: signature-enveloping-rsa.xml Sprache: Isabelle

Original von: 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

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.