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|)),\<zero> ∼ \<zero>"
proof -
  have "((|νx|)),\<zero>, \<zero>) ∈ {((|νx|)),\<zero>, \<zero>), (\<zero>, (|νx|)),\<zero>)}" 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 \<sharp> P"

  shows "(|νx|)),(P \<parallel> Q) ∼ P \<parallel> (|νx|)),Q"
proof -
  let ?X = "{((|νx|)),(P \<parallel> Q), P \<parallel> (|νx|)),Q) | x P Q. x \<sharp> P} ∪ {(P \<parallel> (|νx|)),Q, (|νx|)),(P \<parallel> Q)) | x P Q. x \<sharp> P}"
  from assms have "((|νx|)),(P \<parallel> Q), P \<parallel> (|ν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 ⊕ \<zero> ∼ P"
proof -
  have "(P ⊕ \<zero>, P) ∈ {(P ⊕ \<zero>, P), (P, P ⊕ \<zero>)}" by simp
  thus ?thesis by(coinduct rule: bisimCoinduct) (auto intro: sumIdLeft sumIdRight reflexive) 
qed

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

  shows "P \<parallel> Q ∼ Q \<parallel> P"
proof -
  have "(P \<parallel> Q, Q \<parallel> P) ∈ {(P \<parallel> Q, Q \<parallel> P) | P Q. True} ∪ {(Q \<parallel> P, P \<parallel> 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 \<parallel> Q) \<parallel> R ∼ P \<parallel> (Q \<parallel> R)"
proof -
  have "((P \<parallel> Q) \<parallel> R, P \<parallel> (Q \<parallel> R)) ∈ {((P \<parallel> Q) \<parallel> R, P \<parallel> (Q \<parallel> R)) | P Q R. True} ∪  
                                     {(P \<parallel> (Q \<parallel> R), (P \<parallel> Q) \<parallel> 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 \<parallel> \<zero> ∼ P"
proof -
  have "(P \<parallel> \<zero>, P) ∈ {(P \<parallel> \<zero>, P) | P. True} ∪ {(P, P \<parallel> \<zero>) | 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 \<sharp> P"

  shows "(|νx|)),P ∼ P"
proof -
  have "(|νx|)),P ∼ (|νx|)),P \<parallel> \<zero>" by(rule parId[THEN symmetric])
  moreover have "(|νx|)),P \<parallel> \<zero> ∼ \<zero> \<parallel> (|νx|)),P" by(rule parComm)
  moreover have "\<zero> \<parallel> (|νx|)),P ∼ (|νx|)),(\<zero> \<parallel> P)" by(rule scopeExt[THEN symmetric]) auto
  moreover have "(|νx|)),(\<zero> \<parallel> P) ∼ (|νx|)),(P \<parallel> \<zero>)" by(rule resPres[OF parComm])
  moreover from `x \<sharp> P` have "(|νx|)),(P \<parallel> \<zero>) ∼ P \<parallel> (|νx|)),\<zero>" by(rule scopeExt)
  moreover have  "P \<parallel> (|νx|)),\<zero> ∼ (|νx|)),\<zero> \<parallel> P" by(rule parComm)
  moreover have "(|νx|)),\<zero> \<parallel> P ∼ \<zero> \<parallel> P" by(rule parPres[OF resNil])
  moreover have "\<zero> \<parallel> P ∼ P \<parallel> \<zero>" by(rule parComm)
  moreover have "P \<parallel> \<zero> ∼ P" by(rule parId)
  ultimately show ?thesis by(metis transitive)
qed

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

  assumes "x \<sharp> 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 \<sharp> 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 \<sharp> α"

  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 \<sharp> α`
    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 \<parallel> !P"
proof -
  have "(!P, P \<parallel> !P) ∈ {(!P, P \<parallel> !P), (P \<parallel> !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