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