section ‹Augmenting Flows›
theory Augmenting_Flow
imports ResidualGraph
begin
text ‹
In this theory, we define the concept of an augmenting flow,
augmentation with a flow, and show that augmentation of a flow
with an augmenting flow yields a valid flow again.
›
text ‹We assume that there is a network with a flow @{term f} on it›
context NFlow
begin
subsection ‹Augmentation of a Flow›
text ‹The flow can be augmented by another flow, by adding the flows
of edges parallel to edges in the network, and subtracting the edges
reverse to edges in the network.›
definition augment :: "'capacity flow => 'capacity flow"
where "augment f' ≡ λ(u, v).
if (u, v) ∈ E then
f (u, v) + f' (u, v) - f' (v, u)
else
0"
text ‹We define a syntax similar to Cormen et el.:›
abbreviation (input) augment_syntax (infix "\<up>" 55)
where "!!f f'. f\<up>f' ≡ NFlow.augment c f f'"
text ‹such that we can write @{term [source] "f\<up>f'"} for the flow @{term f}
augmented by @{term f'}.›
abbreviation (in Graph_Syntax) NFlow_augment :: "_ graph => _ flow => _ flow => _ flow"
("\<lbrace>_/ \<parallel>⇩N⇩F/ ⟨_/ \<up>/ _⟩\<rbrace>" 1000)
where "\<lbrace>c \<parallel>⇩N⇩F ⟨f \<up> f'⟩\<rbrace> ≡ NFlow.augment c f f'"
subsection ‹Augmentation yields Valid Flow›
text ‹We show that, if we augment the flow with a valid flow of
the residual graph, the augmented flow is a valid flow again, i.e.
it satisfies the capacity and conservation constraints:›
context
-- ‹Let the \emph{residual flow} @{term f'} be a flow in the residual graph›
fixes f' :: "'capacity flow"
assumes f'_flow: "Flow cf s t f'"
begin
interpretation f'!: Flow cf s t f' by (rule f'_flow)
subsubsection ‹Capacity Constraint›
text ‹First, we have to show that the new flow satisfies the capacity constraint:›
text_raw ‹\DefineSnippet{augment_flow_presv_cap}{›
lemma augment_flow_presv_cap:
shows "0 ≤ (f\<up>f')(u,v) ∧ (f\<up>f')(u,v) ≤ c(u,v)"
proof (cases "(u,v)∈E"; rule conjI)
assume [simp]: "(u,v)∈E"
hence "f(u,v) = cf(v,u)"
using no_parallel_edge by (auto simp: residualGraph_def)
also have "cf(v,u) ≥ f'(v,u)" using f'.capacity_const by auto
finally(xtrans) have "f'(v,u) ≤ f(u,v)" .
{
note [trans] = xtrans
text_raw ‹\isanewline›
text_raw ‹\ \ ›have "(f\<up>f')(u,v) = f(u,v) + f'(u,v) - f'(v,u)"
by (auto simp: augment_def)
also have "… ≥ f(u,v) + f'(u,v) - f(u,v)"
(is "_ ≥ …") using ‹f'(v,u) ≤ f(u,v)› by auto
also have "… = f'(u,v)" by auto
also have "… ≥ 0" using f'.capacity_const by auto
finally show "(f\<up>f')(u,v) ≥ 0" .
}
have "(f\<up>f')(u,v) = f(u,v) + f'(u,v) - f'(v,u)"
by (auto simp: augment_def)
also have "… ≤ f(u,v) + f'(u,v)" using f'.capacity_const by auto
also have "… ≤ f(u,v) + cf(u,v)" using f'.capacity_const by auto
also have "… = f(u,v) + c(u,v) - f(u,v)"
by (auto simp: residualGraph_def)
also have "… = c(u,v)" by auto
finally show "(f\<up>f')(u, v) ≤ c(u, v)" .
qed (auto simp: augment_def cap_positive)
text_raw ‹}%EndSnippet›
subsubsection ‹Conservation Constraint›
text ‹In order to show the conservation constraint, we need some
auxiliary lemmas first.›
text ‹As there are no parallel edges in the network, and all edges
in the residual graph are either parallel or reverse to a network edge,
we can split summations of the residual flow over outgoing/incoming edges in the
residual graph to summations over outgoing/incoming edges in the network.
›
private lemma split_rflow_outgoing:
"(∑v∈cf.E``{u}. f' (u,v)) = (∑v∈E``{u}. f'(u,v)) + (∑v∈E¯``{u}. f'(u,v))"
(is "?LHS = ?RHS")
proof -
from no_parallel_edge have DJ: "E``{u} ∩ E¯``{u} = {}" by auto
have "?LHS = (∑v∈E``{u} ∪ E¯``{u}. f' (u,v))"
apply (rule setsum.mono_neutral_left)
using cfE_ss_invE
by (auto intro: finite_Image)
also have "… = ?RHS"
apply (subst setsum.union_disjoint[OF _ _ DJ])
by (auto intro: finite_Image)
finally show "?LHS = ?RHS" .
qed
private lemma split_rflow_incoming:
"(∑v∈cf.E¯``{u}. f' (v,u)) = (∑v∈E``{u}. f'(v,u)) + (∑v∈E¯``{u}. f'(v,u))"
(is "?LHS = ?RHS")
proof -
from no_parallel_edge have DJ: "E``{u} ∩ E¯``{u} = {}" by auto
have "?LHS = (∑v∈E``{u} ∪ E¯``{u}. f' (v,u))"
apply (rule setsum.mono_neutral_left)
using cfE_ss_invE
by (auto intro: finite_Image)
also have "… = ?RHS"
apply (subst setsum.union_disjoint[OF _ _ DJ])
by (auto intro: finite_Image)
finally show "?LHS = ?RHS" .
qed
text ‹For proving the conservation constraint, let's fix a node @{term u}, which
is neither the source nor the sink: ›
context
fixes u :: node
assumes U_ASM: "u∈V - {s,t}"
begin
text ‹We first show an auxiliary lemma to compare the
effective residual flow on incoming network edges to
the effective residual flow on outgoing network edges.
Intuitively, this lemma shows that the effective residual flow added to the
network edges satisfies the conservation constraint.
›
private lemma flow_summation_aux:
shows "(∑v∈E``{u}. f' (u,v)) - (∑v∈E``{u}. f' (v,u))
= (∑v∈E¯``{u}. f' (v,u)) - (∑v∈E¯``{u}. f' (u,v))"
(is "?LHS = ?RHS" is "?A - ?B = ?RHS")
proof -
text ‹The proof is by splitting the flows, and careful
cancellation of the summands.›
have "?A = (∑v∈cf.E``{u}. f' (u, v)) - (∑v∈E¯``{u}. f' (u, v))"
by (simp add: split_rflow_outgoing)
also have "(∑v∈cf.E``{u}. f' (u, v)) = (∑v∈cf.E¯``{u}. f' (v, u))"
using U_ASM
by (simp add: f'.conservation_const_pointwise)
finally have "?A = (∑v∈cf.E¯``{u}. f' (v, u)) - (∑v∈E¯``{u}. f' (u, v))"
by simp
moreover
have "?B = (∑v∈cf.E¯``{u}. f' (v, u)) - (∑v∈E¯``{u}. f' (v, u))"
by (simp add: split_rflow_incoming)
ultimately show "?A - ?B = ?RHS" by simp
qed
text ‹Finally, we are ready to prove that the augmented flow satisfies the
conservation constraint:›
lemma augment_flow_presv_con:
shows "(∑e ∈ outgoing u. augment f' e) = (∑e ∈ incoming u. augment f' e)"
(is "?LHS = ?RHS")
proof -
text ‹We define shortcuts for the successor and predecessor nodes of @{term u}
in the network:›
let ?Vo = "E``{u}" let ?Vi = "E¯``{u}"
text ‹Using the auxiliary lemma for the effective residual flow,
the proof is straightforward:›
have "?LHS = (∑v∈?Vo. augment f' (u,v))"
by (auto simp: sum_outgoing_pointwise)
also have "…
= (∑v∈?Vo. f (u,v) + f'(u,v) - f'(v,u))"
by (auto simp: augment_def)
also have "…
= (∑v∈?Vo. f (u,v)) + (∑v∈?Vo. f' (u,v)) - (∑v∈?Vo. f' (v,u))"
by (auto simp: setsum_subtractf setsum.distrib)
also have "…
= (∑v∈?Vi. f (v,u)) + (∑v∈?Vi. f' (v,u)) - (∑v∈?Vi. f' (u,v))"
by (auto simp: conservation_const_pointwise[OF U_ASM] flow_summation_aux)
also have "…
= (∑v∈?Vi. f (v,u) + f' (v,u) - f' (u,v))"
by (auto simp: setsum_subtractf setsum.distrib)
also have "…
= (∑v∈?Vi. augment f' (v,u))"
by (auto simp: augment_def)
also have "…
= ?RHS"
by (auto simp: sum_incoming_pointwise)
finally show "?LHS = ?RHS" .
qed
text ‹Note that we tried to follow the proof presented by Cormen et al.~\cite{CLRS09}
as closely as possible. Unfortunately, this proof generalizes the summation to all
nodes immediately, rendering the first equation invalid.
Trying to fix this error, we encountered that the step that uses the conservation
constraints on the augmenting flow is more subtle as indicated in the original proof.
Thus, we moved this argument to an auxiliary lemma. ›
end -- ‹@{term u} is node›
text ‹As main result, we get that the augmented flow is again a valid flow.›
corollary augment_flow_presv: "Flow c s t (f\<up>f')"
using augment_flow_presv_cap augment_flow_presv_con
by unfold_locales auto
subsection ‹Value of the Augmented Flow›
text ‹Next, we show that the value of the augmented flow is the sum of the values
of the original flow and the augmenting flow.›
lemma augment_flow_value: "Flow.val c s (f\<up>f') = val + Flow.val cf s f'"
proof -
interpret f''!: Flow c s t "f\<up>f'" using augment_flow_presv[OF assms] .
txt ‹For this proof, we set up Isabelle's rewriting engine for rewriting of sums.
In particular, we add lemmas to convert sums over incoming or outgoing
edges to sums over all vertices. This allows us to write the summations
from Cormen et al.~a bit more concise, leaving some of the tedious
calculation work to the computer.›
note setsum_simp_setup[simp] =
sum_outgoing_alt[OF capacity_const] s_node
sum_incoming_alt[OF capacity_const]
cf.sum_outgoing_alt[OF f'.capacity_const]
cf.sum_incoming_alt[OF f'.capacity_const]
sum_outgoing_alt[OF f''.capacity_const]
sum_incoming_alt[OF f''.capacity_const]
setsum_subtractf setsum.distrib
txt ‹Note that, if neither an edge nor its reverse is in the graph,
there is also no edge in the residual graph, and thus the flow value
is zero.›
{
fix u v
assume "(u,v)∉E" "(v,u)∉E"
with cfE_ss_invE have "(u,v)∉cf.E" by auto
hence "f'(u,v) = 0" by auto
} note aux1 = this
txt ‹Now, the proposition follows by straightforward rewriting of
the summations:›
have "f''.val = (∑u∈V. augment f' (s, u) - augment f' (u, s))"
unfolding f''.val_def by simp
also have "… = (∑u∈V. f (s, u) - f (u, s) + (f' (s, u) - f' (u, s)))"
-- ‹Note that this is the crucial step of the proof, which Cormen et al. leave as an exercise.›
by (rule setsum.cong) (auto simp: augment_def no_parallel_edge aux1)
also have "… = val + Flow.val cf s f'"
unfolding val_def f'.val_def by simp
finally show ?thesis .
txt ‹Note, there is also an automatic proof. When creating the above
explicit proof, this automatic one has been used to extract meaningful
subgoals, abusing Isabelle as a term rewriter.›
have ?thesis
unfolding val_def f'.val_def f''.val_def
apply (simp del: setsum_simp_setup
add:
sum_outgoing_alt[OF capacity_const] s_node
sum_incoming_alt[OF capacity_const]
sum_outgoing_alt[OF f''.capacity_const]
sum_incoming_alt[OF f''.capacity_const]
cf.sum_outgoing_alt[OF f'.capacity_const]
cf.sum_incoming_alt[OF f'.capacity_const]
setsum_subtractf[symmetric] setsum.distrib[symmetric]
)
apply (rule setsum.cong)
apply (auto simp: augment_def no_parallel_edge aux1)
done
qed
end -- ‹Augmenting flow›
end -- ‹Network flow›
end -- ‹Theory›