Theory Weak_Early_Cong_Pres

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Weak_Early_Cong_Pres
  imports Weak_Early_Cong Weak_Early_Step_Sim_Pres Weak_Early_Bisim_Pres
begin

lemma tauPres:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ≃ Q"

  shows "τ.(P) ≃ τ.(Q)"
proof -
  from assms have "P ≈ Q" by(rule congruenceWeakBisim)
  thus ?thesis by(force intro: Weak_Early_Step_Sim_Pres.tauPres simp add: weakCongruence_def dest: weakBisimE(2))
qed

lemma outputPres:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ≃ Q"

  shows "a{b}.P ≃ a{b}.Q"
proof -
  from assms have "P ≈ Q" by(rule congruenceWeakBisim)
  thus ?thesis by(force intro: Weak_Early_Step_Sim_Pres.outputPres simp add: weakCongruence_def dest: weakBisimE(2))
qed

lemma matchPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P ≃ Q"

  shows "[a⌢b]P ≃ [a⌢b]Q"
using assms
by(auto simp add: weakCongruence_def intro: Weak_Early_Step_Sim_Pres.matchPres)

lemma mismatchPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P ≃ Q"

  shows "[a≠b]P ≃ [a≠b]Q"
using assms
by(auto simp add: weakCongruence_def intro: Weak_Early_Step_Sim_Pres.mismatchPres)

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

  assumes "P ≃ Q"

  shows "P ⊕ R ≃ Q ⊕ R"
using assms
by(auto simp add: weakCongruence_def intro: Weak_Early_Step_Sim_Pres.sumPres Weak_Early_Bisim.reflexive)

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

  assumes "P ≃ Q"

  shows "P ∥ R ≃ Q ∥ R"
proof -
  have "⋀P Q R. ⟦P ↝«weakBisim» Q; P ≈ Q⟧ ⟹ P ∥ R ↝«weakBisim» Q ∥ R"
  proof -
    fix P Q R
    assume "P ↝«weakBisim» Q" and "P ≈ Q"
    thus "P ∥ R ↝«weakBisim» Q ∥ R"
      using Weak_Early_Bisim_Pres.parPres Weak_Early_Bisim_Pres.resPres Weak_Early_Bisim.reflexive Weak_Early_Bisim.eqvt
      by(blast intro: Weak_Early_Step_Sim_Pres.parPres)
  qed
  moreover from assms have "P ≈ Q" by(rule congruenceWeakBisim)
  ultimately show ?thesis using assms
    by(auto simp add: weakCongruence_def dest: weakBisimE)
qed

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

  assumes PeqQ: "P ≃ Q"
  
  shows "<νx>P ≃ <νx>Q"
proof -
  have "⋀P Q x. P ↝«weakBisim» Q ⟹ <νx>P ↝«weakBisim» <νx>Q"
  proof -
    fix P Q x
    assume "P ↝«weakBisim» Q"
    with Weak_Early_Bisim.eqvt Weak_Early_Bisim_Pres.resPres show "<νx>P ↝«weakBisim» <νx>Q"
      by(blast intro: Weak_Early_Step_Sim_Pres.resPres)
  qed
  with assms show ?thesis by(simp add: weakCongruence_def)
qed

lemma bangPres:
  fixes P :: pi
  and   Q :: pi
  
  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 ↝«weakBisim» Q" by(auto simp add: weakCongruence_def)
  moreover from congruenceWeakBisim have "?X ⊆ weakBisim" by auto
  ultimately have "!P ↝«bangRel weakBisim» !Q" using Weak_Early_Bisim.eqvt 
    by(rule Weak_Early_Step_Sim_Pres.bangPres)
  moreover have "bangRel weakBisim ⊆ weakBisim" by(rule bangRelSubWeakBisim)
  ultimately show "!P ↝«weakBisim» !Q"
    by(rule Weak_Early_Step_Sim.monotonic)
qed
  
end