Theory Weak_Cong_Pres

(* 
   Title: The Calculus of Communicating Systems   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Cong_Pres
  imports Weak_Cong Weak_Bisim_Pres Weak_Cong_Sim_Pres
begin

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

  assumes "P ≅ Q"

  shows "α.(P) ≅ α.(Q)"
using assms
proof(induct rule: weakCongISym2)
  case(cSim P Q)
  from ‹P ≅ Q› have "P ≈ Q" by(rule weakCongruenceWeakBisimulation)
  thus ?case by(rule actPres)
qed

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

  assumes "P ≅ Q"

  shows "P ⊕ R ≅ Q ⊕ R"
using assms
proof(induct rule: weakCongISym2)
  case(cSim P Q)
  from ‹P ≅ Q› have "P ↝<weakBisimulation> Q" by(rule weakCongruenceE)
  thus ?case using Weak_Bisim.reflexive
    by(rule_tac sumPres) auto
qed

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

  assumes "P ≅ Q"

  shows "P ∥ R ≅ Q ∥ R"
using assms
proof(induct rule: weakCongISym2)
  case(cSim P Q)
  from ‹P ≅ Q› have "P ↝<weakBisimulation> Q" by(rule weakCongruenceE)
  moreover from ‹P ≅ Q› have "P ≈ Q" by(rule weakCongruenceWeakBisimulation)
  ultimately show ?case using Weak_Bisim_Pres.parPres
    by(rule parPres)
qed

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

  assumes "P ≅ Q"

  shows "⦇νx⦈P ≅ ⦇νx⦈Q"
using assms
proof(induct rule: weakCongISym2)
  case(cSim P Q)
  from ‹P ≅ Q› have "P ↝<weakBisimulation> Q" by(rule weakCongruenceE)
  thus ?case using Weak_Bisim_Pres.resPres
    by(rule resPres)
qed

lemma weakBisimBangRel: "bangRel weakBisimulation ⊆ weakBisimulation"
proof auto
  fix P Q
  assume "(P, Q) ∈ bangRel weakBisimulation"
  thus "P ≈ Q"
  proof(induct rule: bangRel.induct)
    case(BRBang P Q)
    from ‹P ≈ Q› show "!P ≈ !Q" by(rule Weak_Bisim_Pres.bangPres)
  next
    case(BRPar R T P Q)
    from ‹R ≈ T› have "R ∥ P ≈ T ∥ P" by(rule Weak_Bisim_Pres.parPres)
    moreover from ‹P ≈ Q› have "P ∥ T ≈ Q ∥ T" by(rule Weak_Bisim_Pres.parPres)
    hence "T ∥ P ≈ T ∥ Q" by(metis bisimWeakBisimulation Weak_Bisim.transitive parComm)
    ultimately show "R ∥ P ≈ T ∥ Q" by(rule Weak_Bisim.transitive)
  qed
qed

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

  assumes "P ≅ Q"

  shows "!P ≅ !Q"
using assms
proof(induct rule: weakCongISym2)
  case(cSim P Q)
  let ?X = "{(P, Q) | P Q. P ≅ Q}"
  from ‹P ≅ Q› have "(P, Q) ∈ ?X" by auto
  moreover have "⋀P Q. (P, Q) ∈ ?X ⟹ P ↝<weakBisimulation> Q" by(auto dest: weakCongruenceE)
  moreover have "?X ⊆ weakBisimulation" by(auto intro: weakCongruenceWeakBisimulation)
  ultimately have "!P ↝<bangRel weakBisimulation> !Q" by(rule bangPres)
  thus ?case using weakBisimBangRel by(rule Weak_Cong_Sim.weakMonotonic)
qed

end