Theory ZFC_in_HOL.ZFC_Library

theory ZFC_Library
  imports "HOL-Library.Countable_Set" "HOL-Library.Equipollence" "HOL-Cardinals.Cardinals"

begin

text‹Equipollence and Lists.›

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

lemma infinite_times_eqpoll_self:
  assumes "infinite A" shows "A × A ≈ A"
  by (simp add: Times_same_infinite_bij_betw assms eqpoll_def)

lemma infinite_finite_times_lepoll_self:
  assumes "infinite A" "finite B" shows "A × B ≲ A"
proof -
  have "B ≲ A"
    by (simp add: assms finite_lepoll_infinite)
  then have "A × B ≲ A × A"
    by (simp add: subset_imp_lepoll times_lepoll_mono)
  also have "… ≈ A"
    by (simp add: ‹infinite A› infinite_times_eqpoll_self)
  finally show ?thesis .
qed

lemma lists_n_lepoll_self:
  assumes "infinite A" shows "{l ∈ lists A. length l = n} ≲ A"
proof (induction n)
  case 0
  have "{l ∈ lists A. length l = 0} = {[]}"
    by auto
  then show ?case
    by (metis Set.set_insert assms ex_in_conv finite.emptyI singleton_lepoll)
next
  case (Suc n)
  have "{l ∈ lists A. length l = Suc n} = (⋃x∈A. ⋃l ∈ {l ∈ lists A. length l = n}. {x#l})"
    by (auto simp: length_Suc_conv)
  also have "… ≲ A × {l ∈ lists A. length l = n}"
    unfolding lepoll_iff
    by (rule_tac x="λ(x,l). Cons x l" in exI) auto
  also have "… ≲ A"
  proof (cases "finite {l ∈ lists A. length l = n}")
    case True
    then show ?thesis
      using assms infinite_finite_times_lepoll_self by blast
  next
    case False
    have "A × {l ∈ lists A. length l = n} ≲ A × A"
      by (simp add: Suc.IH subset_imp_lepoll times_lepoll_mono)
    also have "… ≈ A"
      by (simp add: assms infinite_times_eqpoll_self)
    finally show ?thesis .
  qed
  finally show ?case .
qed

lemma infinite_eqpoll_lists:
    assumes "infinite A" shows "lists A ≈ A"
proof -
  have "lists A ≲ Sigma UNIV (λn. {l ∈ lists A. length l = n})"
    unfolding lepoll_iff
    by (rule_tac x=snd in exI) (auto simp: in_listsI snd_image_Sigma)
  also have "… ≲ (UNIV::nat set) × A"
    by (rule Sigma_lepoll_mono) (auto simp: lists_n_lepoll_self assms)
  also have "… ≲ A × A"
    by (metis assms infinite_le_lepoll order_refl subset_imp_lepoll times_lepoll_mono)
  also have "… ≈ A"
    by (simp add: assms infinite_times_eqpoll_self)
  finally show ?thesis
    by (simp add: lepoll_antisym lepoll_lists)
qed

end