Theory DBM_Zone_Semantics

subsection ‹Semantics Based on DBMs›

theory DBM_Zone_Semantics
imports DBM_Operations
begin

subsection ‹Single Step›

inductive step_z_dbm ::
  "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('t::time) DBM
    ⇒ ('c ⇒ nat) ⇒ nat ⇒ 's ⇒ ('t::time) DBM ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝⇘_,_⇙ ⟨_, _⟩" [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 (And D D_inv)) D_inv⟩" |
  step_a_z_dbm:
    "A ⊢ l ⟶⇗g,a,r⇖ l'
    ⟹ A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨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_cases: "A ⊢ ⟨l, D⟩ ↝⇘v,n⇙ ⟨l', D'⟩"

declare step_z_dbm.intros[intro]

lemma step_z_dbm_preserves_int:
  assumes "A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨l',D'⟩" "global_clock_numbering A v n" "valid_abstraction A X k"
          "dbm_int D n"
  shows "dbm_int D' n"
using assms
proof (cases, goal_cases)
  case (1 D'')
  hence "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n" by blast+
  from 1(2) have "∀ (x, m) ∈ clkp_set A. m ∈ ℕ" by (auto elim: valid_abstraction.cases)
  from dbm_int_inv_abstr[OF this] 1 have D''_int: "dbm_int D'' n" by simp
  show ?thesis unfolding 1(5) 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" "∀k≤n. k > 0 ⟶ (∃c. v c = k)" by blast+
  from 2(2) have *: "∀ (x, m) ∈ clkp_set A. m ∈ ℕ" by (auto elim: valid_abstraction.cases)
  from dbm_int_inv_abstr[OF this] 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(5) 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(4)
  by (intro And_int_preservation DBM_reset'_int_preservation dbm_int_inv_abstr 2 D''_int)
     (simp_all add: assms(1) * **)
qed

lemma And_correct:
  shows "[M1]⇘v,n⇙ ∩ [M2]⇘v,n⇙ = [And M1 M2]⇘v,n⇙"
using DBM_and_sound1 DBM_and_sound2 DBM_and_complete unfolding DBM_zone_repr_def by auto

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⇙ ⟨l', D'⟩" "global_clock_numbering A v n"
  shows "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝ ⟨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
  with And_correct D'' have
    "[D']⇘v,n⇙ = ([up (And D D'')]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l})"
  unfolding 1(3) by blast
  with up_correct[OF assms(2)] A11 have
    "[D']⇘v,n⇙ = (([D]⇘v,n⇙) ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {u. u ⊢ inv_of A l}"
  by metis
  with 1(2) show ?thesis by 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 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(3) 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(3) 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,3) show ?thesis by auto
qed

lemma step_z_dbm_DBM:
  assumes "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝ ⟨l', Z⟩" "global_clock_numbering A v n"
  obtains D' where "A ⊢ ⟨l, D⟩ ↝⇘v,n⇙ ⟨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 A1 where A1: "A1 = And D D''" by fast
  with And_correct D'' have A11: "[A1]⇘v,n⇙ = ([D]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l})" by blast
  then obtain D_up where D_up': "D_up = up A1" by blast
  with up_correct assms(2) A11 have D_up: "[D_up]⇘v,n⇙ = (([D]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l}))⇧↑" 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
  from A2 D_up' D''_def A1 have "A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨l,A2⟩" by blast
  moreover from A22 D_up have
    "[A2]⇘v,n⇙ = (([D]⇘v,n⇙) ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {u. u ⊢ inv_of A l}"
  by auto
  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(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)
  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(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 ∈ [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(4) A2 D'_def D''_def A1 have "A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨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⇙⟩ ↝ ⟨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 ⊢ ⟨l, D⟩ ↝⇘v,n⇙ ⟨l',D'⟩ ∧ u' ∈ [D']⇘v,n⇙"
proof -
  note A = assms
  from step_z_complete[OF A(2,3)] obtain Z' where Z': "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝ ⟨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⇙ ⟨l',D'⟩" "Z' = [D']⇘v,n⇙"
  by metis
  with Z'(2) show ?thesis by auto
qed


subsection ‹Multi Step›

inductive steps_z_dbm ::
  "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('t::time) DBM
    ⇒ ('c ⇒ nat) ⇒ nat ⇒ 's ⇒ ('t::time) DBM ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝*⇘_,_⇙ ⟨_, _⟩" [61,61,61] 61)
where
  refl: "A ⊢ ⟨l,D⟩ ↝*⇘v,n⇙ ⟨l,D⟩" |
  step: "A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨l',D'⟩ ⟹ A ⊢ ⟨l',D'⟩ ↝*⇘v,n⇙ ⟨l'',D''⟩ ⟹
         A ⊢ ⟨l,D⟩ ↝*⇘v,n⇙ ⟨l'',D''⟩"

declare steps_z_dbm.intros[intro]

lemma steps_z_dbm_sound:
  assumes "A ⊢ ⟨l,D⟩ ↝*⇘v,n⇙ ⟨l',D'⟩"
  and "global_clock_numbering A v n"
  and "u' ∈ [D']⇘v,n⇙"
  shows "∃ u ∈ [D]⇘v,n⇙. A ⊢ ⟨l, u⟩ →* ⟨l',u'⟩" using assms
proof (induction A l D v n l' D' rule: steps_z_dbm.induct)
  case refl thus ?case by fast
next
  case (step A l D v n l' D' l'' D'')
  then obtain u'' where u'': "A ⊢ ⟨l', u''⟩ →* ⟨l'',u'⟩" "u''∈[D']⇘v,n⇙" by blast
  with step_z_sound[OF step_z_dbm_sound[OF step(1,4)]] obtain u where
    "u ∈ [D]⇘v,n⇙" "A ⊢ ⟨l, u⟩ → ⟨l',u''⟩"
  by blast
  with u'' show ?case by blast
qed

lemma steps_z_dbm_complete:
  assumes "A ⊢ ⟨l, u⟩ →* ⟨l',u'⟩"
  and "global_clock_numbering A v n"
  and "u ∈ [D]⇘v,n⇙"
  shows "∃ D'. A ⊢ ⟨l, D⟩ ↝*⇘v,n⇙ ⟨l', D'⟩ ∧ u' ∈ [D']⇘v,n⇙" using assms
proof (induction arbitrary: D rule: steps.induct)
  case refl thus ?case by auto
next
  case (step A l u l' u' l'' u'' D)
  from step_z_dbm_complete[OF step(4,1,5)] obtain D'
  where D': "A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨l',D'⟩" "u' ∈ [D']⇘v,n⇙" by auto
  with step(3)[OF step(4)] obtain D'' where
    "A ⊢ ⟨l',D'⟩ ↝*⇘v,n⇙ ⟨l'',D''⟩" "u'' ∈ [D'']⇘v,n⇙"
  by blast
  with D' show ?case by blast
qed

end
(*>*)