src/HOL/Library/Infinite_Set.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 61810 3c5040d5694a
child 63492 a662e8139804
permissions -rw-r--r--
more symbols;
huffman@27407
     1
(*  Title:      HOL/Library/Infinite_Set.thy
wenzelm@20809
     2
    Author:     Stephan Merz
wenzelm@20809
     3
*)
wenzelm@20809
     4
wenzelm@60500
     5
section \<open>Infinite Sets and Related Concepts\<close>
wenzelm@20809
     6
wenzelm@20809
     7
theory Infinite_Set
traytel@54612
     8
imports Main
wenzelm@20809
     9
begin
wenzelm@20809
    10
lp15@61810
    11
text \<open>The set of natural numbers is infinite.\<close>
wenzelm@20809
    12
hoelzl@60040
    13
lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
hoelzl@60040
    14
  using frequently_cofinite[of "\<lambda>x. x \<in> S"]
hoelzl@60040
    15
  by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially)
hoelzl@60040
    16
hoelzl@60040
    17
lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)"
hoelzl@60040
    18
  using frequently_cofinite[of "\<lambda>x. x \<in> S"]
hoelzl@60040
    19
  by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense)
wenzelm@20809
    20
hoelzl@59000
    21
lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"
hoelzl@60040
    22
  using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
wenzelm@20809
    23
hoelzl@60040
    24
lemma finite_nat_iff_bounded_le: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})"
hoelzl@60040
    25
  using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
wenzelm@20809
    26
hoelzl@60040
    27
lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
hoelzl@60040
    28
  by (simp add: finite_nat_iff_bounded)
wenzelm@20809
    29
lp15@61762
    30
wenzelm@60500
    31
text \<open>
wenzelm@20809
    32
  For a set of natural numbers to be infinite, it is enough to know
wenzelm@61585
    33
  that for any number larger than some \<open>k\<close>, there is some larger
wenzelm@20809
    34
  number that is an element of the set.
wenzelm@60500
    35
\<close>
wenzelm@20809
    36
hoelzl@60040
    37
lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
lp15@61810
    38
apply (clarsimp simp add: finite_nat_set_iff_bounded)
lp15@61810
    39
apply (drule_tac x="Suc (max m k)" in spec)
lp15@61810
    40
using less_Suc_eq by fastforce
wenzelm@20809
    41
huffman@35056
    42
lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
wenzelm@20809
    43
  by simp
wenzelm@20809
    44
wenzelm@20809
    45
lemma range_inj_infinite:
wenzelm@20809
    46
  "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
wenzelm@20809
    47
proof
huffman@27407
    48
  assume "finite (range f)" and "inj f"
wenzelm@20809
    49
  then have "finite (UNIV::nat set)"
huffman@27407
    50
    by (rule finite_imageD)
wenzelm@20809
    51
  then show False by simp
wenzelm@20809
    52
qed
wenzelm@20809
    53
lp15@61762
    54
text \<open>The set of integers is also infinite.\<close>
lp15@61762
    55
lp15@61762
    56
lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) \<longleftrightarrow> infinite ((nat o abs) ` S)"
lp15@61762
    57
  by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD)
lp15@61762
    58
wenzelm@61945
    59
proposition infinite_int_iff_unbounded_le: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
lp15@61762
    60
  apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def)
lp15@61762
    61
  apply (metis abs_ge_zero nat_le_eq_zle le_nat_iff)
lp15@61762
    62
  done
lp15@61762
    63
wenzelm@61945
    64
proposition infinite_int_iff_unbounded: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> > m \<and> n \<in> S)"
lp15@61762
    65
  apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def)
lp15@61762
    66
  apply (metis (full_types) nat_le_iff nat_mono not_le)
lp15@61762
    67
  done
lp15@61762
    68
lp15@61762
    69
proposition finite_int_iff_bounded: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {..<k})"
lp15@61762
    70
  using infinite_int_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
lp15@61762
    71
lp15@61762
    72
proposition finite_int_iff_bounded_le: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {.. k})"
lp15@61762
    73
  using infinite_int_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
lp15@61762
    74
wenzelm@20809
    75
subsection "Infinitely Many and Almost All"
wenzelm@20809
    76
wenzelm@60500
    77
text \<open>
wenzelm@20809
    78
  We often need to reason about the existence of infinitely many
wenzelm@20809
    79
  (resp., all but finitely many) objects satisfying some predicate, so
wenzelm@20809
    80
  we introduce corresponding binders and their proof rules.
wenzelm@60500
    81
\<close>
wenzelm@20809
    82
hoelzl@60040
    83
(* The following two lemmas are available as filter-rules, but not in the simp-set *)
hoelzl@60040
    84
lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" by (fact not_frequently)
hoelzl@60040
    85
lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" by (fact not_eventually)
huffman@34112
    86
huffman@34112
    87
lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
hoelzl@60040
    88
  by (simp add: frequently_const_iff)
huffman@34112
    89
huffman@34112
    90
lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
hoelzl@60040
    91
  by (simp add: eventually_const_iff)
wenzelm@20809
    92
hoelzl@60040
    93
lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
hoelzl@60040
    94
  by (simp only: imp_conv_disj frequently_disj_iff not_eventually)
huffman@34112
    95
hoelzl@60040
    96
lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
lp15@61810
    97
  by (auto intro: eventually_rev_mp eventually_mono)
huffman@34113
    98
hoelzl@60040
    99
lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
lp15@61810
   100
  by (rule frequently_rev_mp[of P]) (auto elim: eventually_mono)
huffman@34112
   101
wenzelm@60500
   102
text \<open>Properties of quantifiers with injective functions.\<close>
huffman@34112
   103
wenzelm@53239
   104
lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
hoelzl@60040
   105
  using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite)
huffman@27407
   106
wenzelm@53239
   107
lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
hoelzl@60040
   108
  using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite)
huffman@34112
   109
wenzelm@60500
   110
text \<open>Properties of quantifiers with singletons.\<close>
huffman@34112
   111
huffman@34112
   112
lemma not_INFM_eq [simp]:
huffman@34112
   113
  "\<not> (INFM x. x = a)"
huffman@34112
   114
  "\<not> (INFM x. a = x)"
hoelzl@60040
   115
  unfolding frequently_cofinite by simp_all
huffman@34112
   116
huffman@34112
   117
lemma MOST_neq [simp]:
huffman@34112
   118
  "MOST x. x \<noteq> a"
huffman@34112
   119
  "MOST x. a \<noteq> x"
hoelzl@60040
   120
  unfolding eventually_cofinite by simp_all
huffman@27407
   121
huffman@34112
   122
lemma INFM_neq [simp]:
huffman@34112
   123
  "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
huffman@34112
   124
  "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
hoelzl@60040
   125
  unfolding frequently_cofinite by simp_all
huffman@34112
   126
huffman@34112
   127
lemma MOST_eq [simp]:
huffman@34112
   128
  "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
huffman@34112
   129
  "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
hoelzl@60040
   130
  unfolding eventually_cofinite by simp_all
huffman@34112
   131
huffman@34112
   132
lemma MOST_eq_imp:
huffman@34112
   133
  "MOST x. x = a \<longrightarrow> P x"
huffman@34112
   134
  "MOST x. a = x \<longrightarrow> P x"
hoelzl@60040
   135
  unfolding eventually_cofinite by simp_all
huffman@34112
   136
wenzelm@60500
   137
text \<open>Properties of quantifiers over the naturals.\<close>
huffman@27407
   138
hoelzl@60040
   139
lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
hoelzl@60040
   140
  by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
hoelzl@60040
   141
hoelzl@60040
   142
lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
hoelzl@60040
   143
  by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
hoelzl@60040
   144
hoelzl@60040
   145
lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
hoelzl@60040
   146
  by (simp add: frequently_cofinite infinite_nat_iff_unbounded)
wenzelm@20809
   147
hoelzl@60040
   148
lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)"
hoelzl@60040
   149
  by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le)
hoelzl@60040
   150
hoelzl@60040
   151
lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
hoelzl@60040
   152
  by (simp add: eventually_frequently)
hoelzl@60040
   153
hoelzl@60040
   154
lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
hoelzl@60040
   155
  by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc)
wenzelm@20809
   156
hoelzl@60040
   157
lemma
hoelzl@60040
   158
  shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
hoelzl@60040
   159
    and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
hoelzl@60040
   160
  by (simp_all add: MOST_Suc_iff)
hoelzl@60040
   161
hoelzl@60040
   162
lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
hoelzl@60040
   163
  by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
wenzelm@20809
   164
hoelzl@60040
   165
(* legacy names *)
hoelzl@60040
   166
lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
hoelzl@60040
   167
lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
hoelzl@60040
   168
lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
hoelzl@60040
   169
lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite)
hoelzl@60040
   170
lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
hoelzl@60040
   171
lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
hoelzl@60040
   172
lemma INFM_mono: "\<exists>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<exists>\<^sub>\<infinity>x. Q x" by (fact frequently_elim1)
lp15@61810
   173
lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_mono)
hoelzl@60040
   174
lemma INFM_disj_distrib: "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)" by (fact frequently_disj_iff)
hoelzl@60040
   175
lemma MOST_rev_mp: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_rev_mp)
hoelzl@60040
   176
lemma MOST_conj_distrib: "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)" by (fact eventually_conj_iff)
hoelzl@60040
   177
lemma MOST_conjI: "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x" by (fact eventually_conj)
hoelzl@60040
   178
lemma INFM_finite_Bex_distrib: "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)" by (fact frequently_bex_finite_distrib)
hoelzl@60040
   179
lemma MOST_finite_Ball_distrib: "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)" by (fact eventually_ball_finite_distrib)
hoelzl@60040
   180
lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE)
hoelzl@60040
   181
lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI)
hoelzl@60040
   182
lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
wenzelm@20809
   183
wenzelm@20809
   184
subsection "Enumeration of an Infinite Set"
wenzelm@20809
   185
wenzelm@60500
   186
text \<open>
wenzelm@20809
   187
  The set's element type must be wellordered (e.g. the natural numbers).
wenzelm@60500
   188
\<close>
wenzelm@20809
   189
hoelzl@60040
   190
text \<open>
hoelzl@60040
   191
  Could be generalized to
hoelzl@60040
   192
    @{term "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}.
hoelzl@60040
   193
\<close>
hoelzl@60040
   194
wenzelm@53239
   195
primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
wenzelm@53239
   196
where
wenzelm@53239
   197
  enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
wenzelm@53239
   198
| enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
wenzelm@20809
   199
wenzelm@53239
   200
lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
wenzelm@20809
   201
  by simp
wenzelm@20809
   202
hoelzl@60040
   203
lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S"
wenzelm@53239
   204
  apply (induct n arbitrary: S)
wenzelm@53239
   205
   apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
wenzelm@53239
   206
  apply simp
wenzelm@53239
   207
  apply (metis DiffE infinite_remove)
wenzelm@53239
   208
  done
wenzelm@20809
   209
wenzelm@20809
   210
declare enumerate_0 [simp del] enumerate_Suc [simp del]
wenzelm@20809
   211
wenzelm@20809
   212
lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
wenzelm@20809
   213
  apply (induct n arbitrary: S)
wenzelm@20809
   214
   apply (rule order_le_neq_trans)
wenzelm@20809
   215
    apply (simp add: enumerate_0 Least_le enumerate_in_set)
wenzelm@20809
   216
   apply (simp only: enumerate_Suc')
hoelzl@60040
   217
   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
wenzelm@20809
   218
    apply (blast intro: sym)
wenzelm@20809
   219
   apply (simp add: enumerate_in_set del: Diff_iff)
wenzelm@20809
   220
  apply (simp add: enumerate_Suc')
wenzelm@20809
   221
  done
wenzelm@20809
   222
hoelzl@60040
   223
lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
wenzelm@20809
   224
  apply (erule less_Suc_induct)
wenzelm@20809
   225
  apply (auto intro: enumerate_step)
wenzelm@20809
   226
  done
wenzelm@20809
   227
wenzelm@20809
   228
hoelzl@50134
   229
lemma le_enumerate:
hoelzl@50134
   230
  assumes S: "infinite S"
hoelzl@50134
   231
  shows "n \<le> enumerate S n"
lp15@61810
   232
  using S
hoelzl@50134
   233
proof (induct n)
wenzelm@53239
   234
  case 0
wenzelm@53239
   235
  then show ?case by simp
wenzelm@53239
   236
next
hoelzl@50134
   237
  case (Suc n)
hoelzl@50134
   238
  then have "n \<le> enumerate S n" by simp
wenzelm@60500
   239
  also note enumerate_mono[of n "Suc n", OF _ \<open>infinite S\<close>]
hoelzl@50134
   240
  finally show ?case by simp
wenzelm@53239
   241
qed
hoelzl@50134
   242
hoelzl@50134
   243
lemma enumerate_Suc'':
hoelzl@50134
   244
  fixes S :: "'a::wellorder set"
wenzelm@53239
   245
  assumes "infinite S"
wenzelm@53239
   246
  shows "enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
wenzelm@53239
   247
  using assms
hoelzl@50134
   248
proof (induct n arbitrary: S)
hoelzl@50134
   249
  case 0
wenzelm@53239
   250
  then have "\<forall>s \<in> S. enumerate S 0 \<le> s"
hoelzl@50134
   251
    by (auto simp: enumerate.simps intro: Least_le)
hoelzl@50134
   252
  then show ?case
hoelzl@50134
   253
    unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"]
wenzelm@53239
   254
    by (intro arg_cong[where f = Least] ext) auto
hoelzl@50134
   255
next
hoelzl@50134
   256
  case (Suc n S)
hoelzl@50134
   257
  show ?case
wenzelm@60500
   258
    using enumerate_mono[OF zero_less_Suc \<open>infinite S\<close>, of n] \<open>infinite S\<close>
hoelzl@50134
   259
    apply (subst (1 2) enumerate_Suc')
hoelzl@50134
   260
    apply (subst Suc)
wenzelm@60500
   261
    using \<open>infinite S\<close>
wenzelm@53239
   262
    apply simp
wenzelm@53239
   263
    apply (intro arg_cong[where f = Least] ext)
wenzelm@53239
   264
    apply (auto simp: enumerate_Suc'[symmetric])
wenzelm@53239
   265
    done
hoelzl@50134
   266
qed
hoelzl@50134
   267
hoelzl@50134
   268
lemma enumerate_Ex:
hoelzl@50134
   269
  assumes S: "infinite (S::nat set)"
hoelzl@50134
   270
  shows "s \<in> S \<Longrightarrow> \<exists>n. enumerate S n = s"
hoelzl@50134
   271
proof (induct s rule: less_induct)
hoelzl@50134
   272
  case (less s)
hoelzl@50134
   273
  show ?case
hoelzl@50134
   274
  proof cases
hoelzl@50134
   275
    let ?y = "Max {s'\<in>S. s' < s}"
hoelzl@50134
   276
    assume "\<exists>y\<in>S. y < s"
wenzelm@53239
   277
    then have y: "\<And>x. ?y < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)"
wenzelm@53239
   278
      by (subst Max_less_iff) auto
wenzelm@53239
   279
    then have y_in: "?y \<in> {s'\<in>S. s' < s}"
wenzelm@53239
   280
      by (intro Max_in) auto
wenzelm@53239
   281
    with less.hyps[of ?y] obtain n where "enumerate S n = ?y"
wenzelm@53239
   282
      by auto
hoelzl@50134
   283
    with S have "enumerate S (Suc n) = s"
hoelzl@50134
   284
      by (auto simp: y less enumerate_Suc'' intro!: Least_equality)
hoelzl@50134
   285
    then show ?case by auto
hoelzl@50134
   286
  next
hoelzl@50134
   287
    assume *: "\<not> (\<exists>y\<in>S. y < s)"
hoelzl@50134
   288
    then have "\<forall>t\<in>S. s \<le> t" by auto
wenzelm@60500
   289
    with \<open>s \<in> S\<close> show ?thesis
hoelzl@50134
   290
      by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0)
hoelzl@50134
   291
  qed
hoelzl@50134
   292
qed
hoelzl@50134
   293
hoelzl@50134
   294
lemma bij_enumerate:
hoelzl@50134
   295
  fixes S :: "nat set"
hoelzl@50134
   296
  assumes S: "infinite S"
hoelzl@50134
   297
  shows "bij_betw (enumerate S) UNIV S"
hoelzl@50134
   298
proof -
hoelzl@50134
   299
  have "\<And>n m. n \<noteq> m \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
wenzelm@60500
   300
    using enumerate_mono[OF _ \<open>infinite S\<close>] by (auto simp: neq_iff)
hoelzl@50134
   301
  then have "inj (enumerate S)"
hoelzl@50134
   302
    by (auto simp: inj_on_def)
wenzelm@53239
   303
  moreover have "\<forall>s \<in> S. \<exists>i. enumerate S i = s"
hoelzl@50134
   304
    using enumerate_Ex[OF S] by auto
wenzelm@60500
   305
  moreover note \<open>infinite S\<close>
hoelzl@50134
   306
  ultimately show ?thesis
hoelzl@50134
   307
    unfolding bij_betw_def by (auto intro: enumerate_in_set)
hoelzl@50134
   308
qed
hoelzl@50134
   309
wenzelm@20809
   310
end
traytel@54612
   311