Theory Reduction_of_Bisimilarity

(*<*)
theory Reduction_of_Bisimilarity
  imports
  Mapping_for_Transition_Systems
  Reactive_Bisimilarity
  Strong_Bisimilarity
begin
(*>*)

section ‹Reduction of Bisimilarity›
text ‹\label{sec:reduction_bisimilarity}›

text ‹The result of this section will be that two processes $p$ and $q$ of an \LTSt{} $\mathbb{T}$ are strongly reactive bisimilar (strongly $X$-bisimilar) iff the corresponding processes $\vartheta(p)$ and $\vartheta(q)$ ($\vartheta_X(p)$ and $\vartheta_X(q)$) of $\mathbb{T}_\vartheta$ are strongly bisimilar. 

We show the $\Longrightarrow$-direction first. For an SRB $\mathcal{R}$, let
$$\mathcal{S} = \{ (\vartheta(p), \vartheta(q)) \mid (p, q) \in \mathcal{R} \} \cup \{ (\vartheta_X(p), \vartheta_X(q)) \mid (p, X, q) \in \mathcal{R} \}.$$
We can prove that $\mathcal{S}$ is an SB, by showing that the mapping satisfies the clauses of the definition of SBs, using the fact that $\mathcal{R}$ is an SRB as well as the rules and generation lemmas for $\rightarrow_\vartheta$. Hence, the existence of an SRB $\mathcal{R}$ with $(p, q) \in \mathcal{R}$ implies the existence of an SB $\mathcal{S}$ with $(\vartheta(p), \vartheta(q)) \in \mathcal{S}$ (and similarly for $\vartheta_X$), so strong reactive/$X$-bisimilarity in $\mathbb{T}$ implies strong bisimilarity in $\mathbb{T}_\vartheta$.

Next, we show the $\Longleftarrow$-direction. Let
$$\mathcal{R} = \{ (p, q) \mid \vartheta(p) \leftrightarrow \vartheta(q) \} \cup \{ (p, X, q) \mid \vartheta_X(p) \leftrightarrow \vartheta_X(q) \}.$$
We can prove that $\mathcal{R}$ is an SRB, again, by showing that all clauses of the definition are satisfied. Hence, strong bisimilarity of $\vartheta(p)$ and $\vartheta(q)$ implies the existence of an SRB $\mathcal{R}$ with $(p, q) \in \mathcal{R}$ (and similarly for $\vartheta_X$), so strong bisimilarity in $\mathbb{T}_\vartheta$ implies strong reactive/$X$-bisimilarity in $\mathbb{T}$.

Thus, we have that strong reactive/$X$-bisimilarity in $\mathbb{T}$ corresponds to strong bisimilarity in $\mathbb{T}_\vartheta$.›


subsection ‹Isabelle›

text ‹We begin by \emph{interpreting} our transition mapping ‹tran_theta› as an ‹lts› and call it ‹lts_theta›. Therefore, we are handling two separate LTSs: the \LTSt{} $\mathbb{T}$ given by the local ‹context lts_timeout_mappable›, and the LTS $\mathbb{T}_\vartheta$ given by the ‹interpretation lts_theta›.
When referring to definitions involving the transition relation of ‹lts_theta›, we have to prefix them, e.g.\@ ‹lts_theta.SB› for the definition of strong bisimulations using ‹⟼⇧^θ› instead of ‹⟼›.

By default, ‹interpretation›s do not import special notation, so we reassign strong bisimilarity notation ‹↔› to ‹lts_theta›, since we do not care about strong bisimilarity in $\mathbb{T}$.›

context lts_timeout_mappable begin

interpretation lts_theta: lts tran_theta .
no_notation local.strongly_bisimilar (‹_ ↔ _› [70, 70] 70)
notation lts_theta.strongly_bisimilar (‹_ ↔ _› [70, 70] 70)


text ‹We can now formalise the proof as described above.›

subsubsection ‹If \dots{} (\boldmath{$\Longrightarrow$})›

definition SRB_mapping ― ‹$\mathcal{S}$› 
  :: ‹('s⇒'a set option⇒'s ⇒ bool) ⇒ ('ss⇒'ss ⇒ bool)›
  where ‹SRB_mapping R P Q ≡ 
    (∃ p q. P = θ(p) ∧ Q = θ(q) ∧ R p None q) ∨
    (∃ p q X. P = θ[X](p) ∧ Q = θ[X](q) ∧ R p (Some X) q)›

lemma SRB_mapping_is_SB:
  assumes ‹SRB R›
  shows ‹lts_theta.SB (SRB_mapping R)› (is ‹lts_theta.SB ?S›)
proof -
  {
    fix P Q P' a
    assume
      ‹?S P Q›
      ‹P ⟼⇧^θa P'›
    have ‹∃Q'. ?S P' Q' ∧ Q ⟼⇧^θa Q'›
      using ‹?S P Q› unfolding SRB_mapping_def
    proof (elim disjE)
      assume ‹∃p q. P = θ(p) ∧ Q = θ(q) ∧ R p None q›
      then obtain p q where ‹P = θ(p)› ‹Q = θ(q)› ‹R p None q› by blast
      from ‹P = θ(p)› ‹P ⟼⇧^θa P'› have
        ‹(∃X. a = ε[X] ∧ P' = θ[X](p) ∧ X ⊆ visible_actions) ∨ a = τ ∧ (∃p'. p ⟼τ  p')›
        using generation_triggered_transitions by blast
      thus ‹∃Q'. ((∃p q. P' = θ(p) ∧ Q' = θ(q) ∧ R p None q) 
        ∨ (∃p q X. P' = θ[X](p) ∧ Q' = θ[X](q) ∧ R p (Some X) q)) ∧ Q ⟼⇧^θa Q'›
      proof (auto, goal_cases)
        case (1 X)
        from ‹X ⊆ visible_actions› ‹Q = θ(q)› have ‹Q ⟼⇧^θε[X] θ[X](q)› 
        using env_stabilise by force
    
        have ‹R p (Some X) q› using SRB_ruleformat(4)[OF assms(1) ‹R p None q› ‹X ⊆ visible_actions›] .
    
        from ‹P' = θ[X](p)› ‹Q ⟼⇧^θε[X] θ[X](q)› ‹R p (Some X) q› ‹a = ε[X]›
        show ?case by blast
      next
        case (2 p')
        have ‹∃q'. q ⟼τ  q' ∧ R p' None q'› using SRB_ruleformat(3)[OF assms(1) ‹R p None q› 2(2)] .
        with ‹P = θ(p)› ‹Q = θ(q)› ‹R p None q› show ?case
          by (metis "2"(1) assms(1) ‹P ⟼⇧^θa P'› generation_triggered_tau SRB_ruleformat(3) triggered_tau)
      qed
    
    next
    
      assume ‹∃p q X. P = θ[X](p) ∧ Q = θ[X](q) ∧ R p (Some X) q›
      then obtain p q X where ‹P = θ[X](p)› ‹Q = θ[X](q)› ‹R p (Some X) q› by fast
      hence ‹X ⊆ visible_actions› using SRB_ruleformat(1)[OF assms(1)] by blast
      
      from ‹P ⟼⇧^θa P'› ‹P = θ[X](p)› have ‹a = t_ε ∨ (∃ p'. p ⟼a p')›
        using generation_stable_transitions by blast
    
      hence ‹a = t_ε ∨ a = τ ∨ a = t ∨ a ∈ visible_actions› using visible_actions_def by fast
      thus ‹∃Q'. ((∃p q. P' = θ(p) ∧ Q' = θ(q) ∧ R p None q) ∨ (∃p q X. P' = θ[X](p) ∧ Q' = θ[X](q) ∧ R p (Some X) q)) ∧ Q ⟼⇧^θa Q'›
      proof (elim disjE)
        assume ‹a = t_ε›
        with ‹P ⟼⇧^θa P'› ‹P = θ[X](p)› have ‹P' = θ(p)› ‹idle p X› using generation_env_timeout by fast+
        with ‹R p (Some X) q› have ‹idle q X›
          using assms GSRB_preserves_idleness SRB_is_GSRB by blast
        with ‹Q = θ[X](q)› ‹X ⊆ visible_actions› have ‹Q ⟼⇧^θt_ε θ(q)› using env_timeout by simp
        from ‹R p (Some X) q› ‹idle p X› have ‹R p None q› using SRB_ruleformat(7)[OF assms(1)] by simp
        with ‹P' = θ(p)› ‹Q ⟼⇧^θt_ε θ(q)› ‹a = t_ε› show ?thesis by blast
      next
        assume ‹a = τ›
        with ‹P ⟼⇧^θa P'› ‹P = θ[X](p)› obtain p' where ‹P' = θ[X](p')› ‹p ⟼τ p'›
          using generation_stable_tau by blast
        with ‹R p (Some X) q› obtain q' where ‹q ⟼τ q'› ‹R p' (Some X) q'›
          using SRB_ruleformat(6)[OF assms(1)] by blast
        with ‹Q = θ[X](q)› ‹X ⊆ visible_actions› have ‹Q ⟼⇧^θτ θ[X](q')› 
          using stable_tau by blast
        with ‹P' = θ[X](p')› ‹R p' (Some X) q'› ‹a = τ› show ?thesis by blast
      next
        assume ‹a = t›
        with ‹P ⟼⇧^θa P'› ‹P = θ[X](p)› obtain p' where ‹P' = θ[X](p')› ‹idle p X› ‹ p ⟼t p'›
          using generation_sys_timeout by blast
        with ‹R p (Some X) q› obtain q' where ‹q ⟼t q'› ‹R p' (Some X) q'›
          using SRB_ruleformat(8)[OF assms(1)] by blast
        from ‹idle p X› ‹R p (Some X) q› have ‹idle q X›
          using assms GSRB_preserves_idleness SRB_is_GSRB by blast
        from ‹q ⟼t q'› ‹Q = θ[X](q)› ‹X ⊆ visible_actions› ‹idle q X› have ‹Q ⟼⇧^θt θ[X](q')› 
          using sys_timeout by blast
        with ‹P' = θ[X](p')› ‹R p' (Some X) q'› ‹a = t› show ?thesis by blast
      next
        thm SRB_ruleformat
        assume ‹a ∈ visible_actions›
        with ‹P ⟼⇧^θa P'› ‹P = θ[X](p)› obtain p' where ‹a ∈ X› ‹P' = θ(p')› ‹p ⟼a p'› 
          using generation_tran_visible by blast
        with ‹R p (Some X) q› obtain q' where ‹q ⟼a q'› ‹R p' None q'›
          using SRB_ruleformat(5)[OF assms(1)] by blast
        with ‹Q = θ[X](q)› ‹X ⊆ visible_actions› ‹a ∈ X› have ‹Q ⟼⇧^θa θ(q')›
          using tran_visible by blast
        with ‹P' = θ(p')› ‹R p' None q'› show ?thesis by blast
      qed
    qed
  }
  note SB_property_half = this

  have SRB_mapping_symmetry: 
    ‹⋀ P Q. SRB R ∧ ?S P Q ⟹ ?S Q P›
    using assms SRB_mapping_def SRB_ruleformat(2) by (smt (verit, best))

  show ‹lts_theta.SB ?S› unfolding lts_theta.SB_def
    using assms SB_property_half SRB_mapping_symmetry by blast
qed

lemma srby_implies_sby:
  assumes ‹p ↔⇩_r q› 
  shows ‹θ(p) ↔ θ(q)›
  using assms SRB_mapping_def SRB_mapping_is_SB lts_theta.strongly_bisimilar_def strongly_reactive_bisimilar_def
  by metis
lemma sxby_implies_sby:
  assumes ‹p ↔⇩_r⇧X q› 
  shows ‹θ[X](p) ↔ θ[X](q)›
  using assms SRB_mapping_def SRB_mapping_is_SB strongly_X_bisimilar_def lts_theta.strongly_bisimilar_def
  by metis


subsubsection ‹\dots{} and only if (\boldmath{$\Longleftarrow$})›

definition strong_bisimilarity_mapping ― ‹$\mathcal{R}$›
  :: ‹'s⇒'a set option⇒'s ⇒ bool›
  where ‹(strong_bisimilarity_mapping) p XoN q 
    ≡ (XoN = None ∧ (θ(p)) ↔ (θ(q))) ∨
    (∃ X. XoN = Some X ∧ X ⊆ visible_actions ∧ 
     θ[X](p) ↔ θ[X](q))›

lemma strong_bisimilarity_mapping_is_SRB:
  shows ‹SRB strong_bisimilarity_mapping› (is ‹SRB ?R›)
  unfolding SRB_def
proof (safe)
  fix p XoN q
  assume ‹?R p XoN q›
  thus ‹?R q XoN p› using lts_theta.strongly_bisimilar_symm unfolding strong_bisimilarity_mapping_def by blast
next
  fix p X q x
  assume ‹?R p (Some X) q› ‹x ∈ X›
  thus ‹x ∈ visible_actions› unfolding strong_bisimilarity_mapping_def by auto
next
  fix p q p'
  assume ‹?R p None q› ‹p ⟼τ p'›

  from ‹?R p None q› have ‹(θ(p)) ↔ (θ(q))› 
    unfolding strong_bisimilarity_mapping_def by auto
  from ‹p ⟼τ p'› have ‹θ(p) ⟼⇧^θτ θ(p')›
    using triggered_tau by blast
  with ‹θ(p) ↔ θ(q)› obtain Q' where ‹θ(q) ⟼⇧^θτ Q'› ‹θ(p') ↔ Q'›
    using lts_theta.strongly_bisimilar_step by blast
  then obtain q' where ‹Q' = θ(q') ∧ q ⟼τ q'›
    using generation_triggered_tau by blast
  with ‹θ(p') ↔ Q'› have ‹∃ q'. q ⟼τ q' ∧ θ(p') ↔ θ(q')› by fast
  with ‹p ⟼τ p'› show ‹∃q'. q ⟼τ  q' ∧ ?R p' None q'› 
    using strong_bisimilarity_mapping_def by auto
next
  fix p q X
  assume ‹?R p None q› ‹X ⊆ visible_actions›
  from ‹?R p None q› have ‹θ(p) ↔ θ(q)› using strong_bisimilarity_mapping_def by simp
  have ‹θ(p) ⟼⇧^θε[X] θ[X](p)› using env_stabilise[OF ‹X ⊆ visible_actions›] .
  with ‹θ(p) ↔ θ(q)› obtain Q' where ‹θ(q) ⟼⇧^θε[X] Q'› ‹θ[X](p) ↔ Q'› 
    using lts_theta.strongly_bisimilar_step(1) by blast
  from ‹θ(q) ⟼⇧^θε[X] Q'› have ‹Q' = θ[X](q)›
    using generation_env_stabilise injectivity_theta(2) by blast
  with ‹θ[X](p) ↔ Q'› have ‹θ[X](p) ↔ θ[X](q)› by simp
  thus ‹?R p (Some X) q› using strong_bisimilarity_mapping_def ‹X ⊆ visible_actions› by simp
next
  fix p X q p' a
  assume ‹?R p (Some X) q› ‹p ⟼a p'› ‹a ∈ X›
  hence ‹θ[X](p) ↔ θ[X](q)› ‹X ⊆ visible_actions› using strong_bisimilarity_mapping_def by blast+
  from ‹p ⟼a p'› ‹X ⊆ visible_actions› ‹a ∈ X› have ‹θ[X](p) ⟼⇧^θa θ(p')› 
    using tran_visible by blast
  with ‹θ[X](p) ↔ θ[X](q)› have ‹∃ Q'. θ[X](q) ⟼⇧^θa Q' ∧ θ(p') ↔ Q'›
    using lts_theta.strongly_bisimilar_step(1) by blast
  then obtain Q' where ‹θ[X](q) ⟼⇧^θa Q'› ‹θ(p') ↔ Q'› by blast
  hence ‹∃ q'. Q' = θ(q') ∧ q ⟼a q'› using generation_tran_visible ‹a ∈ X› ‹X ⊆ visible_actions› by blast
  with ‹θ(p') ↔ Q'› show ‹∃q'. q ⟼a q' ∧ ?R p' None q'› using strong_bisimilarity_mapping_def by blast
next
  fix p X q p'
  assume ‹?R p (Some X) q› ‹p ⟼τ  p'›
  hence ‹θ[X](p) ↔ θ[X](q)› ‹X ⊆ visible_actions› using strong_bisimilarity_mapping_def by blast+
  from ‹p ⟼τ  p'› ‹X ⊆ visible_actions› have ‹θ[X](p) ⟼⇧^θτ θ[X](p')› 
    using stable_tau by blast
  with ‹θ[X](p) ↔ θ[X](q)› have ‹∃ Q'. θ[X](q) ⟼⇧^θτ Q' ∧ θ[X](p') ↔ Q'›
    using lts_theta.strongly_bisimilar_step(1) by blast
  then obtain Q' where ‹θ[X](q) ⟼⇧^θτ Q'› ‹θ[X](p') ↔ Q'› by blast
  hence ‹∃ q'. Q' = θ[X](q') ∧ q ⟼τ  q'› using generation_stable_tau ‹X ⊆ visible_actions› by blast
  with ‹θ[X](p') ↔ Q'› show ‹∃q'. q ⟼τ  q' ∧ ?R p' (Some X) q'› 
    using strong_bisimilarity_mapping_def ‹X ⊆ visible_actions› by blast
next
  fix p X q
  assume ‹?R p (Some X) q› ‹idle p X›
  hence ‹θ[X](p) ↔ θ[X](q)› ‹X ⊆ visible_actions› using strong_bisimilarity_mapping_def by blast+
  from ‹X ⊆ visible_actions› ‹idle p X› have ‹θ[X](p) ⟼⇧^θt_ε θ(p)› 
    using env_timeout by blast
  with ‹θ[X](p) ↔ θ[X](q)› have ‹∃ Q'. θ[X](q) ⟼⇧^θt_ε Q' ∧ θ(p) ↔ Q'›
    using lts_theta.strongly_bisimilar_step(1) by blast
  then obtain Q' where ‹θ[X](q) ⟼⇧^θt_ε Q'› ‹θ(p) ↔ Q'› by blast
  have ‹Q' = θ(q)› using generation_env_timeout[OF ‹θ[X](q) ⟼⇧^θt_ε Q'›] ..
  with ‹θ(p) ↔ Q'› show ‹?R p None q› using strong_bisimilarity_mapping_def by auto
next
  fix p X q p'
  assume ‹?R p (Some X) q› ‹idle p X› ‹p ⟼t  p'›
  hence ‹θ[X](p) ↔ θ[X](q)› ‹X ⊆ visible_actions› using strong_bisimilarity_mapping_def by blast+
  from ‹p ⟼t  p'› ‹X ⊆ visible_actions› ‹idle p X› have ‹θ[X](p) ⟼⇧^θt θ[X](p')› 
    using sys_timeout by blast
  with ‹θ[X](p) ↔ θ[X](q)› have ‹∃ Q'. θ[X](q) ⟼⇧^θt Q' ∧ θ[X](p') ↔ Q'›
    using lts_theta.strongly_bisimilar_step(1) by blast
  then obtain Q' where ‹θ[X](q) ⟼⇧^θt Q'› ‹θ[X](p') ↔ Q'› by blast
  hence ‹∃ q'. Q' = θ[X](q') ∧ q ⟼t  q' ∧ idle q X› using generation_sys_timeout ‹X ⊆ visible_actions› by blast
  with ‹θ[X](p') ↔ Q'› show ‹∃q'. q ⟼t  q' ∧ ?R p' (Some X) q'› 
    using strong_bisimilarity_mapping_def ‹X ⊆ visible_actions› by blast
qed

lemma sby_implies_srby:
  assumes ‹θ(p) ↔ θ(q)› 
  shows ‹p ↔⇩_r q›
  using assms strong_bisimilarity_mapping_is_SRB
    strong_bisimilarity_mapping_def strongly_reactive_bisimilar_def by auto
lemma sby_implies_sxby:
  assumes ‹θ[X](p) ↔ θ[X](q)› ‹X ⊆ visible_actions›
  shows ‹p ↔⇩_r⇧X q› 
  using assms strong_bisimilarity_mapping_is_SRB
    strong_bisimilarity_mapping_def strongly_X_bisimilar_def by auto

text ‹We need to include the assumption ‹X ⊆ visible_actions›, since for \linebreak ‹¬ X ⊆ visible_actions›, ‹θ[X](p)› and ‹θ[X](q)› might be identical (since we do not require injectivity for that subset of the domain), so ‹θ[X](p) ↔ θ[X](q)› would be true, whereas ‹p ↔⇩_r⇧^X q› would be false (since \linebreak ‹X ⊆ visible_actions› is part of the definition of SRBs).›


subsubsection ‹Iff (\boldmath{$\Longleftrightarrow$})›

theorem✐‹tag (proof) visible› strongly_reactive_bisim_iff_triggered_strongly_bisim:
  shows ‹p ↔⇩_r q  ⟺  θ(p) ↔ θ(q)›
  using sby_implies_srby srby_implies_sby by fast

theorem✐‹tag (proof) visible› strongly_X_bisim_iff_stable_strongly_bisim:
  assumes ‹X ⊆ visible_actions›
  shows ‹p ↔⇩_r⇧X q  ⟺  θ[X](p) ↔ θ[X](q)›
  using sxby_implies_sby sby_implies_sxby assms by fast


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