(* Title: HOL/Library/Infinite_Set.thy Author: Stephan Merz *) section {* Infinite Sets and Related Concepts *} theory Infinite_Set imports Main begin subsection "Infinite Sets" text {* Some elementary facts about infinite sets, mostly by Stephan Merz. Beware! Because "infinite" merely abbreviates a negation, these lemmas may not work well with @{text "blast"}. *} abbreviation infinite :: "'a set => bool" where "infinite S ≡ ¬ finite S" text {* Infinite sets are non-empty, and if we remove some elements from an infinite set, the result is still infinite. *} lemma infinite_imp_nonempty: "infinite S ==> S ≠ {}" by auto lemma infinite_remove: "infinite S ==> infinite (S - {a})" by simp lemma Diff_infinite_finite: assumes T: "finite T" and S: "infinite S" shows "infinite (S - T)" using T proof induct from S show "infinite (S - {})" by auto next fix T x assume ih: "infinite (S - T)" have "S - (insert x T) = (S - T) - {x}" by (rule Diff_insert) with ih show "infinite (S - (insert x T))" by (simp add: infinite_remove) qed lemma Un_infinite: "infinite S ==> infinite (S ∪ T)" by simp lemma infinite_Un: "infinite (S ∪ T) <-> infinite S ∨ infinite T" by simp lemma infinite_super: assumes T: "S ⊆ T" and S: "infinite S" shows "infinite T" proof assume "finite T" with T have "finite S" by (simp add: finite_subset) with S show False by simp qed text {* As a concrete example, we prove that the set of natural numbers is infinite. *} lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) <-> (∀m. ∃n≥m. n ∈ S)" using frequently_cofinite[of "λx. x ∈ S"] by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially) lemma infinite_nat_iff_unbounded: "infinite (S::nat set) <-> (∀m. ∃n>m. n ∈ S)" using frequently_cofinite[of "λx. x ∈ S"] by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense) lemma finite_nat_iff_bounded: "finite (S::nat set) <-> (∃k. S ⊆ {..<k})" using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le) lemma finite_nat_iff_bounded_le: "finite (S::nat set) <-> (∃k. S ⊆ {.. k})" using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le) lemma finite_nat_bounded: "finite (S::nat set) ==> ∃k. S ⊆ {..<k}" by (simp add: finite_nat_iff_bounded) text {* For a set of natural numbers to be infinite, it is enough to know that for any number larger than some @{text k}, there is some larger number that is an element of the set. *} lemma unbounded_k_infinite: "∀m>k. ∃n>m. n ∈ S ==> infinite (S::nat set)" by (metis (full_types) infinite_nat_iff_unbounded_le le_imp_less_Suc not_less not_less_iff_gr_or_eq sup.bounded_iff) lemma nat_not_finite: "finite (UNIV::nat set) ==> R" by simp lemma range_inj_infinite: "inj (f::nat => 'a) ==> infinite (range f)" proof assume "finite (range f)" and "inj f" then have "finite (UNIV::nat set)" by (rule finite_imageD) then show False by simp qed text {* For any function with infinite domain and finite range there is some element that is the image of infinitely many domain elements. In particular, any infinite sequence of elements from a finite set contains some element that occurs infinitely often. *} lemma inf_img_fin_dom': assumes img: "finite (f ` A)" and dom: "infinite A" shows "∃y ∈ f ` A. infinite (f -` {y} ∩ A)" proof (rule ccontr) have "A ⊆ (\<Union>y∈f ` A. f -` {y} ∩ A)" by auto moreover assume "¬ ?thesis" with img have "finite (\<Union>y∈f ` A. f -` {y} ∩ A)" by blast ultimately have "finite A" by(rule finite_subset) with dom show False by contradiction qed lemma inf_img_fin_domE': assumes "finite (f ` A)" and "infinite A" obtains y where "y ∈ f`A" and "infinite (f -` {y} ∩ A)" using assms by (blast dest: inf_img_fin_dom') lemma inf_img_fin_dom: assumes img: "finite (f`A)" and dom: "infinite A" shows "∃y ∈ f`A. infinite (f -` {y})" using inf_img_fin_dom'[OF assms] by auto lemma inf_img_fin_domE: assumes "finite (f`A)" and "infinite A" obtains y where "y ∈ f`A" and "infinite (f -` {y})" using assms by (blast dest: inf_img_fin_dom) subsection "Infinitely Many and Almost All" text {* We often need to reason about the existence of infinitely many (resp., all but finitely many) objects satisfying some predicate, so we introduce corresponding binders and their proof rules. *} (* The following two lemmas are available as filter-rules, but not in the simp-set *) lemma not_INFM [simp]: "¬ (INFM x. P x) <-> (MOST x. ¬ P x)" by (fact not_frequently) lemma not_MOST [simp]: "¬ (MOST x. P x) <-> (INFM x. ¬ P x)" by (fact not_eventually) lemma INFM_const [simp]: "(INFM x::'a. P) <-> P ∧ infinite (UNIV::'a set)" by (simp add: frequently_const_iff) lemma MOST_const [simp]: "(MOST x::'a. P) <-> P ∨ finite (UNIV::'a set)" by (simp add: eventually_const_iff) lemma INFM_imp_distrib: "(INFM x. P x --> Q x) <-> ((MOST x. P x) --> (INFM x. Q x))" by (simp only: imp_conv_disj frequently_disj_iff not_eventually) lemma MOST_imp_iff: "MOST x. P x ==> (MOST x. P x --> Q x) <-> (MOST x. Q x)" by (auto intro: eventually_rev_mp eventually_elim1) lemma INFM_conjI: "INFM x. P x ==> MOST x. Q x ==> INFM x. P x ∧ Q x" by (rule frequently_rev_mp[of P]) (auto elim: eventually_elim1) text {* Properties of quantifiers with injective functions. *} lemma INFM_inj: "INFM x. P (f x) ==> inj f ==> INFM x. P x" using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite) lemma MOST_inj: "MOST x. P x ==> inj f ==> MOST x. P (f x)" using finite_vimageI[of "{x. ¬ P x}" f] by (auto simp: eventually_cofinite) text {* Properties of quantifiers with singletons. *} lemma not_INFM_eq [simp]: "¬ (INFM x. x = a)" "¬ (INFM x. a = x)" unfolding frequently_cofinite by simp_all lemma MOST_neq [simp]: "MOST x. x ≠ a" "MOST x. a ≠ x" unfolding eventually_cofinite by simp_all lemma INFM_neq [simp]: "(INFM x::'a. x ≠ a) <-> infinite (UNIV::'a set)" "(INFM x::'a. a ≠ x) <-> infinite (UNIV::'a set)" unfolding frequently_cofinite by simp_all lemma MOST_eq [simp]: "(MOST x::'a. x = a) <-> finite (UNIV::'a set)" "(MOST x::'a. a = x) <-> finite (UNIV::'a set)" unfolding eventually_cofinite by simp_all lemma MOST_eq_imp: "MOST x. x = a --> P x" "MOST x. a = x --> P x" unfolding eventually_cofinite by simp_all text {* Properties of quantifiers over the naturals. *} lemma MOST_nat: "(∀⇩_{∞}n. P (n::nat)) <-> (∃m. ∀n>m. P n)" by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric]) lemma MOST_nat_le: "(∀⇩_{∞}n. P (n::nat)) <-> (∃m. ∀n≥m. P n)" by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric]) lemma INFM_nat: "(∃⇩_{∞}n. P (n::nat)) <-> (∀m. ∃n>m. P n)" by (simp add: frequently_cofinite infinite_nat_iff_unbounded) lemma INFM_nat_le: "(∃⇩_{∞}n. P (n::nat)) <-> (∀m. ∃n≥m. P n)" by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le) lemma MOST_INFM: "infinite (UNIV::'a set) ==> MOST x::'a. P x ==> INFM x::'a. P x" by (simp add: eventually_frequently) lemma MOST_Suc_iff: "(MOST n. P (Suc n)) <-> (MOST n. P n)" by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc) lemma shows MOST_SucI: "MOST n. P n ==> MOST n. P (Suc n)" and MOST_SucD: "MOST n. P (Suc n) ==> MOST n. P n" by (simp_all add: MOST_Suc_iff) lemma MOST_ge_nat: "MOST n::nat. m ≤ n" by (simp add: cofinite_eq_sequentially eventually_ge_at_top) (* legacy names *) lemma Inf_many_def: "Inf_many P <-> infinite {x. P x}" by (fact frequently_cofinite) lemma Alm_all_def: "Alm_all P <-> ¬ (INFM x. ¬ P x)" by simp lemma INFM_iff_infinite: "(INFM x. P x) <-> infinite {x. P x}" by (fact frequently_cofinite) lemma MOST_iff_cofinite: "(MOST x. P x) <-> finite {x. ¬ P x}" by (fact eventually_cofinite) lemma INFM_EX: "(∃⇩_{∞}x. P x) ==> (∃x. P x)" by (fact frequently_ex) lemma ALL_MOST: "∀x. P x ==> ∀⇩_{∞}x. P x" by (fact always_eventually) lemma INFM_mono: "∃⇩_{∞}x. P x ==> (!!x. P x ==> Q x) ==> ∃⇩_{∞}x. Q x" by (fact frequently_elim1) lemma MOST_mono: "∀⇩_{∞}x. P x ==> (!!x. P x ==> Q x) ==> ∀⇩_{∞}x. Q x" by (fact eventually_elim1) lemma INFM_disj_distrib: "(∃⇩_{∞}x. P x ∨ Q x) <-> (∃⇩_{∞}x. P x) ∨ (∃⇩_{∞}x. Q x)" by (fact frequently_disj_iff) lemma MOST_rev_mp: "∀⇩_{∞}x. P x ==> ∀⇩_{∞}x. P x --> Q x ==> ∀⇩_{∞}x. Q x" by (fact eventually_rev_mp) lemma MOST_conj_distrib: "(∀⇩_{∞}x. P x ∧ Q x) <-> (∀⇩_{∞}x. P x) ∧ (∀⇩_{∞}x. Q x)" by (fact eventually_conj_iff) lemma MOST_conjI: "MOST x. P x ==> MOST x. Q x ==> MOST x. P x ∧ Q x" by (fact eventually_conj) lemma INFM_finite_Bex_distrib: "finite A ==> (INFM y. ∃x∈A. P x y) <-> (∃x∈A. INFM y. P x y)" by (fact frequently_bex_finite_distrib) lemma MOST_finite_Ball_distrib: "finite A ==> (MOST y. ∀x∈A. P x y) <-> (∀x∈A. MOST y. P x y)" by (fact eventually_ball_finite_distrib) lemma INFM_E: "INFM x. P x ==> (!!x. P x ==> thesis) ==> thesis" by (fact frequentlyE) lemma MOST_I: "(!!x. P x) ==> MOST x. P x" by (rule eventuallyI) lemmas MOST_iff_finiteNeg = MOST_iff_cofinite subsection "Enumeration of an Infinite Set" text {* The set's element type must be wellordered (e.g. the natural numbers). *} text ‹ Could be generalized to @{term "enumerate' S n = (SOME t. t ∈ s ∧ finite {s∈S. s < t} ∧ card {s∈S. s < t} = n)"}. › primrec (in wellorder) enumerate :: "'a set => nat => 'a" where enumerate_0: "enumerate S 0 = (LEAST n. n ∈ S)" | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n ∈ S}) n" lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n" by simp lemma enumerate_in_set: "infinite S ==> enumerate S n ∈ S" apply (induct n arbitrary: S) apply (fastforce intro: LeastI dest!: infinite_imp_nonempty) apply simp apply (metis DiffE infinite_remove) done declare enumerate_0 [simp del] enumerate_Suc [simp del] lemma enumerate_step: "infinite S ==> enumerate S n < enumerate S (Suc n)" apply (induct n arbitrary: S) apply (rule order_le_neq_trans) apply (simp add: enumerate_0 Least_le enumerate_in_set) apply (simp only: enumerate_Suc') apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 ∈ S - {enumerate S 0}") apply (blast intro: sym) apply (simp add: enumerate_in_set del: Diff_iff) apply (simp add: enumerate_Suc') done lemma enumerate_mono: "m < n ==> infinite S ==> enumerate S m < enumerate S n" apply (erule less_Suc_induct) apply (auto intro: enumerate_step) done lemma le_enumerate: assumes S: "infinite S" shows "n ≤ enumerate S n" using S proof (induct n) case 0 then show ?case by simp next case (Suc n) then have "n ≤ enumerate S n" by simp also note enumerate_mono[of n "Suc n", OF _ `infinite S`] finally show ?case by simp qed lemma enumerate_Suc'': fixes S :: "'a::wellorder set" assumes "infinite S" shows "enumerate S (Suc n) = (LEAST s. s ∈ S ∧ enumerate S n < s)" using assms proof (induct n arbitrary: S) case 0 then have "∀s ∈ S. enumerate S 0 ≤ s" by (auto simp: enumerate.simps intro: Least_le) then show ?case unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"] by (intro arg_cong[where f = Least] ext) auto next case (Suc n S) show ?case using enumerate_mono[OF zero_less_Suc `infinite S`, of n] `infinite S` apply (subst (1 2) enumerate_Suc') apply (subst Suc) using `infinite S` apply simp apply (intro arg_cong[where f = Least] ext) apply (auto simp: enumerate_Suc'[symmetric]) done qed lemma enumerate_Ex: assumes S: "infinite (S::nat set)" shows "s ∈ S ==> ∃n. enumerate S n = s" proof (induct s rule: less_induct) case (less s) show ?case proof cases let ?y = "Max {s'∈S. s' < s}" assume "∃y∈S. y < s" then have y: "!!x. ?y < x <-> (∀s'∈S. s' < s --> s' < x)" by (subst Max_less_iff) auto then have y_in: "?y ∈ {s'∈S. s' < s}" by (intro Max_in) auto with less.hyps[of ?y] obtain n where "enumerate S n = ?y" by auto with S have "enumerate S (Suc n) = s" by (auto simp: y less enumerate_Suc'' intro!: Least_equality) then show ?case by auto next assume *: "¬ (∃y∈S. y < s)" then have "∀t∈S. s ≤ t" by auto with `s ∈ S` show ?thesis by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0) qed qed lemma bij_enumerate: fixes S :: "nat set" assumes S: "infinite S" shows "bij_betw (enumerate S) UNIV S" proof - have "!!n m. n ≠ m ==> enumerate S n ≠ enumerate S m" using enumerate_mono[OF _ `infinite S`] by (auto simp: neq_iff) then have "inj (enumerate S)" by (auto simp: inj_on_def) moreover have "∀s ∈ S. ∃i. enumerate S i = s" using enumerate_Ex[OF S] by auto moreover note `infinite S` ultimately show ?thesis unfolding bij_betw_def by (auto intro: enumerate_in_set) qed subsection "Miscellaneous" text {* A few trivial lemmas about sets that contain at most one element. These simplify the reasoning about deterministic automata. *} definition atmost_one :: "'a set => bool" where "atmost_one S <-> (∀x y. x∈S ∧ y∈S --> x = y)" lemma atmost_one_empty: "S = {} ==> atmost_one S" by (simp add: atmost_one_def) lemma atmost_one_singleton: "S = {x} ==> atmost_one S" by (simp add: atmost_one_def) lemma atmost_one_unique [elim]: "atmost_one S ==> x ∈ S ==> y ∈ S ==> y = x" by (simp add: atmost_one_def) end