Theory LTS_Semantics

subsection ‹Modal Logics on LTS›

theory LTS_Semantics
  imports
    LTS
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 ‹
The definition given above is equivalent which means 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

text ‹If $\varphi$ is equivalent to $\varphi'$ and $\varphi$ distinguishes process @{term ‹p›} from
process @{term ‹q›}, the $\varphi'$ also distinguishes process @{term ‹p›} from process @{term ‹q›}.›
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 @{term ‹p›} and @{term ‹q›} if
for all formulas in this set the fact that @{term ‹p›} satisfies a formula means that also
@{term ‹q›} must 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 @{term ‹p›} and @{term ‹q›}, then no formula in that set
may distinguish @{term ‹p›} from @{term ‹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 @{term ‹p›} and @{term ‹q›} if
this set of formulas 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 @{term ‹p›} and @{term ‹q›}, then no formula in that set
may distinguish @{term ‹p›} from @{term ‹q›} nor the other way around.
›
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

end