Theory Strong_Early_Bisim_Pres

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

(************* Preservation rules *************)

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

  assumes "P ∼ Q"

  shows "τ.(P) ∼ τ.(Q)"
proof -
  let ?X = "{(τ.(P), τ.(Q)) | P Q. P ∼ Q}"
  from ‹P ∼ Q› have "(τ.(P), τ.(Q)) ∈ ?X" by auto
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: tauPres dest: bisimE)
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: bisimE)
  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 P Q. P ∼ Q}"
  from ‹P ∼ Q› have "(a{b}.P, a{b}.Q) ∈ ?X" by auto
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (blast intro: outputPres dest: bisimE)+
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 = "{x. ∃P Q a b. P ∼ Q ∧ x = ([a⌢b]P, [a⌢b]Q)}"
  from assms have "([a⌢b]P, [a⌢b]Q) ∈ ?X" by blast
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (blast intro: matchPres dest: 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 = "{x. ∃P Q a b. P ∼ Q ∧ x = ([a≠b]P, [a≠b]Q)}"
  from assms have "([a≠b]P, [a≠b]Q) ∈ ?X" by blast
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (blast intro: mismatchPres dest: 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) | P Q R. P ∼ Q}"
  from assms have "(P ⊕ R, Q ⊕ R) ∈ ?X" by blast
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto dest: bisimE intro: reflexive sumPres)
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 assms have "(<νx>P, <νx>Q) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim xP xQ)
    moreover {
      fix P Q a
      assume "P ∼ Q"
      hence "P ↝[bisim] Q" by(rule bisimE)
      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(rule eqvt)
      moreover have "eqvt (?X ∪ bisim)" using eqvts
        by(auto simp add: eqvt_def) blast
      ultimately have "<νa>P ↝[(?X ∪ bisim)] <νa>Q"
        by(rule Strong_Early_Sim_Pres.resPres)
    }
    ultimately show ?case by auto
  next
    case(cSym xP xQ)
    thus ?case by(auto dest: bisimE)
  qed
qed

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

  assumes "P ∼ Q"

  shows "P ∥ R ∼ Q ∥ R"
proof -
  let ?X = "{(resChain lst (P ∥ R), resChain lst (Q ∥ R)) | lst P Q R. P ∼ Q}"
  have BC: "⋀P Q. P ∥ Q = resChain [] (P ∥ Q)" by auto
  from assms have "(P ∥ R, Q ∥ R) ∈ ?X" by(blast intro: BC)
  thus ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cSim PR QR)
    moreover {
      fix lst P Q R
      assume "P ∼ Q"
      have "eqvt ?X" using eqvts by(auto simp add: eqvt_def) blast
      moreover have Res: "⋀P Q x. (P, Q) ∈ ?X ⟹ (<νx>P, <νx>Q) ∈ ?X"
        by(auto, rule_tac x="x#lst" in exI) auto
      moreover {
        from ‹P ∼ Q› have "P ↝[bisim] Q" by(rule bisimE)
        moreover note ‹P ∼ Q›
        moreover have "⋀P Q R. P ∼ Q ⟹ (P ∥ R, Q ∥ R) ∈ ?X"
          by(blast intro: BC)
        ultimately have "P ∥ R ↝[?X] Q ∥ R" using Res
          by(rule parPres)
      }

      ultimately have "resChain lst (P ∥ R) ↝[?X] resChain lst (Q ∥ R)"
        by(rule resChainI)
    }
    ultimately show ?case by auto
  next
    case(cSym P Q)
    thus ?case by(auto dest: bisimE)
  qed
qed

lemma bangRelBisimE: 
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi × pi) set"

  assumes A:   "(P, Q) ∈ bangRel Rel"
  and     Sym: "⋀P Q. (P, Q) ∈ Rel ⟹ (Q, P) ∈ Rel"

  shows "(Q, P) ∈ bangRel Rel"
proof -
  from A show ?thesis
  proof(induct)
    fix P Q
    assume "(P, Q) ∈ Rel"
    hence "(Q, P) ∈ Rel" by(rule Sym)
    thus "(!Q, !P) ∈ bangRel Rel" by(rule BRBang)
  next
    fix P Q R T
    assume RRelT: "(R, T) ∈ Rel"
    assume IH: "(Q, P) ∈ bangRel Rel"
    from RRelT have "(T, R) ∈ Rel" by(rule Sym)
    thus "(T ∥ Q, R ∥ P) ∈ bangRel Rel" using IH by(rule BRPar)
  next
    fix P Q a
    assume "(Q, P) ∈ bangRel Rel"
    thus "(<νa>Q, <νa>P) ∈ bangRel Rel" by(rule BRRes)
  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 BRBang)
    thus ?thesis
    proof(coinduct rule: bisimWeakCoinduct)
      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(1) eqvt
            by(rule Strong_Early_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 BRPar BRRes eqvt eqvtBangRel
            by(blast intro: Strong_Early_Sim_Pres.parCompose)
        next
          fix P Q a
          assume "P ↝[?X] Q"
          moreover from eqvtBangRel eqvt have "eqvt ?X" by blast 
          ultimately show "<νa>P ↝[?X] <νa>Q" using BRRes by(blast intro: Strong_Early_Sim_Pres.resPres)
        qed
      }
      with ‹(bP, bQ) ∈ ?X› show ?case by blast
    next
      case(cSym bP bQ)
      thus ?case by(metis bangRelSymetric bisimE)
  qed
qed

end