Theory Worklist_Subsumption_Multiset
section ‹Generic Worklist Algorithm With Subsumption›
theory Worklist_Subsumption_Multiset
imports
Refine_Imperative_HOL.Sepref
Worklist_Algorithms_Misc
Worklist_Locales
Unified_PW
begin
text ‹This section develops an implementation of the worklist algorithm for reachability
without a shared passed-waiting list.
The obtained imperative implementation may be less efficient for the purpose
of timed automata model checking
but the variants obtained from the refinement steps are more general and could serve a wider range
of future use cases.›
subsection ‹Utilities›
definition take_from_set where
"take_from_set s = ASSERT (s ≠ {}) ⪢ SPEC (λ (x, s'). x ∈ s ∧ s' = s - {x})"
lemma take_from_set_correct:
assumes "s ≠ {}"
shows "take_from_set s ≤ SPEC (λ (x, s'). x ∈ s ∧ s' = s - {x})"
using assms unfolding take_from_set_def by simp
lemmas [refine_vcg] = take_from_set_correct[THEN order.trans]
definition take_from_mset where
"take_from_mset s = ASSERT (s ≠ {#}) ⪢ SPEC (λ (x, s'). x ∈# s ∧ s' = s - {#x#})"
lemma take_from_mset_correct:
assumes "s ≠ {#}"
shows "take_from_mset s ≤ SPEC (λ (x, s'). x ∈# s ∧ s' = s - {#x#})"
using assms unfolding take_from_mset_def by simp
lemmas [refine_vcg] = take_from_mset_correct[THEN order.trans]
lemma set_mset_mp: "set_mset m ⊆ s ⟹ n < count m x ⟹ x∈s"
by (meson count_greater_zero_iff le_less_trans subsetCE zero_le)
lemma pred_not_lt_is_zero: "(¬ n - Suc 0 < n) ⟷ n=0" by auto
lemma (in Search_Space_finite_strict) finitely_branching:
assumes "reachable a"
shows "finite (Collect (E a))"
by (metis assms finite_reachable finite_subset mem_Collect_eq reachable_step subsetI)
subsection ‹Standard Worklist Algorithm›
context Search_Space_Defs_Empty begin
definition "worklist_start_subsumed passed wait = (∃ a ∈ passed ∪ set_mset wait. a⇩0 ≼ a)"
definition
"worklist_var =
inv_image (finite_psupset (Collect reachable) <*lex*> measure size) (λ (a, b,c). (a,b))"
definition "worklist_inv_frontier passed wait =
(∀ a ∈ passed. ∀ a'. E a a' ∧ ¬ empty a' ⟶ (∃ b' ∈ passed ∪ set_mset wait. a' ≼ b'))"
definition "worklist_inv ≡ λ (passed, wait, brk).
passed ⊆ Collect reachable ∧
(brk ⟶ (∃ f. reachable f ∧ F f)) ∧
(¬ brk ⟶
worklist_inv_frontier passed wait
∧ (∀ a ∈ passed ∪ set_mset wait. ¬ F a)
∧ worklist_start_subsumed passed wait
∧ set_mset wait ⊆ Collect reachable)
"
definition "add_succ_spec wait a ≡ SPEC (λ(wait',brk).
if ∃a'. E a a' ∧ F a' then
brk
else
¬brk ∧ set_mset wait' ⊆ set_mset wait ∪ {a' . E a a'} ∧
(∀ s ∈ set_mset wait ∪ {a' . E a a' ∧ ¬ empty a'}. ∃ s' ∈ set_mset wait'. s ≼ s')
)"
definition worklist_algo where
"worklist_algo = do
{
if F a⇩0 then RETURN True
else do {
let passed = {};
let wait = {#a⇩0#};
(passed, wait, brk) ← WHILEIT worklist_inv (λ (passed, wait, brk). ¬ brk ∧ wait ≠ {#})
(λ (passed, wait, brk). do
{
(a, wait) ← take_from_mset wait;
ASSERT (reachable a);
if (∃ a' ∈ passed. a ≼ a') then RETURN (passed, wait, brk) else
do
{
(wait,brk) ← add_succ_spec wait a;
let passed = insert a passed;
RETURN (passed, wait, brk)
}
}
)
(passed, wait, False);
RETURN brk
}
}
"
end
subsubsection ‹Correctness Proof›
lemma (in Search_Space) empty_E_star:
"empty x'" if "E⇧*⇧* x x'" "reachable x" "empty x"
using that unfolding reachable_def
by (induction rule: converse_rtranclp_induct)
(blast intro: empty_E[unfolded reachable_def] rtranclp.rtrancl_into_rtrancl)+
context Search_Space_finite_strict begin
lemma wf_worklist_var:
"wf worklist_var"
unfolding worklist_var_def by (auto simp: finite_reachable)
context
begin
private lemma aux1:
assumes "∀x∈passed. ¬ a ≼ x"
and "passed ⊆ Collect reachable"
and "reachable a"
shows "
((insert a passed, wait', brk'),
passed, wait, brk)
∈ worklist_var"
proof -
from assms have "a ∉ passed" by auto
with assms(2,3) show ?thesis
by (auto simp: worklist_inv_def worklist_var_def finite_psupset_def)
qed
private lemma aux2:
assumes
"a' ∈ passed"
"a ≼ a'"
"a ∈# wait"
"worklist_inv_frontier passed wait"
shows "worklist_inv_frontier passed (wait - {#a#})"
using assms unfolding worklist_inv_frontier_def
using trans
apply clarsimp
by (metis (no_types, lifting) Un_iff count_eq_zero_iff count_single mset_contains_eq mset_un_cases)
private lemma aux5:
assumes
"a' ∈ passed"
"a ≼ a'"
"a ∈# wait"
"worklist_start_subsumed passed wait"
shows "worklist_start_subsumed passed (wait - {#a#})"
using assms unfolding worklist_start_subsumed_def apply clarsimp
by (metis Un_iff insert_DiffM2 local.trans mset_right_cancel_elem)
private lemma aux3:
assumes
"set_mset wait ⊆ Collect reachable"
"a ∈# wait"
"∀ s ∈ set_mset (wait - {#a#}) ∪ {a'. E a a' ∧ ¬ empty a'}. ∃ s' ∈ set_mset wait'. s ≼ s'"
"worklist_inv_frontier passed wait"
shows "worklist_inv_frontier (insert a passed) wait'"
proof -
from assms(1,2) have "reachable a"
by (simp add: subset_iff)
with finitely_branching have [simp, intro!]: "finite (Collect (E a))" .
show ?thesis unfolding worklist_inv_frontier_def
apply safe
subgoal
using assms by auto
subgoal for b b'
proof -
assume A: "E b b'" "¬ empty b'" "b ∈ passed"
with assms obtain b'' where b'': "b'' ∈ passed ∪ set_mset wait" "b' ≼ b''"
unfolding worklist_inv_frontier_def by blast
from this(1) show ?thesis
apply standard
subgoal
using ‹b' ≼ b''› by auto
subgoal
apply (cases "a = b''")
subgoal
using b''(2) by blast
subgoal premises prems
proof -
from prems have "b'' ∈# wait - {#a#}"
by (auto simp: mset_remove_member)
with assms prems ‹b' ≼ b''› show ?thesis
by (blast intro: local.trans)
qed
done
done
qed
done
qed
private lemma aux6:
assumes
"a ∈# wait"
"worklist_start_subsumed passed wait"
"∀ s ∈ set_mset (wait - {#a#}) ∪ {a'. E a a' ∧ ¬ empty a'}. ∃ s' ∈ set_mset wait'. s ≼ s'"
shows "worklist_start_subsumed (insert a passed) wait'"
using assms unfolding worklist_start_subsumed_def
apply clarsimp
apply (erule disjE)
apply blast
subgoal premises prems for x
proof (cases "a = x")
case True
with prems show ?thesis by simp
next
case False
with ‹x ∈# wait› have "x ∈ set_mset (wait - {#a#})"
by (metis insert_DiffM insert_noteq_member prems(1))
with prems(2,4) ‹_ ≼ x› show ?thesis
by (auto dest: trans)
qed
done
lemma aux4:
assumes "worklist_inv_frontier passed {#}" "reachable x" "worklist_start_subsumed passed {#}"
"passed ⊆ Collect reachable"
shows "∃ x' ∈ passed. x ≼ x'"
proof -
from ‹reachable x› have "E⇧*⇧* a⇩0 x" by (simp add: reachable_def)
from assms(3) obtain b where "a⇩0 ≼ b" "b ∈ passed" unfolding worklist_start_subsumed_def by auto
have "∃x'. ∃ x''. E⇧*⇧* b x' ∧ x ≼ x' ∧ x' ≼ x'' ∧ x'' ∈ passed" if
"E⇧*⇧* a x" "a ≼ b" "b ≼ b'" "b' ∈ passed"
"reachable a" "reachable b" for a b b'
using that proof (induction arbitrary: b b' rule: converse_rtranclp_induct)
case base
then show ?case by auto
next
case (step a a1 b b')
show ?case
proof (cases "empty a")
case True
with step.prems step.hyps have "empty x" by - (rule empty_E_star, auto)
with step.prems show ?thesis by (auto intro: empty_subsumes)
next
case False
with ‹E a a1› ‹a ≼ b› ‹reachable a› ‹reachable b› obtain b1 where
"E b b1" "a1 ≼ b1"
using mono by blast
show ?thesis
proof (cases "empty b1")
case True
with empty_mono ‹a1 ≼ b1› have "empty a1" by blast
with step.prems step.hyps have "empty x" by - (rule empty_E_star, auto simp: reachable_def)
with step.prems show ?thesis by (auto intro: empty_subsumes)
next
case False
from ‹E b b1› ‹a1 ≼ b1› obtain b1' where "E b' b1'" "b1 ≼ b1'"
using ‹¬ empty a› empty_mono assms(4) mono step.prems by blast
from empty_mono[OF ‹¬ empty b1› ‹b1 ≼ b1'›] have "¬ empty b1'"
by auto
with ‹E b' b1'› ‹b' ∈ passed› assms(1) obtain b1'' where "b1'' ∈ passed" "b1' ≼ b1''"
unfolding worklist_inv_frontier_def by auto
with ‹b1 ≼ _› have "b1 ≼ b1''" using trans by blast
with step.IH[OF ‹a1 ≼ b1› this ‹b1'' ∈ passed›] ‹reachable a› ‹E a a1› ‹reachable b› ‹E b b1›
obtain x' x'' where
"E⇧*⇧* b1 x'" "x ≼ x'" "x' ≼ x''" "x'' ∈ passed"
by auto
moreover from ‹E b b1› ‹E⇧*⇧* b1 x'› have "E⇧*⇧* b x'" by auto
ultimately show ?thesis by auto
qed
qed
qed
from this[OF ‹E⇧*⇧* a⇩0 x› ‹a⇩0 ≼ b› refl ‹b ∈ _›] assms(4) ‹b ∈ passed› show ?thesis
by (auto intro: trans)
qed
theorem worklist_algo_correct:
"worklist_algo ≤ SPEC (λ brk. brk ⟷ F_reachable)"
proof -
note [simp] = size_Diff_submset pred_not_lt_is_zero
note [dest] = set_mset_mp
show ?thesis
unfolding worklist_algo_def add_succ_spec_def F_reachable_def
apply (refine_vcg wf_worklist_var)
apply (solves auto)
apply (solves ‹auto simp:
worklist_inv_def worklist_inv_frontier_def worklist_start_subsumed_def›)
apply (simp; fail)
apply (solves ‹auto simp: worklist_inv_def›)
apply (solves ‹auto simp: worklist_inv_def aux2 aux5
dest: in_diffD
split: if_split_asm›)
apply (solves
‹auto simp: worklist_inv_def worklist_var_def intro: finite_subset[OF _ finite_reachable]›)
apply (clarsimp split: if_split_asm)
apply (clarsimp simp: worklist_inv_def; blast)
apply (auto
simp: worklist_inv_def aux3 aux6 finitely_branching
dest: in_diffD)[]
apply (metis Un_iff in_diffD insert_subset mem_Collect_eq mset_add set_mset_add_mset_insert)
subgoal for ab aaa baa aba aca _ x
proof -
assume
"reachable aba"
"set_mset aca ⊆ set_mset (aaa - {#aba#}) ∪ Collect (E aba)"
"set_mset aaa ⊆ Collect reachable"
"x ∈# aca"
then show ?thesis
by (auto dest: in_diffD)
qed
apply (solves ‹auto simp: worklist_inv_def aux1›)
using F_mono by (fastforce simp: worklist_inv_def dest!: aux4)
qed
lemmas [refine_vcg] = worklist_algo_correct[THEN Orderings.order.trans]
end
end
context Search_Space''_Defs
begin
definition "worklist_inv_frontier' passed wait =
(∀ a ∈ passed. ∀ a'. E a a' ∧ ¬ empty a' ⟶ (∃ b' ∈ passed ∪ set_mset wait. a' ≼ b'))"
definition "worklist_start_subsumed' passed wait = (∃ a ∈ passed ∪ set_mset wait. a⇩0 ≼ a)"
definition "worklist_inv' ≡ λ (passed, wait, brk).
worklist_inv (passed, wait, brk) ∧ (∀ a ∈ passed. ¬ empty a) ∧ (∀ a ∈ set_mset wait. ¬ empty a)
"
definition "add_succ_spec' wait a ≡ SPEC (λ(wait',brk).
(
if ∃a'. E a a' ∧ F a' then
brk
else
¬brk ∧ set_mset wait' ⊆ set_mset wait ∪ {a' . E a a'} ∧
(∀ s ∈ set_mset wait ∪ {a' . E a a' ∧ ¬ empty a'}. ∃ s' ∈ set_mset wait'. s ≼ s')
) ∧ (∀ s ∈ set_mset wait'. ¬ empty s)
)"
definition worklist_algo' where
"worklist_algo' = do
{
if F a⇩0 then RETURN True
else do {
let passed = {};
let wait = {#a⇩0#};
(passed, wait, brk) ← WHILEIT worklist_inv' (λ (passed, wait, brk). ¬ brk ∧ wait ≠ {#})
(λ (passed, wait, brk). do
{
(a, wait) ← take_from_mset wait;
ASSERT (reachable a);
if (∃ a' ∈ passed. a ⊴ a') then RETURN (passed, wait, brk) else
do
{
(wait,brk) ← add_succ_spec' wait a;
let passed = insert a passed;
RETURN (passed, wait, brk)
}
}
)
(passed, wait, False);
RETURN brk
}
}
"
end
context Search_Space''_start
begin
lemma worklist_algo_list_inv_ref[refine]:
fixes x x'
assumes
"¬ F a⇩0" "¬ F a⇩0"
"(x, x') ∈ {((passed,wait,brk), (passed',wait',brk')).
passed = passed' ∧ wait = wait' ∧ brk = brk' ∧ (∀ a ∈ passed. ¬ empty a)
∧ (∀ a ∈ set_mset wait. ¬ empty a)}"
"worklist_inv x'"
shows "worklist_inv' x"
using assms
unfolding worklist_inv'_def worklist_inv_def
by auto
lemma [refine]:
"take_from_mset wait ≤
⇓ {((x, wait), (y, wait')). x = y ∧ wait = wait' ∧ ¬ empty x ∧ (∀ a ∈ set_mset wait. ¬ empty a)}
(take_from_mset wait')"
if "wait = wait'" "∀ a ∈ set_mset wait. ¬ empty a" "wait ≠ {#}"
using that
by (auto 4 5 simp: pw_le_iff refine_pw_simps dest: in_diffD dest!: take_from_mset_correct)
lemma [refine]:
"add_succ_spec' wait x ≤
⇓ ({(wait, wait'). wait = wait' ∧ (∀ a ∈ set_mset wait. ¬ empty a)} ×⇩r bool_rel)
(add_succ_spec wait' x')"
if "wait = wait'" "x = x'" "∀ a ∈ set_mset wait. ¬ empty a"
using that
unfolding add_succ_spec'_def add_succ_spec_def
by (auto simp: pw_le_iff refine_pw_simps)
lemma worklist_algo'_ref[refine]: "worklist_algo' ≤ ⇓Id worklist_algo"
using [[goals_limit=15]]
unfolding worklist_algo'_def worklist_algo_def
apply (refine_rcg)
prefer 3
apply assumption
apply refine_dref_type
by (auto simp: empty_subsumes')
end
context Search_Space''_Defs
begin
definition worklist_algo'' where
"worklist_algo'' ≡
if empty a⇩0 then RETURN False else worklist_algo'
"
end
context Search_Space''_finite_strict
begin
lemma worklist_algo''_correct:
"worklist_algo'' ≤ SPEC (λ brk. brk ⟷ F_reachable)"
proof (cases "empty a⇩0")
case True
then show ?thesis
unfolding worklist_algo''_def F_reachable_def reachable_def
using empty_E_star final_non_empty by auto
next
case False
interpret Search_Space''_start
by standard (rule ‹¬ empty _›)
note worklist_algo'_ref
also note worklist_algo_correct
finally show ?thesis
using False unfolding worklist_algo''_def by simp
qed
end
end