# Theory Stuttering

```subsection‹Main Theorems›

theory Stuttering
imports StutteringLemmas

begin

text ‹
Using the lemmas of the previous section about the invariance by stuttering
of various properties of TESL specifications, we can now prove that the atomic
formulae that compose TESL specifications are invariant by stuttering.
›

text ‹Sporadic specifications are preserved in a dilated run.›
assumes ‹sub ≪ r›
and ‹sub ∈ ⟦c sporadic τ on c'⟧⇩T⇩E⇩S⇩L›
shows ‹r ∈ ⟦c sporadic τ on c'⟧⇩T⇩E⇩S⇩L›
proof -
from assms(1) is_subrun_def obtain f
where ‹dilating f sub r› by blast
hence ‹∀n c. time ((Rep_run sub) n c) = time ((Rep_run r) (f n) c)
∧ hamlet ((Rep_run sub) n c) = hamlet ((Rep_run r) (f n) c)› by (simp add: dilating_def)
moreover from assms(2) have
‹sub ∈ {r. ∃ n. hamlet ((Rep_run r) n c) ∧ time ((Rep_run r) n c') = τ}› by simp
from this obtain k where ‹time ((Rep_run sub) k c') = τ ∧ hamlet ((Rep_run sub) k c)› by auto
ultimately have ‹time ((Rep_run r) (f k) c') = τ ∧ hamlet ((Rep_run r) (f k) c)› by simp
thus ?thesis by auto
qed

text ‹Implications are preserved in a dilated run.›
theorem implies_sub:
assumes ‹sub ≪ r›
and ‹sub ∈ ⟦c⇩1 implies c⇩2⟧⇩T⇩E⇩S⇩L›
shows ‹r ∈ ⟦c⇩1 implies c⇩2⟧⇩T⇩E⇩S⇩L›
proof -
from assms(1) is_subrun_def obtain f where ‹dilating f sub r› by blast
moreover from assms(2) have
‹sub ∈ {r. ∀n. hamlet ((Rep_run r) n c⇩1) ⟶ hamlet ((Rep_run r) n c⇩2)}› by simp
hence ‹∀n. hamlet ((Rep_run sub) n c⇩1) ⟶ hamlet ((Rep_run sub) n c⇩2)› by simp
ultimately have ‹∀n. hamlet ((Rep_run r) n c⇩1) ⟶ hamlet ((Rep_run r) n c⇩2)›
using ticks_imp_ticks_subk ticks_sub by blast
thus ?thesis by simp
qed

theorem implies_not_sub:
assumes ‹sub ≪ r›
and ‹sub ∈ ⟦c⇩1 implies not c⇩2⟧⇩T⇩E⇩S⇩L›
shows ‹r ∈ ⟦c⇩1 implies not c⇩2⟧⇩T⇩E⇩S⇩L›
proof -
from assms(1) is_subrun_def obtain f where ‹dilating f sub r› by blast
moreover from assms(2) have
‹sub ∈ {r. ∀n. hamlet ((Rep_run r) n c⇩1) ⟶ ¬ hamlet ((Rep_run r) n c⇩2)}› by simp
hence ‹∀n. hamlet ((Rep_run sub) n c⇩1) ⟶ ¬ hamlet ((Rep_run sub) n c⇩2)› by simp
ultimately have ‹∀n. hamlet ((Rep_run r) n c⇩1) ⟶ ¬ hamlet ((Rep_run r) n c⇩2)›
using ticks_imp_ticks_subk ticks_sub by blast
thus ?thesis by simp
qed

text ‹Precedence relations are preserved in a dilated run.›
theorem weakly_precedes_sub:
assumes ‹sub ≪ r›
and ‹sub ∈ ⟦c⇩1 weakly precedes c⇩2⟧⇩T⇩E⇩S⇩L›
shows ‹r ∈ ⟦c⇩1 weakly precedes c⇩2⟧⇩T⇩E⇩S⇩L›
proof -
from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast
from assms(2) have
‹sub ∈ {r. ∀n. (run_tick_count r c⇩2 n) ≤ (run_tick_count r c⇩1 n)}› by simp
hence ‹∀n. (run_tick_count sub c⇩2 n) ≤ (run_tick_count sub c⇩1 n)› by simp
from dil_tick_count[OF assms(1) this]
have ‹∀n. (run_tick_count r c⇩2 n) ≤ (run_tick_count r c⇩1 n)› by simp
thus ?thesis by simp
qed

theorem strictly_precedes_sub:
assumes ‹sub ≪ r›
and ‹sub ∈ ⟦c⇩1 strictly precedes c⇩2⟧⇩T⇩E⇩S⇩L›
shows ‹r ∈ ⟦c⇩1 strictly precedes c⇩2⟧⇩T⇩E⇩S⇩L›
proof -
from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast
from assms(2) have
‹sub ∈ { ρ. ∀n::nat. (run_tick_count ρ c⇩2 n) ≤ (run_tick_count_strictly ρ c⇩1 n) }›
by simp
with strictly_precedes_alt_def2[of ‹c⇩2› ‹c⇩1›]  have
‹sub ∈ { ρ. (¬hamlet ((Rep_run ρ) 0 c⇩2))
∧ (∀n::nat. (run_tick_count ρ c⇩2 (Suc n)) ≤ (run_tick_count ρ c⇩1 n)) }›
by blast
hence ‹(¬hamlet ((Rep_run sub) 0 c⇩2))
∧ (∀n::nat. (run_tick_count sub c⇩2 (Suc n)) ≤ (run_tick_count sub c⇩1 n))›
by simp
hence
1:‹(¬hamlet ((Rep_run sub) 0 c⇩2))
∧ (∀n::nat. (tick_count sub c⇩2 (Suc n)) ≤ (tick_count sub c⇩1 n))›
have ‹∀n::nat. (tick_count r c⇩2 (Suc n)) ≤ (tick_count r c⇩1 n)›
proof -
{ fix n::nat
have ‹tick_count r c⇩2 (Suc n) ≤ tick_count r c⇩1 n›
proof (cases ‹∃n⇩0. f n⇩0 = n›)
case True ― ‹n is in the image of f›
from this obtain n⇩0 where fn:‹f n⇩0 = n› by blast
show ?thesis
proof (cases ‹∃sn⇩0. f sn⇩0 = Suc n›)
case True ― ‹Suc n is in the image of f›
from this obtain sn⇩0 where fsn:‹f sn⇩0 = Suc n› by blast
with fn strict_mono_suc * have ‹sn⇩0 = Suc n⇩0›
using  dilating_def dilating_fun_def by blast
with 1 have ‹tick_count sub c⇩2 sn⇩0 ≤ tick_count sub c⇩1 n⇩0› by simp
thus ?thesis using fn fsn tick_count_sub[OF *] by simp
next
case False ― ‹Suc n is not in the image of f›
hence ‹¬hamlet ((Rep_run r) (Suc n) c⇩2)›
using * by (simp add: dilating_def dilating_fun_def)
hence ‹tick_count r c⇩2 (Suc n) = tick_count r c⇩2 n›
also have ‹... = tick_count sub c⇩2 n⇩0›
using fn tick_count_sub[OF *] by simp
finally have ‹tick_count r c⇩2 (Suc n) = tick_count sub c⇩2 n⇩0› .
moreover have ‹tick_count sub c⇩2 n⇩0 ≤ tick_count sub c⇩2 (Suc n⇩0)›
ultimately have
‹tick_count r c⇩2 (Suc n) ≤ tick_count sub c⇩2 (Suc n⇩0)› by simp
moreover have
‹tick_count sub c⇩2 (Suc n⇩0) ≤ tick_count sub c⇩1 n⇩0› using 1 by simp
ultimately have ‹tick_count r c⇩2 (Suc n) ≤ tick_count sub c⇩1 n⇩0› by simp
thus ?thesis using tick_count_sub[OF *] fn by simp
qed
next
case False ― ‹n is not in the image of f›
from greatest_prev_image[OF * this] obtain n⇩p  where
np_prop:‹f n⇩p < n ∧ (∀k. f n⇩p < k ∧ k ≤ n ⟶ (∄k⇩0. f k⇩0 = k))› by blast
from tick_count_latest[OF * this] have
‹tick_count r c⇩1 n = tick_count r c⇩1 (f n⇩p)› .
hence a:‹tick_count r c⇩1 n = tick_count sub c⇩1 n⇩p›
using tick_count_sub[OF *] by simp
have b: ‹tick_count sub c⇩2 (Suc n⇩p) ≤ tick_count sub c⇩1 n⇩p› using 1 by simp
show ?thesis
proof (cases ‹∃sn⇩0. f sn⇩0 = Suc n›)
case True ― ‹Suc n is in the image of f›
from this obtain sn⇩0 where fsn:‹f sn⇩0 = Suc n› by blast
from next_non_stuttering[OF * np_prop this]  have sn_prop:‹sn⇩0 = Suc n⇩p› .
with b have ‹tick_count sub c⇩2 sn⇩0 ≤ tick_count sub c⇩1 n⇩p› by simp
thus ?thesis using tick_count_sub[OF *] fsn a by auto
next
case False ― ‹Suc n is not in the image of f›
hence ‹¬hamlet ((Rep_run r) (Suc n) c⇩2)›
using * by (simp add: dilating_def dilating_fun_def)
hence ‹tick_count r c⇩2 (Suc n) = tick_count r c⇩2 n›
also have ‹... = tick_count sub c⇩2 n⇩p› using np_prop tick_count_sub[OF *]
by (simp add: tick_count_latest[OF * np_prop])
finally have ‹tick_count r c⇩2 (Suc n) = tick_count sub c⇩2 n⇩p› .
moreover have ‹tick_count sub c⇩2 n⇩p ≤ tick_count sub c⇩2 (Suc n⇩p)›
ultimately have
‹tick_count r c⇩2 (Suc n) ≤ tick_count sub c⇩2 (Suc n⇩p)› by simp
moreover have
‹tick_count sub c⇩2 (Suc n⇩p) ≤ tick_count sub c⇩1 n⇩p› using 1 by simp
ultimately have ‹tick_count r c⇩2 (Suc n) ≤ tick_count sub c⇩1 n⇩p› by simp
thus ?thesis using np_prop mono_tick_count  using a by linarith
qed
qed
} thus ?thesis ..
qed
moreover from 1 have ‹¬hamlet ((Rep_run r) 0 c⇩2)›
using * empty_dilated_prefix ticks_sub by fastforce
ultimately show ?thesis by (simp add: tick_count_is_fun strictly_precedes_alt_def2)
qed

text ‹
Time delayed relations are preserved in a dilated run.
›
theorem time_delayed_sub:
assumes ‹sub ≪ r›
and ‹sub ∈ ⟦ a time-delayed by δτ on ms implies b ⟧⇩T⇩E⇩S⇩L›
shows ‹r ∈ ⟦ a time-delayed by δτ on ms implies b ⟧⇩T⇩E⇩S⇩L›
proof -
from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast
from assms(2) have ‹∀n. hamlet ((Rep_run sub) n a)
⟶ (∀m ≥ n. first_time sub ms m (time ((Rep_run sub) n ms) + δτ)
⟶ hamlet ((Rep_run sub) m b))›
using TESL_interpretation_atomic.simps(5)[of ‹a› ‹δτ› ‹ms› ‹b›] by simp
hence **:‹∀n⇩0. hamlet ((Rep_run r) (f n⇩0) a)
⟶ (∀m⇩0 ≥ n⇩0. first_time r ms (f m⇩0) (time ((Rep_run r) (f n⇩0) ms) + δτ)
⟶ hamlet ((Rep_run r) (f m⇩0) b))  ›
using first_time_image[OF *] dilating_def * by fastforce
hence ‹∀n. hamlet ((Rep_run r) n a)
⟶ (∀m ≥ n. first_time r ms m (time ((Rep_run r) n ms) + δτ)
⟶ hamlet ((Rep_run r) m b))›
proof -
{ fix n assume assm:‹hamlet ((Rep_run r) n a)›
from ticks_image_sub[OF * assm] obtain n⇩0 where nfn0:‹n = f n⇩0› by blast
with ** assm have ft0:
‹(∀m⇩0 ≥ n⇩0. first_time r ms (f m⇩0) (time ((Rep_run r) (f n⇩0) ms) + δτ)
⟶ hamlet ((Rep_run r) (f m⇩0) b))› by blast
have ‹(∀m ≥ n. first_time r ms m (time ((Rep_run r) n ms) + δτ)
⟶ hamlet ((Rep_run r) m b)) ›
proof -
{ fix m assume hyp:‹m ≥ n›
have ‹first_time r ms m (time (Rep_run r n ms) + δτ) ⟶ hamlet (Rep_run r m b)›
proof (cases ‹∃m⇩0. f m⇩0 = m›)
case True
from this obtain m⇩0 where ‹m = f m⇩0› by blast
moreover have ‹strict_mono f› using * by (simp add: dilating_def dilating_fun_def)
ultimately show ?thesis using ft0 hyp nfn0 by (simp add: strict_mono_less_eq)
next
case False thus ?thesis
proof (cases ‹m = 0›)
case True
hence ‹m = f 0› using * by (simp add: dilating_def dilating_fun_def)
then show ?thesis using False by blast
next
case False
hence ‹∃pm. m = Suc pm› by (simp add: not0_implies_Suc)
from this obtain pm where mpm:‹m = Suc pm› by blast
hence ‹∄pm⇩0. f pm⇩0 = Suc pm› using ‹∄m⇩0. f m⇩0 = m› by simp
with *  have ‹time (Rep_run r (Suc pm) ms) = time (Rep_run r pm ms)›
using dilating_def dilating_fun_def by blast
hence ‹time (Rep_run r pm ms) = time (Rep_run r m ms)› using mpm by simp
moreover from mpm have ‹pm < m› by simp
ultimately have ‹∃m' < m. time (Rep_run r m' ms) = time (Rep_run r m ms)› by blast
hence ‹¬(first_time r ms m (time (Rep_run r n ms) + δτ))›
thus ?thesis by simp
qed
qed
} thus ?thesis by simp
qed
} thus ?thesis by simp
qed
thus ?thesis by simp
qed

text ‹Time relations are preserved through dilation of a run.›
lemma tagrel_sub':
assumes ‹sub ≪ r›
and ‹sub ∈ ⟦ time-relation ⌊c⇩1,c⇩2⌋ ∈ R ⟧⇩T⇩E⇩S⇩L›
shows ‹R (time ((Rep_run r) n c⇩1), time ((Rep_run r) n c⇩2))›
proof -
from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast
moreover from assms(2) TESL_interpretation_atomic.simps(2) have
‹sub ∈ {r. ∀n. R (time ((Rep_run r) n c⇩1), time ((Rep_run r) n c⇩2))}› by blast
hence 1:‹∀n. R (time ((Rep_run sub) n c⇩1), time ((Rep_run sub) n c⇩2))› by simp
show ?thesis
proof (induction n)
case 0
from 1 have ‹R (time ((Rep_run sub) 0 c⇩1), time ((Rep_run sub) 0 c⇩2))› by simp
moreover from * have ‹f 0 = 0› by (simp add: dilating_def dilating_fun_def)
moreover from * have ‹∀c. time ((Rep_run sub) 0 c) = time ((Rep_run r) (f 0) c)›
ultimately show ?case by simp
next
case (Suc n)
then show ?case
proof (cases ‹∄n⇩0. f n⇩0 = Suc n›)
case True
with * have ‹∀c. time (Rep_run r (Suc n) c) = time (Rep_run r n c)›
thus ?thesis using Suc.IH by simp
next
case False
from this obtain n⇩0 where n⇩0prop:‹f n⇩0 = Suc n› by blast
from 1 have ‹R (time ((Rep_run sub) n⇩0 c⇩1), time ((Rep_run sub) n⇩0 c⇩2))› by simp
moreover from n⇩0prop * have ‹time ((Rep_run sub) n⇩0 c⇩1) = time ((Rep_run r) (Suc n) c⇩1)›
moreover from n⇩0prop * have ‹time ((Rep_run sub) n⇩0 c⇩2) = time ((Rep_run r) (Suc n) c⇩2)›
ultimately show ?thesis by simp
qed
qed
qed

corollary tagrel_sub:
assumes ‹sub ≪ r›
and ‹sub ∈ ⟦ time-relation ⌊c⇩1,c⇩2⌋ ∈ R ⟧⇩T⇩E⇩S⇩L›
shows ‹r ∈ ⟦ time-relation ⌊c⇩1,c⇩2⌋ ∈ R ⟧⇩T⇩E⇩S⇩L›
using tagrel_sub'[OF assms] unfolding TESL_interpretation_atomic.simps(3) by simp

text ‹Time relations are also preserved by contraction›
lemma tagrel_sub_inv:
assumes ‹sub ≪ r›
and ‹r ∈ ⟦ time-relation ⌊c⇩1, c⇩2⌋ ∈ R ⟧⇩T⇩E⇩S⇩L›
shows ‹sub ∈ ⟦ time-relation ⌊c⇩1, c⇩2⌋ ∈ R ⟧⇩T⇩E⇩S⇩L›
proof -
from assms(1) is_subrun_def obtain f where df:‹dilating f sub r› by blast
moreover from assms(2) TESL_interpretation_atomic.simps(2) have
‹r ∈ {ρ. ∀n. R (time ((Rep_run ρ) n c⇩1), time ((Rep_run ρ) n c⇩2))}› by blast
hence ‹∀n. R (time ((Rep_run r) n c⇩1), time ((Rep_run r) n c⇩2))› by simp
hence ‹∀n. (∃n⇩0. f n⇩0 = n) ⟶ R (time ((Rep_run r) n c⇩1), time ((Rep_run r) n c⇩2))› by simp
hence ‹∀n⇩0. R (time ((Rep_run r) (f n⇩0) c⇩1), time ((Rep_run r) (f n⇩0) c⇩2))› by blast
moreover from dilating_def df have
‹∀n c. time ((Rep_run sub) n c) = time ((Rep_run r) (f n) c)› by blast
ultimately have ‹∀n⇩0. R (time ((Rep_run sub) n⇩0 c⇩1), time ((Rep_run sub) n⇩0 c⇩2))› by auto
thus ?thesis by simp
qed

text ‹
Kill relations are preserved in a dilated run.
›
theorem kill_sub:
assumes ‹sub ≪ r›
and ‹sub ∈ ⟦ c⇩1 kills c⇩2 ⟧⇩T⇩E⇩S⇩L›
shows ‹r ∈ ⟦ c⇩1 kills c⇩2 ⟧⇩T⇩E⇩S⇩L›
proof -
from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast
from assms(2) TESL_interpretation_atomic.simps(8) have
‹∀n. hamlet (Rep_run sub n c⇩1) ⟶ (∀m≥n. ¬ hamlet (Rep_run sub m c⇩2))› by simp
hence 1:‹∀n. hamlet (Rep_run r (f n) c⇩1) ⟶ (∀m≥n. ¬ hamlet (Rep_run r (f m) c⇩2))›
using ticks_sub[OF *] by simp
hence ‹∀n. hamlet (Rep_run r (f n) c⇩1) ⟶ (∀m≥ (f n). ¬ hamlet (Rep_run r m c⇩2))›
proof -
{ fix n assume ‹hamlet (Rep_run r (f n) c⇩1)›
with 1 have 2:‹∀ m ≥ n. ¬ hamlet (Rep_run r (f m) c⇩2)› by simp
have ‹∀ m≥ (f n). ¬ hamlet (Rep_run r m c⇩2)›
proof -
{ fix m assume h:‹m ≥ f n›
have ‹¬ hamlet (Rep_run r m c⇩2)›
proof (cases ‹∃m⇩0. f m⇩0 = m›)
case True
from this obtain m⇩0 where fm0:‹f m⇩0 = m› by blast
hence ‹m⇩0 ≥ n›
using * dilating_def dilating_fun_def h strict_mono_less_eq by fastforce
with 2 show ?thesis using fm0 by blast
next
case False
thus ?thesis  using ticks_image_sub'[OF *] by blast
qed
} thus ?thesis by simp
qed
} thus ?thesis by simp
qed
hence ‹∀n. hamlet (Rep_run r n c⇩1) ⟶ (∀m ≥ n. ¬ hamlet (Rep_run r m c⇩2))›
using ticks_imp_ticks_subk[OF *] by blast
thus ?thesis using TESL_interpretation_atomic.simps(8) by blast
qed

lemmas atomic_sub_lemmas = sporadic_sub tagrel_sub implies_sub implies_not_sub
time_delayed_sub weakly_precedes_sub
strictly_precedes_sub kill_sub

text ‹
We can now prove that all atomic specification formulae are preserved
by the dilation of runs.
›
lemma atomic_sub:
assumes ‹sub ≪ r›
and ‹sub ∈ ⟦ φ ⟧⇩T⇩E⇩S⇩L›
shows ‹r ∈ ⟦ φ ⟧⇩T⇩E⇩S⇩L›
using assms(2) atomic_sub_lemmas[OF assms(1)] by (cases φ, simp_all)

text ‹
Finally, any TESL specification is invariant by stuttering.
›
theorem TESL_stuttering_invariant:
assumes ‹sub ≪ r›
shows ‹sub ∈ ⟦⟦ S ⟧⟧⇩T⇩E⇩S⇩L ⟹ r ∈ ⟦⟦ S ⟧⟧⇩T⇩E⇩S⇩L›
proof (induction S)
case Nil
thus ?case by simp
next
case (Cons a s)
from Cons.prems have sa:‹sub ∈ ⟦ a ⟧⇩T⇩E⇩S⇩L› and sb:‹sub ∈ ⟦⟦ s ⟧⟧⇩T⇩E⇩S⇩L›
using TESL_interpretation_image by simp+
from Cons.IH[OF sb] have ‹r ∈ ⟦⟦ s ⟧⟧⇩T⇩E⇩S⇩L› .
moreover from atomic_sub[OF assms(1) sa] have ‹r ∈ ⟦ a ⟧⇩T⇩E⇩S⇩L› .
ultimately show ?case using  TESL_interpretation_image by simp
qed

end
```