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