src/HOL/Library/Countable_Set.thy
changeset 50134 13211e07d931
child 50144 885deccc264e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Countable_Set.thy	Tue Nov 20 18:59:35 2012 +0100
     1.3 @@ -0,0 +1,188 @@
     1.4 +(*  Title:      HOL/Library/Countable_Set.thy
     1.5 +    Author:     Johannes Hölzl
     1.6 +    Author:     Andrei Popescu
     1.7 +*)
     1.8 +
     1.9 +header {* Countable sets *}
    1.10 +
    1.11 +theory Countable_Set
    1.12 +  imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Infinite_Set"
    1.13 +begin
    1.14 +
    1.15 +subsection {* Predicate for countable sets *}
    1.16 +
    1.17 +definition countable :: "'a set \<Rightarrow> bool" where
    1.18 +  "countable S \<longleftrightarrow> (\<exists>f::'a \<Rightarrow> nat. inj_on f S)"
    1.19 +
    1.20 +lemma countableE:
    1.21 +  assumes S: "countable S" obtains f :: "'a \<Rightarrow> nat" where "inj_on f S"
    1.22 +  using S by (auto simp: countable_def)
    1.23 +
    1.24 +lemma countableI: "inj_on (f::'a \<Rightarrow> nat) S \<Longrightarrow> countable S"
    1.25 +  by (auto simp: countable_def)
    1.26 +
    1.27 +lemma countableI': "inj_on (f::'a \<Rightarrow> 'b::countable) S \<Longrightarrow> countable S"
    1.28 +  using comp_inj_on[of f S to_nat] by (auto intro: countableI)
    1.29 +
    1.30 +lemma countableE_bij:
    1.31 +  assumes S: "countable S" obtains f :: "nat \<Rightarrow> 'a" and C :: "nat set" where "bij_betw f C S"
    1.32 +  using S by (blast elim: countableE dest: inj_on_imp_bij_betw bij_betw_inv)
    1.33 +
    1.34 +lemma countableI_bij: "bij_betw f (C::nat set) S \<Longrightarrow> countable S"
    1.35 +  by (blast intro: countableI bij_betw_inv_into bij_betw_imp_inj_on)
    1.36 +
    1.37 +lemma countable_finite: "finite S \<Longrightarrow> countable S"
    1.38 +  by (blast dest: finite_imp_inj_to_nat_seg countableI)
    1.39 +
    1.40 +lemma countableI_bij1: "bij_betw f A B \<Longrightarrow> countable A \<Longrightarrow> countable B"
    1.41 +  by (blast elim: countableE_bij intro: bij_betw_trans countableI_bij)
    1.42 +
    1.43 +lemma countableI_bij2: "bij_betw f B A \<Longrightarrow> countable A \<Longrightarrow> countable B"
    1.44 +  by (blast elim: countableE_bij intro: bij_betw_trans bij_betw_inv_into countableI_bij)
    1.45 +
    1.46 +lemma countable_iff_bij[simp]: "bij_betw f A B \<Longrightarrow> countable A \<longleftrightarrow> countable B"
    1.47 +  by (blast intro: countableI_bij1 countableI_bij2)
    1.48 +
    1.49 +lemma countable_subset: "A \<subseteq> B \<Longrightarrow> countable B \<Longrightarrow> countable A"
    1.50 +  by (auto simp: countable_def intro: subset_inj_on)
    1.51 +
    1.52 +lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)"
    1.53 +  using countableI[of to_nat A] by auto
    1.54 +
    1.55 +subsection {* Enumerate a countable set *}
    1.56 +
    1.57 +lemma countableE_infinite:
    1.58 +  assumes "countable S" "infinite S"
    1.59 +  obtains e :: "'a \<Rightarrow> nat" where "bij_betw e S UNIV"
    1.60 +proof -
    1.61 +  from `countable S`[THEN countableE] guess f .
    1.62 +  then have "bij_betw f S (f`S)"
    1.63 +    unfolding bij_betw_def by simp
    1.64 +  moreover
    1.65 +  from `inj_on f S` `infinite S` have inf_fS: "infinite (f`S)"
    1.66 +    by (auto dest: finite_imageD)
    1.67 +  then have "bij_betw (the_inv_into UNIV (enumerate (f`S))) (f`S) UNIV"
    1.68 +    by (intro bij_betw_the_inv_into bij_enumerate)
    1.69 +  ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) \<circ> f) S UNIV"
    1.70 +    by (rule bij_betw_trans)
    1.71 +  then show thesis ..
    1.72 +qed
    1.73 +
    1.74 +lemma countable_enum_cases:
    1.75 +  assumes "countable S"
    1.76 +  obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}"
    1.77 +        | (infinite) f :: "'a \<Rightarrow> nat" where "infinite S" "bij_betw f S UNIV"
    1.78 +  using ex_bij_betw_finite_nat[of S] countableE_infinite `countable S`
    1.79 +  by (cases "finite S") (auto simp add: atLeast0LessThan)
    1.80 +
    1.81 +definition to_nat_on :: "'a set \<Rightarrow> 'a \<Rightarrow> nat" where
    1.82 +  "to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)"
    1.83 +
    1.84 +definition from_nat_into :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
    1.85 +  "from_nat_into S = inv_into S (to_nat_on S)"
    1.86 +
    1.87 +lemma to_nat_on_finite: "finite S \<Longrightarrow> bij_betw (to_nat_on S) S {..< card S}"
    1.88 +  using ex_bij_betw_finite_nat unfolding to_nat_on_def
    1.89 +  by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S {..<card S}"]) (auto simp add: atLeast0LessThan)
    1.90 +
    1.91 +lemma to_nat_on_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (to_nat_on S) S UNIV"
    1.92 +  using countableE_infinite unfolding to_nat_on_def
    1.93 +  by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto
    1.94 +
    1.95 +lemma from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
    1.96 +  by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_finite)
    1.97 +
    1.98 +lemma from_nat_into_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
    1.99 +  by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_infinite)
   1.100 +
   1.101 +lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A"
   1.102 +  using to_nat_on_infinite[of A] to_nat_on_finite[of A]
   1.103 +  by (cases "finite A") (auto simp: bij_betw_def)
   1.104 +
   1.105 +lemma to_nat_on_inj[simp]:
   1.106 +  "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> to_nat_on A a = to_nat_on A b \<longleftrightarrow> a = b"
   1.107 +  using inj_on_to_nat_on[of A] by (auto dest: inj_onD)
   1.108 +
   1.109 +lemma from_nat_into_to_nat_on: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> from_nat_into A (to_nat_on A a) = a"
   1.110 +  by (auto simp: from_nat_into_def intro!: inv_into_f_f)
   1.111 +
   1.112 +lemma subset_range_from_nat_into: "countable A \<Longrightarrow> A \<subseteq> range (from_nat_into A)"
   1.113 +  by (auto intro: from_nat_into_to_nat_on[symmetric])
   1.114 +
   1.115 +subsection {* Closure properties of countability *}
   1.116 +
   1.117 +lemma countable_SIGMA[intro, simp]:
   1.118 +  "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"
   1.119 +  by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)
   1.120 +
   1.121 +lemma countable_image[intro, simp]: assumes A: "countable A" shows "countable (f`A)"
   1.122 +proof -
   1.123 +  from A guess g by (rule countableE)
   1.124 +  moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
   1.125 +    by (auto intro: inj_on_inv_into inv_into_into)
   1.126 +  ultimately show ?thesis
   1.127 +    by (blast dest: comp_inj_on subset_inj_on intro: countableI)
   1.128 +qed
   1.129 +
   1.130 +lemma countable_UN[intro, simp]:
   1.131 +  fixes I :: "'i set" and A :: "'i => 'a set"
   1.132 +  assumes I: "countable I"
   1.133 +  assumes A: "\<And>i. i \<in> I \<Longrightarrow> countable (A i)"
   1.134 +  shows "countable (\<Union>i\<in>I. A i)"
   1.135 +proof -
   1.136 +  have "(\<Union>i\<in>I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff)
   1.137 +  then show ?thesis by (simp add: assms)
   1.138 +qed
   1.139 +
   1.140 +lemma countable_Un[intro]: "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A \<union> B)"
   1.141 +  by (rule countable_UN[of "{True, False}" "\<lambda>True \<Rightarrow> A | False \<Rightarrow> B", simplified])
   1.142 +     (simp split: bool.split)
   1.143 +
   1.144 +lemma countable_Un_iff[simp]: "countable (A \<union> B) \<longleftrightarrow> countable A \<and> countable B"
   1.145 +  by (metis countable_Un countable_subset inf_sup_ord(3,4))
   1.146 +
   1.147 +lemma countable_Plus[intro, simp]:
   1.148 +  "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A <+> B)"
   1.149 +  by (simp add: Plus_def)
   1.150 +
   1.151 +lemma countable_empty[intro, simp]: "countable {}"
   1.152 +  by (blast intro: countable_finite)
   1.153 +
   1.154 +lemma countable_insert[intro, simp]: "countable A \<Longrightarrow> countable (insert a A)"
   1.155 +  using countable_Un[of "{a}" A] by (auto simp: countable_finite)
   1.156 +
   1.157 +lemma countable_Int1[intro, simp]: "countable A \<Longrightarrow> countable (A \<inter> B)"
   1.158 +  by (force intro: countable_subset)
   1.159 +
   1.160 +lemma countable_Int2[intro, simp]: "countable B \<Longrightarrow> countable (A \<inter> B)"
   1.161 +  by (blast intro: countable_subset)
   1.162 +
   1.163 +lemma countable_INT[intro, simp]: "i \<in> I \<Longrightarrow> countable (A i) \<Longrightarrow> countable (\<Inter>i\<in>I. A i)"
   1.164 +  by (blast intro: countable_subset)
   1.165 +
   1.166 +lemma countable_Diff[intro, simp]: "countable A \<Longrightarrow> countable (A - B)"
   1.167 +  by (blast intro: countable_subset)
   1.168 +
   1.169 +lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
   1.170 +  by (metis Int_absorb2 assms countable_image image_vimage_eq)
   1.171 +
   1.172 +lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
   1.173 +  by (metis countable_vimage top_greatest)
   1.174 +
   1.175 +lemma countable_lists[intro, simp]:
   1.176 +  assumes A: "countable A" shows "countable (lists A)"
   1.177 +proof -
   1.178 +  have "countable (lists (range (from_nat_into A)))"
   1.179 +    by (auto simp: lists_image)
   1.180 +  with A show ?thesis
   1.181 +    by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
   1.182 +qed
   1.183 +
   1.184 +subsection {* Misc lemmas *}
   1.185 +
   1.186 +lemma countable_all:
   1.187 +  assumes S: "countable S"
   1.188 +  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))"
   1.189 +  using S[THEN subset_range_from_nat_into] by auto
   1.190 +
   1.191 +end