Theory Strong_Early_Bisim_Subst_Pres

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Strong_Early_Bisim_Subst_Pres
  imports Strong_Early_Bisim_Subst Strong_Early_Bisim_Pres
begin

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

  shows "τ.(P) ∼⇧s τ.(Q)"
using assms
by(force simp add: substClosed_def intro: Strong_Early_Bisim_Pres.tauPres)

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

  assumes "P ∼⇧s Q"

  shows "a<x>.P ∼⇧s a<x>.Q"
proof(auto simp add: substClosed_def)
  fix σ :: "(name × name) list"
  {
    fix P Q a x σ
    assume "P ∼⇧s Q"
    then have "P[<σ>] ∼⇧s Q[<σ>]" by(rule partUnfold)
    then have "∀y. (P[<σ>])[x::=y] ∼ (Q[<σ>])[x::=y]"
      apply(auto simp add: substClosed_def)
      by(erule_tac x="[(x, y)]" in allE) auto
    moreover assume "x ♯ σ"
    ultimately have "(a<x>.P)[<σ>] ∼ (a<x>.Q)[<σ>]" 
      by(force intro: Strong_Early_Bisim_Pres.inputPres)
  }
  note Goal = this

  obtain y::name where "y ♯ P" and "y ♯ Q" and "y ♯ σ"
    by(generate_fresh "name") auto
  from ‹P ∼⇧s Q› have "([(x, y)] ∙ P) ∼⇧s ([(x, y)] ∙ Q)" by(rule eqvtI)
  hence "(a<y>.([(x, y)] ∙ P))[<σ>] ∼ (a<y>.([(x, y)] ∙ Q))[<σ>]" using ‹y ♯ σ› by(rule Goal)
  moreover from ‹y ♯ P› ‹y ♯ Q› have "a<x>.P = a<y>.([(x, y)] ∙ P)" and "a<x>.Q = a<y>.([(x, y)] ∙ Q)"
    by(simp add: alphaInput)+

  ultimately show "(a<x>.P)[<σ>] ∼ (a<x>.Q)[<σ>]" 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(force simp add: substClosed_def intro: Strong_Early_Bisim_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(force simp add: substClosed_def intro: Strong_Early_Bisim_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(force simp add: substClosed_def intro: Strong_Early_Bisim_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(force simp add: substClosed_def intro: Strong_Early_Bisim_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(force simp add: substClosed_def intro: Strong_Early_Bisim_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: substClosed_def)
  fix s::"(name × name) list"

  have Res: "⋀P Q x s. ⟦P[<s>] ∼ Q[<s>]; x ♯ s⟧ ⟹ (<νx>P)[<s>] ∼ (<νx>Q)[<s>]"
    by(force intro: Strong_Early_Bisim_Pres.resPres)

  have "∃c::name. c ♯ (P, Q, s)" by(blast intro: name_exists_fresh)
  then obtain c::name where cFreshP: "c ♯ P" and cFreshQ: "c ♯ Q" and cFreshs: "c ♯ s"
    by(force simp add: fresh_prod)

  from PeqQ have "P[<([(x, c)] ∙ s)>] ∼ Q[<([(x, c)] ∙ s)>]" by(simp add: substClosed_def)
  hence "([(x, c)] ∙ P[<([(x, c)] ∙ s)>]) ∼ ([(x, c)] ∙ Q[<([(x, c)] ∙ s)>])" by(rule Strong_Early_Bisim.bisimClosed)
  hence "([(x, c)] ∙ P)[<s>] ∼ ([(x, c)] ∙ Q)[<s>]" by simp
  hence "(<νc>([(x, c)] ∙ P))[<s>] ∼ (<νc>([(x, c)] ∙ Q))[<s>]" using cFreshs by(rule Res)

  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
qed

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

  shows "!P ∼⇧s !Q"
using assms
by(force simp add: substClosed_def intro: Strong_Early_Bisim_Pres.bangPres)

end