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.
›
typedef (overloaded) 'τ::linordered_field run =
  ‹{ ρ::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 ρ) = ρ›
by (simp add: Abs_run_inverse)

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)›
    by (simp add:mono_def)
  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) ≠ τ›
    by (simp add: less_le)
  with assms(2) show ?thesis by (simp add: first_time_def)
qed

end