section ‹Implementation of the Edmonds-Karp Algorithm›
theory EdmondsKarp_Refine
imports
EdmondsKarp_Algo
Augmenting_Path_BFS
"../../Refine_Imperative_HOL/IICF/Intf/IICF_Matrix"
"../../Refine_Imperative_HOL/IICF/IICF_Misc"
begin
text ‹We now implement the Edmonds-Karp algorithm.
Note that, during the implementation, we explicitly write down the
whole refined algorithm several times. As refinement is modular, most
of these copies could be avoided--- we inserted them deliberately for
documentation purposes.
›
subsection ‹Refinement to Residual Graph›
text ‹As a first step towards implementation, we refine the algorithm
to work directly on residual graphs. For this, we first have to
establish a relation between flows in a network and residual graphs.
›
subsubsection ‹Refinement of Operations›
context Network
begin
text ‹We define the relation between residual graphs and flows›
definition "cfi_rel ≡ br flow_of_cf (RGraph c s t)"
text ‹It can also be characterized the other way round, i.e.,
mapping flows to residual graphs:›
lemma cfi_rel_alt: "cfi_rel = {(cf,f). cf = residualGraph c f ∧ NFlow c s t f}"
unfolding cfi_rel_def br_def
by (auto
simp: NFlow.is_RGraph RGraph.is_NFlow
simp: RPreGraph.rg_fo_inv[OF RGraph.this_loc_rpg]
simp: NPreflow.fo_rg_inv[OF NFlow.axioms(1)])
text ‹Initially, the residual graph for the zero flow equals the original network›
lemma residualGraph_zero_flow: "residualGraph c (λ_. 0) = c"
unfolding residualGraph_def by (auto intro!: ext)
lemma flow_of_c: "flow_of_cf c = (λ_. 0)"
by (auto simp add: flow_of_cf_def[abs_def])
text ‹The residual capacity is naturally defined on residual graphs›
definition "resCap_cf cf p ≡ Min {cf e | e. e∈set p}"
lemma (in NFlow) resCap_cf_refine: "resCap_cf cf p = resCap p"
unfolding resCap_cf_def resCap_def ..
text ‹Augmentation can be done by @{const Graph.augment_cf}.›
lemma (in NFlow) augment_cf_refine_aux:
assumes AUG: "isAugmentingPath p"
shows "residualGraph c (augment (augmentingFlow p)) (u,v) = (
if (u,v)∈set p then (residualGraph c f (u,v) - resCap p)
else if (v,u)∈set p then (residualGraph c f (u,v) + resCap p)
else residualGraph c f (u,v))"
using augment_alt[OF AUG] by (auto simp: Graph.augment_cf_def)
lemma augment_cf_refine:
assumes R: "(cf,f)∈cfi_rel"
assumes AUG: "NPreflow.isAugmentingPath c s t f p"
shows "(Graph.augment_cf cf (set p) (resCap_cf cf p),
NFlow.augment_with_path c f p) ∈ cfi_rel"
proof -
from R have [simp]: "cf = residualGraph c f" and "NFlow c s t f"
by (auto simp: cfi_rel_alt br_def)
then interpret f: NFlow c s t f by simp
show ?thesis
unfolding f.augment_with_path_def
proof (simp add: cfi_rel_alt; safe intro!: ext)
fix u v
show "Graph.augment_cf f.cf (set p) (resCap_cf f.cf p) (u,v)
= residualGraph c (f.augment (f.augmentingFlow p)) (u,v)"
unfolding f.augment_cf_refine_aux[OF AUG]
unfolding f.cf.augment_cf_def
by (auto simp: f.resCap_cf_refine)
qed (rule f.augment_pres_nflow[OF AUG])
qed
text ‹We rephrase the specification of shortest augmenting path to
take a residual graph as parameter›
end
locale EdKa_Res = Network c s t for c :: "'capacity::linordered_idom graph" and s t +
fixes shortestpath_time :: nat
and augment_with_path_time :: nat
and init_graph :: "nat ⇒ nat"
assumes augment_progress[simp]: "0 ≠ enat shortestpath_time"
begin
interpretation Ed: EdKa c s t shortestpath_time augment_with_path_time
apply standard by simp
definition "find_shortest_augmenting_spec_cf cf ≡
ASSERT (RGraph c s t cf) ⪢
SPECT (emb (λ
None ⇒ ¬Graph.connected cf s t
| Some p ⇒ Graph.isShortestPath cf s p t) shortestpath_time)"
lemma find_shortest_augmenting_spec_cf_refine:
"RGraph c s t cf ⟹ find_shortest_augmenting_spec_cf cf ≤ Ed.find_shortest_augmenting_spec (flow_of_cf cf)"
proof -
assume R: "RGraph c s t cf"
interpret RG: RGraph c s t cf by fact
show ?thesis
unfolding RPreGraph.f_def[symmetric]
unfolding find_shortest_augmenting_spec_cf_def apply(subst Ed.find_shortest_augmenting_spec_def)
apply(rule le_ASSERTI) apply(rule ASSERT_leI) using R apply simp
using Network_axioms apply(simp add: EdKa_def EdKa_axioms_def)
by (auto
simp: pw_le_iff refine_pw_simps Some_eq_emb'_conv numeral_eq_enat
simp: RGraph.this_loc RPreGraph.rg_is_cf
simp: RG.f.isAugmentingPath_def Graph.connected_def Graph.isSimplePath_def
dest: RG.cf.shortestPath_is_path
split: option.split)
qed
text ‹This leads to the following refined algorithm›
definition "edka2 ≡ do {
cf ← SPECT [c ↦ init_graph (card V)];
(cf,_) ← whileT
(λ(cf,brk). ¬brk)
(λ(cf,_). do {
ASSERT (RGraph c s t cf);
p ← find_shortest_augmenting_spec_cf cf;
case p of
None ⇒ RETURNT (cf,True)
| Some p ⇒ do {
ASSERT (p≠[]);
ASSERT (Graph.isShortestPath cf s p t);
cf ← SPECT [Graph.augment_cf cf (set p) (resCap_cf cf p) ↦ augment_with_path_time];
ASSERT (RGraph c s t cf);
RETURNT (cf, False)
}
})
(cf,False);
ASSERT (RGraph c s t cf);
f ← RETURNT (flow_of_cf cf);
RETURNT f
}"
lemma edka2_refine: "edka2 ≤ ⇓Id Ed.edka"
proof -
have [refine_dref_RELATES]: "RELATES cfi_rel" by (simp add: RELATES_def)
show ?thesis
unfolding edka2_def Ed.edka_def
apply(refine_rcg find_shortest_augmenting_spec_cf_refine RETURNT_refine SPECT_refine)
apply refine_dref_type
apply simp_all
subgoal by (auto simp add: cfi_rel_alt residualGraph_zero_flow zero_flow
split: if_splits)
subgoal by (auto simp add: cfi_rel_alt NFlow.is_RGraph)
subgoal by (auto dest!: find_shortest_augmenting_spec_cf_refine
simp add: cfi_rel_def in_br_conv)
subgoal by (simp add: cfi_rel_alt)
subgoal apply (auto split: if_splits simp add: cfi_rel_def in_br_conv )
subgoal by (metis augment_cf_refine cfi_rel_def in_br_conv)
subgoal by (metis augment_cf_refine cfi_rel_def in_br_conv)
done
subgoal by (metis (full_types) cfi_rel_def in_br_conv)
by (simp_all add: cfi_rel_def in_br_conv)
qed
lemma edka2_correct: "edka2 ≤ ⇓Id (SPECT (emb isMaxFlow (enat Ed.edka_time)))"
apply(rule order.trans) apply(rule edka2_refine) using Ed.edka_correct by simp
end
locale RGraph_impl = RGraph c s t cf for c :: "'capacity::linordered_idom graph" and s t cf +
fixes matrix_lookup_time matrix_set_time :: nat
assumes [simp]: "matrix_lookup_time > 0"
begin
subsection ‹Implementation of Bottleneck Computation and Augmentation›
text ‹We will access the capacities in the residual graph
only by a get-operation, which asserts that the edges are valid›
abbreviation (in Graph) (input) valid_edge :: "edge ⇒ bool" where
"valid_edge ≡ λ(u,v). u∈V ∧ v∈V"
definition (in Network) cf_get
:: "'capacity graph ⇒ edge ⇒ nat ⇒ 'capacity nrest"
where "cf_get cff e matrix_lookup_time ≡ ASSERT (valid_edge e) ⪢ mop_matrix_get matrix_lookup_time cff e"
definition (in Network) cf_set
:: "'capacity graph ⇒ edge ⇒ 'capacity ⇒ nat ⇒ 'capacity graph nrest"
where "cf_set cff e cap matrix_set_time ≡ ASSERT (valid_edge e) ⪢ mop_matrix_set matrix_set_time cff e cap"
definition (in Network) resCap_cf_impl_aux :: "nat ⇒ (nat × nat ⇒ 'capacity) ⇒ (nat × nat) list ⇒ 'capacity nrest"
where "resCap_cf_impl_aux matrix_lookup_time cf p ≡
case p of
[] ⇒ RETURNT (0::'capacity)
| (e#p) ⇒ do {
cap ← cf_get cf e matrix_lookup_time;
ASSERT (distinct p);
nfoldli
p (λ_. True)
(λe cap. do {
cape ← cf_get cf e matrix_lookup_time;
mop_min 10 cape cap
})
cap
}"
abbreviation "resCap_cf_impl == resCap_cf_impl_aux matrix_lookup_time cf"
definition (in -) "resCap_cf_impl_time_aux n v1 = 1 + (v1+10) * n"
abbreviation "resCap_cf_impl_time n ≡ resCap_cf_impl_time_aux n matrix_lookup_time"
lemma resCap_cf_impl_time_mono: "n ≤ m ⟹ resCap_cf_impl_time n ≤ resCap_cf_impl_time m"
unfolding resCap_cf_impl_time_aux_def by simp
lemma resCap_cf_impl_refine:
assumes AUG: "cf.isSimplePath s p t"
shows "resCap_cf_impl p ≤ SPECT (emb (λr. r = resCap_cf cf p) (resCap_cf_impl_time (length p)))"
proof -
note [simp del] = Min_insert
note [simp] = Min_insert[symmetric]
from AUG[THEN cf.isSPath_distinct]
have "distinct p" .
moreover from AUG cf.isPath_edgeset have "set p ⊆ cf.E"
by (auto simp: cf.isSimplePath_def)
hence "set p ⊆ Collect valid_edge"
using cf.E_ss_VxV by simp
moreover from AUG have "p≠[]" by (auto simp: s_not_t)
then obtain e p' where "p=e#p'" by (auto simp: neq_Nil_conv)
ultimately show ?thesis
unfolding resCap_cf_impl_aux_def resCap_cf_def cf_get_def
apply (simp only: list.case)
apply(rule T_specifies_I)
apply(vcg'‹-› rules: matrix_get )
apply(rule nfoldli_rule[where I="λl l' cap.
cap = Min (cf`insert e (set l))
∧ set (l@l') ⊆ Collect valid_edge" and body_time="matrix_lookup_time+10"
and P="(λr. r = Min {cf ea |ea. ea ∈ set (e # p')})", THEN T_specifies_rev , THEN T_conseq4])
apply (auto intro!: arg_cong[where f=Min]) []
subgoal apply(rule T_specifies_I) apply(vcg'‹-› rules: mop_min matrix_get)
by (auto simp add: emb_le_Some_conv numeral_eq_enat intro!: arg_cong[where f=Min])
apply (auto simp: emb_eq_Some_conv Some_le_emb'_conv resCap_cf_impl_time_aux_def intro!: arg_cong[where f=Min])
subgoal by (progress ‹clarsimp›)
done
qed
definition (in Graph)
"augment_edge e cap ≡ (c(
e := c e - cap,
prod.swap e := c (prod.swap e) + cap))"
lemma (in Graph) augment_cf_inductive:
fixes e cap s t
defines "c' ≡ augment_edge e cap"
assumes P: "isSimplePath s (e#p) t"
shows "augment_cf (insert e (set p)) cap = Graph.augment_cf c' (set p) cap"
and "∃s'. Graph.isSimplePath c' s' p t"
proof -
obtain u v where [simp]: "e=(u,v)" by (cases e)
from isSPath_no_selfloop[OF P] have [simp]: "⋀u. (u,u)∉set p" "u≠v" by auto
from isSPath_nt_parallel[OF P] have [simp]: "(v,u)∉set p" by auto
from isSPath_distinct[OF P] have [simp]: "(u,v)∉set p" by auto
show "augment_cf (insert e (set p)) cap = Graph.augment_cf c' (set p) cap"
apply (rule ext)
unfolding Graph.augment_cf_def c'_def Graph.augment_edge_def
by auto
have "Graph.isSimplePath c' v p t"
unfolding Graph.isSimplePath_def
apply rule
apply (rule transfer_path)
unfolding Graph.E_def
apply (auto simp: c'_def Graph.augment_edge_def) []
using P apply (auto simp: isSimplePath_def) []
using P apply (auto simp: isSimplePath_def) []
done
thus "∃s'. Graph.isSimplePath c' s' p t" ..
qed
definition (in Network) "augment_edge_impl_aux matrix_lookup_time matrix_set_time cff e cap ≡ do {
v ← cf_get cff e matrix_lookup_time; cf ← cf_set cff e (v-cap) matrix_set_time;
e ← mop_swap 3 e;
v ← cf_get cf e matrix_lookup_time; cf ← cf_set cf e (v+cap) matrix_set_time;
RETURNT cf
}"
abbreviation "augment_edge_impl == augment_edge_impl_aux matrix_lookup_time matrix_set_time"
definition (in -) "augment_edge_impl_time_aux v1 v2 = 2* v1 + 2*v2+3"
abbreviation "augment_edge_impl_time == augment_edge_impl_time_aux matrix_lookup_time matrix_set_time"
lemma augment_edge_impl_refine:
assumes "valid_edge e" "∀u. e≠(u,u)"
shows "augment_edge_impl cff e cap
≤ SPECT (emb (λr. r = Graph.augment_edge cff e cap) augment_edge_impl_time)"
using assms
unfolding augment_edge_impl_aux_def Graph.augment_edge_def
unfolding cf_get_def cf_set_def apply simp
apply(rule T_specifies_I)
apply (vcg'‹auto› rules: matrix_get matrix_set mop_swap) apply (auto simp: emb_le_Some_conv augment_edge_impl_time_aux_def one_enat_def numeral_eq_enat)
done
definition (in Network) augment_cf_impl_aux
where
"augment_cf_impl_aux matrix_lookup_time matrix_set_time cff p x ≡ do {
RECT (λD. λ
([],cf) ⇒ RETURNT cf
| (e#p,cf) ⇒ do {
cf ← augment_edge_impl_aux matrix_lookup_time matrix_set_time cf e x;
D (p,cf)
}
) (p,cff)
}"
abbreviation "augment_cf_impl cff p x == augment_cf_impl_aux matrix_lookup_time matrix_set_time cff p x"
text ‹Deriving the corresponding recursion equations›
lemma augment_cf_impl_simps[simp]:
"augment_cf_impl cff [] x = RETURNT cff"
"augment_cf_impl cff (e#p) x = do {
cf ← augment_edge_impl cff e x;
augment_cf_impl cf p x}"
apply (simp add: augment_cf_impl_aux_def)
apply (subst RECT_unfold, refine_mono)
apply simp
apply (simp add: augment_cf_impl_aux_def)
apply (subst RECT_unfold, refine_mono)
apply simp
done
definition (in -) "augment_cf_impl_time_aux n v1 = 1 + n * v1 "
abbreviation "augment_cf_impl_time n ≡ augment_cf_impl_time_aux n augment_edge_impl_time"
lemma augment_cf_impl_time_mono: "n ≤ m ⟹ augment_cf_impl_time n ≤ augment_cf_impl_time m"
unfolding augment_cf_impl_time_aux_def by simp
lemma augment_cf_impl_aux:
assumes "∀e∈set p. valid_edge e"
assumes "∃s. Graph.isSimplePath cf s p t"
shows "augment_cf_impl cf p x ≤ SPECT [Graph.augment_cf cf (set p) x↦ augment_cf_impl_time (length p)]"
using assms unfolding augment_cf_impl_time_aux_def
proof (induction p arbitrary: cf)
case Nil
then show ?case
by (auto simp add: RETURNT_def le_fun_def one_enat_def Graph.augment_cf_empty)
next
case (Cons a p)
from Cons(2,3)
show ?case
apply clarsimp
apply (subst Graph.augment_cf_inductive, assumption)
apply(rule T_specifies_I)
apply (vcg'‹-› rules: )
apply(rule augment_edge_impl_refine[THEN T_specifies_rev , THEN T_conseq4])
apply (auto dest: Graph.isSPath_no_selfloop)
apply(rule Cons(1)[THEN T_specifies_rev , THEN T_conseq4])
apply simp apply (auto simp add: emb_eq_Some_conv) []
apply (drule Graph.augment_cf_inductive(2)[where cap=x]; simp)
by (auto simp add: emb_eq_Some_conv split: if_splits)
qed
lemma augment_cf_impl_refine:
assumes "Graph.isSimplePath cf s p t"
shows "augment_cf_impl cf p x ≤ SPECT [Graph.augment_cf cf (set p) x↦ augment_cf_impl_time (length p)]"
apply (rule augment_cf_impl_aux)
using assms cf.E_ss_VxV apply (auto simp: cf.isSimplePath_def dest!: cf.isPath_edgeset) []
using assms by blast
end
locale EdKa_Res_Up = Network c s t for c :: "'capacity::linordered_idom graph" and s t +
fixes shortestpath_time :: nat
and matrix_lookup_time matrix_set_time :: nat
and init_graph :: "nat ⇒ nat"
assumes augment_progress[simp]: "0 ≠ enat shortestpath_time"
assumes [simp]: "matrix_lookup_time > 0"
begin
definition (in -) "augment_with_path_time_aux v1 v2 cV = RGraph_impl.resCap_cf_impl_time v1 cV
+ RGraph_impl.augment_cf_impl_time v1 v2 cV"
abbreviation "augment_with_path_time ≡ augment_with_path_time_aux matrix_lookup_time matrix_set_time (card V)"
thm Finite_Graph.isShortestPath_length_less_V
lemma tTT:
fixes ss tt cc
assumes "Graph.isShortestPath cc ss p tt" "ss∈V" "RGraph c s t cc"
shows "RGraph_impl.resCap_cf_impl_time matrix_lookup_time (length p)
+ RGraph_impl.augment_cf_impl_time matrix_lookup_time matrix_set_time (length p) ≤ augment_with_path_time "
proof -
interpret R: RGraph c s t cc by fact
from R.cf.isShortestPath_length_less_V assms have "length p < card V" by simp
then have le: "length p ≤ card V" by auto
thm RGraph_impl.augment_cf_impl_time_mono
term RGraph_impl.resCap_cf_impl_time
have "RGraph_impl.resCap_cf_impl_time matrix_lookup_time (length p) ≤ RGraph_impl.resCap_cf_impl_time matrix_lookup_time (card V)"
apply(rule RGraph_impl.resCap_cf_impl_time_mono)
using assms(3) le by (auto simp: RGraph_impl_def RGraph_impl_axioms_def)
moreover
have "RGraph_impl.augment_cf_impl_time matrix_lookup_time matrix_set_time (length p) ≤ RGraph_impl.augment_cf_impl_time matrix_lookup_time matrix_set_time (card V)"
apply(rule RGraph_impl.augment_cf_impl_time_mono)
using assms(3) le by (auto simp: RGraph_impl_def RGraph_impl_axioms_def)
ultimately
show ?thesis unfolding augment_with_path_time_aux_def by simp
qed
interpretation Ed_Res: EdKa_Res c s t shortestpath_time augment_with_path_time
apply standard by simp
lemmas find_shortest_augmenting_spec_cf = Ed_Res.find_shortest_augmenting_spec_cf_def
abbreviation "resCap_cf_impl' cf p ≡ RGraph_impl.resCap_cf_impl c cf matrix_lookup_time p"
abbreviation "augment_cf_impl' cf p bn ≡ RGraph_impl.augment_cf_impl c matrix_lookup_time matrix_set_time cf p bn"
abbreviation "find_shortest_augmenting_spec_cf ≡ Ed_Res.find_shortest_augmenting_spec_cf"
definition "augment cf p = do {
bn ← resCap_cf_impl' cf p;
augment_cf_impl' cf p bn }"
text ‹Finally, we arrive at the algorithm where augmentation is
implemented algorithmically: ›
definition "edka3 ≡ do {
cf ← SPECT [c ↦ init_graph (card V)];
(cf,_) ← whileT
(λ(cf,brk). ¬brk)
(λ(cf,_). do {
ASSERT (RGraph c s t cf);
p ← find_shortest_augmenting_spec_cf cf;
case p of
None ⇒ RETURNT (cf,True)
| Some p ⇒ do {
ASSERT (p≠[]);
ASSERT (Graph.isShortestPath cf s p t);
cf ← augment cf p;
ASSERT (RGraph c s t cf);
RETURNT (cf, False)
}
})
(cf,False);
ASSERT (RGraph c s t cf);
f ← RETURNT (flow_of_cf cf);
RETURNT f
}"
lemma augment_refine[refine]: "RGraph c s t x1 ⟹ Graph.isShortestPath x1 s pc t ⟹ x1'=x1 ⟹ pc=pc' ⟹
augment x1 pc ≤ ⇓Id (SPECT [Graph.augment_cf x1' (set pc') (resCap_cf x1' pc') ↦ enat augment_with_path_time])"
unfolding augment_def apply simp
apply(rule T_specifies_I)
apply(vcg'‹-› rules: RGraph_impl.resCap_cf_impl_refine[THEN T_specifies_rev , THEN T_conseq4]
RGraph_impl.augment_cf_impl_refine[THEN T_specifies_rev , THEN T_conseq4] )
unfolding RGraph_impl_def apply (simp add: RGraph_impl_axioms_def)
apply(auto simp: RGraph_impl_axioms_def intro: Graph.shortestPath_is_simple)[]
apply (simp add: RGraph_impl_axioms_def)
apply(auto intro: Graph.shortestPath_is_simple)[]
apply (auto split: if_splits simp: RGraph_impl_axioms_def emb_eq_Some_conv)
apply(subst tTT )
by auto
lemma edka3_refine: "edka3 ≤ ⇓Id Ed_Res.edka2"
unfolding edka3_def Ed_Res.edka2_def
apply (refine_rcg augment_refine)
apply refine_dref_type
by auto
lemma edka3_correct: "edka3 ≤ ⇓Id (SPECT (emb isMaxFlow (enat (EdKa.edka_time c shortestpath_time augment_with_path_time init_graph))))"
apply(rule order.trans) apply(rule edka3_refine)
using Ed_Res.edka2_correct by simp
end
term Augmenting_Path_BFS.bfs
locale EdKa_Res_Bfs = Network c s t for c :: "'capacity::linordered_idom graph" and s t +
fixes set_insert_time map_dom_member_time set_pick_extract_time :: "nat ⇒ nat"
and get_succs_list_time :: nat
and map_update_time :: "nat ⇒ nat"
and list_append_time ::nat
and map_lookup_time :: "nat ⇒ nat"
and set_empty_time set_isempty_time init_state_time :: nat
and matrix_lookup_time matrix_set_time init_get_succs_list_time :: nat
and init_graph :: "nat ⇒ nat"
assumes [simp]: "⋀c. map_lookup_time c > 0"
assumes [simp]: "⋀c. set_pick_extract_time c > 0"
assumes [simp]: "matrix_lookup_time > 0"
begin
term Pre_BFS_Impl.pre_bfs_time
definition (in -) "shortest_path_time_aux cV cE v1 v2 v3 v4 v5 v7 v8 v9 v10 v11 v12 =
Pre_BFS_Impl.pre_bfs_time (v1 cV) (v2 cV) v4
(v5 cV) (v3 cV) v7 v8 v9 v12 cE
+ valid_PRED_impl.extract_rpath_time v10 (v11 cV) cV"
abbreviation "shortest_path_time == shortest_path_time_aux (card V) (2 * card E) set_insert_time map_dom_member_time set_pick_extract_time
get_succs_list_time map_update_time set_empty_time set_isempty_time init_state_time list_append_time map_lookup_time init_get_succs_list_time"
lemma [simp]: "enat shortest_path_time ≠ 0"
unfolding shortest_path_time_aux_def using Pre_BFS_Impl.pre_bfs_time_progress[unfolded Pre_BFS_Impl_def, of "set_pick_extract_time (card V)"]
apply(auto)
by (metis add_is_0 enat_0_iff(1) not_gr_zero)
sublocale edru: EdKa_Res_Up c s t shortest_path_time matrix_lookup_time matrix_set_time init_graph
apply standard by auto
abbreviation "resCap_cf_impl'' cf p ≡ edru.resCap_cf_impl' cf p"
abbreviation "augment_cf_impl'' cf p bn ≡ edru.augment_cf_impl' cf p bn"
definition "MYbfs cf ss tt = Augmenting_Path_BFS.bfs cf (set_insert_time (card (Graph.V cf))) (map_dom_member_time (card (Graph.V cf)))
get_succs_list_time (map_update_time (card (Graph.V cf))) (set_pick_extract_time (card (Graph.V cf)))
list_append_time (map_lookup_time (card (Graph.V cf))) set_empty_time set_isempty_time init_state_time init_get_succs_list_time ss tt "
subsection ‹Refinement to use BFS›
text ‹We refine the Edmonds-Karp algorithm to use breadth first search (BFS)›
definition "edka4 ≡ do {
cf ← SPECT [c ↦ init_graph (card V)];
(cf,_) ← whileT
(λ(cf,brk). ¬brk)
(λ(cf,_). do {
ASSERT (RGraph c s t cf);
ASSERT ((Graph.V cf) = (Graph.V c));
p ← MYbfs cf s t;
case p of
None ⇒ RETURNT (cf,True)
| Some p ⇒ do {
ASSERT (p≠[]);
ASSERT (Graph.isShortestPath cf s p t);
bn ← edru.resCap_cf_impl' cf p;
cf ← edru.augment_cf_impl' cf p bn;
ASSERT (RGraph c s t cf);
RETURNT (cf, False)
}
})
(cf,False);
ASSERT (RGraph c s t cf);
f ← RETURNT (flow_of_cf cf);
RETURNT f
}"
text ‹A shortest path can be obtained by BFS›
lemma bfs_refines_shortest_augmenting_spec: fixes cf shows
"cf'=cf ⟹ MYbfs cf s t ≤ ⇓Id (edru.find_shortest_augmenting_spec_cf cf')"
unfolding edru.find_shortest_augmenting_spec_cf apply safe
proof (rule le_R_ASSERTI, goal_cases)
case 1
interpret BFS: Augmenting_Path_BFS cf "set_insert_time (card (Graph.V cf))" "map_dom_member_time (card (Graph.V cf))"
get_succs_list_time "map_update_time (card (Graph.V cf))" "set_pick_extract_time (card (Graph.V cf))"
list_append_time "map_lookup_time (card (Graph.V cf))" set_empty_time set_isempty_time init_state_time
apply standard by auto
have -: "BFS.V = V"
using "1" RGraph.this_loc_rpg RPreGraph.resV_netV by blast
have "BFS.E ⊆ E ∪ (E)¯"
using "1" RGraph.this_loc_rpg RPreGraph.cfE_ss_invE by blast
then have "card (BFS.E) ≤ card (E ∪ (E)¯)"
apply(rule card_mono[rotated]) by auto
also have "… ≤ 2 * card E" apply(rule order.trans[OF card_Un_le])
by simp
finally have "card BFS.E ≤ 2 * card E" .
thm BFS.bfs_correct
have *: "BFS.bfs_time s t ≤ shortest_path_time"
apply(simp add: shortest_path_time_aux_def Augmenting_Path_BFS.bfs_time_def - Augmenting_Path_BFS_def)
apply(rule pre_bfs_time_aux_mono) by fact
show ?case
apply (rule order_trans) unfolding MYbfs_def
apply (rule BFS.bfs_correct)
using RPreGraph.resV_netV[OF RGraph.this_loc_rpg, OF 1(2)]
apply (simp add: RPreGraph.resV_netV[OF RGraph.this_loc_rpg, OF 1(2)])
apply (simp add: RPreGraph.resV_netV[OF RGraph.this_loc_rpg, OF 1(2)])
apply(rule SPECT_ub') using * apply (auto simp: le_fun_def)
done
qed
lemma edka4_refine: "edka4 ≤ ⇓Id edru.edka3"
unfolding edka4_def edru.edka3_def edru.augment_def nres_bind_assoc
apply(refine_rcg bfs_refines_shortest_augmenting_spec)
apply refine_dref_type
by (simp_all add: RPreGraph.resV_netV[OF RGraph.this_loc_rpg] )
lemma edka4_correct: "edka4 ≤ ⇓ Id (SPECT (emb isMaxFlow (enat (EdKa.edka_time c shortest_path_time edru.augment_with_path_time init_graph))))"
apply(rule order.trans) apply(rule edka4_refine)
using edru.edka3_correct by simp
end
locale Succ_Impl = Graph c for c :: "'capacity::linordered_idom graph" +
fixes list_append_time matrix_lookup_time :: nat
begin
subsection ‹Implementing the Successor Function for BFS›
text ‹We implement the successor function in two steps.
The first step shows how to obtain the successor function by
filtering the list of adjacent nodes. This step contains the idea
of the implementation. The second step is purely technical, and makes
explicit the recursion of the filter function as a recursion combinator
in the monad. This is required for the Sepref tool.
›
text ‹Note: We use @{term filter_rev} here, as it is tail-recursive,
and we are not interested in the order of successors.›
definition (in Graph) "rg_succ am cf u ≡
filter_rev (λv. cf (u,v) > 0) (am u)"
lemma (in RGraph) rg_succ_ref1: "⟦is_adj_map am⟧
⟹ (rg_succ am cf u, Graph.E cf``{u}) ∈ ⟨Id⟩list_set_rel"
unfolding Graph.E_def
apply (clarsimp simp: list_set_rel_def br_def rg_succ_def filter_rev_alt;
intro conjI)
using cfE_ss_invE resE_nonNegative
apply (auto
simp: is_adj_map_def less_le Graph.E_def
simp del: cf.zero_cap_simp zero_cap_simp) []
apply (auto simp: is_adj_map_def) []
done
definition (in Graph) ps_get_op :: "_ ⇒ node ⇒ node list nrest"
where "ps_get_op am u ≡ ASSERT (u∈V) ⪢ SPECT [am u↦1]"
definition monadic_filter_rev_aux
:: "'a list ⇒ ('a ⇒ bool nrest) ⇒ 'a list ⇒ 'a list nrest"
where
"monadic_filter_rev_aux a P l ≡ RECT (λ D. (λ(l,a). case l of
[] ⇒ RETURNT a
| (v#l) ⇒ do {
c ← P v;
a ← (if c then
mop_append (λ_. list_append_time) v a
else
RETURNT a
);
D (l,a)
}
)) (l,a)"
lemma monadic_filter_rev_aux_rule:
assumes P_rule: "⋀x. x∈set l ⟹ P x ≤ SPECT (emb (λr. r=Q x) P_t)"
shows "monadic_filter_rev_aux a P l ≤ SPECT (emb (λr. r=filter_rev_aux a Q l) (1+ length l * (P_t+list_append_time)))"
using assms
proof (induction l arbitrary: a)
case Nil
then show ?case
apply (unfold monadic_filter_rev_aux_def) []
apply (subst RECT_unfold, refine_mono)
apply (fold monadic_filter_rev_aux_def) []
apply simp unfolding emb'_def by (auto simp: pw_le_iff)
next
case (Cons a l)
show ?case
apply (unfold monadic_filter_rev_aux_def) []
apply (subst RECT_unfold, refine_mono)
apply (fold monadic_filter_rev_aux_def) []
apply(rule T_specifies_I)
apply (vcg'‹-› rules: mop_append Cons(2)[THEN T_specifies_rev, THEN T_conseq4]
Cons(1)[THEN T_specifies_rev, THEN T_conseq4] )
apply simp apply simp
apply safe
apply(rule Cons(1)[OF Cons(2), THEN T_specifies_rev, THEN T_conseq4] )
apply simp
apply(simp add: Some_le_emb'_conv Some_eq_emb'_conv)
apply(rule Cons(1)[OF Cons(2), THEN T_specifies_rev, THEN T_conseq4] )
apply simp
apply(simp add: Some_le_emb'_conv Some_eq_emb'_conv)
done
qed
definition "monadic_filter_rev = monadic_filter_rev_aux []"
lemma monadic_filter_rev_rule:
assumes "⋀x. x∈set l ⟹ P x ≤ SPECT (emb (λr. r=Q x) P_t)"
shows "monadic_filter_rev P l ≤ SPECT (emb (λr. r=filter_rev Q l) (1+ length l * (P_t+list_append_time)))"
using monadic_filter_rev_aux_rule[where a="[]"] assms
by (auto simp: monadic_filter_rev_def filter_rev_def)
definition "rg_succ2 am cf u ≡ do {
l ← ps_get_op am u;
monadic_filter_rev (λv. do {
x ← Network.cf_get c cf (u,v) matrix_lookup_time;
RETURNT (x>0)
}) l
}"
definition "rg_succ_time len = (2+ len * (matrix_lookup_time+list_append_time))"
lemma rg_succ_ref2:
assumes PS: "is_adj_map am" and V: "u∈V"
and RG: "RGraph c s t cf"
shows "rg_succ2 am cf u ≤ SPECT [rg_succ am cf u ↦ rg_succ_time (length (am u)) ]"
proof -
note n = RG[unfolded RGraph_def, THEN conjunct1]
have "∀v∈set (am u). valid_edge (u,v)"
using PS V
by (auto simp: is_adj_map_def Graph.V_def)
thm monadic_filter_rev_rule
thus ?thesis
unfolding rg_succ2_def rg_succ_def ps_get_op_def
unfolding Network.cf_get_def[OF n] apply simp
apply(rule T_specifies_I)
apply (vcg'‹-› rules: monadic_filter_rev_rule[where Q="(λv. 0 < cf (u, v))" and P_t="matrix_lookup_time", THEN T_specifies_rev, THEN T_conseq4] )
subgoal
apply(rule T_specifies_I)
apply (vcg'‹-› rules: matrix_get) by(auto simp: Some_le_emb'_conv)
apply (simp_all add: V Some_le_emb'_conv emb_eq_Some_conv rg_succ_time_def one_enat_def)
done
qed
term RPreGraph
lemma rg_succ_ref:
assumes A: "is_adj_map am"
assumes B: "u∈V" and RG: "RGraph c s t cf"
shows "rg_succ2 am cf u ≤ SPECT (emb (λl. (l,(Graph.E cf)``{u}) ∈ ⟨Id⟩list_set_rel) (rg_succ_time (length (am u))))"
apply(rule T_specifies_I)
apply (vcg'‹-› rules: rg_succ_ref2[OF A B RG, THEN T_specifies_rev, THEN T_conseq4])
using RGraph.rg_succ_ref1[OF RG A, of u]
apply(auto simp add:Some_eq_emb'_conv Some_le_emb'_conv split: if_splits)
done
lemma rg_succ_ref':
assumes A: "is_adj_map am"
assumes B: "u∈V" and RG: "RGraph c s t cf"
shows "rg_succ2 am cf u ≤ ⇓ (⟨nat_rel⟩list_set_rel) (SPECT [Graph.E cf `` {u} ↦ (rg_succ_time (length (am u)))])"
apply(rule order.trans[OF rg_succ_ref[OF assms]])
apply(rule SPECT_refine)
by (simp add: Some_eq_emb'_conv list_set_rel_def br_def )
end
locale EdKa_Tab = Network c s t for c :: "'capacity::linordered_idom graph" and s t +
fixes set_insert_time map_dom_member_time set_pick_extract_time map_update_time :: "nat ⇒ nat"
and list_append_time ::nat
and map_lookup_time :: "nat ⇒ nat"
and set_empty_time set_isempty_time init_state_time :: nat
and matrix_lookup_time matrix_set_time :: nat
and init_graph_time :: "nat ⇒ nat"
and init_adjm_time :: nat
assumes [simp]: "⋀c. map_lookup_time c > 0"
assumes [simp]: "⋀c. set_pick_extract_time c > 0"
assumes [simp]: "matrix_lookup_time > 0"
begin
subsection ‹Adding Tabulation of Input›
text ‹
Next, we add functions that will be refined to tabulate the input of
the algorithm, i.e., the network's capacity matrix and adjacency map,
into efficient representations.
The capacity matrix is tabulated to give the initial residual graph,
and the adjacency map is tabulated for faster access.
Note, on the abstract level, the tabulation functions are just identity,
and merely serve as marker constants for implementation.
›
definition (in Network) init_cf :: "(nat ⇒ nat) ⇒ 'capacity graph nrest"
where "init_cf init_graph_time ≡ SPECT [ c ↦ init_graph_time (card V) ]"
definition (in Network) init_ps :: "nat ⇒ (node ⇒ node list) ⇒ _"
where "init_ps init_adjm_time am ≡ ASSERT (is_adj_map am) ⪢ SPECT [ am ↦ init_adjm_time ]"
definition (in Network) compute_rflow :: "'capacity graph ⇒ 'capacity flow nrest"
where
"compute_rflow cf ≡ ASSERT (RGraph c s t cf) ⪢ RETURNT (flow_of_cf cf)"
definition (in -) get_succs_list_time_aux where
"get_succs_list_time_aux matrix_lookup_time list_append_time = (matrix_lookup_time+list_append_time)"
abbreviation "get_succs_list_time ≡ get_succs_list_time_aux matrix_lookup_time list_append_time "
term Augmenting_Path_BFS.bfs2
definition "MYrg_succ2 am cf u = Succ_Impl.rg_succ2 c list_append_time matrix_lookup_time am cf u"
definition (in -) "bfs2_op_aux c s t
set_insert_time
map_dom_member_time
map_update_time
set_pick_time
list_append_time
map_lookup_time
set_empty_time
set_isempty_time
matrix_lookup_time
am cf init_state ≡
Augmenting_Path_BFS.bfs2 cf set_insert_time map_dom_member_time map_update_time set_pick_time
list_append_time map_lookup_time set_empty_time set_isempty_time (Succ_Impl.rg_succ2 c list_append_time matrix_lookup_time am cf) init_state s t "
abbreviation "bfs2_op am cf init_state ≡ bfs2_op_aux c s t (set_insert_time (card (Graph.V cf)))
(map_dom_member_time (card (Graph.V cf)))
(map_update_time (card (Graph.V cf)))
(set_pick_extract_time (card (Graph.V cf)))
list_append_time
(map_lookup_time (card (Graph.V cf)))
set_empty_time
set_isempty_time
matrix_lookup_time am cf init_state"
text ‹We split the algorithm into a tabulation function, and the
running of the actual algorithm:›
definition (in Network) "edka5_tabulate init_graph_time init_adjm_time am ≡ do {
cf ← init_cf init_graph_time;
am ← init_ps init_adjm_time am;
RETURNT (cf,am)
}"
abbreviation "prepare_time == (λn. init_graph_time n + init_adjm_time)"
sublocale edka: EdKa_Res_Bfs c s t set_insert_time map_dom_member_time set_pick_extract_time
get_succs_list_time
map_update_time
list_append_time map_lookup_time set_empty_time set_isempty_time init_state_time
matrix_lookup_time matrix_set_time 2 prepare_time
apply(standard) by auto
lemma pff: "RGraph c s t cf ⟹ (Graph.V cf) = (Graph.V c)"
using RGraph.this_loc_rpg RPreGraph.resV_netV by fastforce
definition "edka5_run cf am init_state ≡ do {
(cf,_) ← whileT
(λ(cf,brk). ¬brk)
(λ(cf,_). do {
ASSERT (RGraph c s t cf);
ASSERT ((Graph.V cf) = (Graph.V c));
p ← bfs2_op am cf init_state;
case p of
None ⇒ RETURNT (cf,True)
| Some p ⇒ do {
ASSERT (p≠[]);
ASSERT (Graph.isShortestPath cf s p t);
bn ← edka.resCap_cf_impl'' cf p;
cf ← edka.augment_cf_impl'' cf p bn;
ASSERT (RGraph c s t cf);
RETURNT (cf, False)
}
})
(cf,False);
f ← compute_rflow cf;
RETURNT f
}"
definition "edka5 am init_state ≡ do {
(cf,am) ← edka5_tabulate init_graph_time init_adjm_time am ;
edka5_run cf am init_state
}"
lemma k: "((a, b), aa, ba) ∈ Id ×⇩r bool_rel ⟹ a=aa" by auto
lemma is_adj_mapD_V: "⋀am u. is_adj_map am ⟹ u ∈ V ⟹ distinct (am u) ∧ set (am u) ⊆ V"
unfolding is_adj_map_def unfolding V_def by auto
lemma is_adj_map_app_le_V: "is_adj_map am ⟹ u ∈ V ⟹ length (am u) ≤ card V"
apply(auto dest!: is_adj_mapD_V)
apply(rule order.trans[where b="card (set (am u))"]) using distinct_card[symmetric]
apply fastforce apply(rule card_mono)
by auto
lemma (in RPreGraph) E_is_cfE: "E ∪ E¯ = cf.E ∪ cf.E¯"
using E_ss_cfinvE cfE_ss_invE by blast
lemma (in RPreGraph) hh: assumes "is_adj_map am"
"u ∈ V"
shows "length (am u) ≤ card (cf.E `` {u}) + card (cf.E¯ `` {u})"
proof -
have *: "(E``{u} ∪ E¯``{u}) = (cf.E)``{u} ∪ cf.E¯``{u}" using E_is_cfE by auto
from assms(1) have [simp]: "distinct (am u)" and "set (am u) = E``{u} ∪ E¯``{u}" by(auto simp: is_adj_map_def)
then have "card (E``{u} ∪ E¯``{u}) = card (set (am u))" by simp
also have "… = length (am u)" by(auto intro: distinct_card)
finally have "length (am u) = card (E``{u} ∪ E¯``{u})" by simp
also have "… = card ((cf.E)``{u} ∪ cf.E¯``{u})" using * by auto
also have "… <= card ((cf.E)``{u}) + card ( cf.E¯``{u})" by(rule card_Un_le)
finally show ?thesis .
qed
lemma (in Graph) hh: assumes "is_adj_map am"
"RGraph c s t cf"
"u ∈ V"
shows "length (am u) ≤ card (Graph.E cf `` {u}) + card ((Graph.E cf)¯ `` {u})"
proof -
have "RPreGraph c s t cf" using assms(2) RGraph.this_loc_rpg by auto
from RPreGraph.hh[OF this] assms(1,3) show ?thesis by blast
qed
abbreviation "augment am R ≡ {((cc, cam), ac). (cc, ac)∈R ∧ cam = am}"
lemma augment_conv: "⇓ (augment am Id) (SPECT [a ↦ tt]) = (SPECT [ (a,am) ↦ tt])"
by (auto simp: pw_eq_iff bot_option_def conc_fun_def dest: Sup_Some )
lemma edka_tab: "is_adj_map am ⟹ edka5_tabulate init_graph_time init_adjm_time am ≤ ⇓ (augment am Id) (SPECT [ c ↦ enat (init_graph_time (card V) + init_adjm_time)])"
unfolding edka5_tabulate_def init_cf_def init_ps_def augment_conv
apply(rule T_specifies_I)
apply(vcg'‹-› ) by auto
lemma rg_succ2_impl: "is_adj_map am ⟹
RGraph c s t cf ⟹
(ui, u) ∈ nat_rel ⟹
u ∈ Graph.V cf ⟹
Succ_Impl.rg_succ2 c list_append_time matrix_lookup_time am cf ui
≤ ⇓ (⟨nat_rel⟩list_set_rel) (SPECT [Graph.E cf `` {u} ↦ enat (2 + (card (Graph.E cf `` {u}) + card ((Graph.E cf)¯ `` {u})) * get_succs_list_time)])"
unfolding MYrg_succ2_def
apply(rule order.trans)
apply(rule Succ_Impl.rg_succ_ref') apply simp
apply(simp add: RPreGraph.resV_netV[OF RGraph.this_loc_rpg])
apply simp
apply(rule nrest_Rel_mono)
apply (auto simp add: le_fun_def get_succs_list_time_aux_def Succ_Impl.rg_succ_time_def
RPreGraph.resV_netV[OF RGraph.this_loc_rpg] is_adj_map_app_le_V)
subgoal apply(subst Graph.hh) by auto
done
lemma edka5_refine:
assumes "is_adj_map am"
and init_state_impl:
"⋀src. init_state src ≤ ⇓Id (SPECT [ (False,[src↦src],{src},{},0::nat) ↦ init_state_time ])"
shows "is_adj_map am ⟹ edka5 am init_state ≤ ⇓Id edka.edka4"
unfolding edka5_def edka5_run_def
edka.edka4_def compute_rflow_def
Let_def bfs2_op_aux_def edka.MYbfs_def
apply(refine_rcg edka_tab Augmenting_Path_BFS.bfs2_refine )
apply refine_dref_type
apply simp_all
apply(rule R_intro)
apply(rule Augmenting_Path_BFS.bfs2_refine)
apply(simp add: Augmenting_Path_BFS_def)
subgoal
by (refine_rcg rg_succ2_impl)
subgoal
apply(rule R_intro)
by (refine_rcg init_state_impl)
done
thm edka.edka4_correct
lemma edka5_correct: "⟦is_adj_map am; ⋀src. init_state src ≤ SPECT [ (False,[src↦src],{src},{},0::nat) ↦ init_state_time] ⟧ ⟹ edka5 am init_state ≤ ⇓ Id (SPECT (emb isMaxFlow (enat (EdKa.edka_time c edka.shortest_path_time (EdKa_Res_Up.augment_with_path_time c matrix_lookup_time matrix_set_time) prepare_time))))"
apply(rule order.trans) apply(rule edka5_refine)
using edka.edka4_correct by simp_all
end
end