Theory Unreachability_Certification2
theory Unreachability_Certification2
imports
Unreachability_Misc
Munta_Base.Abstract_Term
"HOL-Library.Parallel"
begin
hide_const (open) list_set_rel
lemma monadic_list_all_mono:
"monadic_list_all P xs ≤ monadic_list_all Q ys" if "list_all2 (λ x y. P x ≤ Q y) xs ys"
proof -
have "nfoldli xs id (λx _. P x) a ≤ nfoldli ys id (λx _. Q x) a" for a
using that by (induction xs ys arbitrary: a; clarsimp; refine_mono)
then show ?thesis
unfolding monadic_list_all_def .
qed
lemma monadic_list_all_mono':
"monadic_list_all P xs ≤ monadic_list_all Q ys"
if "(xs, ys) ∈ ⟨R⟩list_rel" "⋀ x y. (x, y) ∈ R ⟹ P x ≤ Q y"
using that by (intro monadic_list_all_mono) (auto simp: list_all2_iff list_rel_def)
lemma monadic_list_ex_mono:
"monadic_list_ex P xs ≤ monadic_list_ex Q ys" if "list_all2 (λ x y. P x ≤ Q y) xs ys"
proof -
have "nfoldli xs Not (λx _. P x) a ≤ nfoldli ys Not (λx _. Q x) a" for a
using that by (induction xs ys arbitrary: a; clarsimp; refine_mono)
then show ?thesis
unfolding monadic_list_ex_def .
qed
lemma monadic_list_ex_mono':
"monadic_list_ex P xs ≤ monadic_list_ex Q ys"
if "(xs, ys) ∈ ⟨R⟩list_rel" "⋀ x y. (x, y) ∈ R ⟹ P x ≤ Q y"
using that by (intro monadic_list_ex_mono) (auto simp: list_all2_iff list_rel_def)
lemma monadic_list_all_rule':
assumes "⋀x. x ∈ set xs ⟹ Pi x ≤ SPEC (λr. r ⟷ P x)"
shows "monadic_list_all Pi xs ≤ SPEC (λr. r ⟷ list_all P xs)"
using assms unfolding monadic_list_all_def
by (intro nfoldli_rule[where I = "λas bs b. b = list_all P as ∧ set (as @ bs) = set xs"]) auto
lemma case_prod_mono:
"(case x of (a, b) ⇒ f a b) ≤ (case y of (a, b) ⇒ g a b)"
if "(x, y) ∈ K ×⇩r A" "⋀ai bi a b. (ai, a) ∈ K ⟹ (bi, b) ∈ A ⟹ f ai bi ≤ g a b" for x y f g
using that unfolding prod_rel_def by auto
definition list_set_rel where [to_relAPP]:
"list_set_rel R ≡ ⟨R⟩list_rel O {(xs, S). set xs = S}"
lemma list_set_relE:
assumes "(xs, zs) ∈ ⟨R⟩list_set_rel"
obtains ys where "(xs, ys) ∈ ⟨R⟩list_rel" "set ys = zs"
using assms unfolding list_set_rel_def by auto
lemma list_set_rel_Nil[simp, intro]:
"([], {}) ∈ ⟨Id⟩list_set_rel"
unfolding list_set_rel_def by auto
lemma specify_right:
"c ≤ SPEC P ⤜ c'" if "P x" "c ≤ c' x"
using that by (auto intro: SUP_upper2[where i = x] simp: bind_RES)
lemma res_right:
"c ≤ RES S ⤜ c'" if "x ∈ S" "c ≤ c' x"
using that by (auto intro: SUP_upper2[where i = x] simp: bind_RES)
lemma nres_relD:
"c ≤ ⇓R a" if "(c, a) ∈ ⟨R⟩nres_rel"
using that unfolding nres_rel_def by simp
lemma list_rel_setE1:
assumes "x ∈ set xs" "(xs, ys) ∈ ⟨R⟩list_rel"
obtains y where "y ∈ set ys" "(x, y) ∈ R"
using assms unfolding list_rel_def by (auto dest!: list_all2_set1)
lemma list_rel_setE2:
assumes "y ∈ set ys" "(xs, ys) ∈ ⟨R⟩list_rel"
obtains x where "x ∈ set xs" "(x, y) ∈ R"
using assms unfolding list_rel_def by (auto dest!: list_all2_set2)
lemma list_of_set_impl[autoref_rules]:
"(λxs. RETURN xs, list_of_set) ∈ ⟨R⟩list_set_rel → ⟨⟨R⟩list_rel⟩nres_rel"
unfolding list_of_set_def by refine_rcg (auto elim!: list_set_relE intro: RETURN_SPEC_refine)
lemma case_option_mono:
"(case x of None ⇒ a | Some x' ⇒ f x', case y of None ⇒ b | Some x' ⇒ g x') ∈ R"
if "(x, y) ∈ ⟨S⟩option_rel" "(a, b) ∈ R" "(f, g) ∈ S → R"
by (metis fun_relD2 param_case_option' that)
lemmas case_option_mono' =
case_option_mono[where R = "⟨R⟩nres_rel" for R, THEN nres_relD, THEN refine_IdD]
lemma bind_mono:
assumes "m ≤ ⇓ R m'"
and "⋀x y. (x, y) ∈ R ⟹ f x ≤ f' y"
shows "Refine_Basic.bind m f ≤ m' ⤜ f'"
using assms by (force simp: refine_pw_simps pw_le_iff)
lemma list_all_split:
assumes "set xs = (⋃xs ∈ set split. set xs)"
shows "list_all P xs = list_all id (map (list_all P) split)"
unfolding list_all_iff using assms by auto
lemma list_all_default_split:
"list_all P xs = list_all id (map P xs)"
unfolding list_all_iff by auto
locale Reachability_Impl_pure_base =
Reachability_Impl_base where less_eq = less_eq
for less_eq :: "'a ⇒ 'a ⇒ bool" (infix "≼" 50) +
fixes get_succs and K and A and L and Li and lei
and Li_split :: "'ki list list"
assumes K_right_unique: "single_valued K"
assumes K_left_unique: "single_valued (K¯)"
assumes Li_L: "(Li, L) ∈ ⟨K⟩list_set_rel"
assumes lei_less_eq: "(lei, less_eq) ∈ A → A → bool_rel"
assumes get_succs_succs[param]:
"(get_succs, succs) ∈ K → ⟨A⟩list_set_rel → ⟨K ×⇩r ⟨A⟩list_set_rel⟩list_rel"
assumes full_split: "set Li = (⋃xs ∈ set Li_split. set xs)"
begin
lemma lei_refine[refine_mono]:
‹RETURN (lei a b) ≤ RETURN (a' ≼ b')› if ‹(a, a') ∈ A› ‹(b, b') ∈ A›
using that using lei_less_eq by simp (metis pair_in_Id_conv tagged_fun_relD_both)
definition list_all_split :: "_ ⇒ 'ki list ⇒ bool" where [simp]:
"list_all_split = list_all"
definition monadic_list_all_split :: "_ ⇒ 'ki list ⇒ bool nres" where [simp]:
"monadic_list_all_split = monadic_list_all"
lemmas pure_unfolds =
monadic_list_all_RETURN[where 'a = 'ki, folded monadic_list_all_split_def list_all_split_def]
monadic_list_ex_RETURN monadic_list_all_RETURN monadic_list_ex_RETURN
nres_monad1 option.case_distrib[where h = RETURN, symmetric]
if_distrib[where f = RETURN, symmetric] prod.case_distrib[where h = RETURN, symmetric]
lemma list_all_split:
"list_all_split Q Li = list_all id (Parallel.map (list_all Q) Li_split)"
unfolding list_all_split_def list_all_split[OF full_split, symmetric] Parallel.map_def ..
end
locale Reachability_Impl_pure_invariant =
Reachability_Impl_invariant where M = M +
Reachability_Impl_pure_base where Li_split = Li_split
for M :: "'k ⇒ 'a set" and Li_split :: "'ki list list"
locale Reachability_Impl_pure_base2 =
Reachability_Impl_pure_base where less_eq = less_eq and Li_split = Li_split +
Reachability_Impl_base2 where less_eq = less_eq
for less_eq :: "'a ⇒ 'a ⇒ bool" (infix "≼" 50) and Li_split :: "'ki list list" +
fixes Pi and Fi
assumes Pi_P'[refine,param]: "(Pi, P') ∈ K ×⇩r A → bool_rel"
assumes Fi_F[refine]: "(Fi, F) ∈ K ×⇩r A → bool_rel"
locale Reachability_Impl_pure =
Reachability_Impl_common where M = M +
Reachability_Impl_pure_base2 +
Reachability_Impl_pre_start where M = "λx. case M x of None ⇒ {} | Some S ⇒ S"
for M :: "'k ⇒ 'a set option" +
fixes Mi l⇩0i s⇩0i
assumes Mi_M[param]: "(Mi, M) ∈ K → ⟨⟨A⟩list_set_rel⟩option_rel"
assumes l⇩0i_l⇩0[refine,param]: "(l⇩0i, l⇩0) ∈ K"
and s⇩0i_s⇩0[refine,param,refine_mono]: "(s⇩0i, s⇩0) ∈ A"
begin
paragraph ‹Refinement›
definition "check_invariant1 L' ≡
do {
monadic_list_all_split (λl.
case Mi l of
None ⇒ RETURN True
| Some as ⇒ do {
let succs = get_succs l as;
monadic_list_all (λ(l', xs).
do {
if xs = [] then RETURN True
else do {
case Mi l' of
None ⇒ RETURN False
| Some ys ⇒ monadic_list_all (λx.
monadic_list_ex (λy. RETURN (lei x y)) ys
) xs
}
}
) succs
}
) L'
}
"
lemma Mi_M_None_iff[simp]:
"M l = None ⟷ Mi li = None" if "(li, l) ∈ K"
proof -
from that have "(Mi li, M l) ∈ ⟨⟨A⟩list_set_rel⟩option_rel"
by parametricity
then show ?thesis
by auto
qed
lemma check_invariant1_refine[refine]:
"check_invariant1 L1 ≤ check_invariant L'"
if "(L1, L') ∈ ⟨K⟩list_rel" "L = dom M" "set L' ⊆ L"
unfolding check_invariant1_def check_invariant_def Let_def monadic_list_all_split_def
apply (refine_rcg monadic_list_all_mono' refine_IdI that)
apply (clarsimp split: option.splits simp: succs_empty; safe)
apply (simp flip: Mi_M_None_iff; fail)
apply (refine_rcg monadic_list_all_mono')
apply parametricity
subgoal
using Mi_M by (auto dest!: fun_relD1)
apply (clarsimp split: option.splits; safe)
apply (solves ‹
elim list_set_relE specify_right;
auto simp: monadic_list_all_False intro!: res_right simp flip: Mi_M_None_iff›)+
subgoal premises prems for _ _ _ _ li _ l _ S xsi
proof -
have *: ‹li ∈ set Li ⟷ l ∈ L› if ‹(li, l) ∈ K›
using that using Li_L K_left_unique K_right_unique
by (auto dest: single_valuedD elim: list_rel_setE1 list_rel_setE2 elim!: list_set_relE)
have [simp]: "l ∈ L"
using prems(6) that(2) by blast
from prems have "(Mi li, M l) ∈ ⟨⟨A⟩list_set_rel⟩option_rel"
by parametricity
with prems have "(xsi, S) ∈ ⟨A⟩list_set_rel"
by auto
then obtain xs where "(xsi, xs) ∈ ⟨A⟩list_rel" "set xs = S"
by (elim list_set_relE)
with prems show ?thesis
apply (elim list_set_relE, elim specify_right)
apply (clarsimp, safe)
apply (solves auto)
apply (rule specify_right[where x = xs], rule HOL.refl)
supply [refine_mono] = monadic_list_all_mono' monadic_list_ex_mono'
apply refine_mono
done
qed
done
definition check_prop1 where
"check_prop1 L' M' = do {
l ← RETURN L';
monadic_list_all (λl. do {
let S = op_map_lookup l M';
case S of None ⇒ RETURN True | Some S ⇒ do {
xs ← RETURN S;
r ← monadic_list_all (λs.
RETURN (Pi (l, s))
) xs;
RETURN r
}
}
) l
}"
lemma check_prop1_refine:
"(check_prop1, check_prop') ∈ ⟨K⟩list_set_rel → (K → ⟨⟨A⟩list_set_rel⟩option_rel) → ⟨Id⟩nres_rel"
supply [refine] =
list_of_set_impl[THEN fun_relD, THEN nres_relD] monadic_list_all_mono' case_option_mono'
supply [refine_mono] =
monadic_list_all_mono' list_of_set_impl[THEN fun_relD, THEN nres_relD]
unfolding check_prop1_def check_prop'_def list_of_set_def[symmetric] Let_def op_map_lookup_def
apply refine_rcg
apply assumption
apply (refine_rcg refine_IdI, assumption)
apply parametricity
apply (rule bind_mono)
apply refine_mono+
using Pi_P'
apply (auto simp add: prod_rel_def dest!: fun_relD)
done
lemma [refine]:
"(Mi l⇩0i ≠ None, l⇩0 ∈ L) ∈ bool_rel" if "L = dom M"
using that by (auto simp: Mi_M_None_iff[symmetric, OF l⇩0i_l⇩0])
lemma [refine]:
"(Pi (l⇩0i, s⇩0i), P' (l⇩0, s⇩0)) ∈ bool_rel"
by parametricity
definition
"check_all_pre1 ≡ do {
b1 ← RETURN (Mi l⇩0i ≠ None);
b2 ← RETURN (Pi (l⇩0i, s⇩0i));
case Mi l⇩0i of
None ⇒ RETURN False
| Some xs ⇒ do {
b3 ← monadic_list_ex (λs. RETURN (lei s⇩0i s)) xs;
b4 ← check_prop1 Li Mi;
RETURN (b1 ∧ b2 ∧ b3 ∧ b4)
}
}"
lemma check_all_pre1_refine[refine]:
"(check_all_pre1, check_all_pre l⇩0 s⇩0) ∈ ⟨bool_rel⟩nres_rel" if "L = dom M"
proof (cases "M l⇩0")
case None
then show ?thesis
using that check_prop_gt_SUCCEED l⇩0i_l⇩0 unfolding check_all_pre1_def check_all_pre_def
by (refine_rcg) (simp flip: Mi_M_None_iff add: bind_RES; cases "check_prop P'"; simp)
next
case (Some S)
have "(Mi l⇩0i, M l⇩0) ∈ ⟨⟨A⟩list_set_rel⟩option_rel"
by parametricity
with ‹M l⇩0 = _› obtain xs ys where "Mi l⇩0i = Some xs" "(xs, ys) ∈ ⟨A⟩list_rel" "set ys = S"
unfolding option_rel_def by (auto elim: list_set_relE)
with ‹M l⇩0 = _› show ?thesis
unfolding check_all_pre1_def check_all_pre_def
apply (refine_rcg that; simp)
supply [refine_mono] =
monadic_list_ex_mono' monadic_list_ex_RETURN_mono specify_right HOL.refl
check_prop1_refine[THEN fun_relD, THEN fun_relD, THEN nres_relD, THEN refine_IdD,
of Li L Mi M, unfolded check_prop_alt_def]
Li_L Mi_M
apply refine_mono
done
qed
definition
"check_all1 ≡ do {
b ← check_all_pre1;
if b
then do {
r ← check_invariant1 Li;
PRINT_CHECK STR ''State set invariant check'' r;
RETURN r
}
else RETURN False
}
"
lemma check_all1_correct[refine]:
"check_all1 ≤ SPEC (λr. r ⟶ check_all_pre_spec l⇩0 s⇩0 ∧ check_invariant_spec L)" if "L = dom M"
proof -
from check_all_pre1_refine[THEN nres_relD, OF that] have "check_all_pre1 ≤ check_all_pre l⇩0 s⇩0"
by (rule refine_IdD)
also note check_all_pre_correct
finally have [refine]: "check_all_pre1 ≤ SPEC (λr. r ⟶ check_all_pre_spec l⇩0 s⇩0)"
by (rule Orderings.order.trans) simp
obtain L' where "(Li, L') ∈ ⟨K⟩list_rel" "set L' = L"
using Li_L by (elim list_set_relE)
note check_invariant1_refine
also note check_invariant_correct
also have [refine]: "check_invariant1 Li ≤ SPEC (λr. r ⟶ check_invariant_spec L)"
if "check_all_pre_spec l⇩0 s⇩0"
apply (subst (2) ‹_ = L›[symmetric])
apply (rule calculation)
using Li_L ‹(Li, L') ∈ _› that unfolding check_all_pre_spec_def
by (auto simp: ‹_ = L› ‹L = _› dest: P'_P)
show ?thesis
unfolding check_all1_def PRINT_CHECK_def comp_def by (refine_vcg; simp)
qed
definition
"check_final1 L' = do {
monadic_list_all (λl. do {
case op_map_lookup l Mi of None ⇒ RETURN True | Some xs ⇒ do {
monadic_list_all (λs.
RETURN (¬ PR_CONST Fi (l, s))
) xs
}
}
) L'
}"
lemma check_final1_refine:
"check_final1 Li ≤ check_final' L M"
using Li_L apply (elim list_set_relE)
unfolding check_final1_def check_final'_def
apply (erule specify_right)
supply [refine_mono] = monadic_list_all_mono'
apply refine_mono
apply (clarsimp split: option.splits)
apply (refine_rcg monadic_list_all_mono')
apply (simp flip: Mi_M_None_iff; fail)
subgoal premises prems for _ li l xsi S
proof -
from ‹(li, l) ∈ K› have "(Mi li, M l) ∈ ⟨⟨A⟩list_set_rel⟩option_rel"
by parametricity
with prems have "(xsi, S) ∈ ⟨A⟩list_set_rel"
by auto
then obtain xs where "(xsi, xs) ∈ ⟨A⟩list_rel" "set xs = S"
by (elim list_set_relE)
then show ?thesis
using Fi_F ‹(li, l) ∈ K›
by (refine_rcg monadic_list_all_mono' specify_right) (auto dest!: fun_relD)
qed
done
definition
"certify_unreachable1 = do {
b1 ← check_all1;
b2 ← check_final1 Li;
RETURN (b1 ∧ b2)
}"
lemma certify_unreachable1_correct:
"certify_unreachable1 ≤ SPEC (λr. r ⟶ check_all_spec ∧ check_final_spec)" if "L = dom M"
proof -
note check_final1_refine[unfolded check_final_alt_def]
also note check_final_correct
finally have [refine]: "check_final1 Li ≤ SPEC (λr. r = check_final_spec)" .
show ?thesis
unfolding certify_unreachable1_def check_all_spec_def by (refine_vcg that; fast)
qed
paragraph ‹Synthesizing a pure program via rewriting›
lemma check_final1_alt_def:
"check_final1 L' = RETURN (list_all_split
(λl. case op_map_lookup l Mi of None ⇒ True | Some xs ⇒ list_all (λs. ¬ Fi (l, s)) xs) L')"
unfolding check_final1_def
unfolding monadic_list_all_RETURN[symmetric] list_all_split_def
by (fo_rule arg_cong2, intro ext)
(auto split: option.splits simp: monadic_list_all_RETURN[symmetric])
concrete_definition check_final_impl
uses check_final1_alt_def is "_ = RETURN ?f"
schematic_goal check_prop1_alt_def:
"check_prop1 L' M' ≡ RETURN ?f"
unfolding check_prop1_def pure_unfolds Let_def .
concrete_definition check_prop_impl uses check_prop1_alt_def is "_ ≡ RETURN ?f"
schematic_goal check_all_pre1_alt_def:
"check_all_pre1 ≡ RETURN ?f"
unfolding check_all_pre1_def check_prop_impl.refine pure_unfolds .
concrete_definition check_all_pre_impl uses check_all_pre1_alt_def is "_ ≡ RETURN ?f"
schematic_goal check_invariant1_alt_def:
"check_invariant1 Li ≡ RETURN ?f"
unfolding check_invariant1_def Let_def pure_unfolds .
concrete_definition check_invariant_impl uses check_invariant1_alt_def is "_ ≡ RETURN ?f"
schematic_goal certify_unreachable1_alt_def:
"certify_unreachable1 ≡ RETURN ?f"
unfolding
certify_unreachable1_def check_all1_def check_final_impl.refine check_all_pre_impl.refine
check_invariant_impl.refine
pure_unfolds PRINT_CHECK_def comp_def short_circuit_conv .
concrete_definition certify_unreachable_impl_pure1
uses certify_unreachable1_alt_def is "_ ≡ RETURN ?f"
text ‹This is where we add parallel execution:›
schematic_goal certify_unreachable_impl_pure1_alt_def:
"certify_unreachable_impl_pure1 ≡ ?f"
unfolding certify_unreachable_impl_pure1_def
apply (abstract_let check_invariant_impl check_invariant)
apply (abstract_let "check_final_impl Li" check_final)
apply (abstract_let check_all_pre_impl check_all_pre_impl)
apply (time_it "STR ''Time for state set preconditions check''" check_all_pre_impl)
apply (time_it "STR ''Time for state space invariant check''" check_invariant_impl)
apply (time_it "STR ''Time to check final state predicate''" "check_final_impl Li")
unfolding
check_invariant_impl_def check_all_pre_impl_def
check_prop_impl_def check_final_impl_def
list_all_split
apply (subst list_all_default_split[where xs = Li, folded Parallel.map_def])
.
concrete_definition (in -) certify_unreachable_impl_pure
uses Reachability_Impl_pure.certify_unreachable_impl_pure1_alt_def is "_ ≡ ?f"
sublocale correct: Reachability_Impl_correct where
M = "λx. case M x of None ⇒ {} | Some S ⇒ abs_s ` S"
apply standard
oops
end
locale Reachability_Impl_pure_correct =
Reachability_Impl_pure where M = M +
Reachability_Impl_correct where M = "λx. case M x of None ⇒ {} | Some S ⇒ S" for M
begin
theorem certify_unreachable_impl_pure_correct:
"certify_unreachable_impl_pure get_succs Li lei Li_split Pi Fi Mi l⇩0i s⇩0i
⟶ (∄s'. E⇧*⇧* (l⇩0, s⇩0) s' ∧ F s')"
if "L = dom M"
using certify_unreachable1_correct that
unfolding
certify_unreachable_impl_pure1.refine
certify_unreachable_impl_pure.refine[OF Reachability_Impl_pure_axioms]
using certify_unreachableI by simp
end
section ‹Certificates for B\"uchi Properties›
locale Buechi_Impl_pure =
Buechi_Impl_pre where M = "λx. case M x of None ⇒ {} | Some S ⇒ S" +
Reachability_Impl_pure_base2
for M :: "'k ⇒ ('a × nat) set option" +
fixes Mi :: "'ki ⇒ ('ai × nat) list option"
assumes Mi_M[param]: "(Mi, M) ∈ K → ⟨⟨A ×⇩r Id⟩list_set_rel⟩option_rel"
assumes F_mono:
"⋀a b. F a ⟹ P a ⟹ (λ(l, s) (l', s'). l' = l ∧ less_eq s s') a b ⟹ P b ⟹ F b"
fixes inits :: "('k × 'a) set" and initsi :: "('ki × 'ai) list"
assumes initsi_inits[param]: "(initsi, inits) ∈ ⟨K ×⇩r A⟩list_set_rel"
begin
paragraph ‹Refinement›
definition "check_invariant_buechi' L' ≡
monadic_list_all_split (λl.
case Mi l of
None ⇒ RETURN True
| Some as ⇒ do {
monadic_list_all (λ(x, i). do {
let succs = get_succs l [x];
let is_accepting = Fi (l, x);
let cmp = (if is_accepting then (λj. i < j) else (λj. i ≤ j));
monadic_list_all (λ(l', xs).
if xs = [] then
RETURN True
else
case Mi l' of
None ⇒ RETURN False
| Some ys ⇒
monadic_list_all (λy.
monadic_list_ex (λ(z, j). RETURN (lei y z ∧ cmp j)) ys
) xs
) succs
}) as
}) L'"
lemma Mi_M_None_iff[simp]:
"M l = None ⟷ Mi li = None" if "(li, l) ∈ K"
proof -
from that have "(Mi li, M l) ∈ ⟨⟨A ×⇩r Id⟩list_set_rel⟩option_rel"
by parametricity
then show ?thesis
by auto
qed
lemma (in -) list_set_rel_singletonI[param]:
assumes "(ai, a) ∈ A"
shows "([ai], {a}) ∈ ⟨A⟩list_set_rel"
unfolding list_set_rel_def
using assms by (auto intro: relcompI[where b = "[a]"])
lemma check_invariant1_refine[refine]:
"check_invariant_buechi' L1 ≤ check_invariant_buechi buechi_prop L'"
if "(L1, L') ∈ ⟨K⟩list_rel" "L = dom M" "set L' ⊆ L"
unfolding check_invariant_buechi'_def check_invariant_buechi_def Let_def monadic_list_all_split_def
apply (refine_rcg monadic_list_all_mono' refine_IdI that)
apply (clarsimp split: option.splits; safe)
apply (simp add: RES_sng_eq_RETURN; fail)
apply (simp flip: Mi_M_None_iff; fail)
subgoal premises prems for ki k xs xsi
proof -
from prems fun_relD1[OF Mi_M] have "(Mi ki, M k) ∈ ⟨⟨A ×⇩r nat_rel⟩list_set_rel⟩option_rel"
by force
with prems have "(xsi, xs) ∈ ⟨A ×⇩r nat_rel⟩list_set_rel"
by force
from list_set_relE[OF this] obtain ys where
"(xsi, ys) ∈ ⟨A ×⇩r nat_rel⟩list_rel" "set ys = xs" .
then show ?thesis
using ‹(ki, k) ∈ _›
apply -
apply (erule specify_right)
apply (refine_rcg monadic_list_all_mono')
apply assumption
apply (solves ‹parametricity, auto›)
apply (clarsimp split: option.splits split del: if_split; safe)
apply (solves ‹
elim list_set_relE specify_right;
auto simp: monadic_list_all_False intro!: res_right simp flip: Mi_M_None_iff›)+
subgoal premises prems for si i s ki' xsi' k' xs' zs zsi
proof -
have "k' ∈ L"
using prems(6) that(2) by blast
from ‹(ki, k) ∈ K› ‹(si, s) ∈ A› have Fi_F: "Fi (ki, si) ⟷ F (k, s)"
using Fi_F by (force dest: fun_relD1)
from prems fun_relD1[OF Mi_M] have "(Mi ki', M k') ∈ ⟨⟨A ×⇩r nat_rel⟩list_set_rel⟩option_rel"
by force
with prems have "(zsi, zs) ∈ ⟨A ×⇩r nat_rel⟩list_set_rel"
by force
from list_set_relE[OF this] obtain ws where
"(zsi, ws) ∈ ⟨A ×⇩r nat_rel⟩list_rel" "set ws = zs" .
moreover from list_set_relE[OF ‹_ ∈ ⟨A⟩list_set_rel›] obtain ys' where
"(xsi', ys') ∈ ⟨A⟩list_rel" "set ys' = xs'" .
ultimately show ?thesis
using ‹k' ∈ L› lei_refine Fi_F
unfolding buechi_prop_def
supply [refine_mono] = monadic_list_all_mono' monadic_list_ex_mono' specify_right HOL.refl
by (refine_mono | auto)+
qed
done
qed
done
definition check_prop1 where
"check_prop1 L' M' = do {
l ← RETURN L';
monadic_list_all (λl. do {
let S = op_map_lookup l M';
case S of None ⇒ RETURN True | Some S ⇒ do {
xs ← RETURN S;
r ← monadic_list_all (λ(s, _).
RETURN (Pi (l, s))
) xs;
RETURN r
}
}
) l
}"
definition
"check_init1 l⇩0i s⇩0i ≡ do {
b1 ← RETURN (Mi l⇩0i ≠ None);
b2 ← RETURN (Pi (l⇩0i, s⇩0i));
case Mi l⇩0i of
None ⇒ RETURN False
| Some xs ⇒ do {
b3 ← monadic_list_ex (λ(s, _). RETURN (lei s⇩0i s)) xs;
RETURN (b1 ∧ b2 ∧ b3)
}
}"
definition check_prop' where
"check_prop' L' M' = do {
l ← SPEC (λxs. set xs = L');
monadic_list_all (λl. do {
let S = op_map_lookup l M';
case S of None ⇒ RETURN True | Some S ⇒ do {
xs ← SPEC (λxs. set xs = S);
r ← monadic_list_all (λ(s, _).
RETURN (PR_CONST P' (l, s))
) xs;
RETURN r
}
}
) l
}"
definition
"check_all_pre1 ≡ do {
b1 ← monadic_list_all (λ(l⇩0, s⇩0). check_init1 l⇩0 s⇩0) initsi;
b2 ← check_prop1 Li Mi;
RETURN (b1 ∧ b2)
}"
lemma check_prop1_refine:
"(check_prop1, check_prop')
∈ ⟨K⟩list_set_rel → (K → ⟨⟨A ×⇩r Id⟩list_set_rel⟩option_rel) → ⟨Id⟩nres_rel"
supply [refine] =
list_of_set_impl[THEN fun_relD, THEN nres_relD] monadic_list_all_mono' case_option_mono'
supply [refine_mono] =
monadic_list_all_mono' list_of_set_impl[THEN fun_relD, THEN nres_relD]
unfolding check_prop1_def check_prop'_def list_of_set_def[symmetric] Let_def op_map_lookup_def
apply refine_rcg
apply assumption
apply (refine_rcg refine_IdI, assumption)
apply parametricity
apply (rule bind_mono)
apply refine_mono+
using Pi_P' by (auto simp add: prod_rel_def dest!: fun_relD)
sublocale reachability:
Reachability_Impl_pre where M = "image fst o (λx. case M x of None ⇒ {} | Some S ⇒ S)" ..
lemma check_prop_gt_SUCCEED:
"reachability.check_prop P' > SUCCEED" if "L = dom M"
using finite that unfolding reachability.check_prop_def
by (intro monadic_list_all_gt_SUCCEED bind_RES_gt_SUCCEED_I)
(auto split: option.split simp: dom_def intro!: finite_list)
lemma check_prop_alt_def:
"check_prop' L M = reachability.check_prop P'" if "L = dom M"
unfolding reachability.check_prop_def check_prop'_def
apply (fo_rule arg_cong2, simp, fo_rule arg_cong)
apply (clarsimp split: option.split simp: bind_RES)
apply (rule ext)
apply (clarsimp split: option.split simp: bind_RES)
apply (fo_rule arg_cong)
unfolding pure_unfolds image_def
subgoal premises prems
proof -
{
fix l :: ‹'k› and xs:: ‹('a × nat) list›
assume ‹M l = Some (set xs)›
have ‹∃x. set x = {y. ∃x∈set xs. y = fst x} ∧
list_all (λ(s, _). P' (l, s)) xs = list_all (λs. P' (l, s)) x›
by (rule exI[where x = "map fst xs"]) (auto simp: list_all_iff)
}
moreover
{
fix l :: ‹'k› and S :: ‹('a × nat) set› and ys :: ‹'a list›
assume ‹M l = Some S› and ‹set ys = {y. ∃x∈S. y = fst x}›
with ‹L = _› finite have "finite S"
by force
then obtain xs where "set xs = S"
by atomize_elim (rule finite_list)
with ‹set ys = _› have
‹∃x. set x = S ∧ list_all (λs. P' (l, s)) ys = list_all (λ(s, _). P' (l, s)) x›
by (intro exI[where x = xs]) (auto simp: list_all_iff)
}
ultimately show ?thesis
using prems by (safe; simp)
qed
done
lemma check_init1_refine:
"(check_init1, reachability.check_init) ∈ K → A → ⟨bool_rel⟩nres_rel" if "L = dom M"
proof (intro fun_relI)
fix l⇩0 l⇩0i s⇩0 s⇩0i
assume l⇩0i_l⇩0: "(l⇩0i, l⇩0) ∈ K" and s⇩0i_s⇩0: "(s⇩0i, s⇩0) ∈ A"
then have [refine]:
"(Pi (l⇩0i, s⇩0i), P' (l⇩0, s⇩0)) ∈ bool_rel"
by parametricity
have [refine]:
"(Mi l⇩0i ≠ None, l⇩0 ∈ L) ∈ bool_rel"
using that by (auto simp: Mi_M_None_iff[symmetric, OF ‹_ ∈ K›])
show "(check_init1 l⇩0i s⇩0i, reachability.check_init l⇩0 s⇩0) ∈ ⟨bool_rel⟩nres_rel"
proof (cases "M l⇩0")
case None
then show ?thesis
using that l⇩0i_l⇩0 unfolding check_init1_def reachability.check_init_def
by refine_rcg (simp flip: Mi_M_None_iff add: bind_RES; simp)
next
case (Some S)
from ‹_ ∈ K› have "(Mi l⇩0i, M l⇩0) ∈ ⟨⟨A ×⇩r Id⟩list_set_rel⟩option_rel"
by parametricity
with ‹M l⇩0 = _› obtain xs ys where *:
"Mi l⇩0i = Some xs" "(xs, ys) ∈ ⟨A ×⇩r Id⟩list_rel" "set (map fst ys) = fst ` S"
unfolding option_rel_def by (auto elim: list_set_relE)
then have "(xs, map fst ys) ∈ ⟨{((x, i), y). (x, y) ∈ A}⟩list_rel"
unfolding list_rel_def by (auto elim: list_all2_induct)
with * ‹M l⇩0 = _› show ?thesis
unfolding check_init1_def reachability.check_init_def
apply (refine_rcg that; simp)
supply [refine_mono] = monadic_list_ex_mono' specify_right Li_L Mi_M
apply refine_mono
using lei_refine s⇩0i_s⇩0 apply auto
done
qed
qed
lemma check_all_pre1_correct[refine]:
"check_all_pre1 ≤ SPEC (λr. r ⟶ check_all_pre_spec1 inits)" if "L = dom M"
proof -
note check_init1_refine[THEN fun_relD, THEN fun_relD, THEN nres_relD, OF that]
also note reachability.check_init_correct
finally have [refine_mono, refine]:
"check_init1 l⇩0i s⇩0i ≤ SPEC (λr. r = reachability.check_init_spec l⇩0 s⇩0)"
if l⇩0i_l⇩0: "(l⇩0i, l⇩0) ∈ K" and s⇩0i_s⇩0: "(s⇩0i, s⇩0) ∈ A" for l⇩0 l⇩0i s⇩0 s⇩0i
using that by (force intro: Orderings.order.trans)
from initsi_inits obtain inits' where
"inits = set inits'" and [refine_mono]: "(initsi, inits') ∈ ⟨K ×⇩r A⟩list_rel"
unfolding list_set_rel_def by auto
note [refine_mono] = case_prod_mono monadic_list_all_mono'
have [refine]: "monadic_list_all (λ(l⇩0, s⇩0). check_init1 l⇩0 s⇩0) initsi
≤ SPEC (λr. r = list_all (λ(l⇩0, s⇩0). reachability.check_init_spec l⇩0 s⇩0) inits')"
by (rule Orderings.order.trans, refine_mono) (refine_vcg monadic_list_all_rule; auto)
note check_prop1_refine[THEN fun_relD, THEN fun_relD, THEN nres_relD, THEN refine_IdD,
OF Li_L Mi_M, unfolded check_prop_alt_def[OF ‹L = _›]]
also note reachability.check_prop_correct
also note [refine] = calculation
show ?thesis
unfolding check_all_pre1_def
by refine_vcg
(fastforce simp:
check_all_pre_spec1_def reachability.check_init_spec_def list_all_iff ‹inits = set inits'›)
qed
definition
"PRINT_CHECK' s b ≡ RETURN (let b = b; x = print_check s b in b)"
definition
"certify_no_buechi_run ≡ do {
b ← check_all_pre1;
if b
then do {
r ← check_invariant_buechi' Li;
PRINT_CHECK' STR ''State space invariant check'' r
}
else RETURN False
}"
lemma check_all1_refine:
"certify_no_buechi_run ≤ check_buechi inits" if "L = dom M"
proof -
obtain L' where aux: "(Li, L') ∈ ⟨K⟩list_rel" "set L' = L"
using Li_L by (elim list_set_relE)
note check_invariant1_refine
also note check_invariant_buechi_correct
also note [refine] = calculation
have [refine]:
"check_invariant_buechi' Li ≤ SPEC (λr. r ⟶ check_invariant_buechi_spec buechi_prop L)"
if "∀l∈L. ∀(s, _)∈case M l of None ⇒ {} | Some S ⇒ S. P (l, s)"
using aux that ‹L = dom M› by refine_vcg simp+
show ?thesis
using P'_P that unfolding certify_no_buechi_run_def check_buechi_def PRINT_CHECK'_def comp_def
by (refine_mono; refine_vcg;
unfold check_all_pre_spec1_def; fastforce split: prod.splits simp: check_all_pre_spec1_def)
qed
paragraph ‹Synthesizing a pure program via rewriting›
schematic_goal check_prop1_alt_def:
"check_prop1 L' M' ≡ RETURN ?f"
unfolding check_prop1_def pure_unfolds Let_def .
concrete_definition check_prop_impl uses check_prop1_alt_def is "_ ≡ RETURN ?f"
lemma check_all_pre1_printing:
"check_all_pre1 ≡ do {
b1 ← monadic_list_all (λ(l⇩0, s⇩0). check_init1 l⇩0 s⇩0) initsi;
b1 ← PRINT_CHECK' STR ''Initial state check'' b1;
b2 ← check_prop1 Li Mi;
b2 ← PRINT_CHECK' STR ''State set preconditions check'' b2;
RETURN (b1 ∧ b2)
}"
unfolding check_all_pre1_def PRINT_CHECK'_def Let_def pure_unfolds .
schematic_goal check_all_pre1_alt_def:
"check_all_pre1 ≡ RETURN ?f"
unfolding
check_all_pre1_printing check_init1_def check_prop_impl.refine pure_unfolds PRINT_CHECK'_def .
concrete_definition check_all_pre_impl uses check_all_pre1_alt_def is "_ ≡ RETURN ?f"
schematic_goal check_invariant_buechi'_alt_def:
"check_invariant_buechi' Li ≡ RETURN ?f"
unfolding check_invariant_buechi'_def Let_def pure_unfolds .
lemma PRINT_CHECK_unfold:
"PRINT_CHECK s x = RETURN (print_check s x)"
unfolding PRINT_CHECK_def comp_def ..
concrete_definition check_invariant_buechi_impl
uses check_invariant_buechi'_alt_def is "_ ≡ RETURN ?f"
schematic_goal certify_no_buechi_run_alt_def:
"certify_no_buechi_run ≡ RETURN ?f"
unfolding
certify_no_buechi_run_def check_all_pre_impl.refine
check_invariant_buechi_impl.refine
PRINT_CHECK'_def pure_unfolds
short_circuit_conv
.
concrete_definition certify_no_buechi_run_pure1
uses certify_no_buechi_run_alt_def is "_ ≡ RETURN ?f"
text ‹This is where we add parallel execution:›
schematic_goal certify_no_buechi_run_pure1_alt_def:
"certify_no_buechi_run_pure1 ≡ ?f"
unfolding certify_no_buechi_run_pure1_def
apply (abstract_let check_invariant_buechi_impl check_invariant)
apply (abstract_let check_all_pre_impl check_all_pre_impl)
apply (time_it "STR ''Time for state set preconditions check''" check_all_pre_impl)
apply (time_it "STR ''Time for state space invariant check''" check_invariant_buechi_impl)
unfolding
check_invariant_buechi_impl_def check_all_pre_impl_def
check_prop_impl_def
list_all_split
apply (subst list_all_default_split[where xs = Li, folded Parallel.map_def])
.
concrete_definition (in -) certify_no_buechi_run_pure
uses Buechi_Impl_pure.certify_no_buechi_run_pure1_alt_def is "_ ≡ ?f"
end
locale Buechi_Impl_pure_correct =
Buechi_Impl_pure where M = M +
Buechi_Impl_correct where M = "λx. case M x of None ⇒ {} | Some S ⇒ S" for M
begin
theorem certify_no_buechi_run_correct:
"certify_no_buechi_run ≤ SPEC (λr. r ⟶ (∄xs l⇩0 s⇩0.
(l⇩0, s⇩0) ∈ inits ∧ Graph_Defs.run E ((l⇩0, s⇩0) ## xs) ∧ alw (ev (holds F)) ((l⇩0, s⇩0) ## xs)))"
if "L = dom M"
by (rule Orderings.order.trans[OF check_all1_refine[OF that]],
refine_vcg that check_buechi_correct')
(auto intro: no_buechi_run)
theorem certify_no_buechi_run_impl_pure_correct:
"certify_no_buechi_run_pure get_succs Li lei Li_split Pi Fi Mi initsi ⟶ (∄xs l⇩0 s⇩0.
(l⇩0, s⇩0) ∈ inits ∧ Graph_Defs.run E ((l⇩0, s⇩0) ## xs) ∧ alw (ev (holds F)) ((l⇩0, s⇩0) ## xs))"
if "L = dom M"
using certify_no_buechi_run_correct that
unfolding
certify_no_buechi_run_pure1.refine
certify_no_buechi_run_pure.refine[OF Buechi_Impl_pure_axioms]
by simp
end
locale Reachability_Impl_imp_to_pure_base = Certification_Impl_base
where K = K and A = A
for K :: "'k ⇒ ('ki :: {hashable,heap}) ⇒ assn" and A :: "'s ⇒ ('si :: heap) ⇒ assn"
+
fixes to_state :: "'s1 ⇒ 'si Heap" and from_state :: "'si ⇒ 's1 Heap"
and to_loc :: "'k1 ⇒ 'ki" and from_loc :: "'ki ⇒ 'k1"
fixes lei
fixes K_rel and A_rel
fixes L_list :: "'ki list" and Li :: "'k1 list" and L :: "'k set" and L' :: "'k list"
fixes Li_split :: "'k1 list list"
assumes Li: "(L_list, L') ∈ ⟨the_pure K⟩list_rel" "(Li, L') ∈ ⟨K_rel⟩list_rel" "set L' = L"
assumes to_state_ht: "(s1, s) ∈ A_rel ⟹ <emp> to_state s1 <λsi. A s si>"
assumes from_state_ht: "<A s si> from_state si <λs'. ↑((s', s) ∈ A_rel)>⇩t"
assumes from_loc: "(li, l) ∈ the_pure K ⟹ (from_loc li, l) ∈ K_rel"
assumes to_loc: "(l1, l) ∈ K_rel ⟹ (to_loc l1, l) ∈ the_pure K"
assumes K_rel: "single_valued K_rel" "single_valued (K_rel¯)"
assumes lei_less_eq: "(lei, (≼)) ∈ A_rel → A_rel → bool_rel"
assumes full_split: "set Li = (⋃xs ∈ set Li_split. set xs)"
begin
definition
"get_succs l xs ≡
do {
let li = to_loc l;
xsi ← Heap_Monad.fold_map to_state xs;
r ← succsi li xsi;
Heap_Monad.fold_map
(λ(li, xsi). do {xs ← Heap_Monad.fold_map from_state xsi; return (from_loc li, xs)}) r
}"
lemma get_succs:
"(run_heap oo get_succs, succs)
∈ K_rel → ⟨A_rel⟩list_set_rel → ⟨K_rel ×⇩r ⟨A_rel⟩list_set_rel⟩list_rel"
proof -
{
fix l :: ‹'k› and l1 :: ‹'k1› and xs :: ‹'s1 list› and S :: ‹'s set›
assume ‹(l1, l) ∈ K_rel› ‹(xs, S) ∈ ⟨A_rel⟩list_set_rel›
then obtain ys where ys: "(xs, ys) ∈ ⟨A_rel⟩list_rel" "set ys = S"
by (elim list_set_relE)
have 1: "K = pure (the_pure K)"
using pure_K by auto
let ?li = "to_loc l1"
have "<emp> get_succs l1 xs <λr. ↑((r, succs l S) ∈ ⟨K_rel ×⇩r ⟨A_rel⟩list_set_rel⟩list_rel)>⇩t"
unfolding get_succs_def
apply sep_auto
apply (rule Hoare_Triple.cons_pre_rule[rotated])
apply (rule fold_map_ht3[where A = true and R = "pure A_rel" and Q = A and xs = ys])
apply (sep_auto heap: to_state_ht simp: pure_def; fail)
apply (unfold list_assn_pure_conv, sep_auto simp: pure_def ys; fail)
apply sep_auto
apply (rule Hoare_Triple.cons_pre_rule[rotated], rule frame_rule[where R = true])
apply (rule succsi[to_hnr, unfolded hn_refine_def hn_ctxt_def, simplified, of S _ l ?li])
subgoal
using ys ‹(l1, l) ∈ K_rel› unfolding lso_assn_def hr_comp_def br_def ‹set ys = _›[symmetric]
by (subst 1) (sep_auto simp: pure_def to_loc)
apply (sep_auto simp: invalid_assn_def)
apply (rule cons_rule[rotated 2])
apply (rule frame_rule)
apply (rule fold_map_ht1[where
A = true and R = "(K ×⇩a lso_assn A)" and xs = "succs l S" and
Q = "λx xi. (xi, x) ∈ K_rel ×⇩r ⟨A_rel⟩list_set_rel"
])
subgoal
unfolding lso_assn_def
apply (subst 1, subst pure_def)
apply (sep_auto simp: prod_assn_def hr_comp_def br_def split: prod.splits)
apply (rule Hoare_Triple.cons_pre_rule[rotated])
apply (rule fold_map_ht1[where A = true and R = A and Q = "λl l1. (l1, l) ∈ A_rel"])
apply (rule cons_rule[rotated 2], rule frame_rule, rule from_state_ht)
apply frame_inference
apply (sep_auto; fail)
apply solve_entails
using list_all2_swap by (sep_auto simp: list.rel_eq list_set_rel_def from_loc list_rel_def)
apply solve_entails
using list_all2_swap by (sep_auto simp: list_rel_def)
}
then show ?thesis
by (refine_rcg, clarsimp, rule hoare_triple_run_heapD)
qed
definition
"to_pair ≡ λ(l, s). do {s ← to_state s; return (to_loc l, s)}"
lemma to_pair_ht:
"<emp> to_pair a1 <λai. (K ×⇩a A) a ai>" if "(a1, a) ∈ K_rel ×⇩r A_rel"
using that unfolding to_pair_def
by (cases a, cases a1, subst pure_the_pure[symmetric, OF pure_K])
(sep_auto heap: to_state_ht simp: pure_def to_loc prod_assn_def split: prod.splits)
sublocale pure:
Reachability_Impl_pure_base2
where
get_succs = "run_heap oo get_succs" and
K = K_rel and
A = A_rel and
lei = lei and
Pi = "λa. run_heap (do {a ← to_pair a; Pi a})" and
Fi = "λa. run_heap (do {a ← to_pair a; Fi a})"
apply standard
subgoal
by (rule K_rel)
subgoal
by (rule K_rel)
subgoal
using Li unfolding list_set_rel_def by auto
subgoal
by (rule lei_less_eq)
subgoal
using get_succs .
subgoal
by (rule full_split)
subgoal
apply standard
apply (rule hoare_triple_run_heapD)
apply (sep_auto heap: to_pair_ht simp del: prod_rel_simp prod_assn_pair_conv)
apply (rule Hoare_Triple.cons_rule[rotated 2])
apply (rule Pi_P'[to_hnr, unfolded hn_refine_def hn_ctxt_def, simplified], rule ent_refl)
apply (sep_auto simp: pure_def)
done
subgoal
apply standard
apply (rule hoare_triple_run_heapD)
apply (sep_auto heap: to_pair_ht simp del: prod_rel_simp prod_assn_pair_conv)
apply (rule Hoare_Triple.cons_rule[rotated 2])
apply (rule Fi_F[to_hnr, unfolded hn_refine_def hn_ctxt_def, simplified], rule ent_refl)
apply (sep_auto simp: pure_def)
done
done
end
locale Reachability_Impl_imp_to_pure = Reachability_Impl where
l⇩0 = l⇩0 and s⇩0 = s⇩0 and M = M and K = K and A = A
+ Reachability_Impl_imp_to_pure_base
where K_rel = K_rel and A_rel = A_rel and K = K and A = A
for l⇩0 :: 'k and s⇩0 :: 'a
and K :: "'k ⇒ ('ki :: {hashable,heap}) ⇒ assn" and A :: "'a ⇒ ('ai :: heap) ⇒ assn"
and M and K_rel :: "('k1 × 'k) set" and A_rel :: "('a1 × 'a) set" +
fixes Mi :: "'k1 ⇒ 'a1 list option"
assumes Mi_M: "(Mi, M) ∈ K_rel → ⟨⟨A_rel⟩list_set_rel⟩option_rel"
begin
sublocale pure:
Reachability_Impl_pure
where
M = M and
Mi = Mi and
get_succs = "run_heap oo get_succs" and
K = K_rel and
A = A_rel and
lei = lei and
Pi = "λa. run_heap (do {a ← to_pair a; Pi a})" and
Fi = "λa. run_heap (do {a ← to_pair a; Fi a})" and
l⇩0i = "from_loc (run_heap l⇩0i)" and
s⇩0i = "run_heap (do {s ← s⇩0i; from_state s})"
apply standard
apply (rule Mi_M)
subgoal
apply (rule from_loc)
apply (rule hoare_triple_run_heapD)
using l⇩0i_l⇩0[to_hnr, unfolded hn_refine_def hn_ctxt_def, simplified]
apply (subst (asm) pure_the_pure[symmetric, OF pure_K])
apply (sep_auto simp: pure_def elim!: cons_post_rule)
done
subgoal
using s⇩0i_s⇩0[to_hnr, unfolded hn_refine_def hn_ctxt_def, simplified]
by - (rule hoare_triple_run_heapD, sep_auto heap: from_state_ht)
done
end
locale Reachability_Impl_imp_to_pure_correct =
Reachability_Impl_imp_to_pure where M = M
+ Reachability_Impl_correct where M = "λx. case M x of None ⇒ {} | Some S ⇒ S"
for M
begin
sublocale pure:
Reachability_Impl_pure_correct
where
M = M and
Mi = Mi and
get_succs = "run_heap oo get_succs" and
K = K_rel and
A = A_rel and
lei = lei and
Pi = "λa. run_heap (do {a ← to_pair a; Pi a})" and
Fi = "λa. run_heap (do {a ← to_pair a; Fi a})" and
l⇩0i = "from_loc (run_heap l⇩0i)" and
s⇩0i = "run_heap (do {s ← s⇩0i; from_state s})"
by standard
end
locale Buechi_Impl_imp_to_pure = Buechi_Impl_pre where
M = "λx. case M x of None ⇒ {} | Some S ⇒ S"
+ Reachability_Impl_imp_to_pure_base
where K_rel = K_rel and A_rel = A_rel
for M :: "'k ⇒ ('a × nat) set option"
and K_rel :: "('ki × 'k) set" and A_rel :: "('ai × 'a) set" +
fixes inits initsi
assumes initsi_inits: "(uncurry0 initsi, uncurry0 (RETURN (PR_CONST inits)))
∈ unit_assn⇧k →⇩a list_assn (K ×⇩a A)"
fixes Mi :: "'ki ⇒ ('ai × nat) list option"
assumes Mi_M: "(Mi, M) ∈ K_rel → ⟨⟨A_rel ×⇩r Id⟩list_set_rel⟩option_rel"
begin
lemma (in -) list_all2_flip:
"list_all2 P xs ys" if "list_all2 Q ys xs" "(⋀x y. Q y x ⟹ P x y)"
using that by (simp add: list_all2_conv_all_nth)
sublocale pure:
Buechi_Impl_pure
where
M = M and
Mi = Mi and
get_succs = "run_heap oo get_succs" and
K = K_rel and
A = A_rel and
lei = lei and
Pi = "λa. run_heap (do {a ← to_pair a; Pi a})" and
Fi = "λa. run_heap (do {a ← to_pair a; Fi a})" and
inits = "set inits" and
initsi = "
run_heap (do {
xs ← initsi;
Heap_Monad.fold_map (λ(l, s). do {s ← from_state s; return (from_loc l, s)}) xs})"
apply standard
apply (rule Mi_M F_mono; assumption)+
apply (rule hoare_triple_run_heapD)
subgoal
proof -
have ***: "<↑((li, l) ∈ the_pure K) * ↑ ((s1, s) ∈ A_rel) * true> return (from_loc li, s1)
<λ(l1, s1). ↑ ((l1, l) ∈ K_rel) * ↑((s1, s) ∈ A_rel)>⇩t" for li l s1 s
by (sep_auto intro: from_loc)
have 1: "(l, fst (a, b)) ∈ R" if "(l, a) ∈ R" for l a b R
using that by auto
have 2: "(l, snd (a, b)) ∈ R" if "(l, b) ∈ R" for l a b R
using that by auto
have "
<emp> (do {
xs ← initsi;
Heap_Monad.fold_map (λ(l, s). do {s ← from_state s; return (from_loc l, s)}) xs})
<λr. ↑ ((r, inits) ∈ ⟨K_rel ×⇩r A_rel⟩list_rel)>⇩t"
using initsi_inits[to_hnr, unfolded hn_refine_def hn_ctxt_def, simplified]
apply (subst (asm) pure_the_pure[symmetric, OF pure_K])
apply (sep_auto simp: pure_def list_rel_def heap: fold_map_ht1)
prefer 3
apply (sep_auto elim: list_all2_flip)
prefer 2
apply (rule cons_post_rule)
apply (rule ***)
prefer 2
apply (sep_auto heap: from_state_ht elim: 1 2)+
done
then show ?thesis
by (sep_auto simp: pure_def list_set_rel_def relcomp.simps elim!: cons_post_rule)
qed
done
end
locale Buechi_Impl_imp_to_pure_correct =
Buechi_Impl_imp_to_pure where M = M +
Buechi_Impl_correct where M = "λx. case M x of None ⇒ {} | Some S ⇒ S"
for M
begin
sublocale pure:
Buechi_Impl_pure_correct
where
M = M and
Mi = Mi and
get_succs = "run_heap oo get_succs" and
K = K_rel and
A = A_rel and
lei = lei and
Pi = "λa. run_heap (do {a ← to_pair a; Pi a})" and
Fi = "λa. run_heap (do {a ← to_pair a; Fi a})" and
inits = "set inits" and
initsi = "
run_heap (do {
xs ← initsi;
Heap_Monad.fold_map (λ(l, s). do {s ← from_state s; return (from_loc l, s)}) xs})"
..
end
end