Quelle Hartog.thy Sprache: Isabelle

(*  Title:      ZF/AC/Hartog.thy
    Author:     Krzysztof Grabczewski

Hartog's function.
*)

theory Hartog
imports AC_Equiv
begin

definition
  Hartog :: "i \ i" where
   "Hartog(X) \ \ i. \ i \ X"

lemma Ords_in_set: "\a. Ord(a) \ a \ X \ P"
apply (rule_tac X = "{y \ X. Ord (y) }" in ON_class [elim_format])
apply fast
done

lemma Ord_lepoll_imp_ex_well_ord:
     "\Ord(a); a \ X\
      \<Longrightarrow> \<exists>Y. Y \<subseteq> X \<and> (\<exists>R. well_ord(Y,R) \<and> ordertype(Y,R)=a)"
  unfolding lepoll_def
apply (erule exE)
apply (intro exI conjI)
  apply (erule inj_is_fun [THEN fun_is_rel, THEN image_subset])
apply (rule well_ord_rvimage [OF bij_is_inj well_ord_Memrel])
  apply (erule restrict_bij [THEN bij_converse_bij])
apply (rule subset_refl, assumption)
apply (rule trans)
apply (rule bij_ordertype_vimage)
apply (erule restrict_bij [THEN bij_converse_bij])
apply (rule subset_refl)
apply (erule well_ord_Memrel)
apply (erule ordertype_Memrel)
done

lemma Ord_lepoll_imp_eq_ordertype:
     "\Ord(a); a \ X\ \ \Y. Y \ X \ (\R. R \ X*X \ ordertype(Y,R)=a)"
apply (drule Ord_lepoll_imp_ex_well_ord, assumption, clarify)
apply (intro exI conjI)
apply (erule_tac [3] ordertype_Int, auto)
done

lemma Ords_lepoll_set_lemma:
     "(\a. Ord(a) \ a \ X) \
       \<forall>a. Ord(a) \<longrightarrow>
        a \<in> {b. Z \<in> Pow(X)*Pow(X*X), \<exists>Y R. Z=\<langle>Y,R\<rangle> \<and> ordertype(Y,R)=b}"
apply (intro allI impI)
apply (elim allE impE, assumption)
apply (blast dest!: Ord_lepoll_imp_eq_ordertype intro: sym)
done

lemma Ords_lepoll_set: "\a. Ord(a) \ a \ X \ P"
by (erule Ords_lepoll_set_lemma [THEN Ords_in_set])

lemma ex_Ord_not_lepoll: "\a. Ord(a) \ \a \ X"
apply (rule ccontr)
apply (best intro: Ords_lepoll_set)
done

lemma not_Hartog_lepoll_self: "\ Hartog(A) \ A"
  unfolding Hartog_def
apply (rule ex_Ord_not_lepoll [THEN exE])
apply (rule LeastI, auto)
done

lemmas Hartog_lepoll_selfE = not_Hartog_lepoll_self [THEN notE]

lemma Ord_Hartog: "Ord(Hartog(A))"
by (unfold Hartog_def, rule Ord_Least)

lemma less_HartogE1: "\i < Hartog(A); \ i \ A\ \ P"
by (unfold Hartog_def, fast elim: less_LeastE)

lemma less_HartogE: "\i < Hartog(A); i \ Hartog(A)\ \ P"
by (blast intro: less_HartogE1 eqpoll_sym eqpoll_imp_lepoll
                 lepoll_trans [THEN Hartog_lepoll_selfE])

lemma Card_Hartog: "Card(Hartog(A))"
by (fast intro!: CardI Ord_Hartog elim: less_HartogE)

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.