Theory Weak_Early_Sim_Pres
theory Weak_Early_Sim_Pres
imports Weak_Early_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(induct rule: tauCases', auto)
thus ?case by simp
next
case(Free Q' α)
have "τ.(Q) ⟼(α ≺ Q')" by fact
thus ?case
proof(induct rule: tauCases', auto simp only: pi.inject residual.inject)
have "τ.(P) ⟹⇧^ τ ≺ P" by(rule 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"
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(induct rule: outputCases', auto)
thus ?case 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 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'"
and RelStay: "⋀R S c. (R, S) ∈ Rel ⟹ ([c⌢c]R, S) ∈ 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 Match
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: simE)
from PTrans have "[a⌢a]P ⟹c<νx> ≺ P'" by(rule Weak_Early_Step_Semantics.Match)
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: matchCases)
case Match
have "Q ⟼ α ≺ Q'" by fact
with PSimQ obtain P' where "P ⟹⇧^α ≺ P'" and "(P', Q') ∈ Rel"
by(blast dest: simE)
thus ?case
proof(induct rule: transitionCases)
case Step
have "P ⟹α ≺ P'" by fact
hence "[a⌢a]P ⟹α ≺ P'" by(rule Weak_Early_Step_Semantics.Match)
with RelRel' ‹(P', Q') ∈ Rel› show ?case by(force simp add: weakFreeTransition_def)
next
case Stay
have "[a⌢a]P ⟹⇧^τ ≺ [a⌢a]P" by(simp add: weakFreeTransition_def)
moreover from ‹(P, Q') ∈ Rel› have "([a⌢a]P, Q') ∈ Rel" by(blast intro: RelStay)
ultimately show ?case using RelRel' 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 RelRel': "Rel ⊆ Rel'"
and RelStay: "⋀R S c d. ⟦(R, S) ∈ Rel; c ≠ d⟧ ⟹ ([c≠d]R, S) ∈ 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: mismatchCases)
case Mismatch
have aineqb: "a ≠ b" by fact
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: simE)
from PTrans aineqb have "[a≠b]P ⟹c<νx> ≺ P'" by(rule Weak_Early_Step_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 aineqb: "a ≠ b" by fact
have "Q ⟼ α ≺ Q'" by fact
with PSimQ obtain P' where "P ⟹⇧^α ≺ P'" and "(P', Q') ∈ Rel"
by(blast dest: simE)
thus ?case
proof(induct rule: transitionCases)
case Step
have "P ⟹α ≺ P'" by fact
hence "[a≠b]P ⟹α ≺ P'" using aineqb by(rule Weak_Early_Step_Semantics.Mismatch)
with RelRel' ‹(P', Q') ∈ Rel› show ?case by(force simp add: weakFreeTransition_def)
next
case Stay
have "[a≠b]P ⟹⇧^τ ≺ [a≠b]P" by(simp add: weakFreeTransition_def)
moreover from ‹(P, Q') ∈ Rel› aineqb have "([a≠b]P, Q') ∈ Rel" by(blast intro: RelStay)
ultimately show ?case using RelRel' by blast
qed
qed
qed
lemma parCompose:
fixes P :: pi
and Q :: pi
and R :: pi
and S :: 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: "⋀T U x. (T, U) ∈ Rel'' ⟹ (<νx>T, <νx>U) ∈ Rel''"
shows "P ∥ R ↝<Rel''> Q ∥ S"
proof -
show ?thesis
proof(induct rule: simCases)
case(Bound Q' a x)
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 QTrans: "Q ⟼ a<νx> ≺ Q'" and xFreshT: "x ♯ S" by fact+
from xFreshP PSimQ QTrans obtain P' where PTrans:"P ⟹a<νx> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
from PTrans xFreshR have "P ∥ R ⟹a<νx> ≺ (P' ∥ R)" by(rule Weak_Early_Step_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 STrans: "S ⟼ a<νx> ≺ S'" and xFreshQ: "x ♯ Q" by fact+
from xFreshR RSimT STrans obtain R' where RTrans:"R ⟹a<νx> ≺ R'"
and R'Rel'T': "(R', S') ∈ Rel'"
by(blast dest: simE)
from RTrans xFreshP xFreshR have ParTrans: "P ∥ R ⟹a<νx> ≺ (P ∥ R')"
by(blast intro: Weak_Early_Step_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: simE)
from PTrans have Trans: "P ∥ R ⟹⇧^ α ≺ P' ∥ R" by(rule Weak_Early_Semantics.Par1F)
moreover from PRel RRel'T have "(P' ∥ R, Q' ∥ S) ∈ Rel''" by(blast intro: 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: simE)
from RTrans have Trans: "P ∥ R ⟹⇧^ α ≺ P ∥ R'" by(rule Weak_Early_Semantics.Par2F)
moreover from PRelQ RRel have "(P ∥ R', Q ∥ S') ∈ Rel''" by(blast intro: Par)
ultimately show ?case by blast
next
case(cComm1 Q' S' a b)
have QTrans: "Q ⟼ a<b> ≺ Q'" and STrans: "S ⟼ a[b] ≺ S'" by fact+
from PSimQ QTrans obtain P' where PTrans: "P ⟹a<b> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(fastforce dest: simE simp add: weakFreeTransition_def)
from RSimT STrans obtain R' where RTrans: "R ⟹a[b] ≺ R'"
and RRel: "(R', S') ∈ Rel'"
by(fastforce dest: simE simp add: weakFreeTransition_def)
from PTrans RTrans have "P ∥ R ⟹τ ≺ P' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm1)
hence "P ∥ R ⟹⇧^τ ≺ P' ∥ R'"
by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain)
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 QTrans: "Q ⟼a[b] ≺ Q'" and STrans: "S ⟼a<b> ≺ S'" by fact+
from PSimQ QTrans obtain P' where PTrans: "P ⟹a[b] ≺ P'"
and PRel: "(P', Q') ∈ Rel"
by(fastforce dest: simE simp add: weakFreeTransition_def)
from RSimT STrans obtain R' where RTrans: "R ⟹a<b> ≺ R'"
and R'Rel'T': "(R', S') ∈ Rel'"
by(fastforce dest: simE simp add: weakFreeTransition_def)
from PTrans RTrans have "P ∥ R ⟹τ ≺ P' ∥ R'" by(rule Weak_Early_Step_Semantics.Comm2)
hence "P ∥ R ⟹⇧^τ ≺ P' ∥ R'"
by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain)
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 QTrans: "Q ⟼a<x> ≺ Q'" and STrans: "S ⟼a<νx> ≺ S'" by fact+
have "x ♯ (P, R)" by fact
hence xFreshP: "x ♯ P" and xFreshR: "x ♯ R" by(simp add: fresh_prod)+
from PSimQ QTrans obtain P' where PTrans: "P ⟹a<x> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(fastforce dest: simE simp add: weakFreeTransition_def)
from RSimT STrans xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'"
and R'Rel'T': "(R', S') ∈ Rel'"
by(blast dest: simE)
from PTrans RTrans xFreshP have Trans: "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')"
by(rule Weak_Early_Step_Semantics.Close1)
hence "P ∥ R ⟹⇧^τ ≺ <νx>(P' ∥ R')"
by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain)
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 QTrans: "Q ⟼a<νx> ≺ Q'" and STrans: "S ⟼a<x> ≺ S'" by fact+
have "x ♯ (P, R)" by fact
hence xFreshR: "x ♯ R" and xFreshP: "x ♯ P" by(simp add: fresh_prod)+
from PSimQ QTrans xFreshP obtain P' where PTrans: "P ⟹a<νx> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
from RSimT STrans obtain R' where RTrans: "R ⟹a<x> ≺ R'"
and R'Rel'T': "(R', S') ∈ Rel'"
by(fastforce dest: simE simp add: weakFreeTransition_def)
from PTrans RTrans xFreshR have Trans: "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')"
by(rule Weak_Early_Step_Semantics.Close2)
hence "P ∥ R ⟹⇧^τ ≺ <νx>(P' ∥ R')"
by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain)
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
qed
lemma parPres:
fixes P :: pi
and Q :: pi
and R :: pi
and a :: 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 ResRel: "⋀R S y. (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" by(simp add: fresh_prod)+
from Trans yineqx show ?case
proof(induct rule: resCasesB)
case(Open Q')
have QTrans: "Q ⟼a[x] ≺ Q'" and aineqx: "a ≠ x" by fact+
from PSimQ QTrans obtain P' where PTrans: "P ⟹⇧^a[x] ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
from PTrans aineqx have "<νx>P ⟹a<νx> ≺ P'"
by(force intro: Weak_Early_Step_Semantics.Open simp add: weakFreeTransition_def)
with ‹y ♯ P› ‹y ≠ x› have "<νx>P ⟹a<νy> ≺ ([(y, x)] ∙ P')"
by(force intro: weakTransitionAlpha simp add: abs_fresh name_swap)
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'" and xineqa: "x ≠ a" by fact+
from PSimQ yFreshP QTrans obtain P' where PTrans: "P ⟹a<νy> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
from PTrans xineqa yineqx yFreshP have ResTrans: "<νx>P ⟹a<νy> ≺ (<νx>P')"
by(blast intro: Weak_Early_Step_Semantics.ResB)
moreover from P'RelQ' have "((<νx>P'), (<νx>Q')) ∈ Rel'"
by(rule ResRel)
ultimately show ?case by blast
qed
next
case(Free α Q')
have QTrans: "<ν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 QTrans cFreshQ have "<νc>([(x, c)] ∙ Q) ⟼α ≺ Q'" by(simp add: alphaRes)
moreover have "c ♯ α" by(rule cFreshAlpha)
moreover from PSimQ EqvtRel have "([(x, c)] ∙ P) ↝<Rel> ([(x, c)] ∙ Q)"
by(blast intro: eqvtI)
ultimately show ?thesis
apply(induct rule: resCasesF, auto simp add: residual.inject pi.inject name_abs_eq)
by(blast intro: ResF ResRel dest: simE)
qed
ultimately show ?case by force
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 y. (R, S) ∈ Rel ⟹ (<νy>R, <νy>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 ParComp: "⋀R S T U. ⟦(R, S) ∈ Rel; (T, U) ∈ Rel'⟧ ⟹ (R ∥ T, S ∥ U) ∈ Rel'"
and Res: "⋀R S x. (R, S) ∈ Rel' ⟹ (<νx>R, <νx>S) ∈ Rel'"
and RelStay: "⋀R S. (R ∥ !R, S) ∈ Rel' ⟹ (!R, S) ∈ Rel'"
and BangRelRel': "(bangRel Rel) ⊆ Rel'"
and eqvtRel': "eqvt Rel'"
shows "!P ↝<Rel'> !Q"
proof -
let ?Sim = "λP Rs. (∀a x Q'. Rs = a<νx> ≺ Q' ⟶ x ♯ P ⟶ (∃P'. P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ Rel')) ∧
(∀α Q'. Rs = α ≺ Q' ⟶ (∃P'. P ⟹⇧^α ≺ P' ∧ (P', Q') ∈ Rel'))"
{
fix Rs P
assume "!Q ⟼ Rs" and "(P, !Q) ∈ bangRel Rel"
hence "?Sim P Rs" using PRelQ
proof(nominal_induct avoiding: P rule: bangInduct)
case(Par1B a x Q')
have QTrans: "Q ⟼a<ν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 ‹x ♯ P› ‹x ♯ Q› show ?case
proof(auto simp add: residual.inject alpha' name_fresh_fresh)
from PSimQ QTrans xFreshP obtain P' where PTrans: "P ⟹a<νx> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
from PTrans xFreshR have "P ∥ R ⟹a<νx>≺ (P' ∥ R)"
by(rule Weak_Early_Step_Semantics.Par1B)
moreover from P'RelQ' RBangRelT BangRelRel' have "(P' ∥ R, Q' ∥ !Q) ∈ Rel'"
by(blast intro: Rel.BRPar)
ultimately show "∃P'. P ∥ R ⟹a<νx> ≺ P' ∧ (P', Q' ∥ !Q) ∈ Rel'" by blast
next
fix y
assume "(y::name) ♯ Q'" and "y ♯ P" and "y ♯ R"
from QTrans ‹y ♯ Q'› have "Q ⟼a<νy> ≺ ([(x, y)] ∙ Q')" by(simp add: alphaBoundOutput)
with PSimQ ‹y ♯ P› obtain P' where PTrans: "P ⟹a<νy> ≺ P'"
and P'RelQ': "(P', [(x, y)] ∙ Q') ∈ Rel"
by(blast dest: simE)
from PTrans ‹y ♯ R› have "P ∥ R ⟹a<νy>≺ (P' ∥ R)" by(rule Weak_Early_Step_Semantics.Par1B)
moreover from P'RelQ' RBangRelT BangRelRel' have "(P' ∥ R, ([(y, x)] ∙ Q') ∥ !Q) ∈ Rel'"
by(fastforce intro: Rel.BRPar simp add: name_swap)
ultimately show "∃P'. P ∥ R ⟹a<νy> ≺ P' ∧ (P', ([(y, x)] ∙ Q') ∥ !Q) ∈ Rel'" by blast
qed
qed
next
case(Par1F α 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(auto simp add: residual.inject)
from PRelQ have "P ↝<Rel> Q" by(rule Sim)
with QTrans obtain P' where PTrans: "P ⟹⇧^α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
from PTrans have "P ∥ R ⟹⇧^α ≺ P' ∥ R" by(rule Weak_Early_Semantics.Par1F)
moreover from P'RelQ' RBangRelQ have "(P' ∥ R, Q' ∥ !Q) ∈ bangRel Rel"
by(rule Rel.BRPar)
ultimately show "∃P'. P ∥ R ⟹⇧^α ≺ P' ∧ (P', Q' ∥ !Q) ∈ Rel'" using BangRelRel' by blast
qed
qed
next
case(Par2B a x Q' P)
hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (a<νx> ≺ Q')" by simp
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+
show ?case using ‹x ♯ Q›
proof(auto simp add: residual.inject alpha' name_fresh_fresh)
from IH RBangRelQ have "?Sim R (a<νx> ≺ Q')" by blast
with xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'" and R'BangRelQ': "(R', Q') ∈ Rel'"
by(blast dest: simE)
from RTrans xFreshP have "P ∥ R ⟹a<νx> ≺ (P ∥ R')"
by(auto intro: Weak_Early_Step_Semantics.Par2B)
moreover from PRelQ R'BangRelQ' have "(P ∥ R', Q ∥ Q') ∈ Rel'"
by(rule ParComp)
ultimately show "∃P'. P ∥ R ⟹a<νx> ≺ P' ∧ (P', Q ∥ Q') ∈ Rel'" by blast
next
fix y
assume "(y::name) ♯ Q'" and "y ♯ R" and "y ♯ P"
from IH RBangRelQ have "?Sim R (a<νx> ≺ Q')" by blast
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'BangRelQ': "(R', [(x, y)] ∙ Q') ∈ Rel'"
by(blast dest: simE)
from RTrans ‹y ♯ P› have "P ∥ R ⟹a<νy> ≺ (P ∥ R')"
by(auto intro: Weak_Early_Step_Semantics.Par2B)
moreover from PRelQ R'BangRelQ' have "(P ∥ R', Q ∥ ([(y, x)] ∙ Q')) ∈ Rel'"
by(fastforce intro: ParComp simp add: name_swap)
ultimately show "∃P'. P ∥ R ⟹a<νy> ≺ P' ∧ (P', Q ∥ ([(y, x)] ∙ Q')) ∈ Rel'" by blast
qed
qed
next
case(Par2F α Q' P)
hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (α ≺ Q')" by simp
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(auto simp add: residual.inject)
from RBangRelQ have "?Sim R (α ≺ Q')" by(rule IH)
then obtain R' where RTrans: "R ⟹⇧^α ≺ R'" and R'RelQ': "(R', Q') ∈ Rel'"
by(blast dest: simE)
from RTrans have "P ∥ R ⟹⇧^α ≺ P ∥ R'" by(rule Weak_Early_Semantics.Par2F)
moreover from PRelQ R'RelQ' have "(P ∥ R', Q ∥ Q') ∈ Rel'" by(rule ParComp)
ultimately show "∃P'. P ∥ R ⟹⇧^α ≺ P' ∧ (P', Q ∥ Q') ∈ Rel'" by blast
qed
qed
next
case(Comm1 a Q' b Q'' P)
hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (a[b] ≺ Q'')" by simp
have QTrans: "Q ⟼ a<b> ≺ 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(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(fastforce dest: simE simp add: weakFreeTransition_def)
from RBangRelQ have "?Sim R (a[b] ≺ Q'')" by(rule IH)
then obtain R' where RTrans: "R ⟹a[b] ≺ R'"
and R'RelQ'': "(R', Q'') ∈ Rel'"
by(fastforce dest: simE simp add: weakFreeTransition_def)
from PTrans RTrans have "P ∥ R ⟹τ ≺ (P' ∥ R')"
by(rule Weak_Early_Step_Semantics.Comm1)
hence "P ∥ R ⟹⇩τ P' ∥ R'"
by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain)
moreover from P'RelQ' R'RelQ'' have "(P' ∥ R', Q' ∥ Q'') ∈ Rel'"
by(rule ParComp)
ultimately show "∃P'. (P ∥ R, P') ∈ {(P, P'). P ⟼ τ ≺ P'}⇧* ∧ (P', Q' ∥ Q'') ∈ Rel'"
by auto
qed
qed
next
case(Comm2 a b Q' Q'' P)
hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (a<b> ≺ Q'')" by simp
have QTrans: "Q ⟼a[b] ≺ 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(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(fastforce dest: simE simp add: weakFreeTransition_def)
from RBangRelQ have "?Sim R (a<b> ≺ Q'')" by(rule IH)
then obtain R' where RTrans: "R ⟹a<b> ≺ R'" and R'BangRelQ'': "(R', Q'') ∈ Rel'"
by(fastforce dest: simE simp add: weakFreeTransition_def)
from PTrans RTrans have "P ∥ R ⟹τ ≺ (P' ∥ R')"
by(rule Weak_Early_Step_Semantics.Comm2)
hence "P ∥ R ⟹⇩τ P' ∥ R'"
by(auto simp add: trancl_into_rtrancl dest: Weak_Early_Step_Semantics.tauTransitionChain)
moreover from P'RelQ' R'BangRelQ'' have "(P' ∥ R', Q' ∥ Q'') ∈ Rel'"
by(rule ParComp)
ultimately show "∃P'. (P ∥ R, P') ∈ {(P, P'). P ⟼ τ ≺ P'}⇧* ∧ (P', Q' ∥ Q'') ∈ Rel'" by auto
qed
qed
next
case(Close1 a x Q' Q'' P)
hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (a<νx> ≺ Q'')" by simp
have QTrans: "Q ⟼ a<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 xFreshR: "x ♯ R" and xFreshP: "x ♯ P" by simp+
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<x> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(fastforce dest: simE simp add: weakFreeTransition_def)
from RBangRelQ have "?Sim R (a<νx> ≺ Q'') " by(rule IH)
with xFreshR obtain R' where RTrans: "R ⟹a<νx> ≺ R'"
and R'RelQ'': "(R', Q'') ∈ Rel'"
by(blast dest: simE)
from PTrans RTrans xFreshP have "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')"
by(rule Weak_Early_Step_Semantics.Close1)
moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ Q'')) ∈ Rel'"
by(force intro: ParComp Res)
ultimately show "∃P'. (P ∥ R, P') ∈ {(P, P'). P ⟼ τ ≺ P'}⇧* ∧ (P', <νx>(Q' ∥ Q'')) ∈ Rel'" by auto
qed
qed
next
case(Close2 a x Q' Q'' P)
hence IH: "⋀P. (P, !Q) ∈ bangRel Rel ⟹ ?Sim P (a<x> ≺ Q'')" by simp
have QTrans: "Q ⟼ a<ν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+
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: simE)
from RBangRelQ have "?Sim R (a<x> ≺ Q'')" by(rule IH)
with xFreshR obtain R' where RTrans: "R ⟹a<x> ≺ R'"
and R'RelQ'': "(R', Q'') ∈ Rel'"
by(fastforce simp add: weakFreeTransition_def)
from PTrans RTrans xFreshR have "P ∥ R ⟹τ ≺ <νx>(P' ∥ R')"
by(rule Weak_Early_Step_Semantics.Close2)
moreover from P'RelQ' R'RelQ'' have "(<νx>(P' ∥ R'), <νx>(Q' ∥ Q'')) ∈ Rel'"
by(force intro: ParComp Res)
ultimately show "∃P'. (P ∥ R, P') ∈ {(P, P'). P ⟼ τ ≺ P'}⇧* ∧ (P', <νx>(Q' ∥ Q'')) ∈ Rel'" by auto
qed
qed
next
case(Bang Rs)
hence IH: "⋀P. (P, Q ∥ !Q) ∈ bangRel Rel ⟹ ?Sim P Rs" by simp
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 IH: "?Sim (P ∥ !P) Rs" by(rule IH)
show ?case
proof(intro conjI allI impI)
fix Q' a x
assume "Rs = a<νx> ≺ Q'" and "x ♯ !P"
then obtain P' where PTrans: "(P ∥ !P) ⟹a<νx> ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel'" using IH
by(auto simp add: residual.inject)
from PTrans have "!P ⟹a<νx> ≺ P'"
by(force intro: Weak_Early_Step_Semantics.Bang simp add: weakFreeTransition_def)
with P'RelQ' show "∃P'. !P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ Rel'" by blast
next
fix Q' α
assume "Rs = α ≺ Q'"
then obtain P' where PTrans: "(P ∥ !P) ⟹⇧^α ≺ P'"
and P'RelQ': "(P', Q') ∈ Rel'" using IH
by auto
from PTrans show "∃P'. !P ⟹⇧^α ≺ P' ∧ (P', Q') ∈ Rel'" using P'RelQ'
proof(induct rule: transitionCases)
case Step
have "P ∥ !P ⟹α ≺ P'" by fact
hence "!P ⟹α ≺ P'" by(rule Weak_Early_Step_Semantics.Bang)
with P'RelQ' show ?case by(force simp add: weakFreeTransition_def)
next
case Stay
have "!P ⟹⇧^τ ≺ !P" by(simp add: weakFreeTransition_def)
moreover assume "(P ∥ !P, Q') ∈ Rel'"
hence "(!P, Q') ∈ Rel'" by(blast intro: RelStay)
ultimately show ?case by blast
qed
qed
qed
qed
}
moreover from PRelQ have "(!P, !Q) ∈ bangRel Rel" by(rule Rel.BRBang)
ultimately show ?thesis by(auto simp add: weakSimulation_def)
qed
lemma bangRelSim:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
and Rel'l :: "(pi × pi) set"
assumes PBangRelQ: "(P, Q) ∈ bangRel Rel"
and Sim: "⋀R S. (R, S) ∈ Rel ⟹ R ↝<Rel> S"
and ParComp: "⋀R S T U. ⟦(R, S) ∈ Rel; (T, U) ∈ Rel'⟧ ⟹ (R ∥ T, S ∥ U) ∈ Rel'"
and Res: "⋀R S x. (R, S) ∈ Rel' ⟹ (<νx>R, <νx>S) ∈ Rel'"
and RelStay: "⋀R S. (R ∥ !R, S) ∈ Rel' ⟹ (!R, S) ∈ Rel'"
and BangRelRel': "(bangRel Rel) ⊆ Rel'"
and eqvtRel': "eqvt Rel'"
and Eqvt: "eqvt Rel"
shows "P ↝<Rel'> Q"
proof -
from PBangRelQ show ?thesis
proof(induct rule: bangRel.induct)
case(BRBang P Q)
have PRelQ: "(P, Q) ∈ Rel" by fact
thus ?case using ParComp Res BangRelRel' eqvtRel' Eqvt RelStay Sim
by(rule_tac bangPres)
next
case(BRPar P Q R T)
have "(P, Q) ∈ Rel" by fact
moreover hence "P ↝<Rel> Q" by(rule Sim)
moreover have "R ↝<Rel'> T" by fact
moreover have "(R, T) ∈ bangRel Rel" by fact
ultimately show ?case using ParComp eqvtRel' Res Eqvt BangRelRel'
by(blast intro: parCompose)
next
case(BRRes P Q x)
have "P ↝<Rel'> Q" by fact
thus ?case using BangRelRel' eqvtRel' Res by(blast intro: resPres)
qed
qed
end