Theory Closure

theory Closure
  imports Regions
begin

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

(* XXX Move *)
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)
  (* case A: (2 A l Z l' Z' Z'' a l'' Z''' aa Z''a Z'''a l''a) *)
  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

(*
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 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

(*
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 "A ⊢ ⟨l', Closure⇩α Z'⟩ ↝⇩α* ⟨l'',W'⟩" " Z'' ⊆ W'" by auto
  moreover with 2(1) have "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l'',W'⟩" by (auto intro: steps_z_alpha_alt)
  ultimately 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

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 (* End of context for global closure proofs *)

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

(*
lemma steps_z_alpha_V: "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V"
  thm alpha'.closure_V
  apply (induction rule: rtranclp_induct2)
  apply
     (use alpha'.closure_V[simplified] in ‹auto dest: step_z_V simp: step_z_alpha'_def›)
*)

end (* End of context for special region notation and fixed locations *)

(*
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⇩α⇩,⇩l'' Z''' ⊆ Closure⇩α⇩,⇩l'' W''' ∧ W''' ⊆ Z'''"
proof (induction A l Z l' Z' arbitrary: a Z'' Z''' l'' rule: steps_z_alpha.induct, goal_cases)
  case refl then show ?case by blas
next
  case A: (2 A l Z l' Z' Z'' a l'' Z''' aa Z''a Z'''a l''')
  interpret alpha'': AlphaClosure_global _ "k l''" "ℛ l''" by standard (rule finite)
  have [simp]: ‹alpha''.cla = cla l''› unfolding alpha''.cla_def cla_def ..
  note closure_V = alpha''.closure_V[simplified]
  from A(4) obtain 𝒵 where Z''': "Z''' = Closure⇩α⇩,⇩l'' 𝒵" "A ⊢ ⟨l', Z''⟩ ↝⇘↿a⇙ ⟨l'', 𝒵⟩" by auto
  from A(2)[OF A(3) this(2) A(7,8)] A(4) obtain W''' where W''':
    "A ⊢ ⟨l, Z⟩ ↝* ⟨l'',W'''⟩" "Closure⇩α⇩,⇩l'' 𝒵 ⊆ Closure⇩α⇩,⇩l'' W'''" "W''' ⊆ 𝒵"
    by auto
  have "Z''a ⊆ V" by (metis A(5) Z'''(1) closure_V step_z_V)
  have "𝒵 ⊆ V" by (meson A(1) A(3) A(8) Z'''(2) step_z_V steps_z_alpha_V)
  from alpha''.closure_subs[OF this] ‹W''' ⊆ 𝒵› have *: "W''' ⊆ Closure⇩α⇩,⇩l'' 𝒵" by auto
  from A(5) ‹Z''' = _› have "A ⊢ ⟨l'', Closure⇩α⇩,⇩l'' 𝒵⟩ ↝⇘τ⇙ ⟨l'', Z''a⟩" by simp
  from steps_z_alpha_closure_involutive'_aux'[OF this _ A(7) closure_V *] W'''(2) obtain W'
    where ***: "A ⊢ ⟨l'', W'''⟩ ↝⇘τ⇙ ⟨l'', W'⟩" "Closure⇩α⇩,⇩l'' Z''a ⊆ Closure⇩α⇩,⇩l'' W'" "W' ⊆ Z''a"
    by atomize_elim (auto simp: alpha''.closure_involutive[simplified])
  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(6) this(2) A(7) ‹Z''a ⊆ V› this(3)] obtain W''
    where
      "A ⊢ ⟨l'', W'⟩ ↝⇘↿aa⇙ ⟨l''', W''⟩" "Closure⇩α⇩,⇩l''' Z'''a ⊆ Closure⇩α⇩,⇩l''' W''" "W'' ⊆ Z'''a"
    by auto
  with *** W''' show ?case by (blast intro: steps_z_alt)
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⇩α⇩,⇩l' Z' ⊆ Closure⇩α⇩,⇩l' 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' Z'' a l'' Z''')
  interpret alpha'': AlphaClosure_global _ "k l''" "ℛ l''" by standard (rule finite)
  have [simp]: ‹alpha''.cla = cla l''› unfolding alpha''.cla_def cla_def ..
  from 2 obtain Z''a where *: "A ⊢ ⟨l', Z''⟩ ↝⇘↿a⇙ ⟨l'',Z''a⟩" "Z''' = Closure⇩α⇩,⇩l'' Z''a" by auto
  from steps_z_alpha_closure_involutive'[OF 2(1,2) this(1) 2(5,6)] obtain W''' where W''':
    "A ⊢ ⟨l, Z⟩ ↝* ⟨l'',W'''⟩" "Closure⇩α⇩,⇩l'' Z''a ⊆ Closure⇩α⇩,⇩l'' W'''" "W''' ⊆ Z''a" by blast
  have "W''' ⊆ Z'''"
    by (metis
        * 2(1,2,6) W'''(3) alpha''.closure_subs[simplified] order_trans step_z_V steps_z_alpha_V
        )
  with * alpha''.closure_involutive W''' show ?case by auto
qed

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
  interpret alpha': AlphaClosure_global _ "k l'" "ℛ l'" by standard (rule finite)
  have [simp]: ‹alpha'.cla = cla l'› unfolding alpha'.cla_def cla_def ..
  from steps_z_alpha_closure_involutive[OF 1(1-3)] obtain Z'' where
    "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩" "Closure⇩α⇩,⇩l' Z' ⊆ Closure⇩α⇩,⇩l' Z''" "Z'' ⊆ Z'"
  by blast
  moreover with
    1(4) alpha'.cla_empty_iff[OF steps_z_alpha_V[OF 1(1)], OF 1(3)]
    alpha'.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⇩α⇩,⇩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

(*
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 "A ⊢ ⟨l', Closure⇩α⇩,⇩l Z'⟩ ↝⇩α* ⟨l'',W'⟩" " Z'' ⊆ W'" by auto
  moreover with 2(1) have "A ⊢ ⟨l, Z⟩ ↝⇩α* ⟨l'',W'⟩" by (auto intro: steps_z_alpha_alt)
  ultimately 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