# Theory SetUtils

```theory SetUtils
imports Main
begin

― ‹TODO use Inf instead of Min where necessary.›

― ‹TODO can be replaced by @{term "card_Un_disjoint (⟦finite A; finite B; A ∩ B = {}⟧
⟹ card (A ∪ B) = card A + card B)"} ?›
lemma card_union': "(finite s) ∧ (finite t) ∧ (disjnt s t) ⟹ (card (s ∪ t) = card s + card t)"

lemma CARD_INJ_IMAGE_2:
fixes f s
assumes "finite s" "(∀x y. ((x ∈ s) ∧ (y ∈ s)) ⟶ ((f x = f y) ⟷ (x = y)))"
shows "(card (f ` s) = card s)"
proof -
{
fix x y
assume "x ∈ s" "y ∈ s"
then have "f x = f y ⟶ x = y"
using assms(2)
by blast
}
then have "inj_on f s"
then show ?thesis
using assms(1) inj_on_iff_eq_card
by blast
qed

lemma scc_main_lemma_x: "⋀s t x. (x ∈ s) ∧ ¬(x ∈ t) ⟹ ¬(s = t)"
by blast

lemma neq_funs_neq_images:
fixes s
assumes "∀x. x ∈ s ⟶ (∀y. y ∈ s ⟶ f1 x ≠ f2 y)" "∃x. x ∈ s"
shows "f1 ` s ≠ f2 ` s"
using assms
by blast

subsection "Sets of Numbers"

― ‹TODO
Is '<=' natural number lte or overloaded?
If it's overloaded for reals, this might be wrong (e.g. the real set s = [0; 1] is not finite even
though @{term "∀ x ∈ s. x ≤ 1"} holds).›
lemma mems_le_finite_i:
fixes s :: "nat set" and k :: nat
shows "(∀ x. x ∈ s ⟶ x ≤ k) ⟹ finite s"
proof -
assume P: "(∀ x. x ∈ s ⟶ x ≤ k)"
let ?f = "id :: nat ⇒ nat"
let ?S = "{i. i ≤ k}"
have "s ⊆ ?S" using P by blast
moreover have "?f ` ?S = ?S" by auto
moreover have "finite ?S" using nat_seg_image_imp_finite by auto
moreover have "finite s" using calculation finite_subset by auto
ultimately show ?thesis by auto
qed
lemma mems_le_finite:
fixes s :: "nat set" and k :: nat
shows "⋀(s :: nat set) k. (∀ x. x ∈ s ⟶ x ≤ k) ⟹ finite s"
using mems_le_finite_i by auto

― ‹NOTE translated `s` to `nat set` (more generality wasn't required.).›
lemma mem_le_imp_MIN_le:
fixes s :: "nat set" and k :: nat
assumes "∃x. (x ∈ s) ∧ (x ≤ k)"
shows "(Inf s ≤ k)"
proof -
from assms obtain x where 1: "x ∈ s" "x ≤ k"
by blast
{
assume C: "Inf s > k"
then have "Inf s > x" using 1(2)
by fastforce
then have False
using 1(1) cInf_lower leD
by fast
}
then show ?thesis
by fastforce
qed

― ‹NOTE
nat --> bool is the type of a HOL4 set and was translated to 'nat set'.›
― ‹NOTE
We cannot use 'Min' instead of 'Inf' because there is no indication that '{n. s n}' will be
finite. Without that @{term "Min {n. s n} ∈ {n. s n}"} is not necessarily true.›
lemma mem_lt_imp_MIN_lt:
fixes s :: "nat set" and k :: nat
assumes "(∃x. x ∈ s ∧ x < k)"
shows "(Inf s) < k"
proof -
obtain x where 1: "x ∈ s" "x < k"
using assms
by blast
then have 2: "s ≠ {}"
by blast
then have "Inf s ∈ s"
using Inf_nat_def LeastI
by force
moreover have "∀x∈s. Inf s ≤ x"
ultimately show "(Inf s) < k"
using assms leD
by force
qed

― ‹NOTE type for 'k' had to be fixed (type unordered error; also not true for e.g. real sets).›
lemma bound_child_parent_neq_mems_state_set_neq_len:
fixes s and k :: nat
assumes "(∀x. x ∈ s ⟶ x < k)"
shows "finite s"
using assms bounded_nat_set_is_finite
by blast

lemma bound_main_lemma_2: "⋀(s :: nat set) k. (s ≠ {}) ∧ (∀x. x ∈ s ⟶ x ≤ k) ⟹ Sup s ≤ k"
proof -
fix s :: "nat set" and k
{
assume P1: "s ≠ {}"
assume P2: "(∀x. x ∈ s ⟶ x ≤ k)"
have "finite s" using P2 mems_le_finite by auto
moreover have "Max s ∈ s" using P1 calculation Max_in by auto
moreover have "Max s ≤ k" using P2 calculation by auto
}
then show "(s ≠ {}) ∧ (∀x. x ∈ s ⟶ x ≤ k) ⟹ Sup s ≤ k"
qed

― ‹NOTE type of 'k' fixed to nat to be able to use 'bound\_child\_parent\_neq\_mems\_state\_set\_neq\_len'.›
lemma bound_child_parent_not_eq_last_diff_paths: "⋀s (k :: nat).
(s ≠ {})
⟹ (∀x. x ∈ s ⟶ x < k)
⟹ Sup s < k
"

lemma FINITE_ALL_DISTINCT_LISTS_i:
fixes P
assumes "finite P"
shows "
{p. distinct p ∧ set p ⊆ P}
= {[]} ∪ (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P))"
proof -
let ?A="{p. distinct p ∧ set p ⊆ P }"
let ?B="{[]} ∪ (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P))"
{
{
fix a
assume P: "a ∈ ?A"
then have "a ∈ ?B"
proof (cases a)
text ‹ The empty list is distinct and its corresponding set is the empty set which is a
trivial subset of `?B`. The `Nil` case can therefore be derived by automation. ›
case (Cons h list)
{
let ?b'="h"
{
from P have "set a ⊆ P"
by simp
then have "set list ⊆ (P - {h})"
using P dual_order.trans local.Cons
by auto
}
moreover from P Cons
have "distinct list"
by force
ultimately have "a ∈ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ?b')"
using Cons
by blast
moreover {
from P Cons have "?b' ∈ set a"
by simp
moreover from P have "set a ⊆ P"
by simp
ultimately have "?b' ∈ P"
by auto
}
ultimately have
"∃b' ∈ P. a ∈ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) b')"
by meson
}
then obtain b' where
"b' ∈ P" "a ∈ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) b')"
by blast
then show ?thesis
by blast
qed blast
}
then have "?A ⊆ ?B"
by auto
}
moreover {
{
fix b
assume P: "b ∈ ?B"
have "b ∈ ?A"
text ‹ The empty list is in `?B` by construction. The `Nil` case can therefore be derived
straightforwardly.›
proof (cases b)
case (Cons a list)
from P Cons obtain b' where a:
"b' ∈ P" "b ∈ {b' # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {b'})}"
by fast
then obtain p0 where b: "b = b' # p0" "distinct p0" "set p0 ⊆ (P - {b'})"
by blast
then have "distinct (b' # p0)"
moreover have "set (b' # p0) ⊆ P"
using a(1) b(3)
by auto
ultimately show ?thesis
using b(1)
by fast
qed simp
}
then have "?B ⊆ ?A"
by blast
}
ultimately show ?thesis
using set_eq_subset
by blast
qed

lemma FINITE_ALL_DISTINCT_LISTS:
fixes P
assumes "finite P"
shows "finite {p. distinct p ∧ set p ⊆ P}"
using assms
proof (induction "card P" arbitrary: P)
case 0
then have "P = {}"
by force
then show ?case
using 0
by simp
next
case (Suc x)
{
text ‹ Proof the finiteness of the union by proving both sets of the union are finite. The
singleton set `{[]}` is trivially finite. ›
{
{
fix e
assume P: "e ∈ P"
have "
{e # p0 | p0. distinct p0 ∧ set p0 ⊆ P - {e}}
= (λp. e # p) ` { p. distinct p ∧ set p ⊆ P - {e}}"
by blast
moreover {
let ?P'="P - {e}"
from Suc.prems
have "finite ?P'"
by blast
text ‹ The finiteness can now be shown using the induction hypothesis. However `e` might
already be contained in `?P`, so we have to split cases first. ›
have "finite ((λp. e # p) ` {p. distinct p ∧ set p ⊆ ?P'})"
proof (cases "e ∈ P")
case True
then have "x = card ?P'" using Suc.prems Suc(2)
by fastforce
moreover from Suc.prems
have "finite ?P'"
by blast
ultimately show ?thesis
using Suc(1)
by blast
next
case False
then have "?P' = P"
by simp
then have "finite {p. distinct p ∧ set p ⊆ ?P'}"
using False P by linarith
then show ?thesis
using finite_imageI
by blast
qed
}
ultimately have "finite {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}"
by argo
}
then have "finite (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P))"
using Suc.prems
by blast
}
then have
"finite ({[]} ∪ (⋃ ((λe. {e # p0 | p0. distinct p0 ∧ set p0 ⊆ (P - {e})}) ` P)))"
using finite_Un
by blast
}
then show ?case
using FINITE_ALL_DISTINCT_LISTS_i[OF Suc.prems]
by force
qed

lemma subset_inter_diff_empty:
assumes "s ⊆ t"
shows "(s ∩ (u - t) = {})"
using assms
by auto

end```