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