# Theory CZH_Sets_Equipollence

```(* Copyright 2021 (C) Mihails Milehins *)

section‹Equipollence›
theory CZH_Sets_Equipollence
imports CZH_Sets_IF
begin

subsection‹Background›

text‹
The section presents an adaption of the existing framework ‹Equipollence›
in the main library of Isabelle/HOL to the type \<^typ>‹V›.

Some of content of this theory was ported directly (with amendments) from the
theory ‹HOL-Library.Equipollence› in the main library of Isabelle/HOL.
›

subsection‹‹veqpoll››

abbreviation veqpoll :: "V ⇒ V ⇒ bool" (infixl "≈⇩∘" 50)
where "A ≈⇩∘ B ≡ elts A ≈ elts B"

text‹Rules›

lemma (in v11) v11_veqpollI[intro]:
assumes "𝒟⇩∘ r = A" and "ℛ⇩∘ r = B"
shows "A ≈⇩∘ B"
unfolding eqpoll_def
proof(intro exI[of _ ‹λx. r⦇x⦈›] bij_betw_imageI)
from v11.v11_injective v11_axioms show "inj_on (app r) (elts A)"
unfolding assms[symmetric] by (intro inj_onI) blast
show "app r ` elts A = elts B" unfolding assms[symmetric] by force+
qed

lemmas v11_veqpollI[intro] = v11.v11_veqpollI

lemma v11_veqpollE[elim]:
assumes "A ≈⇩∘ B"
obtains f where "v11 f" and "𝒟⇩∘ f = A" and "ℛ⇩∘ f = B"
proof-
from assms obtain f where bij_f: "bij_betw f (elts A) (elts B)"
unfolding eqpoll_def by auto
then have "v11 (λa∈⇩∘A. f a)"
and "𝒟⇩∘ (λa∈⇩∘A. f a) = A"
and "ℛ⇩∘ (λa∈⇩∘A. f a) = B"
by (auto simp add: in_mono vrange_VLambda)
then show ?thesis using that by simp
qed

text‹Set operations.›

lemma veqpoll_vsingleton: "set {x} ≈⇩∘ set {y}"

lemma veqpoll_vinsert:
assumes "A ≈⇩∘ B" and "a ∉⇩∘ A" and "b ∉⇩∘ B"
shows "vinsert a A ≈⇩∘ vinsert b B"
using assms by (simp add: insert_eqpoll_insert_iff)

lemma veqpoll_pair:
assumes "a ≠ b" and "c ≠ d"
shows "set {a, b} ≈⇩∘ set {c, d}"
using assms by (simp add: insert_eqpoll_cong)

lemma veqpoll_vpair:
assumes "a ≠ b" and "c ≠ d"
shows "⟨a, b⟩ ≈⇩∘ ⟨c, d⟩"
using assms
unfolding vpair_def
by (metis doubleton_eq_iff insert_absorb2 veqpoll_pair)

subsection‹‹vlepoll››

abbreviation vlepoll :: "V ⇒ V ⇒ bool" (infixl "≲⇩∘" 50)
where "A ≲⇩∘ B ≡ elts A ≲ elts B"

text‹Set operations.›

lemma vlepoll_vsubset:
assumes "A ⊆⇩∘ B"
shows "A ≲⇩∘ B"
using assms by (simp add: less_eq_V_def subset_imp_lepoll)

text‹Special properties.›

lemma vlepoll_singleton_vinsert: "set {x} ≲⇩∘ vinsert y A"

lemma vlepoll_vempty_iff[simp]: "A ≲⇩∘ 0 ⟷ A = 0" by (rule iffI) fastforce+

subsection‹‹vlespoll››

abbreviation vlesspoll :: "V ⇒ V ⇒ bool" (infixl ‹≺⇩∘› 50)
where "A ≺⇩∘ B ≡ elts A ≺ elts B"

lemma vlesspoll_def: "A ≺⇩∘ B = (A ≲⇩∘ B ∧ ~(A ≈⇩∘ B))" by (simp add: lesspoll_def)

text‹Rules.›

lemmas vlesspollI[intro] = vlesspoll_def[THEN iffD2]

lemmas vlesspollD[dest] = vlesspoll_def[THEN iffD1]

lemma vlesspollE[elim]:
assumes "A ≺⇩∘ B" and "A ≲⇩∘ B ⟹ ~(A ≈⇩∘ B) ⟹ P"
shows P
using assms by (simp add: vlesspoll_def)

lemma (in v11) v11_vlepollI[intro]:
assumes "𝒟⇩∘ r = A" and "ℛ⇩∘ r ⊆⇩∘ B"
shows "A ≲⇩∘ B"
unfolding lepoll_def
proof(intro exI[of _ ‹λx. r⦇x⦈›] conjI)
show "inj_on (app r) (elts A)"
using assms(1) v11.v11_injective v11_axioms by (intro inj_onI) blast
show "app r ` elts A ⊆ elts B"
by (intro subsetI) (metis assms(1,2) imageE rev_vsubsetD vdomain_atD)
qed

lemmas v11_vlepollI[intro] = v11.v11_vlepollI

lemma v11_vlepollE[elim]:
assumes "A ≲⇩∘ B"
obtains f where "v11 f" and "𝒟⇩∘ f = A" and "ℛ⇩∘ f ⊆⇩∘ B"
proof-
from assms obtain f where "inj_on f (elts A)" and "f ` elts A ⊆ elts B"
unfolding lepoll_def by auto
then have "v11 (λa∈⇩∘A. f a)"
and "𝒟⇩∘ (λa∈⇩∘A. f a) = A"
and "ℛ⇩∘ (λa∈⇩∘A. f a) ⊆⇩∘ B"
by (auto simp: in_mono vrange_VLambda)
then show ?thesis using that by simp
qed

text‹\newpage›

end```