Theory Weak_Early_Bisim_SC
theory Weak_Early_Bisim_SC
imports Weak_Early_Bisim Strong_Early_Bisim_SC
begin
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
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
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
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