Theory Normalized_Zone_Semantics_Certification
theory Normalized_Zone_Semantics_Certification
imports Munta_Base.Normalized_Zone_Semantics_Impl_Semantic_Refinement
begin
no_notation TA_Start_Defs.step_impl' ("⟨_, _⟩ ↝⇘_⇙ ⟨_, _⟩" [61,61,61] 61)
context TA_Start_Defs
begin
definition
"E_precise_op l r g l' M ≡
let
M' = FW' (abstr_upd (inv_of A l) (up_canonical_upd M n)) n;
M'' = FW' (abstr_upd (inv_of A l') (reset'_upd (FW' (abstr_upd g M') n) n r 0)) n
in M''"
definition
"E_precise_op' l r g l' M ≡
let
M1 = abstr_repair (inv_of A l) (up_canonical_upd M n);
M2 = filter_diag (λ M. abstr_repair g M) M1;
M3 = filter_diag (λ M. abstr_repair (inv_of A l') (reset'_upd M n r 0)) M2
in M3"
lemma E_precise_op'_alt_def:
"E_precise_op' l r g l' M ≡
let
M' = abstr_repair (inv_of A l) (up_canonical_upd M n);
f1 = λ M. abstr_repair g M;
f2 = λ M. abstr_repair (inv_of A l') (reset'_upd M n r 0)
in filter_diag (filter_diag f2 o f1) M'"
unfolding E_precise_op'_def filter_diag_def
by (rule HOL.eq_reflection) (auto simp: Let_def check_diag_marker)
no_notation step_impl' ("⟨_, _⟩ ↝⇘_⇙ ⟨_, _⟩" [61,61,61] 61)
abbreviation step_impl_precise ("⟨_, _⟩ ↝⇘_⇙ ⟨_, _⟩" [61,61,61] 61)
where
"⟨l, Z⟩ ↝⇘a⇙ ⟨l'', Z''⟩ ≡ ∃ l' Z'.
A ⊢⇩I ⟨l, Z⟩ ↝⇘n,τ⇙ ⟨l', Z'⟩ ∧ A ⊢⇩I ⟨l', Z'⟩ ↝⇘n,↿a⇙ ⟨l'', Z''⟩"
definition "E_precise ≡ (λ(l, Z) (l'', Z''). ∃a. ⟨l, Z⟩ ↝⇘a⇙ ⟨l'', Z''⟩)"
end
locale E_Precise_Bisim = E_From_Op +
assumes op_bisim:
"A ⊢ l ⟶⇗g,a,r⇖ l' ⟹ wf_dbm M ⟹ f l r g l' M ≃ E_precise_op l r g l' M"
and op_wf:
"A ⊢ l ⟶⇗g,a,r⇖ l' ⟹ wf_dbm M ⟹ wf_dbm (f l r g l' M)"
begin
lemma E_precise_E_op:
"E_precise = (λ(l, M) (l', M'''). ∃g a r. A ⊢ l ⟶⇗g,a,r⇖ l' ∧ M''' = E_precise_op l r g l' M)"
unfolding E_precise_op_def E_precise_def by (intro ext) (auto elim!: step_impl.cases)
lemma E_E_from_op_step:
"∃c. E_from_op a c ∧ b ∼ c" if "E_precise a b" "wf_state a"
using that unfolding E_precise_E_op E_from_op_def wf_state_def state_equiv_def
by (blast intro: op_bisim dbm_equiv_sym)
lemma E_from_op_E_step:
"∃c. E_precise a c ∧ b ∼ c" if "E_from_op a b" "wf_state a"
using that unfolding E_precise_E_op E_from_op_def wf_state_def state_equiv_def
by (blast intro: op_bisim)
lemma E_from_op_wf_state:
"wf_state b" if "wf_state a" "E_from_op a b"
using that unfolding E_E_op E_from_op_def wf_state_def state_equiv_def by (blast intro: op_wf)
lemma E_precise_wf_dbm[intro]:
"wf_dbm D'" if "E_precise (l, D) (l', D')" "wf_dbm D"
using that unfolding wf_state_def E_def E_precise_def by (auto intro: step_impl_wf_dbm)
lemma E_precise_wf_state:
"wf_state a ⟹ E_precise a b ⟹ wf_state b"
unfolding wf_state_def by auto
theorem E_from_op_reachability_check:
"(∃ l' D'. E_precise⇧*⇧* a⇩0 (l', D') ∧ F_rel (l', D'))
⟷ (∃ l' D'. E_from_op⇧*⇧* a⇩0 (l', D') ∧ F_rel (l', D'))"
oops
lemma E_from_op_mono:
assumes "E_from_op (l,D) (l',D')"
and "wf_dbm D" "wf_dbm M"
and "[curry (conv_M D)]⇘v,n⇙ ⊆ [curry (conv_M M)]⇘v,n⇙"
shows "∃ M'. E_from_op (l,M) (l',M') ∧ [curry (conv_M D')]⇘v,n⇙ ⊆ [curry (conv_M M')]⇘v,n⇙"
oops
lemma E_from_op_mono':
assumes "E_from_op (l,D) (l',D')"
and "wf_dbm D" "wf_dbm M"
and "dbm_subset n D M"
shows "∃ M'. E_from_op (l,M) (l',M') ∧ dbm_subset n D' M'"
oops
lemma E_equiv:
"∃ b'. E_precise b b' ∧ a' ∼ b'" if "E_precise a a'" "a ∼ b" "wf_state a" "wf_state b"
using that
unfolding wf_state_def E_precise_def
apply safe
apply (frule (2) step_impl_equiv, erule state_equiv_D)
by (safe, drule step_impl_equiv, auto intro: step_impl_wf_dbm simp: state_equiv_def)
lemma E_from_op_bisim:
"Bisimulation_Invariant E_precise E_from_op (∼) wf_state wf_state"
apply standard
subgoal
by (drule E_equiv, assumption+) (auto dest!: E_E_from_op_step)
subgoal
by (drule (1) E_from_op_E_step, safe, drule E_equiv) (auto 4 4 intro: state_equiv_sym)
apply (rule E_precise_wf_state; assumption)
apply (rule E_from_op_wf_state; assumption)
done
lemma E_from_op_bisim_empty:
"Bisimulation_Invariant
(λ(l, M) (l', M'). E_precise (l, M) (l', M') ∧ ¬ check_diag n M')
(λ(l, M) (l', M'). E_from_op (l, M) (l', M') ∧ ¬ check_diag n M')
(∼) wf_state wf_state"
using E_from_op_bisim
apply (rule Bisimulation_Invariant_filter[
where FA = "λ(l, M). ¬ check_diag n M" and FB = "λ(l, M). ¬ check_diag n M"
])
subgoal
unfolding wf_state_def state_equiv_def
apply clarsimp
apply (subst canonical_check_diag_empty_iff[symmetric], erule wf_dbm_altD(1))
apply (subst canonical_check_diag_empty_iff[symmetric], erule wf_dbm_altD(1))
apply (simp add: dbm_equiv_def)
done
apply (solves auto)+
done
end
definition step_z_dbm' ::
"('a, 'c, 't, 's) ta ⇒ 's ⇒ 't :: {linordered_cancel_ab_monoid_add,uminus} DBM
⇒ ('c ⇒ nat) ⇒ nat ⇒ 'a ⇒ 's ⇒ 't DBM ⇒ bool"
("_ ⊢'' ⟨_, _⟩ ↝⇘_,_,_⇙ ⟨_, _⟩" [61,61,61,61] 61) where
"A ⊢' ⟨l,D⟩ ↝⇘v,n,a⇙ ⟨l'',D''⟩ ≡
∃l' D'. A ⊢ ⟨l, D⟩ ↝⇘v,n,τ⇙ ⟨l', D'⟩ ∧ A ⊢ ⟨l', D'⟩ ↝⇘v,n,↿a⇙ ⟨l'', D''⟩"
context TA_Start
begin
lemma E_precise_op'_bisim:
"E_precise_op' l r g l' M ≃ E_precise_op l r g l' M" if "A ⊢ l ⟶⇗g,a,r⇖ l'" "wf_dbm M"
proof -
note intros =
dbm_equiv_refl dbm_equiv_trans[OF filter_diag_equiv, rotated]
wf_dbm_abstr_repair_equiv_FW[rotated] reset'_upd_equiv
have "∀c∈constraint_clk ` set (inv_of A l). 0 < c ∧ c ≤ n"
using clock_range collect_clks_inv_clk_set[of A l] unfolding collect_clks_def by blast
moreover have
"∀c∈constraint_clk ` set (inv_of A l'). 0 < c ∧ c ≤ n"
"∀c∈constraint_clk ` set (inv_of A l'). 0 < c"
using clock_range collect_clks_inv_clk_set[of A l'] unfolding collect_clks_def by blast+
moreover have "∀c∈constraint_clk ` set g. 0 < c ∧ c ≤ n" "∀c∈constraint_clk ` set g. 0 < c"
using clock_range collect_clocks_clk_set[OF that(1)] unfolding collect_clks_def by blast+
moreover have "∀i∈set r. 0 < i ∧ i ≤ n" "∀i∈set r. 0 < i"
using clock_range reset_clk_set[OF that(1)] unfolding collect_clks_def by blast+
moreover note side_conds = calculation that(2)
note wf_intros =
wf_dbm_abstr_repair wf_dbm_reset'_upd wf_dbm_up_canonical_upd filter_diag_wf_dbm
wf_dbm_FW'_abstr_upd
note check_diag_intros =
reset'_upd_check_diag_preservation abstr_repair_check_diag_preservation
show ?thesis unfolding E_precise_op'_def E_precise_op_def
by simp (intro intros check_diag_intros side_conds wf_intros order.refl)
qed
lemma step_z_'_step_z_dbm'_equiv:
"Bisimulation_Invariant
(λ (l, D) (l', D'). ∃ a. step_z' (conv_A A) l D l' D')
(λ (l, D) (l', D'). ∃ a. step_z_dbm' (conv_A A) l D v n a l' D')
(λ(l, Z) (l', M). l = l' ∧ [M]⇘v,n⇙ = Z)
(λ(l, Z). True)
(λ(l, y). True)"
proof (standard, goal_cases)
case prems: (1 a b a')
obtain l Z l' Z' l1 M where unfolds[simp]: "a = (l, Z)" "b = (l', Z')" "a' = (l1, M)"
by force+
from prems have [simp]: "l1 = l"
by auto
from prems have "conv_A A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" "[M]⇘v,n⇙ = Z"
by auto
from this(1) obtain Z1 a where
"conv_A A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l, Z1⟩"
"conv_A A ⊢ ⟨l, Z1⟩ ↝⇘↿a⇙ ⟨l', Z'⟩"
unfolding step_z'_def by safe
note Z1 = this
from step_z_dbm_DBM[OF Z1(1)[folded ‹_ = Z›]] obtain M1 where M1:
"conv_A A ⊢ ⟨l, M⟩ ↝⇘v,n,τ⇙ ⟨l, M1⟩" "Z1 = [M1]⇘v,n⇙" .
from step_z_dbm_DBM[OF Z1(2)[unfolded ‹Z1 = _›]] obtain Z2 where Z2:
"conv_A A ⊢ ⟨l, M1⟩ ↝⇘v,n,↿a⇙ ⟨l', Z2⟩" "Z' = [Z2]⇘v,n⇙" .
with M1 Z1 show ?case
unfolding step_z_dbm'_def by auto
next
case prems: (2 a a' b')
obtain l M l' M' l1 Z where unfolds[simp]: "a' = (l, M)" "b' = (l', M')" "a = (l1, Z)"
by force+
from prems have [simp]: "l1 = l"
by auto
from prems obtain a1 where "conv_A A ⊢' ⟨l, M⟩ ↝⇘v,n,a1⇙ ⟨l', M'⟩" "[M]⇘v,n⇙ = Z"
by auto
from this(1) obtain l1' Z1 where Z1:
"conv_A A ⊢ ⟨l, M⟩ ↝⇘v,n,τ⇙ ⟨l1', Z1⟩"
"conv_A A ⊢ ⟨l1', Z1⟩ ↝⇘v,n,↿a1⇙ ⟨l', M'⟩"
unfolding step_z_dbm'_def by atomize_elim
then have [simp]: "l1' = l"
by (intro step_z_dbm_delay_loc)
from Z1 ‹_ = Z› show ?case
unfolding step_z'_def by (auto dest: step_z_dbm_sound)
next
case (3 a b)
then show ?case
by auto
next
case (4 a b)
then show ?case
by auto
qed
lemma step_z_dbm'_step_impl_precise_equiv:
"Bisimulation_Invariant
(λ (l, D) (l', D'). ∃ a. step_z_dbm' (conv_A A) l D v n a l' D')
(λ(l, D) (l', D'). ∃a. ⟨l, D⟩ ↝⇘a⇙ ⟨l', D'⟩)
(λ(l, M) (l', D). l = l' ∧ [curry (conv_M D)]⇘v,n⇙ = [M]⇘v,n⇙)
(λ(l, y). valid_dbm y)
wf_state"
proof (standard, goal_cases)
case prems: (1 a b a')
obtain l M l' M' l1 D where unfolds[simp]: "a = (l, M)" "b = (l', M')" "a' = (l1, D)"
by force+
from prems have [simp]: "l1 = l"
by auto
from prems obtain a1 where
"step_z_dbm' (conv_A A) l M v n a1 l' M'"
by auto
then obtain l2 M1 where steps:
"conv_A A ⊢ ⟨l, M⟩ ↝⇘v,n,τ⇙ ⟨l2, M1⟩"
"conv_A A ⊢ ⟨l2, M1⟩ ↝⇘v,n,↿a1⇙ ⟨l', M'⟩"
unfolding step_z_dbm'_def by auto
from step_z_dbm_equiv'[OF steps(1), of "curry (conv_M D)"] prems(2-) obtain M2 where
"conv_A A ⊢ ⟨l, curry (conv_M D)⟩ ↝⇘v,n,τ⇙ ⟨l2, M2⟩" "wf_dbm D" "[M1]⇘v,n⇙ = [M2]⇘v,n⇙"
by (auto simp: wf_state_def)
with step_impl_complete''_improved[OF this(1)] obtain D2 where D2:
"A ⊢⇩I ⟨l, D⟩ ↝⇘n,τ⇙ ⟨l2, D2⟩" "[curry (conv_M D2)]⇘v,n⇙ = [M1]⇘v,n⇙"
by auto
from step_impl_wf_dbm[OF D2(1) ‹wf_dbm D›] have "wf_dbm D2" .
from step_z_dbm_equiv'[OF steps(2) sym[OF D2(2)]] obtain D3 where D3:
"conv_A A ⊢ ⟨l2, curry (conv_M D2)⟩ ↝⇘v,n,↿a1⇙ ⟨l', D3⟩" "[M']⇘v,n⇙ = [D3]⇘v,n⇙"
by (elim conjE exE)
from step_impl_complete''_improved[OF D3(1) ‹wf_dbm D2›] obtain D4 where D4:
"A ⊢⇩I ⟨l2, D2⟩ ↝⇘n,↿a1⇙ ⟨l', D4⟩" "[curry (conv_M D4)]⇘v,n⇙ = [D3]⇘v,n⇙"
by auto
with D2(1) have "⟨l, D⟩ ↝⇘a1⇙ ⟨l', D4⟩"
by auto
with D4(2) D3 show ?case
by force
next
case prems: (2 a a' b')
obtain l M l' D' l1 D where unfolds[simp]: "a = (l, M)" "b' = (l', D')" "a' = (l1, D)"
by force+
from prems have [simp]: "l1 = l"
by auto
from prems obtain a1 where "⟨l, D⟩ ↝⇘a1⇙ ⟨l', D'⟩"
by auto
then obtain D1 where steps:
"A ⊢⇩I ⟨l, D⟩ ↝⇘n,τ⇙ ⟨l, D1⟩" "A ⊢⇩I ⟨l, D1⟩ ↝⇘n,↿a1⇙ ⟨l', D'⟩"
by (auto dest: step_impl_delay_loc_eq)
from prems have "wf_dbm D"
by (auto simp: wf_state_def)
with steps have "wf_dbm D1"
by (blast intro: step_impl_wf_dbm)
from step_impl_sound'[OF steps(1)] ‹wf_dbm D› obtain M2 where M2:
"conv_A A ⊢ ⟨l, curry (conv_M D)⟩ ↝⇘v,n,τ⇙ ⟨l, M2⟩"
"[curry (conv_M D1)]⇘v,n⇙ = [M2]⇘v,n⇙"
using wf_dbm_D by auto
from step_impl_sound'[OF steps(2)] ‹wf_dbm D1› obtain M3 where M3:
"step_z_dbm (conv_A A) l (curry (conv_M D1)) v n (↿a1) l' M3"
"[curry (conv_M D')]⇘v,n⇙ = [M3]⇘v,n⇙"
using wf_dbm_D by auto
from step_z_dbm_equiv'[OF M2(1), of M] prems(2) obtain M2' where M2':
"conv_A A ⊢ ⟨l, M⟩ ↝⇘v,n,τ⇙ ⟨l, M2'⟩" "[M2]⇘v,n⇙ = [M2']⇘v,n⇙"
by auto
from step_z_dbm_equiv'[OF M3(1), of M2'] M2(2) M2'(2) obtain M3' where
"conv_A A ⊢ ⟨l, M2'⟩ ↝⇘v,n,↿a1⇙ ⟨l', M3'⟩" "[M3]⇘v,n⇙ = [M3']⇘v,n⇙"
by auto
with M2'(1) M3(2) show ?case
unfolding step_z_dbm'_def by auto
next
case (3 a b)
then show ?case
unfolding step_z_dbm'_def using step_z_norm_valid_dbm'_spec step_z_valid_dbm' by auto
next
case (4 a b)
then show ?case
by (clarsimp simp: norm_step_wf_dbm step_impl_wf_dbm wf_state_def)
qed
lemma E_precise_op'_wf:
assumes "A ⊢ l ⟶⇗g,a,r⇖ l'" "wf_dbm M"
shows "wf_dbm (E_precise_op' l r g l' M)"
proof -
have "∀c∈constraint_clk ` set (inv_of A l). 0 < c ∧ c ≤ n"
using clock_range collect_clks_inv_clk_set[of A l] unfolding collect_clks_def by blast
moreover have "∀c∈constraint_clk ` set (inv_of A l'). 0 < c ∧ c ≤ n"
using clock_range collect_clks_inv_clk_set[of A l'] unfolding collect_clks_def by blast
moreover have "∀c∈constraint_clk ` set g. 0 < c ∧ c ≤ n"
using clock_range collect_clocks_clk_set[OF assms(1)] unfolding collect_clks_def by blast
moreover have "∀i∈set r. 0 < i ∧ i ≤ n"
using clock_range reset_clk_set[OF assms(1)] unfolding collect_clks_def by blast
moreover note side_conds = calculation assms(2)
note wf_intros =
wf_dbm_abstr_repair wf_dbm_reset'_upd wf_dbm_up_canonical_upd filter_diag_wf_dbm
show ?thesis
unfolding E_precise_op'_def by simp (intro wf_intros side_conds order.refl)
qed
sublocale E_precise_op': E_Precise_Bisim _ _ _ _ E_precise_op'
by standard (rule E_precise_op'_bisim E_precise_op'_wf; assumption)+
lemma step_z_dbm'_final_bisim:
"Bisimulation_Invariant
(λ (l, D) (l', D'). ∃ a. step_z_dbm' (conv_A A) l D v n a l' D')
E_precise_op'.E_from_op
(λ (l, M) (l', D'). l' = l ∧ [curry (conv_M D')]⇘v,n⇙ = [M]⇘v,n⇙)
(λ(l, y). valid_dbm y) wf_state"
by (rule Bisimulation_Invariant_sim_replace,
rule Bisimulation_Invariant_composition[
OF step_z_dbm'_step_impl_precise_equiv[folded E_precise_def] E_precise_op'.E_from_op_bisim
]) (auto simp add: state_equiv_def dbm_equiv_def)
end
context E_Precise_Bisim
begin
theorem step_z_dbm'_mono:
assumes "conv_A A ⊢' ⟨l, M⟩ ↝⇘v,n,a⇙ ⟨l', M'⟩" and "[M]⇘v,n⇙ ⊆ [D]⇘v,n⇙"
shows "∃D'. conv_A A ⊢' ⟨l, D⟩ ↝⇘v,n,a⇙ ⟨l', D'⟩ ∧ [M']⇘v,n⇙ ⊆ [D']⇘v,n⇙"
using assms unfolding step_z_dbm'_def
apply clarsimp
apply (drule step_z_dbm_mono, assumption)
apply safe
apply (drule step_z_dbm_mono, assumption)
apply auto
done
interpretation
Bisimulation_Invariant
"(λ (l, D) (l', D'). ∃ a. step_z_dbm' (conv_A A) l D v n a l' D')"
E_from_op
"λ (l, M) (l', D'). l' = l ∧ [curry (conv_M D')]⇘v,n⇙ = [M]⇘v,n⇙"
"λ(l, y). valid_dbm y"
wf_state
by (rule Bisimulation_Invariant_sim_replace,
rule Bisimulation_Invariant_composition[
OF step_z_dbm'_step_impl_precise_equiv[folded E_precise_def] E_from_op_bisim
]) (auto simp add: state_equiv_def dbm_equiv_def)
lemmas step_z_dbm'_E_from_op_bisim = Bisimulation_Invariant_axioms
definition
"E_from_op_empty ≡ λ(l, D) (l', D'). E_from_op (l, D) (l', D') ∧ ¬ check_diag n D'"
interpretation bisim_empty:
Bisimulation_Invariant
"λ(l, M) (l', M'). ∃ a. step_z_dbm' (conv_A A) l M v n a l' M' ∧ [M']⇘v,n⇙ ≠ {}"
"λ(l, D) (l', D'). E_from_op (l, D) (l', D') ∧ ¬ check_diag n D'"
"λ(l, M) (l', D'). l' = l ∧ [curry (conv_M D')]⇘v,n⇙ = [M]⇘v,n⇙"
"λ(l, y). valid_dbm y"
wf_state
using step_z_dbm'_E_from_op_bisim apply (rule Bisimulation_Invariant_filter[
where FA = "λ(l', M'). [M']⇘v,n⇙ ≠ {}" and FB = "λ(l', D'). ¬ check_diag n D'"
])
using canonical_check_diag_empty_iff canonical_empty_check_diag' by (auto simp: wf_state_def)
lemmas step_z_dbm'_E_from_op_bisim_empty =
bisim_empty.Bisimulation_Invariant_axioms[folded E_from_op_empty_def]
lemma E_from_op_mono:
assumes "E_from_op (l,D) (l',D')"
and "wf_dbm D" "wf_dbm M"
and "[curry (conv_M D)]⇘v,n⇙ ⊆ [curry (conv_M M)]⇘v,n⇙"
shows "∃ M'. E_from_op (l,M) (l',M') ∧ [curry (conv_M D')]⇘v,n⇙ ⊆ [curry (conv_M M')]⇘v,n⇙"
proof -
from B_A_step[OF assms(1), of "(l, curry (conv_M D))"] assms(2) obtain a D1 where D1:
"conv_A A ⊢' ⟨l, curry (conv_M D)⟩ ↝⇘v,n,a⇙ ⟨l', D1⟩" "[D1]⇘v,n⇙ = [curry (conv_M D')]⇘v,n⇙"
unfolding wf_state_def by (force dest: wf_dbm_D)
from step_z_dbm'_mono[OF this(1) assms(4)] obtain M1 where M1:
"conv_A A ⊢' ⟨l, curry (conv_M M)⟩ ↝⇘v,n,a⇙ ⟨l', M1⟩"
"[D1]⇘v,n⇙ ⊆ [M1]⇘v,n⇙"
by atomize_elim
with A_B_step[of "(l, curry (conv_M M))" "(l', M1)" "(l, M)"] assms(3) obtain M2 where
"E_from_op (l, M) (l', M2)" "[curry (conv_M M2)]⇘v,n⇙ = [M1]⇘v,n⇙"
unfolding wf_state_def by (force dest: wf_dbm_D)
with assms(3) M1(2) D1(2) show ?thesis
by auto
qed
lemma E_from_op_mono':
assumes "E_from_op (l,D) (l',D')"
and "wf_dbm D" "wf_dbm M"
and "dbm_subset n D M"
shows "∃ M'. E_from_op (l,M) (l',M') ∧ dbm_subset n D' M'"
using assms
apply -
apply (frule E_from_op_mono[where M = M], assumption+)
apply (subst dbm_subset_correct'', assumption+)
apply (rule dbm_subset_conv, assumption)
apply safe
apply (subst (asm) dbm_subset_correct'')
subgoal
using B_invariant[unfolded wf_state_def] by auto
subgoal
using B_invariant[unfolded wf_state_def] by auto
apply (blast intro: dbm_subset_conv_rev)
done
lemma E_from_op_empty_mono':
assumes "E_from_op_empty (l,D) (l',D')"
and "wf_dbm D" "wf_dbm M"
and "dbm_subset n D M"
shows "∃ M'. E_from_op_empty (l,M) (l',M') ∧ dbm_subset n D' M'"
using assms unfolding E_from_op_empty_def using check_diag_subset E_from_op_mono' by blast
end
end