50134

1 
(* Title: HOL/Library/Countable_Set.thy


2 
Author: Johannes Hölzl


3 
Author: Andrei Popescu


4 
*)


5 


6 
header {* Countable sets *}


7 


8 
theory Countable_Set


9 
imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Infinite_Set"


10 
begin


11 


12 
subsection {* Predicate for countable sets *}


13 


14 
definition countable :: "'a set \<Rightarrow> bool" where


15 
"countable S \<longleftrightarrow> (\<exists>f::'a \<Rightarrow> nat. inj_on f S)"


16 


17 
lemma countableE:


18 
assumes S: "countable S" obtains f :: "'a \<Rightarrow> nat" where "inj_on f S"


19 
using S by (auto simp: countable_def)


20 


21 
lemma countableI: "inj_on (f::'a \<Rightarrow> nat) S \<Longrightarrow> countable S"


22 
by (auto simp: countable_def)


23 


24 
lemma countableI': "inj_on (f::'a \<Rightarrow> 'b::countable) S \<Longrightarrow> countable S"


25 
using comp_inj_on[of f S to_nat] by (auto intro: countableI)


26 


27 
lemma countableE_bij:


28 
assumes S: "countable S" obtains f :: "nat \<Rightarrow> 'a" and C :: "nat set" where "bij_betw f C S"


29 
using S by (blast elim: countableE dest: inj_on_imp_bij_betw bij_betw_inv)


30 


31 
lemma countableI_bij: "bij_betw f (C::nat set) S \<Longrightarrow> countable S"


32 
by (blast intro: countableI bij_betw_inv_into bij_betw_imp_inj_on)


33 


34 
lemma countable_finite: "finite S \<Longrightarrow> countable S"


35 
by (blast dest: finite_imp_inj_to_nat_seg countableI)


36 


37 
lemma countableI_bij1: "bij_betw f A B \<Longrightarrow> countable A \<Longrightarrow> countable B"


38 
by (blast elim: countableE_bij intro: bij_betw_trans countableI_bij)


39 


40 
lemma countableI_bij2: "bij_betw f B A \<Longrightarrow> countable A \<Longrightarrow> countable B"


41 
by (blast elim: countableE_bij intro: bij_betw_trans bij_betw_inv_into countableI_bij)


42 


43 
lemma countable_iff_bij[simp]: "bij_betw f A B \<Longrightarrow> countable A \<longleftrightarrow> countable B"


44 
by (blast intro: countableI_bij1 countableI_bij2)


45 


46 
lemma countable_subset: "A \<subseteq> B \<Longrightarrow> countable B \<Longrightarrow> countable A"


47 
by (auto simp: countable_def intro: subset_inj_on)


48 


49 
lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)"


50 
using countableI[of to_nat A] by auto


51 


52 
subsection {* Enumerate a countable set *}


53 


54 
lemma countableE_infinite:


55 
assumes "countable S" "infinite S"


56 
obtains e :: "'a \<Rightarrow> nat" where "bij_betw e S UNIV"


57 
proof 


58 
from `countable S`[THEN countableE] guess f .


59 
then have "bij_betw f S (f`S)"


60 
unfolding bij_betw_def by simp


61 
moreover


62 
from `inj_on f S` `infinite S` have inf_fS: "infinite (f`S)"


63 
by (auto dest: finite_imageD)


64 
then have "bij_betw (the_inv_into UNIV (enumerate (f`S))) (f`S) UNIV"


65 
by (intro bij_betw_the_inv_into bij_enumerate)


66 
ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) \<circ> f) S UNIV"


67 
by (rule bij_betw_trans)


68 
then show thesis ..


69 
qed


70 


71 
lemma countable_enum_cases:


72 
assumes "countable S"


73 
obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}"


74 
 (infinite) f :: "'a \<Rightarrow> nat" where "infinite S" "bij_betw f S UNIV"


75 
using ex_bij_betw_finite_nat[of S] countableE_infinite `countable S`


76 
by (cases "finite S") (auto simp add: atLeast0LessThan)


77 


78 
definition to_nat_on :: "'a set \<Rightarrow> 'a \<Rightarrow> nat" where


79 
"to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)"


80 


81 
definition from_nat_into :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where


82 
"from_nat_into S = inv_into S (to_nat_on S)"


83 


84 
lemma to_nat_on_finite: "finite S \<Longrightarrow> bij_betw (to_nat_on S) S {..< card S}"


85 
using ex_bij_betw_finite_nat unfolding to_nat_on_def


86 
by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S {..<card S}"]) (auto simp add: atLeast0LessThan)


87 


88 
lemma to_nat_on_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (to_nat_on S) S UNIV"


89 
using countableE_infinite unfolding to_nat_on_def


90 
by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto


91 


92 
lemma from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"


93 
by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_finite)


94 


95 
lemma from_nat_into_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"


96 
by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_infinite)


97 


98 
lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A"


99 
using to_nat_on_infinite[of A] to_nat_on_finite[of A]


100 
by (cases "finite A") (auto simp: bij_betw_def)


101 


102 
lemma to_nat_on_inj[simp]:


103 
"countable A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> to_nat_on A a = to_nat_on A b \<longleftrightarrow> a = b"


104 
using inj_on_to_nat_on[of A] by (auto dest: inj_onD)


105 


106 
lemma from_nat_into_to_nat_on: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> from_nat_into A (to_nat_on A a) = a"


107 
by (auto simp: from_nat_into_def intro!: inv_into_f_f)


108 


109 
lemma subset_range_from_nat_into: "countable A \<Longrightarrow> A \<subseteq> range (from_nat_into A)"


110 
by (auto intro: from_nat_into_to_nat_on[symmetric])


111 


112 
subsection {* Closure properties of countability *}


113 


114 
lemma countable_SIGMA[intro, simp]:


115 
"countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"


116 
by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)


117 


118 
lemma countable_image[intro, simp]: assumes A: "countable A" shows "countable (f`A)"


119 
proof 


120 
from A guess g by (rule countableE)


121 
moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"


122 
by (auto intro: inj_on_inv_into inv_into_into)


123 
ultimately show ?thesis


124 
by (blast dest: comp_inj_on subset_inj_on intro: countableI)


125 
qed


126 


127 
lemma countable_UN[intro, simp]:


128 
fixes I :: "'i set" and A :: "'i => 'a set"


129 
assumes I: "countable I"


130 
assumes A: "\<And>i. i \<in> I \<Longrightarrow> countable (A i)"


131 
shows "countable (\<Union>i\<in>I. A i)"


132 
proof 


133 
have "(\<Union>i\<in>I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff)


134 
then show ?thesis by (simp add: assms)


135 
qed


136 


137 
lemma countable_Un[intro]: "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A \<union> B)"


138 
by (rule countable_UN[of "{True, False}" "\<lambda>True \<Rightarrow> A  False \<Rightarrow> B", simplified])


139 
(simp split: bool.split)


140 


141 
lemma countable_Un_iff[simp]: "countable (A \<union> B) \<longleftrightarrow> countable A \<and> countable B"


142 
by (metis countable_Un countable_subset inf_sup_ord(3,4))


143 


144 
lemma countable_Plus[intro, simp]:


145 
"countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A <+> B)"


146 
by (simp add: Plus_def)


147 


148 
lemma countable_empty[intro, simp]: "countable {}"


149 
by (blast intro: countable_finite)


150 


151 
lemma countable_insert[intro, simp]: "countable A \<Longrightarrow> countable (insert a A)"


152 
using countable_Un[of "{a}" A] by (auto simp: countable_finite)


153 


154 
lemma countable_Int1[intro, simp]: "countable A \<Longrightarrow> countable (A \<inter> B)"


155 
by (force intro: countable_subset)


156 


157 
lemma countable_Int2[intro, simp]: "countable B \<Longrightarrow> countable (A \<inter> B)"


158 
by (blast intro: countable_subset)


159 


160 
lemma countable_INT[intro, simp]: "i \<in> I \<Longrightarrow> countable (A i) \<Longrightarrow> countable (\<Inter>i\<in>I. A i)"


161 
by (blast intro: countable_subset)


162 


163 
lemma countable_Diff[intro, simp]: "countable A \<Longrightarrow> countable (A  B)"


164 
by (blast intro: countable_subset)


165 


166 
lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f ` B) \<Longrightarrow> countable B"


167 
by (metis Int_absorb2 assms countable_image image_vimage_eq)


168 


169 
lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f ` B) \<Longrightarrow> countable B"


170 
by (metis countable_vimage top_greatest)


171 


172 
lemma countable_lists[intro, simp]:


173 
assumes A: "countable A" shows "countable (lists A)"


174 
proof 


175 
have "countable (lists (range (from_nat_into A)))"


176 
by (auto simp: lists_image)


177 
with A show ?thesis


178 
by (auto dest: subset_range_from_nat_into countable_subset lists_mono)


179 
qed


180 


181 
subsection {* Misc lemmas *}


182 


183 
lemma countable_all:


184 
assumes S: "countable S"


185 
shows "(\<forall>s\<in>S. P s) \<longleftrightarrow> (\<forall>n::nat. from_nat_into S n \<in> S \<longrightarrow> P (from_nat_into S n))"


186 
using S[THEN subset_range_from_nat_into] by auto


187 


188 
end
