Theory Reactive_Bisimilarity

(*<*)
theory Reactive_Bisimilarity
imports 
  Labelled_Transition_Systems_with_TimeOuts
begin
(*>*)

section ‹Reactive Bisimilarity›
text ‹\label{sec:reactive_bisimilarity}›

text ‹In the examples of the previous section, we saw that there are \LTSt{}s with transitions that can never be performed or that can only be performed in certain environments. The behavioural equivalence implied hereby is defined in @{cite rbs} as \emph{strong reactive bisimilarity}.

\example{%
The processes $p$ and $q$ are behaviourally equivalent for \LTSt{} semantics, i.e.\@ strongly reactive bisimilar.

\lts{
    \node[state]    (p0)                            {$p$};
    \node[state]    (p1) [below left of=p0]         {$p_1$};
    \node[state]    (p2) [below right of=p0]        {$p_2$};
    \node[state]    (p3) [below left of=p2]         {$p_3$};
    \node[state]    (p4) [below right of=p2]        {$p_4$};
    
    \path   (p0) edge node[above left]  {$a$}   (p1)
                 edge node              {$t$}   (p2)
            (p2) edge node[above left]  {$\tau$}(p3)
                 edge node              {$a$}   (p4);
                 
    \node[state]    (q0) [right of=p0,xshift=5cm]   {$q$};
    \node[state]    (q1) [below left of=q0]         {$q_1$};
    \node[state]    (q2) [below right of=q0]        {$q_2$};
    \node[state]    (q3) [below left of=q2]         {$q_3$};
    
    \path   (q0) edge node[above left]  {$a$}   (q1)
                 edge node              {$t$}   (q2)
            (q2) edge node[above left]  {$\tau$}(q3);
}}›

subsubsection ‹Strong Reactive Bisimulations›
text ‹Van~Glabbeek introduces several characterisations of this equivalence, beginning with \emph{strong reactive bisimulation} (SRB) relations. These differ from strong bisimulations in that the relations contain not only pairs of processes, $(p,q)$, but additionally triples consisting of two processes and a set of actions, $(p,X,q)$. The following definition of SRBs is quoted, with minor adaptations, from @{cite ‹definition 1› rbs}:

A \emph{strong reactive bisimulation} is a symmetric relation 
$$\mathcal{R} \subseteq (\Proc \times \mathcal{P}(A) \times \Proc) \cup (\Proc \times \Proc)$$
(meaning that $(p,X,q)\!\in\!\mathcal{R}\!\iff\!(q,X,p)\!\in\!\mathcal{R}$ and
$(p,q)\!\in\!\mathcal{R}\!\iff\!(q,p)\!\in\!\mathcal{R}$),\\
such that,
\newpage
for all $(p,q) \in \mathcal{R}$:
\begin{enumerate}
    \item if $p \xrightarrow{\tau} p'$, then $\exists q'$ such that $q \xrightarrow{\tau} q'$ and $(p',q') \in \mathcal{R}$,
    \item $(p,X,q) \in \mathcal{R}$ for all $X \subseteq A$,
\end{enumerate}
and for all $(p,X,q) \in \mathcal{R}$:
\begin{enumerate}
    \setcounter{enumi}{2}
    \item if $p \xrightarrow{a} p'$ with $a \in X$, then $\exists q'$ such that $q \xrightarrow{a} q'$ and $(p',q') \in \mathcal{R}$,
    \item if $p \xrightarrow{\tau} p'$, then $\exists q'$ such that $q \xrightarrow{\tau} q'$ and $(p',X,q') \in \mathcal{R}$,
    \item if $\mathcal{I}(p) \cap (X \cup \{\tau\}) = \emptyset$, then $(p,q) \in \mathcal{R}$, and
    \item if $\mathcal{I}(p) \cap (X \cup \{\tau\}) = \emptyset$ and $p \xrightarrow{t} p'$, then $\exists q'$ such that $q \xrightarrow{t} q'$\\and $(p',X,q') \in \mathcal{R}$.
\end{enumerate}

We can derive the following intuitions: an environment can either be stable, allowing a specific set of actions, or indeterminate. Indeterminate environments cannot facilitate any transitions, but they can stabilise into arbitrary stable environments. This is expressed by clause 2. Hence, $X$-bisimilarity is behavioural equivalence in stable environments~$X$, and reactive bisimilarity is behavioural equivalence in indeterminate environments (and thus in arbitrary stable environments).

Since only stable environments can facilitate transitions, there are no clauses involving visible action transitions for $(p,q) \in \mathcal{R}$. However, $\tau$-transitions can be performed regardless of the environment, hence clause 1.

At this point, it is important to discuss what exactly it means for an action to be visible or hidden in this context: as we saw in the last section, the environment cannot react (change its set of allowed actions) when the system performs a $\tau$- or a $t$-transition, since these are hidden actions. However, since we are talking about a \emph{strong} bisimilarity (as opposed to e.g.\@ weak bisimilarity), the performance of $\tau$- or $t$-transitions is still relevant when examining and comparing the behavior of systems.

With that, we can look more closely at the remaining clauses:
in clause 3, given $(p,X,q) \in \mathcal{R}$, for $p \xrightarrow{a} p'$ with $a \in X$, we require for the \enquote{mirroring} state $q'$ that $(p',q') \in \mathcal{R}$, because $a$ is a visible action and the transition can thus trigger a change of the environment;%
\footnote{This is why van~Glabbeek talks about \emph{triggered} environments rather than indeterminate ones. I will use both terms interchangeably.}
on the other hand, in clause 4, for $p \xrightarrow{\tau} p'$, and in clause 6, for $p \xrightarrow{t} p'$, we require $(p',X,q') \in \mathcal{R}$, because these actions are hidden and cannot trigger a change of the environment.

Lastly, clause 5 formalises the possibility of the environment timing out (i.e.\@ turning into an indeterminate environment) instead of the system.

These intuitions also form the basis for the process mapping which will be presented in \cref{sec:mapping_lts}.›


subsubsection ‹Strong Reactive/$X$-Bisimilarity›
text ‹Two processes $p$ and $q$ are \emph{strongly reactive bisimilar} ($p \leftrightarrow_r q$) iff there is an SRB containing $(p,q)$, and \emph{strongly $X$-bisimilar} ($p \leftrightarrow_r^X q$), i.e.\@ equivalent in environments~$X$, when there is an SRB containing $(p,X,q)$.›


subsubsection ‹Generalised Strong Reactive Bisimulations›
text ‹Another characterisation of reactive bisimilarity uses \emph{generalised strong reactive bisimulation} (GSRB) relations @{cite ‹definition 3› rbs}, defined over the same set as SRBs. It is proved that both characterisations do, in fact, characterise the same equivalence. More details will be discussed in the formalisation below.›


subsection ‹Isabelle›

text ‹We first formalise both SRB and GSRB relations (as well as strong reactive bisimilarity, defined by the existence of an SRB, as above), and then replicate the proof of their correspondence.›


subsubsection ‹Strong Reactive Bisimulations›

text ‹SRB relations are defined over the set
$$(\Proc \times \mathscr{P}(A) \times \Proc) \cup (\Proc \times \Proc).$$

As can be easily seen, this set it isomorphic to
$$(\Proc \times (\mathscr{P}(A) \cup \{\bot\}) \times \Proc),$$
which is a subset of
$$(\Proc \times (\mathscr{P}(\Act) \cup \{\bot\}) \times \Proc).$$ 

This last set can now be easily formalised in terms of a type, where we formalise
$\mathscr{P}(\Act) \cup \{\bot\}$
as ‹'a set option›.

The fact that SRBs are defined using the power set of visible actions ($A$), whereas our type uses all actions ($\Act$ / ‹'a›), is handled by the first line of the definition below. The second line formalises that symmetry is required by definition. All other lines are direct formalisations of the clauses of the original definition.
\pagebreak›

context lts_timeout begin

― ‹strong reactive bisimulation @{cite ‹definition 1› rbs}›
definition SRB :: ‹('s ⇒ 'a set option ⇒ 's ⇒ bool) ⇒ bool›
  where ‹SRB R ≡
  (∀ p X q. R p (Some X) q  ⟶  X ⊆ visible_actions) ∧
  (∀ p XoN q. R p XoN q  ⟶  R q XoN p) ∧

  (∀ p q. R p None q ⟶
    (∀ p'. p ⟼τ p'  ⟶  (∃ q'. (q ⟼τ q') ∧ R p' None q')) ∧
    (∀ X ⊆ visible_actions. (R p (Some X) q))) ∧

  (∀ p X q. R p (Some X) q ⟶
    (∀ p' a. p ⟼a p' ∧ a ∈ X  ⟶  (∃ q'. (q ⟼a q') ∧ 
      R p' None q')) ∧
    (∀ p'. p ⟼τ p'  ⟶  (∃ q'. (q ⟼τ q') ∧ R p' (Some X) q')) ∧
    (idle p X  ⟶  R p None q) ∧
    (∀ p'. idle p X ∧ (p ⟼t p')  ⟶  (∃ q'. q ⟼t q' ∧ 
      R p' (Some X) q')))›

(* This lemma simply translates the definition above into simple implications that are easy-to-use in proofs. It is not relevant for the thesis document. *)
(*<*)
lemma✐‹tag (proof) unimportant› SRB_ruleformat:
  assumes ‹SRB R›
  shows 
    ‹R p (Some X) q ⟹ X ⊆ visible_actions›
    ‹R p XoN q ⟹ R q XoN p›
    ‹R p None q ⟹ p ⟼τ p' ⟹ ∃ q'. (q ⟼τ q') ∧ R p' None q'›
    ‹R p None q ⟹ X ⊆ visible_actions ⟹ R p (Some X) q›
    ‹R p (Some X) q ⟹ p ⟼a p' ⟹ a ∈ X ⟹ ∃ q'. (q ⟼a q') ∧ R p' None q'›
    ‹R p (Some X) q ⟹ p ⟼τ p' ⟹ ∃ q'. (q ⟼τ q') ∧ R p' (Some X) q'›
    ‹R p (Some X) q ⟹ idle p X ⟹ R p None q›
    ‹R p (Some X) q ⟹ idle p X ⟹ p ⟼t p' ⟹ ∃ q'. q ⟼t q' ∧ R p' (Some X) q'›
  using assms unfolding SRB_def by metis+
(*>*)

subsubsection ‹Strong Reactive/$X$-Bisimilarity›

text ‹Van~Glabbeek differentiates between strong reactive bisimilarity ($(p,q) \in \mathcal{R}$ for an SRB $\mathcal{R}$) and strong $X$-bisimilarity ($(p,X,q) \in \mathcal{R}$ for an SRB $\mathcal{R}$).›

definition strongly_reactive_bisimilar :: ‹'s ⇒ 's ⇒ bool› 
  (‹_ ↔⇩r _› [70, 70] 70)
  where ‹p ↔⇩r q ≡ ∃ R. SRB R ∧ R p None q›

definition strongly_X_bisimilar :: ‹'s ⇒ 'a set ⇒ 's ⇒ bool› 
  (‹_ ↔⇩r⇧_ _› [70, 70, 70] 70)
  where ‹p ↔⇩r⇧X q ≡ ∃ R. SRB R ∧ R p (Some X) q›

text ‹For the upcoming proofs, it is useful to combine both reactive and $X$-bisimilarity into a single relation.›

definition strongly_reactive_or_X_bisimilar 
  :: ‹'s ⇒ 'a set option ⇒ 's ⇒ bool›
  where ‹strongly_reactive_or_X_bisimilar p XoN q 
    ≡ ∃ R. SRB R ∧ R p XoN q›

text ‹Obviously, then, these relations coincide accordingly.›

corollary ‹p ↔⇩r q ⟺ strongly_reactive_or_X_bisimilar p None q›
  using strongly_reactive_bisimilar_def strongly_reactive_or_X_bisimilar_def by force
corollary ‹p ↔⇩r⇧X q ⟺ strongly_reactive_or_X_bisimilar p (Some X) q›
  using strongly_X_bisimilar_def strongly_reactive_or_X_bisimilar_def by force

                                                                
subsubsection ‹Generalised Strong Reactive Bisimulations›

text ‹Since GSRBs are defined over the same set as SRBs, the same considerations concerning the type and the clauses of the definition as above hold.›

― ‹generalised strong reactive bisimulation @{cite ‹definition 3› rbs}›
definition GSRB :: ‹('s ⇒ 'a set option ⇒ 's ⇒ bool) ⇒ bool›
  where ‹GSRB R ≡
    (∀ p X q. R p (Some X) q  ⟶  X ⊆ visible_actions) ∧
    (∀ p XoN q. R p XoN q  ⟶  R q XoN p) ∧

    (∀ p q. R p None q ⟶
      (∀ p' a. p ⟼a p' ∧ a ∈ visible_actions ∪ {τ}  ⟶
        (∃ q'. q ⟼a q' ∧ R p' None q')) ∧
      (∀ X p'. idle p X ∧ X ⊆ visible_actions ∧ p ⟼t p'  ⟶  
        (∃ q'. q ⟼t q' ∧ R p' (Some X) q'))) ∧
    
    (∀ p Y q. R p (Some Y) q ⟶
      (∀ p' a. a ∈ visible_actions ∧ p ⟼a p' ∧ (a∈Y ∨ idle p Y) ⟶
        (∃ q'. q ⟼a q' ∧ R p' None q')) ∧
      (∀ p'. p ⟼τ p'  ⟶  
        (∃ q'. q ⟼τ q' ∧ R p' (Some Y) q')) ∧
      (∀ p' X. idle p (X∪Y) ∧ X ⊆ visible_actions ∧ p ⟼t p'  ⟶  
        (∃ q'. q ⟼t q' ∧ R p' (Some X) q')))›

(* This lemma is not important for the thesis document. *)
(*<*)
lemma✐‹tag (proof) unimportant› GSRB_ruleformat:
  assumes ‹GSRB R›
  shows
    ‹R p (Some X) q ⟹ X ⊆ visible_actions›
    ‹R p XoN q ⟹ R q XoN p›
    ‹R p None q ⟹ p ⟼a p' ⟹ a ∈ visible_actions ∪ {τ} ⟹ ∃ q'. q ⟼a q' ∧ R p' None q'›
    ‹R p None q ⟹ idle p X ⟹ X ⊆ visible_actions ⟹ p ⟼t p' ⟹ ∃ q'. q ⟼t q' ∧ R p' (Some X) q'›
    ‹R p (Some Y) q ⟹ a ∈ visible_actions ⟹ p ⟼a p' ⟹ a ∈ Y ∨ idle p Y ⟹ ∃ q'. q ⟼a q' ∧ R p' None q'›
    ‹R p (Some Y) q ⟹ p ⟼τ p' ⟹ ∃ q'. q ⟼τ q' ∧ R p' (Some Y) q'›
    ‹R p (Some Y) q ⟹ idle p (X∪Y) ⟹ X ⊆ visible_actions ⟹ p ⟼t p' ⟹ ∃ q'. q ⟼t q' ∧ R p' (Some X) q'›
  using assms unfolding GSRB_def by metis+
(*>*)


subsubsection ‹GSRBs characterise strong reactive/$X$-bisimilarity›

text ‹@{cite ‹proposition 4› rbs} reads (notation adapted): \enquote{$p \leftrightarrow_r q$ iff there exists a GSRB $\mathcal{R}$ with $(p,q) \in \mathcal{R}$. Likewise, $p \leftrightarrow_r^X q$ iff there exists a GSRB $\mathcal{R}$ with $(p,X,q) \in \mathcal{R}$.} We shall now replicate the proof of this proposition. First, we prove that each SRB is a GSRB (by showing that each SRB satisfies all clauses of the definition of GSRBs).›

lemma SRB_is_GSRB:
  assumes ‹SRB R›
  shows ‹GSRB R›
  unfolding GSRB_def
proof (safe)
  fix p XoN q
  assume ‹R p XoN q›
  thus ‹R q XoN p› 
    using SRB_ruleformat[OF assms] by blast
next
  fix p X q x
  assume ‹R p (Some X) q› and ‹x ∈ X›
  thus ‹x ∈ visible_actions› 
    using SRB_ruleformat[OF assms] by blast
next
  fix p q p' a
  assume ‹R p None q› and ‹p ⟼a p'› and ‹a ∈ visible_actions›
  thus ‹∃q'. q ⟼a q' ∧ R p' None q'›
    using SRB_ruleformat(4, 5)[OF assms, where ?X = ‹{a}›] by blast
next
  fix p q p' a
  assume ‹R p None q› and ‹p ⟼τ  p'›
  thus ‹∃q'. q ⟼τ  q' ∧ R p' None q'›
    using SRB_ruleformat(3)[OF assms] by blast
next
  fix p q X p'
  assume ‹R p None q› and ‹idle p X› and ‹X ⊆ visible_actions› and ‹p ⟼t p'›
  thus ‹∃q'. q ⟼t  q' ∧ R p' (Some X) q'›
    using SRB_ruleformat(4, 8)[OF assms] by blast
next
  fix p Y q p' a
  assume ‹R p (Some Y) q› and ‹p ⟼a p'› and ‹a ∈ Y›
  thus ‹∃q'. q ⟼a q' ∧ R p' None q'›
    using SRB_ruleformat(5)[OF assms] by blast
next
  fix p Y q p' a
  assume ‹R p (Some Y) q› ‹a ∈ visible_actions› ‹p ⟼a p'›  ‹idle p Y›
  hence ‹R p None q› using SRB_ruleformat(7)[OF assms] by simp
  hence ‹R p (Some {a}) q› using SRB_ruleformat(4)[OF assms] ‹a ∈ visible_actions› by simp
  thus ‹∃q'. q ⟼a q' ∧ R p' None q'› using SRB_ruleformat(5)[OF assms] ‹p ⟼a p'› by blast
next
  fix p Y q p'
  assume ‹R p (Some Y) q› and ‹p ⟼τ p'›
  thus ‹∃q'. q ⟼τ  q' ∧ R p' (Some Y) q'›
    using SRB_ruleformat(6)[OF assms] by blast
next
  fix p Y q p' X
  assume ‹R p (Some Y) q› ‹idle p (X ∪ Y)› ‹X ⊆ visible_actions› ‹p ⟼t p'›
  from ‹idle p (X ∪ Y)› have ‹idle p Y› and ‹idle p X›
    by (simp add: Int_Un_distrib)+
  from ‹R p (Some Y) q› ‹idle p Y› have ‹R p None q›
    using SRB_ruleformat(7)[OF assms] by blast
  with ‹X ⊆ visible_actions› have ‹R p (Some X) q› 
    using SRB_ruleformat(4)[OF assms] by blast
  with ‹idle p X› ‹p ⟼t p'› show ‹∃q'. q ⟼t  q' ∧ R p' (Some X) q'›
    using SRB_ruleformat(8)[OF assms] by blast
qed

text ‹Then, we show that each GSRB can be extended to yield an SRB. First, we define this extension. Generally, GSRBs can be smaller than SRBs when proving reactive bisimilarity of processes, because they require triples $(p,X,q)$ only after encountering $t$-transitions, whereas SRBs require these triples for all processes and all environments. Furthermore, some process pairs $(p,q)$ related to environment time-outs are also omitted in GSRBs. These tuples are re-added by this extension.
\pagebreak›

definition GSRB_extension 
  :: ‹('s⇒'a set option⇒'s ⇒ bool)⇒('s⇒'a set option⇒'s ⇒ bool)›
  where ‹(GSRB_extension R) p XoN q ≡
    (R p XoN q)
    ∨ (some_visible_subset XoN ∧ R p None q)
    ∨ ((XoN = None ∨ some_visible_subset XoN) 
      ∧ (∃ Y. R p (Some Y) q ∧ idle p Y))›

text ‹Now we show that this extension does, in fact, yield an SRB (again, by showing that all clauses of the definition of SRBs are satisfied).›

(* This lemma is required for the next proof, but it is not important for the outline document. *)
(*<*)
lemma✐‹tag (proof) unimportant› GSRB_preserves_idleness:
  assumes 
    ‹GSRB R›
    ‹R p (Some X) q›
    ‹idle p X›
  shows 
    ‹idle q X›
proof (rule ccontr)
  assume ‹¬ idle q X›
  hence ‹initial_actions q ∩ (X ∪ {τ}) ≠ ∅› by blast
  hence ‹∃ a. a ∈ initial_actions q ∧ a ∈ X ∪ {τ}› by blast
  then obtain α where ‹α ∈ initial_actions q› ‹α ∈ X ∪ {τ}› by blast
  then obtain q' where ‹q ⟼α q'› using initial_actions_def by blast

  from assms have ‹R q (Some X) p› 
    by (simp add: GSRB_def)

  from ‹q ⟼α q'› ‹α ∈ X ∪ {τ}› have ‹∃p'. p ⟼α p'›
  proof (safe)
    assume ‹α ∈ X› ‹q ⟼α q'›
    from GSRB_ruleformat(1) assms(1,2) have ‹X ⊆ visible_actions› .
    with ‹R q (Some X) p› ‹α ∈ X› ‹q ⟼α q'› show ‹∃p'. p ⟼α p'› 
      using GSRB_ruleformat(5)[OF assms(1)] by blast
  next
    assume ‹q ⟼τ  q'›
    with ‹R q (Some X) p› show ‹∃p'. p ⟼τ  p'›
      using GSRB_ruleformat(6)[OF assms(1)] by blast
  qed

  with ‹α ∈ initial_actions q› have ‹α ∈ initial_actions p› using initial_actions_def by auto
  with ‹α ∈ X ∪ {τ}› have ‹¬ idle p X› by auto
  with assms show False by simp
qed
(*>*)

lemma GSRB_extension_is_SRB:
  assumes
    ‹GSRB R›
  shows
    ‹SRB (GSRB_extension R)› (is ‹SRB ?R_ext›)
  unfolding SRB_def
proof (safe)
  fix p XoN q
  assume ‹?R_ext p XoN q›
  thus ‹?R_ext q XoN p› 
    unfolding GSRB_extension_def
  proof (elim disjE, goal_cases)
    case 1
    hence ‹R q XoN p›
      using assms GSRB_def by auto
    thus ?case by simp
  next
    case 2
    hence ‹some_visible_subset XoN ∧ R q None p›
      using assms GSRB_def by auto
    thus ?case by simp
  next
    case 3
    then obtain Y where ‹R p (Some Y) q› ‹idle p Y› by auto
    hence ‹R q (Some Y) p›
      using assms GSRB_def by auto
    have ‹idle q Y›
      using GSRB_preserves_idleness[OF assms] ‹R p (Some Y) q› ‹idle p Y› .
    from 3 ‹R q (Some Y) p› ‹idle q Y› show ?case by blast
  qed
next
  fix p X q x
  assume ‹?R_ext p (Some X) q› ‹x ∈ X›
  thus ‹x ∈ visible_actions› 
    unfolding GSRB_extension_def
  proof (elim disjE, goal_cases)
    case 1
    thus ?case using GSRB_ruleformat(1)[OF assms] by blast
  next
    case 2
    thus ?case by auto
  next
    case 3
    thus ?case by auto
  qed
next
  fix p q p'
  assume ‹?R_ext p None q› ‹p ⟼τ p'›
  thus ‹∃q'. q ⟼τ  q' ∧ ?R_ext p' None q'› 
    unfolding GSRB_extension_def
  proof (elim disjE, goal_cases)
    case 1
    then obtain q' where ‹q ⟼τ q'› ‹R p' None q'›
      using GSRB_ruleformat(3)[OF assms] lts_timeout_axioms by fastforce
    thus ?case by auto
  next
    case 2
    hence False by auto
    thus ?case by simp
  next
    thm GSRB_ruleformat(5)[OF assms, where ?a=τ]
    case 3
    hence ‹∃q'. q ⟼τ  q' ∧ R p' None q'›
      using initial_actions_def by fastforce
    thus ?case by auto
  qed
next
  fix p q X
  assume ‹?R_ext p None q› ‹X ⊆ visible_actions›
  thus ‹?R_ext p (Some X) q› 
    unfolding GSRB_extension_def
  proof (elim disjE, goal_cases)
    case 1
    thus ?case by auto
  next
    case 2
    hence False by auto
    thus ?case by simp
  next
    case 3
    hence ‹some_visible_subset (Some X)› by simp
    with 3 show ?case by simp
  qed
next
  fix p X q p' a
  assume ‹?R_ext p (Some X) q› ‹p ⟼a p'› ‹a ∈ X›
  thus ‹∃q'. q ⟼a q' ∧ ?R_ext p' None q'› 
    unfolding GSRB_extension_def
  proof (elim disjE, goal_cases)
    case 1
    thus ?case 
      using GSRB_ruleformat(1,5)[OF assms] by blast
  next
    case 2
    thus ?case 
      using GSRB_ruleformat(3)[OF assms] by blast
  next
    case 3
    then obtain Y where ‹R p (Some Y) q› ‹idle p Y› by blast
    with 3 have ‹a ∈ visible_actions›
      using GSRB_ruleformat(2)[OF assms] by blast
    from 3 ‹idle p Y› show ?case 
      using GSRB_ruleformat(5)[OF assms ‹R p (Some Y) q› ‹a ∈ visible_actions›] by metis
  qed
next
  fix p X q p'
  assume ‹?R_ext p (Some X) q› ‹p ⟼τ p'›
  thus ‹∃q'. q ⟼τ  q' ∧ ?R_ext p' (Some X) q'› 
    unfolding GSRB_extension_def
  proof (elim disjE, goal_cases)
    case 1
    thus ?case 
      using GSRB_ruleformat(6)[OF assms] by meson
  next
    case 2
    thus ?case 
      using GSRB_ruleformat(3)[OF assms] by blast
  next
    case 3
    then obtain Y where ‹idle p Y› by blast
    with 3(1) have False 
      using initial_actions_def by auto
    thus ?case by simp
  qed
next
  fix p X q
  assume ‹?R_ext p (Some X) q› ‹idle p X›
  thus ‹?R_ext p None q› 
    unfolding GSRB_extension_def by auto
next
  fix p X q p'
  assume ‹?R_ext p (Some X) q› ‹idle p X› ‹p ⟼t p'›
  thus ‹∃q'. q ⟼t  q' ∧ ?R_ext p' (Some X) q'› 
    unfolding GSRB_extension_def
  proof (elim disjE, goal_cases)
    case 1
    from 1(1) have ‹idle p (X ∪ X)› by simp
    from GSRB_ruleformat(1)[OF assms 1(3)] have ‹X ⊆ visible_actions› .
    from GSRB_ruleformat(7)[OF assms 1(3) ‹idle p (X ∪ X)› ‹X ⊆ visible_actions› 1(2)]
    show ?case by auto
  next
    case 2
    thus ?case
      using GSRB_ruleformat(4)[OF assms]
      by (metis option.inject)
  next
    case 3
    then obtain Y where ‹R p (Some Y) q› ‹idle p Y› by blast
    from ‹idle p X› ‹idle p Y› have ‹idle p (X ∪ Y)›
      by (smt bot_eq_sup_iff inf_sup_distrib1)
    from 3(3) have ‹X ⊆ visible_actions› by blast
    from GSRB_ruleformat(7)[OF assms ‹R p (Some Y) q› ‹idle p (X ∪ Y)› ‹X ⊆ visible_actions› 3(2)]
    show ?case by auto
  qed
qed

text ‹Finally, we can conclude the following:›

lemma GSRB_whenever_SRB:
  shows ‹(∃ R. GSRB R ∧ R p XoN q)  ⟺  (∃ R. SRB R ∧ R p XoN q)›
  by (metis GSRB_extension_def GSRB_extension_is_SRB SRB_is_GSRB)

text ‹This, now, directly implies that GSRBs do charactarise strong reactive/$X$-bisimilarity.›

proposition✐‹tag (proof) visible› GSRBs_characterise_strong_reactive_bisimilarity:
  ‹p ↔⇩r q ⟺ (∃ R. GSRB R ∧ R p None q)›
  using GSRB_whenever_SRB strongly_reactive_bisimilar_def by blast

proposition✐‹tag (proof) visible› GSRBs_characterise_strong_X_bisimilarity:
  ‹p ↔⇩r⇧X q ⟺ (∃ R. GSRB R ∧ R p (Some X) q)›
  using GSRB_whenever_SRB strongly_X_bisimilar_def by blast

end ― ‹of ‹context lts_timeout››


text ‹As a little meta-comment, I would like to point out that van~Glabbeek's proof spans a total of five lines (\enquote{Clearly, \textelp{}}, \enquote{It is straightforward to check \textelp{}}), whereas the Isabelle proof takes up around 250 lines of code. This just goes to show that for things which are clear and straightforward for humans, it might require quite some effort to \enquote{explain} them to a computer.
\pagebreak›

(*<*)
end ― ‹of ‹theory››
(*>*)