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 \<leadsto><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 \<parallel> R ≅ Q \<parallel> R"
using assms
proof(induct rule: weakCongISym2)
  case(cSim P Q)
  from `P ≅ Q` have "P \<leadsto><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 \<leadsto><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 \<parallel> P ≈ T \<parallel> P" by(rule Weak_Bisim_Pres.parPres)
    moreover from `P ≈ Q` have "P \<parallel> T ≈ Q \<parallel> T" by(rule Weak_Bisim_Pres.parPres)
    hence "T \<parallel> P ≈ T \<parallel> Q" by(metis bisimWeakBisimulation Weak_Bisim.transitive parComm)
    ultimately show "R \<parallel> P ≈ T \<parallel> 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 \<leadsto><weakBisimulation> Q" by(auto dest: weakCongruenceE)
  moreover have "?X ⊆ weakBisimulation" by(auto intro: weakCongruenceWeakBisimulation)
  ultimately have "!P \<leadsto><bangRel weakBisimulation> !Q" by(rule bangPres)
  thus ?case using weakBisimBangRel by(rule Weak_Cong_Sim.weakMonotonic)
qed

end