# Theory Timed_Automata.Closure

```theory Closure
imports Regions
begin

section ‹Correct Approximation of Zones with ‹α›-regions›

locale AlphaClosure =
fixes X k ℛ and V :: "('c, t) cval set"
defines "ℛ ≡ {region X I r | I r. valid_region X k I r}"
defines "V ≡ {v . ∀ x ∈ X. v x ≥ 0}"
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'"
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 New Zone Semantics Abstracting with ‹Closure⇩α››

subsection ‹Single step›

inductive step_z_alpha ::
"('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝⇩α ⟨_, _⟩" [61,61,61] 61)
where
step_alpha: "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Closure⇩α Z'⟩"

inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ ↝⇩α ⟨l',u'⟩"

declare step_z_alpha.intros[intro]

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⟩ ↝ ⟨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

text ‹Single-step soundness and completeness follows trivially from ‹cla_empty_iff›.›

lemma step_z_alpha_sound:
"A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z''⟩ ∧ Z'' ≠ {}"
apply (induction rule: step_z_alpha.induct)
apply (frule step_z_V)
apply assumption
apply (rotate_tac 3)
apply (drule cla_empty_iff)
by auto

lemma step_z_alpha_complete:
"A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l',Z''⟩ ∧ Z'' ≠ {}"
apply (frule step_z_V)
apply assumption
apply (rotate_tac 3)
apply (drule cla_empty_iff)
by auto

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

subsection ‹Multi step›

inductive
steps_z_alpha :: "('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝⇩α* ⟨_, _⟩" [61,61,61] 61)
where
refl: "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l, Z⟩" |
step: "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇩α ⟨l'', Z''⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l'', Z''⟩"

declare steps_z_alpha.intros[intro]

lemma subset_int_mono: "A ⊆ B ⟹ A ∩ C ⊆ B ∩ C" by blast

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⟩ ↝ ⟨l', Z'⟩
⟹ ∃Z''. A ⊢ ⟨l, Z⟩ ↝⇩α ⟨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" .
from closure_constraint_mono'[OF *, of Z] have
"(Closure⇩α Z) ∩ {u. u ⊢ inv_of A l} ⊆ Closure⇩α (Z ∩ {u. u ⊢ inv_of A l})"
unfolding ccval_def by (subst Int_commute) (subst (asm) (2) Int_commute, assumption)
moreover have "…⇧↑ ⊆ Closure⇩α ((Z ∩ {u. u ⊢ inv_of A l})⇧↑)" using A(2) by (blast intro!: closure_delay_mono)
ultimately have "Z' ⊆ Closure⇩α ((Z ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {u. u ⊢ inv_of A l})"
using closure_constraint_mono'[OF *, of "(Z ∩ {u. u ⊢ inv_of A l})⇧↑"] 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_delay_mono)
apply assumption
done
with A(4,3) show ?thesis by auto
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(5) 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(5) 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(4))
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(5) show ?thesis by auto
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⟩ ↝ ⟨l',Z'⟩ ⟹ Closure⇩α Z ⊆ Closure⇩α W ⟹ valid_abstraction A X k ⟹ Z ⊆ V
⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝ ⟨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})⇧↑ ∩ {u. u ⊢ inv_of A l}"
let ?W' = "(W ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {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 ⊢ inv_of A l" "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) v'(4), of "[v']⇩ℛ"] v'(1) have v'1:
"[v']⇩ℛ ∈ Succ ℛ ([u]⇩ℛ)" "[v']⇩ℛ ∈ ℛ"
by auto
from regions_closed'_spec[OF R(1,2) v'(4)] 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,3) R have 3:
"[v']⇩ℛ ⊆ ⦃inv_of A l⦄" "([u]⇩ℛ) ⊆ ⦃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⟩ ↝ ⟨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⟩ ↝ ⟨l',Z'⟩ ⟹ Closure⇩α Z ⊆ Closure⇩α W ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ W ⊆ Z
⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝ ⟨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})⇧↑ ∩ {u. u ⊢ inv_of A l}"
let ?W' = "(W ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {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 ⊢ inv_of A l" "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) v'(4), of "[v']⇩ℛ"] v'(1) have v'1:
"[v']⇩ℛ ∈ Succ ℛ ([u]⇩ℛ)" "[v']⇩ℛ ∈ ℛ"
by auto
from regions_closed'_spec[OF R(1,2) v'(4)] 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,3) R have 3:
"[v']⇩ℛ ⊆ ⦃inv_of A l⦄" "([u]⇩ℛ) ⊆ ⦃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⟩ ↝ ⟨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
moreover have "?W' ⊆ ?Z'" using ‹W ⊆ Z› unfolding zone_set_def by auto
ultimately show ?case by meson
qed

lemma steps_z_alt:
"A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',Z''⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z''⟩"
by (induction rule: steps_z.induct) auto

lemma steps_z_alpha_V: "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V"
apply (induction rule: steps_z_alpha.induct) using closure_V by auto

lemma steps_z_alpha_closure_involutive':
"A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ 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 A l Z l' Z' arbitrary: Z'' l'' rule: steps_z_alpha.induct, goal_cases)
case refl from this(1) show ?case by blast
next
case A: (2 A l Z l' Z' l'' Z'' Z''a l''a)
from A(3) obtain 𝒵 where Z'': "Z'' = Closure⇩α 𝒵" "A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',𝒵⟩" by auto
from A(2)[OF Z''(2) A(5,6)] obtain Z''' where Z''':
"A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩" "Closure⇩α 𝒵 ⊆ Closure⇩α Z'''" "Z''' ⊆ 𝒵"
by auto
from closure_subs have *:
"Z''' ⊆ Closure⇩α 𝒵"
by (metis A(1,6) Z'''(3) Z''(2) step_z_V steps_z_alpha_V subset_trans)
from A(4) Z'' have "A ⊢ ⟨l'', Closure⇩α 𝒵⟩ ↝ ⟨l''a,Z''a⟩" by auto
from steps_z_alpha_closure_involutive'_aux'[OF this(1) _ A(5) closure_V *] Z'''(2,3) obtain W'
where ***: "A ⊢ ⟨l'', Z'''⟩ ↝ ⟨l''a,W'⟩" "Closure⇩α Z''a ⊆ Closure⇩α W'" "W' ⊆ Z''a"
by (auto simp: closure_involutive)
with Z'''(1) have "A ⊢ ⟨l, Z⟩ ↝* ⟨l''a,W'⟩" by (blast intro: steps_z_alt)
with ***(2,3) show ?case by blast
qed

text ‹Old proof using Bouyer's calculation›
lemma steps_z_alpha_closure_involutive'':
"A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',Z''⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V
⟹ ∃ Z'''. A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩ ∧ Closure⇩α Z'' ⊆ Closure⇩α Z'''"
proof (induction A l Z l' Z' arbitrary: Z'' l'' rule: steps_z_alpha.induct, goal_cases)
case refl from this(1) show ?case by blast
next
case A: (2 A l Z l' Z' l'' Z'' Z''a l''a)
from A(3) obtain 𝒵 where Z'': "Z'' = Closure⇩α 𝒵" "A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',𝒵⟩" by auto
from A(2)[OF Z''(2) A(5,6)] obtain Z''' where Z''':
"A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩" "Closure⇩α 𝒵 ⊆ Closure⇩α Z'''"
by auto
from steps_z_alpha_V[OF A(1,6)] step_z_V[OF Z''(2)] have *: "𝒵 ⊆ V" by blast
from A Z'' have "A ⊢ ⟨l'', Closure⇩α 𝒵⟩ ↝ ⟨l''a,Z''a⟩" by auto
from calc[OF A(5) * this] obtain 𝒵' where **:
"A ⊢ ⟨l'', 𝒵⟩ ↝ ⟨l''a,𝒵'⟩" "Z''a ⊆ Closure⇩α 𝒵'"
by auto
from steps_z_alpha_closure_involutive'_aux[OF this(1) Z'''(2) A(5) *] obtain W' where ***:
"A ⊢ ⟨l'', Z'''⟩ ↝ ⟨l''a,W'⟩" "Closure⇩α 𝒵' ⊆ Closure⇩α W'"
by auto
with Z'''(1) have "A ⊢ ⟨l, Z⟩ ↝* ⟨l''a,W'⟩" by (blast intro: steps_z_alt)
with closure_involutive'[OF **(2)] ***(2) show ?case by blast
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 A l Z l' Z' rule: steps_z_alpha.induct)
case refl show ?case by blast
next
case 2: (step A l Z l' Z' l'' Z'')
then obtain Z''a where *: "A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',Z''a⟩" "Z'' = Closure⇩α Z''a" by auto
from steps_z_alpha_closure_involutive'[OF 2(1) this(1) 2(4,5)] obtain Z''' where Z''':
"A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩" "Closure⇩α Z''a ⊆ Closure⇩α Z'''" "Z''' ⊆ Z''a" by blast
have "Z''' ⊆ Z''" by (metis *(1,2) 2(1,5) Z'''(3) closure_subs step_z_V steps_z_alpha_V subset_trans)
with * closure_involutive Z''' show ?case by auto
qed

lemma steps_z_V:
"A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V"
apply (induction rule: steps_z.induct)
apply blast
using step_z_V by metis

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
Z'': "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩" "Closure⇩α Z' ⊆ Closure⇩α Z''" "Z'' ⊆ Z'"
by blast
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
with Z'' show ?case by auto
qed

lemma step_z_mono:
"A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝ ⟨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})⇧↑ ∩ {u. u ⊢ inv_of A l}"
from A have "A ⊢ ⟨l, W⟩ ↝ ⟨l',?W'⟩" by auto
moreover have "Z' ⊆ ?W'"
apply (subst A(4))
apply (rule subset_int_mono)
apply (rule zone_delay_mono)
apply (rule subset_int_mono)
apply (rule A(2))
done
ultimately show ?thesis by auto
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⟩ ↝ ⟨l',?W'⟩" by auto
moreover have "Z' ⊆ ?W'"
apply (subst A(3))
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
qed

lemma step_z_alpha_mono:
"A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ W ⊆ V ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇩α ⟨l',W'⟩ ∧ Z' ⊆ W'"
proof goal_cases
case 1
then obtain Z'' where *: "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z''⟩" "Z' = Closure⇩α Z''" by auto
from step_z_mono[OF this(1) 1(2)] obtain W' where "A ⊢ ⟨l, W⟩ ↝ ⟨l',W'⟩" "Z'' ⊆ W'" by auto
moreover with *(2) have "Z' ⊆ Closure⇩α W'" unfolding cla_def by auto
ultimately show ?case by blast
qed

lemma steps_z_alpha_mono:
"A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ W ⊆ V ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇩α* ⟨l',W'⟩ ∧ Z' ⊆ W'"
proof (induction rule: steps_z_alpha.induct, goal_cases)
case refl then show ?case by auto
next
case (2 A l Z l' Z' l'' Z'')
then obtain W' where "A ⊢ ⟨l, W⟩ ↝⇩α* ⟨l',W'⟩" "Z' ⊆ W'" by auto
with step_z_alpha_mono[OF 2(3) this(2) steps_z_alpha_V[OF this(1) 2(5)]]
show ?case by blast
qed

lemma steps_z_alpha_alt:
"A ⊢ ⟨l, Z⟩ ↝⇩α ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇩α* ⟨l'', Z''⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l'', Z''⟩"
by (rotate_tac, induction rule: steps_z_alpha.induct) blast+

lemma steps_z_alpha_complete:
"A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ Z' ≠ {}
⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z''⟩ ∧ Z' ⊆ Z''"
proof (induction rule: steps_z.induct, goal_cases)
case refl with cla_empty_iff show ?case by blast
next
case (2 A l Z l' Z' l'' Z'')
with step_z_V[OF this(1,5)] obtain Z''' where "A ⊢ ⟨l', Z'⟩ ↝⇩α* ⟨l'',Z'''⟩" "Z'' ⊆ Z'''" by blast
with steps_z_alpha_mono[OF this(1) closure_subs[OF step_z_V[OF 2(1,5)]] closure_V]
obtain W' where W': "A ⊢ ⟨l', Closure⇩α Z'⟩ ↝⇩α* ⟨l'',W'⟩" " Z'' ⊆ W'" by auto
with 2(1) have "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l'',W'⟩" by (auto intro: steps_z_alpha_alt)
with W' show ?case by auto
qed

lemma steps_z_alpha_complete':
"A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ Z' ≠ {}
⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z''⟩ ∧ Z'' ≠ {}"
using steps_z_alpha_complete by fast

end

end
```