(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Strong_Early_Sim_Pres imports Strong_Early_Sim begin lemma tauPres: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" assumes PRelQ: "(P, Q) ∈ Rel" shows "τ.(P) ↝[Rel] τ.(Q)" proof(induct rule: simCases) case(Bound a y Q') have "τ.(Q) ⟼ a<νy> ≺ Q'" by fact hence False by(induct rule: tauCases', auto) thus ?case by simp next case(Free α Q') have "τ.(Q) ⟼ α ≺ Q'" by fact thus "∃P'. τ.(P) ⟼ α ≺ P' ∧ (P', Q') ∈ Rel" proof(induct rule: tauCases', auto simp add: pi.inject residual.inject) have "τ.(P) ⟼ τ ≺ P" by(rule TransitionsEarly.Tau) with PRelQ show "∃P'. τ.(P) ⟼ τ ≺ P' ∧ (P', Q) ∈ Rel" by blast 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 by(erule_tac inputCases') auto next case(Free α Q') from ‹a<x>.Q ⟼ α ≺ Q'› show ?case proof(induct rule: inputCases) case(cInput u) have "a<x>.P ⟼a<u> ≺ P[x::=u]" by(rule Input) moreover from PRelQ have "(P[x::=u], Q[x::=u]) ∈ Rel" by auto ultimately show ?case by blast qed 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(induct rule: simCases) case(Bound c y Q') have "a{b}.Q ⟼ c<νy> ≺ Q'" by fact hence False by(induct rule: outputCases', auto) thus "∃P'. a{b}.P ⟼ c<νy> ≺ P' ∧ (P', Q') ∈ Rel" by simp next case(Free α Q') have "a{b}.Q ⟼ α ≺ Q'" by fact thus "∃P'. a{b}.P ⟼ α ≺ P' ∧ (P', Q') ∈ Rel" proof(induct rule: outputCases', auto simp add: pi.inject residual.inject) have "a{b}.P ⟼ a[b] ≺ P" by(rule TransitionsEarly.Output) with PRelQ show "∃P'. a{b}.P ⟼ a[b] ≺ P' ∧ (P', Q) ∈ Rel" by blast 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 RelRel': "Rel ⊆ Rel'" shows "[a⌢b]P ↝[Rel'] [a⌢b]Q" proof(induct rule: simCases) case(Bound c y Q') have "(y::name) ♯ [a⌢b]P" by fact hence yFreshP: "y ♯ P" by simp have "[a⌢b]Q ⟼ c<νy> ≺ Q'" by fact thus ?case proof(induct rule: matchCases) case Match have "Q ⟼c<νy> ≺ Q'" by fact with PSimQ yFreshP obtain P' where PTrans: "P ⟼c<νy> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) from PTrans have "[a⌢a]P ⟼ c<νy> ≺ P'" by(rule Early_Semantics.Match) moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast ultimately show ?case by blast qed next case(Free α Q') assume "[a⌢b]Q ⟼ α ≺ Q'" thus ?case proof(induct rule: matchCases) case Match have "Q ⟼ α ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟼ α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) from PTrans have "[a⌢a]P ⟼α ≺ P'" by(rule TransitionsEarly.Match) moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast ultimately show ?case by blast 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 RelRel': "Rel ⊆ Rel'" shows "[a≠b]P ↝[Rel'] [a≠b]Q" proof(cases "a = b") assume "a = b" thus ?thesis by(auto simp add: strongSimEarly_def) next assume aineqb: "a ≠ b" 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: mismatchCases) case Mismatch have "Q ⟼c<νx> ≺ Q'" by fact with PSimQ xFreshP obtain P' where PTrans: "P ⟼c<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) from PTrans aineqb have "[a≠b]P ⟼ c<νx> ≺ P'" by(rule Early_Semantics.Mismatch) moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast ultimately show ?case by blast qed next case(Free α Q') have "[a≠b]Q ⟼α ≺ Q'" by fact thus ?case proof(induct rule: mismatchCases) case Mismatch have "Q ⟼ α ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟼ α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: elim) from PTrans ‹a ≠ b› have "[a≠b]P ⟼α ≺ P'" by(rule TransitionsEarly.Mismatch) with RelRel' PRel show ?case by blast qed qed qed lemma sumPres: fixes P :: pi and Q :: pi and R :: pi and Rel :: "(pi × pi) set" and Rel' :: "(pi × pi) set" assumes "P ↝[Rel] Q" and C1: "Id ⊆ Rel'" and "Rel ⊆ Rel'" shows "P ⊕ R ↝[Rel'] Q ⊕ R" proof(induct rule: simCases) case(Bound a y Q') have "y ♯ P ⊕ R" by fact hence "(y::name) ♯ P" and "y ♯ R" by simp+ from ‹Q ⊕ R ⟼a<νy> ≺ Q'› show ?case proof(induct rule: sumCases) case Sum1 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(blast dest: elim) from PTrans have "P ⊕ R ⟼a<νy> ≺ P'" by(rule Early_Semantics.Sum1) moreover from P'RelQ' ‹Rel ⊆ Rel'› have "(P', Q') ∈ Rel'" by blast ultimately show ?case by blast next case Sum2 from ‹R ⟼a<νy> ≺ Q'› have "P ⊕ R ⟼a<νy> ≺ Q'" by(rule Early_Semantics.Sum2) moreover from C1 have "(Q', Q') ∈ Rel'" by auto ultimately show ?case by blast qed next case(Free α Q') from ‹Q ⊕ R ⟼α ≺ Q'› show "∃P'. P ⊕ R ⟼ α ≺ P' ∧ (P', Q') ∈ Rel'" proof(induct rule: sumCases) case Sum1 have "Q ⟼α ≺ Q'" by fact with ‹P ↝[Rel] Q› obtain P' where PTrans: "P ⟼α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) from PTrans have "P ⊕ R ⟼α ≺ P'" by(rule TransitionsEarly.Sum1) moreover from P'RelQ' ‹Rel ⊆ Rel'› have "(P', Q') ∈ Rel'" by blast ultimately show ?case by blast next case Sum2 from ‹R ⟼α ≺ Q'› have "P ⊕ R ⟼α ≺ Q'" by(rule TransitionsEarly.Sum2) moreover from C1 have "(Q', Q') ∈ Rel'" by blast ultimately show ?case by blast 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'] S" and PRelQ: "(P, Q) ∈ Rel" and RRel'T: "(R, S) ∈ Rel'" and Par: "⋀P' Q' R' S'. ⟦(P', Q') ∈ Rel; (R', S') ∈ Rel'⟧ ⟹ (P' ∥ R', Q' ∥ S') ∈ Rel''" and Res: "⋀S T x. (S, T) ∈ Rel'' ⟹ (<νx>S, <νx>T) ∈ Rel''" shows "P ∥ R ↝[Rel''] Q ∥ S" proof(induct rule: simCases) case(Bound a x Q') have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ have "Q ∥ S ⟼ a<νx> ≺ Q'" by fact thus ?case proof(induct rule: parCasesB) case(cPar1 Q') have "Q ⟼ a<νx> ≺ Q'" by fact with PSimQ xFreshP obtain P' where PTrans:"P ⟼ a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) from PTrans xFreshR have "P ∥ R ⟼ a<νx> ≺ (P' ∥ R)" by(rule Early_Semantics.Par1B) moreover from P'RelQ' RRel'T have "(P' ∥ R, Q' ∥ S) ∈ Rel''" by(rule Par) ultimately show ?case by blast next case(cPar2 S') have "S ⟼ a<νx> ≺ S'" by fact with RSimT xFreshR obtain R' where RTrans:"R ⟼ a<νx> ≺ R'" and R'Rel'T': "(R', S') ∈ Rel'" by(blast dest: elim) from RTrans xFreshP have ParTrans: "P ∥ R ⟼ a<νx> ≺ (P ∥ R')" by(rule Early_Semantics.Par2B) moreover from PRelQ R'Rel'T' have "(P ∥ R', Q ∥ S') ∈ Rel''" by(rule Par) ultimately show ?case by blast qed next case(Free α QT') have "Q ∥ S ⟼ α ≺ QT'" by fact thus ?case proof(induct rule: parCasesF[of _ _ _ _ _ "(P, R)"]) case(cPar1 Q') have "Q ⟼ α ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟼ α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: elim) from PTrans have "P ∥ R ⟼ α ≺ P' ∥ R" by(rule Early_Semantics.Par1F) moreover from PRel RRel'T have "(P' ∥ R, Q' ∥ S) ∈ Rel''" by(rule Par) ultimately show ?case by blast next case(cPar2 S') have "S ⟼ α ≺ S'" by fact with RSimT obtain R' where RTrans: "R ⟼ α ≺ R'" and RRel: "(R', S') ∈ Rel'" by(blast dest: elim) from RTrans have "P ∥ R ⟼ α ≺ P ∥ R'" by(rule Early_Semantics.Par2F) moreover from PRelQ RRel have "(P ∥ R', Q ∥ S') ∈ Rel''" by(rule Par) ultimately show ?case by blast next case(cComm1 Q' S' a b) have "Q ⟼ a<b> ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟼a<b> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) have "S ⟼ a[b] ≺ S'" by fact with RSimT obtain R' where RTrans: "R ⟼a[b] ≺ R'" and RRel: "(R', S') ∈ Rel'" by(blast dest: elim) from PTrans RTrans have "P ∥ R ⟼ τ ≺ P' ∥ R'" by(rule Early_Semantics.Comm1) moreover from P'RelQ' RRel have "(P' ∥ R', Q' ∥ S') ∈ Rel''" by(rule Par) ultimately show ?case by blast next case(cComm2 Q' S' a b) have "Q ⟼ (OutputR a b) ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟼a[b] ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: elim) have "S ⟼ a<b> ≺ S'" by fact with RSimT obtain R' where RTrans: "R ⟼a<b> ≺ R'" and R'Rel'T': "(R', S') ∈ Rel'" by(blast dest: elim) from PTrans RTrans have "P ∥ R ⟼ τ ≺ P' ∥ R'" by(rule Early_Semantics.Comm2) moreover from PRel R'Rel'T' have "(P' ∥ R', Q' ∥ S') ∈ Rel''" by(rule Par) ultimately show ?case by blast next case(cClose1 Q' S' a x) have "x ♯ (P, R)" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ have "Q ⟼ a<x> ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟼a<x> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) have "S ⟼ a<νx> ≺ S'" by fact with RSimT xFreshR obtain R' where RTrans: "R ⟼a<νx> ≺ R'" and R'Rel'T': "(R', S') ∈ Rel'" by(blast dest: elim) from PTrans RTrans xFreshP have "P ∥ R ⟼ τ ≺ <νx>(P' ∥ R')" by(rule Early_Semantics.Close1) moreover from P'RelQ' R'Rel'T' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ S')) ∈ Rel''" by(blast intro: Par Res) ultimately show ?case by blast next case(cClose2 Q' S' a x) have "x ♯ (P, R)" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ have "Q ⟼ a<νx> ≺ Q'" by fact with PSimQ xFreshP obtain P' where PTrans: "P ⟼a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) have "S ⟼ a<x> ≺ S'" by fact with RSimT obtain R' where RTrans: "R ⟼a<x> ≺ R'" and R'Rel'T': "(R', S') ∈ Rel'" by(blast dest: elim) from PTrans RTrans xFreshR have "P ∥ R ⟼ τ ≺ <νx>(P' ∥ R')" by(rule Early_Semantics.Close2) moreover from P'RelQ' R'Rel'T' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ S')) ∈ 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: "⋀S T U. (S, T) ∈ Rel ⟹ (S ∥ U, T ∥ U) ∈ Rel'" and Res: "⋀S T x. (S, T) ∈ Rel' ⟹ (<νx>S, <νx>T) ∈ 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 ultimately show ?thesis using Res by(rule parCompose) 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 ResSet: "⋀(R::pi) (S::pi) (y::name). (R, S) ∈ Rel ⟹ (<νy>R, <νy>S) ∈ Rel'" and RelRel': "Rel ⊆ Rel'" and EqvtRel: "eqvt Rel" and EqvtRel': "eqvt Rel'" shows "<νx>P ↝[Rel'] <νx>Q" proof - from EqvtRel' show ?thesis proof(induct rule: simCasesCont[where C = "(P, x)"]) case(Bound a y Q') have Trans: "<νx>Q ⟼a<νy> ≺ Q'" by fact have "y ♯ (P, x)" by fact hence yineqx: "y ≠ x" and yFreshP: "y ♯ (P::pi)" by simp+ from Trans yineqx show ?case proof(induct rule: resCasesB) case(Open Q') have QTrans: "Q ⟼(a::name)[x] ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟼ a[x] ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) have "<νx>P ⟼a<νy> ≺ ([(y, x)] ∙ P')" proof - have aineqx: "a ≠ x" by fact with PTrans have "<νx>P ⟼a<νx> ≺ P'" by(rule TransitionsEarly.Open) moreover have "a<νx> ≺ P' = a<νy> ≺ ([(y, x)] ∙ P')" proof - from PTrans yFreshP have yFreshP': "y ♯ P'" by(force intro: freshTransition) thus ?thesis by(simp add: alphaBoundOutput name_swap) qed ultimately show ?thesis by simp qed moreover from EqvtRel P'RelQ' RelRel' have "([(y, x)] ∙ P', [(y, x)] ∙ Q') ∈ Rel'" by(blast intro: eqvtRelI) ultimately show ?case by blast next case(Res Q') have QTrans: "Q ⟼a<νy> ≺ Q'" by fact with PSimQ yFreshP obtain P' where PTrans: "P ⟼a<νy> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) have xineqa: "x ≠ a" by fact with PTrans yineqx have ResTrans: "<νx>P ⟼a<νy> ≺ (<νx>P')" by(blast intro: ResB) moreover from P'RelQ' have "((<νx>P'), (<νx>Q')) ∈ Rel'" by(rule ResSet) ultimately show "∃P'. <νx>P ⟼ a<νy> ≺ P' ∧ (P', (<νx>Q')) ∈ Rel'" by blast qed next case(Free α Q') have Trans: "<νx>Q ⟼ α ≺ Q'" by fact have "∃c::name. c ♯ (P, Q, Q', α)" by(blast intro: name_exists_fresh) then obtain c::name where cFreshQ: "c ♯ Q" and cFreshAlpha: "c ♯ α" and cFreshQ': "c ♯ Q'" and cFreshP: "c ♯ P" by(force simp add: fresh_prod) from cFreshP have "<νx>P = <νc>([(x, c)] ∙ P)" by(simp add: alphaRes) moreover have "∃P'.<νc>([(x, c)] ∙ P) ⟼ α ≺ P' ∧ (P', Q') ∈ Rel'" proof - from Trans cFreshQ have "<νc>([(x, c)] ∙ Q) ⟼α ≺ Q'" by(simp add: alphaRes) moreover from EqvtRel PSimQ have "([(x, c)] ∙ P) ↝[Rel] ([(x, c)] ∙ Q)" by(blast intro: eqvtI) ultimately show ?thesis using cFreshAlpha apply - apply(erule resCasesF) apply auto by(blast intro: ResF ResSet dest: elim) qed ultimately show "∃P'.<νx>P ⟼ α ≺ P' ∧ (P', Q') ∈ Rel'" by auto qed qed lemma resChainI: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" and lst :: "name list" assumes eqvtRel: "eqvt Rel" and Res: "⋀R S x. (R, S) ∈ Rel ⟹ (<νx>R, <νx>S) ∈ Rel" and PRelQ: "P ↝[Rel] Q" shows "(resChain lst) P ↝[Rel] (resChain lst) Q" proof - show ?thesis proof(induct lst) (* Base case *) from PRelQ show "resChain [] P ↝[Rel] resChain [] Q" by simp next (* Inductive step *) fix a lst assume IH: "(resChain lst P) ↝[Rel] (resChain lst Q)" moreover from Res have "⋀P Q a. (P, Q) ∈ Rel ⟹ (<νa>P, <νa>Q) ∈ Rel" by simp moreover have "Rel ⊆ Rel" by simp ultimately have "<νa>(resChain lst P) ↝[Rel] <νa>(resChain lst Q)" using eqvtRel by(rule_tac resPres) thus "resChain (a # lst) P ↝[Rel] resChain (a # lst) Q" by simp qed qed lemma bangPres: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" assumes PRelQ: "(P, Q) ∈ Rel" and Sim: "⋀R S. (R, S) ∈ Rel ⟹ R ↝[Rel] S" 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' ∧ (P', Q') ∈ 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(Par1B 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': "(P', Q') ∈ Rel" by(blast dest: elim) from PTrans xFreshR have "P ∥ R ⟼ a<νx> ≺ (P' ∥ R)" by(force intro: Early_Semantics.Par1B) moreover from P'RelQ' PBRQ have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel" by(rule Rel.BRPar) ultimately show "∃P'. P ∥ R ⟼a<νx> ≺ P' ∧ (P', Q' ∥ !Q) ∈ 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: alphaBoundOutput) moreover from PRelQ have "P ↝[Rel] Q" by(rule Sim) ultimately obtain P' where PTrans: "P ⟼a<νy> ≺ P'" and P'RelQ': "(P', [(x, y)] ∙ Q') ∈ Rel" using ‹y ♯ P› by(blast dest: elim) from PTrans ‹y ♯ R› have "P ∥ R ⟼a<νy> ≺ (P' ∥ R)" by(force intro: Early_Semantics.Par1B) moreover from P'RelQ' PBRQ have "(P' ∥ R, ([(x, y)] ∙ Q') ∥ !Q) ∈ bangRel Rel" by(rule Rel.BRPar) with ‹x ♯ Q› ‹y ♯ Q› have "(P' ∥ R, ([(y, x)] ∙ Q') ∥ !([(y, x)] ∙ Q)) ∈ bangRel Rel" by(simp add: name_fresh_fresh name_swap) ultimately show "∃P'. P ∥ R ⟼a<νy> ≺ P' ∧ (P', ([(y, x)] ∙ Q') ∥ !([(y, x)] ∙ Q)) ∈ bangRel Rel" by blast qed qed next case(Par1F α 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: elim) from PTrans have "P ∥ R ⟼ α ≺ P' ∥ R" by(rule TransitionsEarly.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(Par2B 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 show "?Sim (P ∥ R) (a<νx> ≺ (Q ∥ Q'))" proof(auto simp add: residual.inject alpha') from RBRQ have "?Sim R (a<νx> ≺ Q')" by(rule IH) with xFreshR obtain R' where RTrans: "R ⟼ a<νx> ≺ R'" and R'BRQ': "(R', Q') ∈ (bangRel Rel)" by(metis elim) from RTrans xFreshP have "P ∥ R ⟼ a<νx> ≺ (P ∥ R')" by(auto intro: Early_Semantics.Par2B) moreover from PRelQ R'BRQ' have "(P ∥ R', Q ∥ Q') ∈ (bangRel Rel)" by(rule Rel.BRPar) ultimately show "∃P'. P ∥ R ⟼ a<νx> ≺ P' ∧ (P', Q ∥ Q') ∈ 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: alphaBoundOutput) with ‹y ♯ R› obtain R' where RTrans: "R ⟼ a<νy> ≺ R'" and R'BRQ': "(R', ([(x, y)] ∙ Q')) ∈ (bangRel Rel)" by(metis elim) from RTrans ‹y ♯ P› have "P ∥ R ⟼ a<νy> ≺ (P ∥ R')" by(auto intro: Early_Semantics.Par2B) moreover from PRelQ R'BRQ' have "(P ∥ R', Q ∥ ([(x, y)] ∙ Q')) ∈ (bangRel Rel)" by(rule Rel.BRPar) with ‹y ♯ Q› ‹x ♯ Q› have "(P ∥ R', ([(y, x)] ∙ Q) ∥ ([(y, x)] ∙ Q')) ∈ (bangRel Rel)" by(simp add: name_swap name_fresh_fresh) ultimately show "∃P'. P ∥ R ⟼ a<νy> ≺ P' ∧ (P', ([(y, x)] ∙ Q) ∥ ([(y, x)] ∙ Q')) ∈ bangRel Rel" by blast qed qed next case(Par2F α 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 elim) 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 TransitionsEarly.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(Comm1 a Q' b Q'' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a[b] ≺ Q'')" by simp have QTrans: "Q ⟼a<b> ≺ 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 RBRQ: "(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 ⟼ a<b> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) from IH RBRQ have RTrans: "∃R'. R ⟼ a[b] ≺ R' ∧ (R', Q'') ∈ bangRel Rel" by(metis elim) 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' ∥ R'" by(rule TransitionsEarly.Comm1) moreover from P'RelQ' 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(Comm2 a b Q' Q'') hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a<b> ≺ Q'')" by simp have QTrans: "Q ⟼ a[b] ≺ 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 RBRQ: "(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 ⟼ a[b] ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: elim) from IH RBRQ have RTrans: "∃R'. R ⟼ a<b> ≺ R' ∧ (R', Q'') ∈ bangRel Rel" by(metis elim) 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' ∥ R'" by(rule TransitionsEarly.Comm2) moreover from P'RelQ' 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(Close1 a x Q' Q'' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟶ ?Sim Pa (a<νx> ≺ Q'')" by simp have QTrans: "Q ⟼ a<x> ≺ Q'" by fact have xFreshQ: "x ♯ Q" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" by fact moreover have xFreshPa: "x ♯ Pa" by fact ultimately show ?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" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ 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(blast dest: elim) from RBRQ xFreshR IH have "∃R'. R ⟼a<νx> ≺ R' ∧ (R', Q'') ∈ bangRel Rel" by(metis elim) then obtain R' where RTrans: "R ⟼a<νx> ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel" by blast from PTrans RTrans xFreshP have "P ∥ R ⟼τ ≺ <νx>(P' ∥ R')" by(rule Early_Semantics.Close1) moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ Q'')) ∈ bangRel Rel" by(force intro: Rel.BRPar BRRes) ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', <νx>(Q' ∥ Q'')) ∈ bangRel Rel" by blast qed qed next case(Close2 a x Q' Q'' Pa P) hence IH: "⋀Pa. (Pa, !Q) ∈ bangRel Rel ⟹ ?Sim Pa (a<x> ≺ Q'')" by simp have QTrans: "Q ⟼ a<νx> ≺ Q'" by fact have xFreshQ: "x ♯ Q" by fact have "(Pa, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ 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" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ 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(blast dest: elim) from RBRQ IH have "∃R'. R ⟼a<x> ≺ R' ∧ (R', Q'') ∈ bangRel Rel" by auto then obtain R' where RTrans: "R ⟼ a<x> ≺ R'" and R'RelQ'': "(R', Q'') ∈ bangRel Rel" by blast from PTrans RTrans xFreshR have "P ∥ R ⟼ τ ≺ <νx>(P' ∥ R')" by(rule Early_Semantics.Close2) moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ Q'')) ∈ bangRel Rel" by(force intro: Rel.BRPar BRRes) ultimately show "∃P'. P ∥ R ⟼ τ ≺ P' ∧ (P', <νx>(Q' ∥ Q'')) ∈ bangRel Rel" by blast qed qed next case(Bang 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: TransitionsEarly.Bang) qed qed } moreover from PRelQ have "(!P, !Q) ∈ bangRel Rel" by(rule BRBang) ultimately show ?thesis by(auto simp add: strongSimEarly_def) qed end