Theory ZFC_in_HOL.General_Cardinals

section ‹ZF sets corresponding to $\mathbb{R}$ and $\mathbb{C}$ and the cardinality of the contimuum›

theory General_Cardinals
  imports ZFC_Typeclasses "HOL-Analysis.Continuum_Not_Denumerable"

begin

subsection ‹Making the embedding from the type class explicit›

definition V_of :: "'a::embeddable ⇒ V"
  where "V_of ≡ SOME f. inj f"

lemma inj_V_of: "inj V_of"
  unfolding V_of_def by (metis embeddable_class.ex_inj some_eq_imp)

declare inv_f_f [OF inj_V_of, simp]

lemma inv_V_of_image_eq [simp]: "inv V_of ` (V_of ` X) = X"
  by (auto simp: image_comp)

lemma infinite_V_of: "infinite (UNIV::'a set) ⟹ infinite (range (V_of::'a::embeddable⇒V))"
  using finite_imageD inj_V_of by blast

lemma countable_V_of: "countable (range (V_of::'a::countable⇒V))"
  by blast

lemma elts_set_V_of: "small X ⟹ elts (ZFC_in_HOL.set (V_of ` X)) ≈ X"
  by (metis inj_V_of inj_eq inj_on_def inj_on_image_eqpoll_self replacement set_of_elts small_iff)

lemma V_of_image_times: "V_of ` (X × Y) ≈ (V_of ` X) × (V_of ` Y)"
proof -
  have "V_of ` (X × Y) ≈ X × Y"
    by (meson inj_V_of inj_eq inj_onI inj_on_image_eqpoll_self)
  also have "… ≈ (V_of ` X) × (V_of ` Y)"
    by (metis eqpoll_sym inj_V_of inj_eq inj_onI inj_on_image_eqpoll_self times_eqpoll_cong)
  finally show ?thesis .
qed

subsection ‹The cardinality of the continuum›

definition "Real_set ≡ ZFC_in_HOL.set (range (V_of::real⇒V))"
definition "Complex_set ≡ ZFC_in_HOL.set (range (V_of::complex⇒V))"
definition "C_continuum ≡ vcard Real_set"

lemma V_of_Real_set: "bij_betw V_of (UNIV::real set) (elts Real_set)"
  by (simp add: Real_set_def bij_betw_def inj_V_of)

lemma uncountable_Real_set: "uncountable (elts Real_set)"
  using V_of_Real_set countable_iff_bij uncountable_UNIV_real by blast

lemma "Card C_continuum"
  by (simp add: C_continuum_def Card_def)

lemma C_continuum_ge: "C_continuum ≥ ℵ1"
  by (metis C_continuum_def Ord_ω1 Ord_cardinal Ord_linear2 countable_iff_vcard_less1 
            uncountable_Real_set)

lemma V_of_Complex_set: "bij_betw V_of (UNIV::complex set) (elts Complex_set)"
  by (simp add: Complex_set_def bij_betw_def inj_V_of)

lemma uncountable_Complex_set: "uncountable (elts Complex_set)"
  using V_of_Complex_set countableI_bij2 uncountable_UNIV_complex by blast

lemma Complex_vcard: "vcard Complex_set = C_continuum"
proof -
  define emb1 where "emb1 ≡ V_of o complex_of_real o inv V_of"
  have "elts Real_set ≈ elts Complex_set"
  proof (rule lepoll_antisym)
    show "elts Real_set ≲ elts Complex_set"
      unfolding lepoll_def
    proof (intro conjI exI)
      show "inj_on emb1 (elts Real_set)"
        unfolding emb1_def Real_set_def
        by (simp add: inj_V_of inj_compose inj_of_real inj_on_imageI)
      show "emb1 ` elts Real_set ⊆ elts Complex_set"
        by (simp add: emb1_def Real_set_def Complex_set_def image_subset_iff)
    qed
    define emb2 where "emb2 ≡ (λz. (V_of (Re z), V_of (Im z))) o inv V_of"
    have "elts Complex_set ≲ elts Real_set × elts Real_set"
      unfolding lepoll_def
    proof (intro conjI exI)
      show "inj_on emb2 (elts Complex_set)"
        unfolding emb2_def Complex_set_def inj_on_def
        by (simp add: complex.expand inj_V_of inj_eq)
      show "emb2 ` elts Complex_set ⊆ elts Real_set × elts Real_set"
        by (simp add: emb2_def Real_set_def Complex_set_def image_subset_iff)
    qed
    also have "…  ≈ elts Real_set"
      by (simp add: infinite_times_eqpoll_self uncountable_Real_set uncountable_infinite)
    finally show "elts Complex_set ≲ elts Real_set" .
  qed
  then show ?thesis
    by (simp add: C_continuum_def cardinal_cong)
qed

lemma gcard_Union_le_cmult:
  assumes "small U" and κ: "⋀x. x ∈ U ⟹ gcard x ≤ κ" and sm: "⋀x. x ∈ U ⟹ small x"
  shows "gcard (⋃U) ≤ gcard U ⊗ κ"
proof -
  have "∃f. f ∈ x → elts κ ∧ inj_on f x" if "x ∈ U" for x
    using κ [OF that] gcard_le_lepoll by (metis image_subset_iff_funcset lepoll_def sm that)
  then obtain φ where φ: "⋀x. x ∈ U ⟹ (φ x) ∈ x → elts κ ∧ inj_on (φ x) x"
    by metis
  define u where "u ≡ λy. @x. x ∈ U ∧ y ∈ x"
  have u: "u y ∈ U ∧ y ∈  (u y)" if "y ∈ ⋃( U)" for y
    unfolding u_def using that by (fast intro!: someI2)
  define ψ where "ψ ≡ λy. (u y, φ (u y) y)"
  have U: "elts (gcard U) ≈ U"
    using assms by (simp add: gcard_eqpoll)
   have "⋃U ≲ U × elts κ"
    unfolding lepoll_def
  proof (intro exI conjI)
    show "inj_on ψ (⋃ U)"
      using φ u by (smt (verit) ψ_def inj_on_def prod.inject)
    show "ψ ` ⋃ U ⊆ U × elts κ"
      using φ u by (auto simp: ψ_def)
  qed
  also have "…  ≈ elts (gcard U ⊗ κ)"
    using U elts_cmult eqpoll_sym eqpoll_trans times_eqpoll_cong by blast
  finally have " (⋃U) ≲ elts (gcard U ⊗ κ)" .
  then show ?thesis
    by (metis cardinal_idem cmult_def gcard_eq_vcard lepoll_imp_gcard_le small_elts)
qed

lemma gcard_Times [simp]: "gcard (X × Y) = gcard X ⊗ gcard Y"
proof (cases "small X ∧ small Y")
  case True
  have "elts (gcard (X × Y)) ≈ X × Y"
    by (simp add: True gcard_eqpoll)
  also have "... ≈ elts (gcard X) × elts (gcard Y)"
    by (simp add: True eqpoll_sym gcard_eqpoll times_eqpoll_cong)
  also have "... ≈ elts (gcard X ⊗ gcard Y)"
    by (simp add: elts_cmult eqpoll_sym)
  finally show ?thesis
    using Card_cardinal_eq cmult_def gcardinal_cong by force
next
  case False
  have "gcard (X × Y) = 0"
    by (metis False Times_empty gcard_big_0 gcard_empty_0 small_Times_iff)
  then show ?thesis
    by (metis False cmult_0 cmult_commute gcard_big_0)
qed

subsection ‹Countable and uncountable sets›

lemma countable_iff_g_le_Aleph0:
  assumes "small X"
  shows "countable X ⟷ gcard X ≤ ℵ0"
proof -
  have "countable X ⟷ X ≲ elts ω"
    by (simp add: ω_def countable_iff_lepoll inj_ord_of_nat)
  also have "... ⟷ gcard X ≤ ℵ0"
    using Card_ω Card_def assms gcard_le_lepoll lepoll_imp_gcard_le by fastforce
  finally show ?thesis .
qed

lemma countable_imp_g_le_Aleph0: "countable X ⟹ gcard X ≤ ℵ0"
  by (meson countable countable_iff_g_le_Aleph0)

lemma finite_iff_g_le_Aleph0: "small X ⟹ finite X ⟷ gcard X < ℵ0"
  by (metis Aleph_0 eqpoll_finite_iff finite_iff_less_Aleph0 gcard_eq_vcard gcard_eqpoll gcardinal_cong)

lemma finite_imp_g_le_Aleph0: "finite X ⟹ gcard X < ℵ0"
  by (meson finite_iff_g_le_Aleph0 finite_imp_small)

lemma countable_infinite_gcard: "countable X ∧ infinite X ⟷ gcard X = ℵ0"
proof -
  have "gcard X = ω"
    if "countable X" and "infinite X"
    using that countable countable_imp_g_le_Aleph0 finite_iff_g_le_Aleph0 less_V_def by auto
  moreover have "countable X" if "gcard X = ω"
    by (metis Aleph_0 countable_iff_g_le_Aleph0 dual_order.refl gcard_big_0 omega_nonzero that)
  moreover have False if "gcard X = ω" and "finite X"
    by (metis Aleph_0 dual_order.irrefl finite_iff_g_le_Aleph0 finite_imp_small that)
  ultimately show ?thesis
    by auto
qed

lemma uncountable_gcard: "small X ⟹ uncountable X ⟷ gcard X > ℵ0"
  by (simp add: Card_is_Ord Ord_not_le countable_iff_g_le_Aleph0)

lemma uncountable_gcard_ge: "small X ⟹ uncountable X ⟷ gcard X ≥ ℵ1"
  by (simp add: uncountable_gcard csucc_le_Card_iff one_V_def)

lemma subset_smaller_gcard:
  assumes κ: "κ ≤ gcard X" "Card κ"
  obtains Y where "Y ⊆ X" "gcard Y = κ"
proof (cases "small X")
  case True
  then have "elts κ ≲ X"
    by (meson assms(1) eqpoll_imp_lepoll gcard_eqpoll lepoll_trans less_eq_V_def subset_imp_lepoll)
  then obtain Y where "Y ⊆ X" "elts κ ≈ Y"
    by (metis bij_betw_def eqpoll_def lepoll_def)
  then show ?thesis
    using Card_def ‹Card κ› gcardinal_cong that by force
next
  case False
  with assms show ?thesis
    by (metis antisym gcard_big_0 le_0 order_refl that)
qed

lemma Real_gcard: "gcard (UNIV::real set) = C_continuum"
  by (metis C_continuum_def V_of_Real_set bij_betw_def gcard_eq_vcard gcard_image)

lemma Complex_gcard: "gcard (UNIV::complex set) = C_continuum"
  by (metis Complex_vcard V_of_Complex_set bij_betw_def gcard_eq_vcard gcard_image)

end