Theory StutteringLemmas

```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     ‹hamlet ((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     ‹hamlet ((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. hamlet ((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 ∧ hamlet ((Rep_run r) k c)}
= image f {k. m < k ∧ k < n ∧ hamlet ((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 ∧ hamlet ((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 ∧ hamlet ((Rep_run r) k c)}
= image f {k. m ≤ k ∧ k < n ∧ hamlet ((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 ∧ hamlet ((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 ∧ hamlet ((Rep_run r) k c)}
= image f {k. m < k ∧ k ≤ n ∧ hamlet ((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 ∧ hamlet ((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 ∧ hamlet ((Rep_run r) k c)}
= image f {k. m ≤ k ∧ k ≤ n ∧ hamlet ((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 ∧ hamlet ((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 ∧ hamlet ((Rep_run r) (f p) c)}
= card {p. f n < p ∧ p < f m ∧ hamlet ((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 ∧ hamlet ((Rep_run r) (f p) c)}
= card {p. f n ≤ p ∧ p < f m ∧ hamlet ((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 ∧ hamlet ((Rep_run r) (f p) c)}
= card {p. f n < p ∧ p ≤ f m ∧ hamlet ((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 ∧ hamlet ((Rep_run r) (f p) c)}
= card {p. f n ≤ p ∧ p ≤ f m ∧ hamlet ((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. hamlet ((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) = τ›
ultimately show ?thesis by blast
qed

text ‹TESL operators are invariant by dilation.›

lemma ticks_sub:
assumes ‹dilating f sub r›
shows   ‹hamlet ((Rep_run sub) n a) = hamlet ((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) ⟶ ¬hamlet ((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. hamlet ((Rep_run r) k c)} = image f {k. hamlet ((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 ‹hamlet ((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 ∧ hamlet ((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. hamlet ((Rep_run sub) k c)›
shows   ‹(LEAST k. k ∈ {t. hamlet ((Rep_run r) t c)})
= f (LEAST k. k ∈ {t. hamlet ((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. hamlet ((Rep_run r) k c)›
shows   ‹∃k⇩0. hamlet ((Rep_run sub) k⇩0 c)›
proof -
from assms(2) obtain k where ‹hamlet ((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     ‹hamlet ((Rep_run r) k c)›
shows   ‹∃k⇩0. f k⇩0 = k ∧ hamlet ((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 ‹hamlet ((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 ∧ hamlet ((Rep_run r) i c)}
= image f {i. m < i ∧ i < n ∧ hamlet ((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 ‹hamlet ((Rep_run sub) i c)› by simp
hence ‹hamlet ((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 ‹hamlet ((Rep_run r) i c)› by simp
from ticks_imp_ticks_subk[OF assms this]
obtain i⇩0 where i0prop:‹f i⇩0 = i ∧ hamlet ((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 ∧ hamlet ((Rep_run r) i c)}
= image f {i. m ≤ i ∧ i < n ∧ hamlet ((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 ‹hamlet ((Rep_run sub) i c)› by simp
hence ‹hamlet ((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 ‹hamlet ((Rep_run r) i c)› by simp
from ticks_imp_ticks_subk[OF assms this]
obtain i⇩0 where i0prop:‹f i⇩0 = i ∧ hamlet ((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 ∧ hamlet ((Rep_run r) i c)}
= image f {i. m < i ∧ i ≤ n ∧ hamlet ((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 ‹hamlet ((Rep_run sub) i c)› by simp
hence ‹hamlet ((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 ‹hamlet ((Rep_run r) i c)› by simp
from ticks_imp_ticks_subk[OF assms this]
obtain i⇩0 where i0prop:‹f i⇩0 = i ∧ hamlet ((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 ∧ hamlet ((Rep_run r) i c)}
= image f {i. m ≤ i ∧ i ≤ n ∧ hamlet ((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 ‹hamlet ((Rep_run sub) i c)› by simp
hence ‹hamlet ((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 ‹hamlet ((Rep_run r) i c)› by simp
from ticks_imp_ticks_subk[OF assms this]
obtain i⇩0 where i0prop:‹f i⇩0 = i ∧ hamlet ((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   ‹¬ hamlet ((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 ∧ hamlet ((Rep_run r) i c)}
= {i. i ≤ f n ∧ hamlet ((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 ∧ hamlet ((Rep_run r) i c)}
= {i. i < f 0 ∧ hamlet ((Rep_run r) i c)}
∪ {i. f 0 ≤ i ∧ i ≤ f n ∧ hamlet ((Rep_run r) i c)}›
by auto
also have ‹... = {i. f 0 ≤ i ∧ i ≤ f n ∧ hamlet ((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 ∧ hamlet ((Rep_run r) i c)}
= image f {i. i ≤ n ∧ hamlet ((Rep_run sub) i c)}›
proof -
have ‹{i. 0 ≤ i ∧ i ≤ f n ∧ hamlet ((Rep_run r) i c)}
= image f {i. 0 ≤ i ∧ i ≤ n ∧ hamlet ((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 ∧ hamlet ((Rep_run r) i c)}
= image f {i. i < n ∧ hamlet ((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 ∧ hamlet ((Rep_run r) i c)}
= image f {i. 0 ≤ i ∧ i < n ∧ hamlet ((Rep_run r) (f i) c)}› .
hence ‹{i. i < f n ∧ hamlet ((Rep_run r) i c)}
= image f {i. i < n ∧ hamlet ((Rep_run r) (f i) c)}›
using f0 by simp
also have ‹... = image f {i. i < n ∧ hamlet ((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 ∧ hamlet ((Rep_run r) i c)}›
also have ‹... = card {i::nat. i = 0 ∧ hamlet ((Rep_run r) 0 c)}›
using le_zero_eq nat_sing_prop[of ‹0› ‹λi. hamlet ((Rep_run r) i c)›] by simp
also have ‹... = (if hamlet ((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 ‹hamlet ((Rep_run r) (Suc k) c)›)
case True
hence ‹{i. i ≤ Suc k ∧ hamlet ((Rep_run r) i c)}
= insert (Suc k) {i. i ≤ k ∧ hamlet ((Rep_run r) i c)}› by auto
hence ‹tick_count r c (Suc k) = Suc (tick_count r c k)›
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 ∧ hamlet ((Rep_run r) i c)}
= {i. i ≤ k ∧ hamlet ((Rep_run r) i c)}›
using le_Suc_eq by auto
hence ‹tick_count r c (Suc k) = tick_count r c k›
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) }
= { ρ. (¬hamlet ((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)›
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 ‹¬hamlet ((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)›
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 ‹¬hamlet ((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)›
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 hamlet ((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 hamlet ((Rep_run r) (Suc n) c)
then Suc (tick_count r c n)
else tick_count r c n)›

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 ‹¬hamlet ((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) ∧ hamlet ((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) ∧ hamlet ((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 ∧ hamlet ((Rep_run r) k c)}› by simp
moreover have *:‹finite {k. f n < k ∧ k ≤ f (Suc n) ∧ hamlet ((Rep_run r) k c)}› by simp
ultimately have ‹{k. k ≤ f (Suc n) ∧ hamlet ((Rep_run r) k c)} =
{k. k ≤ f n ∧ hamlet ((Rep_run r) k c)}
∪ {k. f n < k ∧ k ≤ f (Suc n) ∧ hamlet ((Rep_run r) k c)}›
moreover have ‹{k. k ≤ f n ∧ hamlet ((Rep_run r) k c)}
∩ {k. f n < k ∧ k ≤ f (Suc n) ∧ hamlet ((Rep_run r) k c)} = {}›
by auto
ultimately have ‹card {k. k ≤ f (Suc n) ∧ hamlet (Rep_run r k c)} =
card {k. k ≤ f n ∧ hamlet (Rep_run r k c)}
+ card {k. f n < k ∧ k ≤ f (Suc n) ∧ hamlet (Rep_run r k c)}›
moreover from no_tick_before_suc[OF assms] have
‹{k. f n < k ∧ k ≤ f (Suc n) ∧ hamlet ((Rep_run r) k c)} =
{k. k = f (Suc n) ∧ hamlet ((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 hamlet ((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. hamlet ((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 hamlet ((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 hamlet ((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 ∧ hamlet ((Rep_run r) i c)} =
{i. i ≤ f n⇩p ∧ hamlet ((Rep_run r) i c)}
∪ {i. f n⇩p < i ∧ i ≤ n ∧ hamlet ((Rep_run r) i c)}› using assms(2) by auto
have partition: ‹{i. i ≤ f n⇩p ∧ hamlet ((Rep_run r) i c)}
∩ {i. f n⇩p < i ∧ i ≤ n ∧ hamlet ((Rep_run r) i c)} = {}›
from assms have ‹{i. f n⇩p < i ∧ i ≤ n ∧ hamlet ((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 ∧ hamlet ((Rep_run sub) i c)}›
using tick_count_def[of ‹sub› ‹c› ‹n›] .
also have ‹... = card (image f {i. i ≤ n ∧ hamlet ((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 ∧ hamlet ((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) ⟶ ¬hamlet ((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) ∧ hamlet ((Rep_run r) i c)}› .
also have
‹... = card {i. i < k ∧ hamlet ((Rep_run r) i c)}
+ card {i. k ≤ i ∧ i < f (Suc n) ∧ hamlet ((Rep_run r) i c)}›
using card_mnm' assms(2) by simp
also have ‹... = card {i. i < k ∧ hamlet ((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 ∧ hamlet ((Rep_run sub) i c)}›
using tick_count_strict_def[of ‹sub› ‹c› ‹n›] .
also have ‹... = card (image f {i. i < n ∧ hamlet ((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 ∧ hamlet ((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 ‹hamlet ((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 ‹¬ hamlet ((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)›
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
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)›
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. ¬(hamlet ((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
⟶ ¬ hamlet ((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 ‹hamlet ((Rep_run sub) k c)› by blast
hence ‹hamlet ((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
```