Theory Weak_Late_Sim_Pres
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 ⟹⇩lu in ([(x, y)] ∙ P)→a<y> ≺ P' ∧ (P', ([(x, y)] ∙ Q)[y::=u]) ∈ Rel"
proof(rule allI)
fix u
have "a<x>.P ⟹⇩lu 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) ⟹⇩lu 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 ⟹⇩lu in ([(x, y)] ∙ P)→a<y> ≺ P' ∧ (P', ([(x, y)] ∙ Q)[y::=u]) ∈ Rel"
by blast
qed
thus "∃P''. ∀u. ∃P'. a<x>.P ⟹⇩lu 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 ⟹⇩lu in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
by(force intro: simE)
have "∀u. ∃P'. [a⌢a]P ⟹⇩lu in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'"
proof(rule allI)
fix u
from L1 obtain P' where PTrans: "P ⟹⇩lu in P''→c<x> ≺ P'" and P'RelQ': "(P', Q'[x::=u]) ∈ Rel"
by blast
from PTrans have "[a⌢a]P ⟹⇩lu in P''→c<x> ≺ P'" by(rule Weak_Late_Step_Semantics.Match)
with P'RelQ' RelRel' show "∃P'. [a⌢a]P ⟹⇩lu 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 ⟹⇩lu in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
by(force intro: simE)
have "∀u. ∃P'. [a≠b]P ⟹⇩lu in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'"
proof(rule allI)
fix u
from L1 obtain P' where PTrans: "P ⟹⇩lu in P''→c<x> ≺ P'" and P'RelQ': "(P', Q'[x::=u]) ∈ Rel"
by blast
from PTrans aineqb have "[a≠b]P ⟹⇩lu in P''→c<x> ≺ P'" by(rule Weak_Late_Step_Semantics.Mismatch)
with P'RelQ' RelRel' show "∃P'. [a≠b]P ⟹⇩lu 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 ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
by(blast dest: simE)
have "∀u. ∃P'. P ∥ R ⟹⇩lu 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 ⟹⇩lu in P''→a<x> ≺ P'"
and P'RelQ': "(P', Q'[x::=u]) ∈ Rel" by blast
from PTrans ‹x ♯ R› have "P ∥ R ⟹⇩lu 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 ⟹⇩lu 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 ⟹⇩lu in R''→a<x> ≺ R' ∧ (R', T'[x::=u]) ∈ Rel'"
by(blast dest: simE)
have "∀u. ∃P'. P ∥ R ⟹⇩lu 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 ⟹⇩lu in R''→a<x> ≺ R'"
and R'Rel'T': "(R', T'[x::=u]) ∈ Rel'" by blast
from RTrans ‹x ♯ P› have ParTrans: "P ∥ R ⟹⇩lu 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 ⟹⇩lu 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 ⟹⇩lb 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 ⟹⇩lb 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 ⟹⇩ly 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 ⟹⇩ly 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 ⟹⇩lu in P''→a<y> ≺ P' ∧ (P', Q'[y::=u]) ∈ Rel"
by(blast dest: simE)
have "∀u. ∃P'. <νx>P ⟹⇩lu in (<νx>P'')→a<y> ≺ P' ∧ (P', (<νx>Q')[y::=u]) ∈ Rel'"
proof(rule allI)
fix u
show "∃P'. <νx>P ⟹⇩lu 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 ⟹⇩lc in P''→a<y> ≺ P'"
and P'RelQ': "(P', Q'[y::=c]) ∈ Rel"
by blast
have "<νx>P ⟹⇩lu in (<νx>P'')→a<y> ≺ <νc>([(x, c)] ∙ P')"
proof -
from PTrans yineqx ‹x ≠ a› cineqx have "<νx>P ⟹⇩lc 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 ⟹⇩lu in P''→a<y> ≺ P'"
and P'RelQ': "(P', Q'[y::=u]) ∈ Rel" by blast
from PTrans ‹x ≠ a› yineqx xinequ have "<νx>P ⟹⇩lu 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)
from PRelQ show "resChain [] P ↝⇧^<Rel> resChain [] Q" by simp
next
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 ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
by(blast dest: simE)
have "∀u. ∃P'. P ∥ R ⟹⇩lu in (P'' ∥ R)→a<x> ≺ P' ∧ (P', (Q' ∥ !Q)[x::=u]) ∈ Rel'"
proof(rule allI)
fix u
from L1 obtain P' where PTrans: "P ⟹⇩lu in P''→a<x> ≺ P'"
and P'RelQ': "(P', Q'[x::=u]) ∈ Rel"
by blast
from PTrans xFreshR have "P ∥ R ⟹⇩lu 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 ⟹⇩lu 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 ⟹⇩lu in R''→a<x> ≺ R' ∧ (R', Q'[x::=u]) ∈ Rel'"
by(force simp add: weakSimAct_def)
have "∀u. ∃P'. P ∥ R ⟹⇩lu in (P ∥ R'')→a<x> ≺ P' ∧ (P', (Q ∥ Q')[x::=u]) ∈ Rel'"
proof(rule allI)
fix u
from L1 obtain R' where RTrans: "R ⟹⇩lu in R''→a<x> ≺ R'"
and R'Rel'Q': "(R', Q'[x::=u]) ∈ Rel'"
by blast
from RTrans xFreshP have "P ∥ R ⟹⇩lu 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 ⟹⇩lu 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 ⟹⇩lb 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 ⟹⇩lb 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 ⟹⇩ly 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 ⟹⇩ly 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 ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'"
by(simp add: weakSimAct_def, blast)
have "∀u. ∃P'. !P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'"
proof(rule allI)
fix u
from L1 obtain P' where PTrans: "P ∥ !P ⟹⇩lu in P''→a<x> ≺ P'"
and P'RelQ': "(P', Q'[x::=u]) ∈ Rel'"
by blast
from PTrans have "!P ⟹⇩lu in P''→a<x> ≺ P'" by(rule Weak_Late_Step_Semantics.Bang)
with P'RelQ' show "∃P'. !P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'" by blast
qed
thus "∃P''. ∀u. ∃P'. !P ⟹⇩lu 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