src/HOL/Library/Infinite_Set.thy
author huffman
Tue Jul 01 01:19:08 2008 +0200 (2008-07-01)
changeset 27407 68e111812b83
parent 27368 9f90ac19e32b
child 27487 c8a6ce181805
permissions -rw-r--r--
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
     1 (*  Title:      HOL/Library/Infinite_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 "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]:
   219   shows "infinite (UNIV::int set)"
   220 proof -
   221   from inj_int have "infinite (range int)" by (rule range_inj_infinite)
   222   moreover 
   223   have "range int \<subseteq> (UNIV::int set)" by simp
   224   ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super)
   225 qed
   226 
   227 text {*
   228   The ``only if'' direction is harder because it requires the
   229   construction of a sequence of pairwise different elements of an
   230   infinite set @{text S}. The idea is to construct a sequence of
   231   non-empty and infinite subsets of @{text S} obtained by successively
   232   removing elements of @{text S}.
   233 *}
   234 
   235 lemma linorder_injI:
   236   assumes hyp: "!!x y. x < (y::'a::linorder) ==> f x \<noteq> f y"
   237   shows "inj f"
   238 proof (rule inj_onI)
   239   fix x y
   240   assume f_eq: "f x = f y"
   241   show "x = y"
   242   proof (rule linorder_cases)
   243     assume "x < y"
   244     with hyp have "f x \<noteq> f y" by blast
   245     with f_eq show ?thesis by simp
   246   next
   247     assume "x = y"
   248     then show ?thesis .
   249   next
   250     assume "y < x"
   251     with hyp have "f y \<noteq> f x" by blast
   252     with f_eq show ?thesis by simp
   253   qed
   254 qed
   255 
   256 lemma infinite_countable_subset:
   257   assumes inf: "infinite (S::'a set)"
   258   shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
   259 proof -
   260   def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
   261   def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   262   have Sseq_inf: "\<And>n. infinite (Sseq n)"
   263   proof -
   264     fix n
   265     show "infinite (Sseq n)"
   266     proof (induct n)
   267       from inf show "infinite (Sseq 0)"
   268         by (simp add: Sseq_def)
   269     next
   270       fix n
   271       assume "infinite (Sseq n)" then show "infinite (Sseq (Suc n))"
   272         by (simp add: Sseq_def infinite_remove)
   273     qed
   274   qed
   275   have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
   276   proof -
   277     fix n
   278     show "Sseq n \<subseteq> S"
   279       by (induct n) (auto simp add: Sseq_def)
   280   qed
   281   have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
   282   proof -
   283     fix n
   284     show "pick n \<in> Sseq n"
   285     proof (unfold pick_def, rule someI_ex)
   286       from Sseq_inf have "infinite (Sseq n)" .
   287       then have "Sseq n \<noteq> {}" by auto
   288       then show "\<exists>x. x \<in> Sseq n" by auto
   289     qed
   290   qed
   291   with Sseq_S have rng: "range pick \<subseteq> S"
   292     by auto
   293   have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
   294   proof -
   295     fix n m
   296     show "pick n \<notin> Sseq (n + Suc m)"
   297       by (induct m) (auto simp add: Sseq_def pick_def)
   298   qed
   299   have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
   300   proof -
   301     fix n m
   302     from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
   303     moreover from pick_Sseq_gt
   304     have "pick n \<notin> Sseq (n + Suc m)" .
   305     ultimately show "pick n \<noteq> pick (n + Suc m)"
   306       by auto
   307   qed
   308   have inj: "inj pick"
   309   proof (rule linorder_injI)
   310     fix i j :: nat
   311     assume "i < j"
   312     show "pick i \<noteq> pick j"
   313     proof
   314       assume eq: "pick i = pick j"
   315       from `i < j` obtain k where "j = i + Suc k"
   316         by (auto simp add: less_iff_Suc_add)
   317       with pick_pick have "pick i \<noteq> pick j" by simp
   318       with eq show False by simp
   319     qed
   320   qed
   321   from rng inj show ?thesis by auto
   322 qed
   323 
   324 lemma infinite_iff_countable_subset:
   325     "infinite S = (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
   326   by (auto simp add: infinite_countable_subset range_inj_infinite infinite_super)
   327 
   328 text {*
   329   For any function with infinite domain and finite range there is some
   330   element that is the image of infinitely many domain elements.  In
   331   particular, any infinite sequence of elements from a finite set
   332   contains some element that occurs infinitely often.
   333 *}
   334 
   335 lemma inf_img_fin_dom:
   336   assumes img: "finite (f`A)" and dom: "infinite A"
   337   shows "\<exists>y \<in> f`A. infinite (f -` {y})"
   338 proof (rule ccontr)
   339   assume "\<not> ?thesis"
   340   with img have "finite (UN y:f`A. f -` {y})" by (blast intro: finite_UN_I)
   341   moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
   342   moreover note dom
   343   ultimately show False by (simp add: infinite_super)
   344 qed
   345 
   346 lemma inf_img_fin_domE:
   347   assumes "finite (f`A)" and "infinite A"
   348   obtains y where "y \<in> f`A" and "infinite (f -` {y})"
   349   using assms by (blast dest: inf_img_fin_dom)
   350 
   351 
   352 subsection "Infinitely Many and Almost All"
   353 
   354 text {*
   355   We often need to reason about the existence of infinitely many
   356   (resp., all but finitely many) objects satisfying some predicate, so
   357   we introduce corresponding binders and their proof rules.
   358 *}
   359 
   360 definition
   361   Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
   362   "Inf_many P = infinite {x. P x}"
   363 
   364 definition
   365   Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
   366   "Alm_all P = (\<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_EX:
   377   "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
   378   unfolding Inf_many_def
   379 proof (rule ccontr)
   380   assume inf: "infinite {x. P x}"
   381   assume "\<not> ?thesis" then have "{x. P x} = {}" by simp
   382   then have "finite {x. P x}" by simp
   383   with inf show False by simp
   384 qed
   385 
   386 lemma MOST_iff_finiteNeg: "(\<forall>\<^sub>\<infinity>x. P x) = finite {x. \<not> P x}"
   387   by (simp add: Alm_all_def Inf_many_def)
   388 
   389 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
   390   by (simp add: MOST_iff_finiteNeg)
   391 
   392 lemma INFM_mono:
   393   assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
   394   shows "\<exists>\<^sub>\<infinity>x. Q x"
   395 proof -
   396   from inf have "infinite {x. P x}" unfolding Inf_many_def .
   397   moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
   398   ultimately show ?thesis
   399     by (simp add: Inf_many_def infinite_super)
   400 qed
   401 
   402 lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
   403   unfolding Alm_all_def by (blast intro: INFM_mono)
   404 
   405 lemma INFM_disj_distrib:
   406   "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
   407   unfolding Inf_many_def by (simp add: Collect_disj_eq)
   408 
   409 lemma MOST_conj_distrib:
   410   "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
   411   unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
   412 
   413 lemma MOST_rev_mp:
   414   assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
   415   shows "\<forall>\<^sub>\<infinity>x. Q x"
   416 proof -
   417   have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
   418     using prems by (simp add: MOST_conj_distrib)
   419   thus ?thesis by (rule MOST_mono) simp
   420 qed
   421 
   422 lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
   423 unfolding Alm_all_def not_not ..
   424 
   425 lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
   426 unfolding Alm_all_def not_not ..
   427 
   428 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
   429   unfolding Inf_many_def by simp
   430 
   431 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
   432   unfolding Alm_all_def by simp
   433 
   434 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
   435   by (simp add: Inf_many_def infinite_nat_iff_unbounded)
   436 
   437 lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
   438   by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
   439 
   440 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
   441   by (simp add: Alm_all_def INFM_nat)
   442 
   443 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
   444   by (simp add: Alm_all_def INFM_nat_le)
   445 
   446 
   447 subsection "Enumeration of an Infinite Set"
   448 
   449 text {*
   450   The set's element type must be wellordered (e.g. the natural numbers).
   451 *}
   452 
   453 consts
   454   enumerate   :: "'a::wellorder set => (nat => 'a::wellorder)"
   455 primrec
   456   enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
   457   enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   458 
   459 lemma enumerate_Suc':
   460     "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   461   by simp
   462 
   463 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
   464   apply (induct n arbitrary: S)
   465    apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
   466   apply (fastsimp iff: finite_Diff_singleton)
   467   done
   468 
   469 declare enumerate_0 [simp del] enumerate_Suc [simp del]
   470 
   471 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
   472   apply (induct n arbitrary: S)
   473    apply (rule order_le_neq_trans)
   474     apply (simp add: enumerate_0 Least_le enumerate_in_set)
   475    apply (simp only: enumerate_Suc')
   476    apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
   477     apply (blast intro: sym)
   478    apply (simp add: enumerate_in_set del: Diff_iff)
   479   apply (simp add: enumerate_Suc')
   480   done
   481 
   482 lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   483   apply (erule less_Suc_induct)
   484   apply (auto intro: enumerate_step)
   485   done
   486 
   487 
   488 subsection "Miscellaneous"
   489 
   490 text {*
   491   A few trivial lemmas about sets that contain at most one element.
   492   These simplify the reasoning about deterministic automata.
   493 *}
   494 
   495 definition
   496   atmost_one :: "'a set \<Rightarrow> bool" where
   497   "atmost_one S = (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y)"
   498 
   499 lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
   500   by (simp add: atmost_one_def)
   501 
   502 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
   503   by (simp add: atmost_one_def)
   504 
   505 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
   506   by (simp add: atmost_one_def)
   507 
   508 end