src/HOL/Library/Infinite_Set.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 68406 6beb45f6cf67
child 69516 09bb8f470959
permissions -rw-r--r--
tuned equation
     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 \<open>The set of natural numbers is infinite\<close>
    12 
    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)
    17 
    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)
    22 
    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)
    26 
    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)
    30 
    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)
    34 
    35 
    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>
    41 
    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
    47 
    48 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
    49   by simp
    50 
    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
    61 
    62 
    63 subsection \<open>The set of integers is also infinite\<close>
    64 
    65 lemma infinite_int_iff_infinite_nat_abs: "infinite S \<longleftrightarrow> infinite ((nat \<circ> abs) ` S)"
    66   for S :: "int set"
    67 proof -
    68   have "inj_on nat (abs ` A)" for A
    69     by (rule inj_onI) auto
    70   then show ?thesis
    71     by (auto simp flip: image_comp dest: finite_image_absD finite_imageD)
    72 qed
    73 
    74 proposition infinite_int_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
    75   for S :: "int set"
    76   by (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def)
    77     (metis abs_ge_zero nat_le_eq_zle le_nat_iff)
    78 
    79 proposition infinite_int_iff_unbounded: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> > m \<and> n \<in> S)"
    80   for S :: "int set"
    81   by (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def)
    82     (metis (full_types) nat_le_iff nat_mono not_le)
    83 
    84 proposition finite_int_iff_bounded: "finite S \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {..<k})"
    85   for S :: "int set"
    86   using infinite_int_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
    87 
    88 proposition finite_int_iff_bounded_le: "finite S \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {.. k})"
    89   for S :: "int set"
    90   using infinite_int_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
    91 
    92 
    93 subsection \<open>Infinitely Many and Almost All\<close>
    94 
    95 text \<open>
    96   We often need to reason about the existence of infinitely many
    97   (resp., all but finitely many) objects satisfying some predicate, so
    98   we introduce corresponding binders and their proof rules.
    99 \<close>
   100 
   101 lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
   102   by (rule not_frequently)
   103 
   104 lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
   105   by (rule not_eventually)
   106 
   107 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
   108   by (simp add: frequently_const_iff)
   109 
   110 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
   111   by (simp add: eventually_const_iff)
   112 
   113 lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
   114   by (rule frequently_imp_iff)
   115 
   116 lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
   117   by (auto intro: eventually_rev_mp eventually_mono)
   118 
   119 lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
   120   by (rule frequently_rev_mp[of P]) (auto elim: eventually_mono)
   121 
   122 
   123 text \<open>Properties of quantifiers with injective functions.\<close>
   124 
   125 lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
   126   using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite)
   127 
   128 lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
   129   using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite)
   130 
   131 
   132 text \<open>Properties of quantifiers with singletons.\<close>
   133 
   134 lemma not_INFM_eq [simp]:
   135   "\<not> (INFM x. x = a)"
   136   "\<not> (INFM x. a = x)"
   137   unfolding frequently_cofinite by simp_all
   138 
   139 lemma MOST_neq [simp]:
   140   "MOST x. x \<noteq> a"
   141   "MOST x. a \<noteq> x"
   142   unfolding eventually_cofinite by simp_all
   143 
   144 lemma INFM_neq [simp]:
   145   "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
   146   "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
   147   unfolding frequently_cofinite by simp_all
   148 
   149 lemma MOST_eq [simp]:
   150   "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
   151   "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
   152   unfolding eventually_cofinite by simp_all
   153 
   154 lemma MOST_eq_imp:
   155   "MOST x. x = a \<longrightarrow> P x"
   156   "MOST x. a = x \<longrightarrow> P x"
   157   unfolding eventually_cofinite by simp_all
   158 
   159 
   160 text \<open>Properties of quantifiers over the naturals.\<close>
   161 
   162 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
   163   for P :: "nat \<Rightarrow> bool"
   164   by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq simp flip: not_le)
   165 
   166 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
   167   for P :: "nat \<Rightarrow> bool"
   168   by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq simp flip: not_le)
   169 
   170 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
   171   for P :: "nat \<Rightarrow> bool"
   172   by (simp add: frequently_cofinite infinite_nat_iff_unbounded)
   173 
   174 lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)"
   175   for P :: "nat \<Rightarrow> bool"
   176   by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le)
   177 
   178 lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
   179   by (simp add: eventually_frequently)
   180 
   181 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
   182   by (simp add: cofinite_eq_sequentially)
   183 
   184 lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
   185   and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
   186   by (simp_all add: MOST_Suc_iff)
   187 
   188 lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
   189   by (simp add: cofinite_eq_sequentially)
   190 
   191 \<comment> \<open>legacy names\<close>
   192 lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
   193 lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
   194 lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
   195 lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite)
   196 lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
   197 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
   198 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)
   199 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)
   200 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)
   201 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)
   202 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)
   203 lemma MOST_conjI: "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x" by (fact eventually_conj)
   204 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)
   205 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)
   206 lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE)
   207 lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI)
   208 lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
   209 
   210 
   211 subsection \<open>Enumeration of an Infinite Set\<close>
   212 
   213 text \<open>The set's element type must be wellordered (e.g. the natural numbers).\<close>
   214 
   215 text \<open>
   216   Could be generalized to
   217     @{prop "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}.
   218 \<close>
   219 
   220 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
   221   where
   222     enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
   223   | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
   224 
   225 lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   226   by simp
   227 
   228 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S"
   229 proof (induct n arbitrary: S)
   230   case 0
   231   then show ?case
   232     by (fastforce intro: LeastI dest!: infinite_imp_nonempty)
   233 next
   234   case (Suc n)
   235   then show ?case
   236     by simp (metis DiffE infinite_remove)
   237 qed
   238 
   239 declare enumerate_0 [simp del] enumerate_Suc [simp del]
   240 
   241 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
   242   apply (induct n arbitrary: S)
   243    apply (rule order_le_neq_trans)
   244     apply (simp add: enumerate_0 Least_le enumerate_in_set)
   245    apply (simp only: enumerate_Suc')
   246    apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
   247     apply (blast intro: sym)
   248    apply (simp add: enumerate_in_set del: Diff_iff)
   249   apply (simp add: enumerate_Suc')
   250   done
   251 
   252 lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   253   by (induct m n rule: less_Suc_induct) (auto intro: enumerate_step)
   254 
   255 lemma le_enumerate:
   256   assumes S: "infinite S"
   257   shows "n \<le> enumerate S n"
   258   using S
   259 proof (induct n)
   260   case 0
   261   then show ?case by simp
   262 next
   263   case (Suc n)
   264   then have "n \<le> enumerate S n" by simp
   265   also note enumerate_mono[of n "Suc n", OF _ \<open>infinite S\<close>]
   266   finally show ?case by simp
   267 qed
   268 
   269 lemma enumerate_Suc'':
   270   fixes S :: "'a::wellorder set"
   271   assumes "infinite S"
   272   shows "enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
   273   using assms
   274 proof (induct n arbitrary: S)
   275   case 0
   276   then have "\<forall>s \<in> S. enumerate S 0 \<le> s"
   277     by (auto simp: enumerate.simps intro: Least_le)
   278   then show ?case
   279     unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"]
   280     by (intro arg_cong[where f = Least] ext) auto
   281 next
   282   case (Suc n S)
   283   show ?case
   284     using enumerate_mono[OF zero_less_Suc \<open>infinite S\<close>, of n] \<open>infinite S\<close>
   285     apply (subst (1 2) enumerate_Suc')
   286     apply (subst Suc)
   287      apply (use \<open>infinite S\<close> in simp)
   288     apply (intro arg_cong[where f = Least] ext)
   289     apply (auto simp flip: enumerate_Suc')
   290     done
   291 qed
   292 
   293 lemma enumerate_Ex:
   294   fixes S :: "nat set"
   295   assumes S: "infinite S"
   296     and s: "s \<in> S"
   297   shows "\<exists>n. enumerate S n = s"
   298   using s
   299 proof (induct s rule: less_induct)
   300   case (less s)
   301   show ?case
   302   proof (cases "\<exists>y\<in>S. y < s")
   303     case True
   304     let ?y = "Max {s'\<in>S. s' < s}"
   305     from True have y: "\<And>x. ?y < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)"
   306       by (subst Max_less_iff) auto
   307     then have y_in: "?y \<in> {s'\<in>S. s' < s}"
   308       by (intro Max_in) auto
   309     with less.hyps[of ?y] obtain n where "enumerate S n = ?y"
   310       by auto
   311     with S have "enumerate S (Suc n) = s"
   312       by (auto simp: y less enumerate_Suc'' intro!: Least_equality)
   313     then show ?thesis by auto
   314   next
   315     case False
   316     then have "\<forall>t\<in>S. s \<le> t" by auto
   317     with \<open>s \<in> S\<close> show ?thesis
   318       by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0)
   319   qed
   320 qed
   321 
   322 lemma bij_enumerate:
   323   fixes S :: "nat set"
   324   assumes S: "infinite S"
   325   shows "bij_betw (enumerate S) UNIV S"
   326 proof -
   327   have "\<And>n m. n \<noteq> m \<Longrightarrow> enumerate S n \<noteq> enumerate S m"
   328     using enumerate_mono[OF _ \<open>infinite S\<close>] by (auto simp: neq_iff)
   329   then have "inj (enumerate S)"
   330     by (auto simp: inj_on_def)
   331   moreover have "\<forall>s \<in> S. \<exists>i. enumerate S i = s"
   332     using enumerate_Ex[OF S] by auto
   333   moreover note \<open>infinite S\<close>
   334   ultimately show ?thesis
   335     unfolding bij_betw_def by (auto intro: enumerate_in_set)
   336 qed
   337 
   338 text \<open>A pair of weird and wonderful lemmas from HOL Light.\<close>
   339 lemma finite_transitivity_chain:
   340   assumes "finite A"
   341     and R: "\<And>x. \<not> R x x" "\<And>x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z"
   342     and A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> A \<and> R x y"
   343   shows "A = {}"
   344   using \<open>finite A\<close> A
   345 proof (induct A)
   346   case empty
   347   then show ?case by simp
   348 next
   349   case (insert a A)
   350   with R show ?case
   351     by (metis empty_iff insert_iff)   (* somewhat slow *)
   352 qed
   353 
   354 corollary Union_maximal_sets:
   355   assumes "finite \<F>"
   356   shows "\<Union>{T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} = \<Union>\<F>"
   357     (is "?lhs = ?rhs")
   358 proof
   359   show "?lhs \<subseteq> ?rhs" by force
   360   show "?rhs \<subseteq> ?lhs"
   361   proof (rule Union_subsetI)
   362     fix S
   363     assume "S \<in> \<F>"
   364     have "{T \<in> \<F>. S \<subseteq> T} = {}"
   365       if "\<not> (\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y)"
   366       apply (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"])
   367          apply (use assms that in auto)
   368       apply (blast intro: dual_order.trans psubset_imp_subset)
   369       done
   370     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"
   371       by blast
   372   qed
   373 qed
   374 
   375 end