Theory CZH_Sets_Cardinality

(* Copyright 2021 (C) Mihails Milehins *)

theory CZH_Sets_Cardinality


The section presents further results about the cardinality of terms of the type
typV. The emphasis of this work, however, is on the development of a theory of
finite sets internalized in the type typV.

Many of the results that are presented in this section were carried over
(with amendments) from the theory Finite› in the main library of Isabelle/HOL.

declare One_nat_def[simp del]

subsection‹Cardinality of an arbitrary set›

text‹Elementary properties.›

lemma vcard_veqpoll: "vcard A = vcard B  A  B"
  by (metis cardinal_cong cardinal_eqpoll eqpoll_sym eqpoll_trans)

lemma vcard_vlepoll: "vcard A  vcard B  A  B"
  assume "vcard A  vcard B"
  moreover have "vcard A  A" by (rule cardinal_eqpoll)
  moreover have "vcard B  B" by (rule cardinal_eqpoll)
  ultimately show "A  B"
    by (meson eqpoll_sym lepoll_trans1 lepoll_trans2 vlepoll_vsubset)
qed (simp add: lepoll_imp_Card_le)

lemma vcard_vempty: "vcard A = 0  A = 0"
  have vcard_A: "vcard A  A" by (simp add: cardinal_eqpoll)
  then show ?thesis using eq0_iff eqpoll_iff_bijections by metis

lemmas vcard_vemptyD = vcard_vempty[THEN iffD1]
  and vcard_vemptyI = vcard_vempty[THEN iffD2]

lemma vcard_neq_vempty: "vcard A  0  A  0"
  using vcard_vempty by auto

lemmas vcard_neq_vemptyD = vcard_neq_vempty[THEN iffD1]
  and vcard_neq_vemptyI = vcard_neq_vempty[THEN iffD2]

text‹Set operations.›

lemma vcard_mono:
  assumes "A  B"
  shows "vcard A  vcard B"
  using assms by (simp add: lepoll_imp_Card_le vlepoll_vsubset)

lemma vcard_vinsert_in[simp]:
  assumes "a  A"
  shows "vcard (vinsert a A) = vcard A"
  using assms by (simp add: cardinal_cong insert_absorb)

lemma vcard_vintersection_left: "vcard (A  B)  vcard A" 
  by (simp add: vcard_mono)

lemma vcard_vintersection_right: "vcard (A  B)  vcard B" 
  by (simp add: vcard_mono)

lemma vcard_vunion: 
  assumes "vdisjnt A B"
  shows "vcard (A  B) = vcard A  vcard B"
  using assms by (rule vcard_disjoint_sup)

lemma vcard_vdiff[simp]: "vcard (A - B)  vcard (A  B) = vcard A"
  have ABB: "vdisjnt (A - B) (A  B)" by auto
  have "A - B  A  B = A" by auto
  from vcard_vunion[OF ABB, unfolded this] show ?thesis ..

lemma vcard_vdiff_vsubset:
  assumes "B  A"
  shows "vcard (A - B)  vcard B = vcard A"
  by (metis assms inf.absorb_iff2 vcard_vdiff)


lemma (in vsv) vsv_vcard_vdomain: "vcard (𝒟 r) = vcard r"
  unfolding vcard_veqpoll 
  define f where "f x = x, rx" for x
  have "bij_betw f (elts (𝒟 r)) (elts r)" 
    unfolding f_def bij_betw_def
  proof(intro conjI inj_onI subset_antisym subsetI)
    from vlrestriction_vdomain show 
      "x  r  x  (λx. x, rx) ` elts (𝒟 r)" 
      for x
      unfolding mem_Collect_eq by blast
  qed (auto simp: image_def)
  then show "𝒟 r  r" unfolding eqpoll_def by auto

text‹Special properties.›

lemma vcard_vunion_vintersection: 
  "vcard (A  B)  vcard (A  B) = vcard A  vcard B"
  have AB_ABB: "A  B = B  (A - B)" by auto
  have ABB: "vdisjnt B (A - B)" by auto
  show ?thesis
    unfolding vcard_vunion[OF ABB, folded AB_ABB] cadd_assoc vcard_vdiff
    by (simp add: cadd_commute)

subsection‹Finite sets›

abbreviation vfinite :: "V  bool" 
  where "vfinite A  finite (elts A)"

lemma vfinite_def: "vfinite A  (nω. n  A)"  
  assume "finite (elts A)"
  then obtain n :: nat where eltsA: "elts A  {..<n}" 
    by (simp add: eqpoll_iff_card)
  have on: "ord_of_nat n = set (ord_of_nat ` {..<n})"
    by (simp add: ord_of_nat_eq_initial[symmetric])
  from eltsA have "elts A  elts (ord_of_nat n)" 
    unfolding on by (simp add: inj_on_def)
  moreover have "ord_of_nat n  ω" by (simp add: ω_def)
  ultimately show "nω. n  A" by (auto intro: eqpoll_sym)
  assume "nω. n  A" 
  then obtain n where "n  ω" and "n  A" by auto
  with eqpoll_finite_iff show "finite (elts A)"
    by (auto intro: finite_Ord_omega)


lemmas vfiniteI[intro!] = vfinite_def[THEN iffD2]  

lemmas vfiniteD[dest!] = vfinite_def[THEN iffD1]

lemma vfiniteE1[elim!]:
  assumes "vfinite A" and "nω. n  A  P"
  shows P
  using assms by auto

lemma vfiniteE2[elim]:
  assumes "vfinite A" 
  obtains n where "n  ω" and "n  A"
  using assms by auto

text‹Elementary properties.›

lemma veqpoll_omega_vcard[intro, simp]:
  assumes "n  ω" and "n  A" 
  shows "vcard A = n"
    nat_into_Card[OF assms(1), unfolded Card_def] 
    cardinal_cong[OF assms(2)] 
  by simp

lemma (in vsv) vfinite_vimage[intro]:
  assumes "vfinite A"
  shows "vfinite (r ` A)"
  have rA: "r ` A = r ` (𝒟 r  A)" by fast
  have DrA: "𝒟 r  A  𝒟 r" by simp
  show ?thesis by (simp add: inf_V_def assms vimage_image[OF DrA, folded rA])

lemmas [intro] = vsv.vfinite_vimage

lemma vfinite_veqpoll_trans:
  assumes "vfinite A" and "A  B" 
  shows "vfinite B"
  using assms by (simp add: eqpoll_finite_iff)

lemma vfinite_vlepoll_trans:
  assumes "vfinite A" and "B  A"   
  shows "vfinite B"
  by (meson assms eqpoll_finite_iff finite_lepoll_infinite lepoll_antisym)

lemma vfinite_vlesspoll_trans:
  assumes "vfinite A" and "B  A"   
  shows "vfinite B"
  using assms by (auto simp: vlesspoll_def vfinite_vlepoll_trans)


lemma vfinite_induct[consumes 1, case_names vempty vinsert]:
  assumes "vfinite F"
    and "P 0"
    and "x F. vfinite F; x  F; P F  P (vinsert x F)"
  shows "P F"

  from assms(1) obtain n where n: "n  ω" and "n  F" by clarsimp
  then obtain f'' where bij: "bij_betw f'' (elts n) (elts F)" 
    unfolding eqpoll_def by clarsimp
  define f where "f = (λan. f'' a)"
  interpret v11 f 
    unfolding f_def
  proof(intro v11I)
    show "vsv ((λan. f'' a)¯)"
    proof(intro vsvI)
      fix a b c 
      assume "a, b  (λan. f'' a)¯" and "a, c  (λan. f'' a)¯"
      then have "b, a  (λan. f'' a)" 
        and "c, a  (λan. f'' a)" 
        and "b  n" 
        and "c  n"
        by auto
      moreover then have "f'' b = f'' c" by auto
      ultimately show "b = c" using bij by (metis bij_betw_iff_bijections)
    qed auto
  qed auto
  have dom_f: "𝒟 f = n" unfolding f_def by clarsimp
  have ran_f: " f = F"
  proof(intro vsubset_antisym vsubsetI)
    fix b assume "b   f"
    then obtain a where "a  n" and "b = f'' a" unfolding f_def by auto
    then show "b  F" by (meson bij bij_betw_iff_bijections)
    fix b assume "b  F"
    then obtain a where "a  n" and "b = f'' a" 
      by (metis bij bij_betw_iff_bijections)
    then show "b   f" unfolding f_def by auto

  define f' where "f' n = f ` n" for n
  have F_def: "F = f' n" 
    unfolding f'_def using dom_f ran_f vimage_vdomain by clarsimp
  have "v11 (λan. f' a)"
  proof(intro vsv.vsv_valneq_v11I, unfold vdomain_VLambda)
    show "vsv (λan. f' a)" by simp
    fix x y assume xD: "x  n" and yD: "y  n" and xy: "x  y"
    from x  n y  n n  ω have xn: "x  n" and yn: "y  n"
      by (simp_all add: OrdmemD order.strict_implies_order)
    show "(λan. f' a)x  (λan. f' a)y"
      unfolding beta[OF xD] beta[OF yD] f'_def
      using xn yn xy 
      by (simp add: dom_f v11_vimage_vpsubset_neq)

  define P' where "P' n' = (if n'  n then P (f' n') else True)" for n'
  from n have "P' n"
  proof(induct rule: omega_induct)
    case 0 then show ?case 
      unfolding P'_def f'_def using assms(2) by auto
    case (succ k) show ?case 
    proof(cases succ k  n)
      case True
      then obtain x where xF: "vinsert x (f' k) = (f' (succ k))"
        by (simp add: f'_def succ_def vsubsetD dom_f vsv_vimage_vinsert)
      from True have "k  n" by auto
      with P' k have "P (f' k)" unfolding P'_def by simp
      then have "f' k  f' (succ k)"
        by (simp add: True f'_def k  n dom_f v11_vimage_vpsubset_neq)
      with xF have "x  f' k" by auto
      have "vfinite (f' k)" 
        by (simp add: k  ω f'_def finite_Ord_omega vfinite_vimage)
      from assms(3)[OF vfinite (f' k) x  f' k P (f' k)] show ?thesis 
        unfolding xF P'_def by simp
    qed (unfold P'_def, auto)

  then show ?thesis unfolding P'_def F_def by simp


text‹Set operations.›

lemma vfinite_vempty[simp]: "vfinite (0)" by simp

lemma vfinite_vsingleton[simp]: "vfinite (set {x})" by simp

lemma vfinite_vdoubleton[simp]: "vfinite (set {x, y})" by simp

lemma vfinite_vinsert:
  assumes "vfinite F"
  shows "vfinite (vinsert x F)"
  using assms by simp

lemma vfinite_vinsertD:
  assumes "vfinite (vinsert x F)"
  shows "vfinite F"
  using assms by simp

lemma vfinite_vsubset: 
  assumes "vfinite B" and "A  B" 
  shows "vfinite A"
  using assms
  by (induct arbitrary: A rule: vfinite_induct)
    (simp_all add: less_eq_V_def finite_subset)

lemma vfinite_vunion: "vfinite (A  B)  vfinite A  vfinite B" 
  by (auto simp: elts_sup_iff)

lemma vfinite_vunionI:
  assumes "vfinite A" and "vfinite B"
  shows "vfinite (A  B)"
  using assms by (simp add: elts_sup_iff)

lemma vfinite_vunionD:
  assumes "vfinite (A  B)" 
  shows "vfinite A" and "vfinite B"
  using assms by (auto simp: elts_sup_iff)

lemma vfinite_vintersectionI:
  assumes "vfinite A" and "vfinite B"
  shows "vfinite (A  B)"
  using assms by (simp add: vfinite_vsubset)

lemma vfinite_VPowI: 
  assumes "vfinite A"
  shows "vfinite (VPow A)"
  using assms
proof(induct rule: vfinite_induct)
  case vempty then show ?case by simp
  case (vinsert x F)
  then show ?case 
    unfolding VPow_vinsert 
    using rel_VLambda.vfinite_vimage 
    by (intro vfinite_vunionI) metis+


lemma vfinite_vcard_vfinite: "vfinite (vcard A) = vfinite A" 
  by (simp add: cardinal_eqpoll eqpoll_finite_iff)

lemma vfinite_vcard_omega_iff: "vfinite A  vcard A  ω" 
   using vfinite_vcard_vfinite by auto

lemmas vcard_vfinite_omega = vfinite_vcard_omega_iff[THEN iffD2]
  and vfinite_vcard_omega = vfinite_vcard_omega_iff[THEN iffD1]

lemma vfinite_csucc[intro, simp]:
  assumes "vfinite A"
  shows "csucc (vcard A) = succ (vcard A)"
  using assms by (force simp: finite_csucc)

lemmas [intro, simp] = finite_csucc

text‹Previous connections.›

lemma vcard_vsingleton[simp]: "vcard (set {a}) = 1" by auto

lemma vfinite_vcard_vinsert_nin[simp]:
  assumes "vfinite A" and "a  A"
  shows "vcard (vinsert a A) = csucc (vcard A)"
  using assms by (simp add: ZFC_in_HOL.vinsert_def)