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,r⇖ l') ≡ (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⟩ →⇗d⇖ ⟨l, u ⊕ d⟩"

declare step_t.intros[intro!]

inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩"

lemma step_t_determinacy1:
  "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩ ⟹  A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l'',u''⟩ ⟹ l' = l''"
by auto

lemma step_t_determinacy2:
  "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩ ⟹  A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l'',u''⟩ ⟹ u' = u''"
by auto

lemma step_t_cont1:
  "d ≥ 0 ⟹ e ≥ 0 ⟹ A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩ ⟹ A ⊢ ⟨l', u'⟩ →⇗e⇖ ⟨l'',u''⟩
  ⟹ A ⊢ ⟨l, u⟩ →⇗d+e⇖ ⟨l'',u''⟩"
proof -
  assume A: "d ≥ 0" "e ≥ 0" "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩" "A ⊢ ⟨l', u'⟩ →⇗e⇖ ⟨l'',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,r⇖ l'; u ⊢ g; u' ⊢ inv_of A l'; u' = [r → 0]u⟧ ⟹ (A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l', 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⟩ →⇘a⇙ ⟨l',u'⟩ ⟹ (A ⊢ ⟨l, u⟩ → ⟨l',u'⟩)" |
  step_t: "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',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,r⇖ l'⟧
              ⟹ (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' = [r→0]u" "u ∈ Z"
    unfolding zone_set_def by auto
    with step_a.intros[OF 2 this(1-3)] show "∃u∈Z. 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' = [r→0]u" "A ⊢ l ⟶⇗g,a,r⇖ l'" "u ⊢ g" "[r→0]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' = [r→0]u" "A ⊢ l ⟶⇗g,a,r⇖ l'" "u ⊢ g" "[r→0]u ⊢ inv_of A l'"
  by (cases rule: step_a.cases) auto
  hence "{[r→0]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