Quelle  Run.thy

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, τ_cst 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