Theory Strong_Relations

section ‹Notions of Equivalence›

subsection ‹Strong Simulation and Bisimulation›

theory Strong_Relations
  imports Transition_Systems
begin

context lts
begin
  
definition simulation :: 
  ‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
  ‹simulation R ≡ ∀ p q. R p q ⟶ 
    (∀ p' a. p ⟼a p' ⟶ 
      (∃ q'. R p' q' ∧ (q ⟼a q')))›
  
definition bisimulation :: 
  ‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
  ‹bisimulation R ≡ ∀ p q. R p q ⟶ 
    (∀ p' a. p ⟼a p' ⟶ 
      (∃ q'. R p' q' ∧ (q ⟼a q'))) ∧
    (∀ q' a. q ⟼a q' ⟶ 
      (∃ p'. R p' q' ∧ (p ⟼a p')))›

lemma bisim_ruleformat:
  assumes ‹bisimulation R›
    and ‹R p q›
  shows
    ‹p ⟼a p' ⟹ (∃ q'. R p' q' ∧ (q ⟼a q'))›
    ‹q ⟼a q' ⟹ (∃ p'. R p' q' ∧ (p ⟼a p'))›
  using assms unfolding bisimulation_def by auto

end ―‹context lts›

end