# 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
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"
with g[THEN stutter_sampler_mono] have "g a < g i"
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