Theory Formula

section ‹LTL Formulae›

theory Formula
imports
  "Basics/Stuttering"
  Stuttering_Equivalence.PLTL
begin

  locale formula =
    fixes φ :: "'a pltl"
  begin

    definition language :: "'a stream set"
      where "language  {w. snth w p φ}"
  
    lemma language_entails[iff]: "w  language  snth w p φ" unfolding language_def by simp

  end

  locale formula_next_free =
    formula φ
    for φ :: "'a pltl"
    +
    assumes next_free: "next_free φ"
  begin

    lemma stutter_equivalent_entails[dest]: "u  v  u p φ  v p φ"
      using next_free_stutter_invariant next_free by blast

  end

end