Theory Worklist_Subsumption_Impl1
theory Worklist_Subsumption_Impl1
imports Refine_Imperative_HOL.IICF Worklist_Subsumption1
begin
subsection ‹Implementation on Lists›
lemma list_filter_foldli:
"[x ← xs. P x] = rev (foldli xs (λ x. True) (λ x xs. if P x then x # xs else xs) [])"
(is "_ = rev (foldli xs ?c ?f [])")
proof -
have *:
"rev (foldli xs ?c ?f (ys @ zs)) = rev zs @ rev (foldli xs ?c ?f ys)" for xs ys zs
proof (induction xs arbitrary: ys)
case Nil
then show ?case by simp
next
case (Cons x xs)
from Cons[of "x # ys"] Cons[of ys] show ?case by simp
qed
show ?thesis
apply (induction xs)
apply (simp; fail)
apply simp
apply (subst (2) *[of _ "[]", simplified])
by simp
qed
context notes [split!] = list.split begin
sepref_decl_op list_hdtl: "λ (x # xs) ⇒ (x, xs)" :: "[λl. l≠[]]⇩f ⟨A⟩list_rel → A ×⇩r ⟨A⟩list_rel"
by auto
end
context Worklist4_Impl
begin
sepref_register "PR_CONST a⇩0" "PR_CONST F'" "PR_CONST (⊴)" "PR_CONST succs" "PR_CONST empty"
lemma [def_pat_rules]:
"a⇩0 ≡ UNPROTECT a⇩0" "F' ≡ UNPROTECT F'" "(⊴) ≡ UNPROTECT (⊴)" "succs ≡ UNPROTECT succs"
"empty ≡ UNPROTECT empty"
by simp_all
lemma take_from_list_alt_def:
"take_from_list xs = do {_ ← ASSERT (xs ≠ []); RETURN (hd_tl xs)}"
unfolding take_from_list_def by (auto simp: pw_eq_iff refine_pw_simps)
lemma [safe_constraint_rules]: "CN_FALSE is_pure A ⟹ is_pure A" by simp
sepref_thm filter_insert_wait_impl is
"uncurry (RETURN oo PR_CONST filter_insert_wait)" :: "(list_assn A)⇧d *⇩a A⇧d →⇩a list_assn A"
unfolding filter_insert_wait_alt_def list_ex_foldli list_filter_foldli
unfolding HOL_list.fold_custom_empty
unfolding PR_CONST_def
by sepref
concrete_definition (in -) filter_insert_wait_impl
uses Worklist4_Impl.filter_insert_wait_impl.refine_raw is "(uncurry ?f, _) ∈ _"
lemmas [sepref_fr_rules] = filter_insert_wait_impl.refine[OF Worklist4_Impl_axioms]
sepref_register filter_insert_wait
lemmas [sepref_fr_rules] = hd_tl_hnr
sepref_thm worklist_algo2_impl is "uncurry0 worklist_algo2" :: "unit_assn⇧k →⇩a bool_assn"
unfolding worklist_algo2_def worklist_algo2'_def add_succ2_alt_def PR_CONST_def
supply [[goals_limit = 1]]
supply conv_to_is_Nil[simp]
apply (rewrite in "Let ⌑ _" lso_fold_custom_empty)
unfolding fold_lso_bex
unfolding take_from_list_alt_def
apply (rewrite in "[a⇩0]" HOL_list.fold_custom_empty)
by sepref
concrete_definition (in -) worklist_algo2_impl
for Lei a⇩0i Fi succsi emptyi
uses Worklist4_Impl.worklist_algo2_impl.refine_raw is "(uncurry0 ?f,_)∈_"
end
context Worklist4_Impl_finite_strict
begin
lemma worklist_algo2_impl_hnr_F_reachable:
"(uncurry0 (worklist_algo2_impl Lei a⇩0i Fi succsi emptyi), uncurry0 (RETURN F_reachable))
∈ unit_assn⇧k →⇩a bool_assn"
using worklist_algo2_impl.refine[OF Worklist4_Impl_axioms,
FCOMP worklist_algo2_ref[THEN nres_relI],
FCOMP worklist_algo''_correct[THEN Id_SPEC_refine, THEN nres_relI]]
by (simp add: RETURN_def)
sepref_decl_op F_reachable :: "bool_rel" .
lemma [def_pat_rules]: "F_reachable ≡ op_F_reachable" by simp
lemma hnr_op_F_reachable:
assumes "GEN_ALGO a⇩0i (λa⇩0i. (uncurry0 a⇩0i, uncurry0 (RETURN a⇩0)) ∈ unit_assn⇧k →⇩a A)"
assumes "GEN_ALGO Fi (λFi. (Fi,RETURN o F') ∈ A⇧k →⇩a bool_assn)"
assumes "GEN_ALGO Lei (λLei. (uncurry Lei,uncurry (RETURN oo (⊴))) ∈ A⇧k *⇩a A⇧k →⇩a bool_assn)"
assumes "GEN_ALGO succsi (λsuccsi. (succsi,RETURN o succs) ∈ A⇧k →⇩a list_assn A)"
assumes "GEN_ALGO emptyi (λFi. (Fi,RETURN o empty) ∈ A⇧k →⇩a bool_assn)"
shows
"(uncurry0 (worklist_algo2_impl Lei a⇩0i Fi succsi emptyi), uncurry0 (RETURN (PR_CONST op_F_reachable)))
∈ unit_assn⇧k →⇩a bool_assn"
proof -
from assms interpret Worklist4_Impl E a⇩0 F "(≼)" succs empty "(⊴)" F' A succsi a⇩0i Fi Lei emptyi
by (unfold_locales; simp add: GEN_ALGO_def)
from worklist_algo2_impl_hnr_F_reachable show ?thesis by simp
qed
sepref_decl_impl hnr_op_F_reachable .
end
end