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" ("_ ⟹_ ≺ _" [80, 80, 80] 80)
  where "P ⟹α ≺ P' ≡ ∃P'' P'''. P ⟹⇩τ P'' ∧ P'' ⟼α ≺ P''' ∧ P''' ⟹⇩τ P'"

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

  assumes "P ⟹α ≺ P'"

  obtains P'' P''' where "P ⟹⇩τ P''" and "P'' ⟼α ≺ 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'' ⟼α ≺ P'''"
  and     "P''' ⟹⇩τ P'"

  shows "P ⟹α ≺ P'"
using assms
by(auto simp add: weakCongTrans_def)

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

  assumes "P ⟼α ≺ P'"

  shows "P ⟹α ≺ P'"
using assms
by(force simp add: weakCongTrans_def)

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

  shows "α.(P) ⟹α ≺ 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 ⟹α ≺ P'"

  shows "P ⊕ Q ⟹α ≺ 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 ⟹α ≺ Q'"

  shows "P ⊕ Q ⟹α ≺ 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 ⟹α ≺ P'"

  shows "P ∥ Q ⟹α ≺ P' ∥ 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 ⟹α ≺ Q'"

  shows "P ∥ Q ⟹α ≺ P ∥ 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 ⟹α ≺ P'"
  and     "Q ⟹(coAction α) ≺ Q'"
  and     "α ≠ τ"

  shows "P ∥ Q ⟹τ ≺ P' ∥ Q'"
using assms
apply(auto simp add: weakCongTrans_def)
apply(rule_tac x= "P'' ∥ P''a" in exI)
apply auto
apply(blast dest: tauChainPar1 tauChainPar2)
apply(rule_tac x="P''' ∥ P'''a" in exI)
apply auto
apply(rule Comm)
apply auto
apply(rule_tac P'="P' ∥ P'''a" in tauChainAppend)
by(blast dest: tauChainPar1 tauChainPar2)+

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

  assumes "P ⟹α ≺ P'"
  and     "x ♯ α"

  shows "⦇νx⦈P ⟹α ≺ ⦇ν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 ∥ !P ⟹α ≺ P'"

  shows "!P ⟹α ≺ P'"
using assms
apply(auto simp add: weakCongTrans_def)
apply(case_tac "P'' = P ∥ !P")
apply auto
apply(force intro: Bang simp add: tauChain_def)
by(force intro: tauChainRepl)

end