Theory LTS_Semantics

(* License: LGPL *)

subsection ‹Modal Logics on LTS›

text ‹
  We here supply abstract definitions that would work for all modal logics one might define over an LTS.
  In particular, this contains mechanisms to derive equivalences from sublogics.
›

theory LTS_Semantics
  imports
    Labeled_Transition_Systems
begin

locale lts_semantics = lts step
  for step :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› (‹_ ↦ _ _› [70,70,70] 80) +
  fixes models :: ‹'s ⇒ 'formula ⇒ bool›
begin

definition entails :: ‹'formula ⇒ 'formula ⇒ bool› where
  entails_def[simp]: ‹entails φl φr ≡ (∀p. (models p φl) ⟶ (models p φr))›

definition logical_eq :: ‹'formula ⇒ 'formula ⇒ bool› where
  logical_eq_def[simp]: ‹logical_eq φl φr ≡ entails φl φr ∧ entails φr φl›

text ‹Formula implication is a pre-order. ›
lemma entails_preord: ‹reflp (entails)› ‹transp (entails)›
  by (simp add: reflpI transp_def)+

lemma eq_equiv: ‹equivp logical_eq›
  using equivpI reflpI sympI transpI
  unfolding logical_eq_def entails_def
  by (smt (verit, del_insts))

text ‹
  Formula equivalence is a biimplication on the models predicate.
›
lemma eq_equality[simp]: ‹(logical_eq φl φr) = (∀p. models p φl ⟷ models p φr)›
  by force

lemma logical_eqI[intro]:
  assumes
    ‹⋀s. models s φl ⟹ models s φr›
    ‹⋀s. models s φr ⟹ models s φl›
  shows
    ‹logical_eq φl φr›
  using assms by auto

definition distinguishes :: ‹'formula ⇒ 's ⇒ 's ⇒ bool› where
  distinguishes_def[simp]:
  ‹distinguishes φ p q ≡ models p φ ∧ ¬(models q φ)›

definition distinguishes_from :: ‹'formula ⇒ 's ⇒ 's set ⇒ bool› where
  distinguishes_from_def[simp]:
  ‹distinguishes_from φ p Q ≡ models p φ ∧ (∀q ∈ Q. ¬(models q φ))›

lemma distinction_unlifting:
  assumes
    ‹distinguishes_from φ p Q›
  shows
    ‹∀q∈Q. distinguishes φ p q›
  using assms by simp

lemma no_distinction_fom_self:
  assumes
    ‹distinguishes φ p p›
  shows
    ‹False›
  using assms by simp

lemma dist_equal_dist:
  assumes ‹logical_eq φl φr›
      and ‹distinguishes φl p q›
    shows ‹distinguishes φr p q›
  using assms
  by auto

abbreviation model_set :: ‹'formula ⇒ 's set› where
  ‹model_set φ ≡ {p. models p φ}›

subsection ‹Preorders and Equivalences on Processes Derived from Formula Sets›

text ‹A set of formulas pre-orders two processes ‹p› and ‹q› if, for all formulas in this set, the fact that ‹p› satisfies a formula means that ‹q› must also satisfy this formula.›
definition preordered :: ‹'formula set ⇒ 's ⇒ 's ⇒ bool› where
  preordered_def[simp]:
  ‹preordered φs p q ≡ ∀φ ∈ φs. models p φ ⟶ models q φ›

text ‹If a set of formulas pre-orders two processes ‹p› and ‹q›, then no formula in that set may distinguish ‹p› from ‹q›.›
lemma preordered_no_distinction:
  ‹preordered φs p q = (∀φ ∈ φs. ¬(distinguishes φ p q))›
  by simp

text ‹A formula set derived pre-order is a pre-order.›
lemma preordered_preord:
  ‹reflp (preordered φs)›
  ‹transp (preordered φs)›
  unfolding reflp_def transp_def by auto

text ‹A set of formulas equates two processes if it pre-orders these two processes in both directions.›
definition equivalent :: ‹'formula set ⇒ 's ⇒ 's ⇒ bool› where
  equivalent_def[simp]:
  ‹equivalent φs p q ≡ preordered φs p q ∧ preordered φs q p›

text ‹If a set of formulas equates two processes, then no formula in that set
may distinguish them in any direction.›
lemma equivalent_no_distinction: ‹equivalent φs p q
     = (∀φ ∈ φs. ¬(distinguishes φ p q) ∧ ¬(distinguishes φ q p))›
  by auto

text ‹A formula-set-derived equivalence is an equivalence.›
lemma equivalent_equiv: ‹equivp (equivalent φs)›
proof (rule equivpI)
  show ‹reflp (equivalent φs)›
    by (simp add: reflpI)
  show ‹symp (equivalent φs)›
    unfolding equivalent_no_distinction symp_def
    by auto
  show ‹transp (equivalent φs)›
    unfolding transp_def equivalent_def preordered_def
    by blast
qed

end ― ‹of context ‹lts_semantics››

end