# 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)

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"

lemma vcard_vintersection_right: "vcard (A ∩⇩∘ B) ≤ vcard B"

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
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}"
have on: "ord_of_nat n = set (ord_of_nat ` {..<n})"
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"
show "(λa∈⇩∘n. f' a)⦇x⦈ ≠ (λa∈⇩∘n. f' a)⦇y⦈"
unfolding beta[OF xD] beta[OF yD] f'_def
using xn yn xy
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)

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"

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```