Theory Hennessy_Milner_Logic

section ‹Hennessy--Milner Logic›

theory Hennessy_Milner_Logic
imports
  LTS_Semantics
begin

text ‹
  HML formulas can be the trivial formula, conjunctions, negations and observations of
  possible transitions.
›
datatype ('a,'i) hml_formula =
  HML_true
| HML_conj ‹'i set› ‹'i ⇒ ('a,'i) hml_conjunct›  (‹AND _ _›)
| HML_obs ‹'a› ‹('a,'i) hml_formula›              (‹⟨_⟩_› [60] 60)
and ('a,'i) hml_conjunct = 
  HML_pos ‹('a,'i) hml_formula›                   (‹+_› [20] 60)
| HML_neg ‹('a,'i) hml_formula›                   (‹-_› [20] 60)

context lts
begin

text ‹The model relation›
primrec satisfies :: ‹'s ⇒ ('a, 's) hml_formula ⇒ bool›    (‹_ ⊨ _› [50, 50] 40)
  and satisfies_conj :: ‹'s ⇒ ('a, 's) hml_conjunct ⇒ bool› 
  where
    ‹(p ⊨ HML_true) = True› |
    ‹(p ⊨ HML_conj I F) = (∀ i ∈ I. satisfies_conj p (F i))› |
    ‹(p ⊨ HML_obs α φ) = (∃ p'. p ⟼α p' ∧ p' ⊨ φ)› |
    ‹satisfies_conj p (HML_pos φ) = (p ⊨ φ)› |
    ‹satisfies_conj p (HML_neg φ) = (¬p ⊨ φ)›

interpretation hml: lts_semantics where satisfies = satisfies
  by unfold_locales
interpretation hml_conj: lts_semantics where satisfies = satisfies_conj
  by unfold_locales

abbreviation hml_entails (infixr "⇛" 60) where ‹hml_entails ≡ hml.entails›
abbreviation hml_logical_eq (infix "⇚⇛" 60) where ‹hml_logical_eq ≡ hml.logical_eq›

abbreviation hml_conj_entails (infixr "∧⇛" 60) where ‹hml_conj_entails ≡ hml_conj.entails›
abbreviation hml_conj_logical_eq (infix "⇚∧⇛" 60) where ‹hml_conj_logical_eq ≡ hml_conj.logical_eq›

declare lts_semantics.entails_def[simp]
declare lts_semantics.eq_equality[simp]

abbreviation ‹HML_conj_neg φ ≡ (AND {undefined} (λi. HML_neg φ))›
abbreviation ‹HML_conj_pos φ ≡ (AND {undefined} (λi. HML_pos φ))›

lemma distinguishes_invertible:
  assumes ‹hml.distinguishes φ p q›
  shows ‹hml.distinguishes (HML_conj_neg φ) q p›
  using assms by auto

lemma conjunction_wrapping:
  shows ‹p ⊨ (HML_conj_pos φ) ⟷ p ⊨ φ›
  by auto

text ‹
  If two states are not HML equivalent then there must be a
  distinguishing formula.
›
lemma hml_distinctions:
  assumes ‹¬ hml.equivalent 𝒪 p q›
  shows ‹∃φ. hml.distinguishes φ p q›
  using assms distinguishes_invertible
  unfolding hml.equivalent_def hml.preordered_no_distinction
  by blast


end

end