subsection‹Stuttering Lemmas› theory StutteringLemmas imports StutteringDefs begin text ‹ In this section, we prove several lemmas that will be used to show that TESL specifications are invariant by stuttering. The following one will be useful in proving properties over a sequence of stuttering instants. › lemma bounded_suc_ind: assumes ‹⋀k. k < m ⟹ P (Suc (z + k)) = P (z + k)› shows ‹k < m ⟹ P (Suc (z + k)) = P z› proof (induction k) case 0 with assms(1)[of 0] show ?case by simp next case (Suc k') with assms[of ‹Suc k'›] show ?case by force qed subsection ‹Lemmas used to prove the invariance by stuttering› text ‹Since a dilating function is strictly monotonous, it is injective.› lemma dilating_fun_injects: assumes ‹dilating_fun f r› shows ‹inj_on f A› using assms dilating_fun_def strict_mono_imp_inj_on by blast lemma dilating_injects: assumes ‹dilating f sub r› shows ‹inj_on f A› using assms dilating_def dilating_fun_injects by blast text ‹ If a clock ticks at an instant in a dilated run, that instant is the image by the dilating function of an instant of the original run. › lemma ticks_image: assumes ‹dilating_fun f r› and ‹ticks ((Rep_run r) n c)› shows ‹∃n⇩0. f n⇩0 = n› using dilating_fun_def assms by blast lemma ticks_image_sub: assumes ‹dilating f sub r› and ‹ticks ((Rep_run r) n c)› shows ‹∃n⇩0. f n⇩0 = n› using assms dilating_def ticks_image by blast lemma ticks_image_sub': assumes ‹dilating f sub r› and ‹∃c. ticks ((Rep_run r) n c)› shows ‹∃n⇩0. f n⇩0 = n› using ticks_image_sub[OF assms(1)] assms(2) by blast text ‹ The image of the ticks in an interval by a dilating function is the interval bounded by the image of the bounds of the original interval. This is proven for all 4 kinds of intervals: ▩‹]m, n[›, ▩‹[m, n[›, ▩‹]m, n]› and ▩‹[m, n]›. › lemma dilating_fun_image_strict: assumes ‹dilating_fun f r› shows ‹{k. f m < k ∧ k < f n ∧ ticks ((Rep_run r) k c)} = image f {k. m < k ∧ k < n ∧ ticks ((Rep_run r) (f k) c)}› (is ‹?IMG = image f ?SET›) proof { fix k assume h:‹k ∈ ?IMG› from h obtain k⇩0 where k0prop:‹f k⇩0 = k ∧ ticks ((Rep_run r) (f k⇩0) c)› using ticks_image[OF assms] by blast with h have ‹k ∈ image f ?SET› using assms dilating_fun_def strict_mono_less by blast } thus ‹?IMG ⊆ image f ?SET› .. next { fix k assume h:‹k ∈ image f ?SET› from h obtain k⇩0 where k0prop:‹k = f k⇩0 ∧ k⇩0 ∈ ?SET› by blast hence ‹k ∈ ?IMG› using assms by (simp add: dilating_fun_def strict_mono_less) } thus ‹image f ?SET ⊆ ?IMG› .. qed lemma dilating_fun_image_left: assumes ‹dilating_fun f r› shows ‹{k. f m ≤ k ∧ k < f n ∧ ticks ((Rep_run r) k c)} = image f {k. m ≤ k ∧ k < n ∧ ticks ((Rep_run r) (f k) c)}› (is ‹?IMG = image f ?SET›) proof { fix k assume h:‹k ∈ ?IMG› from h obtain k⇩0 where k0prop:‹f k⇩0 = k ∧ ticks ((Rep_run r) (f k⇩0) c)› using ticks_image[OF assms] by blast with h have ‹k ∈ image f ?SET› using assms dilating_fun_def strict_mono_less strict_mono_less_eq by fastforce } thus ‹?IMG ⊆ image f ?SET› .. next { fix k assume h:‹k ∈ image f ?SET› from h obtain k⇩0 where k0prop:‹k = f k⇩0 ∧ k⇩0 ∈ ?SET› by blast hence ‹k ∈ ?IMG› using assms dilating_fun_def strict_mono_less strict_mono_less_eq by fastforce } thus ‹image f ?SET ⊆ ?IMG› .. qed lemma dilating_fun_image_right: assumes ‹dilating_fun f r› shows ‹{k. f m < k ∧ k ≤ f n ∧ ticks ((Rep_run r) k c)} = image f {k. m < k ∧ k ≤ n ∧ ticks ((Rep_run r) (f k) c)}› (is ‹?IMG = image f ?SET›) proof { fix k assume h:‹k ∈ ?IMG› from h obtain k⇩0 where k0prop:‹f k⇩0 = k ∧ ticks ((Rep_run r) (f k⇩0) c)› using ticks_image[OF assms] by blast with h have ‹k ∈ image f ?SET› using assms dilating_fun_def strict_mono_less strict_mono_less_eq by fastforce } thus ‹?IMG ⊆ image f ?SET› .. next { fix k assume h:‹k ∈ image f ?SET› from h obtain k⇩0 where k0prop:‹k = f k⇩0 ∧ k⇩0 ∈ ?SET› by blast hence ‹k ∈ ?IMG› using assms dilating_fun_def strict_mono_less strict_mono_less_eq by fastforce } thus ‹image f ?SET ⊆ ?IMG› .. qed lemma dilating_fun_image: assumes ‹dilating_fun f r› shows ‹{k. f m ≤ k ∧ k ≤ f n ∧ ticks ((Rep_run r) k c)} = image f {k. m ≤ k ∧ k ≤ n ∧ ticks ((Rep_run r) (f k) c)}› (is ‹?IMG = image f ?SET›) proof { fix k assume h:‹k ∈ ?IMG› from h obtain k⇩0 where k0prop:‹f k⇩0 = k ∧ ticks ((Rep_run r) (f k⇩0) c)› using ticks_image[OF assms] by blast with h have ‹k ∈ image f ?SET› using assms dilating_fun_def strict_mono_less_eq by blast } thus ‹?IMG ⊆ image f ?SET› .. next { fix k assume h:‹k ∈ image f ?SET› from h obtain k⇩0 where k0prop:‹k = f k⇩0 ∧ k⇩0 ∈ ?SET› by blast hence ‹k ∈ ?IMG› using assms by (simp add: dilating_fun_def strict_mono_less_eq) } thus ‹image f ?SET ⊆ ?IMG› .. qed text ‹ On any clock, the number of ticks in an interval is preserved by a dilating function. › lemma ticks_as_often_strict: assumes ‹dilating_fun f r› shows ‹card {p. n < p ∧ p < m ∧ ticks ((Rep_run r) (f p) c)} = card {p. f n < p ∧ p < f m ∧ ticks ((Rep_run r) p c)}› (is ‹card ?SET = card ?IMG›) proof - from dilating_fun_injects[OF assms] have ‹inj_on f ?SET› . moreover have ‹finite ?SET› by simp from inj_on_iff_eq_card[OF this] calculation have ‹card (image f ?SET) = card ?SET› by blast moreover from dilating_fun_image_strict[OF assms] have ‹?IMG = image f ?SET› . ultimately show ?thesis by auto qed lemma ticks_as_often_left: assumes ‹dilating_fun f r› shows ‹card {p. n ≤ p ∧ p < m ∧ ticks ((Rep_run r) (f p) c)} = card {p. f n ≤ p ∧ p < f m ∧ ticks ((Rep_run r) p c)}› (is ‹card ?SET = card ?IMG›) proof - from dilating_fun_injects[OF assms] have ‹inj_on f ?SET› . moreover have ‹finite ?SET› by simp from inj_on_iff_eq_card[OF this] calculation have ‹card (image f ?SET) = card ?SET› by blast moreover from dilating_fun_image_left[OF assms] have ‹?IMG = image f ?SET› . ultimately show ?thesis by auto qed lemma ticks_as_often_right: assumes ‹dilating_fun f r› shows ‹card {p. n < p ∧ p ≤ m ∧ ticks ((Rep_run r) (f p) c)} = card {p. f n < p ∧ p ≤ f m ∧ ticks ((Rep_run r) p c)}› (is ‹card ?SET = card ?IMG›) proof - from dilating_fun_injects[OF assms] have ‹inj_on f ?SET› . moreover have ‹finite ?SET› by simp from inj_on_iff_eq_card[OF this] calculation have ‹card (image f ?SET) = card ?SET› by blast moreover from dilating_fun_image_right[OF assms] have ‹?IMG = image f ?SET› . ultimately show ?thesis by auto qed lemma ticks_as_often: assumes ‹dilating_fun f r› shows ‹card {p. n ≤ p ∧ p ≤ m ∧ ticks ((Rep_run r) (f p) c)} = card {p. f n ≤ p ∧ p ≤ f m ∧ ticks ((Rep_run r) p c)}› (is ‹card ?SET = card ?IMG›) proof - from dilating_fun_injects[OF assms] have ‹inj_on f ?SET› . moreover have ‹finite ?SET› by simp from inj_on_iff_eq_card[OF this] calculation have ‹card (image f ?SET) = card ?SET› by blast moreover from dilating_fun_image[OF assms] have ‹?IMG = image f ?SET› . ultimately show ?thesis by auto qed text ‹The date of an event is preserved by dilation.› lemma ticks_tag_image: assumes ‹dilating f sub r› and ‹∃c. ticks ((Rep_run r) k c)› and ‹time ((Rep_run r) k c) = τ› shows ‹∃k⇩0. f k⇩0 = k ∧ time ((Rep_run sub) k⇩0 c) = τ› proof - from ticks_image_sub'[OF assms(1,2)] have ‹∃k⇩0. f k⇩0 = k› . from this obtain k⇩0 where ‹f k⇩0 = k› by blast moreover with assms(1,3) have ‹time ((Rep_run sub) k⇩0 c) = τ› by (simp add: dilating_def) ultimately show ?thesis by blast qed text ‹TESL operators are invariant by dilation.› lemma ticks_sub: assumes ‹dilating f sub r› shows ‹ticks ((Rep_run sub) n a) = ticks ((Rep_run r) (f n) a)› using assms by (simp add: dilating_def) lemma no_tick_sub: assumes ‹dilating f sub r› shows ‹(∄n⇩0. f n⇩0 = n) ⟶ ¬ticks ((Rep_run r) n a)› using assms dilating_def dilating_fun_def by blast text ‹Lifting a total function to a partial function on an option domain.› definition opt_lift::‹('a ⇒ 'a) ⇒ ('a option ⇒ 'a option)› where ‹opt_lift f ≡ λx. case x of None ⇒ None | Some y ⇒ Some (f y)› text ‹ The set of instants when a clock ticks in a dilated run is the image by the dilation function of the set of instants when it ticks in the subrun. › lemma tick_set_sub: assumes ‹dilating f sub r› shows ‹{k. ticks ((Rep_run r) k c)} = image f {k. ticks ((Rep_run sub) k c)}› (is ‹?R = image f ?S›) proof { fix k assume h:‹k ∈ ?R› with no_tick_sub[OF assms] have ‹∃k⇩0. f k⇩0 = k› by blast from this obtain k⇩0 where k0prop:‹f k⇩0 = k› by blast with ticks_sub[OF assms] h have ‹ticks ((Rep_run sub) k⇩0 c)› by blast with k0prop have ‹k ∈ image f ?S› by blast } thus ‹?R ⊆ image f ?S› by blast next { fix k assume h:‹k ∈ image f ?S› from this obtain k⇩0 where ‹f k⇩0 = k ∧ ticks ((Rep_run sub) k⇩0 c)› by blast with assms have ‹k ∈ ?R› using ticks_sub by blast } thus ‹image f ?S ⊆ ?R› by blast qed text ‹ Strictly monotonous functions preserve the least element. › lemma Least_strict_mono: assumes ‹strict_mono f› and ‹∃x ∈ S. ∀y ∈ S. x ≤ y› shows ‹(LEAST y. y ∈ f ` S) = f (LEAST x. x ∈ S)› using Least_mono[OF strict_mono_mono, OF assms] . text ‹ A non empty set of @{typ nat}s has a least element. › lemma Least_nat_ex: ‹(n::nat) ∈ S ⟹ ∃x ∈ S. (∀y ∈ S. x ≤ y)› by (induction n rule: nat_less_induct, insert not_le_imp_less, blast) text ‹ The first instant when a clock ticks in a dilated run is the image by the dilation function of the first instant when it ticks in the subrun. › lemma Least_sub: assumes ‹dilating f sub r› and ‹∃k::nat. ticks ((Rep_run sub) k c)› shows ‹(LEAST k. k ∈ {t. ticks ((Rep_run r) t c)}) = f (LEAST k. k ∈ {t. ticks ((Rep_run sub) t c)})› (is ‹(LEAST k. k ∈ ?R) = f (LEAST k. k ∈ ?S)›) proof - from assms(2) have ‹∃x. x ∈ ?S› by simp hence least:‹∃x ∈ ?S. ∀y ∈ ?S. x ≤ y› using Least_nat_ex .. from assms(1) have ‹strict_mono f› by (simp add: dilating_def dilating_fun_def) from Least_strict_mono[OF this least] have ‹(LEAST y. y ∈ f ` ?S) = f (LEAST x. x ∈ ?S)› . with tick_set_sub[OF assms(1), of ‹c›] show ?thesis by auto qed text ‹ If a clock ticks in a run, it ticks in the subrun. › lemma ticks_imp_ticks_sub: assumes ‹dilating f sub r› and ‹∃k. ticks ((Rep_run r) k c)› shows ‹∃k⇩0. ticks ((Rep_run sub) k⇩0 c)› proof - from assms(2) obtain k where ‹ticks ((Rep_run r) k c)› by blast with ticks_image_sub[OF assms(1)] ticks_sub[OF assms(1)] show ?thesis by blast qed text ‹ Stronger version: it ticks in the subrun and we know when. › lemma ticks_imp_ticks_subk: assumes ‹dilating f sub r› and ‹ticks ((Rep_run r) k c)› shows ‹∃k⇩0. f k⇩0 = k ∧ ticks ((Rep_run sub) k⇩0 c)› proof - from no_tick_sub[OF assms(1)] assms(2) have ‹∃k⇩0. f k⇩0 = k› by blast from this obtain k⇩0 where ‹f k⇩0 = k› by blast moreover with ticks_sub[OF assms(1)] assms(2) have ‹ticks ((Rep_run sub) k⇩0 c)› by blast ultimately show ?thesis by blast qed text ‹ A dilating function preserves the tick count on an interval for any clock. › lemma dilated_ticks_strict: assumes ‹dilating f sub r› shows ‹{i. f m < i ∧ i < f n ∧ ticks ((Rep_run r) i c)} = image f {i. m < i ∧ i < n ∧ ticks ((Rep_run sub) i c)}› (is ‹?RUN = image f ?SUB›) proof { fix i assume h:‹i ∈ ?SUB› hence ‹m < i ∧ i < n› by simp hence ‹f m < f i ∧ f i < (f n)› using assms by (simp add: dilating_def dilating_fun_def strict_monoD strict_mono_less_eq) moreover from h have ‹ticks ((Rep_run sub) i c)› by simp hence ‹ticks ((Rep_run r) (f i) c)› using ticks_sub[OF assms] by blast ultimately have ‹f i ∈ ?RUN› by simp } thus ‹image f ?SUB ⊆ ?RUN› by blast next { fix i assume h:‹i ∈ ?RUN› hence ‹ticks ((Rep_run r) i c)› by simp from ticks_imp_ticks_subk[OF assms this] obtain i⇩0 where i0prop:‹f i⇩0 = i ∧ ticks ((Rep_run sub) i⇩0 c)› by blast with h have ‹f m < f i⇩0 ∧ f i⇩0 < f n› by simp moreover have ‹strict_mono f› using assms dilating_def dilating_fun_def by blast ultimately have ‹m < i⇩0 ∧ i⇩0 < n› using strict_mono_less strict_mono_less_eq by blast with i0prop have ‹∃i⇩0. f i⇩0 = i ∧ i⇩0 ∈ ?SUB› by blast } thus ‹?RUN ⊆ image f ?SUB› by blast qed lemma dilated_ticks_left: assumes ‹dilating f sub r› shows ‹{i. f m ≤ i ∧ i < f n ∧ ticks ((Rep_run r) i c)} = image f {i. m ≤ i ∧ i < n ∧ ticks ((Rep_run sub) i c)}› (is ‹?RUN = image f ?SUB›) proof { fix i assume h:‹i ∈ ?SUB› hence ‹m ≤ i ∧ i < n› by simp hence ‹f m ≤ f i ∧ f i < (f n)› using assms by (simp add: dilating_def dilating_fun_def strict_monoD strict_mono_less_eq) moreover from h have ‹ticks ((Rep_run sub) i c)› by simp hence ‹ticks ((Rep_run r) (f i) c)› using ticks_sub[OF assms] by blast ultimately have ‹f i ∈ ?RUN› by simp } thus ‹image f ?SUB ⊆ ?RUN› by blast next { fix i assume h:‹i ∈ ?RUN› hence ‹ticks ((Rep_run r) i c)› by simp from ticks_imp_ticks_subk[OF assms this] obtain i⇩0 where i0prop:‹f i⇩0 = i ∧ ticks ((Rep_run sub) i⇩0 c)› by blast with h have ‹f m ≤ f i⇩0 ∧ f i⇩0 < f n› by simp moreover have ‹strict_mono f› using assms dilating_def dilating_fun_def by blast ultimately have ‹m ≤ i⇩0 ∧ i⇩0 < n› using strict_mono_less strict_mono_less_eq by blast with i0prop have ‹∃i⇩0. f i⇩0 = i ∧ i⇩0 ∈ ?SUB› by blast } thus ‹?RUN ⊆ image f ?SUB› by blast qed lemma dilated_ticks_right: assumes ‹dilating f sub r› shows ‹{i. f m < i ∧ i ≤ f n ∧ ticks ((Rep_run r) i c)} = image f {i. m < i ∧ i ≤ n ∧ ticks ((Rep_run sub) i c)}› (is ‹?RUN = image f ?SUB›) proof { fix i assume h:‹i ∈ ?SUB› hence ‹m < i ∧ i ≤ n› by simp hence ‹f m < f i ∧ f i ≤ (f n)› using assms by (simp add: dilating_def dilating_fun_def strict_monoD strict_mono_less_eq) moreover from h have ‹ticks ((Rep_run sub) i c)› by simp hence ‹ticks ((Rep_run r) (f i) c)› using ticks_sub[OF assms] by blast ultimately have ‹f i ∈ ?RUN› by simp } thus ‹image f ?SUB ⊆ ?RUN› by blast next { fix i assume h:‹i ∈ ?RUN› hence ‹ticks ((Rep_run r) i c)› by simp from ticks_imp_ticks_subk[OF assms this] obtain i⇩0 where i0prop:‹f i⇩0 = i ∧ ticks ((Rep_run sub) i⇩0 c)› by blast with h have ‹f m < f i⇩0 ∧ f i⇩0 ≤ f n› by simp moreover have ‹strict_mono f› using assms dilating_def dilating_fun_def by blast ultimately have ‹m < i⇩0 ∧ i⇩0 ≤ n› using strict_mono_less strict_mono_less_eq by blast with i0prop have ‹∃i⇩0. f i⇩0 = i ∧ i⇩0 ∈ ?SUB› by blast } thus ‹?RUN ⊆ image f ?SUB› by blast qed lemma dilated_ticks: assumes ‹dilating f sub r› shows ‹{i. f m ≤ i ∧ i ≤ f n ∧ ticks ((Rep_run r) i c)} = image f {i. m ≤ i ∧ i ≤ n ∧ ticks ((Rep_run sub) i c)}› (is ‹?RUN = image f ?SUB›) proof { fix i assume h:‹i ∈ ?SUB› hence ‹m ≤ i ∧ i ≤ n› by simp hence ‹f m ≤ f i ∧ f i ≤ (f n)› using assms by (simp add: dilating_def dilating_fun_def strict_mono_less_eq) moreover from h have ‹ticks ((Rep_run sub) i c)› by simp hence ‹ticks ((Rep_run r) (f i) c)› using ticks_sub[OF assms] by blast ultimately have ‹f i ∈?RUN› by simp } thus ‹image f ?SUB ⊆ ?RUN› by blast next { fix i assume h:‹i ∈ ?RUN› hence ‹ticks ((Rep_run r) i c)› by simp from ticks_imp_ticks_subk[OF assms this] obtain i⇩0 where i0prop:‹f i⇩0 = i ∧ ticks ((Rep_run sub) i⇩0 c)› by blast with h have ‹f m ≤ f i⇩0 ∧ f i⇩0 ≤ f n› by simp moreover have ‹strict_mono f› using assms dilating_def dilating_fun_def by blast ultimately have ‹m ≤ i⇩0 ∧ i⇩0 ≤ n› using strict_mono_less_eq by blast with i0prop have ‹∃i⇩0. f i⇩0 = i ∧ i⇩0 ∈ ?SUB› by blast } thus ‹?RUN ⊆ image f ?SUB› by blast qed text ‹ No tick can occur in a dilated run before the image of 0 by the dilation function. › lemma empty_dilated_prefix: assumes ‹dilating f sub r› and ‹n < f 0› shows ‹¬ ticks ((Rep_run r) n c)› proof - from assms have False by (simp add: dilating_def dilating_fun_def) thus ?thesis .. qed corollary empty_dilated_prefix': assumes ‹dilating f sub r› shows ‹{i. f 0 ≤ i ∧ i ≤ f n ∧ ticks ((Rep_run r) i c)} = {i. i ≤ f n ∧ ticks ((Rep_run r) i c)}› proof - from assms have ‹strict_mono f› by (simp add: dilating_def dilating_fun_def) hence ‹f 0 ≤ f n› unfolding strict_mono_def by (simp add: less_mono_imp_le_mono) hence ‹∀i. i ≤ f n = (i < f 0) ∨ (f 0 ≤ i ∧ i ≤ f n)› by auto hence ‹{i. i ≤ f n ∧ ticks ((Rep_run r) i c)} = {i. i < f 0 ∧ ticks ((Rep_run r) i c)} ∪ {i. f 0 ≤ i ∧ i ≤ f n ∧ ticks ((Rep_run r) i c)}› by auto also have ‹... = {i. f 0 ≤ i ∧ i ≤ f n ∧ ticks ((Rep_run r) i c)}› using empty_dilated_prefix[OF assms] by blast finally show ?thesis by simp qed corollary dilated_prefix: assumes ‹dilating f sub r› shows ‹{i. i ≤ f n ∧ ticks ((Rep_run r) i c)} = image f {i. i ≤ n ∧ ticks ((Rep_run sub) i c)}› proof - have ‹{i. 0 ≤ i ∧ i ≤ f n ∧ ticks ((Rep_run r) i c)} = image f {i. 0 ≤ i ∧ i ≤ n ∧ ticks ((Rep_run sub) i c)}› using dilated_ticks[OF assms] empty_dilated_prefix'[OF assms] by blast thus ?thesis by simp qed corollary dilated_strict_prefix: assumes ‹dilating f sub r› shows ‹{i. i < f n ∧ ticks ((Rep_run r) i c)} = image f {i. i < n ∧ ticks ((Rep_run sub) i c)}› proof - from assms have dil:‹dilating_fun f r› unfolding dilating_def by simp from dil have f0:‹f 0 = 0› using dilating_fun_def by blast from dilating_fun_image_left[OF dil, of ‹0› ‹n› ‹c›] have ‹{i. f 0 ≤ i ∧ i < f n ∧ ticks ((Rep_run r) i c)} = image f {i. 0 ≤ i ∧ i < n ∧ ticks ((Rep_run r) (f i) c)}› . hence ‹{i. i < f n ∧ ticks ((Rep_run r) i c)} = image f {i. i < n ∧ ticks ((Rep_run r) (f i) c)}› using f0 by simp also have ‹... = image f {i. i < n ∧ ticks ((Rep_run sub) i c)}› using assms dilating_def by blast finally show ?thesis by simp qed text‹A singleton of @{typ nat} can be defined with a weaker property.› lemma nat_sing_prop: ‹{i::nat. i = k ∧ P(i)} = {i::nat. i = k ∧ P(k)}› by auto text ‹ The set definition and the function definition of @{const tick_count} are equivalent. › lemma tick_count_is_fun[code]:‹tick_count r c n = run_tick_count r c n› proof (induction n) case 0 have ‹tick_count r c 0 = card {i. i ≤ 0 ∧ ticks ((Rep_run r) i c)}› by (simp add: tick_count_def) also have ‹... = card {i::nat. i = 0 ∧ ticks ((Rep_run r) 0 c)}› using le_zero_eq nat_sing_prop[of ‹0› ‹λi. ticks ((Rep_run r) i c)›] by simp also have ‹... = (if ticks ((Rep_run r) 0 c) then 1 else 0)› by simp also have ‹... = run_tick_count r c 0› by simp finally show ?case . next case (Suc k) show ?case proof (cases ‹ticks ((Rep_run r) (Suc k) c)›) case True hence ‹{i. i ≤ Suc k ∧ ticks ((Rep_run r) i c)} = insert (Suc k) {i. i ≤ k ∧ ticks ((Rep_run r) i c)}› by auto hence ‹tick_count r c (Suc k) = Suc (tick_count r c k)› by (simp add: tick_count_def) with Suc.IH have ‹tick_count r c (Suc k) = Suc (run_tick_count r c k)› by simp thus ?thesis by (simp add: True) next case False hence ‹{i. i ≤ Suc k ∧ ticks ((Rep_run r) i c)} = {i. i ≤ k ∧ ticks ((Rep_run r) i c)}› using le_Suc_eq by auto hence ‹tick_count r c (Suc k) = tick_count r c k› by (simp add: tick_count_def) thus ?thesis using Suc.IH by (simp add: False) qed qed text ‹ To show that the set definition and the function definition of @{const tick_count_strict} are equivalent, we first show that the ∗‹strictness› of @{const tick_count_strict} can be softened using @{const Suc}. › lemma tick_count_strict_suc:‹tick_count_strict r c (Suc n) = tick_count r c n› unfolding tick_count_def tick_count_strict_def using less_Suc_eq_le by auto lemma tick_count_strict_is_fun[code]: ‹tick_count_strict r c n = run_tick_count_strictly r c n› proof (cases ‹n = 0›) case True hence ‹tick_count_strict r c n = 0› unfolding tick_count_strict_def by simp also have ‹... = run_tick_count_strictly r c 0› using run_tick_count_strictly.simps(1)[symmetric] . finally show ?thesis using True by simp next case False from not0_implies_Suc[OF this] obtain m where *:‹n = Suc m› by blast hence ‹tick_count_strict r c n = tick_count r c m› using tick_count_strict_suc by simp also have ‹... = run_tick_count r c m› using tick_count_is_fun[of ‹r› ‹c› ‹m›] . also have ‹... = run_tick_count_strictly r c (Suc m)› using run_tick_count_strictly.simps(2)[symmetric] . finally show ?thesis using * by simp qed text ‹ This leads to an alternate definition of the strict precedence relation. › lemma strictly_precedes_alt_def1: ‹{ ρ. ∀n::nat. (run_tick_count ρ K⇩2 n) ≤ (run_tick_count_strictly ρ K⇩1 n) } = { ρ. ∀n::nat. (run_tick_count_strictly ρ K⇩2 (Suc n)) ≤ (run_tick_count_strictly ρ K⇩1 n) }› by auto text ‹ The strict precedence relation can even be defined using only @{const ‹run_tick_count›}: › lemma zero_gt_all: assumes ‹P (0::nat)› and ‹⋀n. n > 0 ⟹ P n› shows ‹P n› using assms neq0_conv by blast lemma strictly_precedes_alt_def2: ‹{ ρ. ∀n::nat. (run_tick_count ρ K⇩2 n) ≤ (run_tick_count_strictly ρ K⇩1 n) } = { ρ. (¬ticks ((Rep_run ρ) 0 K⇩2)) ∧ (∀n::nat. (run_tick_count ρ K⇩2 (Suc n)) ≤ (run_tick_count ρ K⇩1 n)) }› (is ‹?P = ?P'›) proof { fix r::‹'a run› assume ‹r ∈ ?P› hence ‹∀n::nat. (run_tick_count r K⇩2 n) ≤ (run_tick_count_strictly r K⇩1 n)› by simp hence 1:‹∀n::nat. (tick_count r K⇩2 n) ≤ (tick_count_strict r K⇩1 n)› using tick_count_is_fun[symmetric, of r] tick_count_strict_is_fun[symmetric, of r] by simp hence ‹∀n::nat. (tick_count_strict r K⇩2 (Suc n)) ≤ (tick_count_strict r K⇩1 n)› using tick_count_strict_suc[symmetric, of ‹r› ‹K⇩2›] by simp hence ‹∀n::nat. (tick_count_strict r K⇩2 (Suc (Suc n))) ≤ (tick_count_strict r K⇩1 (Suc n))› by simp hence ‹∀n::nat. (tick_count r K⇩2 (Suc n)) ≤ (tick_count r K⇩1 n)› using tick_count_strict_suc[symmetric, of ‹r›] by simp hence *:‹∀n::nat. (run_tick_count r K⇩2 (Suc n)) ≤ (run_tick_count r K⇩1 n)› by (simp add: tick_count_is_fun) from 1 have ‹tick_count r K⇩2 0 <= tick_count_strict r K⇩1 0› by simp moreover have ‹tick_count_strict r K⇩1 0 = 0› unfolding tick_count_strict_def by simp ultimately have ‹tick_count r K⇩2 0 = 0› by simp hence ‹¬ticks ((Rep_run r) 0 K⇩2)› unfolding tick_count_def by auto with * have ‹r ∈ ?P'› by simp } thus ‹?P ⊆ ?P'› .. { fix r::‹'a run› assume h:‹r ∈ ?P'› hence ‹∀n::nat. (run_tick_count r K⇩2 (Suc n)) ≤ (run_tick_count r K⇩1 n)› by simp hence ‹∀n::nat. (tick_count r K⇩2 (Suc n)) ≤ (tick_count r K⇩1 n)› by (simp add: tick_count_is_fun) hence ‹∀n::nat. (tick_count r K⇩2 (Suc n)) ≤ (tick_count_strict r K⇩1 (Suc n))› using tick_count_strict_suc[symmetric, of ‹r› ‹K⇩1›] by simp hence *:‹∀n. n > 0 ⟶ (tick_count r K⇩2 n) ≤ (tick_count_strict r K⇩1 n)› using gr0_implies_Suc by blast have ‹tick_count_strict r K⇩1 0 = 0› unfolding tick_count_strict_def by simp moreover from h have ‹¬ticks ((Rep_run r) 0 K⇩2)› by simp hence ‹tick_count r K⇩2 0 = 0› unfolding tick_count_def by auto ultimately have ‹tick_count r K⇩2 0 ≤ tick_count_strict r K⇩1 0› by simp from zero_gt_all[of ‹λn. tick_count r K⇩2 n ≤ tick_count_strict r K⇩1 n›, OF this ] * have ‹∀n. (tick_count r K⇩2 n) ≤ (tick_count_strict r K⇩1 n)› by simp hence ‹∀n. (run_tick_count r K⇩2 n) ≤ (run_tick_count_strictly r K⇩1 n)› by (simp add: tick_count_is_fun tick_count_strict_is_fun) hence ‹r ∈ ?P› .. } thus ‹?P' ⊆ ?P› .. qed text ‹ Some properties of @{const ‹run_tick_count›}, @{const ‹tick_count›} and @{const ‹Suc›}: › lemma run_tick_count_suc: ‹run_tick_count r c (Suc n) = (if ticks ((Rep_run r) (Suc n) c) then Suc (run_tick_count r c n) else run_tick_count r c n)› by simp corollary tick_count_suc: ‹tick_count r c (Suc n) = (if ticks ((Rep_run r) (Suc n) c) then Suc (tick_count r c n) else tick_count r c n)› by (simp add: tick_count_is_fun) text ‹ Some generic properties on the cardinal of sets of nat that we will need later. › lemma card_suc: ‹card {i. i ≤ (Suc n) ∧ P i} = card {i. i ≤ n ∧ P i} + card {i. i = (Suc n) ∧ P i}› proof - have ‹{i. i ≤ n ∧ P i} ∩ {i. i = (Suc n) ∧ P i} = {}› by auto moreover have ‹{i. i ≤ n ∧ P i} ∪ {i. i = (Suc n) ∧ P i} = {i. i ≤ (Suc n) ∧ P i}› by auto moreover have ‹finite {i. i ≤ n ∧ P i}› by simp moreover have ‹finite {i. i = (Suc n) ∧ P i}› by simp ultimately show ?thesis using card_Un_disjoint[of ‹{i. i ≤ n ∧ P i}› ‹{i. i = Suc n ∧ P i}›] by simp qed lemma card_le_leq: assumes ‹m < n› shows ‹card {i::nat. m < i ∧ i ≤ n ∧ P i} = card {i. m < i ∧ i < n ∧ P i} + card {i. i = n ∧ P i}› proof - have ‹{i::nat. m < i ∧ i < n ∧ P i} ∩ {i. i = n ∧ P i} = {}› by auto moreover with assms have ‹{i::nat. m < i ∧ i < n ∧ P i} ∪ {i. i = n ∧ P i} = {i. m < i ∧ i ≤ n ∧ P i}› by auto moreover have ‹finite {i. m < i ∧ i < n ∧ P i}› by simp moreover have ‹finite {i. i = n ∧ P i}› by simp ultimately show ?thesis using card_Un_disjoint[of ‹{i. m < i ∧ i < n ∧ P i}› ‹{i. i = n ∧ P i}›] by simp qed lemma card_le_leq_0: ‹card {i::nat. i ≤ n ∧ P i} = card {i. i < n ∧ P i} + card {i. i = n ∧ P i}› proof - have ‹{i::nat. i < n ∧ P i} ∩ {i. i = n ∧ P i} = {}› by auto moreover have ‹{i. i < n ∧ P i} ∪ {i. i = n ∧ P i} = {i. i ≤ n ∧ P i}› by auto moreover have ‹finite {i. i < n ∧ P i}› by simp moreover have ‹finite {i. i = n ∧ P i}› by simp ultimately show ?thesis using card_Un_disjoint[of ‹{i. i < n ∧ P i}› ‹{i. i = n ∧ P i}›] by simp qed lemma card_mnm: assumes ‹m < n› shows ‹card {i::nat. i < n ∧ P i} = card {i. i ≤ m ∧ P i} + card {i. m < i ∧ i < n ∧ P i}› proof - have 1:‹{i::nat. i ≤ m ∧ P i} ∩ {i. m < i ∧ i < n ∧ P i} = {}› by auto from assms have ‹∀i::nat. i < n = (i ≤ m) ∨ (m < i ∧ i < n)› using less_trans by auto hence 2: ‹{i::nat. i < n ∧ P i} = {i. i ≤ m ∧ P i} ∪ {i. m < i ∧ i < n ∧ P i}› by blast have 3:‹finite {i. i ≤ m ∧ P i}› by simp have 4:‹finite {i. m < i ∧ i < n ∧ P i}› by simp from card_Un_disjoint[OF 3 4 1] 2 show ?thesis by simp qed lemma card_mnm': assumes ‹m < n› shows ‹card {i::nat. i < n ∧ P i} = card {i. i < m ∧ P i} + card {i. m ≤ i ∧ i < n ∧ P i}› proof - have 1:‹{i::nat. i < m ∧ P i} ∩ {i. m ≤ i ∧ i < n ∧ P i} = {}› by auto from assms have ‹∀i::nat. i < n = (i < m) ∨ (m ≤ i ∧ i < n)› using less_trans by auto hence 2: ‹{i::nat. i < n ∧ P i} = {i. i < m ∧ P i} ∪ {i. m ≤ i ∧ i < n ∧ P i}› by blast have 3:‹finite {i. i < m ∧ P i}› by simp have 4:‹finite {i. m ≤ i ∧ i < n ∧ P i}› by simp from card_Un_disjoint[OF 3 4 1] 2 show ?thesis by simp qed lemma nat_interval_union: assumes ‹m ≤ n› shows ‹{i::nat. i ≤ n ∧ P i} = {i::nat. i ≤ m ∧ P i} ∪ {i::nat. m < i ∧ i ≤ n ∧ P i}› using assms le_cases nat_less_le by auto lemma card_sing_prop:‹card {i. i = n ∧ P i} = (if P n then 1 else 0)› proof (cases ‹P n›) case True hence ‹{i. i = n ∧ P i} = {n}› by (simp add: Collect_conv_if) with ‹P n› show ?thesis by simp next case False hence ‹{i. i = n ∧ P i} = {}› by (simp add: Collect_conv_if) with ‹¬P n› show ?thesis by simp qed lemma card_prop_mono: assumes ‹m ≤ n› shows ‹card {i::nat. i ≤ m ∧ P i} ≤ card {i. i ≤ n ∧ P i}› proof - from assms have ‹{i. i ≤ m ∧ P i} ⊆ {i. i ≤ n ∧ P i}› by auto moreover have ‹finite {i. i ≤ n ∧ P i}› by simp ultimately show ?thesis by (simp add: card_mono) qed text ‹ In a dilated run, no tick occurs strictly between two successive instants that are the images by @{term ‹f›} of instants of the original run. › lemma no_tick_before_suc: assumes ‹dilating f sub r› and ‹(f n) < k ∧ k < (f (Suc n))› shows ‹¬ticks ((Rep_run r) k c)› proof - from assms(1) have smf:‹strict_mono f› by (simp add: dilating_def dilating_fun_def) { fix k assume h:‹f n < k ∧ k < f (Suc n) ∧ ticks ((Rep_run r) k c)› hence ‹∃k⇩0. f k⇩0 = k› using assms(1) dilating_def dilating_fun_def by blast from this obtain k⇩0 where ‹f k⇩0 = k› by blast with h have ‹f n < f k⇩0 ∧ f k⇩0 < f (Suc n)› by simp hence False using smf not_less_eq strict_mono_less by blast } thus ?thesis using assms(2) by blast qed text ‹ From this, we show that the number of ticks on any clock at @{term ‹f (Suc n)›} depends only on the number of ticks on this clock at @{term ‹f n›} and whether this clock ticks at @{term ‹f (Suc n)›}. All the instants in between are stuttering instants. › lemma tick_count_fsuc: assumes ‹dilating f sub r› shows ‹tick_count r c (f (Suc n)) = tick_count r c (f n) + card {k. k = f (Suc n) ∧ ticks ((Rep_run r) k c)}› proof - have smf:‹strict_mono f› using assms dilating_def dilating_fun_def by blast moreover have ‹finite {k. k ≤ f n ∧ ticks ((Rep_run r) k c)}› by simp moreover have *:‹finite {k. f n < k ∧ k ≤ f (Suc n) ∧ ticks ((Rep_run r) k c)}› by simp ultimately have ‹{k. k ≤ f (Suc n) ∧ ticks ((Rep_run r) k c)} = {k. k ≤ f n ∧ ticks ((Rep_run r) k c)} ∪ {k. f n < k ∧ k ≤ f (Suc n) ∧ ticks ((Rep_run r) k c)}› by (simp add: nat_interval_union strict_mono_less_eq) moreover have ‹{k. k ≤ f n ∧ ticks ((Rep_run r) k c)} ∩ {k. f n < k ∧ k ≤ f (Suc n) ∧ ticks ((Rep_run r) k c)} = {}› by auto ultimately have ‹card {k. k ≤ f (Suc n) ∧ ticks (Rep_run r k c)} = card {k. k ≤ f n ∧ ticks (Rep_run r k c)} + card {k. f n < k ∧ k ≤ f (Suc n) ∧ ticks (Rep_run r k c)}› by (simp add: * card_Un_disjoint) moreover from no_tick_before_suc[OF assms] have ‹{k. f n < k ∧ k ≤ f (Suc n) ∧ ticks ((Rep_run r) k c)} = {k. k = f (Suc n) ∧ ticks ((Rep_run r) k c)}› using smf strict_mono_less by fastforce ultimately show ?thesis by (simp add: tick_count_def) qed corollary tick_count_f_suc: assumes ‹dilating f sub r› shows ‹tick_count r c (f (Suc n)) = tick_count r c (f n) + (if ticks ((Rep_run r) (f (Suc n)) c) then 1 else 0)› using tick_count_fsuc[OF assms] card_sing_prop[of ‹f (Suc n)› ‹λk. ticks ((Rep_run r) k c)›] by simp corollary tick_count_f_suc_suc: assumes ‹dilating f sub r› shows ‹tick_count r c (f (Suc n)) = (if ticks ((Rep_run r) (f (Suc n)) c) then Suc (tick_count r c (f n)) else tick_count r c (f n))› using tick_count_f_suc[OF assms] by simp lemma tick_count_f_suc_sub: assumes ‹dilating f sub r› shows ‹tick_count r c (f (Suc n)) = (if ticks ((Rep_run sub) (Suc n) c) then Suc (tick_count r c (f n)) else tick_count r c (f n))› using tick_count_f_suc_suc[OF assms] assms by (simp add: dilating_def) text ‹ The number of ticks does not progress during stuttering instants. › lemma tick_count_latest: assumes ‹dilating f sub r› and ‹f n⇩p < n ∧ (∀k. f n⇩p < k ∧ k ≤ n ⟶ (∄k⇩0. f k⇩0 = k))› shows ‹tick_count r c n = tick_count r c (f n⇩p)› proof - have union:‹{i. i ≤ n ∧ ticks ((Rep_run r) i c)} = {i. i ≤ f n⇩p ∧ ticks ((Rep_run r) i c)} ∪ {i. f n⇩p < i ∧ i ≤ n ∧ ticks ((Rep_run r) i c)}› using assms(2) by auto have partition: ‹{i. i ≤ f n⇩p ∧ ticks ((Rep_run r) i c)} ∩ {i. f n⇩p < i ∧ i ≤ n ∧ ticks ((Rep_run r) i c)} = {}› by (simp add: disjoint_iff_not_equal) from assms have ‹{i. f n⇩p < i ∧ i ≤ n ∧ ticks ((Rep_run r) i c)} = {}› using no_tick_sub by fastforce with union and partition show ?thesis by (simp add: tick_count_def) qed text ‹ We finally show that the number of ticks on any clock is preserved by dilation. › lemma tick_count_sub: assumes ‹dilating f sub r› shows ‹tick_count sub c n = tick_count r c (f n)› proof - have ‹tick_count sub c n = card {i. i ≤ n ∧ ticks ((Rep_run sub) i c)}› using tick_count_def[of ‹sub› ‹c› ‹n›] . also have ‹... = card (image f {i. i ≤ n ∧ ticks ((Rep_run sub) i c)})› using assms dilating_def dilating_injects[OF assms] by (simp add: card_image) also have ‹... = card {i. i ≤ f n ∧ ticks ((Rep_run r) i c)}› using dilated_prefix[OF assms, symmetric, of ‹n› ‹c›] by simp also have ‹... = tick_count r c (f n)› using tick_count_def[of ‹r› ‹c› ‹f n›] by simp finally show ?thesis . qed corollary run_tick_count_sub: assumes ‹dilating f sub r› shows ‹run_tick_count sub c n = run_tick_count r c (f n)› proof - have ‹run_tick_count sub c n = tick_count sub c n› using tick_count_is_fun[of ‹sub› c n, symmetric] . also from tick_count_sub[OF assms] have ‹... = tick_count r c (f n)› . also have ‹... = #⇩≤ r c (f n)› using tick_count_is_fun[of r c ‹f n›] . finally show ?thesis . qed text ‹ The number of ticks occurring strictly before the first instant is null. › lemma tick_count_strict_0: assumes ‹dilating f sub r› shows ‹tick_count_strict r c (f 0) = 0› proof - from assms have ‹f 0 = 0› by (simp add: dilating_def dilating_fun_def) thus ?thesis unfolding tick_count_strict_def by simp qed text ‹ The number of ticks strictly before an instant does not progress during stuttering instants. › lemma tick_count_strict_stable: assumes ‹dilating f sub r› assumes ‹(f n) < k ∧ k < (f (Suc n))› shows ‹tick_count_strict r c k = tick_count_strict r c (f (Suc n))› proof - from assms(1) have smf:‹strict_mono f› by (simp add: dilating_def dilating_fun_def) from assms(2) have ‹f n < k› by simp hence ‹∀i. k ≤ i ⟶ f n < i› by simp with no_tick_before_suc[OF assms(1)] have *:‹∀i. k ≤ i ∧ i < f (Suc n) ⟶ ¬ticks ((Rep_run r) i c)› by blast from tick_count_strict_def have ‹tick_count_strict r c (f (Suc n)) = card {i. i < f (Suc n) ∧ ticks ((Rep_run r) i c)}› . also have ‹... = card {i. i < k ∧ ticks ((Rep_run r) i c)} + card {i. k ≤ i ∧ i < f (Suc n) ∧ ticks ((Rep_run r) i c)}› using card_mnm' assms(2) by simp also have ‹... = card {i. i < k ∧ ticks ((Rep_run r) i c)}› using * by simp finally show ?thesis by (simp add: tick_count_strict_def) qed text ‹ Finally, the number of ticks strictly before an instant is preserved by dilation. › lemma tick_count_strict_sub: assumes ‹dilating f sub r› shows ‹tick_count_strict sub c n = tick_count_strict r c (f n)› proof - have ‹tick_count_strict sub c n = card {i. i < n ∧ ticks ((Rep_run sub) i c)}› using tick_count_strict_def[of ‹sub› ‹c› ‹n›] . also have ‹... = card (image f {i. i < n ∧ ticks ((Rep_run sub) i c)})› using assms dilating_def dilating_injects[OF assms] by (simp add: card_image) also have ‹... = card {i. i < f n ∧ ticks ((Rep_run r) i c)}› using dilated_strict_prefix[OF assms, symmetric, of ‹n› ‹c›] by simp also have ‹... = tick_count_strict r c (f n)› using tick_count_strict_def[of ‹r› ‹c› ‹f n›] by simp finally show ?thesis . qed text ‹ The tick count on any clock can only increase. › lemma mono_tick_count: ‹mono (λ k. tick_count r c k)› proof { fix x y::nat assume ‹x ≤ y› from card_prop_mono[OF this] have ‹tick_count r c x ≤ tick_count r c y› unfolding tick_count_def by simp } thus ‹⋀x y. x ≤ y ⟹ tick_count r c x ≤ tick_count r c y› . qed text ‹ In a dilated run, for any stuttering instant, there is an instant which is the image of an instant in the original run, and which is the latest one before the stuttering instant. › lemma greatest_prev_image: assumes ‹dilating f sub r› shows ‹(∄n⇩0. f n⇩0 = n) ⟹ (∃n⇩p. f n⇩p < n ∧ (∀k. f n⇩p < k ∧ k ≤ n ⟶ (∄k⇩0. f k⇩0 = k)))› proof (induction n) case 0 with assms have ‹f 0 = 0› by (simp add: dilating_def dilating_fun_def) thus ?case using "0.prems" by blast next case (Suc n) show ?case proof (cases ‹∃n⇩0. f n⇩0 = n›) case True from this obtain n⇩0 where ‹f n⇩0 = n› by blast hence ‹f n⇩0 < (Suc n) ∧ (∀k. f n⇩0 < k ∧ k ≤ (Suc n) ⟶ (∄k⇩0. f k⇩0 = k))› using Suc.prems Suc_leI le_antisym by blast thus ?thesis by blast next case False from Suc.IH[OF this] obtain n⇩p where ‹f n⇩p < n ∧ (∀k. f n⇩p < k ∧ k ≤ n ⟶ (∄k⇩0. f k⇩0 = k))› by blast hence ‹f n⇩p < Suc n ∧ (∀k. f n⇩p < k ∧ k ≤ n ⟶ (∄k⇩0. f k⇩0 = k))› by simp with Suc(2) have ‹f n⇩p < (Suc n) ∧ (∀k. f n⇩p < k ∧ k ≤ (Suc n) ⟶ (∄k⇩0. f k⇩0 = k))› using le_Suc_eq by auto thus ?thesis by blast qed qed text ‹ If a strictly monotonous function on @{typ ‹nat›} increases only by one, its argument was increased only by one. › lemma strict_mono_suc: assumes ‹strict_mono f› and ‹f sn = Suc (f n)› shows ‹sn = Suc n› proof - from assms(2) have ‹f sn > f n› by simp with strict_mono_less[OF assms(1)] have ‹sn > n› by simp moreover have ‹sn ≤ Suc n› proof - { assume ‹sn > Suc n› from this obtain i where ‹n < i ∧ i < sn› by blast hence ‹f n < f i ∧ f i < f sn› using assms(1) by (simp add: strict_mono_def) with assms(2) have False by simp } thus ?thesis using not_less by blast qed ultimately show ?thesis by (simp add: Suc_leI) qed text ‹ Two successive non stuttering instants of a dilated run are the images of two successive instants of the original run. › lemma next_non_stuttering: assumes ‹dilating f sub r› and ‹f n⇩p < n ∧ (∀k. f n⇩p < k ∧ k ≤ n ⟶ (∄k⇩0. f k⇩0 = k))› and ‹f sn⇩0 = Suc n› shows ‹sn⇩0 = Suc n⇩p› proof - from assms(1) have smf:‹strict_mono f› by (simp add: dilating_def dilating_fun_def) from assms(2) have *:‹∀k. f n⇩p < k ∧ k < Suc n ⟶ (∄k⇩0. f k⇩0 = k)› by simp from assms(2) have ‹f n⇩p < n› by simp with smf assms(3) have **:‹sn⇩0 > n⇩p› using strict_mono_less by fastforce have ‹Suc n ≤ f (Suc n⇩p)› proof - { assume h:‹Suc n > f (Suc n⇩p)› hence ‹Suc n⇩p < sn⇩0› using ** Suc_lessI assms(3) by fastforce hence ‹∃k. k > n⇩p ∧ f k < Suc n› using h by blast with * have False using smf strict_mono_less by blast } thus ?thesis using not_less by blast qed hence ‹sn⇩0 ≤ Suc n⇩p› using assms(3) smf using strict_mono_less_eq by fastforce with ** show ?thesis by simp qed text ‹ The order relation between tick counts on clocks is preserved by dilation. › lemma dil_tick_count: assumes ‹sub ≪ r› and ‹∀n. run_tick_count sub a n ≤ run_tick_count sub b n› shows ‹run_tick_count r a n ≤ run_tick_count r b n› proof - from assms(1) is_subrun_def obtain f where *:‹dilating f sub r› by blast show ?thesis proof (induction n) case 0 from assms(2) have ‹run_tick_count sub a 0 ≤ run_tick_count sub b 0› .. with run_tick_count_sub[OF *, of _ 0] have ‹run_tick_count r a (f 0) ≤ run_tick_count r b (f 0)› by simp moreover from * have ‹f 0 = 0› by (simp add:dilating_def dilating_fun_def) ultimately show ?case by simp next case (Suc n') thus ?case proof (cases ‹∃n⇩0. f n⇩0 = Suc n'›) case True from this obtain n⇩0 where fn0:‹f n⇩0 = Suc n'› by blast show ?thesis proof (cases ‹ticks ((Rep_run sub) n⇩0 a)›) case True have ‹run_tick_count r a (f n⇩0) ≤ run_tick_count r b (f n⇩0)› using assms(2) run_tick_count_sub[OF *] by simp thus ?thesis by (simp add: fn0) next case False hence ‹¬ ticks ((Rep_run r) (Suc n') a)› using * fn0 ticks_sub by fastforce thus ?thesis by (simp add: Suc.IH le_SucI) qed next case False thus ?thesis using * Suc.IH no_tick_sub by fastforce qed qed qed text ‹ Time does not progress during stuttering instants. › lemma stutter_no_time: assumes ‹dilating f sub r› and ‹⋀k. f n < k ∧ k ≤ m ⟹ (∄k⇩0. f k⇩0 = k)› and ‹m > f n› shows ‹time ((Rep_run r) m c) = time ((Rep_run r) (f n) c)› proof - from assms have ‹∀k. k < m - (f n) ⟶ (∄k⇩0. f k⇩0 = Suc ((f n) + k))› by simp hence ‹∀k. k < m - (f n) ⟶ time ((Rep_run r) (Suc ((f n) + k)) c) = time ((Rep_run r) ((f n) + k) c)› using assms(1) by (simp add: dilating_def dilating_fun_def) hence *:‹∀k. k < m - (f n) ⟶ time ((Rep_run r) (Suc ((f n) + k)) c) = time ((Rep_run r) (f n) c)› using bounded_suc_ind[of ‹m - (f n)› ‹λk. time (Rep_run r k c)› ‹f n›] by blast from assms(3) obtain m⇩0 where m0:‹Suc m⇩0 = m - (f n)› using Suc_diff_Suc by blast with * have ‹time ((Rep_run r) (Suc ((f n) + m⇩0)) c) = time ((Rep_run r) (f n) c)› by auto moreover from m0 have ‹Suc ((f n) + m⇩0) = m› by simp ultimately show ?thesis by simp qed lemma time_stuttering: assumes ‹dilating f sub r› and ‹time ((Rep_run sub) n c) = τ› and ‹⋀k. f n < k ∧ k ≤ m ⟹ (∄k⇩0. f k⇩0 = k)› and ‹m > f n› shows ‹time ((Rep_run r) m c) = τ› proof - from assms(3) have ‹time ((Rep_run r) m c) = time ((Rep_run r) (f n) c)› using stutter_no_time[OF assms(1,3,4)] by blast also from assms(1,2) have ‹time ((Rep_run r) (f n) c) = τ› by (simp add: dilating_def) finally show ?thesis . qed text ‹ The first instant at which a given date is reached on a clock is preserved by dilation. › lemma first_time_image: assumes ‹dilating f sub r› shows ‹first_time sub c n t = first_time r c (f n) t› proof assume ‹first_time sub c n t› with before_first_time[OF this] have *:‹time ((Rep_run sub) n c) = t ∧ (∀m < n. time((Rep_run sub) m c) < t)› by (simp add: first_time_def) moreover have ‹∀n c. time (Rep_run sub n c) = time (Rep_run r (f n) c)› using assms(1) by (simp add: dilating_def) ultimately have **: ‹time ((Rep_run r) (f n) c) = t ∧ (∀m < n. time((Rep_run r) (f m) c) < t)› by simp have ‹∀m < f n. time ((Rep_run r) m c) < t› proof - { fix m assume hyp:‹m < f n› have ‹time ((Rep_run r) m c) < t› proof (cases ‹∃m⇩0. f m⇩0 = m›) case True from this obtain m⇩0 where mm0:‹m = f m⇩0› by blast with hyp have m0n:‹m⇩0 < n› using assms(1) by (simp add: dilating_def dilating_fun_def strict_mono_less) hence ‹time ((Rep_run sub) m⇩0 c) < t› using * by blast thus ?thesis by (simp add: mm0 m0n **) next case False hence ‹∃m⇩p. f m⇩p < m ∧ (∀k. f m⇩p < k ∧ k ≤ m ⟶ (∄k⇩0. f k⇩0 = k))› using greatest_prev_image[OF assms] by simp from this obtain m⇩p where mp:‹f m⇩p < m ∧ (∀k. f m⇩p < k ∧ k ≤ m ⟶ (∄k⇩0. f k⇩0 = k))› by blast hence ‹time ((Rep_run r) m c) = time ((Rep_run sub) m⇩p c)› using time_stuttering[OF assms] by blast also from hyp mp have ‹f m⇩p < f n› by linarith hence ‹m⇩p < n› using assms by (simp add:dilating_def dilating_fun_def strict_mono_less) hence ‹time ((Rep_run sub) m⇩p c) < t› using * by simp finally show ?thesis by simp qed } thus ?thesis by simp qed with ** show ‹first_time r c (f n) t› by (simp add: alt_first_time_def) next assume ‹first_time r c (f n) t› hence *:‹time ((Rep_run r) (f n) c) = t ∧ (∀k < f n. time ((Rep_run r) k c) < t)› by (simp add: first_time_def before_first_time) hence ‹time ((Rep_run sub) n c) = t› using assms dilating_def by blast moreover from * have ‹(∀k < n. time ((Rep_run sub) k c) < t)› using assms dilating_def dilating_fun_def strict_monoD by fastforce ultimately show ‹first_time sub c n t› by (simp add: alt_first_time_def) qed text ‹ The first instant of a dilated run is necessarily the image of the first instant of the original run. › lemma first_dilated_instant: assumes ‹strict_mono f› and ‹f (0::nat) = (0::nat)› shows ‹Max {i. f i ≤ 0} = 0› proof - from assms(2) have ‹∀n > 0. f n > 0› using strict_monoD[OF assms(1)] by force hence ‹∀n ≠ 0. ¬(f n ≤ 0)› by simp with assms(2) have ‹{i. f i ≤ 0} = {0}› by blast thus ?thesis by simp qed text ‹ For any instant @{term ‹n›} of a dilated run, let @{term ‹n⇩0›} be the last instant before @{term ‹n›} that is the image of an original instant. All instants strictly after @{term ‹n⇩0›} and before @{term ‹n›} are stuttering instants. › lemma not_image_stut: assumes ‹dilating f sub r› and ‹n⇩0 = Max {i. f i ≤ n}› and ‹f n⇩0 < k ∧ k ≤ n› shows ‹∄k⇩0. f k⇩0 = k› proof - from assms(1) have smf:‹strict_mono f› and fxge:‹∀x. f x ≥ x› by (auto simp add: dilating_def dilating_fun_def) have finite_prefix:‹finite {i. f i ≤ n}› by (simp add: finite_less_ub fxge) from assms(1) have ‹f 0 ≤ n› by (simp add: dilating_def dilating_fun_def) hence ‹{i. f i ≤ n} ≠ {}› by blast from assms(3) fxge have ‹f n⇩0 < n› by linarith from assms(2) have ‹∀x > n⇩0. f x > n› using Max.coboundedI[OF finite_prefix] using not_le by auto with assms(3) strict_mono_less[OF smf] show ?thesis by auto qed text ‹ For any dilating function @{term ‹f›}, @{term ‹dil_inverse f›} is a contracting function. › lemma contracting_inverse: assumes ‹dilating f sub r› shows ‹contracting (dil_inverse f) r sub f› proof - from assms have smf:‹strict_mono f› and no_img_tick:‹∀k. (∄k⇩0. f k⇩0 = k) ⟶ (∀c. ¬(ticks ((Rep_run r) k c)))› and no_img_time:‹⋀n. (∄n⇩0. f n⇩0 = (Suc n)) ⟶ (∀c. time ((Rep_run r) (Suc n) c) = time ((Rep_run r) n c))› and fxge:‹∀x. f x ≥ x› and f0n:‹⋀n. f 0 ≤ n› and f0:‹f 0 = 0› by (auto simp add: dilating_def dilating_fun_def) have finite_prefix:‹⋀n. finite {i. f i ≤ n}› by (auto simp add: finite_less_ub fxge) have prefix_not_empty:‹⋀n. {i. f i ≤ n} ≠ {}› using f0n by blast have 1:‹mono (dil_inverse f)› proof - { fix x::‹nat› and y::‹nat› assume hyp:‹x ≤ y› hence inc:‹{i. f i ≤ x} ⊆ {i. f i ≤ y}› by (simp add: hyp Collect_mono le_trans) from Max_mono[OF inc prefix_not_empty finite_prefix] have ‹(dil_inverse f) x ≤ (dil_inverse f) y› unfolding dil_inverse_def . } thus ?thesis unfolding mono_def by simp qed from first_dilated_instant[OF smf f0] have 2:‹(dil_inverse f) 0 = 0› unfolding dil_inverse_def . from fxge have ‹∀n i. f i ≤ n ⟶ i ≤ n› using le_trans by blast hence 3:‹∀n. (dil_inverse f) n ≤ n› using Max_in[OF finite_prefix prefix_not_empty] unfolding dil_inverse_def by blast from 1 2 3 have *:‹contracting_fun (dil_inverse f)› by (simp add: contracting_fun_def) have ‹∀n. finite {i. f i ≤ n}› by (simp add: finite_prefix) moreover have ‹∀n. {i. f i ≤ n} ≠ {}› using prefix_not_empty by blast ultimately have 4:‹∀n. f ((dil_inverse f) n) ≤ n› unfolding dil_inverse_def using assms(1) dilating_def dilating_fun_def Max_in by blast have 5:‹∀n c k. f ((dil_inverse f) n) < k ∧ k ≤ n ⟶ ¬ ticks ((Rep_run r) k c)› using not_image_stut[OF assms] no_img_tick unfolding dil_inverse_def by blast have 6:‹(∀n c k. f ((dil_inverse f) n) ≤ k ∧ k ≤ n ⟶ time ((Rep_run r) k c) = time ((Rep_run sub) ((dil_inverse f) n) c))› proof - { fix n c k assume h:‹f ((dil_inverse f) n) ≤ k ∧ k ≤ n› let ?τ = ‹time (Rep_run sub ((dil_inverse f) n) c)› have tau:‹time (Rep_run sub ((dil_inverse f) n) c) = ?τ› .. have gn:‹(dil_inverse f) n = Max {i. f i ≤ n}› unfolding dil_inverse_def .. from time_stuttering[OF assms tau, of k] not_image_stut[OF assms gn] have ‹time ((Rep_run r) k c) = time ((Rep_run sub) ((dil_inverse f) n) c)› proof (cases ‹f ((dil_inverse f) n) = k›) case True moreover have ‹∀n c. time (Rep_run sub n c) = time (Rep_run r (f n) c)› using assms by (simp add: dilating_def) ultimately show ?thesis by simp next case False with h have ‹f (Max {i. f i ≤ n}) < k ∧ k ≤ n› by (simp add: dil_inverse_def) with time_stuttering[OF assms tau, of k] not_image_stut[OF assms gn] show ?thesis unfolding dil_inverse_def by auto qed } thus ?thesis by simp qed from * 4 5 6 show ?thesis unfolding contracting_def by simp qed text ‹ The only possible contracting function toward a dense run (a run with no empty instants) is the inverse of the dilating function as defined by @{term ‹dil_inverse›}. › lemma dense_run_dil_inverse_only: assumes ‹dilating f sub r› and ‹contracting g r sub f› and ‹dense_run sub› shows ‹g = (dil_inverse f)› proof from assms(1) have *:‹⋀n. finite {i. f i ≤ n}› using finite_less_ub by (simp add: dilating_def dilating_fun_def) from assms(1) have ‹f 0 = 0› by (simp add: dilating_def dilating_fun_def) hence ‹⋀n. 0 ∈ {i. f i ≤ n}› by simp hence **:‹⋀n. {i. f i ≤ n} ≠ {}› by blast { fix n assume h:‹g n < (dil_inverse f) n› hence ‹∃k > g n. f k ≤ n› unfolding dil_inverse_def using Max_in[OF * **] by blast from this obtain k where kprop:‹g n < k ∧ f k ≤ n› by blast with assms(3) dense_run_def obtain c where ‹ticks ((Rep_run sub) k c)› by blast hence ‹ticks ((Rep_run r) (f k) c)› using ticks_sub[OF assms(1)] by blast moreover from kprop have ‹f (g n) < f k ∧ f k ≤ n› using assms(1) by (simp add: dilating_def dilating_fun_def strict_monoD) ultimately have False using assms(2) unfolding contracting_def by blast } hence 1:‹⋀n. ¬(g n < (dil_inverse f) n)› by blast { fix n assume h:‹g n > (dil_inverse f) n› have ‹∃k ≤ g n. f k > n› proof - { assume ‹∀k ≤ g n. f k ≤ n› with h have False unfolding dil_inverse_def using Max_gr_iff[OF * **] by blast } thus ?thesis using not_less by blast qed from this obtain k where ‹k ≤ g n ∧ f k > n› by blast hence ‹f (g n) ≥ f k ∧ f k > n› using assms(1) by (simp add: dilating_def dilating_fun_def strict_mono_less_eq) hence ‹f (g n) > n› by simp with assms(2) have False unfolding contracting_def by (simp add: leD) } hence 2:‹⋀n. ¬(g n > (dil_inverse f) n)› by blast from 1 2 show ‹⋀n. g n = (dil_inverse f) n› by (simp add: not_less_iff_gr_or_eq) qed end