Quelle  Sequence.thy

(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
    Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
                 Stephan Merz <Stephan.Merz at loria.fr>
    Year:        2011
    Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
*)

section ‹(Infinite) Sequences›

theory Sequence
imports Main
begin

text ‹
 Lamport's Temporal Logic of Actions (TLA) is a linear-time temporal logic,
 and its semantics is defined over infinite sequence of states, which we
 simply represent by the type ‹'a seq›, defined as an abbreviation
 for the type ‹nat ==> 'a›, where ‹'a› is the type of sequence
 elements.

 This theory defines some useful notions about such sequences, and in particular
 concepts related to stuttering (finite repetitions of states), which are
 important for the semantics of TLA. We identify a finite sequence with an
 infinite sequence that ends in infinite stuttering. In this way, we avoid the
 complications of having to handle both finite and infinite sequences of states:
 see e.g. Devillers et al cite‹"Devillers97"› who discuss several variants of
 representing possibly infinite sequences in HOL, Isabelle and PVS.
 ›

type_synonym 'a seq = "nat ==> 'a"

subsection "Some operators on sequences"

text ‹Some general functions on sequences are provided›

definition first :: "'a seq ==> 'a" 
where "first s ≡ s 0"

definition second :: "('a seq) ==> 'a"
where "second s ≡ s 1"

definition suffix :: "'a seq ==> nat ==> 'a seq" (infixl ‹|_s› 60)
where "s |_s i ≡ λ n. s (n+i)"

definition tail :: "'a seq ==> 'a seq"
where "tail s ≡ s |_s 1"

definition
 app :: "'a ==> ('a seq) ==> ('a seq)" (infixl ‹##› 60)
where
 "s ## σ ≡ λ n. if n=0 then s else σ (n - 1)"

text ‹
 ‹s |_s i› returns the suffix of sequence @{term s} from
 index @{term i}. @{term first} returns the first element of a sequence
 while @{term second} returns the second element. @{term tail} returns the
 sequence starting at the second element. @{term "s ## σ"} prefixes the
 sequence @{term σ} by element @{term s}.
 ›

subsubsection "Properties of @{term first} and @{term second}"

lemma first_tail_second: "first(tail s) = second s"
  by (simp add: first_def second_def tail_def suffix_def)


subsubsection "Properties of @{term suffix}"

lemma suffix_first: "first (s |_s n) = s n"
  by (auto simp add: suffix_def first_def)

lemma suffix_second: "second (s |_s n) = s (Suc n)"
  by (auto simp add: suffix_def second_def)

lemma suffix_plus: "s |_s n |_s m = s |_s (m + n)"
  by (simp add: suffix_def add.assoc)

lemma suffix_commute: "((s |_s n) |_s m) = ((s |_s m) |_s n)"
  by (simp add: suffix_plus add.commute)

lemma suffix_plus_com: "s |_s m |_s n = s |_s (m + n)"
proof -
  have "s |_s n |_s m = s |_s (m + n)" by (rule suffix_plus)
  thus "s |_s m |_s n = s |_s (m + n)" by (simp add: suffix_commute)
qed

lemma suffix_zero[simp]: "s |_s 0 = s"
  by (simp add: suffix_def)

lemma suffix_tail: "s |_s 1 = tail s"
  by (simp add: tail_def)

lemma tail_suffix_suc: "s |_s (Suc n) = tail (s |_s n)"
  by (simp add: suffix_def tail_def)

subsubsection "Properties of @{term app}"

lemma seq_app_second: "(s ## σ) 1 = σ 0"
  by (simp add: app_def)

lemma seq_app_first: "(s ## σ) 0 = s" 
  by (simp add: app_def)

lemma seq_app_first_tail: "(first s) ## (tail s) = s"
proof (rule ext)
  fix x
  show "(first s ## tail s) x = s x"
    by (simp add: first_def app_def suffix_def tail_def)
qed

lemma seq_app_tail: "tail (x ## s) = s"
  by (simp add: app_def tail_def suffix_def)

lemma seq_app_greater_than_zero: "n > 0 ==> (s ## σ) n = σ (n - 1)" 
  by (simp add: app_def)


subsection "Finite and Empty Sequences"

text‹
 We identify finite and empty sequences and prove lemmas about them.
 ›

definition fin :: "('a seq) ==> bool"
where "fin s ≡ ∃ i. ∀ j ≥ i. s j = s i"

abbreviation inf :: "('a seq) ==> bool"
where "inf s ≡ ¬(fin s)"

definition last :: "('a seq) ==> nat"
where "last s ≡ LEAST i. (∀ j ≥ i. s j = s i)" 

definition laststate :: "('a seq) ==> 'a"
where "laststate s ≡ s (last s)"

definition emptyseq :: "('a seq) ==> bool"
where "emptyseq ≡ λ s. ∀ i. s i = s 0"

abbreviation notemptyseq :: "('a seq) ==> bool"
where "notemptyseq s ≡ ¬(emptyseq s)"

text ‹
 Predicate @{term fin} holds if there is an element
 in the sequence such that all subsequent elements are identical,
 i.e. the sequence is finite. @{term "last s"} returns the smallest index
 from which on all elements of a finite sequence @{term s} are identical. Note that
 if ‹s› is not finite then an arbitrary number is returned.
 @{term laststate} returns the last element of a finite sequence. We assume
 that the sequence is finite when using @{term last} and @{term laststate}.
 Predicate @{term emptyseq} identifies empty sequences -- i.e. all states in
 the sequence are identical to the initial one, while @{term notemptyseq} holds
 if the given sequence is not empty.
 ›

subsubsection "Properties of @{term emptyseq}"

lemma empty_is_finite: assumes "emptyseq s" shows "fin s"
  using assms by (auto simp: fin_def emptyseq_def)

lemma empty_suffix_is_empty: assumes H: "emptyseq s" shows "emptyseq (s |_s n)"
proof (clarsimp simp: emptyseq_def)
 fix i
 from H have "(s |_s n) i = s 0" by (simp add: emptyseq_def suffix_def)
 moreover
 from H have "(s |_s n) 0 = s 0" by (simp add: emptyseq_def suffix_def)
 ultimately
 show "(s |_s n) i = (s |_s n) 0" by simp
qed

lemma suc_empty: assumes H1: "emptyseq (s |_s m)" shows "emptyseq (s |_s (Suc m))"
proof -
  from H1 have "emptyseq ((s |_s m) |_s 1)" by (rule empty_suffix_is_empty)
  thus ?thesis by (simp add: suffix_plus)
qed

lemma empty_suffix_exteq: assumes H:"emptyseq s" shows "(s |_s n) m = s m"
proof (unfold suffix_def)
  from H have "s (m+n) = s 0" by (simp add: emptyseq_def)
  moreover
  from H have "s m = s 0" by (simp add: emptyseq_def)
  ultimately show "s (m + n) = s m" by simp
qed

lemma empty_suffix_eq: assumes H: "emptyseq s" shows "(s |_s n) = s"
proof (rule ext)
  fix m
  from H show "(s |_s n) m = s m" by (rule empty_suffix_exteq)
qed

lemma seq_empty_all: assumes H: "emptyseq s" shows "s i = s j"
proof -
  from H have "s i = s 0" by (simp add: emptyseq_def)
  moreover
  from H have "s j = s 0" by (simp add: emptyseq_def)
  ultimately
  show ?thesis by simp
qed

subsubsection "Properties of @{term last} and @{term laststate}" 

lemma fin_stut_after_last: assumes H: "fin s" shows "∀j ≥ last s. s j = s (last s)"
proof (clarify)
  fix j
  assume j: "j ≥ last s"
  from H obtain i where "∀j ≥ i. s j = s i" (is "?P i") by (auto simp: fin_def)
  hence "?P (last s)" unfolding last_def by (rule LeastI)
  with j show "s j = s (last s)" by blast
qed


subsection "Stuttering Invariance"

text ‹
 This subsection provides functions for removing stuttering
 steps of sequences, i.e. we formalise Lamports ‹♮› operator.
 Our formal definition is close to that of Wahab in the PVS prover.

 The key novelty with the @{term "Sequence"} theory, is the treatment of
 stuttering invariance, which enables verification of stuttering invariance of
 the operators derived using it. Such proofs require comparing sequences
 up to stuttering. Here, Lamport's cite‹"Lamport94"› method is used to
 mechanise the equality of sequences up to stuttering: he defines
 the ‹♮› operator, which collapses a sequence by removing
 all stuttering steps, except possibly infinite stuttering at the end of the sequence.
 These are left unchanged.
 ›

definition nonstutseq :: "('a seq) ==> bool"
where "nonstutseq s ≡ ∀ i. s i = s (Suc i) ⟶ (∀ j > i. s i = s j)"

definition stutstep :: "('a seq) ==> nat ==> bool"
where "stutstep s n ≡ (s n = s (Suc n))"

definition nextnat :: "('a seq) ==> nat"
where "nextnat s ≡ if emptyseq s then 0 else LEAST i. s i ≠ s 0"

definition nextsuffix :: "('a seq) ==> ('a seq)"
where "nextsuffix s ≡ s |_s (nextnat s)"

fun "next" :: "nat ==> ('a seq) ==> ('a seq)" where
  "next 0 = id"
| "next (Suc n) = nextsuffix o (next n)"

definition collapse :: "('a seq) ==> ('a seq)" (‹♮›)
where "♮ s ≡ λ n. (next n s) 0"

text ‹
 Predicate @{term nonstutseq} identifies sequences without any
 stuttering steps -- except possibly for infinite stuttering at the end.
 Further, @{term "stutstep s n"} is a predicate which holds if the element
 after @{term "s n"} is equal to @{term "s n"}, i.e. @{term "Suc n"} is
 a stuttering step.
 @{term "collapse s"} formalises Lamports @{term "♮"}
 operator. It returns the first state of the result of @{term "next n s"}.
 @{term "next n s"} finds suffix of the $n^{th}$ change. Hence the first
 element, which @{term "♮ s"} returns, is the state after the $n^{th}$
 change. @{term "next n s"} is defined by primitive recursion on
 @{term "n"} using function composition of function @{term nextsuffix}. E.g.
 @{term "next 3 s"} equals @{term "nextsuffix (nextsuffix (nextsuffix s))"}.
 @{term "nextsuffix s"} returns the suffix of the sequence starting at the
 next changing state. It uses @{term "nextnat"} to obtain this. All the real
 computation is done in this function. Firstly, an empty sequence will obviously
 not contain any changes, and ‹0› is therefore returned. In this case
 @{term "nextsuffix"} behaves like the identify function. If the sequence is not
 empty then the smallest number @{term "i"} such that @{term "s i"} is different
 from the initial state is returned. This is achieved by @{term "Least"}.
 ›

subsubsection "Properties of @{term nonstutseq}"

lemma seq_empty_is_nonstut: 
  assumes H: "emptyseq s" shows "nonstutseq s"
  using H by (auto simp: nonstutseq_def seq_empty_all)

lemma notempty_exist_nonstut: 
  assumes H: "¬ emptyseq (s |_s m)" shows "∃ i. s i ≠ s m ∧ i > m"
using H proof (auto simp: emptyseq_def suffix_def)
  fix i
  assume i: "s (i + m) ≠ s m"
  hence "i ≠ 0" by (intro notI, simp)
  with i show ?thesis by auto
qed

subsubsection "Properties of @{term nextnat}"

lemma nextnat_le_unch: assumes H: "n < nextnat s" shows "s n = s 0"
proof (cases "emptyseq s")
  assume "emptyseq s"
  hence "nextnat s = 0" by (simp add: nextnat_def)
  with H show ?thesis by auto
next
  assume "¬ emptyseq s"
  hence a1: "nextnat s = (LEAST i. s i ≠ s 0)" by (simp add: nextnat_def) 
  show ?thesis
  proof (rule ccontr)
    assume a2: "s n ≠ s 0" (is "?P n")
    hence "(LEAST i. s i ≠ s 0) ≤ n" by (rule Least_le)
    hence "¬(n < (LEAST i. s i ≠ s 0))" by auto
    also from H a1 have "n < (LEAST i. s i ≠ s 0)" by simp
    ultimately show False by auto
  qed
qed

lemma stutnempty: 
  assumes H: "¬ stutstep s n" shows "¬ emptyseq (s |_s n)"
proof (unfold emptyseq_def suffix_def)
  from H have "s (Suc n) ≠ s n" by (auto simp add: stutstep_def)
  hence "s (1+n) ≠ s (0+n)" by simp
  thus "¬(∀ i. s (i+n) = s (0+n))" by blast
qed

lemma notstutstep_nexnat1: 
  assumes H: "¬ stutstep s n" shows "nextnat (s |_s n) = 1"
proof -
  from H have h': "nextnat (s |_s n) = (LEAST i. (s |_s n) i ≠ (s |_s n) 0)" 
    by (auto simp add: nextnat_def stutnempty)
  from H have "s (Suc n) ≠ s n" by (auto simp add: stutstep_def)
  hence "(s |_s n) 1 ≠ (s |_s n) 0" (is "?P 1") by (auto simp add: suffix_def)
  hence "Least ?P ≤ 1" by (rule Least_le)
  hence g1: "Least ?P = 0 ∨ Least ?P = 1" by auto
  with h' have g1': "nextnat (s |_s n) = 0 ∨ nextnat (s |_s n) = 1" by auto
  also have "nextnat (s |_s n) ≠ 0" 
  proof -
    from H have "¬ emptyseq (s |_s n)" by (rule stutnempty)
    then obtain i where "(s |_s n) i ≠ (s |_s n) 0" by (auto simp add: emptyseq_def)
    hence "(s |_s n) (LEAST i. (s |_s n) i ≠ (s |_s n) 0) ≠ (s |_s n) 0" by (rule LeastI)
    with h' have g2: "(s |_s n) (nextnat (s |_s n)) ≠ (s |_s n) 0" by auto
    show "(nextnat (s |_s n)) ≠ 0" 
    proof
      assume "(nextnat (s |_s n)) = 0"
      with g2 show "False" by simp
    qed
  qed
  ultimately show  "nextnat (s |_s n) = 1" by auto
qed

lemma stutstep_notempty_notempty: 
  assumes h1: "emptyseq (s |_s Suc n)" (is "emptyseq ?sn")
      and h2: "stutstep s n" 
  shows "emptyseq (s |_s n)" (is "emptyseq ?s")
proof (auto simp: emptyseq_def)
  fix k
  show "?s k = ?s 0"
  proof (cases k)
    assume "k = 0" thus ?thesis by simp
  next
    fix m
    assume k: "k = Suc m"
    hence "?s k = ?sn m" by (simp add: suffix_def)
    also from h1 have "... = ?sn 0" by (simp add: emptyseq_def)
    also from h2 have "... = s n" by (simp add: suffix_def stutstep_def)
    finally show ?thesis by (simp add: suffix_def)
  qed
qed

lemma stutstep_empty_suc:
  assumes "stutstep s n"
  shows "emptyseq (s |_s Suc n) = emptyseq (s |_s n)"
using assms by (auto elim: stutstep_notempty_notempty suc_empty)

lemma stutstep_notempty_sucnextnat: 
  assumes h1: "¬ emptyseq (s |_s n)" and h2: "stutstep s n" 
   shows "(nextnat (s |_s n)) = Suc (nextnat (s |_s (Suc n)))"
proof -
  from h2 have g1: "¬(s (0+n) ≠ s (Suc n))" (is "¬ ?P 0") by (auto simp add: stutstep_def)
  from h1 obtain i where "s (i+n) ≠ s n" by (auto simp: emptyseq_def suffix_def)
  with h2 have g2: "s (i+n) ≠ s (Suc n)" (is "?P i") by (simp add: stutstep_def)
  from g2 g1 have "(LEAST n. ?P n) = Suc (LEAST n. ?P (Suc n))" by (rule Least_Suc)
  from g2 g1 have "(LEAST i. s (i+n) ≠ s (Suc n)) = Suc (LEAST i. s ((Suc i)+n) ≠ s (Suc n))"
    by (rule Least_Suc)
  hence G1: "(LEAST i. s (i+n) ≠ s (Suc n)) = Suc (LEAST i. s (i+Suc n) ≠ s (Suc n))" by auto
  from h1 h2 have "¬ emptyseq (s |_s Suc n)" by (simp add: stutstep_empty_suc)
  hence "nextnat (s |_s Suc n) = (LEAST i. (s |_s Suc n) i ≠ (s |_s Suc n) 0)"
    by (auto simp add: nextnat_def)
  hence g1: "nextnat (s |_s Suc n) = (LEAST i. s (i+(Suc n)) ≠ s (Suc n))"
    by (simp add: suffix_def)
  from h1 have  "nextnat (s |_s n) = (LEAST i. (s |_s n) i ≠ (s |_s n) 0)"
    by (auto simp add: nextnat_def)
  hence g2: "nextnat (s |_s n) = (LEAST i. s (i+n) ≠ s n)" by (simp add: suffix_def)
  with h2 have g2': "nextnat (s |_s n) = (LEAST i. s (i+n) ≠ s (Suc n))"
    by (auto simp add: stutstep_def)
  from G1 g1 g2' show ?thesis by auto
qed

lemma nextnat_empty_neq: assumes H: "¬ emptyseq s" shows "s (nextnat s) ≠ s 0"
proof -
  from H have a1: "nextnat s = (LEAST i. s i ≠ s 0)" by (simp add: nextnat_def)
  from H obtain i where "s i ≠ s 0" by (auto simp: emptyseq_def)
  hence "s (LEAST i. s i ≠ s 0) ≠ s 0" by (rule LeastI)
  with a1 show ?thesis by auto
qed

lemma nextnat_empty_gzero: assumes H: "¬ emptyseq s" shows "nextnat s > 0"
proof -
  from H have a1: "s (nextnat s) ≠ s 0" by (rule nextnat_empty_neq)
  have "nextnat s ≠ 0"
  proof
    assume "nextnat s = 0"
    with a1 show "False" by simp
  qed
  thus "nextnat s > 0" by simp
qed

subsubsection "Properties of @{term nextsuffix}"

lemma empty_nextsuffix: 
  assumes H: "emptyseq s" shows "nextsuffix s = s"
  using H by (simp add: nextsuffix_def nextnat_def)

lemma empty_nextsuffix_id: 
  assumes H: "emptyseq s" shows "nextsuffix s = id s"
  using H by (simp add: empty_nextsuffix)

lemma notstutstep_nextsuffix1: 
  assumes H: "¬ stutstep s n" shows "nextsuffix (s |_s n) = s |_s (Suc n)"
proof (unfold nextsuffix_def)
  show "(s |_s n |_s (nextnat (s |_s n))) = s |_s (Suc n)"
  proof -
    from H have  "nextnat (s |_s n) = 1" by (rule notstutstep_nexnat1)
    hence "(s |_s n |_s (nextnat (s |_s n))) = s |_s n |_s 1" by auto
    thus ?thesis by (simp add: suffix_def)
  qed
qed

subsubsection "Properties of @{term next}"

lemma next_suc_suffix: "next (Suc n) s = nextsuffix (next n s)"
  by simp

lemma next_suffix_com: "nextsuffix (next n s) = (next n (nextsuffix s))"
  by (induct n, auto)

lemma next_plus: "next (m+n) s = next m (next n s)" 
  by (induct m, auto)

lemma next_empty: assumes H: "emptyseq s" shows "next n s = s"
proof (induct n)
  from H show "next 0 s = s" by auto
next
  fix n
  assume a1: "next n s = s"
  have "next (Suc n) s = nextsuffix (next n s)" by auto
  with a1 have "next (Suc n) s = nextsuffix s" by simp
  with H show "next (Suc n) s = s"
    by (simp add: nextsuffix_def nextnat_def)
qed

lemma notempty_nextnotzero: 
  assumes H: "¬emptyseq s" shows "(next (Suc 0) s) 0 ≠ s 0"
proof -
  from H have g1: "s (nextnat s) ≠ s 0" by (rule nextnat_empty_neq)
  have "next (Suc 0) s = nextsuffix s" by auto
  hence "(next (Suc 0) s) 0 = s (nextnat s)" by (simp add: nextsuffix_def suffix_def)
  with g1 show ?thesis by simp
qed

lemma next_ex_id: "∃ i. s i = (next m s) 0"
proof -
  have "∃ i. (s |_s i) = (next m s)"
  proof (induct m)
    have "s |_s 0 = next 0 s" by simp
    thus "∃ i. (s |_s i) = (next 0 s)" ..
  next
    fix m
    assume a1: "∃ i. (s |_s i) = (next m s)"
    then obtain i where a1': "(s |_s i) = (next m s)" ..
    have "next (Suc m) s = nextsuffix (next m s)" by auto
    hence "next (Suc m) s = (next m s) |_s (nextnat (next m s))" by (simp add: nextsuffix_def)
    hence "∃ i. next (Suc m) s = (next m s) |_s i" ..
    then obtain j where "next (Suc m) s = (next m s) |_s j" ..
    with a1' have "next (Suc m) s = (s |_s i) |_s j" by simp
    hence "next (Suc m) s = (s |_s (j+i))" by (simp add: suffix_plus)
    hence "(s |_s (j+i)) = next (Suc m) s" by simp
    thus "∃ i. (s |_s i) = (next (Suc m) s)" ..
  qed
  then obtain i where "(s |_s i) = (next m s)" ..
  hence "(s |_s i) 0 = (next m s) 0" by auto
  hence "s i = (next m s) 0" by (auto simp add: suffix_def)
  thus ?thesis ..
qed

subsubsection "Properties of @{term collapse}"

lemma emptyseq_collapse_eq: assumes A1: "emptyseq s" shows "♮ s = s"
proof (unfold collapse_def, rule ext)
  fix n
  from A1 have "next n s = s" by (rule next_empty)
  moreover
  from A1 have "s n = s 0" by (simp add: emptyseq_def)
  ultimately
  show "(next n s) 0 = s n" by simp
qed

lemma empty_collapse_empty: 
  assumes H: "emptyseq s" shows "emptyseq (♮ s)"
  using H by (simp add: emptyseq_collapse_eq)

lemma collapse_empty_empty: 
  assumes H: "emptyseq (♮ s)" shows "emptyseq s"
proof (rule ccontr)
  assume a1: "¬emptyseq s"
  from H have "∀ i. (next i s) 0 = s 0" by (simp add: collapse_def emptyseq_def)
  moreover
  from a1 have "(next (Suc 0) s) 0 ≠ s 0" by (rule notempty_nextnotzero)
  ultimately show "False" by blast
qed

lemma collapse_empty_iff_empty [simp]: "emptyseq (♮ s) = emptyseq s"
  by (auto elim: empty_collapse_empty collapse_empty_empty)

subsection "Similarity of Sequences"

text‹
 Since adding or removing stuttering steps does not change the validity
 of a stuttering-invarant formula, equality is often too strong,
 and the weaker equality \emph{up to stuttering} is sufficient.
 This is often called \emph{similarity} ($\approx$)
 of sequences in the literature, and is required to
 show that logical operators are stuttering invariant. This
 is mechanised as:
 ›

definition seqsimilar :: "('a seq) ==> ('a seq) ==> bool" (infixl ‹≈› 50)
where "σ ≈ τ ≡ (♮ σ) = (♮ τ)"

subsubsection "Properties of @{term seqsimilar}"

lemma seqsim_refl [iff]: "s ≈ s"
  by (simp add: seqsimilar_def)

lemma seqsim_sym: assumes H: "s ≈ t" shows "t ≈ s"
  using H by (simp add: seqsimilar_def)

lemma seqeq_imp_sim: assumes H: "s = t" shows "s ≈ t"
  using H by simp

lemma seqsim_trans [trans]: assumes h1: "s ≈ t" and h2: "t ≈ z" shows "s ≈ z" 
  using assms by (simp add: seqsimilar_def)

theorem sim_first: assumes H: "s ≈ t" shows "first s = first t"
proof -
  from H have "(♮ s) 0 = (♮ t) 0" by (simp add: seqsimilar_def)
  thus ?thesis by (simp add: collapse_def first_def)
qed

lemmas sim_first2 = sim_first[unfolded first_def]

lemma tail_sim_second: assumes H: "tail s ≈ tail t" shows "second s = second t"
proof -
  from H have "first (tail s) = first (tail t)" by (simp add: sim_first)
  thus "second s = second t" by (simp add: first_tail_second)
qed

lemma seqsimilarI:
  assumes 1: "first s = first t" and 2: "nextsuffix s ≈ nextsuffix t"
  shows "s ≈ t"
  unfolding seqsimilar_def collapse_def
proof
  fix n
  show "next n s 0 = next n t 0"
  proof (cases n)
    assume "n = 0"
    with 1 show ?thesis by (simp add: first_def)
  next
    fix m
    assume m: "n = Suc m"
    from 2 have "next m (nextsuffix s) 0 = next m (nextsuffix t) 0"
      unfolding seqsimilar_def collapse_def by (rule fun_cong)
    with m show ?thesis by (simp add: next_suffix_com)
  qed
qed

lemma seqsim_empty_empty: 
  assumes H1: "s ≈ t" and H2: "emptyseq s" shows "emptyseq t"
proof -
  from H2 have "emptyseq (♮ s)" by simp
  with H1 have "emptyseq (♮ t)" by (simp add: seqsimilar_def)
  thus ?thesis by simp
qed

lemma seqsim_empty_iff_empty:
  assumes H: "s ≈ t" shows "emptyseq s = emptyseq t"
proof
  assume "emptyseq s" with H show "emptyseq t" by (rule seqsim_empty_empty)
next
  assume t: "emptyseq t"
  from H have "t ≈ s" by (rule seqsim_sym)
  from this t show "emptyseq s" by (rule seqsim_empty_empty)
qed

lemma seq_empty_eq: 
  assumes H1: "s 0 = t 0" and H2: "emptyseq s" and H3: "emptyseq t"
  shows "s = t"
proof (rule ext)
  fix n
  from assms have "t n = s n" by (auto simp: emptyseq_def)
  thus "s n = t n" by simp
qed

lemma seqsim_notstutstep: 
  assumes H: "¬ (stutstep s n)" shows "(s |_s (Suc n)) ≈ nextsuffix (s |_s n)"
  using H by (simp add: notstutstep_nextsuffix1)

lemma stut_nextsuf_suc: 
  assumes H: "stutstep s n" shows "nextsuffix (s |_s n) = nextsuffix (s |_s (Suc n))"
proof (cases "emptyseq (s |_s n)")
  case True
  hence g1: "nextsuffix (s |_s n) = (s |_s n)" by (simp add: nextsuffix_def nextnat_def)
  from True have g2: "nextsuffix (s |_s Suc n) = (s |_s Suc n)"
    by (simp add: suc_empty nextsuffix_def nextnat_def)
  have "(s |_s n) = (s |_s Suc n)"
  proof
    fix x
    from True have "s (x + n) = s (0 + n)" "s (Suc x + n) = s (0 + n)"
      unfolding emptyseq_def suffix_def by (blast+)
    thus "(s |_s n) x = (s |_s Suc n) x" by (simp add: suffix_def)
  qed
  with g1 g2 show ?thesis by auto
next
  case False
  with H have "(nextnat (s |_s n)) = Suc (nextnat (s |_s Suc n))"
    by (simp add: stutstep_notempty_sucnextnat)
  thus ?thesis
    by (simp add: nextsuffix_def suffix_plus)
qed

lemma seqsim_suffix_seqsim:
  assumes H: "s ≈ t" shows "nextsuffix s ≈ nextsuffix t"
  unfolding seqsimilar_def collapse_def
proof
  fix n
  from H have "(next (Suc n) s) 0 = (next (Suc n) t) 0"
    unfolding seqsimilar_def collapse_def by (rule fun_cong)
  thus "next n (nextsuffix s) 0 = next n (nextsuffix t) 0"
    by (simp add: next_suffix_com)
qed

lemma seqsim_stutstep:
  assumes H: "stutstep s n" shows "(s |_s (Suc n)) ≈ (s |_s n)" (is "?sn ≈ ?s")
  unfolding seqsimilar_def collapse_def
proof
  fix m
  show "next m (s |_s Suc n) 0 = next m (s |_s n) 0"
  proof (cases m)
    assume "m=0"
    with H show ?thesis by (simp add: suffix_def stutstep_def)
  next
    fix k
    assume m: "m = Suc k"
    with H  have "next m (s |_s Suc n) = next k (nextsuffix (s |_s n))"
      by (simp add: stut_nextsuf_suc next_suffix_com)
    moreover from m have "next m (s |_s n) = next k (nextsuffix (s |_s n))" 
      by (simp add: next_suffix_com)
    ultimately show "next m (s |_s Suc n) 0 = next m (s |_s n) 0" by simp
  qed
qed

lemma addfeqstut: "stutstep ((first t) ## t) 0"
  by (simp add: first_def stutstep_def app_def suffix_def)

lemma addfeqsim: "((first t) ## t) ≈ t"
proof -
  have "stutstep ((first t) ## t) 0" by (rule addfeqstut)
  hence "(((first t) ## t) |_s (Suc 0)) ≈ (((first t) ## t) |_s 0)" by (rule seqsim_stutstep)
  hence "tail ((first t) ## t) ≈ ((first t) ## t)" by (simp add: suffix_def tail_def)
  hence "t ≈ ((first t) ## t)" by (simp add: tail_def app_def suffix_def)
  thus ?thesis by (rule seqsim_sym)
qed

lemma addfirststut:
  assumes H: "first s = second s" shows "s ≈ tail s"
proof -
  have g1: "(first s) ## (tail s) = s" by (rule seq_app_first_tail)
  from H have "(first s) = first (tail s)"
    by (simp add: first_def second_def tail_def suffix_def)
  hence "(first s) ## (tail s) ≈ (tail s)" by (simp add: addfeqsim)
  with g1 show ?thesis by simp
qed

lemma app_seqsimilar:
  assumes h1: "s ≈ t" shows "(x ## s) ≈ (x ## t)"
proof (cases "stutstep (x ## s) 0")
  case True
  from h1 have "first s = first t" by (rule sim_first)
  with True have a2: "stutstep (x ## t) 0"
    by (simp add: stutstep_def first_def app_def)
  from True have "((x ## s) |_s (Suc 0)) ≈ ((x ## s) |_s 0)" by (rule seqsim_stutstep)
  hence "tail (x ## s) ≈ (x ## s)" by (simp add: tail_def suffix_def)
  hence g1: "s ≈ (x ## s)" by (simp add: app_def tail_def suffix_def)
  from a2 have "((x ## t) |_s (Suc 0)) ≈ ((x ## t) |_s 0)" by (rule seqsim_stutstep)
  hence "tail (x ## t) ≈ (x ## t)" by (simp add: tail_def suffix_def)
  hence g2: "t ≈ (x ## t)" by (simp add: app_def tail_def suffix_def)
  from h1 g2 have "s ≈ (x ## t)" by (rule seqsim_trans)
  from this[THEN seqsim_sym] g1 show "(x ## s) ≈ (x ## t)"
    by (rule seqsim_sym[OF seqsim_trans])
next
  case False
  from h1 have "first s = first t" by (rule sim_first)
  with False have a2: "¬ stutstep (x ## t) 0"
    by (simp add: stutstep_def first_def app_def)
  from False have "((x ## s) |_s (Suc 0)) ≈ nextsuffix ((x ## s) |_s 0)"
    by (rule seqsim_notstutstep)
  hence "(tail (x ## s)) ≈ nextsuffix (x ## s)" 
    by (simp add: tail_def)
  hence g1: "s ≈ nextsuffix (x ## s)" by (simp add: seq_app_tail)
  from a2 have "((x ## t) |_s (Suc 0)) ≈ nextsuffix ((x ## t) |_s 0)"
    by (rule seqsim_notstutstep)
  hence "(tail (x ## t)) ≈ nextsuffix (x ## t)" by (simp add: tail_def)
  hence g2: "t ≈ nextsuffix (x ## t)" by (simp add: seq_app_tail)
  with h1 have "s ≈ nextsuffix (x ## t)" by (rule seqsim_trans)
  from this[THEN seqsim_sym] g1 have g3: "nextsuffix (x ## s) ≈ nextsuffix (x ## t)"
    by (rule seqsim_sym[OF seqsim_trans])
  have "first (x ## s) = first (x ## t)" by (simp add: first_def app_def)
  from this g3 show ?thesis by (rule seqsimilarI)
qed

text ‹
 If two sequences are similar then for any suffix of one of them there
 exists a similar suffix of the other one. We will prove a stronger
 result below.
 ›

lemma simstep_disj1: assumes H: "s ≈ t" shows "∃ m. ((s |_s n) ≈ (t |_s m))"
proof (induct n)
  from H have "((s |_s 0) ≈ (t |_s 0))" by auto
  thus "∃ m. ((s |_s 0) ≈ (t |_s m))" ..
next
  fix n
  assume "∃ m. ((s |_s n) ≈ (t |_s m))"
  then obtain m where a1': "(s |_s n) ≈ (t |_s m)" ..
  show "∃ m. ((s |_s (Suc n)) ≈ (t |_s m))"
  proof (cases "stutstep s n")
    case True
    hence "(s |_s (Suc n)) ≈ (s |_s n)" by (rule seqsim_stutstep)
    from this a1' have "((s |_s (Suc n)) ≈ (t |_s m))" by (rule seqsim_trans)
    thus ?thesis ..
  next
    case False
    hence "(s |_s (Suc n)) ≈ nextsuffix (s |_s n)" by (rule seqsim_notstutstep)
    moreover
    from a1' have "nextsuffix (s |_s n) ≈ nextsuffix (t |_s m)" 
      by (simp add: seqsim_suffix_seqsim)
    ultimately have "(s |_s (Suc n)) ≈ nextsuffix (t |_s m)" by (rule seqsim_trans)
    hence "(s |_s (Suc n)) ≈ t |_s (m + (nextnat (t |_s m)))"
      by (simp add: nextsuffix_def suffix_plus_com)
    thus "∃ m. (s |_s (Suc n)) ≈ t |_s m" ..
  qed
qed

lemma nextnat_le_seqsim: 
  assumes n: "n < nextnat s" shows "s ≈ (s |_s n)"
proof (cases "emptyseq s")
  case True   ― ‹case impossible›
  with n show ?thesis by (simp add: nextnat_def)
next
  case False
  from n show ?thesis
  proof (induct n)
    show "s ≈ (s |_s 0)" by simp
  next
    fix n
    assume a2: "n < nextnat s ==> s ≈ (s |_s n)" and a3: "Suc n < nextnat s"
    from a3 have g1: "s (Suc n) = s 0" by (rule nextnat_le_unch)
    from a3 have a3': "n < nextnat s" by simp
    hence "s n = s 0" by (rule nextnat_le_unch)
    with g1 have "stutstep s n" by (simp add: stutstep_def)
    hence g2: "(s |_s n) ≈ (s |_s (Suc n))" by (rule seqsim_stutstep[THEN seqsim_sym])
    with a3' a2 show "s ≈ (s |_s (Suc n))" by (auto elim: seqsim_trans)
  qed
qed

lemma seqsim_prev_nextnat: "s ≈ s |_s ((nextnat s) - 1)"
proof (cases "emptyseq s")
  case True
  hence "s |_s ((nextnat s)-(1::nat)) = s |_s 0" by (simp add: nextnat_def)
  thus ?thesis by simp
next
  case False
  hence "nextnat s > 0" by (rule nextnat_empty_gzero)
  thus ?thesis by (simp add: nextnat_le_seqsim)
qed

text ‹
 Given a suffix ‹s |_s n› of some sequence ‹s› that is
 similar to some suffix ‹t |_s m› of sequence ‹t›, there
 exists some suffix ‹t |_s m'› of ‹t› such that
 ‹s |_s n› and ‹t |_s m'› are similar and also
 ‹s |_s (n+1)› is similar to either ‹t |_s m'› or to
 ‹t |_s (m'+1)›.
 ›

lemma seqsim_suffix_suc:
  assumes H: "s |_s n ≈ t |_s m"
  shows "∃m'. s |_s n ≈ t |_s m' ∧ ((s |_s Suc n ≈ t |_s Suc m') ∨ (s |_s Suc n ≈ t |_s m'))"
proof (cases "stutstep s n")
  case True
  hence "s |_s Suc n ≈ s |_s n" by (rule seqsim_stutstep)
  from this H have "s |_s Suc n ≈ t |_s m" by (rule seqsim_trans)
  with H show ?thesis by blast
next
  case False
  hence "¬ emptyseq (s |_s n)" by (rule stutnempty)
  with H have a2: "¬ emptyseq (t |_s m)" by (simp add: seqsim_empty_iff_empty)
  hence g4: "nextsuffix (t |_s m) = (t |_s m) |_s Suc (nextnat (t |_s m) - 1)"
    by (simp add: nextnat_empty_gzero nextsuffix_def)
  have g3: "(t |_s m) ≈ (t |_s m) |_s (nextnat (t |_s m) - 1)"
    by (rule seqsim_prev_nextnat)
  with H have G1: "s |_s n ≈ (t |_s m) |_s (nextnat (t |_s m) - 1)"
    by (rule seqsim_trans)
  from False have G1': "(s |_s Suc n) = nextsuffix (s |_s n)" 
    by (rule notstutstep_nextsuffix1[THEN sym])
  from H have "nextsuffix (s |_s n) ≈ nextsuffix (t |_s m)"
    by (rule seqsim_suffix_seqsim)
  with G1 G1' g4
  have "s |_s n ≈ t |_s (m + (nextnat (t |_s m) - 1))
      ∧ s |_s (Suc n) ≈ t |_s Suc (m + (nextnat (t |_s m) - 1))"
    by (simp add: suffix_plus_com)
  thus ?thesis by blast
qed

text ‹
 The following main result about similar sequences shows that if
 ‹s ≈ t› holds then for any suffix ‹s |_s n› of ‹s›
 there exists a suffix ‹t |_s m› such that
 \begin{itemize}
 \item ‹s |_s n› and ‹t |_s m› are similar, and
 \item ‹s |_s (n+1)› is similar to either ‹t |_s (m+1)›
 or ‹t |_s m›.
 \end{itemize}
 The idea is to pick the largest ‹m› such that ‹s |_s n ≈ t |_s m›
 (or some such ‹m› if ‹s |_s n› is empty).
 ›

theorem sim_step: 
  assumes H: "s ≈ t" 
  shows "∃ m. s |_s n ≈ t |_s m ∧
              ((s |_s Suc n ≈ t |_s Suc m) ∨ (s |_s Suc n ≈ t |_s m))"
    (is "∃m. ?Sim n m")
proof (induct n)
  from H have "s |_s 0 ≈ t |_s 0" by simp
  thus "∃ m. ?Sim 0 m" by (rule seqsim_suffix_suc)
next
  fix n
  assume "∃ m. ?Sim n m"
  hence "∃k. s |_s Suc n ≈ t |_s k" by blast
  thus "∃ m. ?Sim (Suc n) m" by (blast dest: seqsim_suffix_suc)
qed

end