(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Strong_Late_Sim_SC imports Strong_Late_Sim begin (************** Zero **********************) lemma nilSim[dest]: fixes a :: name and b :: name and x :: name and P :: pi and Q :: pi shows "𝟬 ↝[Rel] τ.(P) ⟹ False" and "𝟬 ↝[Rel] a<x>.P ⟹ False" and "𝟬 ↝[Rel] a{b}.P ⟹ False" by(fastforce simp add: simulation_def intro: Tau Input Output)+ lemma nilSimRight: fixes P :: pi and Rel :: "(pi × pi) set" shows "P ↝[Rel] 𝟬" by(auto simp add: simulation_def) (************** Match *********************) lemma matchIdLeft: fixes a :: name and P :: pi and Rel :: "(pi × pi) set" assumes "Id ⊆ Rel" shows "[a⌢a]P ↝[Rel] P" using assms by(force simp add: simulation_def dest: Match derivativeReflexive) lemma matchIdRight: fixes P :: pi and a :: name and Rel :: "(pi × pi) set" assumes IdRel: "Id ⊆ Rel" shows "P ↝[Rel] [a⌢a]P" using assms by(fastforce simp add: simulation_def elim: matchCases intro: derivativeReflexive) lemma matchNilLeft: fixes a :: name and b :: name and P :: pi assumes "a ≠ b" shows "𝟬 ↝[Rel] [a⌢b]P" using assms by(auto simp add: simulation_def) (************** Mismatch *********************) lemma mismatchIdLeft: fixes a :: name and b :: name and P :: pi and Rel :: "(pi × pi) set" assumes "Id ⊆ Rel" and "a ≠ b" shows "[a≠b]P ↝[Rel] P" using assms by(fastforce simp add: simulation_def intro: Mismatch dest: derivativeReflexive) lemma mismatchIdRight: fixes P :: pi and a :: name and b :: name and Rel :: "(pi × pi) set" assumes IdRel: "Id ⊆ Rel" and aineqb: "a ≠ b" shows "P ↝[Rel] [a≠b]P" using assms by(fastforce simp add: simulation_def elim: mismatchCases intro: derivativeReflexive) lemma mismatchNilLeft: fixes a :: name and P :: pi shows "𝟬 ↝[Rel] [a≠a]P" by(auto simp add: simulation_def) (************** +-operator *****************) lemma sumSym: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" assumes Id: "Id ⊆ Rel" shows "P ⊕ Q ↝[Rel] Q ⊕ P" using assms by(fastforce simp add: simulation_def elim: sumCases intro: Sum1 Sum2 derivativeReflexive) lemma sumIdempLeft: fixes P :: pi and Rel :: "(pi × pi) set" assumes "Id ⊆ Rel" shows "P ↝[Rel] P ⊕ P" using assms by(fastforce simp add: simulation_def elim: sumCases intro: derivativeReflexive) lemma sumIdempRight: fixes P :: pi and Rel :: "(pi × pi) set" assumes I: "Id ⊆ Rel" shows "P ⊕ P ↝[Rel] P" using assms by(fastforce simp add: simulation_def intro: Sum1 derivativeReflexive) lemma sumAssocLeft: fixes P :: pi and Q :: pi and R :: pi and Rel :: "(pi × pi) set" assumes Id: "Id ⊆ Rel" shows "(P ⊕ Q) ⊕ R ↝[Rel] P ⊕ (Q ⊕ R)" using assms by(fastforce simp add: simulation_def elim: sumCases intro: Sum1 Sum2 derivativeReflexive) lemma sumAssocRight: fixes P :: pi and Q :: pi and R :: pi and Rel :: "(pi × pi) set" assumes Id: "Id ⊆ Rel" shows "P ⊕ (Q ⊕ R) ↝[Rel] (P ⊕ Q) ⊕ R" using assms by(fastforce simp add: simulation_def elim: sumCases intro: Sum1 Sum2 derivativeReflexive) lemma sumZeroLeft: fixes P :: pi and Rel :: "(pi × pi) set" assumes Id: "Id ⊆ Rel" shows "P ⊕ 𝟬 ↝[Rel] P" using assms by(fastforce simp add: simulation_def intro: Sum1 derivativeReflexive) lemma sumZeroRight: fixes P :: pi and Rel :: "(pi × pi) set" assumes Id: "Id ⊆ Rel" shows "P ↝[Rel] P ⊕ 𝟬" using assms by(fastforce simp add: simulation_def elim: sumCases intro: derivativeReflexive) lemma sumResLeft: fixes x :: name and P :: pi and Q :: pi assumes Id: "Id ⊆ Rel" and Eqvt: "eqvt Rel" shows "(<νx>P) ⊕ (<νx>Q) ↝[Rel] <νx>(P ⊕ Q)" using Eqvt proof(induct rule: simCasesCont[where C="(x, P, Q)"]) case(Bound a y PQ) from ‹y ♯ (x, P, Q)› have "y ≠ x" and "y ♯ P" and "y ♯ Q" by(simp add: fresh_prod)+ hence "y ♯ P ⊕ Q" by simp with ‹<νx>(P ⊕ Q) ⟼a«y» ≺ PQ› ‹y ≠ x› show ?case proof(induct rule: resCasesB) case(cOpen a PQ) from ‹P ⊕ Q ⟼a[x] ≺ PQ› ‹y ♯ P› ‹y ♯ Q› have "y ♯ PQ" by(force dest: freshFreeDerivative) from ‹P ⊕ Q ⟼a[x] ≺ PQ› show ?case proof(induct rule: sumCases) case cSum1 from ‹P ⟼a[x] ≺ PQ› ‹a ≠ x› have "<νx>P ⟼a<νx> ≺ PQ" by(rule Open) hence "(<νx>P) ⊕ (<νx>Q) ⟼a<νx> ≺ PQ" by(rule Sum1) with ‹y ♯ PQ› have "(<νx>P) ⊕ (<νx>Q) ⟼a<νy> ≺ ([(y, x)] ∙ PQ)" by(simp add: alphaBoundResidual) moreover from Id have "derivative ([(y, x)] ∙ PQ) ([(y, x)] ∙ PQ) (BoundOutputS a) y Rel" by(force simp add: derivative_def) ultimately show ?case by blast next case cSum2 from ‹Q ⟼a[x] ≺ PQ› ‹a ≠ x› have "<νx>Q ⟼a<νx> ≺ PQ" by(rule Open) hence "(<νx>P) ⊕ (<νx>Q) ⟼a<νx> ≺ PQ" by(rule Sum2) with ‹y ♯ PQ› have "(<νx>P) ⊕ (<νx>Q) ⟼a<νy> ≺ ([(y, x)] ∙ PQ)" by(simp add: alphaBoundResidual) moreover from Id have "derivative ([(y, x)] ∙ PQ) ([(y, x)] ∙ PQ) (BoundOutputS a) y Rel" by(force simp add: derivative_def) ultimately show ?case by blast qed next case(cRes PQ) from ‹P ⊕ Q ⟼a«y» ≺ PQ› show ?case proof(induct rule: sumCases) case cSum1 from ‹P ⟼a«y» ≺ PQ› ‹x ♯ a› ‹y ≠ x› have "<νx>P ⟼a«y» ≺ <νx>PQ" by(rule_tac ResB) auto hence "(<νx>P) ⊕ (<νx>Q) ⟼a«y» ≺ <νx>PQ" by(rule Sum1) moreover from Id have "derivative (<νx>PQ) (<νx>PQ) a y Rel" by(cases a) (auto simp add: derivative_def) ultimately show ?case by blast next case cSum2 from ‹Q ⟼a«y» ≺ PQ› ‹x ♯ a› ‹y ≠ x› have "<νx>Q ⟼a«y» ≺ <νx>PQ" by(rule_tac ResB) auto hence "(<νx>P) ⊕ (<νx>Q) ⟼a«y» ≺ <νx>PQ" by(rule Sum2) moreover from Id have "derivative (<νx>PQ) (<νx>PQ) a y Rel" by(cases a) (auto simp add: derivative_def) ultimately show ?case by blast qed qed next case(Free α PQ) from ‹<νx>(P ⊕ Q) ⟼α ≺ PQ› show ?case proof(induct rule: resCasesF) case(cRes PQ) from ‹P ⊕ Q ⟼α ≺ PQ› show ?case proof(induct rule: sumCases) case cSum1 from ‹P ⟼α ≺ PQ› ‹x ♯ α› have "<νx>P ⟼α ≺ <νx>PQ" by(rule ResF) hence "(<νx>P) ⊕ (<νx>Q) ⟼α ≺ <νx>PQ" by(rule Sum1) with Id show ?case by blast next case cSum2 from ‹Q ⟼α ≺ PQ› ‹x ♯ α› have "<νx>Q ⟼α ≺ <νx>PQ" by(rule ResF) hence "(<νx>P) ⊕ (<νx>Q) ⟼α ≺ <νx>PQ" by(rule Sum2) with Id show ?case by blast qed qed qed lemma sumResRight: fixes x :: name and P :: pi and Q :: pi assumes Id: "Id ⊆ Rel" and Eqvt: "eqvt Rel" shows "<νx>(P ⊕ Q) ↝[Rel] (<νx>P) ⊕ (<νx>Q)" using ‹eqvt Rel› proof(induct rule: simCasesCont[where C="(x, P, Q)"]) case(Bound a y PQ) from ‹y ♯ (x, P, Q)› have "y ≠ x" and "y ♯ P" and "y ♯ Q" by(simp add: fresh_prod)+ from ‹(<νx>P) ⊕ (<νx>Q) ⟼a«y» ≺ PQ› show ?case proof(induct rule: sumCases) case cSum1 from ‹<νx>P ⟼a«y» ≺ PQ› show ?case using ‹y ≠ x› ‹y ♯ P› proof(induct rule: resCasesB) case(cOpen a P') from ‹P ⟼a[x] ≺ P'› ‹y ♯ P› have "y ♯ P'" by(rule freshFreeDerivative) from ‹P ⟼a[x] ≺ P'› have "P ⊕ Q ⟼a[x] ≺ P'" by(rule Sum1) hence "<νx>(P ⊕ Q) ⟼a<νx> ≺ P'" using ‹a ≠ x› by(rule Open) with ‹y ♯ P'› have "<νx>(P ⊕ Q) ⟼a<νy> ≺ [(y, x)] ∙ P'" by(simp add: alphaBoundResidual) moreover from Id have "derivative ([(y, x)] ∙ P') ([(y, x)] ∙ P') (BoundOutputS a) y Rel" by(force simp add: derivative_def) ultimately show ?case by blast next case(cRes P') from ‹P ⟼a«y» ≺ P'› have "P ⊕ Q ⟼a«y» ≺ P'" by(rule Sum1) hence "<νx>(P ⊕ Q) ⟼a«y» ≺ <νx>P'" using ‹x ♯ a› ‹y ≠ x› by(rule_tac ResB) auto moreover from Id have "derivative (<νx>P') (<νx>P') a y Rel" by(cases a) (auto simp add: derivative_def) ultimately show ?case by blast qed next case cSum2 from ‹<νx>Q ⟼a«y» ≺ PQ› show ?case using ‹y ≠ x› ‹y ♯ Q› proof(induct rule: resCasesB) case(cOpen a Q') from ‹Q ⟼a[x] ≺ Q'› ‹y ♯ Q› have "y ♯ Q'" by(rule freshFreeDerivative) from ‹Q ⟼a[x] ≺ Q'› have "P ⊕ Q ⟼a[x] ≺ Q'" by(rule Sum2) hence "<νx>(P ⊕ Q) ⟼a<νx> ≺ Q'" using ‹a ≠ x› by(rule Open) with ‹y ♯ Q'› have "<νx>(P ⊕ Q) ⟼a<νy> ≺ [(y, x)] ∙ Q'" by(simp add: alphaBoundResidual) moreover from Id have "derivative ([(y, x)] ∙ Q') ([(y, x)] ∙ Q') (BoundOutputS a) y Rel" by(force simp add: derivative_def) ultimately show ?case by blast next case(cRes Q') from ‹Q ⟼a«y» ≺ Q'› have "P ⊕ Q ⟼a«y» ≺ Q'" by(rule Sum2) hence "<νx>(P ⊕ Q) ⟼a«y» ≺ <νx>Q'" using ‹x ♯ a› ‹y ≠ x› by(rule_tac ResB) auto moreover from Id have "derivative (<νx>Q') (<νx>Q') a y Rel" by(cases a) (auto simp add: derivative_def) ultimately show ?case by blast qed qed next case(Free α PQ) from ‹(<νx>P) ⊕ (<νx>Q) ⟼α ≺ PQ› show ?case proof(induct rule: sumCases) case cSum1 from ‹<νx>P ⟼α ≺ PQ› show ?case proof(induct rule: resCasesF) case(cRes P') from ‹P ⟼α ≺ P'› have "P ⊕ Q ⟼α ≺ P'" by(rule Sum1) hence "<νx>(P ⊕ Q) ⟼α ≺ <νx>P'" using ‹x ♯ α› by(rule ResF) with Id show ?case by blast qed next case cSum2 from ‹<νx>Q ⟼α ≺ PQ› show ?case proof(induct rule: resCasesF) case(cRes Q') from ‹Q ⟼α ≺ Q'› have "P ⊕ Q ⟼α ≺ Q'" by(rule Sum2) hence "<νx>(P ⊕ Q) ⟼α ≺ <νx>Q'" using ‹x ♯ α› by(rule ResF) with Id show ?case by blast qed qed qed (************** |-operator *************) lemma parZeroLeft: fixes P :: pi and Rel :: "(pi × pi) set" assumes ParZero: "⋀Q. (Q ∥ 𝟬, Q) ∈ Rel" shows "P ∥ 𝟬 ↝[Rel] P" proof - { fix P Q a x from ParZero have "derivative (P ∥ 𝟬) P a x Rel" by(case_tac a) (auto simp add: derivative_def) } thus ?thesis using assms by(fastforce simp add: simulation_def intro: Par1B Par1F) qed lemma parZeroRight: fixes P :: pi and Rel :: "(pi × pi) set" assumes ParZero: "⋀Q. (Q, Q ∥ 𝟬) ∈ Rel" shows "P ↝[Rel] P ∥ 𝟬" proof - { fix P Q a x from ParZero have "derivative P (P ∥ 𝟬) a x Rel" by(case_tac a) (auto simp add: derivative_def) } thus ?thesis using assms by(fastforce simp add: simulation_def elim: parCasesF parCasesB)+ qed lemma parSym: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" assumes Sym: "⋀R S. (R ∥ S, S ∥ R) ∈ Rel" and Res: "⋀R S x. (R, S) ∈ Rel ⟹ (<νx>R, <νx>S) ∈ Rel" shows "P ∥ Q ↝[Rel] Q ∥ P" proof(induct rule: simCases) case(Bound a x QP) from ‹x ♯ (P ∥ Q)› have "x ♯ Q" and "x ♯ P" by simp+ with ‹Q ∥ P ⟼ a«x» ≺ QP› show ?case proof(induct rule: parCasesB) case(cPar1 Q') from ‹Q ⟼a«x» ≺ Q'› have "P ∥ Q ⟼a«x» ≺ P ∥ Q'" using ‹x ♯ P› by(rule Par2B) moreover have "derivative (P ∥ Q') (Q' ∥ P) a x Rel" by(cases a, auto simp add: derivative_def intro: Sym) ultimately show ?case by blast next case(cPar2 P') from ‹P ⟼a«x» ≺ P'› have "P ∥ Q ⟼a«x» ≺ P' ∥ Q" using ‹x ♯ Q› by(rule Par1B) moreover have "derivative (P' ∥ Q) (Q ∥ P') a x Rel" by(cases a, auto simp add: derivative_def intro: Sym) ultimately show ?case by blast qed next case(Free α QP) from ‹Q ∥ P ⟼ α ≺ QP› show ?case proof(induct rule: parCasesF[where C="()"]) case(cPar1 Q') from ‹Q ⟼ α ≺ Q'› have "P ∥ Q ⟼ α ≺ P ∥ Q'" by(rule Par2F) moreover have "(P ∥ Q', Q' ∥ P) ∈ Rel" by(rule Sym) ultimately show ?case by blast next case(cPar2 P') from ‹P ⟼ α ≺ P'› have "P ∥ Q ⟼ α ≺ P' ∥ Q" by(rule Par1F) moreover have "(P' ∥ Q, Q ∥ P') ∈ Rel" by(rule Sym) ultimately show ?case by blast next case(cComm1 Q' P' a b x) from ‹P ⟼a[b] ≺ P'› ‹Q ⟼a<x> ≺ Q'› have "P ∥ Q ⟼ τ ≺ P' ∥ (Q'[x::=b])" by(rule Comm2) moreover have "(P' ∥ Q'[x::=b], Q'[x::=b] ∥ P') ∈ Rel" by(rule Sym) ultimately show ?case by blast next case(cComm2 Q' P' a b x) from ‹P ⟼a<x> ≺ P'› ‹Q ⟼a[b] ≺ Q'› have "P ∥ Q ⟼ τ ≺ (P'[x::=b]) ∥ Q'" by(rule Comm1) moreover have "(P'[x::=b] ∥ Q', Q' ∥ P'[x::=b]) ∈ Rel" by(rule Sym) ultimately show ?case by blast next case(cClose1 Q' P' a x y) from ‹P ⟼ a<νy> ≺ P'› ‹Q ⟼ a<x> ≺ Q'› ‹y ♯ Q› have "P ∥ Q ⟼ τ ≺ <νy>(P' ∥ (Q'[x::=y]))" by(rule Close2) moreover have "(<νy>(P' ∥ Q'[x::=y]), <νy>(Q'[x::=y] ∥ P')) ∈ Rel" by(metis Res Sym) ultimately show ?case by blast next case(cClose2 Q' P' a x y) from ‹P ⟼ a<x> ≺ P'› ‹Q ⟼ a<νy> ≺ Q'› ‹y ♯ P› have "P ∥ Q ⟼ τ ≺ <νy>((P'[x::=y]) ∥ Q')" by(rule Close1) moreover have "(<νy>(P'[x::=y] ∥ Q'), <νy>(Q' ∥ P'[x::=y])) ∈ Rel" by(metis Res Sym) ultimately show ?case by blast qed qed lemma parAssocLeft: fixes P :: pi and Q :: pi and R :: pi and Rel :: "(pi × pi) set" assumes Ass: "⋀S T U. ((S ∥ T) ∥ U, S ∥ (T ∥ U)) ∈ Rel" and Res: "⋀S T x. (S, T) ∈ Rel ⟹ (<νx>S, <νx>T) ∈ Rel" and FreshExt: "⋀S T U x. x ♯ S ⟹ (<νx>((S ∥ T) ∥ U), S ∥ <νx>(T ∥ U)) ∈ Rel" and FreshExt': "⋀S T U x. x ♯ U ⟹ ((<νx>(S ∥ T)) ∥ U, <νx>(S ∥ (T ∥ U))) ∈ Rel" shows "(P ∥ Q) ∥ R ↝[Rel] P ∥ (Q ∥ R)" proof(induct rule: simCases) case(Bound a x PQR) from ‹x ♯ (P ∥ Q) ∥ R› have "x ♯ P" and "x ♯ Q" and "x ♯ R" by simp+ hence "x ♯ (Q ∥ R)" by simp with ‹P ∥ (Q ∥ R) ⟼ a«x» ≺ PQR› ‹x ♯ P› show ?case proof(induct rule: parCasesB) case(cPar1 P') from ‹P ⟼ a«x» ≺ P'› have "P ∥ Q ⟼ a«x» ≺ P' ∥ Q" using ‹x ♯ Q› by(rule Par1B) hence "(P ∥ Q) ∥ R ⟼ a«x» ≺ (P' ∥ Q) ∥ R" using ‹x ♯ R› by(rule Par1B) moreover have "derivative ((P' ∥ Q) ∥ R) (P' ∥ (Q ∥ R)) a x Rel" by(cases a, auto intro: Ass simp add: derivative_def) ultimately show ?case by blast next case(cPar2 QR) from ‹Q ∥ R ⟼ a«x» ≺ QR› ‹x ♯ Q› ‹x ♯ R› show ?case proof(induct rule: parCasesB) case(cPar1 Q') from ‹Q ⟼ a«x» ≺ Q'› have "P ∥ Q ⟼ a«x» ≺ P ∥ Q'" using ‹x ♯ P› by(rule Par2B) hence "(P ∥ Q) ∥ R ⟼ a«x» ≺ (P ∥ Q') ∥ R" using ‹x ♯ R›by(rule Par1B) moreover have "derivative ((P ∥ Q') ∥ R) (P ∥ (Q' ∥ R)) a x Rel" by(cases a, auto intro: Ass simp add: derivative_def) ultimately show ?case by blast next case(cPar2 R') from ‹R ⟼ a«x» ≺ R'› have "(P ∥ Q) ∥ R ⟼ a«x» ≺ (P ∥ Q) ∥ R'" using ‹x ♯ P› ‹x ♯ Q› by(rule_tac Par2B) auto moreover have "derivative ((P ∥ Q) ∥ R') (P ∥ (Q ∥ R')) a x Rel" by(cases a, auto intro: Ass simp add: derivative_def) ultimately show ?case by blast qed qed next case(Free α PQR) from ‹P ∥ (Q ∥ R) ⟼ α ≺ PQR› show ?case proof(induct rule: parCasesF[where C="Q"]) case(cPar1 P') from ‹P ⟼ α ≺ P'› have "P ∥ Q ⟼ α ≺ P' ∥ Q" by(rule Par1F) hence "(P ∥ Q) ∥ R ⟼ α ≺ (P' ∥ Q) ∥ R" by(rule Par1F) moreover from Ass have "((P' ∥ Q) ∥ R, P' ∥ (Q ∥ R)) ∈ Rel" by blast ultimately show ?case by blast next case(cPar2 QR) from ‹Q ∥ R ⟼ α ≺ QR› show ?case proof(induct rule: parCasesF[where C="P"]) case(cPar1 Q') from ‹Q ⟼ α ≺ Q'› have "(P ∥ Q) ⟼ α ≺ P ∥ Q'" by(rule Par2F) hence "(P ∥ Q) ∥ R ⟼ α ≺ (P ∥ Q') ∥ R" by(rule Par1F) moreover from Ass have "((P ∥ Q') ∥ R, P ∥ (Q' ∥ R)) ∈ Rel" by blast ultimately show ?case by blast next case(cPar2 R') from ‹R ⟼ α ≺ R'› have "(P ∥ Q) ∥ R ⟼ α ≺ (P ∥ Q) ∥ R'" by(rule Par2F) moreover from Ass have "((P ∥ Q) ∥ R', P ∥ (Q ∥ R')) ∈ Rel" by blast ultimately show ?case by blast next case(cComm1 Q' R' a b x) from ‹Q ⟼a<x> ≺ Q'› ‹x ♯ P› have "P ∥ Q ⟼a<x> ≺ P ∥ Q'" by(rule Par2B) hence "(P ∥ Q) ∥ R ⟼ τ ≺ (P ∥ Q')[x::=b] ∥ R'" using ‹R ⟼a[b] ≺ R'› by(rule Comm1) with ‹x ♯ P› have "(P ∥ Q) ∥ R ⟼ τ ≺ (P ∥ (Q'[x::=b])) ∥ R'" by(simp add: forget) moreover from Ass have "((P ∥ (Q'[x::=b])) ∥ R', P ∥ (Q'[x::=b] ∥ R')) ∈ Rel" by blast ultimately show ?case by blast next case(cComm2 Q' R' a b x) from ‹Q ⟼a[b] ≺ Q'› have "P ∥ Q ⟼a[b] ≺ P ∥ Q'" by(rule Par2F) with ‹x ♯ P› ‹x ♯ Q› ‹R ⟼a<x> ≺ R'› have "(P ∥ Q) ∥ R ⟼ τ ≺ (P ∥ Q') ∥ R'[x::=b]" by(force intro: Comm2) moreover from Ass have "((P ∥ Q') ∥ R'[x::=b], P ∥ (Q' ∥ R'[x::=b])) ∈ Rel" by blast ultimately show ?case by blast next case(cClose1 Q' R' a x y) from ‹Q ⟼a<x> ≺ Q'› ‹x ♯ P› have "P ∥ Q ⟼a<x> ≺ P ∥ Q'" by(rule Par2B) with ‹y ♯ P› ‹y ♯ Q› ‹x ♯ P› ‹R ⟼a<νy> ≺ R'› have "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P ∥ Q')[x::=y] ∥ R')" by(rule_tac Close1) auto with ‹x ♯ P› have "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P ∥ (Q'[x::=y])) ∥ R')" by(simp add: forget) moreover from ‹y ♯ P› have "(<νy>((P ∥ Q'[x::=y]) ∥ R'), P ∥ <νy>(Q'[x::=y] ∥ R')) ∈ Rel" by(rule FreshExt) ultimately show ?case by blast next case(cClose2 Q' R' a x y) from ‹Q ⟼a<νy> ≺ Q'› ‹y ♯ P› have "P ∥ Q ⟼a<νy> ≺ P ∥ Q'" by(rule Par2B) hence Act: "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P ∥ Q') ∥ R'[x::=y])" using ‹R ⟼a<x> ≺ R'› ‹y ♯ R› by(rule Close2) moreover from ‹y ♯ P› have "(<νy>((P ∥ Q') ∥ R'[x::=y]), P ∥ <νy>(Q' ∥ R'[x::=y])) ∈ Rel" by(rule FreshExt) ultimately show ?case by blast qed next case(cComm1 P' QR a b x) from ‹Q ∥ R ⟼ a[b] ≺ QR› show ?case proof(induct rule: parCasesF[where C="()"]) case(cPar1 Q') from ‹P ⟼a<x> ≺ P'› ‹Q ⟼a[b] ≺ Q'› have "P ∥ Q ⟼ τ ≺ P'[x::=b] ∥ Q'" by(rule Comm1) hence "(P ∥ Q) ∥ R ⟼ τ ≺ (P'[x::=b] ∥ Q') ∥ R" by(rule Par1F) moreover from Ass have "((P'[x::=b] ∥ Q') ∥ R, P'[x::=b] ∥ (Q' ∥ R)) ∈ Rel" by blast ultimately show ?case by blast next case(cPar2 R') from ‹P ⟼a<x> ≺ P'› ‹x ♯ Q› have "P ∥ Q ⟼ a<x> ≺ P' ∥ Q" by(rule Par1B) hence "(P ∥ Q) ∥ R ⟼ τ ≺ (P' ∥ Q)[x::=b] ∥ R'" using ‹R ⟼ a[b] ≺ R'› by(rule Comm1) with ‹x ♯ Q› have "(P ∥ Q) ∥ R ⟼ τ ≺ (P'[x::=b] ∥ Q) ∥ R'" by(simp add: forget) moreover from Ass have "((P'[x::=b] ∥ Q) ∥ R', P'[x::=b] ∥ (Q ∥ R')) ∈ Rel" by blast ultimately show ?case by blast next case(cComm1 Q' R') from ‹a[b] = τ› have False by simp thus ?case by simp next case(cComm2 Q' R') from ‹a[b] = τ› have False by simp thus ?case by simp next case(cClose1 Q' R') from ‹a[b] = τ› have False by simp thus ?case by simp next case(cClose2 Q' R') from ‹a[b] = τ› have False by simp thus ?case by simp qed next case(cComm2 P' QR a b x) from ‹x ♯ Q ∥ R› have "x ♯ Q" and "x ♯ R" by simp+ with ‹Q ∥ R ⟼ a<x> ≺ QR› show ?case proof(induct rule: parCasesB) case(cPar1 Q') from ‹P ⟼a[b] ≺ P'› ‹Q ⟼ a<x> ≺ Q'› have "P ∥ Q ⟼ τ ≺ P' ∥ (Q'[x::=b])" by(rule Comm2) hence "(P ∥ Q) ∥ R ⟼ τ ≺ (P' ∥ Q'[x::=b]) ∥ R" by(rule Par1F) moreover from Ass have "((P' ∥ Q'[x::=b]) ∥ R, P' ∥ Q'[x::=b] ∥ R) ∈ Rel" by blast with ‹x ♯ R› have "((P' ∥ Q'[x::=b]) ∥ R, P' ∥ (Q' ∥ R)[x::=b]) ∈ Rel" by(force simp add: forget) ultimately show ?case by blast next case(cPar2 R') from ‹P ⟼a[b] ≺ P'› have "P ∥ Q ⟼ a[b] ≺ P' ∥ Q" by(rule Par1F) hence "(P ∥ Q) ∥ R ⟼ τ ≺ (P' ∥ Q) ∥ (R'[x::=b])" using ‹R ⟼a<x> ≺ R'› by (rule Comm2) moreover from Ass have "((P' ∥ Q) ∥ R'[x::=b], P' ∥ Q ∥ (R'[x::=b])) ∈ Rel" by blast hence "((P' ∥ Q) ∥ R'[x::=b], P' ∥ (Q ∥ R')[x::=b]) ∈ Rel" using ‹x ♯ Q› by(force simp add: forget) ultimately show ?case by blast qed next case(cClose1 P' QR a x y) from ‹x ♯ Q ∥ R› have "x ♯ Q" by simp from ‹y ♯ Q ∥ R› have "y ♯ Q" and "y ♯ R" by simp+ from ‹Q ∥ R ⟼ a<νy> ≺ QR› ‹y ♯ Q› ‹y ♯ R› show ?case proof(induct rule: parCasesB) case(cPar1 Q') from ‹P ⟼a<x> ≺ P'› ‹Q ⟼ a<νy> ≺ Q'› ‹y ♯ P› have "P ∥ Q ⟼ τ ≺ <νy>(P'[x::=y] ∥ Q')" by(rule Close1) hence "(P ∥ Q) ∥ R ⟼ τ ≺ (<νy>(P'[x::=y] ∥ Q')) ∥ R" by(rule Par1F) moreover from ‹y ♯ R› have "((<νy>(P'[x::=y] ∥ Q')) ∥ R, <νy>(P'[x::=y] ∥ Q' ∥ R)) ∈ Rel" by(rule FreshExt') ultimately show ?case by blast next case(cPar2 R') from ‹P ⟼a<x> ≺ P'› ‹x ♯ Q› have "P ∥ Q ⟼ a<x> ≺ P' ∥ Q" by(rule Par1B) with ‹R ⟼ a<νy> ≺ R'› ‹y ♯ P› ‹y ♯ Q› have "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P' ∥ Q)[x::=y] ∥ R')" by(rule_tac Close1) auto with ‹x ♯ Q› have "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P'[x::=y] ∥ Q) ∥ R')" by(simp add: forget) moreover have "(<νy>((P'[x::=y] ∥ Q) ∥ R'), <νy>(P'[x::=y] ∥ (Q ∥ R'))) ∈ Rel" by(metis Ass Res) ultimately show ?case by blast qed next case(cClose2 P' QR a x y) from ‹y ♯ Q ∥ R› have "y ♯ Q" and "y ♯ R" by simp+ from ‹x ♯ Q ∥ R› have "x ♯ Q" and "x ♯ R" by simp+ with ‹Q ∥ R ⟼ a<x> ≺ QR› show ?case proof(induct rule: parCasesB) case(cPar1 Q') from ‹P ⟼a<νy> ≺ P'› ‹Q ⟼a<x> ≺ Q'› have "P ∥ Q ⟼ τ ≺ <νy>(P' ∥ Q'[x::=y])" using ‹y ♯ Q› by(rule Close2) hence "(P ∥ Q) ∥ R ⟼ τ ≺ (<νy>(P' ∥ Q'[x::=y])) ∥ R" by(rule Par1F) moreover from ‹y ♯ R› have "((<νy>(P' ∥ Q'[x::=y])) ∥ R, <νy>(P' ∥ (Q'[x::=y] ∥ R))) ∈ Rel" by(rule FreshExt') with ‹x ♯ R› have "((<νy>(P' ∥ Q'[x::=y])) ∥ R, <νy>(P' ∥ (Q' ∥ R)[x::=y])) ∈ Rel" by(simp add: forget) ultimately show ?case by blast next case(cPar2 R') from ‹P ⟼a<νy> ≺ P'› ‹y ♯ Q› have "P ∥ Q ⟼ a<νy> ≺ P' ∥ Q" by(rule Par1B) hence "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P' ∥ Q) ∥ R'[x::=y])" using ‹R ⟼ a<x> ≺ R'› ‹y ♯ R› by(rule Close2) moreover have "((P' ∥ Q) ∥ R'[x::=y], P' ∥ (Q ∥ R'[x::=y])) ∈ Rel" by(rule Ass) hence "(<νy>((P' ∥ Q) ∥ R'[x::=y]), <νy>(P' ∥ (Q ∥ R'[x::=y]))) ∈ Rel" by(rule Res) hence "(<νy>((P' ∥ Q) ∥ R'[x::=y]), <νy>(P' ∥ (Q ∥ R')[x::=y])) ∈ Rel" using ‹x ♯ Q› by(simp add: forget) ultimately show ?case by blast qed qed qed lemma substRes3: fixes a :: name and P :: pi and x :: name shows "(<νa>P)[x::=a] = <νx>([(x, a)] ∙ P)" proof - have "a ♯ <νa>P" by(simp add: name_fresh_abs) hence "(<νa>P)[x::=a] = [(x, a)] ∙ <νa>P" by(rule injPermSubst[THEN sym]) thus "(<νa>P)[x::=a] = <νx>([(x, a)] ∙ P)" by(simp add: name_calc) qed lemma scopeExtParLeft: fixes P :: pi and Q :: pi and a :: name and lst :: "name list" and Rel :: "(pi × pi) set" assumes "x ♯ P" and Id: "Id ⊆ Rel" and EqvtRel: "eqvt Rel" and Res: "⋀R S y. y ♯ R ⟹ (<νy>(R ∥ S), R ∥ <νy>S) ∈ Rel" and ScopeExt: "⋀R S y z. y ♯ R ⟹ (<νy><νz>(R ∥ S), <νz>(R ∥ <νy>S)) ∈ Rel" shows "<νx>(P ∥ Q) ↝[Rel] P ∥ <νx>Q" using ‹eqvt Rel› proof(induct rule: simCasesCont[where C="(x, P, Q)"]) case(Bound a y PxQ) from ‹y ♯ (x, P, Q)› have "y ≠ x" and "y ♯ P" and "y ♯ Q" by simp+ hence "y ♯ P" and "y ♯ <νx>Q" by(simp add: abs_fresh)+ with ‹P ∥ <νx>Q ⟼ a«y» ≺ PxQ› show ?case proof(induct rule: parCasesB) case(cPar1 P') from ‹P ⟼a«y» ≺ P'› ‹x ♯ P› ‹y ≠ x› have "x ♯ a" and "x ♯ P'" by(force intro: freshBoundDerivative)+ from ‹P ⟼a«y» ≺ P'› ‹y ♯ Q› have "P ∥ Q ⟼a«y» ≺ P' ∥ Q" by(rule Par1B) with ‹x ♯ a› ‹y ≠ x› have "<νx>(P ∥ Q) ⟼ a«y» ≺ <νx>(P' ∥ Q)" by(rule_tac ResB) auto moreover have "derivative (<νx>(P' ∥ Q)) (P' ∥ <νx>Q) a y Rel" proof(cases a, auto simp add: derivative_def) fix u show "((<νx>(P' ∥ Q))[y::=u], P'[y::=u] ∥ ((<νx>Q)[y::=u])) ∈ Rel" proof(cases "x=u") case True have "(<νx>(P' ∥ Q))[y::=x] = <νy>(([(y, x)] ∙ P') ∥ ([(y, x)] ∙ Q))" by(simp add: substRes3) moreover from ‹x ♯ P'› have "P'[y::=x] = [(y, x)] ∙ P'" by(rule injPermSubst[THEN sym]) moreover have "(<νx>Q)[y::=x] = <νy>([(y, x)] ∙ Q)" by(rule substRes3) moreover from ‹x ♯ P'› ‹y ≠ x› have "y ♯ [(y, x)] ∙ P'" by(simp add: name_fresh_left name_calc) ultimately show ?thesis using ‹x = u›by(force intro: Res) next case False with ‹y ≠ x› have "(<νx>(P' ∥ Q))[y::=u] = <νx>(P'[y::=u] ∥ Q[y::=u])" by(simp add: fresh_prod name_fresh) moreover from ‹x ≠ u› ‹y ≠ x› have "(<νx>Q)[y::=u] = <νx>(Q[y::=u])" by(simp add: fresh_prod name_fresh) moreover from ‹x ♯ P'› ‹x ≠ u› have "x ♯ P'[y::=u]" by(simp add: fresh_fact1) ultimately show ?thesis by(force intro: Res) qed next from ‹x ♯ P'› show "(<νx>(P' ∥ Q), P' ∥ <νx>Q) ∈ Rel" by(rule Res) qed ultimately show ?case by blast next case(cPar2 xQ) from ‹<νx>Q ⟼a«y» ≺ xQ› ‹y ≠ x› ‹y ♯ Q› show ?case proof(induct rule: resCasesB) case(cOpen a Q') from ‹Q ⟼a[x] ≺ Q'› ‹y ♯ Q› have yFreshQ': "y ♯ Q'" by(force intro: freshFreeDerivative) from ‹Q ⟼ a[x] ≺ Q'› have "P ∥ Q ⟼ a[x] ≺ P ∥ Q'" by(rule Par2F) hence "<νx>(P ∥ Q) ⟼ a<νx> ≺ P ∥ Q'" using ‹a ≠ x› by(rule Open) with ‹y ♯ P› ‹y ♯ Q'› have "<νx>(P ∥ Q) ⟼ a<νy> ≺ [(x, y)] ∙ (P ∥ Q')" by(subst alphaBoundResidual[where x'=x]) (auto simp add: fresh_left calc_atm) with ‹y ♯ P› ‹x ♯ P› have "<νx>(P ∥ Q) ⟼ a<νy> ≺ P ∥ ([(x, y)] ∙ Q')" by(simp add: name_fresh_fresh) moreover have "derivative (P ∥ ([(x, y)] ∙ Q')) (P ∥ ([(y, x)] ∙ Q')) (BoundOutputS a) y Rel" using Id by(auto simp add: derivative_def name_swap) ultimately show ?case by blast next case(cRes Q') from ‹Q ⟼ a«y» ≺ Q'› ‹y ♯ P› have "P ∥ Q ⟼ a«y» ≺ P ∥ Q'" by(rule Par2B) hence "<νx>(P ∥ Q) ⟼ a«y» ≺ <νx>(P ∥ Q')" using ‹x ♯ a› ‹y ≠ x› by(rule_tac ResB) auto moreover have "derivative (<νx>(P ∥ Q')) (P ∥ <νx>Q') a y Rel" proof(cases a, auto simp add: derivative_def) fix u show "((<νx>(P ∥ Q'))[y::=u], P[y::=u] ∥ (<νx>Q')[y::=u]) ∈ Rel" proof(cases "x=u") case True from ‹x ♯ P› ‹y ♯ P› have "(<νx>(P ∥ Q'))[y::=x] = <νy>(P ∥ ([(y, x)] ∙ Q'))" by(simp add: substRes3 perm_fresh_fresh) moreover from ‹y ♯ P› have "P[y::=x] = P" by(simp add: forget) moreover have "(<νx>Q')[y::=x] = <νy>([(y, x)] ∙ Q')" by(rule substRes3) ultimately show ?thesis using ‹x=u› ‹y ♯ P› by(force intro: Res) next case False with ‹y ≠ x› have "(<νx>(P ∥ Q'))[y::=u] = <νx>((P ∥ Q')[y::=u])" by(simp add: fresh_prod name_fresh) moreover from ‹y ≠ x› ‹x ≠ u› have "(<νx>Q')[y::=u] = <νx>(Q'[y::=u])" by(simp add: fresh_prod name_fresh) moreover from ‹x ♯ P› ‹x ≠ u› have "x ♯ P[y::=u]" by(force simp add: fresh_fact1) ultimately show ?thesis by(force intro: Res) qed next from ‹x ♯ P› show "(<νx>(P ∥ Q'), P ∥ <νx>Q') ∈ Rel" by(rule Res) qed ultimately show ?case by blast qed qed next case(Free α PxQ) from ‹P ∥ <νx>Q ⟼α ≺ PxQ› show ?case proof(induct rule: parCasesF[where C="x"]) case(cPar1 P') from ‹P ⟼ α ≺ P'› ‹x ♯ P›have "x ♯ α" and "x ♯ P'" by(force intro: freshFreeDerivative)+ from ‹P ⟼ α ≺ P'› have "P ∥ Q ⟼ α ≺ P' ∥ Q" by(rule Par1F) hence "<νx>(P ∥ Q) ⟼ α ≺ <νx>(P' ∥ Q)" using ‹x ♯ α› by(rule ResF) moreover from ‹x ♯ P'› have "(<νx>(P' ∥ Q), P' ∥ <νx>Q) ∈ Rel" by(rule Res) ultimately show ?case by blast next case(cPar2 Q') from ‹<νx>Q ⟼ α ≺ Q'› show ?case proof(induct rule: resCasesF) case(cRes Q') from ‹Q ⟼ α ≺ Q'› have "P ∥ Q ⟼ α ≺ P ∥ Q'" by(rule Par2F) hence "<νx>(P ∥ Q) ⟼α ≺ <νx>(P ∥ Q')" using ‹x ♯ α› by(rule ResF) moreover from ‹x ♯ P› have "(<νx>(P ∥ Q'), P ∥ <νx>Q') ∈ Rel" by(rule Res) ultimately show ?case by blast qed next case(cComm1 P' xQ a b y) from ‹y ♯ x› have "y ≠ x" by simp from ‹P ⟼ a<y> ≺ P'› ‹x ♯ P› ‹y ≠ x› have "x ♯ P'" by(force intro: freshBoundDerivative) from ‹<νx>Q ⟼a[b] ≺ xQ› show ?case proof(induct rule: resCasesF) case(cRes Q') from ‹x ♯ a[b]› have "x ≠ b" by simp from ‹P ⟼ a<y> ≺ P'› ‹Q ⟼ a[b] ≺ Q'› have "P ∥ Q ⟼ τ ≺ P'[y::=b] ∥ Q'" by(rule Comm1) hence "<νx>(P ∥ Q) ⟼ τ ≺ <νx>(P'[y::=b] ∥ Q')" by(rule_tac ResF) auto moreover from ‹x ♯ P'› ‹x ≠ b› have "x ♯ P'[y::=b]" by(force intro: fresh_fact1) hence "(<νx>(P'[y::=b] ∥ Q'), P'[y::=b] ∥ <νx>Q') ∈ Rel" by(rule Res) ultimately show ?case by blast qed next case(cComm2 P' xQ a b y) from ‹y ♯ x› ‹y ♯ <νx>Q› have "y ≠ x" and "y ♯ Q" by(simp add: abs_fresh)+ with ‹<νx>Q ⟼a<y> ≺ xQ› show ?case proof(induct rule: resCasesB) case(cOpen b Q') from ‹InputS a = BoundOutputS b› have False by simp thus ?case by simp next case(cRes Q') from ‹P ⟼a[b] ≺ P'› ‹Q ⟼a<y> ≺ Q'› have "P ∥ Q ⟼ τ ≺ P' ∥ Q'[y::=b]" by(rule Comm2) hence "<νx>(P ∥ Q) ⟼ τ ≺ <νx>(P' ∥ Q'[y::=b])" by(rule_tac ResF) auto moreover from ‹P ⟼a[b] ≺ P'› ‹x ♯ P› have "x ♯ P'" and "x ≠ b" by(force dest: freshFreeDerivative)+ from ‹x ♯ P'› have "(<νx>(P' ∥ Q'[y::=b]), P' ∥ <νx>(Q'[y::=b])) ∈ Rel" by(rule Res) with ‹y ≠ x› ‹x ≠ b› have "(<νx>(P' ∥ Q'[y::=b]), P' ∥ (<νx>Q')[y::=b]) ∈ Rel" by simp ultimately show ?case by blast qed next case(cClose1 P' Q' a y z) from ‹y ♯ x› have "y ≠ x" by simp from ‹z ♯ x› ‹z ♯ <νx>Q› have "z ♯ Q" and "z ≠ x" by(simp add: abs_fresh)+ from ‹P ⟼a<y> ≺ P'› ‹z ♯ P› have "z ≠ a" by(force dest: freshBoundDerivative) from ‹<νx>Q ⟼ a<νz> ≺ Q'› ‹z ≠ x› ‹z ♯ Q› show ?case proof(induct rule: resCasesB) case(cOpen b Q') from ‹BoundOutputS a = BoundOutputS b› have "a = b" by simp with ‹Q ⟼ b[x] ≺ Q'› have "([(z, x)] ∙ Q) ⟼ [(z, x)] ∙ (a[x] ≺ Q')" by(rule_tac transitions.eqvt) simp with ‹b ≠ x› ‹z ≠ a› ‹a = b› ‹z ≠ x› have "([(z, x)] ∙ Q) ⟼ a[z] ≺ ([(z, x)] ∙ Q')" by(simp add: name_calc eqvts) with ‹P ⟼a<y> ≺ P'› have "P ∥ ([(z, x)] ∙ Q) ⟼τ ≺ P'[y::=z] ∥ ([(z, x)] ∙ Q')" by(rule Comm1) hence "<νz>(P ∥ ([(x, z)] ∙ Q)) ⟼ τ ≺ <νz>(P'[y::=z] ∥ ([(z, x)] ∙ Q'))" by(rule_tac ResF) auto hence "<νx>(P ∥ Q) ⟼ τ ≺ <νz>(P'[y::=z] ∥ ([(z, x)] ∙ Q'))" using ‹z ♯ P› ‹z ♯ Q› ‹x ♯ P› by(subst alphaRes[where c=z]) auto with Id show ?case by force next case(cRes Q') from ‹P ⟼a<y> ≺ P'› ‹Q ⟼a<νz> ≺ Q'› ‹z ♯ P› have "P ∥ Q ⟼ τ ≺ <νz>(P'[y::=z] ∥ Q')" by(rule Close1) hence "<νx>(P ∥ Q) ⟼ τ ≺ <νx><νz>(P'[y::=z] ∥ Q')" by(rule_tac ResF) auto moreover from ‹P ⟼a<y> ≺ P'› ‹y ≠ x› ‹x ♯ P› have "x ♯ P'" by(force dest: freshBoundDerivative) with ‹z ≠ x› have "x ♯ P'[y::=z]" by(simp add: fresh_fact1) hence "(<νx><νz>(P'[y::=z] ∥ Q'), <νz>(P'[y::=z] ∥ <νx>Q')) ∈ Rel" by(rule ScopeExt) ultimately show ?case by blast qed next case(cClose2 P' xQ a y z) from ‹z ♯ x› ‹z ♯ <νx>Q› have "z ≠ x" and "z ♯ Q" by(auto simp add: abs_fresh) from ‹y ♯ x› ‹y ♯ <νx>Q› have "y ≠ x" and "y ♯ Q" by(auto simp add: abs_fresh) with ‹<νx>Q ⟼a<y> ≺ xQ› show ?case proof(induct rule: resCasesB) case(cOpen b Q') from ‹InputS a = BoundOutputS b› have False by simp thus ?case by simp next case(cRes Q') from ‹P ⟼a<νz> ≺ P'› ‹Q ⟼a<y> ≺ Q'› ‹z ♯ Q› have "P ∥ Q ⟼ τ ≺ <νz>(P' ∥ Q'[y::=z])" by(rule Close2) hence "<νx>(P ∥ Q) ⟼ τ ≺ <νx><νz>(P' ∥ (Q'[y::=z]))" by(rule_tac ResF) auto moreover from ‹P ⟼a<νz> ≺ P'› ‹x ♯ P› ‹z ≠ x› have "x ♯ P'" by(force dest: freshBoundDerivative) hence "(<νx><νz>(P' ∥ (Q'[y::=z])), <νz>(P' ∥ (<νx>(Q'[y::=z])))) ∈ Rel" by(rule ScopeExt) with ‹z ≠ x› ‹y ≠ x› have "(<νx><νz>(P' ∥ (Q'[y::=z])), <νz>(P' ∥ (<νx>Q')[y::=z])) ∈ Rel" by simp ultimately show ?case by blast qed qed qed lemma scopeExtParRight: fixes P :: pi and Q :: pi and a :: name and Rel :: "(pi × pi) set" assumes "x ♯ P" and Id: "Id ⊆ Rel" and "eqvt Rel" and Res: "⋀R S y. y ♯ R ⟹ (R ∥ <νy>S, <νy>(R ∥ S)) ∈ Rel" and ScopeExt: "⋀R S y z. y ♯ R ⟹ (<νz>(R ∥ <νy>S), <νy><νz>(R ∥ S)) ∈ Rel" shows "P ∥ <νx>Q ↝[Rel] <νx>(P ∥ Q)" using ‹eqvt Rel› proof(induct rule: simCasesCont[where C="(x, P, Q)"]) case(Bound a y xPQ) from ‹y ♯ (x, P, Q)› have "y ≠ x" and "y ♯ P" and "y ♯ Q" by simp+ hence "y ≠ x" and "y ♯ P ∥ Q" by(auto simp add: abs_fresh) with ‹<νx>(P ∥ Q) ⟼a«y» ≺ xPQ› show ?case proof(induct rule: resCasesB) case(cOpen a PQ) from ‹P ∥ Q ⟼a[x] ≺ PQ› show ?case proof(induct rule: parCasesF[where C="()"]) case(cPar1 P') from ‹P ⟼a[x] ≺ P'› ‹x ♯ P› have "x ≠ x" by(force dest: freshFreeDerivative) thus ?case by simp next case(cPar2 Q') from ‹Q ⟼a[x] ≺ Q'› ‹y ♯ Q› have "y ♯ Q'" by(force dest: freshFreeDerivative) from ‹Q ⟼a[x] ≺ Q'› ‹a ≠ x› have "<νx>Q ⟼a<νx> ≺ Q'" by(rule Open) hence "P ∥ <νx>Q ⟼a<νx> ≺ P ∥ Q'" using ‹x ♯ P› by(rule Par2B) with ‹y ♯ P› ‹y ♯ Q'› ‹x ♯ P› have "P ∥ <νx>Q ⟼a<νy> ≺ ([(y, x)] ∙ (P ∥ Q'))" by(subst alphaBoundResidual[where x'=x]) (auto simp add: fresh_left calc_atm) moreover with Id have "derivative ([(y, x)] ∙ (P ∥ Q')) ([(y, x)] ∙ (P ∥ Q')) (BoundOutputS a) y Rel" by(auto simp add: derivative_def) ultimately show ?case by blast next case(cComm1 P' Q' b c y) from ‹a[x] = τ› show ?case by simp next case(cComm2 P' Q' b c y) from ‹a[x] = τ› show ?case by simp next case(cClose1 P' Q' b y z) from ‹a[x] = τ› show ?case by simp next case(cClose2 P' Q' b y z) from ‹a[x] = τ› show ?case by simp qed next case(cRes PQ) from ‹P ∥ Q ⟼a«y» ≺ PQ› ‹y ♯ P› ‹y ♯ Q› show ?case proof(induct rule: parCasesB) case(cPar1 P') from ‹y ≠ x› ‹x ♯ P› ‹P ⟼a«y» ≺ P'› have "x ♯ P'" by(force dest: freshBoundDerivative) from ‹P ⟼a«y» ≺ P'› ‹y ♯ Q› have "P ∥ <νx>Q ⟼a«y» ≺ P' ∥ <νx>Q" by(rule_tac Par1B) (auto simp add: abs_fresh) moreover have "derivative (P' ∥ <νx>Q) (<νx>(P' ∥ Q)) a y Rel" proof(cases a, auto simp add: derivative_def) fix u::name obtain z::name where "z ♯ Q" and "y ≠ z" and "z ≠ u" and "z ♯ P" and "z ♯ P'" by(generate_fresh "name") auto thus "(P'[y::=u] ∥ (<νx>Q)[y::=u], (<νx>(P' ∥ Q))[y::=u]) ∈ Rel" using ‹x ♯ P'› by(subst alphaRes[where c=z and a=x], auto) (subst alphaRes[where c=z and a=x], auto intro: Res simp add: fresh_fact1) next from ‹x ♯ P'› show "(P' ∥ <νx>Q, <νx>(P' ∥ Q)) ∈ Rel" by(rule Res) qed ultimately show ?case by blast next case(cPar2 Q') from ‹Q ⟼a«y» ≺ Q'› have "<νx>Q ⟼a«y» ≺ <νx>Q'" using ‹x ♯ a› ‹y ≠ x› by(rule_tac ResB) auto hence "P ∥ <νx>Q ⟼a«y» ≺ P ∥ <νx>Q'" using ‹y ♯ P› by(rule Par2B) moreover have "derivative (P ∥ <νx>Q') (<νx>(P ∥ Q')) a y Rel" proof(cases a, auto simp add: derivative_def) fix u::name obtain z::name where "z ♯ Q" and "z ≠ y" and "z ≠ u" and "z ♯ P" and "z ♯ Q'" by(generate_fresh "name") auto thus "(P[y::=u] ∥ (<νx>Q')[y::=u], (<νx>(P ∥ Q'))[y::=u]) ∈ Rel" using ‹x ♯ P› by(subst alphaRes[where a=x and c=z], auto) (subst alphaRes[where a=x and c=z], auto intro: Res simp add: fresh_fact1) next from ‹x ♯ P› show "(P ∥ <νx>Q', <νx>(P ∥ Q')) ∈ Rel" by(rule Res) qed ultimately show ?case by blast qed qed next case(Free α xPQ) from ‹<νx>(P ∥ Q) ⟼α ≺ xPQ› show ?case proof(induct rule: resCasesF) case(cRes PQ) from ‹P ∥ Q ⟼α ≺ PQ› show ?case proof(induct rule: parCasesF[where C="x"]) case(cPar1 P') from ‹P ⟼α ≺ P'› have "P ∥ <νx>Q ⟼α ≺ P' ∥ <νx>Q" by(rule Par1F) moreover from ‹P ⟼α ≺ P'› ‹x ♯ P› have "x ♯ P'" by(rule freshFreeDerivative) hence "(P' ∥ <νx>Q, <νx>(P' ∥ Q)) ∈ Rel" by(rule Res) ultimately show ?case by blast next case(cPar2 Q') from ‹Q ⟼α ≺ Q'› ‹x ♯ α› have "<νx>Q ⟼α ≺ <νx>Q'" by(rule ResF) hence "P ∥ <νx>Q ⟼α ≺ P ∥ <νx>Q'" by(rule Par2F) moreover from ‹x ♯ P› have "(P ∥ <νx>Q', <νx>(P ∥ Q')) ∈ Rel" by(rule Res) ultimately show ?case by blast next case(cComm1 P' Q' a b y) from ‹x ♯ P› ‹y ♯ x› ‹P ⟼a<y> ≺ P'› have "x ≠ a" and "x ♯ P'" by(force dest: freshBoundDerivative)+ show ?case proof(cases "b=x") case True from ‹Q ⟼a[b] ≺ Q'› ‹x ≠ a› ‹b = x› have "<νx>Q ⟼a<νx> ≺ Q'" by(rule_tac Open) auto with ‹P ⟼a<y> ≺ P'› have "P ∥ <νx>Q ⟼τ ≺ <νx>(P'[y::=x] ∥ Q')" using ‹x ♯ P› by(rule Close1) moreover from Id have "(<νx>(P'[y::=b] ∥ Q'), <νx>(P'[y::=b] ∥ Q')) ∈ Rel" by blast ultimately show ?thesis using ‹b=x› by blast next case False from ‹Q ⟼a[b] ≺ Q'› ‹x ≠ a› ‹b ≠ x› have "<νx>Q ⟼a[b] ≺ <νx>Q'" by(rule_tac ResF) auto with ‹P ⟼a<y> ≺ P'› have "P ∥ <νx>Q ⟼τ ≺ (P'[y::=b] ∥ <νx>Q')" by(rule Comm1) moreover from ‹x ♯ P'› ‹b ≠ x› have "(P'[y::=b] ∥ <νx>Q', <νx>(P'[y::=b] ∥ Q')) ∈ Rel" by(force intro: Res simp add: fresh_fact1) ultimately show ?thesis by blast qed next case(cComm2 P' Q' a b y) from ‹P ⟼a[b] ≺ P'› ‹x ♯ P› have "x ≠ a" and "x ≠ b" and "x ♯ P'" by(force dest: freshFreeDerivative)+ from ‹Q ⟼a<y> ≺ Q'› ‹y ♯ x› ‹x ≠ a› have "<νx>Q ⟼a<y> ≺ <νx>Q'" by(rule_tac ResB) auto with ‹P ⟼a[b] ≺ P'› have "P ∥ <νx>Q ⟼τ ≺ P' ∥ (<νx>Q')[y::=b]" by(rule Comm2) moreover from ‹x ♯ P'› have "(P' ∥ <νx>(Q'[y::=b]), <νx>(P' ∥ Q'[y::=b])) ∈ Rel" by(rule Res) ultimately show ?case using ‹y ♯ x› ‹x ≠ b› by force next case(cClose1 P' Q' a y z) from ‹P ⟼a<y> ≺ P'› ‹x ♯ P› ‹y ♯ x› have "x ≠ a" and "x ♯ P'" by(force dest: freshBoundDerivative)+ from ‹Q ⟼a<νz> ≺ Q'› ‹z ♯ x› ‹x ≠ a› have "<νx>Q ⟼a<νz> ≺ <νx>Q'" by(rule_tac ResB) auto with ‹P ⟼a<y> ≺ P'› have "P ∥ <νx>Q ⟼τ ≺ <νz>(P'[y::=z] ∥ <νx>Q')" using ‹z ♯ P› by(rule Close1) moreover from ‹x ♯ P'› ‹z ♯ x› have "(<νz>(P'[y::=z] ∥ <νx>Q'), <νx>(<νz>(P'[y::=z] ∥ Q'))) ∈ Rel" by(rule_tac ScopeExt) (auto simp add: fresh_fact1) ultimately show ?case by blast next case(cClose2 P' Q' a y z) from ‹P ⟼a<νz> ≺ P'› ‹x ♯ P› ‹z ♯ x› have "x ≠ a" and "x ♯ P'" by(force dest: freshBoundDerivative)+ from ‹Q ⟼a<y> ≺ Q'› ‹y ♯ x› ‹x ≠ a› have "<νx>Q ⟼a<y> ≺ <νx>Q'" by(rule_tac ResB) auto with ‹P ⟼a<νz> ≺ P'› have "P ∥ <νx>Q ⟼τ ≺ <νz>(P' ∥ (<νx>Q')[y::=z])" using ‹z ♯ Q› by(rule_tac Close2) (auto simp add: abs_fresh) moreover from ‹x ♯ P'› have "(<νz>(P' ∥ <νx>(Q'[y::=z])), <νx><νz>(P' ∥ Q'[y::=z])) ∈ Rel" by(rule ScopeExt) ultimately show ?case using ‹z ♯ x› ‹y ♯ x› by force qed qed qed lemma resNilRight: fixes x :: name and Rel :: "(pi × pi) set" shows "𝟬 ↝[Rel] <νx>𝟬" by(fastforce simp add: simulation_def pi.inject alpha' elim: resCasesB' resCasesF) lemma resComm: fixes a :: name and b :: name and P :: pi and Rel :: "(pi × pi) set" assumes ResComm: "⋀