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  " "[r0]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 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 "xX. 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' = [r0]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 "xX. 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 *: "[r0]u'  ?R'" "u'  g" "[r0]u'  inv_of A l'"
    unfolding region_set'_def by auto
    with A(1) have "A  l, u'  l',[r0]u'" apply (intro step.intros(1)) apply rule by auto
    moreover from * u'(1) have "[r0]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 "xX. 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' = [r0]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 "xX. 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 *: "[r0]u'  ?R'" "u'  g" "[r0]u'  inv_of A l'"
    unfolding region_set'_def by auto
    with A(1) have "A  l, u'  l',[r0]u'" apply (intro step.intros(1)) apply rule by auto
    moreover from * u'(1) have "[r0]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