Theory Unified_PW_Hashing
theory Unified_PW_Hashing
imports
Unified_PW
Refine_Imperative_HOL.IICF_List_Mset
Worklist_Algorithms_Misc
Worklist_Algorithms_Tracing
begin
subsection ‹Towards an Implementation of the Unified Passed-Waiting List›
context Worklist1_Defs
begin
definition "add_pw_unified_spec passed wait a ≡ SPEC (λ(passed',wait',brk).
if ∃ x ∈ set (succs a). F x then brk
else passed' ⊆ passed ∪ {x ∈ set (succs a). ¬ (∃ y ∈ passed. x ≼ y)}
∧ passed ⊆ passed'
∧ wait ⊆# wait'
∧ wait' ⊆# wait + mset ([x ← succs a. ¬ (∃ y ∈ passed. x ≼ y)])
∧ (∀ x ∈ set (succs a). ∃ y ∈ passed'. x ≼ y)
∧ (∀ x ∈ set (succs a). ¬ (∃ y ∈ passed. x ≼ y) ⟶ (∃ y ∈# wait'. x ≼ y))
∧ ¬ brk)
"
definition "add_pw passed wait a ≡
nfoldli (succs a) (λ(_, _, brk). ¬brk)
(λa (passed, wait, brk). RETURN (
if F a then
(passed, wait, True)
else if ∃ x ∈ passed. a ≼ x then
(passed, wait, False)
else (insert a passed, add_mset a wait, False)
))
(passed, wait, False)
"
end
context Worklist1
begin
lemma add_pw_unified_spec_ref:
"add_pw_unified_spec passed wait a ≤ add_pw_spec passed wait a"
if "reachable a" "a ∈ passed"
using succs_correct[OF that(1)] that(2)
unfolding add_pw_unified_spec_def add_pw_spec_def
apply simp
apply safe
apply (all ‹auto simp: empty_subsumes; fail | succeed›)
using mset_subset_eqD apply force
using mset_subset_eqD apply force
subgoal premises prems
using prems
by (auto 4 5 simp: filter_mset_eq_empty_iff intro: trans elim!: subset_mset.ord_le_eq_trans)
by (clarsimp, smt UnE mem_Collect_eq subsetCE)
lemma add_pw_ref:
"add_pw passed wait a ≤ ⇓ Id (add_pw_unified_spec passed wait a)"
unfolding add_pw_def add_pw_unified_spec_def
apply (refine_vcg
nfoldli_rule[where I =
"λ l1 l2 (passed', wait', brk).
if brk then ∃ a' ∈ set (succs a). F a'
else passed' ⊆ passed ∪ {x ∈ set l1. ¬ (∃ y ∈ passed. x ≼ y)}
∧ passed ⊆ passed'
∧ wait ⊆# wait'
∧ wait' ⊆# wait + mset [x ← l1. ¬ (∃ y ∈ passed. x ≼ y)]
∧ (∀ x ∈ set l1. ∃ y ∈ passed'. x ≼ y)
∧ (∀ x ∈ set l1. ¬ (∃ y ∈ passed. x ≼ y) ⟶ (∃ y ∈# wait'. x ≼ y))
∧ set l1 ∩ Collect F = {}
"
])
apply (solves auto)
apply (clarsimp split: if_split_asm)
apply safe[]
apply (solves ‹auto simp add: subset_mset.le_iff_add›)+
subgoal premises prems
using prems trans by (metis (no_types, lifting) Un_iff in_mono mem_Collect_eq)
by (auto simp: subset_mset.le_iff_add)
end
context Worklist2_Defs
begin
definition "add_pw' passed wait a ≡
nfoldli (succs a) (λ(_, _, brk). ¬brk)
(λa (passed, wait, brk). RETURN (
if F a then
(passed, wait, True)
else if empty a then
(passed, wait, False)
else if ∃ x ∈ passed. a ⊴ x then
(passed, wait, False)
else (insert a passed, add_mset a wait, False)
))
(passed, wait, False)
"
definition pw_algo_unified where
"pw_algo_unified = do
{
if F a⇩0 then RETURN (True, {})
else if empty a⇩0 then RETURN (False, {})
else do {
(passed, wait) ← RETURN ({a⇩0}, {#a⇩0#});
(passed, wait, brk) ← WHILEIT pw_inv (λ (passed, wait, brk). ¬ brk ∧ wait ≠ {#})
(λ (passed, wait, brk). do
{
(a, wait) ← take_from_mset wait;
ASSERT (reachable a);
if empty a then RETURN (passed, wait, brk) else add_pw' passed wait a
}
)
(passed, wait, False);
RETURN (brk, passed)
}
}
"
end
context Worklist2
begin
lemma empty_subsumes'2:
"empty x ∨ x ⊴ y ⟷ x ≼ y"
using empty_subsumes' empty_subsumes by auto
lemma bex_or:
"P ∨ (∃ x ∈ S. Q x) ⟷ (∃ x ∈ S. P ∨ Q x)" if "S ≠ {}"
using that by auto
lemma add_pw'_ref':
"add_pw' passed wait a ≤ ⇓ (Id ∩ {((p, w, _), _). p ≠ {} ∧ set_mset w ⊆ p}) (add_pw passed wait a)"
if "passed ≠ {}" "set_mset wait ⊆ passed"
unfolding add_pw'_def add_pw_def
apply (rule nfoldli_refine)
apply refine_dref_type
using that apply (solves auto)+
apply refine_rcg
apply (rule Set.IntI)
unfolding z3_rule(44)
apply (subst bex_or)
by (auto simp add: empty_subsumes'2)
lemma add_pw'_ref1[refine]:
"add_pw' passed wait a
≤ ⇓ (Id ∩ {((p, w, _), _). p ≠ {} ∧ set_mset w ⊆ p}) (add_pw_spec passed' wait' a')"
if "passed ≠ {}" "set_mset wait ⊆ passed" "reachable a" "a ∈ passed"
and [simp]: "passed = passed'" "wait = wait'" "a = a'"
proof -
from add_pw_unified_spec_ref[OF that(3-4), of wait] add_pw_ref[of passed wait a] have
"add_pw passed wait a ≤ ⇓ Id (add_pw_spec passed wait a)"
by simp
moreover note add_pw'_ref'[OF that(1,2), of a]
ultimately show ?thesis
by (auto simp: pw_le_iff refine_pw_simps)
qed
lemma refine_weaken:
"p ≤ ⇓ R p'" if "p ≤ ⇓ S p'" "S ⊆ R"
using that by (simp add: pw_le_iff refine_pw_simps; blast)
lemma add_pw'_ref:
"add_pw' passed wait a ≤
⇓ ({((p, w, b), (p', w', b')). p ≠ {} ∧ p = p' ∪ set_mset w ∧ w = w' ∧ b = b'})
(add_pw_spec passed' wait' a')"
if "passed ≠ {}" "set_mset wait ⊆ passed" "reachable a" "a ∈ passed"
and [simp]: "passed = passed'" "wait = wait'" "a = a'"
by (rule add_pw'_ref1[OF that, THEN refine_weaken]; auto)
lemma
"(({a⇩0}, {#a⇩0#}, False), {}, {#a⇩0#}, False)
∈ {((p, w, b), (p', w', b')). p = p' ∪ set_mset w' ∧ w = w' ∧ b = b'}"
by auto
lemma [refine]:
"RETURN ({a⇩0}, {#a⇩0#}) ≤ ⇓ (Id ∩ {((p, w), (p', w')). p ≠ {} ∧ set_mset w ⊆ p}) init_pw_spec"
if "¬ empty a⇩0"
using that unfolding init_pw_spec_def by (auto simp: pw_le_iff refine_pw_simps)
lemma [refine]:
"take_from_mset wait ≤
⇓ {((x, wait), (y, wait')). x = y ∧ wait = wait' ∧ set_mset wait ⊆ passed ∧ x ∈ passed}
(take_from_mset wait')"
if "wait = wait'" "set_mset wait ⊆ passed" "wait ≠ {#}"
using that
by (auto 4 5 simp: pw_le_iff refine_pw_simps dest: in_diffD dest!: take_from_mset_correct)
lemma pw_algo_unified_ref:
"pw_algo_unified ≤ ⇓ Id pw_algo"
unfolding pw_algo_unified_def pw_algo_def
by refine_rcg (auto simp: init_pw_spec_def)
end
subsubsection ‹Utilities›
definition take_from_list where
"take_from_list s = ASSERT (s ≠ []) ⪢ SPEC (λ (x, s'). s = x # s')"
lemma take_from_list_correct:
assumes "s ≠ []"
shows "take_from_list s ≤ SPEC (λ (x, s'). s = x # s')"
using assms unfolding take_from_list_def by simp
lemmas [refine_vcg] = take_from_list_correct[THEN order.trans]
context Worklist_Map_Defs
begin
definition
"add_pw'_map passed wait a ≡
nfoldli (succs a) (λ(_, _, brk). ¬brk)
(λa (passed, wait, _).
do {
RETURN (
if F a then (passed, wait, True) else
let k = key a; passed' = (case passed k of Some passed' ⇒ passed' | None ⇒ {})
in
if empty a then
(passed, wait, False)
else if ∃ x ∈ passed'. a ⊴ x then
(passed, wait, False)
else
(passed(k ↦ (insert a passed')), a # wait, False)
)
}
)
(passed,wait,False)"
definition
"pw_map_inv ≡ λ (passed, wait, brk).
∃ passed' wait'.
(passed, passed') ∈ map_set_rel ∧ (wait, wait') ∈ list_mset_rel ∧
pw_inv (passed', wait', brk)
"
definition pw_algo_map where
"pw_algo_map = do
{
if F a⇩0 then RETURN (True, Map.empty)
else if empty a⇩0 then RETURN (False, Map.empty)
else do {
(passed, wait) ← RETURN ([key a⇩0 ↦ {a⇩0}], [a⇩0]);
(passed, wait, brk) ← WHILEIT pw_map_inv (λ (passed, wait, brk). ¬ brk ∧ wait ≠ [])
(λ (passed, wait, brk). do
{
(a, wait) ← take_from_list wait;
ASSERT (reachable a);
if empty a then RETURN (passed, wait, brk) else add_pw'_map passed wait a
}
)
(passed, wait, False);
RETURN (brk, passed)
}
}
"
end
lemma ran_upd_cases:
"(x ∈ ran m) ∨ (x = y)" if "x ∈ ran (m(a ↦ y))"
using that unfolding ran_def by (auto split: if_split_asm)
lemma ran_upd_cases2:
"(∃ k. m k = Some x ∧ k ≠ a) ∨ (x = y)" if "x ∈ ran (m(a ↦ y))"
using that unfolding ran_def by (auto split: if_split_asm)
context Worklist_Map
begin
lemma add_pw'_map_ref[refine]:
"add_pw'_map passed wait a ≤ ⇓ (map_set_rel ×⇩r list_mset_rel ×⇩r bool_rel) (add_pw' passed' wait' a')"
if "(passed, passed') ∈ map_set_rel" "(wait, wait') ∈ list_mset_rel" "(a, a') ∈ Id"
using that
unfolding add_pw'_map_def add_pw'_def
apply refine_rcg
apply refine_dref_type
apply (solves auto)
apply (solves auto)
apply (solves auto)
subgoal premises assms for a a' _ _ passed' _ wait' f' passed _ wait f
proof -
from assms have [simp]: "a' = a" "f = f'" by simp+
from assms have rel_passed: "(passed, passed') ∈ map_set_rel" by simp
then have union: "passed' = ⋃(ran passed)"
unfolding map_set_rel_def by auto
from assms have rel_wait: "(wait, wait') ∈ list_mset_rel" by simp
from rel_passed have keys[simp]: "key v = k" if "passed k = Some xs" "v ∈ xs" for k xs v
using that unfolding map_set_rel_def by auto
define k where "k ≡ key a"
define xs where "xs ≡ case passed k of None ⇒ {} | Some p ⇒ p"
have xs_ran: "x ∈ ⋃(ran passed)" if "x ∈ xs" for x
using that unfolding xs_def ran_def by (auto split: option.split_asm)
have *: "(∃x ∈ xs. a ⊴ x) ⟷ (∃x∈passed'. a' ⊴ x)"
proof standard
assume "∃x∈xs. a ⊴ x"
with rel_passed show "∃x∈passed'. a' ⊴ x"
unfolding xs_def union by (auto intro: ranI split: option.split_asm)
next
assume "∃x∈passed'. a' ⊴ x"
with rel_passed show "∃x∈xs. a ⊴ x" unfolding xs_def union ran_def k_def map_set_rel_def
using empty_subsumes'2 by force
qed
have "(passed(k ↦ insert a xs), insert a' passed') ∈ map_set_rel"
using ‹(passed, passed') ∈ map_set_rel›
unfolding map_set_rel_def
apply safe
subgoal
unfolding union by (auto dest!: ran_upd_cases xs_ran)
subgoal
unfolding ran_def by auto
subgoal for a''
unfolding union ran_def
apply clarsimp
subgoal for k'
unfolding xs_def by (cases "k' = k") auto
done
by (clarsimp split: if_split_asm, safe,
auto intro!: keys simp: xs_def k_def split: option.split_asm if_split_asm)
with rel_wait rel_passed show ?thesis
unfolding *[symmetric]
unfolding xs_def k_def Let_def
unfolding list_mset_rel_def br_def
by auto
qed
done
lemma init_map_ref[refine]:
"(([key a⇩0 ↦ {a⇩0}], [a⇩0]), {a⇩0}, {#a⇩0#}) ∈ map_set_rel ×⇩r list_mset_rel"
unfolding map_set_rel_def list_mset_rel_def br_def by auto
lemma take_from_list_ref[refine]:
"take_from_list xs ≤ ⇓ (Id ×⇩r list_mset_rel) (take_from_mset ms)" if "(xs, ms) ∈ list_mset_rel"
using that unfolding take_from_list_def take_from_mset_def list_mset_rel_def br_def
by (clarsimp simp: pw_le_iff refine_pw_simps)
lemma pw_algo_map_ref:
"pw_algo_map ≤ ⇓ (Id ×⇩r map_set_rel) pw_algo_unified"
unfolding pw_algo_map_def pw_algo_unified_def
apply refine_rcg
unfolding pw_map_inv_def list_mset_rel_def br_def map_set_rel_def by auto
end
context Worklist_Map2_Defs
begin
definition
"add_pw'_map2 passed wait a ≡
nfoldli (succs a) (λ(_, _, brk). ¬brk)
(λa (passed, wait, _).
do {
RETURN (
if empty a then
(passed, wait, False)
else if F' a then (passed, wait, True)
else
let k = key a; passed' = (case passed k of Some passed' ⇒ passed' | None ⇒ {})
in
if ∃ x ∈ passed'. a ⊴ x then
(passed, wait, False)
else
(passed(k ↦ (insert a passed')), a # wait, False)
)
}
)
(passed,wait,False)"
definition pw_algo_map2 where
"pw_algo_map2 = do
{
if F a⇩0 then RETURN (True, Map.empty)
else if empty a⇩0 then RETURN (False, Map.empty)
else do {
(passed, wait) ← RETURN ([key a⇩0 ↦ {a⇩0}], [a⇩0]);
(passed, wait, brk) ← WHILEIT pw_map_inv (λ (passed, wait, brk). ¬ brk ∧ wait ≠ [])
(λ (passed, wait, brk). do
{
(a, wait) ← take_from_list wait;
ASSERT (reachable a);
if empty a
then RETURN (passed, wait, brk)
else do {
TRACE (ExploredState); add_pw'_map2 passed wait a
}
}
)
(passed, wait, False);
RETURN (brk, passed)
}
}
"
end
context Worklist_Map2
begin
lemma add_pw'_map2_ref[refine]:
"add_pw'_map2 passed wait a ≤ ⇓ Id (add_pw'_map passed' wait' a')"
if "(passed, passed') ∈ Id" "(wait, wait') ∈ Id" "(a, a') ∈ Id"
using that
unfolding add_pw'_map2_def add_pw'_map_def
apply refine_rcg
apply refine_dref_type
by (auto simp: F_split)
lemma pw_algo_map2_ref[refine]:
"pw_algo_map2 ≤ ⇓ Id pw_algo_map"
unfolding pw_algo_map2_def pw_algo_map_def TRACE_bind
apply refine_rcg
apply refine_dref_type
by auto
end
lemma (in Worklist_Map2_finite) pw_algo_map2_correct:
"pw_algo_map2 ≤ SPEC (λ (brk, passed).
(brk ⟷ F_reachable) ∧
(¬ brk ⟶
(∃ p.
(passed, p) ∈ map_set_rel ∧ (∀a. reachable a ∧ ¬ empty a ⟶ (∃b∈p. a ≼ b))
∧ p ⊆ {a. reachable a ∧ ¬ empty a})
)
)"
proof -
note pw_algo_map2_ref
also note pw_algo_map_ref
also note pw_algo_unified_ref
also note pw_algo_correct
finally show ?thesis
unfolding conc_fun_def Image_def by (fastforce intro: Orderings.order.trans)
qed
end