src/HOL/Library/Infinite_Set.thy
author blanchet
Wed Sep 24 15:45:55 2014 +0200 (2014-09-24)
changeset 58425 246985c6b20b
parent 54612 7e291ae244ea
child 58881 b9556a055632
permissions -rw-r--r--
simpler proof
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
traytel@54612
     8
imports Main
wenzelm@20809
     9
begin
wenzelm@20809
    10
wenzelm@20809
    11
subsection "Infinite Sets"
wenzelm@20809
    12
wenzelm@20809
    13
text {*
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@20809
    17
*}
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@20809
    22
text {*
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@20809
    25
*}
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@20809
    65
text {*
wenzelm@20809
    66
  As a concrete example, we prove that the set of natural numbers is
wenzelm@20809
    67
  infinite.
wenzelm@20809
    68
*}
wenzelm@20809
    69
wenzelm@20809
    70
lemma finite_nat_bounded:
wenzelm@20809
    71
  assumes S: "finite (S::nat set)"
wenzelm@20809
    72
  shows "\<exists>k. S \<subseteq> {..<k}"  (is "\<exists>k. ?bounded S k")
wenzelm@53239
    73
  using S
wenzelm@20809
    74
proof induct
wenzelm@20809
    75
  have "?bounded {} 0" by simp
wenzelm@20809
    76
  then show "\<exists>k. ?bounded {} k" ..
wenzelm@20809
    77
next
wenzelm@20809
    78
  fix S x
wenzelm@20809
    79
  assume "\<exists>k. ?bounded S k"
wenzelm@20809
    80
  then obtain k where k: "?bounded S k" ..
wenzelm@20809
    81
  show "\<exists>k. ?bounded (insert x S) k"
wenzelm@20809
    82
  proof (cases "x < k")
wenzelm@20809
    83
    case True
wenzelm@20809
    84
    with k show ?thesis by auto
wenzelm@20809
    85
  next
wenzelm@20809
    86
    case False
wenzelm@20809
    87
    with k have "?bounded S (Suc x)" by auto
wenzelm@20809
    88
    then show ?thesis by auto
wenzelm@20809
    89
  qed
wenzelm@20809
    90
qed
wenzelm@20809
    91
wenzelm@20809
    92
lemma finite_nat_iff_bounded:
wenzelm@53239
    93
  "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@20809
    94
proof
wenzelm@20809
    95
  assume ?lhs
wenzelm@20809
    96
  then show ?rhs by (rule finite_nat_bounded)
wenzelm@20809
    97
next
wenzelm@20809
    98
  assume ?rhs
wenzelm@20809
    99
  then obtain k where "S \<subseteq> {..<k}" ..
wenzelm@20809
   100
  then show "finite S"
wenzelm@20809
   101
    by (rule finite_subset) simp
wenzelm@20809
   102
qed
wenzelm@20809
   103
wenzelm@20809
   104
lemma finite_nat_iff_bounded_le:
wenzelm@53239
   105
  "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..k})"  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@20809
   106
proof
wenzelm@20809
   107
  assume ?lhs
wenzelm@20809
   108
  then obtain k where "S \<subseteq> {..<k}"
wenzelm@20809
   109
    by (blast dest: finite_nat_bounded)
wenzelm@20809
   110
  then have "S \<subseteq> {..k}" by auto
wenzelm@20809
   111
  then show ?rhs ..
wenzelm@20809
   112
next
wenzelm@20809
   113
  assume ?rhs
wenzelm@20809
   114
  then obtain k where "S \<subseteq> {..k}" ..
wenzelm@20809
   115
  then show "finite S"
wenzelm@20809
   116
    by (rule finite_subset) simp
wenzelm@20809
   117
qed
wenzelm@20809
   118
wenzelm@20809
   119
lemma infinite_nat_iff_unbounded:
wenzelm@53239
   120
  "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> n \<in> S)"
wenzelm@53239
   121
  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@20809
   122
proof
wenzelm@20809
   123
  assume ?lhs
wenzelm@20809
   124
  show ?rhs
wenzelm@20809
   125
  proof (rule ccontr)
wenzelm@20809
   126
    assume "\<not> ?rhs"
wenzelm@53239
   127
    then obtain m where m: "\<forall>n. m < n \<longrightarrow> n \<notin> S" by blast
wenzelm@20809
   128
    then have "S \<subseteq> {..m}"
wenzelm@20809
   129
      by (auto simp add: sym [OF linorder_not_less])
wenzelm@20809
   130
    with `?lhs` show False
wenzelm@20809
   131
      by (simp add: finite_nat_iff_bounded_le)
wenzelm@20809
   132
  qed
wenzelm@20809
   133
next
wenzelm@20809
   134
  assume ?rhs
wenzelm@20809
   135
  show ?lhs
wenzelm@20809
   136
  proof
wenzelm@20809
   137
    assume "finite S"
wenzelm@20809
   138
    then obtain m where "S \<subseteq> {..m}"
wenzelm@20809
   139
      by (auto simp add: finite_nat_iff_bounded_le)
wenzelm@53239
   140
    then have "\<forall>n. m < n \<longrightarrow> n \<notin> S" by auto
wenzelm@20809
   141
    with `?rhs` show False by blast
wenzelm@20809
   142
  qed
wenzelm@20809
   143
qed
wenzelm@20809
   144
wenzelm@20809
   145
lemma infinite_nat_iff_unbounded_le:
wenzelm@53239
   146
  "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> n \<in> S)"
wenzelm@53239
   147
  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@20809
   148
proof
wenzelm@20809
   149
  assume ?lhs
wenzelm@20809
   150
  show ?rhs
wenzelm@20809
   151
  proof
wenzelm@20809
   152
    fix m
wenzelm@53239
   153
    from `?lhs` obtain n where "m < n \<and> n \<in> S"
wenzelm@20809
   154
      by (auto simp add: infinite_nat_iff_unbounded)
wenzelm@53239
   155
    then have "m \<le> n \<and> n \<in> S" by simp
wenzelm@20809
   156
    then show "\<exists>n. m \<le> n \<and> n \<in> S" ..
wenzelm@20809
   157
  qed
wenzelm@20809
   158
next
wenzelm@20809
   159
  assume ?rhs
wenzelm@20809
   160
  show ?lhs
wenzelm@20809
   161
  proof (auto simp add: infinite_nat_iff_unbounded)
wenzelm@20809
   162
    fix m
wenzelm@53239
   163
    from `?rhs` obtain n where "Suc m \<le> n \<and> n \<in> S"
wenzelm@20809
   164
      by blast
wenzelm@53239
   165
    then have "m < n \<and> n \<in> S" by simp
wenzelm@20809
   166
    then show "\<exists>n. m < n \<and> n \<in> S" ..
wenzelm@20809
   167
  qed
wenzelm@20809
   168
qed
wenzelm@20809
   169
wenzelm@20809
   170
text {*
wenzelm@20809
   171
  For a set of natural numbers to be infinite, it is enough to know
wenzelm@20809
   172
  that for any number larger than some @{text k}, there is some larger
wenzelm@20809
   173
  number that is an element of the set.
wenzelm@20809
   174
*}
wenzelm@20809
   175
wenzelm@20809
   176
lemma unbounded_k_infinite:
wenzelm@53239
   177
  assumes k: "\<forall>m. k < m \<longrightarrow> (\<exists>n. m < n \<and> n \<in> S)"
wenzelm@20809
   178
  shows "infinite (S::nat set)"
wenzelm@20809
   179
proof -
wenzelm@20809
   180
  {
wenzelm@53239
   181
    fix m have "\<exists>n. m < n \<and> n \<in> S"
wenzelm@53239
   182
    proof (cases "k < m")
wenzelm@20809
   183
      case True
wenzelm@20809
   184
      with k show ?thesis by blast
wenzelm@20809
   185
    next
wenzelm@20809
   186
      case False
wenzelm@53239
   187
      from k obtain n where "Suc k < n \<and> n \<in> S" by auto
wenzelm@53239
   188
      with False have "m < n \<and> n \<in> S" by auto
wenzelm@20809
   189
      then show ?thesis ..
wenzelm@20809
   190
    qed
wenzelm@20809
   191
  }
wenzelm@20809
   192
  then show ?thesis
wenzelm@20809
   193
    by (auto simp add: infinite_nat_iff_unbounded)
wenzelm@20809
   194
qed
wenzelm@20809
   195
huffman@35056
   196
lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
wenzelm@20809
   197
  by simp
wenzelm@20809
   198
wenzelm@20809
   199
lemma range_inj_infinite:
wenzelm@20809
   200
  "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
wenzelm@20809
   201
proof
huffman@27407
   202
  assume "finite (range f)" and "inj f"
wenzelm@20809
   203
  then have "finite (UNIV::nat set)"
huffman@27407
   204
    by (rule finite_imageD)
wenzelm@20809
   205
  then show False by simp
wenzelm@20809
   206
qed
wenzelm@20809
   207
wenzelm@20809
   208
text {*
wenzelm@20809
   209
  For any function with infinite domain and finite range there is some
wenzelm@20809
   210
  element that is the image of infinitely many domain elements.  In
wenzelm@20809
   211
  particular, any infinite sequence of elements from a finite set
wenzelm@20809
   212
  contains some element that occurs infinitely often.
wenzelm@20809
   213
*}
wenzelm@20809
   214
wenzelm@20809
   215
lemma inf_img_fin_dom:
wenzelm@20809
   216
  assumes img: "finite (f`A)" and dom: "infinite A"
wenzelm@20809
   217
  shows "\<exists>y \<in> f`A. infinite (f -` {y})"
wenzelm@20809
   218
proof (rule ccontr)
wenzelm@20809
   219
  assume "\<not> ?thesis"
nipkow@40786
   220
  with img have "finite (UN y:f`A. f -` {y})" by blast
wenzelm@20809
   221
  moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
wenzelm@20809
   222
  moreover note dom
wenzelm@20809
   223
  ultimately show False by (simp add: infinite_super)
wenzelm@20809
   224
qed
wenzelm@20809
   225
wenzelm@20809
   226
lemma inf_img_fin_domE:
wenzelm@20809
   227
  assumes "finite (f`A)" and "infinite A"
wenzelm@20809
   228
  obtains y where "y \<in> f`A" and "infinite (f -` {y})"
wenzelm@23394
   229
  using assms by (blast dest: inf_img_fin_dom)
wenzelm@20809
   230
wenzelm@20809
   231
wenzelm@20809
   232
subsection "Infinitely Many and Almost All"
wenzelm@20809
   233
wenzelm@20809
   234
text {*
wenzelm@20809
   235
  We often need to reason about the existence of infinitely many
wenzelm@20809
   236
  (resp., all but finitely many) objects satisfying some predicate, so
wenzelm@20809
   237
  we introduce corresponding binders and their proof rules.
wenzelm@20809
   238
*}
wenzelm@20809
   239
wenzelm@53239
   240
definition Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10)
wenzelm@53239
   241
  where "Inf_many P \<longleftrightarrow> infinite {x. P x}"
wenzelm@21404
   242
wenzelm@53239
   243
definition Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10)
wenzelm@53239
   244
  where "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)"
wenzelm@20809
   245
wenzelm@21210
   246
notation (xsymbols)
wenzelm@21404
   247
  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
wenzelm@20809
   248
  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
wenzelm@20809
   249
wenzelm@21210
   250
notation (HTML output)
wenzelm@21404
   251
  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
wenzelm@20809
   252
  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
wenzelm@20809
   253
huffman@34112
   254
lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}"
huffman@34112
   255
  unfolding Inf_many_def ..
huffman@34112
   256
huffman@34112
   257
lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}"
huffman@34112
   258
  unfolding Alm_all_def Inf_many_def by simp
huffman@34112
   259
huffman@34112
   260
(* legacy name *)
huffman@34112
   261
lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
huffman@34112
   262
huffman@34112
   263
lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
huffman@34112
   264
  unfolding Alm_all_def not_not ..
wenzelm@20809
   265
huffman@34112
   266
lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
huffman@34112
   267
  unfolding Alm_all_def not_not ..
huffman@34112
   268
huffman@34112
   269
lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
huffman@34112
   270
  unfolding Inf_many_def by simp
huffman@34112
   271
huffman@34112
   272
lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
huffman@34112
   273
  unfolding Alm_all_def by simp
huffman@34112
   274
huffman@34112
   275
lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
wenzelm@53239
   276
  apply (erule contrapos_pp)
wenzelm@53239
   277
  apply simp
wenzelm@53239
   278
  done
wenzelm@20809
   279
wenzelm@20809
   280
lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
huffman@34112
   281
  by simp
huffman@34112
   282
wenzelm@53239
   283
lemma INFM_E:
wenzelm@53239
   284
  assumes "INFM x. P x"
wenzelm@53239
   285
  obtains x where "P x"
huffman@34112
   286
  using INFM_EX [OF assms] by (rule exE)
huffman@34112
   287
wenzelm@53239
   288
lemma MOST_I:
wenzelm@53239
   289
  assumes "\<And>x. P x"
wenzelm@53239
   290
  shows "MOST x. P x"
huffman@34112
   291
  using assms by simp
wenzelm@20809
   292
huffman@27407
   293
lemma INFM_mono:
wenzelm@20809
   294
  assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
wenzelm@20809
   295
  shows "\<exists>\<^sub>\<infinity>x. Q x"
wenzelm@20809
   296
proof -
wenzelm@20809
   297
  from inf have "infinite {x. P x}" unfolding Inf_many_def .
wenzelm@20809
   298
  moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
wenzelm@20809
   299
  ultimately show ?thesis
wenzelm@20809
   300
    by (simp add: Inf_many_def infinite_super)
wenzelm@20809
   301
qed
wenzelm@20809
   302
wenzelm@20809
   303
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
   304
  unfolding Alm_all_def by (blast intro: INFM_mono)
huffman@27407
   305
huffman@27407
   306
lemma INFM_disj_distrib:
huffman@27407
   307
  "(\<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
   308
  unfolding Inf_many_def by (simp add: Collect_disj_eq)
huffman@27407
   309
huffman@34112
   310
lemma INFM_imp_distrib:
huffman@34112
   311
  "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
huffman@34112
   312
  by (simp only: imp_conv_disj INFM_disj_distrib not_MOST)
huffman@34112
   313
huffman@27407
   314
lemma MOST_conj_distrib:
huffman@27407
   315
  "(\<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
   316
  unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
wenzelm@20809
   317
huffman@34112
   318
lemma MOST_conjI:
huffman@34112
   319
  "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
huffman@34112
   320
  by (simp add: MOST_conj_distrib)
huffman@34112
   321
huffman@34113
   322
lemma INFM_conjI:
huffman@34113
   323
  "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
huffman@34113
   324
  unfolding MOST_iff_cofinite INFM_iff_infinite
huffman@34113
   325
  apply (drule (1) Diff_infinite_finite)
huffman@34113
   326
  apply (simp add: Collect_conj_eq Collect_neg_eq)
huffman@34113
   327
  done
huffman@34113
   328
huffman@27407
   329
lemma MOST_rev_mp:
huffman@27407
   330
  assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
huffman@27407
   331
  shows "\<forall>\<^sub>\<infinity>x. Q x"
huffman@27407
   332
proof -
huffman@27407
   333
  have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
huffman@34112
   334
    using assms by (rule MOST_conjI)
huffman@27407
   335
  thus ?thesis by (rule MOST_mono) simp
huffman@27407
   336
qed
huffman@27407
   337
huffman@34112
   338
lemma MOST_imp_iff:
huffman@34112
   339
  assumes "MOST x. P x"
huffman@34112
   340
  shows "(MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
huffman@34112
   341
proof
huffman@34112
   342
  assume "MOST x. P x \<longrightarrow> Q x"
huffman@34112
   343
  with assms show "MOST x. Q x" by (rule MOST_rev_mp)
huffman@34112
   344
next
huffman@34112
   345
  assume "MOST x. Q x"
huffman@34112
   346
  then show "MOST x. P x \<longrightarrow> Q x" by (rule MOST_mono) simp
huffman@34112
   347
qed
huffman@27407
   348
huffman@34112
   349
lemma INFM_MOST_simps [simp]:
huffman@34112
   350
  "\<And>P Q. (INFM x. P x \<and> Q) \<longleftrightarrow> (INFM x. P x) \<and> Q"
huffman@34112
   351
  "\<And>P Q. (INFM x. P \<and> Q x) \<longleftrightarrow> P \<and> (INFM x. Q x)"
huffman@34112
   352
  "\<And>P Q. (MOST x. P x \<or> Q) \<longleftrightarrow> (MOST x. P x) \<or> Q"
huffman@34112
   353
  "\<And>P Q. (MOST x. P \<or> Q x) \<longleftrightarrow> P \<or> (MOST x. Q x)"
huffman@34112
   354
  "\<And>P Q. (MOST x. P x \<longrightarrow> Q) \<longleftrightarrow> ((INFM x. P x) \<longrightarrow> Q)"
huffman@34112
   355
  "\<And>P Q. (MOST x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (MOST x. Q x))"
huffman@34112
   356
  unfolding Alm_all_def Inf_many_def
huffman@34112
   357
  by (simp_all add: Collect_conj_eq)
huffman@34112
   358
huffman@34112
   359
text {* Properties of quantifiers with injective functions. *}
huffman@34112
   360
wenzelm@53239
   361
lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
huffman@34112
   362
  unfolding INFM_iff_infinite
wenzelm@53239
   363
  apply clarify
wenzelm@53239
   364
  apply (drule (1) finite_vimageI)
wenzelm@53239
   365
  apply simp
wenzelm@53239
   366
  done
huffman@27407
   367
wenzelm@53239
   368
lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
huffman@34112
   369
  unfolding MOST_iff_cofinite
wenzelm@53239
   370
  apply (drule (1) finite_vimageI)
wenzelm@53239
   371
  apply simp
wenzelm@53239
   372
  done
huffman@34112
   373
huffman@34112
   374
text {* Properties of quantifiers with singletons. *}
huffman@34112
   375
huffman@34112
   376
lemma not_INFM_eq [simp]:
huffman@34112
   377
  "\<not> (INFM x. x = a)"
huffman@34112
   378
  "\<not> (INFM x. a = x)"
huffman@34112
   379
  unfolding INFM_iff_infinite by simp_all
huffman@34112
   380
huffman@34112
   381
lemma MOST_neq [simp]:
huffman@34112
   382
  "MOST x. x \<noteq> a"
huffman@34112
   383
  "MOST x. a \<noteq> x"
huffman@34112
   384
  unfolding MOST_iff_cofinite by simp_all
huffman@27407
   385
huffman@34112
   386
lemma INFM_neq [simp]:
huffman@34112
   387
  "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
huffman@34112
   388
  "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
huffman@34112
   389
  unfolding INFM_iff_infinite by simp_all
huffman@34112
   390
huffman@34112
   391
lemma MOST_eq [simp]:
huffman@34112
   392
  "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
huffman@34112
   393
  "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
huffman@34112
   394
  unfolding MOST_iff_cofinite by simp_all
huffman@34112
   395
huffman@34112
   396
lemma MOST_eq_imp:
huffman@34112
   397
  "MOST x. x = a \<longrightarrow> P x"
huffman@34112
   398
  "MOST x. a = x \<longrightarrow> P x"
huffman@34112
   399
  unfolding MOST_iff_cofinite by simp_all
huffman@34112
   400
huffman@34112
   401
text {* Properties of quantifiers over the naturals. *}
huffman@27407
   402
wenzelm@53239
   403
lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> P n)"
wenzelm@20809
   404
  by (simp add: Inf_many_def infinite_nat_iff_unbounded)
wenzelm@20809
   405
wenzelm@53239
   406
lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> P n)"
wenzelm@20809
   407
  by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
wenzelm@20809
   408
wenzelm@53239
   409
lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n. m < n \<longrightarrow> P n)"
huffman@27407
   410
  by (simp add: Alm_all_def INFM_nat)
wenzelm@20809
   411
wenzelm@53239
   412
lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n. m \<le> n \<longrightarrow> P n)"
huffman@27407
   413
  by (simp add: Alm_all_def INFM_nat_le)
wenzelm@20809
   414
wenzelm@20809
   415
wenzelm@20809
   416
subsection "Enumeration of an Infinite Set"
wenzelm@20809
   417
wenzelm@20809
   418
text {*
wenzelm@20809
   419
  The set's element type must be wellordered (e.g. the natural numbers).
wenzelm@20809
   420
*}
wenzelm@20809
   421
wenzelm@53239
   422
primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
wenzelm@53239
   423
where
wenzelm@53239
   424
  enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
wenzelm@53239
   425
| enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
wenzelm@20809
   426
wenzelm@53239
   427
lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
wenzelm@20809
   428
  by simp
wenzelm@20809
   429
wenzelm@20809
   430
lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
wenzelm@53239
   431
  apply (induct n arbitrary: S)
wenzelm@53239
   432
   apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
wenzelm@53239
   433
  apply simp
wenzelm@53239
   434
  apply (metis DiffE infinite_remove)
wenzelm@53239
   435
  done
wenzelm@20809
   436
wenzelm@20809
   437
declare enumerate_0 [simp del] enumerate_Suc [simp del]
wenzelm@20809
   438
wenzelm@20809
   439
lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
wenzelm@20809
   440
  apply (induct n arbitrary: S)
wenzelm@20809
   441
   apply (rule order_le_neq_trans)
wenzelm@20809
   442
    apply (simp add: enumerate_0 Least_le enumerate_in_set)
wenzelm@20809
   443
   apply (simp only: enumerate_Suc')
wenzelm@20809
   444
   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
wenzelm@20809
   445
    apply (blast intro: sym)
wenzelm@20809
   446
   apply (simp add: enumerate_in_set del: Diff_iff)
wenzelm@20809
   447
  apply (simp add: enumerate_Suc')
wenzelm@20809
   448
  done
wenzelm@20809
   449
wenzelm@20809
   450
lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
wenzelm@20809
   451
  apply (erule less_Suc_induct)
wenzelm@20809
   452
  apply (auto intro: enumerate_step)
wenzelm@20809
   453
  done
wenzelm@20809
   454
wenzelm@20809
   455
hoelzl@50134
   456
lemma le_enumerate:
hoelzl@50134
   457
  assumes S: "infinite S"
hoelzl@50134
   458
  shows "n \<le> enumerate S n"
hoelzl@50134
   459
  using S 
hoelzl@50134
   460
proof (induct n)
wenzelm@53239
   461
  case 0
wenzelm@53239
   462
  then show ?case by simp
wenzelm@53239
   463
next
hoelzl@50134
   464
  case (Suc n)
hoelzl@50134
   465
  then have "n \<le> enumerate S n" by simp
hoelzl@50134
   466
  also note enumerate_mono[of n "Suc n", OF _ `infinite S`]
hoelzl@50134
   467
  finally show ?case by simp
wenzelm@53239
   468
qed
hoelzl@50134
   469
hoelzl@50134
   470
lemma enumerate_Suc'':
hoelzl@50134
   471
  fixes S :: "'a::wellorder set"
wenzelm@53239
   472
  assumes "infinite S"
wenzelm@53239
   473
  shows "enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
wenzelm@53239
   474
  using assms
hoelzl@50134
   475
proof (induct n arbitrary: S)
hoelzl@50134
   476
  case 0
wenzelm@53239
   477
  then have "\<forall>s \<in> S. enumerate S 0 \<le> s"
hoelzl@50134
   478
    by (auto simp: enumerate.simps intro: Least_le)
hoelzl@50134
   479
  then show ?case
hoelzl@50134
   480
    unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"]
wenzelm@53239
   481
    by (intro arg_cong[where f = Least] ext) auto
hoelzl@50134
   482
next
hoelzl@50134
   483
  case (Suc n S)
hoelzl@50134
   484
  show ?case
hoelzl@50134
   485
    using enumerate_mono[OF zero_less_Suc `infinite S`, of n] `infinite S`
hoelzl@50134
   486
    apply (subst (1 2) enumerate_Suc')
hoelzl@50134
   487
    apply (subst Suc)
wenzelm@53239
   488
    using `infinite S`
wenzelm@53239
   489
    apply simp
wenzelm@53239
   490
    apply (intro arg_cong[where f = Least] ext)
wenzelm@53239
   491
    apply (auto simp: enumerate_Suc'[symmetric])
wenzelm@53239
   492
    done
hoelzl@50134
   493
qed
hoelzl@50134
   494
hoelzl@50134
   495
lemma enumerate_Ex:
hoelzl@50134
   496
  assumes S: "infinite (S::nat set)"
hoelzl@50134
   497
  shows "s \<in> S \<Longrightarrow> \<exists>n. enumerate S n = s"
hoelzl@50134
   498
proof (induct s rule: less_induct)
hoelzl@50134
   499
  case (less s)
hoelzl@50134
   500
  show ?case
hoelzl@50134
   501
  proof cases
hoelzl@50134
   502
    let ?y = "Max {s'\<in>S. s' < s}"
hoelzl@50134
   503
    assume "\<exists>y\<in>S. y < s"
wenzelm@53239
   504
    then have y: "\<And>x. ?y < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)"
wenzelm@53239
   505
      by (subst Max_less_iff) auto
wenzelm@53239
   506
    then have y_in: "?y \<in> {s'\<in>S. s' < s}"
wenzelm@53239
   507
      by (intro Max_in) auto
wenzelm@53239
   508
    with less.hyps[of ?y] obtain n where "enumerate S n = ?y"
wenzelm@53239
   509
      by auto
hoelzl@50134
   510
    with S have "enumerate S (Suc n) = s"
hoelzl@50134
   511
      by (auto simp: y less enumerate_Suc'' intro!: Least_equality)
hoelzl@50134
   512
    then show ?case by auto
hoelzl@50134
   513
  next
hoelzl@50134
   514
    assume *: "\<not> (\<exists>y\<in>S. y < s)"
hoelzl@50134
   515
    then have "\<forall>t\<in>S. s \<le> t" by auto
hoelzl@50134
   516
    with `s \<in> S` show ?thesis
hoelzl@50134
   517
      by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0)
hoelzl@50134
   518
  qed
hoelzl@50134
   519
qed
hoelzl@50134
   520
hoelzl@50134
   521
lemma bij_enumerate:
hoelzl@50134
   522
  fixes S :: "nat set"
hoelzl@50134
   523
  assumes S: "infinite S"
hoelzl@50134
   524
  shows "bij_betw (enumerate S) UNIV S"
hoelzl@50134
   525
proof -
hoelzl@50134
   526
  have "\<And>n m. n \<noteq> m \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
hoelzl@50134
   527
    using enumerate_mono[OF _ `infinite S`] by (auto simp: neq_iff)
hoelzl@50134
   528
  then have "inj (enumerate S)"
hoelzl@50134
   529
    by (auto simp: inj_on_def)
wenzelm@53239
   530
  moreover have "\<forall>s \<in> S. \<exists>i. enumerate S i = s"
hoelzl@50134
   531
    using enumerate_Ex[OF S] by auto
hoelzl@50134
   532
  moreover note `infinite S`
hoelzl@50134
   533
  ultimately show ?thesis
hoelzl@50134
   534
    unfolding bij_betw_def by (auto intro: enumerate_in_set)
hoelzl@50134
   535
qed
hoelzl@50134
   536
wenzelm@20809
   537
subsection "Miscellaneous"
wenzelm@20809
   538
wenzelm@20809
   539
text {*
wenzelm@20809
   540
  A few trivial lemmas about sets that contain at most one element.
wenzelm@20809
   541
  These simplify the reasoning about deterministic automata.
wenzelm@20809
   542
*}
wenzelm@20809
   543
wenzelm@53239
   544
definition atmost_one :: "'a set \<Rightarrow> bool"
wenzelm@53239
   545
  where "atmost_one S \<longleftrightarrow> (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x = y)"
wenzelm@20809
   546
wenzelm@20809
   547
lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
wenzelm@20809
   548
  by (simp add: atmost_one_def)
wenzelm@20809
   549
wenzelm@20809
   550
lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
wenzelm@20809
   551
  by (simp add: atmost_one_def)
wenzelm@20809
   552
wenzelm@20809
   553
lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
wenzelm@20809
   554
  by (simp add: atmost_one_def)
wenzelm@20809
   555
wenzelm@20809
   556
end
traytel@54612
   557