Theory Weak_Early_Step_Semantics
theory Weak_Early_Step_Semantics
imports Early_Tau_Chain
begin
lemma inputSupportDerivative:
assumes "P ⟼a<x> ≺ P'"
shows "(supp P') - {x} ⊆ supp P"
using assms
apply(nominal_induct rule: inputInduct)
apply(auto simp add: pi.supp abs_supp supp_atm)
apply(rule ccontr)
apply(simp add: fresh_def[symmetric])
apply(drule_tac fresh_fact1)
apply(rotate_tac 4)
apply assumption
apply(simp add: fresh_def)
apply force
apply(case_tac "x ♯ P")
apply(drule_tac fresh_fact1)
apply(rotate_tac 2)
apply assumption
apply(simp add: fresh_def)
apply force
apply(rotate_tac 2)
apply(drule_tac fresh_fact2)
apply(simp add: fresh_def)
by force
lemma outputSupportDerivative:
fixes P :: pi
and a :: name
and b :: name
and P' :: pi
assumes "P ⟼a[b] ≺ P'"
shows "(supp P') ⊆ ((supp P)::name set)"
using assms
by(nominal_induct rule: outputInduct) (auto simp add: pi.supp abs_supp)
lemma boundOutputSupportDerivative:
assumes "P ⟼a<νx> ≺ P'"
and "x ♯ P"
shows "(supp P') - {x} ⊆ supp P"
using assms
by(nominal_induct rule: boundOutputInduct) (auto simp add: pi.supp abs_supp supp_atm dest: outputSupportDerivative)
lemma tauSupportDerivative:
assumes "P ⟼τ ≺ P'"
shows "((supp P')::name set) ⊆ supp P"
using assms
proof(nominal_induct rule: tauInduct)
case(Tau P)
thus ?case by(force simp add: pi.supp)
next
case(Match P)
thus ?case by(force simp add: pi.supp)
next
case(Mismatch P)
thus ?case by(force simp add: pi.supp)
next
case(Sum1 P)
thus ?case by(force simp add: pi.supp)
next
case(Sum2 P)
thus ?case by(force simp add: pi.supp)
next
case(Par1 P)
thus ?case by(force simp add: pi.supp)
next
case(Par2 P)
thus ?case by(force simp add: pi.supp)
next
case(Comm1 P a b P' Q Q')
from ‹P ⟼a<b> ≺ P'› have "(supp P') - {b} ⊆ supp P" by(rule inputSupportDerivative)
moreover from ‹Q ⟼ a[b] ≺ Q'› have "((supp Q')::name set) ⊆ supp Q" by(rule outputSupportDerivative)
moreover from ‹Q ⟼ a[b] ≺ Q'› have "b ∈ supp Q"
by(nominal_induct rule: outputInduct) (auto simp add: pi.supp abs_supp supp_atm)
ultimately show ?case by(auto simp add: pi.supp)
next
case(Comm2 P a b P' Q Q')
from ‹P ⟼ a[b] ≺ P'› have "((supp P')::name set) ⊆ supp P" by(rule outputSupportDerivative)
moreover from ‹Q ⟼a<b> ≺ Q'› have "(supp Q') - {b} ⊆ supp Q" by(rule inputSupportDerivative)
moreover from ‹P ⟼ a[b] ≺ P'› have "b ∈ supp P"
by(nominal_induct rule: outputInduct) (auto simp add: pi.supp abs_supp supp_atm)
ultimately show ?case by(auto simp add: pi.supp)
next
case(Close1 P a x P' Q Q')
thus ?case by(auto dest: inputSupportDerivative boundOutputSupportDerivative simp add: abs_supp pi.supp)
next
case(Close2 P a x P' Q Q')
thus ?case by(auto dest: inputSupportDerivative boundOutputSupportDerivative simp add: abs_supp pi.supp)
next
case(Res P P' x)
thus ?case by(force simp add: pi.supp abs_supp)
next
case(Bang P P')
thus ?case by(force simp add: pi.supp)
qed
lemma tauChainSupportDerivative:
fixes P :: pi
and P' :: pi
assumes "P ⟹⇩τ P'"
shows "((supp P')::name set) ⊆ (supp P)"
using assms
by(induct rule: tauChainInduct) (auto dest: tauSupportDerivative)
definition outputTransition :: "pi ⇒ name ⇒ name ⇒ pi ⇒ bool" (‹_ ⟹_<ν_> ≺ _› [80, 80, 80, 80] 80)
where "P ⟹a<νx> ≺ P' ≡ ∃P''' P''. P ⟹⇩τ P''' ∧ P''' ⟼a<νx> ≺ P'' ∧ P'' ⟹⇩τ P'"
definition freeTransition :: "pi ⇒ freeRes⇒ pi ⇒ bool" (‹_ ⟹_ ≺ _› [80, 80, 80] 80)
where "P ⟹α ≺ P' ≡ ∃P''' P''. P ⟹⇩τ P''' ∧ P''' ⟼α ≺ P'' ∧ P'' ⟹⇩τ P'"
lemma transitionI:
fixes P :: pi
and P''' :: pi
and α :: freeRes
and P'' :: pi
and P' :: pi
and a :: name
and x :: name
shows "⟦P ⟹⇩τ P'''; P''' ⟼α ≺ P''; P'' ⟹⇩τ P'⟧ ⟹ P ⟹α ≺ P'"
and "⟦P ⟹⇩τ P'''; P''' ⟼a<νx> ≺ P''; P'' ⟹⇩τ P'⟧ ⟹ P ⟹a<νx> ≺ P'"
by(auto simp add: outputTransition_def freeTransition_def)
lemma transitionE:
fixes P :: pi
and α :: freeRes
and P' :: pi
and a :: name
and x :: name
shows "P ⟹α ≺ P' ⟹ (∃P'' P'''. P ⟹⇩τ P'' ∧ P'' ⟼α ≺ P''' ∧ P''' ⟹⇩τ P')"
and "P ⟹a<νx> ≺ P' ⟹ ∃P'' P'''. P ⟹⇩τ P''' ∧ P''' ⟼a<νx> ≺ P'' ∧ P'' ⟹⇩τ P'"
by(auto simp add: outputTransition_def freeTransition_def)
lemma weakTransitionAlpha:
fixes P :: pi
and a :: name
and x :: name
and P' :: pi
and y :: name
assumes PTrans: "P ⟹a<νx> ≺ P'"
and "y ♯ P"
shows "P ⟹a<νy> ≺ ([(x, y)] ∙ P')"
proof(cases "y=x")
case True
with PTrans show ?thesis by simp
next
case False
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<νx> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(force dest: transitionE)
note PChain
moreover from PChain ‹y ♯ P› have "y ♯ P'''" by(rule freshChain)
with P'''Trans have "y ♯ P''" using ‹y ≠ x› by(rule freshTransition)
with P'''Trans have "P''' ⟼a<νy> ≺ ([(x, y)] ∙ P'')" by(simp add: alphaBoundOutput name_swap)
moreover from P''Chain have "([(x, y)] ∙ P'') ⟹⇩τ ([(x, y)] ∙ P')"
by(rule eqvtChainI)
ultimately show ?thesis by(rule transitionI)
qed
lemma singleActionChain:
fixes P :: pi
and Rs :: residual
shows "P ⟼a<νx> ≺ P' ⟹ P ⟹a<νx> ≺ P'"
and "P ⟼α ≺ P' ⟹ P ⟹α ≺ P'"
proof -
have "P ⟹⇩τ P" by simp
moreover assume "P ⟼a<νx> ≺ P'"
moreover have "P' ⟹⇩τ P'" by simp
ultimately show "P ⟹a<νx> ≺ P'"
by(rule transitionI)
next
have "P ⟹⇩τ P" by simp
moreover assume "P ⟼α ≺ P'"
moreover have "P' ⟹⇩τ P'" by simp
ultimately show "P ⟹α ≺ P'"
by(rule transitionI)
qed
lemma Tau:
fixes P :: pi
shows "τ.(P) ⟹ τ ≺ P"
proof -
have "τ.(P) ⟹⇩τ τ.(P)" by simp
moreover have "τ.(P) ⟼τ ≺ P" by(rule Early_Semantics.Tau)
moreover have "P ⟹⇩τ P" by simp
ultimately show ?thesis by(rule transitionI)
qed
lemma Input:
fixes a :: name
and x :: name
and u :: name
and P :: pi
shows "a<x>.P ⟹ a<u> ≺ P[x::=u]"
proof -
have "a<x>.P ⟹⇩τ a<x>.P" by simp
moreover have "a<x>.P ⟼ a<u> ≺ P[x::=u]" by(rule Early_Semantics.Input)
moreover have "P[x::=u] ⟹⇩τ P[x::=u]" by simp
ultimately show ?thesis by(rule transitionI)
qed
lemma Output:
fixes a :: name
and b :: name
and P :: pi
shows "a{b}.P ⟹a[b] ≺ P"
proof -
have "a{b}.P ⟹⇩τ a{b}.P" by simp
moreover have "a{b}.P ⟼a[b] ≺ P" by(rule Early_Semantics.Output)
moreover have "P ⟹⇩τ P" by simp
ultimately show ?thesis by(rule transitionI)
qed
lemma Match:
fixes P :: pi
and b :: name
and x :: name
and a :: name
and P' :: pi
and α :: freeRes
shows "P ⟹b<νx> ≺ P' ⟹ [a⌢a]P ⟹b<νx> ≺ P'"
and "P ⟹α ≺ P' ⟹ [a⌢a]P ⟹α ≺ P'"
proof -
assume "P ⟹ b<νx> ≺ P'"
then obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼b<νx> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(force dest: transitionE)
show "[a⌢a]P ⟹b<νx> ≺ P'"
proof(cases "P = P'''")
case True
have "[a⌢a]P ⟹⇩τ [a⌢a]P" by simp
moreover from ‹P = P'''› P'''Trans have "[a⌢a]P ⟼ b<νx> ≺ P''"
by(rule_tac Early_Semantics.Match) auto
ultimately show ?thesis using P''Chain by(rule transitionI)
next
case False
from PChain ‹P ≠ P'''› have "[a⌢a]P ⟹⇩τ P'''" by(rule matchChain)
thus ?thesis using P'''Trans P''Chain by(rule transitionI)
qed
next
assume "P ⟹α ≺ P'"
then obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼α ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(force dest: transitionE)
show "[a⌢a]P ⟹α ≺ P'"
proof(cases "P = P'''")
case True
have "[a⌢a]P ⟹⇩τ [a⌢a]P" by simp
moreover from ‹P = P'''› P'''Trans have "[a⌢a]P ⟼α ≺ P''"
by(rule_tac Early_Semantics.Match) auto
ultimately show ?thesis using P''Chain by(rule transitionI)
next
case False
from PChain ‹P ≠ P'''› have "[a⌢a]P ⟹⇩τ P'''" by(rule matchChain)
thus ?thesis using P'''Trans P''Chain by(rule transitionI)
qed
qed
lemma Mismatch:
fixes P :: pi
and c :: name
and x :: name
and a :: name
and b :: name
and P' :: pi
and α :: freeRes
shows "⟦P ⟹c<νx> ≺ P'; a ≠ b⟧ ⟹ [a≠b]P ⟹c<νx> ≺ P'"
and "⟦P ⟹α ≺ P'; a ≠ b⟧ ⟹ [a≠b]P ⟹α ≺ P'"
proof -
assume "P ⟹c<νx> ≺ P'"
then obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼c<νx> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(force dest: transitionE)
assume "a ≠ b"
show "[a≠b]P ⟹c<νx> ≺ P'"
proof(cases "P = P'''")
case True
have "[a≠b]P ⟹⇩τ [a≠b]P" by simp
moreover from ‹P = P'''› ‹a ≠ b› P'''Trans have "[a≠b]P ⟼ c<νx> ≺ P''"
by(rule_tac Early_Semantics.Mismatch) auto
ultimately show ?thesis using P''Chain by(rule transitionI)
next
case False
from PChain ‹a ≠ b› ‹P ≠ P'''› have "[a≠b]P ⟹⇩τ P'''" by(rule mismatchChain)
thus ?thesis using P'''Trans P''Chain by(rule transitionI)
qed
next
assume "P ⟹α ≺ P'"
then obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼α ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(force dest: transitionE)
assume "a ≠ b"
show "[a≠b]P ⟹α ≺ P'"
proof(cases "P = P'''")
case True
have "[a≠b]P ⟹⇩τ [a≠b]P" by simp
moreover from ‹P = P'''› ‹a ≠ b› P'''Trans have "[a≠b]P ⟼α ≺ P''"
by(rule_tac Early_Semantics.Mismatch) auto
ultimately show ?thesis using P''Chain by(rule transitionI)
next
case False
from PChain ‹a ≠ b› ‹P ≠ P'''› have "[a≠b]P ⟹⇩τ P'''" by(rule mismatchChain)
thus ?thesis using P'''Trans P''Chain by(rule transitionI)
qed
qed
lemma Open:
fixes P :: pi
and a :: name
and b :: name
and P' :: pi
assumes PTrans: "P ⟹a[b] ≺ P'"
and "a ≠ b"
shows "<νb>P ⟹a<νb> ≺ P'"
proof -
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a[b] ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(force dest: transitionE)
from PChain have "<νb>P ⟹⇩τ <νb>P'''" by(rule ResChain)
moreover from P'''Trans ‹a ≠ b› have "<νb>P''' ⟼a<νb> ≺ P''" by(rule Open)
ultimately show ?thesis using P''Chain by(rule transitionI)
qed
lemma Sum1:
fixes P :: pi
and a :: name
and x :: name
and P' :: pi
and Q :: pi
and α :: freeRes
shows "P ⟹a<νx> ≺ P' ⟹ P ⊕ Q ⟹a<νx> ≺ P'"
and "P ⟹α ≺ P' ⟹ P ⊕ Q ⟹α ≺ P'"
proof -
assume "P ⟹a<νx> ≺ P'"
then obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<νx> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(force dest: transitionE)
show "P ⊕ Q ⟹a<νx> ≺ P'"
proof(cases "P = P'''")
case True
have "P ⊕ Q ⟹⇩τ P ⊕ Q" by simp
moreover from P'''Trans ‹P = P'''› have "P ⊕ Q ⟼ a<νx> ≺ P''" by(blast intro: Sum1)
ultimately show ?thesis using P''Chain by(rule transitionI)
next
case False
from PChain ‹P ≠ P'''› have "P ⊕ Q ⟹⇩τ P'''" by(rule sum1Chain)
thus ?thesis using P'''Trans P''Chain by(rule transitionI)
qed
next
assume "P ⟹α ≺ P'"
then obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼α ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(force dest: transitionE)
show "P ⊕ Q ⟹α ≺ P'"
proof(cases "P = P'''")
case True
have "P ⊕ Q ⟹⇩τ P ⊕ Q" by simp
moreover from P'''Trans ‹P = P'''› have "P ⊕ Q ⟼α ≺ P''" by(blast intro: Sum1)
ultimately show ?thesis using P''Chain by(rule transitionI)
next
case False
from PChain ‹P ≠ P'''› have "P ⊕ Q ⟹⇩τ P'''" by(rule sum1Chain)
thus ?thesis using P'''Trans P''Chain by(rule transitionI)
qed
qed
lemma Sum2:
fixes Q :: pi
and a :: name
and x :: name
and Q' :: pi
and P :: pi
and α :: freeRes
shows "Q ⟹a<νx> ≺ Q' ⟹ P ⊕ Q ⟹a<νx> ≺ Q'"
and "Q ⟹α ≺ Q' ⟹ P ⊕ Q ⟹α ≺ Q'"
proof -
assume "Q ⟹a<νx> ≺ Q'"
then obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a<νx> ≺ Q''"
and Q''Chain: "Q'' ⟹⇩τ Q'"
by(force dest: transitionE)
show "P ⊕ Q ⟹a<νx> ≺ Q'"
proof(cases "Q = Q'''")
case True
have "P ⊕ Q ⟹⇩τ P ⊕ Q" by simp
moreover from Q'''Trans ‹Q = Q'''› have "P ⊕ Q ⟼a<νx> ≺ Q''" by(blast intro: Sum2)
ultimately show ?thesis using Q''Chain by(rule transitionI)
next
case False
from QChain ‹Q ≠ Q'''› have "P ⊕ Q ⟹⇩τ Q'''" by(rule sum2Chain)
thus ?thesis using Q'''Trans Q''Chain by(rule transitionI)
qed
next
assume "Q ⟹α ≺ Q'"
then obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼α ≺ Q''"
and Q''Chain: "Q'' ⟹⇩τ Q'"
by(force dest: transitionE)
show "P ⊕ Q ⟹α ≺ Q'"
proof(cases "Q = Q'''")
case True
have "P ⊕ Q ⟹⇩τ P ⊕ Q" by simp
moreover from Q'''Trans ‹Q = Q'''› have "P ⊕ Q ⟼α ≺ Q''" by(blast intro: Sum2)
ultimately show ?thesis using Q''Chain by(rule transitionI)
next
case False
from QChain ‹Q ≠ Q'''› have "P ⊕ Q ⟹⇩τ Q'''" by(rule sum2Chain)
thus ?thesis using Q'''Trans Q''Chain by(rule transitionI)
qed
qed
lemma Par1B:
fixes P :: pi
and a :: name
and x :: name
and P' :: pi
and Q :: pi
assumes PTrans: "P ⟹a<νx> ≺ P'"
and "x ♯ Q"
shows "P ∥ Q ⟹a<νx> ≺ (P' ∥ Q)"
proof -
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<νx> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain have "P ∥ Q ⟹⇩τ P''' ∥ Q" by(rule Par1Chain)
moreover from P'''Trans ‹x ♯ Q› have "P''' ∥ Q ⟼a<νx> ≺ (P'' ∥ Q)" by(rule Early_Semantics.Par1B)
moreover from P''Chain have "P'' ∥ Q ⟹⇩τ P' ∥ Q" by(rule Par1Chain)
ultimately show "P ∥ Q ⟹a<νx> ≺ (P' ∥ Q)" by(rule transitionI)
qed
lemma Par1F:
fixes P :: pi
and α :: freeRes
and P' :: pi
and Q :: pi
assumes PTrans: "P ⟹α ≺ P'"
shows "P ∥ Q ⟹α ≺ (P' ∥ Q)"
proof -
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼α ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain have "P ∥ Q ⟹⇩τ P''' ∥ Q" by(rule Par1Chain)
moreover from P'''Trans have "P''' ∥ Q ⟼α ≺ (P'' ∥ Q)" by(rule Early_Semantics.Par1F)
moreover from P''Chain have "P'' ∥ Q ⟹⇩τ P' ∥ Q" by(rule Par1Chain)
ultimately show ?thesis by(rule transitionI)
qed
lemma Par2B:
fixes Q :: pi
and a :: name
and x :: name
and Q' :: pi
and P :: pi
assumes QTrans: "Q ⟹a<νx> ≺ Q'"
and "x ♯ P"
shows "P ∥ Q ⟹a<νx> ≺ (P ∥ Q')"
proof -
from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a<νx> ≺ Q''"
and Q''Chain: "Q'' ⟹⇩τ Q'"
by(blast dest: transitionE)
from QChain have "P ∥ Q ⟹⇩τ P ∥ Q'''" by(rule Par2Chain)
moreover from Q'''Trans ‹x ♯ P› have "P ∥ Q''' ⟼a<νx> ≺ (P ∥ Q'')" by(rule Early_Semantics.Par2B)
moreover from Q''Chain have "P ∥ Q'' ⟹⇩τ P ∥ Q'" by(rule Par2Chain)
ultimately show "P ∥ Q ⟹a<νx> ≺ (P ∥ Q')" by(rule transitionI)
qed
lemma Par2F:
fixes Q :: pi
and α :: freeRes
and Q' :: pi
and P :: pi
assumes QTrans: "Q ⟹α ≺ Q'"
shows "P ∥ Q ⟹α ≺ (P ∥ Q')"
proof -
from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼α ≺ Q''"
and Q''Chain: "Q'' ⟹⇩τ Q'"
by(blast dest: transitionE)
from QChain have "P ∥ Q ⟹⇩τ P ∥ Q'''" by(rule Par2Chain)
moreover from Q'''Trans have "P ∥ Q''' ⟼α ≺ (P ∥ Q'')" by(rule Early_Semantics.Par2F)
moreover from Q''Chain have "P ∥ Q'' ⟹⇩τ P ∥ Q'" by(rule Par2Chain)
ultimately show ?thesis by(rule transitionI)
qed
lemma Comm1:
fixes P :: pi
and a :: name
and b :: name
and P' :: pi
and Q :: pi
and Q' :: pi
assumes PTrans: "P ⟹a<b> ≺ P'"
and QTrans: "Q ⟹a[b] ≺ Q'"
shows "P ∥ Q ⟹τ ≺ P' ∥ Q'"
proof -
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<b> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a[b] ≺ Q''"
and Q''Chain: "Q'' ⟹⇩τ Q'"
by(blast dest: transitionE)
from PChain QChain have "P ∥ Q ⟹⇩τ P''' ∥ Q'''" by(rule chainPar)
moreover from P'''Trans Q'''Trans have "P''' ∥ Q''' ⟼τ ≺ P'' ∥ Q''"
by(rule Early_Semantics.Comm1)
moreover from P''Chain Q''Chain have "P'' ∥ Q'' ⟹⇩τ P' ∥ Q'" by(rule chainPar)
ultimately show ?thesis by(rule transitionI)
qed
lemma Comm2:
fixes P :: pi
and a :: name
and b :: name
and P' :: pi
and Q :: pi
and Q' :: pi
assumes PTrans: "P ⟹a[b] ≺ P'"
and QTrans: "Q ⟹a<b> ≺ Q'"
shows "P ∥ Q ⟹τ ≺ P' ∥ Q'"
proof -
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a[b] ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a<b> ≺ Q''"
and Q''Chain: "Q'' ⟹⇩τ Q'"
by(blast dest: transitionE)
from PChain QChain have "P ∥ Q ⟹⇩τ P''' ∥ Q'''" by(rule chainPar)
moreover from P'''Trans Q'''Trans have "P''' ∥ Q''' ⟼τ ≺ P'' ∥ Q''"
by(rule Early_Semantics.Comm2)
moreover from P''Chain Q''Chain have "P'' ∥ Q'' ⟹⇩τ P' ∥ Q'" by(rule chainPar)
ultimately show ?thesis by(rule transitionI)
qed
lemma Close1:
fixes P :: pi
and a :: name
and x :: name
and P' :: pi
and Q :: pi
and Q' :: pi
assumes PTrans: "P ⟹a<x> ≺ P'"
and QTrans: "Q ⟹a<νx> ≺ Q'"
and "x ♯ P"
shows "P ∥ Q ⟹τ ≺ <νx>(P' ∥ Q')"
proof -
from PTrans obtain P''' P'' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<x> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a<νx> ≺ Q''"
and Q''Chain: "Q'' ⟹⇩τ Q'"
by(blast dest: transitionE)
from PChain QChain have "P ∥ Q ⟹⇩τ P''' ∥ Q'''" by(rule chainPar)
moreover from PChain ‹x ♯ P› have "x ♯ P'''" by(rule freshChain)
with P'''Trans Q'''Trans have "P''' ∥ Q''' ⟼τ ≺ <νx>(P'' ∥ Q'')"
by(rule Early_Semantics.Close1)
moreover from P''Chain Q''Chain have "P'' ∥ Q'' ⟹⇩τ P' ∥ Q'" by(rule chainPar)
hence "<νx>(P'' ∥ Q'') ⟹⇩τ <νx>(P' ∥ Q')" by(rule ResChain)
ultimately show ?thesis by(rule transitionI)
qed
lemma Close2:
fixes P :: pi
and a :: name
and x :: name
and P' :: pi
and Q :: pi
and Q' :: pi
assumes PTrans: "P ⟹a<νx> ≺ P'"
and QTrans: "Q ⟹a<x> ≺ Q'"
and xFreshQ: "x ♯ Q"
shows "P ∥ Q ⟹τ ≺ <νx>(P' ∥ Q')"
proof -
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<νx> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a<x> ≺ Q''"
and Q''Chain: "Q'' ⟹⇩τ Q'"
by(blast dest: transitionE)
from PChain QChain have "P ∥ Q ⟹⇩τ P''' ∥ Q'''" by(rule chainPar)
moreover from QChain ‹x ♯ Q› have "x ♯ Q'''" by(rule freshChain)
with P'''Trans Q'''Trans have "P''' ∥ Q''' ⟼τ ≺ <νx>(P'' ∥ Q'')"
by(rule Early_Semantics.Close2)
moreover from P''Chain Q''Chain have "P'' ∥ Q'' ⟹⇩τ P' ∥ Q'" by(rule chainPar)
hence "<νx>(P'' ∥ Q'') ⟹⇩τ <νx>(P' ∥ Q')" by(rule ResChain)
ultimately show ?thesis by(rule transitionI)
qed
lemma ResF:
fixes P :: pi
and α :: freeRes
and P' :: pi
and x :: name
assumes PTrans: "P ⟹α ≺ P'"
and "x ♯ α"
shows "<νx>P ⟹α ≺ <νx>P'"
proof -
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼α ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain have "<νx>P ⟹⇩τ <νx>P'''" by(rule ResChain)
moreover from P'''Trans ‹x ♯ α› have "<νx>P''' ⟼α ≺ <νx>P''"
by(rule Early_Semantics.ResF)
moreover from P''Chain have "<νx>P'' ⟹⇩τ <νx>P'" by(rule ResChain)
ultimately show ?thesis by(rule transitionI)
qed
lemma ResB:
fixes P :: pi
and a :: name
and x :: name
and P' :: pi
and y :: name
assumes PTrans: "P ⟹a<νx> ≺ P'"
and "y ≠ a"
and "y ≠ x"
shows "<νy>P ⟹a<νx> ≺ (<νy>P')"
proof -
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<νx> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain have "<νy>P ⟹⇩τ <νy>P'''" by(rule ResChain)
moreover from P'''Trans ‹y ≠ a› ‹y ≠ x› have "<νy>P''' ⟼a<νx> ≺ (<νy>P'')"
by(rule Early_Semantics.ResB)
moreover from P''Chain have "<νy>P'' ⟹⇩τ <νy>P'" by(rule ResChain)
ultimately show ?thesis by(rule transitionI)
qed
lemma Bang:
fixes P :: pi
and Rs :: residual
shows "P ∥ !P ⟹a<νx> ≺ P' ⟹ !P ⟹a<νx> ≺ P'"
and "P ∥ !P ⟹α ≺ P' ⟹ !P ⟹α ≺ P'"
proof -
assume PTrans: "P ∥ !P ⟹ a<νx> ≺ P'"
from PTrans obtain P'' P''' where PChain: "P ∥ !P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<νx> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(force dest: transitionE)
show "!P ⟹a<νx> ≺ P'"
proof(cases "P''' = P ∥ !P")
case True
have "!P ⟹⇩τ !P" by simp
moreover from P'''Trans ‹P''' = P ∥ !P› have "!P ⟼a<νx> ≺ P''" by(blast intro: Early_Semantics.Bang)
ultimately show ?thesis using P''Chain by(rule transitionI)
next
case False
from PChain ‹P''' ≠ P ∥ !P› have "!P ⟹⇩τ P'''" by(rule bangChain)
with P'''Trans P''Chain show ?thesis by(blast intro: transitionI)
qed
next
fix α P' P
assume "P ∥ !P ⟹α ≺ P'"
then obtain P'' P''' where PChain: "P ∥ !P ⟹⇩τ P''"
and P''Trans: "P'' ⟼α ≺ P'''"
and P'''Chain: "P''' ⟹⇩τ P'"
by(force dest: transitionE)
show "!P ⟹α ≺ P'"
proof(cases "P'' = P ∥ !P")
assume "P'' = P ∥ !P"
moreover with P''Trans have "!P ⟼α ≺ P'''" by(blast intro: Bang)
ultimately show ?thesis using PChain P'''Chain by(rule_tac transitionI, auto)
next
assume "P'' ≠ P ∥ !P"
with PChain have "!P ⟹⇩τ P''" by(rule bangChain)
with P''Trans P'''Chain show ?thesis by(blast intro: transitionI)
qed
qed
lemma tauTransitionChain:
fixes P :: pi
and P' :: pi
assumes "P ⟹τ ≺ P'"
shows "P ⟹⇩τ P'"
using assms
by(force dest: transitionE tauActTauChain)
lemma chainTransitionAppend:
fixes P :: pi
and P' :: pi
and Rs :: residual
and a :: name
and x :: name
and P'' :: pi
and α :: freeRes
shows "P ⟹a<νx> ≺ P'' ⟹ P'' ⟹⇩τ P' ⟹ P ⟹a<νx> ≺ P'"
and "P ⟹α ≺ P'' ⟹ P'' ⟹⇩τ P' ⟹ P ⟹α ≺ P'"
and "P ⟹⇩τ P'' ⟹ P'' ⟹a<νx> ≺ P' ⟹ P ⟹a<νx> ≺ P'"
and "P ⟹⇩τ P'' ⟹ P'' ⟹α ≺ P' ⟹ P ⟹α ≺ P'"
proof -
assume PTrans: "P ⟹ a<νx> ≺ P''"
assume P''Chain: "P'' ⟹⇩τ P'"
from PTrans obtain P''' P'''' where PChain: "P ⟹⇩τ P''''"
and P''''Trans: "P'''' ⟼a<νx> ≺ P'''"
and P'''Chain: "P''' ⟹⇩τ P''"
by(blast dest: transitionE)
from P'''Chain P''Chain have "P''' ⟹⇩τ P'" by auto
with PChain P''''Trans show "P ⟹a<νx> ≺ P'" by(rule transitionI)
next
assume PTrans: "P ⟹α ≺ P''"
assume P''Chain: "P'' ⟹⇩τ P'"
from PTrans obtain P''' P'''' where PChain: "P ⟹⇩τ P''''"
and P''''Trans: "P'''' ⟼α ≺ P'''"
and P'''Chain: "P''' ⟹⇩τ P''"
by(blast dest: transitionE)
from P'''Chain P''Chain have "P''' ⟹⇩τ P'" by auto
with PChain P''''Trans show "P ⟹α ≺ P'" by(rule transitionI)
next
assume PChain: "P ⟹⇩τ P''"
assume P''Trans: "P'' ⟹ a<νx> ≺ P'"
from P''Trans obtain P''' P'''' where P''Chain: "P'' ⟹⇩τ P''''"
and P''''Trans: "P'''' ⟼a<νx> ≺ P'''"
and P'''Chain: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain P''Chain have "P ⟹⇩τ P''''" by auto
thus "P ⟹a<νx> ≺ P'" using P''''Trans P'''Chain by(rule transitionI)
next
assume PChain: "P ⟹⇩τ P''"
assume P''Trans: "P'' ⟹α ≺ P'"
from P''Trans obtain P''' P'''' where P''Chain: "P'' ⟹⇩τ P''''"
and P''''Trans: "P'''' ⟼α ≺ P'''"
and P'''Chain: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain P''Chain have "P ⟹⇩τ P''''" by auto
thus "P ⟹α ≺ P'" using P''''Trans P'''Chain by(rule transitionI)
qed
lemma freshBoundOutputTransition:
fixes P :: pi
and a :: name
and x :: name
and P' :: pi
and c :: name
assumes PTrans: "P ⟹a<νx> ≺ P'"
and "c ♯ P"
and "c ≠ x"
shows "c ♯ P'"
proof -
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<νx> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain ‹c ♯ P› have "c ♯ P'''" by(rule freshChain)
with P'''Trans have "c ♯ P''" using ‹c ≠ x› by(rule Early_Semantics.freshTransition)
with P''Chain show "c ♯ P'" by(rule freshChain)
qed
lemma freshTauTransition:
fixes P :: pi
and c :: name
assumes PTrans: "P ⟹τ ≺ P'"
and "c ♯ P"
shows "c ♯ P'"
proof -
from PTrans have "P ⟹⇩τ P'" by(rule tauTransitionChain)
thus ?thesis using ‹c ♯ P› by(rule freshChain)
qed
lemma freshOutputTransition:
fixes P :: pi
and a :: name
and b :: name
and P' :: pi
and c :: name
assumes PTrans: "P ⟹a[b] ≺ P'"
and "c ♯ P"
shows "c ♯ P'"
proof -
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a[b] ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain ‹c ♯ P› have "c ♯ P'''" by(rule freshChain)
with P'''Trans have "c ♯ P''" by(rule Early_Semantics.freshTransition)
with P''Chain show ?thesis by(rule freshChain)
qed
lemma eqvtI[eqvt]:
fixes P :: pi
and a :: name
and x :: name
and P' :: pi
and p :: "name prm"
and α :: freeRes
shows "P ⟹a<νx> ≺ P' ⟹ (p ∙ P) ⟹(p ∙ a)<ν(p ∙ x)> ≺ (p ∙ P')"
and "P ⟹α ≺ P' ⟹ (p ∙ P) ⟹(p ∙ α) ≺ (p ∙ P')"
proof -
assume "P ⟹a<νx> ≺ P'"
then obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<νx> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain have "(p ∙ P) ⟹⇩τ (p ∙ P''')" by(rule eqvtChainI)
moreover from P'''Trans have "(p ∙ P''') ⟼ (p ∙ (a<νx> ≺ P''))"
by(rule TransitionsEarly.eqvt)
hence "(p ∙ P''') ⟼ (p ∙ a)<ν(p ∙ x)> ≺ (p ∙ P'')"
by(simp add: eqvts)
moreover from P''Chain have "(p ∙ P'') ⟹⇩τ (p ∙ P')" by(rule eqvtChainI)
ultimately show "(p ∙ P) ⟹(p ∙ a)<ν(p ∙ x)> ≺ (p ∙ P')"
by(rule transitionI)
next
assume "P ⟹α ≺ P'"
then obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼α ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain have "(p ∙ P) ⟹⇩τ (p ∙ P''')" by(rule eqvtChainI)
moreover from P'''Trans have "(p ∙ P''') ⟼ (p ∙ (α ≺ P''))"
by(rule TransitionsEarly.eqvt)
hence "(p ∙ P''') ⟼ (p ∙ α) ≺ (p ∙ P'')"
by(simp add: eqvts)
moreover from P''Chain have "(p ∙ P'') ⟹⇩τ (p ∙ P')" by(rule eqvtChainI)
ultimately show "(p ∙ P) ⟹(p ∙ α) ≺ (p ∙ P')"
by(rule transitionI)
qed
lemma freshInputTransition:
fixes P :: pi
and a :: name
and b :: name
and P' :: pi
and c :: name
assumes PTrans: "P ⟹a<b> ≺ P'"
and "c ♯ P"
and "c ≠ b"
shows "c ♯ P'"
proof -
from PTrans obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<b> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain ‹c ♯ P› have "c ♯ P'''" by(rule freshChain)
with P'''Trans have "c ♯ P''" using ‹c ≠ b› by(rule Early_Semantics.freshInputTransition)
with P''Chain show ?thesis by(rule freshChain)
qed
lemmas freshTransition = freshBoundOutputTransition freshOutputTransition
freshInputTransition freshTauTransition
end