Theory Generic_Push_Relabel
section ‹Generic Push Relabel Algorithm›
theory Generic_Push_Relabel
imports
Flow_Networks.Fofu_Abs_Base
Flow_Networks.Ford_Fulkerson
begin
subsection ‹Labeling›
text ‹The central idea of the push-relabel algorithm is to add natural number
labels ‹l : node ⇒ nat› to each node, and maintain the invariant that for
all edges ‹(u,v)› in the residual graph, we have ‹l u ≤ l v + 1›.›
type_synonym labeling = "node ⇒ nat"
locale Labeling = NPreflow +
fixes l :: labeling
assumes valid: "(u,v) ∈ cf.E ⟹ l(u) ≤ l(v) + 1"
assumes lab_src[simp]: "l s = card V"
assumes lab_sink[simp]: "l t = 0"
begin
text ‹Generalizing validity to paths›
lemma gen_valid: "l(u) ≤ l(x) + length p" if "cf.isPath u p x"
using that by (induction p arbitrary: u; fastforce dest: valid)
text ‹
In a valid labeling, there cannot be an augmenting path~\cormen{26.17}.
The proof works by contradiction, using the validity constraint
to show that any augmenting path would be too long for a simple path.
›
theorem no_augmenting_path: "¬isAugmentingPath p"
proof
assume "isAugmentingPath p"
hence SP: "cf.isSimplePath s p t" unfolding isAugmentingPath_def .
hence "cf.isPath s p t" unfolding cf.isSimplePath_def by auto
from gen_valid[OF this] have "length p ≥ card V" by auto
with cf.simplePath_length_less_V[OF _ SP] show False by auto
qed
text ‹
The idea of push relabel algorithms is to maintain a valid labeling,
and, ultimately, arrive at a valid flow, i.e., no nodes have excess flow.
We then immediately get that the flow is maximal:
›
corollary no_excess_imp_maxflow:
assumes "∀u∈V-{s,t}. excess f u = 0"
shows "isMaxFlow f"
proof -
from assms interpret NFlow
apply unfold_locales
using no_deficient_nodes unfolding excess_def by auto
from noAugPath_iff_maxFlow no_augmenting_path show "isMaxFlow f" by auto
qed
end
subsection ‹Basic Operations›
text ‹
The operations of the push relabel algorithm are local operations on
single nodes and edges.
›
subsubsection ‹Augmentation of Edges›
context Network
begin
text ‹We define a function to augment a single edge in the residual graph.›
definition augment_edge :: "'capacity flow ⇒ _"
where "augment_edge f ≡ λ(u,v) Δ.
if (u,v)∈E then f( (u,v) := f (u,v) + Δ )
else if (v,u)∈E then f( (v,u) := f (v,u) - Δ )
else f"
lemma augment_edge_zero[simp]: "augment_edge f e 0 = f"
unfolding augment_edge_def by (auto split: prod.split)
lemma augment_edge_same[simp]: "e∈E ⟹ augment_edge f e Δ e = f e + Δ"
unfolding augment_edge_def by (auto split!: prod.splits)
lemma augment_edge_other[simp]:"⟦e∈E; e'≠e ⟧ ⟹ augment_edge f e Δ e' = f e'"
unfolding augment_edge_def by (auto split!: prod.splits)
lemma augment_edge_rev_same[simp]:
"(v,u)∈E ⟹ augment_edge f (u,v) Δ (v,u) = f (v,u) - Δ"
using no_parallel_edge
unfolding augment_edge_def by (auto split!: prod.splits)
lemma augment_edge_rev_other[simp]:
"⟦(u,v)∉E; e'≠(v,u)⟧ ⟹ augment_edge f (u,v) Δ e' = f e'"
unfolding augment_edge_def by (auto split!: prod.splits)
lemma augment_edge_cf[simp]: "(u,v)∈E∪E¯ ⟹
cf_of (augment_edge f (u,v) Δ)
= (cf_of f)( (u,v) := cf_of f (u,v) - Δ, (v,u) := cf_of f (v,u) + Δ)"
apply (intro ext; cases "(u,v)∈E")
subgoal for e'
apply (cases "e'=(u,v)")
subgoal by (simp split!: if_splits add: no_self_loop residualGraph_def)
apply (cases "e'=(v,u)")
subgoal by (simp split!: if_splits add: no_parallel_edge residualGraph_def)
subgoal by (simp
split!: if_splits prod.splits
add: residualGraph_def augment_edge_def)
done
subgoal for e'
apply (cases "e'=(u,v)")
subgoal by (simp split!: if_splits add: no_self_loop residualGraph_def)
apply (cases "e'=(v,u)")
subgoal by (simp split!: if_splits add: no_self_loop residualGraph_def)
subgoal by (simp
split!: if_splits prod.splits
add: residualGraph_def augment_edge_def)
done
done
lemma augment_edge_cf': "(u,v)∈cfE_of f ⟹
cf_of (augment_edge f (u,v) Δ)
= (cf_of f)( (u,v) := cf_of f (u,v) - Δ, (v,u) := cf_of f (v,u) + Δ)"
proof -
assume "(u,v)∈cfE_of f"
hence "(u,v)∈E∪E¯" using cfE_of_ss_invE ..
thus ?thesis by simp
qed
text ‹The effect of augmenting an edge on the residual graph›
definition (in -) augment_edge_cf :: "_ flow ⇒ _" where
"augment_edge_cf cf
≡ λ(u,v) Δ. (cf)( (u,v) := cf (u,v) - Δ, (v,u) := cf (v,u) + Δ)"
lemma cf_of_augment_edge:
assumes A: "(u,v)∈cfE_of f"
shows "cf_of (augment_edge f (u,v) Δ) = augment_edge_cf (cf_of f) (u,v) Δ"
proof -
show "cf_of (augment_edge f (u, v) Δ) = augment_edge_cf (cf_of f) (u, v) Δ"
by (simp add: augment_edge_cf_def A augment_edge_cf')
qed
lemma cfE_augment_ss:
assumes EDGE: "(u,v)∈cfE_of f"
shows "cfE_of (augment_edge f (u,v) Δ) ⊆ insert (v,u) (cfE_of f)"
using EDGE
apply (clarsimp simp: augment_edge_cf')
unfolding Graph.E_def
apply (auto split: if_splits)
done
end
context NPreflow begin
text ‹Augmenting an edge ‹(u,v)› with a flow ‹Δ› that does not exceed the
available edge capacity, nor the available excess flow on the source node,
preserves the preflow property.
›
lemma augment_edge_preflow_preserve: "⟦0≤Δ; Δ ≤ cf (u,v); Δ ≤ excess f u⟧
⟹ Preflow c s t (augment_edge f (u,v) Δ)"
apply unfold_locales
subgoal
unfolding residualGraph_def augment_edge_def
using capacity_const
by (fastforce split!: if_splits)
subgoal
proof (intro ballI; clarsimp)
assume "0≤Δ" "Δ ≤ cf (u,v)" "Δ ≤ excess f u"
fix v'
assume V': "v'∈V" "v'≠s" "v'≠t"
show "sum (augment_edge f (u, v) Δ) (outgoing v')
≤ sum (augment_edge f (u, v) Δ) (incoming v')"
proof (cases)
assume "Δ = 0"
with no_deficient_nodes show ?thesis using V' by auto
next
assume "Δ ≠ 0" with ‹0≤Δ› have "0<Δ" by auto
with ‹Δ ≤ cf (u,v)› have "(u,v)∈cf.E" unfolding Graph.E_def by auto
show ?thesis
proof (cases)
assume [simp]: "(u,v)∈E"
hence AE: "augment_edge f (u,v) Δ = f ( (u,v) := f (u,v) + Δ )"
unfolding augment_edge_def by auto
have 1: "∀e∈outgoing v'. augment_edge f (u,v) Δ e = f e" if "v'≠u"
using that unfolding outgoing_def AE by auto
have 2: "∀e∈incoming v'. augment_edge f (u,v) Δ e = f e" if "v'≠v"
using that unfolding incoming_def AE by auto
from ‹(u,v)∈E› no_self_loop have "u≠v" by blast
{
assume "v' ≠ u" "v' ≠ v"
with 1 2 V' no_deficient_nodes have ?thesis by auto
} moreover {
assume [simp]: "v'=v"
have "sum (augment_edge f (u, v) Δ) (outgoing v')
= sum f (outgoing v)"
using 1 ‹u≠v› V' by auto
also have "… ≤ sum f (incoming v)"
using V' no_deficient_nodes by auto
also have "… ≤ sum (augment_edge f (u, v) Δ) (incoming v)"
apply (rule sum_mono)
using ‹0≤Δ›
by (auto simp: incoming_def augment_edge_def split!: if_split)
finally have ?thesis by simp
} moreover {
assume [simp]: "v'=u"
have A1: "sum (augment_edge f (u,v) Δ) (incoming v')
= sum f (incoming u)"
using 2 ‹u≠v› by auto
have "(u,v) ∈ outgoing u" using ‹(u,v)∈E›
by (auto simp: outgoing_def)
note AUX = sum.remove[OF _ this, simplified]
have A2: "sum (augment_edge f (u,v) Δ) (outgoing u)
= sum f (outgoing u) + Δ"
using AUX[of "augment_edge f (u,v) Δ"] AUX[of "f"] by auto
from A1 A2 ‹Δ ≤ excess f u› no_deficient_nodes V' have ?thesis
unfolding excess_def by auto
} ultimately show ?thesis by blast
next
assume [simp]: ‹(u,v)∉E›
hence [simp]: "(v,u)∈E" using cfE_ss_invE ‹(u,v)∈cf.E› by auto
from ‹(u,v)∉E› ‹(v,u)∈E› have "u≠v" by blast
have AE: "augment_edge f (u,v) Δ = f ( (v,u) := f (v,u) - Δ )"
unfolding augment_edge_def by simp
have 1: "∀e∈outgoing v'. augment_edge f (u,v) Δ e = f e" if "v'≠v"
using that unfolding outgoing_def AE by auto
have 2: "∀e∈incoming v'. augment_edge f (u,v) Δ e = f e" if "v'≠u"
using that unfolding incoming_def AE by auto
{
assume "v' ≠ u" "v' ≠ v"
with 1 2 V' no_deficient_nodes have ?thesis by auto
} moreover {
assume [simp]: "v'=u"
have A1: "sum (augment_edge f (u, v) Δ) (outgoing v')
= sum f (outgoing u)"
using 1 ‹u≠v› V' by auto
have "(v,u) ∈ incoming u"
using ‹(v,u)∈E› by (auto simp: incoming_def)
note AUX = sum.remove[OF _ this, simplified]
have A2: "sum (augment_edge f (u,v) Δ) (incoming u)
= sum f (incoming u) - Δ"
using AUX[of "augment_edge f (u,v) Δ"] AUX[of "f"] by auto
from A1 A2 ‹Δ ≤ excess f u› no_deficient_nodes V' have ?thesis
unfolding excess_def by auto
} moreover {
assume [simp]: "v'=v"
have "sum (augment_edge f (u,v) Δ) (outgoing v')
≤ sum f (outgoing v')"
apply (rule sum_mono)
using ‹0<Δ›
by (auto simp: augment_edge_def)
also have "… ≤ sum f (incoming v)"
using no_deficient_nodes V' by auto
also have "… ≤ sum (augment_edge f (u,v) Δ) (incoming v')"
using 2 ‹u≠v› by auto
finally have ?thesis by simp
} ultimately show ?thesis by blast
qed
qed
qed
done
end
subsubsection ‹Push Operation›
context Network
begin
text ‹The push operation pushes as much flow as possible flow from an active
node over an admissible edge.
A node is called \emph{active} if it has positive excess, and an edge ‹(u,v)›
of the residual graph is called admissible, if @{term ‹l u = l v + 1›}.
›
definition push_precond :: "'capacity flow ⇒ labeling ⇒ edge ⇒ bool"
where "push_precond f l
≡ λ(u,v). excess f u > 0 ∧ (u,v)∈cfE_of f ∧ l u = l v + 1"
text ‹The maximum possible flow is determined by the available excess flow at
the source node and the available capacity of the edge.›
definition push_effect :: "'capacity flow ⇒ edge ⇒ 'capacity flow"
where "push_effect f
≡ λ(u,v). augment_edge f (u,v) (min (excess f u) (cf_of f (u,v)))"
lemma push_precondI[intro?]:
"⟦excess f u > 0; (u,v)∈cfE_of f; l u = l v + 1⟧ ⟹ push_precond f l (u,v)"
unfolding push_precond_def by auto
subsubsection ‹Relabel Operation›
text ‹
An active node (not the sink) without any outgoing admissible edges
can be relabeled.
›
definition relabel_precond :: "'capacity flow ⇒ labeling ⇒ node ⇒ bool"
where "relabel_precond f l u
≡ u≠t ∧ excess f u > 0 ∧ (∀v. (u,v)∈cfE_of f ⟶ l u ≠ l v + 1)"
text ‹The new label is computed from the neighbour's labels, to be the minimum
value that will create an outgoing admissible edge.›
definition relabel_effect :: "'capacity flow ⇒ labeling ⇒ node ⇒ labeling"
where "relabel_effect f l u
≡ l( u := Min { l v | v. (u,v)∈cfE_of f } + 1 )"
subsubsection ‹Initialization›
text ‹
The initial preflow exhausts all outgoing edges of the source node.
›
definition "pp_init_f ≡ λ(u,v). if (u=s) then c (u,v) else 0"
text ‹
The initial labeling labels the source with ‹|V|›, and all other nodes
with ‹0›.
›
definition "pp_init_l ≡ (λx. 0)(s := card V)"
end
subsection ‹Abstract Correctness›
text ‹We formalize the abstract correctness argument of the algorithm.
It consists of two parts:
▸ Execution of push and relabel operations maintain a valid labeling
▸ If no push or relabel operations can be executed, the preflow is actually
a flow.
This section corresponds to the proof of \cormen{26.18}.
›
subsubsection ‹Maintenance of Invariants›
context Network
begin
lemma pp_init_invar: "Labeling c s t pp_init_f pp_init_l"
apply (unfold_locales;
((auto simp: pp_init_f_def pp_init_l_def cap_non_negative; fail)
| (intro ballI)?))
proof -
fix v
assume "v∈V - {s,t}"
hence "∀e∈outgoing v. pp_init_f e = 0"
by (auto simp: outgoing_def pp_init_f_def)
hence [simp]: "sum pp_init_f (outgoing v) = 0" by auto
have "0 ≤ pp_init_f e" for e
by (auto simp: pp_init_f_def cap_non_negative split: prod.split)
from sum_bounded_below[of "incoming v" 0 pp_init_f, OF this]
have "0 ≤ sum pp_init_f (incoming v)" by auto
thus "sum pp_init_f (outgoing v) ≤ sum pp_init_f (incoming v)"
by auto
next
fix u v
assume "(u, v) ∈ Graph.E (residualGraph c pp_init_f)"
thus "pp_init_l u ≤ pp_init_l v + 1"
unfolding pp_init_l_def Graph.E_def pp_init_f_def residualGraph_def
by (auto split: if_splits)
qed
lemma pp_init_f_preflow: "NPreflow c s t pp_init_f"
proof -
from pp_init_invar interpret Labeling c s t pp_init_f pp_init_l .
show ?thesis by unfold_locales
qed
end
context Labeling
begin
text ‹Push operations preserve a valid labeling~\cormen{26.16}.›
theorem push_pres_Labeling:
assumes "push_precond f l e"
shows "Labeling c s t (push_effect f e) l"
unfolding push_effect_def
proof (cases e; clarsimp)
fix u v
assume [simp]: "e=(u,v)"
let ?f' = "(augment_edge f (u, v) (min (excess f u) (cf (u, v))))"
from assms have
ACTIVE: "excess f u > 0"
and EDGE: "(u,v)∈cf.E"
and ADM: "l u = l v + 1"
unfolding push_precond_def by auto
interpret cf': Preflow c s t ?f'
apply (rule augment_edge_preflow_preserve)
using ACTIVE resE_nonNegative
by auto
show "Labeling c s t ?f' l"
apply unfold_locales using valid
using cfE_augment_ss[OF EDGE] ADM
apply (fastforce)
by auto
qed
lemma finite_min_cf_outgoing[simp, intro!]: "finite {l v |v. (u, v) ∈ cf.E}"
proof -
have "{l v |v. (u, v) ∈ cf.E} = l`snd`cf.outgoing u"
by (auto simp: cf.outgoing_def)
moreover have "finite (l`snd`cf.outgoing u)" by auto
ultimately show ?thesis by auto
qed
text ‹Relabel operations preserve a valid labeling~\cormen{26.16}.
Moreover, they increase the label of the relabeled node~\cormen{26.15}.
›
theorem
assumes PRE: "relabel_precond f l u"
shows relabel_increase_u: "relabel_effect f l u u > l u" (is ?G1)
and relabel_pres_Labeling: "Labeling c s t f (relabel_effect f l u)" (is ?G2)
proof -
from PRE have
NOT_SINK: "u≠t"
and ACTIVE: "excess f u > 0"
and NO_ADM: "⋀v. (u,v)∈cf.E ⟹ l u ≠ l v + 1"
unfolding relabel_precond_def by auto
from ACTIVE have [simp]: "s≠u" using excess_s_non_pos by auto
from active_has_cf_outgoing[OF ACTIVE] have [simp]: "∃v. (u, v) ∈ cf.E"
by (auto simp: cf.outgoing_def)
from NO_ADM valid have "l u < l v + 1" if "(u,v)∈cf.E" for v
by (simp add: nat_less_le that)
hence LU_INCR: "l u ≤ Min { l v | v. (u,v)∈cf.E }"
by (auto simp: less_Suc_eq_le)
with valid have "∀u'. (u',u)∈cf.E ⟶ l u' ≤ Min { l v | v. (u,v)∈cf.E } + 1"
by (smt ab_semigroup_add_class.add.commute add_le_cancel_left le_trans)
moreover have "∀v. (u,v)∈cf.E ⟶ Min { l v | v. (u,v)∈cf.E } + 1 ≤ l v + 1"
using Min_le by auto
ultimately show ?G1 ?G2
unfolding relabel_effect_def
apply (clarsimp_all simp: PRE)
subgoal using LU_INCR by (simp add: less_Suc_eq_le)
apply (unfold_locales)
subgoal for u' v' using valid by auto
subgoal by auto
subgoal using NOT_SINK by auto
done
qed
lemma relabel_preserve_other: "u≠v ⟹ relabel_effect f l u v = l v"
unfolding relabel_effect_def by auto
subsubsection ‹Maxflow on Termination›
text ‹
If no push or relabel operations can be performed any more,
we have arrived at a maximal flow.
›
theorem push_relabel_term_imp_maxflow:
assumes no_push: "∀(u,v)∈cf.E. ¬push_precond f l (u,v)"
assumes no_relabel: "∀u. ¬relabel_precond f l u"
shows "isMaxFlow f"
proof -
from assms have "∀u∈V-{t}. excess f u ≤ 0"
unfolding push_precond_def relabel_precond_def
by force
with excess_non_negative have "∀u∈V-{s,t}. excess f u = 0" by force
with no_excess_imp_maxflow show ?thesis .
qed
end
subsection ‹Convenience Lemmas›
text ‹We define a locale to reflect the effect of a push operation›
locale push_effect_locale = Labeling +
fixes u v
assumes PRE: "push_precond f l (u,v)"
begin
abbreviation "f' ≡ push_effect f (u,v)"
sublocale l': Labeling c s t f' l
using push_pres_Labeling[OF PRE] .
lemma uv_cf_edge[simp, intro!]: "(u,v)∈cf.E"
using PRE unfolding push_precond_def by auto
lemma excess_u_pos: "excess f u > 0"
using PRE unfolding push_precond_def by auto
lemma l_u_eq[simp]: "l u = l v + 1"
using PRE unfolding push_precond_def by auto
lemma uv_edge_cases:
obtains (par) "(u,v)∈E" "(v,u)∉E"
| (rev) "(v,u)∈E" "(u,v)∉E"
using uv_cf_edge cfE_ss_invE no_parallel_edge by blast
lemma uv_nodes[simp, intro!]: "u∈V" "v∈V"
using E_ss_VxV cfE_ss_invE no_parallel_edge by auto
lemma uv_not_eq[simp]: "u≠v" "v≠u"
using E_ss_VxV cfE_ss_invE[THEN subsetD, OF uv_cf_edge] no_parallel_edge
by auto
definition "Δ = min (excess f u) (cf_of f (u,v))"
lemma Δ_positive: "Δ > 0"
unfolding Δ_def
using excess_u_pos uv_cf_edge[unfolded cf.E_def] resE_positive
by auto
lemma f'_alt: "f' = augment_edge f (u,v) Δ"
unfolding push_effect_def Δ_def by auto
lemma cf'_alt: "l'.cf = augment_edge_cf cf (u,v) Δ"
unfolding push_effect_def Δ_def augment_edge_cf_def
by (auto simp: augment_edge_cf')
lemma excess'_u[simp]: "excess f' u = excess f u - Δ"
unfolding excess_def[where f=f']
proof -
show "sum f' (incoming u) - sum f' (outgoing u) = excess f u - Δ"
proof (cases rule: uv_edge_cases)
case [simp]: par
hence UV_ONI:"(u,v)∈outgoing u - incoming u"
by (auto simp: incoming_def outgoing_def no_self_loop)
have 1: "sum f' (incoming u) = sum f (incoming u)"
apply (rule sum.cong[OF refl])
using UV_ONI unfolding f'_alt
apply (subst augment_edge_other)
by auto
have "sum f' (outgoing u)
= sum f (outgoing u) + (∑x∈outgoing u. if x = (u, v) then Δ else 0)"
unfolding f'_alt augment_edge_def sum.distrib[symmetric]
by (rule sum.cong) auto
also have "… = sum f (outgoing u) + Δ"
using UV_ONI by (auto simp: sum.delta)
finally show ?thesis using 1 unfolding excess_def by simp
next
case [simp]: rev
have UV_INO:"(v,u)∈incoming u - outgoing u"
by (auto simp: incoming_def outgoing_def no_self_loop)
have 1: "sum f' (outgoing u) = sum f (outgoing u)"
apply (rule sum.cong[OF refl])
using UV_INO unfolding f'_alt
apply (subst augment_edge_rev_other)
by (auto)
have "sum f' (incoming u)
= sum f (incoming u) + (∑x∈incoming u. if x = (v, u) then - Δ else 0)"
unfolding f'_alt augment_edge_def sum.distrib[symmetric]
by (rule sum.cong) auto
also have "… = sum f (incoming u) - Δ"
using UV_INO by (auto simp: sum.delta)
finally show ?thesis using 1 unfolding excess_def by auto
qed
qed
lemma excess'_v[simp]: "excess f' v = excess f v + Δ"
unfolding excess_def[where f=f']
proof -
show "sum f' (incoming v) - sum f' (outgoing v) = excess f v + Δ"
proof (cases rule: uv_edge_cases)
case [simp]: par
have UV_INO: "(u,v)∈incoming v - outgoing v"
unfolding incoming_def outgoing_def by (auto simp: no_self_loop)
have 1: "sum f' (outgoing v) = sum f (outgoing v)"
using UV_INO unfolding f'_alt
by (auto simp: augment_edge_def intro: sum.cong)
have "sum f' (incoming v)
= sum f (incoming v) + (∑x∈incoming v. if x=(u,v) then Δ else 0)"
unfolding f'_alt augment_edge_def sum.distrib[symmetric]
apply (rule sum.cong)
using UV_INO unfolding f'_alt by auto
also have "… = sum f (incoming v) + Δ"
using UV_INO by (auto simp: sum.delta)
finally show ?thesis using 1 by (auto simp: excess_def)
next
case [simp]: rev
have UV_INO:"(v,u)∈outgoing v - incoming v"
by (auto simp: incoming_def outgoing_def no_self_loop)
have 1: "sum f' (incoming v) = sum f (incoming v)"
using UV_INO unfolding f'_alt
by (auto simp: augment_edge_def intro: sum.cong)
have "sum f' (outgoing v)
= sum f (outgoing v) + (∑x∈outgoing v. if x=(v,u) then - Δ else 0)"
unfolding f'_alt augment_edge_def sum.distrib[symmetric]
apply (rule sum.cong)
using UV_INO unfolding f'_alt by auto
also have "… = sum f (outgoing v) - Δ"
using UV_INO by (auto simp: sum.delta)
finally show ?thesis using 1 by (auto simp: excess_def)
qed
qed
lemma excess'_other[simp]:
assumes "x ≠ u" "x ≠ v"
shows "excess f' x = excess f x"
proof -
have NE: "(u,v)∉incoming x" "(u,v)∉outgoing x"
"(v,u)∉incoming x" "(v,u)∉outgoing x"
using assms unfolding incoming_def outgoing_def by auto
have
"sum f' (outgoing x) = sum f (outgoing x)"
"sum f' (incoming x) = sum f (incoming x)"
by (auto
simp: augment_edge_def f'_alt NE
split!: if_split
intro: sum.cong)
thus ?thesis
unfolding excess_def by auto
qed
lemma excess'_if:
"excess f' x = (
if x=u then excess f u - Δ
else if x=v then excess f v + Δ
else excess f x)"
by simp
end
subsection ‹Complexity›
text ‹
Next, we analyze the complexity of the generic push relabel algorithm.
We will show that it has a complexity of ‹O(V⇧2E)› basic operations.
Here, we often trade precise estimation of constant factors for simplicity
of the proof.
›
subsubsection ‹Auxiliary Lemmas›
context Network
begin
lemma cardE_nz_aux[simp, intro!]:
"card E ≠ 0" "card E ≥ Suc 0" "card E > 0"
proof -
show "card E ≠ 0" by (simp add: E_not_empty)
thus "card E ≥ Suc 0" by linarith
thus "card E > 0" by auto
qed
text ‹The number of nodes can be estimated by the number of edges.
This estimation is done in various places to get smoother bounds.
›
lemma card_V_est_E: "card V ≤ 2 * card E"
proof -
have "card V ≤ card (fst`E) + card (snd`E)"
by (auto simp: card_Un_le V_alt)
also note card_image_le[OF finite_E]
also note card_image_le[OF finite_E]
finally show "card V ≤ 2 * card E" by auto
qed
end
subsubsection ‹Height Bound›
text ‹A crucial idea of estimating the complexity is the insight that
no label will exceed ‹2|V|-1› during the algorithm.
We define a locale that states this invariant, and show that the algorithm
maintains it. The corresponds to the proof of \cormen{26.20}.
›
locale Height_Bounded_Labeling = Labeling +
assumes height_bound: "∀u∈V. l u ≤ 2*card V - 1"
begin
lemma height_bound': "u∈V ⟹ l u ≤ 2*card V - 1"
using height_bound by auto
end
lemma (in Network) pp_init_height_bound:
"Height_Bounded_Labeling c s t pp_init_f pp_init_l"
proof -
interpret Labeling c s t pp_init_f pp_init_l by (rule pp_init_invar)
show ?thesis by unfold_locales (auto simp: pp_init_l_def)
qed
context Height_Bounded_Labeling
begin
text ‹As push does not change the labeling, it trivially preserves the
height bound.›
lemma push_pres_height_bound:
assumes "push_precond f l e"
shows "Height_Bounded_Labeling c s t (push_effect f e) l"
proof -
from push_pres_Labeling[OF assms]
interpret l': Labeling c s t "push_effect f e" l .
show ?thesis using height_bound by unfold_locales
qed
text ‹
In a valid labeling,
any active node has a (simple) path to the source node in
the residual graph~\cormen{26.19}.
›
lemma (in Labeling) excess_imp_source_path:
assumes "excess f u > 0"
obtains p where "cf.isSimplePath u p s"
proof -
obtain U where U_def: "U = {v|p v. cf.isSimplePath u p v}" by blast
have fct1: "U ⊆ V"
proof
fix v
assume "v ∈ U"
then have "(u, v) ∈ cf.E⇧*"
using U_def cf.isSimplePath_def cf.isPath_rtc by auto
then obtain u' where "u = v ∨ ((u, u') ∈ cf.E⇧* ∧ (u', v) ∈ cf.E)"
by (meson rtranclE)
thus "v ∈ V"
proof
assume "u = v"
thus ?thesis using excess_nodes_only[OF assms] by blast
next
assume "(u, u') ∈ cf.E⇧* ∧ (u', v) ∈ cf.E"
then have "v ∈ cf.V" unfolding cf.V_def by blast
thus ?thesis by simp
qed
qed
have "s ∈ U"
proof(rule ccontr)
assume "s ∉ U"
obtain U' where U'_def: "U' = V - U" by blast
have "(∑u∈U. excess f u)
= (∑u∈U. (∑v∈U'. f (v, u))) - (∑u∈U. (∑v∈U'. f (u, v)))"
proof -
have "(∑u∈U. excess f u)
= (∑u∈U. (∑v∈incoming u. f v)) - (∑u∈U.(∑v∈outgoing u. f v))"
(is "_ = ?R1 - ?R2") unfolding excess_def by (simp add: sum_subtractf)
also have "?R1 = (∑u∈U. (∑v∈V. f (v, u)))"
using sum_incoming_alt_flow fct1 by (meson subsetCE sum.cong)
also have "… = (∑u∈U. (∑v∈U. f (v, u))) + (∑u∈U. (∑v∈U'. f (v, u)))"
proof -
have "(∑v∈V. f (v, u)) = (∑v∈U. f (v, u)) + (∑v∈U'. f (v, u))" for u
using U'_def fct1 finite_V
by (metis ab_semigroup_add_class.add.commute sum.subset_diff)
thus ?thesis by (simp add: sum.distrib)
qed
also have "?R2 = (∑u∈U. (∑v∈V. f (u, v)))"
using sum_outgoing_alt_flow fct1 by (meson subsetCE sum.cong)
also have "… = (∑u∈U. (∑v∈U. f (u, v))) + (∑u∈U. (∑v∈U'. f (u, v)))"
proof -
have "(∑v∈V. f (u, v)) = (∑v∈U. f (u, v)) + (∑v∈U'. f (u, v))" for u
using U'_def fct1 finite_V
by (metis ab_semigroup_add_class.add.commute sum.subset_diff)
thus ?thesis by (simp add: sum.distrib)
qed
also have "(∑u∈U. (∑v∈U. f (u, v))) = (∑u∈U. (∑v∈U. f (v, u)))"
proof -
{
fix A :: "nat set"
assume "finite A"
then have "(∑u∈A. (∑v∈A. f (u, v))) = (∑u∈A. (∑v∈A. f (v, u)))"
proof (induction "card A" arbitrary: A)
case 0
then show ?case by auto
next
case (Suc x)
then obtain A' a
where o1:"A = insert a A'" and o2:"x = card A'" and o3:"finite A'"
by (metis card_insert_disjoint card_le_Suc_iff le_refl nat.inject)
then have lm:"(∑e∈A. g e) = (∑e∈A'. g e) + g a"
for g :: "nat ⇒ 'a"
using Suc.hyps(2)
by (metis card_insert_if n_not_Suc_n
semiring_normalization_rules(24) sum.insert)
have "(∑u∈A. (∑v∈A. f (u, v)))
= (∑u∈A'. (∑v∈A. f (u, v))) + (∑v∈A. f (a, v))"
(is "_ = ?R1 + ?R2") using lm by auto
also have "?R1 = (∑u∈A'. (∑v∈A'. f (u, v))) + (∑u∈A'. f(u, a))"
(is "_ = ?R1_1 + ?R1_2") using lm sum.distrib by force
also note add.assoc
also have "?R1_2 + ?R2 = (∑u∈A'. f(a, u)) + (∑v∈A. f(v, a))"
(is "_ = ?R1_2' + ?R2'") using lm by auto
also have "?R1_1 = (∑u∈A'. (∑v∈A'. f (v, u)))"
(is "_ = ?R1_1'") using Suc.hyps(1)[of A'] o2 o3 by auto
also note add.assoc[symmetric]
also have "?R1_1' + ?R1_2' = (∑u∈A'. (∑v∈A. f (v, u)))"
by (metis (no_types, lifting) lm sum.cong sum.distrib)
finally show ?case using lm[symmetric] by auto
qed
} note this[of U]
thus ?thesis using fct1 finite_V finite_subset by auto
qed
finally show ?thesis by arith
qed
moreover have "(∑u∈U. excess f u) > 0"
proof -
have "u ∈ U" using U_def by simp
moreover have "u ∈ U ⟹ excess f u ≥ 0" for u
using fct1 excess_non_negative' ‹s ∉ U› by auto
ultimately show ?thesis using assms fct1 finite_V
by (metis Diff_cancel Diff_eq_empty_iff
Diff_infinite_finite finite_Diff sum_pos2)
qed
ultimately have
fct2: "(∑u∈U. (∑v∈U'. f (v, u))) - (∑u∈U. (∑v∈U'. f (u, v))) > 0"
by simp
have fct3: "(∑u∈U. (∑v∈U'. f (v, u))) > 0"
proof -
have "(∑u∈U. (∑v∈U'. f (v, u))) ≥ 0"
using capacity_const by (simp add: sum_nonneg)
moreover have "(∑u∈U. (∑v∈U'. f (u, v))) ≥ 0"
using capacity_const by (simp add: sum_nonneg)
ultimately show ?thesis using fct2 by simp
qed
have "∃u' v'. (u' ∈ U ∧ v' ∈ U' ∧ f (v', u') > 0)"
proof(rule ccontr)
assume "¬ (∃u' v'. u' ∈ U ∧ v' ∈ U' ∧ f (v', u') > 0)"
then have "(∀u' v'. (u' ∈ U ∧ v' ∈ U' ⟶ f (v', u') = 0))"
using capacity_const by (metis le_neq_trans)
thus False using fct3 by simp
qed
then obtain u' v' where "u' ∈ U" and "v' ∈ U'" and "f (v', u') > 0"
by blast
obtain p1 where "cf.isSimplePath u p1 u'" using U_def ‹u' ∈ U› by auto
moreover have "(u', v') ∈ cf.E"
proof -
have "(v', u') ∈ E"
using capacity_const ‹f (v', u') > 0›
by (metis not_less zero_flow_simp)
then have "cf (u', v') > 0" unfolding cf_def
using no_parallel_edge ‹f (v', u') > 0› by (auto split: if_split)
thus ?thesis unfolding cf.E_def by simp
qed
ultimately have "cf.isPath u (p1 @ [(u', v')]) v'"
using Graph.isPath_append_edge Graph.isSimplePath_def by blast
then obtain p2 where "cf.isSimplePath u p2 v'"
using cf.isSPath_pathLE by blast
then have "v' ∈ U" using U_def by auto
thus False using ‹v' ∈ U'› and U'_def by simp
qed
then obtain p' where "cf.isSimplePath u p' s" using U_def by auto
thus ?thesis ..
qed
text ‹Relabel operations preserve the height bound~\cormen{26.20}.›
lemma relabel_pres_height_bound:
assumes "relabel_precond f l u"
shows "Height_Bounded_Labeling c s t f (relabel_effect f l u)"
proof -
let ?l' = "relabel_effect f l u"
from relabel_pres_Labeling[OF assms]
interpret l': Labeling c s t f ?l' .
from assms have "excess f u > 0" unfolding relabel_precond_def by auto
with l'.excess_imp_source_path obtain p where p_obt: "cf.isSimplePath u p s" .
have "u ∈ V" using excess_nodes_only ‹excess f u > 0› .
then have "length p < card V"
using cf.simplePath_length_less_V[of u p] p_obt by auto
moreover have "?l' u ≤ ?l' s + length p"
using p_obt l'.gen_valid[of u p s] p_obt
unfolding cf.isSimplePath_def by auto
moreover have "?l' s = card V"
using l'.Labeling_axioms Labeling_def Labeling_axioms_def by auto
ultimately have "?l' u ≤ 2*card V - 1" by auto
thus "Height_Bounded_Labeling c s t f ?l'"
apply unfold_locales
using height_bound relabel_preserve_other
by metis
qed
text ‹Thus, the total number of relabel operations is
bounded by ‹O(V⇧2)›~\cormen{26.21}.
We express this bound by defining a measure function, and show that
it is decreased by relabel operations.
›
definition (in Network) "sum_heights_measure l ≡ ∑v∈V. 2*card V - l v"
corollary relabel_measure:
assumes "relabel_precond f l u"
shows "sum_heights_measure (relabel_effect f l u) < sum_heights_measure l"
proof -
let ?l' = "relabel_effect f l u"
from relabel_pres_height_bound[OF assms]
interpret l': Height_Bounded_Labeling c s t f ?l' .
from assms have "u∈V"
by (simp add: excess_nodes_only relabel_precond_def)
hence V_split: "V = insert u V" by auto
show ?thesis
using relabel_increase_u[OF assms] relabel_preserve_other[of u]
using l'.height_bound
unfolding sum_heights_measure_def
apply (rewrite at "∑_∈⌑. _" V_split)+
apply (subst sum.insert_remove[OF finite_V])+
using ‹u∈V›
by auto
qed
end
lemma (in Network) sum_height_measure_is_OV2:
"sum_heights_measure l ≤ 2*(card V)⇧2"
unfolding sum_heights_measure_def
proof -
have "2 * card V - l v ≤ 2 * card V" for v by auto
then have "(∑v∈V. 2 * card V - l v) ≤ (∑v∈V. 2 * card V)"
by (meson sum_mono)
also have "(∑v∈V. 2 * card V) = card V * (2 * card V)"
using finite_V by auto
finally show "(∑v∈V. 2 * card V - l v) ≤ 2 * (card V)^2"
by (simp add: power2_eq_square)
qed
subsubsection ‹Formulation of the Abstract Algorithm›
text ‹We give a simple relational characterization
of the abstract algorithm as a labeled transition system,
where the labels indicate the type of operation (push or relabel) that
have been executed.
›
context Network
begin