# Theory Countable_Set

theory Countable_Set
imports Countable Infinite_Set
```(*  Title:      HOL/Library/Countable_Set.thy
Author:     Johannes Hölzl
Author:     Andrei Popescu
*)

section ‹Countable sets›

theory Countable_Set
imports Countable Infinite_Set
begin

subsection ‹Predicate for countable sets›

definition countable :: "'a set ⇒ bool" where
"countable S ⟷ (∃f::'a ⇒ nat. inj_on f S)"

lemma countableE:
assumes S: "countable S" obtains f :: "'a ⇒ nat" where "inj_on f S"
using S by (auto simp: countable_def)

lemma countableI: "inj_on (f::'a ⇒ nat) S ⟹ countable S"
by (auto simp: countable_def)

lemma countableI': "inj_on (f::'a ⇒ 'b::countable) S ⟹ countable S"
using comp_inj_on[of f S to_nat] by (auto intro: countableI)

lemma countableE_bij:
assumes S: "countable S" obtains f :: "nat ⇒ 'a" and C :: "nat set" where "bij_betw f C S"
using S by (blast elim: countableE dest: inj_on_imp_bij_betw bij_betw_inv)

lemma countableI_bij: "bij_betw f (C::nat set) S ⟹ countable S"
by (blast intro: countableI bij_betw_inv_into bij_betw_imp_inj_on)

lemma countable_finite: "finite S ⟹ countable S"
by (blast dest: finite_imp_inj_to_nat_seg countableI)

lemma countableI_bij1: "bij_betw f A B ⟹ countable A ⟹ countable B"
by (blast elim: countableE_bij intro: bij_betw_trans countableI_bij)

lemma countableI_bij2: "bij_betw f B A ⟹ countable A ⟹ countable B"
by (blast elim: countableE_bij intro: bij_betw_trans bij_betw_inv_into countableI_bij)

lemma countable_iff_bij[simp]: "bij_betw f A B ⟹ countable A ⟷ countable B"
by (blast intro: countableI_bij1 countableI_bij2)

lemma countable_subset: "A ⊆ B ⟹ countable B ⟹ countable A"
by (auto simp: countable_def intro: subset_inj_on)

lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)"
using countableI[of to_nat A] by auto

subsection ‹Enumerate a countable set›

lemma countableE_infinite:
assumes "countable S" "infinite S"
obtains e :: "'a ⇒ nat" where "bij_betw e S UNIV"
proof -
obtain f :: "'a ⇒ nat" where "inj_on f S"
using ‹countable S› by (rule countableE)
then have "bij_betw f S (f`S)"
unfolding bij_betw_def by simp
moreover
from ‹inj_on f S› ‹infinite S› have inf_fS: "infinite (f`S)"
by (auto dest: finite_imageD)
then have "bij_betw (the_inv_into UNIV (enumerate (f`S))) (f`S) UNIV"
by (intro bij_betw_the_inv_into bij_enumerate)
ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) ∘ f) S UNIV"
by (rule bij_betw_trans)
then show thesis ..
qed

lemma countable_enum_cases:
assumes "countable S"
obtains (finite) f :: "'a ⇒ nat" where "finite S" "bij_betw f S {..<card S}"
| (infinite) f :: "'a ⇒ nat" where "infinite S" "bij_betw f S UNIV"
using ex_bij_betw_finite_nat[of S] countableE_infinite ‹countable S›
by (cases "finite S") (auto simp add: atLeast0LessThan)

definition to_nat_on :: "'a set ⇒ 'a ⇒ nat" where
"to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)"

definition from_nat_into :: "'a set ⇒ nat ⇒ 'a" where
"from_nat_into S n = (if n ∈ to_nat_on S ` S then inv_into S (to_nat_on S) n else SOME s. s∈S)"

lemma to_nat_on_finite: "finite S ⟹ bij_betw (to_nat_on S) S {..< card S}"
using ex_bij_betw_finite_nat unfolding to_nat_on_def
by (intro someI2_ex[where Q="λf. bij_betw f S {..<card S}"]) (auto simp add: atLeast0LessThan)

lemma to_nat_on_infinite: "countable S ⟹ infinite S ⟹ bij_betw (to_nat_on S) S UNIV"
using countableE_infinite unfolding to_nat_on_def
by (intro someI2_ex[where Q="λf. bij_betw f S UNIV"]) auto

lemma bij_betw_from_nat_into_finite: "finite S ⟹ bij_betw (from_nat_into S) {..< card S} S"
unfolding from_nat_into_def[abs_def]
using to_nat_on_finite[of S]
apply (subst bij_betw_cong)
apply (split split_if)
apply (auto cong: bij_betw_cong
intro: bij_betw_inv_into to_nat_on_finite)
done

lemma bij_betw_from_nat_into: "countable S ⟹ infinite S ⟹ bij_betw (from_nat_into S) UNIV S"
unfolding from_nat_into_def[abs_def]
using to_nat_on_infinite[of S, unfolded bij_betw_def]
by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)

lemma inj_on_to_nat_on[intro]: "countable A ⟹ inj_on (to_nat_on A) A"
using to_nat_on_infinite[of A] to_nat_on_finite[of A]
by (cases "finite A") (auto simp: bij_betw_def)

lemma to_nat_on_inj[simp]:
"countable A ⟹ a ∈ A ⟹ b ∈ A ⟹ to_nat_on A a = to_nat_on A b ⟷ a = b"
using inj_on_to_nat_on[of A] by (auto dest: inj_onD)

lemma from_nat_into_to_nat_on[simp]: "countable A ⟹ a ∈ A ⟹ from_nat_into A (to_nat_on A a) = a"
by (auto simp: from_nat_into_def intro!: inv_into_f_f)

lemma subset_range_from_nat_into: "countable A ⟹ A ⊆ range (from_nat_into A)"
by (auto intro: from_nat_into_to_nat_on[symmetric])

lemma from_nat_into: "A ≠ {} ⟹ from_nat_into A n ∈ A"
unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex)

lemma range_from_nat_into_subset: "A ≠ {} ⟹ range (from_nat_into A) ⊆ A"
using from_nat_into[of A] by auto

lemma range_from_nat_into[simp]: "A ≠ {} ⟹ countable A ⟹ range (from_nat_into A) = A"
by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into)

lemma image_to_nat_on: "countable A ⟹ infinite A ⟹ to_nat_on A ` A = UNIV"
using to_nat_on_infinite[of A] by (simp add: bij_betw_def)

lemma to_nat_on_surj: "countable A ⟹ infinite A ⟹ ∃a∈A. to_nat_on A a = n"
by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on)

lemma to_nat_on_from_nat_into[simp]: "n ∈ to_nat_on A ` A ⟹ to_nat_on A (from_nat_into A n) = n"

lemma to_nat_on_from_nat_into_infinite[simp]:
"countable A ⟹ infinite A ⟹ to_nat_on A (from_nat_into A n) = n"
by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into)

lemma from_nat_into_inj:
"countable A ⟹ m ∈ to_nat_on A ` A ⟹ n ∈ to_nat_on A ` A ⟹
from_nat_into A m = from_nat_into A n ⟷ m = n"
by (subst to_nat_on_inj[symmetric, of A]) auto

lemma from_nat_into_inj_infinite[simp]:
"countable A ⟹ infinite A ⟹ from_nat_into A m = from_nat_into A n ⟷ m = n"
using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp

lemma eq_from_nat_into_iff:
"countable A ⟹ x ∈ A ⟹ i ∈ to_nat_on A ` A ⟹ x = from_nat_into A i ⟷ i = to_nat_on A x"
by auto

lemma from_nat_into_surj: "countable A ⟹ a ∈ A ⟹ ∃n. from_nat_into A n = a"
by (rule exI[of _ "to_nat_on A a"]) simp

lemma from_nat_into_inject[simp]:
"A ≠ {} ⟹ countable A ⟹ B ≠ {} ⟹ countable B ⟹ from_nat_into A = from_nat_into B ⟷ A = B"
by (metis range_from_nat_into)

lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A ≠ {} ∧ countable A})"
unfolding inj_on_def by auto

subsection ‹Closure properties of countability›

lemma countable_SIGMA[intro, simp]:
"countable I ⟹ (⋀i. i ∈ I ⟹ countable (A i)) ⟹ countable (SIGMA i : I. A i)"
by (intro countableI'[of "λ(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)

lemma countable_image[intro, simp]:
assumes "countable A"
shows "countable (f`A)"
proof -
obtain g :: "'a ⇒ nat" where "inj_on g A"
using assms by (rule countableE)
moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A ⊆ A"
by (auto intro: inj_on_inv_into inv_into_into)
ultimately show ?thesis
by (blast dest: comp_inj_on subset_inj_on intro: countableI)
qed

lemma countable_image_inj_on: "countable (f ` A) ⟹ inj_on f A ⟹ countable A"
by (metis countable_image the_inv_into_onto)

lemma countable_UN[intro, simp]:
fixes I :: "'i set" and A :: "'i => 'a set"
assumes I: "countable I"
assumes A: "⋀i. i ∈ I ⟹ countable (A i)"
shows "countable (⋃i∈I. A i)"
proof -
have "(⋃i∈I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff)
then show ?thesis by (simp add: assms)
qed

lemma countable_Un[intro]: "countable A ⟹ countable B ⟹ countable (A ∪ B)"
by (rule countable_UN[of "{True, False}" "λTrue ⇒ A | False ⇒ B", simplified])
(simp split: bool.split)

lemma countable_Un_iff[simp]: "countable (A ∪ B) ⟷ countable A ∧ countable B"
by (metis countable_Un countable_subset inf_sup_ord(3,4))

lemma countable_Plus[intro, simp]:
"countable A ⟹ countable B ⟹ countable (A <+> B)"

lemma countable_empty[intro, simp]: "countable {}"
by (blast intro: countable_finite)

lemma countable_insert[intro, simp]: "countable A ⟹ countable (insert a A)"
using countable_Un[of "{a}" A] by (auto simp: countable_finite)

lemma countable_Int1[intro, simp]: "countable A ⟹ countable (A ∩ B)"
by (force intro: countable_subset)

lemma countable_Int2[intro, simp]: "countable B ⟹ countable (A ∩ B)"
by (blast intro: countable_subset)

lemma countable_INT[intro, simp]: "i ∈ I ⟹ countable (A i) ⟹ countable (⋂i∈I. A i)"
by (blast intro: countable_subset)

lemma countable_Diff[intro, simp]: "countable A ⟹ countable (A - B)"
by (blast intro: countable_subset)

lemma countable_insert_eq [simp]: "countable (insert x A) = countable A"
by auto (metis Diff_insert_absorb countable_Diff insert_absorb)

lemma countable_vimage: "B ⊆ range f ⟹ countable (f -` B) ⟹ countable B"
by (metis Int_absorb2 assms countable_image image_vimage_eq)

lemma surj_countable_vimage: "surj f ⟹ countable (f -` B) ⟹ countable B"
by (metis countable_vimage top_greatest)

lemma countable_Collect[simp]: "countable A ⟹ countable {a ∈ A. φ a}"
by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1)

lemma countable_Image:
assumes "⋀y. y ∈ Y ⟹ countable (X `` {y})"
assumes "countable Y"
shows "countable (X `` Y)"
proof -
have "countable (X `` (⋃y∈Y. {y}))"
unfolding Image_UN by (intro countable_UN assms)
then show ?thesis by simp
qed

lemma countable_relpow:
fixes X :: "'a rel"
assumes Image_X: "⋀Y. countable Y ⟹ countable (X `` Y)"
assumes Y: "countable Y"
shows "countable ((X ^^ i) `` Y)"
using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X)

lemma countable_funpow:
fixes f :: "'a set ⇒ 'a set"
assumes "⋀A. countable A ⟹ countable (f A)"
and "countable A"
shows "countable ((f ^^ n) A)"

lemma countable_rtrancl:
"(⋀Y. countable Y ⟹ countable (X `` Y)) ⟹ countable Y ⟹ countable (X^* `` Y)"
unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)

lemma countable_lists[intro, simp]:
assumes A: "countable A" shows "countable (lists A)"
proof -
have "countable (lists (range (from_nat_into A)))"
by (auto simp: lists_image)
with A show ?thesis
by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
qed

lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV"
using finite_list by auto

lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set⇒bool))"

lemma countable_rat: "countable ℚ"
unfolding Rats_def by auto

lemma Collect_finite_subset_eq_lists: "{A. finite A ∧ A ⊆ T} = set ` lists T"
using finite_list by (auto simp: lists_eq_set)

lemma countable_Collect_finite_subset:
"countable T ⟹ countable {A. finite A ∧ A ⊆ T}"
unfolding Collect_finite_subset_eq_lists by auto

lemma countable_set_option [simp]: "countable (set_option x)"
by(cases x) auto

subsection ‹Misc lemmas›

lemma countable_all:
assumes S: "countable S"
shows "(∀s∈S. P s) ⟷ (∀n::nat. from_nat_into S n ∈ S ⟶ P (from_nat_into S n))"
using S[THEN subset_range_from_nat_into] by auto

lemma finite_sequence_to_countable_set:
assumes "countable X" obtains F where "⋀i. F i ⊆ X" "⋀i. F i ⊆ F (Suc i)" "⋀i. finite (F i)" "(⋃i. F i) = X"
proof -  show thesis
apply (rule that[of "λi. if X = {} then {} else from_nat_into X ` {..i}"])
apply (auto simp: image_iff Ball_def intro: from_nat_into split: split_if_asm)
proof -
fix x n assume "x ∈ X" "∀i m. m ≤ i ⟶ x ≠ from_nat_into X m"
with from_nat_into_surj[OF ‹countable X› ‹x ∈ X›]
show False
by auto
qed
qed

subsection ‹Uncountable›

abbreviation uncountable where
"uncountable A ≡ ¬ countable A"

lemma uncountable_def: "uncountable A ⟷ A ≠ {} ∧ ¬ (∃f::(nat ⇒ 'a). range f = A)"
by (auto intro: inj_on_inv_into simp: countable_def)
(metis all_not_in_conv inj_on_iff_surj subset_UNIV)

lemma uncountable_bij_betw: "bij_betw f A B ⟹ uncountable B ⟹ uncountable A"
unfolding bij_betw_def by (metis countable_image)

lemma uncountable_infinite: "uncountable A ⟹ infinite A"
by (metis countable_finite)

lemma uncountable_minus_countable:
"uncountable A ⟹ countable B ⟹ uncountable (A - B)"
using countable_Un[of B "A - B"] assms by auto

lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"
by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable)

end
```