# Theory HOL-Library.Infinite_Set

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

section ‹Infinite Sets and Related Concepts›

theory Infinite_Set
imports Main
begin

subsection ‹The set of natural numbers is infinite›

lemma infinite_nat_iff_unbounded_le: "infinite S ⟷ (∀m. ∃n≥m. n ∈ S)"
for S :: "nat set"
using frequently_cofinite[of "λx. x ∈ S"]
by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially)

lemma infinite_nat_iff_unbounded: "infinite S ⟷ (∀m. ∃n>m. n ∈ S)"
for S :: "nat set"
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 ⟷ (∃k. S ⊆ {..<k})"
for S :: "nat set"
using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)

lemma finite_nat_iff_bounded_le: "finite S ⟷ (∃k. S ⊆ {.. k})"
for S :: "nat set"
using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)

lemma finite_nat_bounded: "finite S ⟹ ∃k. S ⊆ {..<k}"
for S :: "nat set"

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 (drule_tac x="Suc (max m k)" in spec)
using less_Suc_eq apply fastforce
done

lemma nat_not_finite: "finite (UNIV::nat set) ⟹ R"
by simp

lemma range_inj_infinite:
fixes f :: "nat ⇒ 'a"
assumes "inj f"
shows "infinite (range f)"
proof
assume "finite (range f)"
from this assms have "finite (UNIV::nat set)"
by (rule finite_imageD)
then show False by simp
qed

subsection ‹The set of integers is also infinite›

lemma infinite_int_iff_infinite_nat_abs: "infinite S ⟷ infinite ((nat ∘ abs) ` S)"
for S :: "int set"
proof (unfold Not_eq_iff, rule iffI)
assume "finite ((nat ∘ abs) ` S)"
then have "finite (nat ` (abs ` S))"
by (simp add: image_image cong: image_cong)
moreover have "inj_on nat (abs ` S)"
by (rule inj_onI) auto
ultimately have "finite (abs ` S)"
by (rule finite_imageD)
then show "finite S"
by (rule finite_image_absD)
qed simp

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

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

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

proposition finite_int_iff_bounded_le: "finite S ⟷ (∃k. abs ` S ⊆ {.. k})"
for S :: "int set"
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.
›

lemma not_INFM [simp]: "¬ (INFM x. P x) ⟷ (MOST x. ¬ P x)"
by (rule not_frequently)

lemma not_MOST [simp]: "¬ (MOST x. P x) ⟷ (INFM x. ¬ P x)"
by (rule not_eventually)

lemma INFM_const [simp]: "(INFM x::'a. P) ⟷ P ∧ infinite (UNIV::'a set)"

lemma MOST_const [simp]: "(MOST x::'a. P) ⟷ P ∨ finite (UNIV::'a set)"

lemma INFM_imp_distrib: "(INFM x. P x ⟶ Q x) ⟷ ((MOST x. P x) ⟶ (INFM x. Q x))"
by (rule frequently_imp_iff)

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) ⟷ (∃m. ∀n>m. P n)"
for P :: "nat ⇒ bool"
by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq simp flip: not_le)

lemma MOST_nat_le: "(∀⇩∞n. P n) ⟷ (∃m. ∀n≥m. P n)"
for P :: "nat ⇒ bool"
by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq simp flip: not_le)

lemma INFM_nat: "(∃⇩∞n. P n) ⟷ (∀m. ∃n>m. P n)"
for P :: "nat ⇒ bool"

lemma INFM_nat_le: "(∃⇩∞n. P n) ⟷ (∀m. ∃n≥m. P n)"
for P :: "nat ⇒ bool"

lemma MOST_INFM: "infinite (UNIV::'a set) ⟹ MOST x::'a. P x ⟹ INFM x::'a. P x"

lemma MOST_Suc_iff: "(MOST n. P (Suc n)) ⟷ (MOST n. P n)"

lemma MOST_SucI: "MOST n. P n ⟹ MOST n. P (Suc n)"
and MOST_SucD: "MOST n. P (Suc n) ⟹ MOST n. P n"

lemma MOST_ge_nat: "MOST n::nat. m ≤ n"

― ‹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
\<^prop>‹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"
proof (induct n arbitrary: S)
case 0
then show ?case
by (fastforce intro: LeastI dest!: infinite_imp_nonempty)
next
case (Suc n)
then show ?case
by simp (metis DiffE infinite_remove)
qed

declare enumerate_0 [simp del] enumerate_Suc [simp del]

lemma enumerate_step: "infinite S ⟹ enumerate S n < enumerate S (Suc n)"
proof (induction n arbitrary: S)
case 0
then have "enumerate S 0 ≤ enumerate S (Suc 0)"
by (simp add: enumerate_0 Least_le enumerate_in_set)
moreover have "enumerate (S - {enumerate S 0}) 0 ∈ S - {enumerate S 0}"
by (meson "0.prems" enumerate_in_set infinite_remove)
then have "enumerate S 0 ≠ enumerate (S - {enumerate S 0}) 0"
by auto
ultimately show ?case
next
case (Suc n)
then show ?case
qed

lemma enumerate_mono: "m < n ⟹ infinite S ⟹ enumerate S m < enumerate S n"
by (induct m n rule: less_Suc_induct) (auto intro: enumerate_step)

lemma enumerate_mono_iff [simp]:
"infinite S ⟹ enumerate S m < enumerate S n ⟷ m < n"
by (metis enumerate_mono less_asym less_linear)

lemma enumerate_mono_le_iff [simp]:
"infinite S ⟹ enumerate S m ≤ enumerate S n ⟷ m ≤ n"
by (meson enumerate_mono_iff not_le)

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 infinite_enumerate:
assumes fS: "infinite S"
shows "∃r::nat⇒nat. strict_mono r ∧ (∀n. r n ∈ S)"
unfolding strict_mono_def
using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by blast

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)
apply (use ‹infinite S› in simp)
apply (intro arg_cong[where f = Least] ext)
apply (auto simp flip: enumerate_Suc')
done
qed

lemma enumerate_Ex:
fixes S :: "nat set"
assumes S: "infinite S"
and s: "s ∈ S"
shows "∃n. enumerate S n = s"
using s
proof (induct s rule: less_induct)
case (less s)
show ?case
proof (cases "∃y∈S. y < s")
case True
let ?y = "Max {s'∈S. s' < s}"
from True 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 ?thesis by auto
next
case False
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 inj_enumerate:
fixes S :: "'a::wellorder set"
assumes S: "infinite S"
shows "inj (enumerate S)"
unfolding inj_on_def
proof clarsimp
show "⋀x y. enumerate S x = enumerate S y ⟹ x = y"
by (metis neq_iff enumerate_mono[OF _ ‹infinite S›])
qed

text ‹To generalise this, we'd need a condition that all initial segments were finite›
lemma bij_enumerate:
fixes S :: "nat set"
assumes S: "infinite S"
shows "bij_betw (enumerate S) UNIV S"
proof -
have "∀s ∈ S. ∃i. enumerate S i = s"
using enumerate_Ex[OF S] by auto
moreover note ‹infinite S› inj_enumerate
ultimately show ?thesis
unfolding bij_betw_def by (auto intro: enumerate_in_set)
qed

lemma
fixes S :: "nat set"
assumes S: "infinite S"
shows range_enumerate: "range (enumerate S) = S"
and strict_mono_enumerate: "strict_mono (enumerate S)"
by (auto simp add: bij_betw_imp_surj_on bij_enumerate assms strict_mono_def)

text ‹A pair of weird and wonderful lemmas from HOL Light.›
lemma finite_transitivity_chain:
assumes "finite A"
and R: "⋀x. ¬ R x x" "⋀x y z. ⟦R x y; R y z⟧ ⟹ R x z"
and A: "⋀x. x ∈ A ⟹ ∃y. y ∈ A ∧ R x y"
shows "A = {}"
using ‹finite A› A
proof (induct A)
case empty
then show ?case by simp
next
case (insert a A)
have False
using R(1)[of a] R(2)[of _ a] insert(3,4) by blast
thus ?case ..
qed

corollary Union_maximal_sets:
assumes "finite ℱ"
shows "⋃{T ∈ ℱ. ∀U∈ℱ. ¬ T ⊂ U} = ⋃ℱ"
(is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs" by force
show "?rhs ⊆ ?lhs"
proof (rule Union_subsetI)
fix S
assume "S ∈ ℱ"
have "{T ∈ ℱ. S ⊆ T} = {}"
if "¬ (∃y. y ∈ {T ∈ ℱ. ∀U∈ℱ. ¬ T ⊂ U} ∧ S ⊆ y)"
proof -
have §: "⋀x. x ∈ ℱ ∧ S ⊆ x ⟹ ∃y. y ∈ ℱ ∧ S ⊆ y ∧ x ⊂ y"
using that by (blast intro: dual_order.trans psubset_imp_subset)
show ?thesis
proof (rule finite_transitivity_chain [of _ "λT U. S ⊆ T ∧ T ⊂ U"])
qed (use assms in ‹auto intro: §›)
qed
with ‹S ∈ ℱ› show "∃y. y ∈ {T ∈ ℱ. ∀U∈ℱ. ¬ T ⊂ U} ∧ S ⊆ y"
by blast
qed
qed

subsection ‹Properties of @{term enumerate} on finite sets›

lemma finite_enumerate_in_set: "⟦finite S; n < card S⟧ ⟹ enumerate S n ∈ S"
proof (induction n arbitrary: S)
case 0
then show ?case
by (metis all_not_in_conv card.empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
next
case (Suc n)
show ?case
using Suc.prems Suc.IH [of "S - {LEAST n. n ∈ S}"]
by (metis Diff_empty Diff_insert0 Suc_lessD card.remove less_Suc_eq)
qed

lemma finite_enumerate_step: "⟦finite S; Suc n < card S⟧ ⟹ enumerate S n < enumerate S (Suc n)"
proof (induction n arbitrary: S)
case 0
then have "enumerate S 0 ≤ enumerate S (Suc 0)"
by (simp add: Least_le enumerate.simps(1) finite_enumerate_in_set)
moreover have "enumerate (S - {enumerate S 0}) 0 ∈ S - {enumerate S 0}"
by (metis 0 Suc_lessD Suc_less_eq card_Suc_Diff1 enumerate_in_set finite_enumerate_in_set)
then have "enumerate S 0 ≠ enumerate (S - {enumerate S 0}) 0"
by auto
ultimately show ?case
next
case (Suc n)
then show ?case
qed

lemma finite_enumerate_mono: "⟦m < n; finite S; n < card S⟧ ⟹ enumerate S m < enumerate S n"
by (induct m n rule: less_Suc_induct) (auto intro: finite_enumerate_step)

lemma finite_enumerate_mono_iff [simp]:
"⟦finite S; m < card S; n < card S⟧ ⟹ enumerate S m < enumerate S n ⟷ m < n"
by (metis finite_enumerate_mono less_asym less_linear)

lemma finite_le_enumerate:
assumes "finite S" "n < card S"
shows "n ≤ enumerate S n"
using assms
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)
then have "n ≤ enumerate S n" by simp
also note finite_enumerate_mono[of n "Suc n", OF _ ‹finite S›]
finally show ?case
using Suc.prems(2) Suc_leI by blast
qed

lemma finite_enumerate:
assumes fS: "finite S"
shows "∃r::nat⇒nat. strict_mono_on {..<card S} r ∧ (∀n<card S. r n ∈ S)"
unfolding strict_mono_def
using finite_enumerate_in_set[OF fS] finite_enumerate_mono[of _ _ S] fS
by (metis lessThan_iff strict_mono_on_def)

lemma finite_enumerate_Suc'':
fixes S :: "'a::wellorder set"
assumes "finite S" "Suc n < card S"
shows "enumerate S (Suc n) = (LEAST s. s ∈ S ∧ enumerate S n < s)"
using assms
proof (induction 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 (metis Diff_iff dual_order.strict_iff_order singletonD singletonI)
next
case (Suc n S)
then have "Suc n < card (S - {enumerate S 0})"
using Suc.prems(2) finite_enumerate_in_set by force
then show ?case
apply (subst (1 2) enumerate_Suc')
apply (intro arg_cong[where f = Least] HOL.ext)
using finite_enumerate_mono[OF zero_less_Suc ‹finite S›, of n] Suc.prems
by (auto simp flip: enumerate_Suc')
qed

lemma finite_enumerate_initial_segment:
fixes S :: "'a::wellorder set"
assumes "finite S" and n: "n < card (S ∩ {..<s})"
shows "enumerate (S ∩ {..<s}) n = enumerate S n"
using n
proof (induction n)
case 0
have "(LEAST n. n ∈ S ∧ n < s) = (LEAST n. n ∈ S)"
proof (rule Least_equality)
have "∃t. t ∈ S ∧ t < s"
by (metis "0" card_gt_0_iff disjoint_iff_not_equal lessThan_iff)
then show "(LEAST n. n ∈ S) ∈ S ∧ (LEAST n. n ∈ S) < s"
by (meson LeastI Least_le le_less_trans)
then show ?case
by (auto simp: enumerate_0)
next
case (Suc n)
then have less_card: "Suc n < card S"
by (meson assms(1) card_mono inf_sup_ord(1) leD le_less_linear order.trans)
obtain T where T: "T ∈ {s ∈ S. enumerate S n < s}"
by (metis Infinite_Set.enumerate_step enumerate_in_set finite_enumerate_in_set finite_enumerate_step less_card mem_Collect_eq)
have "(LEAST x. x ∈ S ∧ x < s ∧ enumerate S n < x) = (LEAST x. x ∈ S ∧ enumerate S n < x)"
(is "_ = ?r")
proof (intro Least_equality conjI)
show "?r ∈ S"
by (metis (mono_tags, lifting) LeastI mem_Collect_eq T)
have "¬ s ≤ ?r"
using not_less_Least [of _ "λx. x ∈ S ∧ enumerate S n < x"] Suc assms
by (metis (mono_tags, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def less_le_trans)
then show "?r < s"
by auto
show "enumerate S n < ?r"
by (metis (no_types, lifting) LeastI mem_Collect_eq T)
qed (auto simp: Least_le)
then show ?case
using Suc assms by (simp add: finite_enumerate_Suc'' less_card)
qed

lemma finite_enumerate_Ex:
fixes S :: "'a::wellorder set"
assumes S: "finite S"
and s: "s ∈ S"
shows "∃n<card S. enumerate S n = s"
using s S
proof (induction s arbitrary: S rule: less_induct)
case (less s)
show ?case
proof (cases "∃y∈S. y < s")
case True
let ?T = "S ∩ {..<s}"
have "finite ?T"
using less.prems(2) by blast
have TS: "card ?T < card S"
using less.prems by (blast intro: psubset_card_mono [OF ‹finite S›])
from True have y: "⋀x. Max ?T < x ⟷ (∀s'∈S. s' < s ⟶ s' < x)"
by (subst Max_less_iff) (auto simp: ‹finite ?T›)
then have y_in: "Max ?T ∈ {s'∈S. s' < s}"
using Max_in ‹finite ?T› by fastforce
with less.IH[of "Max ?T" ?T] obtain n where n: "enumerate ?T n = Max ?T" "n < card ?T"
using ‹finite ?T› by blast
then have "Suc n < card S"
using TS less_trans_Suc by blast
with S n have "enumerate S (Suc n) = s"
by (subst finite_enumerate_Suc'') (auto simp: y finite_enumerate_initial_segment less finite_enumerate_Suc'' intro!: Least_equality)
then show ?thesis
using ‹Suc n < card S› by blast
next
case False
then have "∀t∈S. s ≤ t" by auto
moreover have "0 < card S"
using card_0_eq less.prems by blast
ultimately show ?thesis
using ‹s ∈ S›
by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0)
qed
qed

lemma finite_enum_subset:
assumes "⋀i. i < card X ⟹ enumerate X i = enumerate Y i" and "finite X" "finite Y" "card X ≤ card Y"
shows "X ⊆ Y"
by (metis assms finite_enumerate_Ex finite_enumerate_in_set less_le_trans subsetI)

lemma finite_enum_ext:
assumes "⋀i. i < card X ⟹ enumerate X i = enumerate Y i" and "finite X" "finite Y" "card X = card Y"
shows "X = Y"
by (intro antisym finite_enum_subset) (auto simp: assms)

lemma finite_bij_enumerate:
fixes S :: "'a::wellorder set"
assumes S: "finite S"
shows "bij_betw (enumerate S) {..<card S} S"
proof -
have "⋀n m. ⟦n ≠ m; n < card S; m < card S⟧ ⟹ enumerate S n ≠ enumerate S m"
using finite_enumerate_mono[OF _ ‹finite S›] by (auto simp: neq_iff)
then have "inj_on (enumerate S) {..<card S}"
by (auto simp: inj_on_def)
moreover have "∀s ∈ S. ∃i<card S. enumerate S i = s"
using finite_enumerate_Ex[OF S] by auto
moreover note ‹finite S›
ultimately show ?thesis
unfolding bij_betw_def by (auto intro: finite_enumerate_in_set)
qed

lemma ex_bij_betw_strict_mono_card:
fixes M :: "'a::wellorder set"
assumes "finite M"
obtains h where "bij_betw h {..<card M} M" and "strict_mono_on {..<card M} h"
proof
show "bij_betw (enumerate M) {..<card M} M"