section ‹Augmenting Paths›
theory Augmenting_Path
imports Residual_Graph
begin
text ‹We define the concept of an augmenting path in the residual graph,
and the residual flow induced by an augmenting path.›
text ‹We fix a network with a preflow @{term f} on it.›
context NPreflow
begin
subsection ‹Definitions›
text ‹An \emph{augmenting path} is a simple path from the source to the sink in the residual graph:›
definition isAugmentingPath :: "path ⇒ bool"
where "isAugmentingPath p ≡ cf.isSimplePath s p t"
text ‹The \emph{residual capacity} of an augmenting path is the smallest capacity
annotated to its edges:›
definition resCap :: "path ⇒ 'capacity"
where "resCap p ≡ Min {cf e | e. e ∈ set p}"
lemma resCap_alt: "resCap p = Min (cf`set p)"
unfolding resCap_def apply (rule arg_cong[where f=Min]) by auto
text ‹An augmenting path induces an \emph{augmenting flow}, which pushes as
much flow as possible along the path:›
definition augmentingFlow :: "path ⇒ 'capacity flow"
where "augmentingFlow p ≡ λ(u, v).
if (u, v) ∈ (set p) then
resCap p
else
0"
subsection ‹Augmenting Flow is Valid Flow›
text ‹In this section, we show that the augmenting flow induced by an
augmenting path is a valid flow in the residual graph.
We start with some auxiliary lemmas.›
text ‹The residual capacity of an augmenting path is always positive.›
lemma resCap_gzero_aux: "cf.isPath s p t ⟹ 0<resCap p"
proof -
assume PATH: "cf.isPath s p t"
hence "set p≠{}" using s_not_t by (auto)
moreover have "∀e∈set p. cf e > 0"
using cf.isPath_edgeset[OF PATH] resE_positive by (auto)
ultimately show ?thesis unfolding resCap_alt by (auto)
qed
lemma resCap_gzero: "isAugmentingPath p ⟹ 0<resCap p"
using resCap_gzero_aux[of p]
by (auto simp: isAugmentingPath_def cf.isSimplePath_def)
text ‹As all edges of the augmenting flow have the same value, we can factor
this out from a summation:›
lemma sum_augmenting_alt:
assumes "finite A"
shows "(∑e ∈ A. (augmentingFlow p) e)
= resCap p * of_nat (card (A∩set p))"
proof -
have "(∑e ∈ A. (augmentingFlow p) e) = sum (λ_. resCap p) (A∩set p)"
apply (subst sum.inter_restrict)
apply (auto simp: augmentingFlow_def assms)
done
thus ?thesis by auto
qed
lemma augFlow_resFlow: "isAugmentingPath p ⟹ Flow cf s t (augmentingFlow p)"
proof (rule cf.intro_Flow; intro allI ballI)
assume AUG: "isAugmentingPath p"
hence SPATH: "cf.isSimplePath s p t" by (simp add: isAugmentingPath_def)
hence PATH: "cf.isPath s p t" by (simp add: cf.isSimplePath_def)
{ text ‹We first show the capacity constraint›
fix e
show "0 ≤ (augmentingFlow p) e ∧ (augmentingFlow p) e ≤ cf e"
proof cases
assume "e ∈ set p"
hence "resCap p ≤ cf e" unfolding resCap_alt by auto
moreover have "(augmentingFlow p) e = resCap p"
unfolding augmentingFlow_def using ‹e ∈ set p› by auto
moreover have "0 < resCap p" using resCap_gzero[OF AUG] by simp
ultimately show ?thesis by auto
next
assume "e ∉ set p"
hence "(augmentingFlow p) e = 0" unfolding augmentingFlow_def by auto
thus ?thesis using resE_nonNegative by auto
qed
}
{ text ‹Next, we show the conservation constraint›
fix v
assume asm_s: "v ∈ Graph.V cf - {s, t}"
have "card (Graph.incoming cf v ∩ set p) = card (Graph.outgoing cf v ∩ set p)"
proof (cases)
assume "v∈set (cf.pathVertices_fwd s p)"
from cf.split_path_at_vertex[OF this PATH] obtain p1 p2 where
P_FMT: "p=p1@p2"
and 1: "cf.isPath s p1 v"
and 2: "cf.isPath v p2 t"
.
from 1 obtain p1' u1 where [simp]: "p1=p1'@[(u1,v)]"
using asm_s by (cases p1 rule: rev_cases) (auto simp: split_path_simps)
from 2 obtain p2' u2 where [simp]: "p2=(v,u2)#p2'"
using asm_s by (cases p2) (auto)
from
cf.isSPath_sg_outgoing[OF SPATH, of v u2]
cf.isSPath_sg_incoming[OF SPATH, of u1 v]
cf.isPath_edgeset[OF PATH]
have "cf.outgoing v ∩ set p = {(v,u2)}" "cf.incoming v ∩ set p = {(u1,v)}"
by (fastforce simp: P_FMT cf.outgoing_def cf.incoming_def)+
thus ?thesis by auto
next
assume "v∉set (cf.pathVertices_fwd s p)"
then have "∀u. (u,v)∉set p ∧ (v,u)∉set p"
by (auto dest: cf.pathVertices_edge[OF PATH])
hence "cf.incoming v ∩ set p = {}" "cf.outgoing v ∩ set p = {}"
by (auto simp: cf.incoming_def cf.outgoing_def)
thus ?thesis by auto
qed
thus "(∑e ∈ Graph.incoming cf v. (augmentingFlow p) e) =
(∑e ∈ Graph.outgoing cf v. (augmentingFlow p) e)"
by (auto simp: sum_augmenting_alt)
}
qed
subsection ‹Value of Augmenting Flow is Residual Capacity›
text ‹Finally, we show that the value of the augmenting flow is the residual
capacity of the augmenting path›
lemma augFlow_val:
"isAugmentingPath p ⟹ Flow.val cf s (augmentingFlow p) = resCap p"
proof -
assume AUG: "isAugmentingPath p"
with augFlow_resFlow interpret f: Flow cf s t "augmentingFlow p" .
note AUG
hence SPATH: "cf.isSimplePath s p t" by (simp add: isAugmentingPath_def)
hence PATH: "cf.isPath s p t" by (simp add: cf.isSimplePath_def)
then obtain v p' where "p=(s,v)#p'" "(s,v)∈cf.E"
using s_not_t by (cases p) auto
hence "cf.outgoing s ∩ set p = {(s,v)}"
using cf.isSPath_sg_outgoing[OF SPATH, of s v]
using cf.isPath_edgeset[OF PATH]
by (fastforce simp: cf.outgoing_def)
moreover have "cf.incoming s ∩ set p = {}" using SPATH no_incoming_s
by (auto
simp: cf.incoming_def ‹p=(s,v)#p'› in_set_conv_decomp[where xs=p']
simp: cf.isSimplePath_append cf.isSimplePath_cons)
ultimately show ?thesis
unfolding f.val_def
by (auto simp: sum_augmenting_alt)
qed
end
end