# Theory Timed_Automata.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'"  "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)
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'"
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"
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"
obtains D' where "Z = [D']⇘v,n⇙"
using step_z_dbm_DBM[OF assms] by blast

lemma step_z_dbm_complete:
assumes  "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
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
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
(*>*)