(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Strong_Late_Sim_Pres imports Strong_Late_Sim begin lemma tauPres: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes PRelQ: "(P, Q) ∈ Rel" shows "τ.(P) ↝[Rel] τ.(Q)" proof - show "τ.(P) ↝[Rel] τ.(Q)" proof(induct rule: simCases) case(Bound a x Q') have "τ.(Q) ⟼ a«x» ≺ Q'" by fact hence False by auto thus ?case by simp next case(Free α Q') have "τ.(Q) ⟼ α ≺ Q'" by fact thus ?case proof(induct rule: tauCases) case cTau have "τ.(P) ⟼ τ ≺ P" by(rule Late_Semantics.Tau) with PRelQ show ?case by blast qed qed qed lemma inputPres: fixes P :: pi and x :: name and Q :: pi and a :: name and Rel :: "(pi × pi) set" assumes PRelQ: "∀y. (P[x::=y], Q[x::=y]) ∈ Rel" and Eqvt: "eqvt Rel" shows "a<x>.P ↝[Rel] a<x>.Q" using Eqvt proof(induct rule: simCasesCont[where C="(x, a, P, Q)"]) case(Bound b y Q') from ‹y ♯ (x, a, P, Q)› have "y ≠ x" "y ≠ a" "y ♯ P" "y ♯ Q" by simp+ from ‹a<x>.Q ⟼b«y» ≺ Q'› ‹y ≠ a› ‹y ≠ x› ‹y ♯ Q› show ?case proof(induct rule: inputCases) case cInput have "a<x>.P ⟼ a<x> ≺ P" by(rule Input) hence "a<x>.P ⟼ a<y> ≺ ([(x, y)] ∙ P)" using ‹y ♯ P› by(simp add: alphaBoundResidual) moreover have "derivative ([(x, y)] ∙ P) ([(x, y)] ∙ Q) (InputS a) y Rel" proof(auto simp add: derivative_def) fix u show "(([(x, y)] ∙ P)[y::=u], ([(x, y)] ∙ Q)[y::=u]) ∈ Rel" proof(cases "y=u") assume "y = u" moreover have "([(y, x)] ∙ P, [(y, x)] ∙ Q) ∈ Rel" proof - from PRelQ have "(P[x::=x], Q[x::=x]) ∈ Rel" by blast hence "(P, Q) ∈ Rel" by simp with Eqvt show ?thesis by(rule eqvtRelI) qed ultimately show ?thesis by simp next assume yinequ: "y ≠ u" show ?thesis proof(cases "x = u") assume "x = u" moreover have "(([(y, x)] ∙ P)[y::=x], ([(y, x)] ∙ Q)[y::=x]) ∈ Rel" proof - from PRelQ have "(P[x::=y], Q[x::=y]) ∈ Rel" by blast with Eqvt have "([(y, x)] ∙ (P[x::=y]), [(y, x)] ∙ (Q[x::=y])) ∈ Rel" by(rule eqvtRelI) with ‹y ≠ x› show ?thesis by(simp add: eqvt_subs name_calc) qed ultimately show ?thesis by simp next assume xinequ: "x ≠ u" hence "(([(y, x)] ∙ P)[y::=u], ([(y, x)] ∙ Q)[y::=u]) ∈ Rel" proof - from PRelQ have "(P[x::=u], Q[x::=u]) ∈ Rel" by blast with Eqvt have "([(y, x)] ∙ (P[x::=u]), [(y, x)] ∙ (Q[x::=u])) ∈ Rel" by(rule eqvtRelI) with ‹y ≠ x› xinequ yinequ show ?thesis by(simp add: eqvt_subs name_calc) qed thus ?thesis by simp qed qed qed ultimately show ?case by blast qed next case(Free α Q') have "a<x>.Q ⟼ α ≺ Q'" by fact hence False by auto thus ?case by blast qed lemma outputPres: fixes P :: pi and Q :: pi and a :: name and b :: name and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes PRelQ: "(P, Q) ∈ Rel" shows "a{b}.P ↝[Rel] a{b}.Q" proof - show ?thesis proof(induct rule: simCases) case(Bound c x Q') have "a{b}.Q ⟼ c«x» ≺ Q'" by fact hence False by auto thus ?case by simp next case(Free α Q') have "a{b}.Q ⟼ α ≺ Q'" by fact thus ?case proof(induct rule: outputCases) case cOutput have "a{b}.P ⟼ a[b] ≺ P" by(rule Late_Semantics.Output) with PRelQ show ?case by blast qed qed qed lemma matchPres: fixes P :: pi and Q :: pi and a :: name and b :: name and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes PSimQ: "P ↝[Rel] Q" and "Rel ⊆ Rel'" shows "[a⌢b]P ↝[Rel'] [a⌢b]Q" proof - show ?thesis proof(induct rule: simCases) case(Bound c x Q') have "x ♯ [a⌢b]P" by fact hence xFreshP: "x ♯ P" by simp have "[a⌢b]Q ⟼ c«x» ≺ Q'" by fact thus ?case proof(induct rule: matchCases) case cMatch have "Q ⟼c«x» ≺ Q'" by fact with PSimQ xFreshP obtain P' where PTrans: "P ⟼c«x» ≺ P'" and Pderivative: "derivative P' Q' c x Rel" by(blast dest: simE) from PTrans have "[a⌢a]P ⟼ c«x» ≺ P'" by(rule Late_Semantics.Match) moreover from Pderivative ‹Rel ⊆ Rel'› have "derivative P' Q' c x Rel'" by(cases c) (auto simp add: derivative_def) ultimately show ?case by blast qed next case(Free α Q') have "[a⌢b]Q ⟼α ≺ Q'" by fact thus ?case proof(induct rule: matchCases) case cMatch have "Q ⟼ α ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟼ α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have "[a⌢a]P ⟼α ≺ P'" by(rule Late_Semantics.Match) with PRel ‹Rel ⊆ Rel'› show ?case by blast qed qed qed lemma mismatchPres: fixes P :: pi and Q :: pi and a :: name and b :: name and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes PSimQ: "P ↝[Rel] Q" and "Rel ⊆ Rel'" shows "[a≠b]P ↝[Rel'] [a≠b]Q" proof(induct rule: simCases) case(Bound c x Q') have "x ♯ [a≠b]P" by fact hence xFreshP: "x ♯ P" by simp from ‹[a≠b]Q ⟼ c«x» ≺ Q'› show ?case proof(induct rule: mismatchCases) case cMismatch have "Q ⟼c«x» ≺ Q'" by fact with PSimQ xFreshP obtain P' where PTrans: "P ⟼c«x» ≺ P'" and Pderivative: "derivative P' Q' c x Rel" by(blast dest: simE) from PTrans ‹a ≠ b› have "[a≠b]P ⟼ c«x» ≺ P'" by(rule Late_Semantics.Mismatch) moreover from Pderivative ‹Rel ⊆ Rel'› have "derivative P' Q' c x Rel'" by(cases c) (auto simp add: derivative_def) ultimately show ?case by blast qed next case(Free α Q') have "[a≠b]Q ⟼α ≺ Q'" by fact thus ?case proof(induct rule: mismatchCases) case cMismatch have "Q ⟼ α ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟼ α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans ‹a ≠ b› have "[a≠b]P ⟼α ≺ P'" by(rule Late_Semantics.Mismatch) with PRel ‹Rel ⊆ Rel'› show ?case by blast qed qed lemma sumPres: fixes P :: pi and Q :: pi and R :: pi assumes PSimQ: "P ↝[Rel] Q" and "Id ⊆ Rel'" and "Rel ⊆ Rel'" shows "P ⊕ R ↝[Rel'] Q ⊕ R" proof - show ?thesis proof(induct rule: simCases) case(Bound a x QR) have "x ♯ P ⊕ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ have "Q ⊕ R ⟼a«x» ≺ QR" by fact thus ?case proof(induct rule: sumCases) case cSum1 have "Q ⟼a«x» ≺ QR" by fact with xFreshP PSimQ obtain P' where PTrans: "P ⟼a«x» ≺ P'" and Pderivative: "derivative P' QR a x Rel" by(blast dest: simE) from PTrans have "P ⊕ R ⟼a«x» ≺ P'" by(rule Late_Semantics.Sum1) moreover from Pderivative ‹Rel ⊆ Rel'› have "derivative P' QR a x Rel'" by(cases a) (auto simp add: derivative_def) ultimately show ?case by blast next case cSum2 from ‹R ⟼a«x» ≺ QR› have "P ⊕ R ⟼a«x» ≺ QR" by(rule Sum2) thus ?case using ‹Id ⊆ Rel'› by(blast intro: derivativeReflexive) qed next case(Free α QR) have "Q ⊕ R ⟼α ≺ QR" by fact thus ?case proof(induct rule: sumCases) case cSum1 have "Q ⟼α ≺ QR" by fact with PSimQ obtain P' where PTrans: "P ⟼α ≺ P'" and PRel: "(P', QR) ∈ Rel" by(blast dest: simE) from PTrans have "P ⊕ R ⟼α ≺ P'" by(rule Late_Semantics.Sum1) with PRel ‹Rel ⊆ Rel'› show ?case by blast next case cSum2 from ‹R ⟼α ≺ QR› have "P ⊕ R ⟼α ≺ QR" by(rule Sum2) thus ?case using ‹Id ⊆ Rel'› by(blast intro: derivativeReflexive) qed qed qed lemma parCompose: fixes P :: pi and Q :: pi and R :: pi and T :: pi and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" and Rel'' :: "(pi × pi) set" assumes PSimQ: "P ↝[Rel] Q" and RSimT: "R ↝[Rel'] T" and PRelQ: "(P, Q) ∈ Rel" and RRel'T: "(R, T) ∈ Rel'" and Par: "⋀P Q R T. ⟦(P, Q) ∈ Rel; (R, T) ∈ Rel'⟧ ⟹ (P ∥ R, Q ∥ T) ∈ Rel''" and Res: "⋀P Q a. (P, Q) ∈ Rel'' ⟹ (<νa>P, <νa>Q) ∈ Rel''" and EqvtRel: "eqvt Rel" and EqvtRel': "eqvt Rel'" and EqvtRel'': "eqvt Rel''" shows "P ∥ R ↝[Rel''] Q ∥ T" using EqvtRel'' proof(induct rule: simCasesCont[where C="()"]) case(Bound a x Q') have "x ♯ P ∥ R" and "x ♯ Q ∥ T" by fact+ hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" and "x ♯ Q" and "x ♯ T" by simp+ have QTTrans: "Q ∥ T ⟼ a«x» ≺ Q'" by fact thus ?case using ‹x ♯ Q› ‹x ♯ T› proof(induct rule: parCasesB) case(cPar1 Q') have QTrans: "Q ⟼ a«x» ≺ Q'" and xFreshT: "x ♯ T" by fact+ from xFreshP PSimQ QTrans obtain P' where PTrans:"P ⟼ a«x» ≺ P'" and Pderivative: "derivative P' Q' a x Rel" by(blast dest: simE) from PTrans xFreshR have "P ∥ R ⟼ a«x» ≺ P' ∥ R" by(rule Late_Semantics.Par1B) moreover from Pderivative xFreshR xFreshT RRel'T have "derivative (P' ∥ R) (Q' ∥ T) a x Rel''" by(cases a, auto intro: Par simp add: derivative_def forget) ultimately show ?case by blast next case(cPar2 T') have TTrans: "T ⟼ a«x» ≺ T'" and xFreshQ: "x ♯ Q" by fact+ from xFreshR RSimT TTrans obtain R' where RTrans:"R ⟼ a«x» ≺ R'" and Rderivative: "derivative R' T' a x Rel'" by(blast dest: simE) from RTrans xFreshP have ParTrans: "P ∥ R ⟼ a«x» ≺ P ∥ R'" by(rule Late_Semantics.Par2B) moreover from Rderivative xFreshP xFreshQ PRelQ have "derivative (P ∥ R') (Q ∥ T') a x Rel''" by(cases a, auto intro: Par simp add: derivative_def forget) ultimately show ?case by blast qed next case(Free α QT') have QTTrans: "Q ∥ T ⟼ α ≺ QT'" by fact thus ?case using PSimQ RSimT PRelQ RRel'T proof(induct rule: parCasesF[where C="(P, R)"]) case(cPar1 Q') have RRel'T: "(R, T) ∈ Rel'" by fact have "P ↝[Rel] Q" and "Q ⟼ α ≺ Q'" by fact+ then obtain P' where PTrans: "P ⟼ α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have Trans: "P ∥ R ⟼ α ≺ P' ∥ R" by(rule Late_Semantics.Par1F) moreover from PRel RRel'T have "(P' ∥ R, Q' ∥ T) ∈ Rel''" by(blast intro: Par) ultimately show ?case by blast next case(cPar2 T') have PRelQ: "(P, Q) ∈ Rel" by fact have "R ↝[Rel'] T" and "T ⟼ α ≺ T'" by fact+ then obtain R' where RTrans: "R ⟼ α ≺ R'" and RRel: "(R', T') ∈ Rel'" by(blast dest: simE) from RTrans have Trans: "P ∥ R ⟼ α ≺ P ∥ R'" by(rule Late_Semantics.Par2F) moreover from PRelQ RRel have "(P ∥ R', Q ∥ T') ∈ Rel''" by(blast intro: Par) ultimately show ?case by blast next case(cComm1 Q' T' a b x) from ‹x ♯ (P, R)› have "x ♯ P" by simp with ‹P ↝[Rel] Q› ‹Q ⟼ a<x> ≺ Q'› ‹x ♯ P› obtain P' where PTrans: "P ⟼a<x> ≺ P'" and Pderivative: "derivative P' Q' (InputS a) x Rel" by(blast dest: simE) from Pderivative have PRel: "(P'[x::=b], Q'[x::=b]) ∈ Rel" by(simp add: derivative_def) have "R ↝[Rel'] T" and "T ⟼ a[b] ≺ T'" by fact+ then obtain R' where RTrans: "R ⟼a[b] ≺ R'" and RRel: "(R', T') ∈ Rel'" by(blast dest: simE) from PTrans RTrans have "P ∥ R ⟼ τ ≺ P'[x::=b] ∥ R'" by(rule Late_Semantics.Comm1) moreover from PRel RRel have "(P'[x::=b] ∥ R', Q'[x::=b] ∥ T') ∈ Rel''" by(blast intro: Par) ultimately show ?case by blast next case(cComm2 Q' T' a b x) have "P ↝[Rel] Q" and "Q ⟼a[b] ≺ Q'" by fact+ then obtain P' where PTrans: "P ⟼a[b] ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from ‹x ♯ (P, R)› have "x ♯ R" by simp with ‹R ↝[Rel'] T› ‹T ⟼a<x> ≺ T'› obtain R' where RTrans: "R ⟼a<x> ≺ R'" and Rderivative: "derivative R' T' (InputS a) x Rel'" by(blast dest: simE) from Rderivative have RRel: "(R'[x::=b], T'[x::=b]) ∈ Rel'" by(simp add: derivative_def) from PTrans RTrans have "P ∥ R ⟼ τ ≺ P' ∥ R'[x::=b]" by(rule Late_Semantics.Comm2) moreover from PRel RRel have "(P' ∥ R'[x::=b], Q' ∥ T'[x::=b]) ∈ Rel''" by(blast intro: Par) ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', Q' ∥ T'[x::=b]) ∈ Rel''" by blast next case(cClose1 Q' T' a x y) from ‹x ♯ (P, R)› have "x ♯ P" by simp with ‹P ↝[Rel] Q› ‹Q ⟼a<x> ≺ Q'› obtain P' where PTrans: "P ⟼a<x> ≺ P'" and Pderivative: "derivative P' Q' (InputS a) x Rel" by(blast dest: simE) from Pderivative have PRel: "(P'[x::=y], Q'[x::=y]) ∈ Rel" by(simp add: derivative_def) from ‹y ♯ (P, R)› have "y ♯ R" and "y ♯ P" by simp+ from ‹R ↝[Rel'] T› ‹T ⟼a<νy> ≺ T'› ‹y ♯ R› obtain R' where RTrans: "R ⟼a<νy> ≺ R'" and Rderivative: "derivative R' T' (BoundOutputS a) y Rel'" by(blast dest: simE) from Rderivative have RRel: "(R', T') ∈ Rel'" by(simp add: derivative_def) from PTrans RTrans ‹y ♯ P› have Trans: "P ∥ R ⟼ τ ≺ <νy>(P'[x::=y] ∥ R')" by(rule Late_Semantics.Close1) moreover from PRel RRel have "(<νy>(P'[x::=y] ∥ R'), <νy>(Q'[x::=y] ∥ T')) ∈ Rel''" by(blast intro: Par Res) ultimately show ?case by blast next case(cClose2 Q' T' a x y) from ‹y ♯ (P, R)› have "y ♯ P" and "y ♯ R" by simp+ from ‹P ↝[Rel] Q› ‹Q ⟼a<νy> ≺ Q'› ‹y ♯ P› obtain P' where PTrans: "P ⟼a<νy> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(force dest: simE simp add: derivative_def) from ‹x ♯ (P, R)› have "x ♯ R" by simp+ with ‹R ↝[Rel'] T› ‹T ⟼a<x> ≺ T'› obtain R' where RTrans: "R ⟼a<x> ≺ R'" and R'Rel'T': "(R'[x::=y], T'[x::=y]) ∈ Rel'" by(force dest: simE simp add: derivative_def) from PTrans RTrans ‹y ♯ R› have Trans: "P ∥ R ⟼ τ ≺ <νy>(P' ∥ R'[x::=y])" by(rule Close2) moreover from P'RelQ' R'Rel'T' have "(<νy>(P' ∥ R'[x::=y]), <νy>(Q' ∥ T'[x::=y])) ∈ Rel''" by(blast intro: Par Res) ultimately show ?case by blast qed qed lemma parPres: fixes P :: pi and Q :: pi and R :: pi and a :: name and b :: name and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes PSimQ: "P ↝[Rel] Q" and PRelQ: "(P, Q) ∈ Rel" and Par: "⋀P Q R. (P, Q) ∈ Rel ⟹ (P ∥ R, Q ∥ R) ∈ Rel'" and Res: "⋀P Q a. (P, Q) ∈ Rel' ⟹ (<νa>P, <νa>Q) ∈ Rel'" and EqvtRel: "eqvt Rel" and EqvtRel': "eqvt Rel'" shows "P ∥ R ↝[Rel'] Q ∥ R" proof - note PSimQ moreover have RSimR: "R ↝[Id] R" by(auto intro: reflexive) moreover note PRelQ moreover have "(R, R) ∈ Id" by auto moreover from Par have "⋀P Q R T. ⟦(P, Q) ∈ Rel; (R, T) ∈ Id⟧ ⟹ (P ∥ R, Q ∥ T) ∈ Rel'" by auto moreover note Res ‹eqvt Rel› moreover have "eqvt Id" by(auto simp add: eqvt_def) ultimately show ?thesis using EqvtRel' by(rule parCompose) qed lemma resDerivative: fixes P :: pi and Q :: pi and a :: subject and x :: name and y :: name and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes Der: "derivative P Q a x Rel" and Rel: "⋀(P::pi) (Q::pi) (x::name). (P, Q) ∈ Rel ⟹ (<νx>P, <νx>Q) ∈ Rel'" and Eqv: "eqvt Rel" shows "derivative (<νy>P) (<νy>Q) a x Rel'" proof - from Der Rel show ?thesis proof(cases a, auto simp add: derivative_def) fix u assume A1: "∀u. (P[x::=u], Q[x::=u]) ∈ Rel" show "((<νy>P)[x::=u], (<νy>Q)[x::=u]) ∈ Rel'" proof(cases "x=y") assume xeqy: "x=y" from A1 have "(P[x::=x], Q[x::=x]) ∈ Rel" by blast hence L1: "(<νy>P, <νy>Q) ∈ Rel'" by(force intro: Rel) have "y ♯ <νy>P" and "y ♯ <νy>Q" by(simp only: freshRes)+ hence "(<νy>P)[y::=u] = <νy>P" and "(<νy>Q)[y::=u] = <νy>Q" by(simp add: forget)+ with L1 xeqy show ?thesis by simp next assume xineqy: "x≠y" show ?thesis proof(cases "y=u") assume yequ: "y=u" have "∃(c::name). c ♯ (P, Q, x, y)" by(blast intro: name_exists_fresh) then obtain c where cFreshP: "c ♯ P" and cFreshQ: "c ♯ Q" and cineqx: "c ≠ x" and cineqy: "y ≠ c" by(force simp add: fresh_prod name_fresh) from A1 have "(P[x::=c], Q[x::=c]) ∈ Rel" by blast with Eqv have "([(y, c)] ∙ (P[x::=c]), [(y, c)] ∙ (Q[x::=c])) ∈ Rel" by(rule eqvtRelI) with xineqy cineqx cineqy have "(([(y, c)] ∙ P)[x::=y], ([(y, c)] ∙ Q)[x::=y]) ∈ Rel" by(simp add: eqvt_subs name_calc) hence "(<νc>(([(y, c)] ∙ P)[x::=y]), <νc>(([(y, c)] ∙ Q)[x::=y])) ∈ Rel'" by(rule Rel) with cineqx cineqy have "((<νc>(([(y, c)] ∙ P)))[x::=y], (<νc>(([(y, c)] ∙ Q)))[x::=y])∈ Rel'" by simp moreover from cFreshP cFreshQ have "<νc>([(y, c)] ∙ P) = <νy>P" and "<νc>([(y, c)] ∙ Q) = <νy>Q" by(simp add: alphaRes)+ ultimately show ?thesis using yequ by simp next assume yinequ: "y ≠ u" from A1 have "(P[x::=u], Q[x::=u]) ∈ Rel" by blast hence "(<νy>(P[x::=u]), <νy>(Q[x::=u])) ∈ Rel'" by(rule Rel) with xineqy yinequ show ?thesis by simp qed qed qed qed lemma resPres: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" and x :: name and Rel' :: "(pi × pi) set" assumes PSimQ: "P ↝[Rel] Q" and ResRel: "⋀(P::pi) (Q::pi) (x::name). (P, Q) ∈ Rel ⟹ (<νx>P, <νx>Q) ∈ Rel'" and RelRel': "Rel ⊆ Rel'" and EqvtRel: "eqvt Rel" and EqvtRel': "eqvt Rel'" shows "<νx>P ↝[Rel'] <νx>Q" using EqvtRel' proof(induct rule: resSimCases[of _ _ _ _ "(P, x)"]) case(BoundOutput Q' a) have QTrans: "Q ⟼a[x] ≺ Q'" and aineqx: "a ≠ x" by fact+ from PSimQ QTrans obtain P' where PTrans: "P ⟼ a[x] ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans aineqx have "<νx>P ⟼a<νx> ≺ P'" by(rule Late_Semantics.Open) moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by force ultimately show ?case by blast next case(BoundR Q' a y) have QTrans: "Q ⟼a«y» ≺ Q'" and xFresha: "x ♯ a" by fact+ have "y ♯ (P, x)" by fact hence yFreshP: "y ♯ P" and yineqx: "y ≠ x" by(simp add: fresh_prod)+ from PSimQ yFreshP QTrans obtain P' where PTrans: "P ⟼a«y» ≺ P'" and Pderivative: "derivative P' Q' a y Rel" by(blast dest: simE) from PTrans xFresha yineqx have ResTrans: "<νx>P ⟼a«y» ≺ <νx>P'" by(blast intro: Late_Semantics.ResB) moreover from Pderivative ResRel EqvtRel have "derivative (<νx>P') (<νx>Q') a y Rel'" by(rule resDerivative) ultimately show ?case by blast next case(FreeR Q' α) have QTrans: "Q ⟼ α ≺ Q'" and xFreshAlpha: "(x::name) ♯ α" by fact+ from QTrans PSimQ obtain P' where PTrans: "P ⟼ α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans xFreshAlpha have "<νx>P ⟼α ≺ <νx>P'" by(rule Late_Semantics.ResF) moreover from P'RelQ' have "(<νx>P', <νx>Q') ∈ Rel'" by(rule ResRel) ultimately show ?case by blast qed lemma resChainI: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" and xs :: "name list" assumes PRelQ: "P ↝[Rel] Q" and eqvtRel: "eqvt Rel" and Res: "⋀P Q x. (P, Q) ∈ Rel ⟹ (<νx>P, <νx>Q) ∈ Rel" shows "(resChain xs) P ↝[Rel] (resChain xs) Q" proof(induct xs) (* Base case *) from PRelQ show "resChain [] P ↝[Rel] resChain [] Q" by simp next (* Inductive step *) fix x xs assume IH: "(resChain xs P) ↝[Rel] (resChain xs Q)" moreover note Res moreover have "Rel ⊆ Rel" by simp ultimately have "<νx>(resChain xs P) ↝[Rel] <νx>(resChain xs Q)" using eqvtRel by(rule_tac resPres) thus "resChain (x # xs) P ↝[Rel] resChain (x # xs) Q" by simp qed lemma bangPres: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" assumes PRelQ: "(P, Q) ∈ Rel" and Sim: "⋀P Q. (P, Q) ∈ Rel ⟹ P ↝[Rel] Q" and eqvtRel: "eqvt Rel" shows "!P ↝[bangRel Rel] !Q" proof - let ?Sim = "λP Rs. (∀a x Q'. Rs = a«x» ≺ Q' ⟶ x ♯ P ⟶ (∃P'. P ⟼a«x» ≺ P' ∧ derivative P' Q' a x (bangRel Rel))) ∧ (∀α Q'. Rs = α ≺ Q' ⟶ (∃P'. P ⟼α ≺ P' ∧ (P', Q') ∈ bangRel Rel))" from eqvtRel have EqvtBangRel: "eqvt(bangRel Rel)" by(rule eqvtBangRel) { fix Pa Rs assume "!Q ⟼ Rs" and "(Pa, !Q) ∈ bangRel Rel" hence "?Sim Pa Rs" using PRelQ proof(nominal_induct avoiding: Pa P rule: bangInduct) case(cPar1B a x Q' Pa P) have QTrans: "Q ⟼ a«x» ≺ Q'" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ Pa" by fact+ thus "?Sim Pa (a«x» ≺ (Q' ∥ !Q))" proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" by fact have PBRQ: "(R, !Q) ∈ bangRel Rel" by fact have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ show ?case proof(auto simp add: residual.inject alpha') from PRelQ have "P ↝[Rel] Q" by(rule Sim) with QTrans xFreshP obtain P' where PTrans: "P ⟼ a«x» ≺ P'" and P'RelQ': "derivative P' Q' a x Rel" by(blast dest: simE) from PTrans xFreshR have "P ∥ R ⟼ a«x» ≺ (P' ∥ R)" by(force intro: Late_Semantics.Par1B) moreover from P'RelQ' PBRQ ‹x ♯ Q› ‹x ♯ R› have "derivative (P' ∥ R) (Q' ∥ !Q) a x (bangRel Rel)" by(cases a) (auto simp add: derivative_def forget intro: Rel.BRPar) ultimately show "∃P'. P ∥ R ⟼a«x» ≺ P' ∧ derivative P' (Q' ∥ !Q) a x (bangRel Rel)" by blast next fix y assume "(y::name) ♯ Q'" and "y ♯ P" and "y ♯ R" and "y ♯ Q" from QTrans ‹y ♯ Q'› have "Q ⟼a«y» ≺ ([(x, y)] ∙ Q')" by(simp add: alphaBoundResidual) moreover from PRelQ have "P ↝[Rel] Q" by(rule Sim) ultimately obtain P' where PTrans: "P ⟼a«y» ≺ P'" and P'RelQ': "derivative P' ([(x, y)] ∙ Q') a y Rel" using ‹y ♯ P› by(blast dest: simE) from PTrans ‹y ♯ R› have "P ∥ R ⟼a«y» ≺ (P' ∥ R)" by(force intro: Late_Semantics.Par1B) moreover from P'RelQ' PBRQ ‹y ♯ Q› ‹y ♯ R› have "derivative (P' ∥ R) (([(x, y)] ∙ Q') ∥ !Q) a y (bangRel Rel)" by(cases a) (auto simp add: derivative_def forget intro: Rel.BRPar) with ‹x ♯ Q› ‹y ♯ Q› have "derivative (P' ∥ R) (([(y, x)] ∙ Q') ∥ !([(y, x)] ∙ Q)) a y (bangRel Rel)" by(simp add: name_fresh_fresh name_swap) ultimately show "∃P'. P ∥ R ⟼a«y» ≺ P' ∧ derivative P' (([(y, x)] ∙ Q') ∥ !([(y, x)] ∙ Q)) a y (bangRel Rel)" by blast qed qed next case(cPar1F α Q' Pa P) have QTrans: "Q ⟼α ≺ Q'" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and BR: "(R, !Q) ∈ bangRel Rel" by fact+ show ?case proof(auto simp add: residual.inject) from PRelQ have "P ↝[Rel] Q" by(rule Sim) with QTrans obtain P' where PTrans: "P ⟼ α ≺ P'" and RRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have "P ∥ R ⟼ α ≺ P' ∥ R" by(rule Par1F) moreover from RRel BR have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel" by(rule Rel.BRPar) ultimately show "∃P'. P ∥ R ⟼ α ≺ P' ∧ (P', Q' ∥ !Q) ∈ bangRel Rel" by blast qed qed next case(cPar2B a x Q' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a«x» ≺ Q')" by simp have "(Pa, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ Pa" by fact+ thus "?Sim Pa (a«x» ≺ (Q ∥ Q'))" proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ from EqvtBangRel ‹x ♯ Q› show "?Sim (P ∥ R) (a«x» ≺ (Q ∥ Q'))" proof(auto simp add: residual.inject alpha' name_fresh_fresh) from RBRQ have "?Sim R (a«x» ≺ Q')" by(rule IH) with xFreshR obtain R' where RTrans: "R ⟼ a«x» ≺ R'" and R'BRQ': "derivative R' Q' a x (bangRel Rel)" by(auto simp add: residual.inject) from RTrans xFreshP have "P ∥ R ⟼ a«x» ≺ (P ∥ R')" by(auto intro: Par2B) moreover from PRelQ R'BRQ' ‹x ♯ Q› ‹x ♯ P› have "derivative (P ∥ R') (Q ∥ Q') a x (bangRel Rel)" by(cases a) (auto simp add: derivative_def forget intro: Rel.BRPar) ultimately show "∃P'. P ∥ R ⟼ a«x» ≺ P' ∧ derivative P' (Q ∥ Q') a x (bangRel Rel)" by blast next fix y assume "(y::name) ♯ Q" and "y ♯ Q'" and "y ♯ P" and "y ♯ R" from RBRQ have "?Sim R (a«x» ≺ Q')" by(rule IH) with ‹y ♯ Q'› have "?Sim R (a«y» ≺ ([(x, y)] ∙ Q'))" by(simp add: alphaBoundResidual) with ‹y ♯ R› obtain R' where RTrans: "R ⟼ a«y» ≺ R'" and R'BRQ': "derivative R' ([(x, y)] ∙ Q') a y (bangRel Rel)" by(auto simp add: residual.inject) from RTrans ‹y ♯ P› have "P ∥ R ⟼ a«y» ≺ (P ∥ R')" by(auto intro: Par2B) moreover from PRelQ R'BRQ' ‹y ♯ P› ‹y ♯ Q› have "derivative (P ∥ R') (Q ∥ ([(x, y)] ∙ Q')) a y (bangRel Rel)" by(cases a) (auto simp add: derivative_def forget intro: Rel.BRPar) hence "derivative (P ∥ R') (Q ∥ ([(y, x)] ∙ Q')) a y (bangRel Rel)" by(simp add: name_swap) ultimately show "∃P'. P ∥ R ⟼ a«y» ≺ P' ∧ derivative P' (Q ∥ ([(y, x)] ∙ Q')) a y (bangRel Rel)" by blast qed qed next case(cPar2F α Q' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (α ≺ Q')" by simp have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+ show ?case proof(auto simp add: residual.inject) from RBRQ IH have "∃R'. R ⟼ α ≺ R' ∧ (R', Q') ∈ bangRel Rel" by(metis simE) then obtain R' where RTrans: "R ⟼ α ≺ R'" and R'RelQ': "(R', Q') ∈ bangRel Rel" by blast from RTrans have "P ∥ R ⟼ α ≺ P ∥ R'" by(rule Par2F) moreover from PRelQ R'RelQ' have "(P ∥ R', Q ∥ Q') ∈ bangRel Rel" by(rule Rel.BRPar) ultimately show " ∃P'. P ∥ R ⟼ α ≺ P' ∧ (P', Q ∥ Q') ∈ bangRel Rel" by blast qed qed next case(cComm1 a x Q' b Q'' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a[b] ≺ Q'')" by simp have QTrans: "Q ⟼a<x> ≺ Q'" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case using ‹x ♯ Pa› proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+ from ‹x ♯ P ∥ R› have "x ♯ P" and "x ♯ R" by simp+ show ?case proof(auto simp add: residual.inject) from PRelQ have "P ↝[Rel] Q" by(rule Sim) with QTrans ‹x ♯ P› obtain P' where PTrans: "P ⟼ a<x> ≺ P'" and P'RelQ': "(P'[x::=b], Q'[x::=b]) ∈ Rel" by(drule_tac simE) (auto simp add: derivative_def) from IH RBRQ have RTrans: "∃R'. R ⟼ a[b] ≺ R' ∧ (R', Q'') ∈ bangRel Rel" by(auto simp add: derivative_def) then obtain R' where RTrans: "R ⟼ a[b] ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel" by blast from PTrans RTrans have "P ∥ R ⟼τ ≺ P'[x::=b] ∥ R'" by(rule Comm1) moreover from P'RelQ' R'RelQ'' have "(P'[x::=b] ∥ R', Q'[x::=b] ∥ Q'') ∈ bangRel Rel" by(rule Rel.BRPar) ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', Q'[x::=b] ∥ Q'') ∈ bangRel Rel" by blast qed qed next case(cComm2 a b Q' x Q'' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a<x> ≺ Q'')" by simp have QTrans: "Q ⟼ a[b] ≺ Q'" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case using ‹x ♯ Pa› proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+ from ‹x ♯ P ∥ R› have "x ♯ P" and "x ♯ R" by simp+ show ?case proof(auto simp add: residual.inject) from PRelQ have "P ↝[Rel] Q" by(rule Sim) with QTrans obtain P' where PTrans: "P ⟼ a[b] ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from IH RBRQ ‹x ♯ R› have RTrans: "∃R'. R ⟼ a<x> ≺ R' ∧ (R'[x::=b], Q''[x::=b]) ∈ bangRel Rel" by(fastforce simp add: derivative_def residual.inject) then obtain R' where RTrans: "R ⟼ a<x> ≺ R'" and R'RelQ'': "(R'[x::=b], Q''[x::=b]) ∈ bangRel Rel" by blast from PTrans RTrans have "P ∥ R ⟼ τ ≺ P' ∥ R'[x::=b]" by(rule Comm2) moreover from P'RelQ' R'RelQ'' have "(P' ∥ R'[x::=b], Q' ∥ Q''[x::=b]) ∈ bangRel Rel" by(rule Rel.BRPar) ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', Q' ∥ (Q''[x::=b])) ∈ bangRel Rel" by blast qed qed next case(cClose1 a x Q' y Q'' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟶ ?Sim Pa (a<νy> ≺ Q'')" by simp have QTrans: "Q ⟼ a<x> ≺ Q'" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact moreover have xFreshPa: "x ♯ Pa" by fact ultimately show ?case using ‹y ♯ Pa› proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" and "y ♯ P ∥ R" by fact+ hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" and "y ♯ R" and "y ♯ P" by simp+ show ?case proof(auto simp add: residual.inject) from PRelQ have "P ↝[Rel] Q" by(rule Sim) with QTrans xFreshP obtain P' where PTrans: "P ⟼a<x> ≺ P'" and P'RelQ': "(P'[x::=y], Q'[x::=y]) ∈ Rel" by(fastforce dest: simE simp add: derivative_def) from RBRQ ‹y ♯ R› IH have "∃R'. R ⟼a<νy> ≺ R' ∧ (R', Q'') ∈ bangRel Rel" by(auto simp add: residual.inject derivative_def) then obtain R' where RTrans: "R ⟼a<νy> ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel" by blast from PTrans RTrans ‹y ♯ P› have "P ∥ R ⟼τ ≺ <νy>(P'[x::=y] ∥ R')" by(rule Close1) moreover from P'RelQ' R'RelQ'' have "(<νy>(P'[x::=y] ∥ R'), <νy>(Q'[x::=y] ∥ Q'')) ∈ bangRel Rel" by(force intro: Rel.BRPar BRRes) ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', <νy>(Q'[x::=y] ∥ Q'')) ∈ bangRel Rel" by blast qed qed next case(cClose2 a x Q' y Q'' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a<y> ≺ Q'')" by simp have QTrans: "Q ⟼ a<νx> ≺ Q'" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ Pa" and "y ♯ Pa" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBRQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" and "y ♯ P ∥ R" by fact+ hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" and "y ♯ R" by simp+ show ?case proof(auto simp add: residual.inject) from PRelQ have "P ↝[Rel] Q" by(rule Sim) with QTrans xFreshP obtain P' where PTrans: "P ⟼a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(fastforce dest: simE simp add: derivative_def) from RBRQ IH ‹y ♯ R› have "∃R'. R ⟼a<y> ≺ R' ∧ (R'[y::=x], Q''[y::=x]) ∈ bangRel Rel" by(fastforce simp add: derivative_def residual.inject) then obtain R' where RTrans: "R ⟼a<y> ≺ R'" and R'RelQ'': "(R'[y::=x], Q''[y::=x]) ∈ bangRel Rel" by blast from PTrans RTrans xFreshR have "P ∥ R ⟼ τ ≺ <νx>(P' ∥ R'[y::=x])" by(rule Close2) moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'[y::=x]), <νx>(Q' ∥ Q''[y::=x])) ∈ bangRel Rel" by(force intro: Rel.BRPar BRRes) ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', <νx>(Q' ∥ Q''[y::=x])) ∈ bangRel Rel" by blast qed qed next case(cBang Rs Pa P) hence IH: "⋀Pa. (Pa, Q ∥ !Q) ∈ bangRel Rel ⟹ ?Sim Pa Rs" by simp have "(Pa, !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRBangCases) case(BRBang P) have PRelQ: "(P, Q) ∈ Rel" by fact hence "(!P, !Q) ∈ bangRel Rel" by(rule Rel.BRBang) with PRelQ have "(P ∥ !P, Q ∥ !Q) ∈ bangRel Rel" by(rule BRPar) with IH have "?Sim (P ∥ !P) Rs" by simp thus ?case by(force intro: Bang) qed qed } moreover from PRelQ have "(!P, !Q) ∈ bangRel Rel" by(rule BRBang) ultimately show ?thesis by(auto simp add: simulation_def) qed end