Theory Branching_Bisimilarity

section ‹Branching Bisimilarity›

theory Branching_Bisimilarity
  imports Eta_Bisimilarity
begin

subsection ‹Definitions of (Stability-Respecting) Branching Bisimilarity›

context LTS_Tau
begin

definition branching_simulation :: ‹('s ⇒ 's ⇒ bool) ⇒ bool› where
  ‹branching_simulation R ≡ ∀p α p' q. R p q ⟶ p ↦ α p' ⟶
    ((α = τ ∧ R p' q) ∨ (∃q' q''. q ↠ q' ∧ q' ↦ α q'' ∧ R p q' ∧ R p' q''))›

lemma branching_simulation_intro:
  assumes
    ‹⋀p α p' q. R p q ⟹ p ↦ α p' ⟹
      ((α = τ ∧ R p' q) ∨ (∃q' q''. q ↠ q' ∧ q' ↦ α q'' ∧ R p q' ∧ R p' q''))›
  shows
    ‹branching_simulation R›
  using assms unfolding branching_simulation_def by simp

definition branching_simulated :: ‹'s ⇒ 's ⇒ bool› where
  ‹branching_simulated p q ≡ ∃R. branching_simulation R ∧ R p q›

definition branching_bisimulated :: ‹'s ⇒ 's ⇒ bool› where
  ‹branching_bisimulated p q ≡ ∃R. branching_simulation R ∧ symp R ∧ R p q›

definition sr_branching_bisimulated :: ‹'s ⇒ 's ⇒ bool› (infix ‹~SRBB› 40) where
  ‹p ~SRBB q ≡ ∃R. branching_simulation R ∧ symp R ∧ stability_respecting R ∧ R p q›

subsection ‹Properties of Branching Bisimulation Equivalences›

lemma branching_bisimilarity_branching_sim: ‹branching_simulation sr_branching_bisimulated›
  unfolding sr_branching_bisimulated_def branching_simulation_def by blast

lemma branching_sim_eta_sim:
  assumes ‹branching_simulation R›
  shows ‹eta_simulation R›
  using assms silent_reachable.refl unfolding branching_simulation_def eta_simulation_def by blast

lemma silence_retains_branching_sim:
assumes
  ‹branching_simulation R›
  ‹R p q›
  ‹p ↠ p'›
shows ‹∃q'. R p' q' ∧ q ↠ q'›
  using assms silence_retains_eta_sim branching_sim_eta_sim by blast

lemma branching_bisimilarity_stability: ‹stability_respecting sr_branching_bisimulated›
  unfolding sr_branching_bisimulated_def stability_respecting_def by blast

lemma sr_branching_bisimulation_silently_retained:
  assumes
    ‹sr_branching_bisimulated p q›
    ‹p ↠ p'›
  shows
    ‹∃q'. q ↠ q' ∧ sr_branching_bisimulated p' q'› using assms(2,1)
  using branching_bisimilarity_branching_sim silence_retains_branching_sim by blast

lemma sr_branching_bisimulation_sim:
  assumes
    ‹sr_branching_bisimulated p q›
    ‹p ↠ p'› ‹p' ↦a α p''›
  shows
    ‹∃q' q''. q ↠ q' ∧ q' ↦a α q'' ∧ sr_branching_bisimulated p' q' ∧ sr_branching_bisimulated p'' q''›
proof -
  obtain q' where ‹q ↠ q'› ‹sr_branching_bisimulated p' q'›
    using assms sr_branching_bisimulation_silently_retained by blast
  thus ?thesis
    using assms(3) branching_bisimilarity_branching_sim silent_reachable_trans
    unfolding branching_simulation_def
    by blast
qed

lemma sr_branching_bisimulated_sym:
  assumes
    ‹sr_branching_bisimulated p q›
  shows
    ‹sr_branching_bisimulated q p›
  using assms unfolding sr_branching_bisimulated_def by (meson sympD)

lemma sr_branching_bisimulated_symp:
  shows ‹symp (~SRBB)›
  using sr_branching_bisimulated_sym
  using sympI by blast

lemma sr_branching_bisimulated_reflp:
  shows ‹reflp (~SRBB)›
    unfolding sr_branching_bisimulated_def stability_respecting_def reflp_def
    using silence_retains_branching_sim silent_reachable.refl
    by (smt (verit) DEADID.rel_symp branching_simulation_intro)

lemma establish_sr_branching_bisim:
  assumes
    ‹∀α p'. p ↦ α p' ⟶
    ((α = τ ∧ p' ~SRBB q) ∨ (∃q' q''. q ↠ q' ∧ q' ↦ α q'' ∧ p ~SRBB q' ∧ p' ~SRBB q''))›
    ‹∀α q'. q ↦ α q' ⟶
    ((α = τ ∧ p ~SRBB q') ∨ (∃p' p''. p ↠ p' ∧ p' ↦ α p'' ∧ p' ~SRBB q ∧ p'' ~SRBB q'))›
    ‹stable_state p ⟶ (∃q'. q ↠ q' ∧ p ~SRBB q' ∧ stable_state q')›
    ‹stable_state q ⟶ (∃p'. p ↠ p' ∧ p' ~SRBB q ∧ stable_state p')›
  shows ‹p ~SRBB q›
proof -
  define R where ‹R ≡ λpp qq. pp ~SRBB qq ∨ (pp = p ∧ qq = q) ∨ (pp = q ∧ qq = p)›
  hence
    R_cases: ‹⋀pp qq. R pp qq ⟹ pp ~SRBB qq ∨ (pp = p ∧ qq = q) ∨ (pp = q ∧ qq = p)› and
    bisim_extension: ‹∀pp qq. pp ~SRBB qq ⟶ R pp qq› by blast+
  have ‹symp R›
    unfolding symp_def R_def sr_branching_bisimulated_def
    by blast
  moreover have ‹stability_respecting R›
    unfolding stability_respecting_def
  proof safe
    fix pp qq
    assume ‹R pp qq› ‹stable_state pp›
    then consider ‹pp ~SRBB qq› | ‹pp = p ∧ qq = q› | ‹pp = q ∧ qq = p›
      using R_cases by blast
    thus ‹∃q'. qq ↠ q' ∧ R pp q' ∧ stable_state q'›
    proof cases
      case 1
      then show ?thesis
        using branching_bisimilarity_stability ‹stable_state pp› bisim_extension
        unfolding stability_respecting_def
        by blast
    next
      case 2
      then show ?thesis
        using assms(3) ‹stable_state pp› unfolding R_def by blast
    next
      case 3
      then show ?thesis
        using assms(4) ‹stable_state pp› ‹symp R› unfolding R_def
        by (meson sr_branching_bisimulated_sym)
    qed
  qed
  moreover have ‹branching_simulation R› unfolding branching_simulation_def
  proof clarify
    fix pp α p' qq
    assume bc: ‹R pp qq› ‹pp ↦ α p'› ‹∄q' q''. qq ↠ q' ∧ q' ↦ α q'' ∧ R pp q' ∧ R p' q''›
    then consider ‹pp ~SRBB qq› | ‹pp = p ∧ qq = q› | ‹pp = q ∧ qq = p›
      using R_cases by blast
    thus ‹α = τ ∧ R p' qq›
    proof cases
      case 1
      then show ?thesis
        by (smt (verit, del_insts) bc bisim_extension
            branching_bisimilarity_branching_sim branching_simulation_def)
    next
      case 2
      then show ?thesis
        using bc assms(1) bisim_extension by blast
    next
      case 3
      then show ?thesis
        using bc assms(2) bisim_extension sr_branching_bisimulated_sym by metis
    qed
  qed
  moreover have ‹R p q› unfolding R_def by blast
  ultimately show ?thesis
    unfolding sr_branching_bisimulated_def by blast
qed

lemma sr_branching_bisimulation_stuttering:
  assumes
    ‹pp ≠ []›
    ‹∀i < length pp - 1.  pp!i ↦ τ pp!(Suc i)›
    ‹hd pp ~SRBB last pp›
    ‹i < length pp›
  shows
    ‹hd pp ~SRBB pp!i›
proof -
  have chain_reachable: ‹∀j < length pp. ∀i ≤ j. pp!i ↠ pp!j›
    using tau_chain_reachabilty assms(2) .
  hence chain_hd_last:
    ‹∀i < length pp. hd pp ↠ pp!i›
    ‹∀i < length pp.  pp!i ↠ last pp›
    by (auto simp add: assms(1) hd_conv_nth last_conv_nth)
  define R where ‹R ≡ λp q. (p = hd pp ∧ (∃i < length pp. pp!i = q)) ∨ ((q = hd pp ∧ (∃i < length pp. pp!i = p))) ∨ p ~SRBB q›
  have later_hd_sim: ‹⋀i p' α. i < length pp ⟹ pp!i ↦ α p'
    ⟹ (hd pp) ↠ (pp!i) ∧ (pp!i) ↦ α p' ∧ R (pp!i) (pp!i) ∧ R p' p'›
    using chain_hd_last sr_branching_bisimulated_reflp
    unfolding R_def
    by (simp add: reflp_def)
  have hd_later_sim: ‹⋀i p' α. i < length pp - 1 ⟹ (hd pp) ↦ α p'
    ⟹ (∃q' q''. (pp!i) ↠ q' ∧ q' ↦ α q'' ∧ R (hd pp) q' ∧ R p' q'')›
  proof -
    fix i p' α
    assume case_assm: ‹i < length pp - 1› ‹(hd pp) ↦ α p'›
    hence ‹(α = τ ∧ p' ~SRBB (last pp)) ∨ (∃q' q''. (last pp) ↠ q' ∧ q' ↦ α q'' ∧ (hd pp) ~SRBB q' ∧ p' ~SRBB q'')›
      using ‹hd pp ~SRBB last pp› branching_bisimilarity_branching_sim branching_simulation_def
      by auto
    thus ‹(∃q' q''. (pp!i) ↠ q' ∧ q' ↦ α q'' ∧ R (hd pp) q' ∧ R p' q'')›
    proof
      assume tau_null_step: ‹α = τ ∧ p' ~SRBB last pp›
      have ‹pp ! i ↠ (pp!(length pp - 2))›
        using case_assm(1) chain_reachable by force
      moreover have ‹pp!(length pp - 2) ↦ α (last pp)›
        using assms(1,2) case_assm(1) last_conv_nth tau_null_step
        by (metis Nat.lessE Suc_1 Suc_diff_Suc less_Suc_eq zero_less_Suc zero_less_diff)
      moreover have ‹R (hd pp) (pp!(length pp - 2)) ∧ R p' (last pp)›
        unfolding R_def
        by (metis assms(1) diff_less length_greater_0_conv less_2_cases_iff tau_null_step)
      ultimately show ‹∃q' q''. pp ! i ↠ q' ∧ q' ↦ α q'' ∧ R (hd pp) q' ∧ R p' q''› by blast
    next
      assume ‹∃q' q''. last pp ↠ q' ∧ q' ↦ α q'' ∧ hd pp ~SRBB q' ∧ p' ~SRBB q''›
      hence ‹∃q' q''. last pp ↠ q' ∧ q' ↦ α q'' ∧ R (hd pp) q' ∧ R p' q''›
        unfolding R_def by blast
      moreover have ‹i < length pp› using case_assm by auto
      ultimately show ‹∃q' q''. pp ! i ↠ q' ∧ q' ↦ α q'' ∧ R (hd pp) q' ∧ R p' q''›
        using chain_hd_last silent_reachable_trans by blast
    qed
  qed
  have ‹branching_simulation R›
  proof (rule branching_simulation_intro)
    fix p α p' q
    assume challenge: ‹R p q› ‹p ↦ α p'›
    from this(1) consider
      ‹(p = hd pp ∧ (∃i < length pp. pp!i = q))› |
      ‹(q = hd pp ∧ (∃i < length pp. pp!i = p))› |
      ‹ p ~SRBB q› unfolding R_def by blast
    thus ‹α = τ ∧ R p' q ∨ (∃q' q''. q ↠ q' ∧ q' ↦ α q'' ∧ R p q' ∧ R p' q'')›
    proof cases
      case 1
      then obtain i where i_spec: ‹i < length pp› ‹pp ! i = q› by blast
      from 1 have ‹p = hd pp› ..
      show ?thesis
      proof (cases ‹i = length pp - 1›)
        case True
        then have ‹q = last pp› using i_spec assms(1)
          by (simp add: last_conv_nth)
        then show ?thesis using challenge(2) assms(3) branching_bisimilarity_branching_sim
          unfolding R_def branching_simulation_def ‹p = hd pp›
          by metis
      next
        case False
        hence ‹i < length pp - 1› using i_spec by auto
        then show ?thesis using ‹p = hd pp› i_spec hd_later_sim challenge(2) by blast
      qed
    next
      case 2
      then show ?thesis
        using later_hd_sim challenge(2) by blast
    next
      case 3
      then show ?thesis
        using challenge(2) branching_bisimilarity_branching_sim
        unfolding branching_simulation_def R_def by metis
    qed
  qed
  moreover have ‹symp R›
    using sr_branching_bisimulated_sym
    unfolding R_def sr_branching_bisimulated_def
    by (smt (verit, best) sympI)
  moreover have ‹stability_respecting R›
    using assms(3) stable_state_stable sr_branching_bisimulated_sym
      branching_bisimilarity_stability
    unfolding R_def stability_respecting_def
    by (metis chain_hd_last)
  moreover have ‹⋀i. i < length pp ⟹ R (hd pp) (pp!i)› unfolding R_def by auto
  ultimately show ?thesis
    using assms(4) sr_branching_bisimulated_def by blast
qed

lemma sr_branching_bisimulation_stabilizes:
  assumes
    ‹sr_branching_bisimulated p q›
    ‹stable_state p›
  shows
    ‹∃q'. q ↠ q' ∧ sr_branching_bisimulated p q' ∧ stable_state q'›
proof -
  from assms obtain R where
    R_spec: ‹branching_simulation R› ‹symp R› ‹stability_respecting R› ‹R p q›
    unfolding sr_branching_bisimulated_def by blast
  then obtain q' where ‹q ↠ q'› ‹stable_state q'›
    using assms(2) unfolding stability_respecting_def by blast
  moreover have ‹sr_branching_bisimulated p q'›
    using sr_branching_bisimulation_stuttering
     assms(1) calculation(1) sr_branching_bisimulated_def sympD
    by (metis assms(2) sr_branching_bisimulation_silently_retained stable_state_stable)
  ultimately show ?thesis by blast
qed

lemma sr_branching_bisim_stronger:
  assumes
    ‹sr_branching_bisimulated p q›
  shows
    ‹branching_bisimulated p q›
  using assms unfolding sr_branching_bisimulated_def branching_bisimulated_def by auto

subsection ‹‹HML_SRBB› as Modal Characterization of Stability-Respecting Branching Bisimilarity›

lemma modal_sym: ‹symp (preordered UNIV)›
proof-
  have ‹∄ p q. preordered UNIV p q ∧ ¬preordered UNIV q p›
  proof safe
    fix p q
    assume contradiction:
      ‹preordered UNIV p q›
      ‹¬preordered UNIV q p›
    then obtain φ where φ_distinguishes: ‹distinguishes φ q p› by auto
    thus False
    proof (cases φ)
      case TT
      then show ?thesis using φ_distinguishes by auto
    next
      case (Internal χ)
      hence ‹distinguishes (ImmConj {undefined} (λi. Neg χ)) p q›
        using φ_distinguishes by simp
      then show ?thesis using contradiction preordered_no_distinction by blast
    next
      case (ImmConj I Ψ)
      then obtain i where i_def: ‹i ∈ I› ‹hml_srbb_conj.distinguishes (Ψ i) q p›
        using φ_distinguishes srbb_dist_imm_conjunction_implies_dist_conjunct by auto
      then show ?thesis
      proof (cases ‹Ψ i›)
        case (Pos χ)
        hence ‹distinguishes (ImmConj {undefined} (λi. Neg χ)) p q› using i_def by simp
        thus ?thesis using contradiction preordered_no_distinction by blast
      next
        case (Neg χ)
        hence ‹distinguishes (Internal χ) p q› using i_def by simp
        thus ?thesis using contradiction preordered_no_distinction by blast
      qed
    qed
  qed
  thus ?thesis unfolding symp_def by blast
qed

lemma modal_branching_sim: ‹branching_simulation (preordered UNIV)›
proof -
  have ‹∄p α p' q. (preordered UNIV) p q ∧ p ↦ α p' ∧
      (α ≠ τ ∨ ¬(preordered UNIV) p' q) ∧
      (∀q' q''. q ↠ q' ⟶ q' ↦ α q'' ⟶ ¬ preordered UNIV p q' ∨ ¬ preordered UNIV p' q'')›
  proof clarify
    fix p α p' q
    define Qα where ‹Qα ≡ {q'. q ↠ q' ∧ (∄φ. distinguishes φ p q')}›
    assume contradiction:
      ‹preordered UNIV p q› ‹p ↦ α p'›
      ‹∀q' q''. q ↠ q' ⟶ q' ↦ α q'' ⟶ ¬ preordered UNIV p q' ∨ ¬ preordered UNIV p' q''›
      ‹α ≠ τ ∨ ¬ preordered UNIV p' q›
    hence distinctions: ‹∀q'. q ↠ q' ⟶
      (∃φ. distinguishes φ p q') ∨
      (∀q''. q' ↦a α q'' ⟶ (∃φ. distinguishes φ p' q''))›
      using preordered_no_distinction
      by (metis equivpI equivp_def lts_semantics.preordered_preord modal_sym)
    hence ‹∀q''. ∀q'∈Qα.
        q' ↦a α q'' ⟶ (∃φ. distinguishes φ p' q'')›
      unfolding Qα_def by auto
    hence ‹∀q''. (∃q'. q ↠ q' ∧ (∄φ. distinguishes φ p q') ∧ q' ↦a α q'')
        ⟶ (∃φ. distinguishes φ p' q'')›
      unfolding Qα_def by blast
    then obtain Φα where
      ‹∀q''. (∃q'. q ↠ q' ∧ (∄φ. distinguishes φ p q') ∧ q' ↦a α q'')
        ⟶ distinguishes (Φα q'') p' q''› by metis
    hence distinctions_α: ‹∀q'∈Qα. ∀q''.
        q' ↦a α q'' ⟶ distinguishes (Φα q'') p' q''›
      unfolding Qα_def by blast
    from distinctions obtain Φη where
      ‹∀q'. q'∈{q'. q ↠ q' ∧ (∃φ. distinguishes φ p q')}
        ⟶ distinguishes (Φη q') p q'› unfolding mem_Collect_eq by moura
    with distinction_conjunctification obtain Ψη where distinctions_η:
      ‹∀q'∈{q'. q ↠ q' ∧ (∃φ. distinguishes φ p q')}. hml_srbb_conj.distinguishes (Ψη q') p q'›
      by blast
    have ‹p ↦a α p'› using ‹p ↦ α p'› by auto
    from distinction_combination[OF this] distinctions_α have obs_dist:
      ‹∀q'∈Qα.
        hml_srbb_inner.distinguishes (Obs α (ImmConj {q''. ∃q'''∈Qα. q''' ↦a α q''}
                                                     (conjunctify_distinctions Φα p'))) p q'›
      unfolding Qα_def by blast
    with distinctions_η have
      ‹hml_srbb_inner_models p (BranchConj α
          (ImmConj {q''. ∃q'''∈Qα. q''' ↦a α q''}
                   (conjunctify_distinctions Φα p'))
          {q'. q ↠ q' ∧ (∃φ. distinguishes φ p q')} Ψη)›
      using contradiction(1) silent_reachable.refl
      unfolding Qα_def distinguishes_def hml_srbb_conj.distinguishes_def hml_srbb_inner.distinguishes_def preordered_def
      by simp force
    moreover have ‹∀q'. q ↠ q' ⟶ ¬ hml_srbb_inner_models q'
        (BranchConj α (ImmConj {q''. ∃q'''∈Qα. q''' ↦a α q''} (conjunctify_distinctions Φα p')) {q'. q ↠ q' ∧ (∃φ. distinguishes φ p q')} Ψη)›
    proof safe
      fix q'
      assume contradiction: ‹q ↠ q'›
        ‹hml_srbb_inner_models q' (BranchConj α (ImmConj {q''. ∃q'''∈Qα. q''' ↦a α q''} (conjunctify_distinctions Φα p')) {q'. q ↠ q' ∧ (∃φ. distinguishes φ p q')} Ψη)›
      thus ‹False›
        using obs_dist distinctions_η
        unfolding distinguishes_def hml_srbb_conj.distinguishes_def hml_srbb_inner.distinguishes_def Qα_def
        by (auto) blast+
    qed
    ultimately have ‹distinguishes (Internal (BranchConj α (ImmConj {q''. ∃q'''∈Qα. q''' ↦a α q''} (conjunctify_distinctions Φα p')) {q'. q ↠ q' ∧ (∃φ. distinguishes φ p q')} Ψη)) p q›
      unfolding distinguishes_def Qα_def
      using silent_reachable.refl by (auto) blast+
    thus False using contradiction(1) preordered_no_distinction by blast
  qed
  thus ?thesis
    unfolding branching_simulation_def by blast
qed

lemma logic_sr_branching_bisim_invariant:
  assumes
    ‹sr_branching_bisimulated p0 q0›
    ‹p0 ⊨SRBB φ›
  shows ‹q0 ⊨SRBB φ›
proof-
  have ‹⋀φ χ ψ.
    (∀p q. sr_branching_bisimulated p q ⟶ p ⊨SRBB φ ⟶ q ⊨SRBB φ) ∧
    (∀p q. sr_branching_bisimulated p q ⟶ hml_srbb_inner_models p χ ⟶ (∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ)) ∧
    (∀p q. sr_branching_bisimulated p q ⟶ hml_srbb_conjunct_models p ψ ⟶ hml_srbb_conjunct_models q ψ)›
  proof-
    fix φ χ ψ
    show
      ‹(∀p q. sr_branching_bisimulated p q ⟶ p ⊨SRBB φ ⟶ q ⊨SRBB φ) ∧
      (∀p q. sr_branching_bisimulated p q ⟶ hml_srbb_inner_models p χ ⟶ (∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ)) ∧
      (∀p q. sr_branching_bisimulated p q ⟶ hml_srbb_conjunct_models p ψ ⟶ hml_srbb_conjunct_models q ψ)›
    proof (induct rule: hml_srbb_hml_srbb_inner_hml_srbb_conjunct.induct)
      case TT
      then show ?case by simp
    next
      case (Internal χ)
      show ?case
      proof safe
        fix p q
        assume ‹sr_branching_bisimulated p q› ‹p ⊨SRBB hml_srbb.Internal χ›
        then obtain p' where ‹p ↠ p'› ‹hml_srbb_inner_models p' χ› by auto
        hence ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ› using Internal ‹hml_srbb_inner_models p' χ›
          by (meson LTS_Tau.silent_reachable_trans ‹p ~SRBB q› sr_branching_bisimulation_silently_retained)
        thus ‹q ⊨SRBB hml_srbb.Internal χ› by auto
      qed
    next
      case (ImmConj I Ψ)
      then show ?case by auto
    next
      case (Obs α φ)
      then show ?case
      proof (safe)
        fix p q
        assume
          ‹sr_branching_bisimulated p q›
          ‹hml_srbb_inner_models p (hml_srbb_inner.Obs α φ)›
        then obtain p' where ‹p ↦a α p'› ‹p' ⊨SRBB φ› by auto
        then obtain q' q'' where ‹q ↠ q'› ‹q' ↦a α q''› ‹sr_branching_bisimulated p' q''›
          using sr_branching_bisimulation_sim[OF ‹sr_branching_bisimulated p q›] silent_reachable.refl
          by blast
        hence ‹q'' ⊨SRBB φ› using ‹p' ⊨SRBB φ› Obs by blast
        hence ‹hml_srbb_inner_models q' (hml_srbb_inner.Obs α φ)›
          using ‹q' ↦a α q''› by auto
        thus ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (hml_srbb_inner.Obs α φ)›
          using ‹q ↠ q'› by blast
      qed
    next
      case (Conj I Ψ)
      show ?case
      proof safe
        fix p q
        assume
          ‹sr_branching_bisimulated p q›
          ‹hml_srbb_inner_models p (hml_srbb_inner.Conj I Ψ)›
        hence ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)› by auto
        hence ‹∀i∈I. hml_srbb_conjunct_models q (Ψ i)›
          using Conj ‹sr_branching_bisimulated p q› by blast
        hence ‹hml_srbb_inner_models q (hml_srbb_inner.Conj I Ψ)› by simp
        thus ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (hml_srbb_inner.Conj I Ψ)›
          using silent_reachable.refl by blast
      qed
    next
      case (StableConj I Ψ) show ?case
      proof safe
        fix p q
        assume
          ‹sr_branching_bisimulated p q›
          ‹hml_srbb_inner_models p (StableConj I Ψ)›
        hence ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)›
          using stable_conj_parts by blast
        from ‹hml_srbb_inner_models p (StableConj I Ψ)› have ‹stable_state p› by auto
        then obtain q' where ‹q ↠ q'› ‹stable_state q'› ‹sr_branching_bisimulated p q'›
          using ‹sr_branching_bisimulated p q› sr_branching_bisimulation_stabilizes by blast
        hence ‹∀i∈I. hml_srbb_conjunct_models q' (Ψ i)›
          using ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)› StableConj by blast
        hence ‹hml_srbb_inner_models q' (StableConj I Ψ)› using ‹stable_state q'› by simp
        thus ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (StableConj I Ψ)›
          using ‹q ↠ q'› by blast
      qed
    next
      case (BranchConj α φ I Ψ)
      show ?case
      proof safe
        fix p q
        assume
          ‹sr_branching_bisimulated p q›
          ‹hml_srbb_inner_models p (BranchConj α φ I Ψ)›
        hence ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)›
              ‹hml_srbb_inner_models p (Obs α φ)›
          using branching_conj_parts branching_conj_obs by blast+
        then obtain p' where ‹p ↦a α p'› ‹p' ⊨SRBB φ› by auto
        then obtain q' q'' where q'_q''_spec:
          ‹q ↠ q'› ‹q' ↦a α q''›
          ‹sr_branching_bisimulated p q'› ‹sr_branching_bisimulated p' q''›
          using sr_branching_bisimulation_sim[OF ‹sr_branching_bisimulated p q›]
            silent_reachable.refl[of p]
          by blast
        hence ‹q'' ⊨SRBB φ› using BranchConj.hyps ‹p' ⊨SRBB φ› by auto
        hence ‹hml_srbb_inner_models q' (Obs α φ)› using q'_q''_spec by auto
        moreover have ‹∀i∈I. hml_srbb_conjunct_models q' (Ψ i)›
          using BranchConj.hyps ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)› q'_q''_spec by blast
        ultimately show ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (BranchConj α φ I Ψ)›
          using ‹q ↠ q'› by auto
      qed
    next
      case (Pos χ)
      show ?case
      proof safe
        fix p q
        assume
          ‹sr_branching_bisimulated p q›
          ‹hml_srbb_conjunct_models p (Pos χ)›
        then obtain p' where ‹p ↠ p'› ‹hml_srbb_inner_models p' χ› by auto
        then obtain q' where ‹q ↠ q'› ‹hml_srbb_inner_models q' χ›
          using Pos ‹p ~SRBB q› sr_branching_bisimulation_silently_retained
          by (meson  silent_reachable_trans)
        thus ‹hml_srbb_conjunct_models q (Pos χ)› by auto
      qed
    next
      case (Neg χ)
      show ?case
      proof safe
        fix p q
        assume
          ‹sr_branching_bisimulated p q›
          ‹hml_srbb_conjunct_models p (Neg χ)›
        hence ‹∀p'. p ↠ p' ⟶ ¬hml_srbb_inner_models p' χ› by simp
        moreover have
          ‹(∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ) ⟶ (∃p'. p ↠ p' ∧ hml_srbb_inner_models p' χ)›
          using Neg sr_branching_bisimulated_sym[OF ‹sr_branching_bisimulated p q›]
            sr_branching_bisimulation_silently_retained
          by (meson silent_reachable_trans)
        ultimately have ‹∀q'. q ↠ q' ⟶ ¬hml_srbb_inner_models q' χ› by blast
        thus ‹hml_srbb_conjunct_models q (Neg χ)› by simp
      qed
    qed
  qed
  thus ?thesis using assms by blast
qed

lemma sr_branching_bisim_is_hmlsrbb: ‹sr_branching_bisimulated p q = preordered UNIV p q›
  using modal_stability_respecting modal_sym modal_branching_sim logic_sr_branching_bisim_invariant
    𝒪_sup preordered_def
  unfolding sr_branching_bisimulated_def by metis

lemma sr_branching_bisimulated_transitive:
  assumes
    ‹p ~SRBB q›
    ‹q ~SRBB r›
  shows
    ‹p ~SRBB r›
  using assms unfolding sr_branching_bisim_is_hmlsrbb by simp

lemma sr_branching_bisimulated_equivalence: ‹equivp (~SRBB)›
proof (rule equivpI)
  show ‹symp (~SRBB)› using sr_branching_bisimulated_symp .
  show ‹reflp (~SRBB)› using sr_branching_bisimulated_reflp .
  show ‹transp (~SRBB)›
    unfolding transp_def using sr_branching_bisimulated_transitive by blast
qed

lemma sr_branching_bisimulation_stuttering_all:
  assumes
    ‹pp ≠ []›
    ‹∀i < length pp - 1.  pp!i ↦ τ pp!(Suc i)›
    ‹hd pp ~SRBB last pp›
    ‹i ≤ j› ‹j < length pp›
  shows
    ‹pp!i ~SRBB pp!j›
  using assms equivp_def sr_branching_bisimulated_equivalence equivp_def order_le_less_trans
    sr_branching_bisimulation_stuttering
  by metis

theorem ‹(p ~SRBB q) = (p ≼ (E ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞) q)›
  using sr_branching_bisim_is_hmlsrbb 𝒪_sup
  unfolding expr_preord_def by auto

end

end