src/HOL/Library/Infinite_Set.thy
author haftmann
Thu Jun 26 10:07:01 2008 +0200 (2008-06-26)
changeset 27368 9f90ac19e32b
parent 25671 5e9d6f77d11a
child 27407 68e111812b83
permissions -rw-r--r--
established Plain theory and image
     1 (*  Title:      HOL/Infnite_Set.thy
     2     ID:         $Id$
     3     Author:     Stephan Merz
     4 *)
     5 
     6 header {* Infinite Sets and Related Concepts *}
     7 
     8 theory Infinite_Set
     9 imports Plain SetInterval Hilbert_Choice
    10 begin
    11 
    12 
    13 subsection "Infinite Sets"
    14 
    15 text {*
    16   Some elementary facts about infinite sets, mostly by Stefan Merz.
    17   Beware! Because "infinite" merely abbreviates a negation, these
    18   lemmas may not work well with @{text "blast"}.
    19 *}
    20 
    21 abbreviation
    22   infinite :: "'a set \<Rightarrow> bool" where
    23   "infinite S == \<not> finite S"
    24 
    25 text {*
    26   Infinite sets are non-empty, and if we remove some elements from an
    27   infinite set, the result is still infinite.
    28 *}
    29 
    30 lemma infinite_imp_nonempty: "infinite S ==> S \<noteq> {}"
    31   by auto
    32 
    33 lemma infinite_remove:
    34   "infinite S \<Longrightarrow> infinite (S - {a})"
    35   by simp
    36 
    37 lemma Diff_infinite_finite:
    38   assumes T: "finite T" and S: "infinite S"
    39   shows "infinite (S - T)"
    40   using T
    41 proof induct
    42   from S
    43   show "infinite (S - {})" by auto
    44 next
    45   fix T x
    46   assume ih: "infinite (S - T)"
    47   have "S - (insert x T) = (S - T) - {x}"
    48     by (rule Diff_insert)
    49   with ih
    50   show "infinite (S - (insert x T))"
    51     by (simp add: infinite_remove)
    52 qed
    53 
    54 lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
    55   by simp
    56 
    57 lemma infinite_super:
    58   assumes T: "S \<subseteq> T" and S: "infinite S"
    59   shows "infinite T"
    60 proof
    61   assume "finite T"
    62   with T have "finite S" by (simp add: finite_subset)
    63   with S show False by simp
    64 qed
    65 
    66 text {*
    67   As a concrete example, we prove that the set of natural numbers is
    68   infinite.
    69 *}
    70 
    71 lemma finite_nat_bounded:
    72   assumes S: "finite (S::nat set)"
    73   shows "\<exists>k. S \<subseteq> {..<k}"  (is "\<exists>k. ?bounded S k")
    74 using S
    75 proof induct
    76   have "?bounded {} 0" by simp
    77   then show "\<exists>k. ?bounded {} k" ..
    78 next
    79   fix S x
    80   assume "\<exists>k. ?bounded S k"
    81   then obtain k where k: "?bounded S k" ..
    82   show "\<exists>k. ?bounded (insert x S) k"
    83   proof (cases "x < k")
    84     case True
    85     with k show ?thesis by auto
    86   next
    87     case False
    88     with k have "?bounded S (Suc x)" by auto
    89     then show ?thesis by auto
    90   qed
    91 qed
    92 
    93 lemma finite_nat_iff_bounded:
    94   "finite (S::nat set) = (\<exists>k. S \<subseteq> {..<k})"  (is "?lhs = ?rhs")
    95 proof
    96   assume ?lhs
    97   then show ?rhs by (rule finite_nat_bounded)
    98 next
    99   assume ?rhs
   100   then obtain k where "S \<subseteq> {..<k}" ..
   101   then show "finite S"
   102     by (rule finite_subset) simp
   103 qed
   104 
   105 lemma finite_nat_iff_bounded_le:
   106   "finite (S::nat set) = (\<exists>k. S \<subseteq> {..k})"  (is "?lhs = ?rhs")
   107 proof
   108   assume ?lhs
   109   then obtain k where "S \<subseteq> {..<k}"
   110     by (blast dest: finite_nat_bounded)
   111   then have "S \<subseteq> {..k}" by auto
   112   then show ?rhs ..
   113 next
   114   assume ?rhs
   115   then obtain k where "S \<subseteq> {..k}" ..
   116   then show "finite S"
   117     by (rule finite_subset) simp
   118 qed
   119 
   120 lemma infinite_nat_iff_unbounded:
   121   "infinite (S::nat set) = (\<forall>m. \<exists>n. m<n \<and> n\<in>S)"
   122   (is "?lhs = ?rhs")
   123 proof
   124   assume ?lhs
   125   show ?rhs
   126   proof (rule ccontr)
   127     assume "\<not> ?rhs"
   128     then obtain m where m: "\<forall>n. m<n \<longrightarrow> n\<notin>S" by blast
   129     then have "S \<subseteq> {..m}"
   130       by (auto simp add: sym [OF linorder_not_less])
   131     with `?lhs` show False
   132       by (simp add: finite_nat_iff_bounded_le)
   133   qed
   134 next
   135   assume ?rhs
   136   show ?lhs
   137   proof
   138     assume "finite S"
   139     then obtain m where "S \<subseteq> {..m}"
   140       by (auto simp add: finite_nat_iff_bounded_le)
   141     then have "\<forall>n. m<n \<longrightarrow> n\<notin>S" by auto
   142     with `?rhs` show False by blast
   143   qed
   144 qed
   145 
   146 lemma infinite_nat_iff_unbounded_le:
   147   "infinite (S::nat set) = (\<forall>m. \<exists>n. m\<le>n \<and> n\<in>S)"
   148   (is "?lhs = ?rhs")
   149 proof
   150   assume ?lhs
   151   show ?rhs
   152   proof
   153     fix m
   154     from `?lhs` obtain n where "m<n \<and> n\<in>S"
   155       by (auto simp add: infinite_nat_iff_unbounded)
   156     then have "m\<le>n \<and> n\<in>S" by simp
   157     then show "\<exists>n. m \<le> n \<and> n \<in> S" ..
   158   qed
   159 next
   160   assume ?rhs
   161   show ?lhs
   162   proof (auto simp add: infinite_nat_iff_unbounded)
   163     fix m
   164     from `?rhs` obtain n where "Suc m \<le> n \<and> n\<in>S"
   165       by blast
   166     then have "m<n \<and> n\<in>S" by simp
   167     then show "\<exists>n. m < n \<and> n \<in> S" ..
   168   qed
   169 qed
   170 
   171 text {*
   172   For a set of natural numbers to be infinite, it is enough to know
   173   that for any number larger than some @{text k}, there is some larger
   174   number that is an element of the set.
   175 *}
   176 
   177 lemma unbounded_k_infinite:
   178   assumes k: "\<forall>m. k<m \<longrightarrow> (\<exists>n. m<n \<and> n\<in>S)"
   179   shows "infinite (S::nat set)"
   180 proof -
   181   {
   182     fix m have "\<exists>n. m<n \<and> n\<in>S"
   183     proof (cases "k<m")
   184       case True
   185       with k show ?thesis by blast
   186     next
   187       case False
   188       from k obtain n where "Suc k < n \<and> n\<in>S" by auto
   189       with False have "m<n \<and> n\<in>S" by auto
   190       then show ?thesis ..
   191     qed
   192   }
   193   then show ?thesis
   194     by (auto simp add: infinite_nat_iff_unbounded)
   195 qed
   196 
   197 lemma nat_infinite [simp]: "infinite (UNIV :: nat set)"
   198   by (auto simp add: infinite_nat_iff_unbounded)
   199 
   200 lemma nat_not_finite [elim]: "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 "inj f"
   213     and  "finite (range f)"
   214   then have "finite (UNIV::nat set)"
   215     by (auto intro: finite_imageD simp del: nat_infinite)
   216   then show False by simp
   217 qed
   218 
   219 lemma int_infinite [simp]:
   220   shows "infinite (UNIV::int set)"
   221 proof -
   222   from inj_int have "infinite (range int)" by (rule range_inj_infinite)
   223   moreover 
   224   have "range int \<subseteq> (UNIV::int set)" by simp
   225   ultimately show "infinite (UNIV::int set)" 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: "!!x y. x < (y::'a::linorder) ==> 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     proof (unfold pick_def, rule someI_ex)
   287       from Sseq_inf have "infinite (Sseq n)" .
   288       then have "Sseq n \<noteq> {}" by auto
   289       then show "\<exists>x. x \<in> Sseq n" by auto
   290     qed
   291   qed
   292   with Sseq_S have rng: "range pick \<subseteq> S"
   293     by auto
   294   have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
   295   proof -
   296     fix n m
   297     show "pick n \<notin> Sseq (n + Suc m)"
   298       by (induct m) (auto simp add: Sseq_def pick_def)
   299   qed
   300   have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
   301   proof -
   302     fix n m
   303     from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
   304     moreover from pick_Sseq_gt
   305     have "pick n \<notin> Sseq (n + Suc m)" .
   306     ultimately show "pick n \<noteq> pick (n + Suc m)"
   307       by auto
   308   qed
   309   have inj: "inj pick"
   310   proof (rule linorder_injI)
   311     fix i j :: nat
   312     assume "i < j"
   313     show "pick i \<noteq> pick j"
   314     proof
   315       assume eq: "pick i = pick j"
   316       from `i < j` obtain k where "j = i + Suc k"
   317         by (auto simp add: less_iff_Suc_add)
   318       with pick_pick have "pick i \<noteq> pick j" by simp
   319       with eq show False by simp
   320     qed
   321   qed
   322   from rng inj show ?thesis by auto
   323 qed
   324 
   325 lemma infinite_iff_countable_subset:
   326     "infinite S = (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
   327   by (auto simp add: infinite_countable_subset range_inj_infinite infinite_super)
   328 
   329 text {*
   330   For any function with infinite domain and finite range there is some
   331   element that is the image of infinitely many domain elements.  In
   332   particular, any infinite sequence of elements from a finite set
   333   contains some element that occurs infinitely often.
   334 *}
   335 
   336 lemma inf_img_fin_dom:
   337   assumes img: "finite (f`A)" and dom: "infinite A"
   338   shows "\<exists>y \<in> f`A. infinite (f -` {y})"
   339 proof (rule ccontr)
   340   assume "\<not> ?thesis"
   341   with img have "finite (UN y:f`A. f -` {y})" by (blast intro: finite_UN_I)
   342   moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
   343   moreover note dom
   344   ultimately show False by (simp add: infinite_super)
   345 qed
   346 
   347 lemma inf_img_fin_domE:
   348   assumes "finite (f`A)" and "infinite A"
   349   obtains y where "y \<in> f`A" and "infinite (f -` {y})"
   350   using assms by (blast dest: inf_img_fin_dom)
   351 
   352 
   353 subsection "Infinitely Many and Almost All"
   354 
   355 text {*
   356   We often need to reason about the existence of infinitely many
   357   (resp., all but finitely many) objects satisfying some predicate, so
   358   we introduce corresponding binders and their proof rules.
   359 *}
   360 
   361 definition
   362   Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
   363   "Inf_many P = infinite {x. P x}"
   364 
   365 definition
   366   Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
   367   "Alm_all P = (\<not> (INFM x. \<not> P x))"
   368 
   369 notation (xsymbols)
   370   Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
   371   Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   372 
   373 notation (HTML output)
   374   Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
   375   Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   376 
   377 lemma INF_EX:
   378   "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
   379   unfolding Inf_many_def
   380 proof (rule ccontr)
   381   assume inf: "infinite {x. P x}"
   382   assume "\<not> ?thesis" then have "{x. P x} = {}" by simp
   383   then have "finite {x. P x}" by simp
   384   with inf show False by simp
   385 qed
   386 
   387 lemma MOST_iff_finiteNeg: "(\<forall>\<^sub>\<infinity>x. P x) = finite {x. \<not> P x}"
   388   by (simp add: Alm_all_def Inf_many_def)
   389 
   390 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
   391   by (simp add: MOST_iff_finiteNeg)
   392 
   393 lemma INF_mono:
   394   assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
   395   shows "\<exists>\<^sub>\<infinity>x. Q x"
   396 proof -
   397   from inf have "infinite {x. P x}" unfolding Inf_many_def .
   398   moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
   399   ultimately show ?thesis
   400     by (simp add: Inf_many_def infinite_super)
   401 qed
   402 
   403 lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
   404   unfolding Alm_all_def by (blast intro: INF_mono)
   405 
   406 lemma INF_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
   407   by (simp add: Inf_many_def infinite_nat_iff_unbounded)
   408 
   409 lemma INF_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
   410   by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
   411 
   412 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
   413   by (simp add: Alm_all_def INF_nat)
   414 
   415 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
   416   by (simp add: Alm_all_def INF_nat_le)
   417 
   418 
   419 subsection "Enumeration of an Infinite Set"
   420 
   421 text {*
   422   The set's element type must be wellordered (e.g. the natural numbers).
   423 *}
   424 
   425 consts
   426   enumerate   :: "'a::wellorder set => (nat => 'a::wellorder)"
   427 primrec
   428   enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
   429   enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   430 
   431 lemma enumerate_Suc':
   432     "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   433   by simp
   434 
   435 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
   436   apply (induct n arbitrary: S)
   437    apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
   438   apply (fastsimp iff: finite_Diff_singleton)
   439   done
   440 
   441 declare enumerate_0 [simp del] enumerate_Suc [simp del]
   442 
   443 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
   444   apply (induct n arbitrary: S)
   445    apply (rule order_le_neq_trans)
   446     apply (simp add: enumerate_0 Least_le enumerate_in_set)
   447    apply (simp only: enumerate_Suc')
   448    apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
   449     apply (blast intro: sym)
   450    apply (simp add: enumerate_in_set del: Diff_iff)
   451   apply (simp add: enumerate_Suc')
   452   done
   453 
   454 lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   455   apply (erule less_Suc_induct)
   456   apply (auto intro: enumerate_step)
   457   done
   458 
   459 
   460 subsection "Miscellaneous"
   461 
   462 text {*
   463   A few trivial lemmas about sets that contain at most one element.
   464   These simplify the reasoning about deterministic automata.
   465 *}
   466 
   467 definition
   468   atmost_one :: "'a set \<Rightarrow> bool" where
   469   "atmost_one S = (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y)"
   470 
   471 lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
   472   by (simp add: atmost_one_def)
   473 
   474 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
   475   by (simp add: atmost_one_def)
   476 
   477 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
   478   by (simp add: atmost_one_def)
   479 
   480 end