Theory Cardinal_AC

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

sectionCardinal Arithmetic Using AC

theory Cardinal_AC imports CardinalArith Zorn begin

subsectionStrengthened Forms of Existing Theorems on Cardinals

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

textThe theorem term||A|| = |A|
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
       |A  C| = |B  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 The relationship between cardinality and le-pollence

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)


subsectionOther Applications of AC

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  (yY. 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

textKunen's Lemma 10.20
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

textKunen's Lemma 10.21
lemma cardinal_UN_le:
  assumes K: "InfCard(K)" 
  shows "(i. iK  |X(i)|  K)  |iK. 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. iK  X(i)  K"
  hence "i. iK  f. f  inj(X(i), K)" by (simp add: lepoll_def) 
  with AC_Pi obtain f where f: "f  (iK. inj(X(i), K))"
    by force 
  { fix z
    assume z: "z  (iK. 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 "(iK. 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 "(iK. X(i))  K" .
qed

textThe same again, using termcsucc
lemma cardinal_UN_lt_csucc:
     "InfCard(K);  i. iK  |X(i)| < csucc(K)
       |iK. X(i)| < csucc(K)"
by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)

textThe 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).
lemma cardinal_UN_Ord_lt_csucc:
     "InfCard(K);  i. iK  j(i) < csucc(K)
       (iK. 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


subsectionThe Main Result for Infinite-Branching Datatypes

textAs above, but the index set need not be a cardinal. Work
backwards along the injection from termW into termK, given
that termW0.

lemma inj_UN_subset:
  assumes f: "f  inj(A,B)" and a: "a  A"
  shows "(xA. C(x))  (yB. 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 "...  (yB. C(if y  range(f) then converse(f) ` y else a))"
    by (rule UN_upper [OF fx]) 
  finally show "C(x)  (yB. 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. wW  j(w) < csucc(K)"
  shows "(wW. 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(wW. j(w))" using j
    by (blast elim: ltE)
  note lt_subset_trans [OF _ _ OU, trans]
  show ?thesis
    proof (cases "W=0")
      case True  ― ‹solve the easy 0 case
      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 "(xW. j(x))  (kK. 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