src/HOL/Library/Infinite_Set.thy
author bulwahn
Tue Apr 05 09:38:28 2011 +0200 (2011-04-05)
changeset 42231 bc1891226d00
parent 40786 0a54cfc9add3
child 44169 bdcc11b2fdc8
permissions -rw-r--r--
removing bounded_forall code equation for characters when loading Code_Char
     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_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
    56   by simp
    57 
    58 lemma infinite_super:
    59   assumes T: "S \<subseteq> T" and S: "infinite S"
    60   shows "infinite T"
    61 proof
    62   assume "finite T"
    63   with T have "finite S" by (simp add: finite_subset)
    64   with S show False by simp
    65 qed
    66 
    67 text {*
    68   As a concrete example, we prove that the set of natural numbers is
    69   infinite.
    70 *}
    71 
    72 lemma finite_nat_bounded:
    73   assumes S: "finite (S::nat set)"
    74   shows "\<exists>k. S \<subseteq> {..<k}"  (is "\<exists>k. ?bounded S k")
    75 using S
    76 proof induct
    77   have "?bounded {} 0" by simp
    78   then show "\<exists>k. ?bounded {} k" ..
    79 next
    80   fix S x
    81   assume "\<exists>k. ?bounded S k"
    82   then obtain k where k: "?bounded S k" ..
    83   show "\<exists>k. ?bounded (insert x S) k"
    84   proof (cases "x < k")
    85     case True
    86     with k show ?thesis by auto
    87   next
    88     case False
    89     with k have "?bounded S (Suc x)" by auto
    90     then show ?thesis by auto
    91   qed
    92 qed
    93 
    94 lemma finite_nat_iff_bounded:
    95   "finite (S::nat set) = (\<exists>k. S \<subseteq> {..<k})"  (is "?lhs = ?rhs")
    96 proof
    97   assume ?lhs
    98   then show ?rhs by (rule finite_nat_bounded)
    99 next
   100   assume ?rhs
   101   then obtain k where "S \<subseteq> {..<k}" ..
   102   then show "finite S"
   103     by (rule finite_subset) simp
   104 qed
   105 
   106 lemma finite_nat_iff_bounded_le:
   107   "finite (S::nat set) = (\<exists>k. S \<subseteq> {..k})"  (is "?lhs = ?rhs")
   108 proof
   109   assume ?lhs
   110   then obtain k where "S \<subseteq> {..<k}"
   111     by (blast dest: finite_nat_bounded)
   112   then have "S \<subseteq> {..k}" by auto
   113   then show ?rhs ..
   114 next
   115   assume ?rhs
   116   then obtain k where "S \<subseteq> {..k}" ..
   117   then show "finite S"
   118     by (rule finite_subset) simp
   119 qed
   120 
   121 lemma infinite_nat_iff_unbounded:
   122   "infinite (S::nat set) = (\<forall>m. \<exists>n. m<n \<and> n\<in>S)"
   123   (is "?lhs = ?rhs")
   124 proof
   125   assume ?lhs
   126   show ?rhs
   127   proof (rule ccontr)
   128     assume "\<not> ?rhs"
   129     then obtain m where m: "\<forall>n. m<n \<longrightarrow> n\<notin>S" by blast
   130     then have "S \<subseteq> {..m}"
   131       by (auto simp add: sym [OF linorder_not_less])
   132     with `?lhs` show False
   133       by (simp add: finite_nat_iff_bounded_le)
   134   qed
   135 next
   136   assume ?rhs
   137   show ?lhs
   138   proof
   139     assume "finite S"
   140     then obtain m where "S \<subseteq> {..m}"
   141       by (auto simp add: finite_nat_iff_bounded_le)
   142     then have "\<forall>n. m<n \<longrightarrow> n\<notin>S" by auto
   143     with `?rhs` show False by blast
   144   qed
   145 qed
   146 
   147 lemma infinite_nat_iff_unbounded_le:
   148   "infinite (S::nat set) = (\<forall>m. \<exists>n. m\<le>n \<and> n\<in>S)"
   149   (is "?lhs = ?rhs")
   150 proof
   151   assume ?lhs
   152   show ?rhs
   153   proof
   154     fix m
   155     from `?lhs` obtain n where "m<n \<and> n\<in>S"
   156       by (auto simp add: infinite_nat_iff_unbounded)
   157     then have "m\<le>n \<and> n\<in>S" by simp
   158     then show "\<exists>n. m \<le> n \<and> n \<in> S" ..
   159   qed
   160 next
   161   assume ?rhs
   162   show ?lhs
   163   proof (auto simp add: infinite_nat_iff_unbounded)
   164     fix m
   165     from `?rhs` obtain n where "Suc m \<le> n \<and> n\<in>S"
   166       by blast
   167     then have "m<n \<and> n\<in>S" by simp
   168     then show "\<exists>n. m < n \<and> n \<in> S" ..
   169   qed
   170 qed
   171 
   172 text {*
   173   For a set of natural numbers to be infinite, it is enough to know
   174   that for any number larger than some @{text k}, there is some larger
   175   number that is an element of the set.
   176 *}
   177 
   178 lemma unbounded_k_infinite:
   179   assumes k: "\<forall>m. k<m \<longrightarrow> (\<exists>n. m<n \<and> n\<in>S)"
   180   shows "infinite (S::nat set)"
   181 proof -
   182   {
   183     fix m have "\<exists>n. m<n \<and> n\<in>S"
   184     proof (cases "k<m")
   185       case True
   186       with k show ?thesis by blast
   187     next
   188       case False
   189       from k obtain n where "Suc k < n \<and> n\<in>S" by auto
   190       with False have "m<n \<and> n\<in>S" by auto
   191       then show ?thesis ..
   192     qed
   193   }
   194   then show ?thesis
   195     by (auto simp add: infinite_nat_iff_unbounded)
   196 qed
   197 
   198 (* duplicates Finite_Set.infinite_UNIV_nat *)
   199 lemma nat_infinite: "infinite (UNIV :: nat set)"
   200   by (auto simp add: infinite_nat_iff_unbounded)
   201 
   202 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
   203   by simp
   204 
   205 text {*
   206   Every infinite set contains a countable subset. More precisely we
   207   show that a set @{text S} is infinite if and only if there exists an
   208   injective function from the naturals into @{text S}.
   209 *}
   210 
   211 lemma range_inj_infinite:
   212   "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
   213 proof
   214   assume "finite (range f)" and "inj f"
   215   then have "finite (UNIV::nat set)"
   216     by (rule finite_imageD)
   217   then show False by simp
   218 qed
   219 
   220 lemma int_infinite [simp]:
   221   shows "infinite (UNIV::int set)"
   222 proof -
   223   from inj_int have "infinite (range int)" by (rule range_inj_infinite)
   224   moreover 
   225   have "range int \<subseteq> (UNIV::int set)" by simp
   226   ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super)
   227 qed
   228 
   229 text {*
   230   The ``only if'' direction is harder because it requires the
   231   construction of a sequence of pairwise different elements of an
   232   infinite set @{text S}. The idea is to construct a sequence of
   233   non-empty and infinite subsets of @{text S} obtained by successively
   234   removing elements of @{text S}.
   235 *}
   236 
   237 lemma linorder_injI:
   238   assumes hyp: "!!x y. x < (y::'a::linorder) ==> f x \<noteq> f y"
   239   shows "inj f"
   240 proof (rule inj_onI)
   241   fix x y
   242   assume f_eq: "f x = f y"
   243   show "x = y"
   244   proof (rule linorder_cases)
   245     assume "x < y"
   246     with hyp have "f x \<noteq> f y" by blast
   247     with f_eq show ?thesis by simp
   248   next
   249     assume "x = y"
   250     then show ?thesis .
   251   next
   252     assume "y < x"
   253     with hyp have "f y \<noteq> f x" by blast
   254     with f_eq show ?thesis by simp
   255   qed
   256 qed
   257 
   258 lemma infinite_countable_subset:
   259   assumes inf: "infinite (S::'a set)"
   260   shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
   261 proof -
   262   def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
   263   def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   264   have Sseq_inf: "\<And>n. infinite (Sseq n)"
   265   proof -
   266     fix n
   267     show "infinite (Sseq n)"
   268     proof (induct n)
   269       from inf show "infinite (Sseq 0)"
   270         by (simp add: Sseq_def)
   271     next
   272       fix n
   273       assume "infinite (Sseq n)" then show "infinite (Sseq (Suc n))"
   274         by (simp add: Sseq_def infinite_remove)
   275     qed
   276   qed
   277   have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
   278   proof -
   279     fix n
   280     show "Sseq n \<subseteq> S"
   281       by (induct n) (auto simp add: Sseq_def)
   282   qed
   283   have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
   284   proof -
   285     fix n
   286     show "pick n \<in> Sseq n"
   287     proof (unfold pick_def, 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 = (\<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
   363   Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
   364   "Inf_many P = infinite {x. P x}"
   365 
   366 definition
   367   Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
   368   "Alm_all P = (\<not> (INFM x. \<not> P x))"
   369 
   370 notation (xsymbols)
   371   Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
   372   Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   373 
   374 notation (HTML output)
   375   Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
   376   Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   377 
   378 lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}"
   379   unfolding Inf_many_def ..
   380 
   381 lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}"
   382   unfolding Alm_all_def Inf_many_def by simp
   383 
   384 (* legacy name *)
   385 lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
   386 
   387 lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
   388   unfolding Alm_all_def not_not ..
   389 
   390 lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
   391   unfolding Alm_all_def not_not ..
   392 
   393 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
   394   unfolding Inf_many_def by simp
   395 
   396 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
   397   unfolding Alm_all_def by simp
   398 
   399 lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
   400   by (erule contrapos_pp, simp)
   401 
   402 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
   403   by simp
   404 
   405 lemma INFM_E: assumes "INFM x. P x" obtains x where "P x"
   406   using INFM_EX [OF assms] by (rule exE)
   407 
   408 lemma MOST_I: assumes "\<And>x. P x" shows "MOST x. P x"
   409   using assms by simp
   410 
   411 lemma INFM_mono:
   412   assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
   413   shows "\<exists>\<^sub>\<infinity>x. Q x"
   414 proof -
   415   from inf have "infinite {x. P x}" unfolding Inf_many_def .
   416   moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
   417   ultimately show ?thesis
   418     by (simp add: Inf_many_def infinite_super)
   419 qed
   420 
   421 lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
   422   unfolding Alm_all_def by (blast intro: INFM_mono)
   423 
   424 lemma INFM_disj_distrib:
   425   "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
   426   unfolding Inf_many_def by (simp add: Collect_disj_eq)
   427 
   428 lemma INFM_imp_distrib:
   429   "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
   430   by (simp only: imp_conv_disj INFM_disj_distrib not_MOST)
   431 
   432 lemma MOST_conj_distrib:
   433   "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
   434   unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
   435 
   436 lemma MOST_conjI:
   437   "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
   438   by (simp add: MOST_conj_distrib)
   439 
   440 lemma INFM_conjI:
   441   "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
   442   unfolding MOST_iff_cofinite INFM_iff_infinite
   443   apply (drule (1) Diff_infinite_finite)
   444   apply (simp add: Collect_conj_eq Collect_neg_eq)
   445   done
   446 
   447 lemma MOST_rev_mp:
   448   assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
   449   shows "\<forall>\<^sub>\<infinity>x. Q x"
   450 proof -
   451   have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
   452     using assms by (rule MOST_conjI)
   453   thus ?thesis by (rule MOST_mono) simp
   454 qed
   455 
   456 lemma MOST_imp_iff:
   457   assumes "MOST x. P x"
   458   shows "(MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
   459 proof
   460   assume "MOST x. P x \<longrightarrow> Q x"
   461   with assms show "MOST x. Q x" by (rule MOST_rev_mp)
   462 next
   463   assume "MOST x. Q x"
   464   then show "MOST x. P x \<longrightarrow> Q x" by (rule MOST_mono) simp
   465 qed
   466 
   467 lemma INFM_MOST_simps [simp]:
   468   "\<And>P Q. (INFM x. P x \<and> Q) \<longleftrightarrow> (INFM x. P x) \<and> Q"
   469   "\<And>P Q. (INFM x. P \<and> Q x) \<longleftrightarrow> P \<and> (INFM x. Q x)"
   470   "\<And>P Q. (MOST x. P x \<or> Q) \<longleftrightarrow> (MOST x. P x) \<or> Q"
   471   "\<And>P Q. (MOST x. P \<or> Q x) \<longleftrightarrow> P \<or> (MOST x. Q x)"
   472   "\<And>P Q. (MOST x. P x \<longrightarrow> Q) \<longleftrightarrow> ((INFM x. P x) \<longrightarrow> Q)"
   473   "\<And>P Q. (MOST x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (MOST x. Q x))"
   474   unfolding Alm_all_def Inf_many_def
   475   by (simp_all add: Collect_conj_eq)
   476 
   477 text {* Properties of quantifiers with injective functions. *}
   478 
   479 lemma INFM_inj:
   480   "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
   481   unfolding INFM_iff_infinite
   482   by (clarify, drule (1) finite_vimageI, simp)
   483 
   484 lemma MOST_inj:
   485   "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
   486   unfolding MOST_iff_cofinite
   487   by (drule (1) finite_vimageI, simp)
   488 
   489 text {* Properties of quantifiers with singletons. *}
   490 
   491 lemma not_INFM_eq [simp]:
   492   "\<not> (INFM x. x = a)"
   493   "\<not> (INFM x. a = x)"
   494   unfolding INFM_iff_infinite by simp_all
   495 
   496 lemma MOST_neq [simp]:
   497   "MOST x. x \<noteq> a"
   498   "MOST x. a \<noteq> x"
   499   unfolding MOST_iff_cofinite by simp_all
   500 
   501 lemma INFM_neq [simp]:
   502   "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
   503   "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
   504   unfolding INFM_iff_infinite by simp_all
   505 
   506 lemma MOST_eq [simp]:
   507   "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
   508   "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
   509   unfolding MOST_iff_cofinite by simp_all
   510 
   511 lemma MOST_eq_imp:
   512   "MOST x. x = a \<longrightarrow> P x"
   513   "MOST x. a = x \<longrightarrow> P x"
   514   unfolding MOST_iff_cofinite by simp_all
   515 
   516 text {* Properties of quantifiers over the naturals. *}
   517 
   518 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
   519   by (simp add: Inf_many_def infinite_nat_iff_unbounded)
   520 
   521 lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
   522   by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
   523 
   524 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
   525   by (simp add: Alm_all_def INFM_nat)
   526 
   527 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
   528   by (simp add: Alm_all_def INFM_nat_le)
   529 
   530 
   531 subsection "Enumeration of an Infinite Set"
   532 
   533 text {*
   534   The set's element type must be wellordered (e.g. the natural numbers).
   535 *}
   536 
   537 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
   538     enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
   539   | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   540 
   541 lemma enumerate_Suc':
   542     "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   543   by simp
   544 
   545 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
   546 apply (induct n arbitrary: S)
   547  apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
   548 apply simp
   549 apply (metis Collect_def Collect_mem_eq DiffE infinite_remove)
   550 done
   551 
   552 declare enumerate_0 [simp del] enumerate_Suc [simp del]
   553 
   554 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
   555   apply (induct n arbitrary: S)
   556    apply (rule order_le_neq_trans)
   557     apply (simp add: enumerate_0 Least_le enumerate_in_set)
   558    apply (simp only: enumerate_Suc')
   559    apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
   560     apply (blast intro: sym)
   561    apply (simp add: enumerate_in_set del: Diff_iff)
   562   apply (simp add: enumerate_Suc')
   563   done
   564 
   565 lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   566   apply (erule less_Suc_induct)
   567   apply (auto intro: enumerate_step)
   568   done
   569 
   570 
   571 subsection "Miscellaneous"
   572 
   573 text {*
   574   A few trivial lemmas about sets that contain at most one element.
   575   These simplify the reasoning about deterministic automata.
   576 *}
   577 
   578 definition
   579   atmost_one :: "'a set \<Rightarrow> bool" where
   580   "atmost_one S = (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y)"
   581 
   582 lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
   583   by (simp add: atmost_one_def)
   584 
   585 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
   586   by (simp add: atmost_one_def)
   587 
   588 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
   589   by (simp add: atmost_one_def)
   590 
   591 end