src/HOL/Library/Infinite_Set.thy
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 60040 1fa1023b13b9
child 60828 e9e272fa8daf
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/Library/Infinite_Set.thy
     2     Author:     Stephan Merz
     3 *)
     4 
     5 section \<open>Infinite Sets and Related Concepts\<close>
     6 
     7 theory Infinite_Set
     8 imports Main
     9 begin
    10 
    11 subsection "Infinite Sets"
    12 
    13 text \<open>
    14   Some elementary facts about infinite sets, mostly by Stephan Merz.
    15   Beware! Because "infinite" merely abbreviates a negation, these
    16   lemmas may not work well with @{text "blast"}.
    17 \<close>
    18 
    19 abbreviation infinite :: "'a set \<Rightarrow> bool"
    20   where "infinite S \<equiv> \<not> finite S"
    21 
    22 text \<open>
    23   Infinite sets are non-empty, and if we remove some elements from an
    24   infinite set, the result is still infinite.
    25 \<close>
    26 
    27 lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}"
    28   by auto
    29 
    30 lemma infinite_remove: "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: "infinite S \<Longrightarrow> infinite (S \<union> T)"
    51   by simp
    52 
    53 lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite 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 \<open>
    66   As a concrete example, we prove that the set of natural numbers is
    67   infinite.
    68 \<close>
    69 
    70 lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
    71   using frequently_cofinite[of "\<lambda>x. x \<in> S"]
    72   by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially)
    73 
    74 lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)"
    75   using frequently_cofinite[of "\<lambda>x. x \<in> S"]
    76   by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense)
    77 
    78 lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"
    79   using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
    80 
    81 lemma finite_nat_iff_bounded_le: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})"
    82   using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
    83 
    84 lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
    85   by (simp add: finite_nat_iff_bounded)
    86 
    87 text \<open>
    88   For a set of natural numbers to be infinite, it is enough to know
    89   that for any number larger than some @{text k}, there is some larger
    90   number that is an element of the set.
    91 \<close>
    92 
    93 lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
    94   by (metis (full_types) infinite_nat_iff_unbounded_le le_imp_less_Suc not_less
    95             not_less_iff_gr_or_eq sup.bounded_iff)
    96 
    97 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
    98   by simp
    99 
   100 lemma range_inj_infinite:
   101   "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
   102 proof
   103   assume "finite (range f)" and "inj f"
   104   then have "finite (UNIV::nat set)"
   105     by (rule finite_imageD)
   106   then show False by simp
   107 qed
   108 
   109 text \<open>
   110   For any function with infinite domain and finite range there is some
   111   element that is the image of infinitely many domain elements.  In
   112   particular, any infinite sequence of elements from a finite set
   113   contains some element that occurs infinitely often.
   114 \<close>
   115 
   116 lemma inf_img_fin_dom':
   117   assumes img: "finite (f ` A)" and dom: "infinite A"
   118   shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)"
   119 proof (rule ccontr)
   120   have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto
   121   moreover
   122   assume "\<not> ?thesis"
   123   with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast
   124   ultimately have "finite A" by(rule finite_subset)
   125   with dom show False by contradiction
   126 qed
   127 
   128 lemma inf_img_fin_domE':
   129   assumes "finite (f ` A)" and "infinite A"
   130   obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)"
   131   using assms by (blast dest: inf_img_fin_dom')
   132 
   133 lemma inf_img_fin_dom:
   134   assumes img: "finite (f`A)" and dom: "infinite A"
   135   shows "\<exists>y \<in> f`A. infinite (f -` {y})"
   136 using inf_img_fin_dom'[OF assms] by auto
   137 
   138 lemma inf_img_fin_domE:
   139   assumes "finite (f`A)" and "infinite A"
   140   obtains y where "y \<in> f`A" and "infinite (f -` {y})"
   141   using assms by (blast dest: inf_img_fin_dom)
   142 
   143 subsection "Infinitely Many and Almost All"
   144 
   145 text \<open>
   146   We often need to reason about the existence of infinitely many
   147   (resp., all but finitely many) objects satisfying some predicate, so
   148   we introduce corresponding binders and their proof rules.
   149 \<close>
   150 
   151 (* The following two lemmas are available as filter-rules, but not in the simp-set *)
   152 lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" by (fact not_frequently)
   153 lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" by (fact not_eventually)
   154 
   155 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
   156   by (simp add: frequently_const_iff)
   157 
   158 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
   159   by (simp add: eventually_const_iff)
   160 
   161 lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
   162   by (simp only: imp_conv_disj frequently_disj_iff not_eventually)
   163 
   164 lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
   165   by (auto intro: eventually_rev_mp eventually_elim1)
   166 
   167 lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
   168   by (rule frequently_rev_mp[of P]) (auto elim: eventually_elim1)
   169 
   170 text \<open>Properties of quantifiers with injective functions.\<close>
   171 
   172 lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
   173   using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite)
   174 
   175 lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
   176   using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite)
   177 
   178 text \<open>Properties of quantifiers with singletons.\<close>
   179 
   180 lemma not_INFM_eq [simp]:
   181   "\<not> (INFM x. x = a)"
   182   "\<not> (INFM x. a = x)"
   183   unfolding frequently_cofinite by simp_all
   184 
   185 lemma MOST_neq [simp]:
   186   "MOST x. x \<noteq> a"
   187   "MOST x. a \<noteq> x"
   188   unfolding eventually_cofinite by simp_all
   189 
   190 lemma INFM_neq [simp]:
   191   "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
   192   "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
   193   unfolding frequently_cofinite by simp_all
   194 
   195 lemma MOST_eq [simp]:
   196   "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
   197   "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
   198   unfolding eventually_cofinite by simp_all
   199 
   200 lemma MOST_eq_imp:
   201   "MOST x. x = a \<longrightarrow> P x"
   202   "MOST x. a = x \<longrightarrow> P x"
   203   unfolding eventually_cofinite by simp_all
   204 
   205 text \<open>Properties of quantifiers over the naturals.\<close>
   206 
   207 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
   208   by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
   209 
   210 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
   211   by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
   212 
   213 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
   214   by (simp add: frequently_cofinite infinite_nat_iff_unbounded)
   215 
   216 lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)"
   217   by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le)
   218 
   219 lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
   220   by (simp add: eventually_frequently)
   221 
   222 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
   223   by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc)
   224 
   225 lemma
   226   shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
   227     and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
   228   by (simp_all add: MOST_Suc_iff)
   229 
   230 lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
   231   by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
   232 
   233 (* legacy names *)
   234 lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
   235 lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
   236 lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
   237 lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite)
   238 lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
   239 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
   240 lemma INFM_mono: "\<exists>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<exists>\<^sub>\<infinity>x. Q x" by (fact frequently_elim1)
   241 lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_elim1)
   242 lemma INFM_disj_distrib: "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)" by (fact frequently_disj_iff)
   243 lemma MOST_rev_mp: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_rev_mp)
   244 lemma MOST_conj_distrib: "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)" by (fact eventually_conj_iff)
   245 lemma MOST_conjI: "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x" by (fact eventually_conj)
   246 lemma INFM_finite_Bex_distrib: "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)" by (fact frequently_bex_finite_distrib)
   247 lemma MOST_finite_Ball_distrib: "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)" by (fact eventually_ball_finite_distrib)
   248 lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE)
   249 lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI)
   250 lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
   251 
   252 subsection "Enumeration of an Infinite Set"
   253 
   254 text \<open>
   255   The set's element type must be wellordered (e.g. the natural numbers).
   256 \<close>
   257 
   258 text \<open>
   259   Could be generalized to
   260     @{term "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}.
   261 \<close>
   262 
   263 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
   264 where
   265   enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
   266 | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   267 
   268 lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   269   by simp
   270 
   271 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S"
   272   apply (induct n arbitrary: S)
   273    apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
   274   apply simp
   275   apply (metis DiffE infinite_remove)
   276   done
   277 
   278 declare enumerate_0 [simp del] enumerate_Suc [simp del]
   279 
   280 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
   281   apply (induct n arbitrary: S)
   282    apply (rule order_le_neq_trans)
   283     apply (simp add: enumerate_0 Least_le enumerate_in_set)
   284    apply (simp only: enumerate_Suc')
   285    apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
   286     apply (blast intro: sym)
   287    apply (simp add: enumerate_in_set del: Diff_iff)
   288   apply (simp add: enumerate_Suc')
   289   done
   290 
   291 lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   292   apply (erule less_Suc_induct)
   293   apply (auto intro: enumerate_step)
   294   done
   295 
   296 
   297 lemma le_enumerate:
   298   assumes S: "infinite S"
   299   shows "n \<le> enumerate S n"
   300   using S 
   301 proof (induct n)
   302   case 0
   303   then show ?case by simp
   304 next
   305   case (Suc n)
   306   then have "n \<le> enumerate S n" by simp
   307   also note enumerate_mono[of n "Suc n", OF _ \<open>infinite S\<close>]
   308   finally show ?case by simp
   309 qed
   310 
   311 lemma enumerate_Suc'':
   312   fixes S :: "'a::wellorder set"
   313   assumes "infinite S"
   314   shows "enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
   315   using assms
   316 proof (induct n arbitrary: S)
   317   case 0
   318   then have "\<forall>s \<in> S. enumerate S 0 \<le> s"
   319     by (auto simp: enumerate.simps intro: Least_le)
   320   then show ?case
   321     unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"]
   322     by (intro arg_cong[where f = Least] ext) auto
   323 next
   324   case (Suc n S)
   325   show ?case
   326     using enumerate_mono[OF zero_less_Suc \<open>infinite S\<close>, of n] \<open>infinite S\<close>
   327     apply (subst (1 2) enumerate_Suc')
   328     apply (subst Suc)
   329     using \<open>infinite S\<close>
   330     apply simp
   331     apply (intro arg_cong[where f = Least] ext)
   332     apply (auto simp: enumerate_Suc'[symmetric])
   333     done
   334 qed
   335 
   336 lemma enumerate_Ex:
   337   assumes S: "infinite (S::nat set)"
   338   shows "s \<in> S \<Longrightarrow> \<exists>n. enumerate S n = s"
   339 proof (induct s rule: less_induct)
   340   case (less s)
   341   show ?case
   342   proof cases
   343     let ?y = "Max {s'\<in>S. s' < s}"
   344     assume "\<exists>y\<in>S. y < s"
   345     then have y: "\<And>x. ?y < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)"
   346       by (subst Max_less_iff) auto
   347     then have y_in: "?y \<in> {s'\<in>S. s' < s}"
   348       by (intro Max_in) auto
   349     with less.hyps[of ?y] obtain n where "enumerate S n = ?y"
   350       by auto
   351     with S have "enumerate S (Suc n) = s"
   352       by (auto simp: y less enumerate_Suc'' intro!: Least_equality)
   353     then show ?case by auto
   354   next
   355     assume *: "\<not> (\<exists>y\<in>S. y < s)"
   356     then have "\<forall>t\<in>S. s \<le> t" by auto
   357     with \<open>s \<in> S\<close> show ?thesis
   358       by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0)
   359   qed
   360 qed
   361 
   362 lemma bij_enumerate:
   363   fixes S :: "nat set"
   364   assumes S: "infinite S"
   365   shows "bij_betw (enumerate S) UNIV S"
   366 proof -
   367   have "\<And>n m. n \<noteq> m \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
   368     using enumerate_mono[OF _ \<open>infinite S\<close>] by (auto simp: neq_iff)
   369   then have "inj (enumerate S)"
   370     by (auto simp: inj_on_def)
   371   moreover have "\<forall>s \<in> S. \<exists>i. enumerate S i = s"
   372     using enumerate_Ex[OF S] by auto
   373   moreover note \<open>infinite S\<close>
   374   ultimately show ?thesis
   375     unfolding bij_betw_def by (auto intro: enumerate_in_set)
   376 qed
   377 
   378 subsection "Miscellaneous"
   379 
   380 text \<open>
   381   A few trivial lemmas about sets that contain at most one element.
   382   These simplify the reasoning about deterministic automata.
   383 \<close>
   384 
   385 definition atmost_one :: "'a set \<Rightarrow> bool"
   386   where "atmost_one S \<longleftrightarrow> (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x = y)"
   387 
   388 lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
   389   by (simp add: atmost_one_def)
   390 
   391 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
   392   by (simp add: atmost_one_def)
   393 
   394 lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
   395   by (simp add: atmost_one_def)
   396 
   397 end
   398