Theory Max_Flow_Min_Cut_Countable

(* Author: Andreas Lochbihler, ETH Zurich & Digital Asset *)

theory Max_Flow_Min_Cut_Countable imports
  MFMC_Bounded
  MFMC_Unbounded
begin

section ‹The Max-Flow Min-Cut theorem›

theorem max_flow_min_cut_countable:
  fixes Δ (structure)
  assumes countable_E [simp]: "countable ❙E"
  and source_neq_sink [simp]: "source Δ ≠ sink Δ"
  and capacity_outside: "∀e. e ∉ ❙E ⟶ capacity Δ e = 0"
  and capacity_finite [simp]: "∀e. capacity Δ e ≠ ⊤"
  shows "∃f S. flow Δ f ∧ cut Δ S ∧ orthogonal Δ f S"
proof -
  interpret countable_network Δ using assms by(unfold_locales) auto
  show ?thesis by(rule max_flow_min_cut)
qed

hide_const (open) A B weight

end