# Theory Helpers

section ‹Helpers›
theory Helpers imports Main begin
text ‹
First, we will prove a few lemmas unrelated to graphs or Menger's Theorem. These lemmas
will simplify some of the other proof steps.
›
text ‹
If two finite sets have different cardinality, then there exists an element in the larger set
that is not in the smaller set.
›
lemma card_finite_less_ex:
assumes finite_A: "finite A"
and finite_B: "finite B"
and card_AB: "card A < card B"
shows "∃b ∈ B. b ∉ A"
proof-
have "card (B - A) > 0" using finite_A finite_B card_AB
by (meson Diff_eq_empty_iff card_eq_0_iff card_mono finite_Diff gr0I leD)
then show ?thesis using finite_B
by (metis Diff_eq_empty_iff card_0_eq finite_Diff neq_iff subsetI)
qed
text ‹
The cardinality of the union of two disjoint finite sets is the sum of their cardinalities
even if we intersect everything with a fixed set @{term X}.
›
lemma card_intersect_sum_disjoint:
assumes "finite B" "finite C" "A = B ∪ C" "B ∩ C = {}"
shows "card (A ∩ X) = card (B ∩ X) + card (C ∩ X)"
by (metis (no_types, lifting) Un_Diff_Int assms card_Un_disjoint finite_Int inf.commute
inf_sup_distrib2 sup_eq_bot_iff)
text ‹
If @{term x} is in a list @{term xs} but is not its last element, then it is also in
@{term "butlast xs"}.
›
lemma set_butlast: "⟦ x ∈ set xs; x ≠ last xs ⟧ ⟹ x ∈ set (butlast xs)"
by (metis butlast.simps(2) in_set_butlast_appendI last.simps last_appendR
list.set_intros(1) split_list_first)
text ‹
If a property @{term P} is satisfiable and if we have a weight measure mapping into the natural
numbers, then there exists an element of minimum weight satisfying @{term P} because the
natural numbers are well-ordered.
›
lemma arg_min_ex:
fixes P :: "'a ⇒ bool" and weight :: "'a ⇒ nat"
assumes "∃x. P x"
obtains x where "P x" "⋀y. P y ⟹ weight x ≤ weight y"
proof (cases "∃x. P x ∧ weight x = 0")
case True then show ?thesis using that by auto
next
case False then show ?thesis
using that ex_least_nat_le[of "λn. ∃x. P x ∧ weight x = n"] assms by (metis not_le_imp_less)
qed
end