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 \<parallel> R ∼ Q \<parallel> R"
proof -
  let ?X = "{(P \<parallel> R, Q \<parallel> R) | P Q R. P ∼ Q}"
  from assms have "(P \<parallel> R, Q \<parallel> 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 \<leadsto>[bangRel bisim] !Q" by(rule bangPres)
    next
      case(BRPar R T P Q)
      from `R ∼ T` have "R \<leadsto>[bisim] T" by(rule bisimE)
      moreover note `R ∼ T` `P \<leadsto>[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