src/HOL/Library/Infinite_Set.thy
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 60040 1fa1023b13b9
child 60828 e9e272fa8daf
permissions -rw-r--r--
isabelle update_cartouches;
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
wenzelm@20809
    11
subsection "Infinite Sets"
wenzelm@20809
    12
wenzelm@60500
    13
text \<open>
blanchet@54557
    14
  Some elementary facts about infinite sets, mostly by Stephan Merz.
wenzelm@20809
    15
  Beware! Because "infinite" merely abbreviates a negation, these
wenzelm@20809
    16
  lemmas may not work well with @{text "blast"}.
wenzelm@60500
    17
\<close>
wenzelm@20809
    18
wenzelm@53239
    19
abbreviation infinite :: "'a set \<Rightarrow> bool"
wenzelm@53239
    20
  where "infinite S \<equiv> \<not> finite S"
wenzelm@20809
    21
wenzelm@60500
    22
text \<open>
wenzelm@20809
    23
  Infinite sets are non-empty, and if we remove some elements from an
wenzelm@20809
    24
  infinite set, the result is still infinite.
wenzelm@60500
    25
\<close>
wenzelm@20809
    26
wenzelm@53239
    27
lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}"
wenzelm@20809
    28
  by auto
wenzelm@20809
    29
wenzelm@53239
    30
lemma infinite_remove: "infinite S \<Longrightarrow> infinite (S - {a})"
wenzelm@20809
    31
  by simp
wenzelm@20809
    32
wenzelm@20809
    33
lemma Diff_infinite_finite:
wenzelm@20809
    34
  assumes T: "finite T" and S: "infinite S"
wenzelm@20809
    35
  shows "infinite (S - T)"
wenzelm@20809
    36
  using T
wenzelm@20809
    37
proof induct
wenzelm@20809
    38
  from S
wenzelm@20809
    39
  show "infinite (S - {})" by auto
wenzelm@20809
    40
next
wenzelm@20809
    41
  fix T x
wenzelm@20809
    42
  assume ih: "infinite (S - T)"
wenzelm@20809
    43
  have "S - (insert x T) = (S - T) - {x}"
wenzelm@20809
    44
    by (rule Diff_insert)
wenzelm@20809
    45
  with ih
wenzelm@20809
    46
  show "infinite (S - (insert x T))"
wenzelm@20809
    47
    by (simp add: infinite_remove)
wenzelm@20809
    48
qed
wenzelm@20809
    49
wenzelm@20809
    50
lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
wenzelm@20809
    51
  by simp
wenzelm@20809
    52
urbanc@35844
    53
lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
urbanc@35844
    54
  by simp
urbanc@35844
    55
wenzelm@20809
    56
lemma infinite_super:
wenzelm@20809
    57
  assumes T: "S \<subseteq> T" and S: "infinite S"
wenzelm@20809
    58
  shows "infinite T"
wenzelm@20809
    59
proof
wenzelm@20809
    60
  assume "finite T"
wenzelm@20809
    61
  with T have "finite S" by (simp add: finite_subset)
wenzelm@20809
    62
  with S show False by simp
wenzelm@20809
    63
qed
wenzelm@20809
    64
wenzelm@60500
    65
text \<open>
wenzelm@20809
    66
  As a concrete example, we prove that the set of natural numbers is
wenzelm@20809
    67
  infinite.
wenzelm@60500
    68
\<close>
wenzelm@20809
    69
hoelzl@60040
    70
lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
hoelzl@60040
    71
  using frequently_cofinite[of "\<lambda>x. x \<in> S"]
hoelzl@60040
    72
  by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially)
hoelzl@60040
    73
hoelzl@60040
    74
lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)"
hoelzl@60040
    75
  using frequently_cofinite[of "\<lambda>x. x \<in> S"]
hoelzl@60040
    76
  by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense)
wenzelm@20809
    77
hoelzl@59000
    78
lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"
hoelzl@60040
    79
  using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
wenzelm@20809
    80
hoelzl@60040
    81
lemma finite_nat_iff_bounded_le: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})"
hoelzl@60040
    82
  using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
wenzelm@20809
    83
hoelzl@60040
    84
lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
hoelzl@60040
    85
  by (simp add: finite_nat_iff_bounded)
wenzelm@20809
    86
wenzelm@60500
    87
text \<open>
wenzelm@20809
    88
  For a set of natural numbers to be infinite, it is enough to know
wenzelm@20809
    89
  that for any number larger than some @{text k}, there is some larger
wenzelm@20809
    90
  number that is an element of the set.
wenzelm@60500
    91
\<close>
wenzelm@20809
    92
hoelzl@60040
    93
lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
hoelzl@60040
    94
  by (metis (full_types) infinite_nat_iff_unbounded_le le_imp_less_Suc not_less
hoelzl@60040
    95
            not_less_iff_gr_or_eq sup.bounded_iff)
wenzelm@20809
    96
huffman@35056
    97
lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
wenzelm@20809
    98
  by simp
wenzelm@20809
    99
wenzelm@20809
   100
lemma range_inj_infinite:
wenzelm@20809
   101
  "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
wenzelm@20809
   102
proof
huffman@27407
   103
  assume "finite (range f)" and "inj f"
wenzelm@20809
   104
  then have "finite (UNIV::nat set)"
huffman@27407
   105
    by (rule finite_imageD)
wenzelm@20809
   106
  then show False by simp
wenzelm@20809
   107
qed
wenzelm@20809
   108
wenzelm@60500
   109
text \<open>
wenzelm@20809
   110
  For any function with infinite domain and finite range there is some
wenzelm@20809
   111
  element that is the image of infinitely many domain elements.  In
wenzelm@20809
   112
  particular, any infinite sequence of elements from a finite set
wenzelm@20809
   113
  contains some element that occurs infinitely often.
wenzelm@60500
   114
\<close>
wenzelm@20809
   115
Andreas@59488
   116
lemma inf_img_fin_dom':
Andreas@59488
   117
  assumes img: "finite (f ` A)" and dom: "infinite A"
Andreas@59488
   118
  shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)"
Andreas@59488
   119
proof (rule ccontr)
Andreas@59488
   120
  have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto
Andreas@59488
   121
  moreover
Andreas@59488
   122
  assume "\<not> ?thesis"
Andreas@59488
   123
  with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast
Andreas@59488
   124
  ultimately have "finite A" by(rule finite_subset)
Andreas@59488
   125
  with dom show False by contradiction
Andreas@59488
   126
qed
Andreas@59488
   127
Andreas@59488
   128
lemma inf_img_fin_domE':
Andreas@59488
   129
  assumes "finite (f ` A)" and "infinite A"
Andreas@59488
   130
  obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)"
Andreas@59488
   131
  using assms by (blast dest: inf_img_fin_dom')
Andreas@59488
   132
wenzelm@20809
   133
lemma inf_img_fin_dom:
wenzelm@20809
   134
  assumes img: "finite (f`A)" and dom: "infinite A"
wenzelm@20809
   135
  shows "\<exists>y \<in> f`A. infinite (f -` {y})"
Andreas@59488
   136
using inf_img_fin_dom'[OF assms] by auto
wenzelm@20809
   137
wenzelm@20809
   138
lemma inf_img_fin_domE:
wenzelm@20809
   139
  assumes "finite (f`A)" and "infinite A"
wenzelm@20809
   140
  obtains y where "y \<in> f`A" and "infinite (f -` {y})"
wenzelm@23394
   141
  using assms by (blast dest: inf_img_fin_dom)
wenzelm@20809
   142
wenzelm@20809
   143
subsection "Infinitely Many and Almost All"
wenzelm@20809
   144
wenzelm@60500
   145
text \<open>
wenzelm@20809
   146
  We often need to reason about the existence of infinitely many
wenzelm@20809
   147
  (resp., all but finitely many) objects satisfying some predicate, so
wenzelm@20809
   148
  we introduce corresponding binders and their proof rules.
wenzelm@60500
   149
\<close>
wenzelm@20809
   150
hoelzl@60040
   151
(* The following two lemmas are available as filter-rules, but not in the simp-set *)
hoelzl@60040
   152
lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" by (fact not_frequently)
hoelzl@60040
   153
lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" by (fact not_eventually)
huffman@34112
   154
huffman@34112
   155
lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
hoelzl@60040
   156
  by (simp add: frequently_const_iff)
huffman@34112
   157
huffman@34112
   158
lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
hoelzl@60040
   159
  by (simp add: eventually_const_iff)
wenzelm@20809
   160
hoelzl@60040
   161
lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
hoelzl@60040
   162
  by (simp only: imp_conv_disj frequently_disj_iff not_eventually)
huffman@34112
   163
hoelzl@60040
   164
lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
hoelzl@60040
   165
  by (auto intro: eventually_rev_mp eventually_elim1)
huffman@34113
   166
hoelzl@60040
   167
lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
hoelzl@60040
   168
  by (rule frequently_rev_mp[of P]) (auto elim: eventually_elim1)
huffman@34112
   169
wenzelm@60500
   170
text \<open>Properties of quantifiers with injective functions.\<close>
huffman@34112
   171
wenzelm@53239
   172
lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
hoelzl@60040
   173
  using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite)
huffman@27407
   174
wenzelm@53239
   175
lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
hoelzl@60040
   176
  using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite)
huffman@34112
   177
wenzelm@60500
   178
text \<open>Properties of quantifiers with singletons.\<close>
huffman@34112
   179
huffman@34112
   180
lemma not_INFM_eq [simp]:
huffman@34112
   181
  "\<not> (INFM x. x = a)"
huffman@34112
   182
  "\<not> (INFM x. a = x)"
hoelzl@60040
   183
  unfolding frequently_cofinite by simp_all
huffman@34112
   184
huffman@34112
   185
lemma MOST_neq [simp]:
huffman@34112
   186
  "MOST x. x \<noteq> a"
huffman@34112
   187
  "MOST x. a \<noteq> x"
hoelzl@60040
   188
  unfolding eventually_cofinite by simp_all
huffman@27407
   189
huffman@34112
   190
lemma INFM_neq [simp]:
huffman@34112
   191
  "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
huffman@34112
   192
  "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
hoelzl@60040
   193
  unfolding frequently_cofinite by simp_all
huffman@34112
   194
huffman@34112
   195
lemma MOST_eq [simp]:
huffman@34112
   196
  "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
huffman@34112
   197
  "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
hoelzl@60040
   198
  unfolding eventually_cofinite by simp_all
huffman@34112
   199
huffman@34112
   200
lemma MOST_eq_imp:
huffman@34112
   201
  "MOST x. x = a \<longrightarrow> P x"
huffman@34112
   202
  "MOST x. a = x \<longrightarrow> P x"
hoelzl@60040
   203
  unfolding eventually_cofinite by simp_all
huffman@34112
   204
wenzelm@60500
   205
text \<open>Properties of quantifiers over the naturals.\<close>
huffman@27407
   206
hoelzl@60040
   207
lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
hoelzl@60040
   208
  by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
hoelzl@60040
   209
hoelzl@60040
   210
lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
hoelzl@60040
   211
  by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
hoelzl@60040
   212
hoelzl@60040
   213
lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
hoelzl@60040
   214
  by (simp add: frequently_cofinite infinite_nat_iff_unbounded)
wenzelm@20809
   215
hoelzl@60040
   216
lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)"
hoelzl@60040
   217
  by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le)
hoelzl@60040
   218
hoelzl@60040
   219
lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
hoelzl@60040
   220
  by (simp add: eventually_frequently)
hoelzl@60040
   221
hoelzl@60040
   222
lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
hoelzl@60040
   223
  by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc)
wenzelm@20809
   224
hoelzl@60040
   225
lemma
hoelzl@60040
   226
  shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
hoelzl@60040
   227
    and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
hoelzl@60040
   228
  by (simp_all add: MOST_Suc_iff)
hoelzl@60040
   229
hoelzl@60040
   230
lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
hoelzl@60040
   231
  by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
wenzelm@20809
   232
hoelzl@60040
   233
(* legacy names *)
hoelzl@60040
   234
lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
hoelzl@60040
   235
lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
hoelzl@60040
   236
lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
hoelzl@60040
   237
lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite)
hoelzl@60040
   238
lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
hoelzl@60040
   239
lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
hoelzl@60040
   240
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)
hoelzl@60040
   241
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_elim1)
hoelzl@60040
   242
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
   243
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
   244
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
   245
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
   246
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
   247
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
   248
lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE)
hoelzl@60040
   249
lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI)
hoelzl@60040
   250
lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
wenzelm@20809
   251
wenzelm@20809
   252
subsection "Enumeration of an Infinite Set"
wenzelm@20809
   253
wenzelm@60500
   254
text \<open>
wenzelm@20809
   255
  The set's element type must be wellordered (e.g. the natural numbers).
wenzelm@60500
   256
\<close>
wenzelm@20809
   257
hoelzl@60040
   258
text \<open>
hoelzl@60040
   259
  Could be generalized to
hoelzl@60040
   260
    @{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
   261
\<close>
hoelzl@60040
   262
wenzelm@53239
   263
primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
wenzelm@53239
   264
where
wenzelm@53239
   265
  enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
wenzelm@53239
   266
| enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
wenzelm@20809
   267
wenzelm@53239
   268
lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
wenzelm@20809
   269
  by simp
wenzelm@20809
   270
hoelzl@60040
   271
lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S"
wenzelm@53239
   272
  apply (induct n arbitrary: S)
wenzelm@53239
   273
   apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
wenzelm@53239
   274
  apply simp
wenzelm@53239
   275
  apply (metis DiffE infinite_remove)
wenzelm@53239
   276
  done
wenzelm@20809
   277
wenzelm@20809
   278
declare enumerate_0 [simp del] enumerate_Suc [simp del]
wenzelm@20809
   279
wenzelm@20809
   280
lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
wenzelm@20809
   281
  apply (induct n arbitrary: S)
wenzelm@20809
   282
   apply (rule order_le_neq_trans)
wenzelm@20809
   283
    apply (simp add: enumerate_0 Least_le enumerate_in_set)
wenzelm@20809
   284
   apply (simp only: enumerate_Suc')
hoelzl@60040
   285
   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
wenzelm@20809
   286
    apply (blast intro: sym)
wenzelm@20809
   287
   apply (simp add: enumerate_in_set del: Diff_iff)
wenzelm@20809
   288
  apply (simp add: enumerate_Suc')
wenzelm@20809
   289
  done
wenzelm@20809
   290
hoelzl@60040
   291
lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
wenzelm@20809
   292
  apply (erule less_Suc_induct)
wenzelm@20809
   293
  apply (auto intro: enumerate_step)
wenzelm@20809
   294
  done
wenzelm@20809
   295
wenzelm@20809
   296
hoelzl@50134
   297
lemma le_enumerate:
hoelzl@50134
   298
  assumes S: "infinite S"
hoelzl@50134
   299
  shows "n \<le> enumerate S n"
hoelzl@50134
   300
  using S 
hoelzl@50134
   301
proof (induct n)
wenzelm@53239
   302
  case 0
wenzelm@53239
   303
  then show ?case by simp
wenzelm@53239
   304
next
hoelzl@50134
   305
  case (Suc n)
hoelzl@50134
   306
  then have "n \<le> enumerate S n" by simp
wenzelm@60500
   307
  also note enumerate_mono[of n "Suc n", OF _ \<open>infinite S\<close>]
hoelzl@50134
   308
  finally show ?case by simp
wenzelm@53239
   309
qed
hoelzl@50134
   310
hoelzl@50134
   311
lemma enumerate_Suc'':
hoelzl@50134
   312
  fixes S :: "'a::wellorder set"
wenzelm@53239
   313
  assumes "infinite S"
wenzelm@53239
   314
  shows "enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
wenzelm@53239
   315
  using assms
hoelzl@50134
   316
proof (induct n arbitrary: S)
hoelzl@50134
   317
  case 0
wenzelm@53239
   318
  then have "\<forall>s \<in> S. enumerate S 0 \<le> s"
hoelzl@50134
   319
    by (auto simp: enumerate.simps intro: Least_le)
hoelzl@50134
   320
  then show ?case
hoelzl@50134
   321
    unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"]
wenzelm@53239
   322
    by (intro arg_cong[where f = Least] ext) auto
hoelzl@50134
   323
next
hoelzl@50134
   324
  case (Suc n S)
hoelzl@50134
   325
  show ?case
wenzelm@60500
   326
    using enumerate_mono[OF zero_less_Suc \<open>infinite S\<close>, of n] \<open>infinite S\<close>
hoelzl@50134
   327
    apply (subst (1 2) enumerate_Suc')
hoelzl@50134
   328
    apply (subst Suc)
wenzelm@60500
   329
    using \<open>infinite S\<close>
wenzelm@53239
   330
    apply simp
wenzelm@53239
   331
    apply (intro arg_cong[where f = Least] ext)
wenzelm@53239
   332
    apply (auto simp: enumerate_Suc'[symmetric])
wenzelm@53239
   333
    done
hoelzl@50134
   334
qed
hoelzl@50134
   335
hoelzl@50134
   336
lemma enumerate_Ex:
hoelzl@50134
   337
  assumes S: "infinite (S::nat set)"
hoelzl@50134
   338
  shows "s \<in> S \<Longrightarrow> \<exists>n. enumerate S n = s"
hoelzl@50134
   339
proof (induct s rule: less_induct)
hoelzl@50134
   340
  case (less s)
hoelzl@50134
   341
  show ?case
hoelzl@50134
   342
  proof cases
hoelzl@50134
   343
    let ?y = "Max {s'\<in>S. s' < s}"
hoelzl@50134
   344
    assume "\<exists>y\<in>S. y < s"
wenzelm@53239
   345
    then have y: "\<And>x. ?y < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)"
wenzelm@53239
   346
      by (subst Max_less_iff) auto
wenzelm@53239
   347
    then have y_in: "?y \<in> {s'\<in>S. s' < s}"
wenzelm@53239
   348
      by (intro Max_in) auto
wenzelm@53239
   349
    with less.hyps[of ?y] obtain n where "enumerate S n = ?y"
wenzelm@53239
   350
      by auto
hoelzl@50134
   351
    with S have "enumerate S (Suc n) = s"
hoelzl@50134
   352
      by (auto simp: y less enumerate_Suc'' intro!: Least_equality)
hoelzl@50134
   353
    then show ?case by auto
hoelzl@50134
   354
  next
hoelzl@50134
   355
    assume *: "\<not> (\<exists>y\<in>S. y < s)"
hoelzl@50134
   356
    then have "\<forall>t\<in>S. s \<le> t" by auto
wenzelm@60500
   357
    with \<open>s \<in> S\<close> show ?thesis
hoelzl@50134
   358
      by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0)
hoelzl@50134
   359
  qed
hoelzl@50134
   360
qed
hoelzl@50134
   361
hoelzl@50134
   362
lemma bij_enumerate:
hoelzl@50134
   363
  fixes S :: "nat set"
hoelzl@50134
   364
  assumes S: "infinite S"
hoelzl@50134
   365
  shows "bij_betw (enumerate S) UNIV S"
hoelzl@50134
   366
proof -
hoelzl@50134
   367
  have "\<And>n m. n \<noteq> m \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
wenzelm@60500
   368
    using enumerate_mono[OF _ \<open>infinite S\<close>] by (auto simp: neq_iff)
hoelzl@50134
   369
  then have "inj (enumerate S)"
hoelzl@50134
   370
    by (auto simp: inj_on_def)
wenzelm@53239
   371
  moreover have "\<forall>s \<in> S. \<exists>i. enumerate S i = s"
hoelzl@50134
   372
    using enumerate_Ex[OF S] by auto
wenzelm@60500
   373
  moreover note \<open>infinite S\<close>
hoelzl@50134
   374
  ultimately show ?thesis
hoelzl@50134
   375
    unfolding bij_betw_def by (auto intro: enumerate_in_set)
hoelzl@50134
   376
qed
hoelzl@50134
   377
wenzelm@20809
   378
subsection "Miscellaneous"
wenzelm@20809
   379
wenzelm@60500
   380
text \<open>
wenzelm@20809
   381
  A few trivial lemmas about sets that contain at most one element.
wenzelm@20809
   382
  These simplify the reasoning about deterministic automata.
wenzelm@60500
   383
\<close>
wenzelm@20809
   384
wenzelm@53239
   385
definition atmost_one :: "'a set \<Rightarrow> bool"
wenzelm@53239
   386
  where "atmost_one S \<longleftrightarrow> (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x = y)"
wenzelm@20809
   387
wenzelm@20809
   388
lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
wenzelm@20809
   389
  by (simp add: atmost_one_def)
wenzelm@20809
   390
wenzelm@20809
   391
lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
wenzelm@20809
   392
  by (simp add: atmost_one_def)
wenzelm@20809
   393
wenzelm@20809
   394
lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
wenzelm@20809
   395
  by (simp add: atmost_one_def)
wenzelm@20809
   396
wenzelm@20809
   397
end
traytel@54612
   398