1(* Title: HOL/Library/Infinite_Set.thy 2 Author: Stephan Merz 3*) 4 5section \<open>Infinite Sets and Related Concepts\<close> 6 7theory Infinite_Set 8 imports Main 9begin 10 11subsection \<open>The set of natural numbers is infinite\<close> 12 13lemma 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 18lemma 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 23lemma 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 27lemma 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 31lemma 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 36text \<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 42lemma 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 48lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R" 49 by simp 50 51lemma range_inj_infinite: 52 fixes f :: "nat \<Rightarrow> 'a" 53 assumes "inj f" 54 shows "infinite (range f)" 55proof 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 60qed 61 62 63subsection \<open>The set of integers is also infinite\<close> 64 65lemma infinite_int_iff_infinite_nat_abs: "infinite S \<longleftrightarrow> infinite ((nat \<circ> abs) ` S)" 66 for S :: "int set" 67proof - 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) 72qed 73 74proposition 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 79proposition 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 84proposition 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 88proposition 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 93subsection \<open>Infinitely Many and Almost All\<close> 94 95text \<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 101lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" 102 by (rule not_frequently) 103 104lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" 105 by (rule not_eventually) 106 107lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)" 108 by (simp add: frequently_const_iff) 109 110lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)" 111 by (simp add: eventually_const_iff) 112 113lemma 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 116lemma 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 119lemma 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 123text \<open>Properties of quantifiers with injective functions.\<close> 124 125lemma 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 128lemma 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 132text \<open>Properties of quantifiers with singletons.\<close> 133 134lemma not_INFM_eq [simp]: 135 "\<not> (INFM x. x = a)" 136 "\<not> (INFM x. a = x)" 137 unfolding frequently_cofinite by simp_all 138 139lemma MOST_neq [simp]: 140 "MOST x. x \<noteq> a" 141 "MOST x. a \<noteq> x" 142 unfolding eventually_cofinite by simp_all 143 144lemma 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 149lemma 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 154lemma 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 160text \<open>Properties of quantifiers over the naturals.\<close> 161 162lemma 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 166lemma 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 170lemma 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 174lemma 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 178lemma 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 181lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)" 182 by (simp add: cofinite_eq_sequentially) 183 184lemma 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 188lemma MOST_ge_nat: "MOST n::nat. m \<le> n" 189 by (simp add: cofinite_eq_sequentially) 190 191\<comment> \<open>legacy names\<close> 192lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite) 193lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp 194lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite) 195lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite) 196lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex) 197lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually) 198lemma 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) 199lemma 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) 200lemma 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) 201lemma 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) 202lemma 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) 203lemma MOST_conjI: "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x" by (fact eventually_conj) 204lemma 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) 205lemma 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) 206lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE) 207lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI) 208lemmas MOST_iff_finiteNeg = MOST_iff_cofinite 209 210 211subsection \<open>Enumeration of an Infinite Set\<close> 212 213text \<open>The set's element type must be wellordered (e.g. the natural numbers).\<close> 214 215text \<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 220primrec (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 225lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n" 226 by simp 227 228lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S" 229proof (induct n arbitrary: S) 230 case 0 231 then show ?case 232 by (fastforce intro: LeastI dest!: infinite_imp_nonempty) 233next 234 case (Suc n) 235 then show ?case 236 by simp (metis DiffE infinite_remove) 237qed 238 239declare enumerate_0 [simp del] enumerate_Suc [simp del] 240 241lemma 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 252lemma 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 255lemma le_enumerate: 256 assumes S: "infinite S" 257 shows "n \<le> enumerate S n" 258 using S 259proof (induct n) 260 case 0 261 then show ?case by simp 262next 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 267qed 268 269lemma 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 274proof (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 281next 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 291qed 292 293lemma 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 299proof (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 320qed 321 322lemma bij_enumerate: 323 fixes S :: "nat set" 324 assumes S: "infinite S" 325 shows "bij_betw (enumerate S) UNIV S" 326proof - 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) 336qed 337 338text \<open>A pair of weird and wonderful lemmas from HOL Light.\<close> 339lemma 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 345proof (induct A) 346 case empty 347 then show ?case by simp 348next 349 case (insert a A) 350 with R show ?case 351 by (metis empty_iff insert_iff) (* somewhat slow *) 352qed 353 354corollary 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") 358proof 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 373qed 374 375end 376