Theory Weak_Late_Step_Sim_Pres
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 ⟹⇩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 ?case using PRelQ
proof(induct rule: outputCases, auto simp add: pi.inject residual.inject)
have "a{b}.P ⟹⇩la[b] ≺ P" by(rule Weak_Late_Step_Semantics.Output)
moreover assume "(P, Q') ∈ Rel"
ultimately show "∃P'. a{b}.P ⟹⇩la[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 ⟹⇩lc<νx> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
from PTrans have "[a⌢a]P ⟹⇩lc<ν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 ⟹⇩lu in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
by(blast dest: 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 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 ⟹⇩lc<νx> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
from PTrans aineqb have "[a≠b]P ⟹⇩lc<ν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 ⟹⇩lu in P''→c<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
by(blast dest: 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 "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 ⟹⇩la<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
from PTrans have "P ⊕ R ⟹⇩la<ν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 ⟹⇩la<νx> ≺ R'" and R'RelQ': "(R', Q') ∈ Rel"
by(blast dest: simE)
from RTrans have "P ⊕ R ⟹⇩la<ν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 ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel"
by(blast dest: simE)
have "∀u. ∃P'. P ⊕ R ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', 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 have "P ⊕ R ⟹⇩lu in P''→a<x> ≺ P'" by(rule Weak_Late_Step_Semantics.Sum1)
with P'RelQ' RelRel' show "∃P'. P ⊕ R ⟹⇩lu 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 ⟹⇩lu in R''→a<x> ≺ R' ∧ (R', Q'[x::=u]) ∈ Rel"
by(blast dest: simE)
have "∀u. ∃P'. P ⊕ R ⟹⇩lu in R''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ Rel'"
proof(rule allI)
fix u
from L1 obtain R' where RTrans: "R ⟹⇩lu in R''→a<x> ≺ R'"
and R'RelQ': "(R', Q'[x::=u]) ∈ Rel" by blast
from RTrans have "P ⊕ R ⟹⇩lu in R''→a<x> ≺ R'" by(rule Weak_Late_Step_Semantics.Sum2)
with R'RelQ' RelRel' show "∃P'. P ⊕ R ⟹⇩lu 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 ⟹⇩la<ν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 ⟹⇩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] ∥ R[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 from P'RelQ' have "(P' ∥ R, Q'[x::=u] ∥ R) ∈ Rel'"
by(rule Par)
ultimately show "∃P'. P ∥ R ⟹⇩lu 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 ⟹⇩lu in (P ∥ R')→a<x> ≺ P' ∧ (P', Q ∥ R'[x::=u]) ∈ Rel'"
proof
fix u
from RTrans have "R ⟹⇩lu in R'→a<x> ≺ R'[x::=u]"
by(rule Weak_Late_Step_Semantics.singleActionChain)
hence "P ∥ R ⟹⇩lu 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 ⟹⇩lu 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 ⟹⇩lb in P''→a<x> ≺ P'"
and P'RelQ': "(P', Q'[x::=b]) ∈ Rel"
by(blast dest: simE)
from RTrans have "R ⟹⇩la[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 ⟹⇩la[b] ≺ P'"
and PRel: "(P', Q') ∈ Rel"
by(blast dest: simE)
from RTrans have "R ⟹⇩lb 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 ⟹⇩ly in P''→a<x> ≺ P'"
and P'RelQ': "(P', Q'[x::=y]) ∈ Rel"
by(blast dest: simE)
from RTrans have "R ⟹⇩la<ν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 ⟹⇩la<νy> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
from RTrans have "R ⟹⇩ly 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 ⟹⇩la[x] ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
have "<νx>P ⟹⇩la<νy> ≺ ([(y, x)] ∙ P')"
proof -
from PTrans aineqx have "<νx>P ⟹⇩la<ν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 ⟹⇩la<νy> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
from PTrans ‹x ≠ a› yineqx yFreshP have ResTrans: "<νx>P ⟹⇩la<ν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 ⟹⇩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 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 ⟹⇩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]) ∈ bangRel 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]) ∈ 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 ⟹⇩lu 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 ⟹⇩la<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel'"
by(force dest: simE)
from PTrans xFreshR have "P ∥ R ⟹⇩la<ν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 ⟹⇩lu in R''→a<x> ≺ R' ∧
(R', Q'[x::=u]) ∈ bangRel Rel'"
by(simp add: weakStepSimAct_def, blast)
have "∀u. ∃P'. P ∥ R ⟹⇩lu 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 ⟹⇩lu in R''→a<x> ≺ R'"
and R'BangRelT': "(R', Q'[x::=u]) ∈ bangRel 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]) ∈ 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 ⟹⇩lu 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 ⟹⇩la<νx> ≺ R'"
and R'BangRelT': "(R', Q') ∈ bangRel Rel'"
by(simp add: weakStepSimAct_def, blast)
from RTrans xFreshP have "P ∥ R ⟹⇩la<ν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 ⟹⇩lb 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 ⟹⇩la[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 ⟹⇩la[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 ⟹⇩lb 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 ⟹⇩ly 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 ⟹⇩la<ν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 ⟹⇩la<ν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 ⟹⇩ly 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) ⟹⇩la<νx> ≺ P'"
and P'RelQ': "(P', Q') ∈ (bangRel Rel')"
by(simp add: weakStepSimAct_def, blast)
from PTrans have "!P ⟹⇩la<νx> ≺ P'"
by(rule Weak_Late_Step_Semantics.Bang)
with P'RelQ' show "∃P'. !P ⟹⇩la<ν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 ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ (bangRel Rel')"
by(simp add: weakStepSimAct_def, blast)
have "∀u. ∃P'. !P ⟹⇩lu in P''→a<x> ≺ P' ∧ (P', Q'[x::=u]) ∈ (bangRel 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]) ∈ (bangRel 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]) ∈ (bangRel Rel')" by blast
qed
thus "∃P''. ∀u. ∃P'. !P ⟹⇩lu 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