Theory Normalized_Zone_Semantics_Certification_Impl
section ‹Checker Implementation for Single Automata›
theory Normalized_Zone_Semantics_Certification_Impl
imports
Munta_Base.Normalized_Zone_Semantics_Impl_Refine
Normalized_Zone_Semantics_Certification
Collections.Refine_Dflt_ICF
Unreachability_Certification2
Unreachability_Certification
"HOL-Library.IArray"
Munta_Model_Checker.Deadlock_Impl
Munta_Base.More_Methods
"HOL-Library.Rewrite"
begin
paragraph ‹Misc›
lemma (in Graph_Defs) run_first_reaches:
"pred_stream (reaches x) xs" if "run (x ## xs)"
proof -
from that obtain a where "run (a ## xs)" "reaches x a"
by auto
then show ?thesis
by (coinduction arbitrary: a xs rule: stream_pred_coinduct) (auto 4 3 elim: run.cases)
qed
lemma (in Graph_Start_Defs) run_reachable:
"pred_stream reachable xs" if "run (s⇩0 ## xs)"
using run_first_reaches[OF that] unfolding reachable_def .
lemma pred_stream_stream_all2_combine:
assumes "pred_stream P xs" "stream_all2 Q xs ys" "⋀x y. P x ⟹ Q x y ⟹ R x y"
shows "stream_all2 R xs ys"
using assms by (auto intro: stream_all2_combine simp: stream.pred_rel eq_onp_def)
lemma stream_all2_pred_stream_combine:
assumes "stream_all2 Q xs ys" "pred_stream P ys" "⋀x y. Q x y ⟹ P y ⟹ R x y"
shows "stream_all2 R xs ys"
using assms by (auto intro: stream_all2_combine simp: stream.pred_rel eq_onp_def)
lemma map_set_rel:
assumes "list_all P xs" "(f, g) ∈ {(xs, ys). xs = ys ∧ P xs} → B"
shows "(map f xs, g ` set xs) ∈ ⟨B⟩list_set_rel"
unfolding list_set_rel_def
apply (rule relcompI[where b = "map g xs"])
apply parametricity
using assms unfolding list_rel_def list_all_iff by (auto intro: list.rel_refl_strong)
context TA_Start
begin
lemma V_I:
assumes "∀ i ∈ {1..<Suc n}. M 0 i ≤ 0"
shows "[M]⇘v,n⇙ ⊆ V"
unfolding V_def DBM_zone_repr_def
proof (safe, goal_cases)
case prems: (1 u i)
then have "v i = i"
using X_alt_def X_def triv_numbering by blast
with prems have "v i > 0" "v i ≤ n" by auto
with prems have "dbm_entry_val u None (Some i) (M 0 (v i))"
unfolding DBM_val_bounded_def by auto
moreover from assms ‹v i > 0› ‹v i ≤ n› have "M 0 (v i) ≤ 0" by auto
ultimately
show ?case
apply (cases "M 0 (v i)")
unfolding neutral less_eq dbm_le_def
by (auto elim!: dbm_lt.cases simp: ‹v i = i›)
qed
end
lemma Simulation_Composition:
fixes A B C
assumes
"Simulation A B sim1" "Simulation B C sim2" "⋀a c. (∃ b. sim1 a b ∧ sim2 b c) ⟷ sim a c"
shows "Simulation A C sim"
proof -
interpret A: Simulation A B sim1
by (rule assms)
interpret B: Simulation B C sim2
by (rule assms)
show ?thesis
by standard (auto dest!: B.A_B_step A.A_B_step simp: assms(3)[symmetric])
qed
lemma fold_generalize_start:
assumes "⋀a. P a ⟹ Q (fold g xs a)" "P a"
shows "Q (fold g xs a)"
using assms by auto
definition
"set_of_list xs = SPEC (λS. set xs = S)"
lemma set_of_list_hnr:
"(return o id, set_of_list) ∈ (list_assn A)⇧d →⇩a lso_assn A"
unfolding set_of_list_def lso_assn_def hr_comp_def br_def by sepref_to_hoare sep_auto
lemma set_of_list_alt_def:
"set_of_list = RETURN o set"
unfolding set_of_list_def by auto
lemmas set_of_list_hnr' = set_of_list_hnr[unfolded set_of_list_alt_def]
lemmas amtx_copy_hnr = amtx_copy_hnr[unfolded op_mtx_copy_def, folded COPY_def[abs_def]]
lemma lso_op_set_is_empty_hnr[sepref_fr_rules]:
"(return o (λxs. xs = []), RETURN o op_set_is_empty) ∈ (lso_assn AA)⇧k →⇩a bool_assn"
unfolding lso_assn_def hr_comp_def br_def by sepref_to_hoare sep_auto
context
fixes n :: nat
begin
qualified definition
"dbm_tab M ≡ λ (i, j). if i ≤ n ∧ j ≤ n then M ! ((n + 1) * i + j) else 0"
private lemma
shows mtx_nonzero_dbm_tab_1: "(a, b) ∈ mtx_nonzero (dbm_tab M) ⟹ a < Suc n"
and mtx_nonzero_dbm_tab_2: "(a, b) ∈ mtx_nonzero (dbm_tab M) ⟹ b < Suc n"
unfolding mtx_nonzero_def dbm_tab_def by (auto split: if_split_asm)
definition
"list_to_dbm M = op_amtx_new (Suc n) (Suc n) (dbm_tab M)"
lemma [sepref_fr_rules]:
"(return o dbm_tab, RETURN o PR_CONST dbm_tab) ∈ id_assn⇧k →⇩a pure (nat_rel ×⇩r nat_rel → Id)"
by sepref_to_hoare sep_auto
lemmas [sepref_opt_simps] = dbm_tab_def
sepref_register dbm_tab
sepref_definition list_to_dbm_impl
is "RETURN o PR_CONST list_to_dbm" :: "id_assn⇧k →⇩a mtx_assn n"
supply mtx_nonzero_dbm_tab_1[simp] mtx_nonzero_dbm_tab_2[simp]
unfolding PR_CONST_def list_to_dbm_def by sepref
lemma the_pure_Id:
"the_pure (λa c. ↑ (c = a)) = Id"
by (subst is_pure_the_pure_id_eq) (auto simp: pure_def intro: is_pureI)
lemma of_list_list_to_dbm:
"(Array.of_list, (RETURN ∘∘ PR_CONST) list_to_dbm)
∈ [λa. length a = Suc n * Suc n]⇩a id_assn⇧k → mtx_assn n"
apply sepref_to_hoare
apply sep_auto
unfolding amtx_assn_def hr_comp_def IICF_Array_Matrix.is_amtx_def
apply (sep_auto eintros del: exI)
subgoal for xs p
apply (rule exI[where x = "list_to_dbm xs"])
apply (rule exI[where x = xs])
apply (sep_auto simp: list_to_dbm_def dbm_tab_def the_pure_Id)
apply (simp add: algebra_simps; fail)
apply sep_auto
done
done
end
definition
"array_freeze a = do {xs ← Array.freeze a; Heap_Monad.return (IArray xs)}"
definition
"array_unfreeze a = Array.of_list (IArray.list_of a)"
definition
"iarray_mtx_rel n m c a ≡
IArray.length a = n * m
∧ (∀i<n.∀j<m. c (i, j) = IArray.sub a (i * m + j))
∧ (∀i j. i ≥ n ∨ j ≥ m ⟶ c (i, j) = 0)"
lemma iarray_mtx_rel_is_amtx:
"x ↦⇩a IArray.list_of a ⟹⇩A IICF_Array_Matrix.is_amtx n m c x" if "iarray_mtx_rel n m c a"
using that unfolding is_amtx_def iarray_mtx_rel_def by simp solve_entails
lemma array_unfreeze_ht:
"<emp> array_unfreeze a <amtx_assn n m id_assn c>" if "iarray_mtx_rel n m c a"
using that unfolding array_unfreeze_def amtx_assn_def by (sep_auto intro: iarray_mtx_rel_is_amtx)
lemma array_freeze_ht:
"<amtx_assn n m id_assn c a> array_freeze a <λa. ↑(iarray_mtx_rel n m c a)>⇩t"
unfolding array_freeze_def amtx_assn_def iarray_mtx_rel_def is_amtx_def
by (sep_auto intro: iarray_mtx_rel_is_amtx)