Theory Weak_Late_Bisim_SC

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Weak_Late_Bisim_SC
  imports Weak_Late_Bisim Strong_Late_Bisim_SC
begin

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

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

lemma resComm:
  fixes P :: pi
  
  shows "a>b>P  b>a>P"
proof -
  have "a>b>P  b>a>P" by(rule Strong_Late_Bisim_SC.resComm)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

(******** Match *********)

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

  shows "[aa]P  P"
proof -
  have "[aa]P  P" by(rule Strong_Late_Bisim_SC.matchId)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

(******** Mismatch *********)

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

  assumes "a  b"

  shows "[ab]P  P"
proof -
  from assms have "[ab]P  P" by(rule Strong_Late_Bisim_SC.mismatchId)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

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

  shows "[aa]P  𝟬"
proof -
  have "[aa]P  𝟬" by(rule Strong_Late_Bisim_SC.mismatchNil) 
  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  Q  P" by(rule Strong_Late_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  P  (Q  R)" by(rule Strong_Late_Bisim_SC.sumAssoc)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma sumZero:
  fixes P :: pi
  
  shows "P  𝟬  P"
proof -
  have "P  𝟬  P" by(rule Strong_Late_Bisim_SC.sumZero)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

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

lemma parZero:
  fixes P :: pi

  shows "P  𝟬  P"
proof -
  have "P  𝟬  P" by(rule Strong_Late_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  Q  P" by(rule Strong_Late_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 assms have "x>(P  Q)  P  x>Q" by(rule Strong_Late_Bisim_SC.scopeExtPar)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

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

  assumes xFreshQ: "x  Q"

  shows "x>(P  Q)  (x>P)  Q"
proof -
  from assms have "x>(P  Q)  (x>P)  Q" by(rule Strong_Late_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  P  (Q  R)" by(rule Strong_Late_Bisim_SC.parAssoc)
  thus ?thesis by(rule strongBisimWeakBisim)
qed
(*
lemma resZero:
  fixes x :: name

  shows "<νx>𝟬 ≈ 𝟬"
proof -
  have "<νx>𝟬 ∼ 𝟬" by(rule Strong_Late_Bisim_SC.resZero)
  thus ?thesis by(rule strongBisimWeakBisim)
qed
*)
lemma freshRes:
  fixes P :: pi
  and   a :: name

  assumes aFreshP: "a  P"

  shows "a>P  P"
proof -
  from assms have "a>P  P" by(rule Strong_Late_Bisim_SC.scopeFresh)
  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 assms have "x>(P  Q)  P  x>Q" by(rule Strong_Late_Bisim_SC.scopeExtSum)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

lemma bangSC:
  fixes P

  shows "!P  P  !P"
proof -
  have "!P  P  !P" by(rule Strong_Late_Bisim_SC.bangSC)
  thus ?thesis by(rule strongBisimWeakBisim)
qed

end