Theory Simulation_Graphs_TA
theory Simulation_Graphs_TA
imports Simulation_Graphs DBM_Zone_Semantics Approx_Beta
begin
section ‹Instantiation of Simulation Locales›
inductive step_trans ::
"('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) cval ⇒ (('c, 't) cconstraint × 'a × 'c list)
⇒ 's ⇒ ('c, 't) cval ⇒ bool"
(‹_ ⊢⇩t ⟨_, _⟩ →⇘_⇙ ⟨_, _⟩› [61,61,61] 61)
where
"⟦A ⊢ l ⟶⇗g,a,r⇖ l'; u ⊢ g; u' ⊢ inv_of A l'; u' = [r → 0]u⟧
⟹ (A ⊢⇩t ⟨l, u⟩ →⇘(g,a,r)⇙ ⟨l', u'⟩)"
inductive step_trans' ::
"('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) cval ⇒ ('c, 't) cconstraint × 'a × 'c list
⇒ 's ⇒ ('c, 't) cval ⇒ bool"
(‹_ ⊢'' ⟨_, _⟩ →⇗_⇖ ⟨_, _⟩› [61,61,61,61] 61)
where
step': "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l', u'⟩ ⟹ A ⊢⇩t ⟨l', u'⟩ →⇘t⇙ ⟨l'', u''⟩ ⟹ A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l'', u''⟩"
inductive step_trans_z ::
"('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) zone
⇒ (('c, 't) cconstraint × 'a × 'c list) action ⇒ 's ⇒ ('c, 't) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇗_⇖ ⟨_, _⟩› [61,61,61,61] 61)
where
step_trans_t_z:
"A ⊢ ⟨l, Z⟩ ↝⇗τ⇖ ⟨l, Z⇧↑ ∩ {u. u ⊢ inv_of A l}⟩" |
step_trans_a_z:
"A ⊢ ⟨l, Z⟩ ↝⇗↿(g,a,r)⇖ ⟨l', zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}⟩"
if "A ⊢ l ⟶⇗g,a,r⇖ l'"
inductive step_trans_z' ::
"('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) zone ⇒ (('c, 't) cconstraint × 'a × 'c list)
⇒ 's ⇒ ('c, 't) zone ⇒ bool"
(‹_ ⊢'' ⟨_, _⟩ ↝⇗_⇖ ⟨_, _⟩› [61,61,61,61] 61)
where
step_trans_z':
"A ⊢ ⟨l, Z⟩ ↝⇗τ⇖ ⟨l, Z'⟩ ⟹ A ⊢ ⟨l, Z'⟩ ↝⇗↿t⇖ ⟨l', Z''⟩ ⟹ A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z''⟩"
lemmas [intro] =
step_trans.intros
step_trans'.intros
step_trans_z.intros
step_trans_z'.intros
context
notes [elim!] =
step.cases step_t.cases
step_trans.cases step_trans'.cases step_trans_z.cases step_trans_z'.cases
begin
lemma step_trans_t_z_sound:
"A ⊢ ⟨l, Z⟩ ↝⇗τ⇖ ⟨l',Z'⟩ ⟹ ∀ u' ∈ Z'. ∃ u ∈ Z. ∃ d. A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩"
by (auto 4 5 simp: zone_delay_def zone_set_def)
lemma step_trans_a_z_sound:
"A ⊢ ⟨l, Z⟩ ↝⇗↿t⇖ ⟨l',Z'⟩ ⟹ ∀ u' ∈ Z'. ∃ u ∈ Z. ∃ d. A ⊢⇩t ⟨l, u⟩ →⇘t⇙ ⟨l',u'⟩"
by (auto 4 4 simp: zone_delay_def zone_set_def)
lemma step_trans_a_z_complete:
"A ⊢⇩t ⟨l, u⟩ →⇘t⇙ ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z'. A ⊢ ⟨l, Z⟩ ↝⇗↿t⇖ ⟨l', Z'⟩ ∧ u' ∈ Z'"
by (auto 4 4 simp: zone_delay_def zone_set_def elim!: step_a.cases)
lemma step_trans_t_z_complete:
"A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z'. A ⊢ ⟨l, Z⟩ ↝⇗τ⇖ ⟨l', Z'⟩ ∧ u' ∈ Z'"
by (auto 4 4 simp: zone_delay_def zone_set_def elim!: step_a.cases)
lemma step_trans_t_z_iff:
"A ⊢ ⟨l, Z⟩ ↝⇗τ⇖ ⟨l', Z'⟩ = A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l', Z'⟩"
by auto
lemma step_z_complete:
"A ⊢ ⟨l, u⟩ → ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z' t. A ⊢ ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩ ∧ u' ∈ Z'"
by (auto 4 4 simp: zone_delay_def zone_set_def elim!: step_a.cases)
lemma step_trans_a_z_exact:
"u' ∈ Z'" if "A ⊢⇩t ⟨l, u⟩ →⇘t⇙ ⟨l', u'⟩" "A ⊢ ⟨l, Z⟩ ↝⇗↿t⇖ ⟨l', Z'⟩" "u ∈ Z"
using that by (auto 4 4 simp: zone_delay_def zone_set_def)
lemma step_trans_t_z_exact:
"u' ∈ Z'" if "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l', u'⟩" "A ⊢ ⟨l, Z⟩ ↝⇗τ⇖ ⟨l', Z'⟩" "u ∈ Z"
using that by (auto simp: zone_delay_def)
lemma step_trans_z'_exact:
"u' ∈ Z'" if "A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l', u'⟩" "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩" "u ∈ Z"
using that by (auto 4 4 simp: zone_delay_def zone_set_def)
lemma step_trans_z_step_z_action:
"A ⊢ ⟨l, Z⟩ ↝⇘↿a⇙ ⟨l',Z'⟩" if "A ⊢ ⟨l, Z⟩ ↝⇗↿(g,a,r)⇖ ⟨l', Z'⟩"
using that by auto
lemma step_trans_z_step_z:
"∃ a. A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩" if "A ⊢ ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩"
using that by auto
lemma step_z_step_trans_z_action:
"∃ g r. A ⊢ ⟨l, Z⟩ ↝⇗↿(g,a,r)⇖ ⟨l', Z'⟩" if "A ⊢ ⟨l, Z⟩ ↝⇘↿a⇙ ⟨l',Z'⟩"
using that by (auto 4 4)
lemma step_z_step_trans_z:
"∃ t. A ⊢ ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩" if "A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩"
using that by cases auto
end
lemma step_z'_step_trans_z':
"∃ t. A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z''⟩" if "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z''⟩"
using that unfolding step_z'_def
by (auto dest!: step_z_step_trans_z_action simp: step_trans_t_z_iff[symmetric])
lemma step_trans_z'_step_z':
"A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z''⟩" if "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z''⟩"
using that unfolding step_z'_def
by (auto elim!: step_trans_z'.cases dest!: step_trans_z_step_z_action simp: step_trans_t_z_iff)
lemma step_trans_z_determ:
"Z1 = Z2" if "A ⊢ ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z1⟩" "A ⊢ ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z2⟩"
using that by (auto elim!: step_trans_z.cases)
lemma step_trans_z'_determ:
"Z1 = Z2" if "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z1⟩" "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z2⟩"
using that by (auto elim!: step_trans_z'.cases step_trans_z.cases)
lemma (in Alpha_defs) step_trans_z_V: "A ⊢ ⟨l, Z⟩ ↝⇗t⇖ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V"
by (induction rule: step_trans_z.induct; blast intro!: reset_V le_infI1 up_V)
subsection ‹Additional Lemmas on Regions›
context AlphaClosure
begin
inductive step_trans_r ::
"('a, 'c, t, 's) ta ⇒ _ ⇒ 's ⇒ ('c, t) zone ⇒ (('c, t) cconstraint × 'a × 'c list) action
⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_,_ ⊢ ⟨_, _⟩ ↝⇗_⇖ ⟨_, _⟩› [61,61,61,61,61] 61)
where
step_trans_t_r:
"A,ℛ ⊢ ⟨l,R⟩ ↝⇗τ⇖ ⟨l,R'⟩" if
"valid_abstraction A X (λ x. real o k x)" "R ∈ ℛ l" "R' ∈ Succ (ℛ l) R" "R' ⊆ ⦃inv_of A l⦄" |
step_trans_a_r:
"A,ℛ ⊢ ⟨l,R⟩ ↝⇗↿(g,a,r)⇖ ⟨l', R'⟩" if
"valid_abstraction A X (λ x. real o k x)" "A ⊢ l ⟶⇗g,a,r⇖ l'" "R ∈ ℛ l"
"R ⊆ ⦃g⦄" "region_set' R r 0 ⊆ R'" "R' ⊆ ⦃inv_of A l'⦄" "R' ∈ ℛ l'"
lemmas [intro] = step_trans_r.intros
lemma step_trans_t_r_iff[simp]:
"A,ℛ ⊢ ⟨l,R⟩ ↝⇗τ⇖ ⟨l',R'⟩ = A,ℛ ⊢ ⟨l,R⟩ ↝⇘τ⇙ ⟨l',R'⟩"
by (auto elim!: step_trans_r.cases)
lemma step_trans_r_step_r_action:
"A,ℛ ⊢ ⟨l,R⟩ ↝⇘↿a⇙ ⟨l',R'⟩" if "A,ℛ ⊢ ⟨l,R⟩ ↝⇗↿(g,a,r)⇖ ⟨l',R'⟩"
using that by (auto elim: step_trans_r.cases)
lemma step_r_step_trans_r_action:
"∃ g r. A,ℛ ⊢ ⟨l,R⟩ ↝⇗↿(g,a,r)⇖ ⟨l',R'⟩" if "A,ℛ ⊢ ⟨l,R⟩ ↝⇘↿a⇙ ⟨l',R'⟩"
using that by (auto elim: step_trans_r.cases)
inductive step_trans_r' ::
"('a, 'c, t, 's) ta ⇒ _ ⇒ 's ⇒ ('c, t) zone ⇒ ('c, t) cconstraint × 'a × 'c list
⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_,_ ⊢'' ⟨_, _⟩ ↝⇗_⇖ ⟨_, _⟩› [61,61,61,61,61] 61)
where
"A,ℛ ⊢' ⟨l,R⟩ ↝⇗t⇖ ⟨l',R''⟩" if "A,ℛ ⊢ ⟨l,R⟩ ↝⇗τ⇖ ⟨l,R'⟩" "A,ℛ ⊢ ⟨l,R'⟩ ↝⇗↿t⇖ ⟨l', R''⟩"
lemma step_trans_r'_step_r':
"A,ℛ ⊢ ⟨l,R⟩ ↝⇩a ⟨l',R'⟩" if "A,ℛ ⊢' ⟨l,R⟩ ↝⇗(g,a,r)⇖ ⟨l',R'⟩"
using that by cases (auto dest: step_trans_r_step_r_action intro!: step_r'.intros)
lemma step_r'_step_trans_r':
"∃ g r. A,ℛ ⊢' ⟨l,R⟩ ↝⇗(g,a,r)⇖ ⟨l',R'⟩" if "A,ℛ ⊢ ⟨l,R⟩ ↝⇩a ⟨l',R'⟩"
using that by cases (auto dest: step_r_step_trans_r_action intro!: step_trans_r'.intros)
lemma step_trans_a_r_sound:
assumes "A,ℛ ⊢ ⟨l, R⟩ ↝⇗↿a⇖ ⟨l',R'⟩"
shows "∀ u ∈ R. ∃ u' ∈ R'. A ⊢⇩t ⟨l, u⟩ →⇘a⇙ ⟨l',u'⟩"
using assms proof cases
case A: (step_trans_a_r g a r)
show ?thesis
unfolding A(1) proof
fix u assume "u ∈ R"
from ‹u ∈ R› A have "u ⊢ g" "[r→0]u ⊢ inv_of A l'" "[r→0]u ∈ R'"
unfolding region_set'_def ccval_def by auto
with A show "∃u'∈R'. A ⊢⇩t ⟨l, u⟩ →⇘(g,a,r)⇙ ⟨l',u'⟩"
by auto
qed
qed
lemma step_trans_r'_sound:
assumes "A,ℛ ⊢' ⟨l, R⟩ ↝⇗t⇖ ⟨l', R'⟩"
shows "∀u∈R. ∃u'∈R'. A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l', u'⟩"
using assms by cases (auto 6 0 dest!: step_trans_a_r_sound step_t_r_sound)
end
context AlphaClosure
begin
context
fixes l l' :: 's and A :: "('a, 'c, t, 's) ta"
assumes valid_abstraction: "valid_abstraction A X k"
begin
interpretation alpha: AlphaClosure_global _ "k l" "ℛ l" by standard (rule finite)
lemma [simp]: "alpha.cla = cla l" unfolding alpha.cla_def cla_def ..
interpretation alpha': AlphaClosure_global _ "k l'" "ℛ l'" by standard (rule finite)
lemma [simp]: "alpha'.cla = cla l'" unfolding alpha'.cla_def cla_def ..
lemma regions_poststable1:
assumes
"A ⊢ ⟨l, Z⟩ ↝⇗a⇖ ⟨l',Z'⟩" "Z ⊆ V" "R' ∈ ℛ l'" "R' ∩ Z' ≠ {}"
shows "∃ R ∈ ℛ l. A,ℛ ⊢ ⟨l,R⟩ ↝⇗a⇖ ⟨l',R'⟩ ∧ R ∩ Z ≠ {}"
using assms proof (induction A ≡ A l ≡ l _ _ l' ≡ l' _rule: step_trans_z.induct)
case A: (step_trans_t_z Z)
from ‹R' ∩ (Z⇧↑ ∩ {u. u ⊢ inv_of A l}) ≠ {}› obtain u d where u:
"u ∈ Z" "u ⊕ d ∈ R'" "u ⊕ d ⊢ inv_of A l" "0 ≤ d"
unfolding zone_delay_def by blast+
with alpha.closure_subs[OF A(2)] obtain R where R1: "u ∈ R" "R ∈ ℛ l"
by (simp add: cla_def) blast
from ‹Z ⊆ V› ‹u ∈ Z› have "∀x∈X. 0 ≤ u x" unfolding V_def by fastforce
from region_cover'[OF this] have R: "[u]⇩l ∈ ℛ l" "u ∈ [u]⇩l" by auto
from SuccI2[OF ℛ_def' this(2,1) ‹0 ≤ d› HOL.refl] u(2) have v'1:
"[u ⊕ d]⇩l ∈ Succ (ℛ l) ([u]⇩l)" "[u ⊕ d]⇩l ∈ ℛ l"
by auto
from alpha.regions_closed'_spec[OF R(1,2) ‹0 ≤ d›] have v'2: "u ⊕ d ∈ [u ⊕ d]⇩l" by simp
from valid_abstraction have
"∀(x, m)∈clkp_set A l. m ≤ real (k l x) ∧ x ∈ X ∧ m ∈ ℕ"
by (auto elim!: valid_abstraction.cases)
then have
"∀(x, m)∈collect_clock_pairs (inv_of A l). m ≤ real (k l x) ∧ x ∈ X ∧ m ∈ ℕ"
unfolding clkp_set_def collect_clki_def inv_of_def by fastforce
from ccompatible[OF this, folded ℛ_def'] v'1(2) v'2 u(2,3) have
"[u ⊕ d]⇩l ⊆ ⦃inv_of A l⦄"
unfolding ccompatible_def ccval_def by auto
from
alpha.valid_regions_distinct_spec[OF v'1(2) _ v'2 ‹u ⊕ d ∈ R'›] ‹R' ∈ _› ‹l = l'›
alpha.region_unique_spec[OF R1]
have "[u ⊕ d]⇩l = R'" "[u]⇩l = R" by auto
from valid_abstraction ‹R ∈ _› ‹_ ∈ Succ (ℛ l) _› ‹_ ⊆ ⦃inv_of A l⦄› have
"A,ℛ ⊢ ⟨l, R⟩ ↝⇘τ⇙ ⟨l, R'⟩"
by (auto simp: comp_def ‹[u ⊕ d]⇩l = R'› ‹_ = R›)
with ‹l = l'› ‹R ∈ _› ‹u ∈ R› ‹u ∈ Z› show ?case by - (rule bexI[where x = R]; auto)
next
case A: (step_trans_a_z g a r Z)
from A(4) obtain u v' where
"u ∈ Z" and v': "v' = [r→0]u" "u ⊢ g" "v' ⊢ inv_of A l'" "v' ∈ R'"
unfolding zone_set_def by blast
from ‹u ∈ Z› alpha.closure_subs[OF A(2)] A(1) obtain u' R where u':
"u ∈ R" "u' ∈ R" "R ∈ ℛ l"
by (simp add: cla_def) blast
then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce
from region_cover'[OF this] have "[u]⇩l ∈ ℛ l" "u ∈ [u]⇩l" by auto
have *:
"[u]⇩l ⊆ ⦃g⦄" "region_set' ([u]⇩l) r 0 ⊆ [[r→0]u]⇩l'"
"[[r→0]u]⇩l' ∈ ℛ l'" "[[r→0]u]⇩l' ⊆ ⦃inv_of A l'⦄"
proof -
from valid_abstraction have "collect_clkvt (trans_of A) ⊆ X"
"∀ l g a r l' c. A ⊢ l ⟶⇗g,a,r⇖ l' ∧ c ∉ set r ⟶ k l' c ≤ k l c"
by (auto elim: valid_abstraction.cases)
with A(1) have "set r ⊆ X" "∀y. y ∉ set r ⟶ k l' y ≤ k l y"
unfolding collect_clkvt_def by (auto 4 8)
with
region_set_subs[
of _ X "k l" _ 0, where k' = "k l'", folded ℛ_def, OF ‹[u]⇩l ∈ ℛ l› ‹u ∈ [u]⇩l› finite
]
show "region_set' ([u]⇩l) r 0 ⊆ [[r→0]u]⇩l'" "[[r→0]u]⇩l' ∈ ℛ l'" by auto
from valid_abstraction have *:
"∀l. ∀(x, m)∈clkp_set A l. m ≤ real (k l x) ∧ x ∈ X ∧ m ∈ ℕ"
by (fastforce elim: valid_abstraction.cases)+
with A(1) have "∀(x, m)∈collect_clock_pairs g. m ≤ real (k l x) ∧ x ∈ X ∧ m ∈ ℕ"
unfolding clkp_set_def collect_clkt_def by fastforce
from ‹u ∈ [u]⇩l› ‹[u]⇩l ∈ ℛ l› ccompatible[OF this, folded ℛ_def] ‹u ⊢ g› show "[u]⇩l ⊆ ⦃g⦄"
unfolding ccompatible_def ccval_def by blast
have **: "[r→0]u ∈ [[r→0]u]⇩l'"
using ‹R' ∈ ℛ l'› ‹v' ∈ R'› alpha'.region_unique_spec v'(1) by blast
from * have
"∀(x, m)∈collect_clock_pairs (inv_of A l'). m ≤ real (k l' x) ∧ x ∈ X ∧ m ∈ ℕ"
unfolding inv_of_def clkp_set_def collect_clki_def by fastforce
from ** ‹[[r→0]u]⇩l' ∈ ℛ l'› ccompatible[OF this, folded ℛ_def] ‹v' ⊢ _› show
"[[r→0]u]⇩l' ⊆ ⦃inv_of A l'⦄"
unfolding ccompatible_def ccval_def ‹v' = _› by blast
qed
from * ‹v' = _› ‹u ∈ [u]⇩l› have "v' ∈ [[r→0]u]⇩l'" unfolding region_set'_def by auto
from alpha'.valid_regions_distinct_spec[OF *(3) ‹R' ∈ ℛ l'› ‹v' ∈ [[r→0]u]⇩l'› ‹v' ∈ R'›]
have "[[r→0]u]⇩l' = R'" .
from alpha.region_unique_spec[OF u'(1,3)] have "[u]⇩l = R" by auto
from A valid_abstraction ‹R ∈ _› * have "A,ℛ ⊢ ⟨l, R⟩ ↝⇗↿(g,a,r)⇖ ⟨l', R'⟩"
by (auto simp: comp_def ‹_ = R'› ‹_ = R›)
with ‹R ∈ _› ‹u ∈ R› ‹u ∈ Z› show ?case by - (rule bexI[where x = R]; auto)
qed
lemma regions_poststable':
assumes
"A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩" "Z ⊆ V" "R' ∈ ℛ l'" "R' ∩ Z' ≠ {}"
shows "∃ R ∈ ℛ l. A,ℛ ⊢ ⟨l,R⟩ ↝⇘a⇙ ⟨l',R'⟩ ∧ R ∩ Z ≠ {}"
using assms
by (cases a)
(auto dest!: regions_poststable1 dest: step_trans_r_step_r_action step_z_step_trans_z_action
simp: step_trans_t_z_iff[symmetric]
)
end
lemma regions_poststable2:
assumes valid_abstraction: "valid_abstraction A X k"
and prems: "A ⊢' ⟨l, Z⟩ ↝⇗a⇖ ⟨l',Z'⟩" "Z ⊆ V" "R' ∈ ℛ l'" "R' ∩ Z' ≠ {}"
shows "∃ R ∈ ℛ l. A,ℛ ⊢' ⟨l,R⟩ ↝⇗a⇖ ⟨l',R'⟩ ∧ R ∩ Z ≠ {}"
using prems(1) proof (cases)
case steps: (step_trans_z' Z1)
with prems have "Z1 ⊆ V"
by (blast dest: step_trans_z_V)
from regions_poststable1[OF valid_abstraction steps(2) ‹Z1 ⊆ V› prems(3,4)] obtain R1 where R1:
"R1 ∈ ℛ l" "A,ℛ ⊢ ⟨l, R1⟩ ↝⇗↿a⇖ ⟨l', R'⟩" "R1 ∩ Z1 ≠ {}"
by auto
from regions_poststable1[OF valid_abstraction steps(1) ‹Z ⊆ V› R1(1,3)] obtain R where
"R∈ℛ l" "A,ℛ ⊢ ⟨l, R⟩ ↝⇗τ⇖ ⟨l, R1⟩" "R ∩ Z ≠ {}"
by auto
with R1(2) show ?thesis
by (auto intro: step_trans_r'.intros)
qed
text ‹
Poststability of Closures:
For every transition in the zone graph and each region in the closure of the resulting zone,
there exists a similar transition in the region graph.
›
lemma regions_poststable:
assumes valid_abstraction: "valid_abstraction A X k"
and A:
"A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l',Z'⟩" "A ⊢ ⟨l', Z'⟩ ↝⇘↿a⇙ ⟨l'',Z''⟩"
"Z ⊆ V" "R'' ∈ ℛ l''" "R'' ∩ Z'' ≠ {}"
shows "∃ R ∈ ℛ l. A,ℛ ⊢ ⟨l,R⟩ ↝⇩a ⟨l'',R''⟩ ∧ R ∩ Z ≠ {}"
proof -
from A(1) ‹Z ⊆ V› have "Z' ⊆ V" by (rule step_z_V)
from A(1) have [simp]: "l' = l" by auto
from regions_poststable'[OF valid_abstraction A(2) ‹Z' ⊆ V› ‹R'' ∈ _› ‹R'' ∩ Z'' ≠ {}›] obtain R'
where R': "R'∈ℛ l'" "A,ℛ ⊢ ⟨l', R'⟩ ↝⇘↿a⇙ ⟨l'', R''⟩" "R' ∩ Z' ≠ {}"
by auto
from regions_poststable'[OF valid_abstraction A(1) ‹Z ⊆ V› R'(1,3)] obtain R where
"R ∈ ℛ l" "A,ℛ ⊢ ⟨l, R⟩ ↝⇘τ⇙ ⟨l, R'⟩" "R ∩ Z ≠ {}"
by auto
with R'(2) show ?thesis by - (rule bexI[where x = "R"]; auto intro: step_r'.intros)
qed
lemma step_t_r_loc:
"l' = l" if "A,ℛ ⊢ ⟨l, R⟩ ↝⇘τ⇙ ⟨l', R'⟩"
using that by cases auto
lemma ℛ_V:
"u ∈ V" if "R ∈ ℛ l" "u ∈ R"
using that unfolding ℛ_def V_def by auto
lemma step_r'_complete:
assumes "A ⊢' ⟨l, u⟩ → ⟨l',u'⟩" "valid_abstraction A X (λ x. real o k x)" "u ∈ V"
shows "∃ a R'. u' ∈ R' ∧ A,ℛ ⊢ ⟨l, [u]⇩l⟩ ↝⇩a ⟨l',R'⟩"
using assms
apply cases
apply (drule step_t_r_complete, (rule assms; fail), simp add: V_def)
apply clarify
apply (frule step_a_r_complete)
by (auto dest: step_t_r_loc simp: ℛ_def simp: region_unique intro!: step_r'.intros)
lemma step_r_ℛ:
"R' ∈ ℛ l'" if "A,ℛ ⊢ ⟨l, R⟩ ↝⇘a⇙ ⟨l', R'⟩"
using that by (auto elim: step_r.cases)
lemma step_r'_ℛ:
"R' ∈ ℛ l'" if "A,ℛ ⊢ ⟨l, R⟩ ↝⇩a ⟨l', R'⟩"
using that by (auto intro: step_r_ℛ elim: step_r'.cases)
end
context Regions
begin
lemma closure_parts_mono:
"{R ∈ ℛ l. R ∩ Z ≠ {}} ⊆ {R ∈ ℛ l. R ∩ Z' ≠ {}}" if "Closure⇩α⇩,⇩l Z ⊆ Closure⇩α⇩,⇩l Z'"
proof (clarify, goal_cases)
case prems: (1 R)
with that have "R ⊆ Closure⇩α⇩,⇩l Z'"
unfolding cla_def by auto
from ‹_ ≠ {}› obtain u where "u ∈ R" "u ∈ Z" by auto
with ‹R ⊆ _› obtain R' where "R' ∈ ℛ l" "u ∈ R'" "R' ∩ Z' ≠ {}" unfolding cla_def by force
from ℛ_regions_distinct[OF ℛ_def' this(1,2) ‹R ∈ _›] ‹u ∈ R› have "R = R'" by auto
with ‹R' ∩ Z' ≠ {}› ‹R ∩ Z' = {}› show ?case by simp
qed
lemma closure_parts_id:
"{R ∈ ℛ l. R ∩ Z ≠ {}} = {R ∈ ℛ l. R ∩ Z' ≠ {}}" if
"Closure⇩α⇩,⇩l Z = Closure⇩α⇩,⇩l Z'"
using closure_parts_mono that by blast
paragraph ‹More lemmas on regions›
context
fixes l' :: 's
begin
interpretation regions: Regions_global _ _ _ "k l'"
by standard (rule finite clock_numbering not_in_X non_empty)+
context
fixes A :: "('a, 'c, t, 's) ta"
assumes valid_abstraction: "valid_abstraction A X k"
begin
lemmas regions_poststable = regions_poststable[OF valid_abstraction]
lemma clkp_set_clkp_set1:
"∃ l. (c, x) ∈ clkp_set A l" if "(c, x) ∈ Timed_Automata.clkp_set A"
using that
unfolding Timed_Automata.clkp_set_def Closure.clkp_set_def
unfolding Timed_Automata.collect_clki_def Closure.collect_clki_def
unfolding Timed_Automata.collect_clkt_def Closure.collect_clkt_def
by fastforce
lemma clkp_set_clkp_set2:
"(c, x) ∈ Timed_Automata.clkp_set A" if "(c, x) ∈ clkp_set A l" for l
using that
unfolding Timed_Automata.clkp_set_def Closure.clkp_set_def
unfolding Timed_Automata.collect_clki_def Closure.collect_clki_def
unfolding Timed_Automata.collect_clkt_def Closure.collect_clkt_def
by fastforce
lemma clock_numbering_le: "∀c∈clk_set A. v c ≤ n"
proof
fix c assume "c ∈ clk_set A"
then have "c ∈ X"
proof (safe, clarsimp, goal_cases)
case (1 x)
then obtain l where "(c, x) ∈ clkp_set A l" by (auto dest: clkp_set_clkp_set1)
with valid_abstraction show "c ∈ X" by (auto elim!: valid_abstraction.cases)
next
case 2
with valid_abstraction show "c ∈ X" by (auto elim!: valid_abstraction.cases)
qed
with clock_numbering show "v c ≤ n" by auto
qed
lemma beta_alpha_step:
"A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l', Closure⇩α⇩,⇩l' Z'⟩" if "A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l', Z'⟩" "Z ∈ V'"
proof -
from that obtain Z1' where Z1': "Z' = Approx⇩β l' Z1'" "A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l', Z1'⟩"
by (clarsimp elim!: step_z_beta.cases)
with ‹Z ∈ V'› have "Z1' ∈ V'"
using valid_abstraction clock_numbering_le by (auto intro: step_z_V')
let ?alpha = "Closure⇩α⇩,⇩l' Z1'" and ?beta = "Closure⇩α⇩,⇩l' (Approx⇩β l' Z1')"
have "?beta ⊆ ?alpha"
using regions.approx_β_closure_α'[OF ‹Z1' ∈ V'›] regions.alpha_interp.closure_involutive
by (auto 4 3 dest: regions.alpha_interp.cla_mono)
moreover have "?alpha ⊆ ?beta"
by (intro regions.alpha_interp.cla_mono[simplified] regions.beta_interp.apx_subset)
ultimately have "?beta = ?alpha" ..
with Z1' show ?thesis by auto
qed
lemma beta_alpha_region_step:
"∃ a. ∃ R ∈ ℛ l. R ∩ Z ≠ {} ∧ A,ℛ ⊢ ⟨l, R⟩ ↝⇩a ⟨l', R'⟩" if
"A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩" "Z ∈ V'" "R' ∈ ℛ l'" "R' ∩ Z' ≠ {}"
proof -
from that(1) obtain l'' a Z'' where steps:
"A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l'', Z''⟩" "A ⊢ ⟨l'', Z''⟩ ↝⇘β(↿a)⇙ ⟨l', Z'⟩"
unfolding step_z_beta'_def by metis
with ‹Z ∈ V'› steps(1) have "Z'' ∈ V'"
using valid_abstraction clock_numbering_le by (blast intro: step_z_V')
from beta_alpha_step[OF steps(2) this] have "A ⊢ ⟨l'', Z''⟩ ↝⇘α↿a⇙ ⟨l', Closure⇩α⇩,⇩l'(Z')⟩" .
from step_z_alpha.cases[OF this] obtain Z1 where Z1:
"A ⊢ ⟨l'', Z''⟩ ↝⇘↿a⇙ ⟨l', Z1⟩" "Closure⇩α⇩,⇩l'(Z') = Closure⇩α⇩,⇩l'(Z1)"
by metis
from closure_parts_id[OF this(2)] that(3,4) have "R' ∩ Z1 ≠ {}" by blast
from regions_poststable[OF steps(1) Z1(1) _ ‹R' ∈ _› this] ‹Z ∈ V'› show ?thesis
by (auto dest: V'_V)
qed
lemmas step_z_beta'_V' = step_z_beta'_V'[OF valid_abstraction clock_numbering_le]
lemma step_trans_z'_closure_subs:
assumes
"A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩" "Z ⊆ V" "∀ R ∈ ℛ l. R ∩ Z ≠ {} ⟶ R ∩ W ≠ {}"
shows
"∃ W'. A ⊢' ⟨l, W⟩ ↝⇗t⇖ ⟨l', W'⟩ ∧ (∀ R ∈ ℛ l'. R ∩ Z' ≠ {} ⟶ R ∩ W' ≠ {})"
proof -
from assms(1) obtain W' where step: "A ⊢' ⟨l, W⟩ ↝⇗t⇖ ⟨l', W'⟩"
by (auto elim!: step_trans_z.cases step_trans_z'.cases)
have "R' ∩ W' ≠ {}" if "R' ∈ ℛ l'" "R' ∩ Z' ≠ {}" for R'
proof -
from regions_poststable2[OF valid_abstraction assms(1) _ that] ‹Z ⊆ V› obtain R where R:
"R∈ℛ l" "A,ℛ ⊢' ⟨l, R⟩ ↝⇗t⇖ ⟨l', R'⟩" "R ∩ Z ≠ {}"
by auto
with assms(3) obtain u where "u ∈ R" "u ∈ W"
by auto
with step_trans_r'_sound[OF R(2)] obtain u' where "u' ∈ R'" "A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l', u'⟩"
by auto
with step_trans_z'_exact[OF this(2) step ‹u ∈ W›] show ?thesis
by auto
qed
with step show ?thesis
by auto
qed
lemma step_trans_z'_closure_eq:
assumes
"A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩" "Z ⊆ V" "W ⊆ V" "∀ R ∈ ℛ l. R ∩ Z ≠ {} ⟷ R ∩ W ≠ {}"
shows
"∃ W'. A ⊢' ⟨l, W⟩ ↝⇗t⇖ ⟨l', W'⟩ ∧ (∀ R ∈ ℛ l'. R ∩ Z' ≠ {} ⟷ R ∩ W' ≠ {})"
proof -
from assms(4) have *:
"∀ R ∈ ℛ l. R ∩ Z ≠ {} ⟶ R ∩ W ≠ {}" "∀ R ∈ ℛ l. R ∩ W ≠ {} ⟶ R ∩ Z ≠ {}"
by auto
from step_trans_z'_closure_subs[OF assms(1,2) *(1)] obtain W' where W':
"A ⊢' ⟨l, W⟩ ↝⇗t⇖ ⟨l', W'⟩" "(∀R∈ℛ l'. R ∩ Z' ≠ {} ⟶ R ∩ W' ≠ {})"
by auto
with step_trans_z'_closure_subs[OF W'(1) ‹W ⊆ V› *(2)] assms(1) show ?thesis
by (fastforce dest: step_trans_z'_determ)
qed
lemma step_z'_closure_subs:
assumes
"A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" "Z ⊆ V" "∀ R ∈ ℛ l. R ∩ Z ≠ {} ⟶ R ∩ W ≠ {}"
shows
"∃ W'. A ⊢ ⟨l, W⟩ ↝ ⟨l', W'⟩ ∧ (∀ R ∈ ℛ l'. R ∩ Z' ≠ {} ⟶ R ∩ W' ≠ {})"
using assms(1)
by (auto
dest: step_trans_z'_step_z'
dest!: step_z'_step_trans_z' step_trans_z'_closure_subs[OF _ assms(2,3)]
)
end
lemma apx_finite:
"finite {Approx⇩β l' Z | Z. Z ⊆ V}" (is "finite ?S")
proof -
have "finite regions.ℛ⇩β"
by (simp add: regions.beta_interp.finite_ℛ)
then have "finite {S. S ⊆ regions.ℛ⇩β}"
by auto
then have "finite {⋃ S | S. S ⊆ regions.ℛ⇩β}"
by auto
moreover have "?S ⊆ {⋃ S | S. S ⊆ regions.ℛ⇩β}"
by (auto dest!: regions.beta_interp.apx_in)
ultimately show ?thesis by (rule finite_subset[rotated])
qed
lemmas apx_subset = regions.beta_interp.apx_subset
lemma step_z_beta'_empty:
"Z' = {}" if "A ⊢ ⟨l, {}⟩ ↝⇩β ⟨l', Z'⟩"
using that
by (auto
elim!: step_z.cases
simp: step_z_beta'_def regions.beta_interp.apx_empty zone_delay_def zone_set_def
)
end
lemma step_z_beta'_complete:
assumes "A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" "u ∈ Z" "Z ⊆ V"
shows "∃ Z'. A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩ ∧ u' ∈ Z'"
proof -
from assms(1) obtain l'' u'' d a where steps:
"A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l'', u''⟩" "A ⊢ ⟨l'', u''⟩ →⇘a⇙ ⟨l', u'⟩"
by (force elim!: step'.cases)
then obtain Z'' where
"A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l'', Z''⟩" "u'' ∈ Z''"
by (meson ‹u ∈ Z› step_t_z_complete)
moreover with steps(2) obtain Z' where
"A ⊢ ⟨l'', Z''⟩ ↝⇘↿a⇙ ⟨l', Z'⟩" "u' ∈ Z'"
by (meson ‹u'' ∈ Z''› step_a_z_complete)
ultimately show ?thesis
unfolding step_z_beta'_def using ‹Z ⊆ V› apx_subset by blast
qed
end
subsection ‹Instantiation of Double Simulation›
subsection ‹Auxiliary Definitions›
definition state_set :: "('a, 'c, 'time, 's) ta ⇒ 's set" where
"state_set A ≡ fst ` (fst A) ∪ (snd o snd o snd o snd) ` (fst A)"
lemma finite_trans_of_finite_state_set:
"finite (state_set A)" if "finite (trans_of A)"
using that unfolding state_set_def trans_of_def by auto
lemma state_setI1:
"l ∈ state_set A" if "A ⊢ l ⟶⇗g,a,r⇖ l'"
using that unfolding state_set_def trans_of_def image_def by (auto 4 4)
lemma state_setI2:
"l' ∈ state_set A" if "A ⊢ l ⟶⇗g,a,r⇖ l'"
using that unfolding state_set_def trans_of_def image_def by (auto 4 4)
lemma (in AlphaClosure) step_r'_state_set:
"l' ∈ state_set A" if "A,ℛ ⊢ ⟨l, R⟩ ↝⇩a ⟨l', R'⟩"
using that by (blast intro: state_setI2 elim: step_r'.cases)
lemma (in Regions) step_z_beta'_state_set2:
"l' ∈ state_set A" if "A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩"
using that unfolding step_z_beta'_def by (force simp: state_set_def trans_of_def)
subsection ‹Instantiation›
locale Regions_TA = Regions X _ _ k for X :: "'c set" and k :: "'s ⇒ 'c ⇒ nat" +
fixes A :: "('a, 'c, t, 's) ta"
assumes valid_abstraction: "valid_abstraction A X k"
and finite_state_set: "finite (state_set A)"
begin
no_notation Regions_Beta.part (‹[_]⇩_› [61,61] 61)
notation part'' (‹[_]⇩_› [61,61] 61)
lemma step_z_beta'_state_set1:
"l ∈ state_set A" if "A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩"
using that unfolding step_z_beta'_def by (force simp: state_set_def trans_of_def)
sublocale sim: Double_Simulation_paired
"λ (l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩"
"λ (l, Z) (l', Z'). ∃ a. A,ℛ ⊢ ⟨l, Z⟩ ↝⇩a ⟨l', Z'⟩ ∧ Z' ≠ {}"
"λ (l, R). l ∈ state_set A ∧ R ∈ ℛ l"
"λ (l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩ ∧ Z' ≠ {}"
"λ (l, Z). l ∈ state_set A ∧ Z ∈ V' ∧ Z ≠ {}"
proof (standard, goal_cases)
case (1 S T)
then show ?case
by (auto dest!: step_r'_sound)
next
case prems: (2 R' l' Z' l Z)
from prems(3) have "l ∈ state_set A"
by (blast intro: step_z_beta'_state_set1)
from prems show ?case
unfolding Double_Simulation_paired_Defs.closure'_def
by (blast dest: beta_alpha_region_step[OF valid_abstraction] step_z_beta'_state_set1)
next
case prems: (3 l R R')
then show ?case
using ℛ_regions_distinct[OF ℛ_def'] by auto
next
case 4
have *: "finite (ℛ l)" for l
unfolding ℛ_def by (intro finite_ℛ finite)
have
"{(l, R). l ∈ state_set A ∧ R ∈ ℛ l} = (⋃ l ∈ state_set A. ((λ R. (l, R)) ` {R. R ∈ ℛ l}))"
by auto
also have "finite …"
by (auto intro: finite_UN_I[OF finite_state_set] *)
finally show ?case by auto
next
case (5 l Z)
then show ?case
apply safe
subgoal for u
using region_cover'[of u l] by (auto dest!: V'_V, auto simp: V_def)
done
qed
sublocale Graph_Defs
"λ (l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩ ∧ Z' ≠ {}" .
lemmas step_z_beta'_V' = step_z_beta'_V'[OF valid_abstraction]
lemma step_r'_complete_spec:
assumes "A ⊢' ⟨l, u⟩ → ⟨l',u'⟩" "u ∈ V"
shows "∃ a R'. u' ∈ R' ∧ A,ℛ ⊢ ⟨l, [u]⇩l⟩ ↝⇩a ⟨l',R'⟩"
using assms valid_abstraction by (auto simp: comp_def V_def intro!: step_r'_complete)
end
subsection ‹Büchi Runs›
locale Regions_TA_Start_State = Regions_TA _ _ _ _ _ A for A :: "('a, 'c, t, 's) ta" +
fixes l⇩0 :: "'s" and Z⇩0 :: "('c, t) zone"
assumes start_state: "l⇩0 ∈ state_set A" "Z⇩0 ∈ V'" "Z⇩0 ≠ {}"
begin
definition "a⇩0 = from_R l⇩0 Z⇩0"
sublocale sim_complete': Double_Simulation_Finite_Complete_paired
"λ (l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩"
"λ (l, Z) (l', Z'). ∃ a. A,ℛ ⊢ ⟨l, Z⟩ ↝⇩a ⟨l', Z'⟩ ∧ Z' ≠ {}"
"λ (l, R). l ∈ state_set A ∧ R ∈ ℛ l"
"λ (l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩ ∧ Z' ≠ {}"
"λ (l, Z). l ∈ state_set A ∧ Z ∈ V' ∧ Z ≠ {}"
l⇩0 Z⇩0
proof (standard, goal_cases)
case (1 x y S)
then show ?case
by (force dest: step_z_beta'_complete[rotated 2, OF V'_V])
next
case 4
have *: "Z ∈ V'" if "A ⊢ ⟨l⇩0, Z⇩0⟩ ↝⇩β* ⟨l, Z⟩" for l Z
using that start_state step_z_beta'_V' by (induction rule: rtranclp_induct2) blast+
have "Z ∈ {Approx⇩β l Z | Z. Z ⊆ V} ∨ (l, Z) = (l⇩0, Z⇩0)"
if "reaches (l⇩0, Z⇩0) (l, Z)" for l Z
using that proof (induction rule: rtranclp_induct2)
case refl
then show ?case
by simp
next
case prems: (step l Z l' Z')
from prems(1) have "A ⊢ ⟨l⇩0, Z⇩0⟩ ↝⇩β* ⟨l, Z⟩"
by induction (auto intro: rtranclp_trans)
then have "Z ∈ V'"
by (rule *)
with prems show ?case
unfolding step_z_beta'_def using start_state(2) by (auto 0 1 dest!: V'_V elim!: step_z_V)
qed
then have "{(l, Z). reaches (l⇩0, Z⇩0) (l, Z) ∧ l ∈ state_set A ∧ Z ∈ V' ∧ Z ≠ {}}
⊆ {(l, Z) | l Z. l ∈ state_set A ∧ Z ∈ {Approx⇩β l Z | Z. Z ⊆ V}} ∪ {(l⇩0, Z⇩0)}"
by auto
also have "finite …" (is "finite ?S")
proof -
have "?S = {(l⇩0, Z⇩0)} ∪ ⋃ ((λ l. (λ Z. (l, Z)) ` {Approx⇩β l Z | Z. Z ⊆ V}) ` (state_set A))"
by blast
also have "finite …"
by (blast intro: apx_finite finite_state_set)
finally show ?thesis .
qed
finally show ?case
by simp
next
case prems: (2 a a')
then show ?case
by (auto intro: step_z_beta'_V' step_z_beta'_state_set2)
next
case 3
from start_state show ?case unfolding a⇩0_def by (auto simp: from_R_fst)
qed
sublocale sim_complete_bisim': Double_Simulation_Finite_Complete_Bisim_Cover_paired
"λ (l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩"
"λ (l, Z) (l', Z'). ∃ a. A,ℛ ⊢ ⟨l, Z⟩ ↝⇩a ⟨l', Z'⟩ ∧ Z' ≠ {}"
"λ (l, R). l ∈ state_set A ∧ R ∈ ℛ l"
"λ (l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩ ∧ Z' ≠ {}"
"λ (l, Z). l ∈ state_set A ∧ Z ∈ V' ∧ Z ≠ {}"
l⇩0 Z⇩0
proof (standard, goal_cases)
case (1 l x l' y S)
then show ?case
apply clarify
apply (drule step_r'_complete_spec, (auto intro: ℛ_V; fail))
by (auto simp: ℛ_def region_unique)
next
case (2 l S l' T)
then show ?case
by (auto simp add: step_r'_state_set step_r'_ℛ)
next
case prems: (3 l Z u)
then show ?case
using region_cover'[of u l] by (auto dest!: V'_V simp: V_def)+
qed
subsection ‹State Formulas›
context
fixes P :: "'s ⇒ bool"
begin
definition "φ = P o fst"
paragraph ‹State formulas are compatible with closures.›
paragraph ‹Runs satisfying a formula all the way long›
interpretation G⇩φ: Graph_Start_Defs
"λ (l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩ ∧ Z' ≠ {} ∧ P l'" "(l⇩0, Z⇩0)" .
theorem Alw_ev_mc1:
"(∀x⇩0∈a⇩0. sim.sim.Alw_ev (Not ∘ φ) x⇩0) ⟷ ¬ (P l⇩0 ∧ (∃a. G⇩φ.reachable a ∧ G⇩φ.reaches1 a a))"
using sim_complete_bisim'.Alw_ev_mc1
unfolding G⇩φ.reachable_def a⇩0_def sim_complete_bisim'.ψ_def φ_def
by auto
end
subsection ‹Leads-To Properties›
context
fixes P Q :: "'s ⇒ bool"
begin
definition "ψ = Q o fst"
interpretation G⇩ψ: Graph_Defs
"λ (l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩ ∧ Z' ≠ {} ∧ Q l'" .
theorem leadsto_mc1:
"(∀x⇩0∈a⇩0. sim.sim.leadsto (φ P) (Not ∘ ψ) x⇩0) ⟷
(∄x. reaches (l⇩0, Z⇩0) x ∧ P (fst x) ∧ Q (fst x) ∧ (∃a. G⇩ψ.reaches x a ∧ G⇩ψ.reaches1 a a))"
if "∀x⇩0∈a⇩0. ¬ sim.sim.deadlock x⇩0"
proof -
from that have *: "∀x⇩0∈Z⇩0. ¬ sim.sim.deadlock (l⇩0, x⇩0)"
unfolding a⇩0_def by auto
show ?thesis
using sim_complete_bisim'.leadsto_mc1[OF *, symmetric, of P Q]
unfolding ψ_def φ_def sim_complete_bisim'.φ'_def sim_complete_bisim'.ψ_def a⇩0_def
by (auto dest: from_R_D from_R_loc)
qed
end
lemma from_R_reaches:
assumes "sim.sim.Steps.reaches (from_R l⇩0 Z⇩0) b"
obtains l Z where "b = from_R l Z"
using assms by cases (fastforce simp: sim.A2'_def dest!: from_R_R_of)+
lemma ta_reaches_ex_iff:
assumes compatible:
"⋀l u u' R.
u ∈ R ⟹ u' ∈ R ⟹ R ∈ ℛ l ⟹ l ∈ state_set A ⟹ P (l, u) = P (l, u')"
shows
"(∃ x⇩0 ∈ a⇩0. ∃ l u. sim.sim.reaches x⇩0 (l, u) ∧ P (l, u)) ⟷
(∃ l Z. ∃ u ∈ Z. reaches (l⇩0, Z⇩0) (l, Z) ∧ P (l, u))"
proof -
have *: "(∃x⇩0 ∈ a⇩0. ∃ l u. sim.sim.reaches x⇩0 (l, u) ∧ P (l, u))
⟷ (∃y. ∃x⇩0∈from_R l⇩0 Z⇩0. sim.sim.reaches x⇩0 y ∧ P y)"
unfolding a⇩0_def by auto
show ?thesis
unfolding *
apply (subst sim_complete_bisim'.sim_reaches_equiv)
subgoal
by (simp add: start_state)
apply (subst sim_complete_bisim'.reaches_ex'[of P])
unfolding a⇩0_def
apply clarsimp
subgoal
unfolding sim.P1'_def by (clarsimp simp: fst_simp) (metis R_ofI compatible fst_conv)
apply safe
apply (rule from_R_reaches, assumption)
using from_R_fst by (force intro: from_R_val)+
qed
lemma ta_reaches_all_iff:
assumes compatible:
"⋀l u u' R.
u ∈ R ⟹ u' ∈ R ⟹ R ∈ ℛ l ⟹ l ∈ state_set A ⟹ P (l, u) = P (l, u')"
shows
"(∀ x⇩0 ∈ a⇩0. ∀ l u. sim.sim.reaches x⇩0 (l, u) ⟶ P (l, u)) ⟷
(∀ l Z. reaches (l⇩0, Z⇩0) (l, Z) ⟶ (∀ u ∈ Z. P (l, u)))"
proof -
have *: "(∀x⇩0 ∈ a⇩0. ∀ l u. sim.sim.reaches x⇩0 (l, u) ⟶ P (l, u))
⟷ (∀y. ∀x⇩0∈from_R l⇩0 Z⇩0. sim.sim.reaches x⇩0 y ⟶ P y)"
unfolding a⇩0_def by auto
show ?thesis
unfolding *
apply (subst sim_complete_bisim'.sim_reaches_equiv)
subgoal
by (simp add: start_state)
apply (subst sim_complete_bisim'.reaches_all''[of P])
unfolding a⇩0_def
apply clarsimp
subgoal
unfolding sim.P1'_def by (clarsimp simp: fst_simp) (metis R_ofI compatible fst_conv)
apply auto
apply (rule from_R_reaches, assumption)
using from_R_fst by (force intro: from_R_val)+
qed
end
end