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