src/HOL/Library/Infinite_Set.thy
author huffman
Sun Feb 07 10:16:10 2010 -0800 (2010-02-07)
changeset 35056 d97b5c3af6d5
parent 34941 156925dd67af
child 35844 65258d2c3214
permissions -rw-r--r--
remove redundant theorem attributes
     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 (* duplicates Finite_Set.infinite_UNIV_nat *)
   196 lemma nat_infinite: "infinite (UNIV :: nat set)"
   197   by (auto simp add: infinite_nat_iff_unbounded)
   198 
   199 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
   200   by simp
   201 
   202 text {*
   203   Every infinite set contains a countable subset. More precisely we
   204   show that a set @{text S} is infinite if and only if there exists an
   205   injective function from the naturals into @{text S}.
   206 *}
   207 
   208 lemma range_inj_infinite:
   209   "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
   210 proof
   211   assume "finite (range f)" and "inj f"
   212   then have "finite (UNIV::nat set)"
   213     by (rule finite_imageD)
   214   then show False by simp
   215 qed
   216 
   217 lemma int_infinite [simp]:
   218   shows "infinite (UNIV::int set)"
   219 proof -
   220   from inj_int have "infinite (range int)" by (rule range_inj_infinite)
   221   moreover 
   222   have "range int \<subseteq> (UNIV::int set)" by simp
   223   ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super)
   224 qed
   225 
   226 text {*
   227   The ``only if'' direction is harder because it requires the
   228   construction of a sequence of pairwise different elements of an
   229   infinite set @{text S}. The idea is to construct a sequence of
   230   non-empty and infinite subsets of @{text S} obtained by successively
   231   removing elements of @{text S}.
   232 *}
   233 
   234 lemma linorder_injI:
   235   assumes hyp: "!!x y. x < (y::'a::linorder) ==> f x \<noteq> f y"
   236   shows "inj f"
   237 proof (rule inj_onI)
   238   fix x y
   239   assume f_eq: "f x = f y"
   240   show "x = y"
   241   proof (rule linorder_cases)
   242     assume "x < y"
   243     with hyp have "f x \<noteq> f y" by blast
   244     with f_eq show ?thesis by simp
   245   next
   246     assume "x = y"
   247     then show ?thesis .
   248   next
   249     assume "y < x"
   250     with hyp have "f y \<noteq> f x" by blast
   251     with f_eq show ?thesis by simp
   252   qed
   253 qed
   254 
   255 lemma infinite_countable_subset:
   256   assumes inf: "infinite (S::'a set)"
   257   shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
   258 proof -
   259   def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
   260   def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   261   have Sseq_inf: "\<And>n. infinite (Sseq n)"
   262   proof -
   263     fix n
   264     show "infinite (Sseq n)"
   265     proof (induct n)
   266       from inf show "infinite (Sseq 0)"
   267         by (simp add: Sseq_def)
   268     next
   269       fix n
   270       assume "infinite (Sseq n)" then show "infinite (Sseq (Suc n))"
   271         by (simp add: Sseq_def infinite_remove)
   272     qed
   273   qed
   274   have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
   275   proof -
   276     fix n
   277     show "Sseq n \<subseteq> S"
   278       by (induct n) (auto simp add: Sseq_def)
   279   qed
   280   have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
   281   proof -
   282     fix n
   283     show "pick n \<in> Sseq n"
   284     proof (unfold pick_def, rule someI_ex)
   285       from Sseq_inf have "infinite (Sseq n)" .
   286       then have "Sseq n \<noteq> {}" by auto
   287       then show "\<exists>x. x \<in> Sseq n" by auto
   288     qed
   289   qed
   290   with Sseq_S have rng: "range pick \<subseteq> S"
   291     by auto
   292   have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
   293   proof -
   294     fix n m
   295     show "pick n \<notin> Sseq (n + Suc m)"
   296       by (induct m) (auto simp add: Sseq_def pick_def)
   297   qed
   298   have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
   299   proof -
   300     fix n m
   301     from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
   302     moreover from pick_Sseq_gt
   303     have "pick n \<notin> Sseq (n + Suc m)" .
   304     ultimately show "pick n \<noteq> pick (n + Suc m)"
   305       by auto
   306   qed
   307   have inj: "inj pick"
   308   proof (rule linorder_injI)
   309     fix i j :: nat
   310     assume "i < j"
   311     show "pick i \<noteq> pick j"
   312     proof
   313       assume eq: "pick i = pick j"
   314       from `i < j` obtain k where "j = i + Suc k"
   315         by (auto simp add: less_iff_Suc_add)
   316       with pick_pick have "pick i \<noteq> pick j" by simp
   317       with eq show False by simp
   318     qed
   319   qed
   320   from rng inj show ?thesis by auto
   321 qed
   322 
   323 lemma infinite_iff_countable_subset:
   324     "infinite S = (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
   325   by (auto simp add: infinite_countable_subset range_inj_infinite infinite_super)
   326 
   327 text {*
   328   For any function with infinite domain and finite range there is some
   329   element that is the image of infinitely many domain elements.  In
   330   particular, any infinite sequence of elements from a finite set
   331   contains some element that occurs infinitely often.
   332 *}
   333 
   334 lemma inf_img_fin_dom:
   335   assumes img: "finite (f`A)" and dom: "infinite A"
   336   shows "\<exists>y \<in> f`A. infinite (f -` {y})"
   337 proof (rule ccontr)
   338   assume "\<not> ?thesis"
   339   with img have "finite (UN y:f`A. f -` {y})" by (blast intro: finite_UN_I)
   340   moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
   341   moreover note dom
   342   ultimately show False by (simp add: infinite_super)
   343 qed
   344 
   345 lemma inf_img_fin_domE:
   346   assumes "finite (f`A)" and "infinite A"
   347   obtains y where "y \<in> f`A" and "infinite (f -` {y})"
   348   using assms by (blast dest: inf_img_fin_dom)
   349 
   350 
   351 subsection "Infinitely Many and Almost All"
   352 
   353 text {*
   354   We often need to reason about the existence of infinitely many
   355   (resp., all but finitely many) objects satisfying some predicate, so
   356   we introduce corresponding binders and their proof rules.
   357 *}
   358 
   359 definition
   360   Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
   361   "Inf_many P = infinite {x. P x}"
   362 
   363 definition
   364   Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
   365   "Alm_all P = (\<not> (INFM x. \<not> P x))"
   366 
   367 notation (xsymbols)
   368   Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
   369   Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   370 
   371 notation (HTML output)
   372   Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
   373   Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   374 
   375 lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}"
   376   unfolding Inf_many_def ..
   377 
   378 lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}"
   379   unfolding Alm_all_def Inf_many_def by simp
   380 
   381 (* legacy name *)
   382 lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
   383 
   384 lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
   385   unfolding Alm_all_def not_not ..
   386 
   387 lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
   388   unfolding Alm_all_def not_not ..
   389 
   390 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
   391   unfolding Inf_many_def by simp
   392 
   393 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
   394   unfolding Alm_all_def by simp
   395 
   396 lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
   397   by (erule contrapos_pp, simp)
   398 
   399 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
   400   by simp
   401 
   402 lemma INFM_E: assumes "INFM x. P x" obtains x where "P x"
   403   using INFM_EX [OF assms] by (rule exE)
   404 
   405 lemma MOST_I: assumes "\<And>x. P x" shows "MOST x. P x"
   406   using assms by simp
   407 
   408 lemma INFM_mono:
   409   assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
   410   shows "\<exists>\<^sub>\<infinity>x. Q x"
   411 proof -
   412   from inf have "infinite {x. P x}" unfolding Inf_many_def .
   413   moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
   414   ultimately show ?thesis
   415     by (simp add: Inf_many_def infinite_super)
   416 qed
   417 
   418 lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
   419   unfolding Alm_all_def by (blast intro: INFM_mono)
   420 
   421 lemma INFM_disj_distrib:
   422   "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
   423   unfolding Inf_many_def by (simp add: Collect_disj_eq)
   424 
   425 lemma INFM_imp_distrib:
   426   "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
   427   by (simp only: imp_conv_disj INFM_disj_distrib not_MOST)
   428 
   429 lemma MOST_conj_distrib:
   430   "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
   431   unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
   432 
   433 lemma MOST_conjI:
   434   "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
   435   by (simp add: MOST_conj_distrib)
   436 
   437 lemma INFM_conjI:
   438   "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
   439   unfolding MOST_iff_cofinite INFM_iff_infinite
   440   apply (drule (1) Diff_infinite_finite)
   441   apply (simp add: Collect_conj_eq Collect_neg_eq)
   442   done
   443 
   444 lemma MOST_rev_mp:
   445   assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
   446   shows "\<forall>\<^sub>\<infinity>x. Q x"
   447 proof -
   448   have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
   449     using assms by (rule MOST_conjI)
   450   thus ?thesis by (rule MOST_mono) simp
   451 qed
   452 
   453 lemma MOST_imp_iff:
   454   assumes "MOST x. P x"
   455   shows "(MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
   456 proof
   457   assume "MOST x. P x \<longrightarrow> Q x"
   458   with assms show "MOST x. Q x" by (rule MOST_rev_mp)
   459 next
   460   assume "MOST x. Q x"
   461   then show "MOST x. P x \<longrightarrow> Q x" by (rule MOST_mono) simp
   462 qed
   463 
   464 lemma INFM_MOST_simps [simp]:
   465   "\<And>P Q. (INFM x. P x \<and> Q) \<longleftrightarrow> (INFM x. P x) \<and> Q"
   466   "\<And>P Q. (INFM x. P \<and> Q x) \<longleftrightarrow> P \<and> (INFM x. Q x)"
   467   "\<And>P Q. (MOST x. P x \<or> Q) \<longleftrightarrow> (MOST x. P x) \<or> Q"
   468   "\<And>P Q. (MOST x. P \<or> Q x) \<longleftrightarrow> P \<or> (MOST x. Q x)"
   469   "\<And>P Q. (MOST x. P x \<longrightarrow> Q) \<longleftrightarrow> ((INFM x. P x) \<longrightarrow> Q)"
   470   "\<And>P Q. (MOST x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (MOST x. Q x))"
   471   unfolding Alm_all_def Inf_many_def
   472   by (simp_all add: Collect_conj_eq)
   473 
   474 text {* Properties of quantifiers with injective functions. *}
   475 
   476 lemma INFM_inj:
   477   "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
   478   unfolding INFM_iff_infinite
   479   by (clarify, drule (1) finite_vimageI, simp)
   480 
   481 lemma MOST_inj:
   482   "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
   483   unfolding MOST_iff_cofinite
   484   by (drule (1) finite_vimageI, simp)
   485 
   486 text {* Properties of quantifiers with singletons. *}
   487 
   488 lemma not_INFM_eq [simp]:
   489   "\<not> (INFM x. x = a)"
   490   "\<not> (INFM x. a = x)"
   491   unfolding INFM_iff_infinite by simp_all
   492 
   493 lemma MOST_neq [simp]:
   494   "MOST x. x \<noteq> a"
   495   "MOST x. a \<noteq> x"
   496   unfolding MOST_iff_cofinite by simp_all
   497 
   498 lemma INFM_neq [simp]:
   499   "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
   500   "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
   501   unfolding INFM_iff_infinite by simp_all
   502 
   503 lemma MOST_eq [simp]:
   504   "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
   505   "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
   506   unfolding MOST_iff_cofinite by simp_all
   507 
   508 lemma MOST_eq_imp:
   509   "MOST x. x = a \<longrightarrow> P x"
   510   "MOST x. a = x \<longrightarrow> P x"
   511   unfolding MOST_iff_cofinite by simp_all
   512 
   513 text {* Properties of quantifiers over the naturals. *}
   514 
   515 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
   516   by (simp add: Inf_many_def infinite_nat_iff_unbounded)
   517 
   518 lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
   519   by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
   520 
   521 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
   522   by (simp add: Alm_all_def INFM_nat)
   523 
   524 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
   525   by (simp add: Alm_all_def INFM_nat_le)
   526 
   527 
   528 subsection "Enumeration of an Infinite Set"
   529 
   530 text {*
   531   The set's element type must be wellordered (e.g. the natural numbers).
   532 *}
   533 
   534 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
   535     enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
   536   | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   537 
   538 lemma enumerate_Suc':
   539     "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   540   by simp
   541 
   542 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
   543 apply (induct n arbitrary: S)
   544  apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
   545 apply simp
   546 apply (metis Collect_def Collect_mem_eq DiffE infinite_remove)
   547 done
   548 
   549 declare enumerate_0 [simp del] enumerate_Suc [simp del]
   550 
   551 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
   552   apply (induct n arbitrary: S)
   553    apply (rule order_le_neq_trans)
   554     apply (simp add: enumerate_0 Least_le enumerate_in_set)
   555    apply (simp only: enumerate_Suc')
   556    apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
   557     apply (blast intro: sym)
   558    apply (simp add: enumerate_in_set del: Diff_iff)
   559   apply (simp add: enumerate_Suc')
   560   done
   561 
   562 lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   563   apply (erule less_Suc_induct)
   564   apply (auto intro: enumerate_step)
   565   done
   566 
   567 
   568 subsection "Miscellaneous"
   569 
   570 text {*
   571   A few trivial lemmas about sets that contain at most one element.
   572   These simplify the reasoning about deterministic automata.
   573 *}
   574 
   575 definition
   576   atmost_one :: "'a set \<Rightarrow> bool" where
   577   "atmost_one S = (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y)"
   578 
   579 lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
   580   by (simp add: atmost_one_def)
   581 
   582 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
   583   by (simp add: atmost_one_def)
   584 
   585 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
   586   by (simp add: atmost_one_def)
   587 
   588 end