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 \<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: 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 \<parallel> P ≈ R \<parallel> P'" 
      by(metis parPres bisimWeakBisimulation transitive parComm)
    moreover from `R ≈ T` `(P', Q') ∈ ?X` have "(R \<parallel> P', T \<parallel> Q') ∈ ?X" by(auto dest: BRPar)
    moreover from `Q' ∼ Q` have "T \<parallel> Q' ∼ T \<parallel> Q" by(metis Strong_Bisim_Pres.parPres Strong_Bisim.transitive parComm)
    ultimately have "(R \<parallel> P, T \<parallel> 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 \<parallel> !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 \<leadsto>⇧^<weakBisimulation> T" by(rule weakBisimulationE)
      moreover note `R ≈ T` `P \<leadsto>⇧^<?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