Theory Strong_Bisim_Pres

(* 
   Title: The Calculus of Communicating Systems   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Strong_Bisim_Pres
  imports Strong_Bisim Strong_Sim_Pres
begin

lemma actPres:
  fixes P :: ccs
  and   Q :: ccs
  and   α :: act

  assumes "P ∼ Q"

  shows "α.(P) ∼ α.(Q)"
proof -
  let ?X = "{(α.(P), α.(Q)) | P Q. P ∼ Q}"
  from assms have "(α.(P), α.(Q)) ∈ ?X" by auto
  thus ?thesis 
    by(coinduct rule: bisimCoinduct) (auto dest: bisimE intro: actPres)
qed

lemma sumPres:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes "P ∼ Q"

  shows "P ⊕ R ∼ Q ⊕ R"
proof -
  let ?X = "{(P ⊕ R, Q ⊕ R) | P Q R. P ∼ Q}"
  from assms have "(P ⊕ R, Q ⊕ R) ∈ ?X" by auto
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: sumPres reflexive dest: bisimE)
qed

lemma parPres:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes "P ∼ Q"

  shows "P ∥ R ∼ Q ∥ R"
proof -
  let ?X = "{(P ∥ R, Q ∥ R) | P Q R. P ∼ Q}"
  from assms have "(P ∥ R, Q ∥ R) ∈ ?X" by blast
  thus ?thesis
    by(coinduct rule: bisimCoinduct, auto) (blast intro: parPres dest: bisimE)+
qed

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

  assumes "P ∼ Q"

  shows "⦇νx⦈P ∼ ⦇νx⦈Q"
proof -
  let ?X = "{(⦇νx⦈P, ⦇νx⦈Q) | x P Q. P ∼ Q}"
  from assms have "(⦇νx⦈P, ⦇νx⦈Q) ∈ ?X" by auto
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: resPres dest: bisimE)
qed

lemma bangPres: 
  fixes P :: ccs
  and   Q :: ccs

  assumes "P ∼ Q"

  shows "!P ∼ !Q"
proof -
  from assms have "(!P, !Q) ∈ bangRel bisim"
    by(auto intro: BRBang)
  thus ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cSim P Q)
    from ‹(P, Q) ∈ bangRel bisim› show ?case
    proof(induct)
      case(BRBang P Q)
      note ‹P ∼ Q› bisimE(1)
      thus "!P ↝[bangRel bisim] !Q" by(rule bangPres)
    next
      case(BRPar R T P Q)
      from ‹R ∼ T› have "R ↝[bisim] T" by(rule bisimE)
      moreover note ‹R ∼ T› ‹P ↝[bangRel bisim] Q› ‹(P, Q) ∈ bangRel bisim› bangRel.BRPar
      ultimately show ?case by(rule Strong_Sim_Pres.parPresAux)
    qed
  next
    case(cSym P Q)
    thus ?case
      by induct (auto dest: bisimE intro: BRPar BRBang)
  qed
qed

end