# Theory Run

```section ‹ Defining Runs ›

theory Run
imports TESL

begin
text ‹
Runs are sequences of instants, and each instant maps a clock to a pair
@{term ‹(h, t)›} where @{term ‹h›} indicates whether the clock ticks or not,
and @{term ‹t›} is the current time on this clock.
The first element of the pair is called the ∗‹hamlet› of the clock (to tick or
not to tick), the second element is called the ∗‹time›.
›

abbreviation hamlet where ‹hamlet ≡ fst›
abbreviation time   where ‹time ≡ snd›

type_synonym 'τ instant = ‹clock ⇒ (bool × 'τ tag_const)›

text‹
Runs have the additional constraint that time cannot go backwards on any clock
in the sequence of instants.
Therefore, for any clock, the time projection of a run is monotonous.
›
‹{ ρ::nat ⇒ 'τ instant. ∀c. mono (λn. time (ρ n c)) }›
proof
show ‹(λ_ _. (True, τ⇩c⇩s⇩t 0)) ∈ {ρ. ∀c. mono (λn. time (ρ n c))}›
unfolding mono_def by blast
qed

lemma Abs_run_inverse_rewrite:
‹∀c. mono (λn. time (ρ n c)) ⟹ Rep_run (Abs_run ρ) = ρ›

text ‹
A ∗‹dense› run is a run in which something happens (at least one clock ticks)
at every instant.
›
definition ‹dense_run ρ ≡ (∀n. ∃c. hamlet ((Rep_run ρ) n c))›

text‹
@{term ‹run_tick_count ρ K n›} counts the number of ticks on clock @{term ‹K›}
in the interval ▩‹[0, n]› of run @{term ‹ρ›}.
›
fun run_tick_count :: ‹('τ::linordered_field) run ⇒ clock ⇒ nat ⇒ nat›
(‹#⇩≤ _ _ _›)
where
‹(#⇩≤ ρ K 0)       = (if hamlet ((Rep_run ρ) 0 K)
then 1
else 0)›
| ‹(#⇩≤ ρ K (Suc n)) = (if hamlet ((Rep_run ρ) (Suc n) K)
then 1 + (#⇩≤ ρ K n)
else (#⇩≤ ρ K n))›

text‹
@{term ‹run_tick_count_strictly ρ K n›} counts the number of ticks on
clock @{term ‹K›} in the interval ▩‹[0, n[› of run @{term ‹ρ›}.
›
fun run_tick_count_strictly :: ‹('τ::linordered_field) run ⇒ clock ⇒ nat ⇒ nat›
(‹#⇩< _ _ _›)
where
‹(#⇩< ρ K 0)       = 0›
| ‹(#⇩< ρ K (Suc n)) = #⇩≤ ρ K n›

text‹
@{term ‹first_time ρ K n τ›} tells whether instant @{term ‹n›} in run @{term‹ρ›}
is the first one where the time on clock @{term ‹K›} reaches @{term ‹τ›}.
›
definition first_time :: ‹'a::linordered_field run ⇒ clock ⇒ nat ⇒ 'a tag_const
⇒ bool›
where
‹first_time ρ K n τ ≡ (time ((Rep_run ρ) n K) = τ)
∧ (∄n'. n' < n ∧ time ((Rep_run ρ) n' K) = τ)›

text‹
The time on a clock is necessarily less than @{term ‹τ›} before the first instant
at which it reaches @{term ‹τ›}.
›
lemma before_first_time:
assumes ‹first_time ρ K n τ›
and ‹m < n›
shows ‹time ((Rep_run ρ) m K) < τ›
proof -
have ‹mono (λn. time (Rep_run ρ n K))› using Rep_run by blast
moreover from assms(2) have ‹m ≤ n› using less_imp_le by simp
moreover have ‹mono (λn. time (Rep_run ρ n K))› using Rep_run by blast
ultimately have  ‹time ((Rep_run ρ) m K) ≤ time ((Rep_run ρ) n K)›
moreover from assms(1) have ‹time ((Rep_run ρ) n K) = τ›
using first_time_def by blast
moreover from assms have ‹time ((Rep_run ρ) m K) ≠ τ›
using first_time_def by blast
ultimately show ?thesis by simp
qed

text‹
This leads to an alternate definition of @{term ‹first_time›}:
›
lemma alt_first_time_def:
assumes ‹∀m < n. time ((Rep_run ρ) m K) < τ›
and ‹time ((Rep_run ρ) n K) = τ›
shows ‹first_time ρ K n τ›
proof -
from assms(1) have ‹∀m < n. time ((Rep_run ρ) m K) ≠ τ›