Theory Normalized_Zone_Semantics_Impl_Refine
theory Normalized_Zone_Semantics_Impl_Refine
imports
Normalized_Zone_Semantics_Impl Difference_Bound_Matrices.DBM_Operations_Impl_Refine
"HOL-Library.IArray"
HOL.Code_Numeral
Worklist_Algorithms.Worklist_Subsumption_Impl1 Worklist_Algorithms.Unified_PW_Impl
Worklist_Algorithms.Liveness_Subsumption_Impl Worklist_Algorithms.Leadsto_Impl
Normalized_Zone_Semantics_Impl_Semantic_Refinement
Munta_Base.Printing Show.Show_Instances
Munta_Base.Abstract_Term
begin
unbundle no_library_syntax
notation fun_rel_syn (infixr "→" 60)
section ‹Imperative Implementation of Reachability Checking›
subsection ‹Misc›
lemma (in -) rtranclp_equiv:
"R⇧*⇧* x y ⟷ S⇧*⇧* x y" if "⋀ x y. P x ⟹ R x y ⟷ S x y" "⋀ x y. P x ⟹ R x y ⟹ P y" "P x"
proof
assume A: "R⇧*⇧* x y"
note that(1)[iff] that(2)[intro]
from A ‹P x› have "P y ∧ S⇧*⇧* x y"
by induction auto
then show "S⇧*⇧* x y" ..
next
assume A: "S⇧*⇧* x y"
note that(1)[iff] that(2)[intro] rtranclp.intros(2)[intro]
from A ‹P x› have "P y ∧ R⇧*⇧* x y"
by (induction; blast)
then show "R⇧*⇧* x y" ..
qed
lemma (in -) tranclp_equiv:
"R⇧+⇧+ x y ⟷ S⇧+⇧+ x y" if "⋀ x y. P x ⟹ R x y ⟷ S x y" "⋀ x y. P x ⟹ R x y ⟹ P y" "P x"
proof
assume A: "R⇧+⇧+ x y"
note that(1)[iff] that(2)[intro]
from A ‹P x› have "P y ∧ S⇧+⇧+ x y"
by induction auto
then show "S⇧+⇧+ x y" ..
next
assume A: "S⇧+⇧+ x y"
note that(1)[iff] that(2)[intro] tranclp.intros(2)[intro]
from A ‹P x› have "P y ∧ R⇧+⇧+ x y"
by (induction; blast)
then show "R⇧+⇧+ x y" ..
qed
lemma (in -) rtranclp_tranclp_equiv:
"R⇧*⇧* x y ∧ R⇧+⇧+ y z ⟷ S⇧*⇧* x y ∧ S⇧+⇧+ y z" if
"⋀ x y. P x ⟹ R x y ⟷ S x y" "⋀ x y. P x ⟹ R x y ⟹ P y" "P x"
proof
assume A: "R⇧*⇧* x y ∧ R⇧+⇧+ y z"
note that(1)[iff] that(2)[intro]
from A[THEN conjunct1] ‹P x› have "P y"
by induction auto
then show "S⇧*⇧* x y ∧ S⇧+⇧+ y z"
using rtranclp_equiv[of P R S x y, OF that] tranclp_equiv[of P R S y z, OF that(1,2)] A
by fastforce
next
assume A: "S⇧*⇧* x y ∧ S⇧+⇧+ y z"
note that(1)[iff] that(2)[intro]
from A[THEN conjunct1] ‹P x› have "P y"
by induction auto
then show "R⇧*⇧* x y ∧ R⇧+⇧+ y z"
using rtranclp_equiv[of P R S x y, OF that] tranclp_equiv[of P R S y z, OF that(1,2)] A
by force
qed
subsection ‹Mapping Transitions and Invariants›
type_synonym
('a, 'c, 'time, 's) transition_fun = "'s ⇒ (('c, 'time) cconstraint * 'a * 'c list * 's) list"
definition transition_rel where
"transition_rel X = {(f, r). ∀ l ∈ X. ∀ x. (l, x) ∈ r ⟷ x ∈ set (f l)}"
definition inv_rel where
"inv_rel R X = b_rel R (λ x. x ∈ X) → Id"
lemma transition_rel_anti_mono:
"transition_rel S ⊆ transition_rel R" if "R ⊆ S"
using that unfolding transition_rel_def by auto
lemma inv_rel_anti_mono:
"inv_rel A S ⊆ inv_rel A R" if "R ⊆ S"
using that unfolding inv_rel_def fun_rel_def b_rel_def by auto
definition state_set :: "('a, 'c, 'time, 's) transition set ⇒ 's set" where
"state_set T = fst ` T ∪ (snd o snd o snd o snd) ` T"
definition
"trace_level (i :: int) (f :: unit ⇒ String.literal Heap) = ()"
locale Show_State_Defs =
fixes n :: nat and show_state :: "'si ⇒ string" and show_clock :: "nat ⇒ string"
begin
definition
"tracei type ≡ λ (l, M).
let _ = trace_level 5 (
λ_. do {
let st = show_state l;
m ← show_dbm_impl n show_clock show M;
let s = type @ '': ('' @ st @ '', <'' @ m @ ''>)'';
let s = String.implode s;
return s
})
in return ()
"
end
locale TA_Impl_No_Ceiling_Defs =
Show_State_Defs n show_state +
TA_Start_No_Ceiling_Defs A l⇩0 n
for show_state :: "'si :: {hashable, heap} ⇒ string"
and A :: "('a, nat, int, 's) ta" and l⇩0 :: 's and n :: nat +
fixes trans_fun :: "('a, nat, int, 's) transition_fun"
and inv_fun :: "(nat, int, 'si :: {hashable, heap}) invassn"
and trans_impl :: "('a, nat, int, 'si) transition_fun"
and l⇩0i :: 'si
begin
abbreviation "states ≡ {l⇩0} ∪ (state_set (trans_of A))"
end
locale TA_Impl_Defs =
TA_Start_Defs A l⇩0 n k +
TA_Impl_No_Ceiling_Defs show_clock show_state A l⇩0 n trans_fun inv_fun trans_impl l⇩0i
for show_clock and show_state :: "'si :: {hashable, heap} ⇒ string"
and A :: "('a, nat, int, 's) ta" and l⇩0 :: 's and n :: nat and k
and trans_fun inv_fun trans_impl l⇩0i
+
fixes ceiling :: "'si ⇒ int iarray"
begin
definition "inv_of_A = inv_of A"
end
locale Reachability_Problem_Impl_Defs =
Reachability_Problem_Defs A l⇩0 n k F +
TA_Impl_No_Ceiling_Defs show_clock show_state A l⇩0 n trans_fun inv_fun trans_impl l⇩0i
for show_clock and show_state :: "'si :: {hashable, heap} ⇒ string"
and A :: "('a, nat, int, 's) ta" and l⇩0 :: 's and n :: nat and k and F :: "'s ⇒ bool"
and trans_fun inv_fun trans_impl and l⇩0i
+
fixes F_fun :: "'si ⇒ bool"
begin
end
definition "FWI'' n M = FWI' M n"
lemma fwi_impl'_refine_FWI'':
"(fwi_impl' n, RETURN oo PR_CONST (λ M. FWI'' n M)) ∈ Id → Id → ⟨Id⟩ nres_rel"
unfolding FWI''_def by (rule fwi_impl'_refine_FWI')
lemmas fwi_impl_refine_FWI'' = fwi_impl.refine[FCOMP fwi_impl'_refine_FWI'']
context
fixes n :: nat
begin
context
notes [map_type_eqs] = map_type_eqI[of "TYPE(nat * nat ⇒ 'e)" "TYPE('e i_mtx)"]
begin
sepref_register "PR_CONST (FWI'' n)"
end
lemmas [sepref_fr_rules] = fwi_impl_refine_FWI''
lemma [def_pat_rules]: "FWI'' $ n ≡ UNPROTECT (FWI'' n)" by simp
sepref_definition repair_pair_impl is
"uncurry2 (RETURN ooo PR_CONST (repair_pair n))" ::
"[λ ((_,a),b). a ≤ n ∧ b ≤ n]⇩a (mtx_assn n)⇧d *⇩a nat_assn⇧k *⇩a nat_assn⇧k → mtx_assn n"
unfolding repair_pair_def FWI''_def[symmetric] PR_CONST_def
by sepref
sepref_register repair_pair
lemmas [sepref_fr_rules] = repair_pair_impl.refine
end
locale TA_Impl_No_Ceiling =
TA_Impl_No_Ceiling_Defs _ _ A l⇩0 n trans_fun inv_fun trans_impl l⇩0i +
TA_Start_No_Ceiling A l⇩0 n
for A :: "('a, nat, int, 's) ta"
and l⇩0 :: 's
and n :: nat
and trans_fun inv_fun
and trans_impl :: "('a, nat, int, 'si :: {hashable, heap}) transition_fun"
and l⇩0i
+
fixes states' and loc_rel :: "('si × 's) set"
assumes trans_fun: "(trans_fun, trans_of A) ∈ transition_rel states'"
and trans_impl:
"(trans_impl, trans_fun) ∈ fun_rel_syn loc_rel (list_rel (Id ×⇩r Id ×⇩r Id ×⇩r loc_rel))"
and inv_fun: "(inv_fun, inv_of A) ∈ inv_rel loc_rel states'"
and states'_states: "states ⊆ states'"
and init_impl: "(l⇩0i, l⇩0) ∈ loc_rel"
and loc_rel_left_unique:
"⋀l li li'. l ∈ states' ⟹ (li, l) ∈ loc_rel ⟹ (li', l) ∈ loc_rel ⟹ li' = li"
and loc_rel_right_unique:
"⋀l l' li. l ∈ states' ⟹ l' ∈ states' ⟹ (li,l) ∈ loc_rel ⟹ (li,l') ∈ loc_rel
⟹ l' = l"
begin
lemma trans_fun':
"(trans_fun, trans_of A) ∈ transition_rel states"
using transition_rel_anti_mono[OF states'_states] trans_fun by blast
lemma inv_fun': "(inv_fun, inv_of A) ∈ inv_rel loc_rel states"
using inv_fun inv_rel_anti_mono[OF states'_states] by blast
abbreviation "location_rel ≡ b_rel loc_rel (λ x. x ∈ states')"
abbreviation "location_assn ≡ pure location_rel"
abbreviation "state_assn ≡ prod_assn id_assn (mtx_assn n)"
abbreviation "state_assn' ≡ prod_assn location_assn (mtx_assn n)"
interpretation DBM_Impl n .
abbreviation
"op_impl_assn ≡
location_assn⇧k *⇩a (list_assn clock_assn)⇧k *⇩a
(list_assn (acconstraint_assn clock_assn id_assn))⇧k *⇩a location_assn⇧k *⇩a mtx_assn⇧d →⇩a mtx_assn"
lemma tracei_refine:
"(uncurry tracei, uncurry (λ_ _. RETURN ())) ∈ id_assn⇧k *⇩a state_assn'⇧k →⇩a unit_assn"
unfolding tracei_def
using show_dbm_impl.refine[to_hnr, unfolded hn_refine_def, of n]
by sepref_to_hoare sep_auto
end
locale TA_Impl =
TA_Impl_Defs _ _ A l⇩0 n k trans_fun inv_fun trans_impl l⇩0i ceiling +
TA_Impl_No_Ceiling _ _ A l⇩0 n trans_fun inv_fun trans_impl l⇩0i states' loc_rel +
TA_Start A l⇩0 n k
for A :: "('a, nat, int, 's) ta"
and l⇩0 :: 's
and n :: nat
and k
and trans_fun inv_fun
and trans_impl :: "('a, nat, int, 'si :: {hashable, heap}) transition_fun"
and l⇩0i
and ceiling
and states' and loc_rel :: "('si × 's) set"
+
assumes ceiling: "(ceiling, IArray o k') ∈ inv_rel loc_rel states'"
begin
lemma ceiling': "(ceiling, IArray o k') ∈ inv_rel loc_rel states"
using ceiling inv_rel_anti_mono[OF states'_states] by blast
end
locale Reachability_Problem_Impl =
Reachability_Problem_Impl_Defs _ _ A l⇩0 n k F trans_fun inv_fun trans_impl l⇩0i +
TA_Impl _ _ A l⇩0 n k trans_fun inv_fun trans_impl l⇩0i ceiling states' loc_rel +
Reachability_Problem A l⇩0 n k F
for A :: "('a, nat, int, 's) ta"
and l⇩0 :: 's
and n :: nat
and k
and F
and trans_fun inv_fun
and trans_impl :: "('a, nat, int, 'si :: {hashable, heap}) transition_fun"
and l⇩0i
and ceiling
and states' and loc_rel :: "('si × 's) set" +
assumes F_fun: "(F_fun, F) ∈ inv_rel loc_rel states'"
begin
lemma F_fun': "(F_fun, F) ∈ inv_rel loc_rel states"
using F_fun inv_rel_anti_mono[OF states'_states] by blast
end
context Search_Space_finite
begin
sublocale liveness_search_space_pre:
Liveness_Search_Space_pre "λ x y. E x y ∧ F x ∧ F y ∧ ¬ empty y" a⇩0 F "(≼)"
"λ v. reachable v ∧ ¬ empty v ∧ F v"
using finite_reachable apply -
apply (standard)
apply (blast intro: finite_subset[rotated] F_mono trans)
apply (blast intro: finite_subset[rotated] F_mono trans)
subgoal
by safe (blast dest: mono F_mono empty_mono)
apply (blast intro: finite_subset[rotated] F_mono trans)
apply (blast intro: finite_subset[rotated] F_mono trans)
done
end
locale TA_Impl_Op =
TA_Impl _ _ A l⇩0 n k trans_fun inv_fun trans_impl l⇩0i ceiling states' loc_rel
+ op: E_From_Op_Bisim A l⇩0 n k f
for A and l⇩0 :: 's and n k
and f trans_fun inv_fun trans_impl and l⇩0i :: "'si:: {hashable,heap}"
and ceiling states' loc_rel
+
fixes op_impl
assumes op_impl: "(uncurry4 op_impl, uncurry4 (λ l r. RETURN ooo f l r)) ∈ op_impl_assn"
locale Reachability_Problem_Impl_Op =
TA_Impl_Op _ _ A l⇩0 n k f trans_fun inv_fun trans_impl l⇩0i ceiling states' loc_rel
+ Reachability_Problem_Impl _ _ _ A l⇩0 n k _ trans_fun inv_fun trans_impl l⇩0i ceiling states' loc_rel
+ op: E_From_Op_Bisim_Finite_Reachability A l⇩0 n k f
for A and l⇩0 :: 's and n k
and f trans_fun inv_fun trans_impl and l⇩0i :: "'si:: {hashable,heap}"
and ceiling states' loc_rel
subsection ‹Implementing of the Successor Function›
paragraph ‹Shared Setup›
context TA_Impl
begin
interpretation DBM_Impl n .
context
notes [map_type_eqs] = map_type_eqI[of "TYPE(nat * nat ⇒ 'e)" "TYPE('e i_mtx)"]
begin
sepref_register trans_impl
sepref_register abstr_upd up_canonical_upd norm_upd reset'_upd reset_canonical_upd
sepref_register "PR_CONST (FW'' n)"
sepref_register "PR_CONST (inv_of_A)"
end
lemmas [sepref_fr_rules] = fw_impl.refine[FCOMP fw_impl'_refine_FW'']
lemma [def_pat_rules]: "FW'' $ n ≡ UNPROTECT (FW'' n)" by simp
lemma trans_impl_clock_bounds3:
"∀ c ∈ collect_clks (inv_of A l). c ≤ n"
using collect_clks_inv_clk_set[of A l] clocks_n by force
lemma inv_fun_rel:
assumes "l ∈ states'" "(l1, l) ∈ loc_rel"
shows "(inv_fun l1, inv_of A l) ∈ ⟨⟨nbn_rel (Suc n), int_rel⟩acconstraint_rel⟩list_rel"
proof -
have "(xs, xs) ∈ ⟨⟨nbn_rel (Suc n), int_rel⟩acconstraint_rel⟩list_rel"
if "∀ c ∈ collect_clks xs. c ≤ n" for xs
using that
apply (induction xs)
apply simp
apply simp
subgoal for a
apply (cases a)
by (auto simp: acconstraint_rel_def p2rel_def rel2p_def)
done
moreover have
"inv_fun l1 = inv_of A l"
using inv_fun assms unfolding inv_rel_def b_rel_def fun_rel_def by auto
ultimately show ?thesis using trans_impl_clock_bounds3 by auto
qed
lemma [sepref_fr_rules]:
"(return o inv_fun, RETURN o PR_CONST inv_of_A)
∈ location_assn⇧k →⇩a list_assn (acconstraint_assn clock_assn int_assn)"
using inv_fun_rel
apply (simp add: b_assn_pure_conv aconstraint_assn_pure_conv list_assn_pure_conv inv_of_A_def)
by sepref_to_hoare (sep_auto simp: pure_def)
lemma [sepref_fr_rules]:
"(return o ceiling, RETURN o PR_CONST k') ∈ location_assn⇧k →⇩a iarray_assn"
using ceiling by sepref_to_hoare (sep_auto simp: inv_rel_def fun_rel_def br_def)
sepref_register "PR_CONST k'"
lemma [def_pat_rules]: "(TA_Start_Defs.k' $ n $ k) ≡ PR_CONST k'" by simp
lemma [simp]:
"length (k' l) > n"
by (simp add: k'_def)
lemma [def_pat_rules]: "(TA_Impl_Defs.inv_of_A $ A) ≡ PR_CONST inv_of_A" by simp
lemma reset_canonical_upd_impl_refine:
"(uncurry3 (reset_canonical_upd_impl n), uncurry3 (λx. RETURN ∘∘∘ reset_canonical_upd x))
∈ [λ(((_, i), j), _).
i ≤ n ∧
j ≤ n]⇩a mtx_assn⇧d *⇩a nat_assn⇧k *⇩a clock_assn⇧k *⇩a id_assn⇧k → mtx_assn"
apply sepref_to_hnr
apply (rule hn_refine_preI)
apply (rule hn_refine_cons[OF _ reset_canonical_upd_impl.refine[to_hnr], simplified])
by (sep_auto simp: hn_ctxt_def b_assn_def entailst_def)+
lemmas [sepref_fr_rules] =
abstr_upd_impl.refine up_canonical_upd_impl.refine norm_upd_impl.refine
reset_canonical_upd_impl_refine
lemma constraint_clk_acconstraint_rel_simps:
assumes "(ai, a) ∈ ⟨nbn_rel (Suc n), id_rel⟩acconstraint_rel"
shows "constraint_clk a < Suc n" "constraint_clk ai = constraint_clk a"
using assms by (cases ai; cases a; auto simp: acconstraint_rel_def p2rel_def rel2p_def)+
lemma [sepref_fr_rules]:
"(return o constraint_clk, RETURN o constraint_clk)
∈ (acconstraint_assn clock_assn id_assn)⇧k →⇩a clock_assn"
apply (simp add: b_assn_pure_conv aconstraint_assn_pure_conv)
by sepref_to_hoare (sep_auto simp: pure_def constraint_clk_acconstraint_rel_simps)
sepref_register constraint_clk
sepref_register
"repair_pair n :: ((nat × nat ⇒ ('b :: {linordered_cancel_ab_monoid_add}) DBMEntry)) ⇒ _" ::
"(('ee DBMEntry) i_mtx) ⇒ nat ⇒ nat ⇒ ((nat × nat ⇒ 'ee DBMEntry))"
sepref_register abstra_upd :: "(nat, 'e) acconstraint ⇒ 'e DBMEntry i_mtx ⇒ 'e DBMEntry i_mtx"
sepref_register n
lemmas [sepref_import_param] = IdI[of n]
sepref_definition abstra_repair_impl is
"uncurry (RETURN oo PR_CONST abstra_repair)" ::
"(acconstraint_assn clock_assn id_assn)⇧k *⇩a mtx_assn⇧d →⇩a mtx_assn"
unfolding abstra_repair_def PR_CONST_def by sepref
sepref_register abstra_repair :: "(nat, 'e) acconstraint ⇒ 'e DBMEntry i_mtx ⇒ 'e DBMEntry i_mtx"
lemmas [sepref_fr_rules] = abstra_repair_impl.refine
sepref_definition abstr_repair_impl is
"uncurry (RETURN oo PR_CONST abstr_repair)" ::
"(list_assn (acconstraint_assn clock_assn id_assn))⇧k *⇩a mtx_assn⇧d →⇩a mtx_assn"
unfolding abstr_repair_def PR_CONST_def by sepref
sepref_register abstr_repair ::
"(nat, 'e) acconstraint list ⇒ 'e DBMEntry i_mtx ⇒ 'e DBMEntry i_mtx"
lemmas [sepref_fr_rules] = abstr_repair_impl.refine
end
paragraph ‹Implementation for an Arbitrary DBM Successor Operation›
context Reachability_Problem_Impl
begin
lemma F_rel_alt_def:
"F_rel = (λ (l, M). F l ∧ ¬ check_diag n M)"
unfolding F_rel_def by auto
sepref_register F
lemma [sepref_fr_rules]:
"(return o F_fun, RETURN o F) ∈ location_assn⇧k →⇩a id_assn"
using F_fun by sepref_to_hoare (sep_auto simp: inv_rel_def b_rel_def fun_rel_def)
sepref_definition F_impl is
"RETURN o (λ (l, M). F l)" :: "state_assn'⇧k →⇩a bool_assn"
by sepref
end
context TA_Impl_Op
begin
definition succs where
"succs ≡ λ (l, D). rev (map (λ (g,a,r,l'). (l', f l r g l' D)) (trans_fun l))"
definition succs_P where
"succs_P P ≡ λ (l, D).
rev (map (λ (g,a,r,l'). (l', f l r g l' D)) (filter (λ (g,a,r,l'). P l') (trans_fun l)))"
definition succs' where
"succs' ≡ λ (l, D). do
{
xs ← nfoldli (trans_fun l) (λ _. True) (λ (g,a,r,l') xs.
RETURN ((l', f l r g l' (op_mtx_copy D)) # xs)
) [];
RETURN xs
}"
definition succs_P' where
"succs_P' P ≡ λ (l, D). do
{
xs ← nfoldli (trans_fun l) (λ _. True) (λ (g,a,r,l') xs.
RETURN (if P l' then (l', f l r g l' (op_mtx_copy D)) # xs else xs)
) [];
RETURN xs
}"
lemma RETURN_split:
"RETURN (f a b) = do
{
a ← RETURN a;
b ← RETURN b;
RETURN (f a b)
}"
by simp
lemma succs'_succs:
"succs' lD = RETURN (succs lD)"
unfolding succs'_def succs_def rev_map_fold
apply (cases lD)
apply simp
apply (rewrite fold_eq_nfoldli)
apply (fo_rule arg_cong fun_cong)+
apply auto
done
lemma succs_P'_succs_P:
"succs_P' P lD = RETURN (succs_P P lD)"
unfolding succs_P'_def succs_P_def rev_map_fold fold_filter
apply (cases lD)
apply simp
apply (rewrite fold_eq_nfoldli)
apply (fo_rule arg_cong fun_cong)+
by auto
lemmas [sepref_fr_rules] = dbm_subset'_impl.refine
sepref_register "PR_CONST (dbm_subset' n)" :: "'e DBMEntry i_mtx ⇒ 'e DBMEntry i_mtx ⇒ bool"
lemma [def_pat_rules]:
"dbm_subset' $ n ≡ PR_CONST (dbm_subset' n)"
by simp
lemmas [sepref_fr_rules] = check_diag_impl.refine
sepref_register "PR_CONST (check_diag n)" :: "'e DBMEntry i_mtx ⇒ bool"
lemma [def_pat_rules]:
"check_diag $ n ≡ PR_CONST (check_diag n)"
by simp
definition
"subsumes' =
(λ (l, M :: ('tt :: {zero,linorder}) DBM') (l', M').
l = l' ∧ pointwise_cmp (≤) n (curry M) (curry M'))"
context
begin
notation fun_rel_syn (infixr "→" 60)
lemma left_unique_location_rel:
"IS_LEFT_UNIQUE location_rel"
unfolding IS_LEFT_UNIQUE_def
by (rule single_valuedI) (auto intro: loc_rel_left_unique single_valuedI)
lemma right_unique_location_rel:
"IS_RIGHT_UNIQUE location_rel"
by (rule single_valuedI) (auto intro: loc_rel_right_unique)
lemma [sepref_import_param]:
"((=), (=)) ∈ location_rel → location_rel → Id"
using left_unique_location_rel right_unique_location_rel
by (blast dest: IS_LEFT_UNIQUED IS_RIGHT_UNIQUED)
sepref_definition subsumes_impl is
"uncurry (RETURN oo subsumes')" :: "state_assn'⇧k *⇩a state_assn'⇧k →⇩a bool_assn"
unfolding subsumes'_def short_circuit_conv dbm_subset'_def[symmetric]
by sepref
end
lemma init_dbm_alt_def:
"init_dbm = op_amtx_dfltNxM (Suc n) (Suc n) (Le 0)"
unfolding init_dbm_def op_amtx_dfltNxM_def neutral by auto
lemma [sepref_import_param]: "(Le 0, PR_CONST (Le 0)) ∈ Id" by simp
lemma [def_pat_rules]: "Le $ 0 ≡ PR_CONST (Le 0)" by simp
sepref_register "PR_CONST (Le 0)"
sepref_definition init_dbm_impl is
"uncurry0 (RETURN (init_dbm :: nat × nat ⇒ _))" :: "unit_assn⇧k →⇩a (mtx_assn n)"
unfolding init_dbm_alt_def by sepref
lemmas [sepref_fr_rules] = init_dbm_impl.refine
sepref_register l⇩0
lemma [sepref_import_param]:
"(l⇩0i, l⇩0) ∈ location_rel"
using init_impl states'_states by auto
sepref_definition a⇩0_impl is
"uncurry0 (RETURN a⇩0)" :: "unit_assn⇧k →⇩a state_assn'"
unfolding a⇩0_def by sepref
lemma trans_impl_trans_of[intro]:
"(g, a, r, l') ∈ set (trans_fun l) ⟹ l ∈ states' ⟹ A ⊢ l ⟶⇗g,a,r⇖ l'"
using trans_fun unfolding transition_rel_def by auto
lemma trans_of_trans_impl[intro]:
"A ⊢ l ⟶⇗g,a,r⇖ l' ⟹ l ∈ states' ⟹ (g, a, r, l') ∈ set (trans_fun l)"
using trans_fun unfolding transition_rel_def by auto
lemma trans_impl_clock_bounds1:
"(g, a, r, l') ∈ set (trans_fun l) ⟹ l ∈ states' ⟹ ∀ c ∈ set r. c ≤ n"
using clocks_n reset_clk_set[OF trans_impl_trans_of] by fastforce
lemma trans_impl_clock_bounds2:
"(g, a, r, l') ∈ set (trans_fun l) ⟹ l ∈ states' ⟹ ∀ c ∈ collect_clks g. c ≤ n"
using clocks_n collect_clocks_clk_set[OF trans_impl_trans_of] by fastforce
lemma trans_impl_states:
"(g, a, r, l') ∈ set (trans_fun l) ⟹ l ∈ states' ⟹ l' ∈ state_set (trans_of A)"
apply (drule trans_impl_trans_of)
apply assumption
unfolding state_set_def
apply (rule UnI2)
by force
lemma trans_impl_states':
"(g, a, r, l') ∈ set (trans_fun l) ⟹ l ∈ states' ⟹ l' ∈ states'"
using trans_impl_states states'_states by auto
lemma trans_of_states[intro]:
"l' ∈ states" if "A ⊢ l ⟶⇗g,a,r⇖ l'" "l ∈ states'"
using that by (auto intro: trans_impl_states)
lemma trans_of_states'[intro]:
"l' ∈ states'" if "A ⊢ l ⟶⇗g,a,r⇖ l'" "l ∈ states'"
using that states'_states by (auto intro: trans_impl_states)
abbreviation "clock_rel ≡ nbn_rel (Suc n)"
lemma [sepref_import_param]:
"(trans_impl, trans_fun)
∈ location_rel →
⟨⟨⟨clock_rel, int_rel⟩ acconstraint_rel⟩ list_rel ×⇩r Id ×⇩r ⟨clock_rel⟩ list_rel ×⇩r location_rel⟩
list_rel"
proof (rule fun_relI)
fix li l
assume "(li, l) ∈ location_rel"
{ fix xs :: "((nat, int) acconstraint list × 'a × nat list × 's) list"
and xs' :: "((nat, int) acconstraint list × 'a × nat list × 'si) list"
assume A:
"∀ g a r l'. (g, a, r, l') ∈ set xs
⟶ (∀ c ∈ collect_clks g. c ≤ n) ∧ (∀ c ∈ set r. c ≤ n) ∧ l' ∈ states'"
assume "(xs', xs) ∈ ⟨Id ×⇩r Id ×⇩r Id ×⇩r loc_rel⟩list_rel"
then have
"(xs', xs) ∈
⟨⟨⟨clock_rel, int_rel⟩acconstraint_rel⟩list_rel
×⇩r Id
×⇩r ⟨clock_rel⟩list_rel
×⇩r location_rel
⟩list_rel"
using A
proof (induction xs' xs)
case 1 then show ?case
by simp
next
case (2 x' x xs' xs)
obtain g a r l' where [simp]: "x = (g, a, r, l')"
by (cases x)
obtain gi ai ri l'i where [simp]: "x' = (gi, ai, ri, l'i)"
by (cases x')
from 2 have r_bounds: "∀ c ∈ set r. c ≤ n"
by auto
from 2 have "∀ c ∈ collect_clks g. c ≤ n"
by auto
then have "(g, g) ∈ ⟨⟨nbn_rel (Suc n), int_rel⟩acconstraint_rel⟩list_rel"
apply (induction g; simp)
subgoal for a
by (cases a)
(auto simp: acconstraint_rel_def p2rel_def rel2p_def split: acconstraint.split)
done
moreover from r_bounds have "(r, r) ∈ ⟨nbn_rel (Suc n)⟩list_rel"
by (induction r) auto
moreover from 2(1,4) have "(l'i, l') ∈ location_rel"
by auto
ultimately have
"(x', x) ∈
⟨⟨clock_rel, int_rel⟩acconstraint_rel⟩list_rel ×⇩r Id ×⇩r ⟨clock_rel⟩list_rel ×⇩r location_rel"
using 2(1) by simp
moreover from 2 have
"(xs', xs)
∈ ⟨⟨⟨clock_rel, int_rel⟩acconstraint_rel⟩list_rel ×⇩r Id
×⇩r ⟨clock_rel⟩list_rel ×⇩r location_rel⟩list_rel"
by force
ultimately show ?case by simp
qed
} note * = this
from
‹(li, l) ∈ _› trans_impl_clock_bounds1 trans_impl_clock_bounds2 trans_impl_states' trans_impl
show "(trans_impl li, trans_fun l)
∈ ⟨⟨⟨clock_rel, int_rel⟩acconstraint_rel⟩list_rel ×⇩r
Id ×⇩r ⟨clock_rel⟩list_rel ×⇩r location_rel⟩list_rel"
by - (rule *, auto, (drule fun_relD, assumption, simp add: relAPP_def)+)
qed
lemma b_rel_subtype[sepref_frame_match_rules]:
"hn_val (b_rel R P) a b ⟹⇩t hn_val R a b"
by (rule enttI) (sep_auto simp: hn_ctxt_def pure_def)
lemma b_rel_subtype_merge[sepref_frame_merge_rules]:
"hn_val (b_rel R p) a b ∨⇩A hn_val R a b ⟹⇩t hn_val R a b"
"hn_val R a b ∨⇩A hn_val (b_rel R p) a b ⟹⇩t hn_val R a b"
by (simp add: b_rel_subtype entt_disjE)+
lemmas [safe_constraint_rules] = CN_FALSEI[of is_pure "asmtx_assn n a" for a]
sepref_register f ::
"'s ⇒ nat list ⇒ (nat, int) acconstraint list ⇒ 's ⇒ int DBMEntry i_mtx ⇒ int DBMEntry i_mtx"
lemmas [sepref_fr_rules] = op_impl
context
notes [id_rules] = itypeI[of "PR_CONST n" "TYPE (nat)"]
and [sepref_import_param] = IdI[of n]
begin
sepref_register trans_fun
sepref_definition succs_impl is
"RETURN o PR_CONST succs" :: "state_assn'⇧k →⇩a list_assn state_assn'"
unfolding PR_CONST_def
unfolding
comp_def succs'_succs[symmetric] succs'_def
FW''_def[symmetric] rev_map_fold inv_of_A_def[symmetric]
apply (rewrite "HOL_list.fold_custom_empty")
by sepref
sepref_register succs :: "'s × (int DBMEntry i_mtx) ⇒ ('s × (int DBMEntry i_mtx)) list"
lemmas [sepref_fr_rules] = succs_impl.refine
sepref_definition succs_impl' is
"RETURN o (filter (λ (l, M). ¬check_diag n M) o succs)" :: "state_assn'⇧k →⇩a list_assn state_assn'"
apply (rewrite in succs PR_CONST_def[symmetric])
unfolding list_filter_foldli
apply (rewrite "HOL_list.fold_custom_empty")
by sepref
end
context
fixes P :: "'s ⇒ bool" and P_fun
assumes P_fun: "(P_fun, P) ∈ inv_rel loc_rel states'"
begin
context
notes [id_rules] = itypeI[of "PR_CONST n" "TYPE (nat)"]
and [sepref_import_param] = IdI[of n]
begin
sepref_register "PR_CONST P"
lemma [sepref_fr_rules]:
"(return o P_fun, RETURN o PR_CONST P) ∈ location_assn⇧k →⇩a id_assn"
using P_fun by sepref_to_hoare (sep_auto simp: inv_rel_def b_rel_def fun_rel_def)
sepref_definition succs_P_impl is
"RETURN o PR_CONST (succs_P P)" :: "state_assn'⇧k →⇩a list_assn state_assn'"
unfolding PR_CONST_def
apply (rewrite in P PR_CONST_def[symmetric])
unfolding
comp_def succs_P'_succs_P[symmetric] succs_P'_def
FW''_def[symmetric] rev_map_fold inv_of_A_def[symmetric]
apply (rewrite "HOL_list.fold_custom_empty")
by sepref
sepref_register "succs_P P" :: "'s × (int DBMEntry i_mtx) ⇒ ('s × (int DBMEntry i_mtx)) list"
lemmas [sepref_fr_rules] = succs_P_impl.refine
sepref_definition succs_P_impl' is
"RETURN o (filter (λ (l, M). ¬check_diag n M) o succs_P P)" :: "state_assn'⇧k →⇩a list_assn state_assn'"
apply (rewrite in "succs_P P" PR_CONST_def[symmetric])
unfolding list_filter_foldli
apply (rewrite "HOL_list.fold_custom_empty")
by sepref
end
end
lemma reachable_states:
"l ∈ states" if "op.E_from_op⇧*⇧* a⇩0 (l, M)"
using that
by (induction "(l, M)" arbitrary: l M; force simp: a⇩0_def state_set_def op.E_from_op_def)
definition "emptiness_check ≡ λ (l, M). check_diag n M"
sepref_definition emptiness_check_impl is
"RETURN o emptiness_check" :: "state_assn'⇧k →⇩a bool_assn"
unfolding emptiness_check_def
by sepref
lemma state_copy:
"RETURN ∘ COPY = (λ (l, M). do {M' ← mop_mtx_copy M; RETURN (l, M')})"
by auto
sepref_definition state_copy_impl is
"RETURN ∘ COPY" :: "state_assn'⇧k →⇩a state_assn'"
unfolding state_copy
by sepref
lemma location_assn_constraints:
"is_pure location_assn"
"IS_LEFT_UNIQUE (the_pure location_assn)"
"IS_RIGHT_UNIQUE (the_pure location_assn)"
using left_unique_location_rel right_unique_location_rel
by (auto elim: single_valued_subset[rotated] simp: b_rel_def IS_LEFT_UNIQUE_def)
lemma not_check_diag_init_dbm[intro, simp]:
"¬ check_diag n init_dbm"
unfolding check_diag_def init_dbm_def by auto
end
subsection ‹Instantiation of Worklist Algorithms›
context Reachability_Problem_Impl_Op
begin
sublocale Worklist0 op.E_from_op a⇩0 F_rel "subsumes n" succs "λ (l, M). check_diag n M"
apply standard
apply (clarsimp simp: op.reachable_def split: prod.split dest!: reachable_states)
unfolding succs_def op.E_from_op_def using states'_states by force
sublocale Worklist1 op.E_from_op a⇩0 F_rel "subsumes n" succs "λ (l, M). check_diag n M" ..
sublocale Worklist2 op.E_from_op a⇩0 F_rel "subsumes n" succs "λ (l, M). check_diag n M" subsumes'
apply standard
unfolding subsumes_def subsumes'_def by auto
sublocale
Worklist3
op.E_from_op a⇩0 F_rel "subsumes n" succs "λ (l, M). check_diag n M" subsumes' "λ (l, M). F l"
apply standard
unfolding F_rel_def by auto
sublocale
Worklist4
op.E_from_op a⇩0 F_rel "subsumes n" succs "λ (l, M). check_diag n M" subsumes' "λ (l, M). F l"
apply standard
unfolding F_rel_def by auto
sublocale
Worklist_Map a⇩0 F_rel "subsumes n" "λ (l, M). check_diag n M" subsumes' op.E_from_op fst succs
apply standard
unfolding subsumes'_def by auto
sublocale
Worklist_Map2
a⇩0 F_rel "subsumes n" "λ (l, M). check_diag n M" subsumes' op.E_from_op
fst succs "λ (l, M). F l"
..
sublocale Worklist4_Impl
op.E_from_op a⇩0 F_rel "subsumes n" succs "λ (l, M). check_diag n M" subsumes' "λ (l, M). F l"
state_assn' succs_impl a⇩0_impl F_impl subsumes_impl emptiness_check_impl
apply standard
apply (unfold PR_CONST_def)
by (rule
a⇩0_impl.refine F_impl.refine subsumes_impl.refine succs_impl.refine[unfolded PR_CONST_def]
emptiness_check_impl.refine[unfolded emptiness_check_def]
)+
sublocale Worklist_Map2_Impl
op.E_from_op a⇩0 F_rel "subsumes n" succs "λ (l, M). check_diag n M" subsumes'
"λ (l, M). F l" state_assn'
succs_impl a⇩0_impl F_impl subsumes_impl emptiness_check_impl fst "return o fst" state_copy_impl
tracei location_assn
apply standard
subgoal
unfolding PR_CONST_def
apply sepref_to_hoare
apply sep_auto
done
subgoal
by (rule state_copy_impl.refine)
subgoal
unfolding trace_def by (rule tracei_refine)
by (rule location_assn_constraints)+
sublocale Worklist_Map2_Hashable
op.E_from_op a⇩0 F_rel "subsumes n" succs "λ (l, M). check_diag n M" subsumes' "λ (l, M). F l"
state_assn' succs_impl a⇩0_impl F_impl subsumes_impl emptiness_check_impl
fst "return o fst" state_copy_impl tracei location_assn by standard
sublocale liveness: Liveness_Search_Space_Key
"λ (l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ F l ∧ F l' ∧ ¬ check_diag n M'" a⇩0
"λ _. False"
"subsumes n" "λ (l, M). op.reachable (l, M) ∧ ¬ check_diag n M ∧ F l"
"filter (λ (l, M). ¬check_diag n M) o succs_P F" fst subsumes'
apply standard
apply blast
apply (blast intro: op.liveness_search_space_pre.trans)
subgoal for a b a'
apply (drule op.liveness_search_space_pre.mono[where a'=a'])
unfolding op.liveness_search_space_pre.G.E'_def by (auto simp: F_rel_def)
apply blast
subgoal
using op.liveness_search_space_pre.finite_V
by (auto elim: finite_subset[rotated] simp: F_rel_def)
subgoal premises prems for a
proof -
have
"set ((filter (λ (l, M). ¬check_diag n M) o succs_P F) a)
= {x. (λ(l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ F l' ∧ ¬ check_diag n M') a x}"
unfolding op.E_from_op_def succs_P_def using prems states'_states
by (safe; force dest!: reachable_states simp: op.reachable_def)
also have "… =
{x. Subgraph_Node_Defs.E'
(λ(l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ F l ∧ F l' ∧ ¬ check_diag n M')
(λ(l, M). op.reachable (l, M) ∧ ¬ check_diag n M ∧ F l) a x}"
unfolding Subgraph_Node_Defs.E'_def using prems by auto
finally show ?thesis .
qed
by (blast intro!: empty_subsumes')+
sublocale liveness: Liveness_Search_Space_Key_Impl
a⇩0 "λ _. False" "subsumes n" "λ (l, M). op.reachable (l, M) ∧ ¬ check_diag n M ∧ F l"
"filter (λ (l, M). ¬check_diag n M) o succs_P F"
"λ (l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ F l ∧ F l' ∧ ¬ check_diag n M'"
subsumes' fst
state_assn' "succs_P_impl' F_fun" a⇩0_impl subsumes_impl "return o fst" state_copy_impl
location_assn
apply standard
apply (rule location_assn_constraints)+
apply (unfold PR_CONST_def, rule a⇩0_impl.refine; fail)
apply (unfold PR_CONST_def, rule subsumes_impl.refine; fail)
apply (unfold PR_CONST_def, rule succs_P_impl'.refine[OF F_fun])
subgoal
by sepref_to_hoare sep_auto
by (rule state_copy_impl.refine)
lemma precond_a⇩0:
"case a⇩0 of (l, M) ⇒ op.reachable (l, M) ∧ ¬ check_diag n M"
unfolding op.reachable_def unfolding a⇩0_def by auto
lemma liveness_step_equiv:
fixes x y
assumes "(λ (l, M). op.reachable (l, M) ∧ ¬ check_diag n M ∧ F l) x"
shows "liveness.G.E' x y ⟷
(λ (l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ F l ∧ F l' ∧ ¬ check_diag n M') x y"
using assms unfolding liveness.G.E'_def by auto
lemma liveness_check_equiv:
"(∃x. liveness.G.G'.reaches a⇩0 x ∧ liveness.G.G'.reaches1 x x) ⟷
(∃ x. op.liveness_pre.reaches a⇩0 x ∧ op.liveness_pre.reaches1 x x)"
if "F l⇩0"
apply (subst rtranclp_tranclp_equiv[OF liveness_step_equiv])
apply assumption
subgoal
unfolding liveness.G.E'_def by auto
subgoal
using that precond_a⇩0 by (auto simp: a⇩0_def)
..
lemma liveness_spec_refine:
"SPEC (λr. r =
(∃x. liveness.G.G'.reaches a⇩0 x ∧ liveness.G.G'.reaches1 x x)) ≤
(SPEC (λ r. r =
(∃ x.
(λ (l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ F l ∧ F l' ∧ ¬ check_diag n M')⇧*⇧* a⇩0 x ∧
(λ (l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ F l ∧ F l' ∧ ¬ check_diag n M')⇧+⇧+ x x)
)
)
" if "F l⇩0"
using liveness_check_equiv[OF that] by auto
lemma liveness_hnr:
"(uncurry0
(dfs_map_impl' (succs_P_impl' F_fun) a⇩0_impl subsumes_impl
(return ∘ fst) state_copy_impl),
uncurry0 (SPEC (λr. r = (∃x. op.liveness_pre.reaches a⇩0 x ∧ op.liveness_pre.reaches1 x x))))
∈ unit_assn⇧k →⇩a bool_assn"
if "F l⇩0"
apply (rule liveness.dfs_map_impl'_hnr[
FCOMP liveness_spec_refine[THEN Id_SPEC_refine, THEN nres_relI]
])
using that precond_a⇩0 by (auto simp: a⇩0_def)
context
fixes Q :: "'s ⇒ bool" and Q_fun
assumes Q_fun: "(Q_fun, Q) ∈ inv_rel loc_rel states'"
begin
interpretation leadsto: Leadsto_Search_Space_Key
a⇩0 "λ _. False" "subsumes n" "λ (l, M). check_diag n M" subsumes'
"λ (l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ ¬ check_diag n M'"
fst "λ _. False" "λ (l, M). F l" "λ (l, M). Q l"
"filter (λ (l, M). ¬check_diag n M) o succs_P Q" "filter (λ (l, M). ¬check_diag n M) o succs"
proof (goal_cases)
case 1
interpret Subgraph_Start
op.E_from_op a⇩0 "λ (l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ ¬ check_diag n M'"
by standard auto
show ?case
apply standard
apply blast
apply (blast intro: liveness.trans)
subgoal for a b a'
by (drule op.mono[where a' = a'], auto dest: op.empty_mono[rotated] intro: reachable)
apply (blast intro: op.empty_subsumes)
apply (rule op.empty_mono; assumption)
subgoal for x x'
by (auto dest: op.E_from_op_check_diag)
apply assumption
apply blast
apply blast
subgoal for a
by (auto dest: succs_correct reachable)
apply (simp; fail)
subgoal
using op.finite_reachable by (auto intro: reachable elim!: finite_subset[rotated])
subgoal for a a'
by (auto simp: empty_subsumes' dest: subsumes_key)
subgoal for a a'
by (auto simp: empty_subsumes' dest: subsumes_key)
subgoal premises prems for a
proof -
have
"set ((filter (λ (l, M). ¬check_diag n M) o succs_P Q) a)
= {x. (λ(l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ Q l' ∧ ¬ check_diag n M') a x}"
unfolding op.E_from_op_def succs_P_def using prems states'_states
by (safe; force dest!: reachable reachable_states simp: op.reachable_def)
then show ?thesis
by auto
qed
done
qed
sepref_register "PR_CONST Q"
lemma [sepref_fr_rules]:
"(return o Q_fun, RETURN o PR_CONST Q) ∈ location_assn⇧k →⇩a id_assn"
using Q_fun by sepref_to_hoare (sep_auto simp: inv_rel_def b_rel_def fun_rel_def)
sepref_definition Q_impl is
"RETURN o (λ (l, M). Q l)" :: "state_assn'⇧k →⇩a bool_assn"
by (rewrite in Q PR_CONST_def[symmetric]) sepref
interpretation leadsto: Leadsto_Search_Space_Key_Impl
"subsumes n" subsumes' location_assn fst a⇩0 "λ _. False" "λ _. False" state_copy_impl
"λ (l, M). F l" "λ (l, M). Q l"
"λ (l, M). op.reachable (l, M) ∧ ¬ check_diag n M"
"λ (l, M). check_diag n M"
"filter (λ (l, M). ¬check_diag n M) o succs_P Q" "filter (λ (l, M). ¬check_diag n M) o succs"
"λ (l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ ¬ check_diag n M'"
state_assn'
"succs_P_impl' Q_fun" a⇩0_impl subsumes_impl "return o fst" succs_impl'
emptiness_check_impl F_impl Q_impl tracei
apply standard
apply blast
apply (blast intro: op.trans)
subgoal for a b a'
apply (drule op.mono[where a' = a'], auto dest: op.empty_mono[rotated])
apply (intro exI conjI)
apply (auto dest: op.empty_mono[rotated])
by (auto simp: empty_subsumes' dest: subsumes_key)
apply blast
subgoal
using op.finite_reachable by (auto elim!: finite_subset[rotated])
subgoal premises prems for a
proof -
have
"set ((filter (λ (l, M). ¬check_diag n M) o succs_P Q) a)
= {x. (λ(l, M) (l', M'). op.E_from_op (l, M) (l', M') ∧ Q l' ∧ ¬ check_diag n M') a x}"
unfolding op.E_from_op_def succs_P_def using prems states'_states
by (safe; force dest!: reachable_states[folded op.reachable_def])
also have "… =
{x. Subgraph_Node_Defs.E'
(λx y.
(case x of (l, M) ⇒ λ(l', M'). op.E_from_op (l, M) (l', M') ∧ ¬ check_diag n M') y
∧ ¬ (case y of (l, M) ⇒ check_diag n M) ∧ (case y of (l, M) ⇒ Q l)
)
(λ(l, M). op.reachable (l, M) ∧ ¬ check_diag n M) a x}"
unfolding Subgraph_Node_Defs.E'_def using prems by auto
finally show ?thesis .
qed
apply blast
apply (clarsimp simp: empty_subsumes'; fail)
apply (rule location_assn_constraints)+
apply (rule liveness.refinements)
apply (rule liveness.refinements)
apply (unfold PR_CONST_def, rule succs_P_impl'.refine[OF Q_fun])
subgoal
by sepref_to_hoare sep_auto
by (rule
succs_impl'.refine liveness.refinements
emptiness_check_impl.refine[unfolded emptiness_check_def]
F_impl.refine Q_impl.refine tracei_refine
)+
definition
"leadsto_spec_alt = SPEC (λr. r ⟷
(∃a. leadsto.A.search_space.reaches a⇩0 a ∧
¬ (case a of (l, M) ⇒ check_diag n M) ∧
(case a of (l, M) ⇒ F l) ∧ (case a of (l, M) ⇒ Q l) ∧
(∃b. leadsto.B.reaches a b ∧ leadsto.B.reaches1 b b))
)
"
lemmas leadsto_impl_hnr =
leadsto.leadsto_impl_hnr[
unfolded leadsto.leadsto_spec_alt_def, unfolded leadsto.reaches_cycle_def,
folded leadsto_spec_alt_def
]
end
end
subsection ‹Implementation of the Invariant Precondition Check›
context TA_Impl_Op
begin
sepref_register "init_dbm :: nat × nat ⇒ _" :: "'e DBMEntry i_mtx"
sepref_register "unbounded_dbm n :: nat × nat ⇒ int DBMEntry" :: "'b DBMEntry i_mtx"
lemmas [sepref_fr_rules] = dbm_subset_impl.refine
sepref_register "PR_CONST (dbm_subset n)" :: "'e DBMEntry i_mtx ⇒ 'e DBMEntry i_mtx ⇒ bool"
lemma [def_pat_rules]:
"dbm_subset $ n ≡ PR_CONST (dbm_subset n)"
by simp
context
notes [id_rules] = itypeI[of "PR_CONST n" "TYPE (nat)"]
and [sepref_import_param] = IdI[of n]
begin
sepref_definition start_inv_check_impl is
"uncurry0 (RETURN (start_inv_check :: bool))" :: "unit_assn⇧k →⇩a bool_assn"
unfolding start_inv_check_def
FW''_def[symmetric] rev_map_fold reset'_upd_def inv_of_A_def[symmetric]
supply [sepref_fr_rules] = unbounded_dbm_impl.refine
by sepref
end
end
subsection ‹Instantiation for the Concrete DBM Successor Operations›
lemma (in Graph_Defs) Alw_ev:
"Alw_ev φ x" if "φ x"
using that unfolding Alw_ev_def by (auto simp: holds.simps)
context TA_Impl
begin
interpretation DBM_Impl n .
context
notes [id_rules] = itypeI[of "PR_CONST n" "TYPE (nat)"]
and [sepref_import_param] = IdI[of n]
begin
sepref_definition E_op'_impl is
"uncurry4 (λ l r. RETURN ooo E_op' l r)" :: "op_impl_assn"
unfolding E_op'_def FW''_def[symmetric] reset'_upd_def inv_of_A_def[symmetric] PR_CONST_def
by sepref
sepref_definition E_op''_impl is
"uncurry4 (λ l r. RETURN ooo E_op'' l r)" :: "op_impl_assn"
unfolding E_op''_def FW''_def[symmetric] reset'_upd_def inv_of_A_def[symmetric] filter_diag_def
by sepref
end
end
subsubsection ‹Correctness Theorems›
context Reachability_Problem_Impl
begin
sublocale Reachability_Problem_Impl_Op
where loc_rel = loc_rel and f = "PR_CONST E_op''" and op_impl = E_op''_impl
unfolding PR_CONST_def by standard (rule E_op''_impl.refine)
lemma E_op_F_reachable:
"op.F_reachable = E_op''.F_reachable" unfolding PR_CONST_def ..
lemma (in -) state_set_eq[simp]:
"Simulation_Graphs_TA.state_set A = state_set (trans_of A)"
unfolding Simulation_Graphs_TA.state_set_def state_set_def trans_of_def ..
lemma op_liveness_reaches_cycle_equiv:
"(λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b) ∧ F (fst b))⇧*⇧* a⇩0 a ∧
(λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b) ∧ F (fst b))⇧+⇧+ a b
⟷ op.liveness_pre.reaches a⇩0 a ∧ op.liveness_pre.reaches1 a b" if "F l⇩0"
using that by - (rule rtranclp_tranclp_equiv[of "F o fst"], auto simp: a⇩0_def)
lemma Alw_ev_impl_hnr:
"(uncurry0
(if F l⇩0 then
dfs_map_impl'
(succs_P_impl' F_fun) a⇩0_impl subsumes_impl (return ∘ fst) state_copy_impl
else return False),
uncurry0 (SPEC (λr. l⇩0 ∈ state_set (trans_of A) ⟶
r ⟷ ¬ (∀u⇩0. (∀c∈{1..n}. u⇩0 c = 0) ⟶ Alw_ev (λ(l, u). ¬ F l) (l⇩0, u⇩0)))))
∈ unit_assn⇧k →⇩a bool_assn"
unfolding state_set_eq[symmetric]
apply (cases "F l⇩0")
subgoal premises prems
proof -
define protected1 where "protected1 = E_op''.liveness_pre.reaches"
define protected2 where "protected2 = E_op''.liveness_pre.reaches1"
show ?thesis
using prems Alw_ev_mc[folded a⇩0_def, of F, unfolded op_liveness_reaches_cycle_equiv[OF prems]]
apply (simp add: )
unfolding protected1_def[symmetric] protected2_def[symmetric]
using liveness_hnr[OF prems, to_hnr, unfolded hn_refine_def]
apply sepref_to_hoare
apply sep_auto
apply (erule cons_post_rule)
unfolding protected1_def[symmetric] protected2_def[symmetric]
by sep_auto
qed
subgoal
using Alw_ev_mc[folded a⇩0_def, of F]
apply simp
by sepref_to_hoare sep_auto
done
context
fixes Q :: "'s ⇒ bool" and Q_fun
assumes Q_fun: "(Q_fun, Q) ∈ inv_rel loc_rel states'"
assumes no_deadlock: "∀u⇩0. (∀c∈{1..n}. u⇩0 c = 0) ⟶ ¬ deadlock (l⇩0, u⇩0)"
begin
lemma leadsto_spec_refine:
"leadsto_spec_alt Q
≤ SPEC (λ r. ¬ r ⟷
(∄x. (λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b))⇧*⇧* (l⇩0, init_dbm) x ∧
F (fst x) ∧
Q (fst x) ∧
(∃a. (λa b. E_op''.E_from_op a b ∧
¬ check_diag n (snd b) ∧ Q (fst b))⇧*⇧*
x a ∧
(λa b. E_op''.E_from_op a b ∧
¬ check_diag n (snd b) ∧ Q (fst b))⇧+⇧+
a a))
)"
proof -
have *:"
(λx y. (case y of (l', M') ⇒ E_op''.E_from_op x (l', M') ∧ ¬ check_diag n M') ∧
¬ (case y of (l, M) ⇒ check_diag n M))
= (λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b))"
by (intro ext) auto
have **:
"(λx y. (case y of (l', M') ⇒ E_op''.E_from_op x (l', M') ∧ ¬ check_diag n M') ∧
(case y of (l, M) ⇒ Q l) ∧ ¬ (case y of (l, M) ⇒ check_diag n M))
= (λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b) ∧ Q (fst b))"
by (intro ext) auto
have ***: "¬ check_diag n b"
if "(λa b. E_op''.E_from_op a b ∧ ¬ check_diag n (snd b))⇧*⇧* a⇩0 (a, b)" for a b
using that by cases (auto simp: a⇩0_def)
show ?thesis
unfolding leadsto_spec_alt_def[OF Q_fun]
unfolding PR_CONST_def a⇩0_def[symmetric] by (auto dest: *** simp: * **)
qed
lemma leadsto_impl_hnr:
"(uncurry0
(leadsto_impl state_copy_impl
(succs_P_impl' Q_fun) a⇩0_impl subsumes_impl (return ∘ fst)
succs_impl' emptiness_check_impl F_impl (Q_impl Q_fun) tracei),
uncurry0
(SPEC
(λr. l⇩0 ∈ state_set (trans_of A) ⟶
(¬ r) =
(∀u⇩0. (∀c∈{1..n}. u⇩0 c = 0) ⟶
leadsto (λ(l, u). F l) (λ(l, u). ¬ Q l) (l⇩0, u⇩0)))))
∈ unit_assn⇧k →⇩a bool_assn"
unfolding state_set_eq[symmetric]
using leadsto_impl_hnr[
OF Q_fun precond_a⇩0,
FCOMP leadsto_spec_refine[THEN Id_SPEC_refine, THEN nres_relI], to_hnr, unfolded hn_refine_def]
using leadsto_mc[OF _ no_deadlock, of F Q]
apply (simp del: state_set_eq)
apply sepref_to_hoare
apply sep_auto
apply (erule cons_post_rule)
apply sep_auto
done
end
end
subsection ‹Instantiation for a Concrete Automaton›