Theory Flow_Networks.Augmenting_Flow
section ‹Augmenting Flows›
theory Augmenting_Flow
imports Residual_Graph
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 "↑" 55)
where "⋀f f'. f↑f' ≡ NFlow.augment c f f'"
text ‹such that we can write @{term [source] "f↑f'"} for the flow @{term f}
augmented by @{term 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
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↑f')(u,v) ∧ (f↑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↑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↑f')(u,v) ≥ 0" .
}
have "(f↑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↑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.
Note that the term @{term ‹E``{u}›} characterizes the successor nodes of @{term ‹u›},
and @{term ‹E¯``{u}›} characterizes the predecessor nodes of @{term ‹u›}.
›
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 sum.mono_neutral_left)
using cfE_ss_invE
by (auto intro: finite_Image)
also have "… = ?RHS"
apply (subst sum.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 sum.mono_neutral_left)
using cfE_ss_invE
by (auto intro: finite_Image)
also have "… = ?RHS"
apply (subst sum.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: sum_subtractf sum.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: sum_subtractf sum.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
text ‹As main result, we get that the augmented flow is again a valid flow.›
corollary augment_flow_presv: "Flow c s t (f↑f')"
using augment_flow_presv_cap augment_flow_presv_con
by (rule_tac intro_Flow) 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↑f') = val + Flow.val cf s f'"
proof -
interpret f'': Flow c s t "f↑f'" using augment_flow_presv .
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 sum_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]
sum_subtractf sum.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.›
have aux1: "f'(u,v) = 0" if "(u,v)∉E" "(v,u)∉E" for u v
proof -
from that cfE_ss_invE have "(u,v)∉cf.E" by auto
thus "f'(u,v) = 0" by auto
qed
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)))"
by (rule sum.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 "f''.val = val + f'.val" .
qed
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.›
lemma "Flow.val c s (f↑f') = val + Flow.val cf s f'"
proof -
interpret f'': Flow c s t "f↑f'" using augment_flow_presv .
have aux1: "f'(u,v) = 0" if A: "(u,v)∉E" "(v,u)∉E" for u v
proof -
from A cfE_ss_invE have "(u,v)∉cf.E" by auto
thus "f'(u,v) = 0" by auto
qed
show ?thesis
unfolding val_def f'.val_def f''.val_def
apply (simp del:
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]
sum_subtractf[symmetric] sum.distrib[symmetric]
)
apply (rule sum.cong)
apply (auto simp: augment_def no_parallel_edge aux1)
done
qed
end
end
end