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