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"   ("_ \<leadsto>[_] _" [80, 80, 80] 80)
where
  "P \<leadsto>[Rel] Q ≡ ∀a Q'. Q \<longmapsto>a \<prec> Q' --> (∃P'. P \<longmapsto>a \<prec> P' ∧ (P', Q') ∈ Rel)"

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

  assumes "!!α Q'. Q \<longmapsto>α \<prec> Q' ==> ∃P'. P \<longmapsto>α \<prec> P' ∧ (P', Q') ∈ Rel"

  shows "P \<leadsto>[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 \<leadsto>[Rel] Q"
  and     "Q \<longmapsto>α \<prec> Q'"

  obtains P' where "P \<longmapsto>α \<prec> 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 \<leadsto>[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 \<leadsto>[Rel] Q"
  and     "Q \<leadsto>[Rel'] R"
  and     "Rel O Rel' ⊆ Rel''"
  
  shows "P \<leadsto>[Rel''] R"
using assms
by(force simp add: simulation_def)

end