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}"
  by (simp add: singleton_eqpoll)

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" 
  by (simp add: singleton_lepoll)

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