Theory Flow_Networks.Ford_Fulkerson
section ‹The Ford-Fulkerson Theorem›
theory Ford_Fulkerson
imports Augmenting_Flow Augmenting_Path
begin
text ‹In this theory, we prove the Ford-Fulkerson theorem,
and its well-known corollary, the min-cut max-flow theorem.
›
text ‹We fix a network with a flow and a cut›
locale NFlowCut = NFlow c s t f + NCut c s t k
for c :: "'capacity::linordered_idom graph" and s t f k
begin
lemma finite_k[simp, intro!]: "finite k"
using cut_ss_V finite_V finite_subset[of k V] by blast
subsection ‹Net Flow›
text ‹We define the \emph{net flow} to be the amount of flow effectively
passed over the cut from the source to the sink:›
definition netFlow :: "'capacity"
where "netFlow ≡ (∑e ∈ outgoing' k. f e) - (∑e ∈ incoming' k. f e)"
text ‹We can show that the net flow equals the value of the flow.
Note: Cormen et al.~\<^cite>‹"CLRS09"› present a whole page full of
summation calculations for this proof, and our formal proof also
looks quite complicated.
›
lemma flow_value: "netFlow = val"
proof -
let ?LCL = "{(u, v). u ∈ k ∧ v ∈ k ∧ (u, v) ∈ E}"
let ?AOG = "{(u, v). u ∈ k ∧ (u, v) ∈ E}"
let ?AIN = "{(v, u) | u v. u ∈ k ∧ (v, u) ∈ E}"
let ?SOG = "λu. (∑e ∈ outgoing u. f e)"
let ?SIN = "λu. (∑e ∈ incoming u. f e)"
let ?SOG' = "(∑e ∈ outgoing' k. f e)"
let ?SIN' = "(∑e ∈ incoming' k. f e)"
text ‹Some setup to make finiteness reasoning implicit›
note [[simproc finite_Collect]]
have
"netFlow = ?SOG' + (∑e ∈ ?LCL. f e) - (?SIN' + (∑e ∈ ?LCL. f e))"
(is "_ = ?SAOG - ?SAIN")
using netFlow_def by auto
also have "?SAOG = (∑y ∈ k - {s}. ?SOG y) + ?SOG s"
proof -
have "?SAOG = (∑e∈(outgoing' k ∪ ?LCL). f e)"
by (rule sum.union_disjoint[symmetric]) (auto simp: outgoing'_def)
also have "outgoing' k ∪ ?LCL = (⋃y∈k-{s}. outgoing y) ∪ outgoing s"
by (auto simp: outgoing_def outgoing'_def s_in_cut)
also have "(∑e∈(⋃(outgoing ` (k - {s})) ∪ outgoing s). f e)
= (∑e∈(⋃(outgoing ` (k - {s}))). f e) + (∑e∈outgoing s. f e)"
by (rule sum.union_disjoint)
(auto simp: outgoing_def intro: finite_Image)
also have "(∑e∈(⋃(outgoing ` (k - {s}))). f e)
= (∑y ∈ k - {s}. ?SOG y)"
by (rule sum.UNION_disjoint)
(auto simp: outgoing_def intro: finite_Image)
finally show ?thesis .
qed
also have "?SAIN = (∑y ∈ k - {s}. ?SIN y) + ?SIN s"
proof -
have "?SAIN = (∑e∈(incoming' k ∪ ?LCL). f e)"
by (rule sum.union_disjoint[symmetric]) (auto simp: incoming'_def)
also have "incoming' k ∪ ?LCL = (⋃y∈k-{s}. incoming y) ∪ incoming s"
by (auto simp: incoming_def incoming'_def s_in_cut)
also have "(∑e∈(⋃(incoming ` (k - {s})) ∪ incoming s). f e)
= (∑e∈(⋃(incoming ` (k - {s}))). f e) + (∑e∈incoming s. f e)"
by (rule sum.union_disjoint)
(auto simp: incoming_def intro: finite_Image)
also have "(∑e∈(⋃(incoming ` (k - {s}))). f e)
= (∑y ∈ k - {s}. ?SIN y)"
by (rule sum.UNION_disjoint)
(auto simp: incoming_def intro: finite_Image)
finally show ?thesis .
qed
finally have "netFlow =
((∑y ∈ k - {s}. ?SOG y) + ?SOG s)
- ((∑y ∈ k - {s}. ?SIN y) + ?SIN s)"
(is "netFlow = ?R") .
also have "?R = ?SOG s - ?SIN s"
proof -
have "(⋀u. u ∈ k - {s} ⟹ ?SOG u = ?SIN u)"
using conservation_const cut_ss_V t_ni_cut by force
thus ?thesis by auto
qed
finally show ?thesis unfolding val_def by simp
qed
text ‹The value of any flow is bounded by the capacity of any cut.
This is intuitively clear, as all flow from the source to the sink has to go
over the cut.›
corollary weak_duality: "val ≤ cap"
proof -
have "(∑e ∈ outgoing' k. f e) ≤ (∑e ∈ outgoing' k. c e)" (is "?L ≤ ?R")
using capacity_const by (metis sum_mono)
then have "(∑e ∈ outgoing' k. f e) ≤ cap" unfolding cap_def by simp
moreover have "val ≤ (∑e ∈ outgoing' k. f e)" using netFlow_def
by (simp add: capacity_const flow_value sum_nonneg)
ultimately show ?thesis by simp
qed
end
subsection ‹Ford-Fulkerson Theorem›
context NFlow begin
text ‹We prove three auxiliary lemmas first, and the state the theorem as a corollary›
lemma fofu_I_II: "isMaxFlow f ⟹ ¬ (∃ p. isAugmentingPath p)"
unfolding isMaxFlow_alt
proof (rule ccontr)
assume asm: "NFlow c s t f
∧ (∀f'. NFlow c s t f' ⟶ Flow.val c s f' ≤ Flow.val c s f)"
assume asm_c: "¬ ¬ (∃ p. isAugmentingPath p)"
then obtain p where obt: "isAugmentingPath p" by blast
have fct1: "Flow cf s t (augmentingFlow p)" using obt augFlow_resFlow by auto
have fct2: "Flow.val cf s (augmentingFlow p) > 0" using obt augFlow_val
resCap_gzero isAugmentingPath_def cf.isSimplePath_def by auto
have "NFlow c s t (augment (augmentingFlow p))"
using fct1 augment_flow_presv Network_axioms
unfolding Flow_def NFlow_def NPreflow_def
by auto
moreover have "Flow.val c s (augment (augmentingFlow p)) > val"
using fct1 fct2 augment_flow_value by auto
ultimately show "False" using asm by auto
qed
lemma fofu_II_III:
"¬ (∃ p. isAugmentingPath p) ⟹ ∃k'. NCut c s t k' ∧ val = NCut.cap c k'"
proof (intro exI conjI)
let ?S = "cf.reachableNodes s"
assume asm: "¬ (∃ p. isAugmentingPath p)"
hence "t∉?S"
unfolding isAugmentingPath_def cf.reachableNodes_def cf.connected_def
by (auto dest: cf.isSPath_pathLE)
then show CUT: "NCut c s t ?S"
proof unfold_locales
show "Graph.reachableNodes cf s ⊆ V"
using cf.reachable_ss_V s_node resV_netV by auto
show "s ∈ Graph.reachableNodes cf s"
unfolding Graph.reachableNodes_def Graph.connected_def
by (metis Graph.isPath.simps(1) mem_Collect_eq)
qed
then interpret NCut c s t ?S .
interpret NFlowCut c s t f ?S by intro_locales
have "∀(u,v)∈outgoing' ?S. f (u,v) = c (u,v)"
proof (rule ballI, rule ccontr, clarify)
fix u v
assume "(u,v)∈outgoing' ?S"
hence "(u,v)∈E" "u∈?S" "v∉?S"
by (auto simp: outgoing'_def)
assume "f (u,v) ≠ c (u,v)"
hence "f (u,v) < c (u,v)"
using capacity_const by (metis (no_types) eq_iff not_le)
hence "cf (u, v) ≠ 0"
unfolding residualGraph_def using ‹(u,v)∈E› by auto
hence "(u, v) ∈ cf.E" unfolding cf.E_def by simp
hence "v∈?S" using ‹u∈?S› by (auto intro: cf.reachableNodes_append_edge)
thus False using ‹v∉?S› by auto
qed
hence "(∑e ∈ outgoing' ?S. f e) = cap"
unfolding cap_def by auto
moreover
have "∀(u,v)∈incoming' ?S. f (u,v) = 0"
proof (rule ballI, rule ccontr, clarify)
fix u v
assume "(u,v)∈incoming' ?S"
hence "(u,v)∈E" "u∉?S" "v∈?S" by (auto simp: incoming'_def)
hence "(v,u)∉E" using no_parallel_edge by auto
assume "f (u,v) ≠ 0"
hence "cf (v, u) ≠ 0"
unfolding residualGraph_def using ‹(u,v)∈E› ‹(v,u)∉E› by auto
hence "(v, u) ∈ cf.E" unfolding cf.E_def by simp
hence "u∈?S" using ‹v∈?S› cf.reachableNodes_append_edge by auto
thus False using ‹u∉?S› by auto
qed
hence "(∑e ∈ incoming' ?S. f e) = 0"
unfolding cap_def by auto
ultimately show "val = cap"
unfolding flow_value[symmetric] netFlow_def by simp
qed
lemma fofu_III_I:
"∃k. NCut c s t k ∧ val = NCut.cap c k ⟹ isMaxFlow f"
proof clarify
fix k
assume "NCut c s t k"
then interpret NCut c s t k .
interpret NFlowCut c s t f k by intro_locales
assume "val = cap"
{
fix f'
assume "Flow c s t f'"
then interpret fc': Flow c s t f' .
interpret fc': NFlowCut c s t f' k by intro_locales
have "fc'.val ≤ cap" using fc'.weak_duality .
also note ‹val = cap›[symmetric]
finally have "fc'.val ≤ val" .
}
thus "isMaxFlow f" unfolding isMaxFlow_def
by simp unfold_locales
qed
text ‹Finally we can state the Ford-Fulkerson theorem: ›
theorem ford_fulkerson: shows
"isMaxFlow f ⟷
¬ Ex isAugmentingPath" and "¬ Ex isAugmentingPath ⟷
(∃k. NCut c s t k ∧ val = NCut.cap c k)"
using fofu_I_II fofu_II_III fofu_III_I by auto
subsection ‹Corollaries›
text ‹In this subsection we present a few corollaries of the
flow-cut relation and the Ford-Fulkerson theorem.
›
text ‹The outgoing flow of the source is the same as the incoming flow of
the sink. Intuitively, this means that no flow is generated or lost in the
network, except at the source and sink.›
corollary inflow_t_outflow_s:
"(∑e ∈ incoming t. f e) = (∑e ∈ outgoing s. f e)"
proof -
txt ‹We choose a cut between the sink and all other nodes›
let ?K = "V - {t}"
interpret NFlowCut c s t f ?K
using s_node s_not_t by unfold_locales auto
txt ‹The cut is chosen such that its outgoing edges are the incoming edges
to the sink, and its incoming edges are the outgoing edges from the sink.
Note that the sink has no outgoing edges.›
have "outgoing' ?K = incoming t"
and "incoming' ?K = {}"
using no_self_loop no_outgoing_t
unfolding outgoing'_def incoming_def incoming'_def outgoing_def V_def
by auto
hence "(∑e ∈ incoming t. f e) = netFlow" unfolding netFlow_def by auto
also have "netFlow = val" by (rule flow_value)
also have "val = (∑e ∈ outgoing s. f e)" by (auto simp: val_alt)
finally show ?thesis .
qed
text ‹As an immediate consequence of the Ford-Fulkerson theorem, we get that
there is no augmenting path if and only if the flow is maximal.›
corollary noAugPath_iff_maxFlow: "(∄p. isAugmentingPath p) ⟷ isMaxFlow f"
using ford_fulkerson by blast
end
text ‹The value of the maximum flow equals the capacity of the minimum cut›
corollary (in Network) maxFlow_minCut: "⟦isMaxFlow f; isMinCut c s t k⟧
⟹ Flow.val c s f = NCut.cap c k"
proof -
assume "isMaxFlow f" "isMinCut c s t k"
then interpret Flow c s t f + NCut c s t k
unfolding isMaxFlow_def isMinCut_def by simp_all
interpret NFlowCut c s t f k by intro_locales
from ford_fulkerson ‹isMaxFlow f›
obtain k' where "NCut c s t k'" and "val = NCut.cap c k'"
by blast
thus "val = cap"
using ‹isMinCut c s t k› weak_duality
unfolding isMinCut_def by auto
qed
end