Theory Flow_Networks.Residual_Graph
section ‹Residual Graph›
theory Residual_Graph
imports Network
begin
text ‹
In this theory, we define the residual graph.
›
subsection ‹Definition›
text ‹The ∗‹residual graph› of a network and a flow indicates how much
flow can be effectively pushed along or reverse to a network edge,
by increasing or decreasing the flow on that edge:›
definition residualGraph :: "_ graph ⇒ _ flow ⇒ _ graph"
where "residualGraph c f ≡ λ(u, v).
if (u, v) ∈ Graph.E c then
c (u, v) - f (u, v)
else if (v, u) ∈ Graph.E c then
f (v, u)
else
0"
context Network begin
abbreviation "cf_of ≡ residualGraph c"
abbreviation "cfE_of f ≡ Graph.E (cf_of f)"
text ‹The edges of the residual graph are either parallel or reverse
to the edges of the network.›
lemma cfE_of_ss_invE: "cfE_of cf ⊆ E ∪ E¯"
unfolding residualGraph_def Graph.E_def
by auto
lemma cfE_of_ss_VxV: "cfE_of f ⊆ V×V"
unfolding V_def
unfolding residualGraph_def Graph.E_def
by auto
lemma cfE_of_finite[simp, intro!]: "finite (cfE_of f)"
using finite_subset[OF cfE_of_ss_VxV] by auto
lemma cf_no_self_loop: "(u,u)∉cfE_of f"
proof
assume a1: "(u, u) ∈ cfE_of f"
have "(u, u) ∉ E"
using no_parallel_edge by blast
then show False
using a1 unfolding Graph.E_def residualGraph_def by fastforce
qed
end
text ‹Let's fix a network with a preflow @{term f} on it›
context NPreflow
begin
text ‹We abbreviate the residual graph by @{term cf}.›
abbreviation "cf ≡ residualGraph c f"
sublocale cf: Graph cf .
lemmas cf_def = residualGraph_def[of c f]
subsection ‹Properties›
lemmas cfE_ss_invE = cfE_of_ss_invE[of f]
text ‹The nodes of the residual graph are exactly the nodes of the network.›
lemma resV_netV[simp]: "cf.V = V"
proof
show "V ⊆ Graph.V cf"
proof
fix u
assume "u ∈ V"
then obtain v where "(u, v) ∈ E ∨ (v, u) ∈ E" unfolding V_def by auto
moreover {
assume "(u, v) ∈ E"
then have "(u, v) ∈ Graph.E cf ∨ (v, u) ∈ Graph.E cf"
proof (cases)
assume "f (u, v) = 0"
then have "cf (u, v) = c (u, v)"
unfolding residualGraph_def using ‹(u, v) ∈ E› by (auto simp:)
then have "cf (u, v) ≠ 0" using ‹(u, v) ∈ E› unfolding E_def by auto
thus ?thesis unfolding Graph.E_def by auto
next
assume "f (u, v) ≠ 0"
then have "cf (v, u) = f (u, v)" unfolding residualGraph_def
using ‹(u, v) ∈ E› no_parallel_edge by auto
then have "cf (v, u) ≠ 0" using ‹f (u, v) ≠ 0› by auto
thus ?thesis unfolding Graph.E_def by auto
qed
} moreover {
assume "(v, u) ∈ E"
then have "(v, u) ∈ Graph.E cf ∨ (u, v) ∈ Graph.E cf"
proof (cases)
assume "f (v, u) = 0"
then have "cf (v, u) = c (v, u)"
unfolding residualGraph_def using ‹(v, u) ∈ E› by (auto)
then have "cf (v, u) ≠ 0" using ‹(v, u) ∈ E› unfolding E_def by auto
thus ?thesis unfolding Graph.E_def by auto
next
assume "f (v, u) ≠ 0"
then have "cf (u, v) = f (v, u)" unfolding residualGraph_def
using ‹(v, u) ∈ E› no_parallel_edge by auto
then have "cf (u, v) ≠ 0" using ‹f (v, u) ≠ 0› by auto
thus ?thesis unfolding Graph.E_def by auto
qed
} ultimately show "u∈cf.V" unfolding cf.V_def by auto
qed
next
show "Graph.V cf ⊆ V" using cfE_ss_invE unfolding Graph.V_def by auto
qed
text ‹Note, that Isabelle is powerful enough to prove the above case
distinctions completely automatically, although it takes some time:›
lemma "cf.V = V"
unfolding residualGraph_def Graph.E_def Graph.V_def
using no_parallel_edge[unfolded E_def]
by auto
text ‹As the residual graph has the same nodes as the network, it is also finite:›
sublocale cf: Finite_Graph cf
by unfold_locales auto
text ‹The capacities on the edges of the residual graph are non-negative›
lemma resE_nonNegative: "cf e ≥ 0"
proof (cases e; simp)
fix u v
{
assume "(u, v) ∈ E"
then have "cf (u, v) = c (u, v) - f (u, v)" unfolding cf_def by auto
hence "cf (u,v) ≥ 0"
using capacity_const cap_non_negative by auto
} moreover {
assume "(v, u) ∈ E"
then have "cf (u,v) = f (v, u)"
using no_parallel_edge unfolding cf_def by auto
hence "cf (u,v) ≥ 0"
using capacity_const by auto
} moreover {
assume "(u, v) ∉ E" "(v, u) ∉ E"
hence "cf (u,v) ≥ 0" unfolding residualGraph_def by simp
} ultimately show "cf (u,v) ≥ 0" by blast
qed
text ‹Again, there is an automatic proof›
lemma "cf e ≥ 0"
apply (cases e)
unfolding residualGraph_def
using no_parallel_edge capacity_const cap_positive
by auto
text ‹All edges of the residual graph are labeled with positive capacities:›
corollary resE_positive: "e ∈ cf.E ⟹ cf e > 0"
proof -
assume "e ∈ cf.E"
hence "cf e ≠ 0" unfolding cf.E_def by auto
thus ?thesis using resE_nonNegative by (meson eq_iff not_le)
qed
lemma reverse_flow: "Preflow cf s t f' ⟹ ∀(u, v) ∈ E. f' (v, u) ≤ f (u, v)"
proof -
assume asm: "Preflow cf s t f'"
then interpret f': Preflow cf s t f' .
{
fix u v
assume "(u, v) ∈ E"
then have "cf (v, u) = f (u, v)"
unfolding residualGraph_def using no_parallel_edge by auto
moreover have "f' (v, u) ≤ cf (v, u)" using f'.capacity_const by auto
ultimately have "f' (v, u) ≤ f (u, v)" by metis
}
thus ?thesis by auto
qed
definition (in Network) "flow_of_cf cf e ≡ (if (e∈E) then c e - cf e else 0)"
lemma (in NPreflow) E_ss_cfinvE: "E ⊆ Graph.E cf ∪ (Graph.E cf)¯"
unfolding residualGraph_def Graph.E_def
apply (clarsimp)
using no_parallel_edge
unfolding E_def
apply simp
done
text ‹Nodes with positive excess must have an outgoing edge in the
residual graph.
Intuitively: The excess flow must come from somewhere.›
lemma active_has_cf_outgoing: "excess f u > 0 ⟹ cf.outgoing u ≠ {}"
unfolding excess_def
proof -
assume "0 < sum f (incoming u) - sum f (outgoing u)"
hence "0 < sum f (incoming u)"
by (metis diff_gt_0_iff_gt linorder_neqE_linordered_idom linorder_not_le
sum_f_non_negative)
with f_non_negative obtain e where "e∈incoming u" "f e > 0"
by (meson not_le sum_nonpos)
then obtain v where "(v,u)∈E" "f (v,u) > 0" unfolding incoming_def by auto
hence "cf (u,v) > 0" unfolding residualGraph_def by auto
thus ?thesis unfolding cf.outgoing_def cf.E_def by fastforce
qed
end
locale RPreGraph
= Network +
fixes cf
assumes EX_RPG: "∃f. NPreflow c s t f ∧ cf = residualGraph c f"
begin
lemma this_loc_rpg: "RPreGraph c s t cf"
by unfold_locales
definition "f ≡ flow_of_cf cf"
lemma f_unique:
assumes "NPreflow c s t f'"
assumes A: "cf = residualGraph c f'"
shows "f' = f"
proof -
interpret f': NPreflow c s t f' by fact
show ?thesis
unfolding f_def[abs_def] flow_of_cf_def[abs_def]
unfolding A residualGraph_def
apply (rule ext)
using f'.capacity_const unfolding E_def
apply (auto split: prod.split)
by (metis antisym)
qed
lemma is_NPreflow: "NPreflow c s t (flow_of_cf cf)"
apply (fold f_def)
using EX_RPG f_unique by metis
sublocale f: NPreflow c s t f unfolding f_def by (rule is_NPreflow)
lemma rg_is_cf[simp]: "residualGraph c f = cf"
using EX_RPG f_unique by auto
lemma rg_fo_inv[simp]: "residualGraph c (flow_of_cf cf) = cf"
using rg_is_cf
unfolding f_def
.
sublocale cf: Graph cf .
lemma resV_netV[simp]: "cf.V = V"
using f.resV_netV by simp
sublocale cf: Finite_Graph cf
apply unfold_locales
apply simp
done
lemma E_ss_cfinvE: "E ⊆ cf.E ∪ cf.E¯"
using f.E_ss_cfinvE by simp
lemma cfE_ss_invE: "cf.E ⊆ E ∪ E¯"
using f.cfE_ss_invE by simp
lemma resE_nonNegative: "cf e ≥ 0"
using f.resE_nonNegative by auto
end
context NPreflow begin
lemma is_RPreGraph: "RPreGraph c s t cf"
apply unfold_locales
apply (rule exI[where x=f])
apply (safe; unfold_locales)
done
lemma fo_rg_inv: "flow_of_cf cf = f"
unfolding flow_of_cf_def[abs_def]
unfolding residualGraph_def
apply (rule ext)
using capacity_const unfolding E_def
apply (clarsimp split: prod.split)
by (metis antisym)
end
lemma (in NPreflow)
"flow_of_cf (residualGraph c f) = f"
by (rule fo_rg_inv)
locale RGraph
= Network +
fixes cf
assumes EX_RG: "∃f. NFlow c s t f ∧ cf = residualGraph c f"
begin
sublocale RPreGraph
proof
from EX_RG obtain f where
"NFlow c s t f" and [simp]: "cf = residualGraph c f" by auto
then interpret NFlow c s t f by simp
show "∃f. NPreflow c s t f ∧ cf = residualGraph c f"
apply (rule exI[where x="f"])
apply simp
by unfold_locales
qed
lemma this_loc: "RGraph c s t cf"
by unfold_locales
lemma this_loc_rpg: "RPreGraph c s t cf"
by unfold_locales
lemma is_NFlow: "NFlow c s t (flow_of_cf cf)"
using EX_RG f_unique is_NPreflow NFlow.axioms(1)
apply (fold f_def) by force
sublocale f: NFlow c s t f unfolding f_def by (rule is_NFlow)
end
context NFlow begin
lemma is_RGraph: "RGraph c s t cf"
apply unfold_locales
apply (rule exI[where x=f])
apply (safe; unfold_locales)
done
text ‹The value of the flow can be computed from the residual graph.›
lemma val_by_cf: "val = (∑(u,v)∈outgoing s. cf (v,u))"
proof -
have "f (s,v) = cf (v,s)" for v
unfolding cf_def by auto
thus ?thesis
unfolding val_alt outgoing_def
by (auto intro!: sum.cong)
qed
end
lemma (in RPreGraph) maxflow_imp_rgraph:
assumes "isMaxFlow (flow_of_cf cf)"
shows "RGraph c s t cf"
proof -
from assms interpret Flow c s t f
unfolding isMaxFlow_def by (simp add: f_def)
interpret NFlow c s t f by unfold_locales
show ?thesis
apply unfold_locales
apply (rule exI[of _ f])
apply (simp add: NFlow_axioms)
done
qed
end