src/HOL/Library/Infinite_Set.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 61810 3c5040d5694a
child 63492 a662e8139804
permissions -rw-r--r--
more symbols;
     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 text \<open>The set of natural numbers is infinite.\<close>
    12 
    13 lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
    14   using frequently_cofinite[of "\<lambda>x. x \<in> S"]
    15   by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially)
    16 
    17 lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)"
    18   using frequently_cofinite[of "\<lambda>x. x \<in> S"]
    19   by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense)
    20 
    21 lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"
    22   using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
    23 
    24 lemma finite_nat_iff_bounded_le: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})"
    25   using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
    26 
    27 lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
    28   by (simp add: finite_nat_iff_bounded)
    29 
    30 
    31 text \<open>
    32   For a set of natural numbers to be infinite, it is enough to know
    33   that for any number larger than some \<open>k\<close>, there is some larger
    34   number that is an element of the set.
    35 \<close>
    36 
    37 lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
    38 apply (clarsimp simp add: finite_nat_set_iff_bounded)
    39 apply (drule_tac x="Suc (max m k)" in spec)
    40 using less_Suc_eq by fastforce
    41 
    42 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
    43   by simp
    44 
    45 lemma range_inj_infinite:
    46   "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
    47 proof
    48   assume "finite (range f)" and "inj f"
    49   then have "finite (UNIV::nat set)"
    50     by (rule finite_imageD)
    51   then show False by simp
    52 qed
    53 
    54 text \<open>The set of integers is also infinite.\<close>
    55 
    56 lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) \<longleftrightarrow> infinite ((nat o abs) ` S)"
    57   by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD)
    58 
    59 proposition infinite_int_iff_unbounded_le: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
    60   apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def)
    61   apply (metis abs_ge_zero nat_le_eq_zle le_nat_iff)
    62   done
    63 
    64 proposition infinite_int_iff_unbounded: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> > m \<and> n \<in> S)"
    65   apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def)
    66   apply (metis (full_types) nat_le_iff nat_mono not_le)
    67   done
    68 
    69 proposition finite_int_iff_bounded: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {..<k})"
    70   using infinite_int_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
    71 
    72 proposition finite_int_iff_bounded_le: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {.. k})"
    73   using infinite_int_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
    74 
    75 subsection "Infinitely Many and Almost All"
    76 
    77 text \<open>
    78   We often need to reason about the existence of infinitely many
    79   (resp., all but finitely many) objects satisfying some predicate, so
    80   we introduce corresponding binders and their proof rules.
    81 \<close>
    82 
    83 (* The following two lemmas are available as filter-rules, but not in the simp-set *)
    84 lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" by (fact not_frequently)
    85 lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" by (fact not_eventually)
    86 
    87 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
    88   by (simp add: frequently_const_iff)
    89 
    90 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
    91   by (simp add: eventually_const_iff)
    92 
    93 lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
    94   by (simp only: imp_conv_disj frequently_disj_iff not_eventually)
    95 
    96 lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
    97   by (auto intro: eventually_rev_mp eventually_mono)
    98 
    99 lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
   100   by (rule frequently_rev_mp[of P]) (auto elim: eventually_mono)
   101 
   102 text \<open>Properties of quantifiers with injective functions.\<close>
   103 
   104 lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
   105   using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite)
   106 
   107 lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
   108   using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite)
   109 
   110 text \<open>Properties of quantifiers with singletons.\<close>
   111 
   112 lemma not_INFM_eq [simp]:
   113   "\<not> (INFM x. x = a)"
   114   "\<not> (INFM x. a = x)"
   115   unfolding frequently_cofinite by simp_all
   116 
   117 lemma MOST_neq [simp]:
   118   "MOST x. x \<noteq> a"
   119   "MOST x. a \<noteq> x"
   120   unfolding eventually_cofinite by simp_all
   121 
   122 lemma INFM_neq [simp]:
   123   "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
   124   "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
   125   unfolding frequently_cofinite by simp_all
   126 
   127 lemma MOST_eq [simp]:
   128   "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
   129   "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
   130   unfolding eventually_cofinite by simp_all
   131 
   132 lemma MOST_eq_imp:
   133   "MOST x. x = a \<longrightarrow> P x"
   134   "MOST x. a = x \<longrightarrow> P x"
   135   unfolding eventually_cofinite by simp_all
   136 
   137 text \<open>Properties of quantifiers over the naturals.\<close>
   138 
   139 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
   140   by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
   141 
   142 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
   143   by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
   144 
   145 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
   146   by (simp add: frequently_cofinite infinite_nat_iff_unbounded)
   147 
   148 lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)"
   149   by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le)
   150 
   151 lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
   152   by (simp add: eventually_frequently)
   153 
   154 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
   155   by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc)
   156 
   157 lemma
   158   shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
   159     and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
   160   by (simp_all add: MOST_Suc_iff)
   161 
   162 lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
   163   by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
   164 
   165 (* legacy names *)
   166 lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
   167 lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
   168 lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
   169 lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite)
   170 lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
   171 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
   172 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)
   173 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_mono)
   174 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)
   175 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)
   176 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)
   177 lemma MOST_conjI: "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x" by (fact eventually_conj)
   178 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)
   179 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)
   180 lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE)
   181 lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI)
   182 lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
   183 
   184 subsection "Enumeration of an Infinite Set"
   185 
   186 text \<open>
   187   The set's element type must be wellordered (e.g. the natural numbers).
   188 \<close>
   189 
   190 text \<open>
   191   Could be generalized to
   192     @{term "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}.
   193 \<close>
   194 
   195 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
   196 where
   197   enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
   198 | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   199 
   200 lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   201   by simp
   202 
   203 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S"
   204   apply (induct n arbitrary: S)
   205    apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
   206   apply simp
   207   apply (metis DiffE infinite_remove)
   208   done
   209 
   210 declare enumerate_0 [simp del] enumerate_Suc [simp del]
   211 
   212 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
   213   apply (induct n arbitrary: S)
   214    apply (rule order_le_neq_trans)
   215     apply (simp add: enumerate_0 Least_le enumerate_in_set)
   216    apply (simp only: enumerate_Suc')
   217    apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
   218     apply (blast intro: sym)
   219    apply (simp add: enumerate_in_set del: Diff_iff)
   220   apply (simp add: enumerate_Suc')
   221   done
   222 
   223 lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   224   apply (erule less_Suc_induct)
   225   apply (auto intro: enumerate_step)
   226   done
   227 
   228 
   229 lemma le_enumerate:
   230   assumes S: "infinite S"
   231   shows "n \<le> enumerate S n"
   232   using S
   233 proof (induct n)
   234   case 0
   235   then show ?case by simp
   236 next
   237   case (Suc n)
   238   then have "n \<le> enumerate S n" by simp
   239   also note enumerate_mono[of n "Suc n", OF _ \<open>infinite S\<close>]
   240   finally show ?case by simp
   241 qed
   242 
   243 lemma enumerate_Suc'':
   244   fixes S :: "'a::wellorder set"
   245   assumes "infinite S"
   246   shows "enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
   247   using assms
   248 proof (induct n arbitrary: S)
   249   case 0
   250   then have "\<forall>s \<in> S. enumerate S 0 \<le> s"
   251     by (auto simp: enumerate.simps intro: Least_le)
   252   then show ?case
   253     unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"]
   254     by (intro arg_cong[where f = Least] ext) auto
   255 next
   256   case (Suc n S)
   257   show ?case
   258     using enumerate_mono[OF zero_less_Suc \<open>infinite S\<close>, of n] \<open>infinite S\<close>
   259     apply (subst (1 2) enumerate_Suc')
   260     apply (subst Suc)
   261     using \<open>infinite S\<close>
   262     apply simp
   263     apply (intro arg_cong[where f = Least] ext)
   264     apply (auto simp: enumerate_Suc'[symmetric])
   265     done
   266 qed
   267 
   268 lemma enumerate_Ex:
   269   assumes S: "infinite (S::nat set)"
   270   shows "s \<in> S \<Longrightarrow> \<exists>n. enumerate S n = s"
   271 proof (induct s rule: less_induct)
   272   case (less s)
   273   show ?case
   274   proof cases
   275     let ?y = "Max {s'\<in>S. s' < s}"
   276     assume "\<exists>y\<in>S. y < s"
   277     then have y: "\<And>x. ?y < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)"
   278       by (subst Max_less_iff) auto
   279     then have y_in: "?y \<in> {s'\<in>S. s' < s}"
   280       by (intro Max_in) auto
   281     with less.hyps[of ?y] obtain n where "enumerate S n = ?y"
   282       by auto
   283     with S have "enumerate S (Suc n) = s"
   284       by (auto simp: y less enumerate_Suc'' intro!: Least_equality)
   285     then show ?case by auto
   286   next
   287     assume *: "\<not> (\<exists>y\<in>S. y < s)"
   288     then have "\<forall>t\<in>S. s \<le> t" by auto
   289     with \<open>s \<in> S\<close> show ?thesis
   290       by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0)
   291   qed
   292 qed
   293 
   294 lemma bij_enumerate:
   295   fixes S :: "nat set"
   296   assumes S: "infinite S"
   297   shows "bij_betw (enumerate S) UNIV S"
   298 proof -
   299   have "\<And>n m. n \<noteq> m \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
   300     using enumerate_mono[OF _ \<open>infinite S\<close>] by (auto simp: neq_iff)
   301   then have "inj (enumerate S)"
   302     by (auto simp: inj_on_def)
   303   moreover have "\<forall>s \<in> S. \<exists>i. enumerate S i = s"
   304     using enumerate_Ex[OF S] by auto
   305   moreover note \<open>infinite S\<close>
   306   ultimately show ?thesis
   307     unfolding bij_betw_def by (auto intro: enumerate_in_set)
   308 qed
   309 
   310 end
   311