section ‹Breadth First Search›
theory Augmenting_Path_BFS
imports
Graph_Impl
"../../Refine_Foreach"
"../../RefineMonadicVCG"
"../../Refine_Imperative_HOL/IICF/Intf/IICF_Set"
"../../Refine_Imperative_HOL/IICF/Intf/IICF_Map"
"../../Refine_Imperative_HOL/IICF/Intf/IICF_List"
"../../Refine_Heuristics"
begin
text ‹
In this theory, we present a verified breadth-first search
with an efficient imperative implementation.
It is parametric in 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 ⇀ 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 ⇀ 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 ⇀ 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"
end
locale Pre_BFS_Impl = Graph +
fixes set_insert_time map_dom_member_time :: nat
and get_succs_list_time :: nat and map_update_time set_pick_extract_time set_empty_time :: nat
and set_isempty_time init_state_time init_get_succs_list_time :: nat
assumes [simp]: "set_pick_extract_time > 0"
begin
definition (in -) "hh v1 v2 v3 == (v1 + ((v2 + v3) + (Suc 0)))"
definition (in -) add_succs_spec_time_aux where "add_succs_spec_time_aux cs v1 v2 v3 = (cs * hh v1 v2 v3)"
abbreviation "hhh == hh map_dom_member_time set_insert_time map_update_time + get_succs_list_time"
abbreviation "add_succs_spec_time cs == add_succs_spec_time_aux cs map_dom_member_time set_insert_time map_update_time"
lemma add_succs_spec_time_mono: "n ≤ m ⟹ add_succs_spec_time n ≤ add_succs_spec_time m"
unfolding add_succs_spec_time_aux_def
using mult_le_cancel2 by blast
definition "add_succs_spec dst succ v PRED N ≡ ASSERT (N ⊆ dom PRED) ⪢
SPECT (emb (λ(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'
) (add_succs_spec_time (card succ))) "
definition (in Graph) "max_dist src ≡ Max (min_dist src`V)"
definition "Vvisited src C d ≡ (⋃x∈{0..<d}. pre_bfs_invar.Vd c src x) ∪ (pre_bfs_invar.Vd c src d - C)"
abbreviation "outedges Vs ≡ {(x, y). (x, y) ∈ E ∧ x ∈ Vs}"
abbreviation "inedges Vs ≡ {(y,x). (y,x) ∈ E ∧ x ∈ Vs}"
lemma u: "⋀Vs. inedges Vs = {(y,x). (x,y) ∈ E¯ ∧ x ∈ Vs}" by simp
lemma card_outedges_singleton: "card (outedges {x}) = card (E``{x})"
proof -
have *: "outedges {x} = {x} × E``{x}" unfolding u by auto
show ?thesis unfolding * card_cartesian_product_singleton ..
qed
lemma card_inedges_singleton: "card (inedges {x}) = card (E¯``{x})"
proof -
thm card_cartesian_product_singleton
have "inedges {x} = E¯``{x} × {x}" unfolding u by auto
then have "card (inedges {x}) = card (E¯``{x} × {x})" by simp
also have "… = card (E¯``{x})" by(simp add: card_cartesian_product)
finally show ?thesis .
qed
abbreviation "bod ≡ (set_pick_extract_time+init_get_succs_list_time +2*set_isempty_time+ set_empty_time)"
definition Te :: "node ⇒ bool × (nat ⇒ nat option) × nat set × nat set × nat
⇒ nat" where "Te src = (λ(f,PRED,C,N,d). if f then 0
else (card (E - (outedges (Vvisited src C d))) * (hhh+bod))
+ (card (E - (inedges (Vvisited src C d))) * (get_succs_list_time))
+ (card N) * (bod) + card C * bod )"
definition pre_bfs :: "node ⇒ node ⇒ (nat × (node⇀node)) option nrest"
where "pre_bfs src dst ≡ do {
s ← SPECT [(False,[src↦src],{src},{},0::nat) ↦ init_state_time];
(f,PRED,_,_,d) ← monadic_WHILEIE (outer_loop_invar src dst) (Te src)
(λ(f,PRED,C,N,d). SPECT [ f=False ∧ C≠{} ↦ set_isempty_time])
(λ(f,PRED,C,N,d). do {
ASSERT (card C≤card V);
(v,C) ← mop_set_pick_extract (λ_. set_pick_extract_time) C;
ASSERT (v∈V);
succ ← SPECT (emb (λl. distinct l ∧ set l = E``{v}) (enat ( init_get_succs_list_time + ((card (E``{v})) + (card (E¯``{v})) )*get_succs_list_time)));
ASSERT (distinct succ);
ASSERT (finite V);
ASSERT (dom PRED ⊆ V);
ASSERT (set succ ⊆ V);
ASSERT (N ⊆ V);
(f,PRED,N) ← add_succs_spec dst (set succ) v PRED N;
if f then
RETURNT (f,PRED,C,N,d+1)
else do {
ASSERT (assn1 src dst (f,PRED,C,N,d));
b ← mop_set_isempty (λ_. set_isempty_time) C;
if (b) then do {
C ← RETURNT N;
N ← mop_set_empty (set_empty_time);
d ← RETURNT (d+1);
RETURNT (f,PRED,C,N,d)
} else RETURNT (f,PRED,C,N,d)
}
})
s;
if f then RETURNT (Some (d, PRED)) else RETURNT None
}"
subsection "Correctness Proof"
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 ↦ src] {src} {} 0"
apply unfold_locales
apply (auto)
apply (auto simp: pre_bfs_invar.Vd_def split: if_split_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
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 []
apply simp
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 (in Graph) "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 (in Graph) 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
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
definition (in -) pre_bfs_time_aux :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat" where
"pre_bfs_time_aux cE v1 v2 v3 v4 v5 = v1 + v2 + ( cE * (v3+v4+v5) + v4) "
lemma (in -) pre_bfs_time_aux_mono: "cE1 ≤ cE2 ⟹ pre_bfs_time_aux cE1 v1 v2 v3 v4 v5
≤ pre_bfs_time_aux cE2 v1 v2 v3 v4 v5"
by(auto simp: pre_bfs_time_aux_def)
abbreviation "pre_bfs_time cE ≡ pre_bfs_time_aux cE init_state_time set_isempty_time hhh bod get_succs_list_time"
lemma pre_bfs_time_progress: "pre_bfs_time cE > 0" by (simp add: pre_bfs_time_aux_def)
lemma Te_start_ub: assumes "valid_PRED c src PRED"
shows "set_isempty_time + init_state_time + (Te src (False, [src ↦ src], {src}, {}, 0)) ≤ pre_bfs_time (card E)"
proof -
from assms have "finite E"
using valid_PRED.FIN_E by blast
then have "card (E - outedges (Vvisited src {src} 0)) ≤ card E"
"card (E - inedges (Vvisited src {src} 0)) ≤ card E"
by(auto intro: card_mono)
then have "Te src (False, [src ↦ src], {src}, {}, 0) ≤ card E * (hhh + bod) + card E * get_succs_list_time + bod"
apply (auto simp add: Te_def pre_bfs_time_aux_def )
using mlex_leI mult_le_mono1 by blast
also have "set_isempty_time + init_state_time + … ≤ pre_bfs_time (card E)"
apply(auto simp: pre_bfs_time_aux_def)
by (simp add: distrib_left)
finally show ?thesis by auto
qed
lemma TeTF_[simp]: "(Te src (True, a1, b1, c1, d1) ≤ Te src (False, x, y, z, f)) ⟷ True"
unfolding Te_def by simp
lemma hlp: "⋀a b c::enat. a ≤ c ⟹ enat ((a::nat)-b) ≤ c"
using diff_le_self dual_order.trans enat_ord_simps(1) by blast
lemma hlp_nat: "⋀a b c::nat. a ≤ c ⟹ ((a)-b) ≤ c"
using diff_le_self dual_order.trans enat_ord_simps(1) by blast
lemma (in nf_invar) cardC: "card C ≤ card V"
by(auto simp: invar_C_ss_V intro!: card_mono)
lemma (in nf_invar) cardN'_: "x∈C ⟹ (N ∪ (E `` {x} - dom PRED)) ⊆ V"
by (smt Diff_iff Graph.connected_inV_iff Graph.succ_ss_V Int_iff N_eq SRC_IN_V UnE mem_Collect_eq pre_bfs_invar.Vd_def subsetCE subsetI)
lemma (in nf_invar) cardN': "x∈C ⟹ card (N ∪ (E `` {x} - dom PRED)) ≤ card V"
apply(rule card_mono[OF FIN_V cardN'_]) by simp
lemma Te_decr_succ_step: assumes "nf_invar c src dst PRED C N d"
and Cx: "C = {x}"
shows
"Te src(False, map_mmupd PRED (E `` {x} - dom PRED) x, N ∪ (E `` {x} - dom PRED), {}, Suc d)
≤ Te src (False, PRED, C, N, d)" (is "?L ≤ ?R")
and "set_isempty_time + set_pick_extract_time + (init_get_succs_list_time + (card (E `` {x}) + card (E¯ `` {x})) * get_succs_list_time) + add_succs_spec_time (card (E `` {x})) + set_isempty_time + set_empty_time
≤ Te src (False, PRED, C, N, d) -
Te src
(False, map_mmupd PRED (E `` {x} - dom PRED) x, N ∪ (E `` {x} - dom PRED), {}, Suc d)" (is "?P ≤ _")
proof -
from assms(2) have xC: "x∈C" by auto
from assms(1) have fE: "finite E" unfolding nf_invar_def nf_invar'_def
using valid_PRED.FIN_E by auto
from assms(1) have fC: "finite C"
using nf_invar.finite_C by blast
have i: "(pre_bfs_invar.Vd c src (Suc d) - (N ∪ (E `` {x} - dom PRED))) = {}"
unfolding nf_invar'.N_eq[OF assms(1)[unfolded nf_invar_def, THEN conjunct1]] assms(2)
apply auto
subgoal using pre_bfs_invar.Vdsucinter_conv by fastforce
subgoal
by (metis IntE Suc_n_not_le_n ‹N = pre_bfs_invar.Vd c src (d + 1) ∩ E `` (pre_bfs_invar.Vd c src d - C)› assms(1) assms(2) nf_invar.inPREDD pre_bfs_invar.in_Vd_conv)
done
have k: "Vvisited src (N ∪ (E `` {x} - dom PRED)) (Suc d)
= Vvisited src {} d"
unfolding Vvisited_def unfolding i by (simp add: Un_commute atLeast0_lessThan_Suc)
have l: "?L ≤ card (E - outedges (Vvisited src {} d)) * (hhh + bod) + card (E - inedges (Vvisited src {} d)) * get_succs_list_time +
(card N) *(bod) + (card (E `` {x} - dom PRED)) * (bod)"
unfolding Te_def apply simp unfolding k
apply (subst card_Un_disjoint)
subgoal using assms(1)
by (meson Efin_imp_Vfin xC fE finite_subset le_sup_iff nf_invar.cardN'_)
subgoal using fE by auto subgoal using assms(1)
by (metis (no_types, lifting) DiffD2 Int_emptyI UnCI nf_invar'.VIS_eq nf_invar_def)
by (auto simp: add_mult_distrib)
have Ein: "E - inedges (Vvisited src C d) = (E - inedges (Vvisited src {} d)) ∪ inedges C"
unfolding Vvisited_def apply auto
by (metis assms(1) nat_neq_iff nf_invar.CVdI pre_bfs_invar.in_Vd_conv)
have Ein2: "card (E - inedges (Vvisited src {} d) ∪ inedges C) = card (E - inedges (Vvisited src {} d)) + card (inedges C)"
apply(rule card_Un_disjoint) apply rule apply fact
subgoal using `finite C` by (metis (no_types, lifting) Collect_mem_eq Diff_iff Ein UnCI ‹finite E› finite_subset mem_Collect_eq subsetI)
apply (auto simp: Vvisited_def) using assms(1) nf_invar.CVdI by blast
have E: "E - outedges (Vvisited src C d) = (E - outedges (Vvisited src {} d)) ∪ outedges C"
unfolding Vvisited_def apply auto
by (metis assms(1) nat_neq_iff nf_invar.CVdI pre_bfs_invar.in_Vd_conv)
have E2: "card (E - outedges (Vvisited src {} d) ∪ outedges C) = card (E - outedges (Vvisited src {} d)) + card (outedges C)"
apply(rule card_Un_disjoint) apply rule apply fact
subgoal using `finite C` by (metis (no_types, lifting) Collect_mem_eq Diff_iff E UnCI ‹finite E› finite_subset mem_Collect_eq subsetI)
apply (auto simp: Vvisited_def) using assms(1) nf_invar.CVdI by blast
have "card (E `` {x} - dom PRED) ≤ card (E `` {x}) " apply(rule card_mono) using fE by auto
also have "… = card (outedges C)" using card_outedges_singleton Cx by simp
finally have c: "card (E `` {x} - dom PRED) ≤ card (outedges C)" by auto
have r: "(card (E - outedges (Vvisited src {} d)) ) * (hhh + bod) + card (outedges C) * (hhh+bod)
+ card (E - inedges (Vvisited src {} d)) * get_succs_list_time + card (inedges C) * get_succs_list_time +
(card N)*(bod) + (card C) * (bod) ≤ ?R"
unfolding Te_def apply clarsimp unfolding E E2 Ein Ein2
by (simp add: distrib_right)
show "?L ≤ ?R" apply(rule order.trans[OF l]) apply(rule order.trans[OF _ r]) using c apply auto
by (simp add: mult_le_mono trans_le_add1)
show "?P ≤ ?R - ?L" apply(rule order.trans[OF _ diff_le_mono[OF r]] )
apply(rule order.trans[OF _ diff_le_mono2[OF l]] )
unfolding assms(2) card_outedges_singleton card_inedges_singleton apply (simp add: add_succs_spec_time_aux_def )
apply(rule dual_order.trans[OF diff_le_mono2[where n="card (E `` {x}) * bod"]])
subgoal by (auto intro!: card_mono simp: fE)
apply (simp add: add.commute add.left_commute distrib_left distrib_right)
done
qed
lemma [simp]: "nf_invar c src dst PRED C N d ⟹ finite V"
using nf_invar'_def nf_invar.axioms(1) valid_PRED.FIN_V by blast
lemma hl: "x ∈ C ⟹ C ≠ {}" by auto
lemma Te_decr_level_step: assumes "nf_invar c src dst PRED C N d"
"C ≠ {}" and xC: "x ∈ C"
shows "Te src
(False, map_mmupd PRED (E `` {x} - dom PRED) x, C - {x},
N ∪ (E `` {x} - dom PRED), d)
≤ Te src (False, PRED, C, N, d)" (is "?L ≤ ?R")
and "set_isempty_time + set_pick_extract_time + (init_get_succs_list_time+ (card (E `` {x}) + card (E¯ `` {x})) * get_succs_list_time) + add_succs_spec_time (card (E `` {x})) + set_isempty_time
≤ Te src (False, PRED, C, N, d) -
Te src
(False, map_mmupd PRED (E `` {x} - dom PRED) x, C - {x},
N ∪ (E `` {x} - dom PRED), d)" (is "?P ≤ _")
proof -
from assms(1) have fE: "finite E" unfolding nf_invar_def nf_invar'_def
using valid_PRED.FIN_E by auto
from assms(1) have fC: "finite C"
using nf_invar.finite_C by blast
have f: "outedges {x} = {x} × E `` {x}" by auto
have f2: "{(xa, y). (xa, y) ∈ E ∧ xa = x} = {x} × E `` {x}" by auto
have v: "Vvisited src (C - {x}) d = Vvisited src C d ∪ {x}" unfolding Vvisited_def apply auto
using assms(1) nf_invar.CVdI xC by blast
have ve: " Vvisited src C d ∩ {x} = {}" unfolding Vvisited_def
by (smt Diff_iff Int_emptyI UN_iff UnE assms(1) atLeastLessThan_iff less_not_refl nf_invar.CVdI pre_bfs_invar.in_Vd_conv singletonD xC)
have 1: "(E - outedges (Vvisited src (C - {x}) d)) ∪ (outedges {x}) = (E - outedges (Vvisited src C d))"
unfolding v using ve by blast
have 11: "card ((E - outedges (Vvisited src (C - {x}) d)) ∪ (outedges {x}))
= card (E - outedges (Vvisited src (C - {x}) d)) + card (outedges {x})"
apply(rule card_Un_disjoint) subgoal using fE by auto
subgoal apply(rule finite_subset[OF _ fE]) by auto
subgoal apply auto
by (simp add: v)
done
have in1: "(E - inedges (Vvisited src (C - {x}) d)) ∪ (inedges {x}) = (E - inedges (Vvisited src C d))"
unfolding v using ve by blast
have in11: "card ((E - inedges (Vvisited src (C - {x}) d)) ∪ (inedges {x}))
= card (E - inedges (Vvisited src (C - {x}) d)) + card (inedges {x})"
apply(rule card_Un_disjoint) subgoal using fE by auto
subgoal apply(rule finite_subset[OF _ fE]) by auto
subgoal apply auto
by (simp add: v)
done
have fN: "finite N"
by (meson Efin_imp_Vfin assms(1) fE le_sup_iff nf_invar.cardN'_ rev_finite_subset xC)
have "(card (E - outedges (Vvisited src (C - {x}) d)))* (hhh + bod) + (card (E `` {x})) * (hhh + bod)
+ (card (E - inedges (Vvisited src (C - {x}) d)))* get_succs_list_time + (card (E¯ `` {x})) * get_succs_list_time
+ card N * bod + card C * bod
= card (E - outedges (Vvisited src C d)) * (hhh + bod) +
card (E - inedges (Vvisited src C d)) * get_succs_list_time + (card N) *(bod) + card C * bod"
unfolding 1[symmetric] 11[unfolded card_outedges_singleton] in1[symmetric] in11[unfolded card_inedges_singleton]
by (simp add: add_mult_distrib)
also have r: "... = ?R" unfolding Te_def by simp
finally have r: " ?R= (card (E - outedges (Vvisited src (C - {x}) d)))* (hhh + bod) + (card (E `` {x})) * (hhh + bod)
+ (card (E - inedges (Vvisited src (C - {x}) d)))* get_succs_list_time + (card (E¯ `` {x})) * get_succs_list_time
+ card N * bod + card C * bod"
by auto
have l1: "?L ≤ card (E - outedges (Vvisited src (C - {x}) d)) * (hhh + bod) +
card (E - inedges (Vvisited src (C - {x}) d)) * get_succs_list_time +
(card N + card (E `` {x}))*(bod) + card (C - {x}) * bod"
unfolding Te_def apply simp apply(rule order.trans[OF card_Un_le]) apply simp apply(rule card_mono) using fE fN by auto
also have l: "… ≤ (card (E - outedges (Vvisited src (C - {x}) d)) + card (E `` {x})) * (hhh + bod)
+ card (E - inedges (Vvisited src (C - {x}) d)) * get_succs_list_time
+ (card N) * (bod) + card (C - {x}) * bod"
by (simp add: add_mult_distrib)
finally have l: "?L ≤ (card (E - outedges (Vvisited src (C - {x}) d)) + card (E `` {x})) * (hhh + bod)
+ card (E - inedges (Vvisited src (C - {x}) d)) * get_succs_list_time
+ (card N) * (bod) + card (C - {x}) * bod" .
show "?L ≤ ?R" apply(rule order.trans[OF l]) unfolding r apply (simp add: add_mult_distrib)
apply(rule order.trans[where b ="card C * bod "])
subgoal apply simp apply(rule card_mono) using fC by auto
subgoal by simp
done
have z: "card {(xa, y). (xa, y) ∈ E ∧ xa = x} = card (E `` {x})" unfolding f2 card_cartesian_product_singleton by auto
have k: "(card N + card (E `` {x})) * bod = card N * bod + card (E `` {x}) * bod"
by (simp add: add_mult_distrib2 mult.commute)
have k2: "card (E `` {x}) * (hhh + bod) = card (E `` {x}) * hhh + card (E `` {x}) *bod "
by (simp add: add_mult_distrib2 mult.commute)
have k3: "(card (E `` {x}) + card (E¯ `` {x})) * get_succs_list_time = card (E `` {x}) * get_succs_list_time + card (E¯ `` {x}) * get_succs_list_time"
by (simp add: add_mult_distrib2 mult.commute)
have d: "(card C - card (C - {x})) = 1" using xC fC
by (simp add: Suc_leI assms(2) card_gt_0_iff)
show "?P ≤ ?R - ?L" unfolding r
apply(rule order.trans[OF _ diff_le_mono2[OF l1]] )
apply (simp add: add_succs_spec_time_aux_def )
unfolding k unfolding k2 unfolding k3 apply simp
apply(subst (3) add.assoc[symmetric])
apply(subst diff_add_assoc) apply (auto intro!: card_mono simp: d fC diff_mult_distrib[symmetric])
by (simp add: add_mult_distrib2)
qed
lemma (in nf_invar) Cge1: "x ∈ C ⟹ card C ≥ 1"
using card_0_eq finite_C by force
lemma Te_pays_exit: assumes "nf_invar c src dst PRED C N d"
"x ∈ C"
shows "set_isempty_time + set_pick_extract_time + (init_get_succs_list_time + (card (E `` {x}) + card (E¯ `` {x})) * get_succs_list_time) + add_succs_spec_time (card (E `` {x}))
≤ Te src (False, PRED, C, N, d) - Te src (True, PRED', C - {x}, N', Suc d)" (is "?P ≤ ?R - ?L")
proof -
from assms(1) have fE: "finite E" unfolding nf_invar_def nf_invar'_def
using valid_PRED.FIN_E by auto
have l: "?L = 0" by(auto simp: Te_def)
have "card (E``{x}) = card (outedges {x})" unfolding card_outedges_singleton ..
also
from assms(2) have "outedges {x} ⊆ E - outedges (Vvisited src C d)"
unfolding Vvisited_def apply auto
by (metis assms(1) less_not_refl nf_invar.CVdI pre_bfs_invar.in_Vd_conv)
then have "card (outedges {x}) ≤ card (E - outedges (Vvisited src C d))"
apply (rule card_mono[rotated]) apply rule apply fact done
finally have out: "card (E``{x}) ≤ card (E - outedges (Vvisited src C d))" .
then have outr1: "card (E - outedges (Vvisited src C d)) * (hhh + bod) ≥ card (E``{x}) * (hhh+bod)"
by(simp only: mult_le_mono)
have "card (E¯``{x}) = card (inedges {x})" unfolding card_inedges_singleton ..
also
from assms(2) have "inedges {x} ⊆ E - inedges (Vvisited src C d)"
unfolding Vvisited_def apply auto
by (metis assms(1) less_not_refl nf_invar.CVdI pre_bfs_invar.in_Vd_conv)
then have "card (inedges {x}) ≤ card (E - inedges (Vvisited src C d))"
apply (rule card_mono[rotated]) apply rule apply fact done
finally have out: "card (E¯``{x}) ≤ card (E - inedges (Vvisited src C d))" .
then have inr1: "card (E - inedges (Vvisited src C d)) * get_succs_list_time ≥ card (E¯``{x}) * get_succs_list_time"
by(simp only: mult_le_mono)
have "card C ≥ 1" using assms(2)
using assms(1) nf_invar.Cge1 by blast
then have p: "bod ≤ card C * bod" by simp
have "card (E``{x}) * hhh + bod + card (E¯``{x}) * get_succs_list_time≤ card (E``{x}) * (hhh+bod) + card N * bod + card C * bod + card (E¯``{x}) * get_succs_list_time"
using p apply auto
by (simp add: add_le_mono trans_le_add1)
also have "… ≤ ?R" unfolding Te_def apply simp
using outr1 inr1 by presburger
finally have r: "card (E``{x}) * hhh + bod + card (E¯``{x}) * get_succs_list_time ≤ ?R" .
show "?P ≤ ?R - ?L" unfolding l
apply(rule dual_order.trans[OF _ ] ) apply simp
apply(rule r)
apply(simp add: add_succs_spec_time_aux_def comm_semiring_class.distrib distrib_left)
done
qed
lemma if_splitI: "(b ⟹ t ≤ A) ⟹ (~b ⟹ t ≤ B) ⟹ t ≤ (if b then A else B)"
by auto
lemma GI: "(b ⟹ t ≤ t') ⟹ (b) ⟹ Some t ≤ G b t'"
by (auto simp: G_def)
lemma rr: "A ≤ B ⟹ a ≤ A ⟹ (A::enat)-a ≤ B -a"
by (simp add: helper)
lemma r: "(a + enat b) - enat b = (a::enat)" apply(cases a) by auto
lemma HI: "((Es0 ≥ Es) ⟹ Some (t' + t + (Es0 - Es)) ≤ Qs) ⟹ (Es0 ≥ Es) ⟹ Some t' ≤ H Qs t Es0 Es"
unfolding H_def unfolding mm3_def apply simp
unfolding mm2_def apply simp apply(cases Qs) apply auto
subgoal
using leD less_le_trans by fastforce
subgoal for i apply(cases t) defer apply simp
apply simp
proof (goal_cases)
case (1 a)
from 1(2) have gl: "a + (Es0 - Es) = a + Es0 - Es" by auto
thm rr[OF 1(1), where a="t + enat (Es0 - Es)"]
have "t' = (t' + enat (a + (Es0 - Es))) - (enat (a + (Es0 - Es)))" by(simp add: r)
also have "… ≤ i - (enat (a + (Es0 - Es)))"
apply(rule rr)
subgoal using 1(1) by (simp add: add.assoc)
by simp
finally show ?case unfolding gl .
qed
done
lemma Te_decr: "nf_invar c src dst f {} N d ⟹ Te src (False, PRED, {}, N, d) ≤ Te src (False, [src ↦ src], {src}, {}, 0)"
unfolding Te_def apply clarsimp
proof (goal_cases)
case 1
with nf_invar.empty_assm have Ne: "N= {}" by blast
from 1 have "finite (Graph.V c)"
by simp
have "Graph.V c = V" by auto
from 1 have "finite (Graph.E c)"
by simp
moreover have "Graph.E c = E" by auto
ultimately have fE: "finite E" by auto
have v_e: "Vvisited src {src} 0 = {}" apply (simp add: Vvisited_def) using pre_bfs_invar.src_Vd0 by auto
from v_e have "E - (outedges (Vvisited src {} d)) ⊆ E - (outedges (Vvisited src {src} 0))" by auto
have Aout: "card (E - (outedges (Vvisited src {} d))) ≤ card (E - (outedges (Vvisited src {src} 0)))"
apply(rule card_mono) apply(rule finite_Diff) apply fact
apply fact done
from v_e have "E - (inedges (Vvisited src {} d)) ⊆ E - (inedges (Vvisited src {src} 0))" by auto
have Ain: "card (E - (inedges (Vvisited src {} d))) ≤ card (E - (inedges (Vvisited src {src} 0)))"
apply(rule card_mono) apply(rule finite_Diff) apply fact
apply fact done
show ?case unfolding Ne apply simp
apply(rule order.trans[OF add_le_mono])
apply(rule mult_le_mono1) apply fact
apply(rule mult_le_mono1) apply fact
by simp
qed
lemma (in nf_invar') domPREDV: "dom PRED ⊆ V"
unfolding VIS_eq N_eq Vd_def V_def apply auto
by (smt Graph.min_dist_is_dist SRC_IN_V V_def dist_cases mem_Collect_eq)
lemma (in nf_invar') N_V: "N ⊆ V"
unfolding N_eq Vd_def V_def by auto
theorem pre_bfs_correct:
assumes [simp]: "src∈V" "src≠dst"
assumes [simp]: "finite V"
shows "pre_bfs src dst ≤ SPECT (emb (bfs_spec src dst) (pre_bfs_time (card E)))"
unfolding pre_bfs_def add_succs_spec_def
apply(rule T_specifies_I)
apply(vcg' ‹clarsimp› rules: if_splitI GI HI mop_set_pick_extract mop_set_empty mop_set_isempty)
apply (simp_all split: bool.splits add: Some_le_mm3_Some_conv Some_le_emb'_conv)
apply safe
apply ( vc_solve simp: domI
Te_pays_exit
Te_decr_level_step(1)
Te_decr_level_step(2)
invar_init
nf_invar.invar_C_ss_V
nf_invar.invar_succ_step
nf_invar.invar_exit'
nf_invar'.invar_shift
nf_invar'.invar_restore
nf_invar.finite_succ
nf_invar.invar_N_ss_Vis)
subgoal apply(subst (asm) Te_decr_succ_step(2)) by auto
subgoal apply(subst (asm) Te_decr_succ_step(2)) by auto
subgoal by (auto intro: nf_invar'.invar_shift nf_invar.invar_succ_step )
subgoal by (auto intro!: Te_decr_succ_step)
subgoal by (auto intro: nf_invar'.invar_shift nf_invar.invar_succ_step )
subgoal by (auto intro!: Te_decr_succ_step)
subgoal by (auto intro: Te_decr_level_step(2))
subgoal by (auto intro: Te_decr_level_step(2))
subgoal by (auto intro: nf_invar'.invar_restore nf_invar.invar_succ_step )
subgoal by(auto intro: Te_decr_level_step)
subgoal by (auto intro: nf_invar'.invar_restore nf_invar.invar_succ_step )
subgoal by(auto intro: Te_decr_level_step)
subgoal by (auto simp: nf_invar_def dest: nf_invar'.N_V)
subgoal using V_def by blast
subgoal by (auto simp: nf_invar_def dest: nf_invar'.domPREDV)
subgoal by(auto dest: nf_invar.cardC)
subgoal by(auto simp: f_invar.invar_found)
subgoal unfolding f_invar_def using Te_start_ub by(auto intro!: hlp_nat )
subgoal by(auto simp: nf_invar.invar_not_found)
subgoal unfolding nf_invar'_def nf_invar_def using Te_start_ub by(auto intro!: hlp_nat )
subgoal using Te_decr by auto
subgoal for a b d e apply(cases a) subgoal by auto using Te_decr by auto
done
end
locale valid_PRED_impl = valid_PRED +
fixes list_append_time map_lookup_time :: nat assumes [simp]: "map_lookup_time > 0"
context Graph
begin
subsection ‹Extraction of Result Path›
definition "extract_rpath_inv src dst PRED = (λ(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)"
definition (in valid_PRED_impl) "extract_rpath_time' = ndist dst * (map_lookup_time + list_append_time)"
definition (in -) "extract_rpath_time_aux cV v1 v2 = cV * (v1 + v2)"
abbreviation (in valid_PRED_impl) "extract_rpath_time cV ≡ extract_rpath_time_aux cV map_lookup_time list_append_time"
lemma (in valid_PRED) ndist_le_V: assumes [simp]: "finite V" and conn: "connected src dst"
shows "ndist dst ≤ card V"
proof -
from conn obtain p where isP: "isPath src p dst" and dist: "distinct (pathVertices src p)"
unfolding connected_def apply auto apply(frule isSPath_pathLE) unfolding isSimplePath_def by blast
have "ndist dst ≤ length p"
unfolding min_dist_def dist_def apply(rule Least_le) apply(rule exI[where x=p])
using isP by simp
also have "… ≤ length (pathVertices src p)" by(simp add: length_pathVertices_eq)
also from dist have "… = card (set (pathVertices src p))"
by(simp add: distinct_card)
also have "… ≤ card V"
apply(rule card_mono) apply simp
using pathVertices_edgeset[OF _ isP] by auto
finally
show "ndist dst ≤ card V" .
qed
definition (in valid_PRED_impl) "Ter = (λ(d,_). ndist d * (map_lookup_time + list_append_time))"
term valid_PRED_impl.Ter
definition (in -) "extract_rpath src dst PRED map_lookup_time list_append_time V ≡ do {
(d,p) ← whileT
(λ(v,p). v≠src) (λ(v,p). do {
ASSERT (v∈dom PRED);
ASSERT (v∈V);
ASSERT (card (dom PRED) ≤ card V);
u ← mop_map_lookup (λ_. map_lookup_time) PRED v;
p ← mop_append (λ_. list_append_time) (u,v) p;
v ← RETURNT u;
RETURNT (v,p)
}) (dst,[]);
RETURNT p
}"
end
context valid_PRED_impl begin
thm FIN_V
lemma domPREDV: "dom PRED ⊆ V"
apply auto subgoal for x y
apply(cases "x=src") using SRC_IN_V apply simp
apply(frule PRED_E) apply simp unfolding V_def by auto
done
lemma extract_rpath_correct':
assumes "dst∈dom PRED"
shows "extract_rpath src dst PRED map_lookup_time list_append_time V
≤ SPECT (emb (λp. isSimplePath src p dst ∧ length p = ndist dst) extract_rpath_time')"
using assms unfolding extract_rpath_def isSimplePath_def
apply(subst whileIET_def[symmetric, where I="extract_rpath_inv src dst PRED" and E =Ter ])
apply simp
apply(rule T_specifies_I)
apply (vcg'‹-› rules: mop_map_lookup mop_append)
apply (auto simp: Some_le_mm3_Some_conv Some_le_emb'_conv
extract_rpath_time'_def extract_rpath_inv_def
PRED_closed[THEN domD] PRED_E PRED_dist Ter_def)
subgoal apply(rule card_mono) by (simp_all add: domPREDV)
subgoal using domPREDV by auto
done
lemma extract_rpath_correct:
assumes "dst∈dom PRED"
shows "extract_rpath src dst PRED map_lookup_time list_append_time V
≤ SPECT (emb (λp. isSimplePath src p dst ∧ length p = ndist dst) (extract_rpath_time (card V)))"
apply(rule dual_order.trans[OF _ extract_rpath_correct'])
apply (auto simp add: emb_le_emb extract_rpath_time_aux_def extract_rpath_time'_def intro!: ndist_le_V)
using assms apply auto
using Graph.isPath_rtc Graph.isSimplePath_def connected_edgeRtc by blast
end
locale Augmenting_Path_BFS = Graph +
fixes set_insert_time map_dom_member_time get_succs_list_time map_update_time set_pick_extract_time :: nat
and list_append_time map_lookup_time set_empty_time set_isempty_time init_state_time init_get_succs_list_time :: nat
assumes [simp]: "map_lookup_time > 0"
assumes [simp]: "set_pick_extract_time > 0"
begin
interpretation pre: Pre_BFS_Impl c set_insert_time map_dom_member_time
get_succs_list_time map_update_time set_pick_extract_time set_empty_time set_isempty_time init_state_time init_get_succs_list_time
apply standard by simp
term Pre_BFS_Impl.pre_bfs
definition "bfs src dst ≡ do {
if src=dst then RETURNT (Some [])
else do {
br ← pre.pre_bfs src dst;
case br of
None ⇒ RETURNT None
| Some (d,PRED) ⇒ do {
p ← extract_rpath src dst PRED map_lookup_time list_append_time V;
RETURNT (Some p)
}
}
}" thm pre.pre_bfs_correct
definition bfs_time where "bfs_time src dst = pre.pre_bfs_time (card E) + valid_PRED_impl.extract_rpath_time list_append_time map_lookup_time (card V)"
lemma bfs_correct:
assumes "src∈V" "finite V"
shows "bfs src dst
≤ SPECT (emb (λ
None ⇒ ¬connected src dst
| Some p ⇒ isShortestPath src p dst) (bfs_time src dst))"
unfolding bfs_def
apply(rule T_specifies_I)
apply(vcg'‹simp› rules: pre.pre_bfs_correct[THEN T_specifies_rev , THEN T_conseq4]
valid_PRED_impl.extract_rpath_correct[THEN T_specifies_rev, THEN T_conseq4])
by (auto simp add: Some_le_mm3_Some_conv Some_le_emb'_conv Some_eq_emb'_conv
assms bfs_time_def
isShortestPath_min_dist_def valid_PRED_impl_def valid_PRED_impl_axioms_def
bfs_spec_def isSimplePath_def)
end
subsection ‹Inserting inner Loop and Successor Function›
context Pre_BFS_Impl begin
definition "foreach_body_time = set_insert_time + 10"
term "(λ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)
)"
definition "inner_loop dst succ u PRED N ≡ nfoldliIE
(λti it (f,PRED',N').
PRED' = map_mmupd PRED ((set ti) - dom PRED) u
∧ N' = N ∪ ((set ti) - dom PRED)
∧ f = (dst∈(set ti) - dom PRED) ∧ dom PRED ⊆ V
) (map_dom_member_time+((set_insert_time+map_update_time) + (1::nat)))
(succ)
(λ(f,PRED,N). ¬f)
(λv (f,PRED,N). do {
ASSERT (card (dom PRED) ≤ card V);
ASSERT (v∈V);
b ← mop_map_dom_member (%_. map_dom_member_time) PRED v;
if b then RETURNT (f,PRED,N)
else do {
PRED ← mop_map_update (λ_. map_update_time) PRED v u;
ASSERT (v∉N);
ASSERT (card N ≤ card V);
N ← mop_set_insert (%_. set_insert_time) v N;
RETURNT (v=dst,PRED,N)
}
})
(False,PRED,N)"
lemma GG: "N ⊆ V ⟹ A ⊆ V ⟹ finite V ⟹ card (N ∪ (A - dom PRED)) ≤ card V"
apply(rule card_mono) by auto
lemma inner_loop_refine:
assumes [simplified, simp]:
"(dsti,dst)∈Id" "(succi,succ)∈Id" "(ui,u)∈Id" "(PREDi,PRED)∈Id" "(Ni,N)∈Id" "ssuc = (set succ)"
"finite V"
and PRED: "dom PRED ⊆ V" and ssuvV: "set succ ⊆ V" and N: "N ⊆ V"
shows "distinct succ ⟹ inner_loop dsti succi ui PREDi Ni
≤ ⇓Id (add_succs_spec dst ssuc u PRED N)"
unfolding inner_loop_def add_succs_spec_def apply simp
apply(rule le_ASSERTI)
apply(rule nfoldliIE_rule)
subgoal using PRED by auto
apply(rule T_specifies_I)
apply (vcg'‹-› rules: mop_map_dom_member T_RESTemb mop_map_update mop_set_insert )
apply(auto simp add: Some_le_mm3_Some_conv Some_le_emb'_conv one_enat_def)
subgoal by (auto simp: it_step_insert_iff map_mmupd_def)
subgoal
by(auto simp: map_mmupd_def)
subgoal apply(subst (asm) GG) using ssuvV N by auto
subgoal apply(subst (asm) GG) using ssuvV N by auto
subgoal using ssuvV by auto
subgoal using ssuvV by auto
subgoal apply(rule card_mono) using ssuvV by auto
subgoal apply(rule card_mono) using ssuvV by auto
subgoal by (auto split: bool.split simp add: domIff intro!: map_mmupd_update_less )
subgoal by (auto split: bool.split simp add: domIff )
subgoal by (auto simp: hh_def add_succs_spec_time_aux_def distinct_card )
done
lemma inner_loop2_correct:
assumes SR: "(succl,succ)∈⟨Id⟩list_set_rel"
assumes [simplified, simp]:
"(dsti,dst)∈Id" "(ui, u) ∈ Id" "(PREDi, PRED) ∈ Id" "(Ni, N) ∈ Id" "finite V"
and PRED: "dom PRED ⊆ V" and ssuvV: "set succl ⊆ V" and N: "N ⊆ V"
shows "inner_loop dsti succl ui PREDi Ni ≤ ⇓Id (add_succs_spec dst succ u PRED N)"
apply(rule inner_loop_refine) using SR ssuvV PRED N by (auto simp: list_set_rel_def br_def)
type_synonym bfs_state = "bool × (node ⇀ node) × node set × node set × nat"
context
fixes succ :: "node ⇒ node list nrest"
fixes init_state :: "node ⇒ bfs_state nrest"
begin
definition "loopguard f C = do {
b ← mop_set_isempty (λ_. set_isempty_time) C;
RETURNT (f=False ∧ ~b) }"
lemma loopguard_correct: "(f,f')∈Id ⟹ (C,C')∈Id ⟹ loopguard f C ≤ ⇓Id ( SPECT [f' = False ∧ C' ≠ {} ↦ enat set_isempty_time] )"
unfolding loopguard_def apply simp
apply(rule T_specifies_I)
by (vcg'‹simp› rules: mop_set_isempty )
definition pre_bfs2 :: "node ⇒ node ⇒ (nat × (node⇀node)) option nrest"
where "pre_bfs2 src dst ≡ do {
s ← init_state src;
(f,PRED,ttt,tt,d) ← monadic_WHILE (λ(f,PRED,C,N,d). loopguard f C)
(λ(f,PRED,C,N,d). do {
ASSERT (C≠{});
ASSERT (card C≤card V);
(v,C) ← mop_set_pick_extract (λ_. set_pick_extract_time) C;
ASSERT (v∈V);
sl ← succ v;
ASSERT (finite V);
ASSERT (dom PRED ⊆ V);
ASSERT (set sl ⊆ V);
ASSERT (N ⊆ V);
(f,PRED,N) ← inner_loop dst sl v PRED N;
if f then
RETURNT (f,PRED,C,N,d+(1::nat))
else do {
ASSERT (assn1 src dst (f,PRED,C,N,d));
b ← mop_set_isempty (λ_. set_isempty_time) C;
if b then do {
C ← RETURNT N;
N ← mop_set_empty set_empty_time;
d ← RETURNT (d+(1::nat));
RETURNT (f,PRED,C,N,d)
} else RETURNT (f,PRED,C,N,d)
}
})
s;
if f then RETURNT (Some (d, PRED)) else RETURNT None
}"
lemma distinct_in_list_set_rel: "distinct l ⟹ (l, set l) ∈ ⟨Id⟩list_set_rel"
by (auto simp add: list_set_rel_def br_def Some_eq_emb'_conv)
lemma pre_bfs2_refine:
assumes succ_impl: "⋀ui u. ⟦(ui,u)∈Id; u∈V⟧
⟹ succ ui ≤ ⇓ (⟨Id⟩list_set_rel) (SPECT [E``{u} ↦ enat (init_get_succs_list_time+ (card (E``{u}) + card (E¯``{u}))*get_succs_list_time )])"
and init_state_impl: "⋀src. init_state src ≤ ⇓Id (SPECT [ (False,[src↦src],{src},{},0::nat) ↦ init_state_time ])"
shows "pre_bfs2 src dst ≤⇓Id (pre_bfs src dst)"
proof -
have i: "⋀t x. SPECT (emb (λl. distinct l ∧ set l = E `` {x}) (enat t)) ≤ ⇓ (⟨Id⟩list_set_rel) (SPECT [E``{x} ↦ enat t])"
apply(rule SPECT_refine)
by(simp add: Some_eq_emb'_conv list_set_rel_def br_def)
have ii: "⋀t x. ⇓ (⟨Id⟩list_set_rel) (SPECT [E``{x} ↦ enat t]) ≤ SPECT (emb (λl. distinct l ∧ set l = E `` {x}) (enat t))"
using Sup_le_iff by (auto simp: conc_fun_def le_fun_def emb'_def list_set_rel_def br_def )
have rew: "⋀tt x. SPECT (emb (λl. distinct l ∧ set l = E `` {x}) (enat tt)) = ⇓ (⟨Id⟩list_set_rel) (SPECT [E``{x} ↦ enat tt])"
apply(rule antisym) using i ii by auto
have succ_impl': "⋀v va. (v,va)∈Id ⟹ va∈V ⟹ succ v ≤ ⇓ (⟨nat_rel⟩list_rel) (SPECT (emb (λl. distinct l ∧ set l = E `` {va}) (enat (init_get_succs_list_time + (card (E `` {va}) + card (E¯ `` {va})) * get_succs_list_time))))"
unfolding rew apply simp apply(rule succ_impl) by auto
show ?thesis
unfolding pre_bfs_def pre_bfs2_def monadic_WHILEIE_def
apply (refine_rcg init_state_impl monadic_WHILE_refine loopguard_correct inner_loop2_correct succ_impl')
apply refine_dref_type
by (auto split: if_splits simp: distinct_in_list_set_rel)
qed
end
end
context Augmenting_Path_BFS
begin
interpretation pre: Pre_BFS_Impl c set_insert_time map_dom_member_time get_succs_list_time map_update_time set_pick_extract_time
set_empty_time set_isempty_time init_state_time init_get_succs_list_time
apply standard by simp
definition "bfs2 succ init_state src dst ≡ do {
if src=dst then
RETURNT (Some [])
else do {
br ← pre.pre_bfs2 succ init_state src dst;
case br of
None ⇒ RETURNT None
| Some (d,PRED) ⇒ do {
p ← extract_rpath src dst PRED map_lookup_time list_append_time V;
RETURNT (Some p)
}
}
}"
lemma bfs2_refine:
assumes succ_impl: "⋀ui u. ⟦(ui,u)∈Id; u∈V⟧
⟹ succ ui ≤ ⇓ (⟨Id⟩list_set_rel) (SPECT [E``{u} ↦ enat (init_get_succs_list_time + (card (E``{u}) + card (E¯``{u}))*get_succs_list_time)])"
and init_state_impl: "⋀src. init_state src ≤ SPECT [ (False,[src↦src],{src},{},0::nat) ↦ init_state_time ]"
shows "bfs2 succ init_state src dst ≤ ⇓Id (bfs src dst)"
unfolding bfs_def bfs2_def
apply auto
apply(rule bindT_mono)
apply(rule pre.pre_bfs2_refine[simplified, OF succ_impl init_state_impl])
by (auto )
end
end