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