src/HOL/Infinite_Set.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 15140 322485b816ac
child 16733 236dfafbeb63
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:      HOL/Infnite_Set.thy
     2     ID:         $Id$
     3     Author:     Stephan Merz 
     4 *)
     5 
     6 header {* Infnite Sets and Related Concepts*}
     7 
     8 theory Infinite_Set
     9 imports Hilbert_Choice Finite_Set SetInterval
    10 begin
    11 
    12 subsection "Infinite Sets"
    13 
    14 text {* Some elementary facts about infinite sets, by Stefan Merz. *}
    15 
    16 syntax
    17   infinite :: "'a set \<Rightarrow> bool"
    18 translations
    19   "infinite S" == "S \<notin> Finites"
    20 
    21 text {*
    22   Infinite sets are non-empty, and if we remove some elements
    23   from an infinite set, the result is still infinite.
    24 *}
    25 
    26 lemma infinite_nonempty:
    27   "\<not> (infinite {})"
    28 by simp
    29 
    30 lemma infinite_remove:
    31   "infinite S \<Longrightarrow> infinite (S - {a})"
    32 by simp
    33 
    34 lemma Diff_infinite_finite:
    35   assumes T: "finite T" and S: "infinite S"
    36   shows "infinite (S-T)"
    37 using T
    38 proof (induct)
    39   from S
    40   show "infinite (S - {})" by auto
    41 next
    42   fix T x
    43   assume ih: "infinite (S-T)"
    44   have "S - (insert x T) = (S-T) - {x}"
    45     by (rule Diff_insert)
    46   with ih
    47   show "infinite (S - (insert x T))"
    48     by (simp add: infinite_remove)
    49 qed
    50 
    51 lemma Un_infinite:
    52   "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 (rule ccontr)
    59   assume "\<not>(infinite T)"
    60   with T
    61   have "finite S" by (simp add: finite_subset)
    62   with S
    63   show False by simp
    64 qed
    65 
    66 text {*
    67   As a concrete example, we prove that the set of natural
    68   numbers is 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   thus "\<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     thus ?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   thus ?rhs by (rule finite_nat_bounded)
    98 next
    99   assume ?rhs
   100   then obtain k where "S \<subseteq> {..<k}" ..
   101   thus "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   hence "S \<subseteq> {..k}" by auto
   112   thus ?rhs ..
   113 next
   114   assume ?rhs
   115   then obtain k where "S \<subseteq> {..k}" ..
   116   thus "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 inf: ?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     hence "S \<subseteq> {..m}"
   130       by (auto simp add: sym[OF not_less_iff_le])
   131     with inf show "False" 
   132       by (simp add: finite_nat_iff_bounded_le)
   133   qed
   134 next
   135   assume unbounded: ?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     hence "\<forall>n. m<n \<longrightarrow> n\<notin>S" by auto
   142     with unbounded 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 inf: ?lhs
   151   show ?rhs
   152   proof
   153     fix m
   154     from inf obtain n where "m<n \<and> n\<in>S"
   155       by (auto simp add: infinite_nat_iff_unbounded)
   156     hence "m\<le>n \<and> n\<in>S" by auto
   157     thus "\<exists>n. m \<le> n \<and> n \<in> S" ..
   158   qed
   159 next
   160   assume unbounded: ?rhs
   161   show ?lhs
   162   proof (auto simp add: infinite_nat_iff_unbounded)
   163     fix m
   164     from unbounded obtain n where "(Suc m)\<le>n \<and> n\<in>S"
   165       by blast
   166     hence "m<n \<and> n\<in>S" by auto
   167     thus "\<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
   173   to know that for any number larger than some @{text k}, there
   174   is some larger 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 (auto simp add: infinite_nat_iff_unbounded)
   181   fix m show "\<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     thus ?thesis ..
   190   qed
   191 qed
   192 
   193 theorem nat_infinite [simp]:
   194   "infinite (UNIV :: nat set)"
   195 by (auto simp add: infinite_nat_iff_unbounded)
   196 
   197 theorem nat_not_finite [elim]:
   198   "finite (UNIV::nat set) \<Longrightarrow> R"
   199 by simp
   200 
   201 text {*
   202   Every infinite set contains a countable subset. More precisely
   203   we show that a set @{text S} is infinite if and only if there exists 
   204   an 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 "inj f"
   211     and  "finite (range f)"
   212   hence "finite (UNIV::nat set)"
   213     by (auto intro: finite_imageD simp del: nat_infinite)
   214   thus "False" by simp
   215 qed
   216 
   217 text {*
   218   The ``only if'' direction is harder because it requires the
   219   construction of a sequence of pairwise different elements of
   220   an infinite set @{text S}. The idea is to construct a sequence of
   221   non-empty and infinite subsets of @{text S} obtained by successively
   222   removing elements of @{text S}.
   223 *}
   224 
   225 lemma linorder_injI:
   226   assumes hyp: "\<forall>x y. x < (y::'a::linorder) \<longrightarrow> f x \<noteq> f y"
   227   shows "inj f"
   228 proof (rule inj_onI)
   229   fix x y
   230   assume f_eq: "f x = f y"
   231   show "x = y"
   232   proof (rule linorder_cases)
   233     assume "x < y"
   234     with hyp have "f x \<noteq> f y" by blast
   235     with f_eq show ?thesis by simp
   236   next
   237     assume "x = y"
   238     thus ?thesis .
   239   next
   240     assume "y < x"
   241     with hyp have "f y \<noteq> f x" by blast
   242     with f_eq show ?thesis by simp
   243   qed
   244 qed
   245 
   246 lemma infinite_countable_subset:
   247   assumes inf: "infinite (S::'a set)"
   248   shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
   249 proof -
   250   def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
   251   def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   252   have Sseq_inf: "\<And>n. infinite (Sseq n)"
   253   proof -
   254     fix n
   255     show "infinite (Sseq n)"
   256     proof (induct n)
   257       from inf show "infinite (Sseq 0)"
   258 	by (simp add: Sseq_def)
   259     next
   260       fix n
   261       assume "infinite (Sseq n)" thus "infinite (Sseq (Suc n))"
   262 	by (simp add: Sseq_def infinite_remove)
   263     qed
   264   qed
   265   have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
   266   proof -
   267     fix n
   268     show "Sseq n \<subseteq> S"
   269       by (induct n, auto simp add: Sseq_def)
   270   qed
   271   have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
   272   proof -
   273     fix n
   274     show "pick n \<in> Sseq n"
   275     proof (unfold pick_def, rule someI_ex)
   276       from Sseq_inf have "infinite (Sseq n)" .
   277       hence "Sseq n \<noteq> {}" by auto
   278       thus "\<exists>x. x \<in> Sseq n" by auto
   279     qed
   280   qed
   281   with Sseq_S have rng: "range pick \<subseteq> S"
   282     by auto
   283   have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
   284   proof -
   285     fix n m
   286     show "pick n \<notin> Sseq (n + Suc m)"
   287       by (induct m, auto simp add: Sseq_def pick_def)
   288   qed
   289   have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
   290   proof -
   291     fix n m
   292     from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
   293     moreover from pick_Sseq_gt
   294     have "pick n \<notin> Sseq (n + Suc m)" .
   295     ultimately show "pick n \<noteq> pick (n + Suc m)"
   296       by auto
   297   qed
   298   have inj: "inj pick"
   299   proof (rule linorder_injI)
   300     show "\<forall>i j. i<(j::nat) \<longrightarrow> pick i \<noteq> pick j"
   301     proof (clarify)
   302       fix i j
   303       assume ij: "i<(j::nat)"
   304 	and eq: "pick i = pick j"
   305       from ij obtain k where "j = i + (Suc k)"
   306 	by (auto simp add: less_iff_Suc_add)
   307       with pick_pick have "pick i \<noteq> pick j" by simp
   308       with eq show "False" by simp
   309     qed
   310   qed
   311   from rng inj show ?thesis by auto
   312 qed
   313 
   314 theorem infinite_iff_countable_subset:
   315   "infinite S = (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
   316   (is "?lhs = ?rhs")
   317 by (auto simp add: infinite_countable_subset
   318                    range_inj_infinite infinite_super)
   319 
   320 text {*
   321   For any function with infinite domain and finite range
   322   there is some element that is the image of infinitely
   323   many domain elements. In particular, any infinite sequence
   324   of elements from a finite set contains some element that
   325   occurs infinitely often.
   326 *}
   327 
   328 theorem inf_img_fin_dom:
   329   assumes img: "finite (f`A)" and dom: "infinite A"
   330   shows "\<exists>y \<in> f`A. infinite (f -` {y})"
   331 proof (rule ccontr)
   332   assume "\<not> (\<exists>y\<in>f ` A. infinite (f -` {y}))"
   333   with img have "finite (UN y:f`A. f -` {y})"
   334     by (blast intro: finite_UN_I)
   335   moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
   336   moreover note dom
   337   ultimately show "False"
   338     by (simp add: infinite_super)
   339 qed
   340 
   341 theorems inf_img_fin_domE = inf_img_fin_dom[THEN bexE]
   342 
   343 
   344 subsection "Infinitely Many and Almost All"
   345 
   346 text {*
   347   We often need to reason about the existence of infinitely many
   348   (resp., all but finitely many) objects satisfying some predicate,
   349   so we introduce corresponding binders and their proof rules.
   350 *}
   351 
   352 consts
   353   Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "INF " 10)
   354   Alm_all  :: "('a \<Rightarrow> bool) \<Rightarrow> bool"      (binder "MOST " 10)
   355 
   356 defs
   357   INF_def:  "Inf_many P \<equiv> infinite {x. P x}"
   358   MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)"
   359 
   360 syntax (xsymbols)
   361   "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
   362   "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
   363 
   364 syntax (HTML output)
   365   "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
   366   "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
   367 
   368 lemma INF_EX:
   369   "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
   370 proof (unfold INF_def, rule ccontr)
   371   assume inf: "infinite {x. P x}"
   372     and notP: "\<not>(\<exists>x. P x)"
   373   from notP have "{x. P x} = {}" by simp
   374   hence "finite {x. P x}" by simp
   375   with inf show "False" by simp
   376 qed
   377 
   378 lemma MOST_iff_finiteNeg:
   379   "(\<forall>\<^sub>\<infinity>x. P x) = finite {x. \<not> P x}"
   380 by (simp add: MOST_def INF_def)
   381 
   382 lemma ALL_MOST:
   383   "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
   384 by (simp add: MOST_iff_finiteNeg)
   385 
   386 lemma INF_mono:
   387   assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
   388   shows "\<exists>\<^sub>\<infinity>x. Q x"
   389 proof -
   390   from inf have "infinite {x. P x}" by (unfold INF_def)
   391   moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
   392   ultimately show ?thesis
   393     by (simp add: INF_def infinite_super)
   394 qed
   395 
   396 lemma MOST_mono:
   397   "\<lbrakk> \<forall>\<^sub>\<infinity>x. P x; \<And>x. P x \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
   398 by (unfold MOST_def, blast intro: INF_mono)
   399 
   400 lemma INF_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
   401 by (simp add: INF_def infinite_nat_iff_unbounded)
   402 
   403 lemma INF_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)"
   404 by (simp add: INF_def infinite_nat_iff_unbounded_le)
   405 
   406 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)"
   407 by (simp add: MOST_def INF_nat)
   408 
   409 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)"
   410 by (simp add: MOST_def INF_nat_le)
   411 
   412 
   413 subsection "Miscellaneous"
   414 
   415 text {*
   416   A few trivial lemmas about sets that contain at most one element.
   417   These simplify the reasoning about deterministic automata.
   418 *}
   419 
   420 constdefs
   421   atmost_one :: "'a set \<Rightarrow> bool"
   422   "atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y"
   423 
   424 lemma atmost_one_empty: "S={} \<Longrightarrow> atmost_one S"
   425 by (simp add: atmost_one_def)
   426 
   427 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
   428 by (simp add: atmost_one_def)
   429 
   430 lemma atmost_one_unique [elim]: "\<lbrakk> atmost_one S; x \<in> S; y \<in> S \<rbrakk> \<Longrightarrow> y=x"
   431 by (simp add: atmost_one_def)
   432 
   433 end