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) = τ›
    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   ‹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)}›
      by (simp add: tick_count_def)
    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)›
          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 ∧ 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›
          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) }
 = { ρ. (¬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)›
      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 ‹¬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)›
      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 ‹¬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)›
      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 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)›
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 ‹¬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)}›
    by (simp add: nat_interval_union strict_mono_less_eq)
  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)}›
    by (simp add: * card_Un_disjoint)
  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)} = {}›
    by (simp add: disjoint_iff_not_equal)
  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)›
      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. ¬(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