(* 
   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)0 ∼ 0"
proof -
  have "((νx)0, 0) ∈ {((νx)0, 0), (0, (νx)0)}" 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 ⊕ 0 ∼ P"
proof -
  have "(P ⊕ 0, P) ∈ {(P ⊕ 0, P), (P, P ⊕ 0)}" 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 ∥ 0 ∼ P"
proof -
  have "(P ∥ 0, P) ∈ {(P ∥ 0, P) | P. True} ∪ {(P, P ∥ 0) | 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 ∥ 0" by(rule parId[THEN symmetric])
  moreover have "(νx)P ∥ 0 ∼ 0 ∥ (νx)P" by(rule parComm)
  moreover have "0 ∥ (νx)P ∼ (νx)(0 ∥ P)" by(rule scopeExt[THEN symmetric]) auto
  moreover have "(νx)(0 ∥ P) ∼ (νx)(P ∥ 0)" by(rule resPres[OF parComm])
  moreover from ‹x ♯ P› have "(νx)(P ∥ 0) ∼ P ∥ (νx)0" by(rule scopeExt)
  moreover have  "P ∥ (νx)0 ∼ (νx)0 ∥ P" by(rule parComm)
  moreover have "(νx)0 ∥ P ∼ 0 ∥ P" by(rule parPres[OF resNil])
  moreover have "0 ∥ P ∼ P ∥ 0" by(rule parComm)
  moreover have "P ∥ 0 ∼ 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