Theory Weak_Cong_Semantics

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

definition weakCongTrans :: "ccs => act => ccs => bool" ("_ ==>_ \<prec> _" [80, 80, 80] 80)
  where "P ==>α \<prec> P' ≡ ∃P'' P'''. P ==>⇩τ P'' ∧ P'' \<longmapsto>α \<prec> P''' ∧ P''' ==>⇩τ P'"

lemma weakCongTransE:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs

  assumes "P ==>α \<prec> P'"

  obtains P'' P''' where "P ==>⇩τ P''" and "P'' \<longmapsto>α \<prec> P'''" and "P''' ==>⇩τ P'"
using assms
by(auto simp add: weakCongTrans_def)

lemma weakCongTransI:
  fixes P    :: ccs
  and   P''  :: ccs
  and   α    :: act
  and   P''' :: ccs
  and   P'   :: ccs

  assumes "P ==>⇩τ P''"
  and     "P'' \<longmapsto>α \<prec> P'''"
  and     "P''' ==>⇩τ P'"

  shows "P ==>α \<prec> P'"
using assms
by(auto simp add: weakCongTrans_def)

lemma transitionWeakCongTransition:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs

  assumes "P \<longmapsto>α \<prec> P'"

  shows "P ==>α \<prec> P'"
using assms
by(force simp add: weakCongTrans_def)

lemma weakCongAction:
  fixes a :: name
  and   P :: ccs

  shows "α.(P) ==>α \<prec> P"
by(auto simp add: weakCongTrans_def)
  (blast intro: Action tauChainRefl)

lemma weakCongSum1:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs
  and   Q  :: ccs

  assumes "P ==>α \<prec> P'"

  shows "P ⊕ Q ==>α \<prec> P'"
using assms
apply(auto simp add: weakCongTrans_def)
apply(case_tac "P=P''")
apply(force simp add: tauChain_def dest: Sum1)
by(force intro: tauChainSum1)

lemma weakCongSum2:
  fixes Q  :: ccs
  and   α  :: act
  and   Q' :: ccs
  and   P  :: ccs

  assumes "Q ==>α \<prec> Q'"

  shows "P ⊕ Q ==>α \<prec> Q'"
using assms
apply(auto simp add: weakCongTrans_def)
apply(case_tac "Q=P''")
apply(force simp add: tauChain_def dest: Sum2)
by(force intro: tauChainSum2)

lemma weakCongPar1:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs
  and   Q  :: ccs

  assumes "P ==>α \<prec> P'"

  shows "P \<parallel> Q ==>α \<prec> P' \<parallel> Q"
using assms
by(auto simp add: weakCongTrans_def)
  (blast dest: tauChainPar1 Par1)

lemma weakCongPar2:
  fixes Q  :: ccs
  and   α  :: act
  and   Q' :: ccs
  and   P  :: ccs

  assumes "Q ==>α \<prec> Q'"

  shows "P \<parallel> Q ==>α \<prec> P \<parallel> Q'"
using assms
by(auto simp add: weakCongTrans_def)
  (blast dest: tauChainPar2 Par2)

lemma weakCongSync:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs
  and   Q  :: ccs

  assumes "P ==>α \<prec> P'"
  and     "Q ==>(coAction α) \<prec> Q'"
  and     "α ≠ τ"

  shows "P \<parallel> Q ==>τ \<prec> P' \<parallel> Q'"
using assms
apply(auto simp add: weakCongTrans_def)
apply(rule_tac x= "P'' \<parallel> P''a" in exI)
apply auto
apply(blast dest: tauChainPar1 tauChainPar2)
apply(rule_tac x="P''' \<parallel> P'''a" in exI)
apply auto
apply(rule Comm)
apply auto
apply(rule_tac P'="P' \<parallel> P'''a" in tauChainAppend)
by(blast dest: tauChainPar1 tauChainPar2)+

lemma weakCongRes:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs
  and   x  :: name

  assumes "P ==>α \<prec> P'"
  and     "x \<sharp> α"

  shows "(|νx|)),P ==>α \<prec> (|νx|)),P'"
using assms
by(auto simp add: weakCongTrans_def)
  (blast dest: tauChainRes Res)

lemma weakCongRepl:
  fixes P  :: ccs
  and   α  :: act
  and   P' :: ccs

  assumes "P \<parallel> !P ==>α \<prec> P'"

  shows "!P ==>α \<prec> P'"
using assms
apply(auto simp add: weakCongTrans_def)
apply(case_tac "P'' = P \<parallel> !P")
apply auto
apply(force intro: Bang simp add: tauChain_def)
by(force intro: tauChainRepl)

end