# Theory Library_Additions

```section ‹Library additions›

theory Library_Additions
imports "ZFC_in_HOL.Ordinal_Exp" "HOL-Library.Ramsey" "Nash_Williams.Nash_Williams"

begin

lemma finite_enumerate_Diff_singleton:
fixes S :: "'a::wellorder set"
assumes "finite S" and i: "i < card S" "enumerate S i < x"
shows "enumerate (S - {x}) i = enumerate S i"
using i
proof (induction i)
case 0
have "(LEAST i. i ∈ S ∧ i≠x) = (LEAST i. i ∈ S)"
proof (rule Least_equality)
have "∃t. t ∈ S ∧ t≠x"
using 0 ‹finite S› finite_enumerate_in_set by blast
then show "(LEAST i. i ∈ S) ∈ S ∧ (LEAST i. i ∈ S) ≠ x"
by (metis "0.prems"(2) LeastI enumerate_0 not_less_Least)
qed (simp add: Least_le)
then show ?case
by (auto simp: enumerate_0)
next
case (Suc i)
then have x: "enumerate S i < x"
by (meson enumerate_step finite_enumerate_step less_trans)
have cardSx: "Suc i < card (S - {x})" and "i < card S"
using Suc ‹finite S› card_Diff_singleton_if[of S] finite_enumerate_Ex by fastforce+
have "(LEAST s. s ∈ S ∧ s≠x ∧ enumerate (S - {x}) i < s) = (LEAST s. s ∈ S ∧ enumerate S i < s)"
(is "_ = ?r")
proof (intro Least_equality conjI)
show "?r ∈ S"
by (metis (lifting) LeastI Suc.prems(1) assms(1) finite_enumerate_in_set finite_enumerate_step)
show "?r ≠ x"
using Suc.prems not_less_Least [of _ "λt. t ∈ S ∧ enumerate S i < t"]
‹finite S› finite_enumerate_in_set finite_enumerate_step by blast
show "enumerate (S - {x}) i < ?r"
by (metis (full_types) Suc.IH Suc.prems(1) ‹i < card S› enumerate_Suc'' enumerate_step finite_enumerate_Suc'' finite_enumerate_step x)
show "⋀y. y ∈ S ∧ y ≠ x ∧ enumerate (S - {x}) i < y ⟹ ?r ≤ y"
by (simp add: Least_le Suc.IH ‹i < card S› x)
qed
then show ?case
using Suc assms by (simp add: finite_enumerate_Suc'' cardSx)
qed

lemma hd_lex: "⟦hd ms < hd ns; length ms = length ns; ns ≠ []⟧ ⟹ (ms, ns) ∈ lex less_than"
by (metis hd_Cons_tl length_0_conv less_than_iff lexord_cons_cons lexord_lex)

lemma sorted_hd_le:
assumes "sorted xs" "x ∈ list.set xs"
shows "hd xs ≤ x"
using assms by (induction xs) (auto simp: less_imp_le)

lemma sorted_le_last:
assumes "sorted xs" "x ∈ list.set xs"
shows "x ≤ last xs"
using assms by (induction xs) (auto simp: less_imp_le)

lemma hd_list_of:
assumes "finite A" "A ≠ {}"
shows "hd (sorted_list_of_set A) = Min A"
proof (rule antisym)
have "Min A ∈ A"
by (simp add: assms)
then show "hd (sorted_list_of_set A) ≤ Min A"
by (simp add: sorted_hd_le ‹finite A›)
next
show "Min A ≤ hd (sorted_list_of_set A)"
by (metis Min_le assms hd_in_set set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff)
qed

lemma sorted_hd_le_last:
assumes "sorted xs" "xs ≠ []"
shows "hd xs ≤ last xs"
using assms by (simp add: sorted_hd_le)

lemma sorted_list_of_set_set_of [simp]: "strict_sorted l ⟹ sorted_list_of_set (list.set l) = l"
by (simp add: strict_sorted_equal)

lemma range_strict_mono_ext:
fixes f::"nat ⇒ 'a::linorder"
assumes eq: "range f = range g"
and sm: "strict_mono f" "strict_mono g"
shows "f = g"
proof
fix n
show "f n = g n"
proof (induction n rule: less_induct)
case (less n)
obtain x y where xy: "f n = g y" "f x = g n"
by (metis eq imageE rangeI)
then have "n = y"
by (metis (no_types) less.IH neq_iff sm strict_mono_less xy)
then show ?case using xy by auto
qed
qed

subsection ‹Other material›

definition strict_mono_sets :: "['a::order set, 'a::order ⇒ 'b::order set] ⇒ bool" where
"strict_mono_sets A f ≡ ∀x∈A. ∀y∈A. x < y ⟶ less_sets (f x) (f y)"

lemma strict_mono_setsD:
assumes "strict_mono_sets A f" "x < y" "x ∈ A" "y ∈ A"
shows "less_sets (f x) (f y)"
using assms by (auto simp: strict_mono_sets_def)

lemma strict_mono_sets_imp_disjoint:
fixes A :: "'a::linorder set"
assumes "strict_mono_sets A f"
shows "pairwise (λx y. disjnt (f x) (f y)) A"
using assms unfolding strict_mono_sets_def pairwise_def
by (meson antisym_conv3 disjnt_sym less_sets_imp_disjnt)

lemma strict_mono_sets_subset:
assumes "strict_mono_sets B f" "A ⊆ B"
shows "strict_mono_sets A f"
using assms by (auto simp: strict_mono_sets_def)

lemma strict_mono_less_sets_Min:
assumes "strict_mono_sets I f" "finite I" "I ≠ {}"
shows "less_sets (f (Min I)) (⋃ (f ` (I - {Min I})))"
using assms by (simp add: strict_mono_sets_def less_sets_UN2 dual_order.strict_iff_order)

lemma pair_less_iff1 [simp]: "((x,y), (x,z)) ∈ pair_less ⟷ y<z"
by (simp add: pair_less_def)

lemma infinite_finite_Inter:
assumes "finite 𝒜" "𝒜≠{}" "⋀A. A ∈ 𝒜 ⟹ infinite A"
and "⋀A B. ⟦A ∈ 𝒜; B ∈ 𝒜⟧ ⟹ A ∩ B ∈ 𝒜"
shows "infinite (⋂𝒜)"
by (simp add: assms finite_Inf_in)

lemma atLeast_less_sets: "⟦less_sets A {x}; B ⊆ {x..}⟧ ⟹ less_sets A B"
by (force simp: less_sets_def subset_iff)

subsection ‹The list-of function›

lemma sorted_list_of_set_insert_remove_cons:
assumes "finite A" "less_sets {a} A"
shows "sorted_list_of_set (insert a A) = a # sorted_list_of_set A"
proof -
have "strict_sorted (a # sorted_list_of_set A)"
using assms less_setsD by auto
moreover have "list.set (a # sorted_list_of_set A) = insert a A"
using assms by force
moreover have "length (a # sorted_list_of_set A) = card (insert a A)"
using assms card_insert_if less_setsD by fastforce
ultimately show ?thesis
by (metis ‹finite A› finite_insert sorted_list_of_set_unique)
qed

lemma sorted_list_of_set_Un:
assumes AB: "less_sets A B" and fin: "finite A" "finite B"
shows "sorted_list_of_set (A ∪ B) = sorted_list_of_set A @ sorted_list_of_set B"
proof -
have "strict_sorted (sorted_list_of_set A @ sorted_list_of_set B)"
using AB unfolding less_sets_def
by (metis fin set_sorted_list_of_set sorted_wrt_append strict_sorted_list_of_set)
moreover have "card A + card B = card (A ∪ B)"
using less_sets_imp_disjnt [OF AB]
by (simp add: assms card_Un_disjoint disjnt_def)
ultimately show ?thesis
by (simp add: assms strict_sorted_equal)
qed

lemma sorted_list_of_set_UN_lessThan:
fixes k::nat
assumes sm: "strict_mono_sets {..<k} A" and "⋀i. i < k ⟹ finite (A i)"
shows "sorted_list_of_set (⋃i<k. A i) = concat (map (sorted_list_of_set ∘ A) (sorted_list_of_set {..<k}))"
using assms
proof (induction k)
case 0
then show ?case
by auto
next
case (Suc k)
have ls: "less_sets (⋃ (A ` {..<k})) (A k)"
using sm Suc.prems(1) strict_mono_setsD by (force simp: less_sets_UN1)
have "sorted_list_of_set (⋃ (A ` {..<Suc k})) = sorted_list_of_set (⋃ (A ` {..<k}) ∪ A k)"
by (simp add: Un_commute lessThan_Suc)
also have "… = sorted_list_of_set (⋃ (A ` {..<k})) @ sorted_list_of_set (A k)"
by (rule sorted_list_of_set_Un) (auto simp: Suc.prems ls)
also have "… = concat (map (sorted_list_of_set ∘ A) (sorted_list_of_set {..<k})) @ sorted_list_of_set (A k)"
using Suc strict_mono_sets_def by fastforce
also have "… = concat (map (sorted_list_of_set ∘ A) (sorted_list_of_set {..<Suc k}))"
using strict_mono_sets_def by fastforce
finally show ?case .
qed

lemma sorted_list_of_set_UN_atMost:
fixes k::nat
assumes "strict_mono_sets {..k} A" and "⋀i. i ≤ k ⟹ finite (A i)"
shows "sorted_list_of_set (⋃i≤k. A i) = concat (map (sorted_list_of_set ∘ A) (sorted_list_of_set {..k}))"
by (metis assms lessThan_Suc_atMost less_Suc_eq_le sorted_list_of_set_UN_lessThan)

subsection ‹Monotonic enumeration of a countably infinite set›

abbreviation "enum ≡ enumerate"

text ‹Could be generalised to infinite countable sets of any type›
lemma nat_infinite_iff:
fixes N :: "nat set"
shows "infinite N ⟷ (∃f::nat⇒nat. N = range f ∧ strict_mono f)"
proof safe
assume "infinite N"
then show "∃f. N = range (f::nat ⇒ nat) ∧ strict_mono f"
by (metis bij_betw_imp_surj_on bij_enumerate enumerate_mono strict_mono_def)
next
fix f :: "nat ⇒ nat"
assume "strict_mono f" and "N = range f" and "finite (range f)"
then show False
using range_inj_infinite strict_mono_imp_inj_on by blast
qed

lemma enum_works:
fixes N :: "nat set"
assumes "infinite N"
shows "N = range (enum N) ∧ strict_mono (enum N)"
by (metis assms bij_betw_imp_surj_on bij_enumerate enumerate_mono strict_monoI)

lemma range_enum: "range (enum N) = N" and strict_mono_enum: "strict_mono (enum N)"
if "infinite N" for N :: "nat set"
using enum_works [OF that] by auto

lemma enum_0_eq_Inf:
fixes N :: "nat set"
assumes "infinite N"
shows "enum N 0 = Inf N"
proof -
have "enum N 0 ∈ N"
using assms range_enum by auto
moreover have "⋀x. x ∈ N ⟹ enum N 0 ≤ x"
by (metis (mono_tags, opaque_lifting) assms imageE le0 less_mono_imp_le_mono range_enum strict_monoD strict_mono_enum)
ultimately show ?thesis
by (metis cInf_eq_minimum)
qed

lemma enum_works_finite:
fixes N :: "nat set"
assumes "finite N"
shows "N = enum N ` {..<card N} ∧ strict_mono_on {..<card N} (enum N)"
using assms
by (metis bij_betw_imp_surj_on finite_bij_enumerate finite_enumerate_mono lessThan_iff strict_mono_onI)

lemma enum_obtain_index_finite:
fixes N :: "nat set"
assumes "x ∈ N" "finite N"
obtains i where "i < card N" "x = enum N i"
by (metis ‹x ∈ N› ‹finite N› enum_works_finite imageE lessThan_iff)

lemma enum_0_eq_Inf_finite:
fixes N :: "nat set"
assumes "finite N" "N ≠ {}"
shows "enum N 0 = Inf N"
proof -
have "enum N 0 ∈ N"
by (metis Nat.neq0_conv assms empty_is_image enum_works_finite image_eqI lessThan_empty_iff lessThan_iff)
moreover have "enum N 0 ≤ x" if "x ∈ N" for x
proof -
obtain i where "i < card N" "x = enum N i"
by (metis ‹x ∈ N› ‹finite N› enum_obtain_index_finite)
with assms show ?thesis
by (metis Nat.neq0_conv finite_enumerate_mono less_or_eq_imp_le)
qed
ultimately show ?thesis
by (metis cInf_eq_minimum)
qed

lemma greaterThan_less_enum:
fixes N :: "nat set"
assumes "N ⊆ {x<..}" "infinite N"
shows "x < enum N i"
using assms range_enum by fastforce

lemma atLeast_le_enum:
fixes N :: "nat set"
assumes "N ⊆ {x..}" "infinite N"
shows "x ≤ enum N i"
using assms range_enum by fastforce

lemma less_sets_empty1 [simp]: "less_sets {} A" and less_sets_empty2 [simp]: "less_sets A {}"
by (simp_all add: less_sets_def)

lemma less_sets_singleton1 [simp]: "less_sets {a} A ⟷ (∀x∈A. a < x)"
and less_sets_singleton2 [simp]: "less_sets A {a} ⟷ (∀x∈A. x < a)"
by (simp_all add: less_sets_def)

lemma less_sets_atMost [simp]: "less_sets {..a} A ⟷ (∀x∈A. a < x)"
and less_sets_alLeast [simp]: "less_sets A {a..} ⟷ (∀x∈A. x < a)"
by (auto simp: less_sets_def)

lemma less_sets_imp_strict_mono_sets:
assumes "⋀i. less_sets (A i) (A (Suc i))" "⋀i. i>0 ⟹ A i ≠ {}"
shows "strict_mono_sets UNIV A"
proof (clarsimp simp: strict_mono_sets_def)
fix i j::nat
assume "i < j"
then show "less_sets (A i) (A j)"
proof (induction "j-i" arbitrary: i j)
case (Suc x)
then show ?case
by (metis Suc_diff_Suc Suc_inject Suc_mono assms less_Suc_eq less_sets_trans zero_less_Suc)
qed auto
qed

lemma less_sets_Suc_Max:
assumes "finite A"
shows "less_sets A {Suc (Max A)..}"
proof (cases "A = {}")
case False
then show ?thesis
by (simp add: assms less_Suc_eq_le)
qed auto

lemma infinite_nat_greaterThan:
fixes m::nat
assumes "infinite N"
shows "infinite (N ∩ {m<..})"
proof -
have "N ⊆ -{m<..} ∪ (N ∩ {m<..})"
by blast
moreover have "finite (-{m<..})"
by simp
ultimately show ?thesis
using assms finite_subset by blast
qed

end

```