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.› lemma sporadic_sub: 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))› by (simp add: tick_count_is_fun) 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› by (simp add: tick_count_suc) 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})› by (simp add: tick_count_suc) 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› by (simp add: tick_count_suc) 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})› by (simp add: tick_count_suc) 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) + δτ))› by (auto simp add: first_time_def) 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)› by (simp add: dilating_def) 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)› by (simp add: dilating_def dilating_fun_def) thus ?thesis using Suc.IH by simp next case False from this obtain n⇩_{0}where n⇩_{0}prop:‹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⇩_{0}prop * have ‹time ((Rep_run sub) n⇩_{0}c⇩_{1}) = time ((Rep_run r) (Suc n) c⇩_{1})› by (simp add: dilating_def) moreover from n⇩_{0}prop * have ‹time ((Rep_run sub) n⇩_{0}c⇩_{2}) = time ((Rep_run r) (Suc n) c⇩_{2})› by (simp add: dilating_def) 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