# Theory Stuttering_Equivalence.Samplers

theory Samplers
imports Main "HOL-Library.Omega_Words_Fun"
begin

section ‹Utility Lemmas›

text ‹
The following lemmas about strictly monotonic functions could go
to the standard library of Isabelle/HOL.
›

text ‹
Strongly monotonic functions over the integers grow without bound.
›
lemma strict_mono_exceeds:
assumes f: "strict_mono (f::nat ⇒ nat)"
shows "∃k. n < f k"
proof (induct n)
from f have "f 0 < f 1" by (rule strict_monoD) simp
hence "0 < f 1" by simp
thus "∃k. 0 < f k" ..
next
fix n
assume "∃k. n < f k"
then obtain k where "n < f k" ..
hence "Suc n ≤ f k" by simp
also from f have "f k < f (Suc k)" by (rule strict_monoD) simp
finally show "∃k. Suc n < f k" ..
qed

text ‹
More precisely, any natural number ‹n ≥ f 0› lies in the interval
between ‹f k› and ‹f (Suc k)›, for some ‹k›.
›
lemma strict_mono_interval:
assumes f: "strict_mono (f::nat ⇒ nat)" and n: "f 0 ≤ n"
obtains k where "f k ≤ n" and "n < f (Suc k)"
proof -
from f[THEN strict_mono_exceeds] obtain m where m: "n < f m" ..
have "m ≠ 0"
proof
assume "m = 0"
with m n show "False" by simp
qed
with m obtain m' where m': "n < f (Suc m')" by (auto simp: gr0_conv_Suc)
let ?k = "LEAST k. n < f (Suc k)"
from m' have 1: "n < f (Suc ?k)" by (rule LeastI)
have "f ?k ≤ n"
proof (rule ccontr)
assume "¬ ?thesis"
hence k: "n < f ?k" by simp
show "False"
proof (cases "?k")
case 0 with k n show "False" by simp
next
case Suc with k show "False" by (auto dest: Least_le)
qed
qed
with 1 that show ?thesis by simp
qed

lemma strict_mono_comp:
assumes g: "strict_mono (g::'a::order ⇒ 'b::order)"
and f: "strict_mono (f::'b::order ⇒ 'c::order)"
shows "strict_mono (f ∘ g)"
using assms by (auto simp: strict_mono_def)

section ‹Stuttering Sampling Functions›

text ‹
Given an ‹ω›-sequence ‹σ›, a stuttering sampling function
is a strictly monotonic function ‹f::nat ⇒ nat› such that
‹f 0 = 0› and for all ‹i› and all ‹f i ≤ k < f (i+1)›,
the elements ‹σ k› are the same. In other words, ‹f› skips some
(but not necessarily all) stuttering steps, but never skips a non-stuttering step.
Given such ‹σ› and ‹f›, the (stuttering-)sampled
reduction of ‹σ› is the sequence of elements of ‹σ› at the
indices ‹f i›, which can simply be written as ‹σ ∘ f›.
›

subsection ‹Definition and elementary properties›

definition stutter_sampler where
― ‹f is a stuttering sampling function for @{text "σ"}›
"stutter_sampler (f::nat ⇒ nat) σ ≡
f 0 = 0
∧ strict_mono f
∧ (∀k n. f k < n ∧ n < f (Suc k) ⟶ σ n = σ (f k))"

lemma stutter_sampler_0: "stutter_sampler f σ ⟹ f 0 = 0"

lemma stutter_sampler_mono: "stutter_sampler f σ ⟹ strict_mono f"

lemma stutter_sampler_between:
assumes f: "stutter_sampler f σ"
and lo: "f k ≤ n" and hi: "n < f (Suc k)"
shows "σ n = σ (f k)"
using assms by (auto simp: stutter_sampler_def less_le)

lemma stutter_sampler_interval:
assumes f: "stutter_sampler f σ"
obtains k where "f k ≤ n" and "n < f (Suc k)"
using f[THEN stutter_sampler_mono] proof (rule strict_mono_interval)
from f show "f 0 ≤ n" by (simp add: stutter_sampler_0)
qed

text ‹
The identity function is a stuttering sampling function for any ‹σ›.
›
lemma id_stutter_sampler [iff]: "stutter_sampler id σ"
by (auto simp: stutter_sampler_def strict_mono_def)

text ‹
Stuttering sampling functions compose, sort of.
›
lemma stutter_sampler_comp:
assumes f: "stutter_sampler f σ"
and g: "stutter_sampler g (σ ∘ f)"
shows "stutter_sampler (f ∘ g) σ"
proof (auto simp: stutter_sampler_def)
from f g show "f (g 0) = 0" by (simp add: stutter_sampler_0)
next
from g[THEN stutter_sampler_mono] f[THEN stutter_sampler_mono]
show "strict_mono (f ∘ g)" by (rule strict_mono_comp)
next
fix i k
assume lo: "f (g i) < k" and hi: "k < f (g (Suc i))"
from f obtain m where 1: "f m ≤ k" and 2: "k < f (Suc m)"
by (rule stutter_sampler_interval)
with f have 3: "σ k = σ (f m)" by (rule stutter_sampler_between)
from lo 2 have "f (g i) < f (Suc m)" by simp
with f[THEN stutter_sampler_mono] have 4: "g i ≤ m" by (simp add: strict_mono_less)
from 1 hi have "f m < f (g (Suc i))" by simp
with f[THEN stutter_sampler_mono] have 5: "m < g (Suc i)"by (simp add: strict_mono_less)
from g 4 5 have "(σ ∘ f) m = (σ ∘ f) (g i)" by (rule stutter_sampler_between)
with 3 show "σ k = σ (f (g i))" by simp
qed

text ‹
Stuttering sampling functions can be extended to suffixes.
›
lemma stutter_sampler_suffix:
assumes f: "stutter_sampler f σ"
shows "stutter_sampler (λk. f (n+k) - f n) (suffix (f n) σ)"
proof (auto simp: stutter_sampler_def strict_mono_def)
fix i j
assume ij: "(i::nat) < j"
from f have mono: "strict_mono f" by (rule stutter_sampler_mono)

from mono[THEN strict_mono_mono] have "f n ≤ f (n+i)"
by (rule monoD) simp
moreover
from mono[THEN strict_mono_mono] have "f n ≤ f (n+j)"
by (rule monoD) simp
moreover
from mono ij have "f (n+i) < f (n+j)" by (auto intro: strict_monoD)
ultimately
show "f (n+i) - f n < f (n+j) - f n" by simp
next
fix i k
assume lo: "f (n+i) - f n < k" and hi: "k < f (Suc (n+i)) - f n"
from lo have "f (n+i) ≤ f n + k" by simp
moreover
from hi have "f n + k < f (Suc (n + i))" by simp
moreover
from f[THEN stutter_sampler_mono, THEN strict_mono_mono]
have "f n ≤ f (n+i)" by (rule monoD) simp
ultimately show "σ (f n + k) = σ (f n + (f (n+i) - f n))"
by (auto dest: stutter_sampler_between[OF f])
qed

subsection ‹Preservation of properties through stuttering sampling›

text ‹
Stuttering sampling preserves the initial element of the sequence, as well as
the presence and relative ordering of different elements.
›

lemma stutter_sampled_0:
assumes "stutter_sampler f σ"
shows "σ (f 0) = σ 0"
using assms[THEN stutter_sampler_0] by simp

lemma stutter_sampled_in_range:
assumes f: "stutter_sampler f σ" and s: "s ∈ range σ"
shows "s ∈ range (σ ∘ f)"
proof -
from s obtain n where n: "σ n = s" by auto
from f obtain k where "f k ≤ n" "n < f (Suc k)" by (rule stutter_sampler_interval)
with f have "σ n = σ (f k)" by (rule stutter_sampler_between)
with n show ?thesis by auto
qed

lemma stutter_sampled_range:
"range (σ ∘ f) = range σ" if "stutter_sampler f σ"
using that stutter_sampled_in_range [of f σ] by auto

lemma stutter_sampled_precedence:
assumes f: "stutter_sampler f σ" and ij: "i ≤ j"
obtains k l where "k ≤ l" "σ (f k) = σ i" "σ (f l) = σ j"
proof -
from f obtain k where k: "f k ≤ i" "i < f (Suc k)" by (rule stutter_sampler_interval)
with f have 1: "σ i = σ (f k)" by (rule stutter_sampler_between)
from f obtain l where l: "f l ≤ j" "j < f (Suc l)" by (rule stutter_sampler_interval)
with f have 2: "σ j = σ (f l)" by (rule stutter_sampler_between)
from k l ij have "f k < f (Suc l)" by simp
with f[THEN stutter_sampler_mono] have "k ≤ l" by (simp add: strict_mono_less)
with 1 2 that show ?thesis by simp
qed

subsection ‹Maximal stuttering sampling›

text ‹
We define a particular sampling function that is maximal in the sense that it
eliminates all finite stuttering. If a sequence ends with infinite stuttering
then it behaves as the identity over the (maximal such) suffix.
›

fun max_stutter_sampler where
"max_stutter_sampler σ 0 = 0"
| "max_stutter_sampler σ (Suc n) =
(let prev = max_stutter_sampler σ n
in  if (∀k > prev. σ k = σ prev)
then Suc prev
else (LEAST k. prev < k ∧ σ k ≠ σ prev))"

text ‹
‹max_stutter_sampler› is indeed a stuttering sampling function.
›
lemma max_stutter_sampler:
"stutter_sampler (max_stutter_sampler σ) σ" (is "stutter_sampler ?ms _")
proof -
have "?ms 0 = 0" by simp
moreover
have "∀n. ?ms n < ?ms (Suc n)"
proof
fix n
show "?ms n < ?ms (Suc n)" (is "?prev < ?next")
proof (cases "∀k > ?prev. σ k = σ ?prev")
case True thus ?thesis by (simp add: Let_def)
next
case False
hence "∃k. ?prev < k ∧ σ k ≠ σ ?prev" by simp
from this[THEN LeastI_ex]
have "?prev < (LEAST k. ?prev < k ∧ σ k ≠ σ ?prev)" ..
with False show ?thesis by (simp add: Let_def)
qed
qed
hence "strict_mono ?ms"
unfolding strict_mono_def by (blast intro: lift_Suc_mono_less)
moreover
have "∀n k. ?ms n < k ∧ k < ?ms (Suc n) ⟶ σ k = σ (?ms n)"
proof (clarify)
fix n k
assume lo: "?ms n < k" (is "?prev < k")
and hi: "k < ?ms (Suc n)" (is "k < ?next")
show "σ k = σ ?prev"
proof (cases "∀k > ?prev. σ k = σ ?prev")
case True
hence "?next = Suc ?prev" by (simp add: Let_def)
with lo hi show ?thesis by simp  ― ‹no room for intermediate index›
next
case False
hence "?next = (LEAST k. ?prev < k ∧ σ k ≠ σ ?prev)"
with lo hi show ?thesis by (auto dest: not_less_Least)
qed
qed
ultimately show ?thesis unfolding stutter_sampler_def by blast
qed

text ‹
We write ‹♮σ› for the sequence ‹σ› sampled by the
maximal stuttering sampler. Also, a sequence is \emph{stutter free}
if it contains no finite stuttering: whenever two subsequent
elements are equal then all subsequent elements are the same.
›
definition stutter_reduced ("♮_"  100) where
"♮σ = σ ∘ (max_stutter_sampler σ)"

definition stutter_free where
"stutter_free σ ≡ ∀k. σ (Suc k) = σ k ⟶ (∀n>k. σ n = σ k)"

lemma stutter_freeI:
assumes "⋀k n. ⟦σ (Suc k) = σ k; n>k⟧ ⟹ σ n = σ k"
shows "stutter_free σ"
using assms unfolding stutter_free_def by blast

lemma stutter_freeD:
assumes "stutter_free σ" and "σ (Suc k) = σ k" and "n>k"
shows "σ n = σ k"
using assms unfolding stutter_free_def by blast

text ‹
Any suffix of a stutter free sequence is itself stutter free.
›
lemma stutter_free_suffix:
assumes sigma: "stutter_free σ"
shows "stutter_free (suffix k σ)"
proof (rule stutter_freeI)
fix j n
assume j: "(suffix k σ) (Suc j) = (suffix k σ) j" and n: "j < n"
from j have "σ (Suc (k+j)) = σ (k+j)" by simp
moreover from n have "k+n > k+j" by simp
ultimately have "σ (k+n) = σ (k+j)" by (rule stutter_freeD[OF sigma])
thus "(suffix k σ) n = (suffix k σ) j" by simp
qed

lemma stutter_reduced_0: "(♮σ) 0 = σ 0"
by (simp add: stutter_reduced_def stutter_sampled_0 max_stutter_sampler)

lemma stutter_free_reduced:
assumes sigma: "stutter_free σ"
shows "♮σ = σ"
proof -
{
fix n
have "max_stutter_sampler σ n = n" (is "?ms n = n")
proof (induct n)
show "?ms 0 = 0" by simp
next
fix n
assume ih: "?ms n = n"
show "?ms (Suc n) = Suc n"
proof (cases "σ (Suc n) = σ (?ms n)")
case True
with ih have "σ (Suc n) = σ n" by simp
with sigma have "∀k > n. σ k = σ n"
unfolding stutter_free_def by blast
with ih show ?thesis by (simp add: Let_def)
next
case False
with ih have "(LEAST k. k>n ∧ σ k ≠ σ (?ms n)) = Suc n"
by (auto intro: Least_equality)
with ih False show ?thesis by (simp add: Let_def)
qed
qed
}
thus ?thesis by (auto simp: stutter_reduced_def)
qed

text ‹
Whenever two sequence elements at two consecutive sampling points of the
maximal stuttering sampler are equal then the sequence stutters infinitely
from the first sampling point onwards. In particular, ‹♮σ› is
stutter free.
›
lemma max_stutter_sampler_nostuttering:
assumes stut: "σ (max_stutter_sampler σ (Suc k)) = σ (max_stutter_sampler σ k)"
and n: "n > max_stutter_sampler σ k" (is "_ > ?ms k")
shows "σ n = σ (?ms k)"
proof (rule ccontr)
assume contr: "¬ ?thesis"
with n have "?ms k < n ∧ σ n ≠ σ (?ms k)" (is "?diff n") ..
hence "?diff (LEAST n. ?diff n)" by (rule LeastI)
with contr have "σ (?ms (Suc k)) ≠ σ (?ms k)" by (auto simp add: Let_def)
from this stut show "False" ..
qed

lemma stutter_reduced_stutter_free: "stutter_free (♮σ)"
proof (rule stutter_freeI)
fix k n
assume k: "(♮σ) (Suc k) = (♮σ) k" and n: "k < n"
from n have "max_stutter_sampler σ k < max_stutter_sampler σ n"
using max_stutter_sampler[THEN stutter_sampler_mono, THEN strict_monoD]
by blast
with k show "(♮σ) n = (♮σ) k"
unfolding stutter_reduced_def
by (auto elim: max_stutter_sampler_nostuttering
simp del: max_stutter_sampler.simps)
qed

lemma stutter_reduced_suffix: "♮ (suffix k (♮σ)) = suffix k (♮σ)"
proof (rule stutter_free_reduced)
have "stutter_free (♮σ)" by (rule stutter_reduced_stutter_free)
thus "stutter_free (suffix k (♮σ))" by (rule stutter_free_suffix)
qed

lemma stutter_reduced_reduced: "♮♮σ = ♮σ"
by (insert stutter_reduced_suffix[of 0 "σ", simplified])

text ‹
One can define a partial order on sampling functions for a given sequence
‹σ› by saying that function ‹g› is better than function ‹f›
if the reduced sequence induced by ‹f› can be further reduced to obtain
the reduced sequence corresponding to ‹g›, i.e. if there exists a
stuttering sampling function ‹h› for the reduced sequence ‹σ ∘ f›
such that ‹σ ∘ f ∘ h = σ ∘ g›. (Note that ‹f ∘ h› is indeed a stuttering
sampling function for ‹σ›, by theorem ‹stutter_sampler_comp›.)

We do not formalize this notion but prove that ‹max_stutter_sampler σ›
is the best sampling function according to this order.
›

theorem sample_max_sample:
assumes f: "stutter_sampler f σ"
shows "♮(σ ∘ f) = ♮σ"
proof -
let ?mss = "max_stutter_sampler σ"
let ?mssf = "max_stutter_sampler (σ ∘ f)"
from f have mssf: "stutter_sampler (f ∘ ?mssf) σ"
by (blast intro: stutter_sampler_comp max_stutter_sampler)
txt ‹
The following is the core invariant of the proof: the sampling functions
‹max_stutter_sampler σ› and ‹f ∘ (max_stutter_sampler (σ ∘ f))›
work in lock-step (i.e., sample the same points), except if ‹σ› ends
in infinite stuttering, at which point function ‹f› may make larger
steps than the maximal sampling functions.
›
{
fix k
have "  ?mss k = f (?mssf k)
∨ ?mss k ≤ f (?mssf k) ∧ (∀n ≥ ?mss k. σ (?mss k) = σ n)"
(is "?P k" is "?A k ∨ ?B k")
proof (induct k)
from f mssf have "?mss 0 = f (?mssf 0)"
thus "?P 0" ..
next
fix k
assume ih: "?P k"
have b: "?B k ⟶ ?B (Suc k)"
proof
assume 0: "?B k" hence 1: "?mss k ≤ f (?mssf k)" ..
(* NB: For some reason "... hence 1: ... and 2: ..." cannot be proved *)
from 0 have 2: "∀n ≥ ?mss k. σ (?mss k) = σ n" ..
hence "∀n > ?mss k. σ (?mss k) = σ n" by auto
hence "∀n > ?mss k. σ n = σ (?mss k)" by auto
hence 3: "?mss (Suc k) = Suc (?mss k)" by (simp add: Let_def)
with 2 have "σ (?mss k) = σ (?mss (Suc k))"
by (auto simp del: max_stutter_sampler.simps)
from sym[OF this] 2 3 have "∀n ≥ ?mss (Suc k). σ (?mss (Suc k)) = σ n"
by (auto simp del: max_stutter_sampler.simps)
moreover
from mssf[THEN stutter_sampler_mono, THEN strict_monoD]
have "f (?mssf k) < f (?mssf (Suc k))"
by (simp del: max_stutter_sampler.simps)
with 1 3 have "?mss (Suc k) ≤ f (?mssf (Suc k))"
by (simp del: max_stutter_sampler.simps)
ultimately show "?B (Suc k)" by blast
qed
from ih show "?P (Suc k)"
proof
assume a: "?A k"
show ?thesis
proof (cases "∀n > ?mss k. σ n = σ (?mss k)")
case True
hence "∀n ≥ ?mss k. σ (?mss k) = σ n" by (auto simp: le_less)
with a have "?B k" by simp
with b show ?thesis by (simp del: max_stutter_sampler.simps)
next
case False
hence diff: "σ (?mss (Suc k)) ≠ σ (?mss k)"
by (blast dest: max_stutter_sampler_nostuttering)
have "?A (Suc k)"
proof (rule antisym)
show "f (?mssf (Suc k)) ≤ ?mss (Suc k)"
proof (rule ccontr)
assume "¬ ?thesis"
hence contr: "?mss (Suc k) < f (?mssf (Suc k))" by simp
from mssf have "σ (?mss (Suc k)) = σ ((f ∘ ?mssf) k)"
proof (rule stutter_sampler_between)
from max_stutter_sampler[of "σ", THEN stutter_sampler_mono]
have "?mss k < ?mss (Suc k)" by (rule strict_monoD) simp
with a show "(f ∘ ?mssf) k ≤ ?mss (Suc k)"
by (simp add: o_def del: max_stutter_sampler.simps)
next
from contr show "?mss (Suc k) < (f ∘ ?mssf) (Suc k)" by simp
qed
with a have "σ (?mss (Suc k)) = σ (?mss k)"
by (simp add: o_def del: max_stutter_sampler.simps)
with diff show "False" ..
qed
next
have "∃m > ?mssf k. f m = ?mss (Suc k)"
proof (rule ccontr)
assume "¬ ?thesis"
hence contr: "∀i. f ((?mssf k) + Suc i) ≠ ?mss (Suc k)" by simp
{
fix i
have "f (?mssf k + i) < ?mss (Suc k)" (is "?F i")
proof (induct i)
from a have "f (?mssf k + 0) = ?mss k" by (simp add: o_def)
also from max_stutter_sampler[of "σ", THEN stutter_sampler_mono]
have "... < ?mss (Suc k)"
by (rule strict_monoD) simp
finally show "?F 0" .
next
fix i
assume ih: "?F i"
show "?F (Suc i)"
proof (rule ccontr)
assume "¬ ?thesis"
then have "?mss (Suc k) ≤ f (?mssf k + Suc i)"
moreover from contr have "f (?mssf k + Suc i) ≠ ?mss (Suc k)"
by blast
ultimately have i: "?mss (Suc k) < f (?mssf k + Suc i)"
from f have "σ (?mss (Suc k)) = σ (f (?mssf k + i))"
proof (rule stutter_sampler_between)
from ih show "f (?mssf k + i) ≤ ?mss (Suc k)"
next
from i show "?mss (Suc k) < f (Suc (?mssf k + i))"
by simp
qed
also from max_stutter_sampler have "... = σ (?mss k)"
proof (rule stutter_sampler_between)
from f[THEN stutter_sampler_mono, THEN strict_mono_mono]
have "f (?mssf k) ≤ f (?mssf k + i)" by (rule monoD) simp
with a show "?mss k ≤ f (?mssf k + i)" by (simp add: o_def)
qed (rule ih)
also note diff
finally show "False" by simp
qed
qed
} note bounded = this
from f[THEN stutter_sampler_mono]
have "strict_mono (λi. f (?mssf k + i))"
by (auto simp: strict_mono_def)
then obtain i where i: "?mss (Suc k) < f (?mssf k + i)"
by (blast dest: strict_mono_exceeds)
from bounded have "f (?mssf k + i) < ?mss (Suc k)" .
with i show "False" by (simp del: max_stutter_sampler.simps)
qed
then obtain m where m: "m > ?mssf k" and m': "f m = ?mss (Suc k)"
by blast
show "?mss (Suc k) ≤ f (?mssf (Suc k))"
proof (rule ccontr)
assume "¬ ?thesis"
hence contr: "f (?mssf (Suc k)) < ?mss (Suc k)" by simp
from mssf[THEN stutter_sampler_mono]
have "(f ∘ ?mssf) k < (f ∘ ?mssf) (Suc k)"
by (rule strict_monoD) simp
with a have "?mss k ≤ f (?mssf (Suc k))"
from this contr have "σ (f (?mssf (Suc k))) = σ (?mss k)"
by (rule stutter_sampler_between[OF max_stutter_sampler])
with a have stut: "(σ ∘ f) (?mssf (Suc k)) = (σ ∘ f) (?mssf k)"
from this m have "(σ ∘ f) m = (σ ∘ f) (?mssf k)"
by (blast intro: max_stutter_sampler_nostuttering)
with diff m' a show "False"
qed
qed
thus ?thesis ..
qed
next
assume "?B k" with b show ?thesis by (simp del: max_stutter_sampler.simps)
qed
qed
}
hence "♮σ = ♮(σ ∘ f)" unfolding stutter_reduced_def by force
thus ?thesis by (rule sym)
qed

end  (* theory Samplers *)