Theory Strong_Bisim_SC

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

lemma resNil:
  fixes x :: name

  shows "⦇νx⦈𝟬 ∼ 𝟬"
proof -
  have "(⦇νx⦈𝟬, 𝟬) ∈ {(⦇νx⦈𝟬, 𝟬), (𝟬, ⦇νx⦈𝟬)}" by simp
  thus ?thesis
    by(coinduct rule: bisimCoinduct)
      (auto intro: resNilLeft resNilRight)
qed

lemma scopeExt:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x ♯ P"

  shows "⦇νx⦈(P ∥ Q) ∼ P ∥ ⦇νx⦈Q"
proof -
  let ?X = "{(⦇νx⦈(P ∥ Q), P ∥ ⦇νx⦈Q) | x P Q. x ♯ P} ∪ {(P ∥ ⦇νx⦈Q, ⦇νx⦈(P ∥ Q)) | x P Q. x ♯ P}"
  from assms have "(⦇νx⦈(P ∥ Q), P ∥ ⦇νx⦈Q) ∈ ?X" by auto
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (force intro: scopeExtLeft scopeExtRight)+
qed

lemma sumComm:
  fixes P :: ccs
  and   Q :: ccs

  shows "P ⊕ Q ∼ Q ⊕ P"
proof -
  have "(P ⊕ Q, Q ⊕ P) ∈ {(P ⊕ Q, Q ⊕ P), (Q ⊕ P, P ⊕ Q)}" by simp
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: sumComm reflexive)
qed

lemma sumAssoc:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  shows "(P ⊕ Q) ⊕ R ∼ P ⊕ (Q ⊕ R)"
proof -
  have "((P ⊕ Q) ⊕ R, P ⊕ (Q ⊕ R)) ∈ {((P ⊕ Q) ⊕ R, P ⊕ (Q ⊕ R)), (P ⊕ (Q ⊕ R), (P ⊕ Q) ⊕ R)}" by simp
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: sumAssocLeft sumAssocRight reflexive)
qed

lemma sumId:
  fixes P :: ccs

  shows "P ⊕ 𝟬 ∼ P"
proof -
  have "(P ⊕ 𝟬, P) ∈ {(P ⊕ 𝟬, P), (P, P ⊕ 𝟬)}" by simp
  thus ?thesis by(coinduct rule: bisimCoinduct) (auto intro: sumIdLeft sumIdRight reflexive) 
qed

lemma parComm:
  fixes P :: ccs
  and   Q :: ccs

  shows "P ∥ Q ∼ Q ∥ P"
proof -
  have "(P ∥ Q, Q ∥ P) ∈ {(P ∥ Q, Q ∥ P) | P Q. True} ∪ {(Q ∥ P, P ∥ Q) | P Q. True}" by auto
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: parComm)
qed

lemma parAssoc:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  shows "(P ∥ Q) ∥ R ∼ P ∥ (Q ∥ R)"
proof -
  have "((P ∥ Q) ∥ R, P ∥ (Q ∥ R)) ∈ {((P ∥ Q) ∥ R, P ∥ (Q ∥ R)) | P Q R. True} ∪  
                                     {(P ∥ (Q ∥ R), (P ∥ Q) ∥ R) | P Q R. True}" by auto
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (force intro: parAssocLeft parAssocRight)+
qed

lemma parId:
  fixes P :: ccs

  shows "P ∥ 𝟬 ∼ P"
proof -
  have "(P ∥ 𝟬, P) ∈ {(P ∥ 𝟬, P) | P. True} ∪ {(P, P ∥ 𝟬) | P. True}" by simp
  thus ?thesis by(coinduct rule: bisimCoinduct) (auto intro: parIdLeft parIdRight)
qed

lemma scopeFresh:
  fixes x :: name
  and   P :: ccs

  assumes "x ♯ P"

  shows "⦇νx⦈P ∼ P"
proof -
  have "⦇νx⦈P ∼ ⦇νx⦈P ∥ 𝟬" by(rule parId[THEN symmetric])
  moreover have "⦇νx⦈P ∥ 𝟬 ∼ 𝟬 ∥ ⦇νx⦈P" by(rule parComm)
  moreover have "𝟬 ∥ ⦇νx⦈P ∼ ⦇νx⦈(𝟬 ∥ P)" by(rule scopeExt[THEN symmetric]) auto
  moreover have "⦇νx⦈(𝟬 ∥ P) ∼ ⦇νx⦈(P ∥ 𝟬)" by(rule resPres[OF parComm])
  moreover from ‹x ♯ P› have "⦇νx⦈(P ∥ 𝟬) ∼ P ∥ ⦇νx⦈𝟬" by(rule scopeExt)
  moreover have  "P ∥ ⦇νx⦈𝟬 ∼ ⦇νx⦈𝟬 ∥ P" by(rule parComm)
  moreover have "⦇νx⦈𝟬 ∥ P ∼ 𝟬 ∥ P" by(rule parPres[OF resNil])
  moreover have "𝟬 ∥ P ∼ P ∥ 𝟬" by(rule parComm)
  moreover have "P ∥ 𝟬 ∼ P" by(rule parId)
  ultimately show ?thesis by(metis transitive)
qed

lemma scopeExtSum:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x ♯ P"

  shows "⦇νx⦈(P ⊕ Q) ∼ P ⊕ ⦇νx⦈Q"
proof -
  have "(⦇νx⦈(P ⊕ Q), P ⊕ ⦇νx⦈Q) ∈ {(⦇νx⦈(P ⊕ Q), P ⊕ ⦇νx⦈Q), (P ⊕ ⦇νx⦈Q, ⦇νx⦈(P ⊕ Q))}"
    by simp
  thus ?thesis using ‹x ♯ P›
    by(coinduct rule: bisimCoinduct) 
      (auto intro: scopeExtSumLeft scopeExtSumRight reflexive scopeFresh scopeFresh[THEN symmetric])
qed

lemma resAct:
  fixes x :: name
  and   α :: act
  and   P :: ccs

  assumes "x ♯ α"

  shows "⦇νx⦈(α.(P)) ∼ α.(⦇νx⦈P)"
proof -
  have "(⦇νx⦈(α.(P)), α.(⦇νx⦈P)) ∈ {(⦇νx⦈(α.(P)), α.(⦇νx⦈P)), (α.(⦇νx⦈P), ⦇νx⦈(α.(P)))}"
    by simp
  thus ?thesis using ‹x ♯ α›
    by(coinduct rule: bisimCoinduct) (auto intro: resActLeft resActRight reflexive)
qed

lemma resComm:
  fixes x :: name
  and   y :: name
  and   P :: ccs

  shows "⦇νx⦈(⦇νy⦈P) ∼ ⦇νy⦈(⦇νx⦈P)"
proof -
  have "(⦇νx⦈(⦇νy⦈P), ⦇νy⦈(⦇νx⦈P)) ∈ {(⦇νx⦈(⦇νy⦈P), ⦇νy⦈(⦇νx⦈P)) | x y P. True}" by auto
  thus ?thesis
  by(coinduct rule: bisimCoinduct) (auto intro: resComm)
qed

lemma bangUnfold:
  fixes P

  shows "!P ∼ P ∥ !P"
proof -
  have "(!P, P ∥ !P) ∈ {(!P, P ∥ !P), (P ∥ !P, !P)}" by auto
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: bangUnfoldLeft bangUnfoldRight reflexive)
qed

lemma bisimStructCong:
  fixes P :: ccs
  and   Q :: ccs

  assumes "P ≡⇩s Q"

  shows "P ∼ Q"
using assms
apply(nominal_induct rule: Struct_Cong.strong_induct)
by(auto intro: reflexive symmetric transitive parComm parAssoc parId sumComm
   sumAssoc sumId resNil scopeExt scopeExtSum resAct resComm bangUnfold)   

end