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,nl,And (up (And D D_inv)) D_inv" |
  step_a_z_dbm:
    "A  l ⟶⇗g,a,rl'
     A  l,D ↝⇘v,nl',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,nl', D'"

declare step_z_dbm.intros[intro]

lemma step_z_dbm_preserves_int:
  assumes "A  l,D ↝⇘v,nl',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" "cclk_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" "cclk_set A. v c  n" "kn. 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 **:"cset 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,nl', 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" "cclk_set A. v c  n" by blast+
  note assms = assms(1) this
  from assms(3) have *: "ccollect_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" "cclk_set A. v c  n" "kn. k > 0  (c. v c = k)" by blast+
  note assms = assms(1) this
  from assms(3) have *: "ccollect_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 *: "ccollect_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 **:"cset 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 "[r0]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,nl', D'" "Z = [D']⇘v,n⇙"
using assms
proof (cases, goal_cases)
  case 1
  hence "clock_numbering' v n" "cclk_set A. v c  n" by metis+
  note assms = assms(1) this
  from assms(3) have *: "ccollect_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,nl,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" "cclk_set A. v c  n" "kn. k > 0  (c. v c = k)" by metis+
  note assms = assms(1) this
  from assms(3) have *: "ccollect_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 *: "ccollect_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 **:"cset 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 "[r0]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,nl',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,nl',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,nl',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,nl,D" |
  step: "A  l,D ↝⇘v,nl',D'  A  l',D' ↝*⇘v,nl'',D'' 
         A  l,D ↝*⇘v,nl'',D''"

declare steps_z_dbm.intros[intro]

lemma steps_z_dbm_sound:
  assumes "A  l,D ↝*⇘v,nl',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,nl', 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,nl',D'" "u'  [D']⇘v,n⇙" by auto
  with step(3)[OF step(4)] obtain D'' where
    "A  l',D' ↝*⇘v,nl'',D''" "u''  [D'']⇘v,n⇙"
  by blast
  with D' show ?case by blast
qed

end
(*>*)