src/HOL/Library/Countable_Set.thy
author hoelzl
Tue Nov 20 18:59:35 2012 +0100 (2012-11-20)
changeset 50134 13211e07d931
child 50144 885deccc264e
permissions -rw-r--r--
add Countable_Set theory
hoelzl@50134
     1
(*  Title:      HOL/Library/Countable_Set.thy
hoelzl@50134
     2
    Author:     Johannes Hölzl
hoelzl@50134
     3
    Author:     Andrei Popescu
hoelzl@50134
     4
*)
hoelzl@50134
     5
hoelzl@50134
     6
header {* Countable sets *}
hoelzl@50134
     7
hoelzl@50134
     8
theory Countable_Set
hoelzl@50134
     9
  imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Infinite_Set"
hoelzl@50134
    10
begin
hoelzl@50134
    11
hoelzl@50134
    12
subsection {* Predicate for countable sets *}
hoelzl@50134
    13
hoelzl@50134
    14
definition countable :: "'a set \<Rightarrow> bool" where
hoelzl@50134
    15
  "countable S \<longleftrightarrow> (\<exists>f::'a \<Rightarrow> nat. inj_on f S)"
hoelzl@50134
    16
hoelzl@50134
    17
lemma countableE:
hoelzl@50134
    18
  assumes S: "countable S" obtains f :: "'a \<Rightarrow> nat" where "inj_on f S"
hoelzl@50134
    19
  using S by (auto simp: countable_def)
hoelzl@50134
    20
hoelzl@50134
    21
lemma countableI: "inj_on (f::'a \<Rightarrow> nat) S \<Longrightarrow> countable S"
hoelzl@50134
    22
  by (auto simp: countable_def)
hoelzl@50134
    23
hoelzl@50134
    24
lemma countableI': "inj_on (f::'a \<Rightarrow> 'b::countable) S \<Longrightarrow> countable S"
hoelzl@50134
    25
  using comp_inj_on[of f S to_nat] by (auto intro: countableI)
hoelzl@50134
    26
hoelzl@50134
    27
lemma countableE_bij:
hoelzl@50134
    28
  assumes S: "countable S" obtains f :: "nat \<Rightarrow> 'a" and C :: "nat set" where "bij_betw f C S"
hoelzl@50134
    29
  using S by (blast elim: countableE dest: inj_on_imp_bij_betw bij_betw_inv)
hoelzl@50134
    30
hoelzl@50134
    31
lemma countableI_bij: "bij_betw f (C::nat set) S \<Longrightarrow> countable S"
hoelzl@50134
    32
  by (blast intro: countableI bij_betw_inv_into bij_betw_imp_inj_on)
hoelzl@50134
    33
hoelzl@50134
    34
lemma countable_finite: "finite S \<Longrightarrow> countable S"
hoelzl@50134
    35
  by (blast dest: finite_imp_inj_to_nat_seg countableI)
hoelzl@50134
    36
hoelzl@50134
    37
lemma countableI_bij1: "bij_betw f A B \<Longrightarrow> countable A \<Longrightarrow> countable B"
hoelzl@50134
    38
  by (blast elim: countableE_bij intro: bij_betw_trans countableI_bij)
hoelzl@50134
    39
hoelzl@50134
    40
lemma countableI_bij2: "bij_betw f B A \<Longrightarrow> countable A \<Longrightarrow> countable B"
hoelzl@50134
    41
  by (blast elim: countableE_bij intro: bij_betw_trans bij_betw_inv_into countableI_bij)
hoelzl@50134
    42
hoelzl@50134
    43
lemma countable_iff_bij[simp]: "bij_betw f A B \<Longrightarrow> countable A \<longleftrightarrow> countable B"
hoelzl@50134
    44
  by (blast intro: countableI_bij1 countableI_bij2)
hoelzl@50134
    45
hoelzl@50134
    46
lemma countable_subset: "A \<subseteq> B \<Longrightarrow> countable B \<Longrightarrow> countable A"
hoelzl@50134
    47
  by (auto simp: countable_def intro: subset_inj_on)
hoelzl@50134
    48
hoelzl@50134
    49
lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)"
hoelzl@50134
    50
  using countableI[of to_nat A] by auto
hoelzl@50134
    51
hoelzl@50134
    52
subsection {* Enumerate a countable set *}
hoelzl@50134
    53
hoelzl@50134
    54
lemma countableE_infinite:
hoelzl@50134
    55
  assumes "countable S" "infinite S"
hoelzl@50134
    56
  obtains e :: "'a \<Rightarrow> nat" where "bij_betw e S UNIV"
hoelzl@50134
    57
proof -
hoelzl@50134
    58
  from `countable S`[THEN countableE] guess f .
hoelzl@50134
    59
  then have "bij_betw f S (f`S)"
hoelzl@50134
    60
    unfolding bij_betw_def by simp
hoelzl@50134
    61
  moreover
hoelzl@50134
    62
  from `inj_on f S` `infinite S` have inf_fS: "infinite (f`S)"
hoelzl@50134
    63
    by (auto dest: finite_imageD)
hoelzl@50134
    64
  then have "bij_betw (the_inv_into UNIV (enumerate (f`S))) (f`S) UNIV"
hoelzl@50134
    65
    by (intro bij_betw_the_inv_into bij_enumerate)
hoelzl@50134
    66
  ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) \<circ> f) S UNIV"
hoelzl@50134
    67
    by (rule bij_betw_trans)
hoelzl@50134
    68
  then show thesis ..
hoelzl@50134
    69
qed
hoelzl@50134
    70
hoelzl@50134
    71
lemma countable_enum_cases:
hoelzl@50134
    72
  assumes "countable S"
hoelzl@50134
    73
  obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}"
hoelzl@50134
    74
        | (infinite) f :: "'a \<Rightarrow> nat" where "infinite S" "bij_betw f S UNIV"
hoelzl@50134
    75
  using ex_bij_betw_finite_nat[of S] countableE_infinite `countable S`
hoelzl@50134
    76
  by (cases "finite S") (auto simp add: atLeast0LessThan)
hoelzl@50134
    77
hoelzl@50134
    78
definition to_nat_on :: "'a set \<Rightarrow> 'a \<Rightarrow> nat" where
hoelzl@50134
    79
  "to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)"
hoelzl@50134
    80
hoelzl@50134
    81
definition from_nat_into :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
hoelzl@50134
    82
  "from_nat_into S = inv_into S (to_nat_on S)"
hoelzl@50134
    83
hoelzl@50134
    84
lemma to_nat_on_finite: "finite S \<Longrightarrow> bij_betw (to_nat_on S) S {..< card S}"
hoelzl@50134
    85
  using ex_bij_betw_finite_nat unfolding to_nat_on_def
hoelzl@50134
    86
  by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S {..<card S}"]) (auto simp add: atLeast0LessThan)
hoelzl@50134
    87
hoelzl@50134
    88
lemma to_nat_on_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (to_nat_on S) S UNIV"
hoelzl@50134
    89
  using countableE_infinite unfolding to_nat_on_def
hoelzl@50134
    90
  by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto
hoelzl@50134
    91
hoelzl@50134
    92
lemma from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
hoelzl@50134
    93
  by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_finite)
hoelzl@50134
    94
hoelzl@50134
    95
lemma from_nat_into_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
hoelzl@50134
    96
  by (auto simp add: from_nat_into_def intro: bij_betw_inv_into to_nat_on_infinite)
hoelzl@50134
    97
hoelzl@50134
    98
lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A"
hoelzl@50134
    99
  using to_nat_on_infinite[of A] to_nat_on_finite[of A]
hoelzl@50134
   100
  by (cases "finite A") (auto simp: bij_betw_def)
hoelzl@50134
   101
hoelzl@50134
   102
lemma to_nat_on_inj[simp]:
hoelzl@50134
   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"
hoelzl@50134
   104
  using inj_on_to_nat_on[of A] by (auto dest: inj_onD)
hoelzl@50134
   105
hoelzl@50134
   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"
hoelzl@50134
   107
  by (auto simp: from_nat_into_def intro!: inv_into_f_f)
hoelzl@50134
   108
hoelzl@50134
   109
lemma subset_range_from_nat_into: "countable A \<Longrightarrow> A \<subseteq> range (from_nat_into A)"
hoelzl@50134
   110
  by (auto intro: from_nat_into_to_nat_on[symmetric])
hoelzl@50134
   111
hoelzl@50134
   112
subsection {* Closure properties of countability *}
hoelzl@50134
   113
hoelzl@50134
   114
lemma countable_SIGMA[intro, simp]:
hoelzl@50134
   115
  "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"
hoelzl@50134
   116
  by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)
hoelzl@50134
   117
hoelzl@50134
   118
lemma countable_image[intro, simp]: assumes A: "countable A" shows "countable (f`A)"
hoelzl@50134
   119
proof -
hoelzl@50134
   120
  from A guess g by (rule countableE)
hoelzl@50134
   121
  moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
hoelzl@50134
   122
    by (auto intro: inj_on_inv_into inv_into_into)
hoelzl@50134
   123
  ultimately show ?thesis
hoelzl@50134
   124
    by (blast dest: comp_inj_on subset_inj_on intro: countableI)
hoelzl@50134
   125
qed
hoelzl@50134
   126
hoelzl@50134
   127
lemma countable_UN[intro, simp]:
hoelzl@50134
   128
  fixes I :: "'i set" and A :: "'i => 'a set"
hoelzl@50134
   129
  assumes I: "countable I"
hoelzl@50134
   130
  assumes A: "\<And>i. i \<in> I \<Longrightarrow> countable (A i)"
hoelzl@50134
   131
  shows "countable (\<Union>i\<in>I. A i)"
hoelzl@50134
   132
proof -
hoelzl@50134
   133
  have "(\<Union>i\<in>I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff)
hoelzl@50134
   134
  then show ?thesis by (simp add: assms)
hoelzl@50134
   135
qed
hoelzl@50134
   136
hoelzl@50134
   137
lemma countable_Un[intro]: "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A \<union> B)"
hoelzl@50134
   138
  by (rule countable_UN[of "{True, False}" "\<lambda>True \<Rightarrow> A | False \<Rightarrow> B", simplified])
hoelzl@50134
   139
     (simp split: bool.split)
hoelzl@50134
   140
hoelzl@50134
   141
lemma countable_Un_iff[simp]: "countable (A \<union> B) \<longleftrightarrow> countable A \<and> countable B"
hoelzl@50134
   142
  by (metis countable_Un countable_subset inf_sup_ord(3,4))
hoelzl@50134
   143
hoelzl@50134
   144
lemma countable_Plus[intro, simp]:
hoelzl@50134
   145
  "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A <+> B)"
hoelzl@50134
   146
  by (simp add: Plus_def)
hoelzl@50134
   147
hoelzl@50134
   148
lemma countable_empty[intro, simp]: "countable {}"
hoelzl@50134
   149
  by (blast intro: countable_finite)
hoelzl@50134
   150
hoelzl@50134
   151
lemma countable_insert[intro, simp]: "countable A \<Longrightarrow> countable (insert a A)"
hoelzl@50134
   152
  using countable_Un[of "{a}" A] by (auto simp: countable_finite)
hoelzl@50134
   153
hoelzl@50134
   154
lemma countable_Int1[intro, simp]: "countable A \<Longrightarrow> countable (A \<inter> B)"
hoelzl@50134
   155
  by (force intro: countable_subset)
hoelzl@50134
   156
hoelzl@50134
   157
lemma countable_Int2[intro, simp]: "countable B \<Longrightarrow> countable (A \<inter> B)"
hoelzl@50134
   158
  by (blast intro: countable_subset)
hoelzl@50134
   159
hoelzl@50134
   160
lemma countable_INT[intro, simp]: "i \<in> I \<Longrightarrow> countable (A i) \<Longrightarrow> countable (\<Inter>i\<in>I. A i)"
hoelzl@50134
   161
  by (blast intro: countable_subset)
hoelzl@50134
   162
hoelzl@50134
   163
lemma countable_Diff[intro, simp]: "countable A \<Longrightarrow> countable (A - B)"
hoelzl@50134
   164
  by (blast intro: countable_subset)
hoelzl@50134
   165
hoelzl@50134
   166
lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
hoelzl@50134
   167
  by (metis Int_absorb2 assms countable_image image_vimage_eq)
hoelzl@50134
   168
hoelzl@50134
   169
lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
hoelzl@50134
   170
  by (metis countable_vimage top_greatest)
hoelzl@50134
   171
hoelzl@50134
   172
lemma countable_lists[intro, simp]:
hoelzl@50134
   173
  assumes A: "countable A" shows "countable (lists A)"
hoelzl@50134
   174
proof -
hoelzl@50134
   175
  have "countable (lists (range (from_nat_into A)))"
hoelzl@50134
   176
    by (auto simp: lists_image)
hoelzl@50134
   177
  with A show ?thesis
hoelzl@50134
   178
    by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
hoelzl@50134
   179
qed
hoelzl@50134
   180
hoelzl@50134
   181
subsection {* Misc lemmas *}
hoelzl@50134
   182
hoelzl@50134
   183
lemma countable_all:
hoelzl@50134
   184
  assumes S: "countable S"
hoelzl@50134
   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))"
hoelzl@50134
   186
  using S[THEN subset_range_from_nat_into] by auto
hoelzl@50134
   187
hoelzl@50134
   188
end