src/HOL/Library/Infinite_Set.thy
author haftmann
Thu Jun 26 10:07:01 2008 +0200 (2008-06-26)
changeset 27368 9f90ac19e32b
parent 25671 5e9d6f77d11a
child 27407 68e111812b83
permissions -rw-r--r--
established Plain theory and image
wenzelm@20809
     1
(*  Title:      HOL/Infnite_Set.thy
wenzelm@20809
     2
    ID:         $Id$
wenzelm@20809
     3
    Author:     Stephan Merz
wenzelm@20809
     4
*)
wenzelm@20809
     5
wenzelm@20809
     6
header {* Infinite Sets and Related Concepts *}
wenzelm@20809
     7
wenzelm@20809
     8
theory Infinite_Set
haftmann@27368
     9
imports Plain SetInterval Hilbert_Choice
wenzelm@20809
    10
begin
wenzelm@20809
    11
haftmann@27368
    12
wenzelm@20809
    13
subsection "Infinite Sets"
wenzelm@20809
    14
wenzelm@20809
    15
text {*
wenzelm@20809
    16
  Some elementary facts about infinite sets, mostly by Stefan Merz.
wenzelm@20809
    17
  Beware! Because "infinite" merely abbreviates a negation, these
wenzelm@20809
    18
  lemmas may not work well with @{text "blast"}.
wenzelm@20809
    19
*}
wenzelm@20809
    20
wenzelm@20809
    21
abbreviation
wenzelm@21404
    22
  infinite :: "'a set \<Rightarrow> bool" where
wenzelm@20809
    23
  "infinite S == \<not> finite S"
wenzelm@20809
    24
wenzelm@20809
    25
text {*
wenzelm@20809
    26
  Infinite sets are non-empty, and if we remove some elements from an
wenzelm@20809
    27
  infinite set, the result is still infinite.
wenzelm@20809
    28
*}
wenzelm@20809
    29
wenzelm@20809
    30
lemma infinite_imp_nonempty: "infinite S ==> S \<noteq> {}"
wenzelm@20809
    31
  by auto
wenzelm@20809
    32
wenzelm@20809
    33
lemma infinite_remove:
wenzelm@20809
    34
  "infinite S \<Longrightarrow> infinite (S - {a})"
wenzelm@20809
    35
  by simp
wenzelm@20809
    36
wenzelm@20809
    37
lemma Diff_infinite_finite:
wenzelm@20809
    38
  assumes T: "finite T" and S: "infinite S"
wenzelm@20809
    39
  shows "infinite (S - T)"
wenzelm@20809
    40
  using T
wenzelm@20809
    41
proof induct
wenzelm@20809
    42
  from S
wenzelm@20809
    43
  show "infinite (S - {})" by auto
wenzelm@20809
    44
next
wenzelm@20809
    45
  fix T x
wenzelm@20809
    46
  assume ih: "infinite (S - T)"
wenzelm@20809
    47
  have "S - (insert x T) = (S - T) - {x}"
wenzelm@20809
    48
    by (rule Diff_insert)
wenzelm@20809
    49
  with ih
wenzelm@20809
    50
  show "infinite (S - (insert x T))"
wenzelm@20809
    51
    by (simp add: infinite_remove)
wenzelm@20809
    52
qed
wenzelm@20809
    53
wenzelm@20809
    54
lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
wenzelm@20809
    55
  by simp
wenzelm@20809
    56
wenzelm@20809
    57
lemma infinite_super:
wenzelm@20809
    58
  assumes T: "S \<subseteq> T" and S: "infinite S"
wenzelm@20809
    59
  shows "infinite T"
wenzelm@20809
    60
proof
wenzelm@20809
    61
  assume "finite T"
wenzelm@20809
    62
  with T have "finite S" by (simp add: finite_subset)
wenzelm@20809
    63
  with S show False by simp
wenzelm@20809
    64
qed
wenzelm@20809
    65
wenzelm@20809
    66
text {*
wenzelm@20809
    67
  As a concrete example, we prove that the set of natural numbers is
wenzelm@20809
    68
  infinite.
wenzelm@20809
    69
*}
wenzelm@20809
    70
wenzelm@20809
    71
lemma finite_nat_bounded:
wenzelm@20809
    72
  assumes S: "finite (S::nat set)"
wenzelm@20809
    73
  shows "\<exists>k. S \<subseteq> {..<k}"  (is "\<exists>k. ?bounded S k")
wenzelm@20809
    74
using S
wenzelm@20809
    75
proof induct
wenzelm@20809
    76
  have "?bounded {} 0" by simp
wenzelm@20809
    77
  then show "\<exists>k. ?bounded {} k" ..
wenzelm@20809
    78
next
wenzelm@20809
    79
  fix S x
wenzelm@20809
    80
  assume "\<exists>k. ?bounded S k"
wenzelm@20809
    81
  then obtain k where k: "?bounded S k" ..
wenzelm@20809
    82
  show "\<exists>k. ?bounded (insert x S) k"
wenzelm@20809
    83
  proof (cases "x < k")
wenzelm@20809
    84
    case True
wenzelm@20809
    85
    with k show ?thesis by auto
wenzelm@20809
    86
  next
wenzelm@20809
    87
    case False
wenzelm@20809
    88
    with k have "?bounded S (Suc x)" by auto
wenzelm@20809
    89
    then show ?thesis by auto
wenzelm@20809
    90
  qed
wenzelm@20809
    91
qed
wenzelm@20809
    92
wenzelm@20809
    93
lemma finite_nat_iff_bounded:
wenzelm@20809
    94
  "finite (S::nat set) = (\<exists>k. S \<subseteq> {..<k})"  (is "?lhs = ?rhs")
wenzelm@20809
    95
proof
wenzelm@20809
    96
  assume ?lhs
wenzelm@20809
    97
  then show ?rhs by (rule finite_nat_bounded)
wenzelm@20809
    98
next
wenzelm@20809
    99
  assume ?rhs
wenzelm@20809
   100
  then obtain k where "S \<subseteq> {..<k}" ..
wenzelm@20809
   101
  then show "finite S"
wenzelm@20809
   102
    by (rule finite_subset) simp
wenzelm@20809
   103
qed
wenzelm@20809
   104
wenzelm@20809
   105
lemma finite_nat_iff_bounded_le:
wenzelm@20809
   106
  "finite (S::nat set) = (\<exists>k. S \<subseteq> {..k})"  (is "?lhs = ?rhs")
wenzelm@20809
   107
proof
wenzelm@20809
   108
  assume ?lhs
wenzelm@20809
   109
  then obtain k where "S \<subseteq> {..<k}"
wenzelm@20809
   110
    by (blast dest: finite_nat_bounded)
wenzelm@20809
   111
  then have "S \<subseteq> {..k}" by auto
wenzelm@20809
   112
  then show ?rhs ..
wenzelm@20809
   113
next
wenzelm@20809
   114
  assume ?rhs
wenzelm@20809
   115
  then obtain k where "S \<subseteq> {..k}" ..
wenzelm@20809
   116
  then show "finite S"
wenzelm@20809
   117
    by (rule finite_subset) simp
wenzelm@20809
   118
qed
wenzelm@20809
   119
wenzelm@20809
   120
lemma infinite_nat_iff_unbounded:
wenzelm@20809
   121
  "infinite (S::nat set) = (\<forall>m. \<exists>n. m<n \<and> n\<in>S)"
wenzelm@20809
   122
  (is "?lhs = ?rhs")
wenzelm@20809
   123
proof
wenzelm@20809
   124
  assume ?lhs
wenzelm@20809
   125
  show ?rhs
wenzelm@20809
   126
  proof (rule ccontr)
wenzelm@20809
   127
    assume "\<not> ?rhs"
wenzelm@20809
   128
    then obtain m where m: "\<forall>n. m<n \<longrightarrow> n\<notin>S" by blast
wenzelm@20809
   129
    then have "S \<subseteq> {..m}"
wenzelm@20809
   130
      by (auto simp add: sym [OF linorder_not_less])
wenzelm@20809
   131
    with `?lhs` show False
wenzelm@20809
   132
      by (simp add: finite_nat_iff_bounded_le)
wenzelm@20809
   133
  qed
wenzelm@20809
   134
next
wenzelm@20809
   135
  assume ?rhs
wenzelm@20809
   136
  show ?lhs
wenzelm@20809
   137
  proof
wenzelm@20809
   138
    assume "finite S"
wenzelm@20809
   139
    then obtain m where "S \<subseteq> {..m}"
wenzelm@20809
   140
      by (auto simp add: finite_nat_iff_bounded_le)
wenzelm@20809
   141
    then have "\<forall>n. m<n \<longrightarrow> n\<notin>S" by auto
wenzelm@20809
   142
    with `?rhs` show False by blast
wenzelm@20809
   143
  qed
wenzelm@20809
   144
qed
wenzelm@20809
   145
wenzelm@20809
   146
lemma infinite_nat_iff_unbounded_le:
wenzelm@20809
   147
  "infinite (S::nat set) = (\<forall>m. \<exists>n. m\<le>n \<and> n\<in>S)"
wenzelm@20809
   148
  (is "?lhs = ?rhs")
wenzelm@20809
   149
proof
wenzelm@20809
   150
  assume ?lhs
wenzelm@20809
   151
  show ?rhs
wenzelm@20809
   152
  proof
wenzelm@20809
   153
    fix m
wenzelm@20809
   154
    from `?lhs` obtain n where "m<n \<and> n\<in>S"
wenzelm@20809
   155
      by (auto simp add: infinite_nat_iff_unbounded)
wenzelm@20809
   156
    then have "m\<le>n \<and> n\<in>S" by simp
wenzelm@20809
   157
    then show "\<exists>n. m \<le> n \<and> n \<in> S" ..
wenzelm@20809
   158
  qed
wenzelm@20809
   159
next
wenzelm@20809
   160
  assume ?rhs
wenzelm@20809
   161
  show ?lhs
wenzelm@20809
   162
  proof (auto simp add: infinite_nat_iff_unbounded)
wenzelm@20809
   163
    fix m
wenzelm@20809
   164
    from `?rhs` obtain n where "Suc m \<le> n \<and> n\<in>S"
wenzelm@20809
   165
      by blast
wenzelm@20809
   166
    then have "m<n \<and> n\<in>S" by simp
wenzelm@20809
   167
    then show "\<exists>n. m < n \<and> n \<in> S" ..
wenzelm@20809
   168
  qed
wenzelm@20809
   169
qed
wenzelm@20809
   170
wenzelm@20809
   171
text {*
wenzelm@20809
   172
  For a set of natural numbers to be infinite, it is enough to know
wenzelm@20809
   173
  that for any number larger than some @{text k}, there is some larger
wenzelm@20809
   174
  number that is an element of the set.
wenzelm@20809
   175
*}
wenzelm@20809
   176
wenzelm@20809
   177
lemma unbounded_k_infinite:
wenzelm@20809
   178
  assumes k: "\<forall>m. k<m \<longrightarrow> (\<exists>n. m<n \<and> n\<in>S)"
wenzelm@20809
   179
  shows "infinite (S::nat set)"
wenzelm@20809
   180
proof -
wenzelm@20809
   181
  {
wenzelm@20809
   182
    fix m have "\<exists>n. m<n \<and> n\<in>S"
wenzelm@20809
   183
    proof (cases "k<m")
wenzelm@20809
   184
      case True
wenzelm@20809
   185
      with k show ?thesis by blast
wenzelm@20809
   186
    next
wenzelm@20809
   187
      case False
wenzelm@20809
   188
      from k obtain n where "Suc k < n \<and> n\<in>S" by auto
wenzelm@20809
   189
      with False have "m<n \<and> n\<in>S" by auto
wenzelm@20809
   190
      then show ?thesis ..
wenzelm@20809
   191
    qed
wenzelm@20809
   192
  }
wenzelm@20809
   193
  then show ?thesis
wenzelm@20809
   194
    by (auto simp add: infinite_nat_iff_unbounded)
wenzelm@20809
   195
qed
wenzelm@20809
   196
wenzelm@20809
   197
lemma nat_infinite [simp]: "infinite (UNIV :: nat set)"
wenzelm@20809
   198
  by (auto simp add: infinite_nat_iff_unbounded)
wenzelm@20809
   199
wenzelm@20809
   200
lemma nat_not_finite [elim]: "finite (UNIV::nat set) \<Longrightarrow> R"
wenzelm@20809
   201
  by simp
wenzelm@20809
   202
wenzelm@20809
   203
text {*
wenzelm@20809
   204
  Every infinite set contains a countable subset. More precisely we
wenzelm@20809
   205
  show that a set @{text S} is infinite if and only if there exists an
wenzelm@20809
   206
  injective function from the naturals into @{text S}.
wenzelm@20809
   207
*}
wenzelm@20809
   208
wenzelm@20809
   209
lemma range_inj_infinite:
wenzelm@20809
   210
  "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
wenzelm@20809
   211
proof
wenzelm@20809
   212
  assume "inj f"
wenzelm@20809
   213
    and  "finite (range f)"
wenzelm@20809
   214
  then have "finite (UNIV::nat set)"
wenzelm@20809
   215
    by (auto intro: finite_imageD simp del: nat_infinite)
wenzelm@20809
   216
  then show False by simp
wenzelm@20809
   217
qed
wenzelm@20809
   218
paulson@22226
   219
lemma int_infinite [simp]:
paulson@22226
   220
  shows "infinite (UNIV::int set)"
paulson@22226
   221
proof -
paulson@22226
   222
  from inj_int have "infinite (range int)" by (rule range_inj_infinite)
paulson@22226
   223
  moreover 
paulson@22226
   224
  have "range int \<subseteq> (UNIV::int set)" by simp
paulson@22226
   225
  ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super)
paulson@22226
   226
qed
paulson@22226
   227
wenzelm@20809
   228
text {*
wenzelm@20809
   229
  The ``only if'' direction is harder because it requires the
wenzelm@20809
   230
  construction of a sequence of pairwise different elements of an
wenzelm@20809
   231
  infinite set @{text S}. The idea is to construct a sequence of
wenzelm@20809
   232
  non-empty and infinite subsets of @{text S} obtained by successively
wenzelm@20809
   233
  removing elements of @{text S}.
wenzelm@20809
   234
*}
wenzelm@20809
   235
wenzelm@20809
   236
lemma linorder_injI:
wenzelm@20809
   237
  assumes hyp: "!!x y. x < (y::'a::linorder) ==> f x \<noteq> f y"
wenzelm@20809
   238
  shows "inj f"
wenzelm@20809
   239
proof (rule inj_onI)
wenzelm@20809
   240
  fix x y
wenzelm@20809
   241
  assume f_eq: "f x = f y"
wenzelm@20809
   242
  show "x = y"
wenzelm@20809
   243
  proof (rule linorder_cases)
wenzelm@20809
   244
    assume "x < y"
wenzelm@20809
   245
    with hyp have "f x \<noteq> f y" by blast
wenzelm@20809
   246
    with f_eq show ?thesis by simp
wenzelm@20809
   247
  next
wenzelm@20809
   248
    assume "x = y"
wenzelm@20809
   249
    then show ?thesis .
wenzelm@20809
   250
  next
wenzelm@20809
   251
    assume "y < x"
wenzelm@20809
   252
    with hyp have "f y \<noteq> f x" by blast
wenzelm@20809
   253
    with f_eq show ?thesis by simp
wenzelm@20809
   254
  qed
wenzelm@20809
   255
qed
wenzelm@20809
   256
wenzelm@20809
   257
lemma infinite_countable_subset:
wenzelm@20809
   258
  assumes inf: "infinite (S::'a set)"
wenzelm@20809
   259
  shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
wenzelm@20809
   260
proof -
wenzelm@20809
   261
  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
wenzelm@20809
   262
  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
wenzelm@20809
   263
  have Sseq_inf: "\<And>n. infinite (Sseq n)"
wenzelm@20809
   264
  proof -
wenzelm@20809
   265
    fix n
wenzelm@20809
   266
    show "infinite (Sseq n)"
wenzelm@20809
   267
    proof (induct n)
wenzelm@20809
   268
      from inf show "infinite (Sseq 0)"
wenzelm@20809
   269
        by (simp add: Sseq_def)
wenzelm@20809
   270
    next
wenzelm@20809
   271
      fix n
wenzelm@20809
   272
      assume "infinite (Sseq n)" then show "infinite (Sseq (Suc n))"
wenzelm@20809
   273
        by (simp add: Sseq_def infinite_remove)
wenzelm@20809
   274
    qed
wenzelm@20809
   275
  qed
wenzelm@20809
   276
  have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
wenzelm@20809
   277
  proof -
wenzelm@20809
   278
    fix n
wenzelm@20809
   279
    show "Sseq n \<subseteq> S"
wenzelm@20809
   280
      by (induct n) (auto simp add: Sseq_def)
wenzelm@20809
   281
  qed
wenzelm@20809
   282
  have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
wenzelm@20809
   283
  proof -
wenzelm@20809
   284
    fix n
wenzelm@20809
   285
    show "pick n \<in> Sseq n"
wenzelm@20809
   286
    proof (unfold pick_def, rule someI_ex)
wenzelm@20809
   287
      from Sseq_inf have "infinite (Sseq n)" .
wenzelm@20809
   288
      then have "Sseq n \<noteq> {}" by auto
wenzelm@20809
   289
      then show "\<exists>x. x \<in> Sseq n" by auto
wenzelm@20809
   290
    qed
wenzelm@20809
   291
  qed
wenzelm@20809
   292
  with Sseq_S have rng: "range pick \<subseteq> S"
wenzelm@20809
   293
    by auto
wenzelm@20809
   294
  have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
wenzelm@20809
   295
  proof -
wenzelm@20809
   296
    fix n m
wenzelm@20809
   297
    show "pick n \<notin> Sseq (n + Suc m)"
wenzelm@20809
   298
      by (induct m) (auto simp add: Sseq_def pick_def)
wenzelm@20809
   299
  qed
wenzelm@20809
   300
  have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
wenzelm@20809
   301
  proof -
wenzelm@20809
   302
    fix n m
wenzelm@20809
   303
    from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
wenzelm@20809
   304
    moreover from pick_Sseq_gt
wenzelm@20809
   305
    have "pick n \<notin> Sseq (n + Suc m)" .
wenzelm@20809
   306
    ultimately show "pick n \<noteq> pick (n + Suc m)"
wenzelm@20809
   307
      by auto
wenzelm@20809
   308
  qed
wenzelm@20809
   309
  have inj: "inj pick"
wenzelm@20809
   310
  proof (rule linorder_injI)
wenzelm@20809
   311
    fix i j :: nat
wenzelm@20809
   312
    assume "i < j"
wenzelm@20809
   313
    show "pick i \<noteq> pick j"
wenzelm@20809
   314
    proof
wenzelm@20809
   315
      assume eq: "pick i = pick j"
wenzelm@20809
   316
      from `i < j` obtain k where "j = i + Suc k"
wenzelm@20809
   317
        by (auto simp add: less_iff_Suc_add)
wenzelm@20809
   318
      with pick_pick have "pick i \<noteq> pick j" by simp
wenzelm@20809
   319
      with eq show False by simp
wenzelm@20809
   320
    qed
wenzelm@20809
   321
  qed
wenzelm@20809
   322
  from rng inj show ?thesis by auto
wenzelm@20809
   323
qed
wenzelm@20809
   324
wenzelm@20809
   325
lemma infinite_iff_countable_subset:
wenzelm@20809
   326
    "infinite S = (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
wenzelm@20809
   327
  by (auto simp add: infinite_countable_subset range_inj_infinite infinite_super)
wenzelm@20809
   328
wenzelm@20809
   329
text {*
wenzelm@20809
   330
  For any function with infinite domain and finite range there is some
wenzelm@20809
   331
  element that is the image of infinitely many domain elements.  In
wenzelm@20809
   332
  particular, any infinite sequence of elements from a finite set
wenzelm@20809
   333
  contains some element that occurs infinitely often.
wenzelm@20809
   334
*}
wenzelm@20809
   335
wenzelm@20809
   336
lemma inf_img_fin_dom:
wenzelm@20809
   337
  assumes img: "finite (f`A)" and dom: "infinite A"
wenzelm@20809
   338
  shows "\<exists>y \<in> f`A. infinite (f -` {y})"
wenzelm@20809
   339
proof (rule ccontr)
wenzelm@20809
   340
  assume "\<not> ?thesis"
wenzelm@20809
   341
  with img have "finite (UN y:f`A. f -` {y})" by (blast intro: finite_UN_I)
wenzelm@20809
   342
  moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
wenzelm@20809
   343
  moreover note dom
wenzelm@20809
   344
  ultimately show False by (simp add: infinite_super)
wenzelm@20809
   345
qed
wenzelm@20809
   346
wenzelm@20809
   347
lemma inf_img_fin_domE:
wenzelm@20809
   348
  assumes "finite (f`A)" and "infinite A"
wenzelm@20809
   349
  obtains y where "y \<in> f`A" and "infinite (f -` {y})"
wenzelm@23394
   350
  using assms by (blast dest: inf_img_fin_dom)
wenzelm@20809
   351
wenzelm@20809
   352
wenzelm@20809
   353
subsection "Infinitely Many and Almost All"
wenzelm@20809
   354
wenzelm@20809
   355
text {*
wenzelm@20809
   356
  We often need to reason about the existence of infinitely many
wenzelm@20809
   357
  (resp., all but finitely many) objects satisfying some predicate, so
wenzelm@20809
   358
  we introduce corresponding binders and their proof rules.
wenzelm@20809
   359
*}
wenzelm@20809
   360
wenzelm@20809
   361
definition
berghofe@22432
   362
  Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
wenzelm@20809
   363
  "Inf_many P = infinite {x. P x}"
wenzelm@21404
   364
wenzelm@21404
   365
definition
wenzelm@21404
   366
  Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
berghofe@22432
   367
  "Alm_all P = (\<not> (INFM x. \<not> P x))"
wenzelm@20809
   368
wenzelm@21210
   369
notation (xsymbols)
wenzelm@21404
   370
  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
wenzelm@20809
   371
  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
wenzelm@20809
   372
wenzelm@21210
   373
notation (HTML output)
wenzelm@21404
   374
  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
wenzelm@20809
   375
  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
wenzelm@20809
   376
wenzelm@20809
   377
lemma INF_EX:
wenzelm@20809
   378
  "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
wenzelm@20809
   379
  unfolding Inf_many_def
wenzelm@20809
   380
proof (rule ccontr)
wenzelm@20809
   381
  assume inf: "infinite {x. P x}"
wenzelm@20809
   382
  assume "\<not> ?thesis" then have "{x. P x} = {}" by simp
wenzelm@20809
   383
  then have "finite {x. P x}" by simp
wenzelm@20809
   384
  with inf show False by simp
wenzelm@20809
   385
qed
wenzelm@20809
   386
wenzelm@20809
   387
lemma MOST_iff_finiteNeg: "(\<forall>\<^sub>\<infinity>x. P x) = finite {x. \<not> P x}"
wenzelm@20809
   388
  by (simp add: Alm_all_def Inf_many_def)
wenzelm@20809
   389
wenzelm@20809
   390
lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
wenzelm@20809
   391
  by (simp add: MOST_iff_finiteNeg)
wenzelm@20809
   392
wenzelm@20809
   393
lemma INF_mono:
wenzelm@20809
   394
  assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
wenzelm@20809
   395
  shows "\<exists>\<^sub>\<infinity>x. Q x"
wenzelm@20809
   396
proof -
wenzelm@20809
   397
  from inf have "infinite {x. P x}" unfolding Inf_many_def .
wenzelm@20809
   398
  moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
wenzelm@20809
   399
  ultimately show ?thesis
wenzelm@20809
   400
    by (simp add: Inf_many_def infinite_super)
wenzelm@20809
   401
qed
wenzelm@20809
   402
wenzelm@20809
   403
lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
wenzelm@20809
   404
  unfolding Alm_all_def by (blast intro: INF_mono)
wenzelm@20809
   405
wenzelm@20809
   406
lemma INF_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
wenzelm@20809
   407
  by (simp add: Inf_many_def infinite_nat_iff_unbounded)
wenzelm@20809
   408
wenzelm@20809
   409
lemma INF_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
wenzelm@20809
   410
  by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
wenzelm@20809
   411
wenzelm@20809
   412
lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
wenzelm@20809
   413
  by (simp add: Alm_all_def INF_nat)
wenzelm@20809
   414
wenzelm@20809
   415
lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
wenzelm@20809
   416
  by (simp add: Alm_all_def INF_nat_le)
wenzelm@20809
   417
wenzelm@20809
   418
wenzelm@20809
   419
subsection "Enumeration of an Infinite Set"
wenzelm@20809
   420
wenzelm@20809
   421
text {*
wenzelm@20809
   422
  The set's element type must be wellordered (e.g. the natural numbers).
wenzelm@20809
   423
*}
wenzelm@20809
   424
wenzelm@20809
   425
consts
wenzelm@20809
   426
  enumerate   :: "'a::wellorder set => (nat => 'a::wellorder)"
wenzelm@20809
   427
primrec
wenzelm@20809
   428
  enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
wenzelm@20809
   429
  enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
wenzelm@20809
   430
wenzelm@20809
   431
lemma enumerate_Suc':
wenzelm@20809
   432
    "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
wenzelm@20809
   433
  by simp
wenzelm@20809
   434
wenzelm@20809
   435
lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
wenzelm@20809
   436
  apply (induct n arbitrary: S)
wenzelm@20809
   437
   apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
wenzelm@20809
   438
  apply (fastsimp iff: finite_Diff_singleton)
wenzelm@20809
   439
  done
wenzelm@20809
   440
wenzelm@20809
   441
declare enumerate_0 [simp del] enumerate_Suc [simp del]
wenzelm@20809
   442
wenzelm@20809
   443
lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
wenzelm@20809
   444
  apply (induct n arbitrary: S)
wenzelm@20809
   445
   apply (rule order_le_neq_trans)
wenzelm@20809
   446
    apply (simp add: enumerate_0 Least_le enumerate_in_set)
wenzelm@20809
   447
   apply (simp only: enumerate_Suc')
wenzelm@20809
   448
   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
wenzelm@20809
   449
    apply (blast intro: sym)
wenzelm@20809
   450
   apply (simp add: enumerate_in_set del: Diff_iff)
wenzelm@20809
   451
  apply (simp add: enumerate_Suc')
wenzelm@20809
   452
  done
wenzelm@20809
   453
wenzelm@20809
   454
lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
wenzelm@20809
   455
  apply (erule less_Suc_induct)
wenzelm@20809
   456
  apply (auto intro: enumerate_step)
wenzelm@20809
   457
  done
wenzelm@20809
   458
wenzelm@20809
   459
wenzelm@20809
   460
subsection "Miscellaneous"
wenzelm@20809
   461
wenzelm@20809
   462
text {*
wenzelm@20809
   463
  A few trivial lemmas about sets that contain at most one element.
wenzelm@20809
   464
  These simplify the reasoning about deterministic automata.
wenzelm@20809
   465
*}
wenzelm@20809
   466
wenzelm@20809
   467
definition
wenzelm@21404
   468
  atmost_one :: "'a set \<Rightarrow> bool" where
wenzelm@20809
   469
  "atmost_one S = (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y)"
wenzelm@20809
   470
wenzelm@20809
   471
lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
wenzelm@20809
   472
  by (simp add: atmost_one_def)
wenzelm@20809
   473
wenzelm@20809
   474
lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
wenzelm@20809
   475
  by (simp add: atmost_one_def)
wenzelm@20809
   476
wenzelm@20809
   477
lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
wenzelm@20809
   478
  by (simp add: atmost_one_def)
wenzelm@20809
   479
wenzelm@20809
   480
end