Theory Weak_Bisim_Pres

(* 
   Title: The Calculus of Communicating Systems   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Bisim_Pres
  imports Weak_Bisim Weak_Sim_Pres Strong_Bisim_SC
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: weakBisimulationCoinduct) (auto dest: weakBisimulationE intro: actPres)
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: weakBisimulationCoinduct, auto) 
      (blast intro: parPres dest: weakBisimulationE)+
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: weakBisimulationCoinduct) (auto intro: resPres dest: weakBisimulationE)
qed

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

  assumes "P ≈ Q"

  shows "!P ≈ !Q"
proof -
  let ?X = "bangRel weakBisimulation"
  let ?Y = "weakBisimulation O ?X O bisim"
  {
    fix R T P Q
    assume "R ≈ T" and "(P, Q) ∈ ?Y"
    from ‹(P, Q) ∈ ?Y› obtain P' Q' where "P ≈ P'" and "(P', Q') ∈ ?X" and "Q' ∼ Q"
      by auto
    from ‹P ≈ P'› have "R ∥ P ≈ R ∥ P'" 
      by(metis parPres bisimWeakBisimulation transitive parComm)
    moreover from ‹R ≈ T› ‹(P', Q') ∈ ?X› have "(R ∥ P', T ∥ Q') ∈ ?X" by(auto dest: BRPar)
    moreover from ‹Q' ∼ Q› have "T ∥ Q' ∼ T ∥ Q" by(metis Strong_Bisim_Pres.parPres Strong_Bisim.transitive parComm)
    ultimately have "(R ∥ P, T ∥ Q) ∈ ?Y" by auto
  } note BRParAux = this

  from assms have "(!P, !Q) ∈ ?X" by(auto intro: BRBang)
  thus ?thesis
  proof(coinduct rule: weakBisimWeakUpto)
    case(cSim P Q)
    from ‹(P, Q) ∈ bangRel weakBisimulation› show ?case
    proof(induct)
      case(BRBang P Q)
      note ‹P ≈ Q› weakBisimulationE(1) BRParAux
      moreover have "?X ⊆ ?Y" by(auto intro: Strong_Bisim.reflexive reflexive)
      moreover {
        fix P Q
        assume "(P ∥ !P, Q) ∈ ?Y"
        hence "(!P, Q) ∈ ?Y" using bangUnfold
          by(blast dest: Strong_Bisim.transitive transitive bisimWeakBisimulation)
      }
      ultimately show ?case by(rule bangPres)
    next
      case(BRPar R T P Q)
      from ‹R ≈ T› have "R ↝⇧^<weakBisimulation> T" by(rule weakBisimulationE)
      moreover note ‹R ≈ T› ‹P ↝⇧^<?Y> Q› 
      moreover from ‹(P, Q) ∈ ?X› have "(P, Q) ∈ ?Y" by(blast intro: Strong_Bisim.reflexive reflexive)
      ultimately show ?case using BRParAux by(rule Weak_Sim_Pres.parPresAux)
    qed
  next
    case(cSym P Q)
    thus ?case
      by induct (auto dest: weakBisimulationE intro: BRPar BRBang)
  qed
qed

end