Theory Stuttering_Equivalence.PLTL

theory PLTL
  imports Main LTL.LTL Samplers StutterEquivalence
begin

section ‹Stuttering Invariant LTL Formulas›

text ‹
  We show that the next-free fragment of propositional linear-time
  temporal logic PLTL is invariant to finite stuttering.
›

subsection ‹Finite Conjunctions and Disjunctions in PLTL›

(* It would be tempting to define these operators as follows:

definition OR where "OR Φ = Finite_Set.fold or false Φ"
definition AND where "AND Φ = Finite_Set.fold and true Φ"

However, this would only work if "or" and "and" were left-commutative,
which they are not (syntactically). We must therefore resort to
the more general fold_graph predicate, effectively picking a
conjunction (or disjunction) in arbitrary order. 

An alternative would be to define these generalized operators
over lists of formulas, but working with sets is more natural
in the following.
*)

definition OR where "OR Φ  SOME φ. fold_graph Or_ltlp False_ltlp Φ φ"

definition AND where "AND Φ  SOME φ. fold_graph And_ltlp True_ltlp Φ φ"

lemma fold_graph_OR: "finite Φ  fold_graph Or_ltlp False_ltlp Φ (OR Φ)"
  unfolding OR_def by (rule someI2_ex[OF finite_imp_fold_graph])

lemma fold_graph_AND: "finite Φ  fold_graph And_ltlp True_ltlp Φ (AND Φ)"
  unfolding AND_def by (rule someI2_ex[OF finite_imp_fold_graph])

lemma holds_of_OR [simp]: 
  assumes fin: "finite (Φ::'a pltl set)"
  shows "(σ p OR Φ) = (φΦ. σ p φ)"
proof -
  {
    fix ψ::"'a pltl"
    assume "fold_graph Or_ltlp False_ltlp Φ ψ"
    hence "(σ p ψ) = (φΦ. σ p φ)"
      by (rule fold_graph.induct) auto
  }
  with fold_graph_OR[OF fin] show ?thesis by simp
qed

lemma holds_of_AND [simp]: 
  assumes fin: "finite (Φ::'a pltl set)"
  shows "(σ p AND Φ) = (φΦ. σ p φ)"
proof -
  {
    fix ψ::"'a pltl"
    assume "fold_graph And_ltlp True_ltlp Φ ψ"
    hence "(σ p ψ) = (φΦ. σ p φ)"
      by (rule fold_graph.induct) auto
  }
  with fold_graph_AND[OF fin] show ?thesis by simp
qed

subsection ‹Next-Free PLTL Formulas›

text ‹
  A PLTL formula is called \emph{next-free} if it does not contain any
  subformula.
›

fun next_free :: "'a pltl  bool"
where
  "next_free falsep = True"
| "next_free (atomp(p)) = True"
| "next_free (φ impliesp ψ) = (next_free φ  next_free ψ)"
| "next_free (Xp φ) = False"
| "next_free (φ Up ψ) = (next_free φ  next_free ψ)"

lemma next_free_not [simp]: 
  "next_free (notp φ) = next_free φ"
  by (simp add: Not_ltlp_def)

lemma next_free_true [simp]: 
  "next_free truep"
  by (simp add: True_ltlp_def)

lemma next_free_or [simp]: 
  "next_free (φ orp ψ) = (next_free φ  next_free ψ)"
  by (simp add: Or_ltlp_def)

lemma next_free_and [simp]: "next_free (φ andp ψ) = (next_free φ  next_free ψ)"
  by (simp add: And_ltlp_def)

lemma next_free_eventually [simp]: 
  "next_free (Fp φ) = next_free φ"
  by (simp add: Eventually_ltlp_def)

lemma next_free_always [simp]: 
  "next_free (Gp φ) = next_free φ"
  by (simp add: Always_ltlp_def)

lemma next_free_release [simp]:
  "next_free (φ Rp ψ) = (next_free φ  next_free ψ)"
  by (simp add: Release_ltlp_def)

lemma next_free_weak_until [simp]:
  "next_free (φ Wp ψ) = (next_free φ  next_free ψ)"
  by (auto simp: WeakUntil_ltlp_def)

lemma next_free_strong_release [simp]:
  "next_free (φ Mp ψ) = (next_free φ  next_free ψ)"
  by (auto simp: StrongRelease_ltlp_def)

lemma next_free_OR [simp]: 
  assumes fin: "finite (Φ::'a pltl set)"
  shows "next_free (OR Φ) = (φΦ. next_free φ)"
proof -
  {
    fix ψ::"'a pltl"
    assume "fold_graph Or_ltlp False_ltlp Φ ψ"
    hence "next_free ψ = (φΦ. next_free φ)"
      by (rule fold_graph.induct) auto
  }
  with fold_graph_OR[OF fin] show ?thesis by simp
qed

lemma next_free_AND [simp]: 
  assumes fin: "finite (Φ::'a pltl set)"
  shows "next_free (AND Φ) = (φΦ. next_free φ)"
proof -
  {
    fix ψ::"'a pltl"
    assume "fold_graph And_ltlp True_ltlp Φ ψ"
    hence "next_free ψ = (φΦ. next_free φ)"
      by (rule fold_graph.induct) auto
  }
  with fold_graph_AND[OF fin] show ?thesis by simp
qed


subsection ‹Stuttering Invariance of PLTL Without ``Next''›

text ‹
  A PLTL formula is \emph{stuttering invariant} if for any stuttering equivalent
  state sequences σ ≈ τ›, the formula holds of σ› iff it
  holds of τ›.
›

definition stutter_invariant where
  "stutter_invariant φ = (σ τ. (σ  τ)  (σ p φ) = (τ p φ))"

text ‹
  Since stuttering equivalence is symmetric, it is enough to show an
  implication in the above definition instead of an equivalence.
›

lemma stutter_invariantI [intro!]:
  assumes "σ τ. σ  τ; σ p φ  τ p φ"
  shows "stutter_invariant φ"
proof -
  {
    fix σ τ
    assume st: "σ  τ" and f: "σ p φ"
    hence "τ p φ" by (rule assms)
  }
moreover
  {
    fix σ τ
    assume st: "σ  τ" and f: "τ p φ"
    from st have "τ  σ" by (rule stutter_equiv_sym)
    from this f have "σ p φ" by (rule assms)
  }
ultimately show ?thesis by (auto simp: stutter_invariant_def)
qed

lemma stutter_invariantD [dest]:
  assumes "stutter_invariant φ" and "σ  τ"
  shows "(σ p φ) = (τ p φ)"
  using assms by (auto simp: stutter_invariant_def)

text ‹
  We first show that next-free PLTL formulas are indeed stuttering invariant.
  The proof proceeds by straightforward induction on the syntax of PLTL formulas.
›
theorem next_free_stutter_invariant:
  "next_free φ  stutter_invariant (φ::'a pltl)"
proof (induct "φ")
    show "stutter_invariant falsep" by auto
next
  fix p :: "'a  bool"
  show "stutter_invariant (atomp(p))"
  proof
    fix σ τ
    assume "σ  τ" "σ p atomp(p)"
    thus "τ p atomp(p)" by (simp add: stutter_equiv_0)
  qed
next
  fix φ ψ :: "'a pltl"
  assume ih: "next_free φ  stutter_invariant φ"
             "next_free ψ  stutter_invariant ψ"
  assume "next_free (φ impliesp ψ)"
  with ih show "stutter_invariant (φ impliesp ψ)" by auto
next
  fix φ :: "'a pltl"
  assume "next_free (Xp φ)"  ― ‹hence contradiction›
  thus "stutter_invariant (Xp φ)" by simp
next
  fix φ ψ :: "'a pltl"
  assume ih: "next_free φ  stutter_invariant φ"
             "next_free ψ  stutter_invariant ψ"
  assume "next_free (φ Up ψ)"
  with ih have stinv: "stutter_invariant φ" "stutter_invariant ψ" by auto
  show "stutter_invariant (φ Up ψ)"
  proof
    fix σ τ
    assume st: "σ  τ" and unt: "σ p φ Up ψ"
    from unt obtain m
      where 1: "σ[m..] p ψ" and 2: "j<m. (σ[j..] p φ)" by auto
    from st obtain n
      where 3: "(σ[m..])  (τ[n..])" and 4: "i<n. j<m. (σ[j..])  (τ[i..])"
      by (rule stutter_equiv_suffixes_right)
    from 1 3 stinv have "τ[n..] p ψ" by auto
    moreover
    from 2 4 stinv have "i<n. (τ[i..] p φ)" by force
    ultimately show "τ p φ Up ψ" by auto
  qed
qed


subsection ‹Atoms, Canonical State Sequences, and Characteristic Formulas›

text ‹
  We now address the converse implication: any stutter invariant PLTL
  formula φ› can be equivalently expressed by a next-free formula.
  The construction of that formula requires attention to the atomic
  formulas that appear in φ›. We will also prove that the
  next-free formula does not need any new atoms beyond those present
  in φ›.

  The following function collects the atoms (of type 'a ⇒ bool›)
  of a PLTL formula.
›


lemma atoms_pltl_OR [simp]:
  assumes fin: "finite (Φ::'a pltl set)"
  shows "atoms_pltl (OR Φ) = (φΦ. atoms_pltl φ)"
proof -
  {
    fix ψ::"'a pltl"
    assume "fold_graph Or_ltlp False_ltlp Φ ψ"
    hence "atoms_pltl ψ = (φΦ. atoms_pltl φ)"
      by (rule fold_graph.induct) auto
  }
  with fold_graph_OR[OF fin] show ?thesis by simp
qed

lemma atoms_pltl_AND [simp]:
  assumes fin: "finite (Φ::'a pltl set)"
  shows "atoms_pltl (AND Φ) = (φΦ. atoms_pltl φ)"
proof -
  {
    fix ψ::"'a pltl"
    assume "fold_graph And_ltlp True_ltlp Φ ψ"
    hence "atoms_pltl ψ = (φΦ. atoms_pltl φ)"
      by (rule fold_graph.induct) auto
  }
  with fold_graph_AND[OF fin] show ?thesis by simp
qed

text ‹
  Given a set of atoms A› as above, we say that two states
  are A›-similar if they agree on all atoms in A›.
  Two state sequences σ› and τ› are A›-similar
  if corresponding states are A›-equal.
›

definition state_sim :: "['a, ('a  bool) set, 'a]  bool" 
  ("_ ~_~ _" [70,100,70] 50) where
  "s ~A~ t = (pA. p s  p t)"

definition seq_sim :: "[nat  'a, ('a  bool) set, nat  'a]  bool"
  ("_ _ _" [70,100,70] 50)  where
  "σ A τ = (n. (σ n) ~A~ (τ n))"

text ‹
  These relations are (indexed) equivalence relations. Moreover
  s ~A~ t› implies s ~B~ t› for B ⊆ A›,
  and similar for σ ≃A≃ τ› and σ ≃B≃ τ›.
›

lemma state_sim_refl [simp]: "s ~A~ s"
  by (simp add: state_sim_def)

lemma state_sim_sym: "s ~A~ t  t ~A~ s"
  by (auto simp: state_sim_def)

lemma state_sim_trans[trans]: "s ~A~ t  t ~A~ u  s ~A~ u"
  unfolding state_sim_def by blast

lemma state_sim_mono:
  assumes "s ~A~ t" and "B  A"
  shows "s ~B~ t"
  using assms unfolding state_sim_def by auto

lemma seq_sim_refl [simp]: "σ A σ"
  by (simp add: seq_sim_def)

lemma seq_sim_sym: "σ A τ  τ A σ"
  by (auto simp: seq_sim_def state_sim_sym)

lemma seq_sim_trans[trans]: "ρ A σ  σ A τ  ρ A τ"
  unfolding seq_sim_def by (blast intro: state_sim_trans)

lemma seq_sim_mono:
  assumes "σ A τ" and "B  A"
  shows "σ B τ"
  using assms unfolding seq_sim_def by (blast intro: state_sim_mono)

text ‹
  State sequences that are similar w.r.t. the atoms of a PLTL formula
  evaluate that formula to the same value.  
›

lemma pltl_seq_sim: "σ  atoms_pltl φ  τ  (σ p φ) = (τ p φ)"
  (is "?sim σ φ τ  ?P σ φ τ")
proof (induct φ arbitrary: σ τ)
  fix σ τ
  show "?P σ falsep τ" by simp
next
  fix p σ τ
  assume "?sim σ (atomp(p)) τ" thus "?P σ (atomp(p)) τ"
    by (auto simp: seq_sim_def state_sim_def)
next
  fix φ ψ σ τ
  assume ih: "σ τ. ?sim σ φ τ  ?P σ φ τ" 
             "σ τ. ?sim σ ψ τ  ?P σ ψ τ"
     and sim: "?sim σ (φ impliesp ψ) τ"
  from sim have "?sim σ φ τ" "?sim σ ψ τ"
    by (auto elim: seq_sim_mono)
  with ih show "?P σ (φ impliesp ψ) τ" by simp
next
  fix φ σ τ
  assume ih: "σ τ. ?sim σ φ τ  ?P σ φ τ"
     and sim: "σ  atoms_pltl (Xp φ)  τ"
  from sim have "(σ[1..])  atoms_pltl φ  (τ[1..])"
    by (auto simp: seq_sim_def)
  with ih show "?P σ (Xp φ) τ" by auto
next
  fix φ ψ σ τ
  assume ih: "σ τ. ?sim σ φ τ  ?P σ φ τ" 
             "σ τ. ?sim σ ψ τ  ?P σ ψ τ"
     and sim: "?sim σ (φ Up ψ) τ"
  from sim have "i. (σ[i..])  atoms_pltl φ  (τ[i..])" "j. (σ[j..])  atoms_pltl ψ  (τ[j..])"
    by (auto simp: seq_sim_def state_sim_def)
  with ih have "i. ?P (σ[i..]) φ (τ[i..])" "j. ?P (σ[j..]) ψ (τ[j..])"
    by blast+
  thus "?P σ (φ Up ψ) τ"
    by (meson semantics_pltl.simps(5))
qed

text ‹
  The following function picks an arbitrary representative among
  A›-similar states. Because the choice is functional,
  any two A›-similar states are mapped to the same state.
›

definition canonize where
  "canonize A s  SOME t. t ~A~ s"

lemma canonize_state_sim: "canonize A s ~A~ s"
  unfolding canonize_def by (rule someI, rule state_sim_refl)

lemma canonize_canonical:
  assumes st: "s ~A~ t"
  shows "canonize A s = canonize A t"
proof -
  from st have "u. (u ~A~s) = (u ~A~ t)"
    by (auto elim: state_sim_sym state_sim_trans)
  thus ?thesis unfolding canonize_def by simp
qed

lemma canonize_idempotent:
  "canonize A (canonize A s) = canonize A s"
  by (rule canonize_canonical[OF canonize_state_sim])

text ‹
  In a canonical state sequence, any two A›-similar states
  are in fact equal.
›

definition canonical_sequence where
  "canonical_sequence A σ  m (n::nat). σ m ~A~ σ n  σ m = σ n"

text ‹
  Every suffix of a canonical sequence is canonical, as is any
  (sampled) subsequence, in particular any stutter-sampling.
›

lemma canonical_suffix:
  "canonical_sequence A σ  canonical_sequence A (σ[k..])"
  by (auto simp: canonical_sequence_def)

lemma canonical_sampled:
  "canonical_sequence A σ  canonical_sequence A (σ  f)"
  by (auto simp: canonical_sequence_def)

lemma canonical_reduced:
  "canonical_sequence A σ  canonical_sequence A (σ)"
  unfolding stutter_reduced_def by (rule canonical_sampled)

text ‹
  For any sequence σ› there exists a canonical
  A›-similar sequence τ›. Such a τ›
  can be obtained by canonizing all states of σ›.
›

lemma canonical_exists:
  obtains τ where "τ A σ" "canonical_sequence A τ"
proof -
  have "(canonize A  σ) A σ"
    by (simp add: seq_sim_def canonize_state_sim)
  moreover
  have "canonical_sequence A (canonize A  σ)"
    by (auto simp: canonical_sequence_def canonize_idempotent
             dest: canonize_canonical)
  ultimately
  show ?thesis using that by blast
qed

text ‹
  Given a state s› and a set A› of atoms, we define
  the characteristic formula of s› as the conjunction of
  all atoms in A› that hold of s› and the negation of
  the atoms in A› that do not hold of s›.
›

definition characteristic_formula where
  "characteristic_formula A s 
   ((AND { atomp(p) | p . p  A  p s }) andp (AND { notp (atomp(p)) | p . p  A  ¬(p s) }))"

lemma characteristic_holds: 
  "finite A  σ p characteristic_formula A (σ 0)"
  by (auto simp: characteristic_formula_def)

lemma characteristic_state_sim:
  assumes fin: "finite A"
  shows "(σ 0 ~A~ τ 0) = (τ p characteristic_formula A (σ (0::nat)))"
proof
  assume sim: "σ 0 ~A~ τ 0"
  {
    fix p
    assume "p  A"
    with sim have "p (τ 0) = p (σ 0)" by (auto simp: state_sim_def)
  }
  with fin show "τ p characteristic_formula A (σ 0)"
    by (auto simp: characteristic_formula_def) (blast+)
next
  assume "τ p characteristic_formula A (σ 0)"
  with fin show "σ 0 ~A~ τ 0"
    by (auto simp: characteristic_formula_def state_sim_def)
qed


subsection ‹Stuttering Invariant PLTL Formulas Don't Need Next›

text ‹
  The following is the main lemma used in the proof of the
  completeness theorem: for any PLTL formula φ› there
  exists a next-free formula ψ› such that the two
  formulas evaluate to the same value over stutter-free and
  canonical sequences (w.r.t. some A ⊇ atoms_pltl φ›).
›

lemma ex_next_free_stutter_free_canonical:
  assumes A: "atoms_pltl φ  A" and fin: "finite A"
  shows "ψ. next_free ψ  atoms_pltl ψ  A 
             (σ. stutter_free σ  canonical_sequence A σ  (σ p ψ) = (σ p φ))"
    (is "ψ. ?P φ ψ")
using A proof (induct φ)
  txt ‹The cases of false› and atomic formulas are trivial.›
  have "?P falsep falsep" by auto
  thus "ψ. ?P falsep ψ" ..
next
  fix p
  assume "atoms_pltl (atomp(p))  A"
  hence "?P (atomp(p)) (atomp(p))" by auto
  thus "ψ. ?P (atomp(p)) ψ" ..
next
  txt ‹Implication is easy, using the induction hypothesis.›
  fix φ ψ
  assume "atoms_pltl φ  A  φ'. ?P φ φ'"
     and "atoms_pltl ψ  A  ψ'. ?P ψ ψ'"
     and "atoms_pltl (φ impliesp ψ)  A"
  then obtain φ' ψ' where "?P φ φ'" "?P ψ ψ'" by auto
  hence "?P (φ impliesp ψ) (φ' impliesp ψ')" by auto
  thus "χ. ?P (φ impliesp ψ) χ" ..
next
  txt ‹The case of until› follows similarly.›
  fix φ ψ
  assume "atoms_pltl φ  A  φ'. ?P φ φ'"
     and "atoms_pltl ψ  A  ψ'. ?P ψ ψ'"
     and "atoms_pltl (φ Up ψ)  A"
  then obtain φ' ψ' where 1: "?P φ φ'" and 2: "?P ψ ψ'" by auto
  {
    fix σ
    assume sigma: "stutter_free σ" "canonical_sequence A σ"
    hence "k. stutter_free (σ[k..])" "k. canonical_sequence A (σ[k..])"
      by (auto simp: stutter_free_suffix canonical_suffix)
    with 1 2 
    have "k. (σ[k..] p φ') = (σ[k..] p φ)"
     and "k. (σ[k..] p ψ') = (σ[k..] p ψ)"
      by (blast+)
    hence "(σ p φ' Up ψ') = (σ p φ Up ψ)"
      by auto
  }
  with 1 2 have "?P (φ Up ψ) (φ' Up ψ')" by auto
  thus "χ. ?P (φ Up ψ) χ" ..
next
  txt ‹The interesting case is the one of the next›-operator.›
  fix φ
  assume ih: "atoms_pltl φ  A  ψ. ?P φ ψ" and at: "atoms_pltl (Xp φ)  A"
  then obtain ψ where psi: "?P φ ψ" by auto
  txt ‹A valuation (over A›) is a set val ⊆ A› of atoms. We
    define some auxiliary notions: the valuation corresponding to a state and
    the characteristic formula for a valuation. Finally, we define the formula
    psi'› that we will prove to be equivalent to Xp φ› over
    the stutter-free and canonical sequence σ›.›
  define stval where "stval = (λs. { p  A . p s })"
  define chi where "chi = (λval. ((AND {atomp(p) | p . p  val}) andp
                        (AND {notp (atomp(p)) | p . p  A - val})))"
  define psi' where "psi' = ((ψ andp (OR {Gp (chi val) | val . val  A })) orp
                  (OR {(chi val) andp ((chi val) Up ( ψ andp (chi val'))) | val val'.
                        val  A  val'  A  val'  val }))"
        (is "_ = (( _ andp (OR ?ALW)) orp (OR ?UNT))")

  have "s. {notp (atomp(p)) | p . p  A - stval s}
           = {notp (atomp(p)) | p . p  A  ¬(p s)}"
    by (auto simp: stval_def)
  hence chi1: "s. chi (stval s) = characteristic_formula A s"
    by (auto simp: chi_def stval_def characteristic_formula_def)
  {
    fix val τ
    assume val: "val  A" and tau: "τ p chi val"
    with fin have "val = stval (τ 0)"
      by (auto simp: stval_def chi_def finite_subset)
  }
  note chi2 = this

  have "?UNT  (λ(val,val'). (chi val) andp ((chi val) Up (ψ andp (chi val'))))
               ` (Pow A × Pow A)"
    (is "_  ?S")
    by auto
  with fin have fin_UNT: "finite ?UNT"
    by (auto simp: finite_subset)

  have nf: "next_free psi'"
  proof -
    from fin have "val. val  A  next_free (chi val)"
      by (auto simp: chi_def finite_subset)
    with fin fin_UNT psi show ?thesis
      by (force simp: psi'_def finite_subset)
  qed

  have atoms_pltl: "atoms_pltl psi'  A"
  proof -
    from fin have at_chi: "val. val  A  atoms_pltl (chi val)  A"
      by (auto simp: chi_def finite_subset)
    with fin psi have at_alw: "atoms_pltl (ψ andp (OR ?ALW))  A"
      by auto blast?    (** FRAGILE: auto leaves trivial goal about subset **)
    from fin fin_UNT psi at_chi have "atoms_pltl (OR ?UNT)  A"
      by auto (blast+)? (** FRAGILE: even more left-over goals here **)
    with at_alw show ?thesis by (auto simp: psi'_def)
  qed

  {
    fix σ
    assume st: "stutter_free σ" and can: "canonical_sequence A σ"
    have "(σ p Xp φ) = (σ p psi')"
    proof (cases "σ (Suc 0) = σ 0")
      case True
      txt ‹In the case of a stuttering transition at the beginning, we must have
        infinite stuttering, and the first disjunct of psi'› holds,
        whereas the second does not.›
      {
        fix n
        have "σ n = σ 0"
        proof (cases n)
          case 0 thus ?thesis by simp
        next
          case Suc
          hence "n > 0" by simp
          with True st show ?thesis unfolding stutter_free_def by blast
        qed
      }
      note alleq = this
      have suffix: "n. σ[n..] = σ"
      proof (rule ext)
        fix n i
        have "(σ[n..]) i = σ 0" by (auto intro: alleq)
        moreover have "σ i = σ 0" by (rule alleq)
        ultimately show "(σ[n..]) i = σ i" by simp
      qed
      with st can psi have 1: "(σ p Xp φ) = (σ p ψ)" by simp

      from fin have "σ p chi (stval (σ 0))" by (simp add: chi1 characteristic_holds)
      with suffix have "σ p Gp (chi (stval (σ 0)))" (is "_ p ?alw") by simp
      moreover have "?alw  ?ALW" by (auto simp: stval_def)
      ultimately have 2: "σ p OR ?ALW"
        using fin by (auto simp: finite_subset simp del: semantics_pltl_sugar)

      have 3: "¬(σ p OR ?UNT)"
      proof
        assume unt: "σ p OR ?UNT"
        with fin_UNT obtain val val' k where
          val: "val  A" "val'  A" "val'  val" and
          now: "σ p chi val" and k: "σ[k..] p chi val'"
          by auto (blast+)?  (* FRAGILE: similar as above *)
        from val  A now have "val = stval (σ 0)" by (rule chi2)
        moreover
        from val'  A k suffix have "val' = stval (σ 0)" by (simp add: chi2)
        moreover note val'  val
        ultimately show "False" by simp
      qed

      from 1 2 3 show ?thesis by (simp add: psi'_def)

    next
      case False
      txt ‹Otherwise, σ ⊨p Xp φ› is equivalent to σ› satisfying
        the second disjunct of psi'›. We show both implications separately.›
      let ?val = "stval (σ 0)"
      let ?val' = "stval (σ 1)"
      from False can have vals: "?val'  ?val"
        by (auto simp: canonical_sequence_def state_sim_def stval_def)
        
      show ?thesis
      proof
        assume phi: "σ p Xp φ"
        from fin have 1: "σ p chi ?val" by (simp add: chi1 characteristic_holds)

        from st can have "stutter_free (σ[1..])" "canonical_sequence A (σ[1..])"
          by (auto simp: stutter_free_suffix canonical_suffix)
        with phi psi have 2: "σ[1..] p ψ" by auto

        from fin have "σ[1..] p characteristic_formula A ((σ[1..]) 0)"
          by (rule characteristic_holds)
        hence 3: "σ[1..] p chi ?val'" by (simp add: chi1)

        from 1 2 3 have "σ p And_ltlp (chi ?val) ((chi ?val) Up (And_ltlp ψ (chi ?val')))"
          (is "_ p ?unt")
          by auto
        moreover from vals have "?unt  ?UNT"
          by (auto simp: stval_def)
        ultimately have "σ p OR ?UNT"
          using fin_UNT[THEN holds_of_OR] by blast
        thus "σ p psi'" by (simp add: psi'_def)

      next
        assume psi': "σ p psi'"
        have "¬(σ p OR ?ALW)"
        proof
          assume "σ p OR ?ALW"
          with fin obtain val where 1: "val  A" and 2: "n. (σ[n..] p chi val)"
            by (force simp: finite_subset)
          from 2 have "σ[0..] p chi val" ..
          with 1 have "val = ?val" by (simp add: chi2)
          moreover
          from 2 have "σ[1..] p chi val" ..
          with 1 have "val = ?val'" by (force dest: chi2)
          ultimately
          show "False" using vals by simp
        qed
        with psi' have "σ p OR ?UNT" by (simp add: psi'_def)
        with fin_UNT obtain val val' k where
          val: "val  A" "val'  A" "val'  val" and
          now: "σ p chi val" and
          k: "σ[k..] p ψ" "σ[k..] p chi val'" and
          i: "i<k. (σ[i..] p chi val)"
          by auto (blast+)?  (* FRAGILE: similar as above *)

        from val now have 1: "val = ?val" by (simp add: chi2)

        have 2: "k  0"
        proof
          assume "k=0"
          with val k have "val' = ?val" by (simp add: chi2)
          with 1 val'  val show "False" by simp
        qed

        have 3: "k  1"
        proof (rule ccontr)
          assume "¬(k  1)"
          with i have "σ[1..] p chi val" by simp
          with 1 have "σ[1..] p characteristic_formula A (σ 0)" 
            by (simp add: chi1)
          hence "(σ 0) ~A~ ((σ[1..]) 0)"
            using characteristic_state_sim[OF fin] by blast
          with can have "σ 0 = σ 1"
            by (simp add: canonical_sequence_def)
          with σ (Suc 0)  σ 0 show "False" by simp
        qed

        from 2 3 have "k=1" by simp
        moreover
        from st can have "stutter_free (σ[1..])" "canonical_sequence A (σ[1..])"
          by (auto simp: stutter_free_suffix canonical_suffix)
        ultimately show "σ p Xp φ" using σ[k..] p ψ psi by auto
      qed
    qed
  }
  with nf atoms_pltl show "ψ'. ?P (Xp φ) ψ'" by blast
qed

text ‹
  Comparing the definition of the next-free formula in the case of
  formulas Xp φ› with the one that appears in~cite"peled:ltl-x",
  there is a subtle difference. Peled and Wilke define the second disjunct as
  a disjunction of formulas
%
  \begin{center}\(
    (chi val) Up (ψ andp (chi val'))›
  \)\end{center}
%
  for subsets val, val' ⊆ A› whereas we conjoin the formula
  chi val› to the ``until'' formula. This conjunct is indeed
  necessary in order to rule out the case of the ``until'' formula
  being true because of chi val'› being true immediately.
  The subtle error in the definition of the formula was acknowledged 
  by Peled and Wilke and apparently had not been noticed since the 
  publication of~cite"peled:ltl-x" in 1996 (which has been cited more
  than a hundred times according to Google Scholar). Although the error
  was corrected easily, the fact that authors, reviewers, and readers
  appear to have missed it for so long underscores the usefulness of
  formal proofs.

  We now show that any stuttering invariant PLTL formula
  can be expressed without the Xp operator.
›

theorem stutter_invariant_next_free:
  assumes phi: "stutter_invariant φ"
  obtains ψ where "next_free ψ" "atoms_pltl ψ  atoms_pltl φ"
                  "σ. (σ p ψ) = (σ p φ)"
proof -
  have "atoms_pltl φ  atoms_pltl φ" "finite (atoms_pltl φ)" by simp_all
  then obtain ψ where
    psi: "next_free ψ" "atoms_pltl ψ  atoms_pltl φ" and
    equiv: "σ. stutter_free σ  canonical_sequence (atoms_pltl φ) σ  (σ p ψ) = (σ p φ)"
    by (blast dest: ex_next_free_stutter_free_canonical)
  from next_free ψ have sinv: "stutter_invariant ψ"
    by (rule next_free_stutter_invariant)
  {
    fix σ
    obtain τ where 1: "τ  atoms_pltl φ  σ" and 2: "canonical_sequence (atoms_pltl φ) τ"
      by (rule canonical_exists)
    from 1 atoms_pltl ψ  atoms_pltl φ have 3: "τ  atoms_pltl ψ  σ"
      by (rule seq_sim_mono)

    from 1 have "(σ p φ) = (τ p φ)" by (simp add: pltl_seq_sim)
    also from phi stutter_reduced_equivalent have "... = (τ p φ)" by auto
    also from 2[THEN canonical_reduced] equiv stutter_reduced_stutter_free 
    have "... = (τ p ψ)" by auto
    also from sinv stutter_reduced_equivalent have "... = (τ p ψ)" by auto
    also from 3 have "... = (σ p ψ)" by (simp add: pltl_seq_sim)
    finally have "(σ p ψ) = (σ p φ)" by (rule sym)
  }
  with psi that show ?thesis by blast
qed

text ‹
  Combining theorems next_free_stutter_invariant› and
  stutter_invariant_next_free›, it follows that a PLTL
  formula is stuttering invariant iff it is equivalent to a next-free
  formula.
›

theorem pltl_stutter_invariant:
  "stutter_invariant φ  
   (ψ. next_free ψ  atoms_pltl ψ  atoms_pltl φ  (σ. σ p ψ  σ p φ))"
proof -
  {
    assume "stutter_invariant φ"
    hence "ψ. next_free ψ  atoms_pltl ψ  atoms_pltl φ  (σ. σ p ψ  σ p φ)"
      by (rule stutter_invariant_next_free) blast
  }
  moreover
  {
    fix ψ
    assume 1: "next_free ψ" and 2: "σ. σ p ψ  σ p φ"
    from 1 have "stutter_invariant ψ" by (rule next_free_stutter_invariant)
    with 2 have "stutter_invariant φ" by blast
  }
  ultimately show ?thesis by blast
qed


subsection ‹Stutter Invariance for LTL with Syntactic Sugar›

text ‹We lift the results for PLTL to an extensive version of LTL.›

primrec ltlc_next_free :: "'a ltlc  bool"
  where
    "ltlc_next_free truec = True"
  | "ltlc_next_free falsec = True"
  | "ltlc_next_free (propc(q)) = True"
  | "ltlc_next_free (notc φ) = ltlc_next_free φ"
  | "ltlc_next_free (φ andc ψ) = (ltlc_next_free φ  ltlc_next_free ψ)"
  | "ltlc_next_free (φ orc ψ) = (ltlc_next_free φ  ltlc_next_free ψ)"
  | "ltlc_next_free (φ impliesc ψ) = (ltlc_next_free φ  ltlc_next_free ψ)"
  | "ltlc_next_free (Xc φ) = False"
  | "ltlc_next_free (Fc φ) = ltlc_next_free φ"
  | "ltlc_next_free (Gc φ) = ltlc_next_free φ"
  | "ltlc_next_free (φ Uc ψ) = (ltlc_next_free φ  ltlc_next_free ψ)"
  | "ltlc_next_free (φ Rc ψ) = (ltlc_next_free φ  ltlc_next_free ψ)"
  | "ltlc_next_free (φ Wc ψ) = (ltlc_next_free φ  ltlc_next_free ψ)"
  | "ltlc_next_free (φ Mc ψ) = (ltlc_next_free φ  ltlc_next_free ψ)"

lemma ltlc_next_free_iff[simp]: "next_free (ltlc_to_pltl φ)  ltlc_next_free φ"
  by (induction φ) auto

text ‹A next free formula cannot distinguish between stutter-equivalent runs.›

theorem ltlc_next_free_stutter_invariant:
  assumes next_free: "ltlc_next_free φ"
  assumes eq: "r  r'"
  shows "r c φ  r' c φ"
proof -
  {
    fix r r'
    assume eq: "r  r'" and holds: "r c φ"
    then have "r p (ltlc_to_pltl φ)"by simp

    from next_free_stutter_invariant[of "ltlc_to_pltl φ"] next_free
    have "PLTL.stutter_invariant (ltlc_to_pltl φ)" by simp
    from stutter_invariantD[OF this eq] holds have "r' c φ" by simp
  } note aux=this

  from aux[of r r'] aux[of r' r] eq stutter_equiv_sym[OF eq] show ?thesis
    by blast
qed


end