# Theory Set_Extensions

```section ‹Sets›

theory Set_Extensions
imports
"HOL-Library.Infinite_Set"
begin

declare finite_subset[intro]

lemma set_not_emptyI[intro 0]: "x ∈ S ⟹ S ≠ {}" by auto
lemma sets_empty_iffI[intro 0]:
assumes "⋀ a. a ∈ A ⟹ ∃ b. b ∈ B"
assumes "⋀ b. b ∈ B ⟹ ∃ a. a ∈ A"
shows "A = {} ⟷ B = {}"
using assms by auto
lemma disjointI[intro 0]:
assumes "⋀ x. x ∈ A ⟹ x ∈ B ⟹ False"
shows "A ∩ B = {}"
using assms by auto
lemma range_subsetI[intro 0]:
assumes "⋀ x. f x ∈ S"
shows "range f ⊆ S"
using assms by blast

lemma finite_imageI_range:
assumes "finite (range f)"
shows "finite (f ` A)"
using finite_subset image_mono subset_UNIV assms by metis

lemma inf_img_fin_domE':
assumes "infinite A"
assumes "finite (f ` A)"
obtains y
where "y ∈ f ` A" "infinite (A ∩ f -` {y})"
proof (rule ccontr)
assume 1: "¬ thesis"
have 2: "finite (⋃ y ∈ f ` A. A ∩ f -` {y})"
proof (rule finite_UN_I)
show "finite (f ` A)" using assms(2) by this
show "⋀ y. y ∈ f ` A ⟹ finite (A ∩ f -` {y})" using that 1 by blast
qed
have 3: "A ⊆ (⋃ y ∈ f ` A. A ∩ f -` {y})" by blast
show False using assms(1) 2 3 by blast
qed

lemma vimage_singleton[simp]: "f -` {y} = {x. f x = y}" unfolding vimage_def by simp

lemma these_alt_def: "Option.these S = Some -` S" unfolding Option.these_def by force
lemma the_vimage_subset: "the -` {a} ⊆ {None, Some a}" by auto

lemma finite_induct_reverse[consumes 1, case_names remove]:
assumes "finite S"
assumes "⋀ S. finite S ⟹ (⋀ x. x ∈ S ⟹ P (S - {x})) ⟹ P S"
shows "P S"
using assms(1)
proof (induct rule: finite_psubset_induct)
case (psubset S)
show ?case
proof (rule assms(2))
show "finite S" using psubset(1) by this
next
fix x
assume 0: "x ∈ S"
show "P (S - {x})"
proof (rule psubset(2))
show "S - {x} ⊂ S" using 0 by auto
qed
qed
qed

lemma zero_not_in_Suc_image[simp]: "0 ∉ Suc ` A" by auto

lemma Collect_split_Suc:
"¬ P 0 ⟹ {i. P i} = Suc ` {i. P (Suc i)}"
"P 0 ⟹ {i. P i} = {0} ∪ Suc ` {i. P (Suc i)}"
proof -
assume "¬ P 0"
thus "{i. P i} = Suc ` {i. P (Suc i)}"
by (auto, metis image_eqI mem_Collect_eq nat.exhaust)
next
assume "P 0"
thus "{i. P i} = {0} ∪ Suc ` {i. P (Suc i)}"
by (auto, metis imageI mem_Collect_eq not0_implies_Suc)
qed

lemma Collect_subsume[simp]:
assumes "⋀ x. x ∈ A ⟹ P x"
shows "{x ∈ A. P x} = A"
using assms unfolding simp_implies_def by auto

lemma Max_ge':
assumes "finite A" "A ≠ {}"
assumes "b ∈ A" "a ≤ b"
shows "a ≤ Max A"
using assms Max_ge_iff by auto

abbreviation "least A ≡ LEAST k. k ∈ A"

lemma least_contains[intro?, simp]:
fixes A :: "'a :: wellorder set"
assumes "k ∈ A"
shows "least A ∈ A"
using assms by (metis LeastI)
lemma least_contains'[intro?, simp]:
fixes A :: "'a :: wellorder set"
assumes "A ≠ {}"
shows "least A ∈ A"
using assms by (metis LeastI equals0I)
lemma least_least[intro?, simp]:
fixes A :: "'a :: wellorder set"
assumes "k ∈ A"
shows "least A ≤ k"
using assms by (metis Least_le)
lemma least_unique:
fixes A :: "'a :: wellorder set"
assumes "k ∈ A" "k ≤ least A"
shows "k = least A"
using assms by (metis Least_le antisym)
lemma least_not_less:
fixes A :: "'a :: wellorder set"
assumes "k < least A"
shows "k ∉ A"
using assms by (metis not_less_Least)
lemma leastI2_order[simp]:
fixes A :: "'a :: wellorder set"
assumes "A ≠ {}" "⋀ k. k ∈ A ⟹ (⋀ l. l ∈ A ⟹ k ≤ l) ⟹ P k"
shows "P (least A)"
proof (rule LeastI2_order)
show "least A ∈ A" using assms(1) by rule
next
fix k
assume 1: "k ∈ A"
show "least A ≤ k" using 1 by rule
next
fix k
assume 1: "k ∈ A" "∀ l. l ∈ A ⟶ k ≤ l"
show "P k" using assms(2) 1 by auto
qed

lemma least_singleton[simp]:
fixes a :: "'a :: wellorder"
shows "least {a} = a"
by (metis insert_not_empty least_contains' singletonD)

lemma least_image[simp]:
fixes f :: "'a :: wellorder ⇒ 'b :: wellorder"
assumes "A ≠ {}" "⋀ k l. k ∈ A ⟹ l ∈ A ⟹ k ≤ l ⟹ f k ≤ f l"
shows "least (f ` A) = f (least A)"
proof (rule leastI2_order)
show "A ≠ {}" using assms(1) by this
next
fix k
assume 1: "k ∈ A" "⋀ i. i ∈ A ⟹ k ≤ i"
show "least (f ` A) = f k"
proof (rule leastI2_order)
show "f ` A ≠ {}" using assms(1) by simp
next
fix l
assume 2: "l ∈ f ` A" "⋀ i. i ∈ f ` A ⟹ l ≤ i"
show "l = f k" using assms(2) 1 2 by force
qed
qed

lemma least_le:
fixes A B :: "'a :: wellorder set"
assumes "B ≠ {}"
assumes "⋀ i. i ≤ least A ⟹ i ≤ least B ⟹ i ∈ B ⟹ i ∈ A"
shows "least A ≤ least B"
proof (rule ccontr)
assume 1: "¬ least A ≤ least B"
have 2: "least B ∈ A" using assms(1, 2) 1 by simp
have 3: "least A ≤ least B" using 2 by rule
show False using 1 3 by rule
qed
lemma least_eq:
fixes A B :: "'a :: wellorder set"
assumes "A ≠ {}" "B ≠ {}"
assumes "⋀ i. i ≤ least A ⟹ i ≤ least B ⟹ i ∈ A ⟷ i ∈ B"
shows "least A = least B"
using assms by (auto intro: antisym least_le)

lemma least_Suc[simp]:
assumes "A ≠ {}"
shows "least (Suc ` A) = Suc (least A)"
proof (rule antisym)
obtain k where 10: "k ∈ A" using assms by blast
have 11: "Suc k ∈ Suc ` A" using 10 by auto
have 20: "least A ∈ A" using 10 LeastI by metis
have 21: "least (Suc ` A) ∈ Suc ` A" using 11 LeastI by metis
have 30: "⋀ l. l ∈ A ⟹ least A ≤ l" using 10 Least_le by metis
have 31: "⋀ l. l ∈ Suc ` A ⟹ least (Suc ` A) ≤ l" using 11 Least_le by metis
show "least (Suc ` A) ≤ Suc (least A)" using 20 31 by auto
show "Suc (least A) ≤ least (Suc ` A)" using 21 30 by auto
qed

lemma least_Suc_diff[simp]: "Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})"
proof (cases "A = {}")
case True
show ?thesis unfolding True by simp
next
case False
have "Suc ` A - {least (Suc ` A)} = Suc ` A - {Suc (least A)}" using False by simp
also have "… = Suc ` A - Suc ` {least A}" by simp
also have "… = Suc ` (A - {least A})" by blast
finally show ?thesis by this
qed

lemma Max_diff_least[simp]:
fixes A :: "'a :: wellorder set"
assumes "finite A" "A - {least A} ≠ {}"
shows "Max (A - {least A}) = Max A"
proof -
have 1: "least A ∈ A" using assms(2) by auto
obtain a where 2: "a ∈ A - {least A}" using assms(2) by blast
have "Max A = Max (insert (least A) (A - {least A}))" using insert_absorb 1 by force
also have "… = max (least A) (Max (A - {least A}))"
proof (rule Max_insert)
show "finite (A - {least A})" using assms(1) by auto
show "A - {least A} ≠ {}" using assms(2) by this
qed
also have "… = Max (A - {least A})"
proof (rule max_absorb2, rule Max_ge')
show "finite (A - {least A})" using assms(1) by auto
show "A - {least A} ≠ {}" using assms(2) by this
show "a ∈ A - {least A}" using 2 by this
show "least A ≤ a" using 2 by simp
qed
finally show ?thesis by rule
qed

lemma nat_set_card_equality_less:
fixes A :: "nat set"
assumes "x ∈ A" "y ∈ A" "card {z ∈ A. z < x} = card {z ∈ A. z < y}"
shows "x = y"
proof (cases x y rule: linorder_cases)
case less
have 0: "finite {z ∈ A. z < y}" by simp
have 1: "{z ∈ A. z < x} ⊂ {z ∈ A. z < y}" using assms(1, 2) less by force
have 2: "card {z ∈ A. z < x} < card {z ∈ A. z < y}" using psubset_card_mono 0 1 by this
show ?thesis using assms(3) 2 by simp
next
case equal
show ?thesis using equal by this
next
case greater
have 0: "finite {z ∈ A. z < x}" by simp
have 1: "{z ∈ A. z < y} ⊂ {z ∈ A. z < x}" using assms(1, 2) greater by force
have 2: "card {z ∈ A. z < y} < card {z ∈ A. z < x}" using psubset_card_mono 0 1 by this
show ?thesis using assms(3) 2 by simp
qed

lemma nat_set_card_equality_le:
fixes A :: "nat set"
assumes "x ∈ A" "y ∈ A" "card {z ∈ A. z ≤ x} = card {z ∈ A. z ≤ y}"
shows "x = y"
proof (cases x y rule: linorder_cases)
case less
have 0: "finite {z ∈ A. z ≤ y}" by simp
have 1: "{z ∈ A. z ≤ x} ⊂ {z ∈ A. z ≤ y}" using assms(1, 2) less by force
have 2: "card {z ∈ A. z ≤ x} < card {z ∈ A. z ≤ y}" using psubset_card_mono 0 1 by this
show ?thesis using assms(3) 2 by simp
next
case equal
show ?thesis using equal by this
next
case greater
have 0: "finite {z ∈ A. z ≤ x}" by simp
have 1: "{z ∈ A. z ≤ y} ⊂ {z ∈ A. z ≤ x}" using assms(1, 2) greater by force
have 2: "card {z ∈ A. z ≤ y} < card {z ∈ A. z ≤ x}" using psubset_card_mono 0 1 by this
show ?thesis using assms(3) 2 by simp
qed

lemma nat_set_card_mono[simp]:
fixes A :: "nat set"
assumes "x ∈ A"
shows "card {z ∈ A. z < x} < card {z ∈ A. z < y} ⟷ x < y"
proof
assume 1: "card {z ∈ A. z < x} < card {z ∈ A. z < y}"
show "x < y"
proof (rule ccontr)
assume 2: "¬ x < y"
have 3: "card {z ∈ A. z < y} ≤ card {z ∈ A. z < x}" using 2 by (auto intro: card_mono)
show "False" using 1 3 by simp
qed
next
assume 1: "x < y"
show "card {z ∈ A. z < x} < card {z ∈ A. z < y}"
proof (intro psubset_card_mono psubsetI)
show "finite {z ∈ A. z < y}" by simp
show "{z ∈ A. z < x} ⊆ {z ∈ A. z < y}" using 1 by auto
show "{z ∈ A. z < x} ≠ {z ∈ A. z < y}" using assms 1 by blast
qed
qed

lemma card_one[elim]:
assumes "card A = 1"
obtains a
where "A = {a}"
using assms by (metis One_nat_def card_Suc_eq)

lemma image_alt_def: "f ` A = {f x |x. x ∈ A}" by auto

lemma supset_mono_inductive[mono]:
assumes "⋀ x. x ∈ B ⟶ x ∈ C"
shows "A ⊆ B ⟶ A ⊆ C"
using assms by auto
lemma Collect_mono_inductive[mono]:
assumes "⋀ x. P x ⟶ Q x"
shows "x ∈ {x. P x} ⟶ x ∈ {x. Q x}"
using assms by auto

lemma image_union_split:
assumes "f ` (A ∪ B) = g ` C"
obtains D E
where "f ` A = g ` D" "f ` B = g ` E" "D ⊆ C" "E ⊆ C"
using assms unfolding image_Un
by (metis (erased, lifting) inf_sup_ord(3) inf_sup_ord(4) subset_imageE)
lemma image_insert_split:
assumes "inj g" "f ` insert a B = g ` C"
obtains d E
where "f a = g d" "f ` B = g ` E" "d ∈ C" "E ⊆ C"
proof -
have 1: "f ` ({a} ∪ B) = g ` C" using assms(2) by simp
obtain D E where 2: "f ` {a} = g ` D" "f ` B = g ` E" "D ⊆ C" "E ⊆ C"
using image_union_split 1 by this
obtain d where 3: "D = {d}" using assms(1) 2(1) by (auto, metis (erased, opaque_lifting) imageE
image_empty image_insert inj_image_eq_iff singletonI)
show ?thesis using that 2 unfolding 3 by simp
qed

end```