src/HOL/Library/Countable_Set.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 60500 903bb1495239
child 62370 4a35e3945cab
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Library/Countable_Set.thy
     2     Author:     Johannes Hölzl
     3     Author:     Andrei Popescu
     4 *)
     5 
     6 section \<open>Countable sets\<close>
     7 
     8 theory Countable_Set
     9 imports Countable Infinite_Set
    10 begin
    11 
    12 subsection \<open>Predicate for countable sets\<close>
    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 \<open>Enumerate a countable set\<close>
    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   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 ..
    70 qed
    71 
    72 lemma 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 
    79 definition 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 
    82 definition 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 
    85 lemma 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 
    89 lemma 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 
    93 lemma 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 split_if)
    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 
   103 lemma 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 
   108 lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A"
   109   using to_nat_on_infinite[of A] to_nat_on_finite[of A]
   110   by (cases "finite A") (auto simp: bij_betw_def)
   111 
   112 lemma to_nat_on_inj[simp]:
   113   "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> to_nat_on A a = to_nat_on A b \<longleftrightarrow> a = b"
   114   using inj_on_to_nat_on[of A] by (auto dest: inj_onD)
   115 
   116 lemma from_nat_into_to_nat_on[simp]: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> from_nat_into A (to_nat_on A a) = a"
   117   by (auto simp: from_nat_into_def intro!: inv_into_f_f)
   118 
   119 lemma subset_range_from_nat_into: "countable A \<Longrightarrow> A \<subseteq> range (from_nat_into A)"
   120   by (auto intro: from_nat_into_to_nat_on[symmetric])
   121 
   122 lemma from_nat_into: "A \<noteq> {} \<Longrightarrow> from_nat_into A n \<in> A"
   123   unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex)
   124 
   125 lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A"
   126   using from_nat_into[of A] by auto
   127 
   128 lemma range_from_nat_into[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> range (from_nat_into A) = A"
   129   by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into)
   130 
   131 lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV"
   132   using to_nat_on_infinite[of A] by (simp add: bij_betw_def)
   133 
   134 lemma to_nat_on_surj: "countable A \<Longrightarrow> infinite A \<Longrightarrow> \<exists>a\<in>A. to_nat_on A a = n"
   135   by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on)
   136 
   137 lemma 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"
   138   by (simp add: f_inv_into_f from_nat_into_def)
   139 
   140 lemma to_nat_on_from_nat_into_infinite[simp]:
   141   "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
   142   by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into)
   143 
   144 lemma from_nat_into_inj:
   145   "countable A \<Longrightarrow> m \<in> to_nat_on A ` A \<Longrightarrow> n \<in> to_nat_on A ` A \<Longrightarrow>
   146     from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
   147   by (subst to_nat_on_inj[symmetric, of A]) auto
   148 
   149 lemma from_nat_into_inj_infinite[simp]:
   150   "countable A \<Longrightarrow> infinite A \<Longrightarrow> from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
   151   using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp
   152 
   153 lemma eq_from_nat_into_iff:
   154   "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"
   155   by auto
   156 
   157 lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a"
   158   by (rule exI[of _ "to_nat_on A a"]) simp
   159 
   160 lemma from_nat_into_inject[simp]:
   161   "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> countable B \<Longrightarrow> from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
   162   by (metis range_from_nat_into)
   163 
   164 lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})"
   165   unfolding inj_on_def by auto
   166 
   167 subsection \<open>Closure properties of countability\<close>
   168 
   169 lemma countable_SIGMA[intro, simp]:
   170   "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"
   171   by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)
   172 
   173 lemma countable_image[intro, simp]:
   174   assumes "countable A"
   175   shows "countable (f`A)"
   176 proof -
   177   obtain g :: "'a \<Rightarrow> nat" where "inj_on g A"
   178     using assms by (rule countableE)
   179   moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
   180     by (auto intro: inj_on_inv_into inv_into_into)
   181   ultimately show ?thesis
   182     by (blast dest: comp_inj_on subset_inj_on intro: countableI)
   183 qed
   184 
   185 lemma countable_image_inj_on: "countable (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> countable A"
   186   by (metis countable_image the_inv_into_onto)
   187 
   188 lemma countable_UN[intro, simp]:
   189   fixes I :: "'i set" and A :: "'i => 'a set"
   190   assumes I: "countable I"
   191   assumes A: "\<And>i. i \<in> I \<Longrightarrow> countable (A i)"
   192   shows "countable (\<Union>i\<in>I. A i)"
   193 proof -
   194   have "(\<Union>i\<in>I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff)
   195   then show ?thesis by (simp add: assms)
   196 qed
   197 
   198 lemma countable_Un[intro]: "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A \<union> B)"
   199   by (rule countable_UN[of "{True, False}" "\<lambda>True \<Rightarrow> A | False \<Rightarrow> B", simplified])
   200      (simp split: bool.split)
   201 
   202 lemma countable_Un_iff[simp]: "countable (A \<union> B) \<longleftrightarrow> countable A \<and> countable B"
   203   by (metis countable_Un countable_subset inf_sup_ord(3,4))
   204 
   205 lemma countable_Plus[intro, simp]:
   206   "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A <+> B)"
   207   by (simp add: Plus_def)
   208 
   209 lemma countable_empty[intro, simp]: "countable {}"
   210   by (blast intro: countable_finite)
   211 
   212 lemma countable_insert[intro, simp]: "countable A \<Longrightarrow> countable (insert a A)"
   213   using countable_Un[of "{a}" A] by (auto simp: countable_finite)
   214 
   215 lemma countable_Int1[intro, simp]: "countable A \<Longrightarrow> countable (A \<inter> B)"
   216   by (force intro: countable_subset)
   217 
   218 lemma countable_Int2[intro, simp]: "countable B \<Longrightarrow> countable (A \<inter> B)"
   219   by (blast intro: countable_subset)
   220 
   221 lemma countable_INT[intro, simp]: "i \<in> I \<Longrightarrow> countable (A i) \<Longrightarrow> countable (\<Inter>i\<in>I. A i)"
   222   by (blast intro: countable_subset)
   223 
   224 lemma countable_Diff[intro, simp]: "countable A \<Longrightarrow> countable (A - B)"
   225   by (blast intro: countable_subset)
   226 
   227 lemma countable_insert_eq [simp]: "countable (insert x A) = countable A"
   228     by auto (metis Diff_insert_absorb countable_Diff insert_absorb)
   229 
   230 lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
   231   by (metis Int_absorb2 assms countable_image image_vimage_eq)
   232 
   233 lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
   234   by (metis countable_vimage top_greatest)
   235 
   236 lemma countable_Collect[simp]: "countable A \<Longrightarrow> countable {a \<in> A. \<phi> a}"
   237   by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1)
   238 
   239 lemma countable_Image:
   240   assumes "\<And>y. y \<in> Y \<Longrightarrow> countable (X `` {y})"
   241   assumes "countable Y"
   242   shows "countable (X `` Y)"
   243 proof -
   244   have "countable (X `` (\<Union>y\<in>Y. {y}))"
   245     unfolding Image_UN by (intro countable_UN assms)
   246   then show ?thesis by simp
   247 qed
   248 
   249 lemma countable_relpow:
   250   fixes X :: "'a rel"
   251   assumes Image_X: "\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)"
   252   assumes Y: "countable Y"
   253   shows "countable ((X ^^ i) `` Y)"
   254   using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X)
   255 
   256 lemma countable_funpow:
   257   fixes f :: "'a set \<Rightarrow> 'a set"
   258   assumes "\<And>A. countable A \<Longrightarrow> countable (f A)"
   259   and "countable A"
   260   shows "countable ((f ^^ n) A)"
   261 by(induction n)(simp_all add: assms)
   262 
   263 lemma countable_rtrancl:
   264   "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)"
   265   unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)
   266 
   267 lemma countable_lists[intro, simp]:
   268   assumes A: "countable A" shows "countable (lists A)"
   269 proof -
   270   have "countable (lists (range (from_nat_into A)))"
   271     by (auto simp: lists_image)
   272   with A show ?thesis
   273     by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
   274 qed
   275 
   276 lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV"
   277   using finite_list by auto
   278 
   279 lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))"
   280   by (simp add: Collect_finite_eq_lists)
   281 
   282 lemma countable_rat: "countable \<rat>"
   283   unfolding Rats_def by auto
   284 
   285 lemma Collect_finite_subset_eq_lists: "{A. finite A \<and> A \<subseteq> T} = set ` lists T"
   286   using finite_list by (auto simp: lists_eq_set)
   287 
   288 lemma countable_Collect_finite_subset:
   289   "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
   290   unfolding Collect_finite_subset_eq_lists by auto
   291 
   292 lemma countable_set_option [simp]: "countable (set_option x)"
   293 by(cases x) auto
   294 
   295 subsection \<open>Misc lemmas\<close>
   296 
   297 lemma countable_all:
   298   assumes S: "countable S"
   299   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))"
   300   using S[THEN subset_range_from_nat_into] by auto
   301 
   302 lemma finite_sequence_to_countable_set:
   303    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"
   304 proof -  show thesis
   305     apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"])
   306     apply (auto simp: image_iff Ball_def intro: from_nat_into split: split_if_asm)
   307   proof -
   308     fix x n assume "x \<in> X" "\<forall>i m. m \<le> i \<longrightarrow> x \<noteq> from_nat_into X m"
   309     with from_nat_into_surj[OF \<open>countable X\<close> \<open>x \<in> X\<close>]
   310     show False
   311       by auto
   312   qed
   313 qed
   314 
   315 subsection \<open>Uncountable\<close>
   316 
   317 abbreviation uncountable where
   318   "uncountable A \<equiv> \<not> countable A"
   319 
   320 lemma uncountable_def: "uncountable A \<longleftrightarrow> A \<noteq> {} \<and> \<not> (\<exists>f::(nat \<Rightarrow> 'a). range f = A)"
   321   by (auto intro: inj_on_inv_into simp: countable_def)
   322      (metis all_not_in_conv inj_on_iff_surj subset_UNIV)
   323 
   324 lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A"
   325   unfolding bij_betw_def by (metis countable_image)
   326   
   327 lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A"
   328   by (metis countable_finite)
   329   
   330 lemma uncountable_minus_countable:
   331   "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
   332   using countable_Un[of B "A - B"] assms by auto
   333 
   334 lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"
   335   by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable)
   336 
   337 end