1(* Title: HOL/Library/Countable_Set.thy 2 Author: Johannes H��lzl 3 Author: Andrei Popescu 4*) 5 6section \<open>Countable sets\<close> 7 8theory Countable_Set 9imports Countable Infinite_Set 10begin 11 12subsection \<open>Predicate for countable sets\<close> 13 14definition countable :: "'a set \<Rightarrow> bool" where 15 "countable S \<longleftrightarrow> (\<exists>f::'a \<Rightarrow> nat. inj_on f S)" 16 17lemma 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 21lemma countableI: "inj_on (f::'a \<Rightarrow> nat) S \<Longrightarrow> countable S" 22 by (auto simp: countable_def) 23 24lemma 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 27lemma 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 31lemma 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 34lemma countable_finite: "finite S \<Longrightarrow> countable S" 35 by (blast dest: finite_imp_inj_to_nat_seg countableI) 36 37lemma 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 40lemma 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 43lemma countable_iff_bij[simp]: "bij_betw f A B \<Longrightarrow> countable A \<longleftrightarrow> countable B" 44 by (blast intro: countableI_bij1 countableI_bij2) 45 46lemma countable_subset: "A \<subseteq> B \<Longrightarrow> countable B \<Longrightarrow> countable A" 47 by (auto simp: countable_def intro: subset_inj_on) 48 49lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)" 50 using countableI[of to_nat A] by auto 51 52subsection \<open>Enumerate a countable set\<close> 53 54lemma countableE_infinite: 55 assumes "countable S" "infinite S" 56 obtains e :: "'a \<Rightarrow> nat" where "bij_betw e S UNIV" 57proof - 58 obtain f :: "'a \<Rightarrow> nat" where "inj_on f S" 59 using \<open>countable S\<close> by (rule countableE) 60 then have "bij_betw f S (f`S)" 61 unfolding bij_betw_def by simp 62 moreover 63 from \<open>inj_on f S\<close> \<open>infinite S\<close> have inf_fS: "infinite (f`S)" 64 by (auto dest: finite_imageD) 65 then have "bij_betw (the_inv_into UNIV (enumerate (f`S))) (f`S) UNIV" 66 by (intro bij_betw_the_inv_into bij_enumerate) 67 ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) \<circ> f) S UNIV" 68 by (rule bij_betw_trans) 69 then show thesis .. 70qed 71 72lemma countable_enum_cases: 73 assumes "countable S" 74 obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}" 75 | (infinite) f :: "'a \<Rightarrow> nat" where "infinite S" "bij_betw f S UNIV" 76 using ex_bij_betw_finite_nat[of S] countableE_infinite \<open>countable S\<close> 77 by (cases "finite S") (auto simp add: atLeast0LessThan) 78 79definition to_nat_on :: "'a set \<Rightarrow> 'a \<Rightarrow> nat" where 80 "to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)" 81 82definition from_nat_into :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where 83 "from_nat_into S n = (if n \<in> to_nat_on S ` S then inv_into S (to_nat_on S) n else SOME s. s\<in>S)" 84 85lemma to_nat_on_finite: "finite S \<Longrightarrow> bij_betw (to_nat_on S) S {..< card S}" 86 using ex_bij_betw_finite_nat unfolding to_nat_on_def 87 by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S {..<card S}"]) (auto simp add: atLeast0LessThan) 88 89lemma to_nat_on_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (to_nat_on S) S UNIV" 90 using countableE_infinite unfolding to_nat_on_def 91 by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto 92 93lemma bij_betw_from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S" 94 unfolding from_nat_into_def[abs_def] 95 using to_nat_on_finite[of S] 96 apply (subst bij_betw_cong) 97 apply (split if_split) 98 apply (simp add: bij_betw_def) 99 apply (auto cong: bij_betw_cong 100 intro: bij_betw_inv_into to_nat_on_finite) 101 done 102 103lemma bij_betw_from_nat_into: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S" 104 unfolding from_nat_into_def[abs_def] 105 using to_nat_on_infinite[of S, unfolded bij_betw_def] 106 by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite) 107 108lemma countable_as_injective_image: 109 assumes "countable A" "infinite A" 110 obtains f :: "nat \<Rightarrow> 'a" where "A = range f" "inj f" 111by (metis bij_betw_def bij_betw_from_nat_into [OF assms]) 112 113lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A" 114 using to_nat_on_infinite[of A] to_nat_on_finite[of A] 115 by (cases "finite A") (auto simp: bij_betw_def) 116 117lemma to_nat_on_inj[simp]: 118 "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> to_nat_on A a = to_nat_on A b \<longleftrightarrow> a = b" 119 using inj_on_to_nat_on[of A] by (auto dest: inj_onD) 120 121lemma from_nat_into_to_nat_on[simp]: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> from_nat_into A (to_nat_on A a) = a" 122 by (auto simp: from_nat_into_def intro!: inv_into_f_f) 123 124lemma subset_range_from_nat_into: "countable A \<Longrightarrow> A \<subseteq> range (from_nat_into A)" 125 by (auto intro: from_nat_into_to_nat_on[symmetric]) 126 127lemma from_nat_into: "A \<noteq> {} \<Longrightarrow> from_nat_into A n \<in> A" 128 unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex) 129 130lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A" 131 using from_nat_into[of A] by auto 132 133lemma range_from_nat_into[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> range (from_nat_into A) = A" 134 by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into) 135 136lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV" 137 using to_nat_on_infinite[of A] by (simp add: bij_betw_def) 138 139lemma to_nat_on_surj: "countable A \<Longrightarrow> infinite A \<Longrightarrow> \<exists>a\<in>A. to_nat_on A a = n" 140 by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on) 141 142lemma to_nat_on_from_nat_into[simp]: "n \<in> to_nat_on A ` A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n" 143 by (simp add: f_inv_into_f from_nat_into_def) 144 145lemma to_nat_on_from_nat_into_infinite[simp]: 146 "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n" 147 by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into) 148 149lemma from_nat_into_inj: 150 "countable A \<Longrightarrow> m \<in> to_nat_on A ` A \<Longrightarrow> n \<in> to_nat_on A ` A \<Longrightarrow> 151 from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" 152 by (subst to_nat_on_inj[symmetric, of A]) auto 153 154lemma from_nat_into_inj_infinite[simp]: 155 "countable A \<Longrightarrow> infinite A \<Longrightarrow> from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" 156 using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp 157 158lemma eq_from_nat_into_iff: 159 "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> i \<in> to_nat_on A ` A \<Longrightarrow> x = from_nat_into A i \<longleftrightarrow> i = to_nat_on A x" 160 by auto 161 162lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a" 163 by (rule exI[of _ "to_nat_on A a"]) simp 164 165lemma from_nat_into_inject[simp]: 166 "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> countable B \<Longrightarrow> from_nat_into A = from_nat_into B \<longleftrightarrow> A = B" 167 by (metis range_from_nat_into) 168 169lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})" 170 unfolding inj_on_def by auto 171 172subsection \<open>Closure properties of countability\<close> 173 174lemma countable_SIGMA[intro, simp]: 175 "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)" 176 by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def) 177 178lemma countable_image[intro, simp]: 179 assumes "countable A" 180 shows "countable (f`A)" 181proof - 182 obtain g :: "'a \<Rightarrow> nat" where "inj_on g A" 183 using assms by (rule countableE) 184 moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A" 185 by (auto intro: inj_on_inv_into inv_into_into) 186 ultimately show ?thesis 187 by (blast dest: comp_inj_on subset_inj_on intro: countableI) 188qed 189 190lemma countable_image_inj_on: "countable (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> countable A" 191 by (metis countable_image the_inv_into_onto) 192 193lemma countable_UN[intro, simp]: 194 fixes I :: "'i set" and A :: "'i => 'a set" 195 assumes I: "countable I" 196 assumes A: "\<And>i. i \<in> I \<Longrightarrow> countable (A i)" 197 shows "countable (\<Union>i\<in>I. A i)" 198proof - 199 have "(\<Union>i\<in>I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff) 200 then show ?thesis by (simp add: assms) 201qed 202 203lemma countable_Un[intro]: "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A \<union> B)" 204 by (rule countable_UN[of "{True, False}" "\<lambda>True \<Rightarrow> A | False \<Rightarrow> B", simplified]) 205 (simp split: bool.split) 206 207lemma countable_Un_iff[simp]: "countable (A \<union> B) \<longleftrightarrow> countable A \<and> countable B" 208 by (metis countable_Un countable_subset inf_sup_ord(3,4)) 209 210lemma countable_Plus[intro, simp]: 211 "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A <+> B)" 212 by (simp add: Plus_def) 213 214lemma countable_empty[intro, simp]: "countable {}" 215 by (blast intro: countable_finite) 216 217lemma countable_insert[intro, simp]: "countable A \<Longrightarrow> countable (insert a A)" 218 using countable_Un[of "{a}" A] by (auto simp: countable_finite) 219 220lemma countable_Int1[intro, simp]: "countable A \<Longrightarrow> countable (A \<inter> B)" 221 by (force intro: countable_subset) 222 223lemma countable_Int2[intro, simp]: "countable B \<Longrightarrow> countable (A \<inter> B)" 224 by (blast intro: countable_subset) 225 226lemma countable_INT[intro, simp]: "i \<in> I \<Longrightarrow> countable (A i) \<Longrightarrow> countable (\<Inter>i\<in>I. A i)" 227 by (blast intro: countable_subset) 228 229lemma countable_Diff[intro, simp]: "countable A \<Longrightarrow> countable (A - B)" 230 by (blast intro: countable_subset) 231 232lemma countable_insert_eq [simp]: "countable (insert x A) = countable A" 233 by auto (metis Diff_insert_absorb countable_Diff insert_absorb) 234 235lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B" 236 by (metis Int_absorb2 countable_image image_vimage_eq) 237 238lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B" 239 by (metis countable_vimage top_greatest) 240 241lemma countable_Collect[simp]: "countable A \<Longrightarrow> countable {a \<in> A. \<phi> a}" 242 by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1) 243 244lemma countable_Image: 245 assumes "\<And>y. y \<in> Y \<Longrightarrow> countable (X `` {y})" 246 assumes "countable Y" 247 shows "countable (X `` Y)" 248proof - 249 have "countable (X `` (\<Union>y\<in>Y. {y}))" 250 unfolding Image_UN by (intro countable_UN assms) 251 then show ?thesis by simp 252qed 253 254lemma countable_relpow: 255 fixes X :: "'a rel" 256 assumes Image_X: "\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)" 257 assumes Y: "countable Y" 258 shows "countable ((X ^^ i) `` Y)" 259 using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X) 260 261lemma countable_funpow: 262 fixes f :: "'a set \<Rightarrow> 'a set" 263 assumes "\<And>A. countable A \<Longrightarrow> countable (f A)" 264 and "countable A" 265 shows "countable ((f ^^ n) A)" 266by(induction n)(simp_all add: assms) 267 268lemma countable_rtrancl: 269 "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X\<^sup>* `` Y)" 270 unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow) 271 272lemma countable_lists[intro, simp]: 273 assumes A: "countable A" shows "countable (lists A)" 274proof - 275 have "countable (lists (range (from_nat_into A)))" 276 by (auto simp: lists_image) 277 with A show ?thesis 278 by (auto dest: subset_range_from_nat_into countable_subset lists_mono) 279qed 280 281lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV" 282 using finite_list by auto 283 284lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))" 285 by (simp add: Collect_finite_eq_lists) 286 287lemma countable_int: "countable \<int>" 288 unfolding Ints_def by auto 289 290lemma countable_rat: "countable \<rat>" 291 unfolding Rats_def by auto 292 293lemma Collect_finite_subset_eq_lists: "{A. finite A \<and> A \<subseteq> T} = set ` lists T" 294 using finite_list by (auto simp: lists_eq_set) 295 296lemma countable_Collect_finite_subset: 297 "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}" 298 unfolding Collect_finite_subset_eq_lists by auto 299 300lemma countable_set_option [simp]: "countable (set_option x)" 301by(cases x) auto 302 303subsection \<open>Misc lemmas\<close> 304 305lemma countable_subset_image: 306 "countable B \<and> B \<subseteq> (f ` A) \<longleftrightarrow> (\<exists>A'. countable A' \<and> A' \<subseteq> A \<and> (B = f ` A'))" 307 (is "?lhs = ?rhs") 308proof 309 assume ?lhs 310 show ?rhs 311 by (rule exI [where x="inv_into A f ` B"]) 312 (use \<open>?lhs\<close> in \<open>auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into\<close>) 313next 314 assume ?rhs 315 then show ?lhs by force 316qed 317 318lemma infinite_countable_subset': 319 assumes X: "infinite X" shows "\<exists>C\<subseteq>X. countable C \<and> infinite C" 320proof - 321 from infinite_countable_subset[OF X] guess f .. 322 then show ?thesis 323 by (intro exI[of _ "range f"]) (auto simp: range_inj_infinite) 324qed 325 326lemma countable_all: 327 assumes S: "countable S" 328 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))" 329 using S[THEN subset_range_from_nat_into] by auto 330 331lemma finite_sequence_to_countable_set: 332 assumes "countable X" obtains F where "\<And>i. F i \<subseteq> X" "\<And>i. F i \<subseteq> F (Suc i)" "\<And>i. finite (F i)" "(\<Union>i. F i) = X" 333proof - show thesis 334 apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"]) 335 apply (auto simp: image_iff Ball_def intro: from_nat_into split: if_split_asm) 336 proof - 337 fix x n assume "x \<in> X" "\<forall>i m. m \<le> i \<longrightarrow> x \<noteq> from_nat_into X m" 338 with from_nat_into_surj[OF \<open>countable X\<close> \<open>x \<in> X\<close>] 339 show False 340 by auto 341 qed 342qed 343 344lemma transfer_countable[transfer_rule]: 345 "bi_unique R \<Longrightarrow> rel_fun (rel_set R) (=) countable countable" 346 by (rule rel_funI, erule (1) bi_unique_rel_set_lemma) 347 (auto dest: countable_image_inj_on) 348 349subsection \<open>Uncountable\<close> 350 351abbreviation uncountable where 352 "uncountable A \<equiv> \<not> countable A" 353 354lemma uncountable_def: "uncountable A \<longleftrightarrow> A \<noteq> {} \<and> \<not> (\<exists>f::(nat \<Rightarrow> 'a). range f = A)" 355 by (auto intro: inj_on_inv_into simp: countable_def) 356 (metis all_not_in_conv inj_on_iff_surj subset_UNIV) 357 358lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A" 359 unfolding bij_betw_def by (metis countable_image) 360 361lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A" 362 by (metis countable_finite) 363 364lemma uncountable_minus_countable: 365 "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)" 366 using countable_Un[of B "A - B"] by auto 367 368lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A" 369 by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable) 370 371end 372