Theory HM_Logic_Infinitary

section ‹Infinitary Hennessy--Milner Logic›

theory HM_Logic_Infinitary
  imports 
    Weak_Relations
begin

datatype ('a,'x)HML_formula =
  HML_true 
| HML_conj ‹'x set› ‹'x ⇒ ('a,'x)HML_formula›  (‹AND _ _›)
| HML_neg ‹('a,'x)HML_formula›                  (‹~_› [20] 60)
| HML_poss ‹'a› ‹('a,'x)HML_formula›            (‹⟨_⟩_› [60] 60)

―‹The HML formulation is derived from that by Max Pohlmann @{cite pohlmann2021reactivebisim}.›

subsection ‹Satisfaction Relation›

context lts_tau
begin

function satisfies :: ‹'s ⇒ ('a, 's) HML_formula ⇒ bool› 
  (‹_ ⊨ _› [50, 50] 50)
  where
    ‹(p ⊨ HML_true) = True› 
  | ‹(p ⊨ HML_conj I F) = (∀ i ∈ I. p ⊨ (F i))› 
  | ‹(p ⊨ HML_neg φ) = (¬ p ⊨ φ)›
  | ‹(p ⊨ HML_poss α φ) =
      (∃ p'. ((tau α ∧ p ⟼* tau p') ∨ (¬ tau α ∧ p ⟼α p')) ∧ p' ⊨ φ)›
  using HML_formula.exhaust by (auto, blast)

inductive_set HML_wf_rel :: ‹('s × ('a, 's) HML_formula) rel› 
  where
    ‹φ = F i ∧ i ∈ I ⟹ ((p, φ), (p, HML_conj I F)) ∈ HML_wf_rel› 
  | ‹((p, φ), (p, HML_neg φ)) ∈ HML_wf_rel› 
  | ‹((p, φ), (p', HML_poss α φ)) ∈ HML_wf_rel›

lemma HML_wf_rel_is_wf: ‹wf HML_wf_rel› 
  unfolding wf_def
proof (safe)
  fix P::‹'s × ('a, 's) HML_formula ⇒ bool› and t::‹'s × ('a, 's) HML_formula›
  obtain p φ where ‹t = (p, φ)› by force
  assume ‹∀x. (∀y. (y, x) ∈ HML_wf_rel ⟶ P y) ⟶ P x›
  hence ‹P (p, φ)›
  proof (induct φ arbitrary: p)
    case HML_true
    then show ?case
      by (metis HML_formula.distinct(1,3,5) HML_wf_rel.cases old.prod.exhaust)
  next
    case (HML_conj I F)
    thus ?case
      by (smt (verit) HML_formula.distinct(7,9) HML_formula.inject(1) HML_wf_rel.cases
         case_prodD case_prodE' lts_tau.HML_wf_rel_def mem_Collect_eq range_eqI)
  next
    case (HML_neg φ)
    thus ?case
      by (metis HML_formula.distinct(11,7) HML_formula.inject(2) HML_wf_rel.cases surj_pair)
  next
    case (HML_poss a φ)
    thus ?case
      by (smt (verit, del_insts) HML_formula.distinct(3,5,9,11)  HML_formula.inject(3)
        HML_wf_rel.cases case_prodD case_prodE' HML_wf_rel_def mem_Collect_eq)
  qed
  thus ‹P t› using ‹t = (p, φ)› by simp
qed

termination satisfies using HML_wf_rel_is_wf 
  by (standard, (simp add: HML_wf_rel.intros)+)

inductive_set HML_direct_subformulas :: ‹(('a, 's) HML_formula) rel›
  where
    ‹φ = F i ∧ i ∈ I ⟹ (φ, HML_conj I F) ∈ HML_direct_subformulas› 
  | ‹(φ, HML_neg φ) ∈ HML_direct_subformulas› 
  | ‹(φ, HML_poss α φ) ∈ HML_direct_subformulas›

lemma HML_direct_subformulas_wf: ‹wf HML_direct_subformulas› 
  unfolding wf_def
proof (safe)
  fix P x
  assume ‹∀x. (∀y. (y, x) ∈ HML_direct_subformulas ⟶ P y) ⟶ P x›
  thus ‹P x›
  proof induct
    case HML_true
    then show ?case using HML_direct_subformulas.simps by blast
  next
    case (HML_conj I F)
    then show ?case
      by (metis HML_direct_subformulas.cases HML_formula.distinct(7,9)
          HML_formula.inject(1) range_eqI)
  next
    case (HML_neg φ)
    then show ?case
      by (metis HML_direct_subformulas.simps HML_formula.distinct(11,7) HML_formula.inject(2))
  next
    case (HML_poss a φ)
    then show ?case
      by (metis HML_direct_subformulas.simps HML_formula.distinct(11,9) HML_formula.inject(3))
  qed
qed

definition HML_subformulas where ‹HML_subformulas ≡ (HML_direct_subformulas)⇧+›

lemma HML_subformulas_wf: ‹wf HML_subformulas›
  using HML_direct_subformulas_wf HML_subformulas_def wf_trancl
  by fastforce

lemma conj_only_depends_on_indexset:
  assumes ‹∀i∈I. f1 i = f2 i›
  shows ‹(p ⊨ HML_conj I f1) = (p ⊨ HML_conj I f2)›
  using assms by auto

subsection ‹Distinguishing Formulas›

definition HML_equivalent :: ‹'s ⇒ 's ⇒ bool›
  where ‹HML_equivalent p q 
    ≡ (∀ φ::('a, 's) HML_formula. (p ⊨ φ) ⟷ (q ⊨ φ))›

fun distinguishes ::  ‹('a,'s) HML_formula ⇒ 's ⇒ 's ⇒ bool›
  where
   ‹distinguishes φ p q = (p ⊨ φ ∧ ¬ q ⊨ φ)›

fun distinguishes_from_set ::  ‹('a,'s) HML_formula ⇒ 's ⇒ 's set ⇒ bool›
  where
   ‹distinguishes_from_set φ p Q = (p ⊨ φ ∧ (∀q. q ∈ Q ⟶ ¬ q ⊨ φ))›

lemma distinguishing_formula:
  assumes ‹¬ HML_equivalent p q›
  shows ‹∃ φ. p ⊨ φ ∧ ¬ q ⊨ φ›
  using assms  satisfies.simps(3) unfolding HML_equivalent_def 
  by blast

lemma HML_equivalent_symm:
  assumes ‹HML_equivalent p q›
  shows ‹HML_equivalent q p›
  using HML_equivalent_def assms by presburger

subsection ‹Weak-NOR Hennessy--Milner Logic›

definition HML_weaknor ::
  ‹'x set ⇒ ('x ⇒ ('a,'x)HML_formula) ⇒ ('a,'x)HML_formula›
  where ‹HML_weaknor I F = HML_poss τ (HML_conj I (λf. HML_neg (F f)))›

definition HML_weaknot ::
  ‹('a,'x)HML_formula ⇒ ('a,'x)HML_formula›
  where ‹HML_weaknot φ = HML_weaknor {undefined} (λi. φ)›

inductive_set HML_weak_formulas :: ‹('a,'x)HML_formula set› where
  Base: ‹HML_true ∈ HML_weak_formulas› |
  Obs: ‹φ ∈ HML_weak_formulas ⟹ (⟨τ⟩⟨a⟩φ) ∈ HML_weak_formulas› |
  Conj: ‹(⋀i. i ∈ I ⟹ F i ∈ HML_weak_formulas) ⟹ HML_weaknor I F ∈ HML_weak_formulas›

lemma weak_backwards_truth:
  assumes
    ‹φ ∈ HML_weak_formulas›
    ‹p ⟼* tau  p'›
    ‹p' ⊨ φ›
  shows
    ‹p ⊨ φ›
  using assms
proof cases
  case Base
  then show ?thesis by force
next
  case (Obs φ a)
  then show ?thesis
    using assms(2,3) satisfies.simps(4) steps_concat tau_tau by blast
next
  case (Conj I F)
  then show ?thesis
    unfolding HML_weaknor_def tau_def
    using tau_tau assms steps_concat
    by force
qed

lemma tau_a_obs_implies_delay_step: 
  assumes ‹p  ⊨ ⟨τ⟩⟨a⟩φ›
  shows ‹∃p'. p =⊳a p' ∧ p' ⊨ φ›
proof - 
  obtain p'' where ‹p ⇒^τ p'' ∧ p'' ⊨ ⟨a⟩φ› using assms by auto
  thus ?thesis using satisfies.simps(4) steps_concat tau_tau by blast
qed

lemma delay_step_implies_tau_a_obs: 
  assumes 
    ‹p =⊳a p'›
    ‹p' ⊨ φ›
  shows ‹p  ⊨ ⟨τ⟩⟨a⟩φ›
proof - 
  obtain p'' where ‹p ⇒^τ p''› and ‹p'' ⇒^a p'›
    using assms steps.refl tau_tau by blast
  thus ?thesis
    by (metis assms(1,2) lts_tau.satisfies.simps(4) lts_tau.tau_tau)
qed

end
end