Theory Worklist_Subsumption1
theory Worklist_Subsumption1
imports Worklist_Subsumption_Multiset
begin
subsection ‹From Multisets to Lists›
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 Search_Space_Defs_Empty
begin
definition "worklist_inv_frontier_list passed wait =
(∀ a ∈ passed. ∀ a'. E a a' ∧ ¬ empty a' ⟶ (∃ b' ∈ passed ∪ set wait. a' ≼ b'))"
definition "start_subsumed_list passed wait = (∃ a ∈ passed ∪ set wait. a⇩0 ≼ a)"
definition "worklist_inv_list ≡ λ (passed, wait, brk).
passed ⊆ Collect reachable ∧
(brk ⟶ (∃ f. reachable f ∧ F f)) ∧
(¬ brk ⟶
worklist_inv_frontier_list passed wait
∧ (∀ a ∈ passed ∪ set wait. ¬ F a)
∧ start_subsumed_list passed wait
∧ set wait ⊆ Collect reachable)
∧ (∀ a ∈ passed. ¬ empty a) ∧ (∀ a ∈ set wait. ¬ empty a)
"
definition "add_succ_spec_list wait a ≡ SPEC (λ(wait',brk).
(
if ∃a'. E a a' ∧ F a' then
brk
else
¬brk ∧ set wait' ⊆ set wait ∪ {a' . E a a'} ∧
(∀ s ∈ set wait ∪ {a' . E a a' ∧ ¬ empty a'}. ∃ s' ∈ set wait'. s ≼ s')
) ∧ (∀ s ∈ set wait'. ¬ empty s)
)"
end
context Search_Space''_Defs
begin
definition worklist_algo_list where
"worklist_algo_list = do
{
if F a⇩0 then RETURN True
else do {
let passed = {};
let wait = [a⇩0];
(passed, wait, brk) ← WHILEIT worklist_inv_list (λ (passed, wait, brk). ¬ brk ∧ wait ≠ [])
(λ (passed, wait, brk). do
{
(a, wait) ← take_from_list wait;
ASSERT (reachable a);
if (∃ a' ∈ passed. a ⊴ a') then RETURN (passed, wait, brk) else
do
{
(wait,brk) ← add_succ_spec_list wait a;
let passed = insert a passed;
RETURN (passed, wait, brk)
}
}
)
(passed, wait, False);
RETURN brk
}
}
"
end
context Search_Space''_pre
begin
lemma worklist_algo_list_inv_ref:
fixes x x'
assumes
"¬ F a⇩0" "¬ F a⇩0"
"(x, x') ∈ {((passed,wait,brk), (passed',wait',brk')). passed = passed' ∧ mset wait = wait' ∧ brk = brk' }"
"worklist_inv' x'"
shows "worklist_inv_list x"
using assms
unfolding worklist_inv'_def worklist_inv_def worklist_inv_list_def
unfolding worklist_inv_frontier_def worklist_inv_frontier_list_def
unfolding worklist_start_subsumed_def start_subsumed_list_def
by auto
lemma take_from_list_take_from_mset_ref[refine]:
"take_from_list xs ≤ ⇓ {((x, xs),(y, m)). x = y ∧ mset xs = m} (take_from_mset m)"
if "mset xs = m"
using that unfolding take_from_list_def take_from_mset_def
by (clarsimp simp: pw_le_iff refine_pw_simps)
lemma add_succ_spec_list_add_succ_spec_ref[refine]:
"add_succ_spec_list xs b ≤ ⇓ {((xs, b), (m, b')). mset xs = m ∧ b = b'} (add_succ_spec' m b')"
if "mset xs = m" "b = b'"
using that unfolding add_succ_spec_list_def add_succ_spec'_def
by (clarsimp simp: pw_le_iff refine_pw_simps)
lemma worklist_algo_list_ref[refine]: "worklist_algo_list ≤ ⇓Id worklist_algo'"
unfolding worklist_algo_list_def worklist_algo'_def
apply (refine_rcg)
apply blast
prefer 2
apply (rule worklist_algo_list_inv_ref; assumption)
by auto
end
subsection ‹Towards an Implementation›
context Worklist1_Defs
begin
definition
"add_succ1 wait a ≡
nfoldli (succs a) (λ(_,brk). ¬brk)
(λa (wait,brk).
do {
ASSERT (∀ x ∈ set wait. ¬ empty x);
if F a then RETURN (wait,True) else RETURN (
if (∃ x ∈ set wait. a ≼ x ∧ ¬ x ≼ a) ∨ empty a
then [x ← wait. ¬ x ≼ a]
else a # [x ← wait. ¬ x ≼ a],False)
}
)
(wait,False)"
end
context Worklist2_Defs
begin
definition
"add_succ1' wait a ≡
nfoldli (succs a) (λ(_,brk). ¬brk)
(λa (wait,brk).
if F a then RETURN (wait,True) else RETURN (
if empty a
then wait
else if ∃ x ∈ set wait. a ⊴ x ∧ ¬ x ⊴ a
then [x ← wait. ¬ x ⊴ a]
else a # [x ← wait. ¬ x ⊴ a],False)
)
(wait,False)"
end
context Worklist1
begin
lemma add_succ1_ref[refine]:
"add_succ1 wait a ≤ ⇓(Id ×⇩r bool_rel) (add_succ_spec_list wait' a')"
if "(wait,wait')∈Id" "(a,a')∈b_rel Id reachable" "∀ x ∈ set wait'. ¬ empty x"
using that
apply simp
unfolding add_succ_spec_list_def add_succ1_def
apply (refine_vcg nfoldli_rule[where I =
"λl1 _ (wait',brk).
(if brk then ∃a'. E a a' ∧ F a'
else set wait' ⊆ set wait ∪ set l1 ∧ set l1 ∩ Collect F = {}
∧ (∀ x ∈ set wait ∪ set l1. ¬ empty x ⟶ (∃ x' ∈ set wait'. x ≼ x')))
∧ (∀ x ∈ set wait'. ¬ empty x)"]
)
apply (solves auto)
apply (solves auto)
using succs_correct[of a] apply (solves auto)
using succs_correct[of a] apply (solves auto)
apply (solves auto)
subgoal
apply (clarsimp split: if_split_asm; intro conjI)
apply blast
apply blast
apply (meson empty_mono local.trans)
apply blast
apply (meson empty_mono local.trans)
done
using succs_correct[of a] apply (solves auto)+
done
end
context Worklist2
begin
lemma add_succ1'_ref[refine]:
"add_succ1' wait a ≤ ⇓(Id ×⇩r bool_rel) (add_succ1 wait' a')"
if "(wait,wait')∈Id" "(a,a')∈b_rel Id reachable" "∀ x ∈ set wait'. ¬ empty x"
unfolding add_succ1'_def add_succ1_def
using that
apply (refine_vcg nfoldli_refine)
apply refine_dref_type
apply (solves ‹auto simp: empty_subsumes' cong: filter_cong›)+
apply (simp add: empty_subsumes' cong: filter_cong)
by (metis empty_mono empty_subsumes' filter_True)
lemma add_succ1'_ref'[refine]:
"add_succ1' wait a ≤ ⇓(Id ×⇩r bool_rel) (add_succ_spec_list wait' a')"
if "(wait,wait')∈Id" "(a,a')∈b_rel Id reachable" "∀ x ∈ set wait'. ¬ empty x"
using that
proof -
note add_succ1'_ref
also note add_succ1_ref
finally show ?thesis
using that by - auto
qed
definition worklist_algo1' where
"worklist_algo1' = do
{
if F a⇩0 then RETURN True
else do {
let passed = {};
let wait = [a⇩0];
(passed, wait, brk) ← WHILEIT worklist_inv_list (λ (passed, wait, brk). ¬ brk ∧ wait ≠ [])
(λ (passed, wait, brk). do
{
(a, wait) ← take_from_list wait;
if (∃ a' ∈ passed. a ⊴ a') then RETURN (passed, wait, brk) else
do
{
(wait,brk) ← add_succ1' wait a;
let passed = insert a passed;
RETURN (passed, wait, brk)
}
}
)
(passed, wait, False);
RETURN brk
}
}
"
lemma take_from_list_ref[refine]:
"take_from_list wait ≤
⇓ {((x, wait), (y, wait')). x = y ∧ wait = wait' ∧ ¬ empty x ∧ (∀ a ∈ set wait. ¬ empty a)}
(take_from_list wait')"
if "wait = wait'" "∀ a ∈ set wait. ¬ empty a" "wait ≠ []"
using that
by (auto 4 4 simp: pw_le_iff refine_pw_simps dest!: take_from_list_correct)
lemma worklist_algo1_list_ref[refine]: "worklist_algo1' ≤ ⇓Id worklist_algo_list"
unfolding worklist_algo1'_def worklist_algo_list_def
apply (refine_rcg)
apply refine_dref_type
unfolding worklist_inv_list_def
by auto
definition worklist_algo1 where
"worklist_algo1 ≡ if empty a⇩0 then RETURN False else worklist_algo1'"
lemma worklist_algo1_ref[refine]: "worklist_algo1 ≤ ⇓Id worklist_algo''"
proof -
have "worklist_algo1' ≤ worklist_algo'" if "¬ empty a⇩0"
proof -
note worklist_algo1_list_ref
also note worklist_algo_list_ref
finally show "worklist_algo1' ≤ worklist_algo'"
by simp
qed
then show ?thesis
unfolding worklist_algo1_def worklist_algo''_def by simp
qed
end
context Worklist3_Defs
begin
definition
"add_succ2 wait a ≡
nfoldli (succs a) (λ(_,brk). ¬brk)
(λa (wait,brk).
if empty a then RETURN (wait, False)
else if F' a then RETURN (wait,True)
else RETURN (
if ∃ x ∈ set wait. a ⊴ x ∧ ¬ x ⊴ a
then [x ← wait. ¬ x ⊴ a]
else a # [x ← wait. ¬ x ⊴ a],False)
)
(wait,False)"
definition
"filter_insert_wait wait a ≡
if ∃ x ∈ set wait. a ⊴ x ∧ ¬ x ⊴ a
then [x ← wait. ¬ x ⊴ a]
else a # [x ← wait. ¬ x ⊴ a]"
end
context Worklist3
begin
lemma filter_insert_wait_alt_def:
"filter_insert_wait wait a = (
let
(f, xs) =
fold (λ x (f, xs). if x ⊴ a then (f, xs) else (f ∨ a ⊴ x, x # xs)) wait (False, [])
in
if f then rev xs else a # rev xs
)
"
proof -
have
"fold (λ x (f, xs). if x ⊴ a then (f, xs) else (f ∨ a ⊴ x, x # xs)) wait (f, xs)
= (f ∨ (∃ x ∈ set wait. a ⊴ x ∧ ¬ x ⊴ a), rev [x ← wait. ¬ x ⊴ a] @ xs)" for f xs
by (induction wait arbitrary: f xs; simp)
then show ?thesis unfolding filter_insert_wait_def by auto
qed
lemma add_succ2_alt_def:
"add_succ2 wait a ≡
nfoldli (succs a) (λ(_,brk). ¬brk)
(λa (wait,brk).
if empty a then RETURN (wait, False)
else if F' a then RETURN (wait, True)
else RETURN (filter_insert_wait wait a, False)
)
(wait,False)"
unfolding add_succ2_def filter_insert_wait_def by (intro HOL.eq_reflection HOL.refl)
lemma add_succ2_ref[refine]:
"add_succ2 wait a ≤ ⇓(Id ×⇩r bool_rel) (add_succ1' wait' a')"
if "(wait,wait')∈Id" "(a,a')∈Id"
unfolding add_succ2_def add_succ1'_def
apply (rule nfoldli_refine)
apply refine_dref_type
using that by (auto simp: F_split)
definition worklist_algo2' where
"worklist_algo2' = do
{
if F' a⇩0 then RETURN True
else do {
let passed = {};
let wait = [a⇩0];
(passed, wait, brk) ← WHILEIT worklist_inv_list (λ (passed, wait, brk). ¬ brk ∧ wait ≠ [])
(λ (passed, wait, brk). do
{
(a, wait) ← take_from_list wait;
if (∃ a' ∈ passed. a ⊴ a') then RETURN (passed, wait, brk) else
do
{
(wait,brk) ← add_succ2 wait a;
let passed = insert a passed;
RETURN (passed, wait, brk)
}
}
)
(passed, wait, False);
RETURN brk
}
}
"
lemma worklist_algo2'_ref[refine]: "worklist_algo2' ≤ ⇓Id worklist_algo1'" if "¬ empty a⇩0"
unfolding worklist_algo2'_def worklist_algo1'_def
using that
supply take_from_list_ref [refine del]
apply refine_rcg
apply refine_dref_type
by (auto simp: F_split)
definition worklist_algo2 where
"worklist_algo2 ≡ if empty a⇩0 then RETURN False else worklist_algo2'"
lemma worklist_algo2_ref[refine]: "worklist_algo2 ≤ ⇓Id worklist_algo''"
proof -
have "worklist_algo2 ≤ ⇓Id worklist_algo1"
unfolding worklist_algo2_def worklist_algo1_def
by refine_rcg standard
also note worklist_algo1_ref
finally show ?thesis .
qed
end
end