author wenzelm
Mon Dec 28 17:43:30 2015 +0100 (2015-12-28)
changeset 61952 546958347e05
parent 61945 1135b8de26c3
child 63492 a662e8139804
permissions -rw-r--r--
prefer symbols for "Union", "Inter";
     1 (*  Title:      HOL/Library/Infinite_Set.thy
     2     Author:     Stephan Merz
     3 *)
     5 section \<open>Infinite Sets and Related Concepts\<close>
     7 theory Infinite_Set
     8 imports Main
     9 begin
    11 text \<open>The set of natural numbers is infinite.\<close>
    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)
    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)
    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)
    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)
    27 lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
    28   by (simp add: finite_nat_iff_bounded)
    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>
    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
    42 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
    43   by simp
    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
    54 text \<open>The set of integers is also infinite.\<close>
    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)
    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
    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
    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)
    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)
    75 subsection "Infinitely Many and Almost All"
    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>
    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)
    87 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
    88   by (simp add: frequently_const_iff)
    90 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
    91   by (simp add: eventually_const_iff)
    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)
    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)
    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)
   102 text \<open>Properties of quantifiers with injective functions.\<close>
   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)
   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)
   110 text \<open>Properties of quantifiers with singletons.\<close>
   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
   117 lemma MOST_neq [simp]:
   118   "MOST x. x \<noteq> a"
   119   "MOST x. a \<noteq> x"
   120   unfolding eventually_cofinite by simp_all
   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
   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
   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
   137 text \<open>Properties of quantifiers over the naturals.\<close>
   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])
   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])
   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)
   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)
   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)
   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)
   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)
   162 lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
   163   by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
   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
   184 subsection "Enumeration of an Infinite Set"
   186 text \<open>
   187   The set's element type must be wellordered (e.g. the natural numbers).
   188 \<close>
   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>
   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"
   200 lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   201   by simp
   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
   210 declare enumerate_0 [simp del] enumerate_Suc [simp del]
   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
   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
   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
   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
   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
   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
   310 end