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