author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 64967 1ab49aa7f3c0
child 66837 6ba663ff2b1c
permissions -rw-r--r--
tuned proofs;
     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 subsection \<open>The set of natural numbers is infinite\<close>
    13 lemma infinite_nat_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
    14   for S :: "nat set"
    15   using frequently_cofinite[of "\<lambda>x. x \<in> S"]
    16   by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially)
    18 lemma infinite_nat_iff_unbounded: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)"
    19   for S :: "nat set"
    20   using frequently_cofinite[of "\<lambda>x. x \<in> S"]
    21   by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense)
    23 lemma finite_nat_iff_bounded: "finite S \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"
    24   for S :: "nat set"
    25   using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
    27 lemma finite_nat_iff_bounded_le: "finite S \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})"
    28   for S :: "nat set"
    29   using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
    31 lemma finite_nat_bounded: "finite S \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
    32   for S :: "nat set"
    33   by (simp add: finite_nat_iff_bounded)
    36 text \<open>
    37   For a set of natural numbers to be infinite, it is enough to know
    38   that for any number larger than some \<open>k\<close>, there is some larger
    39   number that is an element of the set.
    40 \<close>
    42 lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
    43   apply (clarsimp simp add: finite_nat_set_iff_bounded)
    44   apply (drule_tac x="Suc (max m k)" in spec)
    45   using less_Suc_eq apply fastforce
    46   done
    48 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
    49   by simp
    51 lemma range_inj_infinite:
    52   fixes f :: "nat \<Rightarrow> 'a"
    53   assumes "inj f"
    54   shows "infinite (range f)"
    55 proof
    56   assume "finite (range f)"
    57   from this assms have "finite (UNIV::nat set)"
    58     by (rule finite_imageD)
    59   then show False by simp
    60 qed
    63 subsection \<open>The set of integers is also infinite\<close>
    65 lemma infinite_int_iff_infinite_nat_abs: "infinite S \<longleftrightarrow> infinite ((nat \<circ> abs) ` S)"
    66   for S :: "int set"
    67   by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD)
    69 proposition infinite_int_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
    70   for S :: "int set"
    71   by (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def)
    72     (metis abs_ge_zero nat_le_eq_zle le_nat_iff)
    74 proposition infinite_int_iff_unbounded: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> > m \<and> n \<in> S)"
    75   for S :: "int set"
    76   by (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def)
    77     (metis (full_types) nat_le_iff nat_mono not_le)
    79 proposition finite_int_iff_bounded: "finite S \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {..<k})"
    80   for S :: "int set"
    81   using infinite_int_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
    83 proposition finite_int_iff_bounded_le: "finite S \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {.. k})"
    84   for S :: "int set"
    85   using infinite_int_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
    88 subsection \<open>Infinitely Many and Almost All\<close>
    90 text \<open>
    91   We often need to reason about the existence of infinitely many
    92   (resp., all but finitely many) objects satisfying some predicate, so
    93   we introduce corresponding binders and their proof rules.
    94 \<close>
    96 lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
    97   by (rule not_frequently)
    99 lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
   100   by (rule not_eventually)
   102 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
   103   by (simp add: frequently_const_iff)
   105 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
   106   by (simp add: eventually_const_iff)
   108 lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
   109   by (rule frequently_imp_iff)
   111 lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
   112   by (auto intro: eventually_rev_mp eventually_mono)
   114 lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
   115   by (rule frequently_rev_mp[of P]) (auto elim: eventually_mono)
   118 text \<open>Properties of quantifiers with injective functions.\<close>
   120 lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
   121   using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite)
   123 lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
   124   using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite)
   127 text \<open>Properties of quantifiers with singletons.\<close>
   129 lemma not_INFM_eq [simp]:
   130   "\<not> (INFM x. x = a)"
   131   "\<not> (INFM x. a = x)"
   132   unfolding frequently_cofinite by simp_all
   134 lemma MOST_neq [simp]:
   135   "MOST x. x \<noteq> a"
   136   "MOST x. a \<noteq> x"
   137   unfolding eventually_cofinite by simp_all
   139 lemma INFM_neq [simp]:
   140   "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
   141   "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
   142   unfolding frequently_cofinite by simp_all
   144 lemma MOST_eq [simp]:
   145   "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
   146   "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
   147   unfolding eventually_cofinite by simp_all
   149 lemma MOST_eq_imp:
   150   "MOST x. x = a \<longrightarrow> P x"
   151   "MOST x. a = x \<longrightarrow> P x"
   152   unfolding eventually_cofinite by simp_all
   155 text \<open>Properties of quantifiers over the naturals.\<close>
   157 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
   158   for P :: "nat \<Rightarrow> bool"
   159   by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
   161 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
   162   for P :: "nat \<Rightarrow> bool"
   163   by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
   165 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
   166   for P :: "nat \<Rightarrow> bool"
   167   by (simp add: frequently_cofinite infinite_nat_iff_unbounded)
   169 lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)"
   170   for P :: "nat \<Rightarrow> bool"
   171   by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le)
   173 lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
   174   by (simp add: eventually_frequently)
   176 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
   177   by (simp add: cofinite_eq_sequentially)
   179 lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
   180   and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
   181   by (simp_all add: MOST_Suc_iff)
   183 lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
   184   by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
   186 (* legacy names *)
   187 lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
   188 lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
   189 lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
   190 lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite)
   191 lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
   192 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
   193 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)
   194 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)
   195 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)
   196 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)
   197 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)
   198 lemma MOST_conjI: "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x" by (fact eventually_conj)
   199 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)
   200 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)
   201 lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE)
   202 lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI)
   203 lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
   206 subsection \<open>Enumeration of an Infinite Set\<close>
   208 text \<open>The set's element type must be wellordered (e.g. the natural numbers).\<close>
   210 text \<open>
   211   Could be generalized to
   212     @{prop "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}.
   213 \<close>
   215 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
   216   where
   217     enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
   218   | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   220 lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   221   by simp
   223 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S"
   224 proof (induct n arbitrary: S)
   225   case 0
   226   then show ?case
   227     by (fastforce intro: LeastI dest!: infinite_imp_nonempty)
   228 next
   229   case (Suc n)
   230   then show ?case
   231     by simp (metis DiffE infinite_remove)
   232 qed
   234 declare enumerate_0 [simp del] enumerate_Suc [simp del]
   236 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
   237   apply (induct n arbitrary: S)
   238    apply (rule order_le_neq_trans)
   239     apply (simp add: enumerate_0 Least_le enumerate_in_set)
   240    apply (simp only: enumerate_Suc')
   241    apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
   242     apply (blast intro: sym)
   243    apply (simp add: enumerate_in_set del: Diff_iff)
   244   apply (simp add: enumerate_Suc')
   245   done
   247 lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   248   by (induct m n rule: less_Suc_induct) (auto intro: enumerate_step)
   250 lemma le_enumerate:
   251   assumes S: "infinite S"
   252   shows "n \<le> enumerate S n"
   253   using S
   254 proof (induct n)
   255   case 0
   256   then show ?case by simp
   257 next
   258   case (Suc n)
   259   then have "n \<le> enumerate S n" by simp
   260   also note enumerate_mono[of n "Suc n", OF _ \<open>infinite S\<close>]
   261   finally show ?case by simp
   262 qed
   264 lemma enumerate_Suc'':
   265   fixes S :: "'a::wellorder set"
   266   assumes "infinite S"
   267   shows "enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
   268   using assms
   269 proof (induct n arbitrary: S)
   270   case 0
   271   then have "\<forall>s \<in> S. enumerate S 0 \<le> s"
   272     by (auto simp: enumerate.simps intro: Least_le)
   273   then show ?case
   274     unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"]
   275     by (intro arg_cong[where f = Least] ext) auto
   276 next
   277   case (Suc n S)
   278   show ?case
   279     using enumerate_mono[OF zero_less_Suc \<open>infinite S\<close>, of n] \<open>infinite S\<close>
   280     apply (subst (1 2) enumerate_Suc')
   281     apply (subst Suc)
   282      apply (use \<open>infinite S\<close> in simp)
   283     apply (intro arg_cong[where f = Least] ext)
   284     apply (auto simp: enumerate_Suc'[symmetric])
   285     done
   286 qed
   288 lemma enumerate_Ex:
   289   fixes S :: "nat set"
   290   assumes S: "infinite S"
   291     and s: "s \<in> S"
   292   shows "\<exists>n. enumerate S n = s"
   293   using s
   294 proof (induct s rule: less_induct)
   295   case (less s)
   296   show ?case
   297   proof (cases "\<exists>y\<in>S. y < s")
   298     case True
   299     let ?y = "Max {s'\<in>S. s' < s}"
   300     from True have y: "\<And>x. ?y < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)"
   301       by (subst Max_less_iff) auto
   302     then have y_in: "?y \<in> {s'\<in>S. s' < s}"
   303       by (intro Max_in) auto
   304     with less.hyps[of ?y] obtain n where "enumerate S n = ?y"
   305       by auto
   306     with S have "enumerate S (Suc n) = s"
   307       by (auto simp: y less enumerate_Suc'' intro!: Least_equality)
   308     then show ?thesis by auto
   309   next
   310     case False
   311     then have "\<forall>t\<in>S. s \<le> t" by auto
   312     with \<open>s \<in> S\<close> show ?thesis
   313       by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0)
   314   qed
   315 qed
   317 lemma bij_enumerate:
   318   fixes S :: "nat set"
   319   assumes S: "infinite S"
   320   shows "bij_betw (enumerate S) UNIV S"
   321 proof -
   322   have "\<And>n m. n \<noteq> m \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
   323     using enumerate_mono[OF _ \<open>infinite S\<close>] by (auto simp: neq_iff)
   324   then have "inj (enumerate S)"
   325     by (auto simp: inj_on_def)
   326   moreover have "\<forall>s \<in> S. \<exists>i. enumerate S i = s"
   327     using enumerate_Ex[OF S] by auto
   328   moreover note \<open>infinite S\<close>
   329   ultimately show ?thesis
   330     unfolding bij_betw_def by (auto intro: enumerate_in_set)
   331 qed
   333 text \<open>A pair of weird and wonderful lemmas from HOL Light.\<close>
   334 lemma finite_transitivity_chain:
   335   assumes "finite A"
   336     and R: "\<And>x. \<not> R x x" "\<And>x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z"
   337     and A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> A \<and> R x y"
   338   shows "A = {}"
   339   using \<open>finite A\<close> A
   340 proof (induct A)
   341   case empty
   342   then show ?case by simp
   343 next
   344   case (insert a A)
   345   with R show ?case
   346     by (metis empty_iff insert_iff)   (* somewhat slow *)
   347 qed
   349 corollary Union_maximal_sets:
   350   assumes "finite \<F>"
   351   shows "\<Union>{T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} = \<Union>\<F>"
   352     (is "?lhs = ?rhs")
   353 proof
   354   show "?lhs \<subseteq> ?rhs" by force
   355   show "?rhs \<subseteq> ?lhs"
   356   proof (rule Union_subsetI)
   357     fix S
   358     assume "S \<in> \<F>"
   359     have "{T \<in> \<F>. S \<subseteq> T} = {}"
   360       if "\<not> (\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y)"
   361       apply (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"])
   362          apply (use assms that in auto)
   363       apply (blast intro: dual_order.trans psubset_imp_subset)
   364       done
   365     with \<open>S \<in> \<F>\<close> show "\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y"
   366       by blast
   367   qed
   368 qed
   370 end