Theory CZH_Sets_Cardinality

(* Copyright 2021 (C) Mihails Milehins *)

section‹Cardinality›
theory CZH_Sets_Cardinality
  imports 
    CZH_Sets_Nat
    CZH_Sets_Equipollence
begin



subsection‹Background›


text‹
The section presents further results about the cardinality of terms of the type
\<^typ>‹V›. The emphasis of this work, however, is on the development of a theory of
finite sets internalized in the type \<^typ>‹V›.

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"
proof
  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"
proof-
  have vcard_A: "vcard A ≈⇩∘ A" by (simp add: cardinal_eqpoll)
  then show ?thesis using eq0_iff eqpoll_iff_bijections by metis
qed

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"
proof-
  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 ..
qed

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


text‹Connections.›

lemma (in vsv) vsv_vcard_vdomain: "vcard (𝒟⇩∘ r) = vcard r"
  unfolding vcard_veqpoll 
proof-
  define f where "f x = ⟨x, r⦇x⦈⟩" 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, r⦇x⦈⟩) ` elts (𝒟⇩∘ r)" 
      for x
      unfolding mem_Collect_eq by blast
  qed (auto simp: image_def)
  then show "𝒟⇩∘ r ≈⇩∘ r" unfolding eqpoll_def by auto
qed


text‹Special properties.›

lemma vcard_vunion_vintersection: 
  "vcard (A ∪⇩∘ B) ⊕ vcard (A ∩⇩∘ B) = vcard A ⊕ vcard B"
proof-
  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)
qed



subsection‹Finite sets›

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

lemma vfinite_def: "vfinite A ⟷ (∃n∈⇩∘ω. n ≈⇩∘ A)"  
proof
  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)
next
  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)
qed


text‹Rules.›

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"
  using 
    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)"
proof-
  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])
qed

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)


text‹Induction.›

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"
proof-

  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 = (λa∈⇩∘n. f'' a)"
  interpret v11 f 
    unfolding f_def
  proof(intro v11I)
    show "vsv ((λa∈⇩∘n. f'' a)¯⇩∘)"
    proof(intro vsvI)
      fix a b c 
      assume "⟨a, b⟩ ∈⇩∘ (λa∈⇩∘n. f'' a)¯⇩∘" and "⟨a, c⟩ ∈⇩∘ (λa∈⇩∘n. f'' a)¯⇩∘"
      then have "⟨b, a⟩ ∈⇩∘ (λa∈⇩∘n. f'' a)" 
        and "⟨c, a⟩ ∈⇩∘ (λa∈⇩∘n. 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)
  next
    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
  qed

  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 (λa∈⇩∘n. f' a)"
  proof(intro vsv.vsv_valneq_v11I, unfold vdomain_VLambda)
    show "vsv (λa∈⇩∘n. 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 "(λa∈⇩∘n. f' a)⦇x⦈ ≠ (λa∈⇩∘n. 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)
  qed

  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
  next
    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)
  qed  

  then show ?thesis unfolding P'_def F_def by simp

qed


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
next
  case (vinsert x F)
  then show ?case 
    unfolding VPow_vinsert 
    using rel_VLambda.vfinite_vimage 
    by (intro vfinite_vunionI) metis+
qed


text‹Connections.›

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)

text‹\newpage›

end