Theory Strong_Late_Bisim_Pres

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Strong_Late_Bisim_Pres
  imports Strong_Late_Bisim Strong_Late_Sim_Pres
begin

lemma tauPres:
  fixes P :: pi
  and   Q :: pi

  assumes "P ∼ Q"

  shows "τ.(P) ∼ τ.(Q)"
proof -
  let ?X = "{(τ.(P), τ.(Q)), (τ.(Q), τ.(P))}"
  have "(τ.(P), τ.(Q)) ∈ ?X" by auto
  thus ?thesis using ‹P ∼ Q›
    by(coinduct rule: bisimCoinduct)
      (auto intro: Strong_Late_Sim_Pres.tauPres dest: symmetric)
qed

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"
proof -
  let ?X = "{(a<x>.P, a<x>.Q) | a x P Q. ∀y. P[x::=y] ∼ Q[x::=y]}"
  {
    fix axP axQ p
    assume "(axP, axQ) ∈ ?X"
    then obtain a x P Q where A: "∀y. P[x::=y] ∼ Q[x::=y]" and B: "axP = a<x>.P" and C: "axQ = a<x>.Q"
      by auto
    have "⋀y. ((p::name prm) ∙ P)[(p ∙ x)::=y] ∼ (p ∙ Q)[(p ∙ x)::=y]"
    proof -
      fix y
      from A have "P[x::=(rev p ∙ y)] ∼ Q[x::=(rev p ∙ y)]"
        by blast
      hence "(p ∙ (P[x::=(rev p ∙ y)])) ∼ p ∙ (Q[x::=(rev p ∙ y)])"
        by(rule bisimClosed)
      thus "(p ∙ P)[(p ∙ x)::=y] ∼ (p ∙ Q)[(p ∙ x)::=y]"
        by(simp add: eqvts pt_pi_rev[OF pt_name_inst, OF at_name_inst])
    qed
    hence "((p::name prm) ∙ axP, p ∙ axQ) ∈ ?X" using B C
      by auto
  }
  hence "eqvt ?X" by(simp add: eqvt_def)

  from PSimQ have "(a<x>.P, a<x>.Q) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim P Q)
    thus ?case using ‹eqvt ?X›
      by(force intro: inputPres)
  next
    case(cSym P Q)
    thus ?case
      by(blast dest: symmetric)
  qed
qed

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

  assumes "P ∼ Q"

  shows "a{b}.P ∼ a{b}.Q"
proof -
  let ?X = "{(a{b}.P, a{b}.Q), (a{b}.Q, a{b}.P)}"
  have "(a{b}.P, a{b}.Q) ∈ ?X" by auto
  thus ?thesis using ‹P ∼ Q›
    by(coinduct rule: bisimCoinduct)
      (auto intro: Strong_Late_Sim_Pres.outputPres dest: symmetric)
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"
proof -
  let ?X = "{([a⌢b]P, [a⌢b]Q), ([a⌢b]Q, [a⌢b]P)}"
  have "([a⌢b]P, [a⌢b]Q) ∈ ?X" by auto
  thus ?thesis using ‹P ∼ Q›
    by(coinduct rule: bisimCoinduct)
      (auto intro: Strong_Late_Sim_Pres.matchPres dest: symmetric bisimE)
qed

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

  assumes "P ∼ Q"

  shows "[a≠b]P ∼ [a≠b]Q"
proof -
  let ?X = "{([a≠b]P, [a≠b]Q), ([a≠b]Q, [a≠b]P)}"
  have "([a≠b]P, [a≠b]Q) ∈ ?X" by auto
  thus ?thesis using ‹P ∼ Q›
    by(coinduct rule: bisimCoinduct)
      (auto intro: Strong_Late_Sim_Pres.mismatchPres dest: symmetric bisimE)
qed

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

  assumes "P ∼ Q"

  shows "P ⊕ R ∼ Q ⊕ R"
proof -
  let ?X = "{(P ⊕ R, Q ⊕ R), (Q ⊕ R, P ⊕ R)}"
  have "(P ⊕ R, Q ⊕ R) ∈ ?X" by auto
  thus ?thesis using ‹P ∼ Q›
    by(coinduct rule: bisimCoinduct)
      (auto intro: Strong_Late_Sim_Pres.sumPres reflexive dest: symmetric bisimE)
qed

lemma resPres:
  fixes P :: pi
  and   Q :: pi
  and   x :: name
  
  assumes "P ∼ Q"

  shows "<νx>P ∼ <νx>Q"
proof -
  let ?X = "{x. ∃P Q. P ∼ Q ∧ (∃a. x = (<νa>P, <νa>Q))}"
  from ‹P ∼ Q› have "(<νx>P, <νx>Q) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim xP xQ)
    {
      fix P Q a
      assume PSimQ: "P ↝[bisim] Q"
      moreover have "⋀P Q a. P ∼ Q ⟹ (<νa>P, <νa>Q) ∈ ?X ∪ bisim" by blast
      moreover have "bisim ⊆ ?X ∪ bisim" by blast
      moreover have "eqvt bisim" by simp
      moreover have "eqvt ?X"
        by(auto simp add: eqvt_def) (blast intro: bisimClosed)
      hence "eqvt (?X ∪ bisim)" by auto
      ultimately have "<νa>P ↝[(?X ∪ bisim)] <νa>Q"
        by(rule Strong_Late_Sim_Pres.resPres)
    }
    with ‹(xP, xQ) ∈ ?X› show ?case
      by(auto dest: bisimE)
  next
    case(cSym xP xQ)
    thus ?case by(auto dest: symmetric)
  qed
qed

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

  assumes "P ∼ Q"

  shows "P ∥ R ∼ Q ∥ R"
proof -
  let ?X = "{(resChain lst (P ∥ R), resChain lst (Q ∥ R)) | lst P R Q. P ∼ Q}"
  have EmptyChain: "⋀P Q. P ∥ Q = resChain [] (P ∥ Q)" by auto
  with ‹P ∼ Q› have "(P ∥ R, Q ∥ R) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim PR QR)
    {
      fix P Q R lst

      assume "P ∼ Q"

      hence "P ↝[bisim] Q" by(rule bisimE)
      moreover note ‹P ∼ Q›
      moreover have "⋀P Q R. P ∼ Q ⟹ (P ∥ R, Q ∥ R) ∈ ?X"
        by auto (blast intro: EmptyChain)
      moreover 
      {
        fix xP xQ x
        assume "(xP, xQ) ∈ ?X"
        then obtain P Q R lst 
          where "P ∼ Q" and "xP = resChain lst (P ∥ R)" and xQeq: "xQ = resChain lst (Q ∥ R)"
          by auto
        moreover hence "(resChain (x#lst) (P ∥ R), resChain (x#lst) (Q ∥ R)) ∈ ?X"
          by blast
        ultimately have "(<νx>xP, <νx>xQ) ∈ ?X" by auto
      }
      note ResPres = this
      moreover have "eqvt bisim" by simp
      moreover have "eqvt ?X"
        by(auto simp add: eqvt_def) (blast intro: bisimClosed)
      ultimately have "P ∥ R ↝[(?X)] Q ∥ R" by(rule parPres)
      hence "resChain lst (P ∥ R) ↝[?X] (resChain lst (Q ∥ R))" using ‹eqvt ?X› ResPres 
        by(rule resChainI)
      hence "resChain lst (P ∥ R) ↝[(?X ∪ bisim)] (resChain lst (Q ∥ R))"
        by(force intro: Strong_Late_Sim.monotonic)
    }
    with ‹(PR, QR) ∈ ?X› show ?case
      by auto
  next
    case(cSym PR QR)
    thus ?case by(blast dest: symmetric)
  qed
qed


lemma bangPres:
  fixes P :: pi
  and   Q :: pi

  assumes PBiSimQ: "P ∼ Q"

  shows "!P ∼ !Q"
proof -
  let ?X = "bangRel bisim"
  from PBiSimQ have "(!P, !Q) ∈ ?X" by(rule Rel.BRBang)
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim bP bQ)
    {
      fix P Q
      assume "(P, Q) ∈ ?X"
      hence "P ↝[?X] Q"
      proof(induct)
        fix P Q
        assume "P ∼ Q"
        thus "!P ↝[?X] !Q" using bisimE bisimEqvt
          by(rule Strong_Late_Sim_Pres.bangPres)
      next
        fix P Q R T
        assume RBiSimT: "R ∼ T"
        assume PBangRelQ: "(P, Q) ∈ ?X"
        assume PSimQ: "P ↝[?X] Q"
        from RBiSimT  have "R ↝[bisim] T" by(blast dest: bisimE)
        thus "R ∥ P ↝[?X] T ∥ Q" using PSimQ RBiSimT PBangRelQ Rel.BRPar Rel.BRRes bisimEqvt eqvtBangRel
          by(blast intro: Strong_Late_Sim_Pres.parCompose)
      next
        fix P Q a
        assume "P ↝[?X] Q"
        moreover from eqvtBangRel bisimEqvt have "eqvt ?X" by blast 
        ultimately show "<νa>P ↝[?X] <νa>Q" using Rel.BRRes by(blast intro: Strong_Late_Sim_Pres.resPres)
      qed
      hence "P ↝[((bangRel bisim) ∪ bisim)] Q" by(rule_tac Strong_Late_Sim.monotonic) auto
    }
    with ‹(bP, bQ) ∈ ?X› show ?case by auto
  next
    case(cSym bP bQ)
    thus ?case by(metis bangRelSymetric symmetric)
  qed
qed

end