Theory Prpu_Common_Impl
section ‹Tools for Implementing Push-Relabel Algorithms›
theory Prpu_Common_Impl
imports
Prpu_Common_Inst
Flow_Networks.Network_Impl
Flow_Networks.NetCheck
begin
subsection ‹Basic Operations›
type_synonym excess_impl = "node ⇒ capacity_impl"
context Network_Impl
begin
subsubsection ‹Excess Map›
text ‹Obtain an excess map with all nodes mapped to zero.›
definition x_init :: "excess_impl nres" where "x_init ≡ return (λ_. 0)"
text ‹Get the excess of a node.›
definition x_get :: "excess_impl ⇒ node ⇒ capacity_impl nres"
where "x_get x u ≡ do {
assert (u∈V);
return (x u)
}"
text ‹Add a capacity to the excess of a node.›
definition x_add :: "excess_impl ⇒ node ⇒ capacity_impl ⇒ excess_impl nres"
where "x_add x u Δ ≡ do {
assert (u∈V);
return (x(u := x u + Δ))
}"
subsubsection ‹Labeling›
text ‹Obtain the initial labeling: All nodes are zero, except the
source which is labeled by ‹|V|›. The exact cardinality of ‹V› is passed
as a parameter.
›
definition l_init :: "nat ⇒ (node ⇒ nat) nres"
where "l_init C ≡ return ((λ_. 0)(s := C))"
text ‹Get the label of a node.›
definition l_get :: "(node ⇒ nat) ⇒ node ⇒ nat nres"
where "l_get l u ≡ do {
assert (u ∈ V);
return (l u)
}"
text ‹Set the label of a node.›
definition l_set :: "(node ⇒ nat) ⇒ node ⇒ nat ⇒ (node ⇒ nat) nres"
where "l_set l u a ≡ do {
assert (u∈V);
assert (a < 2*card V);
return (l(u := a))
}"
subsubsection ‹Label Frequency Counts for Gap Heuristics›
text ‹Obtain the frequency counts for the initial labeling.
Again, the cardinality of ‹|V|›, which is required to determine the label
of the source node, is passed as an explicit parameter.
›
definition cnt_init :: "nat ⇒ (nat ⇒ nat) nres"
where "cnt_init C ≡ do {
assert (C<2*N);
return ((λ_. 0)(0 := C - 1, C := 1))
}"
text ‹Get the count for a label value.›
definition cnt_get :: "(nat ⇒ nat) ⇒ nat ⇒ nat nres"
where "cnt_get cnt lv ≡ do {
assert (lv < 2*N);
return (cnt lv)
}"
text ‹Increment the count for a label value by one.›
definition cnt_incr :: "(nat ⇒ nat) ⇒ nat ⇒ (nat ⇒ nat) nres"
where "cnt_incr cnt lv ≡ do {
assert (lv < 2*N);
return (cnt ( lv := cnt lv + 1 ))
}"
text ‹Decrement the count for a label value by one.›
definition cnt_decr :: "(nat ⇒ nat) ⇒ nat ⇒ (nat ⇒ nat) nres"
where "cnt_decr cnt lv ≡ do {
assert (lv < 2*N ∧ cnt lv > 0);
return (cnt ( lv := cnt lv - 1 ))
}"
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 ‹Explicit Computation of the Excess›
definition "xf_rel ≡ { ((excess f,cf_of f),f) | f. True }"
lemma xf_rel_RELATES[refine_dref_RELATES]: "RELATES xf_rel"
by (auto simp: RELATES_def)
definition "pp_init_x
≡ λu. (if u=s then (∑(u,v)∈outgoing s. - c(u,v)) else c (s,u))"
lemma excess_pp_init_f[simp]: "excess pp_init_f = pp_init_x"
apply (intro ext)
subgoal for u
unfolding excess_def pp_init_f_def pp_init_x_def
apply (cases "u=s")
subgoal
unfolding outgoing_def incoming_def
by (auto intro: sum.cong simp: sum_negf)
subgoal proof -
assume [simp]: "u≠s"
have [simp]:
"(case e of (u, v) ⇒ if u = s then c (u, v) else 0) = 0"
if "e∈outgoing u" for e
using that by (auto simp: outgoing_def)
have [simp]: "(case e of (u, v) ⇒ if u = s then c (u, v) else 0)
= (if e = (s,u) then c (s,u) else 0)"
if "e∈incoming u" for e
using that by (auto simp: incoming_def split: if_splits)
show ?thesis by (simp add: sum.delta) (simp add: incoming_def)
qed
done
done
definition "pp_init_cf
≡ λ(u,v). if (v=s) then c (v,u) else if u=s then 0 else c (u,v)"
lemma cf_of_pp_init_f[simp]: "cf_of pp_init_f = pp_init_cf"
apply (intro ext)
unfolding pp_init_cf_def pp_init_f_def residualGraph_def
using no_parallel_edge
by auto
lemma pp_init_x_rel: "((pp_init_x, pp_init_cf), pp_init_f) ∈ xf_rel"
unfolding xf_rel_def by auto
subsubsection ‹Algorithm to Compute Initial Excess and Flow›
definition "pp_init_xcf2_aux ≡ do {
let x=(λ_. 0);
let cf=c;
foreach (adjacent_nodes s) (λv (x,cf). do {
assert ((s,v)∈E);
assert (s ≠ v);
let a = cf (s,v);
assert (x v = 0);
let x = x( s := x s - a, v := a );
let cf = cf( (s,v) := 0, (v,s) := a);
return (x,cf)
}) (x,cf)
}"
lemma pp_init_xcf2_aux_spec:
shows "pp_init_xcf2_aux ≤ SPEC (λ(x,cf). x=pp_init_x ∧ cf = pp_init_cf)"
proof -
have ADJ_S_AUX: "adjacent_nodes s = {v . (s,v)∈E}"
unfolding adjacent_nodes_def using no_incoming_s by auto
have CSU_AUX: "c (s,u) = 0" if "u∉adjacent_nodes s" for u
using that unfolding adjacent_nodes_def by auto
show ?thesis
unfolding pp_init_xcf2_aux_def
apply (refine_vcg FOREACH_rule[where I="λit (x,cf).
x s = (∑v∈adjacent_nodes s - it. - c(s,v))
∧ (∀v∈adjacent_nodes s. x v = (if v∈it then 0 else c (s,v)))
∧ (∀v∈-insert s (adjacent_nodes s). x v = 0)
∧ (∀v∈adjacent_nodes s.
if v∉it then cf (s,v) = 0 ∧ cf (v,s) = c (s,v)
else cf (s,v) = c (s,v) ∧ cf (v,s) = c (v,s))
∧ (∀u v. u≠s ∧ v≠s ⟶ cf (u,v) = c (u,v) )
∧ (∀u. u∉adjacent_nodes s ⟶ cf (u,s) = 0 ∧ cf (s,u) = 0)
"])
apply (vc_solve simp: it_step_insert_iff simp: CSU_AUX)
subgoal for v it by (auto simp: ADJ_S_AUX)
subgoal for u it _ v by (auto split: if_splits)
subgoal by (auto simp: ADJ_S_AUX)
subgoal by (auto simp: ADJ_S_AUX)
subgoal by (auto split: if_splits)
subgoal for x
unfolding pp_init_x_def
apply (intro ext)
subgoal for u
apply (clarsimp simp: ADJ_S_AUX outgoing_def; intro conjI)
applyS (auto intro!: sum.reindex_cong[where l=snd] intro: inj_onI)
applyS (metis (mono_tags, lifting) Compl_iff Graph.zero_cap_simp insertE mem_Collect_eq)
done
done
subgoal for x cf
unfolding pp_init_cf_def
apply (intro ext)
apply (clarsimp; auto simp: CSU_AUX)
done
done
qed
definition "pp_init_xcf2 am ≡ do {
x ← x_init;
cf ← cf_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)
}"
lemma pp_init_xcf2_refine_aux:
assumes AM: "is_adj_map am"
shows "pp_init_xcf2 am ≤ ⇓Id (pp_init_xcf2_aux)"
unfolding pp_init_xcf2_def pp_init_xcf2_aux_def
unfolding x_init_def cf_init_def am_get_def cf_get_def cf_set_def x_add_def
apply (simp only: nres_monad_laws)
supply LFO_refine[OF am_to_adj_nodes_refine[OF AM], refine]
apply refine_rcg
using E_ss_VxV
by auto
lemma pp_init_xcf2_refine[refine2]:
assumes AM: "is_adj_map am"
shows "pp_init_xcf2 am ≤⇓xf_rel (RETURN pp_init_f)"
using pp_init_xcf2_refine_aux[OF AM] pp_init_xcf2_aux_spec pp_init_x_rel
by (auto simp: pw_le_iff refine_pw_simps)
subsubsection ‹Computing the Minimal Adjacent Label›
definition (in Network) "min_adj_label_aux cf l u ≡ do {
assert (u∈V);
x ← foreach (adjacent_nodes u) (λv x. do {
assert ((u,v)∈E∪E¯);
assert (v∈V);
if (cf (u,v) ≠ 0) then
case x of
None ⇒ return (Some (l v))
| Some xx ⇒ return (Some (min (l v) (xx)))
else
return x
}) None;
assert (x≠None);
return (the x)
}"
lemma (in -) set_filter_xform_aux:
"{ f x | x. ( x = a ∨ x∈S ∧ x∉it ) ∧ P x }
= (if P a then {f a} else {}) ∪ {f x | x. x∈S-it ∧ P x}"
by auto
lemma (in Labeling) min_adj_label_aux_spec:
assumes PRE: "relabel_precond f l u"
shows "min_adj_label_aux cf l u ≤ SPEC (λx. x = Min { l v | v. (u,v)∈cf.E })"
proof -
have AUX: "cf (u,v) ≠ 0 ⟷ (u,v)∈cf.E" for v unfolding cf.E_def by auto
have EQ: "{ l v | v. (u,v)∈cf.E }
= { l v | v. v∈adjacent_nodes u ∧ cf (u,v)≠0 }"
unfolding AUX
using cfE_ss_invE
by (auto simp: adjacent_nodes_def)
define Min_option :: "nat set ⇀ nat"
where "Min_option X ≡ if X={} then None else Some (Min X)" for X
from PRE active_has_cf_outgoing have "cf.outgoing u ≠ {}"
unfolding relabel_precond_def by auto
hence [simp]: "u∈V" unfolding cf.outgoing_def using cfE_of_ss_VxV by auto
from ‹cf.outgoing u ≠ {}›
have AUX2: "∃v. v ∈ adjacent_nodes u ∧ cf (u, v) ≠ 0"
by (smt AUX Collect_empty_eq Image_singleton_iff UnCI adjacent_nodes_def
cf.outgoing_def cf_def converse_iff prod.simps(2))
show ?thesis unfolding min_adj_label_aux_def EQ
apply (refine_vcg
FOREACH_rule[where
I="λit x. x = Min_option
{ l v | v. v∈adjacent_nodes u - it ∧ cf (u,v)≠0 }"]
)
apply (vc_solve
simp: Min_option_def it_step_insert_iff set_filter_xform_aux
split: if_splits)
subgoal unfolding adjacent_nodes_def by auto
subgoal unfolding adjacent_nodes_def by auto
subgoal using adjacent_nodes_ss_V by auto
subgoal using adjacent_nodes_ss_V by auto
subgoal by (auto simp: Min.insert_remove)
subgoal using AUX2 by auto
done
qed
definition "min_adj_label am cf l u ≡ do {
assert (u∈V);
adj ← am_get am u;
x ← nfoldli adj (λ_. True) (λv x. do {
assert ((u,v)∈ E ∪ E¯);
assert (v∈V);
cfuv ← cf_get cf (u,v);
if (cfuv ≠ 0) then do {
lv ← l_get l v;
case x of
None ⇒ return (Some lv)
| Some xx ⇒ return (Some (min lv xx))
} else
return x
}) None;
assert (x≠None);
return (the x)
}"
lemma min_adj_label_refine[THEN order_trans, refine_vcg]:
assumes "Height_Bounded_Labeling c s t f l"
assumes AM: "(am,adjacent_nodes)∈nat_rel→⟨nat_rel⟩list_set_rel"
assumes PRE: "relabel_precond f l u"
assumes [simp]: "cf = cf_of f"
shows "min_adj_label am cf l u ≤ SPEC (λx. x
= Min { l v | v. (u,v)∈cfE_of f })"
proof -
interpret Height_Bounded_Labeling c s t f l by fact
have "min_adj_label am (cf_of f) l u ≤ ⇓Id (min_adj_label_aux (cf_of f) l u)"
unfolding min_adj_label_def min_adj_label_aux_def Let_def
unfolding am_get_def cf_get_def l_get_def
apply (simp only: nres_monad_laws)
supply LFO_refine[OF fun_relD[OF AM IdI] _ IdI, refine]
apply (refine_rcg)
apply refine_dref_type
by auto
also note min_adj_label_aux_spec[OF PRE]
finally show ?thesis by simp
qed
subsubsection ‹Refinement of Relabel›
text ‹Utilities to Implement Relabel Operations›
definition "relabel2 am cf l u ≡ do {
assert (u∈V - {s,t});
nl ← min_adj_label am cf l u;
l ← l_set l u (nl+1);
return l
}"
lemma relabel2_refine[refine]:
assumes "((x,cf),f)∈xf_rel"
assumes AM: "(am,adjacent_nodes)∈nat_rel→⟨nat_rel⟩list_set_rel"
assumes [simplified,simp]: "(li,l)∈Id" "(ui,u)∈Id"
shows "relabel2 am cf li ui ≤ ⇓Id (relabel f l u)"
proof -
have [simp]: "{l v |v. v ∈ V ∧ cf_of f (u, v) ≠ 0} = {l v |v. cf_of f (u, v) ≠ 0}"
using cfE_of_ss_VxV[of f]
by (auto simp: Graph.E_def)
show ?thesis
using assms
unfolding relabel2_def relabel_def
unfolding l_set_def
apply (refine_vcg AM)
apply (vc_solve (nopre) simp: xf_rel_def relabel_effect_def solve: asm_rl)
subgoal premises prems for a proof -
from prems interpret Height_Bounded_Labeling c s t f l by simp
interpret l': Height_Bounded_Labeling c s t f "relabel_effect f l u"
by (rule relabel_pres_height_bound) (rule prems)
from prems have "u∈V" by simp
from prems have "a + 1 = relabel_effect f l u u"
by (auto simp: relabel_effect_def)
also note l'.height_bound[THEN bspec, OF ‹u∈V›]
finally show "a + 1 < 2 * card V" using card_V_ge2 by auto
qed
done
qed
subsubsection ‹Refinement of Push›
definition "push2_aux x cf ≡ λ(u,v). do {
assert ( (u,v) ∈ E ∪ E¯ );
assert ( u ≠ v );
let Δ = min (x u) (cf (u,v));
return ((x( u := x u - Δ, v := x v + Δ ),augment_edge_cf cf (u,v) Δ))
}"
lemma push2_aux_refine:
"⟦((x,cf),f)∈xf_rel; (ei,e)∈Id×⇩rId⟧
⟹ push2_aux x cf ei ≤ ⇓xf_rel (push f l e)"
unfolding push_def 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 "push2 x cf ≡ λ(u,v). do {
assert ( (u,v) ∈ E ∪ E¯ );
xu ← x_get x u;
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 + Δ);
return (x,cf)
}"
lemma push2_refine[refine]:
assumes "((x,cf),f)∈xf_rel" "(ei,e)∈Id×⇩rId"
shows "push2 x cf ei ≤ ⇓xf_rel (push f l e)"
proof -
have "push2 x cf ei ≤ (push2_aux x cf ei)"
unfolding push2_def push2_aux_def
unfolding x_get_def x_add_def cf_get_def cf_set_def
unfolding augment_edge_cf_def
apply (simp only: nres_monad_laws)
apply refine_vcg
using E_ss_VxV
by auto
also note push2_aux_refine[OF assms]
finally show ?thesis .
qed
subsubsection ‹Adding frequency counters to labeling›
definition "l_invar l ≡ ∀v. l v ≠ 0 ⟶ v∈V"
definition "clc_invar ≡ λ(cnt,l).
(∀lv. cnt lv = card { u∈V . l u = lv })
∧ (∀u. l u < 2*N) ∧ l_invar l"
definition "clc_rel ≡ br snd clc_invar"
definition "clc_init C ≡ do {
l ← l_init C;
cnt ← cnt_init C;
return (cnt,l)
}"
definition "clc_get ≡ λ(cnt,l) u. l_get l u"
definition "clc_set ≡ λ(cnt,l) u a. do {
assert (a<2*N);
lu ← l_get l u;
cnt ← cnt_decr cnt lu;
l ← l_set l u a;
lu ← l_get l u;
cnt ← cnt_incr cnt lu;
return (cnt,l)
}"
definition "clc_has_gap ≡ λ(cnt,l) lu. do {
nlu ← cnt_get cnt lu;
return (nlu = 0)
}"
lemma cardV_le_N: "card V ≤ N" using card_mono[OF _ V_ss] by auto
lemma N_not_Z: "N ≠ 0" using card_V_ge2 cardV_le_N by auto
lemma N_ge_2: "2≤N" using card_V_ge2 cardV_le_N by auto
lemma clc_init_refine[refine]:
assumes [simplified,simp]: "(Ci,C)∈nat_rel"
assumes [simp]: "C = card V"
shows "clc_init Ci ≤⇓clc_rel (l_init C)"
proof -
have AUX: "{u. u ≠ s ∧ u ∈ V} = V-{s}" by auto
show ?thesis
unfolding clc_init_def l_init_def cnt_init_def
apply refine_vcg
unfolding clc_rel_def clc_invar_def
using cardV_le_N N_not_Z
by (auto simp: in_br_conv V_not_empty AUX l_invar_def)
qed
lemma clc_get_refine[refine]:
"⟦ (clc,l)∈clc_rel; (ui,u)∈nat_rel ⟧ ⟹ clc_get clc ui ≤⇓Id (l_get l u)"
unfolding clc_get_def clc_rel_def
by (auto simp: in_br_conv split: prod.split)
definition l_get_rlx :: "(node ⇒ nat) ⇒ node ⇒ nat nres"
where "l_get_rlx l u ≡ do {
assert (u < N);
return (l u)
}"
definition "clc_get_rlx ≡ λ(cnt,l) u. l_get_rlx l u"
lemma clc_get_rlx_refine[refine]:
"⟦ (clc,l)∈clc_rel; (ui,u)∈nat_rel ⟧
⟹ clc_get_rlx clc ui ≤⇓Id (l_get_rlx l u)"
unfolding clc_get_rlx_def clc_rel_def
by (auto simp: in_br_conv split: prod.split)
lemma card_insert_disjointI:
"⟦ finite Y; X = insert x Y; x∉Y ⟧ ⟹ card X = Suc (card Y)"
by auto
lemma clc_set_refine[refine]:
"⟦ (clc,l) ∈ clc_rel; (ui,u)∈nat_rel; (ai,a)∈nat_rel ⟧ ⟹
clc_set clc ui ai ≤⇓clc_rel (l_set l u a)"
unfolding clc_set_def l_set_def l_get_def cnt_decr_def cnt_incr_def
apply refine_vcg
apply vc_solve
unfolding clc_rel_def in_br_conv clc_invar_def l_invar_def
subgoal using cardV_le_N by auto
applyS auto
applyS (auto simp: simp: card_gt_0_iff)
subgoal for cnt ll
apply clarsimp
apply (intro impI conjI; clarsimp?)
subgoal
apply (subst le_imp_diff_is_add; simp)
apply (rule card_insert_disjointI[where x=u])
by auto
subgoal
apply (rule card_insert_disjointI[where x=u, symmetric])
by auto
subgoal
by (auto intro!: arg_cong[where f=card])
done
done
lemma clc_has_gap_correct[THEN order_trans, refine_vcg]:
"⟦(clc,l)∈clc_rel; k<2*N⟧
⟹ clc_has_gap clc k ≤ (spec r. r ⟷ gap_precond l k)"
unfolding clc_has_gap_def cnt_get_def gap_precond_def
apply refine_vcg
unfolding clc_rel_def clc_invar_def in_br_conv
by auto
subsubsection ‹Refinement of Gap-Heuristics›
text ‹Utilities to Implement Gap-Heuristics›
definition "gap_aux C l k ≡ do {
nfoldli [0..<N] (λ_. True) (λv l. do {
lv ← l_get_rlx l v;
if (k < lv ∧ lv < C) then do {
assert (C+1 < 2*N);
l ← l_set l v (C+1);
return l
} else return l
}) l
}"
lemma gap_effect_invar[simp]: "l_invar l ⟹ l_invar (gap_effect l k)"
unfolding gap_effect_def l_invar_def
by auto
lemma relabel_effect_invar[simp]: "⟦l_invar l; u∈V⟧ ⟹ l_invar (relabel_effect f l u)"
unfolding relabel_effect_def l_invar_def by auto
lemma gap_aux_correct[THEN order_trans, refine_vcg]:
"⟦l_invar l; C=card V⟧ ⟹ gap_aux C l k ≤ SPEC (λr. r=gap_effect l k)"
unfolding gap_aux_def l_get_rlx_def l_set_def
apply (simp only: nres_monad_laws)
apply (refine_vcg nfoldli_rule[where I = "λit1 it2 l'. ∀u. if u∈set it2 then l' u = l u else l' u = gap_effect l k u"])
apply (vc_solve simp: upt_eq_lel_conv)
subgoal
apply (frule gap_effect_invar[where k=k])
unfolding l_invar_def using V_ss by force
subgoal using N_not_Z cardV_le_N by auto
subgoal unfolding l_invar_def by auto
subgoal unfolding gap_effect_def by auto
subgoal for v l' u
apply (drule spec[where x=u])
by (auto split: if_splits simp: gap_effect_def)
subgoal by auto
done
definition "gap2 C clc k ≡ do {
nfoldli [0..<N] (λ_. True) (λv clc. do {
lv ← clc_get_rlx clc v;
if (k < lv ∧ lv < C) then do {
clc ← clc_set clc v (C+1);
return clc
} else return clc
}) clc
}"
lemma gap2_refine[refine]:
assumes [simplified,simp]: "(Ci,C)∈nat_rel" "(ki,k)∈nat_rel"
assumes CLC: "(clc,l)∈clc_rel"
shows "gap2 Ci clc ki ≤⇓clc_rel (gap_aux C l k)"
unfolding gap2_def gap_aux_def
apply (refine_rcg CLC)
apply refine_dref_type
by auto
definition "gap_relabel_aux C f l u ≡ do {
lu ← l_get l u;
l ← relabel f l u;
if gap_precond l lu then
gap_aux C l lu
else return l
}"
lemma gap_relabel_aux_refine:
assumes [simp]: "C = card V" "l_invar l"
shows "gap_relabel_aux C f l u ≤ gap_relabel f l u"
unfolding gap_relabel_aux_def gap_relabel_def relabel_def
gap_relabel_effect_def l_get_def
apply (simp only: Let_def nres_monad_laws)
apply refine_vcg
by auto
definition "min_adj_label_clc am cf clc u ≡ case clc of (_,l) ⇒ min_adj_label am cf l u"
definition "clc_relabel2 am cf clc u ≡ do {
assert (u∈V - {s,t});
nl ← min_adj_label_clc am cf clc u;
clc ← clc_set clc u (nl+1);
return clc
}"
lemma clc_relabel2_refine[refine]:
assumes XF: "((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]: "(ui,u)∈Id"
shows "clc_relabel2 am cf clc ui ≤ ⇓clc_rel (relabel f l u)"
proof -
have "clc_relabel2 am cf clc ui ≤⇓clc_rel (relabel2 am cf l ui)"
unfolding clc_relabel2_def relabel2_def
apply (refine_rcg)
apply (refine_dref_type)
apply (vc_solve simp: CLC)
subgoal
using CLC
unfolding clc_rel_def in_br_conv min_adj_label_clc_def
by (auto split: prod.split)
done
also note relabel2_refine[OF XF AM, of l l ui u]
finally show ?thesis by simp
qed
definition "gap_relabel2 C am cf clc u ≡ do {
lu ← clc_get clc u;
clc ← clc_relabel2 am cf clc u;
has_gap ← clc_has_gap clc lu;
if has_gap then gap2 C clc lu
else
RETURN clc
}"
lemma 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" "(ui,u)∈Id"
shows "gap_relabel2 Ci am cf clc ui ≤ ⇓clc_rel (gap_relabel_aux C f l u)"
unfolding gap_relabel2_def gap_relabel_aux_def
apply (refine_vcg XCF AM CLC if_bind_cond_refine bind_refine')
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 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]: "(ui,u)∈Id"
assumes CC: "C = card V"
shows "gap_relabel2 C am cf clc ui ≤⇓clc_rel (gap_relabel f l u)"
proof -
from CLC have LINV: "l_invar l" unfolding clc_rel_def in_br_conv clc_invar_def by auto
note gap_relabel2_refine_aux[OF XCF CLC AM IdI IdI]
also note gap_relabel_aux_refine[OF CC LINV]
finally show ?thesis by simp
qed
subsection ‹Refinement to Efficient Data Structures›
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 x_get x_add
sepref_register l_init l_get l_get_rlx l_set
sepref_register clc_init clc_get clc_set clc_has_gap clc_get_rlx
sepref_register cnt_init cnt_get cnt_incr cnt_decr
sepref_register gap2 min_adj_label min_adj_label_clc
sepref_register push2 relabel2 clc_relabel2 gap_relabel2
sepref_register pp_init_xcf2
end
subsubsection ‹Excess by Array›
definition "x_assn ≡ is_nf N (0::capacity_impl)"
lemma x_init_hnr[sepref_fr_rules]:
"(uncurry0 (Array.new N 0), uncurry0 x_init) ∈ unit_assn⇧k →⇩a x_assn"
apply sepref_to_hoare unfolding x_assn_def x_init_def
by (sep_auto heap: nf_init_rule)
lemma x_get_hnr[sepref_fr_rules]:
"(uncurry Array.nth, uncurry (PR_CONST x_get))
∈ x_assn⇧k *⇩a node_assn⇧k →⇩a cap_assn"
apply sepref_to_hoare
unfolding x_assn_def x_get_def by (sep_auto simp: refine_pw_simps)
definition (in -) "x_add_impl x u Δ ≡ do {
xu ← Array.nth x u;
x ← Array.upd u (xu+Δ) x;
return x
}"
lemma x_add_hnr[sepref_fr_rules]:
"(uncurry2 x_add_impl, uncurry2 (PR_CONST x_add))
∈ x_assn⇧d *⇩a node_assn⇧k *⇩a cap_assn⇧k →⇩a x_assn"
apply sepref_to_hoare
unfolding x_assn_def x_add_impl_def x_add_def
by (sep_auto simp: refine_pw_simps)
subsubsection ‹Labeling by Array›
definition "l_assn ≡ is_nf N (0::nat)"
definition (in -) "l_init_impl N s cardV ≡ do {
l ← Array.new N (0::nat);
l ← Array.upd s cardV l;
return l
}"
lemma l_init_hnr[sepref_fr_rules]:
"(l_init_impl N s, (PR_CONST l_init)) ∈ nat_assn⇧k →⇩a l_assn"
apply sepref_to_hoare
unfolding l_assn_def l_init_def l_init_impl_def
by (sep_auto heap: nf_init_rule)
lemma l_get_hnr[sepref_fr_rules]:
"(uncurry Array.nth, uncurry (PR_CONST l_get))
∈ l_assn⇧k *⇩a node_assn⇧k →⇩a nat_assn"
apply sepref_to_hoare
unfolding l_assn_def l_get_def by (sep_auto simp: refine_pw_simps)
lemma l_get_rlx_hnr[sepref_fr_rules]:
"(uncurry Array.nth, uncurry (PR_CONST l_get_rlx))
∈ l_assn⇧k *⇩a node_assn⇧k →⇩a nat_assn"
apply sepref_to_hoare
unfolding l_assn_def l_get_rlx_def by (sep_auto simp: refine_pw_simps)
lemma l_set_hnr[sepref_fr_rules]:
"(uncurry2 (λa i x. Array.upd i x a), uncurry2 (PR_CONST l_set))
∈ l_assn⇧d *⇩a node_assn⇧k *⇩a nat_assn⇧k →⇩a l_assn"
apply sepref_to_hoare
unfolding l_assn_def l_set_def
by (sep_auto simp: refine_pw_simps split: prod.split)
subsubsection ‹Label Frequency by Array›
definition "cnt_assn (f::node⇒nat) a
≡ ∃⇩Al. a↦⇩al * ↑(length l = 2*N ∧ (∀i<2*N. l!i = f i) ∧ (∀i≥2*N. f i = 0))"
definition (in -) "cnt_init_impl N C ≡ do {
a ← Array.new (2*N) (0::nat);
a ← Array.upd 0 (C-1) a;
a ← Array.upd C 1 a;
return a
}"
definition (in -) "cnt_incr_impl a k ≡ do {
freq ← Array.nth a k;
a ← Array.upd k (freq+1) a;
return a
}"
definition (in -) "cnt_decr_impl a k ≡ do {
freq ← Array.nth a k;
a ← Array.upd k (freq-1) a;
return a
}"
lemma cnt_init_hnr[sepref_fr_rules]: "(cnt_init_impl N, PR_CONST cnt_init) ∈ nat_assn⇧k →⇩a cnt_assn"
apply sepref_to_hoare
unfolding cnt_init_def cnt_init_impl_def cnt_assn_def
by (sep_auto simp: refine_pw_simps)
lemma cnt_get_hnr[sepref_fr_rules]: "(uncurry Array.nth, uncurry (PR_CONST cnt_get)) ∈ cnt_assn⇧k *⇩a nat_assn⇧k →⇩a nat_assn"
apply sepref_to_hoare
unfolding cnt_get_def cnt_assn_def
by (sep_auto simp: refine_pw_simps)
lemma cnt_incr_hnr[sepref_fr_rules]: "(uncurry cnt_incr_impl, uncurry (PR_CONST cnt_incr)) ∈ cnt_assn⇧d *⇩a nat_assn⇧k →⇩a cnt_assn"
apply sepref_to_hoare
unfolding cnt_incr_def cnt_incr_impl_def cnt_assn_def
by (sep_auto simp: refine_pw_simps)
lemma cnt_decr_hnr[sepref_fr_rules]: "(uncurry cnt_decr_impl, uncurry (PR_CONST cnt_decr)) ∈ cnt_assn⇧d *⇩a nat_assn⇧k →⇩a cnt_assn"
apply sepref_to_hoare
unfolding cnt_decr_def cnt_decr_impl_def cnt_assn_def
by (sep_auto simp: refine_pw_simps)
subsubsection ‹Combined Frequency Count and Labeling›
definition "clc_assn ≡ cnt_assn ×⇩a l_assn"
sepref_thm clc_init_impl is "PR_CONST clc_init" :: "nat_assn⇧k →⇩a clc_assn"
unfolding clc_init_def PR_CONST_def clc_assn_def
by sepref
concrete_definition (in -) clc_init_impl
uses Network_Impl.clc_init_impl.refine_raw
lemmas [sepref_fr_rules] = clc_init_impl.refine[OF Network_Impl_axioms]
sepref_thm clc_get_impl is "uncurry (PR_CONST clc_get)"
:: "clc_assn⇧k *⇩a node_assn⇧k →⇩a nat_assn"
unfolding clc_get_def PR_CONST_def clc_assn_def
by sepref
concrete_definition (in -) clc_get_impl
uses Network_Impl.clc_get_impl.refine_raw is "(uncurry ?f,_)∈_"
lemmas [sepref_fr_rules] = clc_get_impl.refine[OF Network_Impl_axioms]
sepref_thm clc_get_rlx_impl is "uncurry (PR_CONST clc_get_rlx)"
:: "clc_assn⇧k *⇩a node_assn⇧k →⇩a nat_assn"
unfolding clc_get_rlx_def PR_CONST_def clc_assn_def
by sepref
concrete_definition (in -) clc_get_rlx_impl
uses Network_Impl.clc_get_rlx_impl.refine_raw is "(uncurry ?f,_)∈_"
lemmas [sepref_fr_rules] = clc_get_rlx_impl.refine[OF Network_Impl_axioms]
sepref_thm clc_set_impl is "uncurry2 (PR_CONST clc_set)"
:: "clc_assn⇧d *⇩a node_assn⇧k *⇩a nat_assn⇧k →⇩a clc_assn"
unfolding clc_set_def PR_CONST_def clc_assn_def
by sepref
concrete_definition (in -) clc_set_impl
uses Network_Impl.clc_set_impl.refine_raw is "(uncurry2 ?f,_)∈_"
lemmas [sepref_fr_rules] = clc_set_impl.refine[OF Network_Impl_axioms]
sepref_thm clc_has_gap_impl is "uncurry (PR_CONST clc_has_gap)"
:: "clc_assn⇧k *⇩a nat_assn⇧k →⇩a bool_assn"
unfolding clc_has_gap_def PR_CONST_def clc_assn_def
by sepref
concrete_definition (in -) clc_has_gap_impl
uses Network_Impl.clc_has_gap_impl.refine_raw is "(uncurry ?f,_)∈_"
lemmas [sepref_fr_rules] = clc_has_gap_impl.refine[OF Network_Impl_axioms]
subsubsection ‹Push›
sepref_thm push_impl is "uncurry2 (PR_CONST push2)"
:: "x_assn⇧d *⇩a cf_assn⇧d *⇩a edge_assn⇧k →⇩a (x_assn×⇩acf_assn)"
unfolding push2_def PR_CONST_def
by sepref
concrete_definition (in -) push_impl
uses Network_Impl.push_impl.refine_raw is "(uncurry2 ?f,_)∈_"
lemmas [sepref_fr_rules] = push_impl.refine[OF Network_Impl_axioms]
subsubsection ‹Relabel›
sepref_thm min_adj_label_impl is "uncurry3 (PR_CONST min_adj_label)"
:: "am_assn⇧k *⇩a cf_assn⇧k *⇩a l_assn⇧k *⇩a node_assn⇧k →⇩a nat_assn"
unfolding min_adj_label_def PR_CONST_def
by sepref
concrete_definition (in -) min_adj_label_impl
uses Network_Impl.min_adj_label_impl.refine_raw is "(uncurry3 ?f,_)∈_"
lemmas [sepref_fr_rules] = min_adj_label_impl.refine[OF Network_Impl_axioms]
sepref_thm relabel_impl is "uncurry3 (PR_CONST relabel2)"
:: "am_assn⇧k *⇩a cf_assn⇧k *⇩a l_assn⇧d *⇩a node_assn⇧k →⇩a l_assn"
unfolding relabel2_def PR_CONST_def
by sepref
concrete_definition (in -) relabel_impl
uses Network_Impl.relabel_impl.refine_raw is "(uncurry3 ?f,_)∈_"
lemmas [sepref_fr_rules] = relabel_impl.refine[OF Network_Impl_axioms]
subsubsection ‹Gap-Relabel›
sepref_thm gap_impl is "uncurry2 (PR_CONST gap2)"
:: "nat_assn⇧k *⇩a clc_assn⇧d *⇩a nat_assn⇧k →⇩a clc_assn"
unfolding gap2_def PR_CONST_def
by sepref
concrete_definition (in -) gap_impl
uses Network_Impl.gap_impl.refine_raw is "(uncurry2 ?f,_)∈_"
lemmas [sepref_fr_rules] = gap_impl.refine[OF Network_Impl_axioms]
sepref_thm min_adj_label_clc_impl is "uncurry3 (PR_CONST min_adj_label_clc)"
:: "am_assn⇧k *⇩a cf_assn⇧k *⇩a clc_assn⇧k *⇩a nat_assn⇧k →⇩a nat_assn"
unfolding min_adj_label_clc_def PR_CONST_def clc_assn_def
by sepref
concrete_definition (in -) min_adj_label_clc_impl
uses Network_Impl.min_adj_label_clc_impl.refine_raw is "(uncurry3 ?f,_)∈_"
lemmas [sepref_fr_rules] = min_adj_label_clc_impl.refine[OF Network_Impl_axioms]
sepref_thm clc_relabel_impl is "uncurry3 (PR_CONST clc_relabel2)"
:: "am_assn⇧k *⇩a cf_assn⇧k *⇩a clc_assn⇧d *⇩a node_assn⇧k →⇩a clc_assn"
unfolding clc_relabel2_def PR_CONST_def
by sepref
concrete_definition (in -) clc_relabel_impl
uses Network_Impl.clc_relabel_impl.refine_raw is "(uncurry3 ?f,_)∈_"
lemmas [sepref_fr_rules] = clc_relabel_impl.refine[OF Network_Impl_axioms]
sepref_thm gap_relabel_impl is "uncurry4 (PR_CONST gap_relabel2)"
:: "nat_assn⇧k *⇩a am_assn⇧k *⇩a cf_assn⇧k *⇩a clc_assn⇧d *⇩a node_assn⇧k
→⇩a clc_assn"
unfolding gap_relabel2_def PR_CONST_def
by sepref
concrete_definition (in -) gap_relabel_impl
uses Network_Impl.gap_relabel_impl.refine_raw is "(uncurry4 ?f,_)∈_"
lemmas [sepref_fr_rules] = gap_relabel_impl.refine[OF Network_Impl_axioms]
subsubsection ‹Initialization›
sepref_thm pp_init_xcf2_impl is "(PR_CONST pp_init_xcf2)"
:: "am_assn⇧k →⇩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 "(?f,_)∈_"
lemmas [sepref_fr_rules] = pp_init_xcf2_impl.refine[OF Network_Impl_axioms]
end
end