Theory Weak_Late_Step_Semantics
theory Weak_Late_Step_Semantics
imports Late_Tau_Chain
begin
definition inputTransition :: "pi ⇒ name ⇒ pi ⇒ name ⇒ name ⇒ pi ⇒ bool" (‹_ ⟹⇩l_ in _→_<_> ≺ _› [80, 80, 80, 80, 80] 80)
where "P ⟹⇩lu in P'' →a<x> ≺ P' ≡ ∃P'''. P ⟹⇩τ P''' ∧ P''' ⟼a<x> ≺ P'' ∧ P''[x::=u] ⟹⇩τ P'"
definition transition :: "(pi × Late_Semantics.residual) set" where
"transition ≡ {x. ∃P P' α P'' P'''. P ⟹⇩τ P' ∧ P' ⟼α ≺ P'' ∧ P'' ⟹⇩τ P''' ∧ x = (P, α ≺ P''')} ∪
{x. ∃P P' a y P'' P'''. P ⟹⇩τ P' ∧ (P' ⟼(a<νy> ≺ P'')) ∧ P'' ⟹⇩τ P''' ∧ x = (P, (a<νy> ≺ P'''))}"
abbreviation weakTransition_judge :: "pi ⇒ Late_Semantics.residual ⇒ bool" (‹_ ⟹⇩l _› [80, 80] 80)
where "P ⟹⇩l Rs ≡ (P, Rs) ∈ transition"
lemma weakNonInput[dest]:
fixes P :: pi
and a :: name
and x :: name
and P' :: pi
assumes "P ⟹⇩la<x> ≺ P'"
shows False
using assms
by(auto simp add: transition_def residual.inject)
lemma transitionI:
fixes P :: pi
and P''' :: pi
and α :: freeRes
and P'' :: pi
and P' :: pi
and a :: name
and x :: name
and u :: name
shows "⟦P ⟹⇩τ P'''; P''' ⟼α ≺ P''; P'' ⟹⇩τ P'⟧ ⟹ P ⟹⇩lα ≺ P'"
and "⟦P ⟹⇩τ P'''; P''' ⟼a<νx> ≺ P''; P'' ⟹⇩τ P'⟧ ⟹ P ⟹⇩la<νx> ≺ P'"
and "⟦P ⟹⇩τ P'''; P''' ⟼a<x> ≺ P''; P''[x::=u] ⟹⇩τ P'⟧ ⟹ P ⟹⇩lu in P''→a<x> ≺ P'"
proof -
assume "P ⟹⇩τ P'''" and "P''' ⟼ α ≺ P''" and "P'' ⟹⇩τ P'"
thus "P ⟹⇩l α ≺ P'"
by(force simp add: transition_def)
next
assume "P ⟹⇩τ P'''" and "P''' ⟼a<νx> ≺ P''" and "P'' ⟹⇩τ P'"
thus "P ⟹⇩la<νx> ≺ P'"
by(force simp add: transition_def)
next
assume "P ⟹⇩τ P'''" and "P''' ⟼a<x> ≺ P''" and "P''[x::=u] ⟹⇩τ P'"
thus "P ⟹⇩lu in P''→a<x> ≺ P'"
by(force simp add: inputTransition_def)
qed
lemma transitionE:
fixes P :: pi
and α :: freeRes
and P' :: pi
and P'' :: pi
and a :: name
and u :: name
and x :: name
shows "P ⟹⇩lα ≺ P' ⟹ ∃P'' P'''. P ⟹⇩τ P'' ∧ P'' ⟼α ≺ P''' ∧ P''' ⟹⇩τ P'" (is "_ ⟹ ?thesis1")
and "⟦P ⟹⇩la<νx> ≺ P'; x ♯ P⟧ ⟹ ∃P'' P'''. P ⟹⇩τ P''' ∧ P''' ⟼a<νx> ≺ P'' ∧ P'' ⟹⇩τ P'"
and "⟦P ⟹⇩lu in P''→a<x> ≺ P'⟧ ⟹ ∃P'''. P ⟹⇩τ P''' ∧ P''' ⟼a<x> ≺ P'' ∧ P''[x::=u] ⟹⇩τ P'"
proof -
assume "P ⟹⇩lα ≺ P'"
thus ?thesis1 by(auto simp add: transition_def residual.inject)
next
assume "P ⟹⇩la<νx> ≺ P'" and "x ♯ P"
thus "∃P'' P'''. P ⟹⇩τ P''' ∧ P''' ⟼a<νx> ≺ P'' ∧ P'' ⟹⇩τ P'"
using [[hypsubst_thin = true]]
apply(auto simp add: transition_def residualInject name_abs_eq)
apply(rule_tac x="[(x, y)] ∙ P''" in exI)
apply(rule_tac x=P' in exI)
apply(clarsimp)
apply(auto)
apply(subgoal_tac "x ♯ P''")
apply(simp add: alphaBoundResidual name_swap)
using freshChain
apply(force dest: freshBoundDerivative)
using eqvtChainI
by simp
next
assume PTrans: "P ⟹⇩lu in P''→a<x> ≺ P'"
thus "∃P'''. P ⟹⇩τ P''' ∧ P''' ⟼ a<x> ≺ P'' ∧ P''[x::=u] ⟹⇩τ P'"
by(auto simp add: inputTransition_def)
qed
lemma alphaInput:
fixes P :: pi
and u :: name
and P'' :: pi
and a :: name
and x :: name
and P' :: pi
and y :: name
assumes PTrans: "P ⟹⇩lu in P''→a<x> ≺ P'"
and yFreshP: "y ♯ P"
shows "P ⟹⇩lu in ([(x, y)] ∙ P'')→a<y> ≺ P'"
proof(cases "x=y")
assume "x=y"
with PTrans show ?thesis by simp
next
assume xineqy: "x≠y"
from PTrans obtain P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<x> ≺ P''"
and P''Chain: "P''[x::=u] ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain yFreshP have "y ♯ P'''" by(rule freshChain)
with P'''Trans xineqy have yFreshP'': "y ♯ P''" by(blast dest: freshBoundDerivative)
with P'''Trans have "P''' ⟼a<y> ≺ [(x, y)] ∙ P''" by(simp add: alphaBoundResidual)
moreover from P''Chain yFreshP'' have "([(x, y)] ∙ P'')[y::=u] ⟹⇩τ P'"
by(simp add: renaming name_swap)
ultimately show ?thesis using PChain by(blast intro: transitionI)
qed
lemma tauActionChain:
fixes P :: pi
and P' :: pi
shows "P ⟹⇩lτ ≺ P' ⟹ P ⟹⇩τ P'"
and "P ≠ P' ⟹ P ⟹⇩τ P' ⟹ P ⟹⇩lτ ≺ P'"
proof -
assume "P ⟹⇩lτ ≺ P'"
then obtain P'' P''' where "P ⟹⇩τ P''"
and "P'' ⟼τ ≺ P'''"
and "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
thus "P ⟹⇩τ P'" by auto
next
assume "P ⟹⇩τ P'" and "P ≠ P'"
thus "P ⟹⇩lτ ≺ P'"
proof(induct rule: tauChainInduct)
case id
thus ?case by simp
next
case(ih P'' P''')
have "P ⟹⇩τ P''" and "P'' ⟼ τ ≺ P'''" by fact+
moreover have "P''' ⟹⇩τ P'''" by simp
ultimately show ?case by(rule transitionI)
qed
qed
lemma singleActionChain:
fixes P :: pi
and a :: name
and x :: name
and α :: freeRes
and u :: name
shows "P ⟼a<νx> ≺ P' ⟹ P ⟹⇩la<νx> ≺ P'"
and "⟦P ⟼a<x> ≺ P'⟧ ⟹ P ⟹⇩lu in P'→a<x> ≺ P'[x::=u]"
and "P ⟼α ≺ P' ⟹ P ⟹⇩lα ≺ P'"
proof -
assume "P ⟼a<νx> ≺ P'"
moreover have "P ⟹⇩τ P" by simp
moreover have "P' ⟹⇩τ P'" by simp
ultimately show "P ⟹⇩la<νx> ≺ P'" by(blast intro: transitionI)
next
assume "P ⟼a<x> ≺ P'"
moreover have "P ⟹⇩τ P" by simp
moreover have "P'[x::=u] ⟹⇩τ P'[x::=u]" by simp
ultimately show "P ⟹⇩lu in P'→a<x> ≺ P'[x::=u]" by(blast intro: transitionI)
next
assume "P ⟼α ≺ P'"
moreover have "P ⟹⇩τ P" by simp
moreover have "P' ⟹⇩τ P'" by simp
ultimately show "P ⟹⇩lα ≺ P'" by(blast intro: transitionI)
qed
lemma Tau:
fixes P :: pi
shows "τ.(P) ⟹⇩l τ ≺ P"
proof -
have "τ.(P) ⟹⇩τ τ.(P)" by simp
moreover have "τ.(P) ⟼τ ≺ P" by(rule transitions.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 ⟹⇩lu in P→a<x> ≺ P[x::=u]"
proof -
have "a<x>.P ⟹⇩τ a<x>.P" by simp
moreover have "a<x>.P ⟼ a<x> ≺ P" by(rule 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 ⟹⇩la[b] ≺ P"
proof -
have "a{b}.P ⟹⇩τ a{b}.P" by simp
moreover have "a{b}.P ⟼a[b] ≺ P" by(rule transitions.Output)
moreover have "P ⟹⇩τ P" by simp
ultimately show ?thesis by(rule transitionI)
qed
lemma Match:
fixes P :: pi
and Rs :: residual
and a :: name
and u :: name
and b :: name
and x :: name
and P' :: pi
shows "P ⟹⇩l Rs ⟹ [a⌢a]P ⟹⇩l Rs"
and "P ⟹⇩lu in P''→b<x> ≺ P' ⟹ [a⌢a]P ⟹⇩lu in P''→b<x> ≺ P'"
proof -
assume PTrans: "P ⟹⇩l Rs"
thus "[a⌢a]P ⟹⇩l Rs"
proof(nominal_induct avoiding: P rule: residual.strong_inducts)
case(BoundR b x P')
have PTrans: "P ⟹⇩l b«x» ≺ P'" and xFreshP: "x ♯ P" by fact+
from PTrans obtain b' where beq: "b = BoundOutputS b'" by(cases b) auto
with PTrans xFreshP obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼b'<νx> ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
show ?case
proof(cases "P = P''")
assume "P = P''"
moreover have "[a⌢a]P ⟹⇩τ [a⌢a]P" by simp
moreover from P''Trans have "[a⌢a]P'' ⟼ b'<νx> ≺ P'''" by(rule Match)
ultimately show ?thesis using beq P'''Trans by(blast intro: transitionI)
next
assume "P ≠ P''"
with PTrans have "[a⌢a]P ⟹⇩τ P''" by(rule matchChain)
thus ?thesis using beq P''Trans P'''Trans by(blast intro: transitionI)
qed
next
case(FreeR α P')
have "P ⟹⇩l α ≺ P'" by fact
then obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼ α ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
show ?case
proof(cases "P = P''")
assume "P = P''"
moreover have "[a⌢a]P ⟹⇩τ [a⌢a]P" by simp
moreover from P''Trans have "[a⌢a]P'' ⟼ α ≺ P'''" by(rule transitions.Match)
ultimately show ?thesis using P'''Trans by(blast intro: transitionI)
next
assume "P ≠ P''"
with PTrans have "[a⌢a]P ⟹⇩τ P''" by(rule matchChain)
thus ?thesis using P''Trans P'''Trans by(rule transitionI)
qed
qed
next
assume "P ⟹⇩lu in P''→b<x> ≺ P'"
then obtain P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼b<x> ≺ P''"
and P''Chain: "P''[x::=u] ⟹⇩τ P'"
by(blast dest: transitionE)
show "[a⌢a]P ⟹⇩lu in P''→b<x> ≺ P'"
proof(cases "P=P'''")
assume "P=P'''"
moreover have "[a⌢a]P ⟹⇩τ [a⌢a]P" by simp
moreover from P'''Trans have "[a⌢a]P''' ⟼b<x> ≺ P''" by(rule Late_Semantics.Match)
ultimately show ?thesis using P''Chain by(blast intro: transitionI)
next
assume "P ≠ P'''"
with PChain 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 Rs :: residual
and a :: name
and c :: name
and u :: name
and b :: name
and x :: name
and P' :: pi
shows "⟦P ⟹⇩l Rs; a ≠ c⟧ ⟹ [a≠c]P ⟹⇩l Rs"
and "⟦P ⟹⇩lu in P''→b<x> ≺ P'; a ≠ c⟧ ⟹ [a≠c]P ⟹⇩lu in P''→b<x> ≺ P'"
proof -
assume PTrans: "P ⟹⇩l Rs"
and aineqc: "a ≠ c"
thus "[a≠c]P ⟹⇩l Rs"
proof(nominal_induct avoiding: P rule: residual.strong_inducts)
case(BoundR b x P')
have PTrans: "P ⟹⇩l b«x» ≺ P'" and xFreshP: "x ♯ P" by fact+
from PTrans obtain b' where beq: "b = BoundOutputS b'" by(cases b, auto)
with PTrans xFreshP obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼b'<νx> ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
show ?case
proof(cases "P = P''")
assume "P = P''"
moreover have "[a≠c]P ⟹⇩τ [a≠c]P" by simp
moreover from P''Trans aineqc have "[a≠c]P'' ⟼b'<νx> ≺ P'''" by(rule transitions.Mismatch)
ultimately show ?thesis using beq P'''Trans by(blast intro: transitionI)
next
assume "P ≠ P''"
with PTrans aineqc have "[a≠c]P ⟹⇩τ P''" by(rule mismatchChain)
thus ?thesis using beq P''Trans P'''Trans by(blast intro: transitionI)
qed
next
case(FreeR α P')
have "P ⟹⇩l α ≺ P'" by fact
then obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼ α ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
show ?case
proof(cases "P = P''")
assume "P = P''"
moreover have "[a≠c]P ⟹⇩τ [a≠c]P" by simp
moreover from P''Trans ‹a ≠ c› have "[a≠c]P'' ⟼ α ≺ P'''" by(rule transitions.Mismatch)
ultimately show ?thesis using P'''Trans by(blast intro: transitionI)
next
assume "P ≠ P''"
with PTrans aineqc have "[a≠c]P ⟹⇩τ P''" by(rule mismatchChain)
thus ?thesis using P''Trans P'''Trans by(rule transitionI)
qed
qed
next
assume aineqc: "a ≠ c"
assume "P ⟹⇩lu in P''→b<x> ≺ P'"
then obtain P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼b<x> ≺ P''"
and P''Chain: "P''[x::=u] ⟹⇩τ P'"
by(blast dest: transitionE)
show "[a≠c]P ⟹⇩lu in P''→b<x> ≺ P'"
proof(cases "P=P'''")
assume "P=P'''"
moreover have "[a≠c]P ⟹⇩τ [a≠c]P" by simp
moreover from P'''Trans aineqc have "[a≠c]P''' ⟼b<x> ≺ P''" by(rule Late_Semantics.Mismatch)
ultimately show ?thesis using P''Chain by(blast intro: transitionI)
next
assume "P ≠ P'''"
with PChain aineqc have "[a≠c]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 Trans: "P ⟹⇩la[b] ≺ P'"
and aInEqb: "a ≠ b"
shows "<νb>P ⟹⇩la<νb> ≺ P'"
proof -
from Trans obtain P'' P''' where A: "P ⟹⇩τ P''"
and B: "P'' ⟼a[b] ≺ P'''"
and C: "P''' ⟹⇩τ P'"
by(force dest: transitionE)
from A have "<νb>P ⟹⇩τ <νb>P''" by(rule ResChain)
moreover from B aInEqb have "<νb>P'' ⟼a<νb> ≺ P'''" by(rule Open)
ultimately show ?thesis using C by(force simp add: transition_def)
qed
lemma Sum1:
fixes P :: pi
and Rs :: residual
and Q :: pi
and u :: name
and P'' :: pi
and a :: name
and x :: name
and P' :: pi
shows "P ⟹⇩l Rs ⟹ P ⊕ Q ⟹⇩l Rs"
and "P ⟹⇩lu in P''→a<x> ≺ P' ⟹ P ⊕ Q ⟹⇩lu in P''→a<x> ≺ P'"
proof -
assume "P ⟹⇩l Rs"
thus "P ⊕ Q ⟹⇩l Rs"
proof(nominal_induct avoiding: P rule: residual.strong_inducts)
case(BoundR a x P' P)
have PTrans: "P ⟹⇩la«x» ≺ P'"
and xFreshP: "x ♯ P" by fact+
from PTrans obtain a' where aeq: "a = BoundOutputS a'" by(cases a, auto)
with PTrans xFreshP obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼a'<νx> ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
show ?case
proof(cases "P = P''")
assume "P = P''"
moreover have "P ⊕ Q ⟹⇩τ P ⊕ Q" by simp
moreover from P''Trans have "P'' ⊕ Q ⟼a'<νx> ≺ P'''" by(rule transitions.Sum1)
ultimately show ?thesis using P'''Trans aeq by(blast intro: transitionI)
next
assume "P ≠ P''"
with PTrans have "P ⊕ Q ⟹⇩τ P''" by(rule sum1Chain)
thus ?thesis using P''Trans P'''Trans aeq by(blast intro: transitionI)
qed
next
case(FreeR α P')
have "P ⟹⇩l α ≺ P'" by fact
then obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼ α ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
show ?case
proof(cases "P = P''")
assume "P = P''"
moreover have "P ⊕ Q ⟹⇩τ P ⊕ Q" by simp
moreover from P''Trans have "P'' ⊕ Q ⟼ α ≺ P'''" by(rule transitions.Sum1)
ultimately show ?thesis using P'''Trans by(blast intro: transitionI)
next
assume "P ≠ P''"
with PTrans have "P ⊕ Q ⟹⇩τ P''" by(rule sum1Chain)
thus ?thesis using P''Trans P'''Trans by(rule transitionI)
qed
qed
next
assume "P ⟹⇩lu in P''→a<x> ≺ P'"
then obtain P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<x> ≺ P''"
and P''Chain: "P''[x::=u] ⟹⇩τ P'"
by(blast dest: transitionE)
show "P ⊕ Q ⟹⇩lu in P''→a<x> ≺ P'"
proof(cases "P = P'''")
assume "P = P'''"
moreover have "P ⊕ Q ⟹⇩τ P ⊕ Q" by simp
moreover from P'''Trans have "P''' ⊕ Q ⟼a<x> ≺ P''" by(rule transitions.Sum1)
ultimately show ?thesis using P''Chain by(blast intro: transitionI)
next
assume "P ≠ P'''"
with PChain have "P ⊕ Q ⟹⇩τ P'''" by(rule sum1Chain)
thus ?thesis using P'''Trans P''Chain by(blast intro: transitionI)
qed
qed
lemma Sum2:
fixes Q :: pi
and Rs :: residual
and P :: pi
and u :: name
and Q'' :: pi
and a :: name
and x :: name
and Q' :: pi
shows "Q ⟹⇩l Rs ⟹ P ⊕ Q ⟹⇩l Rs"
and "Q ⟹⇩lu in Q''→a<x> ≺ Q' ⟹ P ⊕ Q ⟹⇩lu in Q''→a<x> ≺ Q'"
proof -
assume "Q ⟹⇩l Rs"
thus "P ⊕ Q ⟹⇩l Rs"
proof(nominal_induct avoiding: Q rule: residual.strong_inducts)
case(BoundR a x Q' Q)
have QTrans: "Q ⟹⇩la«x» ≺ Q'"
and xFreshQ: "x ♯ Q" by fact+
from QTrans obtain a' where aeq: "a = BoundOutputS a'" by(cases a, auto)
with QTrans xFreshQ obtain Q'' Q''' where QTrans: "Q ⟹⇩τ Q''"
and Q''Trans: "Q'' ⟼a'<νx> ≺ Q'''"
and Q'''Trans: "Q''' ⟹⇩τ Q'"
by(blast dest: transitionE)
show ?case
proof(cases "Q = Q''")
assume "Q = Q''"
moreover have "P ⊕ Q ⟹⇩τ P ⊕ Q" by simp
moreover from Q''Trans have "P ⊕ Q'' ⟼a'<νx> ≺ Q'''" by(rule transitions.Sum2)
ultimately show ?thesis using Q'''Trans aeq by(blast intro: transitionI)
next
assume "Q ≠ Q''"
with QTrans have "P ⊕ Q ⟹⇩τ Q''" by(rule sum2Chain)
thus ?thesis using Q''Trans Q'''Trans aeq by(blast intro: transitionI)
qed
next
case(FreeR α Q')
have "Q ⟹⇩l α ≺ Q'" by fact
then obtain Q'' Q''' where QTrans: "Q ⟹⇩τ Q''"
and Q''Trans: "Q'' ⟼ α ≺ Q'''"
and Q'''Trans: "Q''' ⟹⇩τ Q'"
by(blast dest: transitionE)
show ?case
proof(cases "Q = Q''")
assume "Q = Q''"
moreover have "P ⊕ Q ⟹⇩τ P ⊕ Q" by simp
moreover from Q''Trans have "P ⊕ Q'' ⟼ α ≺ Q'''" by(rule transitions.Sum2)
ultimately show ?thesis using Q'''Trans by(blast intro: transitionI)
next
assume "Q ≠ Q''"
with QTrans have "P ⊕ Q ⟹⇩τ Q''" by(rule sum2Chain)
thus ?thesis using Q''Trans Q'''Trans by(rule transitionI)
qed
qed
next
assume "Q ⟹⇩lu in Q''→a<x> ≺ Q'"
then obtain Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a<x> ≺ Q''"
and Q''Chain: "Q''[x::=u] ⟹⇩τ Q'"
by(blast dest: transitionE)
show "P ⊕ Q ⟹⇩lu in Q''→a<x> ≺ Q'"
proof(cases "Q = Q'''")
assume "Q = Q'''"
moreover have "P ⊕ Q ⟹⇩τ P ⊕ Q" by simp
moreover from Q'''Trans have "P ⊕ Q''' ⟼a<x> ≺ Q''" by(rule transitions.Sum2)
ultimately show ?thesis using Q''Chain by(blast intro: transitionI)
next
assume "Q ≠ Q'''"
with QChain have "P ⊕ Q ⟹⇩τ Q'''" by(rule sum2Chain)
thus ?thesis using Q'''Trans Q''Chain by(blast intro: transitionI)
qed
qed
lemma Par1B:
fixes P :: pi
and a :: name
and x :: name
and P' :: pi
and u :: name
and P'' :: pi
shows "⟦P ⟹⇩la<νx> ≺ P'; x ♯ Q⟧ ⟹ P ∥ Q ⟹⇩la<νx> ≺ (P' ∥ Q)"
and "⟦P ⟹⇩lu in P''→a<x> ≺ P'; x ♯ Q⟧ ⟹ P ∥ Q ⟹⇩lu in (P'' ∥ Q)→a<x> ≺ P' ∥ Q"
proof -
assume PTrans: "P ⟹⇩l a<νx> ≺ P'"
assume xFreshQ: "x ♯ Q"
have Goal: "⋀P a x P' Q. ⟦P ⟹⇩la<νx> ≺ P'; x ♯ P; x ♯ Q⟧ ⟹ P ∥ Q ⟹⇩la<νx> ≺ (P' ∥ Q)"
proof -
fix P a x P' Q
assume PTrans: "P ⟹⇩la<νx> ≺ P'"
assume xFreshP: "x ♯ P"
assume xFreshQ: "x ♯ (Q::pi)"
from PTrans xFreshP obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼a<νx> ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
from PTrans have "P ∥ Q ⟹⇩τ P'' ∥ Q" by(rule Par1Chain)
moreover from P''Trans xFreshQ have "P'' ∥ Q ⟼a<νx> ≺ (P''' ∥ Q)" by(rule Par1B)
moreover from P'''Trans have "P''' ∥ Q ⟹⇩τ P' ∥ Q" by(rule Par1Chain)
ultimately show "P ∥ Q ⟹⇩la<νx> ≺ (P' ∥ Q)" by(rule transitionI)
qed
have "∃c::name. c ♯ (P, P', Q)" by(blast intro: name_exists_fresh)
then obtain c::name where cFreshP: "c ♯ P" and cFreshP': "c ♯ P'" and cFreshQ: "c ♯ Q"
by(force simp add: fresh_prod)
from cFreshP' have "a<νx> ≺ P' = a<νc> ≺ ([(x, c)] ∙ P')" by(rule alphaBoundResidual)
moreover have "a<νx> ≺ (P' ∥ Q) = a<νc> ≺ (([(x, c)] ∙ P') ∥ Q)"
proof -
from cFreshP' cFreshQ have "c ♯ P' ∥ Q" by simp
hence "a<νx> ≺ (P' ∥ Q) = a<νc> ≺ ([(x, c)] ∙ (P' ∥ Q))" by(rule alphaBoundResidual)
with cFreshQ xFreshQ show ?thesis by(simp add: name_fresh_fresh)
qed
ultimately show "P ∥ Q ⟹⇩l a<νx> ≺ P' ∥ Q" using PTrans cFreshP cFreshQ by(force intro: Goal)
next
assume PTrans: "P ⟹⇩lu in P''→a<x> ≺ P'"
and xFreshQ: "x ♯ Q"
from PTrans obtain P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<x> ≺ P''"
and P''Chain: "P''[x::=u] ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain have "P ∥ Q ⟹⇩τ P''' ∥ Q" by(rule Par1Chain)
moreover from P'''Trans xFreshQ have "P''' ∥ Q ⟼a<x> ≺ (P'' ∥ Q)" by(rule Par1B)
moreover have "(P'' ∥ Q)[x::=u] ⟹⇩τ P' ∥ Q"
proof -
from P''Chain have "P''[x::=u] ∥ Q ⟹⇩τ P' ∥ Q" by(rule Par1Chain)
with xFreshQ show ?thesis by(simp add: forget)
qed
ultimately show "P ∥ Q ⟹⇩lu in (P'' ∥ Q)→a<x> ≺ (P' ∥ Q)" by(rule transitionI)
qed
lemma Par1F:
fixes P :: pi
and α :: freeRes
and P' :: pi
assumes PTrans: "P ⟹⇩lα ≺ P'"
shows "P ∥ Q ⟹⇩lα ≺ (P' ∥ Q)"
proof -
from PTrans obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼α ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
from PTrans have "P ∥ Q ⟹⇩τ P'' ∥ Q" by(rule Par1Chain)
moreover from P''Trans have "P'' ∥ Q ⟼α ≺ (P''' ∥ Q)" by(rule transitions.Par1F)
moreover from P'''Trans 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
and u :: name
and Q'' :: pi
shows "Q ⟹⇩la<νx> ≺ Q' ⟹ x ♯ P ⟹ P ∥ Q ⟹⇩la<νx> ≺ (P ∥ Q')"
and "Q ⟹⇩lu in Q''→a<x> ≺ Q' ⟹ x ♯ P ⟹ P ∥ Q ⟹⇩lu in (P ∥ Q'')→a<x> ≺ P ∥ Q'"
proof -
assume QTrans: "Q ⟹⇩l a<νx> ≺ Q'"
assume xFreshP: "x ♯ P"
have Goal: "⋀Q a x Q' P. ⟦Q ⟹⇩la<νx> ≺ Q'; x ♯ Q; x ♯ P⟧ ⟹ P ∥ Q ⟹⇩la<νx> ≺ (P ∥ Q')"
proof -
fix Q a x Q' P
assume QTrans: "Q ⟹⇩la<νx> ≺ Q'"
assume xFreshQ: "x ♯ Q"
assume xFreshP: "x ♯ (P::pi)"
from QTrans xFreshQ obtain Q'' Q''' where QTrans: "Q ⟹⇩τ Q''"
and Q''Trans: "Q'' ⟼a<νx> ≺ Q'''"
and Q'''Trans: "Q''' ⟹⇩τ Q'"
by(blast dest: transitionE)
from QTrans have "P ∥ Q ⟹⇩τ P ∥ Q''" by(rule Par2Chain)
moreover from Q''Trans xFreshP have "P ∥ Q'' ⟼a<νx> ≺ (P ∥ Q''')" by(rule Par2B)
moreover from Q'''Trans have "P ∥ Q''' ⟹⇩τ P ∥ Q'" by(rule Par2Chain)
ultimately show "P ∥ Q ⟹⇩la<νx> ≺ (P ∥ Q')" by(rule transitionI)
qed
have "∃c::name. c ♯ (Q, Q', P)" by(blast intro: name_exists_fresh)
then obtain c::name where cFreshQ: "c ♯ Q" and cFreshQ': "c ♯ Q'" and cFreshP: "c ♯ P"
by(force simp add: fresh_prod)
from cFreshQ' have "a<νx> ≺ Q' = a<νc> ≺ ([(x, c)] ∙ Q')" by(rule alphaBoundResidual)
moreover have "a<νx> ≺ (P ∥ Q') = a<νc> ≺ (P ∥ ([(x, c)] ∙ Q'))"
proof -
from cFreshQ' cFreshP have "c ♯ P ∥ Q'" by simp
hence "a<νx> ≺ (P ∥ Q') = a<νc> ≺ ([(x, c)] ∙ (P ∥ Q'))" by(rule alphaBoundResidual)
with cFreshP xFreshP show ?thesis by(simp add: name_fresh_fresh)
qed
ultimately show "P ∥ Q ⟹⇩l a<νx> ≺ P ∥ Q'" using QTrans cFreshQ cFreshP by(force intro: Goal)
next
assume QTrans: "Q ⟹⇩lu in Q''→a<x> ≺ Q'"
and xFreshP: "x ♯ P"
from QTrans obtain Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a<x> ≺ Q''"
and Q''Chain: "Q''[x::=u] ⟹⇩τ Q'"
by(blast dest: transitionE)
from QChain have "P ∥ Q ⟹⇩τ P ∥ Q'''" by(rule Par2Chain)
moreover from Q'''Trans xFreshP have "P ∥ Q''' ⟼a<x> ≺ (P ∥ Q'')" by(rule Par2B)
moreover have "(P ∥ Q'')[x::=u] ⟹⇩τ P ∥ Q'"
proof -
from Q''Chain have "P ∥ (Q''[x::=u]) ⟹⇩τ P ∥ Q'" by(rule Par2Chain)
with xFreshP show ?thesis by(simp add: forget)
qed
ultimately show "P ∥ Q ⟹⇩lu in (P ∥ Q'')→a<x> ≺ (P ∥ Q')" by(rule transitionI)
qed
lemma Par2F:
fixes Q :: pi
and α :: freeRes
and Q' :: pi
assumes QTrans: "Q ⟹⇩lα ≺ Q'"
shows "P ∥ Q ⟹⇩lα ≺ (P ∥ Q')"
proof -
from QTrans obtain Q'' Q''' where QTrans: "Q ⟹⇩τ Q''"
and Q''Trans: "Q'' ⟼α ≺ Q'''"
and Q'''Trans: "Q''' ⟹⇩τ Q'"
by(blast dest: transitionE)
from QTrans have "P ∥ Q ⟹⇩τ P ∥ Q''" by(rule Par2Chain)
moreover from Q''Trans have "P ∥ Q'' ⟼α ≺ (P ∥ Q''')" by(rule transitions.Par2F)
moreover from Q'''Trans have "P ∥ Q''' ⟹⇩τ P ∥ Q'" by(rule Par2Chain)
ultimately show ?thesis by(rule transitionI)
qed
lemma Comm1:
fixes P :: pi
and b :: name
and P'' :: pi
and a :: name
and x :: name
and P' :: pi
and Q :: pi
and Q' :: pi
assumes PTrans: "P ⟹⇩lb in P'' →a<x> ≺ P'"
and QTrans: "Q ⟹⇩la[b] ≺ Q'"
shows "P ∥ Q ⟹⇩lτ ≺ P' ∥ Q'"
proof -
from PTrans obtain P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<x> ≺ P''"
and P''Chain: "P''[x::=b] ⟹⇩τ 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''[x::=b] ∥ Q''"
by(rule Comm1)
moreover from P''Chain Q''Chain have "P''[x::=b] ∥ 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 x :: name
and Q'' :: pi
and Q' :: pi
assumes PTrans: "P ⟹⇩la[b] ≺ P'"
and QTrans: "Q ⟹⇩lb in Q''→a<x> ≺ Q'"
shows "P ∥ Q ⟹⇩lτ ≺ 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''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a<x> ≺ Q''"
and Q''Chain: "Q''[x::=b] ⟹⇩τ 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''[x::=b])"
by(rule Comm2)
moreover from P''Chain Q''Chain have "P'' ∥ (Q''[x::=b]) ⟹⇩τ P' ∥ Q'" by(rule chainPar)
ultimately show ?thesis by(rule transitionI)
qed
lemma Close1:
fixes P :: pi
and y :: name
and P'' :: pi
and a :: name
and x :: name
and P' :: pi
and Q :: pi
and Q' :: pi
assumes PTrans: "P ⟹⇩ly in P''→a<x> ≺ P'"
and QTrans: "Q ⟹⇩la<νy> ≺ Q'"
and yFreshP: "y ♯ P"
and yFreshQ: "y ♯ Q"
shows "P ∥ Q ⟹⇩lτ ≺ <νy>(P' ∥ Q')"
proof -
from PTrans obtain P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<x> ≺ P''"
and P''Chain: "P''[x::=y] ⟹⇩τ P'"
by(blast dest: transitionE)
from QTrans yFreshQ obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a<νy> ≺ Q''"
and Q''Chain: "Q'' ⟹⇩τ Q'"
by(blast dest: transitionE)
from PChain yFreshP have yFreshP''': "y ♯ P'''" by(rule freshChain)
from PChain QChain have "P ∥ Q ⟹⇩τ P''' ∥ Q'''" by(rule chainPar)
moreover from P'''Trans Q'''Trans yFreshP''' have "P''' ∥ Q''' ⟼τ ≺ <νy>(P''[x::=y] ∥ Q'')"
by(rule Close1)
moreover have "<νy>(P''[x::=y] ∥ Q'') ⟹⇩τ <νy>(P' ∥ Q')"
proof -
from P''Chain Q''Chain have "P''[x::=y] ∥ Q'' ⟹⇩τ P' ∥ Q'" by(rule chainPar)
thus ?thesis by(rule ResChain)
qed
ultimately show "P ∥ Q ⟹⇩lτ ≺ <νy>(P' ∥ Q')" by(rule transitionI)
qed
lemma Close2:
fixes P :: pi
and y :: name
and a :: name
and x :: name
and P' :: pi
and Q :: pi
and Q'' :: pi
and Q' :: pi
assumes PTrans: "P ⟹⇩la<νy> ≺ P'"
and QTrans: "Q ⟹⇩ly in Q''→a<x> ≺ Q'"
and yFreshP: "y ♯ P"
and yFreshQ: "y ♯ Q"
shows "P ∥ Q ⟹⇩lτ ≺ <νy>(P' ∥ Q')"
proof -
from PTrans yFreshP obtain P'' P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<νy> ≺ P''"
and P''Chain: "P'' ⟹⇩τ P'"
by(blast dest: transitionE)
from QTrans obtain Q''' where QChain: "Q ⟹⇩τ Q'''"
and Q'''Trans: "Q''' ⟼a<x> ≺ Q''"
and Q''Chain: "Q''[x::=y] ⟹⇩τ Q'"
by(blast dest: transitionE)
from QChain yFreshQ have yFreshQ''': "y ♯ Q'''" by(rule freshChain)
from PChain QChain have "P ∥ Q ⟹⇩τ P''' ∥ Q'''" by(rule chainPar)
moreover from P'''Trans Q'''Trans yFreshQ''' have "P''' ∥ Q''' ⟼τ ≺ <νy>(P'' ∥ (Q''[x::=y]))"
by(rule Close2)
moreover have "<νy>(P'' ∥ (Q''[x::=y])) ⟹⇩τ <νy>(P' ∥ Q')"
proof -
from P''Chain Q''Chain have "P'' ∥ (Q''[x::=y]) ⟹⇩τ P' ∥ Q'" by(rule chainPar)
thus ?thesis by(rule ResChain)
qed
ultimately show "P ∥ Q ⟹⇩lτ ≺ <νy>(P' ∥ Q')" by(rule transitionI)
qed
lemma ResF:
fixes P :: pi
and α :: freeRes
and P' :: pi
and x :: name
assumes PTrans: "P ⟹⇩lα ≺ P'"
and xFreshAlpha: "x ♯ α"
shows "<νx>P ⟹⇩lα ≺ <ν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 xFreshAlpha have "<νx>P'' ⟼α ≺ <νx>P'''"
by(rule transitions.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
and u :: name
and P'' :: pi
shows "⟦P ⟹⇩la<νx> ≺ P'; y ≠ a; y ≠ x; x ♯ P⟧ ⟹ <νy>P ⟹⇩la<νx> ≺ (<νy>P')"
and "⟦P ⟹⇩lu in P''→a<x> ≺ P'; y ≠ a; y ≠ x; y ≠ u⟧ ⟹ <νy>P ⟹⇩lu in (<νy>P'')→a<x> ≺ (<νy>P')"
proof -
assume PTrans: "P ⟹⇩la<νx> ≺ P'"
and yineqa: "y ≠ a"
and yineqx: "y ≠ x"
and xFreshP: "x ♯ P"
from PTrans xFreshP 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 yineqa yineqx have "<νy>P'' ⟼a<νx> ≺ (<νy>P''')"
by(force intro: ResB)
moreover from P'''Chain have "<νy>P''' ⟹⇩τ <νy>P'" by(rule ResChain)
ultimately show "<νy>P ⟹⇩l a<νx> ≺ <νy>P'" by(rule transitionI)
next
assume PTrans: "P ⟹⇩lu in P''→a<x> ≺ P'"
and yineqa: "y ≠ a"
and yineqx: "y ≠ x"
and yinequ: "y ≠ u"
from PTrans obtain P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<x> ≺ P''"
and P''Chain: "P''[x::=u] ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain have "<νy>P ⟹⇩τ <νy>P'''" by(rule ResChain)
moreover from P'''Trans yineqa yineqx have "<νy>P''' ⟼a<x> ≺ (<νy>P'')"
by(force intro: ResB)
moreover have "(<νy>P'')[x::=u] ⟹⇩τ <νy>P'"
proof -
from P''Chain have "<νy>(P''[x::=u]) ⟹⇩τ <νy>P'" by(rule ResChain)
with yineqx yinequ show ?thesis by(simp add: eqvt_subs[THEN sym])
qed
ultimately show "<νy>P ⟹⇩lu in (<νy>P'')→a<x> ≺ <νy>P'" by(rule transitionI)
qed
lemma Bang:
fixes P :: pi
and Rs :: residual
and u :: name
and P'' :: pi
and a :: name
and x :: name
and P' :: pi
shows "P ∥ !P ⟹⇩l Rs ⟹ !P ⟹⇩l Rs"
and "P ∥ !P ⟹⇩lu in P''→a<x> ≺ P' ⟹ !P ⟹⇩lu in P''→a<x> ≺ P'"
proof -
assume "P ∥ !P ⟹⇩l Rs"
thus "!P ⟹⇩l Rs"
proof(nominal_induct avoiding: P rule: residual.strong_inducts)
case(BoundR a x P' P)
assume xFreshP: "x ♯ P"
assume PTrans: "P ∥ !P ⟹⇩la«x» ≺ P'"
from PTrans obtain a' where aeq: "a = BoundOutputS a'" by(cases a, auto)
with PTrans xFreshP 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 ⟹⇩la«x» ≺ P'"
proof(cases "P'' = P ∥ !P")
assume "P'' = P ∥ !P"
moreover with P''Trans have "!P ⟼a'<νx> ≺ P'''" by(blast intro: transitions.Bang)
ultimately show ?thesis using PChain P'''Chain aeq by(simp, rule_tac transitionI, auto)
next
assume "P'' ≠ P ∥ !P"
with PChain have "!P ⟹⇩τ P''" by(rule bangChain)
with P''Trans P'''Chain aeq show ?thesis by(blast intro: transitionI)
qed
next
fix α P' P
assume "P ∥ !P ⟹⇩lα ≺ 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 ⟹⇩lα ≺ P'"
proof(cases "P'' = P ∥ !P")
assume "P'' = P ∥ !P"
moreover with P''Trans have "!P ⟼α ≺ P'''" by(blast intro: transitions.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
next
assume "P ∥ !P ⟹⇩lu in P''→a<x> ≺ P'"
then obtain P''' where PChain: "P ∥ !P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<x> ≺ P''"
and P''Chain: "P''[x::=u] ⟹⇩τ P'"
by(force dest: transitionE)
show "!P ⟹⇩lu in P''→a<x> ≺ P'"
proof(cases "P''' = P ∥ !P")
assume "P''' = P ∥ !P"
moreover with P'''Trans have "!P ⟼a<x> ≺ P''" by(blast intro: transitions.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 ⟹⇩lτ ≺ P'"
shows "P ⟹⇩τ P'"
using assms
by(auto simp add: transition_def residualInject)
lemma chainTransitionAppend:
fixes P :: pi
and P' :: pi
and Rs :: residual
and a :: name
and x :: name
and P'' :: pi
and u :: name
and P''' :: pi
and α :: freeRes
shows "P ⟹⇩τ P' ⟹ P' ⟹⇩l Rs ⟹ P ⟹⇩l Rs"
and "P ⟹⇩τ P'' ⟹ P'' ⟹⇩lu in P'''→a<x> ≺ P' ⟹ P ⟹⇩lu in P'''→a<x> ≺ P'"
and "P ⟹⇩la<νx> ≺ P'' ⟹ P'' ⟹⇩τ P' ⟹ x ♯ P ⟹ P ⟹⇩la<νx> ≺ P'"
and "P ⟹⇩lu in P'''→a<x> ≺ P'' ⟹ P'' ⟹⇩τ P' ⟹ P ⟹⇩lu in P'''→a<x> ≺ P'"
and "P ⟹⇩lα ≺ P'' ⟹ P'' ⟹⇩τ P' ⟹ P ⟹⇩lα ≺ P'"
proof -
assume "P ⟹⇩τ P'" and "P' ⟹⇩l Rs"
thus "P ⟹⇩l Rs"
by(auto simp add: transition_def residualInject) (blast dest: rtrancl_trans)+
next
assume "P ⟹⇩τ P''" and "P'' ⟹⇩lu in P'''→a<x> ≺ P'"
thus "P ⟹⇩lu in P'''→a<x> ≺ P'"
apply(auto simp add: inputTransition_def residualInject)
by(blast dest: rtrancl_trans)+
next
assume PTrans: "P ⟹⇩l a<νx> ≺ P''"
assume P''Chain: "P'' ⟹⇩τ P'"
assume xFreshP: "x ♯ P"
from PTrans xFreshP 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 ⟹⇩la<νx> ≺ P'" by(rule transitionI)
next
assume PTrans: "P ⟹⇩lu in P'''→a<x> ≺ P''"
assume P''Chain: "P'' ⟹⇩τ P'"
from PTrans obtain P'''' where PChain: "P ⟹⇩τ P''''"
and P''''Trans: "P'''' ⟼a<x> ≺ P'''"
and P'''Chain: "P'''[x::=u] ⟹⇩τ P''"
by(blast dest: transitionE)
from P'''Chain P''Chain have "P'''[x::=u] ⟹⇩τ P'" by auto
with PChain P''''Trans show "P ⟹⇩lu in P'''→a<x> ≺ P'" by(blast intro: transitionI)
next
assume PTrans: "P ⟹⇩lα ≺ 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 ⟹⇩lα ≺ P'" by(rule transitionI)
qed
lemma freshInputTransition:
fixes P :: pi
and a :: name
and x :: name
and u :: name
and P'' :: pi
and P' :: pi
and c :: name
assumes PTrans: "P ⟹⇩lu in P''→a<x> ≺ P'"
and cFreshP: "c ♯ P"
and cinequ: "c ≠ u"
shows "c ♯ P'"
proof -
from PTrans obtain P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<x> ≺ P''"
and P''Chain: "P''[x::=u] ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain cFreshP have cFreshP''': "c ♯ P'''" by(rule freshChain)
show "c ♯ P'"
proof(cases "x=c")
assume xeqc: "x=c"
from cinequ have "c ♯ P''[c::=u]" apply - by(rule fresh_fact2)
with P''Chain xeqc show ?thesis by(force intro: freshChain)
next
assume xineqc: "x≠c"
with P'''Trans cFreshP''' have "c ♯ P''" by(blast dest: freshBoundDerivative)
with cinequ have "c ♯ P''[x::=u]"
apply -
apply(rule fresh_fact1)
by simp
with P''Chain show ?thesis by(rule freshChain)
qed
qed
lemma freshBoundOutputTransition:
fixes P :: pi
and a :: name
and x :: name
and P' :: pi
and c :: name
assumes PTrans: "P ⟹⇩la<νx> ≺ P'"
and cFreshP: "c ♯ P"
and cineqx: "c ≠ x"
shows "c ♯ P'"
proof -
have Goal: "⋀P a x P' c. ⟦P ⟹⇩la<νx> ≺ P'; x ♯ P; c ♯ P; c ≠ x⟧ ⟹ c ♯ P'"
proof -
fix P a x P' c
assume PTrans: "P ⟹⇩la<νx> ≺ P'"
assume xFreshP: "x ♯ P"
assume cFreshP: "(c::name) ♯ P"
assume cineqx: "c ≠ x"
from PTrans xFreshP obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼a<νx> ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
from PTrans cFreshP have "c ♯ P''" by(rule freshChain)
with P''Trans cineqx have "c ♯ P'''" by(blast dest: Late_Semantics.freshBoundDerivative)
with P'''Trans show "c ♯ P'" by(rule freshChain)
qed
have "∃d::name. d ♯ (P, P', c)" by(blast intro: name_exists_fresh)
then obtain d::name where dFreshP: "d ♯ P" and dFreshP': "d ♯ P'" and cineqd: "c ≠ d"
by(force simp add: fresh_prod)
from PTrans dFreshP' have "P ⟹⇩la<νd> ≺ ([(x, d)] ∙ P')" by(simp add: alphaBoundResidual)
hence "c ♯ [(x, d)] ∙ P'" using dFreshP cFreshP cineqd by(rule Goal)
with cineqd cineqx show ?thesis by(simp add: name_fresh_left name_calc)
qed
lemma freshTauTransition:
fixes P :: pi
and c :: name
assumes PTrans: "P ⟹⇩lτ ≺ P'"
and cFreshP: "c ♯ P"
shows "c ♯ P'"
proof -
from PTrans have "P ⟹⇩τ P'" by(rule tauTransitionChain)
thus ?thesis using cFreshP by(rule freshChain)
qed
lemma freshOutputTransition:
fixes P :: pi
and a :: name
and b :: name
and P' :: pi
and c :: name
assumes PTrans: "P ⟹⇩la[b] ≺ P'"
and cFreshP: "c ♯ P"
shows "c ♯ P'"
proof -
from PTrans obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼a[b] ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
from PTrans cFreshP have "c ♯ P''" by(rule freshChain)
with P''Trans have "c ♯ P'''" by(blast dest: Late_Semantics.freshFreeDerivative)
with P'''Trans show ?thesis by(rule freshChain)
qed
lemma eqvtI:
fixes P :: pi
and Rs :: residual
and perm :: "name prm"
and u :: name
and P'' :: pi
and a :: name
and x :: name
and P' :: pi
shows "P ⟹⇩l Rs ⟹ (perm ∙ P) ⟹⇩l (perm ∙ Rs)"
and "P ⟹⇩lu in P''→a<x> ≺ P' ⟹ (perm ∙ P) ⟹⇩l(perm ∙ u) in (perm ∙ P'')→(perm ∙ a)<(perm ∙ x)> ≺ (perm ∙ P')"
proof -
assume "P ⟹⇩l Rs"
thus "(perm ∙ P) ⟹⇩l (perm ∙ Rs)"
proof(nominal_induct Rs avoiding: P rule: residual.strong_inducts)
case(BoundR a x P' P)
have PTrans: "P ⟹⇩la«x» ≺ P'" by fact
moreover then obtain b where aeqb: "a = BoundOutputS b" by(cases a, auto)
moreover have "x ♯ P" by fact
ultimately obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼b<νx> ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
from PTrans have "(perm ∙ P) ⟹⇩τ (perm ∙ P'')" by(rule eqvtChainI)
moreover from P''Trans have "(perm ∙ P'') ⟼ (perm ∙ (b<νx> ≺ P'''))"
by(rule eqvts)
moreover from P'''Trans have "(perm ∙ P''') ⟹⇩τ (perm ∙ P')" by(rule eqvtChainI)
ultimately show ?case using aeqb by(force intro: transitionI)
next
case(FreeR α P' P)
have "P ⟹⇩lα ≺ P'" by fact
then obtain P'' P''' where PTrans: "P ⟹⇩τ P''"
and P''Trans: "P'' ⟼α ≺ P'''"
and P'''Trans: "P''' ⟹⇩τ P'"
by(blast dest: transitionE)
from PTrans have "(perm ∙ P) ⟹⇩τ (perm ∙ P'')" by(rule eqvtChainI)
moreover from P''Trans have "(perm ∙ P'') ⟼ (perm ∙ (α ≺ P'''))"
by(rule eqvts)
moreover from P'''Trans have "(perm ∙ P''') ⟹⇩τ (perm ∙ P')" by(rule eqvtChainI)
ultimately show ?case by(force intro: transitionI)
qed
next
assume "P ⟹⇩lu in P''→a<x> ≺ P'"
then obtain P''' where PChain: "P ⟹⇩τ P'''"
and P'''Trans: "P''' ⟼a<x> ≺ P''"
and P''Chain: "P''[x::=u] ⟹⇩τ P'"
by(blast dest: transitionE)
from PChain have "(perm ∙ P) ⟹⇩τ (perm ∙ P''')" by(rule eqvtChainI)
moreover from P'''Trans have "(perm ∙ P''') ⟼ (perm ∙ (a<x> ≺ P''))"
by(rule eqvts)
moreover from P''Chain have "(perm ∙ P''[x::=u]) ⟹⇩τ (perm ∙ P')" by(rule eqvtChainI)
ultimately show "(perm ∙ P) ⟹⇩l(perm ∙ u) in (perm ∙ P'')→(perm ∙ a)<(perm ∙ x)> ≺ (perm ∙ P')"
by(force intro: transitionI simp add: eqvt_subs[THEN sym] perm_bij)
qed
lemmas freshTransition = freshBoundOutputTransition freshOutputTransition
freshInputTransition freshTauTransition
end