Theory Strong_Sim

(* 
   Title: The Calculus of Communicating Systems   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Strong_Sim
  imports Agent
begin

definition simulation :: "ccs ⇒ (ccs × ccs) set ⇒ ccs ⇒ bool"   ("_ ↝[_] _" [80, 80, 80] 80)
where
  "P ↝[Rel] Q ≡ ∀a Q'. Q ⟼a ≺ Q' ⟶ (∃P'. P ⟼a ≺ P' ∧ (P', Q') ∈ Rel)"

lemma simI[case_names Sim]:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs

  assumes "⋀α Q'. Q ⟼α ≺ Q' ⟹ ∃P'. P ⟼α ≺ P' ∧ (P', Q') ∈ Rel"

  shows "P ↝[Rel] Q"
using assms
by(auto simp add: simulation_def)

lemma simE:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  and   Q   :: ccs
  and   α   :: act
  and   Q'  :: ccs

  assumes "P ↝[Rel] Q"
  and     "Q ⟼α ≺ Q'"

  obtains P' where "P ⟼α ≺ P'" and "(P', Q') ∈ Rel"
using assms
by(auto simp add: simulation_def)

lemma reflexive:
  fixes P   :: ccs
  and   Rel :: "(ccs × ccs) set"
  
  assumes "Id ⊆ Rel"

  shows "P ↝[Rel] P"
using assms
by(auto simp add: simulation_def)
  
lemma transitive:
  fixes P     :: ccs
  and   Rel   :: "(ccs × ccs) set"
  and   Q     :: ccs
  and   Rel'  :: "(ccs × ccs) set"
  and   R     :: ccs
  and   Rel'' :: "(ccs × ccs) set"
  
  assumes "P ↝[Rel] Q"
  and     "Q ↝[Rel'] R"
  and     "Rel O Rel' ⊆ Rel''"
  
  shows "P ↝[Rel''] R"
using assms
by(force simp add: simulation_def)

end