Theory Unified_PW
section ‹Unified Passed-Waiting-List›
theory Unified_PW
imports Refine_Imperative_HOL.Sepref Worklist_Common Worklist_Algorithms_Subsumption_Graphs
begin
hide_const wait
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
subsection ‹Generalized Worklist Algorithm›
context Search_Space_Defs_Empty
begin
definition "reachable_subsumed S = {x' | x x'. reachable x' ∧ ¬ empty x' ∧ x' ≼ x ∧ x ∈ S}"
definition
"pw_var =
inv_image (
{(b, b'). b ∧ ¬ b'}
<*lex*>
{(passed', passed).
passed' ⊆ {a. reachable a ∧ ¬ empty a} ∧ passed ⊆ {a. reachable a ∧ ¬ empty a} ∧
reachable_subsumed passed ⊂ reachable_subsumed passed'}
<*lex*>
measure size
)
(λ (a, b, c). (c, a, b))
"
definition "pw_inv_frontier passed wait =
(∀ a ∈ passed. (∃ a' ∈ set_mset wait. a ≼ a') ∨
(∀ a'. E a a' ∧ ¬ empty a' ⟶ (∃ b' ∈ passed ∪ set_mset wait. a' ≼ b')))"
definition "start_subsumed passed wait = (¬ empty a⇩0 ⟶ (∃ a ∈ passed ∪ set_mset wait. a⇩0 ≼ a))"
definition "pw_inv ≡ λ (passed, wait, brk).
(brk ⟶ (∃ f. reachable f ∧ F f)) ∧
(¬ brk ⟶
passed ⊆ {a. reachable a ∧ ¬ empty a}
∧ pw_inv_frontier passed wait
∧ (∀ a ∈ passed ∪ set_mset wait. ¬ F a)
∧ start_subsumed passed wait
∧ set_mset wait ⊆ Collect reachable)
"
definition "add_pw_spec passed wait a ≡ SPEC (λ(passed',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. ∃ s' ∈ set_mset wait'. s ≼ s') ∧
(∀ s ∈ {a' . E a a' ∧ ¬ empty a'}. ∃ s' ∈ set_mset wait' ∪ passed. s ≼ s') ∧
(∀ s ∈ passed ∪ {a}. ∃ s' ∈ passed'. s ≼ s') ∧
(passed' ⊆ passed ∪ {a} ∪ {a' . E a a' ∧ ¬ empty a'} ∧
((∃ x ∈ passed'. ¬ (∃ x' ∈ passed. x ≼ x')) ∨ wait' ⊆# wait ∧ passed = passed')
)
)"
definition
"init_pw_spec ≡
SPEC (λ (passed, wait).
if empty a⇩0 then passed = {} ∧ wait ⊆# {#a⇩0#} else passed ⊆ {a⇩0} ∧ wait = {#a⇩0#})"
abbreviation subsumed_elem :: "'a ⇒ 'a set ⇒ bool"
where "subsumed_elem a M ≡ ∃ a'. a' ∈ M ∧ a ≼ a'"
notation
subsumed_elem ("(_/ ∈'' _)" [51, 51] 50)
definition "pw_inv_frontier' passed wait =
(∀ a. a ∈ passed ⟶
(a ∈' set_mset wait)
∨ (∀ a'. E a a' ∧ ¬ empty a' ⟶ (a' ∈' passed ∪ set_mset wait)))"
lemma pw_inv_frontier_frontier':
"pw_inv_frontier' passed wait" if
"pw_inv_frontier passed wait" "passed ⊆ Collect reachable"
using that unfolding pw_inv_frontier'_def pw_inv_frontier_def by (blast intro: trans)
lemma
"pw_inv_frontier passed wait" if "pw_inv_frontier' passed wait"
using that unfolding pw_inv_frontier_def pw_inv_frontier'_def by blast
definition pw_algo where
"pw_algo = do
{
if F a⇩0 then RETURN (True, {})
else if empty a⇩0 then RETURN (False, {})
else do {
(passed, wait) ← init_pw_spec;
(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_spec passed wait a
}
)
(passed, wait, False);
RETURN (brk, passed)
}
}
"
end
subsubsection ‹Correctness Proof›
instance nat :: preorder ..
context Search_Space_finite begin
lemma wf_worklist_var_aux:
"wf {(passed', passed).
passed' ⊆ {a. reachable a ∧ ¬ empty a} ∧ passed ⊆ {a. reachable a ∧ ¬ empty a} ∧
reachable_subsumed passed ⊂ reachable_subsumed passed'}"
proof (rule finite_acyclic_wf, goal_cases)
case 1
have "{(passed', passed).
passed' ⊆ {a. reachable a ∧ ¬ empty a} ∧ passed ⊆ {a. reachable a ∧ ¬ empty a} ∧
reachable_subsumed passed ⊂ reachable_subsumed passed'}
⊆ {(passed', passed).
passed ⊆ {a. reachable a ∧ ¬ empty a} ∧ passed' ⊆ {a. reachable a ∧ ¬ empty a}}"
unfolding reachable_subsumed_def by auto
moreover have "finite …" using finite_reachable using [[simproc add: finite_Collect]] by simp
ultimately show ?case by (rule finite_subset)
next
case 2
have *: "class.preorder (≤) ((<) :: nat ⇒ nat ⇒ bool)"
by (rule preorder_class.axioms)
show ?case
proof (rule preorder.acyclicI_order[where f = "λ a. card (reachable_subsumed a)"],
rule preorder_class.axioms, rule psubset_card_mono)
fix a
have "reachable_subsumed a ⊆ {a. reachable a ∧ ¬ empty a}"
unfolding reachable_subsumed_def by blast
then show "finite (reachable_subsumed a)" using finite_reachable by (rule finite_subset)
qed auto
qed
lemma wf_worklist_var:
"wf pw_var"
unfolding pw_var_def
by (auto 4 3 intro: wf_worklist_var_aux finite_acyclic_wf preorder.acyclicI_order[where f = id]
preorder_class.axioms)
context
begin
private lemma aux5:
assumes
"a' ∈ passed'"
"a ∈# wait"
"a ≼ a'"
"start_subsumed passed wait"
"∀s∈passed. ∃x∈passed'. s ≼ x"
"∀s∈#wait - {#a#}. Multiset.Bex wait' ((≼) s)"
shows "start_subsumed passed' wait'"
using assms unfolding start_subsumed_def apply clarsimp
by (metis Un_iff insert_DiffM2 local.trans mset_right_cancel_elem)
private lemma aux11:
assumes
"empty a"
"start_subsumed passed wait"
shows "start_subsumed passed (wait - {#a#})"
using assms unfolding start_subsumed_def
by auto (metis UnI2 diff_single_trivial empty_mono insert_DiffM insert_noteq_member)
lemma aux3_aux:
assumes "pw_inv_frontier' passed wait"
"¬ b ∈' set_mset wait"
"E b b'"
"¬ empty b" "¬ empty b'"
"b ∈' passed"
"reachable b" "passed ⊆ {a. reachable a ∧ ¬ empty a}"
shows "b' ∈' passed ∪ set_mset wait"
proof -
from ‹b ∈' _› obtain b1 where b1: "b ≼ b1" "b1 ∈ passed"
by blast
with mono[OF this(1) ‹E b b'›] ‹passed ⊆ _› ‹reachable b› ‹¬ empty b› obtain b1' where
"E b1 b1'" "b' ≼ b1'"
by auto
moreover then have "¬ empty b1'"
using assms(5) empty_mono by blast
moreover from assms b1 have "¬ b1 ∈' set_mset wait"
by (blast intro: trans)
ultimately show ?thesis
using assms(1) b1
unfolding pw_inv_frontier'_def
by (blast intro: trans)
qed
private lemma pw_inv_frontier_empty_elem:
assumes "pw_inv_frontier passed wait" "passed ⊆ {a. reachable a ∧ ¬ empty a}" "empty a"
shows "pw_inv_frontier passed (wait - {#a#})"
using assms unfolding pw_inv_frontier_def
by simp
(smt UnCI UnE diff_single_trivial empty_mono insert_DiffM2 mset_cancel_elem(1)
subset_Collect_conv)
private lemma aux3:
assumes
"set_mset wait ⊆ Collect reachable"
"a ∈# wait"
"∀ s ∈ set_mset (wait - {#a#}). ∃ s' ∈ set_mset wait'. s ≼ s'"
"∀ s ∈ {a'. E a a' ∧ ¬ empty a'}. ∃ s' ∈ passed ∪ set_mset wait'. s ≼ s'"
"∀ s ∈ passed ∪ {a}. ∃ s' ∈ passed'. s ≼ s'"
"passed' ⊆ passed ∪ {a} ∪ {a' . E a a' ∧ ¬ empty a}"
"pw_inv_frontier passed wait"
"passed ⊆ {a. reachable a ∧ ¬ empty a}"
shows "pw_inv_frontier passed' wait'"
proof -
from assms(1,2) have "reachable a"
by (simp add: subset_iff)
from assms have assms':
"set_mset wait ⊆ Collect reachable"
"a ∈# wait"
"∀ s. s ∈' set_mset (wait - {#a#}) ⟶ s ∈' set_mset wait'"
"∀ s ∈ {a'. E a a' ∧ ¬ empty a'}. s ∈' passed ∪ set_mset wait'"
"∀ s. s ∈' passed ∪ {a} ⟶ s ∈' passed'"
"passed' ⊆ passed ∪ {a} ∪ {a' . E a a'}"
"pw_inv_frontier' passed wait"
"passed ⊆ {a. reachable a ∧ ¬ empty a}"
by (blast intro: trans pw_inv_frontier_frontier')+
show ?thesis unfolding pw_inv_frontier_def
apply safe
unfolding Bex_def
subgoal for b b'
proof (goal_cases)
case A: 1
from A(1) assms(6) consider "b ∈ passed" | "a = b" | "E a b"
by auto
note cases = this
from cases ‹¬ b ∈' set_mset wait'› assms'(4) ‹reachable a› ‹passed ⊆ _› have "reachable b"
by cases (auto intro: reachable_step)
with A(3,4) have "¬ empty b" by (auto simp: empty_E)
from cases this ‹reachable b› consider "a = b" | "a ≠ b" "b ∈' passed" "reachable b"
using ‹¬ b ∈' set_mset wait'› assms'(4) by cases (fastforce intro: reachable_step)+
then consider "b ≼ a" "reachable b" | "¬ b ≼ a" "b ∈' passed" "reachable b"
using ‹¬ b ∈' set_mset wait'› assms'(4) ‹reachable a› by fastforce+
then show ?case
proof cases
case 1
with A(3,4) have "¬ empty b"
by (auto simp: empty_E)
with mono[OF 1(1) ‹E b b'› 1(2) ‹reachable a›] obtain b1' where
"E a b1'" "b' ≼ b1'"
by auto
with ‹¬ empty b'› have "b1' ∈' passed ∪ set_mset wait'"
using assms'(4) by (auto dest: empty_mono)
with ‹b' ≼ _› assms'(5) show ?thesis
by (auto intro: trans)
next
case 2
with A(3,4) have "¬ empty b"
by (auto simp: empty_E)
from 2 ‹¬ b ∈' set_mset wait'› assms'(2,3) have "¬ b ∈' set_mset wait"
by (metis insert_DiffM2 mset_right_cancel_elem)
from
aux3_aux[OF
assms'(7) this ‹E b b'› ‹¬ empty b› ‹¬ empty b'› ‹b ∈' passed› ‹reachable b› assms'(8)
]
have "b' ∈' passed ∪ set_mset wait" .
with assms'(2,3,5) show ?thesis
by auto (metis insert_DiffM insert_noteq_member)
qed
qed
done
qed
private lemma aux6:
assumes
"a ∈# wait"
"start_subsumed passed wait"
"∀ s ∈ set_mset (wait - {#a#}) ∪ {a'. E a a' ∧ ¬ empty a'}. ∃ s' ∈ set_mset wait'. s ≼ s'"
shows "start_subsumed (insert a passed) wait'"
using assms unfolding 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 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)+
lemma aux4:
assumes "pw_inv_frontier passed {#}" "reachable x" "start_subsumed passed {#}"
"passed ⊆ {a. reachable a ∧ ¬ empty a}" "¬ empty x"
shows "∃ x' ∈ passed. x ≼ x'"
proof -
from ‹reachable x› have "E⇧*⇧* a⇩0 x" by (simp add: reachable_def)
have "¬ empty a⇩0" using ‹E⇧*⇧* a⇩0 x› assms(5) empty_E_star by blast
with assms(3) obtain b where "a⇩0 ≼ b" "b ∈ passed" unfolding 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 pw_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 intro: reachable_step)
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
lemmas [intro] = reachable_step
private lemma aux7:
assumes
"a ∈# wait"
"set_mset wait ⊆ Collect reachable"
"set_mset wait' ⊆ set_mset (wait - {#a#}) ∪ Collect (E a)"
"x ∈# wait'"
shows "reachable x"
using assms by (auto dest: in_diffD)
private lemma aux8:
"x ∈ reachable_subsumed S'" if "x ∈ reachable_subsumed S" "∀s∈S. ∃x∈S'. s ≼ x"
using that unfolding reachable_subsumed_def by (auto intro: trans)
private lemma aux9:
assumes
"set_mset wait' ⊆ set_mset (wait - {#a#}) ∪ Collect (E a)"
"x ∈# wait'" "∀a'. E a a' ⟶ ¬ F a'" "F x"
"∀a∈passed ∪ set_mset wait. ¬ F a"
shows False
proof -
from assms(1,2) have "x ∈ set_mset wait ∨ x ∈ Collect (E a)"
by (meson UnE in_diffD subsetCE)
with assms(3,4,5) show ?thesis
by auto
qed
private lemma aux10:
assumes "∀a∈passed' ∪ set_mset wait. ¬ F a" "F x" "x ∈# wait - {#a#}"
shows "False"
by (meson UnI2 assms in_diffD)
lemma aux12:
"size wait' < size wait" if "wait' ⊆# wait - {#a#}" "a ∈# wait"
using that
by (metis
Diff_eq_empty_iff_mset add_diff_cancel_left' add_mset_add_single add_mset_not_empty
insert_subset_eq_iff mset_le_add_mset_decr_left1 mset_subset_size subset_mset_def)
lemma aux13:
assumes
"passed ⊆ {a. reachable a ∧ ¬ empty a}"
"passed' ⊆ insert a (passed ∪ {a'. E a a' ∧ ¬ empty a'})"
"¬ empty a"
"reachable a"
"∀s∈passed. ∃x∈passed'. s ≼ x"
"a'' ∈ passed'"
"∀x∈passed. ¬ a'' ≼ x"
shows
"passed' ⊆ {a. reachable a ∧ ¬ empty a} ∧ reachable_subsumed passed ⊂ reachable_subsumed passed'
∨ passed' = passed ∧ size wait'' < size wait"
proof -
have "passed' ⊆ {a. reachable a ∧ ¬ empty a}"
using ‹passed ⊆ _› ‹passed' ⊆ _› ‹¬ empty a› ‹reachable a› by auto
moreover have "reachable_subsumed passed ⊂ reachable_subsumed passed'"
unfolding reachable_subsumed_def
using ‹∀s∈passed. ∃x∈passed'. s ≼ x› assms(5-) ‹passed' ⊆ {a. reachable a ∧ ¬ empty a}›
by (auto 4 3 intro: trans)
ultimately show ?thesis
using ‹passed ⊆ _› unfolding pw_var_def by auto
qed
method solve_vc =
rule aux3 aux5 aux7 aux10 aux11 pw_inv_frontier_empty_elem; assumption; fail |
rule aux3; auto; fail | auto intro: aux9; fail | auto dest: in_diffD; fail
end
end
theorem (in Search_Space'_finite) pw_algo_correct:
"pw_algo ≤ SPEC (λ (brk, passed).
(brk ⟷ F_reachable)
∧ (¬ brk ⟶
(∀ a. reachable a ∧ ¬ empty a ⟶ (∃ b ∈ passed. a ≼ b))
∧ passed ⊆ {a. reachable a ∧ ¬ empty a})
)"
proof -
note [simp] = size_Diff_submset pred_not_lt_is_zero
note [dest] = set_mset_mp
show ?thesis
unfolding pw_algo_def init_pw_spec_def add_pw_spec_def F_reachable_def
apply (refine_vcg wf_worklist_var)
apply (solves auto)
subgoal
using empty_E_star final_non_empty unfolding reachable_def by auto
subgoal
using empty_E_star final_non_empty unfolding reachable_def by auto
subgoal
using empty_E_star final_non_empty unfolding reachable_def by auto
subgoal
using empty_E_star final_non_empty unfolding reachable_def by auto
subgoal
using empty_E_star final_non_empty unfolding reachable_def by auto
apply (fastforce simp: pw_inv_def pw_inv_frontier_def start_subsumed_def
split: if_split_asm dest: mset_subset_eqD)
apply (simp; fail)
apply (solves ‹auto simp: pw_inv_def›)
subgoal for _ passed wait _ passed' _ _ brk _ a wait'
by (clarsimp simp: pw_inv_def split: if_split_asm; safe; solve_vc)
apply (clarsimp simp: pw_var_def nonempty_has_size; fail)
subgoal for _ passed wait _ passed' _ _ brk _ a wait'
by (clarsimp simp: pw_inv_def split: if_split_asm; safe; solve_vc)
subgoal for _ _ _ _ passed _ wait brk _ a wait'
by (clarsimp simp: pw_inv_def split: if_split_asm; safe)
(simp_all add: aux12 aux13 pw_var_def)
using F_mono by (fastforce simp: pw_inv_def dest!: aux4 dest: final_non_empty)+
qed
lemmas (in Search_Space'_finite) [refine_vcg] = pw_algo_correct[THEN Orderings.order.trans]
end