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