Theory HML_SRBB

(* License: LGPL *)

section ‹Hennessy--Milner Logic for Stability-Respecting Branching Bisimilarity›

theory HML_SRBB
  imports LTS_Semantics
begin

text ‹
  This section describes a variant of Hennessy--Milner logic that characterizes stability-respecting branching bisimilarity (SRBB).
›

text ‹The following mutually-recursive datatype family describes a grammar of ‹HML_SRBB› formulas.›

datatype
  ('act, 'i) hml_srbb =
    TT |
    Internal ‹('act, 'i) hml_srbb_inner› |
    ImmConj ‹'i set› ‹'i ⇒ ('act, 'i) hml_srbb_conjunct›
and
  ('act, 'i) hml_srbb_inner =
    Obs 'act ‹('act, 'i) hml_srbb› |
    Conj ‹'i set› ‹'i ⇒ ('act, 'i) hml_srbb_conjunct› |
    StableConj ‹'i set› ‹'i ⇒ ('act, 'i) hml_srbb_conjunct› |
    BranchConj 'act ‹('act, 'i) hml_srbb›
               ‹'i set› ‹'i ⇒ ('act, 'i) hml_srbb_conjunct›
and
  ('act, 'i) hml_srbb_conjunct =
    Pos ‹('act, 'i) hml_srbb_inner› |
    Neg ‹('act, 'i) hml_srbb_inner›

text ‹
  The constructors correspond to more conventional notation of HML as follows:

  ▪ type‹hml_srbb› (members usually referred to as ‹φ›):
    ▪ term‹TT› encodes ‹⊤›
    ▪ term‹(Internal χ)› encodes ‹⟨ε⟩χ›
    ▪ term‹(ImmConj I ψs)› encodes $\bigwedge\nolimits_{i \in \mathrm{\texttt{I}}} {\psi s}(i)$
  ▪ type‹hml_srbb_inner› (usually ‹χ›):
    ▪ term‹(Obs α φ)› encodes ‹(α)φ›
    ▪ term‹(Conj I ψs)› encodes $\bigwedge\nolimits_{i \in \mathrm{\texttt{I}}} {\psi s}(i)$
    ▪ term‹(StableConj I ψs)› encodes $\neg\langle\tau\rangle\top \land \bigwedge\nolimits_{i \in \mathrm{\texttt{I}}} {\psi s}(i)$
    ▪ term‹(BranchConj α φ I ψs)› encodes $(\alpha)\varphi \land \bigwedge\nolimits_{i \in \mathrm{\texttt{I}}} {\psi s}(i)$
  ▪ type‹hml_srbb_conjunct› (usually ‹ψ›):
    ▪ term‹(Pos χ)› encodes ‹⟨ε⟩χ›
    ▪ term‹(Neg χ)› encodes ‹¬⟨ε⟩χ›
›

subsection ‹Semantics of HML$_\text{SRBB}$ Formulas›

text ‹
  This section describes how semantic meaning is assigned to HML$_\text{SRBB}$ formulas in the context of a LTS.
  We define what it means for a process ‹p› to satisfy an HML$_\text{SRBB}$ formula ‹φ›, written as ‹p ⊨SRBB φ›.
›

context lts_tau
begin

primrec
      hml_srbb_models :: ‹'s ⇒ ('a, 's) hml_srbb ⇒ bool› (infixl ‹⊨SRBB› 60)
  and hml_srbb_inner_models :: ‹'s ⇒ ('a, 's) hml_srbb_inner ⇒ bool›
  and hml_srbb_conjunct_models :: ‹'s ⇒ ('a, 's) hml_srbb_conjunct ⇒ bool› where
  ‹hml_srbb_models state TT =
    True› |
  ‹hml_srbb_models state (Internal χ) =
    (∃p'. state ↠ p' ∧ (hml_srbb_inner_models p' χ))› |
  ‹hml_srbb_models state (ImmConj I ψs) =
    (∀i∈I. hml_srbb_conjunct_models state (ψs i))› |

  ‹hml_srbb_inner_models state (Obs a φ) =
    ((∃p'. state ↦ a p' ∧ hml_srbb_models p' φ) ∨ a = τ ∧ hml_srbb_models state φ)› |
  ‹hml_srbb_inner_models state (Conj I ψs) =
    (∀i∈I. hml_srbb_conjunct_models state (ψs i))› |
  ‹hml_srbb_inner_models state (StableConj I ψs) =
    ((∄p'. state ↦ τ p') ∧ (∀i∈I. hml_srbb_conjunct_models state (ψs i)))› |
  ‹hml_srbb_inner_models state (BranchConj a φ I ψs) =
    (((∃p'. state ↦ a p' ∧ hml_srbb_models p' φ) ∨ a = τ ∧ hml_srbb_models state φ)
    ∧ (∀i∈I. hml_srbb_conjunct_models state (ψs i)))› |

  ‹hml_srbb_conjunct_models state (Pos χ) =
    (∃p'. state ↠ p' ∧ hml_srbb_inner_models p' χ)› |
  ‹hml_srbb_conjunct_models state (Neg χ) =
    (∄p'. state ↠ p' ∧ hml_srbb_inner_models p' χ)›

sublocale lts_semantics ‹step› ‹hml_srbb_models› .
sublocale hml_srbb_inner: lts_semantics where models = hml_srbb_inner_models .
sublocale hml_srbb_conj: lts_semantics where models = hml_srbb_conjunct_models .

subsection ‹Distinguishing Formulas›

lemma verum_never_distinguishes:
  ‹¬ distinguishes TT p q›
  by simp

text ‹
  If $\bigwedge\nolimits_{i \in I} {\psi s}(i)$ distinguishes ‹p› from ‹q›, then there must be at least one conjunct in this conjunction that distinguishes ‹p› from ‹q›.
›
lemma srbb_dist_imm_conjunction_implies_dist_conjunct:
  assumes ‹distinguishes (ImmConj I ψs) p q›
  shows ‹∃i∈I. hml_srbb_conj.distinguishes (ψs i) p q›
  using assms by auto

lemma srbb_dist_conjunction_implies_dist_conjunct:
  assumes ‹hml_srbb_inner.distinguishes (Conj I ψs) p q›
  shows ‹∃i∈I. hml_srbb_conj.distinguishes (ψs i) p q›
  using assms by auto

lemma srbb_dist_branch_conjunction_implies_dist_conjunct_or_branch:
  assumes
    ‹hml_srbb_inner.distinguishes (BranchConj α φ I ψs) p q›
  shows
    ‹(∃i∈I. hml_srbb_conj.distinguishes (ψs i) p q)
       ∨ hml_srbb_inner.distinguishes (Obs α φ) p q›
  using assms by force

lemma srbb_dist_conjunct_implies_dist_imm_conjunction:
  assumes
    ‹i∈I›
    ‹hml_srbb_conj.distinguishes (ψs i) p q›
    ‹∀i∈I. hml_srbb_conjunct_models p (ψs i)›
  shows
    ‹distinguishes (ImmConj I ψs) p q›
  using assms by auto

lemma srbb_dist_conjunct_implies_dist_conjunction:
  assumes
    ‹i∈I›
    ‹hml_srbb_conj.distinguishes (ψs i) p q›
    ‹∀i∈I. hml_srbb_conjunct_models p (ψs i)›
  shows
    ‹hml_srbb_inner.distinguishes (Conj I ψs) p q›
  using assms by auto

lemma srbb_dist_conjunct_or_branch_implies_dist_branch_conjunction:
  assumes
    ‹∀i ∈ I. hml_srbb_conjunct_models p (ψs i)›
    ‹hml_srbb_inner_models p (Obs α φ)›
    ‹(i∈I ∧ hml_srbb_conj.distinguishes (ψs i) p q)
         ∨ (hml_srbb_inner.distinguishes (Obs α φ) p q)›
  shows
    ‹hml_srbb_inner.distinguishes (BranchConj α φ I ψs) p q›
  using assms by force

subsection ‹HML$_\text{SRBB}$ Implication and Equivalence›

abbreviation hml_srbb_impl
  :: ‹('a, 's) hml_srbb ⇒ ('a, 's) hml_srbb ⇒ bool›  (infixr ‹⇛› 70)
where
  ‹hml_srbb_impl ≡ entails›

abbreviation
  hml_srbb_impl_inner
  :: ‹('a, 's) hml_srbb_inner ⇒ ('a, 's) hml_srbb_inner ⇒ bool›
  (infix ‹χ⇛› 70)
where
  ‹(χ⇛) ≡ hml_srbb_inner.entails›

abbreviation
  hml_srbb_impl_conjunct
  :: ‹('a, 's) hml_srbb_conjunct ⇒ ('a, 's) hml_srbb_conjunct ⇒ bool›
  (infix ‹ψ⇛› 70)
where
  ‹(ψ⇛) ≡ hml_srbb_conj.entails›

abbreviation
  hml_srbb_eq
  :: ‹('a, 's) hml_srbb ⇒ ('a, 's) hml_srbb ⇒ bool›
  (infix ‹⇚srbb⇛› 70)
where
  ‹(⇚srbb⇛) ≡ logical_eq›

abbreviation
  hml_srbb_eq_inner
  :: ‹('a, 's) hml_srbb_inner ⇒ ('a, 's) hml_srbb_inner ⇒ bool›
  (infix ‹⇚χ⇛› 70)
where
  ‹(⇚χ⇛) ≡ hml_srbb_inner.logical_eq›

abbreviation
  hml_srbb_eq_conjunct
  :: ‹('a, 's) hml_srbb_conjunct ⇒ ('a, 's) hml_srbb_conjunct ⇒ bool›
  (infix ‹⇚ψ⇛› 70)
  where
  ‹(⇚ψ⇛) ≡ hml_srbb_conj.logical_eq›

subsection ‹Substitution and Congruence›

lemma srbb_internal_subst:
  assumes
    ‹χl ⇚χ⇛ χr›
    ‹φ ⇚srbb⇛ (Internal χl)›
  shows
    ‹φ ⇚srbb⇛ (Internal χr)›
  using assms by force

lemma internal_srbb_cong:
  assumes ‹χl ⇚χ⇛ χr›
  shows ‹(Internal χl) ⇚srbb⇛ (Internal χr)›
  using assms by auto


lemma immconj_cong:
  assumes
    ‹ψsl ` I = ψsr ` I›
    ‹ψsl s ⇚ψ⇛ ψsr s›
  shows
    ‹ImmConj (I ∪ {s}) ψsl ⇚srbb⇛ ImmConj (I ∪ {s}) ψsr›
  using assms
  by (auto) (metis (mono_tags, lifting) image_iff)+

lemma obs_srbb_cong:
  assumes ‹φl ⇚srbb⇛ φr›
  shows ‹(Obs α φl) ⇚χ⇛ (Obs α φr)›
  using assms by auto

subsection ‹Trivial and Equivalent Formulas›

lemma empty_conj_trivial[simp]:
  ‹state ⊨SRBB ImmConj {} ψs›
  ‹hml_srbb_inner_models state (Conj {} ψs)›
  ‹hml_srbb_inner_models state (Obs τ TT)›
  by simp+

lemma empty_branch_conj_tau:
  ‹hml_srbb_inner_models state (BranchConj τ TT {} ψs)›
  by auto

lemma stable_conj_parts:
  assumes
    ‹hml_srbb_inner_models p (StableConj I Ψ)›
    ‹i ∈ I›
  shows
    ‹hml_srbb_conjunct_models p (Ψ i)›
  using assms by auto

lemma branching_conj_parts:
  assumes
    ‹hml_srbb_inner_models p (BranchConj α φ I Ψ)›
    ‹i ∈ I›
  shows
    ‹hml_srbb_conjunct_models p (Ψ i)›
  using assms by auto

lemma branching_conj_obs:
  assumes ‹hml_srbb_inner_models p (BranchConj α φ I Ψ)›
  shows ‹hml_srbb_inner_models p (Obs α φ)›
  using assms by auto

lemma srbb_obs_τ_is_χTT: ‹Obs τ TT ⇚χ⇛ Conj {} ψs›
  by simp

lemma srbb_obs_is_empty_branch_conj: ‹Obs α φ ⇚χ⇛ BranchConj α φ {} ψs›
  by auto

lemma srbb_TT_is_χTT: ‹TT ⇚srbb⇛ Internal (Conj {} ψs)›
  using lts_tau.refl by force

lemma srbb_TT_is_empty_conj: ‹TT ⇚srbb⇛ ImmConj {} ψs›
  by simp

text ‹Positive conjuncts in stable conjunctions can be replaced by negative ones.›
lemma srbb_stable_Neg_normalizable:
  assumes
    ‹i ∈ I› ‹Ψ i = Pos χ›
    ‹Ψ' = Ψ(i:= Neg (StableConj {left} (λ_. Neg χ)))›
  shows
    ‹Internal (StableConj I Ψ) ⇚srbb⇛ Internal (StableConj I Ψ')›
proof (rule logical_eqI)
  fix p
  assume ‹p ⊨SRBB Internal (StableConj I Ψ)›
  then obtain p' where p'_spec: ‹p ↠ p'› ‹hml_srbb_inner_models p' (StableConj I Ψ)› by auto
  hence ‹stable_state p'› by auto
  from p'_spec have ‹∃p''. p' ↠ p'' ∧ hml_srbb_inner_models p'' χ›
    using assms(1,2) by auto
  with ‹stable_state p'› have ‹hml_srbb_inner_models p' χ›
    using stable_state_stable by blast
  hence ‹hml_srbb_conjunct_models p' (Neg (StableConj {left} (λ_. Neg χ)))›
    using ‹stable_state p'› stable_state_stable by (auto, blast)
  hence ‹hml_srbb_inner_models p' (StableConj I Ψ')›
    unfolding assms(3) using p'_spec by auto
  thus ‹p ⊨SRBB hml_srbb.Internal (StableConj I Ψ')›
    using ‹p ↠ p'› by auto
next
  fix p
  assume ‹p ⊨SRBB Internal (StableConj I Ψ')›
  then obtain p' where p'_spec: ‹p ↠ p'› ‹hml_srbb_inner_models p' (StableConj I Ψ')› by auto
  hence ‹stable_state p'› by auto
  from p'_spec(2) have other_conjuncts: ‹∀j∈I. i ≠ j ⟶ hml_srbb_conjunct_models p' (Ψ j)›
    using assms stable_conj_parts fun_upd_apply by metis
  from p'_spec(2) have ‹hml_srbb_conjunct_models p' (Ψ' i)›
    using assms(1) stable_conj_parts by blast
  hence ‹hml_srbb_conjunct_models p' (Neg (StableConj {left} (λ_. Neg χ)))›
    unfolding assms(3) by auto
  with ‹stable_state p'› have ‹hml_srbb_inner_models p' χ›
    using stable_state_stable by (auto, metis silent_reachable.simps)
  then have ‹hml_srbb_conjunct_models p' (Pos χ)›
    using lts_tau.refl by fastforce
  hence ‹hml_srbb_inner_models p' (StableConj I Ψ)›
    using p'_spec assms other_conjuncts by auto
  thus ‹p ⊨SRBB hml_srbb.Internal (StableConj I Ψ)›
    using p'_spec(1) by auto
qed

text ‹All positive conjuncts in stable conjunctions can be replaced by negative ones at once.›
lemma srbb_stable_Neg_normalizable_set:
  assumes
    ‹Ψ' = (λi. case (Ψ i) of
      Pos χ ⇒ Neg (StableConj {left} (λ_. Neg χ)) |
      Neg χ ⇒ Neg χ)›
  shows
    ‹Internal (StableConj I Ψ) ⇚srbb⇛ Internal (StableConj I Ψ')›
proof (rule logical_eqI)
  fix p
  assume ‹p ⊨SRBB Internal (StableConj I Ψ)›
  then obtain p' where p'_spec: ‹p ↠ p'› ‹hml_srbb_inner_models p' (StableConj I Ψ)› by auto
  hence ‹stable_state p'› by auto
  from p'_spec have
    ‹∀χ i. i∈I ∧ Ψ i = Pos χ ⟶ (∃p''. p' ↠ p'' ∧ hml_srbb_inner_models p'' χ)›
    by fastforce
  with ‹stable_state p'› have ‹∀χ i. i∈I ∧ Ψ i = Pos χ ⟶ hml_srbb_inner_models p' χ›
    using stable_state_stable by blast
  hence pos_rewrite: ‹∀χ i. i∈I ∧ Ψ i = Pos χ ⟶
      hml_srbb_conjunct_models p' (Neg (StableConj {left} (λ_. Neg χ)))›
    using ‹stable_state p'› stable_state_stable by (auto, blast)
  hence ‹hml_srbb_inner_models p' (StableConj I Ψ')›
    unfolding assms using p'_spec
    by (auto, metis (no_types, lifting) hml_srbb_conjunct.exhaust hml_srbb_conjunct.simps(5,6)
        pos_rewrite)
  thus ‹p ⊨SRBB Internal (StableConj I Ψ')›
    using ‹p ↠ p'› by auto
next
  fix p
  assume ‹p ⊨SRBB Internal (StableConj I Ψ')›
  then obtain p' where p'_spec: ‹p ↠ p'› ‹hml_srbb_inner_models p' (StableConj I Ψ')› by auto
  hence ‹stable_state p'› by auto
  from p'_spec(2) have other_conjuncts:
      ‹∀χ i. i∈I ∧ Ψ i = Neg χ ⟶ hml_srbb_conjunct_models p' (Ψ i)›
    using assms stable_conj_parts by (metis hml_srbb_conjunct.simps(6))
  from p'_spec(2) have ‹∀χ i. i∈I ∧ Ψ i = Pos χ ⟶ hml_srbb_conjunct_models p' (Ψ' i)›
    using assms(1) stable_conj_parts by blast
  hence ‹∀χ i. i∈I ∧ Ψ i = Pos χ ⟶
      hml_srbb_conjunct_models p' (Neg (StableConj {left} (λ_. Neg χ)))›
    unfolding assms by auto
  with ‹stable_state p'› have ‹∀χ i. i∈I ∧ Ψ i = Pos χ ⟶ hml_srbb_inner_models p' χ›
    using stable_state_stable by (auto, metis silent_reachable.simps)
  then have pos_conjuncts:
      ‹∀χ i. i∈I ∧ Ψ i = Pos χ ⟶hml_srbb_conjunct_models p' (Pos χ)›
    using hml_srbb_conjunct_models.simps(1) silent_reachable.simps by blast
  hence ‹hml_srbb_inner_models p' (StableConj I Ψ)›
    using p'_spec assms other_conjuncts
    by (auto, metis other_conjuncts pos_conjuncts hml_srbb_conjunct.exhaust)
  thus ‹p ⊨SRBB Internal (StableConj I Ψ)›
    using p'_spec(1) by auto
qed

definition conjunctify_distinctions ::
  ‹('s ⇒ ('a, 's) hml_srbb) ⇒ 's ⇒ ('s ⇒ ('a, 's) hml_srbb_conjunct)› where
  ‹conjunctify_distinctions Φ p ≡ λq.
    case (Φ q) of
      TT ⇒ undefined
    | Internal χ ⇒ Pos χ
    | ImmConj I Ψ ⇒ Ψ (SOME i. i∈I ∧ hml_srbb_conj.distinguishes (Ψ i) p q)›

lemma distinction_conjunctification:
  assumes
    ‹∀q∈I. distinguishes (Φ q) p q›
  shows
    ‹∀q∈I. hml_srbb_conj.distinguishes ((conjunctify_distinctions Φ p) q) p q›
  unfolding conjunctify_distinctions_def
proof
  fix q
  assume q_I: ‹q∈I›
  show ‹hml_srbb_conj.distinguishes
          (case Φ q of hml_srbb.Internal x ⇒ hml_srbb_conjunct.Pos x
           | ImmConj I Ψ ⇒ Ψ (SOME i. i ∈ I ∧ hml_srbb_conj.distinguishes (Ψ i) p q))
          p q›
  proof (cases ‹Φ q›)
    case TT
    then show ?thesis using assms q_I by fastforce
  next
    case (Internal χ)
    then show ?thesis using assms q_I by auto
  next
    case (ImmConj J Ψ)
    then have ‹∃i ∈ J. hml_srbb_conj.distinguishes (Ψ i) p q›
      using assms q_I by auto
    then show ?thesis
      by (metis (mono_tags, lifting) ImmConj hml_srbb.simps(11) someI)
  qed
qed

lemma distinction_combination:
  fixes p q
  defines
    ‹Qα ≡ {q'. q ↠ q' ∧ (∄φ. distinguishes φ p q')}›
  assumes
    ‹p ↦a α p'›
    ‹∀q'∈ Qα.
      ∀q''. q' ↦a α q'' ⟶ (distinguishes (Φ q'') p' q'')›
  shows
    ‹∀q'∈Qα.
      hml_srbb_inner.distinguishes (Obs α (ImmConj {q''. ∃q'''∈Qα. q''' ↦a α q''}
                                                   (conjunctify_distinctions Φ p'))) p q'›
proof -
  have ‹∀q'∈ Qα. ∀q''∈{q''. q' ↦a α q''}.
      hml_srbb_conj.distinguishes ((conjunctify_distinctions Φ p') q'') p' q''›
  proof clarify
    fix q' q''
    assume ‹q' ∈ Qα› ‹q' ↦a α q''›
    thus ‹hml_srbb_conj.distinguishes (conjunctify_distinctions Φ p' q'') p' q''›
      using distinction_conjunctification assms(3)
      by (metis mem_Collect_eq)
  qed
  hence ‹∀q'∈ Qα. ∀q''∈{q''. ∃q1'∈Qα. q1' ↦a α q''}.
      hml_srbb_conj.distinguishes ((conjunctify_distinctions Φ p') q'') p' q''› by blast
  hence ‹∀q'∈ Qα. ∀q''. q' ↦a α q''
    ⟶ distinguishes (ImmConj {q''. ∃q1'∈Qα. q1' ↦a α q''}
                               (conjunctify_distinctions Φ p')) p' q''› by auto
  thus ‹∀q'∈Qα.
      hml_srbb_inner.distinguishes (Obs α (ImmConj {q''. ∃q'''∈Qα. q''' ↦a α q''}
                                                   (conjunctify_distinctions Φ p'))) p q'›
    by (auto) (metis assms(2))+
qed

definition conjunctify_distinctions_dual ::
  ‹('s ⇒ ('a, 's) hml_srbb) ⇒ 's ⇒ ('s ⇒ ('a, 's) hml_srbb_conjunct)› where
  ‹conjunctify_distinctions_dual Φ p ≡ λq.
    case (Φ q) of
      TT ⇒ undefined
    | Internal χ ⇒ Neg χ
    | ImmConj I Ψ ⇒
      (case Ψ (SOME i. i∈I ∧ hml_srbb_conj.distinguishes (Ψ i) q p) of
        Pos χ ⇒ Neg χ | Neg χ ⇒ Pos χ)›

lemma dual_conjunct:
  assumes
    ‹hml_srbb_conj.distinguishes ψ p q›
  shows
    ‹hml_srbb_conj.distinguishes (case ψ of
               hml_srbb_conjunct.Pos χ ⇒ hml_srbb_conjunct.Neg χ
               | hml_srbb_conjunct.Neg χ ⇒ hml_srbb_conjunct.Pos χ) q p›
  using assms
  by (cases ψ, auto)

lemma distinction_conjunctification_dual:
  assumes
    ‹∀q∈I. distinguishes (Φ q) q p›
  shows
    ‹∀q∈I. hml_srbb_conj.distinguishes (conjunctify_distinctions_dual Φ p q) p q›
  unfolding conjunctify_distinctions_dual_def
proof
  fix q
  assume q_I: ‹q∈I›
  show ‹hml_srbb_conj.distinguishes
          (case Φ q of hml_srbb.Internal x ⇒ hml_srbb_conjunct.Neg x
           | ImmConj I Ψ ⇒
               ( case Ψ (SOME i. i ∈ I ∧ hml_srbb_conj.distinguishes (Ψ i) q p) of
                  hml_srbb_conjunct.Pos x ⇒ hml_srbb_conjunct.Neg x
               | hml_srbb_conjunct.Neg x ⇒ hml_srbb_conjunct.Pos x))
          p q›
  proof (cases ‹Φ q›)
    case TT
    then show ?thesis using assms q_I by fastforce
  next
    case (Internal χ)
    then show ?thesis using assms q_I by auto
  next
    case (ImmConj J Ψ)
    then have ‹∃i ∈ J. hml_srbb_conj.distinguishes (Ψ i) q p›
      using assms q_I by auto
    hence ‹hml_srbb_conj.distinguishes (case Ψ
      (SOME i. i ∈ J ∧ hml_srbb_conj.distinguishes (Ψ i) q p) of
               hml_srbb_conjunct.Pos x ⇒ hml_srbb_conjunct.Neg x
               | hml_srbb_conjunct.Neg x ⇒ hml_srbb_conjunct.Pos x) p q›
      by (metis (no_types, lifting) dual_conjunct someI_ex)
    then show ?thesis unfolding ImmConj by auto
  qed
qed

lemma distinction_conjunctification_two_way:
  fixes Φ p I
  defines
    ‹conjfy q ≡
      (if distinguishes (Φ q) p q
      then conjunctify_distinctions Φ
      else conjunctify_distinctions_dual Φ) p q›
  assumes
    ‹∀q∈I. distinguishes (Φ q) p q ∨ distinguishes (Φ q) q p›
  shows
    ‹∀q∈I. hml_srbb_conj.distinguishes (conjfy q) p q›
proof safe
  fix q
  assume ‹q ∈ I›
  then consider ‹distinguishes (Φ q) p q›
    | ‹distinguishes (Φ q) q p› using assms by blast
  thus ‹hml_srbb_conj.distinguishes (conjfy q) p q›
  proof cases
    case 1
    then show ?thesis using distinction_conjunctification conjfy_def
      by (smt (verit) singleton_iff)
  next
    case 2
    then show ?thesis using distinction_conjunctification_dual singleton_iff
      unfolding distinguishes_def conjfy_def
      by (smt (verit, ccfv_threshold))
  qed
qed

end ― ‹of ‹lts_tau››

end