Theory Infinite_Set

(*  Title:      HOL/Library/Infinite_Set.thy
    Author:     Stephan Merz
*)

section ‹Infinite Sets and Related Concepts›

theory Infinite_Set
imports Main
begin

text ‹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 ‹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)"
apply (clarsimp simp add: finite_nat_set_iff_bounded)
apply (drule_tac x="Suc (max m k)" in spec)
using less_Suc_eq by fastforce

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 ‹The set of integers is also infinite.›

lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) ⟷ infinite ((nat o abs) ` S)"
  by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD)

proposition infinite_int_iff_unbounded_le: "infinite (S::int set) ⟷ (∀m. ∃n. ¦n¦ ≥ m ∧ n ∈ S)"
  apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def)
  apply (metis abs_ge_zero nat_le_eq_zle le_nat_iff)
  done

proposition infinite_int_iff_unbounded: "infinite (S::int set) ⟷ (∀m. ∃n. ¦n¦ > m ∧ n ∈ S)"
  apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def)
  apply (metis (full_types) nat_le_iff nat_mono not_le)
  done

proposition finite_int_iff_bounded: "finite (S::int set) ⟷ (∃k. abs ` S ⊆ {..<k})"
  using infinite_int_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)

proposition finite_int_iff_bounded_le: "finite (S::int set) ⟷ (∃k. abs ` S ⊆ {.. k})"
  using infinite_int_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)

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_mono)

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_mono)

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_mono)
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

end