Theory Timed_Automata.Closure
theory Closure
imports Regions
begin
section ‹Correct Approximation of Zones with ‹α›-regions›
lemma subset_int_mono: "A ⊆ B ⟹ A ∩ C ⊆ B ∩ C" by blast
lemma zone_set_mono:
"A ⊆ B ⟹ zone_set A r ⊆ zone_set B r"
unfolding zone_set_def by auto
lemma zone_delay_mono:
"A ⊆ B ⟹ A⇧↑ ⊆ B⇧↑"
unfolding zone_delay_def by auto
lemma step_z_mono:
"A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇘a⇙ ⟨l',W'⟩ ∧ Z' ⊆ W'"
proof (cases rule: step_z.cases, assumption, goal_cases)
case A: 1
let ?W' = "W⇧↑ ∩ {u. u ⊢ inv_of A l}"
from A have "A ⊢ ⟨l, W⟩ ↝⇘a⇙ ⟨l',?W'⟩" by auto
moreover have "Z' ⊆ ?W'"
apply (subst A(5))
apply (rule subset_int_mono)
by (auto intro!: zone_delay_mono A(2))
ultimately show ?thesis by meson
next
case A: (2 g a r)
let ?W' = "zone_set (W ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
from A have "A ⊢ ⟨l, W⟩ ↝⇘↿a⇙ ⟨l',?W'⟩" by auto
moreover have "Z' ⊆ ?W'"
apply (subst A(4))
apply (rule subset_int_mono)
apply (rule zone_set_mono)
apply (rule subset_int_mono)
apply (rule A(2))
done
ultimately show ?thesis by (auto simp: A(3))
qed
section ‹Old Variant Using a Global Set of Regions›
paragraph ‹Shared Definitions for Local and Global Sets of Regions›
locale Alpha_defs =
fixes X :: "'c set"
begin
definition V :: "('c, t) cval set" where "V ≡ {v . ∀ x ∈ X. v x ≥ 0}"
lemma up_V: "Z ⊆ V ⟹ Z⇧↑ ⊆ V"
unfolding V_def zone_delay_def cval_add_def by auto
lemma reset_V: "Z ⊆ V ⟹ (zone_set Z r) ⊆ V"
unfolding V_def unfolding zone_set_def by (induction r, auto)
lemma step_z_V: "A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V"
apply (induction rule: step_z.induct)
apply (rule le_infI1)
apply (rule up_V)
apply blast
apply (rule le_infI1)
apply (rule reset_V)
by blast
end
text ‹
This is the classic variant using a global clock ceiling ‹k› and thus a global set of regions.
It is also the version that is necessary to prove the classic extrapolation correct.
It is preserved here for comparison with P. Bouyer's proofs and to outline the only slight
adoptions that are necessary to obtain the new version.
›
locale AlphaClosure_global =
Alpha_defs X for X :: "'c set" +
fixes k ℛ
defines "ℛ ≡ {region X I r | I r. valid_region X k I r}"
assumes finite: "finite X"
begin
lemmas set_of_regions_spec = set_of_regions[OF _ _ _ finite, of _ k, folded ℛ_def]
lemmas region_cover_spec = region_cover[of X _ k, folded ℛ_def]
lemmas region_unique_spec = region_unique[of ℛ X k, folded ℛ_def, simplified]
lemmas regions_closed'_spec = regions_closed'[of ℛ X k, folded ℛ_def, simplified]
lemma valid_regions_distinct_spec:
"R ∈ ℛ ⟹ R' ∈ ℛ ⟹ v ∈ R ⟹ v ∈ R' ⟹ R = R'"
unfolding ℛ_def using valid_regions_distinct
by auto (drule valid_regions_distinct, assumption+, simp)+
definition cla (‹Closure⇩α _› [71] 71)
where
"cla Z = ⋃ {R ∈ ℛ. R ∩ Z ≠ {}}"
subsubsection ‹The Nice and Easy Properties Proved by Bouyer›
lemma closure_constraint_id:
"∀(x, m)∈collect_clock_pairs g. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ ⟹ Closure⇩α ⦃g⦄ = ⦃g⦄ ∩ V"
proof goal_cases
case 1
show ?case
proof auto
fix v assume v: "v ∈ Closure⇩α ⦃g⦄"
then obtain R where R: "v ∈ R" "R ∈ ℛ" "R ∩ ⦃g⦄ ≠ {}" unfolding cla_def by auto
with ccompatible[OF 1, folded ℛ_def] show "v ∈ ⦃g⦄" unfolding ccompatible_def by auto
from R show "v ∈ V" unfolding V_def ℛ_def by auto
next
fix v assume v: "v ∈ ⦃g⦄" "v ∈ V"
with region_cover[of X v k, folded ℛ_def] obtain R where "R ∈ ℛ" "v ∈ R" unfolding V_def by auto
then show "v ∈ Closure⇩α ⦃g⦄" unfolding cla_def using v by auto
qed
qed
lemma closure_id':
"Z ≠ {} ⟹ Z ⊆ R ⟹ R ∈ ℛ ⟹ Closure⇩α Z = R"
proof goal_cases
case 1
note A = this
then have "R ⊆ Closure⇩α Z" unfolding cla_def by auto
moreover
{ fix R' assume R': "Z ∩ R' ≠ {}" "R' ∈ ℛ" "R ≠ R'"
with A obtain v where "v ∈ R" "v ∈ R'" by auto
with ℛ_regions_distinct[OF _ A(3) this(1) R'(2-)] ℛ_def have False by auto
}
ultimately show ?thesis unfolding cla_def by auto
qed
lemma closure_id:
"Closure⇩α Z ≠ {} ⟹ Z ⊆ R ⟹ R ∈ ℛ ⟹ Closure⇩α Z = R"
proof goal_cases
case 1
then have "Z ≠ {}" unfolding cla_def by auto
with 1 closure_id' show ?case by blast
qed
lemma closure_update_mono:
"Z ⊆ V ⟹ set r ⊆ X ⟹ zone_set (Closure⇩α Z) r ⊆ Closure⇩α(zone_set Z r)"
proof -
assume A: "Z ⊆ V" "set r ⊆ X"
let ?U = "{R ∈ ℛ. Z ∩ R ≠ {}}"
from A(1) region_cover_spec have "∀ v ∈ Z. ∃ R. R ∈ ℛ ∧ v ∈ R" unfolding V_def by auto
then have "Z = ⋃ {Z ∩ R | R. R ∈ ?U}"
proof (auto, goal_cases)
case (1 v)
then obtain R where "R ∈ ℛ" "v ∈ R" by auto
moreover with 1 have "Z ∩ R ≠ {}" "v ∈ Z ∩ R" by auto
ultimately show ?case by auto
qed
then obtain U where U: "Z = ⋃ {Z ∩ R | R. R ∈ U}" "∀ R ∈ U. R ∈ ℛ" by blast
{ fix R assume R: "R ∈ U"
{ fix v' assume v': "v' ∈ zone_set (Closure⇩α (Z ∩ R)) r - Closure⇩α(zone_set (Z ∩ R) r)"
then obtain v where *:
"v ∈ Closure⇩α (Z ∩ R)" "v' = [r → 0]v"
unfolding zone_set_def by auto
with closure_id[of "Z ∩ R" R] R U(2) have **:
"Closure⇩α (Z ∩ R) = R" "Closure⇩α (Z ∩ R) ∈ ℛ"
by fastforce+
with region_set'_id[OF _ *(1) finite _ _ A(2), of k 0, folded ℛ_def, OF this(2)]
have ***: "zone_set R r ∈ ℛ" "[r→0]v ∈ zone_set R r"
unfolding zone_set_def region_set'_def by auto
from * have "Z ∩ R ≠ {}" unfolding cla_def by auto
then have "zone_set (Z ∩ R) r ≠ {}" unfolding zone_set_def by auto
from closure_id'[OF this _ ***(1)] have "Closure⇩α zone_set (Z ∩ R) r = zone_set R r"
unfolding zone_set_def by auto
with v' **(1) have False by auto
}
then have "zone_set (Closure⇩α (Z ∩ R)) r ⊆ Closure⇩α(zone_set (Z ∩ R) r)" by auto
} note Z_i = this
from U(1) have "Closure⇩α Z = ⋃ {Closure⇩α (Z ∩ R) | R. R ∈ U}" unfolding cla_def by auto
then have "zone_set (Closure⇩α Z) r = ⋃ {zone_set (Closure⇩α (Z ∩ R)) r | R. R ∈ U}"
unfolding zone_set_def by auto
also have "… ⊆ ⋃ {Closure⇩α(zone_set (Z ∩ R) r) | R. R ∈ U}" using Z_i by auto
also have "… = Closure⇩α ⋃ {(zone_set (Z ∩ R) r) | R. R ∈ U}" unfolding cla_def by auto
also have "… = Closure⇩α zone_set (⋃ {Z ∩ R| R. R ∈ U}) r"
proof goal_cases
case 1
have "zone_set (⋃ {Z ∩ R| R. R ∈ U}) r = ⋃ {(zone_set (Z ∩ R) r) | R. R ∈ U}"
unfolding zone_set_def by auto
then show ?case by auto
qed
finally show "zone_set (Closure⇩α Z) r ⊆ Closure⇩α(zone_set Z r)" using U by simp
qed
lemma SuccI3:
"R ∈ ℛ ⟹ v ∈ R ⟹ t ≥ 0 ⟹ (v ⊕ t) ∈ R' ⟹ R' ∈ ℛ ⟹ R' ∈ Succ ℛ R"
apply (intro SuccI2[of ℛ X k, folded ℛ_def, simplified])
apply assumption+
apply (intro region_unique[of ℛ X k, folded ℛ_def, simplified, symmetric])
by assumption+
lemma closure_delay_mono:
"Z ⊆ V ⟹ (Closure⇩α Z)⇧↑ ⊆ Closure⇩α (Z⇧↑)"
proof
fix v assume v: "v ∈ (Closure⇩α Z)⇧↑" and Z: "Z ⊆ V"
then obtain u u' t R where A:
"u ∈ Closure⇩α Z" "v = (u ⊕ t)" "u ∈ R" "u' ∈ R" "R ∈ ℛ" "u' ∈ Z" "t ≥ 0"
unfolding cla_def zone_delay_def by blast
from A(3,5) have "∀ x ∈ X. u x ≥ 0" unfolding ℛ_def by fastforce
with region_cover_spec[of v] A(2,7) obtain R' where R':
"R' ∈ ℛ" "v ∈ R'"
unfolding cval_add_def by auto
with set_of_regions_spec[OF A(5,4), OF SuccI3, of u] A obtain t where t:
"t ≥ 0" "[u' ⊕ t]⇩ℛ = R'"
by auto
with A have "(u' ⊕ t) ∈ Z⇧↑" unfolding zone_delay_def by auto
moreover from regions_closed'_spec[OF A(5,4)] t have "(u' ⊕ t) ∈ R'" by auto
ultimately have "R' ∩ (Z⇧↑) ≠ {}" by auto
with R' show "v ∈ Closure⇩α (Z⇧↑)" unfolding cla_def by auto
qed
lemma region_V: "R ∈ ℛ ⟹ R ⊆ V" using V_def ℛ_def region.cases by auto
lemma closure_V:
"Closure⇩α Z ⊆ V"
unfolding cla_def using region_V by auto
lemma closure_V_int:
"Closure⇩α Z = Closure⇩α (Z ∩ V)"
unfolding cla_def using region_V by auto
lemma closure_constraint_mono:
"Closure⇩α g = g ⟹ g ∩ (Closure⇩α Z) ⊆ Closure⇩α (g ∩ Z)"
unfolding cla_def by auto
lemma closure_constraint_mono':
assumes "Closure⇩α g = g ∩ V"
shows "g ∩ (Closure⇩α Z) ⊆ Closure⇩α (g ∩ Z)"
proof -
from assms closure_V_int have "Closure⇩α (g ∩ V) = g ∩ V" by auto
from closure_constraint_mono[OF this, of Z] have
"g ∩ (V ∩ Closure⇩α Z) ⊆ Closure⇩α (g ∩ Z ∩ V)"
by (metis Int_assoc Int_commute)
with closure_V[of Z] closure_V_int[of "g ∩ Z"] show ?thesis by auto
qed
lemma cla_empty_iff:
"Z ⊆ V ⟹ Z = {} ⟷ Closure⇩α Z = {}"
unfolding cla_def V_def using region_cover_spec by fast
lemma closure_involutive_aux:
"U ⊆ ℛ ⟹ Closure⇩α ⋃ U = ⋃ U"
unfolding cla_def using valid_regions_distinct_spec by blast
lemma closure_involutive_aux':
"∃ U. U ⊆ ℛ ∧ Closure⇩α Z = ⋃ U"
unfolding cla_def by (rule exI[where x = "{R ∈ ℛ. R ∩ Z ≠ {}}"]) auto
lemma closure_involutive:
"Closure⇩α Closure⇩α Z = Closure⇩α Z"
using closure_involutive_aux closure_involutive_aux' by metis
lemma closure_involutive':
"Z ⊆ Closure⇩α W ⟹ Closure⇩α Z ⊆ Closure⇩α W"
unfolding cla_def using valid_regions_distinct_spec by fast
lemma closure_subs:
"Z ⊆ V ⟹ Z ⊆ Closure⇩α Z"
unfolding cla_def V_def using region_cover_spec by fast
lemma cla_mono':
"Z' ⊆ V ⟹ Z ⊆ Z' ⟹ Closure⇩α Z ⊆ Closure⇩α Z'"
by (meson closure_involutive' closure_subs subset_trans)
lemma cla_mono:
"Z ⊆ Z' ⟹ Closure⇩α Z ⊆ Closure⇩α Z'"
using closure_V_int cla_mono'[of "Z' ∩ V" "Z ∩ V"] by auto
section ‹A Zone Semantics Abstracting with ‹Closure⇩α››
subsection ‹Single step›
inductive step_z_alpha ::
"('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 'a action ⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇘α(_)⇙ ⟨_, _⟩› [61,61,61] 61)
where
step_alpha: "A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l', Closure⇩α Z'⟩"
inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ ↝⇘α(a)⇙ ⟨l',u'⟩"
declare step_z_alpha.intros[intro]
definition
step_z_alpha' :: "('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇩α ⟨_, _⟩› [61,61,61] 61)
where
"A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Z''⟩ = (∃ Z' a. A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l, Z'⟩ ∧ A ⊢ ⟨l, Z'⟩ ↝⇘α(↿a)⇙ ⟨l', Z''⟩)"
text ‹Single-step soundness and completeness follows trivially from ‹cla_empty_iff›.›
lemma step_z_alpha_sound:
"A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z''⟩ ∧ Z'' ≠ {}"
by (induction rule: step_z_alpha.induct) (auto dest: cla_empty_iff step_z_V)
lemma step_z_alpha'_sound:
"A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z''⟩ ∧ Z'' ≠ {}"
oops
lemma step_z_alpha_complete':
"A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l',Z''⟩ ∧ Z' ⊆ Z''"
by (auto dest: closure_subs step_z_V)
lemma step_z_alpha_complete:
"A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l',Z''⟩ ∧ Z'' ≠ {}"
by (blast dest: step_z_alpha_complete')
lemma step_z_alpha'_complete':
"A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l',Z''⟩ ∧ Z' ⊆ Z''"
unfolding step_z_alpha'_def step_z'_def by (blast dest: step_z_alpha_complete' step_z_V)
lemma step_z_alpha'_complete:
"A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l',Z''⟩ ∧ Z'' ≠ {}"
by (blast dest: step_z_alpha'_complete')
subsection ‹Multi step›
abbreviation
steps_z_alpha :: "('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇩α* ⟨_, _⟩› [61,61,61] 61)
where
"A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l', Z''⟩ ≡ (λ (l, Z) (l', Z''). A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Z''⟩)⇧*⇧* (l, Z) (l', Z'')"
text ‹P. Bouyer's calculation for @{term "Post(Closure⇩α Z, e) ⊆ Closure⇩α(Post (Z, e))"}›
text ‹This is now obsolete as we argue solely with monotonicty of ‹steps_z› w.r.t ‹Closure⇩α››
lemma calc:
"valid_abstraction A X k ⟹ Z ⊆ V ⟹ A ⊢ ⟨l, Closure⇩α Z⟩ ↝⇘a⇙ ⟨l', Z'⟩
⟹ ∃Z''. A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l', Z''⟩ ∧ Z' ⊆ Z''"
proof (cases rule: step_z.cases, assumption, goal_cases)
case 1
note A = this
from A(1) have "∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
by (fastforce elim: valid_abstraction.cases)
then have "∀(x, m)∈collect_clock_pairs (inv_of A l). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
unfolding clkp_set_def collect_clki_def inv_of_def by auto
from closure_constraint_id[OF this] have *: "Closure⇩α ⦃inv_of A l⦄ = ⦃inv_of A l⦄ ∩ V" .
have "(Closure⇩α Z)⇧↑ ⊆ Closure⇩α (Z⇧↑)" using A(2) by (blast intro!: closure_delay_mono)
then have "Z' ⊆ Closure⇩α (Z⇧↑ ∩ {u. u ⊢ inv_of A l})"
using closure_constraint_mono'[OF *, of "Z⇧↑"] unfolding ccval_def by (auto simp: Int_commute A(6))
with A(4,3) show ?thesis by (auto elim!: step_z.cases)
next
case (2 g a r)
note A = this
from A(1) have *:
"∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
"collect_clkvt (trans_of A) ⊆ X"
"finite X"
by (auto elim: valid_abstraction.cases)
from *(1) A(5) have "∀(x, m)∈collect_clock_pairs (inv_of A l'). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
unfolding clkp_set_def collect_clki_def inv_of_def by fastforce
from closure_constraint_id[OF this] have **: "Closure⇩α ⦃inv_of A l'⦄ = ⦃inv_of A l'⦄ ∩ V" .
from *(1) A(6) have "∀(x, m)∈collect_clock_pairs g. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
unfolding clkp_set_def collect_clkt_def by fastforce
from closure_constraint_id[OF this] have ***: "Closure⇩α ⦃g⦄ = ⦃g⦄ ∩ V" .
from *(2) A(6) have ****: "set r ⊆ X" unfolding collect_clkvt_def by fastforce
from closure_constraint_mono'[OF ***, of Z] have
"(Closure⇩α Z) ∩ {u. u ⊢ g} ⊆ Closure⇩α (Z ∩ {u. u ⊢ g})" unfolding ccval_def
by (subst Int_commute) (subst (asm) (2) Int_commute, assumption)
moreover have "zone_set … r ⊆ Closure⇩α (zone_set (Z ∩ {u. u ⊢ g}) r)" using **** A(2)
by (intro closure_update_mono, auto)
ultimately have "Z' ⊆ Closure⇩α (zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'})"
using closure_constraint_mono'[OF **, of "zone_set (Z ∩ {u. u ⊢ g}) r"] unfolding ccval_def
apply (subst A(5))
apply (subst (asm) (5 7) Int_commute)
apply (rule subset_trans)
defer
apply assumption
apply (subst subset_int_mono)
defer
apply rule
apply (rule subset_trans)
defer
apply assumption
apply (rule zone_set_mono)
apply assumption
done
with A(6) show ?thesis by (auto simp: A(4))
qed
text ‹
Turning P. Bouyers argument for multiple steps into an inductive proof is not direct.
With this initial argument we can get to a point where the induction hypothesis is applicable.
This breaks the "information hiding" induced by the different variants of steps.
›
lemma steps_z_alpha_closure_involutive'_aux:
"A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩ ⟹ Closure⇩α Z ⊆ Closure⇩α W ⟹ valid_abstraction A X k ⟹ Z ⊆ V
⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇘a⇙ ⟨l',W'⟩ ∧ Closure⇩α Z' ⊆ Closure⇩α W'"
proof (induction rule: step_z.induct)
case A: (step_t_z A l Z)
let ?Z' = "Z⇧↑ ∩ {u. u ⊢ inv_of A l}"
let ?W' = "W⇧↑ ∩ {u. u ⊢ inv_of A l}"
from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp
have step_z: "A ⊢ ⟨l, W⟩ ↝⇘τ⇙ ⟨l,?W'⟩" by auto
moreover have "Closure⇩α ?Z' ⊆ Closure⇩α ?W'"
proof
fix v assume v: "v ∈ Closure⇩α ?Z'"
then obtain R' v' where 1: "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto
then obtain u d where
"u ∈ Z" and v': "v' = u ⊕ d" "u ⊕ d ⊢ inv_of A l" "0 ≤ d"
unfolding zone_delay_def by blast
with closure_subs[OF A(3)] A(1) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ"
unfolding cla_def by blast
then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce
from region_cover'[OF ℛ_def' this] have R: "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto
from SuccI2[OF ℛ_def' this(2,1) ‹0 ≤ d›, of "[v']⇩ℛ"] v'(1) have v'1:
"[v']⇩ℛ ∈ Succ ℛ ([u]⇩ℛ)" "[v']⇩ℛ ∈ ℛ"
by auto
from regions_closed'_spec[OF R(1,2) ‹0 ≤ d›] v'(1) have v'2: "v' ∈ [v']⇩ℛ" by simp
from A(2) have *:
"∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
"collect_clkvt (trans_of A) ⊆ X"
"finite X"
by (auto elim: valid_abstraction.cases)
from *(1) u'(2) have "∀(x, m)∈collect_clock_pairs (inv_of A l). m ≤ real (k 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 v'(1,2) have 3:
"[v']⇩ℛ ⊆ ⦃inv_of A l⦄"
unfolding ccompatible_def ccval_def by auto
with A v'1 R(1) ℛ_def' have "A,ℛ ⊢ ⟨l, ([u]⇩ℛ)⟩ ↝ ⟨l,([v']⇩ℛ)⟩" by auto
with valid_regions_distinct_spec[OF v'1(2) 1(1) v'2 1(3)] region_unique_spec[OF u'(2,4)]
have step_r: "A,ℛ ⊢ ⟨l, R⟩ ↝ ⟨l, R'⟩" and 2: "[v']⇩ℛ = R'" "[u]⇩ℛ = R" by auto
from set_of_regions_spec[OF u'(4,3)] v'1(1) 2 obtain t where t: "t ≥ 0" "[u' ⊕ t]⇩ℛ = R'" by auto
with regions_closed'_spec[OF u'(4,3) this(1)] step_t_r(1) have *: "u' ⊕ t ∈ R'" by auto
with t(1) 3 2 u'(1,3) have "A ⊢ ⟨l, u'⟩ → ⟨l, u' ⊕ t⟩" "u' ⊕ t ∈ ?W'"
unfolding zone_delay_def ccval_def by auto
with * 1(1) have "R' ⊆ Closure⇩α ?W'" unfolding cla_def by auto
with 1(2) show "v ∈ Closure⇩α ?W'" ..
qed
ultimately show ?case by auto
next
case A: (step_a_z A l g a r l' Z)
let ?Z' = "zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
let ?W' = "zone_set (W ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp
from A(1) have step_z: "A ⊢ ⟨l, W⟩ ↝⇘↿a⇙ ⟨l',?W'⟩" by auto
moreover have "Closure⇩α ?Z' ⊆ Closure⇩α ?W'"
proof
fix v assume v: "v ∈ Closure⇩α ?Z'"
then obtain R' v' where 1: "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto
then obtain u where
"u ∈ Z" and v': "v' = [r→0]u" "u ⊢ g" "v' ⊢ inv_of A l'"
unfolding zone_set_def by blast
let ?R'= "region_set' (([u]⇩ℛ) ∩ {u. u ⊢ g}) r 0 ∩ {u. u ⊢ inv_of A l'}"
from ‹u ∈ Z› closure_subs[OF A(4)] A(2) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ"
unfolding cla_def by blast
then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce
from region_cover'[OF ℛ_def' this] have R: "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto
from step_r_complete_aux[OF ℛ_def' A(3) this(2,1) A(1) v'(2)] v'
have *: "[u]⇩ℛ = ([u]⇩ℛ) ∩ {u. u ⊢ g}" "?R' = region_set' ([u]⇩ℛ) r 0" "?R' ∈ ℛ" by auto
from ℛ_def' A(3) have "collect_clkvt (trans_of A) ⊆ X" "finite X"
by (auto elim: valid_abstraction.cases)
with A(1) have r: "set r ⊆ X" unfolding collect_clkvt_def by fastforce
from * v'(1) R(2) have "v' ∈ ?R'" unfolding region_set'_def by auto
moreover have "A,ℛ ⊢ ⟨l,([u]⇩ℛ)⟩ ↝ ⟨l',?R'⟩" using R(1) ℛ_def' A(1,3) v'(2) by auto
thm valid_regions_distinct_spec
with valid_regions_distinct_spec[OF *(3) 1(1) ‹v' ∈ ?R'› 1(3)] region_unique_spec[OF u'(2,4)]
have 2: "?R' = R'" "[u]⇩ℛ = R" by auto
with * u' have *: "[r→0]u' ∈ ?R'" "u' ⊢ g" "[r→0]u' ⊢ inv_of A l'"
unfolding region_set'_def by auto
with A(1) have "A ⊢ ⟨l, u'⟩ → ⟨l',[r→0]u'⟩" apply (intro step.intros(1)) apply rule by auto
moreover from * u'(1) have "[r→0]u' ∈ ?W'" unfolding zone_set_def by auto
ultimately have "R' ⊆ Closure⇩α ?W'" using *(1) 1(1) 2(1) unfolding cla_def by auto
with 1(2) show "v ∈ Closure⇩α ?W'" ..
qed
ultimately show ?case by meson
qed
lemma steps_z_alpha_closure_involutive'_aux':
"A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩ ⟹ Closure⇩α Z ⊆ Closure⇩α W ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ W ⊆ Z
⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇘a⇙ ⟨l',W'⟩ ∧ Closure⇩α Z' ⊆ Closure⇩α W' ∧ W' ⊆ Z'"
proof (induction rule: step_z.induct)
case A: (step_t_z A l Z)
let ?Z' = "Z⇧↑ ∩ {u. u ⊢ inv_of A l}"
let ?W' = "W⇧↑ ∩ {u. u ⊢ inv_of A l}"
from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp
have step_z: "A ⊢ ⟨l, W⟩ ↝⇘τ⇙ ⟨l,?W'⟩" by auto
moreover have "Closure⇩α ?Z' ⊆ Closure⇩α ?W'"
proof
fix v assume v: "v ∈ Closure⇩α ?Z'"
then obtain R' v' where 1: "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto
then obtain u d where
"u ∈ Z" and v': "v' = u ⊕ d" "u ⊕ d ⊢ inv_of A l" "0 ≤ d"
unfolding zone_delay_def by blast
with closure_subs[OF A(3)] A(1) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ"
unfolding cla_def by blast
then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce
from region_cover'[OF ℛ_def' this] have R: "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto
from SuccI2[OF ℛ_def' this(2,1) ‹0 ≤ d›, of "[v']⇩ℛ"] v'(1) have v'1:
"[v']⇩ℛ ∈ Succ ℛ ([u]⇩ℛ)" "[v']⇩ℛ ∈ ℛ"
by auto
from regions_closed'_spec[OF R(1,2) ‹0 ≤ d›] v'(1) have v'2: "v' ∈ [v']⇩ℛ" by simp
from A(2) have *:
"∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
"collect_clkvt (trans_of A) ⊆ X"
"finite X"
by (auto elim: valid_abstraction.cases)
from *(1) u'(2) have "∀(x, m)∈collect_clock_pairs (inv_of A l). m ≤ real (k 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 v'(1,2) have 3:
"[v']⇩ℛ ⊆ ⦃inv_of A l⦄"
unfolding ccompatible_def ccval_def by auto
with A v'1 R(1) ℛ_def' have "A,ℛ ⊢ ⟨l, ([u]⇩ℛ)⟩ ↝ ⟨l,([v']⇩ℛ)⟩" by auto
with valid_regions_distinct_spec[OF v'1(2) 1(1) v'2 1(3)] region_unique_spec[OF u'(2,4)]
have step_r: "A,ℛ ⊢ ⟨l, R⟩ ↝ ⟨l, R'⟩" and 2: "[v']⇩ℛ = R'" "[u]⇩ℛ = R" by auto
from set_of_regions_spec[OF u'(4,3)] v'1(1) 2 obtain t where t: "t ≥ 0" "[u' ⊕ t]⇩ℛ = R'" by auto
with regions_closed'_spec[OF u'(4,3) this(1)] step_t_r(1) have *: "u' ⊕ t ∈ R'" by auto
with t(1) 3 2 u'(1,3) have "A ⊢ ⟨l, u'⟩ → ⟨l, u' ⊕ t⟩" "u' ⊕ t ∈ ?W'"
unfolding zone_delay_def ccval_def by auto
with * 1(1) have "R' ⊆ Closure⇩α ?W'" unfolding cla_def by auto
with 1(2) show "v ∈ Closure⇩α ?W'" ..
qed
moreover have "?W' ⊆ ?Z'" using ‹W ⊆ Z› unfolding zone_delay_def by auto
ultimately show ?case by auto
next
case A: (step_a_z A l g a r l' Z)
let ?Z' = "zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
let ?W' = "zone_set (W ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp
from A(1) have step_z: "A ⊢ ⟨l, W⟩ ↝⇘↿a⇙ ⟨l',?W'⟩" by auto
moreover have "Closure⇩α ?Z' ⊆ Closure⇩α ?W'"
proof
fix v assume v: "v ∈ Closure⇩α ?Z'"
then obtain R' v' where "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto
then obtain u where
"u ∈ Z" and v': "v' = [r→0]u" "u ⊢ g" "v' ⊢ inv_of A l'"
unfolding zone_set_def by blast
let ?R'= "region_set' (([u]⇩ℛ) ∩ {u. u ⊢ g}) r 0 ∩ {u. u ⊢ inv_of A l'}"
from ‹u ∈ Z› closure_subs[OF A(4)] A(2) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ"
unfolding cla_def by blast
then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce
from region_cover'[OF ℛ_def' this] have "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto
have *:
"[u]⇩ℛ = ([u]⇩ℛ) ∩ {u. u ⊢ g}"
"region_set' ([u]⇩ℛ) r 0 ⊆ [[r→0]u]⇩ℛ" "[[r→0]u]⇩ℛ ∈ ℛ"
"([[r→0]u]⇩ℛ) ∩ {u. u ⊢ inv_of A l'} = [[r→0]u]⇩ℛ"
proof -
from A(3) have "collect_clkvt (trans_of A) ⊆ X"
by (auto elim: valid_abstraction.cases)
with A(1) have "set r ⊆ X" "∀y. y ∉ set r ⟶ k y ≤ k y"
unfolding collect_clkvt_def by fastforce+
with
region_set_subs[of _ X k _ 0, where k' = k, folded ℛ_def, OF ‹[u]⇩ℛ ∈ ℛ› ‹u ∈ [u]⇩ℛ› finite]
show "region_set' ([u]⇩ℛ) r 0 ⊆ [[r→0]u]⇩ℛ" "[[r→0]u]⇩ℛ ∈ ℛ" by auto
from A(3) have *:
"∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
by (fastforce elim: valid_abstraction.cases)+
from * A(1) have ***: "∀(x, m)∈collect_clock_pairs g. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
unfolding clkp_set_def collect_clkt_def by fastforce
from ‹u ∈ [u]⇩ℛ› ‹[u]⇩ℛ ∈ ℛ› ccompatible[OF this, folded ℛ_def] ‹u ⊢ g› show
"[u]⇩ℛ = ([u]⇩ℛ) ∩ {u. u ⊢ g}"
unfolding ccompatible_def ccval_def by blast
have **: "[r→0]u ∈ [[r→0]u]⇩ℛ"
using ‹R' ∈ ℛ› ‹v' ∈ R'› region_unique_spec v'(1) by blast
from * have
"∀(x, m)∈collect_clock_pairs (inv_of A l'). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ"
unfolding inv_of_def clkp_set_def collect_clki_def by fastforce
from ** ‹[[r→0]u]⇩ℛ ∈ ℛ› ccompatible[OF this, folded ℛ_def] ‹v' ⊢ _› show
"([[r→0]u]⇩ℛ) ∩ {u. u ⊢ inv_of A l'} = [[r→0]u]⇩ℛ"
unfolding ccompatible_def ccval_def ‹v' = _› by blast
qed
from * ‹v' = _› ‹u ∈ [u]⇩ℛ› have "v' ∈ [[r→0]u]⇩ℛ" unfolding region_set'_def by auto
from valid_regions_distinct_spec[OF *(3) ‹R' ∈ ℛ› ‹v' ∈ [[r→0]u]⇩ℛ› ‹v' ∈ R'›]
have "[[r→0]u]⇩ℛ = R'" .
from region_unique_spec[OF u'(2,4)] have "[u]⇩ℛ = R" by auto
from ‹[u]⇩ℛ = R› *(1,2) *(4) ‹u' ∈ R› have
"[r→0]u' ∈ [[r→0]u]⇩ℛ" "u' ⊢ g" "[r→0]u' ⊢ inv_of A l'"
unfolding region_set'_def by auto
with u'(1) have "[r→0]u' ∈ ?W'" unfolding zone_set_def by auto
with ‹[r→0]u' ∈ [[r→0]u]⇩ℛ› ‹[[r→0]u]⇩ℛ ∈ ℛ› have "[[r→0]u]⇩ℛ ⊆ Closure⇩α ?W'"
unfolding cla_def by auto
with ‹v ∈ R'› show "v ∈ Closure⇩α ?W'" unfolding ‹_ = R'› ..
qed
moreover have "?W' ⊆ ?Z'" using ‹W ⊆ Z› unfolding zone_set_def by auto
ultimately show ?case by meson
qed
lemma steps_z_alpha_V: "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V"
by (induction rule: rtranclp_induct2)
(use closure_V in ‹auto dest: step_z_V simp: step_z_alpha'_def›)
lemma steps_z_alpha_closure_involutive':
"A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇘τ⇙ ⟨l', Z''⟩ ⟹ A ⊢ ⟨l', Z''⟩ ↝⇘↿a⇙ ⟨l'',Z'''⟩
⟹ valid_abstraction A X k ⟹ Z ⊆ V
⟹ ∃ W'''. A ⊢ ⟨l, Z⟩ ↝* ⟨l'',W'''⟩ ∧ Closure⇩α Z''' ⊆ Closure⇩α W''' ∧ W''' ⊆ Z'''"
proof (induction arbitrary: a Z'' Z''' l'' rule: rtranclp_induct2)
case refl then show ?case unfolding step_z'_def by blast
next
case A: (step l' Z' l''1 Z''1)
from A(2) obtain Z'1 𝒵 a' where Z''1:
"Z''1 = Closure⇩α 𝒵" "A ⊢ ⟨l', Z'⟩ ↝⇘τ⇙ ⟨l', Z'1⟩" "A ⊢ ⟨l', Z'1⟩ ↝⇘↿a'⇙ ⟨l''1,𝒵⟩"
unfolding step_z_alpha'_def by auto
from A(3)[OF this(2,3) A(6,7)] obtain W''' where W''':
"A ⊢ ⟨l, Z⟩ ↝* ⟨l''1,W'''⟩" "Closure⇩α 𝒵 ⊆ Closure⇩α W'''" "W''' ⊆ 𝒵"
by auto
have "Z'' ⊆ V"
by (metis A(4) Z''1(1) closure_V step_z_V)
have "𝒵 ⊆ V"
by (meson A Z''1 step_z_V steps_z_alpha_V)
from closure_subs[OF this] ‹W''' ⊆ 𝒵› have *: "W''' ⊆ Closure⇩α 𝒵" by auto
from A(4) ‹Z''1 = _› have "A ⊢ ⟨l''1, Closure⇩α 𝒵⟩ ↝⇘τ⇙ ⟨l''1, Z''⟩" by simp
from steps_z_alpha_closure_involutive'_aux'[OF this _ A(6) closure_V *] W'''(2) obtain W'
where ***: "A ⊢ ⟨l''1, W'''⟩ ↝⇘τ⇙ ⟨l''1, W'⟩" "Closure⇩α Z'' ⊆ Closure⇩α W'" "W' ⊆ Z''"
by atomize_elim (auto simp: closure_involutive)
text ‹This shows how we could easily add more steps before doing the final closure operation!›
from steps_z_alpha_closure_involutive'_aux'[OF A(5) this(2) A(6) ‹Z'' ⊆ V› this(3)] obtain W''
where
"A ⊢ ⟨l''1, W'⟩ ↝⇘↿a⇙ ⟨l'', W''⟩" "Closure⇩α Z''' ⊆ Closure⇩α W''" "W'' ⊆ Z'''"
by auto
with *** W''' show ?case
unfolding step_z'_def by (blast intro: rtranclp.rtrancl_into_rtrancl)
qed
lemma steps_z_alpha_closure_involutive:
"A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V
⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩ ∧ Closure⇩α Z' ⊆ Closure⇩α Z'' ∧ Z'' ⊆ Z'"
proof (induction rule: rtranclp_induct2)
case refl show ?case by blast
next
case 2: (step l' Z' l'' Z''')
then obtain Z'' a Z''1 where *:
"A ⊢ ⟨l', Z'⟩ ↝⇘τ⇙ ⟨l',Z''⟩" "A ⊢ ⟨l', Z''⟩ ↝⇘↿a⇙ ⟨l'',Z''1⟩" "Z''' = Closure⇩α Z''1"
unfolding step_z_alpha'_def by auto
from steps_z_alpha_closure_involutive'[OF 2(1) this(1,2) 2(4,5)] obtain W''' where W''':
"A ⊢ ⟨l, Z⟩ ↝* ⟨l'',W'''⟩" "Closure⇩α Z''1 ⊆ Closure⇩α W'''" "W''' ⊆ Z''1" by blast
have "W''' ⊆ Z'''"
unfolding *
by (rule order_trans[OF ‹W''' ⊆ Z''1›] closure_subs step_z_V steps_z_alpha_V * 2(1,5))+
with * closure_involutive W''' show ?case by auto
qed
lemma steps_z_V:
"A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V"
unfolding step_z'_def by (induction rule: rtranclp_induct2) (auto dest!: step_z_V)
lemma steps_z_alpha_sound:
"A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ Z' ≠ {}
⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩ ∧ Z'' ≠ {} ∧ Z'' ⊆ Z'"
proof goal_cases
case 1
from steps_z_alpha_closure_involutive[OF 1(1-3)] obtain Z'' where
"A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩" "Closure⇩α Z' ⊆ Closure⇩α Z''" "Z'' ⊆ Z'"
by blast
moreover with 1(4) cla_empty_iff[OF steps_z_alpha_V[OF 1(1)], OF 1(3)]
cla_empty_iff[OF steps_z_V, OF this(1) 1(3)] have "Z'' ≠ {}" by auto
ultimately show ?case by auto
qed
lemma step_z_alpha_mono:
"A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ W ⊆ V ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇘α(a)⇙ ⟨l',W'⟩ ∧ Z' ⊆ W'"
proof goal_cases
case 1
then obtain Z'' where *: "A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z''⟩" "Z' = Closure⇩α Z''" by auto
from step_z_mono[OF this(1) 1(2)] obtain W' where "A ⊢ ⟨l, W⟩ ↝⇘a⇙ ⟨l',W'⟩" "Z'' ⊆ W'" by auto
moreover with *(2) have "Z' ⊆ Closure⇩α W'" unfolding cla_def by auto
ultimately show ?case by blast
qed
end
section ‹New Variant›
subsubsection ‹New Definitions›
hide_const collect_clkt collect_clki clkp_set valid_abstraction
definition collect_clkt :: "('a, 'c, 't, 's) transition set ⇒ 's ⇒ ('c *'t) set"
where
"collect_clkt S l = ⋃ {collect_clock_pairs (fst (snd t)) | t . t ∈ S ∧ fst t = l}"
definition collect_clki :: "('c, 't, 's) invassn ⇒ 's ⇒ ('c *'t) set"
where
"collect_clki I s = collect_clock_pairs (I s)"
definition clkp_set :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c *'t) set"
where
"clkp_set A s = collect_clki (inv_of A) s ∪ collect_clkt (trans_of A) s"
lemma collect_clkt_alt_def:
"collect_clkt S l = ⋃ (collect_clock_pairs ` (fst o snd) ` {t. t ∈ S ∧ fst t = l})"
unfolding collect_clkt_def by fastforce
inductive valid_abstraction
where
"⟦∀ l. ∀(x,m) ∈ clkp_set A l. m ≤ k l x ∧ x ∈ X ∧ m ∈ ℕ; collect_clkvt (trans_of A) ⊆ X; finite X;
∀ l g a r l' c. A ⊢ l ⟶⇗g,a,r⇖ l' ∧ c ∉ set r ⟶ k l' c ≤ k l c
⟧
⟹ valid_abstraction A X k"
locale AlphaClosure =
Alpha_defs X for X :: "'c set" +
fixes k :: "'s ⇒ 'c ⇒ nat" and ℛ
defines "ℛ l ≡ {region X I r | I r. valid_region X (k l) I r}"
assumes finite: "finite X"
begin
section ‹A Semantics Based on Localized Regions›
subsection ‹Single step›
inductive step_r ::
"('a, 'c, t, 's) ta ⇒ _ ⇒ 's ⇒ ('c, t) zone ⇒ 'a action ⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_,_ ⊢ ⟨_, _⟩ ↝⇘_⇙ ⟨_, _⟩› [61,61,61,61,61] 61)
where
step_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_a_r:
"A,ℛ ⊢ ⟨l,R⟩ ↝⇘↿a⇙ ⟨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'"
inductive_cases[elim!]: "A,ℛ ⊢ ⟨l, u⟩ ↝⇘a⇙ ⟨l', u'⟩"
declare step_r.intros[intro]
inductive step_r' ::
"('a, 'c, t, 's) ta ⇒ _ ⇒ 's ⇒ ('c, t) zone ⇒ 'a ⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_,_ ⊢ ⟨_, _⟩ ↝⇩_ ⟨_, _⟩› [61,61,61,61,61] 61)
where
"A,ℛ ⊢ ⟨l,R⟩ ↝⇩a ⟨l',R''⟩" if "A,ℛ ⊢ ⟨l,R⟩ ↝⇘τ⇙ ⟨l,R'⟩" "A,ℛ ⊢ ⟨l,R'⟩ ↝⇘↿a⇙ ⟨l', R''⟩"
lemmas ℛ_def' = meta_eq_to_obj_eq[OF ℛ_def]
lemmas region_cover' = region_cover'[OF ℛ_def']
abbreviation part'' (‹[_]⇩_› [61,61] 61) where "part'' u l1 ≡ part u (ℛ l1)"
no_notation part (‹[_]⇩_› [61,61] 61)
lemma step_r_complete_aux:
fixes R u r A l' g
defines "R' ≡ [[r→0]u]⇩l'"
assumes "valid_abstraction A X (λ x. real o k x)"
and "u ∈ R"
and "R ∈ ℛ l"
and "A ⊢ l ⟶⇗g,a,r⇖ l'"
and "u ⊢ g"
and "[r→0]u ⊢ inv_of A l'"
shows "R = R ∩ {u. u ⊢ g} ∧ region_set' R r 0 ⊆ R' ∧ R' ∈ ℛ l' ∧ R' ⊆ ⦃inv_of A l'⦄"
proof -
note A = assms(2-)
from A(1) obtain a1 b1 where *:
"A = (a1, b1)"
"∀l. ∀x∈clkp_set (a1, b1) l. case x of (x, m) ⇒ m ≤ real (k l x) ∧ x ∈ X ∧ m ∈ ℕ"
"collect_clkvt (trans_of (a1, b1)) ⊆ X"
"finite X"
"∀l g a r l' c. (a1, b1) ⊢ l ⟶⇗g,a,r⇖ l' ∧ c ∉ set r ⟶ k l' c ≤ k l c"
by (clarsimp elim!: valid_abstraction.cases)
from A(4) *(1,3) have r: "set r ⊆ X" unfolding collect_clkvt_def by fastforce
from A(4) *(1,5) have ceiling_mono: "∀y. y ∉ set r ⟶ k l' y ≤ k l y" by auto
from A(4) *(1,2) 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 ccompatible[OF this, folded ℛ_def] A(2,3,5) have "R ⊆ ⦃g⦄"
unfolding ccompatible_def ccval_def by blast
then have R_id: "R ∩ {u. u ⊢ g} = R" unfolding ccval_def by auto
from
region_set_subs[OF A(3)[unfolded ℛ_def] A(2) ‹finite X› _ r ceiling_mono, of 0, folded ℛ_def]
have **:
"[[r→0]u]⇩l' ⊇ region_set' R r 0" "[[r→0]u]⇩l' ∈ ℛ l'" "[r→0]u ∈ [[r→0]u]⇩l'"
by auto
let ?R = "[[r→0]u]⇩l'"
from *(1,2) 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 ccompatible[OF this, folded ℛ_def] **(2-) A(6) have "?R ⊆ ⦃inv_of A l'⦄"
unfolding ccompatible_def ccval_def by blast
then have ***: "?R ∩ {u. u ⊢ inv_of A l'} = ?R" unfolding ccval_def by auto
with **(1,2) R_id ‹?R ⊆ _› show ?thesis by (auto simp: R'_def)
qed
lemma step_t_r_complete:
assumes
"A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩" "valid_abstraction A X (λ x. real o k x)" "∀ x ∈ X. u x ≥ 0"
shows "∃ R'. A,ℛ ⊢ ⟨l, ([u]⇩l)⟩ ↝⇘τ⇙ ⟨l',R'⟩ ∧ u' ∈ R' ∧ R' ∈ ℛ l'"
using assms(1) proof (cases)
case A: 1
hence u': "u' = (u ⊕ d)" "u ⊕ d ⊢ inv_of A l" "0 ≤ d" and "l = l'" by auto
from region_cover'[OF assms(3)] have R: "[u]⇩l ∈ ℛ l" "u ∈ [u]⇩l" by auto
from SuccI2[OF ℛ_def' this(2,1) ‹0 ≤ d›, of "[u']⇩l"] u'(1) have u'1:
"[u']⇩l ∈ Succ (ℛ l) ([u]⇩l)" "[u']⇩l ∈ ℛ l"
by auto
from regions_closed'[OF ℛ_def' R ‹0 ≤ d›] u'(1) have u'2: "u' ∈ [u']⇩l" by simp
from assms(2) obtain a1 b1 where
"A = (a1, b1)"
"∀l. ∀x∈clkp_set (a1, b1) l. case x of (x, m) ⇒ m ≤ real (k l x) ∧ x ∈ X ∧ m ∈ ℕ"
"collect_clkvt (trans_of (a1, b1)) ⊆ X"
"finite X"
"∀l g a r l' c. (a1, b1) ⊢ l ⟶⇗g,a,r⇖ l' ∧ c ∉ set r ⟶ k l' c ≤ k l c"
by (clarsimp elim!: valid_abstraction.cases)
note * = this
from *(1,2) u'(2) 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] u'1(2) u'2 u'(1,2) have "[u']⇩l ⊆ ⦃inv_of A l⦄"
unfolding ccompatible_def ccval_def by auto
with u'1 R(1) assms have "A,ℛ ⊢ ⟨l, ([u]⇩l)⟩ ↝⇘τ⇙ ⟨l,([u']⇩l)⟩" by auto
with u'1(2) u'2 ‹l = l'› show ?thesis by meson
qed
lemma step_a_r_complete:
assumes
"A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l',u'⟩" "valid_abstraction A X (λ x. real o k x)" "∀ x ∈ X. u x ≥ 0"
shows "∃ R'. A,ℛ ⊢ ⟨l, ([u]⇩l)⟩ ↝⇘↿a⇙ ⟨l',R'⟩ ∧ u' ∈ R' ∧ R' ∈ ℛ l'"
using assms(1) proof cases
case A: (1 g r)
then obtain g r where u': "u' = [r→0]u" "A ⊢ l ⟶⇗g,a,r⇖ l'" "u ⊢ g" "u' ⊢ inv_of A l'"
by auto
let ?R'= "[[r→0]u]⇩l'"
from region_cover'[OF assms(3)] have R: "[u]⇩l ∈ ℛ l" "u ∈ [u]⇩l" by auto
from step_r_complete_aux[OF assms(2) this(2,1) u'(2,3)] u' have *:
"[u]⇩l ⊆ ⦃g⦄" "?R' ⊇ region_set' ([u]⇩l) r 0" "?R' ∈ ℛ l'" "?R' ⊆ ⦃inv_of A l'⦄"
by (auto simp: ccval_def)
from assms(2,3) have "collect_clkvt (trans_of A) ⊆ X" "finite X"
by (auto elim: valid_abstraction.cases)
with u'(2) have r: "set r ⊆ X" unfolding collect_clkvt_def by fastforce
from * u'(1) R(2) have "u' ∈ ?R'" unfolding region_set'_def by auto
moreover have "A,ℛ ⊢ ⟨l,([u]⇩l)⟩ ↝⇘↿a⇙ ⟨l',?R'⟩" using R(1) u'(2) * assms(2,3) by (auto 4 3)
ultimately show ?thesis using *(3) by meson
qed
lemma step_r_complete:
assumes
"A ⊢ ⟨l, u⟩ → ⟨l',u'⟩" "valid_abstraction A X (λ x. real o k x)" "∀ x ∈ X. u x ≥ 0"
shows "∃ R' a. A,ℛ ⊢ ⟨l, ([u]⇩l)⟩ ↝⇘a⇙ ⟨l',R'⟩ ∧ u' ∈ R' ∧ R' ∈ ℛ l'"
using assms by cases (drule step_a_r_complete step_t_r_complete; auto)+
text ‹
Compare this to lemma ‹step_z_sound›. This version is weaker because for regions we may very well
arrive at a successor for which not every valuation can be reached by the predecessor.
This is the case for e.g. the region with only Greater (k x) bounds.
›
lemma step_t_r_sound:
assumes "A,ℛ ⊢ ⟨l, R⟩ ↝⇘τ⇙ ⟨l',R'⟩"
shows "∀ u ∈ R. ∃ u' ∈ R'. ∃ d ≥ 0. A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩"
using assms(1) proof cases
case A: step_t_r
show ?thesis
proof
fix u assume "u ∈ R"
from set_of_regions[OF A(3)[unfolded ℛ_def], folded ℛ_def, OF this A(4)] A(2)
obtain t where t: "t ≥ 0" "[u ⊕ t]⇩l = R'" by (auto elim: valid_abstraction.cases)
with regions_closed'[OF ℛ_def' A(3) ‹u ∈ R› this(1)] step_t_r(1) have "(u ⊕ t) ∈ R'" by auto
with t(1) A(5) have "A ⊢ ⟨l, u⟩ →⇗t⇖ ⟨l,(u ⊕ t)⟩" unfolding ccval_def by auto
with t ‹_ ∈ R'› ‹l' = l› show "∃u'∈R'. ∃ t ≥ 0. A ⊢ ⟨l, u⟩ →⇗t⇖ ⟨l',u'⟩" by meson
qed
qed
lemma step_a_r_sound:
assumes "A,ℛ ⊢ ⟨l, R⟩ ↝⇘↿a⇙ ⟨l',R'⟩"
shows "∀ u ∈ R. ∃ u' ∈ R'. A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l',u'⟩"
using assms proof cases
case A: (step_a_r g r)
show ?thesis
proof
fix u assume "u ∈ R"
from ‹u ∈ R› A(4-6) have "u ⊢ g" "[r→0]u ⊢ inv_of A l'" "[r→0]u ∈ R'"
unfolding region_set'_def ccval_def by auto
with A(2) have "A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l',[r→0]u⟩" by (blast intro: step_a.intros)
with ‹_ ∈ R'› show "∃u'∈R'. A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l',u'⟩" by meson
qed
qed
lemma step_r_sound:
assumes "A,ℛ ⊢ ⟨l, R⟩ ↝⇘a⇙ ⟨l',R'⟩"
shows "∀ u ∈ R. ∃ u' ∈ R'. A ⊢ ⟨l, u⟩ → ⟨l',u'⟩"
using assms
by (cases a; simp) (drule step_a_r_sound step_t_r_sound; fastforce)+
lemma step_r'_sound:
assumes "A,ℛ ⊢ ⟨l, R⟩ ↝⇩a ⟨l',R'⟩"
shows "∀ u ∈ R. ∃ u' ∈ R'. A ⊢' ⟨l, u⟩ → ⟨l',u'⟩"
using assms by cases (blast dest!: step_a_r_sound step_t_r_sound)
section ‹A New Zone Semantics Abstracting with ‹Closure⇩α⇩,⇩l››
definition cla (‹Closure⇩α⇩,⇩_(_)› [71,71] 71)
where
"cla l Z = ⋃ {R ∈ ℛ l. R ∩ Z ≠ {}}"
subsection ‹Single step›
inductive step_z_alpha ::
"('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 'a action ⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇘α(_)⇙ ⟨_, _⟩› [61,61,61] 61)
where
step_alpha: "A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l', Closure⇩α⇩,⇩l' Z'⟩"
inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ ↝⇘α(a)⇙ ⟨l',u'⟩"
declare step_z_alpha.intros[intro]
text ‹Single-step soundness and completeness follows trivially from ‹cla_empty_iff›.›
lemma step_z_alpha_sound:
"A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {}
⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z''⟩ ∧ Z'' ≠ {}"
apply (induction rule: step_z_alpha.induct)
apply (frule step_z_V)
apply assumption
apply (rotate_tac 3)
by (fastforce simp: cla_def)
context
fixes l l' :: 's
begin
interpretation alpha: AlphaClosure_global _ "k l'" "ℛ l'" by standard (rule finite)
lemma [simp]:
"alpha.cla = cla l'"
unfolding cla_def alpha.cla_def ..
lemma step_z_alpha_complete:
"A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {}
⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l',Z''⟩ ∧ Z'' ≠ {}"
apply (frule step_z_V)
apply assumption
apply (rotate_tac 3)
apply (drule alpha.cla_empty_iff)
by auto
end
subsection ‹Multi step›
definition
step_z_alpha' :: "('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇩α ⟨_, _⟩› [61,61,61] 61)
where
"A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Z''⟩ = (∃ Z' a. A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l, Z'⟩ ∧ A ⊢ ⟨l, Z'⟩ ↝⇘α(↿a)⇙ ⟨l', Z''⟩)"
abbreviation
steps_z_alpha :: "('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇩α* ⟨_, _⟩› [61,61,61] 61)
where
"A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l', Z''⟩ ≡ (λ (l, Z) (l', Z''). A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Z''⟩)⇧*⇧* (l, Z) (l', Z'')"
text ‹P. Bouyer's calculation for @{term "Post(Closure⇩α⇩,⇩l Z, e) ⊆ Closure⇩α⇩,⇩l(Post (Z, e))"}›
text ‹This is now obsolete as we argue solely with monotonicty of ‹steps_z› w.r.t ‹Closure⇩α⇩,⇩l››
text ‹
Turning P. Bouyers argument for multiple steps into an inductive proof is not direct.
With this initial argument we can get to a point where the induction hypothesis is applicable.
This breaks the "information hiding" induced by the different variants of steps.
›
context
fixes l l' :: 's
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 steps_z_alpha_closure_involutive'_aux':
"A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩ ⟹ Closure⇩α⇩,⇩l Z ⊆ Closure⇩α⇩,⇩l W ⟹ valid_abstraction A X k ⟹ Z ⊆ V
⟹ W ⊆ Z ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇘a⇙ ⟨l',W'⟩ ∧ Closure⇩α⇩,⇩l' Z' ⊆ Closure⇩α⇩,⇩l' W' ∧ W' ⊆ Z'"
proof (induction A ≡ A l ≡ l _ _ l' ≡ l' _rule: step_z.induct)
case A: (step_t_z Z)
let ?Z' = "Z⇧↑ ∩ {u. u ⊢ inv_of A l}"
let ?W' = "W⇧↑ ∩ {u. u ⊢ inv_of A l}"
have step_z: "A ⊢ ⟨l, W⟩ ↝⇘τ⇙ ⟨l,?W'⟩" by auto
moreover have "Closure⇩α⇩,⇩l ?Z' ⊆ Closure⇩α⇩,⇩l ?W'"
proof
fix v assume v: "v ∈ Closure⇩α⇩,⇩l ?Z'"
then obtain R' v' where 1: "R' ∈ ℛ l" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto
then obtain u d where
"u ∈ Z" and v': "v' = u ⊕ d" "u ⊕ d ⊢ inv_of A l" "0 ≤ d"
unfolding zone_delay_def by blast
with alpha.closure_subs[OF A(4)] A(2) obtain u' R where u':
"u' ∈ W" "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 R: "[u]⇩l ∈ ℛ l" "u ∈ [u]⇩l" by auto
from SuccI2[OF ℛ_def' this(2,1) ‹0 ≤ d›, of "[v']⇩l"] v'(1) have v'1:
"[v']⇩l ∈ Succ (ℛ l) ([u]⇩l)" "[v']⇩l ∈ ℛ l"
by auto
from alpha.regions_closed'_spec[OF R(1,2) ‹0 ≤ d›] v'(1) have v'2: "v' ∈ [v']⇩l" by simp
from A(3) 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 v'(1,2) have 3:
"[v']⇩l ⊆ ⦃inv_of A l⦄"
unfolding ccompatible_def ccval_def by auto
from
alpha.valid_regions_distinct_spec[OF v'1(2) 1(1) v'2 1(3)]
alpha.region_unique_spec[OF u'(2,4)]
have 2: "[v']⇩l = R'" "[u]⇩l = R" by auto
from alpha.set_of_regions_spec[OF u'(4,3)] v'1(1) 2 obtain t where t:
"t ≥ 0" "[u' ⊕ t]⇩l = R'" by auto
with alpha.regions_closed'_spec[OF u'(4,3) this(1)] step_t_r(1) have *: "u' ⊕ t ∈ R'" by auto
with t(1) 3 2 u'(1,3) have "A ⊢ ⟨l, u'⟩ → ⟨l, u' ⊕ t⟩" "u' ⊕ t ∈ ?W'"
unfolding zone_delay_def ccval_def by auto
with * 1(1) have "R' ⊆ Closure⇩α⇩,⇩l ?W'" unfolding cla_def by auto
with 1(2) show "v ∈ Closure⇩α⇩,⇩l ?W'" ..
qed
moreover have "?W' ⊆ ?Z'" using ‹W ⊆ Z› unfolding zone_delay_def by auto
ultimately show ?case unfolding ‹l = l'› by auto
next
case A: (step_a_z g a r Z)
let ?Z' = "zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
let ?W' = "zone_set (W ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
from A(1) have step_z: "A ⊢ ⟨l, W⟩ ↝⇘↿a⇙ ⟨l',?W'⟩" by auto
moreover have "Closure⇩α⇩,⇩l' ?Z' ⊆ Closure⇩α⇩,⇩l' ?W'"
proof
fix v assume v: "v ∈ Closure⇩α⇩,⇩l' ?Z'"
then obtain R' v' where "R' ∈ ℛ l'" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto
then obtain u where
"u ∈ Z" and v': "v' = [r→0]u" "u ⊢ g" "v' ⊢ inv_of A l'"
unfolding zone_set_def by blast
let ?R'= "region_set' (([u]⇩l) ∩ {u. u ⊢ g}) r 0 ∩ {u. u ⊢ inv_of A l'}"
from ‹u ∈ Z› alpha.closure_subs[OF A(4)] A(2) obtain u' R where u':
"u' ∈ W" "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 = ([u]⇩l) ∩ {u. u ⊢ g}"
"region_set' ([u]⇩l) r 0 ⊆ [[r→0]u]⇩l'" "[[r→0]u]⇩l' ∈ ℛ l'"
"([[r→0]u]⇩l') ∩ {u. u ⊢ inv_of A l'} = [[r→0]u]⇩l'"
proof -
from A(3) 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 A(3) 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 = ([u]⇩l) ∩ {u. u ⊢ 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') ∩ {u. u ⊢ inv_of A l'} = [[r→0]u]⇩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'(2,4)] have "[u]⇩l = R" by auto
from ‹[u]⇩l = R› *(1,2) *(4) ‹u' ∈ R› have
"[r→0]u' ∈ [[r→0]u]⇩l'" "u' ⊢ g" "[r→0]u' ⊢ inv_of A l'"
unfolding region_set'_def by auto
with u'(1) have "[r→0]u' ∈ ?W'" unfolding zone_set_def by auto
with ‹[r→0]u' ∈ [[r→0]u]⇩l'› ‹[[r→0]u]⇩l' ∈ ℛ l'› have "[[r→0]u]⇩l' ⊆ Closure⇩α⇩,⇩l' ?W'"
unfolding cla_def by auto
with ‹v ∈ R'› show "v ∈ Closure⇩α⇩,⇩l' ?W'" unfolding ‹_ = R'› ..
qed
moreover have "?W' ⊆ ?Z'" using ‹W ⊆ Z› unfolding zone_set_def by auto
ultimately show ?case by meson
qed
end
lemma step_z_alpha_mono:
"A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ W ⊆ V ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇘α(a)⇙ ⟨l',W'⟩ ∧ Z' ⊆ W'"
proof goal_cases
case 1
then obtain Z'' where *: "A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z''⟩" "Z' = Closure⇩α⇩,⇩l' Z''" by auto
from step_z_mono[OF this(1) 1(2)] obtain W' where "A ⊢ ⟨l, W⟩ ↝⇘a⇙ ⟨l',W'⟩" "Z'' ⊆ W'" by auto
moreover with *(2) have "Z' ⊆ Closure⇩α⇩,⇩l' W'" unfolding cla_def by auto
ultimately show ?case by blast
qed
end
end