(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Strong_Late_Bisim_SC imports Strong_Late_Bisim_Pres Strong_Late_Sim_SC begin lemma nilBisim[dest]: fixes a :: name and b :: name and x :: name and P :: pi shows "τ.(P) ∼ 𝟬 ⟹ False" and "a<x>.P ∼ 𝟬 ⟹ False" and "a{b}.P ∼ 𝟬 ⟹ False" and "𝟬 ∼ τ.(P) ⟹ False" and "𝟬 ∼ a<x>.P ⟹ False" and "𝟬 ∼ a{b}.P ⟹ False" by(auto dest: bisimE symmetric) (******** Structural Congruence **********) lemma matchId: fixes a :: name and P :: pi shows "[a⌢a]P ∼ P" proof - let ?X = "{([a⌢a]P, P), (P, [a⌢a]P)}" have "([a⌢a]P, P) ∈ ?X" by simp thus ?thesis by(coinduct rule: bisimCoinduct) (auto intro: matchIdLeft matchIdRight reflexive) qed lemma matchNil: fixes a :: name and b :: name assumes "a ≠ b" shows "[a⌢b]P ∼ 𝟬" proof - let ?X = "{([a⌢b]P, 𝟬), (𝟬, [a⌢b]P)}" have "([a⌢b]P, 𝟬) ∈ ?X" by simp thus ?thesis using ‹a ≠ b› by(coinduct rule: bisimCoinduct) (auto intro: matchNilLeft nilSimRight reflexive) qed lemma mismatchId: fixes a :: name and b :: name and P :: pi assumes "a ≠ b" shows "[a≠b]P ∼ P" proof - let ?X = "{([a≠b]P, P), (P, [a≠b]P)}" have "([a≠b]P, P) ∈ ?X" by simp thus ?thesis using ‹a ≠ b› by(coinduct rule: bisimCoinduct) (auto intro: mismatchIdLeft mismatchIdRight reflexive) qed lemma mismatchNil: fixes a :: name and P :: pi shows "[a≠a]P ∼ 𝟬" proof - let ?X = "{([a≠a]P, 𝟬), (𝟬, [a≠a]P)}" have "([a≠a]P, 𝟬) ∈ ?X" by simp thus ?thesis by(coinduct rule: bisimCoinduct) (auto intro: mismatchNilLeft nilSimRight reflexive) qed (******** The ν-operator *****************) lemma nilRes: fixes x :: name shows "<νx>𝟬 ∼ 𝟬" proof - let ?X = "{(<νx>𝟬, 𝟬), (𝟬, <νx>𝟬)}" have "(<νx>𝟬, 𝟬) ∈ ?X" by simp thus ?thesis by(coinduct rule: bisimCoinduct) (auto intro: nilSimRight resNilRight) qed lemma resComm: fixes x :: name and y :: name and P :: pi shows "<νx><νy>P ∼ <νy><νx>P" proof - let ?X = "{(<νx><νy>P, <νy><νx>P) | x y P. True}" have "(<νx><νy>P, <νy><νx>P) ∈ ?X" by auto thus ?thesis proof(coinduct rule: bisimCoinduct) case(cSim xyP yxP) { fix x y P have "⋀x y P. (<νx><νy>P, <νy><νx>P) ∈ ?X ∪ bisim" by auto moreover have "Id ⊆ ?X ∪ bisim" by(auto intro: reflexive) moreover have "eqvt ?X" by(force simp add: eqvt_def) hence "eqvt(?X ∪ bisim)" by auto ultimately have "<νx><νy>P ↝[(?X ∪ bisim)] <νy><νx>P" by(rule resComm) } with ‹(xyP, yxP) ∈ ?X› show ?case by auto next case(cSym xyP yxP) thus ?case by auto qed qed (******** The +-operator *********) lemma sumSym: fixes P :: pi and Q :: pi shows "P ⊕ Q ∼ Q ⊕ P" proof - let ?X = "{(P ⊕ Q, Q ⊕ P), (Q ⊕ P, P ⊕ Q)}" have "(P ⊕ Q, Q ⊕ P) ∈ ?X" by simp thus ?thesis by(coinduct rule: bisimCoinduct) (auto intro: reflexive sumSym) qed lemma sumIdemp: fixes P :: pi shows "P ⊕ P ∼ P" proof - let ?X = "{(P ⊕ P, P), (P, P ⊕ P)}" have "(P ⊕ P, P) ∈ ?X" by simp thus ?thesis by(coinduct rule: bisimCoinduct) (auto intro: reflexive sumIdempLeft sumIdempRight) qed lemma sumAssoc: fixes P :: pi and Q :: pi and R :: pi shows "(P ⊕ Q) ⊕ R ∼ P ⊕ (Q ⊕ R)" proof - let ?X = "{((P ⊕ Q) ⊕ R, P ⊕ (Q ⊕ R)), (P ⊕ (Q ⊕ R), (P ⊕ Q) ⊕ R)}" have "((P ⊕ Q) ⊕ R, P ⊕ (Q ⊕ R)) ∈ ?X" by simp thus ?thesis by(coinduct rule: bisimCoinduct) (auto intro: reflexive sumAssocLeft sumAssocRight) qed lemma sumZero: fixes P :: pi shows "P ⊕ 𝟬 ∼ P" proof - let ?X = "{(P ⊕ 𝟬, P), (P, P ⊕ 𝟬)}" have "(P ⊕ 𝟬, P) ∈ ?X" by simp thus ?thesis by(coinduct rule: bisimCoinduct) (auto intro: reflexive sumZeroLeft sumZeroRight) qed (******** The |-operator *********) lemma parZero: fixes P :: pi shows "P ∥ 𝟬 ∼ P" proof - let ?X = "{(P ∥ 𝟬, P) | P. True} ∪ {(P, P ∥ 𝟬) | P . True}" have "(P ∥ 𝟬, P) ∈ ?X" by blast thus ?thesis by(coinduct rule: bisimCoinduct, auto intro: parZeroRight parZeroLeft) qed lemma parSym: fixes P :: pi and Q :: pi shows "P ∥ Q ∼ Q ∥ P" proof - let ?X = "{(resChain lst (P ∥ Q), resChain lst (Q ∥ P)) | lst P Q. True}" have "(P ∥ Q, Q ∥ P) ∈ ?X" by(blast intro: resChain.base[THEN sym]) thus ?thesis proof(coinduct rule: bisimCoinduct) case(cSim PQ QP) { fix lst P Q have "⋀P Q. (P ∥ Q, Q ∥ P) ∈ ?X ∪ bisim" by(blast intro: resChain.base[THEN sym]) moreover have Res: "⋀x P Q. (P, Q) ∈ ?X ∪ bisim ⟹ (<νx>P, <νx>Q) ∈ ?X ∪ bisim" by(auto intro: resPres resChain.step[THEN sym]) ultimately have "P ∥ Q ↝[(?X ∪ bisim)] Q ∥ P" by(rule parSym) moreover have "eqvt ?X" by(force simp add: eqvt_def) hence "eqvt(?X ∪ bisim)" by auto ultimately have "resChain lst (P ∥ Q) ↝[(?X ∪ bisim)] resChain lst (Q ∥ P)" using Res by(rule resChainI) } with ‹(PQ, QP) ∈ ?X› show ?case by auto next case(cSym PQ QP) thus ?case by auto qed qed lemma scopeExtPar: fixes P :: pi and Q :: pi and x :: name assumes "x ♯ P" shows "<νx>(P ∥ Q) ∼ P ∥ <νx>Q" proof - let ?X = "{(resChain lst (<νx>(P ∥ Q)), resChain lst (P ∥ <νx>Q)) | lst x P Q. x ♯ P} ∪ {(resChain lst (P ∥ <νx>Q), resChain lst (<νx>(P ∥ Q))) | lst x P Q. x ♯ P}" let ?Y = "bisim O (?X ∪ bisim) O bisim" have Res: "⋀P Q x. (P, Q) ∈ ?X ⟹ (<νx>P, <νx>Q) ∈ ?X" by(blast intro: resChain.step[THEN sym]) from ‹x ♯ P› have "(<νx>(P ∥ Q), P ∥ <νx>Q) ∈ ?X" by(blast intro: resChain.base[THEN sym]) moreover have EqvtX: "eqvt ?X" by(fastforce simp add: eqvt_def name_fresh_left name_rev_per) ultimately show ?thesis proof(coinduct rule: bisimTransitiveCoinduct) case(cSim P Q) { fix P Q lst x assume "(x::name) ♯ (P::pi)" moreover have "Id ⊆ ?Y" by(blast intro: reflexive) moreover from ‹eqvt ?X› bisimEqvt have "eqvt ?Y" by blast moreover have "⋀P Q x. x ♯ P ⟹ (<νx>(P ∥ Q), P ∥ <νx>Q) ∈ ?Y" by(blast intro: resChain.base[THEN sym] reflexive) moreover { fix P Q x y have "<νx><νy>(P ∥ Q) ∼ <νy><νx>(P ∥ Q)" by(rule resComm) moreover assume "x ♯ P" hence "(<νx>(P ∥ Q), P ∥ <νx>Q) ∈ ?X" by(fastforce intro: resChain.base[THEN sym]) hence "(<νy><νx>(P ∥ Q), <νy>(P ∥ <νx>Q)) ∈ ?X" by(rule Res) ultimately have "(<νx><νy>(P ∥ Q), <νy>(P ∥ <νx>Q)) ∈ ?Y" by(blast intro: reflexive) } ultimately have "<νx>(P ∥ Q) ↝[?Y] (P ∥ <νx>Q)" by(rule scopeExtParLeft) moreover note ‹eqvt ?Y› moreover from Res have "⋀P Q x. (P, Q) ∈ ?Y ⟹ (<νx>P, <νx>Q) ∈ ?Y" by(blast intro: resChain.step[THEN sym] dest: resPres) ultimately have "resChain lst (<νx>(P ∥ Q)) ↝[?Y] resChain lst (P ∥ <νx>Q)" by(rule resChainI) } moreover { fix P Q lst x assume "(x::name) ♯ (P::pi)" moreover have "Id ⊆ ?Y" by(blast intro: reflexive) moreover from ‹eqvt ?X› bisimEqvt have "eqvt ?Y" by blast moreover have "⋀P Q x. x ♯ P ⟹ (P ∥ <νx>Q, <νx>(P ∥ Q)) ∈ ?Y" by(blast intro: resChain.base[THEN sym] reflexive) moreover { fix P Q x y have "<νy><νx>(P ∥ Q) ∼ <νx><νy>(P ∥ Q)" by(rule resComm) moreover assume "x ♯ P" hence "(P ∥ <νx>Q, <νx>(P ∥ Q)) ∈ ?X" by(fastforce intro: resChain.base[THEN sym]) hence "(<νy>(P ∥ <νx>Q), <νy><νx>(P ∥ Q)) ∈ ?X" by(rule Res) ultimately have "(<νy>(P ∥ <νx>Q), <νx><νy>(P ∥ Q)) ∈ ?Y" by(blast intro: reflexive) } ultimately have "(P ∥ <νx>Q) ↝[?Y] <νx>(P ∥ Q)" by(rule scopeExtParRight) moreover note ‹eqvt ?Y› moreover from Res have "⋀P Q x. (P, Q) ∈ ?Y ⟹ (<νx>P, <νx>Q) ∈ ?Y" by(blast intro: resChain.step[THEN sym] dest: resPres) ultimately have "resChain lst (P ∥ <νx>Q) ↝[?Y] resChain lst (<νx>(P ∥ Q))" by(rule resChainI) } ultimately show ?case using ‹(P, Q) ∈ ?X› by auto next case(cSym P Q) thus ?case by auto (blast dest: symmetric transitive intro: resChain.base[THEN sym] reflexive)+ qed qed lemma scopeExtPar': fixes P :: pi and Q :: pi and x :: name assumes xFreshQ: "x ♯ Q" shows "<νx>(P ∥ Q) ∼ (<νx>P) ∥ Q" proof - have "<νx>(P ∥ Q) ∼ <νx>(Q ∥ P)" proof - have "P ∥ Q ∼ Q ∥ P" by(rule parSym) thus ?thesis by(rule resPres) qed moreover from xFreshQ have "<νx>(Q ∥ P) ∼ Q ∥ (<νx>P)" by(rule scopeExtPar) moreover have "Q ∥ <νx>P ∼ (<νx>P) ∥ Q" by(rule parSym) ultimately show ?thesis by(blast intro: transitive) qed lemma parAssoc: fixes P :: pi and Q :: pi and R :: pi shows "(P ∥ Q) ∥ R ∼ P ∥ (Q ∥ R)" proof - let ?X = "{(resChain lst ((P ∥ Q) ∥ R), resChain lst (P ∥ (Q ∥ R))) | lst P Q R. True}" let ?Y = "bisim O (?X ∪ bisim) O bisim" have ResX: "⋀P Q x. (P, Q) ∈ ?X ⟹ (<νx>P, <νx>Q) ∈ ?X" by(blast intro: resChain.step[symmetric]) hence ResY: "⋀P Q x. (P, Q) ∈ ?Y ⟹ (<νx>P, <νx>Q) ∈ ?Y" by(blast intro: resChain.step[symmetric] dest: resPres) have "((P ∥ Q) ∥ R, P ∥ (Q ∥ R)) ∈ ?X" by(blast intro: resChain.base[symmetric]) moreover have "eqvt ?X" by(fastforce simp add: eqvt_def) ultimately show ?thesis proof(coinduct rule: bisimTransitiveCoinduct) case(cSim P Q) { fix P Q R lst have "⋀P Q R. ((P ∥ Q) ∥ R, P ∥ (Q ∥ R)) ∈ ?Y" by(blast intro: reflexive resChain.base[symmetric]) moreover have "⋀P Q x. (P, Q) ∈ ?Y ⟹ (<νx>P, <νx>Q) ∈ ?Y" by(blast intro: resChain.step[symmetric] resPres) moreover { fix P Q R x have "(<νx>((P ∥ Q) ∥ R), <νx>(P ∥ (Q ∥ R))) ∈ ?X" by(rule_tac ResX) (blast intro: resChain.base[symmetric]) moreover assume "x ♯ P" hence "<νx>(P ∥ (Q ∥ R)) ∼ P ∥ <νx>(Q ∥ R)" by(rule scopeExtPar) ultimately have "(<νx>((P ∥ Q) ∥ R), P ∥ <νx>(Q ∥ R)) ∈ ?Y" by(blast intro: reflexive) } moreover { fix P Q R x have "(<νx>((P ∥ Q) ∥ R), <νx>(P ∥ (Q ∥ R))) ∈ ?X" by(rule_tac ResX) (blast intro: resChain.base[symmetric]) moreover assume "x ♯ R" hence "<νx>(P ∥ Q) ∥ R ∼ <νx>((P ∥ Q) ∥ R)" by(metis scopeExtPar' symmetric) ultimately have "(<νx>(P ∥ Q) ∥ R, <νx>(P ∥ (Q ∥ R))) ∈ ?Y" by(blast intro: reflexive) } ultimately have "(P ∥ Q) ∥ R ↝[?Y] P ∥ (Q ∥ R)" by(rule parAssocLeft) moreover from ‹eqvt ?X› bisimEqvt have "eqvt ?Y" by blast ultimately have "resChain lst ((P ∥ Q) ∥ R) ↝[?Y] resChain lst (P ∥ (Q ∥ R))" using ResY by(rule resChainI) } with ‹(P, Q) ∈ ?X› show ?case by auto next case(cSym P Q) { fix P Q R lst have "P ∥ (Q ∥ R) ∼ (R ∥ Q) ∥ P" by(metis parPres parSym transitive) moreover have "((R ∥ Q) ∥ P, R ∥ (Q ∥ P)) ∈ ?X" by(blast intro: resChain.base[symmetric]) moreover have "R ∥ (Q ∥ P) ∼ (P ∥ Q) ∥ R" by(metis parPres parSym transitive) ultimately have "(P ∥ (Q ∥ R), (P ∥ Q) ∥ R) ∈ ?Y" by blast hence "(resChain lst (P ∥ (Q ∥ R)), resChain lst ((P ∥ Q) ∥ R)) ∈ ?Y" using ResY by(induct lst) auto } with ‹(P, Q) ∈ ?X› show ?case by blast qed qed lemma scopeFresh: fixes x :: name and P :: pi assumes "x ♯ P" shows "<νx>P ∼ P" proof - have "<νx>P ∼ <νx>P ∥ 𝟬" by(rule parZero[THEN symmetric]) moreover have "<νx>P ∥ 𝟬 ∼ 𝟬 ∥ <νx>P" by(rule parSym) moreover have "𝟬 ∥ <νx>P ∼ <νx>(𝟬 ∥ P)" by(rule scopeExtPar[THEN symmetric]) auto moreover have "<νx>(𝟬 ∥ P) ∼ <νx>(P ∥ 𝟬)" by(rule resPres[OF parSym]) moreover from ‹x ♯ P› have "<νx>(P ∥ 𝟬) ∼ P ∥ <νx>𝟬" by(rule scopeExtPar) moreover have "P ∥ <νx>𝟬 ∼ <νx>𝟬 ∥ P" by(rule parSym) moreover have "<νx>𝟬 ∥ P ∼ 𝟬 ∥ P" by(rule parPres[OF nilRes]) moreover have "𝟬 ∥ P ∼ P ∥ 𝟬" by(rule parSym) moreover have "P ∥ 𝟬 ∼ P" by(rule parZero) ultimately show ?thesis by(metis transitive) qed lemma sumRes: fixes x :: name and P :: pi and Q :: pi shows "<νx>(P ⊕ Q) ∼ (<νx>P) ⊕ (<νx>Q)" proof - let ?X = "{(<νx>(P ⊕ Q), <νx>P ⊕ <νx>Q) | x P Q. True} ∪ {(<νx>P ⊕ <νx>Q, <νx>(P ⊕ Q)) | x P Q. True}" have "(<νx>(P ⊕ Q), <νx>P ⊕ <νx>Q) ∈ ?X" by auto moreover have "eqvt ?X" by(fastforce simp add: eqvt_def) ultimately show ?thesis by(coinduct rule: bisimCoinduct) (fastforce intro: sumResLeft sumResRight reflexive)+ qed lemma scopeExtSum: fixes P :: pi and Q :: pi and x :: name assumes "x ♯ P" shows "<νx>(P ⊕ Q) ∼ P ⊕ <νx>Q" proof - have "<νx>(P ⊕ Q) ∼ <νx>P ⊕ <νx>Q" by(rule sumRes) moreover from ‹x ♯ P› have "<νx>P ⊕ <νx>Q ∼ P ⊕ <νx>Q" by(rule sumPres[OF scopeFresh]) ultimately show ?thesis by(rule transitive) qed lemma bangSC: fixes P :: pi shows "!P ∼ P ∥ !P" proof - let ?X = "{(!P, P ∥ !P), (P ∥ !P, !P)}" have "(!P, P ∥ !P) ∈ ?X" by simp thus ?thesis by(coinduct rule: bisimCoinduct) (auto intro: bangLeftSC bangRightSC reflexive) qed lemma resNil: fixes x :: name and y :: name and P :: pi and b :: name shows "<νx>x<y>.P ∼ 𝟬" and "<νx>x{b}.P ∼ 𝟬" proof - let ?X = "{(<νx>x<y>.P, 𝟬), (𝟬, <νx>x<y>.P)}" have "(<νx>x<y>.P, 𝟬) ∈ ?X" by simp thus "<νx>x<y>.P ∼ 𝟬" by(coinduct rule: bisimCoinduct) (auto simp add: simulation_def) next let ?X = "{(<νx>x{b}.P, 𝟬), (𝟬, <νx>x{b}.P)}" have "(<νx>x{b}.P, 𝟬) ∈ ?X" by simp thus "<νx>x{b}.P ∼ 𝟬" by(coinduct rule: bisimCoinduct) (auto simp add: simulation_def) qed lemma resInput: fixes x :: name and a :: name and y :: name and P :: pi assumes "x ≠ a" and "x ≠ y" shows "<νx>a<y>.P ∼ a<y>.(<νx>P)" proof - let ?X = "{(<νx>a<y>.P, a<y>.(<νx>P)) | x a y P. x ≠ a ∧ x ≠ y} ∪ {(a<y>.(<νx>P), <νx>a<y>.P) | x a y P. x ≠ a ∧ x ≠ y}" from assms have "(<νx>a<y>.P, a<y>.(<νx>P)) ∈ ?X" by auto moreover have "eqvt ?X" by(fastforce simp add: eqvt_def pt_bij[OF pt_name_inst, OF at_name_inst]) ultimately show ?thesis by(coinduct rule: bisimCoinduct) (fastforce intro: resInputLeft reflexive resInputRight)+ qed lemma resOutput: fixes x :: name and a :: name and b :: name and P :: pi assumes "x ≠ a" and "x ≠ b" shows "<νx>a{b}.P ∼ a{b}.(<νx>P)" proof - let ?X = "{(<νx>a{b}.P, a{b}.(<νx>P)) | x a b P. x ≠ a ∧ x ≠ b} ∪ {(a{b}.(<νx>P), <νx>a{b}.P) | x a b P. x ≠ a ∧ x ≠ b}" from assms have "(<νx>a{b}.P, a{b}.(<νx>P)) ∈ ?X" by blast moreover have "eqvt ?X" by(fastforce simp add: eqvt_def pt_bij[OF pt_name_inst, OF at_name_inst]) ultimately show ?thesis by(coinduct rule: bisimCoinduct) (fastforce intro: resOutputLeft resOutputRight reflexive)+ qed lemma resTau: fixes x :: name and P :: pi shows "<νx>τ.(P) ∼ τ.(<νx>P)" proof - let ?X = "{(<νx>τ.(P), τ.(<νx>P)), (τ.(<νx>P), <νx>τ.(P))}" have "(<νx>τ.(P), τ.(<νx>P)) ∈ ?X" by auto thus ?thesis by(coinduct rule: bisimCoinduct) (fastforce intro: resTauLeft resTauRight reflexive)+ qed inductive structCong :: "pi ⇒ pi ⇒ bool" (‹_ ≡⇩_{s}_› [70, 70] 70) where Refl: "P ≡⇩_{s}P" | Sym: "P ≡⇩_{s}Q ⟹ Q ≡⇩_{s}P" | Trans: "⟦P ≡⇩_{s}Q; Q ≡⇩_{s}R⟧ ⟹ P ≡⇩_{s}R" | SumComm: "P ⊕ Q ≡⇩_{s}Q ⊕ P" | SumAssoc: "(P ⊕ Q) ⊕ R ≡⇩_{s}P ⊕ (Q ⊕ R)" | SumId: "P ⊕ 𝟬 ≡⇩_{s}P" | ParComm: "P ∥ Q ≡⇩_{s}Q ∥ P" | ParAssoc: "(P ∥ Q) ∥ R ≡⇩_{s}P ∥ (Q ∥ R)" | ParId: "P ∥ 𝟬 ≡⇩_{s}P" | MatchId: "[a⌢a]P ≡⇩_{s}P" | ResNil: "<νx>𝟬 ≡⇩_{s}𝟬" | ResComm: "<νx><νy>P ≡⇩_{s}<νy><νx>P" | ResSum: "<νx>(P ⊕ Q) ≡⇩_{s}<νx>P ⊕ <νx>Q" | ScopeExtPar: "x ♯ P ⟹ <νx>(P ∥ Q) ≡⇩_{s}P ∥ <νx>Q" | InputRes: "⟦x ≠ a; x ≠ y⟧ ⟹ <νx>a<y>.P ≡⇩_{s}a<y>.(<νx>P)" | OutputRes: "⟦x ≠ a; x ≠ b⟧ ⟹ <νx>a{b}.P ≡⇩_{s}a{b}.(<νx>P)" | TauRes: "<νx>τ.(P) ≡⇩_{s}τ.(<νx>P)" | BangUnfold: "!P ≡⇩_{s}P ∥ !P" lemma structCongBisim: fixes P :: pi and Q :: pi assumes "P ≡⇩_{s}Q" shows "P ∼ Q" using assms by(induct rule: structCong.induct) (auto intro: reflexive symmetric transitive sumSym sumAssoc sumZero parSym parAssoc parZero nilRes resComm resInput resOutput resTau sumRes scopeExtPar bangSC matchId mismatchId) end