Theory Timed_Automata.Timed_Automata

theory Timed_Automata
  imports Main
begin

chapter ‹Basic Definitions and Semantics›

section ‹Time›

class time = linordered_ab_group_add +
  assumes dense: "x < y  z. x < z  z < y"
  assumes non_trivial: " x. x  0"

begin

lemma non_trivial_neg: " x. x < 0"
proof -
  from non_trivial obtain x where "x  0" by auto
  then show ?thesis
  proof (cases "x < 0", auto, goal_cases)
    case 1
    then have "x > 0" by auto
    then have "(-x) < 0" by auto
    then show ?case by blast
  qed
qed

end

datatype ('c, 't :: time) cconstraint =
  AND "('c, 't) cconstraint" "('c, 't) cconstraint" |
  LT 'c 't |
  LE 'c 't |
  EQ 'c 't |
  GT 'c 't |
  GE 'c 't

section ‹Syntactic Definition›

text ‹
  For an informal description of timed automata we refer to Bengtsson and Yi cite"BengtssonY03".
  We define a timed automaton A›

type_synonym
  ('c, 'time, 's) invassn = "'s  ('c, 'time) cconstraint"

type_synonym
  ('a, 'c, 'time, 's) transition = "'s * ('c, 'time) cconstraint * 'a * 'c list * 's"

type_synonym
  ('a, 'c, 'time, 's) ta = "('a, 'c, 'time, 's) transition set * ('c, 'time, 's) invassn"

definition trans_of :: "('a, 'c, 'time, 's) ta  ('a, 'c, 'time, 's) transition set" where
  "trans_of  fst"
definition inv_of  :: "('a, 'c, 'time, 's) ta  ('c, 'time, 's) invassn" where
  "inv_of  snd"

abbreviation transition ::
  "('a, 'c, 'time, 's) ta  's  ('c, 'time) cconstraint  'a  'c list  's  bool"
("_  _ ⟶⇗_,_,_ _" [61,61,61,61,61,61] 61) where
  "(A  l ⟶⇗g,a,rl')  (l,g,a,r,l')  trans_of A"

subsection ‹Collecting Information About Clocks›

fun collect_clks :: "('c, 't :: time) cconstraint  'c set"
where
  "collect_clks (AND cc1 cc2) = collect_clks cc1  collect_clks cc2" |
  "collect_clks (LT c _) = {c}" |
  "collect_clks (LE c _) = {c}" |
  "collect_clks (EQ c _) = {c}" |
  "collect_clks (GE c _) = {c}" |
  "collect_clks (GT c _) = {c}"

fun collect_clock_pairs :: "('c, 't :: time) cconstraint  ('c * 't) set"
where
  "collect_clock_pairs (LT x m) = {(x, m)}" |
  "collect_clock_pairs (LE x m) = {(x, m)}" |
  "collect_clock_pairs (EQ x m) = {(x, m)}" |
  "collect_clock_pairs (GE x m) = {(x, m)}" |
  "collect_clock_pairs (GT x m) = {(x, m)}" |
  "collect_clock_pairs (AND cc1 cc2) = (collect_clock_pairs cc1  collect_clock_pairs cc2)"

definition collect_clkt :: "('a, 'c, 't::time, 's) transition set  ('c *'t) set"
where
  "collect_clkt S =  {collect_clock_pairs (fst (snd t)) | t . t  S}"

definition collect_clki :: "('c, 't :: time, 's) invassn  ('c *'t) set"
where
  "collect_clki I =  {collect_clock_pairs (I x) | x. True}"

definition clkp_set :: "('a, 'c, 't :: time, 's) ta  ('c *'t) set"
where
  "clkp_set A = collect_clki (inv_of A)  collect_clkt (trans_of A)"

definition collect_clkvt :: "('a, 'c, 't::time, 's) transition set  'c set"
where
  "collect_clkvt S =  {set ((fst o snd o snd o snd) t) | t . t  S}"

abbreviation clk_set where "clk_set A  fst ` clkp_set A  collect_clkvt (trans_of A)"

(* We don not need this here but most other theories will make use of this predicate *)
inductive valid_abstraction
where
  "(x,m)  clkp_set A. m  k x  x  X  m  ; collect_clkvt (trans_of A)  X; finite X
   valid_abstraction A X k"

section ‹Operational Semantics›

type_synonym ('c, 't) cval = "'c  't"

definition cval_add :: "('c,'t) cval  't::time  ('c,'t) cval" (infixr "" 64)
where
  "u  d = (λ x. u x + d)"

inductive clock_val :: "('c, 't) cval  ('c, 't::time) cconstraint  bool" ("_  _" [62, 62] 62)
where
  "u  cc1; u  cc2  u  AND cc1 cc2" |
  "u c < d  u  LT c d" |
  "u c  d  u  LE c d" |
  "u c = d  u  EQ c d" |
  "u c  d  u  GE c d" |
  "u c > d  u  GT c d"

declare clock_val.intros[intro]

inductive_cases[elim!]: "u  AND cc1 cc2"
inductive_cases[elim!]: "u  LT c d"
inductive_cases[elim!]: "u  LE c d"
inductive_cases[elim!]: "u  EQ c d"
inductive_cases[elim!]: "u  GE c d"
inductive_cases[elim!]: "u  GT c d"

fun clock_set :: "'c list  't::time  ('c,'t) cval  ('c,'t) cval"
where
  "clock_set [] _ u = u" |
  "clock_set (c#cs) t u = (clock_set cs t u)(c:=t)"

abbreviation clock_set_abbrv :: "'c list  't::time  ('c,'t) cval  ('c,'t) cval"
("[__]_" [65,65,65] 65)
where
  "[r  t]u  clock_set r t u"

inductive step_t ::
  "('a, 'c, 't, 's) ta  's  ('c, 't) cval  ('t::time)  's  ('c, 't) cval  bool"
("_  _, _ →⇗_ _, _" [61,61,61] 61)                      
where
  "u  inv_of A l; u  d  inv_of A l; d  0  A  l, u →⇗dl, u  d"

declare step_t.intros[intro!]

inductive_cases[elim!]: "A  l, u →⇗dl',u'"

lemma step_t_determinacy1:
  "A  l, u →⇗dl',u'   A  l, u →⇗dl'',u''  l' = l''"
by auto

lemma step_t_determinacy2:
  "A  l, u →⇗dl',u'   A  l, u →⇗dl'',u''  u' = u''"
by auto

lemma step_t_cont1:
  "d  0  e  0  A  l, u →⇗dl',u'  A  l', u' →⇗el'',u''
   A  l, u →⇗d+el'',u''"
proof -
  assume A: "d  0" "e  0" "A  l, u →⇗dl',u'" "A  l', u' →⇗el'',u''"
  hence "u' = (u  d)" "u'' = (u'  e)" by auto
  hence "u'' = (u  (d + e))" unfolding cval_add_def by auto
  with A show ?thesis by auto
qed

inductive step_a ::
  "('a, 'c, 't, 's) ta  's  ('c, ('t::time)) cval  'a  's  ('c, 't) cval  bool"
("_  _, _ →⇘_ _, _" [61,61,61] 61)
where
  "A  l ⟶⇗g,a,rl'; u  g; u'  inv_of A l'; u' = [r  0]u  (A  l, u →⇘al', u')"

inductive step ::
  "('a, 'c, 't, 's) ta  's  ('c, ('t::time)) cval  's  ('c, 't) cval  bool"
("_  _, _  _,_" [61,61,61] 61)
where
  step_a: "A  l, u →⇘al',u'  (A  l, u  l',u')" |
  step_t: "A  l, u →⇗dl',u'  (A  l, u  l',u')"

inductive_cases[elim!]: "A  l, u  l',u'"

declare step.intros[intro]

inductive
  steps :: "('a, 'c, 't, 's) ta  's  ('c, ('t::time)) cval  's  ('c, 't) cval  bool"
("_  _, _ →* _, _" [61,61,61] 61)
where
  refl: "A  l, u →* l, u" |
  step: "A  l, u  l', u'  A  l', u' →* l'', u''  A  l, u →* l'', u''"

declare steps.intros[intro]

section ‹Zone Semantics›

type_synonym ('c, 't) zone = "('c, 't) cval set"

definition zone_delay :: "('c, ('t::time)) zone  ('c, 't) zone"
("_" [71] 71)
where
  "Z = {u  d|u d. u  Z  d  (0::'t)}"

definition zone_set :: "('c, 't::time) zone  'c list  ('c, 't) zone"
("__  0⇙" [71] 71)
where
  "zone_set Z r = {[r  (0::'t)]u | u . u  Z}"

inductive step_z ::
  "('a, 'c, 't, 's) ta  's  ('c, ('t::time)) zone  's  ('c, 't) zone  bool"
("_  _, _  _, _" [61,61,61] 61)
where
  step_t_z: "A  l, Z  l, (Z  {u. u  inv_of A l})  {u. u  inv_of A l}" |
  step_a_z: "A  l ⟶⇗g,a,rl'
               (A  l, Z  l', zone_set (Z  {u. u  g}) r  {u. u  inv_of A l'} )"

inductive_cases[elim!]: "A  l, u  l', u'"

declare step_z.intros[intro]

lemma step_z_sound:
  "A  l, Z  l',Z'  ( u'  Z'.  u  Z.  A  l, u  l',u')"
proof (induction rule: step_z.induct, goal_cases)
  case 1 thus ?case unfolding zone_delay_def by blast
next
  case (2 A l g a r l' Z)
  show ?case
  proof
    fix u' assume "u'  zone_set (Z  {u. u  g}) r  {u. u  inv_of A l'}"
    then obtain u where
      "u  g" "u'  inv_of A l'" "u' = [r0]u" "u  Z"
    unfolding zone_set_def by auto
    with step_a.intros[OF 2 this(1-3)] show "uZ. A  l, u  l',u'" by fast
  qed
qed

lemma step_z_complete:
  "A  l, u  l', u'  u  Z   Z'. A  l, Z  l', Z'  u'  Z'"
proof (induction rule: step.induct, goal_cases)
  case (1 A l u a l' u')
  then obtain g r
  where u': "u' = [r0]u" "A  l ⟶⇗g,a,rl'" "u  g" "[r0]u  inv_of A l'"
  by (cases rule: step_a.cases) auto
  hence "u'  zone_set (Z  {u. u  g}) r  {u. u  inv_of A l'}"
  unfolding zone_set_def using u  Z by blast
  with u'(1,2) show ?case by blast
next
  case (2 A l u d l' u')
  hence u': "u' = (u  d)" "u  inv_of A l" "u  d  inv_of A l" "0  d" and "l = l'" by auto
  with u' u  Z have
    "u'  {u''  d |u'' d. u''  Z  {u. u  inv_of A l}  0  d}  {u. u  inv_of A l}"
  by fastforce
  thus ?case using l = l'  step_t_z[unfolded zone_delay_def, of A l] by blast
qed

text ‹
  Corresponds to version in old papers --
  not strong enough for inductive proof over transitive closure relation.
›
lemma step_z_complete1:
  "A  l, u  l', u'   Z. A  l, {u}  l', Z  u'  Z"
proof (induction rule: step.induct, goal_cases)
  case (1 A l u a l' u')
  then obtain g r
  where u': "u' = [r0]u" "A  l ⟶⇗g,a,rl'" "u  g" "[r0]u  inv_of A l'"
  by (cases rule: step_a.cases) auto
  hence "{[r0]u} = zone_set ({u}  {u. u  g}) r  {u. u  inv_of A l'}"
  unfolding zone_set_def by blast
  with u'(1,2) show ?case by auto 
next
  case (2 A l u d l' u')
  hence u': "u' = (u  d)" "u  inv_of A l" "u  d  inv_of A l" "0  d" and "l = l'" by auto
  hence "{u} = {u}  {u''. u''  inv_of A l}" by fastforce 
  with u'(1) have "{u'} = {u''  d |u''. u''  {u}  {u''. u''  inv_of A l}}" by fastforce
  with u' have
    "u'  {u''  d |u'' d. u''  {u}  {u. u  inv_of A l}  0  d}  {u. u  inv_of A l}"
  by fastforce
  thus ?case using l = l' step_t_z[unfolded zone_delay_def, of A l "{u}"] by blast
qed

text ‹
  Easier proof.
›
lemma step_z_complete2:
  "A  l, u  l', u'   Z. A  l, {u}  l', Z  u'  Z"
using step_z_complete by fast

inductive
  steps_z :: "('a, 'c, 't, 's) ta  's  ('c, ('t::time)) 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.intros[intro]

lemma steps_z_sound:
  "A  l, Z ↝* l', Z'  u'  Z'   u  Z. A  l, u →* l', u'"
proof (induction A l _ l' _ arbitrary: rule: steps_z.induct, goal_cases)
  case refl thus ?case by fast
next
  case (step A l Z l' Z' l'' Z'')
  then obtain u'' where u'': "A  l', u'' →* l'',u'" "u''  Z'" by auto
  then obtain u where "u  Z" "A  l, u  l',u''" using step_z_sound[OF step(1)] by blast
  with u'' show ?case by blast
qed

lemma steps_z_complete:
  "A  l, u →* l', u'  u  Z   Z'. A  l, Z ↝* l', Z'  u'  Z'"
proof (induction arbitrary: Z rule: steps.induct)
  case refl thus ?case by auto
next
  case (step A l u l' u' l'' u'' Z)
  from step_z_complete[OF this(1,4)] obtain Z' where Z': "A  l, Z  l',Z'" "u'  Z'" by auto
  then obtain Z'' where "A  l', Z' ↝* l'',Z''" "u''  Z''" using step by metis
  with Z' show ?case by blast
qed

end