Quelle Cardinal_AC.thy Sprache: Isabelle

(*  Title:      ZF/Cardinal_AC.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

These results help justify infinite-branching datatypes
*)

section\<open>Cardinal Arithmetic Using AC\<close>

theory Cardinal_AC imports CardinalArith Zorn begin

subsection\<open>Strengthened Forms of Existing Theorems on Cardinals\<close>

lemma cardinal_eqpoll: "|A| \ A"
apply (rule AC_well_ord [THEN exE])
apply (erule well_ord_cardinal_eqpoll)
done

text\<open>The theorem \<^term>\<open>||A|| = |A|\<close>\<close>
lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp]

lemma cardinal_eqE: "|X| = |Y| \ X \ Y"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule well_ord_cardinal_eqE, assumption+)
done

lemma cardinal_eqpoll_iff: "|X| = |Y| \ X \ Y"
by (blast intro: cardinal_cong cardinal_eqE)

lemma cardinal_disjoint_Un:
     "\|A|=|B|; |C|=|D|; A \ C = 0; B \ D = 0\
      \<Longrightarrow> |A \<union> C| = |B \<union> D|"
by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)

lemma lepoll_imp_cardinal_le: "A \ B \ |A| \ |B|"
apply (rule AC_well_ord [THEN exE])
apply (erule well_ord_lepoll_imp_cardinal_le, assumption)
done

lemma cadd_assoc: "(i \ j) \ k = i \ (j \ k)"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule well_ord_cadd_assoc, assumption+)
done

lemma cmult_assoc: "(i \ j) \ k = i \ (j \ k)"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule well_ord_cmult_assoc, assumption+)
done

lemma cadd_cmult_distrib: "(i \ j) \ k = (i \ k) \ (j \ k)"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule well_ord_cadd_cmult_distrib, assumption+)
done

lemma InfCard_square_eq: "InfCard(|A|) \ A*A \ A"
apply (rule AC_well_ord [THEN exE])
apply (erule well_ord_InfCard_square_eq, assumption)
done

subsection \<open>The relationship between cardinality and le-pollence\<close>

lemma Card_le_imp_lepoll:
  assumes "|A| \ |B|" shows "A \ B"
proof -
  have "A \ |A|"
    by (rule cardinal_eqpoll [THEN eqpoll_sym])
  also have "... \ |B|"
    by (rule le_imp_subset [THEN subset_imp_lepoll]) (rule assms)
  also have "... \ B"
    by (rule cardinal_eqpoll)
  finally show ?thesis .
qed

lemma le_Card_iff: "Card(K) \ |A| \ K \ A \ K"
apply (erule Card_cardinal_eq [THEN subst], rule iffI,
       erule Card_le_imp_lepoll)
apply (erule lepoll_imp_cardinal_le)
done

lemma cardinal_0_iff_0 [simp]: "|A| = 0 \ A = 0"
apply auto
apply (drule cardinal_0 [THEN ssubst])
apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
done

lemma cardinal_lt_iff_lesspoll:
  assumes i: "Ord(i)" shows "i < |A| \ i \ A"
proof
  assume "i < |A|"
  hence  "i \ |A|"
    by (blast intro: lt_Card_imp_lesspoll Card_cardinal)
  also have "... \ A"
    by (rule cardinal_eqpoll)
  finally show "i \ A" .
next
  assume "i \ A"
  also have "... \ |A|"
    by (blast intro: cardinal_eqpoll eqpoll_sym)
  finally have "i \ |A|" .
  thus  "i < |A|" using i
    by (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt)
qed

lemma cardinal_le_imp_lepoll: " i \ |A| \ i \ A"
  by (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)

subsection\<open>Other Applications of AC\<close>

lemma surj_implies_inj:
  assumes f: "f \ surj(X,Y)" shows "\g. g \ inj(Y,X)"
proof -
  from f AC_Pi [of Y "\y. f-``{y}"]
  obtain z where z: "z \ (\y\Y. f -`` {y})"
    by (auto simp add: surj_def) (fast dest: apply_Pair)
  show ?thesis
    proof
      show "z \ inj(Y, X)" using z surj_is_fun [OF f]
        by (blast dest: apply_type Pi_memberD
                  intro: apply_equality Pi_type f_imp_injective)
    qed
qed

text\<open>Kunen's Lemma 10.20\<close>
lemma surj_implies_cardinal_le:
  assumes f: "f \ surj(X,Y)" shows "|Y| \ |X|"
proof (rule lepoll_imp_cardinal_le)
  from f [THEN surj_implies_inj] obtain g where "g \ inj(Y,X)" ..
  thus "Y \ X"
    by (auto simp add: lepoll_def)
qed

text\<open>Kunen's Lemma 10.21\<close>
lemma cardinal_UN_le:
  assumes K: "InfCard(K)"
  shows "(\i. i\K \ |X(i)| \ K) \ |\i\K. X(i)| \ K"
proof (simp add: K InfCard_is_Card le_Card_iff)
  have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K)
  assume "\i. i\K \ X(i) \ K"
  hence "\i. i\K \ \f. f \ inj(X(i), K)" by (simp add: lepoll_def)
  with AC_Pi obtain f where f: "f \ (\i\K. inj(X(i), K))"
    by force
  { fix z
    assume z: "z \ (\i\K. X(i))"
    then obtain i where i: "i \ K" "Ord(i)" "z \ X(i)"
      by (blast intro: Ord_in_Ord [of K])
    hence "(\ i. z \ X(i)) \ i" by (fast intro: Least_le)
    hence "(\ i. z \ X(i)) < K" by (best intro: lt_trans1 ltI i)
    hence "(\ i. z \ X(i)) \ K" and "z \ X(\ i. z \ X(i))"
      by (auto intro: LeastI ltD i)
  } note mems = this
  have "(\i\K. X(i)) \ K \ K"
    proof (unfold lepoll_def)
      show "\f. f \ inj(\RepFun(K, X), K \ K)"
        apply (rule exI)
        apply (rule_tac c = "\z. \\ i. z \ X(i), f ` (\ i. z \ X(i)) ` z\"
                    and d = "\\i,j\. converse (f`i) ` j" in lam_injective)
        apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
        done
    qed
  also have "... \ K"
    by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq)
  finally show "(\i\K. X(i)) \ K" .
qed

text\<open>The same again, using \<^term>\<open>csucc\<close>\<close>
lemma cardinal_UN_lt_csucc:
     "\InfCard(K); \i. i\K \ |X(i)| < csucc(K)\
      \<Longrightarrow> |\<Union>i\<in>K. X(i)| < csucc(K)"
by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)

text\<open>The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
  the least ordinal j such that i:Vfrom(A,j).\<close>
lemma cardinal_UN_Ord_lt_csucc:
     "\InfCard(K); \i. i\K \ j(i) < csucc(K)\
      \<Longrightarrow> (\<Union>i\<in>K. j(i)) < csucc(K)"
apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
apply (blast intro!: Ord_UN elim: ltE)
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])
done

subsection\<open>The Main Result for Infinite-Branching Datatypes\<close>

text\<open>As above, but the index set need not be a cardinal. Work
backwards along the injection from \<^term>\<open>W\<close> into \<^term>\<open>K\<close>, given
that \<^term>\<open>W\<noteq>0\<close>.\<close>

lemma inj_UN_subset:
  assumes f: "f \ inj(A,B)" and a: "a \ A"
  shows "(\x\A. C(x)) \ (\y\B. C(if y \ range(f) then converse(f)`y else a))"
proof (rule UN_least)
  fix x
  assume x: "x \ A"
  hence fx: "f ` x \ B" by (blast intro: f inj_is_fun [THEN apply_type])
  have "C(x) \ C(if f ` x \ range(f) then converse(f) ` (f ` x) else a)"
    using f x by (simp add: inj_is_fun [THEN apply_rangeI])
  also have "... \ (\y\B. C(if y \ range(f) then converse(f) ` y else a))"
    by (rule UN_upper [OF fx])
  finally show "C(x) \ (\y\B. C(if y \ range(f) then converse(f)`y else a))" .
qed

theorem le_UN_Ord_lt_csucc:
  assumes IK: "InfCard(K)" and WK: "|W| \ K" and j: "\w. w\W \ j(w) < csucc(K)"
  shows "(\w\W. j(w)) < csucc(K)"
proof -
  have CK: "Card(K)"
    by (simp add: InfCard_is_Card IK)
  then obtain f where f: "f \ inj(W, K)" using WK
    by(auto simp add: le_Card_iff lepoll_def)
  have OU: "Ord(\w\W. j(w))" using j
    by (blast elim: ltE)
  note lt_subset_trans [OF _ _ OU, trans]
  show ?thesis
    proof (cases "W=0")
      case True  \<comment> \<open>solve the easy 0 case\<close>
      thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc)
    next
      case False
        then obtain x where x: "x \ W" by blast
        have "(\x\W. j(x)) \ (\k\K. j(if k \ range(f) then converse(f) ` k else x))"
          by (rule inj_UN_subset [OF f x])
        also have "... < csucc(K)" using IK
          proof (rule cardinal_UN_Ord_lt_csucc)
            fix k
            assume "k \ K"
            thus "j(if k \ range(f) then converse(f) ` k else x) < csucc(K)" using f x j
              by (simp add: inj_converse_fun [THEN apply_type])
          qed
        finally show ?thesis .
    qed
qed

end

quality95%

¤ Dauer der Verarbeitung: 0.2 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.