Theory Edka_Checked_Impl
section ‹Combination with Network Checker›
theory Edka_Checked_Impl
imports Flow_Networks.NetCheck EdmondsKarp_Impl
begin
text ‹
In this theory, we combine the Edmonds-Karp implementation with the
network checker.
›
subsection ‹Adding Statistic Counters›
text ‹We first add some statistic counters, that we use for profiling›
definition stat_outer_c :: "unit Heap" where "stat_outer_c = return ()"
lemma insert_stat_outer_c: "m = stat_outer_c ⪢ m"
unfolding stat_outer_c_def by simp
definition stat_inner_c :: "unit Heap" where "stat_inner_c = return ()"
lemma insert_stat_inner_c: "m = stat_inner_c ⪢ m"
unfolding stat_inner_c_def by simp
code_printing
code_module stat ⇀ (SML) ‹
structure stat = struct
val outer_c = ref 0;
fun outer_c_incr () = (outer_c := !outer_c + 1; ())
val inner_c = ref 0;
fun inner_c_incr () = (inner_c := !inner_c + 1; ())
end
›
| constant stat_outer_c ⇀ (SML) "stat.outer'_c'_incr"
| constant stat_inner_c ⇀ (SML) "stat.inner'_c'_incr"
schematic_goal [code]: "edka_imp_run_0 s t N f brk = ?foo"
apply (subst edka_imp_run.code)
apply (rewrite in "⌑" insert_stat_outer_c)
by (rule refl)
thm bfs_impl.code
schematic_goal [code]: "bfs_impl_0 succ_impl ci ti x = ?foo"
apply (subst bfs_impl.code)
apply (rewrite in "imp_nfoldli _ _ ⌑ _" insert_stat_inner_c)
by (rule refl)
subsection ‹Combined Algorithm›
definition "edmonds_karp el s t ≡ do {
case prepareNet el s t of
None ⇒ return None
| Some (c,am,N) ⇒ do {
f ← edka_imp c s t N am ;
return (Some (c,am,N,f))
}
}"
export_code edmonds_karp checking SML
lemma network_is_impl: "Network c s t ⟹ Network_Impl c s t" by intro_locales
theorem edmonds_karp_correct:
"<emp> edmonds_karp el s t <λ
None ⇒ ↑(¬ln_invar el ∨ ¬Network (ln_α el) s t)
| Some (c,am,N,fi) ⇒
∃⇩Af. Network_Impl.is_rflow c s t N f fi
* ↑(ln_α el = c ∧ Graph.is_adj_map c am
∧ Network.isMaxFlow c s t f
∧ ln_invar el ∧ Network c s t ∧ Graph.V c ⊆ {0..<N})
>⇩t"
unfolding edmonds_karp_def
using prepareNet_correct[of el s t]
by (sep_auto
split: option.splits
heap: Network_Impl.edka_imp_correct
simp: ln_rel_def br_def network_is_impl)
context
begin
private definition "is_rflow ≡ Network_Impl.is_rflow"
text_raw ‹\DefineSnippet{edmonds_karp_correct}{›
theorem
fixes el defines "c ≡ ln_α el"
shows
"<emp>
edmonds_karp el s t
<λ None ⇒ ↑(¬ln_invar el ∨ ¬Network c s t)
| Some (_,_,N,cf) ⇒
↑(ln_invar el ∧ Network c s t ∧ Graph.V c ⊆ {0..<N})
* (∃⇩Af. is_rflow c s t N f cf * ↑(Network.isMaxFlow c s t f))
>⇩t"
text_raw ‹}%EndSnippet›
unfolding c_def is_rflow_def
by (sep_auto heap: edmonds_karp_correct[of el s t] split: option.split)
end
subsection ‹Usage Example: Computing Maxflow Value ›
text ‹We implement a function to compute the value of the maximum flow.›
lemma (in Network) am_s_is_incoming:
assumes "is_adj_map am"
shows "E``{s} = set (am s)"
using assms no_incoming_s
unfolding is_adj_map_def
by auto
context RGraph begin
lemma val_by_adj_map:
assumes "is_adj_map am"
shows "f.val = (∑v∈set (am s). c (s,v) - cf (s,v))"
proof -
have "f.val = (∑v∈E``{s}. c (s,v) - cf (s,v))"
unfolding f.val_alt
by (simp add: sum_outgoing_pointwise f_def flow_of_cf_def)
also have "… = (∑v∈set (am s). c (s,v) - cf (s,v))"
by (simp add: am_s_is_incoming[OF assms])
finally show ?thesis .
qed
end
context Network
begin
definition "get_cap e ≡ c e"
definition (in -) get_am :: "(node ⇒ node list) ⇒ node ⇒ node list"
where "get_am am v ≡ am v"
definition "compute_flow_val am cf ≡ do {
let succs = get_am am s;
sum_impl
(λv. do {
let csv = get_cap (s,v);
cfsv ← cf_get cf (s,v);
return (csv - cfsv)
}) (set succs)
}"
lemma (in RGraph) compute_flow_val_correct:
assumes "is_adj_map am"
shows "compute_flow_val am cf ≤ (spec v. v = f.val)"
unfolding val_by_adj_map[OF assms]
unfolding compute_flow_val_def cf_get_def get_cap_def get_am_def
apply (refine_vcg sum_impl_correct)
apply (vc_solve simp: s_node)
unfolding am_s_is_incoming[symmetric, OF assms]
by (auto simp: V_def)
text ‹For technical reasons (poor foreach-support of Sepref tool),
we have to add another refinement step: ›
definition "compute_flow_val2 am cf ≡ (do {
let succs = get_am am s;
nfoldli succs (λ_. True)
(λx a. do {
b ← do {
let csv = get_cap (s, x);
cfsv ← cf_get cf (s, x);
return (csv - cfsv)
};
return (a + b)
})
0
})"
lemma (in RGraph) compute_flow_val2_correct:
assumes "is_adj_map am"
shows "compute_flow_val2 am cf ≤ (spec v. v = f.val)"
proof -
have [refine_dref_RELATES]: "RELATES (⟨Id⟩list_set_rel)"
by (simp add: RELATES_def)
show ?thesis
apply (rule order_trans[OF _ compute_flow_val_correct[OF assms]])
unfolding compute_flow_val2_def compute_flow_val_def sum_impl_def
apply (rule refine_IdD)
apply (refine_rcg LFO_refine bind_refine')
apply refine_dref_type
apply vc_solve
using assms
by (auto
simp: list_set_rel_def br_def get_am_def is_adj_map_def
simp: refine_pw_simps)
qed
end
context Edka_Impl begin
term is_am
lemma [sepref_import_param]: "(c,PR_CONST get_cap) ∈ Id×⇩rId → Id"
by (auto simp: get_cap_def)
lemma [def_pat_rules]:
"Network.get_cap$c ≡ UNPROTECT get_cap" by simp
sepref_register
"PR_CONST get_cap" :: "node×node ⇒ capacity_impl"
lemma [sepref_import_param]: "(get_am,get_am) ∈ Id → Id → ⟨Id⟩list_rel"
by (auto simp: get_am_def intro!: ext)
schematic_goal compute_flow_val_imp:
fixes am :: "node ⇒ node list" and cf :: "capacity_impl graph"
notes [id_rules] =
itypeI[Pure.of am "TYPE(node ⇒ node list)"]
itypeI[Pure.of cf "TYPE(capacity_impl i_mtx)"]
notes [sepref_import_param] = IdI[of N] IdI[of am]
shows "hn_refine
(hn_ctxt (asmtx_assn N id_assn) cf cfi)
(?c::?'d Heap) ?Γ ?R (compute_flow_val2 am cf)"
unfolding compute_flow_val2_def
using [[id_debug, goals_limit = 1]]
by sepref
concrete_definition (in -) compute_flow_val_imp for c s N am cfi
uses Edka_Impl.compute_flow_val_imp
prepare_code_thms (in -) compute_flow_val_imp_def
end
context Network_Impl begin
lemma compute_flow_val_imp_correct_aux:
assumes VN: "Graph.V c ⊆ {0..<N}"
assumes ABS_PS: "is_adj_map am"
assumes RG: "RGraph c s t cf"
shows "
<asmtx_assn N id_assn cf cfi>
compute_flow_val_imp c s N am cfi
<λv. asmtx_assn N id_assn cf cfi * ↑(v = Flow.val c s (flow_of_cf cf))>⇩t"
proof -
interpret rg: RGraph c s t cf by fact
have EI: "Edka_Impl c s t N" by unfold_locales fact
from hn_refine_ref[OF
rg.compute_flow_val2_correct[OF ABS_PS]
compute_flow_val_imp.refine[OF EI], of cfi]
show ?thesis
apply (simp add: hn_ctxt_def pure_def hn_refine_def rg.f_def)
apply (erule cons_post_rule)
apply sep_auto
done
qed
lemma compute_flow_val_imp_correct:
assumes VN: "Graph.V c ⊆ {0..<N}"
assumes ABS_PS: "Graph.is_adj_map c am"
shows "
<is_rflow N f cfi>
compute_flow_val_imp c s N am cfi
<λv. is_rflow N f cfi * ↑(v = Flow.val c s f)>⇩t"
apply (rule hoare_triple_preI)
apply (clarsimp simp: is_rflow_def)
apply vcg
apply (rule cons_rule[OF _ _ compute_flow_val_imp_correct_aux[where cfi=cfi]])
apply (sep_auto simp: VN ABS_PS)+
done
end
definition "edmonds_karp_val el s t ≡ do {
r ← edmonds_karp el s t;
case r of
None ⇒ return None
| Some (c,am,N,cfi) ⇒ do {
v ← compute_flow_val_imp c s N am cfi;
return (Some v)
}
}"
theorem edmonds_karp_val_correct:
"<emp> edmonds_karp_val el s t <λ
None ⇒ ↑(¬ln_invar el ∨ ¬Network (ln_α el) s t)
| Some v ⇒ ↑(∃f N.
ln_invar el ∧ Network (ln_α el) s t
∧ Graph.V (ln_α el) ⊆ {0..<N}
∧ Network.isMaxFlow (ln_α el) s t f
∧ v = Flow.val (ln_α el) s f)
>⇩t"
unfolding edmonds_karp_val_def
by (sep_auto
intro: network_is_impl
heap: edmonds_karp_correct Network_Impl.compute_flow_val_imp_correct)
end