Theory DFS_Framework.Rec_Impl
section ‹Recursive DFS Implementation›
theory Rec_Impl
imports General_DFS_Structure
begin
locale rec_impl_defs =
graph_defs G + gen_dfs_defs gds V0
for G :: "('v, 'more) graph_rec_scheme"
and gds :: "('v,'s)gen_dfs_struct"
+
fixes pending :: "'s ⇒ 'v rel"
fixes stack :: "'s ⇒ 'v list"
fixes choose_pending :: "'v ⇒ 'v option ⇒ 's ⇒ 's nres"
begin
definition "gen_step' s ≡ do { ASSERT (gen_rwof s);
if gds_is_empty_stack gds s then do {
v0 ← SPEC (λv0. v0 ∈ V0 ∧ ¬ gds_is_discovered gds v0 s);
gds_new_root gds v0 s
} else do {
let u = hd (stack s);
Vs ← SELECT (λv. (u,v)∈pending s);
s ← choose_pending u Vs s;
case Vs of
None ⇒ gds_finish gds u s
| Some v ⇒
if gds_is_discovered gds v s
then if gds_is_finished gds v s then gds_cross_edge gds u v s
else gds_back_edge gds u v s
else gds_discover gds u v s
}}"
definition "gen_dfs' ≡ gds_init gds ⤜ WHILE gen_cond gen_step'"
abbreviation "gen_rwof' ≡ rwof (gds_init gds) gen_cond gen_step'"
definition rec_impl where [DFS_code_unfold]:
"rec_impl ≡ do {
s ← gds_init gds;
FOREACHci
(λit s.
gen_rwof' s
∧ (¬gds_is_break gds s ⟶ gds_is_empty_stack gds s
∧ V0-it ⊆ gen_discovered s))
V0
(Not o gds_is_break gds)
(λv0 s. do {
let s0 = GHOST s;
if gds_is_discovered gds v0 s then
RETURN s
else do {
s ← gds_new_root gds v0 s;
if gds_is_break gds s then
RETURN s
else do {
REC_annot
(λ(u,s). gen_rwof' s ∧ ¬gds_is_break gds s
∧ (∃stk. stack s = u#stk)
∧ E ∩ {u}×UNIV ⊆ pending s)
(λ(u,s) s'.
gen_rwof' s'
∧ (¬gds_is_break gds s' ⟶
stack s' = tl (stack s)
∧ pending s' = pending s - {u} × UNIV
∧ gen_discovered s' ⊇ gen_discovered s
))
(λD (u,s). do {
s ← FOREACHci
(λit s'. gen_rwof' s'
∧ (¬gds_is_break gds s' ⟶
stack s' = stack s
∧ pending s' = (pending s - {u}×(E``{u} - it))
∧ gen_discovered s' ⊇ gen_discovered s ∪ (E``{u} - it)
))
(E``{u}) (λs. ¬gds_is_break gds s)
(λv s. do {
s ← choose_pending u (Some v) s;
if gds_is_discovered gds v s then do {
if gds_is_finished gds v s then
gds_cross_edge gds u v s
else
gds_back_edge gds u v s
} else do {
s ← gds_discover gds u v s;
if gds_is_break gds s then RETURN s else D (v,s)
}
})
s;
if gds_is_break gds s then
RETURN s
else do {
s ← choose_pending u (None) s;
s ← gds_finish gds u s;
RETURN s
}
}) (v0,s)
}
}
}) s
}"
definition rec_impl_for_paper where "rec_impl_for_paper ≡ do {
s ← gds_init gds;
FOREACHc V0 (Not o gds_is_break gds) (λv0 s. do {
if gds_is_discovered gds v0 s then RETURN s
else do {
s ← gds_new_root gds v0 s;
if gds_is_break gds s then RETURN s
else do {
REC (λD (u,s). do {
s ← FOREACHc (E``{u}) (λs. ¬gds_is_break gds s) (λv s. do {
s ← choose_pending u (Some v) s;
if gds_is_discovered gds v s then do {
if gds_is_finished gds v s then gds_cross_edge gds u v s
else gds_back_edge gds u v s
} else do {
s ← gds_discover gds u v s;
if gds_is_break gds s then RETURN s else D (v,s)
}
})
s;
if gds_is_break gds s then RETURN s
else do {
s ← choose_pending u (None) s;
gds_finish gds u s
}
}) (v0,s)
}
}
}) s
}"
end
locale rec_impl =
fb_graph G + gen_dfs gds V0 + rec_impl_defs G gds pending stack choose_pending
for G :: "('v, 'more) graph_rec_scheme"
and gds :: "('v,'s)gen_dfs_struct"
and pending :: "'s ⇒ 'v rel"
and stack :: "'s ⇒ 'v list"
and choose_pending :: "'v ⇒ 'v option ⇒ 's ⇒ 's nres"
+
assumes [simp]: "gds_is_empty_stack gds s ⟷ stack s = []"
assumes init_spec:
"gds_init gds ≤⇩n SPEC (λs. stack s = [] ∧ pending s = {})"
assumes new_root_spec:
"⟦pre_new_root v0 s⟧
⟹ gds_new_root gds v0 s ≤⇩n SPEC (λs'.
stack s' = [v0] ∧ pending s' = {v0}×E``{v0} ∧
gen_discovered s' = insert v0 (gen_discovered s))"
assumes get_pending_fmt: "⟦ pre_get_pending s ⟧ ⟹
do {
let u = hd (stack s);
vo ← SELECT (λv. (u,v)∈pending s);
s ← choose_pending u vo s;
RETURN (u,vo,s)
}
≤ gds_get_pending gds s"
assumes choose_pending_spec: "⟦pre_get_pending s; u = hd (stack s);
case vo of
None ⇒ pending s `` {u} = {}
| Some v ⇒ v∈pending s `` {u}
⟧ ⟹
choose_pending u vo s ≤⇩n SPEC (λs'.
(case vo of
None ⇒ pending s' = pending s
| Some v ⇒ pending s' = pending s - {(u,v)}) ∧
stack s' = stack s ∧
(∀x. gds_is_discovered gds x s' = gds_is_discovered gds x s)
)"
assumes finish_spec: "⟦pre_finish u s0 s⟧
⟹ gds_finish gds u s ≤⇩n SPEC (λs'.
pending s' = pending s ∧
stack s' = tl (stack s) ∧
(∀x. gds_is_discovered gds x s' = gds_is_discovered gds x s))"
assumes cross_edge_spec: "pre_cross_edge u v s0 s
⟹ gds_cross_edge gds u v s ≤⇩n SPEC (λs'.
pending s' = pending s ∧ stack s' = stack s ∧
(∀x. gds_is_discovered gds x s' = gds_is_discovered gds x s))"
assumes back_edge_spec: "pre_back_edge u v s0 s
⟹ gds_back_edge gds u v s ≤⇩n SPEC (λs'.
pending s' = pending s ∧ stack s' = stack s ∧
(∀x. gds_is_discovered gds x s' = gds_is_discovered gds x s))"
assumes discover_spec: "pre_discover u v s0 s
⟹ gds_discover gds u v s ≤⇩n SPEC (λs'.
pending s' = pending s ∪ ({v} × E``{v}) ∧ stack s' = v#stack s ∧
gen_discovered s' = insert v (gen_discovered s))"
begin
lemma gen_step'_refine:
"⟦gen_rwof s; gen_cond s⟧ ⟹ gen_step' s ≤ gen_step s"
apply (simp only: gen_step'_def gen_step_def)
apply (clarsimp)
apply (rule order_trans[OF _ bind_mono(1)[OF get_pending_fmt order_refl]])
apply (simp add: pw_le_iff refine_pw_simps
split: option.splits if_split)
apply (simp add: pre_defs gen_cond_def)
done
lemma gen_dfs'_refine: "gen_dfs' ≤ gen_dfs"
unfolding gen_dfs'_def gen_dfs_def WHILE_eq_I_rwof[where f=gen_step]
apply (rule refine_IdD)
apply (refine_rcg)
by (simp_all add: gen_step'_refine)
lemma gen_rwof'_imp_rwof:
assumes NF: "nofail gen_dfs"
assumes A: "gen_rwof' s"
shows "gen_rwof s"
apply (rule rwof_step_refine)
apply (rule NF[unfolded gen_dfs_def])
apply fact
apply (rule leof_lift[OF gen_step'_refine], assumption+) []
done
lemma reachable_invar:
"gen_rwof' s ⟹ set (stack s) ⊆ reachable ∧ pending s ⊆ E
∧ set (stack s) ⊆ gen_discovered s ∧ distinct (stack s)
∧ pending s ⊆ set (stack s) × UNIV"
apply (erule establish_rwof_invar[rotated -1])
apply (rule leof_trans[OF init_spec], auto) []
apply (subst gen_step'_def)
apply (refine_rcg refine_vcg
leof_trans[OF new_root_spec]
SELECT_rule[THEN leof_lift]
leof_trans[OF choose_pending_spec[THEN leof_strengthen_SPEC]]
leof_trans[OF finish_spec]
leof_trans[OF cross_edge_spec]
leof_trans[OF back_edge_spec]
leof_trans[OF discover_spec]
)
apply simp_all
subgoal by (simp add: pre_defs, simp add: gen_cond_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (simp add: pre_defs, simp add: gen_cond_def)
apply ((unfold pre_defs, intro conjI); assumption?) []
subgoal by (clarsimp simp: gen_cond_def)
subgoal by (clarsimp simp: gen_cond_def)
subgoal
apply (rule pwD2[OF get_pending_fmt])
subgoal by (simp add: pre_defs gen_cond_def)
subgoal by (clarsimp simp: refine_pw_simps; blast)
done
subgoal by (force simp: neq_Nil_conv) []
subgoal by (clarsimp simp: neq_Nil_conv gen_cond_def, blast) []
subgoal by (clarsimp simp: neq_Nil_conv gen_cond_def; auto)
apply (unfold pre_defs, intro conjI, assumption) []
subgoal by (clarsimp_all simp: gen_cond_def)
subgoal by (clarsimp_all simp: gen_cond_def)
apply (rule pwD2[OF get_pending_fmt])
apply (simp add: pre_defs gen_cond_def; fail)
apply (clarsimp simp: refine_pw_simps select_def, blast; fail)
apply (simp; fail)
apply (simp; fail)
subgoal by auto
subgoal by fast
apply (unfold pre_defs, intro conjI, assumption) []
apply (clarsimp simp: gen_cond_def; fail)
apply (clarsimp simp: gen_cond_def; fail)
apply (rule pwD2[OF get_pending_fmt])
apply (simp add: pre_defs gen_cond_def; fail)
apply (clarsimp simp: refine_pw_simps select_def, blast; fail)
apply (simp; fail)
subgoal
apply clarsimp
by (meson ImageI SigmaD1 rtrancl_image_unfold_right subset_eq)
subgoal
apply clarsimp
by blast
apply force
apply force
apply fast
apply (auto simp: pre_defs gen_cond_def; fail)
apply fast
apply ((unfold pre_defs, intro conjI); assumption?)
apply (clarsimp simp: gen_cond_def; fail)
apply (clarsimp simp: gen_cond_def; fail)
apply (rule pwD2[OF get_pending_fmt])
apply (simp add: pre_defs gen_cond_def; fail)
apply (clarsimp simp: refine_pw_simps; fail)
apply (auto simp: neq_Nil_conv; fail)
apply (auto simp: neq_Nil_conv; fail)
apply (clarsimp simp: neq_Nil_conv; blast)
done
lemma mk_spec_aux:
"⟦m ≤⇩n SPEC Φ; m≤SPEC gen_rwof' ⟧ ⟹ m ≤ SPEC (λs. gen_rwof' s ∧ Φ s)"
by (rule SPEC_rule_conj_leofI1)
definition "post_choose_pending u vo s0 s ≡
gen_rwof' s0
∧ gen_cond s0
∧ stack s0 ≠ []
∧ u=hd (stack s0)
∧ inres (choose_pending u vo s0) s
∧ stack s = stack s0
∧ (∀x. gds_is_discovered gds x s = gds_is_discovered gds x s0)
∧ (case vo of
None ⇒ pending s0``{u}={} ∧ pending s = pending s0
| Some v ⇒ v ∈ pending s0``{u} ∧ pending s = pending s0 - {(u,v)})"
context
assumes nofail:
"nofail (gds_init gds ⤜ WHILE gen_cond gen_step')"
assumes nofail2:
"nofail (gen_dfs)"
begin
lemma pcp_imp_pgp:
"post_choose_pending u vo s0 s ⟹ post_get_pending u vo s0 s"
unfolding post_choose_pending_def pre_defs
apply (intro conjI)
apply (simp add: gen_rwof'_imp_rwof[OF nofail2])
apply simp
apply (simp add: gen_cond_def)
apply (rule pwD2[OF get_pending_fmt])
apply (simp add: pre_defs gen_cond_def
gen_rwof'_imp_rwof[OF nofail2])
apply (auto simp add: refine_pw_simps select_def split: option.splits) []
done
schematic_goal gds_init_refine: "?prop"
apply (rule mk_spec_aux[OF init_spec])
apply (rule rwof_init[OF nofail])
done
schematic_goal gds_new_root_refine:
"⟦pre_new_root v0 s; gen_rwof' s⟧ ⟹ gds_new_root gds v0 s ≤ SPEC ?Φ"
apply (rule mk_spec_aux[OF new_root_spec], assumption)
apply (rule order_trans[OF _ rwof_step[OF nofail, where s=s]])
unfolding gen_step'_def pre_new_root_def gen_cond_def
apply (auto simp: pw_le_iff refine_pw_simps)
done
schematic_goal gds_choose_pending_refine:
assumes 1: "pre_get_pending s"
assumes 2: "gen_rwof' s"
assumes [simp]: "u=hd (stack s)"
assumes 3: "case vo of
None ⇒ pending s `` {u} = {}
| Some v ⇒ v ∈ pending s `` {u}"
shows "choose_pending u vo s ≤ SPEC (post_choose_pending u vo s)"
proof -
from WHILE_nofail_imp_rwof_nofail[OF nofail 2] 1 3 have
"nofail (choose_pending u vo s)"
unfolding pre_defs gen_step'_def gen_cond_def
by (auto simp: refine_pw_simps select_def
split: option.splits if_split_asm)
also have "choose_pending u vo s ≤⇩n SPEC (post_choose_pending u vo s)"
apply (rule leof_trans[OF choose_pending_spec[OF 1 _ 3, THEN leof_strengthen_SPEC]])
apply simp
apply (rule leof_RES_rule)
using 1
apply (simp add: post_choose_pending_def 2 pre_defs gen_cond_def split: option.splits)
using 3
apply auto
done
finally (leofD) show ?thesis .
qed
schematic_goal gds_finish_refine:
"⟦pre_finish u s0 s; post_choose_pending u None s0 s⟧ ⟹ gds_finish gds u s ≤ SPEC ?Φ"
apply (rule mk_spec_aux[OF finish_spec], assumption)
apply (rule order_trans[OF _ rwof_step[OF nofail, where s=s0]])
unfolding gen_step'_def pre_defs gen_cond_def post_choose_pending_def
apply (auto simp: pw_le_iff refine_pw_simps split: option.split)
done
schematic_goal gds_cross_edge_refine:
"⟦pre_cross_edge u v s0 s; post_choose_pending u (Some v) s0 s⟧ ⟹ gds_cross_edge gds u v s ≤ SPEC ?Φ"
apply (rule mk_spec_aux[OF cross_edge_spec], assumption)
apply (rule order_trans[OF _ rwof_step[OF nofail, where s=s0]])
unfolding gen_step'_def pre_defs gen_cond_def post_choose_pending_def
apply (simp add: pw_le_iff refine_pw_simps select_def split: option.split, blast)
apply simp
apply blast
done
schematic_goal gds_back_edge_refine:
"⟦pre_back_edge u v s0 s; post_choose_pending u (Some v) s0 s⟧ ⟹ gds_back_edge gds u v s ≤ SPEC ?Φ"
apply (rule mk_spec_aux[OF back_edge_spec], assumption)
apply (rule order_trans[OF _ rwof_step[OF nofail, where s=s0]])
unfolding gen_step'_def pre_defs gen_cond_def post_choose_pending_def
apply (simp add: pw_le_iff refine_pw_simps select_def split: option.split, blast)
apply simp
apply blast
done
schematic_goal gds_discover_refine:
"⟦pre_discover u v s0 s; post_choose_pending u (Some v) s0 s⟧ ⟹ gds_discover gds u v s ≤ SPEC ?Φ"
apply (rule mk_spec_aux[OF discover_spec], assumption)
apply (rule order_trans[OF _ rwof_step[OF nofail, where s=s0]])
unfolding gen_step'_def pre_defs gen_cond_def post_choose_pending_def
apply (simp add: pw_le_iff refine_pw_simps select_def split: option.split, blast)
apply simp
apply blast
done
end
lemma rec_impl_aux: "⟦ xd∉Domain P ⟧ ⟹ P - {y} × (succ y - ita) - {(y, xd)} - {xd} × UNIV =
P - insert (y, xd) ({y} × (succ y - ita))"
apply auto
done
lemma rec_impl: "rec_impl ≤ gen_dfs"
apply (rule le_nofailI)
apply (rule order_trans[OF _ gen_dfs'_refine])
unfolding gen_dfs'_def
apply (rule WHILE_refine_rwof)
unfolding rec_impl_def
apply (refine_rcg refine_vcg
order_trans[OF gds_init_refine]
order_trans[OF gds_choose_pending_refine]
order_trans[OF gds_new_root_refine]
order_trans[OF gds_finish_refine]
order_trans[OF gds_back_edge_refine]
order_trans[OF gds_cross_edge_refine]
order_trans[OF gds_discover_refine]
)
apply (simp_all split: if_split_asm)
using [[goals_limit = 1]]
apply (auto simp add: pre_defs; fail)
apply (auto simp add: pre_defs gen_rwof'_imp_rwof; fail)
apply (auto; fail)
apply (auto dest: reachable_invar; fail)
apply (auto simp add: pre_defs gen_rwof'_imp_rwof; fail)
apply (auto; fail)
apply (auto; fail)
apply ((drule pcp_imp_pgp, auto simp add: pre_defs gen_rwof'_imp_rwof); fail)
apply (auto simp: post_choose_pending_def; fail)
apply (auto simp: post_choose_pending_def; fail)
apply (auto simp: post_choose_pending_def; fail)
apply ((drule pcp_imp_pgp, auto simp add: pre_defs gen_rwof'_imp_rwof); fail)
apply (auto simp: post_choose_pending_def; fail)
apply (auto simp: post_choose_pending_def; fail)
apply (auto simp: post_choose_pending_def; fail)
apply ((drule pcp_imp_pgp, auto simp add: pre_defs gen_rwof'_imp_rwof); fail)
apply (rule order_trans)
apply rprems
apply (auto; fail) []
subgoal
apply (rule SPEC_rule)
apply (simp add: post_choose_pending_def gen_rwof'_imp_rwof
split: if_split_asm)
apply (clarsimp
simp: gen_rwof'_imp_rwof Un_Diff
split: if_split_asm) []
apply (clarsimp simp: it_step_insert_iff neq_Nil_conv)
apply (rule conjI)
subgoal
apply (rule rec_impl_aux)
apply (drule reachable_invar)+
apply (metis Domain.cases SigmaD1 mem_Collect_eq rev_subsetD)
done
subgoal
apply (rule conjI)
apply auto []
apply (metis order_trans)
done
done
apply (auto simp add: pre_defs gen_rwof'_imp_rwof; fail)
apply (auto; fail)
apply (auto dest: reachable_invar; fail)
apply ((drule pcp_imp_pgp, auto simp add: pre_defs gen_rwof'_imp_rwof); fail)
apply (auto simp: post_choose_pending_def; fail)
apply (auto simp: post_choose_pending_def; fail)
apply (auto simp: post_choose_pending_def; fail)
apply (auto; fail)
apply (auto simp: gen_cond_def; fail)
apply (auto simp: gen_cond_def; fail)
done
end
end