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