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"


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::embeddableV))"
  using finite_imageD inj_V_of by blast

lemma countable_V_of: "countable (range (V_of::'a::countableV))"
  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 .

subsection ‹The cardinality of the continuum›

definition "Real_set  ZFC_in_HOL.set (range (V_of::realV))"
definition "Complex_set  ZFC_in_HOL.set (range (V_of::complexV))"
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 

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)
    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)
    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" .
  then show ?thesis
    by (simp add: C_continuum_def cardinal_cong)

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

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

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 .

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

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
  case False
  with assms show ?thesis
    by (metis antisym gcard_big_0 le_0 order_refl that)

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)