src/HOL/Library/Infinite_Set.thy
author Andreas Lochbihler
Wed Feb 27 10:33:30 2013 +0100 (2013-02-27)
changeset 51288 be7e9a675ec9
parent 50134 13211e07d931
child 53239 2f21813cf2f0
permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
huffman@27407
     1
(*  Title:      HOL/Library/Infinite_Set.thy
wenzelm@20809
     2
    Author:     Stephan Merz
wenzelm@20809
     3
*)
wenzelm@20809
     4
wenzelm@20809
     5
header {* Infinite Sets and Related Concepts *}
wenzelm@20809
     6
wenzelm@20809
     7
theory Infinite_Set
haftmann@30663
     8
imports Main
wenzelm@20809
     9
begin
wenzelm@20809
    10
wenzelm@20809
    11
subsection "Infinite Sets"
wenzelm@20809
    12
wenzelm@20809
    13
text {*
wenzelm@20809
    14
  Some elementary facts about infinite sets, mostly by Stefan Merz.
wenzelm@20809
    15
  Beware! Because "infinite" merely abbreviates a negation, these
wenzelm@20809
    16
  lemmas may not work well with @{text "blast"}.
wenzelm@20809
    17
*}
wenzelm@20809
    18
wenzelm@20809
    19
abbreviation
wenzelm@21404
    20
  infinite :: "'a set \<Rightarrow> bool" where
wenzelm@20809
    21
  "infinite S == \<not> finite S"
wenzelm@20809
    22
wenzelm@20809
    23
text {*
wenzelm@20809
    24
  Infinite sets are non-empty, and if we remove some elements from an
wenzelm@20809
    25
  infinite set, the result is still infinite.
wenzelm@20809
    26
*}
wenzelm@20809
    27
wenzelm@20809
    28
lemma infinite_imp_nonempty: "infinite S ==> S \<noteq> {}"
wenzelm@20809
    29
  by auto
wenzelm@20809
    30
wenzelm@20809
    31
lemma infinite_remove:
wenzelm@20809
    32
  "infinite S \<Longrightarrow> infinite (S - {a})"
wenzelm@20809
    33
  by simp
wenzelm@20809
    34
wenzelm@20809
    35
lemma Diff_infinite_finite:
wenzelm@20809
    36
  assumes T: "finite T" and S: "infinite S"
wenzelm@20809
    37
  shows "infinite (S - T)"
wenzelm@20809
    38
  using T
wenzelm@20809
    39
proof induct
wenzelm@20809
    40
  from S
wenzelm@20809
    41
  show "infinite (S - {})" by auto
wenzelm@20809
    42
next
wenzelm@20809
    43
  fix T x
wenzelm@20809
    44
  assume ih: "infinite (S - T)"
wenzelm@20809
    45
  have "S - (insert x T) = (S - T) - {x}"
wenzelm@20809
    46
    by (rule Diff_insert)
wenzelm@20809
    47
  with ih
wenzelm@20809
    48
  show "infinite (S - (insert x T))"
wenzelm@20809
    49
    by (simp add: infinite_remove)
wenzelm@20809
    50
qed
wenzelm@20809
    51
wenzelm@20809
    52
lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
wenzelm@20809
    53
  by simp
wenzelm@20809
    54
urbanc@35844
    55
lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
urbanc@35844
    56
  by simp
urbanc@35844
    57
wenzelm@20809
    58
lemma infinite_super:
wenzelm@20809
    59
  assumes T: "S \<subseteq> T" and S: "infinite S"
wenzelm@20809
    60
  shows "infinite T"
wenzelm@20809
    61
proof
wenzelm@20809
    62
  assume "finite T"
wenzelm@20809
    63
  with T have "finite S" by (simp add: finite_subset)
wenzelm@20809
    64
  with S show False by simp
wenzelm@20809
    65
qed
wenzelm@20809
    66
wenzelm@20809
    67
text {*
wenzelm@20809
    68
  As a concrete example, we prove that the set of natural numbers is
wenzelm@20809
    69
  infinite.
wenzelm@20809
    70
*}
wenzelm@20809
    71
wenzelm@20809
    72
lemma finite_nat_bounded:
wenzelm@20809
    73
  assumes S: "finite (S::nat set)"
wenzelm@20809
    74
  shows "\<exists>k. S \<subseteq> {..<k}"  (is "\<exists>k. ?bounded S k")
wenzelm@20809
    75
using S
wenzelm@20809
    76
proof induct
wenzelm@20809
    77
  have "?bounded {} 0" by simp
wenzelm@20809
    78
  then show "\<exists>k. ?bounded {} k" ..
wenzelm@20809
    79
next
wenzelm@20809
    80
  fix S x
wenzelm@20809
    81
  assume "\<exists>k. ?bounded S k"
wenzelm@20809
    82
  then obtain k where k: "?bounded S k" ..
wenzelm@20809
    83
  show "\<exists>k. ?bounded (insert x S) k"
wenzelm@20809
    84
  proof (cases "x < k")
wenzelm@20809
    85
    case True
wenzelm@20809
    86
    with k show ?thesis by auto
wenzelm@20809
    87
  next
wenzelm@20809
    88
    case False
wenzelm@20809
    89
    with k have "?bounded S (Suc x)" by auto
wenzelm@20809
    90
    then show ?thesis by auto
wenzelm@20809
    91
  qed
wenzelm@20809
    92
qed
wenzelm@20809
    93
wenzelm@20809
    94
lemma finite_nat_iff_bounded:
wenzelm@20809
    95
  "finite (S::nat set) = (\<exists>k. S \<subseteq> {..<k})"  (is "?lhs = ?rhs")
wenzelm@20809
    96
proof
wenzelm@20809
    97
  assume ?lhs
wenzelm@20809
    98
  then show ?rhs by (rule finite_nat_bounded)
wenzelm@20809
    99
next
wenzelm@20809
   100
  assume ?rhs
wenzelm@20809
   101
  then obtain k where "S \<subseteq> {..<k}" ..
wenzelm@20809
   102
  then show "finite S"
wenzelm@20809
   103
    by (rule finite_subset) simp
wenzelm@20809
   104
qed
wenzelm@20809
   105
wenzelm@20809
   106
lemma finite_nat_iff_bounded_le:
wenzelm@20809
   107
  "finite (S::nat set) = (\<exists>k. S \<subseteq> {..k})"  (is "?lhs = ?rhs")
wenzelm@20809
   108
proof
wenzelm@20809
   109
  assume ?lhs
wenzelm@20809
   110
  then obtain k where "S \<subseteq> {..<k}"
wenzelm@20809
   111
    by (blast dest: finite_nat_bounded)
wenzelm@20809
   112
  then have "S \<subseteq> {..k}" by auto
wenzelm@20809
   113
  then show ?rhs ..
wenzelm@20809
   114
next
wenzelm@20809
   115
  assume ?rhs
wenzelm@20809
   116
  then obtain k where "S \<subseteq> {..k}" ..
wenzelm@20809
   117
  then show "finite S"
wenzelm@20809
   118
    by (rule finite_subset) simp
wenzelm@20809
   119
qed
wenzelm@20809
   120
wenzelm@20809
   121
lemma infinite_nat_iff_unbounded:
wenzelm@20809
   122
  "infinite (S::nat set) = (\<forall>m. \<exists>n. m<n \<and> n\<in>S)"
wenzelm@20809
   123
  (is "?lhs = ?rhs")
wenzelm@20809
   124
proof
wenzelm@20809
   125
  assume ?lhs
wenzelm@20809
   126
  show ?rhs
wenzelm@20809
   127
  proof (rule ccontr)
wenzelm@20809
   128
    assume "\<not> ?rhs"
wenzelm@20809
   129
    then obtain m where m: "\<forall>n. m<n \<longrightarrow> n\<notin>S" by blast
wenzelm@20809
   130
    then have "S \<subseteq> {..m}"
wenzelm@20809
   131
      by (auto simp add: sym [OF linorder_not_less])
wenzelm@20809
   132
    with `?lhs` show False
wenzelm@20809
   133
      by (simp add: finite_nat_iff_bounded_le)
wenzelm@20809
   134
  qed
wenzelm@20809
   135
next
wenzelm@20809
   136
  assume ?rhs
wenzelm@20809
   137
  show ?lhs
wenzelm@20809
   138
  proof
wenzelm@20809
   139
    assume "finite S"
wenzelm@20809
   140
    then obtain m where "S \<subseteq> {..m}"
wenzelm@20809
   141
      by (auto simp add: finite_nat_iff_bounded_le)
wenzelm@20809
   142
    then have "\<forall>n. m<n \<longrightarrow> n\<notin>S" by auto
wenzelm@20809
   143
    with `?rhs` show False by blast
wenzelm@20809
   144
  qed
wenzelm@20809
   145
qed
wenzelm@20809
   146
wenzelm@20809
   147
lemma infinite_nat_iff_unbounded_le:
wenzelm@20809
   148
  "infinite (S::nat set) = (\<forall>m. \<exists>n. m\<le>n \<and> n\<in>S)"
wenzelm@20809
   149
  (is "?lhs = ?rhs")
wenzelm@20809
   150
proof
wenzelm@20809
   151
  assume ?lhs
wenzelm@20809
   152
  show ?rhs
wenzelm@20809
   153
  proof
wenzelm@20809
   154
    fix m
wenzelm@20809
   155
    from `?lhs` obtain n where "m<n \<and> n\<in>S"
wenzelm@20809
   156
      by (auto simp add: infinite_nat_iff_unbounded)
wenzelm@20809
   157
    then have "m\<le>n \<and> n\<in>S" by simp
wenzelm@20809
   158
    then show "\<exists>n. m \<le> n \<and> n \<in> S" ..
wenzelm@20809
   159
  qed
wenzelm@20809
   160
next
wenzelm@20809
   161
  assume ?rhs
wenzelm@20809
   162
  show ?lhs
wenzelm@20809
   163
  proof (auto simp add: infinite_nat_iff_unbounded)
wenzelm@20809
   164
    fix m
wenzelm@20809
   165
    from `?rhs` obtain n where "Suc m \<le> n \<and> n\<in>S"
wenzelm@20809
   166
      by blast
wenzelm@20809
   167
    then have "m<n \<and> n\<in>S" by simp
wenzelm@20809
   168
    then show "\<exists>n. m < n \<and> n \<in> S" ..
wenzelm@20809
   169
  qed
wenzelm@20809
   170
qed
wenzelm@20809
   171
wenzelm@20809
   172
text {*
wenzelm@20809
   173
  For a set of natural numbers to be infinite, it is enough to know
wenzelm@20809
   174
  that for any number larger than some @{text k}, there is some larger
wenzelm@20809
   175
  number that is an element of the set.
wenzelm@20809
   176
*}
wenzelm@20809
   177
wenzelm@20809
   178
lemma unbounded_k_infinite:
wenzelm@20809
   179
  assumes k: "\<forall>m. k<m \<longrightarrow> (\<exists>n. m<n \<and> n\<in>S)"
wenzelm@20809
   180
  shows "infinite (S::nat set)"
wenzelm@20809
   181
proof -
wenzelm@20809
   182
  {
wenzelm@20809
   183
    fix m have "\<exists>n. m<n \<and> n\<in>S"
wenzelm@20809
   184
    proof (cases "k<m")
wenzelm@20809
   185
      case True
wenzelm@20809
   186
      with k show ?thesis by blast
wenzelm@20809
   187
    next
wenzelm@20809
   188
      case False
wenzelm@20809
   189
      from k obtain n where "Suc k < n \<and> n\<in>S" by auto
wenzelm@20809
   190
      with False have "m<n \<and> n\<in>S" by auto
wenzelm@20809
   191
      then show ?thesis ..
wenzelm@20809
   192
    qed
wenzelm@20809
   193
  }
wenzelm@20809
   194
  then show ?thesis
wenzelm@20809
   195
    by (auto simp add: infinite_nat_iff_unbounded)
wenzelm@20809
   196
qed
wenzelm@20809
   197
huffman@35056
   198
(* duplicates Finite_Set.infinite_UNIV_nat *)
huffman@35056
   199
lemma nat_infinite: "infinite (UNIV :: nat set)"
wenzelm@20809
   200
  by (auto simp add: infinite_nat_iff_unbounded)
wenzelm@20809
   201
huffman@35056
   202
lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
wenzelm@20809
   203
  by simp
wenzelm@20809
   204
wenzelm@20809
   205
text {*
wenzelm@20809
   206
  Every infinite set contains a countable subset. More precisely we
wenzelm@20809
   207
  show that a set @{text S} is infinite if and only if there exists an
wenzelm@20809
   208
  injective function from the naturals into @{text S}.
wenzelm@20809
   209
*}
wenzelm@20809
   210
wenzelm@20809
   211
lemma range_inj_infinite:
wenzelm@20809
   212
  "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
wenzelm@20809
   213
proof
huffman@27407
   214
  assume "finite (range f)" and "inj f"
wenzelm@20809
   215
  then have "finite (UNIV::nat set)"
huffman@27407
   216
    by (rule finite_imageD)
wenzelm@20809
   217
  then show False by simp
wenzelm@20809
   218
qed
wenzelm@20809
   219
paulson@22226
   220
lemma int_infinite [simp]:
paulson@22226
   221
  shows "infinite (UNIV::int set)"
paulson@22226
   222
proof -
paulson@22226
   223
  from inj_int have "infinite (range int)" by (rule range_inj_infinite)
paulson@22226
   224
  moreover 
paulson@22226
   225
  have "range int \<subseteq> (UNIV::int set)" by simp
paulson@22226
   226
  ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super)
paulson@22226
   227
qed
paulson@22226
   228
wenzelm@20809
   229
text {*
wenzelm@20809
   230
  The ``only if'' direction is harder because it requires the
wenzelm@20809
   231
  construction of a sequence of pairwise different elements of an
wenzelm@20809
   232
  infinite set @{text S}. The idea is to construct a sequence of
wenzelm@20809
   233
  non-empty and infinite subsets of @{text S} obtained by successively
wenzelm@20809
   234
  removing elements of @{text S}.
wenzelm@20809
   235
*}
wenzelm@20809
   236
wenzelm@20809
   237
lemma linorder_injI:
wenzelm@20809
   238
  assumes hyp: "!!x y. x < (y::'a::linorder) ==> f x \<noteq> f y"
wenzelm@20809
   239
  shows "inj f"
wenzelm@20809
   240
proof (rule inj_onI)
wenzelm@20809
   241
  fix x y
wenzelm@20809
   242
  assume f_eq: "f x = f y"
wenzelm@20809
   243
  show "x = y"
wenzelm@20809
   244
  proof (rule linorder_cases)
wenzelm@20809
   245
    assume "x < y"
wenzelm@20809
   246
    with hyp have "f x \<noteq> f y" by blast
wenzelm@20809
   247
    with f_eq show ?thesis by simp
wenzelm@20809
   248
  next
wenzelm@20809
   249
    assume "x = y"
wenzelm@20809
   250
    then show ?thesis .
wenzelm@20809
   251
  next
wenzelm@20809
   252
    assume "y < x"
wenzelm@20809
   253
    with hyp have "f y \<noteq> f x" by blast
wenzelm@20809
   254
    with f_eq show ?thesis by simp
wenzelm@20809
   255
  qed
wenzelm@20809
   256
qed
wenzelm@20809
   257
wenzelm@20809
   258
lemma infinite_countable_subset:
wenzelm@20809
   259
  assumes inf: "infinite (S::'a set)"
wenzelm@20809
   260
  shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
wenzelm@20809
   261
proof -
wenzelm@20809
   262
  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
wenzelm@20809
   263
  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
wenzelm@20809
   264
  have Sseq_inf: "\<And>n. infinite (Sseq n)"
wenzelm@20809
   265
  proof -
wenzelm@20809
   266
    fix n
wenzelm@20809
   267
    show "infinite (Sseq n)"
wenzelm@20809
   268
    proof (induct n)
wenzelm@20809
   269
      from inf show "infinite (Sseq 0)"
wenzelm@20809
   270
        by (simp add: Sseq_def)
wenzelm@20809
   271
    next
wenzelm@20809
   272
      fix n
wenzelm@20809
   273
      assume "infinite (Sseq n)" then show "infinite (Sseq (Suc n))"
wenzelm@20809
   274
        by (simp add: Sseq_def infinite_remove)
wenzelm@20809
   275
    qed
wenzelm@20809
   276
  qed
wenzelm@20809
   277
  have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
wenzelm@20809
   278
  proof -
wenzelm@20809
   279
    fix n
wenzelm@20809
   280
    show "Sseq n \<subseteq> S"
wenzelm@20809
   281
      by (induct n) (auto simp add: Sseq_def)
wenzelm@20809
   282
  qed
wenzelm@20809
   283
  have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
wenzelm@20809
   284
  proof -
wenzelm@20809
   285
    fix n
wenzelm@20809
   286
    show "pick n \<in> Sseq n"
wenzelm@20809
   287
    proof (unfold pick_def, rule someI_ex)
wenzelm@20809
   288
      from Sseq_inf have "infinite (Sseq n)" .
wenzelm@20809
   289
      then have "Sseq n \<noteq> {}" by auto
wenzelm@20809
   290
      then show "\<exists>x. x \<in> Sseq n" by auto
wenzelm@20809
   291
    qed
wenzelm@20809
   292
  qed
wenzelm@20809
   293
  with Sseq_S have rng: "range pick \<subseteq> S"
wenzelm@20809
   294
    by auto
wenzelm@20809
   295
  have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
wenzelm@20809
   296
  proof -
wenzelm@20809
   297
    fix n m
wenzelm@20809
   298
    show "pick n \<notin> Sseq (n + Suc m)"
wenzelm@20809
   299
      by (induct m) (auto simp add: Sseq_def pick_def)
wenzelm@20809
   300
  qed
wenzelm@20809
   301
  have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
wenzelm@20809
   302
  proof -
wenzelm@20809
   303
    fix n m
wenzelm@20809
   304
    from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
wenzelm@20809
   305
    moreover from pick_Sseq_gt
wenzelm@20809
   306
    have "pick n \<notin> Sseq (n + Suc m)" .
wenzelm@20809
   307
    ultimately show "pick n \<noteq> pick (n + Suc m)"
wenzelm@20809
   308
      by auto
wenzelm@20809
   309
  qed
wenzelm@20809
   310
  have inj: "inj pick"
wenzelm@20809
   311
  proof (rule linorder_injI)
wenzelm@20809
   312
    fix i j :: nat
wenzelm@20809
   313
    assume "i < j"
wenzelm@20809
   314
    show "pick i \<noteq> pick j"
wenzelm@20809
   315
    proof
wenzelm@20809
   316
      assume eq: "pick i = pick j"
wenzelm@20809
   317
      from `i < j` obtain k where "j = i + Suc k"
wenzelm@20809
   318
        by (auto simp add: less_iff_Suc_add)
wenzelm@20809
   319
      with pick_pick have "pick i \<noteq> pick j" by simp
wenzelm@20809
   320
      with eq show False by simp
wenzelm@20809
   321
    qed
wenzelm@20809
   322
  qed
wenzelm@20809
   323
  from rng inj show ?thesis by auto
wenzelm@20809
   324
qed
wenzelm@20809
   325
wenzelm@20809
   326
lemma infinite_iff_countable_subset:
wenzelm@20809
   327
    "infinite S = (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
wenzelm@20809
   328
  by (auto simp add: infinite_countable_subset range_inj_infinite infinite_super)
wenzelm@20809
   329
wenzelm@20809
   330
text {*
wenzelm@20809
   331
  For any function with infinite domain and finite range there is some
wenzelm@20809
   332
  element that is the image of infinitely many domain elements.  In
wenzelm@20809
   333
  particular, any infinite sequence of elements from a finite set
wenzelm@20809
   334
  contains some element that occurs infinitely often.
wenzelm@20809
   335
*}
wenzelm@20809
   336
wenzelm@20809
   337
lemma inf_img_fin_dom:
wenzelm@20809
   338
  assumes img: "finite (f`A)" and dom: "infinite A"
wenzelm@20809
   339
  shows "\<exists>y \<in> f`A. infinite (f -` {y})"
wenzelm@20809
   340
proof (rule ccontr)
wenzelm@20809
   341
  assume "\<not> ?thesis"
nipkow@40786
   342
  with img have "finite (UN y:f`A. f -` {y})" by blast
wenzelm@20809
   343
  moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
wenzelm@20809
   344
  moreover note dom
wenzelm@20809
   345
  ultimately show False by (simp add: infinite_super)
wenzelm@20809
   346
qed
wenzelm@20809
   347
wenzelm@20809
   348
lemma inf_img_fin_domE:
wenzelm@20809
   349
  assumes "finite (f`A)" and "infinite A"
wenzelm@20809
   350
  obtains y where "y \<in> f`A" and "infinite (f -` {y})"
wenzelm@23394
   351
  using assms by (blast dest: inf_img_fin_dom)
wenzelm@20809
   352
wenzelm@20809
   353
wenzelm@20809
   354
subsection "Infinitely Many and Almost All"
wenzelm@20809
   355
wenzelm@20809
   356
text {*
wenzelm@20809
   357
  We often need to reason about the existence of infinitely many
wenzelm@20809
   358
  (resp., all but finitely many) objects satisfying some predicate, so
wenzelm@20809
   359
  we introduce corresponding binders and their proof rules.
wenzelm@20809
   360
*}
wenzelm@20809
   361
wenzelm@20809
   362
definition
berghofe@22432
   363
  Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
wenzelm@20809
   364
  "Inf_many P = infinite {x. P x}"
wenzelm@21404
   365
wenzelm@21404
   366
definition
wenzelm@21404
   367
  Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
berghofe@22432
   368
  "Alm_all P = (\<not> (INFM x. \<not> P x))"
wenzelm@20809
   369
wenzelm@21210
   370
notation (xsymbols)
wenzelm@21404
   371
  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
wenzelm@20809
   372
  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
wenzelm@20809
   373
wenzelm@21210
   374
notation (HTML output)
wenzelm@21404
   375
  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
wenzelm@20809
   376
  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
wenzelm@20809
   377
huffman@34112
   378
lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}"
huffman@34112
   379
  unfolding Inf_many_def ..
huffman@34112
   380
huffman@34112
   381
lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}"
huffman@34112
   382
  unfolding Alm_all_def Inf_many_def by simp
huffman@34112
   383
huffman@34112
   384
(* legacy name *)
huffman@34112
   385
lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
huffman@34112
   386
huffman@34112
   387
lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
huffman@34112
   388
  unfolding Alm_all_def not_not ..
wenzelm@20809
   389
huffman@34112
   390
lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
huffman@34112
   391
  unfolding Alm_all_def not_not ..
huffman@34112
   392
huffman@34112
   393
lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
huffman@34112
   394
  unfolding Inf_many_def by simp
huffman@34112
   395
huffman@34112
   396
lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
huffman@34112
   397
  unfolding Alm_all_def by simp
huffman@34112
   398
huffman@34112
   399
lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
huffman@34112
   400
  by (erule contrapos_pp, simp)
wenzelm@20809
   401
wenzelm@20809
   402
lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
huffman@34112
   403
  by simp
huffman@34112
   404
huffman@34112
   405
lemma INFM_E: assumes "INFM x. P x" obtains x where "P x"
huffman@34112
   406
  using INFM_EX [OF assms] by (rule exE)
huffman@34112
   407
huffman@34112
   408
lemma MOST_I: assumes "\<And>x. P x" shows "MOST x. P x"
huffman@34112
   409
  using assms by simp
wenzelm@20809
   410
huffman@27407
   411
lemma INFM_mono:
wenzelm@20809
   412
  assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
wenzelm@20809
   413
  shows "\<exists>\<^sub>\<infinity>x. Q x"
wenzelm@20809
   414
proof -
wenzelm@20809
   415
  from inf have "infinite {x. P x}" unfolding Inf_many_def .
wenzelm@20809
   416
  moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
wenzelm@20809
   417
  ultimately show ?thesis
wenzelm@20809
   418
    by (simp add: Inf_many_def infinite_super)
wenzelm@20809
   419
qed
wenzelm@20809
   420
wenzelm@20809
   421
lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
huffman@27407
   422
  unfolding Alm_all_def by (blast intro: INFM_mono)
huffman@27407
   423
huffman@27407
   424
lemma INFM_disj_distrib:
huffman@27407
   425
  "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
huffman@27407
   426
  unfolding Inf_many_def by (simp add: Collect_disj_eq)
huffman@27407
   427
huffman@34112
   428
lemma INFM_imp_distrib:
huffman@34112
   429
  "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
huffman@34112
   430
  by (simp only: imp_conv_disj INFM_disj_distrib not_MOST)
huffman@34112
   431
huffman@27407
   432
lemma MOST_conj_distrib:
huffman@27407
   433
  "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
huffman@27407
   434
  unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
wenzelm@20809
   435
huffman@34112
   436
lemma MOST_conjI:
huffman@34112
   437
  "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
huffman@34112
   438
  by (simp add: MOST_conj_distrib)
huffman@34112
   439
huffman@34113
   440
lemma INFM_conjI:
huffman@34113
   441
  "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
huffman@34113
   442
  unfolding MOST_iff_cofinite INFM_iff_infinite
huffman@34113
   443
  apply (drule (1) Diff_infinite_finite)
huffman@34113
   444
  apply (simp add: Collect_conj_eq Collect_neg_eq)
huffman@34113
   445
  done
huffman@34113
   446
huffman@27407
   447
lemma MOST_rev_mp:
huffman@27407
   448
  assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
huffman@27407
   449
  shows "\<forall>\<^sub>\<infinity>x. Q x"
huffman@27407
   450
proof -
huffman@27407
   451
  have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
huffman@34112
   452
    using assms by (rule MOST_conjI)
huffman@27407
   453
  thus ?thesis by (rule MOST_mono) simp
huffman@27407
   454
qed
huffman@27407
   455
huffman@34112
   456
lemma MOST_imp_iff:
huffman@34112
   457
  assumes "MOST x. P x"
huffman@34112
   458
  shows "(MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
huffman@34112
   459
proof
huffman@34112
   460
  assume "MOST x. P x \<longrightarrow> Q x"
huffman@34112
   461
  with assms show "MOST x. Q x" by (rule MOST_rev_mp)
huffman@34112
   462
next
huffman@34112
   463
  assume "MOST x. Q x"
huffman@34112
   464
  then show "MOST x. P x \<longrightarrow> Q x" by (rule MOST_mono) simp
huffman@34112
   465
qed
huffman@27407
   466
huffman@34112
   467
lemma INFM_MOST_simps [simp]:
huffman@34112
   468
  "\<And>P Q. (INFM x. P x \<and> Q) \<longleftrightarrow> (INFM x. P x) \<and> Q"
huffman@34112
   469
  "\<And>P Q. (INFM x. P \<and> Q x) \<longleftrightarrow> P \<and> (INFM x. Q x)"
huffman@34112
   470
  "\<And>P Q. (MOST x. P x \<or> Q) \<longleftrightarrow> (MOST x. P x) \<or> Q"
huffman@34112
   471
  "\<And>P Q. (MOST x. P \<or> Q x) \<longleftrightarrow> P \<or> (MOST x. Q x)"
huffman@34112
   472
  "\<And>P Q. (MOST x. P x \<longrightarrow> Q) \<longleftrightarrow> ((INFM x. P x) \<longrightarrow> Q)"
huffman@34112
   473
  "\<And>P Q. (MOST x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (MOST x. Q x))"
huffman@34112
   474
  unfolding Alm_all_def Inf_many_def
huffman@34112
   475
  by (simp_all add: Collect_conj_eq)
huffman@34112
   476
huffman@34112
   477
text {* Properties of quantifiers with injective functions. *}
huffman@34112
   478
huffman@34112
   479
lemma INFM_inj:
huffman@34112
   480
  "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
huffman@34112
   481
  unfolding INFM_iff_infinite
huffman@34112
   482
  by (clarify, drule (1) finite_vimageI, simp)
huffman@27407
   483
huffman@34112
   484
lemma MOST_inj:
huffman@34112
   485
  "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
huffman@34112
   486
  unfolding MOST_iff_cofinite
huffman@34112
   487
  by (drule (1) finite_vimageI, simp)
huffman@34112
   488
huffman@34112
   489
text {* Properties of quantifiers with singletons. *}
huffman@34112
   490
huffman@34112
   491
lemma not_INFM_eq [simp]:
huffman@34112
   492
  "\<not> (INFM x. x = a)"
huffman@34112
   493
  "\<not> (INFM x. a = x)"
huffman@34112
   494
  unfolding INFM_iff_infinite by simp_all
huffman@34112
   495
huffman@34112
   496
lemma MOST_neq [simp]:
huffman@34112
   497
  "MOST x. x \<noteq> a"
huffman@34112
   498
  "MOST x. a \<noteq> x"
huffman@34112
   499
  unfolding MOST_iff_cofinite by simp_all
huffman@27407
   500
huffman@34112
   501
lemma INFM_neq [simp]:
huffman@34112
   502
  "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
huffman@34112
   503
  "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
huffman@34112
   504
  unfolding INFM_iff_infinite by simp_all
huffman@34112
   505
huffman@34112
   506
lemma MOST_eq [simp]:
huffman@34112
   507
  "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
huffman@34112
   508
  "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
huffman@34112
   509
  unfolding MOST_iff_cofinite by simp_all
huffman@34112
   510
huffman@34112
   511
lemma MOST_eq_imp:
huffman@34112
   512
  "MOST x. x = a \<longrightarrow> P x"
huffman@34112
   513
  "MOST x. a = x \<longrightarrow> P x"
huffman@34112
   514
  unfolding MOST_iff_cofinite by simp_all
huffman@34112
   515
huffman@34112
   516
text {* Properties of quantifiers over the naturals. *}
huffman@27407
   517
huffman@27407
   518
lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
wenzelm@20809
   519
  by (simp add: Inf_many_def infinite_nat_iff_unbounded)
wenzelm@20809
   520
huffman@27407
   521
lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
wenzelm@20809
   522
  by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
wenzelm@20809
   523
wenzelm@20809
   524
lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
huffman@27407
   525
  by (simp add: Alm_all_def INFM_nat)
wenzelm@20809
   526
wenzelm@20809
   527
lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
huffman@27407
   528
  by (simp add: Alm_all_def INFM_nat_le)
wenzelm@20809
   529
wenzelm@20809
   530
wenzelm@20809
   531
subsection "Enumeration of an Infinite Set"
wenzelm@20809
   532
wenzelm@20809
   533
text {*
wenzelm@20809
   534
  The set's element type must be wellordered (e.g. the natural numbers).
wenzelm@20809
   535
*}
wenzelm@20809
   536
haftmann@34941
   537
primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
haftmann@34941
   538
    enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
haftmann@34941
   539
  | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
wenzelm@20809
   540
wenzelm@20809
   541
lemma enumerate_Suc':
wenzelm@20809
   542
    "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
wenzelm@20809
   543
  by simp
wenzelm@20809
   544
wenzelm@20809
   545
lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
nipkow@29901
   546
apply (induct n arbitrary: S)
nipkow@44890
   547
 apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
nipkow@29901
   548
apply simp
huffman@44454
   549
apply (metis DiffE infinite_remove)
nipkow@29901
   550
done
wenzelm@20809
   551
wenzelm@20809
   552
declare enumerate_0 [simp del] enumerate_Suc [simp del]
wenzelm@20809
   553
wenzelm@20809
   554
lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
wenzelm@20809
   555
  apply (induct n arbitrary: S)
wenzelm@20809
   556
   apply (rule order_le_neq_trans)
wenzelm@20809
   557
    apply (simp add: enumerate_0 Least_le enumerate_in_set)
wenzelm@20809
   558
   apply (simp only: enumerate_Suc')
wenzelm@20809
   559
   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
wenzelm@20809
   560
    apply (blast intro: sym)
wenzelm@20809
   561
   apply (simp add: enumerate_in_set del: Diff_iff)
wenzelm@20809
   562
  apply (simp add: enumerate_Suc')
wenzelm@20809
   563
  done
wenzelm@20809
   564
wenzelm@20809
   565
lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
wenzelm@20809
   566
  apply (erule less_Suc_induct)
wenzelm@20809
   567
  apply (auto intro: enumerate_step)
wenzelm@20809
   568
  done
wenzelm@20809
   569
wenzelm@20809
   570
hoelzl@50134
   571
lemma le_enumerate:
hoelzl@50134
   572
  assumes S: "infinite S"
hoelzl@50134
   573
  shows "n \<le> enumerate S n"
hoelzl@50134
   574
  using S 
hoelzl@50134
   575
proof (induct n)
hoelzl@50134
   576
  case (Suc n)
hoelzl@50134
   577
  then have "n \<le> enumerate S n" by simp
hoelzl@50134
   578
  also note enumerate_mono[of n "Suc n", OF _ `infinite S`]
hoelzl@50134
   579
  finally show ?case by simp
hoelzl@50134
   580
qed simp
hoelzl@50134
   581
hoelzl@50134
   582
lemma enumerate_Suc'':
hoelzl@50134
   583
  fixes S :: "'a::wellorder set"
hoelzl@50134
   584
  shows "infinite S  \<Longrightarrow> enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
hoelzl@50134
   585
proof (induct n arbitrary: S)
hoelzl@50134
   586
  case 0
hoelzl@50134
   587
  then have "\<forall>s\<in>S. enumerate S 0 \<le> s"
hoelzl@50134
   588
    by (auto simp: enumerate.simps intro: Least_le)
hoelzl@50134
   589
  then show ?case
hoelzl@50134
   590
    unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"]
hoelzl@50134
   591
    by (intro arg_cong[where f=Least] ext) auto
hoelzl@50134
   592
next
hoelzl@50134
   593
  case (Suc n S)
hoelzl@50134
   594
  show ?case
hoelzl@50134
   595
    using enumerate_mono[OF zero_less_Suc `infinite S`, of n] `infinite S`
hoelzl@50134
   596
    apply (subst (1 2) enumerate_Suc')
hoelzl@50134
   597
    apply (subst Suc)
hoelzl@50134
   598
    apply (insert `infinite S`, simp)
hoelzl@50134
   599
    by (intro arg_cong[where f=Least] ext)
hoelzl@50134
   600
       (auto simp: enumerate_Suc'[symmetric])
hoelzl@50134
   601
qed
hoelzl@50134
   602
hoelzl@50134
   603
lemma enumerate_Ex:
hoelzl@50134
   604
  assumes S: "infinite (S::nat set)"
hoelzl@50134
   605
  shows "s \<in> S \<Longrightarrow> \<exists>n. enumerate S n = s"
hoelzl@50134
   606
proof (induct s rule: less_induct)
hoelzl@50134
   607
  case (less s)
hoelzl@50134
   608
  show ?case
hoelzl@50134
   609
  proof cases
hoelzl@50134
   610
    let ?y = "Max {s'\<in>S. s' < s}"
hoelzl@50134
   611
    assume "\<exists>y\<in>S. y < s"
hoelzl@50134
   612
    then have y: "\<And>x. ?y < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)" by (subst Max_less_iff) auto
hoelzl@50134
   613
    then have y_in: "?y \<in> {s'\<in>S. s' < s}" by (intro Max_in) auto
hoelzl@50134
   614
    with less.hyps[of ?y] obtain n where "enumerate S n = ?y" by auto
hoelzl@50134
   615
    with S have "enumerate S (Suc n) = s"
hoelzl@50134
   616
      by (auto simp: y less enumerate_Suc'' intro!: Least_equality)
hoelzl@50134
   617
    then show ?case by auto
hoelzl@50134
   618
  next
hoelzl@50134
   619
    assume *: "\<not> (\<exists>y\<in>S. y < s)"
hoelzl@50134
   620
    then have "\<forall>t\<in>S. s \<le> t" by auto
hoelzl@50134
   621
    with `s \<in> S` show ?thesis
hoelzl@50134
   622
      by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0)
hoelzl@50134
   623
  qed
hoelzl@50134
   624
qed
hoelzl@50134
   625
hoelzl@50134
   626
lemma bij_enumerate:
hoelzl@50134
   627
  fixes S :: "nat set"
hoelzl@50134
   628
  assumes S: "infinite S"
hoelzl@50134
   629
  shows "bij_betw (enumerate S) UNIV S"
hoelzl@50134
   630
proof -
hoelzl@50134
   631
  have "\<And>n m. n \<noteq> m \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
hoelzl@50134
   632
    using enumerate_mono[OF _ `infinite S`] by (auto simp: neq_iff)
hoelzl@50134
   633
  then have "inj (enumerate S)"
hoelzl@50134
   634
    by (auto simp: inj_on_def)
hoelzl@50134
   635
  moreover have "\<forall>s\<in>S. \<exists>i. enumerate S i = s"
hoelzl@50134
   636
    using enumerate_Ex[OF S] by auto
hoelzl@50134
   637
  moreover note `infinite S`
hoelzl@50134
   638
  ultimately show ?thesis
hoelzl@50134
   639
    unfolding bij_betw_def by (auto intro: enumerate_in_set)
hoelzl@50134
   640
qed
hoelzl@50134
   641
wenzelm@20809
   642
subsection "Miscellaneous"
wenzelm@20809
   643
wenzelm@20809
   644
text {*
wenzelm@20809
   645
  A few trivial lemmas about sets that contain at most one element.
wenzelm@20809
   646
  These simplify the reasoning about deterministic automata.
wenzelm@20809
   647
*}
wenzelm@20809
   648
wenzelm@20809
   649
definition
wenzelm@21404
   650
  atmost_one :: "'a set \<Rightarrow> bool" where
wenzelm@20809
   651
  "atmost_one S = (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y)"
wenzelm@20809
   652
wenzelm@20809
   653
lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
wenzelm@20809
   654
  by (simp add: atmost_one_def)
wenzelm@20809
   655
wenzelm@20809
   656
lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
wenzelm@20809
   657
  by (simp add: atmost_one_def)
wenzelm@20809
   658
wenzelm@20809
   659
lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
wenzelm@20809
   660
  by (simp add: atmost_one_def)
wenzelm@20809
   661
wenzelm@20809
   662
end
haftmann@46783
   663