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