src/HOL/Library/Infinite_Set.thy
author paulson
Thu Feb 01 13:41:19 2007 +0100 (2007-02-01)
changeset 22226 699385e6cb45
parent 21404 eb85850d3eb7
child 22432 1d00d26fee0d
permissions -rw-r--r--
new theorem int_infinite
     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 Main
    10 begin
    11 
    12 subsection "Infinite Sets"
    13 
    14 text {*
    15   Some elementary facts about infinite sets, mostly by Stefan Merz.
    16   Beware! Because "infinite" merely abbreviates a negation, these
    17   lemmas may not work well with @{text "blast"}.
    18 *}
    19 
    20 abbreviation
    21   infinite :: "'a set \<Rightarrow> bool" where
    22   "infinite S == \<not> finite S"
    23 
    24 text {*
    25   Infinite sets are non-empty, and if we remove some elements from an
    26   infinite set, the result is still infinite.
    27 *}
    28 
    29 lemma infinite_imp_nonempty: "infinite S ==> S \<noteq> {}"
    30   by auto
    31 
    32 lemma infinite_remove:
    33   "infinite S \<Longrightarrow> infinite (S - {a})"
    34   by simp
    35 
    36 lemma Diff_infinite_finite:
    37   assumes T: "finite T" and S: "infinite S"
    38   shows "infinite (S - T)"
    39   using T
    40 proof induct
    41   from S
    42   show "infinite (S - {})" by auto
    43 next
    44   fix T x
    45   assume ih: "infinite (S - T)"
    46   have "S - (insert x T) = (S - T) - {x}"
    47     by (rule Diff_insert)
    48   with ih
    49   show "infinite (S - (insert x T))"
    50     by (simp add: infinite_remove)
    51 qed
    52 
    53 lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
    54   by simp
    55 
    56 lemma infinite_super:
    57   assumes T: "S \<subseteq> T" and S: "infinite S"
    58   shows "infinite T"
    59 proof
    60   assume "finite T"
    61   with T have "finite S" by (simp add: finite_subset)
    62   with S show False by simp
    63 qed
    64 
    65 text {*
    66   As a concrete example, we prove that the set of natural numbers is
    67   infinite.
    68 *}
    69 
    70 lemma finite_nat_bounded:
    71   assumes S: "finite (S::nat set)"
    72   shows "\<exists>k. S \<subseteq> {..<k}"  (is "\<exists>k. ?bounded S k")
    73 using S
    74 proof induct
    75   have "?bounded {} 0" by simp
    76   then show "\<exists>k. ?bounded {} k" ..
    77 next
    78   fix S x
    79   assume "\<exists>k. ?bounded S k"
    80   then obtain k where k: "?bounded S k" ..
    81   show "\<exists>k. ?bounded (insert x S) k"
    82   proof (cases "x < k")
    83     case True
    84     with k show ?thesis by auto
    85   next
    86     case False
    87     with k have "?bounded S (Suc x)" by auto
    88     then show ?thesis by auto
    89   qed
    90 qed
    91 
    92 lemma finite_nat_iff_bounded:
    93   "finite (S::nat set) = (\<exists>k. S \<subseteq> {..<k})"  (is "?lhs = ?rhs")
    94 proof
    95   assume ?lhs
    96   then show ?rhs by (rule finite_nat_bounded)
    97 next
    98   assume ?rhs
    99   then obtain k where "S \<subseteq> {..<k}" ..
   100   then show "finite S"
   101     by (rule finite_subset) simp
   102 qed
   103 
   104 lemma finite_nat_iff_bounded_le:
   105   "finite (S::nat set) = (\<exists>k. S \<subseteq> {..k})"  (is "?lhs = ?rhs")
   106 proof
   107   assume ?lhs
   108   then obtain k where "S \<subseteq> {..<k}"
   109     by (blast dest: finite_nat_bounded)
   110   then have "S \<subseteq> {..k}" by auto
   111   then show ?rhs ..
   112 next
   113   assume ?rhs
   114   then obtain k where "S \<subseteq> {..k}" ..
   115   then show "finite S"
   116     by (rule finite_subset) simp
   117 qed
   118 
   119 lemma infinite_nat_iff_unbounded:
   120   "infinite (S::nat set) = (\<forall>m. \<exists>n. m<n \<and> n\<in>S)"
   121   (is "?lhs = ?rhs")
   122 proof
   123   assume ?lhs
   124   show ?rhs
   125   proof (rule ccontr)
   126     assume "\<not> ?rhs"
   127     then obtain m where m: "\<forall>n. m<n \<longrightarrow> n\<notin>S" by blast
   128     then have "S \<subseteq> {..m}"
   129       by (auto simp add: sym [OF linorder_not_less])
   130     with `?lhs` show False
   131       by (simp add: finite_nat_iff_bounded_le)
   132   qed
   133 next
   134   assume ?rhs
   135   show ?lhs
   136   proof
   137     assume "finite S"
   138     then obtain m where "S \<subseteq> {..m}"
   139       by (auto simp add: finite_nat_iff_bounded_le)
   140     then have "\<forall>n. m<n \<longrightarrow> n\<notin>S" by auto
   141     with `?rhs` show False by blast
   142   qed
   143 qed
   144 
   145 lemma infinite_nat_iff_unbounded_le:
   146   "infinite (S::nat set) = (\<forall>m. \<exists>n. m\<le>n \<and> n\<in>S)"
   147   (is "?lhs = ?rhs")
   148 proof
   149   assume ?lhs
   150   show ?rhs
   151   proof
   152     fix m
   153     from `?lhs` obtain n where "m<n \<and> n\<in>S"
   154       by (auto simp add: infinite_nat_iff_unbounded)
   155     then have "m\<le>n \<and> n\<in>S" by simp
   156     then show "\<exists>n. m \<le> n \<and> n \<in> S" ..
   157   qed
   158 next
   159   assume ?rhs
   160   show ?lhs
   161   proof (auto simp add: infinite_nat_iff_unbounded)
   162     fix m
   163     from `?rhs` obtain n where "Suc m \<le> n \<and> n\<in>S"
   164       by blast
   165     then have "m<n \<and> n\<in>S" by simp
   166     then show "\<exists>n. m < n \<and> n \<in> S" ..
   167   qed
   168 qed
   169 
   170 text {*
   171   For a set of natural numbers to be infinite, it is enough to know
   172   that for any number larger than some @{text k}, there is some larger
   173   number that is an element of the set.
   174 *}
   175 
   176 lemma unbounded_k_infinite:
   177   assumes k: "\<forall>m. k<m \<longrightarrow> (\<exists>n. m<n \<and> n\<in>S)"
   178   shows "infinite (S::nat set)"
   179 proof -
   180   {
   181     fix m have "\<exists>n. m<n \<and> n\<in>S"
   182     proof (cases "k<m")
   183       case True
   184       with k show ?thesis by blast
   185     next
   186       case False
   187       from k obtain n where "Suc k < n \<and> n\<in>S" by auto
   188       with False have "m<n \<and> n\<in>S" by auto
   189       then show ?thesis ..
   190     qed
   191   }
   192   then show ?thesis
   193     by (auto simp add: infinite_nat_iff_unbounded)
   194 qed
   195 
   196 lemma nat_infinite [simp]: "infinite (UNIV :: nat set)"
   197   by (auto simp add: infinite_nat_iff_unbounded)
   198 
   199 lemma nat_not_finite [elim]: "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 "inj f"
   212     and  "finite (range f)"
   213   then have "finite (UNIV::nat set)"
   214     by (auto intro: finite_imageD simp del: nat_infinite)
   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 prems 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 "INF " 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> (INF 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 INF_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 INF_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: INF_mono)
   404 
   405 lemma INF_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
   406   by (simp add: Inf_many_def infinite_nat_iff_unbounded)
   407 
   408 lemma INF_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
   409   by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
   410 
   411 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
   412   by (simp add: Alm_all_def INF_nat)
   413 
   414 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
   415   by (simp add: Alm_all_def INF_nat_le)
   416 
   417 
   418 subsection "Enumeration of an Infinite Set"
   419 
   420 text {*
   421   The set's element type must be wellordered (e.g. the natural numbers).
   422 *}
   423 
   424 consts
   425   enumerate   :: "'a::wellorder set => (nat => 'a::wellorder)"
   426 primrec
   427   enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
   428   enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   429 
   430 lemma enumerate_Suc':
   431     "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   432   by simp
   433 
   434 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
   435   apply (induct n arbitrary: S)
   436    apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
   437   apply (fastsimp iff: finite_Diff_singleton)
   438   done
   439 
   440 declare enumerate_0 [simp del] enumerate_Suc [simp del]
   441 
   442 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
   443   apply (induct n arbitrary: S)
   444    apply (rule order_le_neq_trans)
   445     apply (simp add: enumerate_0 Least_le enumerate_in_set)
   446    apply (simp only: enumerate_Suc')
   447    apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
   448     apply (blast intro: sym)
   449    apply (simp add: enumerate_in_set del: Diff_iff)
   450   apply (simp add: enumerate_Suc')
   451   done
   452 
   453 lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   454   apply (erule less_Suc_induct)
   455   apply (auto intro: enumerate_step)
   456   done
   457 
   458 
   459 subsection "Miscellaneous"
   460 
   461 text {*
   462   A few trivial lemmas about sets that contain at most one element.
   463   These simplify the reasoning about deterministic automata.
   464 *}
   465 
   466 definition
   467   atmost_one :: "'a set \<Rightarrow> bool" where
   468   "atmost_one S = (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y)"
   469 
   470 lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
   471   by (simp add: atmost_one_def)
   472 
   473 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
   474   by (simp add: atmost_one_def)
   475 
   476 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
   477   by (simp add: atmost_one_def)
   478 
   479 end