Theory Weak_Late_Cong_Pres

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Weak_Late_Cong_Pres
  imports Weak_Late_Cong Weak_Late_Step_Sim_Pres Weak_Late_Bisim_Pres
begin

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

  shows "τ.(P) ≃ τ.(Q)"
using assms
by(blast intro: unfoldI Weak_Late_Step_Sim_Pres.tauPres dest: congruenceWeakBisim symetric)

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

  shows "a{b}.P ≃ a{b}.Q"
using assms
by(blast intro: unfoldI Weak_Late_Step_Sim_Pres.outputPres dest: congruenceWeakBisim symetric)

lemma inputPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   x :: name

  assumes PSimQ: "∀y. P[x::=y] ≃ Q[x::=y]"
  
  shows "a<x>.P ≃ a<x>.Q"
using assms
apply(rule_tac unfoldI)
apply(rule_tac Weak_Late_Step_Sim_Pres.inputPres, auto intro: congruenceWeakBisim)
by(rule_tac Weak_Late_Step_Sim_Pres.inputPres, auto intro: congruenceWeakBisim Weak_Late_Bisim.symmetric)

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(blast intro: unfoldI Weak_Late_Step_Sim_Pres.matchPres dest: unfoldE symetric)

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(blast intro: unfoldI Weak_Late_Step_Sim_Pres.mismatchPres dest: unfoldE symetric)

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

  assumes "P ≃ Q"

  shows "P ⊕ R ≃ Q ⊕ R"
using assms
by(blast intro: Weak_Late_Bisim.reflexive unfoldI Weak_Late_Step_Sim_Pres.sumPres dest: unfoldE symetric)

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_Late_Bisim_Pres.parPres Weak_Late_Bisim_Pres.resPres Weak_Late_Bisim.reflexive Weak_Late_Bisim.eqvt
      by(blast intro: Weak_Late_Step_Sim_Pres.parPres)
  qed
  with assms show ?thesis
    by(blast intro: unfoldI dest: congruenceWeakBisim unfoldE symetric)
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_Late_Bisim.eqvt Weak_Late_Bisim_Pres.resPres show "<νx>P ↝<weakBisim> <νx>Q"
      by(blast intro: Weak_Late_Step_Sim_Pres.resPres)
  qed
  with assms show ?thesis
    by(blast intro: unfoldI dest: congruenceWeakBisim unfoldE symetric)
qed

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

  shows "!P ≃ !Q"
proof -
  have "⋀P Q. ⟦P ↝<weakBisim> Q; P ≃ Q⟧ ⟹ !P ↝<weakBisim> !Q"
  proof -
    fix P Q
    assume "P ↝<weakBisim> Q" and "P ≃ Q"
    hence "!P ↝<bangRel weakBisim> !Q" using unfoldE(1) congruenceWeakBisim Weak_Late_Bisim.eqvt 
      by(rule Weak_Late_Step_Sim_Pres.bangPres)
    moreover have "bangRel weakBisim ⊆ weakBisim"
      proof auto
        fix a b
        assume "(a, b) ∈ bangRel weakBisim"
        thus   "a ≈ b"
          apply(induct rule: bangRel.induct)
          apply (metis Weak_Late_Bisim_Pres.bangPres)
          apply (metis Weak_Late_Bisim.reflexive Weak_Late_Bisim.symmetric Weak_Late_Bisim.transitive Weak_Late_Bisim_Pres.parPres Weak_Late_Bisim_SC.parSym)
          by (metis Weak_Late_Bisim_Pres.resPres)
      qed
    ultimately show"!P ↝<weakBisim> !Q" 
      by(rule Weak_Late_Step_Sim.monotonic)
  qed

  with assms show ?thesis
    by(blast intro: unfoldI dest: unfoldE symetric congruenceWeakBisim)
qed

end