# 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