(* 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