Theory TA_Simulation
section ‹Simulations on Timed Automata›
theory TA_Simulation
imports
Timed_Automata.Timed_Automata
Timed_Automata.Normalized_Zone_Semantics
Timed_Automata.Simulation_Graphs_TA
"HOL-Eisbach.Eisbach"
Simulation_Graphs2
Munta_Base.Normalized_Zone_Semantics_Impl_Semantic_Refinement
"HOL-ex.Sketch_and_Explore"
begin
text ‹
This theory essentially formalizes the concepts from Guangyuan Li's FORMATS 2009 paper
``Checking Timed Büchi Automata Emptiness Using LU-Abstractions'' \<^cite>‹"Li:FORMATS:2009"›.
›
no_notation dbm_le ("_ ≼ _" [51, 51] 50)
subsection ‹Preliminaries›
lemma
step_z_state_setI1: "l ∈ state_set A" and
step_z_state_setI2: "l' ∈ state_set A" if "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩"
using that unfolding step_z'_def by (force simp: state_set_def trans_of_def)+
lemma step_trans_z'_sound:
"A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩ ⟹ ∀u' ∈ Z'. ∃u ∈ Z. ∃d. A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l',u'⟩"
by (fastforce dest!: step_trans_a_z_sound step_trans_t_z_sound elim!: step_trans_z'.cases)
lemma step_trans_z'_exact_strong:
assumes "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩"
shows "Z' = {u'. ∃u ∈ Z. A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l', u'⟩}"
using step_trans_z'_sound assms by (auto dest: step_trans_z'_exact step_trans_z'_sound)
lemma step_a_step_trans_iff:
"A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l', u'⟩ ⟷ (∃g r. A ⊢⇩t ⟨l, u⟩ →⇘(g,a,r)⇙ ⟨l', u'⟩)"
unfolding step_a.simps step_trans.simps by fast
lemma step_trans'_step_trans_iff:
"(∃t. A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l', u'⟩) ⟷ A ⊢' ⟨l, u⟩ → ⟨l', u'⟩"
unfolding step_trans'.simps step'.simps step_a_step_trans_iff by fast
subsection ‹Time-Abstract Simulation›
locale Time_Abstract_Simulation =
fixes A :: "('a, 'c, 't :: time, 'l) ta"
fixes sim :: "'l × ('c ⇒ 't :: time) ⇒ 'l × ('c ⇒ 't) ⇒ bool" (infix "≼" 60)
assumes sim:
"⋀l l' l⇩1 u u' u⇩1 t. (l, u) ≼ (l', u') ⟹ A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l⇩1, u⇩1⟩
⟹ ∃u⇩1'. A ⊢' ⟨l', u'⟩ →⇗t⇖ ⟨l⇩1, u⇩1'⟩ ∧ (l⇩1, u⇩1) ≼ (l⇩1, u⇩1')"
assumes refl: "⋀u. u ≼ u" and trans: "⋀u v w. u ≼ v ⟹ v ≼ w ⟹ u ≼ w"
begin
lemma simE:
assumes "(l, u) ≼ (l', u')" "A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l⇩1, u⇩1⟩"
obtains u⇩1' where "A ⊢' ⟨l', u'⟩ →⇗t⇖ ⟨l⇩1, u⇩1'⟩" "(l⇩1, u⇩1) ≼ (l⇩1, u⇩1')"
using assms sim by blast
definition abs :: "'l ⇒ ('c, 't) zone ⇒ ('c, 't) zone" ("α _ _" [71,71] 71) where
"α l W = {v. ∃v' ∈ W. (l, v) ≼ (l, v')}"
lemma simulation_mono:
assumes "α l Z ⊆ α l Z'" "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l⇩1, Z⇩1⟩" "A ⊢' ⟨l, Z'⟩ ↝⇗t⇖ ⟨l⇩1, Z⇩1'⟩"
shows "α l⇩1 Z⇩1 ⊆ α l⇩1 Z⇩1'"
proof -
have
"Z⇩1 = {u'. ∃u ∈ Z. A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l⇩1, u'⟩}" "Z⇩1' = {u'. ∃u ∈ Z'. A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l⇩1, u'⟩}"
by (intro step_trans_z'_exact_strong assms(2,3))+
show ?thesis
unfolding abs_def
proof safe
fix u v
assume "v ∈ Z⇩1" "(l⇩1, u) ≼ (l⇩1, v)"
with ‹Z⇩1 = _› obtain u⇩0 where "u⇩0 ∈ Z" and step: "A ⊢' ⟨l, u⇩0⟩ →⇗t⇖ ⟨l⇩1, v⟩"
by auto
from ‹u⇩0 ∈ Z› ‹α l Z ⊆ _› obtain v⇩0 where "v⇩0 ∈ Z'" "(l, u⇩0) ≼ (l, v⇩0)"
unfolding abs_def using refl[of "(l, u⇩0)"] by auto
from simE[OF ‹(l, u⇩0) ≼ (l, v⇩0)› step] obtain v' where
"A ⊢' ⟨l, v⇩0⟩ →⇗t⇖ ⟨l⇩1, v'⟩" "(l⇩1, v) ≼ (l⇩1, v')" .
with ‹v⇩0 ∈ Z'› ‹Z⇩1' = _› have "v' ∈ Z⇩1'"
by auto
moreover from ‹_ ≼ (l⇩1, v)› ‹(l⇩1, v) ≼ _› have "(l⇩1, u) ≼ (l⇩1, v')"
by (rule trans)
ultimately show "∃x∈Z⇩1'. (l⇩1, u) ≼ (l⇩1, x)"
by fast
qed
qed
lemma simulation:
assumes "α l Z = α l Z'" "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z⇩1⟩" "A ⊢' ⟨l, Z'⟩ ↝⇗t⇖ ⟨l', Z⇩1'⟩"
shows "α l' Z⇩1 = α l' Z⇩1'"
using simulation_mono assms by blast
lemma simulation':
assumes "α l Z = α l Z'" "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z⇩1⟩"
shows "∃Z⇩1'. A ⊢' ⟨l, Z'⟩ ↝⇗t⇖ ⟨l', Z⇩1'⟩ ∧ α l' Z⇩1 = α l' Z⇩1'"
proof -
from ‹A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z⇩1⟩› obtain Z⇩1' where "A ⊢' ⟨l, Z'⟩ ↝⇗t⇖ ⟨l', Z⇩1'⟩"
by (auto elim!: step_trans_z'.cases step_trans_z.cases)
with simulation assms show ?thesis
by blast
qed
lemma abs_involutive:
"α l (α l Z) = α l Z"
unfolding abs_def by (auto intro: refl trans)
lemma abs_widens:
"Z ⊆ α l Z"
unfolding abs_def by (auto intro: refl)
text ‹
This is Lemma 4 from the paper
``Better Abstractions for Timed Automata'' (🌐‹https://arxiv.org/abs/1110.3705›)
›
corollary transition_compatibility:
assumes "A ⊢' ⟨l, α l Z⟩ ↝⇗t⇖ ⟨l', W⟩" "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩"
shows "α l' W = α l' Z'"
by (rule simulation[OF _ assms(1,2)], rule abs_involutive)
inductive step_abs ::
"('a, 'c, 't, 'l) ta ⇒ 'l ⇒ ('c, 't) zone ⇒ 'a ⇒ 'l ⇒ ('c, 't) zone ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝⇘α(_)⇙ ⟨_, _⟩" [61,61,61] 61)
where
step_alpha:
"A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇘↿a⇙ ⟨l'', Z''⟩
⟹ A ⊢ ⟨l, α l Z⟩ ↝⇘α(a)⇙ ⟨l'', α l'' Z''⟩"
interpretation sim1: Simulation where
A = "λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" and
B = "λ(l, Z) (l', Z'). ∃a. A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l', Z'⟩" and
sim = "λ(l, u) (l', Z). l' = l ∧ u ∈ Z ∧ α l Z = Z"
apply standard
unfolding step'.simps step_abs.simps
apply clarsimp
subgoal premises prems for l v l'' v'' Z d l' v' a
proof -
from ‹v ∈ Z› ‹A ⊢ ⟨l, v⟩ →⇗d⇖ ⟨l', v'⟩› obtain Z' where
"A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l', Z'⟩" "v' ∈ Z'"
by (auto dest: step_t_z_complete)
moreover obtain Z'' where
"A ⊢ ⟨l', Z'⟩ ↝⇘↿a⇙ ⟨l'', Z''⟩" "v'' ∈ Z''"
using prems ‹v' ∈ Z'› by (auto dest: step_a_z_complete)
ultimately show ?thesis
using ‹α l Z = Z› abs_involutive abs_widens by blast
qed
done
interpretation sim2: Simulation where
A = "λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" and
B = "λ(l, Z) (l', Z'). ∃a. A ⊢ ⟨l, α l Z⟩ ↝⇘α(a)⇙ ⟨l', α l' Z'⟩" and
sim = "λ(l, u) (l', Z). l' = l ∧ u ∈ Z"
apply standard
unfolding step'.simps step_abs.simps
apply clarsimp
subgoal premises prems for l v l'' v'' Z d l' v' a
proof -
from ‹v ∈ Z› ‹A ⊢ ⟨l, v⟩ →⇗d⇖ ⟨l', v'⟩› obtain Z' where
"A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l', Z'⟩" "v' ∈ Z'"
by (auto dest: step_t_z_complete)
moreover obtain Z'' where
"A ⊢ ⟨l', Z'⟩ ↝⇘↿a⇙ ⟨l'', Z''⟩" "v'' ∈ Z''"
using prems ‹v' ∈ Z'› by (auto dest: step_a_z_complete)
ultimately show ?thesis
by fastforce
qed
done
sublocale self_simulation: Self_Simulation where
E = "λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" and P = "λ_. True"
apply standard
apply (force dest: sim simp: step_trans'_step_trans_iff[symmetric])
using refl trans unfolding reflp_def transp_def by blast+
end
context Regions_TA
begin
definition sim_regions (infix "≡⇩M" 60) where
"sim_regions ≡ λ(l, u) (l', u').
(l' = l ∧ l ∈ state_set A ∧ (∃R ∈ ℛ l. u ∈ R ∧ u' ∈ R))
∨ (l ∉ state_set A ∨ u ∉ V) ∧ (l' ∉ state_set A ∨ u' ∉ V)"
abbreviation
"valid ≡ λ(l, u). l ∈ state_set A ∧ u ∈ V"
lemma ℛ_I:
assumes "l ∈ state_set A" "u ∈ V"
shows "∃R ∈ ℛ l. u ∈ R"
using assms regions_partition[where ℛ = ‹ℛ l› and X = X and k = "k l" and u = u] ℛ_def[of l]
unfolding V_def by blast
lemma regions_finite:
"finite (ℛ l)"
using finite_ℛ[OF finite] unfolding ℛ_def .
lemma valid_iff:
"valid (l, u) ⟷ valid (l', u')" if "(l, u) ≡⇩M (l', u')"
using that unfolding sim_regions_def by (auto dest: ℛ_V)
lemma refl:
"(l, u) ≡⇩M (l, u)"
unfolding sim_regions_def by (cases "valid (l, u)"; simp add: ℛ_I)
lemma sym:
"(l, u) ≡⇩M (l', u') ⟷ (l', u') ≡⇩M (l, u)"
unfolding sim_regions_def by auto
lemma trans:
"(l, u) ≡⇩M (l'', u'')" if "(l, u) ≡⇩M (l', u')" "(l', u') ≡⇩M (l'', u'')"
proof (cases "valid (l, u)")
case True
with that have "valid (l, u)" "valid (l', u')" "valid (l'', u'')"
using valid_iff by metis+
then show ?thesis
using that unfolding sim_regions_def by (auto dest: ℛ_regions_distinct[rotated 2])
next
case False
with that have "¬ valid (l, u)" "¬ valid (l', u')" "¬ valid (l'', u'')"
using valid_iff by metis+
then show ?thesis
unfolding sim_regions_def by simp
qed
lemma equiv:
"equivp (≡⇩M)"
using refl sym trans by - (rule equivpI; unfold equivp_def reflp_def symp_def transp_def; fast)
lemma same_loc:
"l' = l" if "(l, u) ≡⇩M (l', u')" "valid (l, u)"
using that unfolding sim_regions_def by auto
lemma regions_simI:
"(l, u) ≡⇩M (l, u')" if "l ∈ state_set A" "R ∈ ℛ l" "u ∈ R" "u' ∈ R"
using that unfolding sim_regions_def by auto
lemma regions_simD:
"u' ∈ R" if "l ∈ state_set A" "R ∈ ℛ l" "u ∈ R" "(l, u) ≡⇩M (l', u')"
using that unfolding sim_regions_def by (auto dest: ℛ_V ℛ_regions_distinct)
lemma finite_quotient:
"finite (UNIV // {(x, y). x ≡⇩M y})"
proof -
let ?S = "state_set A × (⋃l ∈ state_set A. ℛ l)" and ?f = "λ(l, R). from_R l R"
let ?invalid = "{(l, u). ¬valid (l, u)}"
have "Collect ((≡⇩M) (l, u)) ∈ ?f ` ?S"
if "valid (l, u)" for l u
proof -
from that refl[of l u] obtain R where *: "l ∈ state_set A" "R ∈ ℛ l" "u ∈ R"
unfolding sim_regions_def by auto
with ‹valid _› have "Collect ((≡⇩M) (l, u)) = from_R l R"
unfolding from_R_def by (auto simp: same_loc intro: regions_simI regions_simD)
with * show ?thesis
by auto
qed
moreover have "Collect ((≡⇩M) (l, u)) = ?invalid" if "¬ valid (l, u)" for l u
using that unfolding sim_regions_def by (auto simp: ℛ_V)
ultimately have "UNIV // {(x, y). x ≡⇩M y} ⊆ (?f ` ?S) ∪ {?invalid}"
apply -
apply (rule subsetI)
apply (erule quotientE)
apply clarsimp
by blast
also have "finite …"
by (blast intro: finite_state_set regions_finite)+
finally show ?thesis .
qed
sublocale region_self_simulation: Self_Simulation where
E = "λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" and sim = "(≡⇩M)" and P = valid
apply (standard; clarsimp?)
subgoal simulation premises prems for l u l1 u1 l' u'
proof -
from ‹u ∈ V› ‹A ⊢' ⟨l, u⟩ → ⟨l1, u1⟩›[THEN step_r'_complete_spec] obtain a R1 where
"u1 ∈ R1" "A,ℛ ⊢ ⟨l, [u]⇩l⟩ ↝⇩a ⟨l1, R1⟩"
by blast
moreover from prems have "u' ∈ [u]⇩l"
unfolding V_def by (auto elim: regions_simD dest: region_cover')
ultimately obtain u1' where "u1' ∈ R1" "A ⊢' ⟨l, u'⟩ → ⟨l1, u1'⟩"
by (auto 4 3 dest: step_r'_sound)
moreover from ‹u1 ∈ R1› ‹u1' ∈ R1› ‹A,ℛ ⊢ ⟨l, [u]⇩l⟩ ↝⇩a ⟨l1, R1⟩› have "(l1, u1) ≡⇩M (l1, u1')"
by (meson regions_simI step_r'_ℛ step_r'_state_set)
moreover from prems have "valid (l', u')"
using valid_iff by auto
moreover from prems have "l' = l"
by - (erule same_loc, simp)
ultimately show ?thesis
using ‹(l, u) ≡⇩M (l', u')› by blast
qed
subgoal invariant
by (meson ℛ_V step_r'_ℛ step_r'_complete_spec step_r'_state_set)
using refl trans unfolding reflp_def transp_def by fast+
end
subsection ‹LU-Simulation›
definition
"constraints_of A l = ⋃ (set ` insert (inv_of A l) {g. ∃a r l'. (l, g, a, r, l') ∈ trans_of A})"
definition
"is_lower A L ≡
∀l. ∀ac ∈ constraints_of A l. case ac of
GT c x ⇒ L l c ≥ x |
GE c x ⇒ L l c ≥ x |
EQ c x ⇒ L l c ≥ x |
_ ⇒ True"
definition
"is_upper A U ≡
∀l. ∀ac ∈ constraints_of A l. case ac of
LT c x ⇒ U l c ≥ x |
LE c x ⇒ U l c ≥ x |
EQ c x ⇒ U l c ≥ x |
_ ⇒ True"
definition
"is_locally_consistent A k ≡
∀(l, g, a, r, l') ∈ trans_of A. ∀x ∈ clk_set A - set r. k l x ≥ k l' x"
lemma is_locally_consistentD:
assumes "is_locally_consistent A k" "A ⊢ l ⟶⇗g,a,r⇖ l⇩1"
shows "∀x ∈ clk_set A - set r. k l x ≥ k l⇩1 x"
using assms unfolding is_locally_consistent_def by fast
locale TA_LU =
fixes A :: "('a, 'c, 't :: time, 'l) ta"
fixes L :: "'l ⇒ 'c ⇒ 't" and U :: "'l ⇒ 'c ⇒ 't"
assumes is_lower: "is_lower A L" and is_upper: "is_upper A U"
and locally_consistent: "is_locally_consistent A L" "is_locally_consistent A U"
begin
definition sim :: "'l × ('c ⇒ 't :: time) ⇒ 'l × ('c ⇒ 't) ⇒ bool" (infix "≼" 60) where
"sim ≡ λ(l, v) (l', v').
l' = l ∧ (∀x ∈ clk_set A. (v' x < v x ⟶ v' x > L l x) ∧ (v' x > v x ⟶ v x > U l x))"
lemma simE:
assumes "(l, v) ≼ (l', v')" "x ∈ clk_set A"
obtains "l' = l" "v x = v' x"
| "l' = l" "v x > v' x" "v' x > L l x"
| "l' = l" "v x < v' x" "v x > U l x"
using assms unfolding sim_def by force
lemma sim_locD:
"l' = l" if "(l, v) ≼ (l', v')"
using that unfolding sim_def by auto
lemma sim_nonneg:
"u x ≥ 0" if "(l, u) ≼ (l', u')" "u' x ≥ 0" "x ∈ clk_set A" "U l x ≥ 0"
using that by (auto elim: simE)
lemma sim_time_shift:
"(l, v ⊕ d) ≼ (l', v' ⊕ d)" if "(l, v) ≼ (l', v')" "d ≥ 0"
using that unfolding cval_add_def sim_def by simp (metis add.commute add_strict_increasing2)
lemma constraints_of_clk_set:
assumes "g ∈ constraints_of A l"
shows
"g = LT c x ⟹ c ∈ clk_set A"
"g = LE c x ⟹ c ∈ clk_set A"
"g = EQ c x ⟹ c ∈ clk_set A"
"g = GE c x ⟹ c ∈ clk_set A"
"g = GT c x ⟹ c ∈ clk_set A"
using assms
unfolding constraints_of_def
unfolding collect_clkvt_def clkp_set_def
unfolding
Timed_Automata.clkp_set_def Timed_Automata.collect_clki_def Timed_Automata.collect_clkt_def
unfolding collect_clock_pairs_def
by auto (smt UnCI Union_iff constraint_pair.simps fst_conv image_eqI mem_Collect_eq)+
lemma constraint_simulation:
assumes "g ∈ constraints_of A l" "(l, v) ≼ (l', v')" "v ⊢⇩a g"
shows "v' ⊢⇩a g"
using assms(3,1,2) is_lower is_upper unfolding is_lower_def is_upper_def
by cases(all ‹frule (1) constraints_of_clk_set; erule (1) simE; fastforce simp: clock_val_a.simps›)
lemma inv_simulation:
assumes "v ⊢ inv_of A l" "(l, v) ≼ (l', v')"
shows "v' ⊢ inv_of A l"
proof -
from assms(1) have "∀ac ∈ set (inv_of A l). v ⊢⇩a ac"
unfolding clock_val_def list_all_iff by auto
moreover have "∀ac ∈ set (inv_of A l). ac ∈ constraints_of A l"
unfolding constraints_of_def by auto
ultimately show ?thesis
using ‹_ ≼ _› unfolding clock_val_def list_all_iff by (auto intro: constraint_simulation)
qed
lemma guard_simulation:
assumes "A ⊢ l ⟶⇗g,a,r⇖ l⇩1" "v ⊢ g" "(l, v) ≼ (l', v')"
shows "v' ⊢ g"
proof -
from assms(2) have "∀ac ∈ set g. v ⊢⇩a ac"
unfolding clock_val_def list_all_iff by auto
moreover from assms(1) have "∀ac ∈ set g. ac ∈ constraints_of A l"
unfolding constraints_of_def by auto
ultimately show ?thesis
using ‹_ ≼ _› unfolding clock_val_def list_all_iff by (auto intro: constraint_simulation)
qed
lemma sim_delay:
assumes "(l, v) ≼ (l', v')" "d ≥ 0"
shows "(l, v ⊕ d) ≼ (l', v' ⊕ d)"
using assms unfolding cval_add_def sim_def by (auto simp: add_strict_increasing2 gt_swap)
lemma clock_set_iff:
"([r→0]v) c = (if c ∈ set r then 0 else v c)"
by auto
lemma sim_reset:
assumes "A ⊢ l ⟶⇗g,a,r⇖ l⇩1" "v ⊢ g" "(l, v) ≼ (l', v')"
shows "(l⇩1, [r→0]v) ≼ (l⇩1, [r→0]v')"
proof -
from assms(1) have
"∀x ∈ clk_set A - set r. L l x ≥ L l⇩1 x" "∀x ∈ clk_set A - set r. U l x ≥ U l⇩1 x"
using locally_consistent by - (intro is_locally_consistentD; assumption)+
then show ?thesis
using assms(2,3) unfolding sim_def by (auto simp: clock_set_iff) force+
qed
lemma step_t_simulation:
"(l, u) ≼ (l', u') ⟹ A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l⇩1, u⇩1⟩
⟹ ∃u⇩1'. A ⊢ ⟨l⇩1, u'⟩ →⇗d⇖ ⟨l⇩1, u⇩1'⟩ ∧ (l⇩1, u⇩1) ≼ (l, u⇩1')"
unfolding step_t.simps by (auto dest: sim_delay inv_simulation sim_locD)
lemma step_a_simulation:
"(l, u) ≼ (l', u') ⟹ A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l⇩1, u⇩1⟩
⟹ ∃u⇩1'. A ⊢ ⟨l, u'⟩ →⇘a⇙ ⟨l⇩1, u⇩1'⟩ ∧ (l⇩1, u⇩1) ≼ (l⇩1, u⇩1')"
unfolding step_a.simps
apply clarsimp
apply (frule (2) guard_simulation)
apply (drule (2) sim_reset[rotated -1])
apply (frule (1) inv_simulation)
apply auto
done
lemma step_trans_simulation:
"(l, u) ≼ (l', u') ⟹ A ⊢⇩t ⟨l, u⟩ →⇘t⇙ ⟨l⇩1, u⇩1⟩
⟹ ∃u⇩1'. A ⊢⇩t ⟨l, u'⟩ →⇘t⇙ ⟨l⇩1, u⇩1'⟩ ∧ (l⇩1, u⇩1) ≼ (l⇩1, u⇩1')"
unfolding step_trans.simps
apply clarsimp
apply (frule (2) guard_simulation)
apply (drule (2) sim_reset[rotated -1])
apply (frule (1) inv_simulation)
apply auto
done
sublocale Time_Abstract_Simulation A sim
apply standard
subgoal
unfolding step_trans'.simps using step_t_simulation step_trans_simulation
by simp (metis sim_locD)
subgoal
unfolding sim_def by auto
subgoal premises prems for u v w
proof -
define clks where "clks = clk_set A"
from prems show ?thesis
unfolding sim_def clks_def[symmetric] by fastforce+
qed
done
end
subsection ‹Simulation on Reachability Invariants›
locale Invariant_Simulation =
fixes L :: "'l set" and M :: "'l ⇒ 's set"
and SE E SE' E' sim :: "('l × 's) ⇒ ('l × 's) ⇒ bool"
assumes SE_SE':
"⋀l l' x y x'. sim (l, x) (l, x') ⟹ SE (l, x) (l', y)
⟹ ∃y'. SE' (l, x') (l', y') ∧ sim (l', y) (l', y')"
assumes SE'_SE:
"⋀l l' x y x' y'. sim (l, x) (l, x') ⟹ sim (l', y) (l', y') ⟹ SE' (l, x') (l', y')
⟹ SE (l, x) (l', y)"
and E'_E:
"⋀l l' a a' b'. sim (l, a) (l, a') ⟹ E' (l, a') (l', b')
⟹ (∃b. E (l, a) (l', b) ∧ sim (l', b) (l', b'))"
begin
definition
"M' ≡ λl. {x'. ∃x ∈ M l. sim (l, x) (l, x')}"
lemma invariant_simulation:
assumes
"∀l ∈ L. ∀s ∈ M l. ∀l' s'. E (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s'' ∈ M l'. SE (l', s') (l', s''))"
shows
"∀l ∈ L. ∀s ∈ M' l. ∀l' s'. E' (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s'' ∈ M' l'. SE' (l', s') (l', s''))"
apply safe
subgoal
using assms unfolding M'_def by (auto dest: E'_E)
subgoal premises prems
proof -
have "∃s''. (∃x∈M l'. sim (l', x) (l', s'')) ∧ SE' (l', s') (l', s'')"
if "l ∈ L" "E' (l, s) (l', s')" "x ∈ M l" "sim (l, x) (l, s)"
for l :: 'l and s :: 's and l' :: 'l and s' :: 's and x :: 's
proof -
from that E'_E obtain x' where "sim (l', x') (l', s')" "E (l, x) (l', x')"
by force
with ‹l ∈ L› ‹x ∈ M l› assms obtain x'' where "x'' ∈ M l'" "SE (l', x') (l', x'')"
by force
from this(2) ‹sim (l', x') _› obtain s'' where
"SE' (l', s') (l', s'')" "sim (l', x'') (l', s'')"
by atomize_elim (rule SE_SE')
with ‹x'' ∈ _› show "∃s''. (∃x∈M l'. sim (l', x) (l', s'')) ∧ SE' (l', s') (l', s'')"
by auto
qed
with prems show ?thesis
unfolding M'_def by auto
qed
done
interpretation Simulation where
A = E' and
B = E and
sim = "λ(l, s) (l', s'). l' = l ∧ sim (l, s') (l', s)"
by standard (auto dest: E'_E)
context
fixes f :: "'l × 's ⇒ nat"
begin
definition
"f' ≡ λ(l, s). Max ({f (l, s') | s'. sim (l, s') (l, s) ∧ s' ∈ M l})"
context
assumes finite: "finite L" "∀ l ∈ L. finite (M l)"
assumes f_topo: "⋀l s l1 s1 l2 s2.
l ∈ L ⟹ s ∈ M l ⟹ l2 ∈ L ⟹ s2 ∈ M l2 ⟹ E (l, s) (l1, s1) ⟹ SE (l1, s1) (l2, s2) ⟹
f (l, s) ≤ f (l2, s2)"
begin
lemma topo_simulation: "⋀l s l1 s1 l2 s2.
l ∈ L ⟹ s ∈ M' l ⟹ l2 ∈ L ⟹ s2 ∈ M' l2 ⟹ E' (l, s) (l1, s1) ⟹ SE' (l1, s1) (l2, s2) ⟹
f' (l, s) ≤ f' (l2, s2)"
subgoal premises prems for l s l1 s1 l2 s2
proof -
have "f' (l, s) ≤ f' (l'', s'')"
if "l ∈ L"
and "l'' ∈ L"
and "E' (l, s) (l', s')"
and "SE' (l', s') (l'', s'')"
and "x ∈ M l"
and "sim (l, x) (l, s)"
and "x'' ∈ M l''"
and "sim (l'', x'') (l'', s'')"
for l s l' s' l'' s'' x x''
proof -
let ?S = "λ l'' s''. {f (l'', s') |s'. sim (l'', s') (l'', s'') ∧ s' ∈ M l''}"
have finiteI: "finite (?S l s)" if "l ∈ L" for l s
using finite that using [[simproc add: finite_Collect]] by simp
have "Max (?S l s) ∈ ?S l s"
using ‹l ∈ L› ‹sim (l, x) _› ‹x ∈ _› by (intro Max_in) (auto intro: finiteI)
then obtain y where "f' (l, s) = f (l, y)" "sim (l, y) (l, s)" "y ∈ M l"
unfolding f'_def by auto
with E'_E ‹E' (l,s) _› ‹sim (l, x) _› obtain x' where
"E (l, y) (l', x')" "sim (l', x') (l', s')"
by metis
moreover from ‹SE' (l',s') _› ‹sim (l', x') _› ‹sim (l'', x'') _› have "SE (l', x') (l'', x'')"
using SE'_SE by metis
ultimately have "f (l, y) ≤ f (l'', x'')"
using that f_topo[of l y l'' x'' l' x'] ‹y ∈ M l› by auto
with ‹_ = f (l, y)› have "f' (l, s) ≤ f (l'', x'')"
by simp
also from ‹x'' ∈ _› ‹l'' ∈ _› ‹sim (l'', x'') _› have "… ≤ f' (l'', s'')"
unfolding f'_def by (auto intro: finiteI Max_ge)
finally show ?thesis .
qed
then show ?thesis
using prems unfolding M'_def by auto
qed
done
end
end
end
subsection ‹Abstraction-Simulation on Reachability Invariants›
locale Abstraction_Simulation =
fixes L :: "'l set" and M :: "'l ⇒ 's set"
and SE E SE' :: "('l × 's) ⇒ ('l × 's) ⇒ bool"
and α :: "'l ⇒ 's ⇒ 's"
assumes SE_SE': "⋀l l' x y. SE (l, x) (l', α l' y) ⟹ SE' (l, α l x) (l', α l' y)"
assumes SE'_SE: "⋀l l' x y. SE' (l, α l x) (l', α l' y) ⟹ SE (l, x) (l', α l' y)"
and simulation:
"⋀l l' a a' b.
α l a = α l a' ⟹ E (l, a) (l', b) ⟹ (∃b'. E (l, a') (l', b') ∧ α l' b = α l' b')"
begin
definition
"M' ≡ λl. α l ` M l"
inductive E' where
"E (l, s) (l', s') ⟹ E' (l, α l s) (l', α l' s')"
sublocale sim: Invariant_Simulation where
sim = "λ(l, x) (l', y). l' = l ∧ y = α l x" and
SE = "λ(l, x) (l', y). SE (l, x) (l', α l' y)" and
SE' = "λ(l, x) (l', y). SE' (l, x) (l', y)" and
E = E and
E' = E'
apply standard
subgoal for l l' x y x'
apply clarsimp
by (rule SE_SE')
subgoal for l l' x y x' y'
apply clarsimp
by (rule SE'_SE)
subgoal for l l' a a' b'
using simulation by (auto elim!: E'.cases)
done
interpretation sim2: Simulation where
sim = "λ(l, x) (l', y). l' = l ∧ y = α l x" and
A = E and
B = E'
by standard (force simp: E'.simps)
interpretation bisim: Bisimulation where
sim = "λ(l, x) (l', y). l' = l ∧ y = α l x" and
A = E and
B = E'
apply standard
subgoal
using sim2.A_B_step .
subgoal for a a' b'
by (cases b') (auto dest: sim.E'_E[rotated])
done
lemma simulationE:
assumes "α l a = α l a'" "E (l, a) (l', b)"
obtains b' where "E (l, a') (l', b')" "α l' b = α l' b'"
using assms simulation by blast
lemma M'_eq:
"sim.M' = M'"
unfolding sim.M'_def M'_def by auto
lemma invariant_simulation:
assumes
"∀l∈L. ∀s∈M l. ∀l' s'. E (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s''∈M l'. SE (l', s') (l', α l' s''))"
shows
"∀l∈L. ∀s∈M' l. ∀l' s'. E' (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s''∈M' l'. SE' (l', s') (l', s''))"
using sim.invariant_simulation assms unfolding M'_eq by fast
lemma
assumes
"∀l∈L. ∀s∈M l. ∀l' s'. E (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s''∈M l'. SE (l', s') (l', α l' s''))"
shows
"∀l∈L. ∀s∈M' l. ∀l' s'. E' (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s''∈M' l'. SE' (l', s') (l', s''))"
proof -
{ fix x l s l' s'
assume "l ∈ L" "x ∈ M l" "(l, s) → (l', s')" "α l x = α l s"
then have "l' ∈ L"
using assms simulation by metis
}
moreover
{ fix l l' :: 'l and s s' x :: 's
assume "l ∈ L" "E (l, s) (l', s')" "α l x = α l s" "x ∈ M l"
with simulation obtain x' where "α l' s' = α l' x'" "E (l, x) (l', x')"
by metis
with ‹l ∈ L› ‹x ∈ M l› assms obtain x'' where "x'' ∈ M l'" "SE (l', x') (l', α l' x'')"
by force
from this(2) have "SE' (l', α l' x') (l', α l' x'')"
by (rule SE_SE')
with ‹x'' ∈ _› ‹α l' s' = _› have "∃s''∈M l'. SE' (l', α l' s') (l', α l' s'')"
by auto
}
ultimately show ?thesis
unfolding M'_def by - (safe; (erule E'.cases; clarsimp))
qed
context
fixes f :: "'l × 's ⇒ nat"
assumes finite: "finite L" "∀ l ∈ L. finite (M l)"
assumes f_topo: "⋀l s l1 s1 l2 s2.
l ∈ L ⟹ s ∈ M l ⟹ l2 ∈ L ⟹ s2 ∈ M l2 ⟹ E (l, s) (l1, s1) ⟹ SE (l1, s1) (l2, α l2 s2)
⟹ f (l, s) ≤ f (l2, s2)"
begin
definition
"f' ≡ λ(l, s). Max ({f (l, s') | s'. α l s' = s ∧ s' ∈ M l})"
lemma f'_eq:
"sim.f' f = f'"
unfolding sim.f'_def f'_def by (rule ext; clarsimp; metis)
lemma topo_simulation: "⋀l s l1 s1 l2 s2.
l ∈ L ⟹ s ∈ M' l ⟹ l2 ∈ L ⟹ s2 ∈ M' l2 ⟹ E' (l, s) (l1, s1) ⟹ SE' (l1, s1) (l2, s2) ⟹
f' (l, s) ≤ f' (l2, s2)"
by (rule sim.topo_simulation[where f = f, OF finite, unfolded M'_eq f'_eq])
((rule f_topo; simp; fail), simp+)
end
end
subsection ‹Instantiation for Abstractions based on Time-Abstraction Simulations›
context Time_Abstract_Simulation
begin
context
fixes SE :: "('l × ('c, 't) zone) ⇒ ('l × ('c, 't) zone) ⇒ bool"
assumes SE_subsumption: "⋀l l' Z Z'. SE (l, Z) (l', Z') ⟹ l' = l ∧ Z ⊆ α l' Z'"
and SE_determ:
"⋀l l' Z Z' W. SE (l, Z) (l', Z') ⟹ α l Z = α l W ⟹ SE (l, W) (l', Z')"
begin
lemma step_z'_step_trans_z'_iff:
"A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z''⟩ ⟷ (∃t. A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z''⟩)"
using step_trans_z'_step_z' step_z'_step_trans_z' by metis
interpretation Abstraction_Simulation where
SE = "λ(l, Z) (l', Z'). ∃W. Z' = α l W ∧ SE (l, Z) (l', W)" and
E = "λ(l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" and
SE' = "λ(l, Z) (l', Z'). ∃W W'. Z = α l W ∧ Z' = α l' W' ∧ SE (l, W) (l', W')" and
α = abs
apply (standard; clarsimp)
subgoal
using SE_subsumption by metis
subgoal for l l' x y W W'
using SE_subsumption SE_determ by metis
subgoal
unfolding step_z'_step_trans_z'_iff using simulation' by metis
done
interpretation inv: Invariant_Simulation where
SE = "λ(l, Z) (l', Z'). ∃W. l' = l ∧ α l Z' = α l W ∧ SE (l, Z) (l', W)" and
E = "λ(l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" and E' = E' and
SE' = "λ(l, Z) (l', Z'). ∃W W'. l' = l ∧ Z = α l W ∧ Z' = α l' W' ∧ SE (l, W) (l', W')" and
sim = "λ(l, Z) (l', Z'). l' = l ∧ Z' = α l Z"
apply (standard; clarsimp simp: abs_involutive)
subgoal for l Z' W
by blast
subgoal for l Z W Z' W'
using SE_determ by auto
subgoal for l l' Z Z'
using sim.E'_E by auto
done
end
end
subsection ‹``Sandwiches'' of Abstraction-Simulations›
locale Time_Abstract_Simulation_Sandwich =
Regions_TA where A = A +
Time_Abstract_Simulation where A = A for A :: "('a, 'c, real, 'l) ta" +
assumes sim_V: "(l, u) ≼ (l', u') ⟹ u' ∈ V ⟹ u ∈ V"
fixes I β
assumes I_invariant: "I Z ⟹ A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ⟹ I Z'"
assumes β_α: "I Z ⟹ Z ⊆ V ⟹ l ∈ state_set A ⟹ β l Z ⊆ α l Z"
and β_widens: "I Z ⟹ Z ⊆ V ⟹ l ∈ state_set A ⟹ Z ⊆ β l Z"
and β_I: "I Z ⟹ Z ⊆ V ⟹ l ∈ state_set A ⟹ I (β l Z)"
and finite_abstraction: "finite {β l Z | l Z. I Z ∧ Z ⊆ V ∧ l ∈ state_set A}"
fixes l⇩0 :: 'l and Z⇩0 :: "('c, real) zone"
assumes l⇩0_state_set: "l⇩0 ∈ state_set A" and Z⇩0_V: "Z⇩0 ⊆ V" and Z⇩0_I: "I Z⇩0"
begin
inductive step_beta ::
"('a, 'c, real, 'l) ta ⇒ 'l ⇒ ('c, real) zone ⇒ 'a ⇒ 'l ⇒ ('c, real) zone ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝⇘β(_)⇙ ⟨_, _⟩" [61,61,61] 61)
where
step_beta:
"A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇘↿a⇙ ⟨l'', Z''⟩
⟹ A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l'', β l'' Z''⟩"
no_notation step_z_beta ("_ ⊢ ⟨_, _⟩ ↝⇘β(_)⇙ ⟨_, _⟩" [61,61,61,61] 61)
no_notation step_z_alpha ("_ ⊢ ⟨_, _⟩ ↝⇘α(_)⇙ ⟨_, _⟩" [61,61,61] 61)
lemma step_beta_alt_def:
"(∃a. A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l', W⟩) ⟷ (∃Z'. A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ∧ W = β l' Z')"
unfolding step_beta.simps step_z'_def by auto
lemma step_betaE:
assumes "A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l', W⟩"
obtains Z' where "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" "W = β l' Z'"
using step_beta_alt_def assms by metis
definition
"loc_is l s ≡ ∀(l', _) ∈ s. l' = l"
lemma α_V:
"α l Z ⊆ V" if "Z ⊆ V"
using that sim_V unfolding V_def abs_def by auto
lemma β_V:
"β l Z ⊆ V" if "Z ⊆ V" "I Z" "l ∈ state_set A"
using β_α α_V that by blast
lemma step_z'_V:
"Z' ⊆ V" if "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" "Z ⊆ V"
by (meson step_z_V step_z'_def that)
text ‹Corresponds to lemma 6 of \<^cite>‹"Li:FORMATS:2009"›.›
lemma backward_simulation:
assumes
"b ∈ S'" "loc_is l S" "loc_is l' S'" "A ⊢ ⟨l, R_of S⟩ ↝⇘β(a)⇙ ⟨l', R_of S'⟩"
"I (R_of S)" "R_of S ⊆ V"
shows "∃a∈S. ∃b'. (case a of (l, u) ⇒ λ(l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩) b' ∧ b ≼ b'"
proof -
let ?Z = "R_of S" and ?Z' = "R_of S'"
obtain u1 where "b = (l', u1)"
using assms(1,3) unfolding loc_is_def by (cases b) auto
then have "u1 ∈ ?Z'"
using assms(1) by blast
from assms(4) obtain Z' where "A ⊢ ⟨l, ?Z⟩ ↝ ⟨l', Z'⟩" "?Z' = β l' Z'"
by (erule step_betaE)
then have "β l' Z' ⊆ α l' Z'"
using assms(5,6) by (intro β_α) (auto dest: I_invariant step_z'_V step_z_state_setI2)
with ‹u1 ∈ ?Z'› ‹?Z' = _› obtain u1' where "u1' ∈ Z'" "(l', u1) ≼ (l', u1')"
unfolding abs_def by auto
with ‹A ⊢ ⟨l, ?Z⟩ ↝ ⟨l', Z'⟩› obtain u where "A ⊢' ⟨l, u⟩ → ⟨l', u1'⟩" "u ∈ ?Z"
by (meson step_z_sound')
with ‹_ ≼ _› show ?thesis
using assms(2) unfolding R_of_def loc_is_def ‹b = _› by fastforce
qed
lemma step'_step_beta:
assumes
"(l, u) ∈ a'" "A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" "loc_is l1 a'" "R_of a' ⊆ V" "I (R_of a')"
shows
"∃b'. (∃a l l'. loc_is l a' ∧ loc_is l' b' ∧ a' ≠ {} ∧ b' ≠ {} ∧
A ⊢ ⟨l, R_of a'⟩ ↝⇘βa⇙ ⟨l', R_of b'⟩) ∧ (l', u') ∈ b'"
proof -
let ?Z = "R_of a'"
from ‹(l, u) ∈ _› ‹loc_is _ _› have [simp]: "l1 = l"
unfolding loc_is_def by auto
from assms(1) have "u ∈ ?Z"
unfolding R_of_def by force
with assms(2) obtain Z' where step: "A ⊢ ⟨l, ?Z⟩ ↝ ⟨l', Z'⟩" "u' ∈ Z'"
by (metis step_z_complete')
then obtain a where "A ⊢ ⟨l, R_of a'⟩ ↝⇘βa⇙ ⟨l', β l' Z'⟩"
by atomize_elim (unfold step_beta_alt_def, fast)
moreover from β_widens have "u' ∈ β l' Z'"
using step ‹_ ⊆ V› ‹I ?Z› by (blast dest: step_z'_V I_invariant step_z_state_setI2)
ultimately show ?thesis
using ‹loc_is _ _› ‹(l, u) ∈ _›
by (inst_existentials "from_R l' (β l' Z')" a l l')
(auto simp: from_R_def loc_is_def R_of_def image_def)
qed
definition beta_step where
"beta_step ≡ λs s'. ∃a l l'. loc_is l s ∧ loc_is l' s' ∧ s ≠ {} ∧ s' ≠ {} ∧
A ⊢ ⟨l, R_of s⟩ ↝⇘β(a)⇙ ⟨l', R_of s'⟩"
lemma beta_step_inv:
assumes "beta_step a b" "∃l∈state_set A. loc_is l a ∧ R_of a ⊆ V ∧ I (R_of a)"
shows "∃l∈state_set A. loc_is l b ∧ R_of b ⊆ V ∧ I (R_of b)"
using assms unfolding beta_step_def
using β_V step_z'_V step_z_state_setI2 β_I I_invariant step_betaE by metis
lemma from_R_R_of:
assumes "loc_is l S"
shows "from_R l (R_of S) = S"
using assms from_R_R_of unfolding loc_is_def by force
interpretation backward_simulation: Backward_Double_Simulation_Complete where
E = "λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" and
G = beta_step and
sim' = "(≡⇩M)" and
P = valid and
Q = "λs. ∃l ∈ state_set A. loc_is l s ∧ R_of s ⊆ V ∧ I (R_of s)" and
a⇩0 = "from_R l⇩0 Z⇩0"
proof (standard, goal_cases)
case (1 a b a')
then show ?case
by (intro self_simulation.A_B_step TrueI)
next
case (2 b B A)
then show ?case
unfolding beta_step_def by clarify (rule backward_simulation)
next
case (3 a)
then show ?case
by (rule refl)
next
case 4
then show ?case
by (rule self_simulation.trans)
next
case 5
then show ?case
by (rule equiv)
next
case 6
then show ?case
by (rule finite_quotient)
next
case (7 a b a')
then show ?case
unfolding beta_step_def by clarify (rule step'_step_beta)
next
case (8 a b)
then show ?case
by (rule region_self_simulation.PA_invariant.invariant)
next
case (9 a b)
then show ?case
by (rule beta_step_inv[rotated])
next
case 10
let ?S = "{from_R l (β l Z) | l Z. l ∈ state_set A ∧ Z ⊆ V ∧ I Z}"
have "{x. beta_step⇧*⇧* (from_R l⇩0 Z⇩0) x} ⊆ ?S ∪ {from_R l⇩0 Z⇩0}"
apply (rule subsetI)
apply simp
subgoal
proof (induction "from_R l⇩0 Z⇩0" _ rule: rtranclp.induct)
case rtrancl_refl
then show ?case
by simp
next
case (rtrancl_into_rtrancl b c)
let ?Z = "R_of b" and ?Z' = "R_of c"
from ‹beta_step b c› obtain a l l' where step:
"loc_is l b" "loc_is l' c" "b ≠ {}" "c ≠ {}"
"A ⊢ ⟨l, R_of b⟩ ↝⇘βa⇙ ⟨l', R_of c⟩"
unfolding beta_step_def by blast
with rtrancl_into_rtrancl(2) ‹loc_is l b› have "l ∈ state_set A" "?Z ⊆ V" "I ?Z"
apply -
subgoal
by (metis step_betaE step_z_state_setI1)
subgoal
using Z⇩0_V β_V by (metis R_of_from_R)
subgoal
using Z⇩0_I β_I by (metis R_of_from_R)
done
with step(1,2,5) show ?case
using from_R_R_of step_z_state_setI2 step_z'_V step_betaE I_invariant by metis
qed
done
moreover have "finite (?S ∪ {from_R l⇩0 Z⇩0})"
proof -
let ?T = "(λ(l, Z). from_R l Z) ` (state_set A × {β l Z |l Z. I Z ∧ Z ⊆ V ∧ l ∈ state_set A})"
have "?S ⊆ ?T"
by auto
also from finite_state_set finite_abstraction have "finite ?T"
by auto
finally show ?thesis
by fast
qed
ultimately show ?case
by (rule finite_subset)
next
case (11 a)
then show ?case
unfolding loc_is_def by auto
next
case 12
then show ?case
using l⇩0_state_set Z⇩0_V Z⇩0_I by (auto simp: V_def loc_is_def from_R_def R_of_def image_def)
qed
end
subsection ‹Invariants on DBM-based Model Checking›
context Regions
begin
inductive step_z_dbm' ::
"('a, 'c, 't, 's) ta ⇒ 's ⇒ 't :: {linordered_cancel_ab_monoid_add,uminus} DBM
⇒ 'a ⇒ 's ⇒ 't DBM ⇒ bool"
("_ ⊢'' ⟨_, _⟩ ↝⇘_⇙ ⟨_, _⟩" [61,61,61] 61) for A l D a l'' D''
where
"A ⊢' ⟨l,D⟩ ↝⇘a⇙ ⟨l'',D''⟩" if "A ⊢ ⟨l,D⟩ ↝⇘v,n,τ⇙ ⟨l',D'⟩" "A ⊢ ⟨l',D'⟩ ↝⇘v,n,↿a⇙ ⟨l'',D''⟩"
lemmas step_z_dbm'_def = step_z_dbm'.simps
inductive step_impl' ::
"('a, nat, 't :: linordered_ab_group_add, 's) ta ⇒ 's ⇒ 't DBM'
⇒ 'a ⇒ 's ⇒ 't DBM' ⇒ bool"
("_ ⊢⇩I'' ⟨_, _⟩ ↝⇘_⇙ ⟨_, _⟩" [61,61,61] 61) for A l D a l'' D''
where
"A ⊢⇩I' ⟨l,D⟩ ↝⇘a⇙ ⟨l'',D''⟩" if "A ⊢⇩I ⟨l, D⟩ ↝⇘n,τ⇙ ⟨l',D'⟩" "A ⊢⇩I ⟨l',D'⟩ ↝⇘n,↿a⇙ ⟨l'',D''⟩"
lemmas step_impl'_def = step_impl'.simps
end
definition
"dbm_nonneg n M ≡ ∀i ≤ n. i > 0 ⟶ M 0 i ≤ 0"
named_theorems dbm_nonneg
lemma dbm_nonneg_And[dbm_nonneg]:
assumes "dbm_nonneg n M" "dbm_nonneg n M'"
shows "dbm_nonneg n (And M M')"
using assms by (auto simp: dbm_nonneg_def min_def)
lemma dbm_nonneg_abstra[dbm_nonneg]:
assumes "dbm_nonneg n M"
shows "dbm_nonneg n (abstra ac M v)"
using assms by (cases ac) (auto simp: dbm_nonneg_def min_def)
lemma dbm_nonneg_abstr[dbm_nonneg]:
assumes "dbm_nonneg n M"
shows "dbm_nonneg n (abstr g M v)"
using assms(1) unfolding abstr.simps
by (rule fold_acc_preserv'[where P = "dbm_nonneg n", rotated]) (rule dbm_nonneg_abstra)
lemma dbm_nonneg_up[dbm_nonneg]:
"dbm_nonneg n (up M)" if "dbm_nonneg n M"
using that unfolding dbm_nonneg_def up_def by auto
lemma dbm_nonneg_reset[dbm_nonneg]:
fixes M :: "'t :: time DBM"
assumes "dbm_nonneg n M" "x > 0"
shows "dbm_nonneg n (reset M n x 0)"
using assms unfolding reset_def dbm_nonneg_def by (auto simp: neutral min_def)
lemma dbm_nonneg_reset'[dbm_nonneg]:
fixes M :: "'t :: time DBM"
assumes "dbm_nonneg n M" "∀c ∈ set r. v c > 0"
shows "dbm_nonneg n (reset' M n r v 0)"
using assms by (induction r) (auto intro: dbm_nonneg_reset)
lemma dbm_nonneg_fw_upd[dbm_nonneg]:
"dbm_nonneg n (fw_upd M k' i j)" if "dbm_nonneg n M"
using that unfolding dbm_nonneg_def fw_upd_def upd_def min_def by auto
lemma dbm_nonneg_fwi[dbm_nonneg]:
"dbm_nonneg n (fwi M n k' i j)" if "dbm_nonneg n M"
using that by (induction M _ _ _ _ rule: fwi.induct) (auto intro!: dbm_nonneg_fw_upd)
lemma dbm_nonneg_fw[dbm_nonneg]:
"dbm_nonneg n (fw M n k)" if "dbm_nonneg n M"
using that by (induction k) (auto intro!: dbm_nonneg_fwi)
lemma dbm_nonneg_FW[dbm_nonneg]:
"dbm_nonneg n (FW M n)" if "dbm_nonneg n M"
using that by (rule dbm_nonneg_fw)
definition
"empty_dbm ≡ λ_ _. Lt 0"
lemma neg_diag_zero_empty_dbmI:
assumes "M 0 0 < 0"
shows "[M]⇘v,n⇙ = {}"
using assms
unfolding DBM_zone_repr_def DBM_val_bounded_def DBM.neutral DBM.less_eq[symmetric] by auto
lemma empty_dbm_empty_zone:
"[empty_dbm]⇘v,n⇙ = {}"
unfolding empty_dbm_def by (rule neg_diag_zero_empty_dbmI) (simp add: DBM.neutral)
lemma canonical_empty_dbm:
"canonical empty_dbm n"
unfolding empty_dbm_def by (auto simp: DBM.add)
lemma dbm_int_empty_dbm:
"dbm_int empty_dbm n"
unfolding empty_dbm_def by auto
lemma dbm_nonneg_empty_dbm:
"dbm_nonneg n empty_dbm"
unfolding dbm_nonneg_def empty_dbm_def DBM.neutral by simp
lemmas [simp] = any_le_inf
lemma DBM_val_boundedD1:
assumes "u ⊢⇘v,n⇙ M" "v c ≤ n"
shows "Le (- u c) ≤ M 0 (v c)"
using assms unfolding dbm_entry_val.simps DBM_val_bounded_def by auto
lemma DBM_val_boundedD2:
assumes "u ⊢⇘v,n⇙ M" "v c ≤ n"
shows "Le (u c) ≤ M (v c) 0"
using assms unfolding dbm_entry_val.simps DBM_val_bounded_def by auto
lemma DBM_val_boundedD3:
assumes "u ⊢⇘v,n⇙ M" "v c1 ≤ n" "v c2 ≤ n"
shows "Le (u c1 - u c2) ≤ M (v c1) (v c2)"
using assms unfolding dbm_entry_val.simps DBM_val_bounded_def by force
lemma dbm_default_And:
assumes "dbm_default M n" "dbm_default M' n"
shows "dbm_default (And M M') n"
using assms by auto
lemma dbm_default_abstra:
assumes "dbm_default M n" "constraint_pair ac = (x, m)" "v x ≤ n"
shows "dbm_default (abstra ac M v) n"
using assms by (cases ac) auto
lemma dbm_default_abstr:
assumes "dbm_default M n" "∀(x, m)∈collect_clock_pairs g. v x ≤ n"
shows "dbm_default (abstr g M v) n"
using assms(1) unfolding abstr.simps
proof (rule fold_acc_preserv'[where P = "λM. dbm_default M n", rotated], goal_cases)
case (1 ac acc)
then obtain x m where "constraint_pair ac = (x, m)"
by force
with assms(2) 1 show ?case
by (intro dbm_default_abstra) (auto simp: collect_clock_pairs_def)
qed
lemma dbm_entry_dense:
fixes a b :: "'t :: time DBMEntry"
assumes "a + b ≥ 0" "b > 0"
obtains x where "x > 0" "b ≥ Le x" "Le (-x) ≤ a"
proof -
consider "a = ∞" | "a ≠ ∞" "a + b = 0" | "a ≠ ∞" "a + b > 0"
using assms(1) by force
then show ?thesis
proof cases
case 1
with assms show ?thesis
proof (cases b)
case (Le x)
with assms(2) 1 show ?thesis
by (intro that[of x]) (auto simp: DBM.neutral DBM.add)
next
case (Lt x2)
with assms(2) 1 show ?thesis
using that time_class.dense by (auto simp: DBM.neutral DBM.add)
next
case INF
with 1 assms(2) that show ?thesis
by (metis add_inf(2) any_le_inf dbm_less_eq_simps(2) neg_less_iff_less sum_gt_neutral_dest)
qed
next
case 2
then obtain x where "a = Le (-x)" "b = Le x"
unfolding neutral by (cases a; cases b; simp add: DBM.add eq_neg_iff_add_eq_0)
with ‹b > 0› show ?thesis
by (intro that[of x]; simp add: neutral)
next
case 3
note intro = that
have 1: "0 < x + y ⟹ - y ≤ x" for x y :: 't
by (metis ab_semigroup_add_class.add.commute add.right_inverse add_le_cancel_left less_imp_le)
have 2: thesis if "0 < x + y" "0 < y" "a = Le x" "b = Lt y" for x y :: 't
proof (cases "x > 0")
case True
then have "- x ≤ 0"
by auto
from ‹y > 0› dense obtain z where "0 < z" "z < y"
by auto
with that ‹- x ≤ 0› show ?thesis
using dual_order.trans by (intro intro[of z]; fastforce)
next
case False
from that have "-x < y"
using 1 minus_less_iff by fastforce
with dense obtain z where "- x < z" "z < y"
by auto
with False that show ?thesis
by (intro intro[of z]; simp add: less_imp_le minus_less_iff)
(meson leI less_le_trans neg_less_0_iff_less)
qed
include no_library_syntax
have 3: thesis if "a = Le x" "b = ∞" for x :: 't
by (smt (z3) 3(2) Le_le_LtI Lt_le_LeI add.inverse_inverse any_le_inf intro neg_0_less_iff_less
non_trivial_neg not_less order_trans sum_gt_neutral_dest that(2))
have 4: thesis if "a = Lt x" "b = ∞" for x :: 't
by (metis that ‹0 < a + b› add.inverse_inverse dbm_less_eq_simps(2) dbm_less_simps(2) intro leI
less_imp_le less_le_trans neg_0_less_iff_less sum_gt_neutral_dest)
have 5: thesis if "0 < x + y" "0 < y" "a = Lt x" "b = Le y" for x y
by (metis that Le_le_LtI antisym_conv1 diff_0_right diff_less_eq intro less_irrefl minus_diff_eq)
have 6: thesis if "0 < y" "a = Lt x" "b = Lt y" for x y
using that ‹a + b > 0›
apply -
apply (drule sum_gt_neutral_dest)
apply safe
subgoal for d
by (cases "d ≥ 0", cases "d = 0")
(smt intro Le_le_LtI Lt_le_LeI
add.inverse_inverse not_less neg_less_0_iff_less dense order_trans)+
done
have 7: thesis if "0 < x + y" "0 < y" "a = Le x" "b = Le y" for x y
using that by (intro intro[of y]) (auto simp: DBM.add intro: 1)
from ‹a + b > 0› ‹b > 0› ‹a ≠ ∞› show thesis
by (cases a; cases b) (auto simp: DBM.add neutral intro: 2 3 4 5 6 7)
qed
qed
lemma canonical_diag:
fixes M :: "'t :: time DBM"
assumes "canonical M n" "i ≤ n"
shows "M i i ≥ Lt 0"
proof (rule ccontr)
assume "¬ M i i ≥ Lt 0"
then have "M i i < Lt 0"
by auto
then have "M i i + M i i < M i i"
by (cases "M i i") (auto simp: DBM.add)
with assms show False
by force
qed
lemma canonical_diag_nonnegI:
fixes M :: "'t :: time DBM"
assumes "canonical M n" "∀i ≤ n. M i i ≠ Lt 0"
shows "∀i ≤ n. M i i ≥ 0"
proof clarify
fix i assume "i ≤ n"
then show "M i i ≥ 0"
using canonical_diag[OF assms(1) ‹i ≤ n›] assms(2) by (cases "M i i"; auto simp: DBM.neutral)
qed
context Regions_common
begin
lemma canonical_non_emptyI:
assumes "[M]⇘v,n⇙ ≠ {}"
shows "canonical (FW M n) n"
by (simp add: assms fw_shortest non_empty_cyc_free)
definition
"canonical_dbm M ≡ canonical M n ∧ dbm_nonneg n M ∧ dbm_int M n"
abbreviation
"vabstr' (Z :: ('c, t) zone) M ≡ Z = [M]⇘v,n⇙ ∧ canonical_dbm M"
lemma V_structuralI:
assumes "dbm_nonneg n M"
shows "[M]⇘v,n⇙ ⊆ V"
using clock_numbering(3) assms unfolding V_def DBM_zone_repr_def
by (clarsimp simp: neutral) (meson assms clock_numbering(1) dbm_positive dbm_nonneg_def)
lemma canonical_dbm_valid:
"valid_dbm M" if "canonical_dbm M"
using that unfolding canonical_dbm_def by (auto dest: V_structuralI)
lemma dbm_nonnegI:
assumes "canonical M n" "[M]⇘v,n⇙ ⊆ V" "∀i ≤ n. M i i ≠ Lt 0"
shows "dbm_nonneg n M"
proof (rule ccontr)
assume A: "¬ dbm_nonneg n M"
from assms(1,3) have diag_nonneg: "∀i ≤ n. M i i ≥ 0"
by (rule canonical_diag_nonnegI)
from A obtain i where "i > 0" "i ≤ n" "M 0 i > 0"
unfolding dbm_nonneg_def by auto
moreover have "M i 0 + M 0 i ≥ 0"
proof -
from assms(1) ‹i ≤ n› have "M i i ≥ Lt 0"
by (rule canonical_diag)
with ‹i ≤ n› assms(3) have "M i i ≥ 0"
by (cases "M i i"; auto simp: neutral)
also from ‹canonical M n› ‹i ≤ n› have "M i 0 + M 0 i ≥ M i i"
by auto
finally show ?thesis .
qed
ultimately obtain x where "x > 0" "M 0 i ≥ Le x" "Le (-x) ≤ M i 0"
by - (rule dbm_entry_dense)
moreover from ‹i > 0› ‹i ≤ n› obtain c where "c ∈ X" "v c ≤ n" "i = v c"
using clock_numbering by auto
moreover from clock_numbering(1) cn_weak assms(1) have "cycle_free M n"
by (intro non_empty_cycle_free canonical_nonneg_diag_non_empty diag_nonneg) auto
ultimately obtain u where "u ∈ [M]⇘v,n⇙" "u c < 0"
using assms(1)
by (auto simp: clock_numbering(1) intro: canonical_saturated_1[where M = M and v = v])
with assms(2) ‹c ∈ X› show False
unfolding V_def DBM_zone_repr_def by force
qed
lemma vabstr'_V:
obtains M where "vabstr' V M"
proof -
interpret beta_regions: Beta_Regions'
where k = "k l"
apply -
apply unfold_locales
apply (rule finite)
apply (simp add: non_empty)
apply (rule clock_numbering cn_weak not_in_X)+
done
have V_eq: "beta_regions.V = V"
unfolding beta_regions.V_def V_def ..
let ?M = "beta_regions.V_dbm"
from beta_regions.V_dbm_eq_V beta_regions.V_dbm_int beta_regions.normalized_V_dbm have *:
"[?M]⇘v,n⇙ = V" "dbm_int ?M n" "beta_regions.normalized ?M"
unfolding V_eq by auto
moreover have "dbm_nonneg n ?M"
unfolding beta_regions.V_dbm_def dbm_nonneg_def DBM.neutral by simp
ultimately show ?thesis
apply -
apply (rule that[of "FW ?M n"])
apply (rule conjI)
subgoal
using FW_zone_equiv_spec by blast
unfolding canonical_dbm_def
apply (intro conjI dbm_nonneg_FW FW_int_preservation canonical_non_emptyI)
apply (auto simp: V_def)
done
qed
lemma canonical_dbm_empty_dbm:
"canonical_dbm empty_dbm"
unfolding canonical_dbm_def
by (intro conjI canonical_empty_dbm dbm_int_empty_dbm dbm_nonneg_empty_dbm)
lemma vabstr'_empty_dbm:
"vabstr' {} empty_dbm"
by (intro conjI empty_dbm_empty_zone[symmetric] canonical_dbm_empty_dbm)
lemma vabstr'I:
assumes "dbm_int M' n" "Z' ⊆ V" "Z' = [M']⇘v,n⇙"
obtains M' where "vabstr' Z' M'"
proof (cases "Z' = {}")
case True
then show ?thesis
by (intro that[of empty_dbm], simp only: vabstr'_empty_dbm)
next
case False
with assms obtain M' where *: "Z' = [M']⇘v,n⇙" "dbm_int M' n" "canonical M' n"
by (metis FW_canonical' FW_valid_preservation FW_zone_equiv_spec
dbm_non_empty_diag valid_dbm.simps)
with assms(2) have "dbm_nonneg n M'"
by - (rule dbm_nonnegI; smt ‹Z' ≠ {}› dbm_less_eq_simps(2) dbm_non_empty_diag neutral)
let ?M = "FW M' n"
from * ‹dbm_nonneg n M'› show ?thesis
apply (intro that[of ?M] conjI)
apply (simp add: FW_zone_equiv_spec[symmetric])
unfolding canonical_dbm_def
unfolding dbm_nonneg_def[symmetric]
apply (intro conjI FW_canonical' dbm_nonneg_FW FW_int_preservation; assumption?)
subgoal diag_nonneg
using FW_zone_equiv_spec False dbm_non_empty_diag by blast
done
qed
end
context Regions_TA
begin
text ‹The following does not hold:›
lemma
fixes M :: "real DBM"
assumes "canonical M n"
and "∀i ≤ n. M 0 i ≤ 0"
shows "∀i ≤ n. 0 ≤ M i i"
oops
lemma global_clock_numbering:
"global_clock_numbering A v n"
using clock_numbering(1) clock_numbering_le cn_weak valid_abstraction by blast
sublocale step_z'_bisim_step_z_dbm': Bisimulation
"λ(l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩"
"λ(l, M) (l', M'). ∃a. A ⊢' ⟨l,M⟩ ↝⇘a⇙ ⟨l',M'⟩"
"λ(l, Z) (l', M). l' = l ∧ Z = [M]⇘v,n⇙"
apply (standard; clarsimp simp: step_z_dbm'_def step_z'_def)
subgoal
using global_clock_numbering by (auto elim!: step_z_dbm_DBM)
subgoal
by (blast dest: step_z_dbm_sound[OF _ global_clock_numbering])
done
lemma step_z_dbm_preserves_int:
"dbm_int M' n" if "A ⊢ ⟨l,M⟩ ↝⇘v,n,a⇙ ⟨l',M'⟩" "dbm_int M n"
apply (rule step_z_dbm_preserves_int; (rule that global_clock_numbering)?)
using valid_abstraction valid_abstraction_pairsD by fastforce
lemma step_z_dbm'_preserves_int:
"dbm_int M' n" if "A ⊢' ⟨l,M⟩ ↝⇘a⇙ ⟨l',M'⟩" "dbm_int M n"
using that by cases (erule step_z_dbm_preserves_int)+
lemma step_z'_vabstr':
"∃M. vabstr' Z' M" if "∃M. vabstr' Z M" "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩"
proof -
from that obtain M where "vabstr' Z M"
by auto
with step_z'_bisim_step_z_dbm'.A_B_step[of "(l, Z)" _ "(l, M)"] that(2) obtain a M' where *:
"A ⊢' ⟨l, M⟩ ↝⇘a⇙ ⟨l', M'⟩" "Z' = [M']⇘v,n⇙"
by force
with ‹vabstr' Z M› have "dbm_int M' n"
by - (rule step_z_dbm'_preserves_int, auto simp: canonical_dbm_def)
moreover from *(1) ‹vabstr' Z M› have "Z' ⊆ V"
by (metis canonical_dbm_valid step_z'_def step_z_V that(2) valid_dbm.simps)
ultimately obtain M' where "vabstr' Z' M'"
using ‹Z' = _› by - (rule vabstr'I)
then show ?thesis
by (intro exI)
qed
end
subsection ‹Instantiating the ``Sandwich'' for Extrapolations on DBMs›
=
Regions_TA where A = A +
Time_Abstract_Simulation where A = A for A :: "('a, 'c, real, 'l) ta" +
assumes : "u' ∈ V ⟹ (l, u) ≼ (l', u') ⟹ u ∈ V"
fixes extra :: "'l ⇒ real DBM ⇒ real DBM" and l⇩0 and M⇩0
assumes : "vabstr' Z M ⟹ Z ⊆ [extra l M]⇘v,n⇙"
and : "vabstr' Z M ⟹ [extra l M]⇘v,n⇙ ⊆ α l Z"
and : "finite {extra l M | M. canonical_dbm M}"
and : "dbm_int M n ⟹ dbm_int (extra l M) n"
assumes : "l⇩0 ∈ state_set A" and : "[M⇩0]⇘v,n⇙ ⊆ V" and : "dbm_int M⇩0 n"
begin
where
"apx l Z ≡ let M = (SOME M. canonical_dbm M ∧ Z = [M]⇘v,n⇙) in [extra l M]⇘v,n⇙"
lemma :
"[M]⇘v,n⇙ ⊆ apx l ([M]⇘v,n⇙)" if "canonical_dbm M"
by (smt (z3) apx_def extra_widens someI_ex that)
lemma :
"apx l ([M]⇘v,n⇙) ⊆ α l ([M]⇘v,n⇙)" if "canonical_dbm M"
by (smt (z3) apx_def extra_α someI_ex that)
lemma :
"α l Z ⊆ V" if "Z ⊆ V"
using that simulation_nonneg unfolding V_def abs_def by auto
lemma :
"apx l ([M]⇘v,n⇙) ⊆ V" if "canonical_dbm M"
proof -
from that have "apx l ([M]⇘v,n⇙) ⊆ α l ([M]⇘v,n⇙)"
by (rule apx_abs)
moreover from that have "… ⊆ V"
unfolding canonical_dbm_def by (intro α_V V_structuralI, elim conjE)
finally show ?thesis .
qed
lemma :
"apx l {} = {}"
proof -
have "vabstr' {} empty_dbm"
by (rule vabstr'_empty_dbm)
from canonical_dbm_empty_dbm have "apx l {} ⊆ α l {}"
by (subst empty_dbm_empty_zone[symmetric])+ (rule apx_abs)
also have "… = {}"
unfolding abs_def by auto
finally show ?thesis
by simp
qed
lemma :
assumes "canonical_dbm M"
shows "∃M'. apx l ([M]⇘v,n⇙) = [extra l M']⇘v,n⇙ ∧ canonical_dbm M'"
using assms unfolding apx_def by (smt (z3) someI_ex)
lemma :
assumes "vabstr' Z M" "Z ⊆ V"
obtains M where "vabstr' (apx l Z) M"
proof (cases "Z = {}")
case False
from apx_ex assms obtain M' where *:
"apx l Z = [extra l M']⇘v,n⇙" "canonical_dbm M'"
using apx_ex by blast
with FW_zone_equiv_spec have "apx l Z = [FW (extra l M') n]⇘v,n⇙"
by auto
moreover from ‹canonical_dbm M'› have "canonical_dbm (FW (extra l M') n)"
proof -
from assms have "Z ⊆ apx l Z"
by (auto intro!: apx_widens)
with ‹Z ≠ {}› have "apx l Z ≠ {}"
by auto
then have "canonical (FW (extra l M') n) n"
unfolding * by (rule canonical_non_emptyI)
moreover have "dbm_nonneg n (FW (extra l M') n)"
using ‹apx l Z = [FW (extra l M') n]⇘v,n⇙› ‹apx l Z ≠ {}› ‹canonical (FW _ _) _›
apply (intro dbm_nonnegI)
apply assumption
subgoal
using apx_V assms(1) by blast
subgoal
by (metis DBMEntry.distinct(1) Le_less_Lt antisym_conv dbm_non_empty_diag leI neutral)
done
moreover have "dbm_int (FW (extra l M') n) n"
using *(2) unfolding canonical_dbm_def by (intro FW_int_preservation extra_int, elim conjE)
ultimately show ?thesis
unfolding canonical_dbm_def by (intro conjI)
qed
ultimately show ?thesis
by (auto intro: that)
next
case True
then show ?thesis
by (intro that[of empty_dbm])(auto simp: empty_dbm_empty_zone apx_empty canonical_dbm_empty_dbm)
qed
lemma :
"finite {apx l Z |l Z. ∃M. vabstr' Z M ∧ l ∈ state_set A}" (is "finite ?S")
proof -
{ fix l assume "l ∈ state_set A"
from extra_finite have "finite {[extra l M]⇘v,n⇙ | M. canonical_dbm M}"
proof -
have "{[extra l M]⇘v,n⇙ | M. canonical_dbm M}
= (λM. [M]⇘v,n⇙) ` {extra l M | M. canonical_dbm M}"
by auto
with extra_finite show ?thesis
by simp
qed
also from apx_ex have "{apx l Z |Z. ∃M. vabstr' Z M} ⊆ …"
by auto
finally (finite_subset[rotated]) have "finite {apx l Z |Z. ∃M. vabstr' Z M}" .
} note * = this
have "?S = (⋃ l ∈ state_set A. {apx l Z |Z. ∃M. vabstr' Z M})"
by auto
also have "finite …"
using * finite_state_set by auto
finally show ?thesis .
qed
sublocale Time_Abstract_Simulation_Sandwich
where β = apx and I = "λZ. ∃M. vabstr' Z M" and Z⇩0 = "[M⇩0]⇘v,n⇙"
proof standard
show "u ∈ V" if "(l, u) ≼ (l', u')" "u' ∈ V" for l l' :: 'l and u u' :: "'c ⇒ real"
using that by (rule simulation_nonneg[rotated])
show "∃M. vabstr' Z' M"
if "∃M. vabstr' Z M" and "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" for Z Z' :: "('c ⇒ real) set" and l l' :: 'l
using that by (rule step_z'_vabstr')
show "apx l Z ⊆ α l Z"
if "∃M. vabstr' Z M" "Z ⊆ V" for Z :: "('c ⇒ real) set" and l :: 'l
using that apx_abs by auto
show "Z ⊆ apx l Z" if "∃M. vabstr' Z M" "Z ⊆ V" for Z :: "('c ⇒ real) set" and l :: 'l
using that apx_widens by auto
show "∃M. vabstr' (apx l Z) M"
if "∃M. vabstr' Z M" "Z ⊆ V" for Z :: "('c ⇒ real) set" and l :: 'l
using that by (elim exE) (rule vabstr'_apx, auto)
show "finite {apx l Z |l Z. (∃M. vabstr' Z M) ∧ Z ⊆ V ∧ l ∈ state_set A}"
using apx_finite by (rule finite_subset[rotated]) auto
show "l⇩0 ∈ state_set A"
by (rule l⇩0_state_set)
show "[M⇩0]⇘v,n⇙ ⊆ V"
by (rule M⇩0_V)
show "∃M. vabstr' ([M⇩0]⇘v,n⇙) M"
by (rule vabstr'I; (rule M⇩0_int M⇩0_V)?) auto
qed
end
end