section ‹Breadth First Search›
theory Augmenting_Path_BFS
imports Refine_Add_Fofu Graph_Impl
Refine_Monadic_Syntax_Sugar
begin
text ‹
In this theory, we present a verified breadth-first search
with an efficient imperative implementation.
It is parametric over the successor function.
›
subsection ‹Algorithm›
locale pre_bfs_invar = Graph +
fixes src dst :: node
begin
abbreviation "ndist v ≡ min_dist src v"
definition Vd :: "nat => node set"
where
"!!d. Vd d ≡ {v. connected src v ∧ ndist v = d}"
lemma Vd_disj: "!!d d'. d≠d' ==> Vd d ∩ Vd d' = {}"
by (auto simp: Vd_def)
lemma src_Vd0[simp]: "Vd 0 = {src}"
by (auto simp: Vd_def)
lemma in_Vd_conv: "v∈Vd d <-> connected src v ∧ ndist v = d"
by (auto simp: Vd_def)
lemma Vd_succ:
assumes "u∈Vd d"
assumes "(u,v)∈E"
assumes "∀i≤d. v∉Vd i"
shows "v∈Vd (Suc d)"
using assms
by (metis connected_append_edge in_Vd_conv le_SucE min_dist_succ)
end
locale valid_PRED = pre_bfs_invar +
fixes PRED :: "node \<rightharpoonup> node"
assumes SRC_IN_V[simp]: "src∈V"
assumes FIN_V[simp, intro!]: "finite V"
assumes PRED_src[simp]: "PRED src = Some src"
assumes PRED_dist: "[|v≠src; PRED v = Some u|] ==> ndist v = Suc (ndist u)"
assumes PRED_E: "[|v≠src; PRED v = Some u|] ==> (u,v)∈E"
assumes PRED_closed: "[| PRED v = Some u |] ==> u∈dom PRED"
begin
lemma FIN_E[simp, intro!]: "finite E" using E_ss_VxV by simp
lemma FIN_succ[simp, intro!]: "finite (E``{u})" by (auto intro: finite_Image)
end
locale nf_invar' = valid_PRED c src dst PRED for c src dst
and PRED :: "node \<rightharpoonup> node"
and C N :: "node set"
and d :: nat
+
assumes VIS_eq: "dom PRED = N ∪ {u. ∃i≤d. u∈Vd i}"
assumes C_ss: "C ⊆ Vd d"
assumes N_eq: "N = Vd (d+1) ∩ E``(Vd d - C)"
assumes dst_ne_VIS: "dst ∉ dom PRED"
locale nf_invar = nf_invar' +
assumes empty_assm: "C={} ==> N={}"
locale f_invar = valid_PRED c src dst PRED for c src dst
and PRED :: "node \<rightharpoonup> node"
and d :: nat
+
assumes dst_found: "dst ∈ dom PRED ∩ Vd d"
context Graph begin
abbreviation "outer_loop_invar src dst ≡ λ(f,PRED,C,N,d).
(f --> f_invar c src dst PRED d) ∧
(¬f --> nf_invar c src dst PRED C N d)
"
abbreviation "assn1 src dst ≡ λ(f,PRED,C,N,d). ¬f ∧ nf_invar' c src dst PRED C N d"
definition "add_succ_spec dst succ v PRED N ≡ ASSERT (N ⊆ dom PRED) » SPEC (λ(f,PRED',N').
case f of
False => dst ∉ succ - dom PRED ∧ PRED' = map_mmupd PRED (succ - dom PRED) v ∧ N' = N ∪ (succ - dom PRED)
| True => dst ∈ succ - dom PRED ∧ PRED ⊆⇩m PRED' ∧ PRED' ⊆⇩m map_mmupd PRED (succ - dom PRED) v ∧ dst∈dom PRED'
)"
definition pre_bfs :: "node => node => (nat × (node\<rightharpoonup>node)) option nres"
where "pre_bfs src dst ≡ do {
(f,PRED,_,_,d) \<leftarrow> WHILEIT (outer_loop_invar src dst) (λ(f,PRED,C,N,d). f=False ∧ C≠{})
(λ(f,PRED,C,N,d). do {
v \<leftarrow> SPEC (λv. v∈C); let C = C-{v};
ASSERT (v∈V);
let succ = (E``{v});
ASSERT (finite succ);
(f,PRED,N) \<leftarrow> add_succ_spec dst succ v PRED N;
if f then
RETURN (f,PRED,C,N,d+1)
else do {
ASSERT (assn1 src dst (f,PRED,C,N,d));
if (C={}) then do {
let C=N;
let N={};
let d=d+1;
RETURN (f,PRED,C,N,d)
} else RETURN (f,PRED,C,N,d)
}
})
(False,[src\<mapsto>src],{src},{},0::nat);
if f then RETURN (Some (d, PRED)) else RETURN None
}"
subsection "Verification Tasks"
lemma (in nf_invar') ndist_C[simp]: "[|v∈C|] ==> ndist v = d"
using C_ss by (auto simp: Vd_def)
lemma (in nf_invar) CVdI: "[|u∈C|] ==> u∈Vd d"
using C_ss by (auto)
lemma (in nf_invar) inPREDD:
"[|PRED v = Some u|] ==> v∈N ∨ (∃i≤d. v∈Vd i)"
using VIS_eq by (auto)
lemma (in nf_invar') C_ss_VIS: "[|v∈C|] ==> v∈dom PRED"
using C_ss VIS_eq by blast
lemma (in nf_invar) invar_succ_step:
assumes "v∈C"
assumes "dst ∉ E``{v} - dom PRED"
shows "nf_invar' c src dst (map_mmupd PRED (E``{v} - dom PRED) v) (C-{v}) (N ∪ (E``{v} - dom PRED)) d"
proof -
from C_ss_VIS[OF ‹v∈C›] dst_ne_VIS have "v≠dst" by auto
show ?thesis
using ‹v∈C› ‹v≠dst›
apply unfold_locales
apply simp
apply simp
apply (auto simp: map_mmupd_def) []
apply (erule map_mmupdE)
using PRED_dist apply blast
apply (unfold VIS_eq) []
apply clarify
apply (metis CVdI Vd_succ in_Vd_conv)
using PRED_E apply (auto elim!: map_mmupdE) []
using PRED_closed apply (auto elim!: map_mmupdE dest: C_ss_VIS) []
using VIS_eq apply auto []
using C_ss apply auto []
apply (unfold N_eq) []
apply (frule CVdI)
apply (auto) []
apply (erule (1) Vd_succ)
using VIS_eq apply (auto) []
apply (auto dest!: inPREDD simp: N_eq in_Vd_conv) []
using dst_ne_VIS assms(2) apply auto []
done
qed
lemma invar_init: "[|src≠dst; src∈V; finite V|] ==> nf_invar c src dst [src \<mapsto> src] {src} {} 0"
apply unfold_locales
apply (auto)
apply (auto simp: pre_bfs_invar.Vd_def split: split_if_asm)
done
lemma (in nf_invar) invar_exit:
assumes "dst∈C"
shows "f_invar c src dst PRED d"
apply unfold_locales
using assms VIS_eq C_ss by auto
lemma (in nf_invar) invar_C_ss_V: "u∈C ==> u∈V"
apply (drule CVdI)
apply (auto simp: in_Vd_conv connected_inV_iff)
done
lemma (in nf_invar) invar_N_ss_Vis: "u∈N ==> ∃v. PRED u = Some v"
using VIS_eq by auto
lemma (in pre_bfs_invar) Vdsucinter_conv[simp]: "Vd (Suc d) ∩ E `` Vd d = Vd (Suc d)"
apply (auto)
by (metis Image_iff in_Vd_conv min_dist_suc)
lemma (in nf_invar') invar_shift:
assumes [simp]: "C={}"
shows "nf_invar c src dst PRED N {} (Suc d)"
apply unfold_locales
apply vc_solve
using VIS_eq N_eq[simplified] apply (auto simp add: le_Suc_eq) []
using N_eq apply auto []
using N_eq[simplified] apply auto []
using dst_ne_VIS apply auto []
done
lemma (in nf_invar') invar_restore:
assumes [simp]: "C≠{}"
shows "nf_invar c src dst PRED C N d"
apply unfold_locales by auto
definition "bfs_spec src dst r ≡ (
case r of None => ¬ connected src dst
| Some (d,PRED) => connected src dst ∧ min_dist src dst = d ∧ valid_PRED c src PRED ∧ dst∈dom PRED)"
lemma (in f_invar) invar_found:
shows "bfs_spec src dst (Some (d,PRED))"
unfolding bfs_spec_def
apply simp
using dst_found
apply (auto simp: in_Vd_conv)
by unfold_locales
lemma (in nf_invar) invar_not_found:
assumes [simp]: "C={}"
shows "bfs_spec src dst None"
unfolding bfs_spec_def
apply simp
proof (rule notI)
have [simp]: "N={}" using empty_assm by simp
assume C: "connected src dst"
then obtain d' where dstd': "dst ∈ Vd d'"
by (auto simp: in_Vd_conv)
txt {* We make a case-distinction whether @{text "d'≤d"}: *}
have "d'≤d ∨ Suc d ≤ d'" by auto
moreover {
assume "d'≤d"
with VIS_eq dstd' have "dst ∈ dom PRED" by auto
with dst_ne_VIS have False by auto
} moreover {
assume "Suc d ≤ d'"
txt {* In the case @{text "d+1 ≤ d'"}, we also obtain a node
that has a shortest path of length @{text "d+1"}: *}
with min_dist_le[OF C] dstd' obtain v' where "v' ∈ Vd (Suc d)"
by (auto simp: in_Vd_conv)
txt {* However, the invariant states that such nodes are either in
@{text "N"} or are successors of @{text "C"}. As @{text "N"}
and @{text "C"} are both empty, we again get a contradiction. *}
with N_eq have False by auto
} ultimately show False by blast
qed
lemma map_le_mp: "[|m⊆⇩mm'; m k = Some v|] ==> m' k = Some v"
by (force simp: map_le_def)
lemma (in nf_invar) dst_notin_Vdd[intro, simp]: "i≤d ==> dst∉Vd i"
using VIS_eq dst_ne_VIS by auto
lemma (in nf_invar) invar_exit':
assumes "u∈C" "(u,dst) ∈ E" "dst ∈ dom PRED'"
assumes SS1: "PRED ⊆⇩m PRED'" and SS2: "PRED' ⊆⇩m map_mmupd PRED (E``{u} - dom PRED) u"
shows "f_invar c src dst PRED' (Suc d)"
apply unfold_locales
apply simp_all
using map_le_mp[OF SS1 PRED_src] apply simp
apply (drule map_le_mp[OF SS2])
apply (erule map_mmupdE)
using PRED_dist apply auto []
apply (unfold VIS_eq) []
apply clarify
using ‹u∈C›
apply (metis CVdI Vd_succ in_Vd_conv)
apply (drule map_le_mp[OF SS2])
using PRED_E apply (auto elim!: map_mmupdE) []
apply (drule map_le_mp[OF SS2])
apply (erule map_mmupdE)
using map_le_implies_dom_le[OF SS1]
using PRED_closed apply (blast) []
using C_ss_VIS[OF ‹u∈C›] map_le_implies_dom_le[OF SS1] apply blast
using ‹dst ∈ dom PRED'› apply simp
using ‹u∈C› CVdI[OF ‹u∈C›] ‹(u,dst)∈E›
apply (auto) []
apply (erule (1) Vd_succ)
using VIS_eq apply (auto) []
done
definition "max_dist src ≡ Max (min_dist src`V)"
definition "outer_loop_rel src ≡
inv_image (less_than_bool <*lex*> greater_bounded (max_dist src + 1) <*lex*> finite_psubset)
(λ(f,PRED,C,N,d). (¬f,d,C))"
lemma outer_loop_rel_wf:
assumes "finite V"
shows "wf (outer_loop_rel src)"
using assms
unfolding outer_loop_rel_def
by auto
lemma (in nf_invar) C_ne_max_dist:
assumes "C≠{}"
shows "d ≤ max_dist src"
proof -
from assms obtain u where "u∈C" by auto
with C_ss have "u∈Vd d" by auto
hence "min_dist src u = d" "u∈V" by (auto simp: in_Vd_conv connected_inV_iff)
thus "d≤max_dist src"
unfolding max_dist_def by auto
qed
lemma (in nf_invar) Vd_ss_V: "Vd d ⊆ V"
by (auto simp: Vd_def connected_inV_iff)
lemma (in nf_invar) finite_C[simp, intro!]: "finite C"
using C_ss FIN_V Vd_ss_V by (blast intro: finite_subset)
lemma (in nf_invar) finite_succ: "finite (E``{u})"
by auto
theorem pre_bfs_correct:
assumes [simp]: "src∈V" "src≠dst"
assumes [simp]: "finite V"
shows "pre_bfs src dst ≤ SPEC (bfs_spec src dst)"
unfolding pre_bfs_def add_succ_spec_def
apply (intro refine_vcg)
apply (rule outer_loop_rel_wf[where src=src])
apply (vc_solve simp:
invar_init
nf_invar.invar_exit'
nf_invar.invar_C_ss_V
nf_invar.invar_succ_step
nf_invar'.invar_shift
nf_invar'.invar_restore
f_invar.invar_found
nf_invar.invar_not_found
nf_invar.invar_N_ss_Vis
nf_invar.finite_succ
)
apply (vc_solve
simp: remove_subset outer_loop_rel_def
simp: nf_invar.C_ne_max_dist nf_invar.finite_C)
done
definition bfs_core :: "node => node => (nat × (node\<rightharpoonup>node)) option nres"
where "bfs_core src dst ≡ do {
(f,P,_,_,d) \<leftarrow> while⇩T (λ(f,P,C,N,d). f=False ∧ C≠{})
(λ(f,P,C,N,d). do {
v \<leftarrow> spec v. v∈C; let C = C-{v};
let succ = (E``{v});
(f,P,N) \<leftarrow> add_succ_spec dst succ v P N;
if f then
return (f,P,C,N,d+1)
else do {
if (C={}) then do {
let C=N; let N={}; let d=d+1;
return (f,P,C,N,d)
} else return (f,P,C,N,d)
}
})
(False,[src\<mapsto>src],{src},{},0::nat);
if f then return (Some (d, P)) else return None
}"
theorem
assumes "src∈V" "src≠dst" "finite V"
shows "bfs_core src dst ≤ (spec p. bfs_spec src dst p)"
apply (rule order_trans[OF _ pre_bfs_correct])
apply (rule refine_IdD)
unfolding bfs_core_def pre_bfs_def
apply refine_rcg
apply refine_dref_type
apply (vc_solve simp: assms)
done
subsection ‹Extraction of Result Path›
definition "extract_rpath src dst PRED ≡ do {
(_,p) \<leftarrow> WHILEIT
(λ(v,p).
v∈dom PRED
∧ isPath v p dst
∧ distinct (pathVertices v p)
∧ (∀v'∈set (pathVertices v p). pre_bfs_invar.ndist c src v ≤ pre_bfs_invar.ndist c src v')
∧ pre_bfs_invar.ndist c src v + length p = pre_bfs_invar.ndist c src dst)
(λ(v,p). v≠src) (λ(v,p). do {
ASSERT (v∈dom PRED);
let u=the (PRED v);
let p = (u,v)#p;
let v=u;
RETURN (v,p)
}) (dst,[]);
RETURN p
}"
end
context valid_PRED begin
lemma extract_rpath_correct:
assumes "dst∈dom PRED"
shows "extract_rpath src dst PRED ≤ SPEC (λp. isSimplePath src p dst ∧ length p = ndist dst)"
using assms unfolding extract_rpath_def isSimplePath_def
apply (refine_vcg wf_measure[where f="λ(d,_). ndist d"])
apply (vc_solve simp: PRED_closed[THEN domD] PRED_E PRED_dist)
apply auto
done
end
context Graph begin
definition "bfs src dst ≡ do {
if src=dst then RETURN (Some [])
else do {
br \<leftarrow> pre_bfs src dst;
case br of
None => RETURN None
| Some (d,PRED) => do {
p \<leftarrow> extract_rpath src dst PRED;
RETURN (Some p)
}
}
}"
lemma bfs_correct:
assumes "src∈V" "finite V"
shows "bfs src dst ≤ SPEC (λNone => ¬connected src dst | Some p => isShortestPath src p dst)"
unfolding bfs_def
apply (refine_vcg
pre_bfs_correct[THEN order_trans]
valid_PRED.extract_rpath_correct[THEN order_trans]
)
using assms
apply (vc_solve simp: bfs_spec_def isShortestPath_min_dist_def isSimplePath_def)
done
end
context Finite_Graph begin
interpretation Refine_Monadic_Syntax .
theorem
assumes "src∈V"
shows "bfs src dst ≤ (spec p.
case p of None => ¬connected src dst | Some p => isShortestPath src p dst)"
unfolding bfs_def
apply (refine_vcg
pre_bfs_correct[THEN order_trans]
valid_PRED.extract_rpath_correct[THEN order_trans]
)
using assms
apply (vc_solve simp: bfs_spec_def isShortestPath_min_dist_def isSimplePath_def)
done
end
subsection ‹Inserting inner Loop and Successor Function›
context Graph begin
definition "inner_loop dst succ u PRED N ≡ FOREACHci
(λit (f,PRED',N').
PRED' = map_mmupd PRED ((succ - it) - dom PRED) u
∧ N' = N ∪ ((succ - it) - dom PRED)
∧ f = (dst∈(succ - it) - dom PRED)
)
(succ)
(λ(f,PRED,N). ¬f)
(λv (f,PRED,N). do {
if v∈dom PRED then RETURN (f,PRED,N)
else do {
let PRED = PRED(v \<mapsto> u);
ASSERT (v∉N);
let N = insert v N;
RETURN (v=dst,PRED,N)
}
})
(False,PRED,N)"
lemma inner_loop_refine[refine]:
assumes [simp]: "finite succ"
assumes [simplified, simp]: "(succi,succ)∈Id" "(ui,u)∈Id" "(PREDi,PRED)∈Id" "(Ni,N)∈Id"
shows "inner_loop dst succi ui PREDi Ni ≤ \<Down>Id (add_succ_spec dst succ u PRED N)"
unfolding inner_loop_def add_succ_spec_def
apply refine_vcg
apply (auto simp: it_step_insert_iff; fail) +
apply (auto simp: it_step_insert_iff fun_neq_ext_iff map_mmupd_def split: split_if_asm) []
apply (auto simp: it_step_insert_iff split: bool.split; fail) +
apply (auto simp: it_step_insert_iff intro: map_mmupd_update_less split: bool.split)
done
definition "inner_loop2 dst succl u PRED N ≡ nfoldli
(succl) (λ(f,_,_). ¬f) (λv (f,PRED,N). do {
if PRED v ≠ None then RETURN (f,PRED,N)
else do {
let PRED = PRED(v \<mapsto> u);
ASSERT (v∉N);
let N = insert v N;
RETURN ((v=dst),PRED,N)
}
}) (False,PRED,N)"
lemma inner_loop2_refine:
assumes SR: "(succl,succ)∈⟨Id⟩list_set_rel"
shows "inner_loop2 dst succl u PRED N ≤ \<Down>Id (inner_loop dst succ u PRED N)"
using assms
unfolding inner_loop2_def inner_loop_def
apply (refine_rcg LFOci_refine SR)
apply (vc_solve)
apply auto
done
thm conc_trans[OF inner_loop2_refine inner_loop_refine, no_vars]
lemma inner_loop2_correct:
assumes "(succl, succ) ∈ ⟨Id⟩list_set_rel"
assumes [simplified, simp]: "(dsti,dst)∈Id" "(ui, u) ∈ Id" "(PREDi, PRED) ∈ Id" "(Ni, N) ∈ Id"
shows "inner_loop2 dsti succl ui PREDi Ni ≤ \<Down> Id (add_succ_spec dst succ u PRED N)"
apply simp
apply (rule conc_trans[OF inner_loop2_refine inner_loop_refine, simplified])
using assms(1-2)
apply (simp_all)
done
type_synonym bfs_state = "bool × (node \<rightharpoonup> node) × node set × node set × nat"
context
fixes succ :: "node => node list nres"
begin
definition init_state :: "node => bfs_state nres"
where
"init_state src ≡ RETURN (False,[src\<mapsto>src],{src},{},0::nat)"
definition pre_bfs2 :: "node => node => (nat × (node\<rightharpoonup>node)) option nres"
where "pre_bfs2 src dst ≡ do {
s \<leftarrow> init_state src;
(f,PRED,_,_,d) \<leftarrow> WHILET (λ(f,PRED,C,N,d). f=False ∧ C≠{})
(λ(f,PRED,C,N,d). do {
ASSERT (C≠{});
v \<leftarrow> op_set_pick C; let C = C-{v};
ASSERT (v∈V);
sl \<leftarrow> succ v;
(f,PRED,N) \<leftarrow> inner_loop2 dst sl v PRED N;
if f then
RETURN (f,PRED,C,N,d+1)
else do {
ASSERT (assn1 src dst (f,PRED,C,N,d));
if (C={}) then do {
let C=N;
let N={};
let d=d+1;
RETURN (f,PRED,C,N,d)
} else RETURN (f,PRED,C,N,d)
}
})
s;
if f then RETURN (Some (d, PRED)) else RETURN None
}"
lemma pre_bfs2_refine:
assumes succ_impl: "!!ui u. [|(ui,u)∈Id; u∈V|] ==> succ ui ≤ SPEC (λl. (l,E``{u}) ∈ ⟨Id⟩list_set_rel)"
shows "pre_bfs2 src dst ≤\<Down>Id (pre_bfs src dst)"
unfolding pre_bfs_def pre_bfs2_def init_state_def
apply (subst nres_monad1)
apply (refine_rcg inner_loop2_correct succ_impl)
apply refine_dref_type
apply vc_solve
done
end
definition "bfs2 succ src dst ≡ do {
if src=dst then
RETURN (Some [])
else do {
br \<leftarrow> pre_bfs2 succ src dst;
case br of
None => RETURN None
| Some (d,PRED) => do {
p \<leftarrow> extract_rpath src dst PRED;
RETURN (Some p)
}
}
}"
lemma bfs2_refine:
assumes succ_impl: "!!ui u. [|(ui,u)∈Id; u∈V|] ==> succ ui ≤ SPEC (λl. (l,E``{u}) ∈ ⟨Id⟩list_set_rel)"
shows "bfs2 succ src dst ≤ \<Down>Id (bfs src dst)"
unfolding bfs_def bfs2_def
apply (refine_vcg pre_bfs2_refine)
apply refine_dref_type
using assms
apply (vc_solve)
done
end
lemma bfs2_refine_succ:
assumes [refine]: "!!ui u. [|(ui,u)∈Id; u∈Graph.V c|] ==> succi ui ≤ \<Down>Id (succ u)"
assumes [simplified, simp]: "(si,s)∈Id" "(ti,t)∈Id" "(ci,c)∈Id"
shows "Graph.bfs2 ci succi si ti ≤ \<Down>Id (Graph.bfs2 c succ s t)"
unfolding Graph.bfs2_def Graph.pre_bfs2_def
apply (refine_rcg param_nfoldli[param_fo, THEN nres_relD] nres_relI fun_relI)
apply refine_dref_type
apply vc_solve
done
subsection ‹Imperative Implementation›
context Impl_Succ begin
definition op_bfs :: "'ga => node => node => path option nres" where [simp]: "op_bfs c s t ≡ Graph.bfs2 (absG c) (succ c) s t"
lemma pat_op_dfs[pat_rules]:
"Graph.bfs2$(absG$c)$(succ$c)$s$t ≡ UNPROTECT op_bfs$c$s$t" by simp
sepref_register "PR_CONST op_bfs" "'ig => node => node => path option nres"
type_synonym ibfs_state = "bool × (node,node) i_map × node set × node set × nat"
sepref_register Graph.init_state "node => ibfs_state nres"
schematic_lemma init_state_impl:
fixes src :: nat
notes [id_rules] =
itypeI[Pure.of src "TYPE(nat)"]
shows "hn_refine (hn_val nat_rel src srci) (?c::?'c Heap) ?Γ' ?R (Graph.init_state src)"
using [[id_debug, goals_limit = 1]]
unfolding Graph.init_state_def
apply (subst CTYPE_ANNOT_def[symmetric, Pure.of "[src\<mapsto>src]" "TYPE((nat,nat)i_map)"])
apply (subst op_empty_ls_def[symmetric])
apply (subst op_empty_ls_def[symmetric])
apply (rewrite in "insert src _" op_set_ins_dj_def[symmetric])
by sepref_keep
concrete_definition (in -) init_state_impl uses Impl_Succ.init_state_impl
lemmas [sepref_fr_rules] = init_state_impl.refine[OF this_loc,to_hfref]
schematic_lemma bfs_impl:
notes [sepref_opt_simps] = heap_WHILET_def
fixes s t :: nat
notes [id_rules] =
itypeI[Pure.of s "TYPE(nat)"]
itypeI[Pure.of t "TYPE(nat)"]
itypeI[Pure.of c "TYPE('ig)"]
-- ‹Declare parameters to operation identification›
shows "hn_refine (
hn_ctxt (isG) c ci
* hn_val nat_rel s si
* hn_val nat_rel t ti) (?c::?'c Heap) ?Γ' ?R (PR_CONST op_bfs c s t)"
unfolding op_bfs_def PR_CONST_def
unfolding Graph.bfs2_def Graph.pre_bfs2_def
Graph.inner_loop2_def Graph.extract_rpath_def
unfolding nres_monad_laws
apply (rewrite in "nfoldli _ _ \<hole> _" op_set_ins_dj_def[symmetric])
using [[id_debug, goals_limit = 1]]
apply sepref_keep
done
concrete_definition (in -) bfs_impl uses Impl_Succ.bfs_impl
-- ‹Extract generated implementation into constant›
prepare_code_thms (in -) bfs_impl_def
lemmas bfs_impl_fr_rule = bfs_impl.refine[OF this_loc,to_hfref]
end
export_code bfs_impl checking SML_imp
end