Theory DBM_Zone_Semantics

section ‹Semantics Based on DBMs›

theory DBM_Zone_Semantics
imports TA_DBM_Operations
begin

no_notation infinity (‹∞›)
hide_const (open) D

subsection ‹Single Step›

inductive step_z_dbm ::
  "('a, 'c, 't, 's) ta ⇒ 's ⇒ 't :: {linordered_cancel_ab_monoid_add,uminus} DBM
    ⇒ ('c ⇒ nat) ⇒ nat ⇒ 'a action ⇒ 's ⇒ 't DBM ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇘_,_,_⇙ ⟨_, _⟩› [61,61,61,61] 61)
where
  step_t_z_dbm:
    "D_inv = abstr (inv_of A l) (λi j. ∞) v ⟹ A ⊢ ⟨l,D⟩ ↝⇘v,n,τ⇙ ⟨l,And (up D) D_inv⟩" |
  step_a_z_dbm:
    "A ⊢ l ⟶⇗g,a,r⇖ l'
    ⟹ A ⊢ ⟨l,D⟩ ↝⇘v,n,↿a⇙ ⟨l',And (reset' (And D (abstr g (λi j. ∞) v)) n r v 0)
                                             (abstr (inv_of A l') (λi j. ∞) v)⟩"
inductive_cases step_z_t_cases: "A ⊢ ⟨l, D⟩ ↝⇘v,n,τ⇙ ⟨l', D'⟩"
inductive_cases step_z_a_cases: "A ⊢ ⟨l, D⟩ ↝⇘v,n,↿a⇙ ⟨l', D'⟩"
lemmas step_z_cases = step_z_a_cases step_z_t_cases

declare step_z_dbm.intros[intro]

lemma step_z_dbm_preserves_int_all:
  fixes D D' :: "('t :: {time, ring_1} DBM)"
  assumes "A ⊢ ⟨l,D⟩ ↝⇘v,n,a⇙ ⟨l',D'⟩" "global_clock_numbering A v n" "∀ (x, m) ∈ clkp_set A. m ∈ ℕ"
          "dbm_int_all D"
  shows "dbm_int_all D'"
using assms
proof (cases, goal_cases)
  case (1 D'')
  hence "∀c∈clk_set A. v c ≤ n" by blast+
  from dbm_int_all_inv_abstr[OF 1(2)] 1 have D''_int: "dbm_int_all D''" by simp
  show ?thesis unfolding 1(6)
    by (intro And_int_all_preservation up_int_all_preservation dbm_int_inv_abstr D''_int 1)
next
  case (2 g a r)
  hence assms: "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n"
    by blast+
  from dbm_int_all_inv_abstr[OF 2(2)] have D'_int:
    "dbm_int_all (abstr (inv_of A l') (λi j. ∞) v)"
  by simp
  from dbm_int_all_guard_abstr 2 have D''_int: "dbm_int_all (abstr g (λi j. ∞) v)" by simp
  have "set r ⊆ clk_set A" using 2(6) unfolding trans_of_def collect_clkvt_def by fastforce
  hence *:"∀c∈set r. v c ≤ n" using assms(2) by fastforce
  show ?thesis unfolding 2(5)
  by (intro And_int_all_preservation DBM_reset'_int_all_preservation dbm_int_all_inv_abstr 2 D''_int)
     (simp_all add: assms(1) *)
qed

lemma step_z_dbm_preserves_int:
  fixes D D' :: "('t :: {time, ring_1} DBM)"
  assumes "A ⊢ ⟨l,D⟩ ↝⇘v,n,a⇙ ⟨l',D'⟩" "global_clock_numbering A v n" "∀ (x, m) ∈ clkp_set A. m ∈ ℕ"
          "dbm_int D n"
  shows "dbm_int D' n"
using assms
proof (cases, goal_cases)
  case (1 D'')
  from dbm_int_inv_abstr[OF 1(2)] 1 have D''_int: "dbm_int D'' n" by simp
  show ?thesis unfolding 1(6)
    by (intro And_int_preservation up_int_preservation dbm_int_inv_abstr D''_int 1)
next
  case (2 g a r)
  hence assms: "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n"
    by blast+
  from dbm_int_inv_abstr[OF 2(2)] have D'_int: "dbm_int (abstr (inv_of A l') (λi j. ∞) v) n"
    by simp
  from dbm_int_guard_abstr 2 have D''_int: "dbm_int (abstr g (λi j. ∞) v) n" by simp
  have "set r ⊆ clk_set A" using 2(6) unfolding trans_of_def collect_clkvt_def by fastforce
  hence *:"∀c∈set r. v c ≤ n" using assms(2) by fastforce
  show ?thesis unfolding 2(5)
  by (intro And_int_preservation DBM_reset'_int_preservation dbm_int_inv_abstr 2 D''_int)
     (simp_all add: assms(1) 2(2) *)
qed

lemma up_correct:
  assumes "clock_numbering' v n"
  shows "[up M]⇘v,n⇙ = [M]⇘v,n⇙⇧↑"
using assms
 apply safe
  apply (rule DBM_up_sound')
   apply assumption+
 apply (rule DBM_up_complete')
  apply auto
done

lemma step_z_dbm_sound:
  assumes "A ⊢ ⟨l, D⟩ ↝⇘v,n,a⇙ ⟨l', D'⟩" "global_clock_numbering A v n"
  shows "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇘a⇙ ⟨l', [D']⇘v,n⇙⟩"
using assms
proof (cases, goal_cases)
  case (1 D'')
  hence "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n" by blast+
  note assms = assms(1) this
  from assms(3) have *: "∀c∈collect_clks (inv_of A l). v c ≤ n"
  unfolding clkp_set_def collect_clki_def inv_of_def by (fastforce simp: collect_clks_id)
  from 1 have D'':"[D'']⇘v,n⇙ = {u. u ⊢ inv_of A l}" using dbm_abstr_zone_eq[OF assms(2) *] by metis
  with And_correct have A11: "[And D D'']⇘v,n⇙ = ([D]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l})" by blast
  from D'' have
    "[D']⇘v,n⇙ = ([up D]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l})"
    unfolding 1(4) And_correct[symmetric] by simp
  with up_correct[OF assms(2)] A11 have "[D']⇘v,n⇙ = ([D]⇘v,n⇙)⇧↑ ∩ {u. u ⊢ inv_of A l}" by metis
  then show ?thesis by (auto simp: 1(2,3))
next
  case (2 g a r)
  hence "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n" "∀k≤n. k > 0 ⟶ (∃c. v c = k)" by blast+
  note assms = assms(1) this
  from assms(3) have *: "∀c∈collect_clks (inv_of A l'). v c ≤ n"
  unfolding clkp_set_def collect_clki_def inv_of_def by (fastforce simp: collect_clks_id)
  have D':
    "[abstr (inv_of A l') (λi j. ∞) v]⇘v,n⇙ = {u. u ⊢ inv_of A l'}"
  using 2 dbm_abstr_zone_eq[OF assms(2) *] by simp
  from assms(3) 2(4) have *: "∀c∈collect_clks g. v c ≤ n"
  unfolding clkp_set_def collect_clkt_def inv_of_def by (fastforce simp: collect_clks_id)
  have D'':"[abstr g (λi j. ∞) v]⇘v,n⇙ = {u. u ⊢ g}" using 2 dbm_abstr_zone_eq[OF assms(2) *] by auto
  with And_correct have A11: "[And D (abstr g (λi j. ∞) v)]⇘v,n⇙ = ([D]⇘v,n⇙) ∩ ({u. u ⊢ g})" by blast
  let ?D = "reset' (And D (abstr g (λi j. ∞) v)) n r v 0"
  have "set r ⊆ clk_set A" using 2(4) unfolding trans_of_def collect_clkvt_def by fastforce
  hence **:"∀c∈set r. v c ≤ n" using assms(3) by fastforce
  have D_reset: "[?D]⇘v,n⇙ = zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r"
  proof safe
    fix u assume u: "u ∈ [?D]⇘v,n⇙"
    from DBM_reset'_sound[OF assms(4,2) ** this] obtain ts where
      "set_clocks r ts u ∈ [And D (abstr g (λi j. ∞) v)]⇘v,n⇙"
    by auto
    with A11 have *: "set_clocks r ts u ∈ ([D]⇘v,n⇙) ∩ ({u. u ⊢ g})" by blast
    from DBM_reset'_resets[OF assms(4,2) **] u
    have "∀c ∈ set r. u c = 0" unfolding DBM_zone_repr_def by auto
    from reset_set[OF this] have "[r→0]set_clocks r ts u = u" by simp
    with * show "u ∈ zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r" unfolding zone_set_def by force
  next
    fix u assume u: "u ∈ zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r"
    from DBM_reset'_complete[OF _ assms(2) **] u A11
    show "u ∈ [?D]⇘v,n⇙" unfolding DBM_zone_repr_def zone_set_def by force
  qed
  from D' And_correct D_reset have A22:
    "[And ?D (abstr (inv_of A l') (λi j. ∞) v)]⇘v,n⇙ = ([?D]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l'})"
  by blast
  with D_reset 2(2-4) show ?thesis by auto
qed

lemma step_z_dbm_DBM:
  assumes "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇘a⇙ ⟨l', Z⟩" "global_clock_numbering A v n"
  obtains D' where "A ⊢ ⟨l, D⟩ ↝⇘v,n,a⇙ ⟨l', D'⟩" "Z = [D']⇘v,n⇙"
using assms
proof (cases, goal_cases)
  case 1
  hence "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n" by metis+
  note assms = assms(1) this
  from assms(3) have *: "∀c∈collect_clks (inv_of A l). v c ≤ n"
  unfolding clkp_set_def collect_clki_def inv_of_def by (fastforce simp: collect_clks_id)
  obtain D'' where D''_def: "D'' = abstr (inv_of A l) (λi j. ∞) v" by auto
  hence D'':"[D'']⇘v,n⇙ = {u. u ⊢ inv_of A l}" using dbm_abstr_zone_eq[OF assms(2) *] by metis
  obtain D_up where D_up': "D_up = up D" by blast
  with up_correct assms(2) have D_up: "[D_up]⇘v,n⇙ = ([D]⇘v,n⇙)⇧↑" by metis
  obtain A2 where A2: "A2 = And D_up D''" by fast
  with And_correct D'' have A22: "[A2]⇘v,n⇙ = ([D_up]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l})" by blast
  have "A ⊢ ⟨l, D⟩ ↝⇘v,n,τ⇙ ⟨l, A2⟩" unfolding A2 D_up' D''_def by blast
  moreover have
    "[A2]⇘v,n⇙ = ([D]⇘v,n⇙)⇧↑ ∩ {u. u ⊢ inv_of A l}"
  unfolding A22 D_up ..
  ultimately show thesis using 1 by (intro that[of A2]) auto
next
  case (2 g a r)
  hence "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n" "∀k≤n. k > 0 ⟶ (∃c. v c = k)" by metis+
  note assms = assms(1) this
  from assms(3) have *: "∀c∈collect_clks (inv_of A l'). v c ≤ n"
  unfolding clkp_set_def collect_clki_def inv_of_def by (fastforce simp: collect_clks_id)
  obtain D' where D'_def: "D' = abstr (inv_of A l') (λi j. ∞) v" by blast
  hence D':"[D']⇘v,n⇙ = {u. u ⊢ inv_of A l'}" using dbm_abstr_zone_eq[OF assms(2) *] by simp
  from assms(3) 2(5) have *: "∀c∈collect_clks g. v c ≤ n"
  unfolding clkp_set_def collect_clkt_def inv_of_def by (fastforce simp: collect_clks_id)
  obtain D'' where D''_def: "D'' = abstr g (λi j. ∞) v" by blast
  hence D'':"[D'']⇘v,n⇙ = {u. u ⊢ g}" using dbm_abstr_zone_eq[OF assms(2) *] by auto
  obtain A1 where A1: "A1 = And D D''" by fast
  with And_correct D'' have A11: "[A1]⇘v,n⇙ = ([D]⇘v,n⇙) ∩ ({u. u ⊢ g})" by blast
  let ?D = "reset' A1 n r v 0"
  have "set r ⊆ clk_set A" using 2(5) unfolding trans_of_def collect_clkvt_def by fastforce
  hence **:"∀c∈set r. v c ≤ n" using assms(3) by fastforce
  have D_reset: "[?D]⇘v,n⇙ = zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r"
  proof safe
    fix u assume u: "u ∈ [?D]⇘v,n⇙"
    from DBM_reset'_sound[OF assms(4,2) ** this] obtain ts where
      "set_clocks r ts u ∈ [A1]⇘v,n⇙"
    by auto
    with A11 have *: "set_clocks r ts u ∈ ([D]⇘v,n⇙) ∩ ({u. u ⊢ g})" by blast
    from DBM_reset'_resets[OF assms(4,2) **] u
    have "∀c ∈ set r. u c = 0" unfolding DBM_zone_repr_def by auto
    from reset_set[OF this] have "[r→0]set_clocks r ts u = u" by simp
    with * show "u ∈ zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r" unfolding zone_set_def by force
  next
    fix u assume u: "u ∈ zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r"
    from DBM_reset'_complete[OF _ assms(2) **] u A11
    show "u ∈ [?D]⇘v,n⇙" unfolding DBM_zone_repr_def zone_set_def by force
  qed
  obtain A2 where A2: "A2 = And ?D D'" by fast
  with And_correct D' have A22: "[A2]⇘v,n⇙ = ([?D]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l'})" by blast
  from 2(5) A2 D'_def D''_def A1 have "A ⊢ ⟨l,D⟩ ↝⇘v,n,↿a⇙ ⟨l',A2⟩" by blast
  moreover from A22 D_reset have
    "[A2]⇘v,n⇙ = zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
  by auto
  ultimately show ?thesis using 2 by (intro that[of A2]) simp+
qed

lemma step_z_computable:
  assumes "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇘a⇙ ⟨l',Z⟩" "global_clock_numbering A v n"
  obtains D' where "Z = [D']⇘v,n⇙"
using step_z_dbm_DBM[OF assms] by blast

lemma step_z_dbm_complete:
  assumes "global_clock_numbering A v n" "A ⊢ ⟨l, u⟩ → ⟨l',u'⟩"
  and     "u ∈ [(D )]⇘v,n⇙"
  shows "∃ D' a. A ⊢ ⟨l, D⟩ ↝⇘v,n,a⇙ ⟨l',D'⟩ ∧ u' ∈ [D']⇘v,n⇙"
proof -
  note A = assms
  from step_z_complete[OF A(2,3)] obtain Z' a where Z':
    "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇘a⇙ ⟨l',Z'⟩" "u' ∈ Z'" by auto
  with step_z_dbm_DBM[OF Z'(1) A(1)] obtain D' where D':
    "A ⊢ ⟨l, D⟩ ↝⇘v,n,a⇙ ⟨l',D'⟩" "Z' = [D']⇘v,n⇙"
  by metis
  with Z'(2) show ?thesis by auto
qed


subsection ‹Additional Useful Properties›

lemma step_z_equiv:
  assumes "global_clock_numbering A v n" "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇘a⇙ ⟨l', Z⟩" "[D]⇘v,n⇙ = [M]⇘v,n⇙"
  shows "A ⊢ ⟨l, [M]⇘v,n⇙⟩ ↝⇘a⇙ ⟨l', Z⟩"
using step_z_dbm_complete[OF assms(1)] step_z_dbm_sound[OF _ assms(1), THEN step_z_sound]
assms(2,3) by force

lemma step_z_dbm_equiv:
  assumes "global_clock_numbering A v n" "A ⊢ ⟨l, D⟩ ↝⇘v,n,a⇙ ⟨l', D'⟩" "[D]⇘v,n⇙ = [M]⇘v,n⇙"
  shows "∃ M'. A ⊢ ⟨l, M⟩ ↝⇘v,n,a⇙ ⟨l', M'⟩ ∧ [D']⇘v,n⇙ = [M']⇘v,n⇙"
proof -
  from step_z_dbm_sound[OF assms(2,1)] have "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇘a⇙ ⟨l', [D']⇘v,n⇙⟩" .
  with step_z_equiv[OF assms(1) this assms(3)] have "A ⊢ ⟨l, [M]⇘v,n⇙⟩ ↝⇘a⇙ ⟨l', [D']⇘v,n⇙⟩" by auto
  from step_z_dbm_DBM[OF this assms(1)] show ?thesis by auto
qed

lemma step_z_empty:
  assumes "A ⊢ ⟨l, {}⟩ ↝⇘a⇙ ⟨l', Z⟩"
  shows "Z = {}"
using step_z_sound[OF assms] by auto

lemma step_z_dbm_empty:
  assumes "global_clock_numbering A v n" "A ⊢ ⟨l, D⟩ ↝⇘v,n,a⇙ ⟨l', D'⟩" "[D]⇘v,n⇙ = {}"
  shows "[D']⇘v,n⇙ = {}"
using step_z_dbm_sound[OF assms(2,1)] assms(3) by - (rule step_z_empty, auto)

end