Theory Weak_Early_Bisim_SC

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Weak_Early_Bisim_SC
  imports Weak_Early_Bisim Strong_Early_Bisim_SC
begin

(******** Structural Congruence **********)

lemma weakBisimStructCong:
  fixes P :: pi
  and   Q :: pi

  assumes "P ≡⇩s Q"

  shows "P ≈ Q"
using assms
by(metis earlyBisimStructCong strongBisimWeakBisim)

lemma matchId:
  fixes a :: name
  and   P :: pi

  shows "[a⌢a]P ≈ P"
proof -
  have "[a⌢a]P ∼⇩e P" by(rule Strong_Early_Bisim_SC.matchId)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma mismatchId:
  fixes a :: name
  and   b :: name
  and   P :: pi

  assumes "a ≠ b"

  shows "[a≠b]P ≈ P"
proof -
  from ‹a ≠ b› have "[a≠b]P ∼⇩e P" by(rule Strong_Early_Bisim_SC.mismatchId)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma mismatchNil:
  fixes a :: name
  and   P :: pi

  shows "[a≠a]P ≈ 𝟬"
proof -
  have "[a≠a]P ∼⇩e 𝟬" by(rule Strong_Early_Bisim_SC.mismatchNil)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

(******** The ν-operator *****************)

lemma resComm:
  fixes P :: pi
  
  shows "<νa><νb>P ≈ <νb><νa>P"
proof -
  have "<νa><νb>P ∼⇩e <νb><νa>P" by(rule Strong_Early_Bisim_SC.resComm)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

(******** The +-operator *********)

lemma sumSym:
  fixes P :: pi
  and   Q :: pi
  
  shows "P ⊕ Q ≈ Q ⊕ P"
proof -
  have "P ⊕ Q ∼⇩e Q ⊕ P" by(rule Strong_Early_Bisim_SC.sumSym)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma sumAssoc:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi
  
  shows "(P ⊕ Q) ⊕ R ≈ P ⊕ (Q ⊕ R)"
proof -
  have "(P ⊕ Q) ⊕ R ∼⇩e P ⊕ (Q ⊕ R)" by(rule Strong_Early_Bisim_SC.sumAssoc)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma sumZero:
  fixes P :: pi
  
  shows "P ⊕ 𝟬 ≈ P"
proof -
  have "P ⊕ 𝟬 ∼⇩e P" by(rule Strong_Early_Bisim_SC.sumZero)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

(******** The |-operator *********)

lemma parZero:
  fixes P :: pi

  shows "P ∥ 𝟬 ≈ P"
proof -
  have "P ∥ 𝟬 ∼⇩e P" by(rule Strong_Early_Bisim_SC.parZero)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma parSym:
  fixes P :: pi
  and   Q :: pi

  shows "P ∥ Q ≈ Q ∥ P"
proof -
  have "P ∥ Q ∼⇩e Q ∥ P" by(rule Strong_Early_Bisim_SC.parSym)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma scopeExtPar:
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes "x ♯ P"

  shows "<νx>(P ∥ Q) ≈ P ∥ <νx>Q"
proof -
  from ‹x ♯ P› have "<νx>(P ∥ Q) ∼⇩e P ∥ <νx>Q" by(rule Strong_Early_Bisim_SC.scopeExtPar)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma scopeExtPar':
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes "x ♯ Q"

  shows "<νx>(P ∥ Q) ≈ (<νx>P) ∥ Q"
proof - 
  from ‹x ♯ Q› have "<νx>(P ∥ Q) ∼⇩e (<νx>P) ∥ Q" by(rule Strong_Early_Bisim_SC.scopeExtPar')
  thus ?thesis by(rule strongBisimWeakBisim)
qed

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

  shows "(P ∥ Q) ∥ R ≈ P ∥ (Q ∥ R)"
proof -
  have "(P ∥ Q) ∥ R ∼⇩e P ∥ (Q ∥ R)" by(rule Strong_Early_Bisim_SC.parAssoc)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma freshRes:
  fixes P :: pi
  and   a :: name

  assumes "a ♯ P"

  shows "<νa>P ≈ P"
proof -
  from ‹a ♯ P› have "<νa>P ∼⇩e P" by(rule Strong_Early_Bisim_SC.freshRes)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma scopeExtSum:
  fixes P :: pi
  and   Q :: pi
  and   x :: name
  
  assumes "x ♯ P"

  shows "<νx>(P ⊕ Q) ≈ P ⊕ <νx>Q"
proof -
  from ‹x ♯ P› have "<νx>(P ⊕ Q) ∼⇩e P ⊕ <νx>Q" by(rule Strong_Early_Bisim_SC.scopeExtSum)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma bangSC:
  fixes P

  shows "!P ≈ P ∥ !P"
proof -
  have "!P ∼⇩e P ∥ !P" by(rule Strong_Early_Bisim_SC.bangSC)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

end