Theory LTS_Semantics

section ‹LTS Semantics›

theory LTS_Semantics
  imports
    Labeled_Transition_Systems
begin

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

abbreviation model_set :: "'formula ⇒ 's set" where
  "model_set φ ≡ {p. satisfies p φ}"

abbreviation ‹tautological φ ≡ ∀p. satisfies p φ›
abbreviation ‹globally_false φ ≡ ∀p. ¬satisfies p φ›

lemma tautological_univ_model:
  ‹tautological φ ⟷ model_set φ = UNIV›
  by blast

subsection ‹Logical Equivalence›

definition entails :: ‹'formula ⇒ 'formula ⇒ bool› where
  entails_def[simp]: "entails φl φr ≡ (∀p. (satisfies p φl) ⟶ (satisfies 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
satisfies predicate.
›
lemma eq_equality[simp]: "(logical_eq φl φr) = (∀p. satisfies p φl = satisfies p φr)"
  by force

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

subsection ‹Distinctions›

abbreviation distinguishes :: "'formula ⇒ 's ⇒ 's ⇒ bool" where
  "distinguishes φ p q ≡ satisfies p φ ∧ ¬(satisfies q φ)"

definition distinguishes_from :: "'formula ⇒ 's ⇒ 's set ⇒ bool" where
  distinguishes_from_def[simp]:
  "distinguishes_from φ p Q ≡ satisfies p φ ∧ (∀q ∈ Q. ¬(satisfies 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

subsection ‹Formula Set derived Pre-Order and Equivalence on Processes›

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. ›
abbreviation preordered :: "'formula set ⇒ 's ⇒ 's ⇒ bool" where
  "preordered 𝒪 p q ≡ ∀φ ∈ 𝒪. satisfies p φ ⟶ satisfies 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 𝒪 p q = (∀φ ∈ 𝒪. ¬(distinguishes φ p q))"
  by simp

text ‹A formula set derived pre-order is a pre-order.›
lemma preordered_preord:
  "reflp (preordered 𝒪)"
  "transp (preordered 𝒪)"
  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 𝒪 p q ≡ preordered 𝒪 p q ∧ preordered 𝒪 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 𝒪 p q
     = (∀φ ∈ 𝒪. ¬(distinguishes φ p q) ∧ ¬(distinguishes φ q p))"
  by auto

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

subsection ‹Expressiveness and Distinctiveness of Sublogics›

definition ‹leq_expressive 𝒪 𝒪' ≡ ∀φ∈𝒪. ∃φ'∈𝒪'. ∀s. satisfies s φ ⟷ satisfies s φ'›
abbreviation ‹eq_expressive 𝒪 𝒪' ≡ leq_expressive 𝒪 𝒪' ∧ leq_expressive 𝒪' 𝒪›
definition ‹leq_distinctive 𝒪 𝒪' ≡ ∀p q. ∀φ∈𝒪. distinguishes φ p q ⟶ (∃φ'∈𝒪'. distinguishes φ' p q)›
abbreviation ‹eq_distinctive 𝒪 𝒪' ≡ leq_distinctive 𝒪 𝒪' ∧ leq_distinctive 𝒪' 𝒪›

lemma expressiveness_entails_distinctiveness:
  assumes
    ‹leq_expressive 𝒪 𝒪'›
  shows
    ‹leq_distinctive 𝒪 𝒪'›
  using assms unfolding leq_expressive_def leq_distinctive_def
  by fastforce

lemma expressiveness_eq_entails_distinctiveness_eq:
  assumes
    ‹eq_expressive 𝒪 𝒪'›
  shows
    ‹eq_distinctive 𝒪 𝒪'›
  using assms expressiveness_entails_distinctiveness by blast
― ‹The converse is not true. For instance, adding Falsum or Verum to an observation language is neutral with respect to distinctiveness, but increases expressiveness.›

lemma subset_distinctiveness:
  assumes
    ‹𝒪 ⊆ 𝒪'›
  shows
    ‹leq_distinctive 𝒪 𝒪'›
  using assms unfolding leq_distinctive_def by blast

lemma subset_expressiveness:
  assumes
    ‹𝒪 ⊆ 𝒪'›
  shows
    ‹leq_expressive 𝒪 𝒪'›
  using assms unfolding leq_expressive_def by blast

lemma preorder_distinctiveness_contraposition:
  assumes
    ‹leq_distinctive 𝒪 𝒪'›
    ‹preordered 𝒪' p q›
  shows
    ‹preordered 𝒪 p q ›
  using assms unfolding leq_distinctive_def by blast

lemma preorder_expressiveness_contraposition:
  assumes
    ‹leq_expressive 𝒪 𝒪'›
    ‹preordered 𝒪' p q›
  shows
    ‹preordered 𝒪 p q ›
  using assms preorder_distinctiveness_contraposition expressiveness_entails_distinctiveness
  by blast

lemma preorder_contraposition:
  assumes
    ‹𝒪 ⊆ 𝒪'›
    ‹preordered 𝒪' p q›
  shows
    ‹preordered 𝒪 p q›
  using assms preorder_distinctiveness_contraposition subset_distinctiveness by blast

lemma equiv_contraposition:
  assumes
    ‹𝒪 ⊆ 𝒪'›
    ‹equivalent 𝒪' p q›
  shows
    ‹equivalent 𝒪 p q›
  using assms unfolding equivalent_def by blast

lemma trivialities_dont_add_distinctivenes:
  assumes
    ‹tautological φ ∨ globally_false φ›
  shows
    ‹eq_distinctive 𝒪 (𝒪 ∪ {φ})›
  using assms unfolding leq_distinctive_def by blast


end

end