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 ∗‹ticks› of the clock (to tick or not to tick), the second element is called the ∗‹time›. › abbreviation ticks where ‹ticks ≡ 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. ticks ((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 ticks ((Rep_run ρ) 0 K) then 1 else 0)› | ‹(#⇩≤ ρ K (Suc n)) = (if ticks ((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