(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Weak_Late_Step_Sim_Pres imports Weak_Late_Step_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(induct rule: simCases) case(Bound Q' a y) have "τ.(Q) ⟼a<νy> ≺ Q'" by fact hence False by auto thus ?case by simp next case(Input Q' a x) 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 using PRelQ proof(induct rule: tauCases, auto simp add: pi.inject residual.inject) have "τ.(P) ⟹⇩_{l}τ ≺ P" by(rule Weak_Late_Step_Semantics.Tau) moreover assume "(P, Q') ∈ Rel" ultimately show "∃P'. τ.(P) ⟹⇩_{l}τ ≺ P' ∧ (P', Q') ∈ Rel" by blast qed qed lemma inputPres: fixes P :: pi and Q :: pi and a :: name and x :: 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" proof - show ?thesis using Eqvt proof(induct rule: simCasesCont[of _ "(P, a, x, Q)"]) case(Bound Q' b y) have "a<x>.Q ⟼b<νy> ≺ Q'" by fact hence False by auto thus ?case by simp next case(Input Q' b y) have "y ♯ (P, a, x, Q)" by fact hence yFreshP: "(y::name) ♯ P" and yineqx: "y ≠ x" and "y ≠ a" and "y ♯ Q" by(simp add: fresh_prod)+ have "a<x>.Q ⟼b<y> ≺ Q'" by fact thus ?case using ‹y ≠ a› ‹y ≠ x› ‹y ♯ Q› proof(induct rule: inputCases, auto simp add: subject.inject) have "∀u. ∃P'. a<x>.P ⟹⇩_{l}u in ([(x, y)] ∙ P)→a<y> ≺ P' ∧ (P', ([(x, y)] ∙ Q)[y::=u]) ∈ Rel" proof(rule allI) fix u have "a<x>.P ⟹⇩_{l}u in ([(x, y)] ∙ P)→a<y> ≺ ([(x, y)] ∙ P)[y::=u]" (is "?goal") proof - from yFreshP have "a<x>.P = a<y>.([(x, y)] ∙ P)" by(rule Agent.alphaInput) moreover have "a<y>.([(x, y)] ∙ P) ⟹⇩_{l}u in ([(x, y)] ∙ P)→a<y> ≺ ([(x, y)] ∙ P)[y::=u]" by(rule Weak_Late_Step_Semantics.Input) ultimately show ?goal by(simp add: name_swap) qed moreover have "(([(x, y)] ∙ P)[y::=u], ([(x, y)] ∙ Q)[y::=u]) ∈ Rel" proof - from PRelQ have "(P[x::=u], Q[x::=u]) ∈ Rel" by auto with ‹y ♯ P› ‹y ♯ Q› show ?thesis by(simp add: renaming) qed ultimately show "∃P'. a<x>.P ⟹⇩_{l}u in ([(x, y)] ∙ P)→a<y> ≺ P' ∧ (P', ([(x, y)] ∙ Q)[y::=u]) ∈ Rel" by blast qed thus "∃P''. ∀u. ∃P'. a<x>.P ⟹⇩_{l}u in P''→a<y> ≺ P' ∧ (P', ([(x, y)] ∙ Q)[y::=u]) ∈ Rel" by blast qed next case(Free Q' α) have "a<x>.Q ⟼α ≺ Q'" by fact hence False by auto thus ?case by simp 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 Q' c x) have "a{b}.Q ⟼c<νx> ≺ Q'" by fact hence False by auto thus ?case by simp next case(Input Q' c x) 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 using PRelQ proof(induct rule: outputCases, auto simp add: pi.inject residual.inject) have "a{b}.P ⟹⇩_{l}a[b] ≺ P" by(rule Weak_Late_Step_Semantics.Output) moreover assume "(P, Q') ∈ Rel" ultimately show "∃P'. a{b}.P ⟹⇩_{l}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 Q' c x) have "x ♯ [a⌢b]P" by fact hence xFreshP: "(x::name) ♯ 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 ⟹⇩_{l}c<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have "[a⌢a]P ⟹⇩_{l}c<νx> ≺ P'" by(rule Weak_Late_Step_Semantics.Match) moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast ultimately show ?case by blast qed next case(Input Q' c x) have "x ♯ [a⌢b]P" by fact hence xFreshP: "(x::name) ♯ 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 L1: "∀u. ∃P'. P ⟹⇩_{l}u in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" by(blast dest: simE) have "∀u. ∃P'. [a⌢a]P ⟹⇩_{l}u in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" proof(rule allI) fix u from L1 obtain P' where PTrans: "P ⟹⇩_{l}u in P''→c<x> ≺ P'" and P'RelQ': "(P', Q'[x::=u]) ∈ Rel" by blast from PTrans have "[a⌢a]P ⟹⇩_{l}u in P''→c<x> ≺ P'" by(rule Weak_Late_Step_Semantics.Match) with P'RelQ' RelRel' show "∃P'. [a⌢a]P ⟹⇩_{l}u in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" by blast qed thus ?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 ⟹⇩_{l}α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have "[a⌢a]P ⟹⇩_{l}α ≺ P'" by(rule Weak_Late_Step_Semantics.Match) with PRel RelRel' 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: weakStepSimDef) next assume aineqb: "a≠b" show ?thesis proof(induct rule: simCases) case(Bound Q' c x) have "x ♯ [a≠b]P" by fact hence xFreshP: "(x::name) ♯ P" by simp have "[a≠b]Q ⟼ c<νx> ≺ Q'" by fact thus ?case proof(induct rule: mismatchCases) case cMismatch have "Q ⟼c<νx> ≺ Q'" by fact with PSimQ xFreshP obtain P' where PTrans: "P ⟹⇩_{l}c<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans aineqb have "[a≠b]P ⟹⇩_{l}c<νx> ≺ P'" by(rule Weak_Late_Step_Semantics.Mismatch) moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast ultimately show ?case by blast qed next case(Input Q' c x) have "x ♯ [a≠b]P" by fact hence xFreshP: "(x::name) ♯ P" by simp have "[a≠b]Q ⟼c<x> ≺ Q'" by fact thus ?case proof(induct rule: mismatchCases) case cMismatch have "Q ⟼ c<x> ≺ Q'" by fact with PSimQ xFreshP obtain P'' where L1: "∀u. ∃P'. P ⟹⇩_{l}u in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" by(blast dest: simE) have "∀u. ∃P'. [a≠b]P ⟹⇩_{l}u in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" proof(rule allI) fix u from L1 obtain P' where PTrans: "P ⟹⇩_{l}u in P''→c<x> ≺ P'" and P'RelQ': "(P', Q'[x::=u]) ∈ Rel" by blast from PTrans aineqb have "[a≠b]P ⟹⇩_{l}u in P''→c<x> ≺ P'" by(rule Weak_Late_Step_Semantics.Mismatch) with P'RelQ' RelRel' show "∃P'. [a≠b]P ⟹⇩_{l}u in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" by blast qed thus ?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 ⟹⇩_{l}α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans ‹a ≠ b› have "[a≠b]P ⟹⇩_{l}α ≺ P'" by(rule Weak_Late_Step_Semantics.Mismatch) with PRel RelRel' show ?case by blast qed qed qed lemma sumCompose: fixes P :: pi and Q :: pi and R :: pi and T :: pi assumes PSimQ: "P ↝<Rel> Q" and RSimT: "R ↝<Rel> T" and RelRel': "Rel ⊆ Rel'" shows "P ⊕ R ↝<Rel'> Q ⊕ T" proof(induct rule: simCases) case(Bound Q' a x) have "x ♯ P ⊕ R" by fact hence xFreshP: "(x::name) ♯ P" and xFreshR: "x ♯ R" by simp+ have "Q ⊕ T ⟼a<νx> ≺ Q'" by fact thus ?case proof(induct rule: sumCases) case cSum1 have "Q ⟼a<νx> ≺ Q'" by fact with xFreshP PSimQ obtain P' where PTrans: "P ⟹⇩_{l}a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have "P ⊕ R ⟹⇩_{l}a<νx> ≺ P'" by(rule Weak_Late_Step_Semantics.Sum1) moreover from P'RelQ' RelRel' have "(P', Q') ∈ Rel'" by blast ultimately show ?case by blast next case cSum2 have "T ⟼a<νx> ≺ Q'" by fact with xFreshR RSimT obtain R' where RTrans: "R ⟹⇩_{l}a<νx> ≺ R'" and R'RelQ': "(R', Q') ∈ Rel" by(blast dest: simE) from RTrans have "P ⊕ R ⟹⇩_{l}a<νx> ≺ R'" by(rule Weak_Late_Step_Semantics.Sum2) moreover from R'RelQ' RelRel' have "(R', Q') ∈ Rel'" by blast ultimately show ?thesis by blast qed next case(Input Q' a x) have "x ♯ P ⊕ R" by fact hence xFreshP: "(x::name) ♯ P" and xFreshR: "x ♯ R" by simp+ have "Q ⊕ T ⟼a<x> ≺ Q'" by fact thus ?case proof(induct rule: sumCases) case cSum1 have "Q ⟼a<x> ≺ Q'" by fact with xFreshP PSimQ obtain P'' where L1: "∀u. ∃P'. P ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" by(blast dest: simE) have "∀u. ∃P'. P ⊕ R ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" proof(rule allI) fix u from L1 obtain P' where PTrans: "P ⟹⇩_{l}u in P''→a<x> ≺ P'" and P'RelQ': "(P', Q'[x::=u]) ∈ Rel" by blast from PTrans have "P ⊕ R ⟹⇩_{l}u in P''→a<x> ≺ P'" by(rule Weak_Late_Step_Semantics.Sum1) with P'RelQ' RelRel' show "∃P'. P ⊕ R ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" by blast qed thus ?case by blast next case cSum2 have "T ⟼a<x> ≺ Q'" by fact with xFreshR RSimT obtain R'' where L1: "∀u. ∃R'. R ⟹⇩_{l}u in R''→a<x> ≺ R' ∧ (R', Q'[x::=u]) ∈ Rel" by(blast dest: simE) have "∀u. ∃P'. P ⊕ R ⟹⇩_{l}u in R''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" proof(rule allI) fix u from L1 obtain R' where RTrans: "R ⟹⇩_{l}u in R''→a<x> ≺ R'" and R'RelQ': "(R', Q'[x::=u]) ∈ Rel" by blast from RTrans have "P ⊕ R ⟹⇩_{l}u in R''→a<x> ≺ R'" by(rule Weak_Late_Step_Semantics.Sum2) with R'RelQ' RelRel' show "∃P'. P ⊕ R ⟹⇩_{l}u in R''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" by blast qed thus ?case by blast qed next case(Free Q' α) have "Q ⊕ T ⟼α ≺ Q'" by fact thus ?case proof(induct rule: sumCases) case cSum1 have "Q ⟼α ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟹⇩_{l}α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have "P ⊕ R ⟹⇩_{l}α ≺ P'" by(rule Weak_Late_Step_Semantics.Sum1) with RelRel' PRel show ?case by blast next case cSum2 have "T ⟼α ≺ Q'" by fact with RSimT obtain R' where RTrans: "R ⟹⇩_{l}α ≺ R'" and RRel: "(R', Q') ∈ Rel" by(blast dest: simE) from RTrans have "P ⊕ R ⟹⇩_{l}α ≺ R'" by(rule Weak_Late_Step_Semantics.Sum2) with RelRel' RRel show ?case by blast qed qed lemma sumPres: fixes P :: pi and Q :: pi and R :: pi assumes PSimQ: "P ↝<Rel> Q" and Id: "Id ⊆ Rel" and RelRel': "Rel ⊆ Rel'" shows "P ⊕ R ↝<Rel'> Q ⊕ R" proof - from Id have Refl: "R ↝<Rel> R" by(rule reflexive) from PSimQ Refl RelRel' show ?thesis by(rule sumCompose) qed lemma parPres: fixes P :: pi and Q :: pi and R :: pi 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" using EqvtRel' proof(induct rule: simCasesCont[where C="(P, Q, R)"]) case(Bound Q' a x) have "x ♯ (P, Q, R)" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" and "x ♯ Q" by simp+ from ‹Q ∥ R ⟼ a<νx> ≺ Q'› ‹x ♯ Q› ‹x ♯ R› show ?case proof(induct rule: parCasesB) case(cPar1 Q') have QTrans: "Q ⟼ a<νx> ≺ Q'" by fact from xFreshP PSimQ QTrans obtain P' where PTrans:"P ⟹⇩_{l}a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans xFreshR have "P ∥ R ⟹⇩_{l}a<νx> ≺ (P' ∥ R)" by(rule Weak_Late_Step_Semantics.Par1B) moreover from P'RelQ' have "(P' ∥ R, Q' ∥ R) ∈ Rel'" by(rule Par) ultimately show ?case by blast next case(cPar2 R') have RTrans: "R ⟼ a<νx> ≺ R'" by fact hence "R ⟹⇩_{l}a<νx> ≺ R'" by(auto simp add: weakTransition_def dest: Weak_Late_Step_Semantics.singleActionChain) with xFreshP xFreshR have ParTrans: "P ∥ R ⟹⇩_{l}a<νx> ≺ P ∥ R'" by(blast intro: Weak_Late_Step_Semantics.Par2B) moreover from PRelQ have "(P ∥ R', Q ∥ R') ∈ Rel'" by(rule Par) ultimately show ?case by blast qed next case(Input Q' a x) have "x ♯ (P, Q, R)" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" and "x ♯ Q" by simp+ from ‹Q ∥ R ⟼a<x> ≺ Q'› ‹x ♯ Q› ‹x ♯ R› show ?case proof(induct rule: parCasesB) case(cPar1 Q') have QTrans: "Q ⟼a<x> ≺ Q'" by fact from xFreshP PSimQ QTrans obtain P'' where L1: "∀u. ∃P'. P ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" by(blast dest: simE) have "∀u. ∃P'. P ∥ R ⟹⇩_{l}u in (P'' ∥ R)→a<x> ≺ P' ∧ (P', Q'[x::=u] ∥ R[x::=u]) ∈ Rel'" proof(rule allI) fix u from L1 obtain P' where PTrans:"P ⟹⇩_{l}u in P''→a<x> ≺ P'" and P'RelQ': "(P', Q'[x::=u]) ∈ Rel" by blast from PTrans xFreshR have "P ∥ R ⟹⇩_{l}u in (P'' ∥ R)→a<x> ≺ (P' ∥ R)" by(rule Weak_Late_Step_Semantics.Par1B) moreover from P'RelQ' have "(P' ∥ R, Q'[x::=u] ∥ R) ∈ Rel'" by(rule Par) ultimately show "∃P'. P ∥ R ⟹⇩_{l}u in (P'' ∥ R)→a<x> ≺ P' ∧ (P', Q'[x::=u] ∥ (R[x::=u])) ∈ Rel'" using xFreshR by(force simp add: forget) qed thus ?case by force next case(cPar2 R') have RTrans: "R ⟼a<x> ≺ R'" by fact have "∀u. ∃P'. P ∥ R ⟹⇩_{l}u in (P ∥ R')→a<x> ≺ P' ∧ (P', Q ∥ R'[x::=u]) ∈ Rel'" proof fix u from RTrans have "R ⟹⇩_{l}u in R'→a<x> ≺ R'[x::=u]" by(rule Weak_Late_Step_Semantics.singleActionChain) hence "P ∥ R ⟹⇩_{l}u in P ∥ R'→a<x> ≺ P ∥ R'[x::=u]" using ‹x ♯ P› by(rule Weak_Late_Step_Semantics.Par2B) moreover from PRelQ have "(P ∥ R'[x::=u], Q ∥ R'[x::=u]) ∈ Rel'" by(rule Par) ultimately show "∃P'. P ∥ R ⟹⇩_{l}u in (P ∥ R')→a<x> ≺ P' ∧ (P', Q ∥ R'[x::=u]) ∈ Rel'" by blast qed thus ?case using ‹x ♯ Q› by(fastforce simp add: forget) qed next case(Free QR' α) have "Q ∥ R ⟼ α ≺ QR'" 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 ⟹⇩_{l}α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have Trans: "P ∥ R ⟹⇩_{l}α ≺ P' ∥ R" by(rule Weak_Late_Step_Semantics.Par1F) moreover from PRel have "(P' ∥ R, Q' ∥ R) ∈ Rel'" by(blast intro: Par) ultimately show ?case by blast next case(cPar2 R') have "R ⟼ α ≺ R'" by fact hence "R ⟹⇩_{l}α ≺ R'" by(rule Weak_Late_Step_Semantics.singleActionChain) hence "P ∥ R ⟹⇩_{l}α ≺ (P ∥ R')" by(rule Weak_Late_Step_Semantics.Par2F) moreover from PRelQ have "(P ∥ R', Q ∥ R') ∈ Rel'" by(blast intro: Par) ultimately show ?case by blast next case(cComm1 Q' R' a b x) have QTrans: "Q ⟼ a<x> ≺ Q'" and RTrans: "R ⟼ a[b] ≺ R'" by fact+ have "x ♯ (P, R)" by fact hence xFreshP: "x ♯ P" by(simp add: fresh_prod) from PSimQ QTrans xFreshP obtain P' P'' where PTrans: "P ⟹⇩_{l}b in P''→a<x> ≺ P'" and P'RelQ': "(P', Q'[x::=b]) ∈ Rel" by(blast dest: simE) from RTrans have "R ⟹⇩_{l}a[b] ≺ R'" by(rule Weak_Late_Step_Semantics.singleActionChain) with PTrans have "P ∥ R ⟹⇩_{l}τ ≺ P' ∥ R'" by(rule Weak_Late_Step_Semantics.Comm1) moreover from P'RelQ' have "(P' ∥ R', Q'[x::=b] ∥ R') ∈ Rel'" by(rule Par) ultimately show ?case by blast next case(cComm2 Q' R' a b x) have QTrans: "Q ⟼a[b] ≺ Q'" and RTrans: "R ⟼a<x> ≺ R'" by fact+ have "x ♯ (P, R)" by fact hence xFreshR: "x ♯ R" by(simp add: fresh_prod) from PSimQ QTrans obtain P' where PTrans: "P ⟹⇩_{l}a[b] ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from RTrans have "R ⟹⇩_{l}b in R'→a<x> ≺ R'[x::=b]" by(rule Weak_Late_Step_Semantics.singleActionChain) with PTrans have "P ∥ R ⟹⇩_{l}τ ≺ P' ∥ R'[x::=b]" by(rule Weak_Late_Step_Semantics.Comm2) moreover from PRel have "(P' ∥ R'[x::=b], Q' ∥ R'[x::=b]) ∈ Rel'" by(rule Par) ultimately show ?case by blast next case(cClose1 Q' R' a x y) have QTrans: "Q ⟼a<x> ≺ Q'" and RTrans: "R ⟼a<νy> ≺ R'" by fact+ have "x ♯ (P, R)" and "y ♯ (P, R)" by fact+ hence xFreshP: "x ♯ P" and yFreshR: "y ♯ R" and yFreshP: "y ♯ P" by(simp add: fresh_prod)+ from PSimQ QTrans xFreshP obtain P' P'' where PTrans: "P ⟹⇩_{l}y in P''→a<x> ≺ P'" and P'RelQ': "(P', Q'[x::=y]) ∈ Rel" by(blast dest: simE) from RTrans have "R ⟹⇩_{l}a<νy> ≺ R'" by(auto simp add: weakTransition_def dest: Weak_Late_Step_Semantics.singleActionChain) with PTrans have Trans: "P ∥ R ⟹⇩_{l}τ ≺ <νy>(P' ∥ R')" using yFreshP yFreshR by(rule Weak_Late_Step_Semantics.Close1) moreover from P'RelQ' have "(<νy>(P' ∥ R'), <νy>(Q'[x::=y] ∥ R')) ∈ Rel'" by(blast intro: Par Res) ultimately show ?case by blast next case(cClose2 Q' R' a x y) have QTrans: "Q ⟼a<νy> ≺ Q'" and RTrans: "R ⟼a<x> ≺ R'" by fact+ have "x ♯ (P, R)" and "y ♯ (P, R)" by fact+ hence xFreshR: "x ♯ R" and yFreshP: "y ♯ P" and yFreshR: "y ♯ R" by(simp add: fresh_prod)+ from PSimQ QTrans yFreshP obtain P' where PTrans: "P ⟹⇩_{l}a<νy> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from RTrans have "R ⟹⇩_{l}y in R'→a<x> ≺ R'[x::=y]" by(rule Weak_Late_Step_Semantics.singleActionChain) with PTrans have "P ∥ R ⟹⇩_{l}τ ≺ <νy>(P' ∥ R'[x::=y])" using yFreshP yFreshR by(rule Weak_Late_Step_Semantics.Close2) moreover from P'RelQ' have "(<νy>(P' ∥ R'[x::=y]), <νy>(Q' ∥ R'[x::=y])) ∈ Rel'" by(blast intro: Par Res) ultimately show ?case by blast 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" proof - from EqvtRel' show ?thesis proof(induct rule: simCasesCont[of _ "(P, Q, x)"]) case(Bound Q' a y) have Trans: "<νx>Q ⟼a<νy> ≺ Q'" by fact have "y ♯ (P, Q, x)" by fact hence yineqx: "y ≠ x" and yFreshP: "y ♯ P" and "y ♯ Q" by(simp add: fresh_prod)+ from Trans ‹y ≠ x› ‹y ♯ Q› show ?case proof(induct rule: resCasesB) case(cOpen a Q') have QTrans: "Q ⟼a[x] ≺ Q'" and aineqx: "a ≠ x" by fact+ from PSimQ QTrans obtain P' where PTrans: "P ⟹⇩_{l}a[x] ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) have "<νx>P ⟹⇩_{l}a<νy> ≺ ([(y, x)] ∙ P')" proof - from PTrans aineqx have "<νx>P ⟹⇩_{l}a<νx> ≺ P'" by(rule Weak_Late_Step_Semantics.Open) moreover from PTrans yFreshP have "y ♯ P'" by(force intro: Weak_Late_Step_Semantics.freshTransition) ultimately show ?thesis by(simp add: alphaBoundResidual name_swap) 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(cRes Q') have QTrans: "Q ⟼a<νy> ≺ Q'" by fact from ‹x ♯ BoundOutputS a› have "x ≠ a" by simp from PSimQ yFreshP QTrans obtain P' where PTrans: "P ⟹⇩_{l}a<νy> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans ‹x ≠ a› yineqx yFreshP have ResTrans: "<νx>P ⟹⇩_{l}a<νy> ≺ (<νx>P')" by(blast intro: Weak_Late_Step_Semantics.ResB) moreover from P'RelQ' have "((<νx>P'), (<νx>Q')) ∈ Rel'" by(rule ResRel) ultimately show ?case by blast qed next case(Input Q' a y) have "y ♯ (P, Q, x)" by fact hence yineqx: "y ≠ x" and yFreshP: "y ♯ P" and "y ♯ Q" by(simp add: fresh_prod)+ have "<νx>Q ⟼a<y> ≺ Q'" by fact thus ?case using yineqx ‹y ♯ Q› proof(induct rule: resCasesB) case(cOpen a Q') thus ?case by simp next case(cRes Q') have QTrans: "Q ⟼a<y> ≺ Q'" by fact from ‹x ♯ InputS a› have "x ≠ a" by simp from PSimQ QTrans yFreshP obtain P'' where L1: "∀u. ∃P'. P ⟹⇩_{l}u in P''→a<y> ≺ P' ∧ (P', Q'[y::=u]) ∈ Rel" by(blast dest: simE) have "∀u. ∃P'. <νx>P ⟹⇩_{l}u in (<νx>P'')→a<y> ≺ P' ∧ (P', (<νx>Q')[y::=u]) ∈ Rel'" proof(rule allI) fix u show "∃P'. <νx>P ⟹⇩_{l}u in <νx>P''→a<y> ≺ P' ∧ (P', (<νx>Q')[y::=u]) ∈ Rel'" proof(cases "x=u") assume xequ: "x=u" have "∃c::name. c ♯ (P, P'', Q', x, y, a)" by(blast intro: name_exists_fresh) then obtain c::name where cFreshP: "c ♯ P" and cFreshP'': "c ♯ P''" and cFreshQ': "c ♯ Q'" and cineqx: "c ≠ x" and cineqy: "c ≠ y" and cineqa: "c ≠ a" by(force simp add: fresh_prod) from L1 obtain P' where PTrans: "P ⟹⇩_{l}c in P''→a<y> ≺ P'" and P'RelQ': "(P', Q'[y::=c]) ∈ Rel" by blast have "<νx>P ⟹⇩_{l}u in (<νx>P'')→a<y> ≺ <νc>([(x, c)] ∙ P')" proof - from PTrans yineqx ‹x ≠ a› cineqx have "<νx>P ⟹⇩_{l}c in (<νx>P'')→a<y> ≺ <νx>P'" by(blast intro: Weak_Late_Step_Semantics.ResB) hence "([(x, c)] ∙ <νx>P) ⟹⇩_{l}([(x, c)] ∙ c) in ([(x, c)] ∙ <νx>P'')→([(x, c)] ∙ a)<([(x, c)] ∙ y)> ≺ [(x, c)] ∙ <νx>P'" by(rule Weak_Late_Step_Semantics.eqvtI) moreover from cFreshP have "<νc>([(x, c)] ∙ P) = <νx>P" by(simp add: alphaRes) moreover from cFreshP'' have "<νc>([(x, c)] ∙ P'') = <νx>P''" by(simp add: alphaRes) ultimately show ?thesis using ‹x ≠ a› cineqa yineqx cineqy cineqx xequ by(simp add: name_calc) qed moreover have "(<νc>([(x, c)] ∙ P'), (<νx>Q')[y::=u]) ∈ Rel'" proof - from P'RelQ' have "(<νx>P', <νx>(Q'[y::=c])) ∈ Rel'" by(rule ResRel) with EqvtRel' have "([(x, c)] ∙ <νx>P', [(x, c)] ∙ <νx>(Q'[y::=c])) ∈ Rel'" by(rule eqvtRelI) with cineqy yineqx cineqx have "(<νc>([(x, c)] ∙ P'), (<νc>([(x, c)] ∙ Q'))[y::=x]) ∈ Rel'" by(simp add: name_calc eqvt_subs) with cFreshQ' xequ show ?thesis by(simp add: alphaRes) qed ultimately show ?thesis by blast next assume xinequ: "x ≠ u" from L1 obtain P' where PTrans: "P ⟹⇩_{l}u in P''→a<y> ≺ P'" and P'RelQ': "(P', Q'[y::=u]) ∈ Rel" by blast from PTrans ‹x ≠ a› yineqx xinequ have "<νx>P ⟹⇩_{l}u in (<νx>P'')→a<y> ≺ <νx>P'" by(blast intro: Weak_Late_Step_Semantics.ResB) moreover from P'RelQ' xinequ yineqx have "(<νx>P', (<νx>Q')[y::=u]) ∈ Rel'" by(force intro: ResRel) ultimately show ?thesis by blast qed qed thus ?case by blast qed next case(Free Q' α) have "<νx>Q ⟼ α ≺ Q'" by fact thus ?case proof(induct rule: resCasesF) case(cRes Q') have "Q ⟼α ≺ Q'" by fact with PSimQ obtain P' where PTrans: "P ⟹⇩_{l}α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) have "<νx>P ⟹⇩_{l}α ≺ <νx>P'" proof - have xFreshAlpha: "x ♯ α" by fact with PTrans show ?thesis by(rule Weak_Late_Step_Semantics.ResF) qed moreover from P'RelQ' have "(<νx>P', <νx>Q') ∈ Rel'" by(rule ResRel) ultimately show ?case by blast qed qed qed lemma bangPres: fixes P :: pi and Q :: pi and Rel :: "(pi × pi) set" assumes PSimQ: "P ↝<Rel'> Q" and PRelQ: "(P, Q) ∈ Rel" and Sim: "⋀P Q. (P, Q) ∈ Rel ⟹ P ↝<Rel'> Q" and RelRel': "⋀P Q. (P, Q) ∈ Rel ⟹ (P, Q) ∈ Rel'" and eqvtRel': "eqvt Rel'" shows "!P ↝<bangRel Rel'> !Q" proof - from eqvtRel' have EqvtBangRel': "eqvt(bangRel Rel')" by(rule eqvtBangRel) from RelRel' have BRelRel': "⋀P Q. (P, Q) ∈ bangRel Rel ⟹ (P, Q) ∈ bangRel Rel'" by(auto intro: bangRelSubset) have "⋀Rs P. ⟦!Q ⟼ Rs; (P, !Q) ∈ bangRel Rel⟧ ⟹ weakStepSimAct P Rs P (bangRel Rel')" proof - fix Rs P assume "!Q ⟼ Rs" and "(P, !Q) ∈ bangRel Rel" thus "weakStepSimAct P Rs P (bangRel Rel')" proof(nominal_induct avoiding: P rule: bangInduct) case(cPar1B aa x Q' P) have QTrans: "Q ⟼aa«x» ≺ Q'" and xFreshQ: "x ♯ Q" by fact+ have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ from PRelQ have PSimQ: "P ↝<Rel'> Q" by(rule Sim) from EqvtBangRel' show ?case proof(induct rule: simActBoundCases) case(Input a) have "aa = InputS a" by fact with PSimQ QTrans xFreshP obtain P'' where L1: "∀u. ∃P'. P ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" by(blast dest: simE) have "∀u. ∃P'. P ∥ R ⟹⇩_{l}u in (P'' ∥ R)→a<x> ≺ P' ∧ (P', (Q' ∥ !Q)[x::=u]) ∈ bangRel Rel'" proof(rule allI) fix u from L1 obtain P' where PTrans: "P ⟹⇩_{l}u in P''→a<x> ≺ P'" and P'RelQ': "(P', Q'[x::=u]) ∈ Rel'" by blast from PTrans xFreshR have "P ∥ R ⟹⇩_{l}u in (P'' ∥ R)→a<x>≺ P' ∥ R" by(rule Weak_Late_Step_Semantics.Par1B) moreover have "(P' ∥ R, (Q' ∥ !Q)[x::=u]) ∈ bangRel Rel'" proof - from P'RelQ' RBangRelQ have "(P' ∥ R, Q'[x::=u] ∥ !Q) ∈ bangRel Rel'" by(blast intro: BRelRel' Rel.BRPar) with xFreshQ show ?thesis by(force simp add: forget) qed ultimately show "∃P'. P ∥ R ⟹⇩_{l}u in (P'' ∥ R)→a<x> ≺ P' ∧ (P', (Q' ∥ !Q)[x::=u]) ∈ bangRel Rel'" by blast qed thus ?case by blast next case(BoundOutput a) have "aa = BoundOutputS a" by fact with PSimQ QTrans xFreshP obtain P' where PTrans: "P ⟹⇩_{l}a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'" by(force dest: simE) from PTrans xFreshR have "P ∥ R ⟹⇩_{l}a<νx>≺ P' ∥ R" by(rule Weak_Late_Step_Semantics.Par1B) moreover from P'RelQ' RBangRelQ have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel'" by(blast intro: Rel.BRPar BRelRel') ultimately show ?case by blast qed qed next case(cPar1F α Q' P) have QTrans: "Q ⟼ α ≺ Q'" by fact have "(P, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ show ?case proof(induct rule: simActFreeCases) case Free from PRelQ have "P ↝<Rel'> Q" by(rule Sim) with QTrans obtain P' where PTrans: "P ⟹⇩_{l}α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'" by(blast dest: simE) from PTrans have "P ∥ R ⟹⇩_{l}α ≺ P' ∥ R" by(rule Weak_Late_Step_Semantics.Par1F) moreover from P'RelQ' RBangRelQ have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel'" by(blast intro: BRelRel' Rel.BRPar) ultimately show ?case by blast qed qed next case(cPar2B aa x Q' P) have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakStepSimAct P (aa«x» ≺ Q') P (bangRel Rel')" by fact have xFreshQ: "x ♯ Q" by fact have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by simp+ from RBangRelQ have IH: "weakStepSimAct R (aa«x» ≺ Q') R (bangRel Rel')" by(rule IH) from EqvtBangRel' show ?case proof(induct rule: simActBoundCases) case(Input a) have "aa = InputS a" by fact with xFreshR IH obtain R'' where L1: "∀u. ∃R'. R ⟹⇩_{l}u in R''→a<x> ≺ R' ∧ (R', Q'[x::=u]) ∈ bangRel Rel'" by(simp add: weakStepSimAct_def, blast) have "∀u. ∃P'. P ∥ R ⟹⇩_{l}u in (P ∥ R'')→a<x> ≺ P' ∧ (P', (Q ∥ Q')[x::=u]) ∈ bangRel Rel'" proof(rule allI) fix u from L1 obtain R' where RTrans: "R ⟹⇩_{l}u in R''→a<x> ≺ R'" and R'BangRelT': "(R', Q'[x::=u]) ∈ bangRel Rel'" by blast from RTrans xFreshP have "P ∥ R ⟹⇩_{l}u in (P ∥ R'')→a<x> ≺ P ∥ R'" by(rule Weak_Late_Step_Semantics.Par2B) moreover have "(P ∥ R', (Q ∥ Q')[x::=u]) ∈ bangRel Rel'" proof - from PRelQ R'BangRelT' have "(P ∥ R', Q ∥ Q'[x::=u]) ∈ bangRel Rel'" by(blast intro: RelRel' Rel.BRPar) with xFreshQ show ?thesis by(simp add: forget) qed ultimately show "∃P'. P ∥ R ⟹⇩_{l}u in (P ∥ R'')→a<x> ≺ P' ∧ (P', (Q ∥ Q')[x::=u]) ∈ bangRel Rel'" by blast qed thus ?case by blast next case(BoundOutput a) have "aa = BoundOutputS a" by fact with IH xFreshR obtain R' where RTrans: "R ⟹⇩_{l}a<νx> ≺ R'" and R'BangRelT': "(R', Q') ∈ bangRel Rel'" by(simp add: weakStepSimAct_def, blast) from RTrans xFreshP have "P ∥ R ⟹⇩_{l}a<νx> ≺ P ∥ R'" by(auto intro: Weak_Late_Step_Semantics.Par2B) moreover from PRelQ R'BangRelT' have "(P ∥ R', Q ∥ Q') ∈ bangRel Rel'" by(blast intro: RelRel' Rel.BRPar) ultimately show ?case by blast qed qed next case(cPar2F α Q') have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakStepSimAct P (α ≺ Q') P (bangRel Rel')" by fact+ have "(P, Q ∥ !Q) ∈ bangRel Rel" by fact thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ show ?case proof(induct rule: simActFreeCases) case Free from RBangRelQ have "weakStepSimAct R (α ≺ Q') R (bangRel Rel')" by(rule IH) then obtain R' where RTrans: "R ⟹⇩_{l}α ≺ R'" and R'BangRelQ': "(R', Q') ∈ bangRel Rel'" by(simp add: weakStepSimAct_def, blast) from RTrans have "P ∥ R ⟹⇩_{l}α ≺ P ∥ R'" by(rule Weak_Late_Step_Semantics.Par2F) moreover from PRelQ R'BangRelQ' have "(P ∥ R', Q ∥ Q') ∈ bangRel Rel'" by(blast intro: RelRel' Rel.BRPar) ultimately show ?case by blast qed qed next case(cComm1 a x Q' b Q'' P) have QTrans: "Q ⟼ a<x> ≺ Q'" by fact have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakStepSimAct P (a[b] ≺ Q'') P (bangRel Rel')" by fact+ have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" by fact hence xFreshP: "x ♯ P" by simp show ?case proof(induct rule: simActFreeCases) case Free from PRelQ have "P ↝<Rel'> Q" by(rule Sim) with QTrans xFreshP obtain P' P'' where PTrans: "P ⟹⇩_{l}b in P''→a<x> ≺ P'" and P'RelQ': "(P', Q'[x::=b]) ∈ Rel'" by(blast dest: simE) from RBangRelQ have "weakStepSimAct R (a[b] ≺ Q'') R (bangRel Rel')" by(rule IH) then obtain R' where RTrans: "R ⟹⇩_{l}a[b] ≺ R'" and R'RelT': "(R', Q'') ∈ bangRel Rel'" by(simp add: weakStepSimAct_def, blast) from PTrans RTrans have "P ∥ R ⟹⇩_{l}τ ≺ (P' ∥ R')" by(rule Weak_Late_Step_Semantics.Comm1) moreover from P'RelQ' R'RelT' have "(P' ∥ R', Q'[x::=b] ∥ Q'') ∈ bangRel Rel'" by(blast intro: RelRel' Rel.BRPar) ultimately show ?case by blast qed qed next case(cComm2 a b Q' x Q'' P) have QTrans: "Q ⟼a[b] ≺ Q'" by fact have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakStepSimAct P (a<x> ≺ Q'') P (bangRel Rel')" by fact have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" by fact hence xFreshR: "x ♯ R" by simp show ?case proof(induct rule: simActFreeCases) case Free from PRelQ have "P ↝<Rel'> Q" by(rule Sim) with QTrans obtain P' where PTrans: "P ⟹⇩_{l}a[b] ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'" by(blast dest: simE) from RBangRelQ have "weakStepSimAct R (a<x> ≺ Q'') R (bangRel Rel')" by(rule IH) with xFreshR obtain R' R'' where RTrans: "R ⟹⇩_{l}b in R''→a<x> ≺ R'" and R'BangRelQ'': "(R', Q''[x::=b]) ∈ bangRel Rel'" by(simp add: weakStepSimAct_def, blast) from PTrans RTrans have "P ∥ R ⟹⇩_{l}τ ≺ (P' ∥ R')" by(rule Weak_Late_Step_Semantics.Comm2) moreover from P'RelQ' R'BangRelQ'' have "(P' ∥ R', Q' ∥ Q''[x::=b]) ∈ bangRel Rel'" by(rule Rel.BRPar) ultimately show ?case by blast qed qed next case(cClose1 a x Q' y Q'' P) have QTrans: "Q ⟼ a<x> ≺ Q'" by fact have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakStepSimAct P (a<νy> ≺ Q'') P (bangRel Rel')" by fact have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" and "y ♯ P" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" and "y ♯ P ∥ R" by fact+ hence xFreshP: "x ♯ P" and yFreshR: "y ♯ R" and yFreshP: "y ♯ P" by simp+ show ?case proof(induct rule: simActFreeCases) case Free from PRelQ have "P ↝<Rel'> Q" by(rule Sim) with QTrans xFreshP obtain P' P'' where PTrans: "P ⟹⇩_{l}y in P''→a<x> ≺ P'" and P'RelQ': "(P', Q'[x::=y]) ∈ Rel'" by(blast dest: simE) from RBangRelQ have "weakStepSimAct R (a<νy> ≺ Q'') R (bangRel Rel')" by(rule IH) with yFreshR obtain R' where RTrans: "R ⟹⇩_{l}a<νy> ≺ R'" and R'BangRelQ'': "(R', Q'') ∈ bangRel Rel'" by(simp add: weakStepSimAct_def, blast) from PTrans RTrans yFreshP yFreshR have "P ∥ R ⟹⇩_{l}τ ≺ <νy>(P' ∥ R')" by(rule Weak_Late_Step_Semantics.Close1) moreover from P'RelQ' R'BangRelQ'' have "(<νy>(P' ∥ R'), <νy>(Q'[x::=y] ∥ Q'')) ∈ bangRel Rel'" by(force intro: Rel.BRPar Rel.BRRes) ultimately show ?case by blast qed qed next case(cClose2 a y Q' x Q'') have QTrans: "Q ⟼ a<νy> ≺ Q'" by fact have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakStepSimAct P (a<x> ≺ Q'') P (bangRel Rel')" by fact have "(P, Q ∥ !Q) ∈ bangRel Rel" and "x ♯ P" and "y ♯ P" by fact+ thus ?case proof(induct rule: BRParCases) case(BRPar P R) have PRelQ: "(P, Q) ∈ Rel" and RBangRelQ: "(R, !Q) ∈ bangRel Rel" by fact+ have "x ♯ P ∥ R" and "y ♯ P ∥ R" by fact+ hence xFreshR: "x ♯ R" and yFreshR: "y ♯ R" and yFreshP: "y ♯ P" by simp+ show ?case proof(induct rule: simActFreeCases) case Free from PRelQ have "P ↝<Rel'> Q" by(rule Sim) with QTrans yFreshP obtain P' where PTrans: "P ⟹⇩_{l}a<νy> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'" by(blast dest: simE) from RBangRelQ have "weakStepSimAct R (a<x> ≺ Q'') R (bangRel Rel')" by(rule IH) with xFreshR obtain R' R'' where RTrans: "R ⟹⇩_{l}y in R''→a<x> ≺ R'" and R'BangRelT': "(R', Q''[x::=y]) ∈ bangRel Rel'" by(simp add: weakStepSimAct_def, blast) from PTrans RTrans yFreshP yFreshR have "P ∥ R ⟹⇩_{l}τ ≺ <νy>(P' ∥ R')" by(rule Weak_Late_Step_Semantics.Close2) moreover from P'RelQ' R'BangRelT' have "(<νy>(P' ∥ R'), <νy>(Q' ∥ Q''[x::=y])) ∈ bangRel Rel'" by(force intro: Rel.BRPar Rel.BRRes) ultimately show ?case by blast qed qed next case(cBang Rs) have IH: "⋀P. (P, Q ∥ !Q) ∈ bangRel Rel ⟹ weakStepSimAct P Rs P (bangRel Rel')" by fact have "(P, !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 Rel.BRPar) hence "weakStepSimAct (P ∥ !P) Rs (P ∥ !P) (bangRel Rel')" by(rule IH) thus ?case proof(simp (no_asm) add: weakStepSimAct_def, auto) fix Q' a x assume "weakStepSimAct (P ∥ !P) (a<νx> ≺ Q') (P ∥ !P) (bangRel Rel')" and "x ♯ P" then obtain P' where PTrans: "(P ∥ !P) ⟹⇩_{l}a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ (bangRel Rel')" by(simp add: weakStepSimAct_def, blast) from PTrans have "!P ⟹⇩_{l}a<νx> ≺ P'" by(rule Weak_Late_Step_Semantics.Bang) with P'RelQ' show "∃P'. !P ⟹⇩_{l}a<νx> ≺ P' ∧ (P', Q') ∈ bangRel Rel'" by blast next fix Q' a x assume "weakStepSimAct (P ∥ !P) (a<x> ≺ Q') (P ∥ !P) (bangRel Rel')" and "x ♯ P" then obtain P'' where L1: "∀u. ∃P'. P ∥ !P ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ (bangRel Rel')" by(simp add: weakStepSimAct_def, blast) have "∀u. ∃P'. !P ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ (bangRel Rel')" proof(rule allI) fix u from L1 obtain P' where PTrans: "P ∥ !P ⟹⇩_{l}u in P''→a<x> ≺ P'" and P'RelQ': "(P', Q'[x::=u]) ∈ (bangRel Rel')" by blast from PTrans have "!P ⟹⇩_{l}u in P''→a<x> ≺ P'" by(rule Weak_Late_Step_Semantics.Bang) with P'RelQ' show "∃P'. !P ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ (bangRel Rel')" by blast qed thus "∃P''. ∀u. ∃P'. !P ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ (bangRel Rel')" by blast next fix Q' α assume "weakStepSimAct (P ∥ !P) (α ≺ Q') (P ∥ !P) (bangRel Rel')" then obtain P' where PTrans: "(P ∥ !P) ⟹⇩_{l}α ≺ P'" and P'RelQ': "(P', Q') ∈ (bangRel Rel')" by(simp add: weakStepSimAct_def, blast) from PTrans have "!P ⟹⇩_{l}α ≺ P'" by(rule Weak_Late_Step_Semantics.Bang) with P'RelQ' show "∃P'. !P ⟹⇩_{l}α ≺ P' ∧ (P', Q') ∈ (bangRel Rel')" by blast qed qed qed qed moreover from PRelQ have "(!P, !Q) ∈ bangRel Rel" by(rule Rel.BRBang) ultimately show ?thesis by(simp add: weakStepSim_def) qed end