Theory Cardinality_Continuum.Cardinality_Continuum_Library

(*
  File:     Cardinality_Continuum/Cardinality_Continuum_Library.thy
  Author:   Manuel Eberl (University of Innsbruck)

  Some missing facts about cardinality and equipollence, but most notably
  the definition and cardinality results about the "finite subsets of" operator and the
  "functions with finite support" operator.
*)
section ‹Auxiliary material›
theory Cardinality_Continuum_Library
  imports "HOL-Library.Equipollence" "HOL-Cardinals.Cardinals"
begin

subsection ‹Miscellaneous facts about cardinalities›

(* Equipollence *)
lemma eqpoll_Pow [intro]:
  assumes "A ≈ B"
  shows   "Pow A ≈ Pow B"
proof -
  from assms obtain f where "bij_betw f A B"
    unfolding eqpoll_def by blast
  hence "bij_betw ((`) f) (Pow A) (Pow B)"
    by (rule bij_betw_Pow)
  thus ?thesis
    unfolding eqpoll_def by blast
qed

lemma lepoll_UNIV_nat_iff: "A ≲ (UNIV :: nat set) ⟷ countable A"
  unfolding countable_def lepoll_def by simp

lemma countable_eqpoll:     
  assumes "countable A" "A ≈ B"
  shows   "countable B"
  using assms countable_iff_bij unfolding eqpoll_def by blast

lemma countable_eqpoll_cong: "A ≈ B ⟹ countable A ⟷ countable B"
  using countable_eqpoll[of A B] countable_eqpoll[of B A]
  by (auto simp: eqpoll_sym)

lemma eqpoll_UNIV_nat_iff: "A ≈ (UNIV :: nat set) ⟷ countable A ∧ infinite A"
proof
  assume *: "A ≈ (UNIV :: nat set)"
  show "countable A ∧ infinite A"
    using eqpoll_finite_iff[OF *] countable_eqpoll_cong[OF *] by simp
next
  assume *: "countable A ∧ infinite A"
  thus "A ≈ (UNIV :: nat set)"
    by (meson countableE_infinite eqpoll_def)
qed


(* HOL-Cardinals *)
lemma ordLeq_finite_infinite:
  "finite A ⟹ infinite B ⟹ (card_of A, card_of B) ∈ ordLeq"
  by (meson card_of_Well_order card_of_ordLeq_finite ordLeq_total)

lemma eqpoll_imp_card_of_ordIso: "A ≈ B ⟹ |A| =o |B|"
  by (simp add: eqpoll_iff_card_of_ordIso)

lemma card_of_Func: "|Func A B| =o |B| ^c |A|"
  by (simp add: cexp_def)

lemma card_of_leq_natLeq_iff_countable:
  "|X| ≤o natLeq ⟷ countable X"
proof -
  have "countable X  ⟷ |X| ≤o |UNIV :: nat set|"
    unfolding countable_def by (meson card_of_ordLeq top_greatest)
  with card_of_nat show ?thesis
    using ordIso_symmetric ordLeq_ordIso_trans by blast
qed

lemma card_of_Sigma_cong:
  assumes "⋀x. x ∈ A ⟹ |B x| =o |B' x|"
  shows   "|SIGMA x:A. B x| =o |SIGMA x:A. B' x|"
proof -
  have "∃f. bij_betw f (B x) (B' x)" if "x ∈ A" for x
    using assms that card_of_ordIso by blast
  then obtain f where f: "⋀x. x ∈ A ⟹ bij_betw (f x) (B x) (B' x)"
    by metis
  have "bij_betw (λ(x,y). (x, f x y)) (SIGMA x:A. B x) (SIGMA x:A. B' x)"
    using f by (fastforce simp: bij_betw_def inj_on_def image_def)
  thus ?thesis
    by (rule card_of_ordIsoI)
qed

lemma Cfinite_cases:
  assumes "Cfinite c"
  obtains n :: nat where "(c, natLeq_on n) ∈ ordIso"
proof -
  from assms have "card_of (Field c) =o natLeq_on (card (Field c))"
    by (simp add: cfinite_def finite_imp_card_of_natLeq_on)
  with that[of "card (Field c)"] show ?thesis
    using assms card_of_unique ordIso_transitive by blast
qed

lemma empty_nat_ordIso_czero: "({} :: (nat × nat) set) =o czero"
proof -
  have "({} :: (nat × nat) set) =o |{} :: nat set|"
    using finite_imp_card_of_natLeq_on[of "{} :: nat set"] by (simp add: ordIso_symmetric)
  moreover have "|{} :: nat set| =o czero"
    by (simp add: card_of_ordIso_czero_iff_empty)
  ultimately show "({} :: (nat × nat) set) =o czero"
    using ordIso_symmetric ordIso_transitive by blast
qed

lemma card_order_on_empty: "card_order_on {} {}"
  unfolding card_order_on_def well_order_on_def linear_order_on_def partial_order_on_def
            preorder_on_def antisym_def trans_def refl_on_def total_on_def ordLeq_def embed_def
  by (auto intro!: ordLeq_refl)

lemma natLeq_on_plus_ordIso: "natLeq_on (m + n) =o natLeq_on m +c natLeq_on n"
proof -
  have "{0..<m+n} = {0..<m} ∪ {m..<m+n}"
    by auto
  also have "card_of ({0..<m} ∪ {m..<m+n}) =o card_of ({0..<m} <+> {m..<m+n})"
    by (rule card_of_Un_Plus_ordIso) auto
  also have "card_of ({0..<m} <+> {m..<m+n}) =o card_of {0..<m} +c card_of {m..<m+n}"
    by (rule Plus_csum)
  also have "card_of {0..<m} +c card_of {m..<m+n} =o natLeq_on m +c natLeq_on n"
    using finite_imp_card_of_natLeq_on[of "{m..<m+n}"]
    by (intro csum_cong card_of_less) auto
  finally have "|{0..<m+n}| =o natLeq_on m +c natLeq_on n" .
  moreover have "card_of {0..<m+n} =o natLeq_on (m + n)"
    by (rule card_of_less)
  ultimately show ?thesis
    using ordIso_symmetric ordIso_transitive by blast
qed

lemma natLeq_on_1_ord_iso: "natLeq_on 1 =o BNF_Cardinal_Arithmetic.cone"
proof -
  have "|{0..<1::nat}| =o natLeq_on 1"
    by (rule card_of_less)
  hence "|{0::nat}| =o natLeq_on 1"
    by simp
  moreover have "|{0::nat}| =o BNF_Cardinal_Arithmetic.cone"
    by (rule single_cone)
  ultimately show ?thesis
    using ordIso_symmetric ordIso_transitive by blast
qed

lemma cexp_infinite_finite_ordLeq:
  assumes "Cinfinite c" "Cfinite c'"
  shows   "c ^c c' ≤o c"
proof -
  have c: "Card_order c"
    using assms by auto
  from assms obtain n where n: "c' =o natLeq_on n"
    using Cfinite_cases by auto
  have "c ^c c' =o c ^c natLeq_on n"
    using assms(2) by (intro cexp_cong2 c n) auto
  also have "c ^c natLeq_on n ≤o c"
  proof (induction n)
    case 0
    have "c ^c natLeq_on 0 =o c ^c czero"
      by (intro cexp_cong2) (use assms in ‹auto simp: empty_nat_ordIso_czero card_order_on_empty›)
    also have "c ^c czero =o BNF_Cardinal_Arithmetic.cone"
      by (rule cexp_czero)
    also have "BNF_Cardinal_Arithmetic.cone ≤o c"
      using assms by (simp add: Cfinite_cone Cfinite_ordLess_Cinfinite ordLess_imp_ordLeq)
    finally show ?case .
  next
    case (Suc n)
    have "c ^c natLeq_on (Suc n) =o c ^c (natLeq_on n +c natLeq_on 1)"
      using assms natLeq_on_plus_ordIso[of n 1]
      by (intro cexp_cong2) (auto simp: natLeq_on_Card_order intro: ordIso_symmetric)
    also have "c ^c (natLeq_on n +c natLeq_on 1) =o c ^c natLeq_on n *c c ^c natLeq_on 1"
      by (rule cexp_csum)
    also have "c ^c natLeq_on n *c c ^c natLeq_on 1 ≤o c *c c"
    proof (rule cprod_mono)
      show "c ^c natLeq_on n ≤o c"
        by (rule Suc.IH)
      have "c ^c natLeq_on 1 =o c ^c BNF_Cardinal_Arithmetic.cone"
        by (intro cexp_cong2 c natLeq_on_1_ord_iso natLeq_on_Card_order)
      also have "c ^c BNF_Cardinal_Arithmetic.cone =o c"
        by (intro cexp_cone c)
      finally show "c ^c natLeq_on 1 ≤o c"
        by (rule ordIso_imp_ordLeq)
    qed
    also have "c *c c =o c"
      using assms(1) by (rule cprod_infinite)
    finally show "c ^c natLeq_on (Suc n) ≤o c" .
  qed
  finally show ?thesis .  
qed

lemma cexp_infinite_finite_ordIso:
  assumes "Cinfinite c" "Cfinite c'" "BNF_Cardinal_Arithmetic.cone ≤o c'"
  shows   "c ^c c' =o c"
proof -
  have c: "Card_order c"
    using assms by auto
  have "c =o c ^c BNF_Cardinal_Arithmetic.cone"
    by (rule ordIso_symmetric, rule cexp_cone) fact
  also have "c ^c BNF_Cardinal_Arithmetic.cone ≤o c ^c c'"
    by (intro cexp_mono2 c assms Card_order_cone) (use cone_not_czero in auto)
  finally have "c ≤o c ^c c'" .
  moreover have "c ^c c' ≤o c"
    by (rule cexp_infinite_finite_ordLeq) fact+
  ultimately show ?thesis
    by (simp add: ordIso_iff_ordLeq)
qed

lemma Cfinite_ordLeq_Cinfinite:
  assumes "Cfinite c" "Cinfinite c'"
  shows   "c ≤o c'"
  using assms Cfinite_ordLess_Cinfinite ordLess_imp_ordLeq by blast

lemma cfinite_card_of_iff [simp]: "BNF_Cardinal_Arithmetic.cfinite (card_of X) ⟷ finite X"
  by (simp add: cfinite_def)

lemma cinfinite_card_of_iff [simp]: "BNF_Cardinal_Arithmetic.cinfinite (card_of X) ⟷ infinite X"
  by (simp add: cinfinite_def)

lemma Func_conv_PiE: "Func A B = PiE A (λ_. B)"
  by (auto simp: Func_def PiE_def extensional_def)

lemma finite_Func [intro]:
  assumes "finite A" "finite B"
  shows   "finite (Func A B)"
  using assms unfolding Func_conv_PiE by (intro finite_PiE)

lemma ordLeq_antisym: "(c, c') ∈ ordLeq ⟹ (c', c) ∈ ordLeq ⟹ (c, c') ∈ ordIso"
  using ordIso_iff_ordLeq by auto

lemma cmax_cong:
  assumes "(c1, c1') ∈ ordIso" "(c2, c2') ∈ ordIso" "Card_order c1" "Card_order c2"
  shows   "cmax c1 c2 =o cmax c1' c2'"
proof -
  have [intro]: "Card_order c1'" "Card_order c2'"
    using assms Card_order_ordIso2 by auto
  have "c1 ≤o c2 ∨ c2 ≤o c1"
    by (intro ordLeq_total) (use assms in auto)
  thus ?thesis
  proof
    assume le: "c1 ≤o c2"
    with assms have le': "c1' ≤o c2'"
      by (meson ordIso_iff_ordLeq ordLeq_transitive)
    have "cmax c1 c2 =o c2"
      by (rule cmax2) (use le assms in auto)
    moreover have "cmax c1' c2' =o c2'"
      by (rule cmax2) (use le' assms in auto)
    ultimately show ?thesis
      using assms ordIso_symmetric ordIso_transitive by metis
  next
    assume le: "c2 ≤o c1"
    with assms have le': "c2' ≤o c1'"
      by (meson ordIso_iff_ordLeq ordLeq_transitive)
    have "cmax c1 c2 =o c1"
      by (rule cmax1) (use le assms in auto)
    moreover have "cmax c1' c2' =o c1'"
      by (rule cmax1) (use le' assms in auto)
    ultimately show ?thesis
      using assms ordIso_symmetric ordIso_transitive by metis
  qed
qed


subsection ‹The set of finite subsets›

text ‹
  We define an operator ‹FinPow(X)› that, given a set ‹X›, returns the set of all
  finite subsets of that set. For finite ‹X›, this is boring since it is obviously just the
  power set. For infinite ‹X›, it is however a useful concept to have.

  We will show that if ‹X› is infinite then the cardinality of ‹FinPow(X)› is exactly
  the same as that of ‹X›.
›
definition FinPow :: "'a set ⇒ 'a set set" where
  "FinPow X = {Y. Y ⊆ X ∧ finite Y}"

lemma finite_FinPow [intro]: "finite A ⟹ finite (FinPow A)"
  by (auto simp: FinPow_def)

lemma in_FinPow_iff: "Y ∈ FinPow X ⟷ Y ⊆ X ∧ finite Y"
  by (auto simp: FinPow_def)

lemma FinPow_subseteq_Pow: "FinPow X ⊆ Pow X"
  unfolding FinPow_def by blast

lemma FinPow_eq_Pow: "finite X ⟹ FinPow X = Pow X"
  unfolding FinPow_def using finite_subset by blast

theorem card_of_FinPow_infinite:
  assumes "infinite A"
  shows   "|FinPow A| =o |A|"
proof -
  have "set ` lists A = FinPow A"
    using finite_list[where ?'a = 'a] by (force simp: FinPow_def)
  hence "|FinPow A| ≤o |lists A|"
    by (metis card_of_image)
  also have "|lists A| =o |A|"
    using assms by (rule card_of_lists_infinite)
  finally have "|FinPow A| ≤o |A|" .
  moreover have "inj_on (λx. {x}) A" "(λx. {x}) ` A ⊆ FinPow A"
    by (auto simp: inj_on_def FinPow_def)
  hence "|A| ≤o |FinPow A|"
    using card_of_ordLeq by blast
  ultimately show ?thesis
    by (simp add: ordIso_iff_ordLeq)
qed


subsection ‹The set of functions with finite support›

text ‹
  Next, we define an operator $\text{Func\_finsupp}_z(A, B)$ that, given sets ‹A› and ‹B› and
  an element ‹z ∈ B›, returns the set of functions ‹f : A → B› that have ∗‹finite support›, i.e.\ 
  that map all but a finite subset of ‹A› to ‹z›.
›
definition Func_finsupp :: "'b ⇒ 'a set ⇒ 'b set ⇒ ('a ⇒ 'b) set" where
  "Func_finsupp z A B = {f∈A → B. (∀x. x ∉ A ⟶ f x = z) ∧ finite {x. f x ≠ z}}"

lemma bij_betw_Func_finsup_Func_finite:
  assumes "finite A"
  shows   "bij_betw (λf. restrict f A) (Func_finsupp z A B) (Func A B)"
  by (rule bij_betwI[of _ _ _ "λf x. if x ∈ A then f x else z"])
     (use assms in ‹auto simp: Func_finsupp_def Func_def›)

lemma eqpoll_Func_finsup_Func_finite: "finite A ⟹ Func_finsupp z A B ≈ Func A B"
  by (meson bij_betw_Func_finsup_Func_finite eqpoll_def)

lemma card_of_Func_finsup_finite: "finite A ⟹ |Func_finsupp z A B| =o |B| ^c |A|"
  using eqpoll_Func_finsup_Func_finite
  by (metis Field_card_of cexp_def eqpoll_imp_card_of_ordIso)

text ‹
  The cases where $A$ and $B$ are both finite or $B = \{0\}$ or $A = \emptyset$ are of course
  trivial.

  Perhaps not completely obviously, it turns out that in all other cases, the cardinality of
  $\text{Func\_finsupp}_z(A, B)$ is exactly $\text{max}(|A|, |B|)$.
›
theorem card_of_Func_finsupp_infinite:
  assumes "z ∈ B" and "B - {z} ≠ {}" and "A ≠ {}"
  assumes "infinite A ∨ infinite B"
  shows   "|Func_finsupp z A B| =o cmax |A| |B|"
proof -
  have inf_cmax: "Cinfinite (cmax |A| |B| )"
    using assms by (simp add: Card_order_cmax cinfinite_def finite_cmax)

  have "bij_betw (λf. ({x. f x ≠ z}, restrict f {x. f x ≠ z}))
          (Func_finsupp z A B) (SIGMA X:FinPow A. Func X (B - {z}))"
    by (rule bij_betwI[of _ _ _ "λ(X,f) x. if x ∈ -X ∪ -A then z else f x"])
       (fastforce simp: Func_def Func_finsupp_def FinPow_def fun_eq_iff ‹z ∈ B› split: if_splits)+
  hence "|Func_finsupp z A B| =o |SIGMA X:FinPow A. Func X (B - {z})|"
    by (rule card_of_ordIsoI)

  also have "|SIGMA X:FinPow A. Func X (B - {z})| =o cmax |A| |B|"
  proof (rule ordLeq_antisym)
    show "|SIGMA X:FinPow A. Func X (B - {z})| ≤o cmax |A| |B|"
    proof (intro card_of_Sigma_ordLeq_infinite_Field ballI)
      show "infinite (Field (cmax |A| |B| ))"
        using assms by (simp add: finite_cmax)
    next
      show "Card_order (cmax |A| |B| )"
        by (intro Card_order_cmax) auto
    next
      show "|FinPow A| ≤o cmax |A| |B|"
      proof (cases "finite A")
        assume "infinite A"
        hence "|FinPow A| =o |A|"
          by (rule card_of_FinPow_infinite)
        also have "|A| ≤o cmax |A| |B|"
          by (simp add: ordLeq_cmax)
        finally show ?thesis .
      next
        assume A: "finite A"
        have "finite (FinPow A)"
          using A by auto
        thus "|FinPow A| ≤o cmax |A| |B|"
          using A by (intro Cfinite_ordLeq_Cinfinite inf_cmax) auto
      qed
    next
      show "|Func X (B - {z})| ≤o cmax |A| |B|" if "X ∈ FinPow A" for X
      proof (cases "finite B")
        case True
        have "finite X"
          using that by (auto simp: FinPow_def)
        hence "finite (Func X (B - {z}))"
          using True by blast
        with inf_cmax show ?thesis
          by (intro Cfinite_ordLeq_Cinfinite) auto
      next
        case False
        have "|Func X (B - {z})| =o |B - {z}| ^c |X|"
          by (rule card_of_Func)
        also have "|B - {z}| ^c |X| ≤o |B - {z}|"
          by (rule cexp_infinite_finite_ordLeq) (use False that in ‹auto simp: FinPow_def›)
        also have "|B - {z}| =o |B|"
          using False by (simp add: infinite_card_of_diff_singl)
        also have "|B| ≤o cmax |A| |B|"
          by (simp add: ordLeq_cmax)
        finally show ?thesis .
      qed
    qed
  next
    have "cmax |A| |B| =o |A| *c |B - {z}|"
    proof (cases "|A| ≤o |B|")
      case False
      have "¬|B - {z}| =o czero"
        using ‹B - {z} ≠ {}› by (subst card_of_ordIso_czero_iff_empty) auto
      from False and assms have "infinite A"
        using ordLeq_finite_infinite by blast
      from False have "|B| ≤o |A|"
        by (simp add: ordLess_imp_ordLeq)
      have "|B - {z}| ≤o |B|"
        by (rule card_of_mono1) auto
      also note ‹|B| ≤o |A|›
      finally have "|A| *c |B - {z}| =o |A|"
        using ‹infinite A› ‹¬|B - {z}| =o czero› by (intro cprod_infinite1') auto
      moreover have "cmax |A| |B| =o |A|"
        using ‹|B| ≤o |A|› by (simp add: cmax1)
      ultimately show ?thesis
        using ordIso_symmetric ordIso_transitive by blast
    next
      case True
      from True and assms have "infinite B"
        using card_of_ordLeq_finite by blast
      have "|A| *c |B - {z}| =o |A| *c |B|"
        using ‹infinite B›  by (intro cprod_cong2) (simp add: infinite_card_of_diff_singl)
      also have "|A| *c |B| =o |B|"
        using True ‹infinite B› assms(3)
        by (simp add: card_of_ordIso_czero_iff_empty cprod_infinite2')
      also have "|B| =o cmax |A| |B|"
        using True by (meson card_of_Card_order cmax2 ordIso_symmetric)
      finally show ?thesis
        using ordIso_symmetric ordIso_transitive by blast
    qed
    also have "|A| *c |B - {z}| =o |A × (B - {z})|"
      by (metis Field_card_of card_of_refl cprod_def)
    also have "|A × (B - {z})| ≤o |SIGMA X:(λx. {x})`A. B - {z}|"
      by (intro card_of_Sigma_mono[of "λx. {x}"]) auto
    also have "|SIGMA X:(λx. {x})`A. B - {z}| =o |SIGMA X:(λx. {x})`A. Func X (B - {z})|"
    proof (rule card_of_Sigma_cong; safe)
      fix x assume x: "x ∈ A"
      have "|Func {x} (B - {z})| =o |B - {z}| ^c |{x}|"
        by (simp add: card_of_Func)
      also have "|B - {z}| ^c |{x}| =o |B - {z}| ^c BNF_Cardinal_Arithmetic.cone"
        by (intro cexp_cong2) (auto simp: single_cone)
      also have "|B - {z}| ^c Wellorder_Constructions.cone =o |B - {z}|"
        using card_of_Card_order cexp_cone by blast
      finally show "|B - {z}| =o |Func {x} (B - {z})|"
        using ordIso_symmetric by blast
    qed
    also have "|SIGMA X:(λx. {x})`A. Func X (B - {z})| ≤o |SIGMA X:FinPow A. Func X (B - {z})|"
      by (rule card_of_Sigma_mono) (auto simp: FinPow_def)
    finally show "cmax |A| |B| ≤o |SIGMA X:FinPow A. Func X (B - {z})|" .
  qed
  finally show ?thesis .
qed

end