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"
  by (simp add: stutter_sampler_def)

lemma stutter_sampler_mono: "stutter_sampler f σ ⟹ strict_mono f"
  by (simp add: stutter_sampler_def)

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)"
        by (auto simp add: Let_def)
      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] 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)"
        by (simp add: max_stutter_sampler stutter_sampler_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)" 
                      by (simp add: o_def)
                    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)"
                      by (simp add: less_le)
                    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)" 
                        by (simp add: o_def)
                    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))"
                by (simp add: o_def)
              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)"
                by (simp add: o_def)
              from this m have "(σ ∘ f) m = (σ ∘ f) (?mssf k)"
                by (blast intro: max_stutter_sampler_nostuttering)
              with diff m' a show "False"
                by (simp add: o_def)
            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 *)