Theory Timed_Automata.Timed_Automata

theory Timed_Automata
  imports "library/Graphs" Difference_Bound_Matrices.Zones
begin

chapter ‹Basic Definitions and Semantics›

section ‹Syntactic Definition›

text ‹Clock constraints›
datatype ('c, 't) acconstraint =
  LT 'c 't |
  LE 'c 't |
  EQ 'c 't |
  GT 'c 't |
  GE 'c 't

type_synonym ('c, 't) cconstraint = "('c, 't) acconstraint list"

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 constraint_clk :: "('c, 't) acconstraint ⇒ 'c"
where
  "constraint_clk (LT c _) = c" |
  "constraint_clk (LE c _) = c" |
  "constraint_clk (EQ c _) = c" |
  "constraint_clk (GE c _) = c" |
  "constraint_clk (GT c _) = c"

definition collect_clks :: "('c, 't) cconstraint ⇒ 'c set"
where
  "collect_clks cc ≡ constraint_clk ` set cc"

fun constraint_pair :: "('c, 't) acconstraint ⇒ ('c * 't)"
where
  "constraint_pair (LT x m) = (x, m)" |
  "constraint_pair (LE x m) = (x, m)" |
  "constraint_pair (EQ x m) = (x, m)" |
  "constraint_pair (GE x m) = (x, m)" |
  "constraint_pair (GT x m) = (x, m)"

definition collect_clock_pairs :: "('c, 't) cconstraint ⇒ ('c * 't) set"
where
  "collect_clock_pairs cc = constraint_pair ` set cc"

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

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

definition clkp_set :: "('a, 'c, 't, '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, '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 do 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›

inductive clock_val_a (‹_ ⊢⇩a _› [62, 62] 62) where
  "⟦u c < d⟧ ⟹ u ⊢⇩a LT c d" |
  "⟦u c ≤ d⟧ ⟹ u ⊢⇩a LE c d" |
  "⟦u c = d⟧ ⟹ u ⊢⇩a EQ c d" |
  "⟦u c ≥ d⟧ ⟹ u ⊢⇩a GE c d" |
  "⟦u c > d⟧ ⟹ u ⊢⇩a GT c d"

inductive_cases[elim!]: "u ⊢⇩a LT c d"
inductive_cases[elim!]: "u ⊢⇩a LE c d"
inductive_cases[elim!]: "u ⊢⇩a EQ c d"
inductive_cases[elim!]: "u ⊢⇩a GE c d"
inductive_cases[elim!]: "u ⊢⇩a GT c d"

declare clock_val_a.intros[intro]

definition clock_val :: "('c, 't) cval ⇒ ('c, 't::time) cconstraint ⇒ bool" (‹_ ⊢ _› [62, 62] 62)
where
  "u ⊢ cc = list_all (clock_val_a u) cc"

lemma atomic_guard_continuous:
  assumes "u ⊢⇩a g" "u ⊕ t ⊢⇩a g" "0 ≤ (t'::'t::time)" "t' ≤ t"
  shows "u ⊕ t' ⊢⇩a g"
  using assms
  by (induction g;
      auto 4 3
        simp: cval_add_def order_le_less_subst2 order_subst2 add_increasing2
        intro: less_le_trans
     )

lemma guard_continuous:
  assumes "u ⊢ g" "u ⊕ t ⊢ g" "0 ≤ t'" "t' ≤ t"
  shows "u ⊕ t' ⊢ g"
  using assms by (auto intro: atomic_guard_continuous simp: clock_val_def list_all_iff)


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 ⊕ d ⊢ inv_of A l; d ≥ 0⟧ ⟹ A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l, u ⊕ d⟩"

lemmas [intro] = step_t.intros

context
  notes step_t.cases[elim!] step_t.intros[intro!]
begin

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

end (* End of context for aggressive elimination and intro rules *)

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'⟩)"

declare step.intros[intro]
declare step.cases[elim]

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 ‹Contracting Runs›

inductive step' ::
  "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) cval ⇒ 's ⇒ ('c, 't) cval ⇒ bool"
(‹_ ⊢'' ⟨_, _⟩ → ⟨_, _⟩› [61,61,61] 61)
where
  step': "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l', u'⟩ ⟹ A ⊢ ⟨l', u'⟩ →⇘a⇙ ⟨l'', u''⟩ ⟹ A ⊢' ⟨l, u⟩ → ⟨l'', u''⟩"

lemmas step'[intro]

lemma step'_altI:
  assumes
    "A ⊢ l ⟶⇗g,a,r⇖ l'" "u ⊕ d ⊢ g" "u ⊕ d ⊢ inv_of A l" "0 ≤ d"
    "u' = [r → 0](u ⊕ d)" "u' ⊢ inv_of A l'"
  shows "A ⊢' ⟨l, u⟩ → ⟨l', u'⟩"
  using assms by (auto intro: step_a.intros)

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''⟩"

lemmas steps'.intros[intro]

lemma steps'_altI:
  "A ⊢' ⟨l, u⟩ →* ⟨l'', u''⟩" if "A ⊢' ⟨l, u⟩ →* ⟨l', u'⟩" "A ⊢' ⟨l', u'⟩ → ⟨l'', u''⟩"
  using that by induction auto

lemma step_d_refl[intro]:
  "A ⊢ ⟨l, u⟩ →⇗0⇖ ⟨l, u⟩" if "u ⊢ inv_of A l"
proof -
  from that have "A ⊢ ⟨l, u⟩ →⇗0⇖ ⟨l, u ⊕ 0⟩" by - (rule step_t.intros; force simp: cval_add_def)
  then show ?thesis by (simp add: cval_add_def)
qed

lemma cval_add_simp:
  "(u ⊕ d) ⊕ d' = u ⊕ (d + d')" for d d' :: "'t :: time"
  unfolding cval_add_def by auto

context
  notes [elim!]  = step'.cases step_t.cases
  and   [intro!] = step_t.intros
begin

lemma step_t_trans:
  "A ⊢ ⟨l, u⟩ →⇗d + d'⇖ ⟨l, u''⟩" if "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l, u'⟩" "A ⊢ ⟨l, u'⟩ →⇗d'⇖ ⟨l, u''⟩"
  using that by (auto simp add: cval_add_simp)

lemma steps'_complete:
  "∃ u'. A ⊢' ⟨l, u⟩ →* ⟨l', u'⟩" if "A ⊢ ⟨l, u⟩ →* ⟨l', u'⟩" "u ⊢ inv_of A l"
  using that
proof (induction)
  case (refl A l u)
  then show ?case by blast
next
  case (step A l u l' u' l'' u'')
  then have "u' ⊢ inv_of A l'" by (auto elim: step_a.cases)
  from step(1) show ?case
  proof cases
    case (step_a a)
    with ‹u ⊢ _› ‹u' ⊢ _› step(3) show ?thesis by (auto 4 5)
  next
    case (step_t d)
    then have [simp]: "l' = l" by auto
    from step(3) ‹u' ⊢ _› obtain u0 where "A ⊢' ⟨l, u'⟩ →* ⟨l'', u0⟩" by auto
    then show ?thesis
    proof cases
      case refl'
      then show ?thesis by blast
    next
      case (step' l1 u1)
      with step_t show ?thesis by (auto 4 7 intro: step_t_trans)
    qed
  qed
qed

lemma steps'_sound:
  "A ⊢ ⟨l, u⟩ →* ⟨l', u'⟩" if "A ⊢' ⟨l, u⟩ →* ⟨l', u'⟩"
  using that by (induction; blast)

lemma steps_steps'_equiv:
  "(∃ u'. A ⊢ ⟨l, u⟩ →* ⟨l', u'⟩) ⟷ (∃ u'. A ⊢' ⟨l, u⟩ →* ⟨l', u'⟩)" if "u ⊢ inv_of A l"
  using that steps'_sound steps'_complete by metis

end (* End of context for aggressive elimination and intro rules *)


section ‹Zone Semantics›

datatype 'a action = Tau (‹τ›) | Action 'a (‹↿_›)

inductive step_z ::
  "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) zone ⇒ 'a action ⇒ 's ⇒ ('c, 't) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇘_⇙ ⟨_, _⟩› [61,61,61,61] 61)
where
  step_t_z:
  "A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l, Z⇧↑ ∩ {u. u ⊢ inv_of A l}⟩" |
  step_a_z:
  "A ⊢ ⟨l, Z⟩ ↝⇘↿a⇙ ⟨l', zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}⟩"
  if "A ⊢ l ⟶⇗g,a,r⇖ l'"

lemmas step_z.intros[intro]
inductive_cases step_t_z_E[elim]: "A ⊢ ⟨l, u⟩ ↝⇘τ⇙ ⟨l', u'⟩"
inductive_cases step_a_z_E[elim]: "A ⊢ ⟨l, u⟩ ↝⇘↿a⇙ ⟨l', u'⟩"

subsection ‹Zone Semantics for Compressed Runs›

definition
  step_z' :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) zone ⇒ 's ⇒ ('c, 't) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝ ⟨_, _⟩› [61,61,61] 61)
where
  "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z''⟩ ≡ (∃ Z' a. A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l, Z'⟩ ∧ A ⊢ ⟨l, Z'⟩ ↝⇘↿a⇙ ⟨l', Z''⟩)"

abbreviation
  steps_z :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) zone ⇒ 's ⇒ ('c, 't) zone ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝* ⟨_, _⟩› [61,61,61] 61)
where
  "A ⊢ ⟨l, Z⟩ ↝* ⟨l', Z''⟩ ≡ (λ (l, Z) (l', Z''). A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z''⟩)⇧*⇧* (l, Z) (l', Z'')"

context
  notes [elim!]  = step.cases step'.cases step_t.cases step_z.cases
begin

lemma step_t_z_sound:
  "A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l',Z'⟩ ⟹ ∀ u' ∈ Z'. ∃ u ∈ Z. ∃ d.  A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩"
  by (auto 4 5 simp: zone_delay_def zone_set_def)

lemma step_a_z_sound:
  "A ⊢ ⟨l, Z⟩ ↝⇘↿a⇙ ⟨l',Z'⟩ ⟹ ∀ u' ∈ Z'. ∃ u ∈ Z. ∃ d.  A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l',u'⟩"
  by (auto 4 4 simp: zone_delay_def zone_set_def intro: step_a.intros)

lemma step_z_sound:
  "A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l',Z'⟩ ⟹ ∀ u' ∈ Z'. ∃ u ∈ Z.  A ⊢ ⟨l, u⟩ → ⟨l',u'⟩"
  by (auto 4 6 simp: zone_delay_def zone_set_def intro: step_a.intros)

lemma step_a_z_complete:
  "A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z'. A ⊢ ⟨l, Z⟩ ↝⇘↿a⇙ ⟨l', Z'⟩ ∧ u' ∈ Z'"
  by (auto 4 4 simp: zone_delay_def zone_set_def elim!: step_a.cases)

lemma step_t_z_complete:
  "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z'. A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l', Z'⟩ ∧ u' ∈ Z'"
  by (auto 4 4 simp: zone_delay_def zone_set_def elim!: step_a.cases)

lemma step_z_complete:
  "A ⊢ ⟨l, u⟩ → ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z' a. A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l', Z'⟩ ∧ u' ∈ Z'"
  by (auto 4 4 simp: zone_delay_def zone_set_def elim!: step_a.cases)

end (* End of context for aggressive elimination rules *)

lemma step_z_sound':
  "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ ∀ u' ∈ Z'. ∃ u ∈ Z.  A ⊢' ⟨l, u⟩ → ⟨l',u'⟩"
  unfolding step_z'_def by (fastforce dest!: step_t_z_sound step_a_z_sound)

lemma step_z_complete':
  "A ⊢' ⟨l, u⟩ → ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z'. A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ∧ u' ∈ Z'"
  unfolding step_z'_def by (auto dest!: step_a_z_complete step_t_z_complete elim!: step'.cases)

lemma steps_z_sound:
  "A ⊢ ⟨l, Z⟩ ↝* ⟨l', Z'⟩ ⟹ u' ∈ Z' ⟹ ∃ u ∈ Z. A ⊢' ⟨l, u⟩ →* ⟨l', u'⟩"
  by (induction arbitrary: u' rule: rtranclp_induct2;
      fastforce intro: steps'_altI dest!: step_z_sound')

lemma steps_z_complete:
  "A ⊢' ⟨l, u⟩ →* ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z'. A ⊢ ⟨l, Z⟩ ↝* ⟨l', Z'⟩ ∧ u' ∈ Z'"
  oops

lemma ta_zone_sim:
  "Simulation
    (λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)
    (λ(l, Z) (l', Z''). A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z''⟩)
    (λ(l, u) (l', Z). u ∈ Z ∧ l = l')"
  by standard (auto dest!: step_z_complete')

lemma steps'_iff:
  "(λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩)⇧*⇧* (l, u) (l', u') ⟷ A ⊢' ⟨l, u⟩ →* ⟨l', u'⟩"
  apply standard
  subgoal
    by (induction rule: rtranclp_induct2; blast intro: steps'_altI)
  subgoal
    by (induction rule: steps'.induct; blast intro: converse_rtranclp_into_rtranclp)
  done

lemma steps_z_complete:
  "A ⊢' ⟨l, u⟩ →* ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z'. A ⊢ ⟨l, Z⟩ ↝* ⟨l', Z'⟩ ∧ u' ∈ Z'"
  using Simulation.simulation_reaches[OF ta_zone_sim, of A "(l, u)" "(l', u')"]
  unfolding steps'_iff by auto

end (* Theory *)