Theory Weak_Early_Cong_Subst_Pres

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

lemma weakCongStructCong:
  fixes P :: pi
  and   Q :: pi

  assumes "P ≡⇩s Q"

  shows "P ≃⇧s Q"
using assms
by(metis earlyCongStructCong strongEqWeakCong)


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

  shows "τ.(P) ≃⇧s τ.(Q)"
using assms
by(auto simp add: weakCongruenceSubst_def intro: Weak_Early_Cong_Pres.tauPres)

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

  assumes PeqQ: "P ≃⇧s Q"

  shows "a<x>.P ≃⇧s a<x>.Q"
proof(auto simp add: weakCongruenceSubst_def)
  fix s::"(name × name) list"

  from congruenceWeakBisim have Input: "⋀P Q a x s. ⟦P[<s>] ≃⇧s Q[<s>]; x ♯ s⟧ ⟹ (a<x>.P)[<s>] ≃ (a<x>.Q)[<s>]"
    apply(auto simp add: weakCongruenceSubst_def weakCongruence_def)
    apply(rule Weak_Early_Step_Sim_Pres.inputPres, auto)
    apply(erule_tac x="[(x, y)]" in allE, auto)
    apply(rule Weak_Early_Step_Sim_Pres.inputPres, auto)
    by(erule_tac x="[(x, y)]" in allE, auto)

  then obtain c::name where cFreshP: "c ♯ P" and cFreshQ: "c ♯ Q" and cFreshs: "c ♯ s"
    by(force intro: name_exists_fresh[of "(P, Q, s)"])

  from PeqQ have "P[<([(x, c)] ∙ s)>] ≃⇧s Q[<([(x, c)] ∙ s)>]" by(rule partUnfold)
  hence "([(x, c)] ∙ P[<([(x, c)] ∙ s)>]) ≃⇧s  ([(x, c)] ∙ Q[<([(x, c)] ∙ s)>])" by(rule Weak_Early_Cong_Subst.eqvtI)
  hence "([(x, c)] ∙ P)[<s>] ≃⇧s ([(x, c)] ∙ Q)[<s>]" by simp
  hence "(a<c>.([(x, c)] ∙ P))[<s>] ≃ (a<c>.([(x, c)] ∙ Q))[<s>]" using cFreshs by(rule Input)

  moreover from cFreshP cFreshQ have "a<x>.P = a<c>.([(x, c)] ∙ P)" and "a<x>.Q = a<c>.([(x, c)] ∙ Q)"
    by(simp add: Agent.alphaInput)+

  ultimately show "(a<x>.P)[<s>] ≃ (a<x>.Q)[<s>]" by simp
qed

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

  shows "a{b}.P ≃⇧s a{b}.Q"
using assms
by(auto simp add: weakCongruenceSubst_def intro: Weak_Early_Cong_Pres.outputPres)

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

  assumes "P ≃⇧s Q"

  shows "[a⌢b]P ≃⇧s [a⌢b]Q"
using assms
by(auto simp add: weakCongruenceSubst_def intro: Weak_Early_Cong_Pres.matchPres)

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

  assumes "P ≃⇧s Q"

  shows "[a≠b]P ≃⇧s [a≠b]Q"
using assms
by(auto simp add: weakCongruenceSubst_def intro: Weak_Early_Cong_Pres.mismatchPres)

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

  assumes "P ≃⇧s Q"

  shows "P ⊕ R ≃⇧s Q ⊕ R"
using assms
by(auto simp add: weakCongruenceSubst_def intro: Weak_Early_Cong_Pres.sumPres)

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

  assumes "P ≃⇧s Q"

  shows "P ∥ R ≃⇧s Q ∥ R"
using assms
by(auto simp add: weakCongruenceSubst_def intro: Weak_Early_Cong_Pres.parPres)

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

  assumes PeqQ: "P ≃⇧s Q"
  
  shows "<νx>P ≃⇧s <νx>Q"
proof(auto simp add: weakCongruenceSubst_def)
  fix s::"(name × name) list"

  have Goal: "⋀P Q x s. ⟦P[<s>] ↝«weakBisim» Q[<s>]; x ♯ s⟧ ⟹ (<νx>P)[<s>] ↝«weakBisim» (<νx>Q)[<s>]"
    by(force intro: Weak_Early_Step_Sim_Pres.resPres Weak_Early_Bisim_Pres.resPres Weak_Early_Bisim.eqvt)
  
  then obtain c::name where cFreshP: "c ♯ P" and cFreshQ: "c ♯ Q" and cFreshs: "c ♯ s"
    by(force intro: name_exists_fresh[of "(P, Q, s)"])

  from PeqQ have "P[<([(x, c)] ∙ s)>] ↝«weakBisim» Q[<([(x, c)] ∙ s)>]" and 
                 "Q[<([(x, c)] ∙ s)>] ↝«weakBisim» P[<([(x, c)] ∙ s)>]"
    by(force simp add: weakCongruenceSubst_def weakCongruence_def)+

  hence "([(x, c)] ∙ (P[<([(x, c)] ∙ s)>])) ↝«weakBisim» ([(x, c)] ∙ (Q[<([(x, c)] ∙ s)>]))" and 
        "([(x, c)] ∙ (Q[<([(x, c)] ∙ s)>])) ↝«weakBisim» ([(x, c)] ∙ (P[<([(x, c)] ∙ s)>]))"
    by(blast intro: Weak_Early_Step_Sim.eqvtI Weak_Early_Bisim.eqvt)+

  hence "([(x, c)] ∙ P)[<s>] ↝«weakBisim» ([(x, c)] ∙ Q)[<s>]" and
        "([(x, c)] ∙ Q)[<s>] ↝«weakBisim» ([(x, c)] ∙ P)[<s>]" by simp+

  with cFreshs have "(<νc>([(x, c)] ∙ P))[<s>] ↝«weakBisim» (<νc>([(x, c)] ∙ Q))[<s>]" and
                    "(<νc>([(x, c)] ∙ Q))[<s>] ↝«weakBisim» (<νc>([(x, c)] ∙ P))[<s>]"
    by(blast intro: Goal)+

  moreover from cFreshP cFreshQ have "<νx>P = <νc>([(x, c)] ∙ P)" and "<νx>Q = <νc>([(x, c)] ∙ Q)"
    by(simp add: alphaRes)+

  ultimately show "(<νx>P)[<s>] ≃ (<νx>Q)[<s>]"
    by(simp add: weakCongruence_def)
qed

lemma bangPres:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ≃⇧s Q"

  shows "!P ≃⇧s !Q"
using assms
by(auto simp add: weakCongruenceSubst_def intro: Weak_Early_Cong_Pres.bangPres)

end