Theory Stuttering_Equivalence.StutterEquivalence

theory StutterEquivalence
imports Samplers

begin

section ‹Stuttering Equivalence›

text ‹
  Stuttering equivalence of two sequences is formally defined as the equality
  of their maximally reduced versions.
›

definition stutter_equiv  (infix "≈" 50) where
  "σ ≈ τ ≡ ♮σ = ♮τ"

text ‹
  Stuttering equivalence is an equivalence relation.
›

lemma stutter_equiv_refl: "σ ≈ σ"
  unfolding stutter_equiv_def ..

lemma stutter_equiv_sym [sym]: "σ ≈ τ ⟹ τ ≈ σ"
  unfolding stutter_equiv_def by (rule sym)

lemma stutter_equiv_trans [trans]: "ρ ≈ σ ⟹ σ ≈ τ ⟹ ρ ≈ τ"
  unfolding stutter_equiv_def by simp

text ‹
  In particular, any sequence sampled by a stuttering sampler
  is stuttering equivalent to the original one.
›
lemma sampled_stutter_equiv:
  assumes "stutter_sampler f σ"
  shows "σ ∘ f ≈ σ"
  using assms unfolding stutter_equiv_def by (rule sample_max_sample)

lemma stutter_reduced_equivalent: "♮σ ≈ σ"
  unfolding stutter_equiv_def by (rule stutter_reduced_reduced)

text ‹
  For proving stuttering equivalence of two sequences, it is enough
  to exhibit two arbitrary sampling functions that equalize the reductions
  of the sequences. This can be more convenient than computing the
  maximal stutter-reduced version of the sequences.
›

lemma stutter_equivI:
  assumes f: "stutter_sampler f σ" and g: "stutter_sampler g τ" 
      and eq: "σ ∘ f = τ ∘ g"
  shows "σ ≈ τ"
proof -
  from f have "♮σ = ♮(σ ∘ f)" by (rule sample_max_sample[THEN sym])
  also from eq have "... = ♮(τ ∘ g)" by simp
  also from g have "... = ♮τ" by (rule sample_max_sample)
  finally show ?thesis by (unfold stutter_equiv_def)
qed

text ‹
  The corresponding elimination rule is easy to prove, given that the
  maximal stuttering sampling function is a stuttering sampling function.
›

lemma stutter_equivE:
  assumes eq: "σ ≈ τ"
  and p: "⋀f g. ⟦ stutter_sampler f σ; stutter_sampler g τ; σ ∘ f = τ ∘ g ⟧ ⟹ P"
  shows "P"
proof (rule p)
  from eq show "σ ∘ (max_stutter_sampler σ) = τ ∘ (max_stutter_sampler τ)"
    by (unfold stutter_equiv_def stutter_reduced_def)
qed (rule max_stutter_sampler)+

text ‹
  Therefore we get the following alternative characterization: two
  sequences are stuttering equivalent iff there are stuttering sampling
  functions that equalize the two sequences.
›
lemma stutter_equiv_eq:
  "σ ≈ τ = (∃f g. stutter_sampler f σ ∧ stutter_sampler g τ ∧ σ ∘ f = τ ∘ g)"
  by (blast intro: stutter_equivI elim: stutter_equivE)

text ‹
  The initial elements of stutter equivalent sequences are equal.
›
lemma stutter_equiv_0:
  assumes "σ ≈ τ"
  shows "σ 0 = τ 0"
proof -
  have "σ 0 = (♮σ) 0" by (rule stutter_reduced_0[THEN sym])
  with assms[unfolded stutter_equiv_def] show ?thesis
    by (simp add: stutter_reduced_0)
qed

abbreviation suffix_notation ("_ [_..]")
where
  "suffix_notation w k ≡ suffix k w"

text ‹
  Given any stuttering sampling function ‹f› for sequence ‹σ›,
  any suffix of ‹σ› starting at index ‹f n› is stuttering
  equivalent to the suffix of the stutter-reduced version of ‹σ›
  starting at ‹n›.
›
lemma suffix_stutter_equiv:
  assumes f: "stutter_sampler f σ"
  shows "suffix (f n) σ ≈ suffix n (σ ∘ f)"
proof -
  from f have "stutter_sampler (λk. f (n+k) - f n) (σ[f n ..])"
    by (rule stutter_sampler_suffix)
  moreover
  have "stutter_sampler id ((σ ∘ f)[n ..])"
    by (rule id_stutter_sampler)
  moreover
  have "(σ[f n ..]) ∘ (λk. f (n+k) - f n) = ((σ ∘ f)[n ..]) ∘ id"
  proof (rule ext, auto)
    fix i
    from f[THEN stutter_sampler_mono, THEN strict_mono_mono]
    have "f n ≤ f (n+i)" by (rule monoD) simp
    thus "σ (f n + (f (n+i) - f n)) = σ (f (n+i))" by simp
  qed
  ultimately show ?thesis
    by (rule stutter_equivI)
qed

text ‹
  Given a stuttering sampling function ‹f› and a point ‹n›
  within the interval from ‹f k› to ‹f (k+1)›, the suffix
  starting at ‹n› is stuttering equivalent to the suffix starting
  at ‹f k›.
›
lemma stutter_equiv_within_interval:
  assumes f: "stutter_sampler f σ"
      and lo: "f k ≤ n" and hi: "n < f (Suc k)"
  shows "σ[n ..] ≈ σ[f k ..]"
proof -
  have "stutter_sampler id (σ[n ..])" by (rule id_stutter_sampler)
  moreover
  from lo have "stutter_sampler (λi. if i=0 then 0 else n + i - f k) (σ[f k ..])"
    (is "stutter_sampler ?f _")
  proof (auto simp: stutter_sampler_def strict_mono_def)
    fix i
    assume i: "i < Suc n - f k"
    from f show "σ (f k + i) = σ (f k)"
    proof (rule stutter_sampler_between)
      from i hi show "f k + i < f (Suc k)" by simp
    qed simp
  qed
  moreover
  have "(σ[n ..]) ∘ id = (σ[f k ..]) ∘ ?f"
  proof (rule ext, auto)
    from f lo hi show "σ n = σ (f k)" by (rule stutter_sampler_between)
  next
    fix i
    from lo show "σ (n+i) = σ (f k + (n + i - f k))" by simp
  qed
  ultimately show ?thesis by (rule stutter_equivI)
qed

text ‹
  Given two stuttering equivalent sequences ‹σ› and ‹τ›,
  we obtain a zig-zag relationship as follows: for any suffix ‹τ[n..]›
  there is a suffix ‹σ[m..]› such that:
  \begin{enumerate}
  \item ‹σ[m..] ≈ τ[n..]› and
  \item for every suffix ‹σ[j..]› where ‹j<m› there is a
    corresponding suffix ‹τ[k..]› for some ‹k<n›.
  \end{enumerate}
›
theorem stutter_equiv_suffixes_left:
  assumes "σ ≈ τ"
  obtains m where "σ[m..] ≈ τ[n..]" and "∀j<m. ∃k<n. σ[j..] ≈ τ[k..]"
using assms proof (rule stutter_equivE)
  fix f g
  assume f: "stutter_sampler f σ"
     and g: "stutter_sampler g τ"
     and eq: "σ ∘ f = τ ∘ g"
  from g obtain i where i: "g i ≤ n" "n < g (Suc i)"
    by (rule stutter_sampler_interval)
  with g have "τ[n..] ≈ τ[g i ..]"
    by (rule stutter_equiv_within_interval)
  also from g have "... ≈ (τ ∘ g)[i ..]"
    by (rule suffix_stutter_equiv)
  also from eq have "... = (σ ∘ f)[i ..]"
    by simp
  also from f have "... ≈ σ[f i ..]"
    by (rule suffix_stutter_equiv[THEN stutter_equiv_sym])
  finally have "σ[f i ..] ≈ τ[n ..]"
    by (rule stutter_equiv_sym)
  moreover
  {
    fix j
    assume j: "j < f i"
    from f obtain a where a: "f a ≤ j" "j < f (Suc a)"
      by (rule stutter_sampler_interval)
    from a j have "f a < f i" by simp
    with f[THEN stutter_sampler_mono] have "a < i"
      by (simp add: strict_mono_less)
    with g[THEN stutter_sampler_mono] have "g a < g i"
      by (simp add: strict_mono_less)
    with i have 1: "g a < n" by simp

    from f a have "σ[j..] ≈ σ[f a ..]"
      by (rule stutter_equiv_within_interval)
    also from f have "... ≈ (σ ∘ f)[a ..]"
      by (rule suffix_stutter_equiv)
    also from eq have "... = (τ ∘ g)[a ..]" by simp
    also from g have "... ≈ τ[g a ..]"
      by (rule suffix_stutter_equiv[THEN stutter_equiv_sym])
    finally have "σ[j ..] ≈ τ[g a ..]" .
    with 1 have "∃k<n. σ[j..] ≈ τ[k ..]" by blast
  }
  moreover
  note that
  ultimately show ?thesis by blast
qed

theorem stutter_equiv_suffixes_right:
  assumes "σ ≈ τ"
  obtains n where "σ[m..] ≈ τ[n..]" and "∀j<n. ∃k<m. σ[k..] ≈ τ[j..]"
proof -
  from assms have "τ ≈ σ" 
    by (rule stutter_equiv_sym)
  then obtain n where "τ[n..] ≈ σ[m..]" "∀j<n. ∃k<m. τ[j..] ≈ σ[k..]"
    by (rule stutter_equiv_suffixes_left)
  with that show ?thesis 
    by (blast dest: stutter_equiv_sym)
qed

text ‹
  In particular, if ‹σ› and ‹τ› are stutter equivalent then
  every element that occurs in one sequence also occurs in the other.
›
lemma stutter_equiv_element_left:
  assumes "σ ≈ τ"
  obtains m where "σ m = τ n" and "∀j<m. ∃k<n. σ j = τ k"
proof -
  from assms obtain m where "σ[m..] ≈ τ[n..]" "∀j<m. ∃k<n. σ[j..] ≈ τ[k..]"
    by (rule stutter_equiv_suffixes_left)
  with that show ?thesis
    by (force dest: stutter_equiv_0)
qed

lemma stutter_equiv_element_right:
  assumes "σ ≈ τ"
  obtains n where "σ m = τ n" and "∀j<n. ∃k<m. σ k = τ j"
proof -
  from assms obtain n where "σ[m..] ≈ τ[n..]" "∀j<n. ∃k<m. σ[k..] ≈ τ[j..]"
    by (rule stutter_equiv_suffixes_right)
  with that show ?thesis
    by (force dest: stutter_equiv_0)
qed

end