# Theory Timed_Automata.Timed_Automata

```theory Timed_Automata
imports Main
begin

chapter ‹Basic Definitions and Semantics›

section ‹Time›

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"

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
```