src/HOL/Library/Infinite_Set.thy
author haftmann
Mon Mar 23 08:14:24 2009 +0100 (2009-03-23)
changeset 30663 0b6aff7451b2
parent 29901 f4b3f8fbf599
child 34112 ca842111d698
permissions -rw-r--r--
Main is (Complex_Main) base entry point in library theories
     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_EX:
   375   "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
   376   unfolding Inf_many_def
   377 proof (rule ccontr)
   378   assume inf: "infinite {x. P x}"
   379   assume "\<not> ?thesis" then have "{x. P x} = {}" by simp
   380   then have "finite {x. P x}" by simp
   381   with inf show False by simp
   382 qed
   383 
   384 lemma MOST_iff_finiteNeg: "(\<forall>\<^sub>\<infinity>x. P x) = finite {x. \<not> P x}"
   385   by (simp add: Alm_all_def Inf_many_def)
   386 
   387 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
   388   by (simp add: MOST_iff_finiteNeg)
   389 
   390 lemma INFM_mono:
   391   assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
   392   shows "\<exists>\<^sub>\<infinity>x. Q x"
   393 proof -
   394   from inf have "infinite {x. P x}" unfolding Inf_many_def .
   395   moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
   396   ultimately show ?thesis
   397     by (simp add: Inf_many_def infinite_super)
   398 qed
   399 
   400 lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
   401   unfolding Alm_all_def by (blast intro: INFM_mono)
   402 
   403 lemma INFM_disj_distrib:
   404   "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
   405   unfolding Inf_many_def by (simp add: Collect_disj_eq)
   406 
   407 lemma MOST_conj_distrib:
   408   "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
   409   unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
   410 
   411 lemma MOST_rev_mp:
   412   assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
   413   shows "\<forall>\<^sub>\<infinity>x. Q x"
   414 proof -
   415   have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
   416     using prems by (simp add: MOST_conj_distrib)
   417   thus ?thesis by (rule MOST_mono) simp
   418 qed
   419 
   420 lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
   421 unfolding Alm_all_def not_not ..
   422 
   423 lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
   424 unfolding Alm_all_def not_not ..
   425 
   426 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
   427   unfolding Inf_many_def by simp
   428 
   429 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
   430   unfolding Alm_all_def by simp
   431 
   432 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
   433   by (simp add: Inf_many_def infinite_nat_iff_unbounded)
   434 
   435 lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
   436   by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
   437 
   438 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
   439   by (simp add: Alm_all_def INFM_nat)
   440 
   441 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
   442   by (simp add: Alm_all_def INFM_nat_le)
   443 
   444 
   445 subsection "Enumeration of an Infinite Set"
   446 
   447 text {*
   448   The set's element type must be wellordered (e.g. the natural numbers).
   449 *}
   450 
   451 consts
   452   enumerate   :: "'a::wellorder set => (nat => 'a::wellorder)"
   453 primrec
   454   enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
   455   enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   456 
   457 lemma enumerate_Suc':
   458     "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   459   by simp
   460 
   461 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
   462 apply (induct n arbitrary: S)
   463  apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
   464 apply simp
   465 apply (metis Collect_def Collect_mem_eq DiffE infinite_remove)
   466 done
   467 
   468 declare enumerate_0 [simp del] enumerate_Suc [simp del]
   469 
   470 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
   471   apply (induct n arbitrary: S)
   472    apply (rule order_le_neq_trans)
   473     apply (simp add: enumerate_0 Least_le enumerate_in_set)
   474    apply (simp only: enumerate_Suc')
   475    apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
   476     apply (blast intro: sym)
   477    apply (simp add: enumerate_in_set del: Diff_iff)
   478   apply (simp add: enumerate_Suc')
   479   done
   480 
   481 lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   482   apply (erule less_Suc_induct)
   483   apply (auto intro: enumerate_step)
   484   done
   485 
   486 
   487 subsection "Miscellaneous"
   488 
   489 text {*
   490   A few trivial lemmas about sets that contain at most one element.
   491   These simplify the reasoning about deterministic automata.
   492 *}
   493 
   494 definition
   495   atmost_one :: "'a set \<Rightarrow> bool" where
   496   "atmost_one S = (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y)"
   497 
   498 lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
   499   by (simp add: atmost_one_def)
   500 
   501 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
   502   by (simp add: atmost_one_def)
   503 
   504 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
   505   by (simp add: atmost_one_def)
   506 
   507 end