Theory Unreachability_Misc
section ‹Certificates for (Un)Reachability Properties›
theory Unreachability_Misc
imports
Simulation_Graphs_Certification
Worklist_Algorithms.Leadsto_Impl
Munta_Base.Printing
Difference_Bound_Matrices.DBM_Imperative_Loops
Munta_Base.Trace_Timing
begin
paragraph ‹Misc›
theorem (in -) arg_max_nat_lemma2:
fixes f :: "'a ⇒ nat"
assumes "P k"
and "finite (Collect P)"
shows "P (arg_max f P) ∧ (∀y. P y ⟶ f y ≤ f (arg_max f P))"
proof -
let ?b = "Max (f ` Collect P) + 1"
from assms(2) have "∀y. P y ⟶ f y < ?b"
by (auto intro: Max_ge le_imp_less_Suc)
with assms(1) show ?thesis
by (rule arg_max_nat_lemma)
qed
paragraph ‹Misc ‹heap››
lemma hoare_triple_success:
assumes "<P> c <Q>" and "(h, as) ⊨ P"
shows "success c h"
using assms unfolding hoare_triple_def Let_def success_def
by (cases "execute c h") (force simp: run.simps)+
lemma run_return: "run (return x) (Some h) (Some h) x" for h
by (auto simp: execute_simps intro: run.regular)
lemma return_htD:
assumes "<Q x> return x <PP>"
shows "Q x ⟹⇩A PP x"
using assms unfolding hoare_triple_def Let_def by (force intro: run_return entailsI)
definition run_heap :: "'a Heap ⇒ 'a" where
"run_heap h = fst (the (execute h Heap.empty))"
code_printing constant run_heap ⇀ (SML) "(fn f => f ()) _"
code_printing constant run_heap ⇀ (OCaml) "(fun f -> f ()) _"
definition run_map_heap :: "('a ⇒ 'b Heap) ⇒ 'a list ⇒ 'b list" where
"run_map_heap f xs = map (run_heap o f) xs"
lemma hoare_triple_executeD:
assumes "<emp> c <λr. ↑(P r)>⇩t"
shows "P (fst (the (execute c h)))"
proof -
have "(h, {}) ⊨ emp"
by simp
with assms(1) have "success c h"
by (rule hoare_triple_success)
then obtain r h' where "execute c h = Some (r, h')"
unfolding success_def by auto
then have "run c (Some h) (Some h') r"
by (intro regular) auto
with ‹execute c h = _› show ?thesis
using assms unfolding hoare_triple_def by (force intro: mod_emp_simp)
qed
lemma hoare_triple_run_heapD:
assumes "<emp> c <λr. ↑(P r)>⇩t"
shows "P (run_heap c)"
using hoare_triple_executeD[OF assms] unfolding run_heap_def .
lemma list_all2_conjI:
assumes "list_all2 P as bs" "list_all2 Q as bs"
shows "list_all2 (λa b. P a b ∧ Q a b) as bs"
using assms unfolding list_all2_conv_all_nth by auto
lemma hoare_triple_run_map_heapD:
assumes "list_all (λx. <emp> c x <λr. ↑(P x r)>⇩t) xs"
shows "list_all2 P xs (run_map_heap c xs)"
using assms unfolding run_map_heap_def list_all2_map2 list.pred_rel
by (elim list_all2_mono) (auto simp: eq_onp_def intro: hoare_triple_run_heapD)
lemma hoare_triple_run_map_heapD':
assumes "list_all2 (λx xi. <emp> c xi <λr. ↑(P x r)>⇩t) xs xsi"
shows "list_all2 P xs (run_map_heap c xsi)"
using assms unfolding run_map_heap_def list_all2_map2 list.pred_rel
by (elim list_all2_mono) (auto simp: eq_onp_def intro: hoare_triple_run_heapD)
definition
"parallel_fold_map = Heap_Monad.fold_map"
paragraph ‹Misc ‹nres››
lemma no_fail_RES_bindI:
assumes "⋀x. x ∈ S ⟹ nofail (f x)"
shows "nofail (RES S ⤜ f)"
using assms pw_RES_bind_choose(1) by blast
lemma nfoldli_ub_RES_rule:
assumes "⋀x s. x ∈ set xs ⟹ s ∈ S ⟹ f x s ≤ RES S" "s ∈ S"
shows "nfoldli xs c f s ≤ RES S"
using assms
by (induction xs arbitrary: s; simp; metis (no_types) inres_simps(2) pw_bind_le_iff pw_le_iff)
lemma nfoldli_ub_rule:
assumes "⋀x s. x ∈ set xs ⟹ inres ub s ⟹ f x s ≤ ub" "inres ub s"
shows "nfoldli xs c f s ≤ ub"
using nfoldli_ub_RES_rule assms by (metis inres_def nofail_RES_conv nres_order_simps(21) pw_leI')
lemma nfoldli_nofail_rule:
assumes "⋀x s. x ∈ set xs ⟹ inres ub s ⟹ f x s ≤ ub" "inres ub s" "nofail ub"
shows "nofail (nfoldli xs c f s)"
using assms by - (erule pwD1[rotated], rule nfoldli_ub_rule)
lemma SUCCEED_lt_RES_iff[simp]:
"SUCCEED < RES S ⟷ S ≠ {}"
unfolding bot_nres_def by (subst less_nres.simps) auto
lemma SUCCEED_lt_RETURN[intro, simp]:
"SUCCEED < RETURN x"
unfolding RETURN_def by simp
lemma SUCCEED_lt_FAIL[intro, simp]:
"SUCCEED < FAIL"
unfolding bot_nres_def top_nres_def by (subst less_nres.simps) auto
lemma bind_RES_gt_SUCCEED_I:
assumes "⋀s. f s > SUCCEED" "S ≠ {}"
shows "do {x ← RES S; f x} > SUCCEED"
by (metis RES_bind_choose assms(1) assms(2) le_less preorder_class.less_le_not_le set_notEmptyE)
paragraph ‹Monadic ‹list_all› and ‹list_ex››
definition
"monadic_list_all P xs ≡ nfoldli xs id (λx _. P x) True"
text ‹Debug version›
definition
"monadic_list_all_fail P xs ≡
nfoldli xs (λx. x = None) (λx _. do {b ← P x; RETURN (if b then None else Some x)}) None"
lemma monadic_list_all_fail_alt_def:
"monadic_list_all_fail P xs =
nfoldli xs (λx. x = None) (λx _. do {
b ← P (COPY x); if b then RETURN None else RETURN (Some x)}) None"
unfolding monadic_list_all_fail_def
apply (intro arg_cong2[where f = "nfoldli xs (λx. x = None)"] ext)
apply simp
apply (rule bind_cong)
apply auto
done
definition
"monadic_list_all_fail' P xs ≡
nfoldli xs (λx. x = None) (λx _. do {
r ← P x; RETURN (case r of None ⇒ None | Some r ⇒ Some r)})
None"
lemma monadic_list_all_fail'_alt_def:
"monadic_list_all_fail' P xs =
nfoldli xs (λx. x = None) (λx _. do {
r ← P x; case r of None ⇒ RETURN None | Some r ⇒ RETURN (Some r)})
None"
unfolding monadic_list_all_fail'_def
apply (intro arg_cong2[where f = "nfoldli xs (λx. x = None)"] ext)
apply simp
apply (rule bind_cong)
apply (auto split: option.splits)
done
lemma monadic_list_all_fail_monadic_list_all_fail':
"monadic_list_all_fail P xs =
monadic_list_all_fail' (λx. do {b ← P x; RETURN (if b then None else Some x)}) xs"
unfolding monadic_list_all_fail_def monadic_list_all_fail'_def
apply (intro arg_cong2[where f = "nfoldli xs (λx. x = None)"] ext)
apply simp
apply (rule bind_cong)
apply auto
done
lemma monadic_list_all_rule:
assumes "⋀x. 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
definition
"monadic_list_ex P xs ≡ nfoldli xs Not (λx _. P x) False"
lemma monadic_list_ex_rule:
assumes "⋀x. Pi x ≤ SPEC (λr. r = P x)"
shows "monadic_list_ex Pi xs ≤ SPEC (λr. r ⟷ list_ex P xs)"
using assms unfolding monadic_list_ex_def
by (intro nfoldli_rule[where I = "λas bs b. b = list_ex P as ∧ set (as @ bs) = set xs"]) auto
lemma monadic_list_ex_empty[simp]:
"monadic_list_ex P [] = RETURN False"
unfolding monadic_list_ex_def by simp
lemma monadic_list_all_empty[simp]:
"monadic_list_all P [] = RETURN True"
unfolding monadic_list_all_def by simp
lemma monadic_list_all_False: "monadic_list_all (λx. RETURN False) xs = RETURN (xs = [])"
by (cases xs) (auto simp: monadic_list_all_def)
lemma monadic_list_all_RETURN:
"monadic_list_all (λx. RETURN (P x)) xs = RETURN (list_all P xs)"
proof (induction xs)
case Nil
then show ?case
by auto
next
case (Cons x xs)
then show ?case
by (cases "P x") (auto simp: monadic_list_all_def)
qed
lemma monadic_list_ex_RETURN:
"monadic_list_ex (λx. RETURN (P x)) xs = RETURN (list_ex P xs)"
proof (induction xs)
case Nil
then show ?case
by auto
next
case (Cons x xs)
then show ?case
by (cases "P x") (auto simp: monadic_list_ex_def)
qed
lemma monadic_list_ex_RETURN_mono:
assumes "set xs = set ys"
shows "monadic_list_ex (λs. RETURN (P s)) xs ≤ monadic_list_ex (λs. RETURN (P s)) ys"
using assms by (simp add: monadic_list_ex_RETURN list_ex_iff)
lemma monadic_list_ex_nofailI:
assumes "⋀ x. x ∈ set xs ⟹ nofail (f x)"
shows "nofail (monadic_list_ex f xs)"
using assms unfolding monadic_list_ex_def
by - (rule nfoldli_nofail_rule[where ub = "RES UNIV"]; simp add: pw_le_iff)
lemma monadic_list_all_nofailI:
assumes "⋀ x. x ∈ set xs ⟹ nofail (f x)"
shows "nofail (monadic_list_all f xs)"
using assms unfolding monadic_list_all_def
by - (rule nfoldli_nofail_rule[where ub = "RES UNIV"]; simp add: pw_le_iff)
context
fixes xs and g :: "_ ⇒ bool nres"
assumes g_gt_SUCCEED: "⋀x. x ∈ set xs ⟹ g x > SUCCEED"
begin
private lemma nfoldli_gt_SUCCEED: "nfoldli xs c (λx _. g x) a > SUCCEED" for a c
using g_gt_SUCCEED
proof (induction xs arbitrary: a)
case (Cons x xs)
then show ?case
by (cases "g x"; force intro: bind_RES_gt_SUCCEED_I simp: monadic_list_all_def)
qed simp
lemma monadic_list_all_gt_SUCCEED:
"monadic_list_all g xs > SUCCEED"
using nfoldli_gt_SUCCEED unfolding monadic_list_all_def .
lemma monadic_list_ex_gt_SUCCEED:
"monadic_list_ex g xs > SUCCEED"
using nfoldli_gt_SUCCEED unfolding monadic_list_ex_def .
end
lemma monadic_list_ex_is_RETURN:
"∃ r. monadic_list_ex (λx. RETURN (P x)) xs = RETURN r"
proof (induction xs)
case Nil
then show ?case
by auto
next
case (Cons x xs)
then show ?case
by (cases "P x") (auto simp: monadic_list_ex_def)
qed
lemma monadic_list_all_list_ex_is_RETURN:
"∃r. monadic_list_all (λx. monadic_list_ex (λy. RETURN (P x y)) ys) xs = RETURN r"
proof -
let ?f = "λx. SOME r. monadic_list_ex (λy. RETURN (P x y)) ys = RETURN r"
have "monadic_list_all (λx. monadic_list_ex (λy. RETURN (P x y)) ys) xs
= monadic_list_all (λx. RETURN (?f x)) xs"
by (fo_rule arg_cong2; intro HOL.refl monadic_list_ex_is_RETURN ext someI_ex)
then show ?thesis
by (simp add: monadic_list_all_RETURN)
qed
lemma monadic_list_all_mono[refine_mono]:
"monadic_list_all P xs ≤ monadic_list_all Q xs" if "∀ x ∈ set xs. P x ≤ Q x"
proof -
have "nfoldli xs id (λx _. P x) a ≤ nfoldli xs id (λx _. Q x) a" for a
using that by (induction xs arbitrary: a; clarsimp; refine_mono)
then show ?thesis
unfolding monadic_list_all_def .
qed
lemma monadic_list_ex_mono[refine_mono]:
"monadic_list_ex P xs ≤ monadic_list_ex Q xs" if "∀ x ∈ set xs. P x ≤ Q x"
proof -
have "nfoldli xs Not (λx _. P x) a ≤ nfoldli xs Not (λx _. Q x) a" for a
using that by (induction xs arbitrary: a; clarsimp; refine_mono)
then show ?thesis
unfolding monadic_list_ex_def .
qed
paragraph ‹Abstract ‹nres› algorithm›
context Reachability_Invariant_paired_defs
begin
context
fixes P :: "('l × 's) ⇒ bool"
begin
definition "check_prop ≡
do {
xs ← SPEC (λxs. set xs = PR_CONST L);
monadic_list_all (λl. do {
xs ← SPEC (λxs. set xs = PR_CONST M l);
monadic_list_all (λs. RETURN (PR_CONST P (l, s))) xs
}
) xs
}"
lemma check_prop_correct:
"check_prop ≤ SPEC (λr. r ⟷ (∀l ∈ L. ∀s ∈ M l. P (l, s)))"
unfolding check_prop_def
by (refine_vcg monadic_list_all_rule monadic_list_ex_rule) (auto simp: list_all_iff)
end
end
locale Reachability_Impl_base =
Unreachability_Invariant_paired_pre_defs where E = E for E :: "'l × 's ⇒ _" +
fixes succs :: "'l ⇒ 's set ⇒ ('l × 's set) list"
assumes succs_correct:
"⋀l. ∀s ∈ xs. P (l, s)
⟹ {(l', s')| l' ys s'. (l', ys) ∈ set (succs l xs) ∧ s' ∈ ys}
= (⋃ s ∈ xs. Collect (E (l, s)))"
locale Reachability_Impl_invariant =
Reachability_Impl_base where E = E +
Unreachability_Invariant_paired_defs where E = E for E :: "'l × 's ⇒ _"
begin
definition "check_invariant L' ≡
do {
monadic_list_all (λl.
do {
let as = M l;
let succs = succs l as;
monadic_list_all (λ(l', xs).
do {
xs ← SPEC (λxs'. set xs' = xs);
if xs = [] then RETURN True else do {
b1 ← RETURN (l' ∈ L);
ys ← SPEC (λxs. set xs = M l');
b2 ← monadic_list_all (λx.
monadic_list_ex (λy. RETURN (x ≼ y)) ys
) xs;
RETURN (b1 ∧ b2)
}
}
) succs
}
) L'
}
"
definition
"check_invariant_spec L' ≡
∀l ∈ L'. ∀s ∈ M l. ∀l' s'. E (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s'' ∈ M l'. s' ≼ s'')"
definition
"check_invariant_spec_pre L' ≡
∀l ∈ set L'. ∀(l',ys) ∈ set (succs l (M l)). ∀s' ∈ ys. l' ∈ L ∧ (∃s'' ∈ M l'. s' ≼ s'')"
lemma check_invariant_correct_pre:
"check_invariant L' ≤ RETURN (check_invariant_spec_pre L')"
unfolding check_invariant_def check_invariant_spec_pre_def
by (refine_vcg monadic_list_all_rule monadic_list_ex_rule) (auto simp: list_all_iff list_ex_iff)
context
fixes L'
assumes pre: "∀l ∈ L. ∀s ∈ M l. P (l, s)" "set L' ⊆ L"
begin
lemma check_invariant_spec_pre_eq_check_invariant_spec:
"check_invariant_spec_pre L' = check_invariant_spec (set L')"
proof -
have *: "(∀ (l',ys) ∈ set (succs l xs). ∀ s' ∈ ys. l' ∈ L ∧ (∃ s'' ∈ M l'. s' ≼ s'')) =
(∀s∈M l.
∀l' s'.
E (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s''∈M l'. s' ≼ s''))"
if "xs = M l" "l ∈ L"
for l xs
using succs_correct[of xs l] pre(1) that
apply clarsimp
apply safe
apply clarsimp_all
apply fastforce
apply fastforce
subgoal premises prems for a b s'
proof -
from prems have "∀s∈xs. P (l, s)"
by auto
from succs_correct[OF this] prems(3,6,7) obtain s where "s ∈ M l" "E (l, s) (a, s')"
by fastforce
with prems show ?thesis
by auto
qed
apply fastforce
done
then show ?thesis
unfolding check_invariant_spec_def check_invariant_spec_pre_def
by (simp add: * pre(2)[THEN subsetD])
qed
lemma check_invariant_correct_strong:
"check_invariant L' ≤ RETURN (check_invariant_spec (set L'))"
using check_invariant_correct_pre
unfolding check_invariant_spec_pre_eq_check_invariant_spec[symmetric] .
lemma check_invariant_correct:
"check_invariant L' ≤ SPEC (λr. r ⟶ check_invariant_spec (set L'))"
using check_invariant_correct_strong by (rule Orderings.order.trans) simp
end
end
locale Reachability_Impl_base2 =
Reachability_Impl_base where E = E +
Unreachability_Invariant_paired_pre_defs where E = E
for E :: "'l × 's ⇒ _" +
fixes P' and F
assumes P'_P: "⋀ l s. P' (l, s) ⟹ P (l, s)"
assumes F_mono: "⋀a b. P a ⟹ F a ⟹ (λ(l, s) (l', s'). l' = l ∧ s ≼ s') a b ⟹ P b ⟹ F b"
locale Reachability_Impl_pre =
Reachability_Impl_invariant where E = E +
Reachability_Impl_base2 where E = E for E :: "'l × 's ⇒ _"
begin
definition
"check_final ≡ do {
l ← SPEC (λxs. set xs = L);
monadic_list_all (λl. do {
xs ← SPEC (λxs. set xs = M l);
monadic_list_all (λs.
RETURN (¬ F (l, s))
) xs
}
) l
}
"
definition
"check_final_spec = (∀s'∈{(l, s) |l s. l ∈ L ∧ s ∈ M l}. ¬ F s')"
lemma check_final_correct:
"check_final ≤ SPEC (λr. r ⟷ check_final_spec)"
unfolding check_final_def check_final_spec_def
by (refine_vcg monadic_list_all_rule) (auto simp: list_all_iff list_ex_iff)
lemma check_final_nofail:
"nofail check_final"
by (metis check_final_correct nofail_simps(2) pwD1)
definition
"check_init l⇩0 s⇩0 ≡ do {
b1 ← RETURN (l⇩0 ∈ L);
b2 ← RETURN (P' (l⇩0, s⇩0));
xs ← SPEC (λxs. set xs = M l⇩0);
b3 ← monadic_list_ex (λs. RETURN (s⇩0 ≼ s)) xs;
RETURN (b1 ∧ b2 ∧ b3)
}"
definition check_all_pre_alt_def:
"check_all_pre l⇩0 s⇩0 ≡ do {
b1 ← check_init l⇩0 s⇩0;
b2 ← check_prop P';
RETURN (b1 ∧ b2)
}"
lemma check_all_pre_def:
"check_all_pre l⇩0 s⇩0 = do {
b1 ← RETURN (l⇩0 ∈ L);
b2 ← RETURN (P' (l⇩0, s⇩0));
xs ← SPEC (λxs. set xs = M l⇩0);
b3 ← monadic_list_ex (λs. RETURN (s⇩0 ≼ s)) xs;
b4 ← check_prop P';
RETURN (b1 ∧ b2 ∧ b3 ∧ b4)
}"
unfolding check_all_pre_alt_def check_init_def by simp
definition
"check_init_spec l⇩0 s⇩0 ≡ l⇩0 ∈ L ∧ (∃ s' ∈ M l⇩0. s⇩0 ≼ s') ∧ P' (l⇩0, s⇩0)"
definition
"check_all_pre_spec l⇩0 s⇩0 ≡
(∀l ∈ L. ∀s ∈ M l. P' (l, s)) ∧ l⇩0 ∈ L ∧ (∃ s' ∈ M l⇩0. s⇩0 ≼ s') ∧ P' (l⇩0, s⇩0)"
lemma check_all_pre_correct:
"check_all_pre l⇩0 s⇩0 ≤ RETURN (check_all_pre_spec l⇩0 s⇩0)"
unfolding check_all_pre_def check_all_pre_spec_def
by (refine_vcg check_prop_correct monadic_list_ex_rule; standard; auto simp: list_ex_iff)
lemma check_init_correct:
"check_init l⇩0 s⇩0 ≤ RETURN (check_init_spec l⇩0 s⇩0)"
unfolding check_init_def check_init_spec_def
by (refine_vcg monadic_list_ex_rule; standard; auto simp: list_ex_iff)
end
locale Reachability_Impl_pre_start =
Reachability_Impl_pre where E = E for E :: "'l × 's ⇒ _" +
fixes l⇩0 :: 'l and s⇩0 :: 's
begin
definition
"check_all ≡ do {
b ← check_all_pre l⇩0 s⇩0;
if b then SPEC (λr. r ⟶ check_invariant_spec L) else RETURN False
}"
definition
"certify_unreachable = do {
b1 ← check_all;
b2 ← check_final;
RETURN (b1 ∧ b2)
}"
lemma certify_unreachable_alt_def:
"certify_unreachable = do {
b1 ← check_all_pre l⇩0 s⇩0;
b2 ← SPEC (λr. r ⟶ check_invariant_spec L);
b3 ← check_final;
RETURN (b1 ∧ b2 ∧ b3)
}"
unfolding certify_unreachable_def check_all_def
apply simp
apply (fo_rule arg_cong2, auto)
apply (rule ext)
apply simp
by (metis RETURN_rule Refine_Basic.bind_mono(1) dual_order.eq_iff let_to_bind_conv lhs_step_bind nofail_simps(2))
definition
"check_all_spec ≡ check_all_pre_spec l⇩0 s⇩0 ∧ check_invariant_spec L"
lemma check_all_correct:
"check_all ≤ SPEC (λr. r ⟶ check_all_spec)"
unfolding check_all_def check_all_spec_def check_all_pre_def check_all_pre_spec_def
by (refine_vcg check_prop_correct check_invariant_correct monadic_list_ex_rule)
(auto simp: list_ex_iff dest: P'_P)
end
locale Reachability_Impl_correct =
Reachability_Impl_pre_start where E = E +
Unreachability_Invariant_paired_pre where E = E for E :: "'l × 's ⇒ _"
begin
lemma Unreachability_Invariant_pairedI[rule_format]:
"check_all_spec
⟶ Unreachability_Invariant_paired (≼) (≺) M L E P l⇩0 s⇩0 (λ(l, u) (l', u'). l' = l ∧ u ≼ u')"
unfolding check_all_spec_def check_all_pre_spec_def check_invariant_spec_def
by clarsimp (standard, auto dest: P'_P)
lemma check_all_correct':
"check_all ≤ SPEC (λr. r ⟶
Unreachability_Invariant_paired (≼) (≺) M L E P l⇩0 s⇩0 (λ(l, u) (l', u'). l' = l ∧ u ≼ u'))"
by (refine_vcg Unreachability_Invariant_pairedI check_all_correct) fast
lemma certify_unreachableI:
"check_all_spec ∧ check_final_spec ⟶ (∄s'. E⇧*⇧* (l⇩0, s⇩0) s' ∧ F s')"
by (rule impI Unreachability_Invariant_paired.final_unreachable Unreachability_Invariant_pairedI)+
(auto intro: F_mono simp: check_final_spec_def)
lemma certify_unreachable_correct:
"certify_unreachable ≤ SPEC (λr. r ⟶ check_all_spec ∧ check_final_spec)"
unfolding certify_unreachable_def by (refine_vcg check_all_correct check_final_correct; fast)
lemma certify_unreachable_correct':
"certify_unreachable ≤ SPEC (λr. r ⟶ (∄s'. E⇧*⇧* (l⇩0, s⇩0) s' ∧ F s'))"
by (refine_vcg certify_unreachableI[rule_format] certify_unreachable_correct; fast)
end
locale Buechi_Impl_invariant =
Reachability_Impl_base where E = E for E :: "'l × 's ⇒ _" +
fixes L :: "'l set" and M :: "'l ⇒ ('s × nat) set"
begin
definition "check_invariant_buechi R L' ≡
monadic_list_all (λl.
do {
let as = M l;
as ← SPEC (λxs'. set xs' = as);
monadic_list_all (λ(x, i). do {
let succs = succs l {x};
monadic_list_all (λ(l', xs). do {
xs ← SPEC (λxs'. set xs' = xs);
b1 ← RETURN (l' ∈ L);
if xs = [] then RETURN True else do {
ys ← SPEC (λxs. set xs = M l');
b2 ← monadic_list_all (λy.
monadic_list_ex (λ(z, j). RETURN (R l l' i j x y z)) ys
) xs;
RETURN (b1 ∧ b2)
}
}) succs
}) as
}) L'"
definition
"check_invariant_buechi_spec R L' ≡
∀l ∈ L'. ∀(s, i) ∈ M l. ∀l' s'.
E (l, s) (l', s') ⟶ l' ∈ L ∧ (∃(s'', j) ∈ M l'. R l l' i j s s' s'')"
lemma check_invariant_buechi_correct:
"check_invariant_buechi R L' ≤ SPEC (λr. r ⟶ check_invariant_buechi_spec R (set L'))"
(is "_ ≤ ?rhs")
if assms: "∀l ∈ L. ∀(s, _) ∈ M l. P (l, s)" "set L' ⊆ L"
proof -
have *: "
(case x of (s, i) ⇒ ∀x∈set (succs l {s}). case x of (l', ys) ⇒
∀s' ∈ ys. l' ∈ L ∧ (∃(s'', j) ∈ M l'. R l l' i j s s' s'')) =
(case x of (s, i) ⇒
∀l' s'. E (l, s) (l', s') ⟶ l' ∈ L ∧ (∃(s'', j) ∈ M l'. R l l' i j s s' s''))"
if "x ∈ M l" "l ∈ L" for x l using succs_correct[of "{fst x}" l] assms(1) that by fastforce
let ?R = "λl s i l' s'. (∃(s'', j) ∈ M l'. R l l' i j s s' s'')"
let ?Q = "λl s i. λ(l',ys). (∀s' ∈ ys. l' ∈ L ∧ ?R l s i l' s')"
let ?P = "λl (s, i). ∀(l',ys) ∈ set (succs l {s}). ?Q l s i (l', ys)"
have "check_invariant_buechi R L' ≤ SPEC (λr. r ⟷
(∀l ∈ set L'. ∀(s, i) ∈ M l. ∀(l',ys) ∈ set (succs l {s}). (∀s' ∈ ys. l' ∈ L ∧
(∃(s'', j) ∈ M l'. R l l' i j s s' s''))))"
unfolding check_invariant_buechi_def
apply (rule monadic_list_all_rule[unfolded list_all_iff])
apply refine_vcg
subgoal for l xs
apply (refine_vcg monadic_list_all_rule[unfolded list_all_iff, where P = "?P l"])
subgoal for _ s i
apply (refine_vcg monadic_list_all_rule[unfolded list_all_iff, where P = "?Q l s i"])
apply (solves auto)
subgoal for _ l'
apply (refine_vcg monadic_list_all_rule[unfolded list_all_iff, where P = "?R l s i l'"])
subgoal for s'
apply (refine_vcg monadic_list_ex_rule[unfolded list_ex_iff])
by auto
by auto
by auto
by auto
done
also have "… ≤ ?rhs"
unfolding check_invariant_buechi_spec_def by (auto simp: * assms(2)[THEN subsetD])
finally show ?thesis .
qed
end
locale Buechi_Impl_pre =
Buechi_Impl_invariant where M = M +
Reachability_Impl_base2 for M :: "'l ⇒ ('s × nat) set" +
assumes finite: "finite L" "∀l ∈ L. finite (M l)"
begin
definition
"buechi_prop l l' i j s s' s'' ≡ l' ∈ L ∧ s' ≼ s'' ∧
(if F (l, s) then i < j else i ≤ j)"
text ‹
Old alternative definition.
Slightly easier to work with but subsumptions are not deterministic.›
definition
"has_SE ≡ λs l. ∃s' j. s ≼ s' ∧ (s', j) ∈ M l"
definition
"SE ≡ λ(l, s) (l', s'). l' = l ∧ l ∈ L ∧ has_SE s l ∧
(∃j. (s', j) = arg_max (λ(s, i). i) (λ(s', j). s ≼ s' ∧ (s', j) ∈ M l))"
lemma
assumes "SE (l, s) (l', s')"
shows SE_same_loc: "l' = l" and SE_subsumes: "s ≼ s'"
and SE_is_arg_max: "∃j. is_arg_max (λ(s, i). i) (λ(s', j). s ≼ s' ∧ (s', j) ∈ M l) (s', j)"
(is "∃j. is_arg_max ?f ?P (s', j)")
proof -
from assms have "has_SE s l'" "l' ∈ L" and [simp]: "l' = l"
unfolding SE_def by auto
then obtain s1 j where "?P (s1, j)"
unfolding has_SE_def by auto
moreover have "finite (Collect ?P)"
using finite ‹l' ∈ L› by (auto intro: finite_subset)
moreover note arg_max_rule = arg_max_nat_lemma2[of ?P, OF calculation, of "λ(s, i). i"]
then show "l' = l" "s ≼ s'" "∃j. is_arg_max ?f ?P (s', j)"
using assms unfolding is_arg_max_linorder SE_def is_arg_max_linorder by auto
qed
lemma SE_deterministic:
assumes "⋀s. s1 ≼ s ⟷ s2 ≼ s"
assumes "SE (l, s1) (l', s1')" "SE (l, s2) (l', s2')"
shows "s2' = s1'"
using assms(2,3) unfolding SE_def by (clarsimp simp: assms(1)) (metis prod.inject)
lemma SE_I:
assumes "(s'', j) ∈ M l'" "buechi_prop l l' i j s s' s''"
shows "∃(s'', j) ∈ M l'. SE (l', s') (l', s'')"
proof -
let ?P = "λ(s1, j). s' ≼ s1 ∧ (s1, j) ∈ M l'"
let ?f = "λ(s, i). i"
from assms have "?P (s'', j)" "l' ∈ L"
unfolding buechi_prop_def by auto
have "finite (Collect ?P)"
using finite ‹l' ∈ L› by (auto intro: finite_subset)
from arg_max_nat_lemma2[OF ‹?P (s'', j) › this, of ?f] ‹l' ∈ L› show ?thesis
unfolding has_SE_def SE_def is_arg_max_linorder by (auto 4 3)
qed
definition
"check_all_pre_spec1 inits ≡
(∀l ∈ L. ∀s ∈ fst ` M l. P' (l, s)) ∧
(∀(l⇩0, s⇩0) ∈ inits. l⇩0 ∈ L ∧ (∃ (s', _) ∈ M l⇩0. s⇩0 ≼ s') ∧ P' (l⇩0, s⇩0))"
definition
"check_buechi inits ≡ do {
b ← SPEC (λr. r ⟶ check_all_pre_spec1 inits);
if b then do {
ASSERT (check_all_pre_spec1 inits);
SPEC (λr. r ⟶ check_invariant_buechi_spec (buechi_prop ) L)
} else RETURN False
}"
definition
"check_buechi_spec inits ≡
check_all_pre_spec1 inits
∧ (∀l ∈ L. ∀(s, i) ∈ M l. ∀l' s'. E (l, s) (l', s')
⟶ (∃(s'', j) ∈ M l'. buechi_prop l l' i j s s' s''))"
definition
"check_buechi_spec' inits ≡
(∀(l⇩0, s⇩0) ∈ inits. Unreachability_Invariant_paired (≼) (≺) (λl. fst ` M l) L E P l⇩0 s⇩0 SE)
∧ (∀l ∈ L. ∀(s, i) ∈ M l. ∀l' s'. E (l, s) (l', s')
⟶ (∃(s'', j) ∈ M l'. buechi_prop l l' i j s s' s''))"
lemma check_buechi_correct:
"check_buechi inits ≤ SPEC (λr. r ⟶ check_buechi_spec inits)"
unfolding check_buechi_def check_invariant_buechi_spec_def check_buechi_spec_def
by (refine_vcg; blast)
end
locale Buechi_Impl_correct =
Buechi_Impl_pre where M = M and E = E+
Unreachability_Invariant_paired_pre where E = E for E and M :: "'l ⇒ ('s × nat) set"
begin
lemma check_buechi_correct':
"check_buechi inits ≤ SPEC (λr. r ⟶ check_buechi_spec' inits)"
proof -
have "Unreachability_Invariant_paired (≼) (≺) (λl. fst ` M l) L E P l⇩0 s⇩0 SE"
if "(l⇩0, s⇩0) ∈ inits" "check_all_pre_spec1 inits" "check_invariant_buechi_spec (buechi_prop ) L"
for l⇩0 s⇩0
using that unfolding check_invariant_buechi_spec_def check_all_pre_spec1_def
apply -
apply standard
apply (use SE_I SE_same_loc SE_subsumes in
‹auto 4 3 dest!: P'_P simp: list_ex_iff Ball_def_raw Bex_def_raw›)
apply (smt case_prodE fst_conv)
done
then show ?thesis
unfolding check_buechi_def check_invariant_buechi_spec_def check_buechi_spec'_def
by (refine_vcg; blast)
qed
definition f_topo where
"f_topo ≡ λ(l, s). Max {i. (s, i) ∈ M l}"
lemma
assumes "l ∈ L" "(s, i) ∈ M l"
shows f_in: "(s, f_topo (l, s)) ∈ M l" (is "?P1")
and f_ge: "∀j. (s, j) ∈ M l ⟶ j ≤ f_topo (l, s)" (is "?P2")
proof -
have "finite {i. (s, i) ∈ M l}"
using finite ‹l ∈ L› [[simproc add: finite_Collect]] by auto
with assms(2) show ?P1 ?P2
unfolding f_topo_def by (auto intro: Max_ge dest: Max_in)
qed
lemma f_topo:
fixes l :: ‹'l› and s :: ‹'s› and l1 :: ‹'l› and s1 :: ‹'s› and l2 :: ‹'l› and s2 :: ‹'s›
assumes
"check_buechi_spec' inits"
‹l ∈ L› and
‹s ∈ fst ` M l› and
‹l2 ∈ L› and
‹s2 ∈ fst ` M l2› and
‹E (l, s) (l1, s1)› and
‹SE (l1, s1) (l2, s2)›
shows ‹if F (l, s) then f_topo (l, s) < f_topo (l2, s2) else f_topo (l, s) ≤ f_topo (l2, s2)›
proof -
let ?P = "λs l' (s', j). s ≼ s' ∧ (s', j) ∈ M l'"
let ?f = "λ(s, i). i"
let ?le = "λl s i j. if F(l, s) then i < j else i ≤ j"
from ‹SE _ _› obtain j where "(s2, j) ∈ M l2" and [simp]: "l2 = l1"
and is_max: "is_arg_max ?f (?P s1 l1) (s2, j)"
using SE_is_arg_max SE_same_loc SE_subsumes
by atomize_elim (fastforce simp: Lattices_Big.ord_class.is_arg_max_def)
from f_in assms have "(s, f_topo (l, s)) ∈ M l"
by auto
with assms obtain s' i where "(s', i) ∈ M l2" "buechi_prop l l2 (f_topo (l, s)) i s s1 s'"
unfolding check_buechi_spec'_def by fastforce
then have "(s', i) ∈ M l2" "s1 ≼ s'" "?le l s (f_topo (l, s)) i"
unfolding buechi_prop_def by auto
from is_max ‹(s', i) ∈ _› ‹s1 ≼ s'› have "i ≤ j"
unfolding is_arg_max_linorder by simp
also from f_ge ‹(s2, j) ∈ M l2› have "j ≤ f_topo (l2, s2)"
using assms by auto
finally show ?thesis
using ‹?le l s _ _› by auto
qed
lemma no_buechi_run:
assumes check: "check_buechi_spec' inits"
assumes accepting_run:
"(l⇩0, s⇩0) ∈ inits" "Graph_Defs.run E ((l⇩0, s⇩0) ## xs)" "alw (ev (holds F)) ((l⇩0, s⇩0) ## xs)"
shows False
proof -
interpret Unreachability_Invariant_paired "(≼)" "(≺)" "λl. fst ` M l" L E P l⇩0 s⇩0 SE
using check ‹_ ∈ inits› unfolding check_buechi_spec'_def by blast
show ?thesis
apply (rule no_buechi_run[where F = F and f = f_topo])
apply (rule F_mono; assumption)
using finite apply blast+
apply (rule f_topo, rule check, assumption+)
apply (rule accepting_run)+
done
qed
end
locale Reachability_Impl_common =
Reachability_Impl_pre where less_eq = less_eq and M = "λx. case M x of None ⇒ {} | Some S ⇒ S"
for less_eq :: "'b ⇒ 'b ⇒ bool" (infix "≼" 50) and M :: "'k ⇒ 'b set option" +
assumes L_finite: "finite L"
and M_ran_finite: "∀S ∈ ran M. finite S"
and succs_finite: "∀l S. ∀(l', S') ∈ set (succs l S). finite S ⟶ finite S'"
and succs_empty: "⋀l. succs l {} = []"
begin
lemma M_listD:
assumes "M l = Some S"
shows "∃ xs. set xs = S"
using M_ran_finite assms unfolding ran_def by (auto intro: finite_list)
lemma L_listD:
shows "∃ xs. set xs = L"
using L_finite by (rule finite_list)
lemma check_prop_gt_SUCCEED:
"check_prop P' > SUCCEED"
unfolding check_prop_def using L_listD
by (fastforce split: option.split dest: M_listD
intro: monadic_list_all_gt_SUCCEED bind_RES_gt_SUCCEED_I
)
definition
"check_final' 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);
monadic_list_all (λs.
RETURN (¬ PR_CONST F (l, s))
) xs
}
}
) l
}"
lemma check_final_alt_def:
"check_final' L M = check_final"
unfolding check_final'_def check_final_def
by (fo_rule arg_cong2, simp, fo_rule arg_cong) (auto split: option.split simp: bind_RES)
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
}"
lemma check_prop_alt_def:
"check_prop' L M = check_prop P'"
unfolding check_prop_def check_prop'_def
by (fo_rule arg_cong2, simp, fo_rule arg_cong) (auto split: option.split simp: bind_RES)
lemma check_prop'_alt_def:
"check_prop' L' M' = do {
l ← SPEC (λxs. set xs = L');
monadic_list_all (λl. do {
let (S, M) = op_map_extract 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
}"
unfolding check_prop'_def
by (fo_rule arg_cong2, simp, fo_rule arg_cong) (auto split: option.split simp: bind_RES)
end
locale Certification_Impl_base = Reachability_Impl_base2 where less = less
for less :: "'s ⇒ 's ⇒ bool" (infix "≺" 50) +
fixes A :: "'s ⇒ ('si :: heap) ⇒ assn"
and K :: "'k ⇒ ('ki :: {hashable,heap}) ⇒ assn"
and Fi and keyi and Pi and copyi and Lei and succsi
assumes [sepref_fr_rules]: "(keyi,RETURN o PR_CONST fst) ∈ (prod_assn K A)⇧k →⇩a K"
assumes copyi[sepref_fr_rules]: "(copyi, RETURN o COPY) ∈ A⇧k →⇩a A"
assumes Pi_P'[sepref_fr_rules]: "(Pi,RETURN o PR_CONST P') ∈ (prod_assn K A)⇧k →⇩a bool_assn"
assumes Fi_F[sepref_fr_rules]: "(Fi,RETURN o PR_CONST F) ∈ (prod_assn K A)⇧d →⇩a bool_assn"
assumes succsi[sepref_fr_rules]:
"(uncurry succsi,uncurry (RETURN oo PR_CONST succs))
∈ K⇧k *⇩a (lso_assn A)⇧d →⇩a list_assn (K ×⇩a lso_assn A)"
assumes Lei[sepref_fr_rules]:
"(uncurry Lei,uncurry (RETURN oo PR_CONST less_eq)) ∈ A⇧k *⇩a A⇧k →⇩a bool_assn"
assumes pure_K: "is_pure K"
assumes left_unique_K: "IS_LEFT_UNIQUE (the_pure K)"
assumes right_unique_K: "IS_RIGHT_UNIQUE (the_pure K)"
locale Reachability_Impl =
Reachability_Impl_common where M = M +
Certification_Impl_base where K = K and A = A +
Reachability_Impl_correct where M = "λx. case M x of None ⇒ {} | Some S ⇒ S"
for M :: "'k ⇒ 'a set option"
and K :: "'k ⇒ 'ki :: {hashable,heap} ⇒ assn" and A :: "'a ⇒ 'ai :: heap ⇒ assn" +
fixes l⇩0i :: "'ki Heap" and s⇩0i :: "'ai Heap"
assumes l⇩0i_l⇩0[sepref_fr_rules]:
"(uncurry0 l⇩0i, uncurry0 (RETURN (PR_CONST l⇩0))) ∈ unit_assn⇧k →⇩a K"
assumes s⇩0i_s⇩0[sepref_fr_rules]:
"(uncurry0 s⇩0i, uncurry0 (RETURN (PR_CONST s⇩0))) ∈ unit_assn⇧k →⇩a A"
definition
"print_check s b = println (s + STR '': '' + (if b then STR ''passed'' else STR ''failed''))"
definition
"PRINT_CHECK = RETURN oo print_check"
lemma [sepref_import_param]:
"(print_check, print_check) ∈ Id → Id → Id"
by simp
sepref_definition print_check_impl is
"uncurry PRINT_CHECK" :: "id_assn⇧k *⇩a id_assn⇧k →⇩a id_assn"
unfolding PRINT_CHECK_def by sepref
sepref_register PRINT_CHECK
lemmas [sepref_fr_rules] = print_check_impl.refine
paragraph ‹Misc implementation›
sepref_decl_op map_lookup_copy: "λk (m :: _ ⇀ _). (m k, m)"
:: "K → ⟨K,V⟩map_rel → ⟨V⟩option_rel ×⇩r ⟨K,V⟩map_rel"
where "single_valued K" "single_valued (K¯)"
apply (rule fref_ncI)
apply parametricity
unfolding map_rel_def
apply (elim IntE)
apply parametricity
done
definition
"heap_map copy xs ≡ do {
xs ← imp_nfoldli xs (λ_. return True) (λx xs. do {x ← copy x; return (x # xs)}) [];
return (rev xs)
}"
definition
"monadic_map copy xs ≡ do {
xs ← monadic_nfoldli xs (λ_. RETURN True) (λx xs. do {x ← copy x; RETURN (x # xs)}) [];
RETURN (rev xs)
}"
context
begin
private lemma monadic_nfoldli_rev:
"monadic_nfoldli x (λ_. RETURN True) (λx xs. RETURN (x # xs)) [] ≤ SPEC (λr. r = rev x)"
unfolding nfoldli_to_monadic[where c = "λ_.True", symmetric]
by (rule nfoldli_rule[where I = "λ xs ys zs. rev zs @ ys = x"]) auto
private lemma frame2:
"hn_ctxt (list_assn A) x xi * hn_invalid (list_assn A) [] [] * hn_ctxt (list_assn A) xa x'
⟹⇩t hn_ctxt (list_assn A) x xi * hn_ctxt (list_assn A) xa x'"
by (simp add: frame_rem2 frame_rem3)
private lemma frame3:
"hn_ctxt (list_assn A) x xi * hn_invalid (list_assn A) [] []
⟹⇩t hn_ctxt (list_assn A) x xi * hn_ctxt (pure UNIV) xa x'"
by (simp add: frame_rem2 frame_rem3 pure_def entt_fr_drop hn_ctxt_def)
lemma list_rev_aux: "list_assn A a c ⟹⇩A list_assn A (rev a) (rev c)"
apply (subst list_assn_aux_len, clarsimp)
apply (induction rule: list_induct2)
apply (sep_auto; fail)
apply (sep_auto, erule ent_frame_fwd, frame_inference, sep_auto)
done
theorem copy_list_refine:
assumes
copy: "(copy, RETURN o COPY) ∈ A⇧k →⇩a A"
shows
"hn_refine
(hn_ctxt (list_assn A) x xi)
(heap_map copy $ xi)
(hn_ctxt (list_assn A) x xi)
(list_assn A)
(monadic_map (RETURN ∘ COPY) $ x)"
unfolding monadic_map_def heap_map_def
apply sep_auto
apply (rule hnr_bind)
apply (rule monadic_nfoldli_refine_aux'[
where S = "set x" and Rs = "list_assn A" and Rl = A and Rl' = A and Rl'' = A and Γ = emp,
THEN hn_refine_cons_pre[rotated]])
apply sep_auto
subgoal
by standard (sep_auto simp: pure_def)
subgoal
supply [sep_heap_rules] = copy[to_hnr, unfolded hn_refine_def, simplified]
apply standard
apply sep_auto
by (smt assn_times_comm ent_refl ent_star_mono hn_ctxt_def invalidate_clone star_aci(3))
apply (sep_auto; fail)
apply (sep_auto simp: pure_def; fail)
prefer 2
apply (rule frame3; fail)
apply standard
apply sep_auto
apply (drule order_trans, rule monadic_nfoldli_rev)
apply (rule ent_true_drop(2))
apply (rule ent_star_mono)
apply sep_auto
unfolding hn_ctxt_def
apply (rule list_rev_aux)
done
end
lemma monadic_map_refine':
"(heap_map copy, monadic_map (RETURN o COPY)) ∈ (list_assn A)⇧k →⇩a list_assn A"
if "(copy, RETURN o COPY) ∈ A⇧k →⇩a A"
using that by (rule copy_list_refine[to_hfref])
lemma copy_list_COPY:
"monadic_map (RETURN o COPY) = RETURN o COPY" (is "?l = ?r")
proof (rule ext)
fix xs :: "'a list"
have *: "
monadic_nfoldli xs (λ_. RETURN True)
(λx xs. (RETURN ∘ (λx. x)) x ⤜ (λx. RETURN (x # xs))) as
= RETURN (rev xs @ as)" for as
by (induction xs arbitrary: as) auto
show "?l xs = ?r xs"
unfolding monadic_map_def COPY_def by (subst *) simp
qed
lemma copy_list_lso_assn_refine:
"(heap_map copy, RETURN o COPY) ∈ (lso_assn A)⇧k →⇩a lso_assn A"
if "(copy, RETURN o COPY) ∈ A⇧k →⇩a A"
supply [sep_heap_rules] =
monadic_map_refine'[OF that, to_hnr, unfolded copy_list_COPY hn_refine_def hn_ctxt_def, simplified]
unfolding lso_assn_def hr_comp_def by sepref_to_hoare sep_auto
end