(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Weak_Late_Sim_Pres imports Weak_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(induct rule: simCases) case(Bound Q' a x) have "τ.(Q) ⟼a<νx> ≺ 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 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 "∃P'. a{b}.P ⟹⇩_{l}⇧^{^}α ≺ P' ∧ (P', Q') ∈ Rel" using PRelQ proof(induct rule: outputCases, auto simp add: pi.inject residual.inject) have "a{b}.P ⟹⇩_{l}⇧^{^}a[b] ≺ P" by(rule 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 RelStay: "⋀P Q a. (P, Q) ∈ Rel ⟹ ([a⌢a]P, Q) ∈ Rel" 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_Semantics.Match) with P'RelQ' RelRel' show ?case by blast qed next case(Input Q' c x) 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 L1: "∀u. ∃P'. P ⟹⇩_{l}u in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel" by(force intro: 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 show ?case proof(induct rule: transitionCases) case Step have "P ⟹⇩_{l}α ≺ P'" by fact hence "[a⌢a]P ⟹⇩_{l}α ≺ P'" by(rule Weak_Late_Step_Semantics.Match) with PRel RelRel' show ?case by(force simp add: weakTransition_def) next case Stay have "α ≺ P' = τ ≺ P" by fact hence alphaEqTau: "α = τ" and PeqP': "P = P'" by(simp add: residual.inject)+ have "[a⌢a]P ⟹⇩_{l}⇧^{^}τ ≺ [a⌢a]P" by(simp add: weakTransition_def) moreover from PeqP' PRel have "([a⌢a]P, Q') ∈ Rel" by(blast intro: RelStay) ultimately show ?case using RelRel' alphaEqTau 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 RelStay: "⋀P Q a b. ⟦(P, Q) ∈ Rel; a ≠ b⟧ ⟹ ([a≠b]P, Q) ∈ Rel" 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: weakSimulation_def) 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_Semantics.Mismatch) with P'RelQ' RelRel' show ?case by blast qed next case(Input Q' c x) 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 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(force intro: 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 "a ≠ b" by fact 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 show ?case proof(induct rule: transitionCases) case Step have "P ⟹⇩_{l}α ≺ P'" by fact hence "[a≠b]P ⟹⇩_{l}α ≺ P'" using ‹a ≠ b› by(rule Weak_Late_Step_Semantics.Mismatch) with PRel RelRel' show ?case by(force simp add: weakTransition_def) next case Stay have "α ≺ P' = τ ≺ P" by fact hence alphaEqTau: "α = τ" and PeqP': "P = P'" by(simp add: residual.inject)+ have "[a≠b]P ⟹⇩_{l}⇧^{^}τ ≺ [a≠b]P" by(simp add: weakTransition_def) moreover from PeqP' PRel aineqb have "([a≠b]P, Q') ∈ Rel" by(blast intro: RelStay) ultimately show ?case using alphaEqTau RelRel' by blast qed 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 ‹eqvt Rel''› proof(induct rule: simCasesCont[where C="(P, Q, R, T)"]) case(Bound Q' a x) from ‹x ♯ (P, Q, R, T)› have "x ♯ P" and "x ♯ R" and "x ♯ Q" and "x ♯ T" by simp+ from ‹Q ∥ T ⟼ a<νx> ≺ Q'› ‹x ♯ Q› ‹x ♯ T› show ?case proof(induct rule: parCasesB) case(cPar1 Q') from PSimQ ‹Q ⟼ a<νx> ≺ Q'› ‹x ♯ P› obtain P' where PTrans:"P ⟹⇩_{l}⇧^{^}a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans ‹x ♯ R› have "P ∥ R ⟹⇩_{l}⇧^{^}a<νx> ≺ (P' ∥ R)" by(rule Weak_Late_Semantics.Par1B) moreover from P'RelQ' RRel'T have "(P' ∥ R, Q' ∥ T) ∈ Rel''" by(rule Par) ultimately show ?case by blast next case(cPar2 T') from RSimT ‹T ⟼ a<νx> ≺ T'› ‹x ♯ R› obtain R' where RTrans:"R ⟹⇩_{l}⇧^{^}a<νx> ≺ R'" and R'Rel'T': "(R', T') ∈ Rel'" by(blast dest: simE) from RTrans ‹x ♯ P› ‹x ♯ R› have ParTrans: "P ∥ R ⟹⇩_{l}⇧^{^}a<νx> ≺ (P ∥ R')" by(blast intro: Weak_Late_Semantics.Par2B) moreover from PRelQ R'Rel'T' have "(P ∥ R', Q ∥ T') ∈ Rel''" by(rule Par) ultimately show ?case by blast qed next case(Input Q' a x) from ‹x ♯ (P, Q, R, T)› have "x ♯ P" and "x ♯ R" and "x ♯ Q" and "x ♯ T" by simp+ from ‹Q ∥ T ⟼ a<x> ≺ Q'› ‹x ♯ Q› ‹x ♯ T› show ?case proof(induct rule: parCasesB) case(cPar1 Q') from PSimQ ‹Q ⟼a<x> ≺ Q'› ‹x ♯ P› 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] ∥ T[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 ‹x ♯ R› have "P ∥ R ⟹⇩_{l}u in (P'' ∥ R)→a<x> ≺ (P' ∥ R)" by(rule Weak_Late_Step_Semantics.Par1B) moreover from P'RelQ' RRel'T have "(P' ∥ R, Q'[x::=u] ∥ T) ∈ Rel''" by(rule Par) ultimately show "∃P'. P ∥ R ⟹⇩_{l}u in (P'' ∥ R)→a<x> ≺ P' ∧ (P', Q'[x::=u] ∥ (T[x::=u])) ∈ Rel''" using ‹x ♯ T› by(force simp add: forget) qed thus ?case by force next case(cPar2 T') from RSimT ‹T ⟼a<x> ≺ T'› ‹x ♯ R› obtain R'' where L1: "∀u. ∃R'. R ⟹⇩_{l}u in R''→a<x> ≺ R' ∧ (R', T'[x::=u]) ∈ Rel'" by(blast dest: simE) have "∀u. ∃P'. P ∥ R ⟹⇩_{l}u in (P ∥ R'')→a<x> ≺ P' ∧ (P', Q[x::=u] ∥ T'[x::=u]) ∈ Rel''" proof(rule allI) fix u from L1 obtain R' where RTrans:"R ⟹⇩_{l}u in R''→a<x> ≺ R'" and R'Rel'T': "(R', T'[x::=u]) ∈ Rel'" by blast from RTrans ‹x ♯ P› have ParTrans: "P ∥ R ⟹⇩_{l}u in (P ∥ R'')→a<x> ≺ (P ∥ R')" by(rule Weak_Late_Step_Semantics.Par2B) moreover from PRelQ R'Rel'T' have "(P ∥ R', Q ∥ T'[x::=u]) ∈ Rel''" by(rule Par) ultimately show "∃P'. P ∥ R ⟹⇩_{l}u in (P ∥ R'')→a<x> ≺ P' ∧ (P', Q[x::=u] ∥ T'[x::=u]) ∈ Rel''" using ‹x ♯ Q› by(force simp add: forget) qed thus ?case by force qed next case(Free QT' α) have "Q ∥ T ⟼ α ≺ 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 ⟹⇩_{l}⇧^{^}α ≺ P'" and PRel: "(P', Q') ∈ Rel" by(blast dest: simE) from PTrans have Trans: "P ∥ R ⟹⇩_{l}⇧^{^}α ≺ P' ∥ R" by(rule Weak_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 "T ⟼ α ≺ T'" by fact with RSimT obtain R' where RTrans: "R ⟹⇩_{l}⇧^{^}α ≺ R'" and RRel: "(R', T') ∈ Rel'" by(blast dest: simE) from RTrans have Trans: "P ∥ R ⟹⇩_{l}⇧^{^}α ≺ P ∥ R'" by(rule Weak_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) have QTrans: "Q ⟼ a<x> ≺ Q'" and TTrans: "T ⟼ a[b] ≺ T'" 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 RSimT TTrans obtain R' where RTrans: "R ⟹⇩_{l}⇧^{^}a[b] ≺ R'" and RRel: "(R', T') ∈ Rel'" by(blast dest: simE) from PTrans RTrans have "P ∥ R ⟹⇩_{l}⇧^{^}τ ≺ P' ∥ R'" by(rule Weak_Late_Semantics.Comm1) moreover from P'RelQ' RRel have "(P' ∥ R', Q'[x::=b] ∥ T') ∈ Rel''" by(rule Par) ultimately show ?case by blast next case(cComm2 Q' T' a b x) have QTrans: "Q ⟼a[b] ≺ Q'" and TTrans: "T ⟼a<x> ≺ T'" 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 RSimT TTrans xFreshR obtain R' R'' where RTrans: "R ⟹⇩_{l}b in R''→a<x> ≺ R'" and R'Rel'T': "(R', T'[x::=b]) ∈ Rel'" by(blast dest: simE) from PTrans RTrans have "P ∥ R ⟹⇩_{l}⇧^{^}τ ≺ P' ∥ R'" by(rule Weak_Late_Semantics.Comm2) moreover from PRel R'Rel'T' have "(P' ∥ R', Q' ∥ T'[x::=b]) ∈ Rel''" by(rule Par) ultimately show ?case by blast next case(cClose1 Q' T' a x y) have QTrans: "Q ⟼a<x> ≺ Q'" and TTrans: "T ⟼a<νy> ≺ T'" 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 RSimT TTrans yFreshR obtain R' where RTrans: "R ⟹⇩_{l}⇧^{^}a<νy> ≺ R'" and R'Rel'T': "(R', T') ∈ Rel'" by(blast dest: simE) from PTrans RTrans yFreshP yFreshR have Trans: "P ∥ R ⟹⇩_{l}⇧^{^}τ ≺ <νy>(P' ∥ R')" by(rule Weak_Late_Semantics.Close1) moreover from P'RelQ' R'Rel'T' have "(<νy>(P' ∥ 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) have QTrans: "Q ⟼a<νy> ≺ Q'" and TTrans: "T ⟼a<x> ≺ T'" 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 RSimT TTrans xFreshR obtain R' R'' where RTrans: "R ⟹⇩_{l}y in R''→a<x> ≺ R'" and R'Rel'T': "(R', T'[x::=y]) ∈ Rel'" by(blast dest: simE) from PTrans RTrans yFreshP yFreshR have Trans: "P ∥ R ⟹⇩_{l}⇧^{^}τ ≺ <νy>(P' ∥ R')" by(rule Weak_Late_Semantics.Close2) moreover from P'RelQ' R'Rel'T' have "(<νy>(P' ∥ R'), <ν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 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_Semantics.Open) moreover from PTrans yFreshP have "y ♯ P'" by(force intro: 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_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 ResF) qed moreover from P'RelQ' have "(<νx>P', <νx>Q') ∈ Rel'" by(rule ResRel) ultimately show ?case by blast qed 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: "⋀P Q a. (P, Q) ∈ Rel ⟹ (<νa>P, <νa>Q) ∈ 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 PSimQ: "P ↝⇧^{^}<Rel> Q" and PRelQ: "(P, Q) ∈ Rel" and Sim: "⋀P Q. (P, Q) ∈ Rel ⟹ P ↝⇧^{^}<Rel> Q" and ParComp: "⋀P Q R T. ⟦(P, Q) ∈ Rel; (R, T) ∈ Rel'⟧ ⟹ (P ∥ R, Q ∥ T) ∈ Rel'" and Res: "⋀P Q x. (P, Q) ∈ Rel' ⟹ (<νx>P, <νx>Q) ∈ Rel'" and RelStay: "⋀P Q. (P ∥ !P, Q) ∈ Rel' ⟹ (!P, Q) ∈ Rel'" and BangRelRel': "(bangRel Rel) ⊆ Rel'" and eqvtRel': "eqvt Rel'" shows "!P ↝⇧^{^}<Rel'> !Q" proof - have "⋀Rs P. ⟦!Q ⟼ Rs; (P, !Q) ∈ bangRel Rel⟧ ⟹ weakSimAct P Rs P Rel'" proof - fix Rs P assume "!Q ⟼ Rs" and "(P, !Q) ∈ bangRel Rel" thus "weakSimAct P Rs P Rel'" proof(nominal_induct avoiding: P rule: bangInduct) case(cPar1B aa x Q') 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 RBangRelT: "(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 eqvtRel' 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]) ∈ 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]) ∈ Rel'" proof - from P'RelQ' RBangRelT have "(P' ∥ R, Q'[x::=u] ∥ !Q) ∈ bangRel Rel" by(rule Rel.BRPar) with xFreshQ BangRelRel' show ?thesis by(auto simp add: forget) qed ultimately show "∃P'. P ∥ R ⟹⇩_{l}u in (P'' ∥ R)→a<x> ≺ P' ∧ (P', (Q' ∥ !Q)[x::=u]) ∈ 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(blast dest: simE) from PTrans xFreshR have "P ∥ R ⟹⇩_{l}⇧^{^}a<νx>≺ P' ∥ R" by(rule Weak_Late_Semantics.Par1B) moreover from P'RelQ' RBangRelT BangRelRel' have "(P' ∥ R, Q' ∥ !Q) ∈ Rel'" by(blast intro: Rel.BRPar) 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 Der 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_Semantics.Par1F) moreover from P'RelQ' RBangRelQ have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel" by(rule Rel.BRPar) ultimately show ?case using BangRelRel' by blast qed qed next case(cPar2B aa x Q' P) have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimAct P (aa«x» ≺ Q') P 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 eqvtRel' show ?case proof(induct rule: simActBoundCases) case(Input a) have "aa = InputS a" by fact with RBangRelQ IH have "weakSimAct R (a<x> ≺ Q') R Rel'" by blast with xFreshR obtain R'' where L1: "∀u. ∃R'. R ⟹⇩_{l}u in R''→a<x> ≺ R' ∧ (R', Q'[x::=u]) ∈ Rel'" by(force simp add: weakSimAct_def) have "∀u. ∃P'. P ∥ R ⟹⇩_{l}u in (P ∥ R'')→a<x> ≺ P' ∧ (P', (Q ∥ 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'Rel'Q': "(R', Q'[x::=u]) ∈ 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]) ∈ Rel'" proof - from PRelQ R'Rel'Q' have "(P ∥ R', Q ∥ Q'[x::=u]) ∈ Rel'" by(rule ParComp) 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]) ∈ Rel'" by blast qed thus ?case by blast next case(BoundOutput a) have "aa = BoundOutputS a" by fact with IH RBangRelQ have "weakSimAct R (a<νx> ≺ Q') R Rel'" by blast with xFreshR obtain R' where RTrans: "R ⟹⇩_{l}⇧^{^}a<νx> ≺ R'" and R'BangRelQ': "(R', Q') ∈ Rel'" by(simp add: weakSimAct_def, blast) from RTrans xFreshP have "P ∥ R ⟹⇩_{l}⇧^{^}a<νx> ≺ P ∥ R'" by(auto intro: Weak_Late_Semantics.Par2B) moreover from PRelQ R'BangRelQ' have "(P ∥ R', Q ∥ Q') ∈ Rel'" by(rule ParComp) ultimately show ?case by blast qed qed next case(cPar2F α Q' P) have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimAct P (α ≺ Q') P 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 Der from RBangRelQ have "weakSimAct R (α ≺ Q') R Rel'" by(rule IH) then obtain R' where RTrans: "R ⟹⇩_{l}⇧^{^}α ≺ R'" and R'RelQ': "(R', Q') ∈ Rel'" by(simp add: weakSimAct_def, blast) from RTrans have "P ∥ R ⟹⇩_{l}⇧^{^}α ≺ P ∥ R'" by(rule Weak_Late_Semantics.Par2F) moreover from PRelQ R'RelQ' have "(P ∥ R', Q ∥ Q') ∈ Rel'" by(rule ParComp) 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 ⟹ weakSimAct P (a[b] ≺ Q'') P 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 Der 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 "weakSimAct R (a[b] ≺ Q'') R Rel'" by(rule IH) then obtain R' where RTrans: "R ⟹⇩_{l}⇧^{^}a[b] ≺ R'" and R'RelQ'': "(R', Q'') ∈ Rel'" by(simp add: weakSimAct_def, blast) from PTrans RTrans have "P ∥ R ⟹⇩_{l}⇧^{^}τ ≺ (P' ∥ R')" by(rule Weak_Late_Semantics.Comm1) moreover from P'RelQ' R'RelQ'' have "(P' ∥ R', Q'[x::=b] ∥ Q'') ∈ Rel'" by(rule ParComp) 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 ⟹ weakSimAct P (a<x> ≺ Q'') P 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 Der 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 "weakSimAct R (a<x> ≺ Q'') R 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]) ∈ Rel'" by(simp add: weakSimAct_def, blast) from PTrans RTrans have "P ∥ R ⟹⇩_{l}⇧^{^}τ ≺ (P' ∥ R')" by(rule Weak_Late_Semantics.Comm2) moreover from P'RelQ' R'BangRelQ'' have "(P' ∥ R', Q' ∥ Q''[x::=b]) ∈ Rel'" by(rule ParComp) 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 ⟹ weakSimAct P (a<νy> ≺ Q'') P 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" by fact hence xFreshP: "x ♯ P" by simp have "y ♯ P ∥ R" by fact hence yFreshR: "y ♯ R" and yFreshP: "y ♯ P" by simp+ show ?case proof(induct rule: simActFreeCases) case Der 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 "weakSimAct R (a<νy> ≺ Q'') R Rel'" by(rule IH) with yFreshR obtain R' where RTrans: "R ⟹⇩_{l}⇧^{^}a<νy> ≺ R'" and R'RelQ'': "(R', Q'') ∈ Rel'" by(simp add: weakSimAct_def, blast) from PTrans RTrans yFreshP yFreshR have "P ∥ R ⟹⇩_{l}⇧^{^}τ ≺ <νy>(P' ∥ R')" by(rule Weak_Late_Semantics.Close1) moreover from P'RelQ' R'RelQ'' have "(<νy>(P' ∥ R'), <νy>(Q'[x::=y] ∥ Q'')) ∈ Rel'" by(force intro: ParComp Res) ultimately show ?case by blast qed qed next case(cClose2 a y Q' x Q'' P) have QTrans: "Q ⟼ a<νy> ≺ Q'" by fact have IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ weakSimAct P (a<x> ≺ Q'') P 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" by fact hence xFreshR: "x ♯ R" by simp have "y ♯ P ∥ R" by fact hence yFreshP: "y ♯ P" and yFreshR: "y ♯ R" by simp+ show ?case proof(induct rule: simActFreeCases) case Der 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 "weakSimAct R (a<x> ≺ Q'') R Rel'" by(rule IH) with xFreshR obtain R' R'' where RTrans: "R ⟹⇩_{l}y in R''→a<x> ≺ R'" and R'RelQ'': "(R', Q''[x::=y]) ∈ Rel'" by(simp add: weakSimAct_def, blast) from PTrans RTrans yFreshP yFreshR have "P ∥ R ⟹⇩_{l}⇧^{^}τ ≺ <νy>(P' ∥ R')" by(rule Weak_Late_Semantics.Close2) moreover from P'RelQ' R'RelQ'' have "(<νy>(P' ∥ R'), <νy>(Q' ∥ Q''[x::=y])) ∈ Rel'" by(force intro: ParComp Res) ultimately show ?case by blast qed qed next case(cBang Rs) have IH: "⋀P. (P, Q ∥ !Q) ∈ bangRel Rel ⟹ weakSimAct P Rs P 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 "weakSimAct (P ∥ !P) Rs (P ∥ !P) Rel'" by(rule IH) thus ?case proof(simp (no_asm) add: weakSimAct_def, auto) fix Q' a x assume "weakSimAct (P ∥ !P) (a<νx> ≺ Q') (P ∥ !P) Rel'" and "x ♯ P" then obtain P' where PTrans: "(P ∥ !P) ⟹⇩_{l}⇧^{^}a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'" by(simp add: weakSimAct_def, blast) from PTrans have "!P ⟹⇩_{l}⇧^{^}a<νx> ≺ P'" by(force intro: Weak_Late_Step_Semantics.Bang simp add: weakTransition_def) with P'RelQ' show "∃P'. !P ⟹⇩_{l}⇧^{^}a<νx> ≺ P' ∧ (P', Q') ∈ Rel'" by blast next fix Q' a x assume "weakSimAct (P ∥ !P) (a<x> ≺ Q') (P ∥ !P) Rel'" and "x ♯ P" then obtain P'' where L1: "∀u. ∃P'. P ∥ !P ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" by(simp add: weakSimAct_def, blast) have "∀u. ∃P'. !P ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ 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]) ∈ 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]) ∈ Rel'" by blast qed thus "∃P''. ∀u. ∃P'. !P ⟹⇩_{l}u in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" by blast next fix Q' α assume "weakSimAct (P ∥ !P) (α ≺ Q') (P ∥ !P) Rel'" then obtain P' where PTrans: "(P ∥ !P) ⟹⇩_{l}⇧^{^}α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'" by(simp add: weakSimAct_def, blast) from PTrans show "∃P'. !P ⟹⇩_{l}⇧^{^}α ≺ P' ∧ (P', Q') ∈ Rel'" proof(induct rule: transitionCases) case Step have "P ∥ !P ⟹⇩_{l}α ≺ P'" by fact hence "!P ⟹⇩_{l}α ≺ P'" by(rule Weak_Late_Step_Semantics.Bang) with P'RelQ' show ?case by(force simp add: weakTransition_def) next case Stay have "α ≺ P' = τ ≺ P ∥ !P" by fact hence αeqτ: "α = τ" and P'eqP: "P' = P ∥ !P" by(simp add: residual.inject)+ have "!P ⟹⇩_{l}⇧^{^}τ ≺ !P" by(simp add: weakTransition_def) moreover from P'eqP P'RelQ' have "(!P, Q') ∈ Rel'" by(blast intro: RelStay) ultimately show ?case using αeqτ by blast qed qed qed qed qed moreover from PRelQ have "(!P, !Q) ∈ bangRel Rel" by(rule Rel.BRBang) ultimately show ?thesis by(simp add: simDef) qed end