Theory Fifo_Push_Relabel_Impl
section ‹Implementation of the FIFO Push/Relabel Algorithm›
theory Fifo_Push_Relabel_Impl
imports
Fifo_Push_Relabel
Prpu_Common_Impl
begin
subsection ‹Basic Operations›
context Network_Impl
begin
subsubsection ‹Queue›
text ‹Obtain the empty queue.›
definition q_empty :: "node list nres" where
"q_empty ≡ return []"
text ‹Check whether a queue is empty.›
definition q_is_empty :: "node list ⇒ bool nres" where
"q_is_empty Q ≡ return ( Q = [] )"
text ‹Enqueue a node.›
definition q_enqueue :: "node ⇒ node list ⇒ node list nres" where
"q_enqueue v Q ≡ do {
assert (v∈V);
return (Q@[v])
}"
text ‹Dequeue a node.›
definition q_dequeue :: "node list ⇒ (node × node list) nres" where
"q_dequeue Q ≡ do {
assert (Q≠[]);
return (hd Q, tl Q)
}"
end
subsection ‹Refinements to Basic Operations›
context Network_Impl
begin
text ‹In this section, we refine the algorithm to actually use the
basic operations.
›
subsubsection ‹Refinement of Push›
definition "fifo_push2_aux x cf Q ≡ λ(u,v). do {
assert ( (u,v) ∈ E ∪ E¯ );
assert ( u ≠ v );
let Δ = min (x u) (cf (u,v));
let Q = (if v≠s ∧ v≠t ∧ x v = 0 then Q@[v] else Q);
return ((x( u := x u - Δ, v := x v + Δ ),augment_edge_cf cf (u,v) Δ),Q)
}"
lemma fifo_push2_aux_refine:
"⟦((x,cf),f)∈xf_rel; (ei,e)∈Id×⇩rId; (Qi,Q)∈Id⟧
⟹ fifo_push2_aux x cf Qi ei ≤ ⇓(xf_rel ×⇩r Id) (fifo_push f l Q e)"
unfolding fifo_push_def fifo_push2_aux_def
apply refine_vcg
apply (vc_solve simp: xf_rel_def no_self_loop)
subgoal for u v
unfolding push_precond_def using cfE_of_ss_invE by auto
subgoal for u v
proof -
assume [simp]: "Labeling c s t f l"
then interpret Labeling c s t f l .
assume "push_precond f l (u, v)"
then interpret l': push_effect_locale c s t f l u v by unfold_locales
show ?thesis
apply (safe intro!: ext)
using l'.excess'_if l'.Δ_def l'.cf'_alt l'.uv_not_eq(1)
by (auto)
qed
done
definition "fifo_push2 x cf Q ≡ λ(u,v). do {
assert ( (u,v) ∈ E ∪ E¯ );
xu ← x_get x u;
xv ← x_get x v;
cfuv ← cf_get cf (u,v);
cfvu ← cf_get cf (v,u);
let Δ = min xu cfuv;
x ← x_add x u (-Δ);
x ← x_add x v Δ;
cf ← cf_set cf (u,v) (cfuv - Δ);
cf ← cf_set cf (v,u) (cfvu + Δ);
if v≠s ∧ v≠t ∧ xv = 0 then do {
Q ← q_enqueue v Q;
return ((x,cf),Q)
} else
return ((x,cf),Q)
}"
lemma fifo_push2_refine[refine]:
assumes "((x,cf),f)∈xf_rel" "(ei,e)∈Id×⇩rId" "(Qi,Q)∈Id"
shows "fifo_push2 x cf Qi ei ≤ ⇓(xf_rel ×⇩r Id) (fifo_push f l Q e)"
proof -
have "fifo_push2 x cf Qi ei ≤ (fifo_push2_aux x cf Qi ei)"
unfolding fifo_push2_def fifo_push2_aux_def
unfolding x_get_def x_add_def cf_get_def cf_set_def q_enqueue_def
unfolding augment_edge_cf_def
apply (simp only: nres_monad_laws)
apply refine_vcg
using E_ss_VxV
by auto
also note fifo_push2_aux_refine[OF assms]
finally show ?thesis .
qed
subsubsection ‹Refinement of Gap-Relabel›
definition "fifo_gap_relabel_aux C f l Q u ≡ do {
Q ← q_enqueue u Q;
lu ← l_get l u;
l ← relabel f l u;
if gap_precond l lu then do {
l ← gap_aux C l lu;
return (l,Q)
} else return (l,Q)
}"
lemma fifo_gap_relabel_aux_refine:
assumes [simp]: "C = card V" "l_invar l"
shows "fifo_gap_relabel_aux C f l Q u ≤ fifo_gap_relabel f l Q u"
unfolding fifo_gap_relabel_aux_def fifo_gap_relabel_def relabel_def
gap_relabel_effect_def l_get_def q_enqueue_def
apply (simp only: Let_def nres_monad_laws)
apply refine_vcg
by auto
definition "fifo_gap_relabel2 C am cf clc Q u ≡ do {
Q ← q_enqueue u Q;
lu ← clc_get clc u;
clc ← clc_relabel2 am cf clc u;
has_gap ← clc_has_gap clc lu;
if has_gap then do {
clc ← gap2 C clc lu;
RETURN (clc,Q)
} else
RETURN (clc,Q)
}"
lemma fifo_gap_relabel2_refine_aux:
assumes XCF: "((x, cf), f) ∈ xf_rel"
assumes CLC: "(clc,l)∈clc_rel"
assumes AM: "(am,adjacent_nodes)∈nat_rel→⟨nat_rel⟩list_set_rel"
assumes [simplified,simp]: "(Ci,C)∈Id" "(Qi,Q)∈Id" "(ui,u)∈Id"
shows "fifo_gap_relabel2 Ci am cf clc Qi ui
≤ ⇓(clc_rel ×⇩r Id) (fifo_gap_relabel_aux C f l Q u)"
unfolding fifo_gap_relabel2_def fifo_gap_relabel_aux_def
apply (refine_vcg XCF AM CLC if_bind_cond_refine bind_refine')
apply refine_dref_type
apply (vc_solve solve: refl )
subgoal for _ lu
using CLC
unfolding clc_get_def l_get_def clc_rel_def in_br_conv clc_invar_def
by (auto simp: refine_pw_simps split: prod.splits)
done
lemma fifo_gap_relabel2_refine[refine]:
assumes XCF: "((x, cf), f) ∈ xf_rel"
assumes CLC: "(clc,l)∈clc_rel"
assumes AM: "(am,adjacent_nodes)∈nat_rel→⟨nat_rel⟩list_set_rel"
assumes [simplified,simp]: "(Qi,Q)∈Id" "(ui,u)∈Id"
assumes CC: "C = card V"
shows "fifo_gap_relabel2 C am cf clc Qi ui
≤⇓(clc_rel ×⇩r Id) (fifo_gap_relabel f l Q u)"
proof -
from CLC have LINV: "l_invar l"
unfolding clc_rel_def in_br_conv clc_invar_def by auto
note fifo_gap_relabel2_refine_aux[OF XCF CLC AM IdI IdI IdI]
also note fifo_gap_relabel_aux_refine[OF CC LINV]
finally show ?thesis by simp
qed
subsubsection ‹Refinement of Discharge›
context begin
text ‹
Some lengthy, multi-step refinement of discharge,
changing the iteration to iteration over adjacent nodes with filter,
and showing that we can do the filter wrt.\ the current state, rather than
the original state before the loop.
›
lemma am_nodes_as_filter:
assumes "is_adj_map am"
shows "{v . (u,v)∈cfE_of f} = set (filter (λv. cf_of f (u,v) ≠ 0) (am u))"
using assms cfE_of_ss_invE
unfolding is_adj_map_def Graph.E_def
by fastforce
private lemma adjacent_nodes_iterate_refine1:
fixes ff u f
assumes AMR: "(am,adjacent_nodes)∈Id → ⟨Id⟩list_set_rel"
assumes CR: "⋀s si. (si,s)∈Id ⟹ cci si ⟷ cc s"
assumes FR: "⋀v vi s si. ⟦(vi,v)∈Id; v∈V; (u,v)∈E∪E¯; (si,s)∈Id⟧ ⟹
ffi vi si ≤ ⇓Id (do {
if (cf_of f (u,v) ≠ 0) then ff v s else RETURN s
})" (is "⋀v vi s si. ⟦_;_;_;_⟧ ⟹ _ ≤ ⇓_ (?ff' v s)")
assumes S0R: "(s0i,s0)∈Id"
assumes UR: "(ui,u)∈Id"
shows "nfoldli (am ui) cci ffi s0i
≤⇓Id (FOREACHc {v . (u,v)∈cfE_of f} cc ff s0)"
proof -
from fun_relD[OF AMR] have AM: "is_adj_map am"
unfolding is_adj_map_def
by (auto simp: list_set_rel_def in_br_conv adjacent_nodes_def)
from AM have AM_SS_V: "set (am u) ⊆ V" "{u}×set (am u) ⊆ E ∪ E¯"
unfolding is_adj_map_def using E_ss_VxV by auto
thm nfoldli_refine
have "nfoldli (am ui) cci ffi s0 ≤ ⇓Id (nfoldli (am ui) cc ?ff' s0)"
apply (refine_vcg FR)
apply (rule list_rel_congD)
apply refine_dref_type
using CR
apply vc_solve
using AM_SS_V UR by auto
also have "nfoldli (am ui) cc ?ff' s0
≤⇓Id (FOREACHc (adjacent_nodes u) cc ?ff' s0)"
by (rule LFOc_refine[OF fun_relD[OF AMR UR]]; simp)
also have "FOREACHc (adjacent_nodes u) cc ?ff' s0
≤ FOREACHc {v . (u,v)∈cfE_of f} cc ff s0"
apply (subst am_nodes_as_filter[OF AM])
apply (subst FOREACHc_filter_deforestation2)
subgoal using AM unfolding is_adj_map_def by auto
subgoal
apply (rule eq_refl)
apply ((fo_rule cong)+; (rule refl)?)
subgoal
using fun_relD[OF AMR IdI[of u]]
by (auto simp: list_set_rel_def in_br_conv)
done
done
finally show ?thesis using S0R by simp
qed
private definition "dis_loop_aux am f⇩0 l Q u ≡ do {
assert (u∈V - {s,t});
assert (distinct (am u));
nfoldli (am u) (λ(f,l,Q). excess f u ≠ 0) (λv (f,l,Q). do {
assert ((u,v)∈E∪E¯ ∧ v∈V);
if (cf_of f⇩0 (u,v) ≠ 0) then do {
if (l u = l v + 1) then do {
(f',Q) ← fifo_push f l Q (u,v);
assert (∀v'. v'≠v ⟶ cf_of f' (u,v') = cf_of f (u,v'));
return (f',l,Q)
} else return (f,l,Q)
} else return (f,l,Q)
}) (f⇩0,l,Q)
}"
private definition "fifo_discharge_aux am f⇩0 l Q ≡ do {
(u,Q) ← q_dequeue Q;
assert (u∈V ∧ u≠s ∧ u≠t);
(f,l,Q) ← dis_loop_aux am f⇩0 l Q u;
if excess f u ≠ 0 then do {
(l,Q) ← fifo_gap_relabel f l Q u;
return (f,l,Q)
} else do {
return (f,l,Q)
}
}"
private lemma fifo_discharge_aux_refine:
assumes AM: "(am,adjacent_nodes)∈Id → ⟨Id⟩list_set_rel"
assumes [simplified,simp]: "(fi,f)∈Id" "(li,l)∈Id" "(Qi,Q)∈Id"
shows "fifo_discharge_aux am fi li Qi ≤ ⇓Id (fifo_discharge f l Q)"
unfolding fifo_discharge_aux_def fifo_discharge_def dis_loop_aux_def
unfolding q_dequeue_def
apply (simp only: nres_monad_laws)
apply (refine_rcg adjacent_nodes_iterate_refine1[OF AM])
apply refine_dref_type
apply vc_solve
subgoal
using fun_relD[OF AM IdI[of "hd Q"]]
unfolding list_set_rel_def by (auto simp: in_br_conv)
done
private definition "dis_loop_aux2 am f⇩0 l Q u ≡ do {
assert (u∈V - {s,t});
assert (distinct (am u));
nfoldli (am u) (λ(f,l,Q). excess f u ≠ 0) (λv (f,l,Q). do {
assert ((u,v)∈E∪E¯ ∧ v∈V);
if (cf_of f (u,v) ≠ 0) then do {
if (l u = l v + 1) then do {
(f',Q) ← fifo_push f l Q (u,v);
assert (∀v'. v'≠v ⟶ cf_of f' (u,v') = cf_of f (u,v'));
return (f',l,Q)
} else return (f,l,Q)
} else return (f,l,Q)
}) (f⇩0,l,Q)
}"
private lemma dis_loop_aux2_refine:
shows "dis_loop_aux2 am f⇩0 l Q u ≤⇓Id (dis_loop_aux am f⇩0 l Q u)"
unfolding dis_loop_aux2_def dis_loop_aux_def
apply (intro ASSERT_refine_right ASSERT_refine_left; assumption?)
apply (rule nfoldli_invar_refine[where
I="λit1 it2 (f,_,_). ∀v∈set it2. cf_of f (u,v) = cf_of f⇩0 (u,v)"])
apply refine_dref_type
apply vc_solve
apply (auto simp: pw_leof_iff refine_pw_simps fifo_push_def; metis)
done
private definition "dis_loop_aux3 am x cf l Q u ≡ do {
assert (u∈V ∧ distinct (am u));
monadic_nfoldli (am u)
(λ((x,cf),l,Q). do { xu ← x_get x u; return (xu ≠ 0) })
(λv ((x,cf),l,Q). do {
cfuv ← cf_get cf (u,v);
if (cfuv ≠ 0) then do {
lu ← l_get l u;
lv ← l_get l v;
if (lu = lv + 1) then do {
((x,cf),Q) ← fifo_push2 x cf Q (u,v);
return ((x,cf),l,Q)
} else return ((x,cf),l,Q)
} else return ((x,cf),l,Q)
}) ((x,cf),l,Q)
}"
private lemma dis_loop_aux3_refine:
assumes [simplified,simp]: "(ami,am)∈Id" "(li,l)∈Id" "(Qi,Q)∈Id" "(ui,u)∈Id"
assumes XF: "((x,cf),f)∈xf_rel"
shows "dis_loop_aux3 ami x cf li Qi ui
≤⇓(xf_rel ×⇩r Id ×⇩r Id) (dis_loop_aux2 am f l Q u)"
unfolding dis_loop_aux3_def dis_loop_aux2_def
unfolding x_get_def cf_get_def l_get_def
apply (simp only: nres_monad_laws nfoldli_to_monadic)
apply (refine_rcg)
apply refine_dref_type
using XF
by (vc_solve simp: xf_rel_def in_br_conv)
definition "dis_loop2 am x cf clc Q u ≡ do {
assert (distinct (am u));
amu ← am_get am u;
monadic_nfoldli amu
(λ((x,cf),clc,Q). do { xu ← x_get x u; return (xu ≠ 0) })
(λv ((x,cf),clc,Q). do {
cfuv ← cf_get cf (u,v);
if (cfuv ≠ 0) then do {
lu ← clc_get clc u;
lv ← clc_get clc v;
if (lu = lv + 1) then do {
((x,cf),Q) ← fifo_push2 x cf Q (u,v);
return ((x,cf),clc,Q)
} else return ((x,cf),clc,Q)
} else return ((x,cf),clc,Q)
}) ((x,cf),clc,Q)
}"
private lemma dis_loop2_refine_aux:
assumes [simplified,simp]: "(xi,x)∈Id" "(cfi,cf)∈Id" "(ami,am)∈Id"
assumes [simplified,simp]: "(li,l)∈Id" "(Qi,Q)∈Id" "(ui,u)∈Id"
assumes CLC: "(clc,l)∈clc_rel"
shows "dis_loop2 ami xi cfi clc Qi ui
≤⇓(Id ×⇩r clc_rel ×⇩r Id) (dis_loop_aux3 am x cf l Q u)"
unfolding dis_loop2_def dis_loop_aux3_def am_get_def
apply (simp only: nres_monad_laws)
apply refine_rcg
apply refine_dref_type
apply (vc_solve simp: CLC)
done
lemma dis_loop2_refine[refine]:
assumes XF: "((x,cf),f)∈xf_rel"
assumes CLC: "(clc,l)∈clc_rel"
assumes [simplified,simp]: "(ami,am)∈Id" "(Qi,Q)∈Id" "(ui,u)∈Id"
shows "dis_loop2 ami x cf clc Qi ui
≤⇓(xf_rel ×⇩r clc_rel ×⇩r Id) (dis_loop_aux am f l Q u)"
proof -
have [simp]:
"((Id ×⇩r clc_rel ×⇩r Id) O (xf_rel ×⇩r Id)) = xf_rel ×⇩r clc_rel ×⇩r Id"
by (auto simp: prod_rel_comp)
note dis_loop2_refine_aux[OF IdI IdI IdI IdI IdI IdI CLC]
also note dis_loop_aux3_refine[OF IdI IdI IdI IdI XF]
also note dis_loop_aux2_refine
finally show ?thesis
by (auto simp: conc_fun_chain monoD[OF conc_fun_mono])
qed
definition "fifo_discharge2 C am x cf clc Q ≡ do {
(u,Q) ← q_dequeue Q;
assert (u∈V ∧ u≠s ∧ u≠t);
((x,cf),clc,Q) ← dis_loop2 am x cf clc Q u;
xu ← x_get x u;
if xu ≠ 0 then do {
(clc,Q) ← fifo_gap_relabel2 C am cf clc Q u;
return ((x,cf),clc,Q)
} else do {
return ((x,cf),clc,Q)
}
}"
lemma fifo_discharge2_refine[refine]:
assumes AM: "(am,adjacent_nodes)∈nat_rel→⟨nat_rel⟩list_set_rel"
assumes XCF: "((x, cf), f) ∈ xf_rel"
assumes CLC: "(clc,l)∈clc_rel"
assumes [simplified,simp]: "(Qi,Q)∈Id"
assumes CC: "C = card V"
shows "fifo_discharge2 C am x cf clc Qi
≤⇓(xf_rel ×⇩r clc_rel ×⇩r Id) (fifo_discharge f l Q)"
proof -
have "fifo_discharge2 C am x cf clc Q
≤⇓(xf_rel ×⇩r clc_rel ×⇩r Id) (fifo_discharge_aux am f l Q)"
unfolding fifo_discharge2_def fifo_discharge_aux_def
unfolding x_get_def
apply (simp only: nres_monad_laws)
apply (refine_rcg XCF CLC AM IdI)
apply (vc_solve simp: CC)
subgoal unfolding xf_rel_def in_br_conv by auto
applyS assumption
done
also note fifo_discharge_aux_refine[OF AM IdI IdI IdI]
finally show ?thesis by simp
qed
end
subsubsection ‹Computing the Initial Queue›
definition "q_init am ≡ do {
Q ← q_empty;
ams ← am_get am s;
nfoldli ams (λ_. True) (λv Q. do {
if v≠t then q_enqueue v Q else return Q
}) Q
}"
lemma q_init_correct[THEN order_trans, refine_vcg]:
assumes AM: "is_adj_map am"
shows "q_init am
≤ (spec l. distinct l ∧ set l = {v ∈ V - {s, t}. excess pp_init_f v ≠ 0})"
proof -
from am_to_adj_nodes_refine[OF AM] have "set (am s) ⊆ V"
using adjacent_nodes_ss_V
by (auto simp: list_set_rel_def in_br_conv)
hence "q_init am ≤ RETURN (filter ((≠) t) (am s))"
unfolding q_init_def q_empty_def q_enqueue_def am_get_def
apply (refine_vcg nfoldli_rule[where I="λl1 _ l. l = filter ((≠) t) l1"])
by auto
also have "…
≤ (spec l. distinct l ∧ set l = {v ∈ V - {s, t}. excess pp_init_f v ≠ 0})"
proof -
from am_to_adj_nodes_refine[OF AM]
have [simp]: "distinct (am s)" "set (am s) = adjacent_nodes s"
unfolding list_set_rel_def
by (auto simp: in_br_conv)
show ?thesis
using E_ss_VxV
apply (auto simp: pp_init_x_def adjacent_nodes_def)
unfolding Graph.E_def by auto
qed
finally show ?thesis .
qed
subsubsection ‹Refining the Main Algorithm›
definition "fifo_push_relabel_aux am ≡ do {
cardV ← init_C am;
assert (cardV = card V);
let f = pp_init_f;
l ← l_init cardV;
Q ← q_init am;
(f,l,_) ← monadic_WHILEIT (λ_. True)
(λ(f,l,Q). do {qe ← q_is_empty Q; return (¬qe)})
(λ(f,l,Q). do {
fifo_discharge f l Q
})
(f,l,Q);
assert (Height_Bounded_Labeling c s t f l);
return f
}"
lemma fifo_push_relabel_aux_refine:
assumes AM: "is_adj_map am"
shows "fifo_push_relabel_aux am ≤ ⇓Id (fifo_push_relabel)"
unfolding fifo_push_relabel_aux_def fifo_push_relabel_def
unfolding l_init_def pp_init_l_def q_is_empty_def bind_to_let_conv
apply (rule specify_left[OF init_C_correct[OF AM]])
apply (refine_rcg q_init_correct[OF AM])
apply refine_dref_type
apply vc_solve
done
definition "fifo_push_relabel2 am ≡ do {
cardV ← init_C am;
(x,cf) ← pp_init_xcf2 am;
clc ← clc_init cardV;
Q ← q_init am;
((x,cf),clc,Q) ← monadic_WHILEIT (λ_. True)
(λ((x,cf),clc,Q). do {qe ← q_is_empty Q; return (¬qe)})
(λ((x,cf),clc,Q). do {
fifo_discharge2 cardV am x cf clc Q
})
((x,cf),clc,Q);
return cf
}"
lemma fifo_push_relabel2_refine:
assumes AM: "is_adj_map am"
shows "fifo_push_relabel2 am
≤ ⇓(br (flow_of_cf) (RPreGraph c s t)) fifo_push_relabel"
proof -
{
fix f l n
assume "Height_Bounded_Labeling c s t f l"
then interpret Height_Bounded_Labeling c s t f l .
have G1: "flow_of_cf cf = f" by (rule fo_rg_inv)
have G2: "RPreGraph c s t cf" by (rule is_RPreGraph)
note G1 G2
} note AUX1=this
have "fifo_push_relabel2 am
≤ ⇓(br (flow_of_cf) (RPreGraph c s t)) (fifo_push_relabel_aux am)"
unfolding fifo_push_relabel2_def fifo_push_relabel_aux_def
apply (refine_rcg)
apply (refine_dref_type)
apply (vc_solve simp: AM am_to_adj_nodes_refine[OF AM])
subgoal using AUX1 by (auto simp: in_br_conv xf_rel_def AM)
done
also note fifo_push_relabel_aux_refine[OF AM]
finally show ?thesis .
qed
end
subsection ‹Separating out the Initialization of the Adjacency Matrix›
context Network_Impl
begin
text ‹We split the algorithm into an initialization of the adjacency
matrix, and the actual algorithm. This way, the algorithm can handle
pre-initialized adjacency matrices.
›
definition "fifo_push_relabel_init2 ≡ cf_init"
definition "pp_init_xcf2' am cf ≡ do {
x ← x_init;
assert (s∈V);
adj ← am_get am s;
nfoldli adj (λ_. True) (λv (x,cf). do {
assert ((s,v)∈E);
assert (s ≠ v);
a ← cf_get cf (s,v);
x ← x_add x s (-a);
x ← x_add x v a;
cf ← cf_set cf (s,v) 0;
cf ← cf_set cf (v,s) a;
return (x,cf)
}) (x,cf)
}"
definition "fifo_push_relabel_run2 am cf ≡ do {
cardV ← init_C am;
(x,cf) ← pp_init_xcf2' am cf;
clc ← clc_init cardV;
Q ← q_init am;
((x,cf),clc,Q) ← monadic_WHILEIT (λ_. True)
(λ((x,cf),clc,Q). do {qe ← q_is_empty Q; return (¬qe)})
(λ((x,cf),clc,Q). do {
fifo_discharge2 cardV am x cf clc Q
})
((x,cf),clc,Q);
return cf
}"
lemma fifo_push_relabel2_alt:
"fifo_push_relabel2 am = do {
cf ← fifo_push_relabel_init2;
fifo_push_relabel_run2 am cf
}"
unfolding fifo_push_relabel_init2_def fifo_push_relabel_run2_def
fifo_push_relabel2_def pp_init_xcf2_def pp_init_xcf2'_def
cf_init_def
by simp
end
subsection ‹Refinement To Efficient Data Structures›
context Network_Impl
begin
subsubsection ‹Registration of Abstract Operations›
text ‹We register all abstract operations at once,
auto-rewriting the capacity matrix type›
context includes Network_Impl_Sepref_Register
begin
sepref_register q_empty q_is_empty q_enqueue q_dequeue
sepref_register fifo_push2
sepref_register fifo_gap_relabel2
sepref_register dis_loop2 fifo_discharge2
sepref_register q_init pp_init_xcf2'
sepref_register fifo_push_relabel_run2 fifo_push_relabel_init2
sepref_register fifo_push_relabel2
end
subsubsection ‹Queue by Two Stacks›
definition (in -) "q_α ≡ λ(L,R). L@rev R"
definition (in -) "q_empty_impl ≡ ([],[])"
definition (in -) "q_is_empty_impl ≡ λ(L,R). is_Nil L ∧ is_Nil R"
definition (in -) "q_enqueue_impl ≡ λx (L,R). (L,x#R)"
definition (in -) "q_dequeue_impl
≡ λ(x#L,R) ⇒ (x,(L,R)) | ([],R) ⇒ case rev R of (x#L) ⇒ (x,(L,[]))"
lemma q_empty_impl_correct[simp]: "q_α q_empty_impl = []"
by (auto simp: q_α_def q_empty_impl_def)
lemma q_enqueue_impl_correct[simp]: "q_α (q_enqueue_impl x Q) = q_α Q @ [x]"
by (auto simp: q_α_def q_enqueue_impl_def split: prod.split)
lemma q_is_empty_impl_correct[simp]: "q_is_empty_impl Q ⟷ q_α Q = []"
unfolding q_α_def q_is_empty_impl_def
by (cases Q) (auto split: list.splits)
lemma q_dequeue_impl_correct_aux:
"⟦q_α Q = x#xs⟧ ⟹ apsnd q_α (q_dequeue_impl Q) = (x,xs)"
unfolding q_α_def q_dequeue_impl_def
by (cases Q) (auto split!: list.split)
lemma q_dequeue_impl_correct[simp]:
assumes "q_dequeue_impl Q = (x,Q')"
assumes "q_α Q ≠ []"
shows "x = hd (q_α Q)" and "q_α Q' = tl (q_α Q)"
using assms q_dequeue_impl_correct_aux[of Q]
by - (cases "q_α Q"; auto)+
definition "q_assn ≡ pure (br q_α (λ_. True))"
lemma q_empty_impl_hnr[sepref_fr_rules]:
"(uncurry0 (return q_empty_impl), uncurry0 q_empty) ∈ unit_assn⇧k →⇩a q_assn"
apply (sepref_to_hoare)
unfolding q_assn_def q_empty_def pure_def
by (sep_auto simp: in_br_conv)
lemma q_is_empty_impl_hnr[sepref_fr_rules]:
"(return o q_is_empty_impl, q_is_empty) ∈ q_assn⇧k →⇩a bool_assn"
apply (sepref_to_hoare)
unfolding q_assn_def q_is_empty_def pure_def
by (sep_auto simp: in_br_conv)
lemma q_enqueue_impl_hnr[sepref_fr_rules]:
"(uncurry (return oo q_enqueue_impl), uncurry (PR_CONST q_enqueue))
∈ nat_assn⇧k *⇩a q_assn⇧d →⇩a q_assn"
apply (sepref_to_hoare)
unfolding q_assn_def q_enqueue_def pure_def
by (sep_auto simp: in_br_conv refine_pw_simps)
lemma q_dequeue_impl_hnr[sepref_fr_rules]:
"(return o q_dequeue_impl, q_dequeue) ∈ q_assn⇧d →⇩a nat_assn ×⇩a q_assn"
apply (sepref_to_hoare)
unfolding q_assn_def q_dequeue_def pure_def prod_assn_def
by (sep_auto simp: in_br_conv refine_pw_simps split: prod.split)
subsubsection ‹Push›
sepref_thm fifo_push_impl is "uncurry3 (PR_CONST fifo_push2)"
:: "x_assn⇧d *⇩a cf_assn⇧d *⇩a q_assn⇧d *⇩a edge_assn⇧k
→⇩a ((x_assn×⇩acf_assn)×⇩aq_assn)"
unfolding fifo_push2_def PR_CONST_def
by sepref
concrete_definition (in -) fifo_push_impl
uses Network_Impl.fifo_push_impl.refine_raw is "(uncurry3 ?f,_)∈_"
lemmas [sepref_fr_rules] = fifo_push_impl.refine[OF Network_Impl_axioms]
subsubsection ‹Gap-Relabel›
sepref_thm fifo_gap_relabel_impl is "uncurry5 (PR_CONST fifo_gap_relabel2)"
:: "nat_assn⇧k *⇩a am_assn⇧k *⇩a cf_assn⇧k *⇩a clc_assn⇧d *⇩a q_assn⇧d *⇩a node_assn⇧k
→⇩a clc_assn ×⇩a q_assn"
unfolding fifo_gap_relabel2_def PR_CONST_def
by sepref
concrete_definition (in -) fifo_gap_relabel_impl
uses Network_Impl.fifo_gap_relabel_impl.refine_raw is "(uncurry5 ?f,_)∈_"
lemmas [sepref_fr_rules] = fifo_gap_relabel_impl.refine[OF Network_Impl_axioms]
subsubsection ‹Discharge›
sepref_thm fifo_dis_loop_impl is "uncurry5 (PR_CONST dis_loop2)"
:: "am_assn⇧k *⇩a x_assn⇧d *⇩a cf_assn⇧d *⇩a clc_assn⇧d *⇩a q_assn⇧d *⇩a node_assn⇧k
→⇩a (x_assn×⇩acf_assn)×⇩aclc_assn ×⇩a q_assn"
unfolding dis_loop2_def PR_CONST_def
by sepref
concrete_definition (in -) fifo_dis_loop_impl
uses Network_Impl.fifo_dis_loop_impl.refine_raw is "(uncurry5 ?f,_)∈_"
lemmas [sepref_fr_rules] = fifo_dis_loop_impl.refine[OF Network_Impl_axioms]
sepref_thm fifo_fifo_discharge_impl is "uncurry5 (PR_CONST fifo_discharge2)"
:: "nat_assn⇧k *⇩a am_assn⇧k *⇩a x_assn⇧d *⇩a cf_assn⇧d *⇩a clc_assn⇧d *⇩a q_assn⇧d
→⇩a (x_assn×⇩acf_assn)×⇩aclc_assn ×⇩a q_assn"
unfolding fifo_discharge2_def PR_CONST_def
by sepref
concrete_definition (in -) fifo_fifo_discharge_impl
uses Network_Impl.fifo_fifo_discharge_impl.refine_raw is "(uncurry5 ?f,_)∈_"
lemmas [sepref_fr_rules] =
fifo_fifo_discharge_impl.refine[OF Network_Impl_axioms]
subsubsection ‹Computing the Initial State›
sepref_thm fifo_init_C_impl is "(PR_CONST init_C)"
:: "am_assn⇧k →⇩a nat_assn"
unfolding init_C_def PR_CONST_def
by sepref
concrete_definition (in -) fifo_init_C_impl
uses Network_Impl.fifo_init_C_impl.refine_raw is "(?f,_)∈_"
lemmas [sepref_fr_rules] = fifo_init_C_impl.refine[OF Network_Impl_axioms]
sepref_thm fifo_q_init_impl is "(PR_CONST q_init)"
:: "am_assn⇧k →⇩a q_assn"
unfolding q_init_def PR_CONST_def
by sepref
concrete_definition (in -) fifo_q_init_impl
uses Network_Impl.fifo_q_init_impl.refine_raw is "(?f,_)∈_"
lemmas [sepref_fr_rules] = fifo_q_init_impl.refine[OF Network_Impl_axioms]
sepref_thm pp_init_xcf2'_impl is "uncurry (PR_CONST pp_init_xcf2')"
:: "am_assn⇧k *⇩a cf_assn⇧d →⇩a x_assn ×⇩a cf_assn"
unfolding pp_init_xcf2'_def PR_CONST_def
by sepref
concrete_definition (in -) pp_init_xcf2'_impl
uses Network_Impl.pp_init_xcf2'_impl.refine_raw is "(uncurry ?f,_)∈_"
lemmas [sepref_fr_rules] = pp_init_xcf2'_impl.refine[OF Network_Impl_axioms]
subsubsection ‹Main Algorithm›
sepref_thm fifo_push_relabel_run_impl
is "uncurry (PR_CONST fifo_push_relabel_run2)"
:: "am_assn⇧k *⇩a cf_assn⇧d →⇩a cf_assn"
unfolding fifo_push_relabel_run2_def PR_CONST_def
by sepref
concrete_definition (in -) fifo_push_relabel_run_impl
uses Network_Impl.fifo_push_relabel_run_impl.refine_raw is "(uncurry ?f,_)∈_"
lemmas [sepref_fr_rules] =
fifo_push_relabel_run_impl.refine[OF Network_Impl_axioms]
sepref_thm fifo_push_relabel_init_impl
is "uncurry0 (PR_CONST fifo_push_relabel_init2)"
:: "unit_assn⇧k →⇩a cf_assn"
unfolding fifo_push_relabel_init2_def PR_CONST_def
by sepref
concrete_definition (in -) fifo_push_relabel_init_impl
uses Network_Impl.fifo_push_relabel_init_impl.refine_raw
is "(uncurry0 ?f,_)∈_"
lemmas [sepref_fr_rules] =
fifo_push_relabel_init_impl.refine[OF Network_Impl_axioms]
sepref_thm fifo_push_relabel_impl is "(PR_CONST fifo_push_relabel2)"
:: "am_assn⇧k →⇩a cf_assn"
unfolding fifo_push_relabel2_alt PR_CONST_def
by sepref
concrete_definition (in -) fifo_push_relabel_impl
uses Network_Impl.fifo_push_relabel_impl.refine_raw is "(?f,_)∈_"
lemmas [sepref_fr_rules] = fifo_push_relabel_impl.refine[OF Network_Impl_axioms]
end
export_code fifo_push_relabel_impl checking SML_imp
subsection ‹Combining the Refinement Steps›
theorem (in Network_Impl) fifo_push_relabel_impl_correct[sep_heap_rules]:
assumes AM: "is_adj_map am"
shows "
<am_assn am ami>
fifo_push_relabel_impl c s t N ami
<λcfi. ∃⇩Acf.
am_assn am ami * cf_assn cf cfi
* ↑(isMaxFlow (flow_of_cf cf) ∧ RGraph_Impl c s t N cf)>⇩t"
proof -
note fifo_push_relabel2_refine[OF AM]
also note fifo_push_relabel_correct
finally have R1:
"fifo_push_relabel2 am
≤ ⇓ (br flow_of_cf (RPreGraph c s t)) (SPEC isMaxFlow)" .
have [simp]: "nofail (⇓R (RES X))" for R X by (auto simp: refine_pw_simps)
note R2 = fifo_push_relabel_impl.refine[
OF Network_Impl_axioms, to_hnr, unfolded autoref_tag_defs]
note R3 = hn_refine_ref[OF R1 R2, of ami]
note R4 = R3[unfolded hn_ctxt_def pure_def, THEN hn_refineD, simplified]
note RGII = rgraph_and_network_impl_imp_rgraph_impl[OF
RPreGraph.maxflow_imp_rgraph
Network_Impl_axioms
]
show ?thesis
by (sep_auto
heap: R4
simp: RGII
simp: pw_le_iff refine_pw_simps in_br_conv)
qed
subsection ‹Combination with Network Checker and Main Correctness Theorem›
definition "fifo_push_relabel_impl_tab_am c s t N am ≡ do {
ami ← Array.make N am;
cfi ← fifo_push_relabel_impl c s t N ami;
return (ami,cfi)
}"
theorem fifo_push_relabel_impl_tab_am_correct[sep_heap_rules]:
assumes NW: "Network c s t"
assumes VN: "Graph.V c ⊆ {0..<N}"
assumes ABS_PS: "Graph.is_adj_map c am"
shows "
<emp>
fifo_push_relabel_impl_tab_am c s t N am
<λ(ami,cfi). ∃⇩Acf.
am_assn N am ami * cf_assn N cf cfi
* ↑(Network.isMaxFlow c s t (Network.flow_of_cf c cf)
∧ RGraph_Impl c s t N cf
)>⇩t"
proof -
interpret Network c s t by fact
interpret Network_Impl c s t N using VN by unfold_locales
from ABS_PS have [simp]: "am u = []" if "u≥N" for u
unfolding is_adj_map_def
using E_ss_VxV VN that
apply (subgoal_tac "u∉V")
by (auto simp del: inV_less_N)
show ?thesis
unfolding fifo_push_relabel_impl_tab_am_def
apply vcg
apply (rule Hoare_Triple.cons_rule[
OF _ _ fifo_push_relabel_impl_correct[OF ABS_PS]])
subgoal unfolding am_assn_def is_nf_def by sep_auto
apply (rule ent_refl)
subgoal by sep_auto
done
qed
definition "fifo_push_relabel el s t ≡ do {
case prepareNet el s t of
None ⇒ return None
| Some (c,am,N) ⇒ do {
(ami,cf) ← fifo_push_relabel_impl_tab_am c s t N am;
return (Some (c,ami,N,cf))
}
}"
export_code fifo_push_relabel checking SML_imp
text ‹
Main correctness statement:
▪ If ‹fifo_push_relabel› returns ‹None›, the edge list was invalid or
described an invalid network.
▪ If it returns ‹Some (c,am,N,cfi)›, then the edge list is valid and describes
a valid network. Moreover, ‹cfi› is an integer square matrix of dimension
‹N›, which describes a valid residual graph in the network, whose
corresponding flow is maximal. Finally, ‹am› is a valid adjacency map of the
graph, and the nodes of the graph are integers less than ‹N›.
›
theorem fifo_push_relabel_correct[sep_heap_rules]:
"<emp>
fifo_push_relabel el s t
<λ
None ⇒ ↑(¬ln_invar el ∨ ¬Network (ln_α el) s t)
| Some (c,ami,N,cfi) ⇒
↑(c = ln_α el ∧ ln_invar el ∧ Network c s t)
* (∃⇩Aam cf. am_assn N am ami * cf_assn N cf cfi
* ↑(RGraph_Impl c s t N cf ∧ Graph.is_adj_map c am
∧ Network.isMaxFlow c s t (Network.flow_of_cf c cf))
)
>⇩t
"
unfolding fifo_push_relabel_def
using prepareNet_correct[of el s t]
by (sep_auto simp: ln_rel_def in_br_conv)
subsubsection ‹Justification of Splitting into Prepare and Run Phase›
definition "fifo_push_relabel_prepare_impl el s t ≡ do {
case prepareNet el s t of
None ⇒ return None
| Some (c,am,N) ⇒ do {
ami ← Array.make N am;
cfi ← fifo_push_relabel_init_impl c N;
return (Some (N,ami,c,cfi))
}
}"
theorem justify_fifo_push_relabel_prep_run_split:
"fifo_push_relabel el s t =
do {
pr ← fifo_push_relabel_prepare_impl el s t;
case pr of
None ⇒ return None
| Some (N,ami,c,cf) ⇒ do {
cf ← fifo_push_relabel_run_impl s t N ami cf;
return (Some (c,ami,N,cf))
}
}"
unfolding fifo_push_relabel_def fifo_push_relabel_prepare_impl_def
fifo_push_relabel_impl_tab_am_def fifo_push_relabel_impl_def
by (auto split: option.split)
subsection ‹Usage Example: Computing Maxflow Value ›
text ‹We implement a function to compute the value of the maximum flow.›
definition "fifo_push_relabel_compute_flow_val el s t ≡ do {
r ← fifo_push_relabel el s t;
case r of
None ⇒ return None
| Some (c,am,N,cf) ⇒ do {
v ← compute_flow_val_impl s N am cf;
return (Some v)
}
}"
text ‹The computed flow value is correct›
theorem fifo_push_relabel_compute_flow_val_correct:
"<emp>
fifo_push_relabel_compute_flow_val el s t
<λ
None ⇒ ↑(¬ln_invar el ∨ ¬Network (ln_α el) s t)
| Some v ⇒ ↑( ln_invar el
∧ (let c = ln_α el in
Network c s t ∧ Network.is_max_flow_val c s t v
))
>⇩t"
proof -
{
fix cf N
assume "RGraph_Impl (ln_α el) s t N cf"
then interpret RGraph "(ln_α el)" s t cf by (rule RGraph_Impl.axioms)
have "f = flow_of_cf cf" unfolding f_def by simp
} note aux=this
show ?thesis
unfolding fifo_push_relabel_compute_flow_val_def
by (sep_auto simp: Network.is_max_flow_val_def aux)
qed
export_code fifo_push_relabel_compute_flow_val checking SML_imp
end