Theory Bisim_Struct_Cong
theory Bisim_Struct_Cong
imports Bisim_Pres Sim_Struct_Cong Structural_Congruence
begin
context env begin
lemma bisimParComm:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
shows "Ψ ⊳ P ∥ Q ∼ Q ∥ P"
proof -
let ?X = "{((Ψ::'b), ⦇ν*xvec⦈((P::('a, 'b, 'c) psi) ∥ Q), ⦇ν*xvec⦈(Q ∥ P)) | xvec Ψ P Q. xvec ♯* Ψ}"
have "eqvt ?X"
by(force simp add: eqvt_def pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst] eqvts)
have "(Ψ, P ∥ Q, Q ∥ P) ∈ ?X"
apply auto by(rule_tac x="[]" in exI) auto
thus ?thesis
proof(coinduct rule: bisimWeakCoinduct)
case(cStatEq Ψ PQ QP)
from ‹(Ψ, PQ, QP) ∈ ?X›
obtain xvec P Q where PFrQ: "PQ = ⦇ν*xvec⦈(P ∥ Q)" and QFrP: "QP = ⦇ν*xvec⦈(Q ∥ P)" and "xvec ♯* Ψ"
by auto
obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "A⇩P ♯* Q"
by(rule_tac C="(Ψ, Q)" in freshFrame) auto
obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* A⇩P" and "A⇩Q ♯* Ψ⇩P"
by(rule_tac C="(Ψ, A⇩P, Ψ⇩P)" in freshFrame) auto
from FrQ ‹A⇩Q ♯* A⇩P› ‹A⇩P ♯* Q› have "A⇩P ♯* Ψ⇩Q" by(force dest: extractFrameFreshChain)
have "⟨(xvec@A⇩P@A⇩Q), Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q⟩ ≃⇩F ⟨(xvec@A⇩Q@A⇩P), Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩P⟩"
by(simp add: frameChainAppend)
(metis frameResChainPres frameResChainComm frameNilStatEq compositionSym Associativity Commutativity FrameStatEqTrans)
with FrP FrQ PFrQ QFrP ‹A⇩P ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ⇩P› ‹A⇩Q ♯* A⇩P› ‹xvec ♯* Ψ› ‹A⇩P ♯* Ψ› ‹A⇩Q ♯* Ψ›
show ?case by(auto simp add: frameChainAppend)
next
case(cSim Ψ PQ QP)
from ‹(Ψ, PQ, QP) ∈ ?X›
obtain xvec P Q where PFrQ: "PQ = ⦇ν*xvec⦈(P ∥ Q)" and QFrP: "QP = ⦇ν*xvec⦈(Q ∥ P)"
and "xvec ♯* Ψ"
by auto
moreover have "Ψ ⊳ ⦇ν*xvec⦈(P ∥ Q) ↝[?X] ⦇ν*xvec⦈(Q ∥ P)"
proof -
have "Ψ ⊳ P ∥ Q ↝[?X] Q ∥ P"
proof -
note ‹eqvt ?X›
moreover have "⋀Ψ P Q. (Ψ, P ∥ Q, Q ∥ P) ∈ ?X"
apply auto by(rule_tac x="[]" in exI) auto
moreover have "⋀Ψ P Q xvec. ⟦(Ψ, P, Q) ∈ ?X; xvec ♯* Ψ⟧ ⟹ (Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) ∈ ?X"
apply(induct xvec, auto)
by(rule_tac x="xvec@xveca" in exI) (auto simp add: resChainAppend)
ultimately show ?thesis by(rule simParComm)
qed
moreover note ‹eqvt ?X› ‹xvec ♯* Ψ›
moreover have "⋀Ψ P Q x. ⟦(Ψ, P, Q) ∈ ?X; x ♯ Ψ⟧ ⟹ (Ψ, ⦇νx⦈P, ⦇νx⦈Q) ∈ ?X"
apply auto
by(rule_tac x="x#xvec" in exI) auto
ultimately show ?thesis by(rule resChainPres)
qed
ultimately show ?case by simp
next
case(cExt Ψ PQ QP Ψ')
from ‹(Ψ, PQ, QP) ∈ ?X›
obtain xvec P Q where PFrQ: "PQ = ⦇ν*xvec⦈(P ∥ Q)" and QFrP: "QP = ⦇ν*xvec⦈(Q ∥ P)"
and "xvec ♯* Ψ"
by auto
obtain p where "(p ∙ xvec) ♯* Ψ"
and "(p ∙ xvec) ♯* P"
and "(p ∙ xvec) ♯* Q"
and "(p ∙ xvec) ♯* Ψ'"
and S: "(set p) ⊆ (set xvec) × (set(p ∙ xvec))" and "distinctPerm p"
by(rule_tac c="(Ψ, P, Q, Ψ')" in name_list_avoiding) auto
from ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* Q› S have "⦇ν*xvec⦈(P ∥ Q) = ⦇ν*(p ∙ xvec)⦈(p ∙ (P ∥ Q))"
by(subst resChainAlpha) auto
hence PQAlpha: "⦇ν*xvec⦈(P ∥ Q) = ⦇ν*(p ∙ xvec)⦈((p ∙ P) ∥ (p ∙ Q))"
by(simp add: eqvts)
from ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* Q› S have "⦇ν*xvec⦈(Q ∥ P) = ⦇ν*(p ∙ xvec)⦈(p ∙ (Q ∥ P))"
by(subst resChainAlpha) auto
hence QPAlpha: "⦇ν*xvec⦈(Q ∥ P) = ⦇ν*(p ∙ xvec)⦈((p ∙ Q) ∥ (p ∙ P))"
by(simp add: eqvts)
from ‹(p ∙ xvec) ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ'› have "(Ψ ⊗ Ψ', ⦇ν*(p ∙ xvec)⦈((p ∙ P) ∥ (p ∙ Q)), ⦇ν*(p ∙ xvec)⦈((p ∙ Q) ∥ (p ∙ P))) ∈ ?X"
by auto
with PFrQ QFrP PQAlpha QPAlpha show ?case by simp
next
case(cSym Ψ PR QR)
thus ?case by blast
qed
qed
lemma bisimResComm:
fixes x :: name
and Ψ :: 'b
and y :: name
and P :: "('a, 'b, 'c) psi"
shows "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ∼ ⦇νy⦈(⦇νx⦈P)"
proof(cases "x=y")
case True
thus ?thesis by(blast intro: bisimReflexive)
next
case False
{
fix x::name and y::name and P::"('a, 'b, 'c) psi"
assume "x ♯ Ψ" and "y ♯ Ψ"
let ?X = "{((Ψ::'b), ⦇νx⦈(⦇νy⦈(P::('a, 'b, 'c) psi)), ⦇νy⦈(⦇νx⦈P)) | Ψ x y P. x ♯ Ψ ∧ y ♯ Ψ}"
from ‹x ♯ Ψ› ‹y ♯ Ψ› have "(Ψ, ⦇νx⦈(⦇νy⦈P), ⦇νy⦈(⦇νx⦈P)) ∈ ?X" by auto
hence "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ∼ ⦇νy⦈(⦇νx⦈P)"
proof(coinduct rule: bisimCoinduct)
case(cStatEq Ψ xyP yxP)
from ‹(Ψ, xyP, yxP) ∈ ?X› obtain x y P where "x ♯ Ψ" and "y ♯ Ψ" and "xyP = ⦇νx⦈(⦇νy⦈P)" and "yxP = ⦇νy⦈(⦇νx⦈P)" by auto
moreover obtain A⇩P Ψ⇩P where "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "x ♯ A⇩P" and "y ♯ A⇩P"
by(rule_tac C="(x, y, Ψ)" in freshFrame) auto
ultimately show ?case by(force intro: frameResComm FrameStatEqTrans)
next
case(cSim Ψ xyP yxP)
from ‹(Ψ, xyP, yxP) ∈ ?X› obtain x y P where "x ♯ Ψ" and "y ♯ Ψ" and "xyP = ⦇νx⦈(⦇νy⦈P)" and "yxP = ⦇νy⦈(⦇νx⦈P)" by auto
note ‹x ♯ Ψ› ‹y ♯ Ψ›
moreover have "eqvt ?X" by(force simp add: eqvt_def pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
hence "eqvt(?X ∪ bisim)" by auto
moreover have "⋀Ψ P. (Ψ, P, P) ∈ ?X ∪ bisim" by(blast intro: bisimReflexive)
moreover have "⋀Ψ x y P. ⟦x ♯ Ψ; y ♯ Ψ⟧ ⟹ (Ψ, ⦇νx⦈(⦇νy⦈P), ⦇νy⦈(⦇νx⦈P)) ∈ ?X ∪ bisim" by auto
ultimately have "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ↝[(?X ∪ bisim)] ⦇νy⦈(⦇νx⦈P)" by(rule resComm)
with ‹xyP = ⦇νx⦈(⦇νy⦈P)› ‹yxP = ⦇νy⦈(⦇νx⦈P)› show ?case
by simp
next
case(cExt Ψ xyP yxP Ψ')
from ‹(Ψ, xyP, yxP) ∈ ?X› obtain x y P where "x ♯ Ψ" and "y ♯ Ψ" and xyPeq: "xyP = ⦇νx⦈(⦇νy⦈P)" and yxPeq: "yxP = ⦇νy⦈(⦇νx⦈P)" by auto
show ?case
proof(case_tac "x=y")
assume "x = y"
with xyPeq yxPeq show ?case
by(blast intro: bisimReflexive)
next
assume "x ≠ y"
obtain x' where "x' ♯ Ψ" and "x' ♯ Ψ'" and "x' ≠ x" and "x' ≠ y" and "x' ♯ P" by(generate_fresh "name") (auto simp add: fresh_prod)
obtain y' where "y' ♯ Ψ" and "y' ♯ Ψ'" and "y' ≠ x" and "x' ≠ y'" and "y' ≠ y" and "y' ♯ P" by(generate_fresh "name") (auto simp add: fresh_prod)
with xyPeq ‹y' ♯ P› ‹x' ♯ P› ‹x ≠ y› ‹x' ≠ y› ‹y' ≠ x› have "⦇νx⦈(⦇νy⦈P) = ⦇νx'⦈(⦇νy'⦈([(x, x')] ∙ [(y, y')] ∙ P))"
apply(subst alphaRes[of x']) apply(simp add: abs_fresh) by(subst alphaRes[of y' _ y]) (auto simp add: eqvts calc_atm)
moreover with yxPeq ‹y' ♯ P› ‹x' ♯ P› ‹x ≠ y› ‹x' ≠ y› ‹y' ≠ x› ‹x' ≠ y'› have "⦇νy⦈(⦇νx⦈P) = ⦇νy'⦈(⦇νx'⦈([(y, y')] ∙ [(x, x')] ∙ P))"
apply(subst alphaRes[of y']) apply(simp add: abs_fresh) by(subst alphaRes[of x' _ x]) (auto simp add: eqvts calc_atm)
with ‹x ≠ y› ‹x' ≠ y› ‹y' ≠ y› ‹x' ≠ x› ‹y' ≠ x› ‹x' ≠ y'› have "⦇νy⦈(⦇νx⦈P) = ⦇νy'⦈(⦇νx'⦈([(x, x')] ∙ [(y, y')] ∙ P))"
by(subst perm_compose) (simp add: calc_atm)
moreover from ‹x' ♯ Ψ› ‹x' ♯ Ψ'› ‹y' ♯ Ψ› ‹y' ♯ Ψ'› have "(Ψ ⊗ Ψ', ⦇νx'⦈(⦇νy'⦈([(x, x')] ∙ [(y, y')] ∙ P)), ⦇νy'⦈(⦇νx'⦈([(x, x')] ∙ [(y, y')] ∙ P))) ∈ ?X"
by auto
ultimately show ?case using xyPeq yxPeq by simp
qed
next
case(cSym Ψ xyP yxP)
thus ?case by auto
qed
}
moreover obtain x'::name where "x' ♯ Ψ" and "x' ♯ P" and "x' ≠ x" and "x' ≠ y"
by(generate_fresh "name") auto
moreover obtain y'::name where "y' ♯ Ψ" and "y' ♯ P" and "y' ≠ x" and "y' ≠ y" and "y' ≠ x'"
by(generate_fresh "name") auto
ultimately have "Ψ ⊳ ⦇νx'⦈(⦇νy'⦈([(y, y'), (x, x')] ∙ P)) ∼ ⦇νy'⦈(⦇νx'⦈([(y, y'), (x, x')] ∙ P))" by auto
thus ?thesis using ‹x' ♯ P› ‹x' ≠ x› ‹x' ≠ y› ‹y' ♯ P› ‹y' ≠ x› ‹y' ≠ y› ‹y' ≠ x'› ‹x ≠ y›
apply(subst alphaRes[where x=x and y=x' and P=P], auto)
apply(subst alphaRes[where x=y and y=y' and P=P], auto)
apply(subst alphaRes[where x=x and y=x' and P="⦇νy'⦈([(y, y')] ∙ P)"], auto simp add: abs_fresh fresh_left)
apply(subst alphaRes[where x=y and y=y' and P="⦇νx'⦈([(x, x')] ∙ P)"], auto simp add: abs_fresh fresh_left)
by(subst perm_compose) (simp add: eqvts calc_atm)
qed
lemma bisimResComm':
fixes x :: name
and Ψ :: 'b
and xvec :: "name list"
and P :: "('a, 'b, 'c) psi"
assumes "x ♯ Ψ"
and "xvec ♯* Ψ"
shows "Ψ ⊳ ⦇νx⦈(⦇ν*xvec⦈P) ∼ ⦇ν*xvec⦈(⦇νx⦈P)"
using assms
by(induct xvec) (auto intro: bisimResComm bisimReflexive bisimResPres bisimTransitive)
lemma bisimScopeExt:
fixes x :: name
and Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
assumes "x ♯ P"
shows "Ψ ⊳ ⦇νx⦈(P ∥ Q) ∼ P ∥ ⦇νx⦈Q"
proof -
{
fix x::name and Q :: "('a, 'b, 'c) psi"
assume "x ♯ Ψ" and "x ♯ P"
let ?X1 = "{((Ψ::'b), ⦇ν*xvec⦈(⦇νx⦈((P::('a, 'b, 'c) psi) ∥ Q)), ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)) | Ψ xvec x P Q. x ♯ Ψ ∧ x ♯ P ∧ xvec ♯* Ψ}"
let ?X2 = "{((Ψ::'b), ⦇ν*xvec⦈((P::('a, 'b, 'c) psi) ∥ ⦇νx⦈Q), ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))) | Ψ xvec x P Q. x ♯ Ψ ∧ x ♯ P ∧ xvec ♯* Ψ}"
let ?X = "?X1 ∪ ?X2"
from ‹x ♯ Ψ› ‹x ♯ P› have "(Ψ, ⦇νx⦈(P ∥ Q), P ∥ ⦇νx⦈Q) ∈ ?X"
by(auto, rule_tac x="[]" in exI) (auto simp add: fresh_list_nil)
moreover have "eqvt ?X"
by(rule eqvtUnion)
(fastforce simp add: eqvt_def eqvts pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst] pt_fresh_bij[OF pt_name_inst, OF at_name_inst])+
ultimately have "Ψ ⊳ ⦇νx⦈(P ∥ Q) ∼ P ∥ ⦇νx⦈Q"
proof(coinduct rule: transitiveCoinduct)
case(cStatEq Ψ R T)
show ?case
proof(case_tac "(Ψ, R, T) ∈ ?X1")
assume "(Ψ, R, T) ∈ ?X1"
then obtain xvec x P Q where "R = ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))" and "T = ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)" and "xvec ♯* Ψ" and "x ♯ P" and "x ♯ Ψ"
by auto
moreover obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "x ♯ A⇩P" and "A⇩P ♯* Q"
by(rule_tac C="(Ψ, x, Q)" in freshFrame) auto
moreover obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "x ♯ A⇩Q" and "A⇩Q ♯* A⇩P" and "A⇩Q ♯* Ψ⇩P"
by(rule_tac C="(Ψ, x, A⇩P, Ψ⇩P)" in freshFrame) auto
moreover from FrQ ‹A⇩P ♯* Q› ‹A⇩Q ♯* A⇩P› have "A⇩P ♯* Ψ⇩Q"
by(drule_tac extractFrameFreshChain) auto
moreover from ‹x ♯ P› ‹x ♯ A⇩P› FrP have "x ♯ Ψ⇩P" by(drule_tac extractFrameFresh) auto
ultimately show ?case
by(force simp add: frameChainAppend intro: frameResComm' FrameStatEqTrans frameResChainPres)
next
assume "(Ψ, R, T) ∉ ?X1"
with ‹(Ψ, R, T) ∈ ?X› have "(Ψ, R, T) ∈ ?X2" by blast
then obtain xvec x P Q where "T = ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))" and "R = ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)" and "xvec ♯* Ψ" and "x ♯ P" and "x ♯ Ψ"
by auto
moreover obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "x ♯ A⇩P" and "A⇩P ♯* Q"
by(rule_tac C="(Ψ, x, Q)" in freshFrame) auto
moreover obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "x ♯ A⇩Q" and "A⇩Q ♯* A⇩P" and "A⇩Q ♯* Ψ⇩P"
by(rule_tac C="(Ψ, x, A⇩P, Ψ⇩P)" in freshFrame) auto
moreover from FrQ ‹A⇩P ♯* Q› ‹A⇩Q ♯* A⇩P› have "A⇩P ♯* Ψ⇩Q"
by(drule_tac extractFrameFreshChain) auto
moreover from ‹x ♯ P› ‹x ♯ A⇩P› FrP have "x ♯ Ψ⇩P" by(drule_tac extractFrameFresh) auto
ultimately show ?case
apply auto
by(force simp add: frameChainAppend intro: frameResComm' FrameStatEqTrans frameResChainPres FrameStatEqSym)
qed
next
case(cSim Ψ R T)
let ?Y = "{(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ ((Ψ, P', Q') ∈ ?X ∨ Ψ ⊳ P' ∼ Q') ∧ Ψ ⊳ Q' ∼ Q}"
from ‹eqvt ?X› have "eqvt ?Y" by blast
have C1: "⋀Ψ R T y. ⟦(Ψ, R, T) ∈ ?Y; (y::name) ♯ Ψ⟧ ⟹ (Ψ, ⦇νy⦈R, ⦇νy⦈T) ∈ ?Y"
proof -
fix Ψ R T y
assume "(Ψ, R, T) ∈ ?Y"
then obtain R' T' where "Ψ ⊳ R ∼ R'" and "(Ψ, R', T') ∈ (?X ∪ bisim)" and "Ψ ⊳ T' ∼ T" by fastforce
assume "(y::name) ♯ Ψ"
show "(Ψ, ⦇νy⦈R, ⦇νy⦈T) ∈ ?Y"
proof(case_tac "(Ψ, R', T') ∈ ?X")
assume "(Ψ, R', T') ∈ ?X"
show ?thesis
proof(case_tac "(Ψ, R', T') ∈ ?X1")
assume "(Ψ, R', T') ∈ ?X1"
then obtain xvec x P Q where R'eq: "R' = ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))" and T'eq: "T' = ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)"
and "xvec ♯* Ψ" and "x ♯ P" and "x ♯ Ψ"
by auto
from ‹Ψ ⊳ R ∼ R'› ‹y ♯ Ψ› have "Ψ ⊳ ⦇νy⦈R ∼ ⦇νy⦈R'" by(rule bisimResPres)
moreover from ‹xvec ♯* Ψ› ‹y ♯ Ψ› ‹x ♯ P› ‹x ♯ Ψ› have "(Ψ, ⦇ν*(y#xvec)⦈⦇νx⦈(P ∥ Q), ⦇ν*(y#xvec)⦈(P ∥ ⦇νx⦈Q)) ∈ ?X1"
by(force simp del: resChain.simps)
with R'eq T'eq have "(Ψ, ⦇νy⦈R', ⦇νy⦈T') ∈ ?X ∪ bisim" by simp
moreover from ‹Ψ ⊳ T' ∼ T› ‹y ♯ Ψ› have "Ψ ⊳ ⦇νy⦈T' ∼ ⦇νy⦈T" by(rule bisimResPres)
ultimately show ?thesis by blast
next
assume "(Ψ, R', T') ∉ ?X1"
with ‹(Ψ, R', T') ∈ ?X› have "(Ψ, R', T') ∈ ?X2" by blast
then obtain xvec x P Q where T'eq: "T' = ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))" and R'eq: "R' = ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)" and "xvec ♯* Ψ" and "x ♯ P" and "x ♯ Ψ"
by auto
from ‹Ψ ⊳ R ∼ R'› ‹y ♯ Ψ› have "Ψ ⊳ ⦇νy⦈R ∼ ⦇νy⦈R'" by(rule bisimResPres)
moreover from ‹xvec ♯* Ψ› ‹y ♯ Ψ› ‹x ♯ P› ‹x ♯ Ψ› have "(Ψ, ⦇ν*(y#xvec)⦈(P ∥ ⦇νx⦈Q), ⦇ν*(y#xvec)⦈(⦇νx⦈(P ∥ Q))) ∈ ?X2"
by(force simp del: resChain.simps)
with R'eq T'eq have "(Ψ, ⦇νy⦈R', ⦇νy⦈T') ∈ ?X ∪ bisim" by simp
moreover from ‹Ψ ⊳ T' ∼ T› ‹y ♯ Ψ› have "Ψ ⊳ ⦇νy⦈T' ∼ ⦇νy⦈T" by(rule bisimResPres)
ultimately show ?thesis by blast
qed
next
assume "(Ψ, R', T') ∉ ?X"
with ‹(Ψ, R', T') ∈ ?X ∪ bisim› have "Ψ ⊳ R' ∼ T'" by blast
with ‹Ψ ⊳ R ∼ R'› ‹Ψ ⊳ T' ∼ T› ‹y ♯ Ψ› show ?thesis
by(blast dest: bisimResPres)
qed
qed
show ?case
proof(case_tac "(Ψ, R, T) ∈ ?X1")
assume "(Ψ, R, T) ∈ ?X1"
then obtain xvec x P Q where Req: "R = ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))" and Teq: "T = ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)" and "xvec ♯* Ψ" and "x ♯ P" and "x ♯ Ψ"
by auto
have "Ψ ⊳ ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q)) ↝[?Y] ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)"
proof -
have "Ψ ⊳ ⦇νx⦈(P ∥ Q) ↝[?Y] P ∥ ⦇νx⦈Q"
proof -
note ‹x ♯ P› ‹x ♯ Ψ› ‹eqvt ?Y›
moreover have "⋀Ψ P. (Ψ, P, P) ∈ ?Y" by(blast intro: bisimReflexive)
moreover have "⋀x Ψ P Q xvec. ⟦x ♯ Ψ; x ♯ P; xvec ♯* Ψ⟧ ⟹ (Ψ, ⦇νx⦈(⦇ν*xvec⦈(P ∥ Q)), ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)) ∈ ?Y"
proof -
fix x Ψ P Q xvec
assume "(x::name) ♯ (Ψ::'b)" and "x ♯ (P::('a, 'b, 'c) psi)" and "(xvec::name list) ♯* Ψ"
from ‹x ♯ Ψ› ‹xvec ♯* Ψ› have "Ψ ⊳ ⦇νx⦈(⦇ν*xvec⦈(P ∥ Q)) ∼ ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))"
by(rule bisimResComm')
moreover from ‹xvec ♯* Ψ› ‹x ♯ Ψ› ‹x ♯ P› have "(Ψ, ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q)), ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)) ∈ ?X ∪ bisim"
by blast
ultimately show "(Ψ, ⦇νx⦈(⦇ν*xvec⦈(P ∥ Q)), ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)) ∈ ?Y"
by(blast intro: bisimReflexive)
qed
moreover have "⋀Ψ xvec P x. ⟦x ♯ Ψ; xvec ♯* Ψ⟧ ⟹ (Ψ, ⦇νx⦈(⦇ν*xvec⦈P), ⦇ν*xvec⦈(⦇νx⦈P)) ∈ ?Y"
by(blast intro: bisimResComm' bisimReflexive)
ultimately show ?thesis by(rule scopeExtLeft)
qed
thus ?thesis using ‹eqvt ?Y› ‹xvec ♯* Ψ› C1
by(rule resChainPres)
qed
with Req Teq show ?case by simp
next
assume "(Ψ, R, T) ∉ ?X1"
with ‹(Ψ, R, T) ∈ ?X› have "(Ψ, R, T) ∈ ?X2" by blast
then obtain xvec x P Q where Teq: "T = ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))" and Req: "R = ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)" and "xvec ♯* Ψ" and "x ♯ P" and "x ♯ Ψ"
by auto
have "Ψ ⊳ ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q) ↝[?Y] ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))"
proof -
have "Ψ ⊳ P ∥ ⦇νx⦈Q ↝[?Y] ⦇νx⦈(P ∥ Q)"
proof -
note ‹x ♯ P› ‹x ♯ Ψ› ‹eqvt ?Y›
moreover have "⋀Ψ P. (Ψ, P, P) ∈ ?Y" by(blast intro: bisimReflexive)
moreover have "⋀x Ψ P Q xvec. ⟦x ♯ Ψ; x ♯ P; xvec ♯* Ψ⟧ ⟹ (Ψ, ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q), ⦇νx⦈(⦇ν*xvec⦈(P ∥ Q))) ∈ ?Y"
proof -
fix x Ψ P Q xvec
assume "(x::name) ♯ (Ψ::'b)" and "x ♯ (P::('a, 'b, 'c) psi)" and "(xvec::name list) ♯* Ψ"
from ‹xvec ♯* Ψ› ‹x ♯ Ψ› ‹x ♯ P› have "(Ψ, ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q), ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))) ∈ ?X ∪ bisim"
by blast
moreover from ‹x ♯ Ψ› ‹xvec ♯* Ψ› have "Ψ ⊳ ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q)) ∼ ⦇νx⦈(⦇ν*xvec⦈(P ∥ Q))"
by(blast intro: bisimResComm' bisimE)
ultimately show "(Ψ, ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q), ⦇νx⦈(⦇ν*xvec⦈(P ∥ Q))) ∈ ?Y"
by(blast intro: bisimReflexive)
qed
ultimately show ?thesis by(rule scopeExtRight)
qed
thus ?thesis using ‹eqvt ?Y› ‹xvec ♯* Ψ› C1
by(rule resChainPres)
qed
with Req Teq show ?case by simp
qed
next
case(cExt Ψ R T Ψ')
show ?case
proof(case_tac "(Ψ, R, T) ∈ ?X1")
assume "(Ψ, R, T) ∈ ?X1"
then obtain xvec x P Q where Req: "R = ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))" and Teq: "T = ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)" and "xvec ♯* Ψ" and "x ♯ P" and "x ♯ Ψ"
by auto
obtain y::name where "y ♯ P" and "y ♯ Q" and "y ♯ xvec" and "y ♯ Ψ" and "y ♯ Ψ'"
by(generate_fresh "name", auto simp add: fresh_prod)
obtain p where "(p ∙ xvec) ♯* Ψ" and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Q" and "(p ∙ xvec) ♯* Ψ'"
and "x ♯ (p ∙ xvec)" and "y ♯ (p ∙ xvec)"
and S: "(set p) ⊆ (set xvec) × (set(p ∙ xvec))" and "distinctPerm p"
by(rule_tac c="(Ψ, P, Q, x, y, Ψ')" in name_list_avoiding) auto
from ‹y ♯ P› have "(p ∙ y) ♯ (p ∙ P)" by(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
with S ‹y ♯ xvec› ‹y ♯ (p ∙ xvec)› have "y ♯ (p ∙ P)" by simp
with ‹(p ∙ xvec) ♯* Ψ› ‹y ♯ Ψ› ‹(p ∙ xvec) ♯* Ψ'› ‹y ♯ Ψ'›
have "(Ψ ⊗ Ψ', ⦇ν*(p ∙ xvec)⦈(⦇νy⦈((p ∙ P) ∥ (p ∙ [(x, y)] ∙ Q))), ⦇ν*(p ∙ xvec)⦈((p ∙ P) ∥ (⦇νy⦈(p ∙ [(x, y)] ∙ Q)))) ∈ ?X"
by auto
moreover from Req ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* Q› ‹y ♯ xvec› ‹y ♯ (p ∙ xvec)› ‹x ♯ (p ∙ xvec)› ‹y ♯ P› ‹y ♯ Q› ‹x ♯ P› S
have "R = ⦇ν*(p ∙ xvec)⦈(⦇νy⦈((p ∙ P) ∥ (p ∙ [(x, y)] ∙ Q)))"
apply(erule_tac rev_mp)
apply(subst alphaRes[of y])
apply(clarsimp simp add: eqvts)
apply(subst resChainAlpha[of p])
by(auto simp add: eqvts)
moreover from Teq ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* Q› ‹y ♯ xvec› ‹y ♯ (p ∙ xvec)› ‹x ♯ (p ∙ xvec)› ‹y ♯ P› ‹y ♯ Q› ‹x ♯ P› S
have "T = ⦇ν*(p ∙ xvec)⦈((p ∙ P) ∥ ⦇νy⦈(p ∙ [(x, y)] ∙ Q))"
apply(erule_tac rev_mp)
apply(subst alphaRes[of y])
apply(clarsimp simp add: eqvts)
apply(subst resChainAlpha[of p])
by(auto simp add: eqvts)
ultimately show ?case
by blast
next
assume "(Ψ, R, T) ∉ ?X1"
with ‹(Ψ, R, T) ∈ ?X› have "(Ψ, R, T) ∈ ?X2" by blast
then obtain xvec x P Q where Teq: "T = ⦇ν*xvec⦈(⦇νx⦈(P ∥ Q))" and Req: "R = ⦇ν*xvec⦈(P ∥ ⦇νx⦈Q)" and "xvec ♯* Ψ" and "x ♯ P" and "x ♯ Ψ"
by auto
obtain y::name where "y ♯ P" and "y ♯ Q" and "y ♯ xvec" and "y ♯ Ψ" and "y ♯ Ψ'"
by(generate_fresh "name", auto simp add: fresh_prod)
obtain p where "(p ∙ xvec) ♯* Ψ" and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Q" and "(p ∙ xvec) ♯* Ψ'"
and "x ♯ (p ∙ xvec)" and "y ♯ (p ∙ xvec)"
and S: "(set p) ⊆ (set xvec) × (set(p ∙ xvec))" and "distinctPerm p"
by(rule_tac c="(Ψ, P, Q, x, y, Ψ')" in name_list_avoiding) auto
from ‹y ♯ P› have "(p ∙ y) ♯ (p ∙ P)" by(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
with S ‹y ♯ xvec› ‹y ♯ (p ∙ xvec)› have "y ♯ (p ∙ P)" by simp
with ‹(p ∙ xvec) ♯* Ψ› ‹y ♯ Ψ› ‹(p ∙ xvec) ♯* Ψ'› ‹y ♯ Ψ'›
have "(Ψ ⊗ Ψ', ⦇ν*(p ∙ xvec)⦈((p ∙ P) ∥ ⦇νy⦈(p ∙ [(x, y)] ∙ Q)), ⦇ν*(p ∙ xvec)⦈(⦇νy⦈((p ∙ P) ∥ (p ∙ [(x, y)] ∙ Q)))) ∈ ?X2"
by auto
moreover from Teq ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* Q› ‹y ♯ xvec› ‹y ♯ (p ∙ xvec)› ‹x ♯ (p ∙ xvec)› ‹y ♯ P› ‹y ♯ Q› ‹x ♯ P› S
have "T = ⦇ν*(p ∙ xvec)⦈(⦇νy⦈((p ∙ P) ∥ (p ∙ [(x, y)] ∙ Q)))"
apply(erule_tac rev_mp)
apply(subst alphaRes[of y])
apply(clarsimp simp add: eqvts)
apply(subst resChainAlpha[of p])
by(auto simp add: eqvts)
moreover from Req ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* Q› ‹y ♯ xvec› ‹y ♯ (p ∙ xvec)› ‹x ♯ (p ∙ xvec)› ‹y ♯ P› ‹y ♯ Q› ‹x ♯ P› S
have "R = ⦇ν*(p ∙ xvec)⦈((p ∙ P) ∥ ⦇νy⦈(p ∙ [(x, y)] ∙ Q))"
apply(erule_tac rev_mp)
apply(subst alphaRes[of y])
apply(clarsimp simp add: eqvts)
apply(subst resChainAlpha[of p])
by(auto simp add: eqvts)
ultimately show ?case
by blast
qed
next
case(cSym Ψ P Q)
thus ?case
by(blast dest: bisimE)
qed
}
moreover obtain y::name where "y ♯ Ψ" and "y ♯ P" "y ♯ Q"
by(generate_fresh "name") auto
ultimately have "Ψ ⊳ ⦇νy⦈(P ∥ ([(x, y)] ∙ Q)) ∼ P ∥ ⦇νy⦈([(x, y)] ∙ Q)" by auto
thus ?thesis using assms ‹y ♯ P› ‹y ♯ Q›
apply(subst alphaRes[where x=x and y=y and P=Q], auto)
by(subst alphaRes[where x=x and y=y and P="P ∥ Q"]) auto
qed
lemma bisimScopeExtChain:
fixes xvec :: "name list"
and Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
assumes "xvec ♯* Ψ"
and "xvec ♯* P"
shows "Ψ ⊳ ⦇ν*xvec⦈(P ∥ Q) ∼ P ∥ (⦇ν*xvec⦈Q)"
using assms
by(induct xvec) (auto intro: bisimScopeExt bisimReflexive bisimTransitive bisimResPres)
lemma bisimParAssoc:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
shows "Ψ ⊳ (P ∥ Q) ∥ R ∼ P ∥ (Q ∥ R)"
proof -
let ?X = "{(Ψ, ⦇ν*xvec⦈((P ∥ Q) ∥ R), ⦇ν*xvec⦈(P ∥ (Q ∥ R))) | Ψ xvec P Q R. xvec ♯* Ψ}"
let ?Y = "{(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ ?X ∧ Ψ ⊳ Q' ∼ Q}"
have "(Ψ, (P ∥ Q) ∥ R, P ∥ (Q ∥ R)) ∈ ?X"
by(auto, rule_tac x="[]" in exI) auto
moreover have "eqvt ?X" by(force simp add: eqvt_def simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst] eqvts)
ultimately show ?thesis
proof(coinduct rule: weakTransitiveCoinduct')
case(cStatEq Ψ PQR PQR')
from ‹(Ψ, PQR, PQR') ∈ ?X› obtain xvec P Q R where "xvec ♯* Ψ" and "PQR = ⦇ν*xvec⦈((P ∥ Q) ∥ R)" and "PQR' = ⦇ν*xvec⦈(P ∥ (Q ∥ R))"
by auto
moreover obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "A⇩P ♯* Q" and "A⇩P ♯* R"
by(rule_tac C="(Ψ, Q, R)" in freshFrame) auto
moreover obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* A⇩P" and "A⇩Q ♯* Ψ⇩P" and "A⇩Q ♯* R"
by(rule_tac C="(Ψ, A⇩P, Ψ⇩P, R)" in freshFrame) auto
moreover obtain A⇩R Ψ⇩R where FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" and "A⇩R ♯* Ψ" and "A⇩R ♯* A⇩P" and "A⇩R ♯* Ψ⇩P" and "A⇩R ♯* A⇩Q" and "A⇩R ♯* Ψ⇩Q"
by(rule_tac C="(Ψ, A⇩P, Ψ⇩P, A⇩Q, Ψ⇩Q)" in freshFrame) auto
moreover from FrQ ‹A⇩P ♯* Q› ‹A⇩Q ♯* A⇩P› have "A⇩P ♯* Ψ⇩Q"
by(drule_tac extractFrameFreshChain) auto
moreover from FrR ‹A⇩P ♯* R› ‹A⇩R ♯* A⇩P› have "A⇩P ♯* Ψ⇩R"
by(drule_tac extractFrameFreshChain) auto
moreover from FrR ‹A⇩Q ♯* R› ‹A⇩R ♯* A⇩Q› have "A⇩Q ♯* Ψ⇩R"
by(drule_tac extractFrameFreshChain) auto
ultimately show ?case using freshCompChain
by auto (metis frameChainAppend compositionSym Associativity frameNilStatEq frameResChainPres)
next
case(cSim Ψ T S)
from ‹(Ψ, T, S) ∈ ?X› obtain xvec P Q R where "xvec ♯* Ψ" and TEq: "T = ⦇ν*xvec⦈((P ∥ Q) ∥ R)"
and SEq: "S = ⦇ν*xvec⦈(P ∥ (Q ∥ R))"
by auto
from ‹eqvt ?X›have "eqvt ?Y" by blast
have C1: "⋀Ψ T S yvec. ⟦(Ψ, T, S) ∈ ?Y; yvec ♯* Ψ⟧ ⟹ (Ψ, ⦇ν*yvec⦈T, ⦇ν*yvec⦈S) ∈ ?Y"
proof -
fix Ψ T S yvec
assume "(Ψ, T, S) ∈ ?Y"
then obtain T' S' where "Ψ ⊳ T ∼ T'" and "(Ψ, T', S') ∈ ?X" and "Ψ ⊳ S' ∼ S" by fastforce
assume "(yvec::name list) ♯* Ψ"
from ‹(Ψ, T', S') ∈ ?X› obtain xvec P Q R where T'eq: "T' = ⦇ν*xvec⦈((P ∥ Q) ∥ R)" and S'eq: "S' = ⦇ν*xvec⦈(P ∥ (Q ∥ R))"
and "xvec ♯* Ψ"
by auto
from ‹Ψ ⊳ T ∼ T'› ‹yvec ♯* Ψ› have "Ψ ⊳ ⦇ν*yvec⦈T ∼ ⦇ν*yvec⦈T'" by(rule bisimResChainPres)
moreover from ‹xvec ♯* Ψ› ‹yvec ♯* Ψ› have "(Ψ, ⦇ν*(yvec@xvec)⦈((P ∥ Q) ∥ R), ⦇ν*(yvec@xvec)⦈(P ∥ (Q ∥ R))) ∈ ?X"
by force
with T'eq S'eq have "(Ψ, ⦇ν*yvec⦈T', ⦇ν*yvec⦈S') ∈ ?X" by(simp add: resChainAppend)
moreover from ‹Ψ ⊳ S' ∼ S› ‹yvec ♯* Ψ› have "Ψ ⊳ ⦇ν*yvec⦈S' ∼ ⦇ν*yvec⦈S" by(rule bisimResChainPres)
ultimately show "(Ψ, ⦇ν*yvec⦈T, ⦇ν*yvec⦈S) ∈ ?Y" by blast
qed
have C2: "⋀Ψ T S y. ⟦(Ψ, T, S) ∈ ?Y; y ♯ Ψ⟧ ⟹ (Ψ, ⦇νy⦈T, ⦇νy⦈S) ∈ ?Y"
by(drule_tac yvec2="[y]" in C1) auto
have "Ψ ⊳ ⦇ν*xvec⦈((P ∥ Q) ∥ R) ↝[?Y] ⦇ν*xvec⦈(P ∥ (Q ∥ R))"
proof -
have "Ψ ⊳ (P ∥ Q) ∥ R ↝[?Y] P ∥ (Q ∥ R)"
proof -
note ‹eqvt ?Y›
moreover have "⋀Ψ P Q R. (Ψ, (P ∥ Q) ∥ R, P ∥ (Q ∥ R)) ∈ ?Y"
proof -
fix Ψ P Q R
have "(Ψ::'b, ((P::('a, 'b, 'c) psi) ∥ Q) ∥ R, P ∥ (Q ∥ R)) ∈ ?X"
by(auto, rule_tac x="[]" in exI) auto
thus "(Ψ, (P ∥ Q) ∥ R, P ∥ (Q ∥ R)) ∈ ?Y"
by(blast intro: bisimReflexive)
qed
moreover have "⋀xvec Ψ P Q R. ⟦xvec ♯* Ψ; xvec ♯* P⟧ ⟹ (Ψ, ⦇ν*xvec⦈((P ∥ Q) ∥ R), P ∥ (⦇ν*xvec⦈(Q ∥ R))) ∈ ?Y"
proof -
fix xvec Ψ P Q R
assume "(xvec::name list) ♯* (Ψ::'b)" and "xvec ♯* (P::('a, 'b, 'c) psi)"
from ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈((P ∥ Q) ∥ R), ⦇ν*xvec⦈(P ∥ (Q ∥ R))) ∈ ?X" by blast
moreover from ‹xvec ♯* Ψ› ‹xvec ♯* P› have "Ψ ⊳ ⦇ν*xvec⦈(P ∥ (Q ∥ R)) ∼ P ∥ (⦇ν*xvec⦈(Q ∥ R))"
by(rule bisimScopeExtChain)
ultimately show "(Ψ, ⦇ν*xvec⦈((P ∥ Q) ∥ R), P ∥ (⦇ν*xvec⦈(Q ∥ R))) ∈ ?Y"
by(blast intro: bisimReflexive)
qed
moreover have "⋀xvec Ψ P Q R. ⟦xvec ♯* Ψ; xvec ♯* R⟧ ⟹ (Ψ, (⦇ν*xvec⦈(P ∥ Q)) ∥ R, ⦇ν*xvec⦈(P ∥ (Q ∥ R))) ∈ ?Y"
proof -
fix xvec Ψ P Q R
assume "(xvec::name list) ♯* (Ψ::'b)" and "xvec ♯* (R::('a, 'b, 'c) psi)"
have "Ψ ⊳ (⦇ν*xvec⦈(P ∥ Q)) ∥ R ∼ R ∥ (⦇ν*xvec⦈(P ∥ Q))" by(rule bisimParComm)
moreover from ‹xvec ♯* Ψ› ‹xvec ♯* R› have "Ψ ⊳ ⦇ν*xvec⦈(R ∥ (P ∥ Q)) ∼ R ∥ (⦇ν*xvec⦈(P ∥ Q))" by(rule bisimScopeExtChain)
hence "Ψ ⊳ R ∥ (⦇ν*xvec⦈(P ∥ Q)) ∼ ⦇ν*xvec⦈(R ∥ (P ∥ Q))" by(rule bisimE)
moreover from ‹xvec ♯* Ψ› have "Ψ ⊳ ⦇ν*xvec⦈(R ∥ (P ∥ Q)) ∼ ⦇ν*xvec⦈((P ∥ Q) ∥ R)"
by(metis bisimResChainPres bisimParComm)
moreover from ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈((P ∥ Q) ∥ R), ⦇ν*xvec⦈(P ∥ (Q ∥ R))) ∈ ?X" by blast
ultimately show "(Ψ, (⦇ν*xvec⦈(P ∥ Q)) ∥ R, ⦇ν*xvec⦈(P ∥ (Q ∥ R))) ∈ ?Y" by(blast dest: bisimTransitive intro: bisimReflexive)
qed
ultimately show ?thesis using C1
by(rule parAssocLeft)
qed
thus ?thesis using ‹eqvt ?Y› ‹xvec ♯* Ψ› C2
by(rule resChainPres)
qed
with TEq SEq show ?case by simp
next
case(cExt Ψ T S Ψ')
from ‹(Ψ, T, S) ∈ ?X› obtain xvec P Q R where "xvec ♯* Ψ" and TEq: "T = ⦇ν*xvec⦈((P ∥ Q) ∥ R)"
and SEq: "S = ⦇ν*xvec⦈(P ∥ (Q ∥ R))"
by auto
obtain p where "(p ∙ xvec) ♯* Ψ" and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Q" and "(p ∙ xvec) ♯* R" and "(p ∙ xvec) ♯* Ψ'"
and S: "(set p) ⊆ (set xvec) × (set(p ∙ xvec))" and "distinctPerm p"
by(rule_tac c="(Ψ, P, Q, R, Ψ')" in name_list_avoiding) auto
from ‹(p ∙ xvec) ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ'› have "(Ψ ⊗ Ψ', ⦇ν*(p ∙ xvec)⦈(((p ∙ P) ∥ (p ∙ Q)) ∥ (p ∙ R)), ⦇ν*(p ∙ xvec)⦈((p ∙ P) ∥ ((p ∙ Q) ∥ (p ∙ R)))) ∈ ?X"
by auto
moreover from TEq ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* Q› ‹(p ∙ xvec) ♯* R› S have "T = ⦇ν*(p ∙ xvec)⦈(((p ∙ P) ∥ (p ∙ Q)) ∥ (p ∙ R))"
apply auto by(subst resChainAlpha[of p]) auto
moreover from SEq ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* Q› ‹(p ∙ xvec) ♯* R› S have "S = ⦇ν*(p ∙ xvec)⦈((p ∙ P) ∥ ((p ∙ Q) ∥ (p ∙ R)))"
apply auto by(subst resChainAlpha[of p]) auto
ultimately show ?case by simp
next
case(cSym Ψ T S)
from ‹(Ψ, T, S) ∈ ?X› obtain xvec P Q R where "xvec ♯* Ψ" and TEq: "T = ⦇ν*xvec⦈((P ∥ Q) ∥ R)"
and SEq: "⦇ν*xvec⦈(P ∥ (Q ∥ R)) = S"
by auto
from ‹xvec ♯* Ψ› have "Ψ ⊳ ⦇ν*xvec⦈(P ∥ (Q ∥ R)) ∼ ⦇ν*xvec⦈((R ∥ Q) ∥ P)"
by(metis bisimParComm bisimParPres bisimTransitive bisimResChainPres)
moreover from ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈((R ∥ Q) ∥ P), ⦇ν*xvec⦈(R ∥ (Q ∥ P))) ∈ ?X" by blast
moreover from ‹xvec ♯* Ψ› have "Ψ ⊳ ⦇ν*xvec⦈(R ∥ (Q ∥ P)) ∼ ⦇ν*xvec⦈((P ∥ Q) ∥ R)"
by(metis bisimParComm bisimParPres bisimTransitive bisimResChainPres)
ultimately show ?case using TEq SEq by(blast dest: bisimTransitive)
qed
qed
lemma bisimParNil:
fixes P :: "('a, 'b, 'c) psi"
shows "Ψ ⊳ P ∥ 𝟬 ∼ P"
proof -
let ?X1 = "{(Ψ, P ∥ 𝟬, P) | Ψ P. True}"
let ?X2 = "{(Ψ, P, P ∥ 𝟬) | Ψ P. True}"
let ?X = "?X1 ∪ ?X2"
have "eqvt ?X" by(auto simp add: eqvt_def)
have "(Ψ, P ∥ 𝟬, P) ∈ ?X" by simp
thus ?thesis
proof(coinduct rule: bisimWeakCoinduct)
case(cStatEq Ψ Q R)
show ?case
proof(case_tac "(Ψ, Q, R) ∈ ?X1")
assume "(Ψ, Q, R) ∈ ?X1"
then obtain P where "Q = P ∥ 𝟬" and "R = P" by auto
moreover obtain A⇩P Ψ⇩P where "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ"
by(rule freshFrame)
ultimately show ?case
apply auto by(metis frameResChainPres frameNilStatEq Identity Associativity AssertionStatEqTrans Commutativity)
next
assume "(Ψ, Q, R) ∉ ?X1"
with ‹(Ψ, Q, R) ∈ ?X› have "(Ψ, Q, R) ∈ ?X2" by blast
then obtain P where "Q = P" and "R = P ∥ 𝟬" by auto
moreover obtain A⇩P Ψ⇩P where "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ"
by(rule freshFrame)
ultimately show ?case
apply auto by(metis frameResChainPres frameNilStatEq Identity Associativity AssertionStatEqTrans AssertionStatEqSym Commutativity)
qed
next
case(cSim Ψ Q R)
thus ?case using ‹eqvt ?X›
by(auto intro: parNilLeft parNilRight)
next
case(cExt Ψ Q R Ψ')
thus ?case by auto
next
case(cSym Ψ Q R)
thus ?case by auto
qed
qed
lemma bisimResNil:
fixes x :: name
and Ψ :: 'b
shows "Ψ ⊳ ⦇νx⦈𝟬 ∼ 𝟬"
proof -
{
fix x::name
assume "x ♯ Ψ"
have "Ψ ⊳ ⦇νx⦈𝟬 ∼ 𝟬"
proof -
let ?X1 = "{(Ψ, ⦇νx⦈𝟬, 𝟬) | Ψ x. x ♯ Ψ}"
let ?X2 = "{(Ψ, 𝟬, ⦇νx⦈𝟬) | Ψ x. x ♯ Ψ}"
let ?X = "?X1 ∪ ?X2"
from ‹x ♯ Ψ› have "(Ψ, ⦇νx⦈𝟬, 𝟬) ∈ ?X" by auto
thus ?thesis
proof(coinduct rule: bisimWeakCoinduct)
case(cStatEq Ψ P Q)
thus ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
next
case(cSim Ψ P Q)
thus ?case
by(force intro: resNilLeft resNilRight)
next
case(cExt Ψ P Q Ψ')
obtain y where "y ♯ Ψ" and "y ♯ Ψ'" and "y ≠ x"
by(generate_fresh "name") (auto simp add: fresh_prod)
show ?case
proof(case_tac "(Ψ, P, Q) ∈ ?X1")
assume "(Ψ, P, Q) ∈ ?X1"
then obtain x where "P = ⦇νx⦈𝟬" and "Q = 𝟬" by auto
moreover have "⦇νx⦈𝟬 = ⦇νy⦈ 𝟬" by(subst alphaRes) auto
ultimately show ?case using ‹y ♯ Ψ› ‹y ♯ Ψ'› by auto
next
assume "(Ψ, P, Q) ∉ ?X1"
with ‹(Ψ, P, Q) ∈ ?X› have "(Ψ, P, Q) ∈ ?X2" by auto
then obtain x where "Q = ⦇νx⦈𝟬" and "P = 𝟬" by auto
moreover have "⦇νx⦈𝟬 = ⦇νy⦈ 𝟬" by(subst alphaRes) auto
ultimately show ?case using ‹y ♯ Ψ› ‹y ♯ Ψ'› by auto
qed
next
case(cSym Ψ P Q)
thus ?case by auto
qed
qed
}
moreover obtain y::name where "y ♯ Ψ" by(generate_fresh "name") auto
ultimately have "Ψ ⊳ ⦇νy⦈𝟬 ∼ 𝟬" by auto
thus ?thesis by(subst alphaRes[where x=x and y=y]) auto
qed
lemma bisimOutputPushRes:
fixes x :: name
and Ψ :: 'b
and M :: 'a
and N :: 'a
and P :: "('a, 'b, 'c) psi"
assumes "x ♯ M"
and "x ♯ N"
shows "Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ∼ M⟨N⟩.⦇νx⦈P"
proof -
{
fix x::name and P::"('a, 'b, 'c) psi"
assume "x ♯ Ψ" and "x ♯ M" and "x ♯ N"
let ?X1 = "{(Ψ, ⦇νx⦈(M⟨N⟩.P), M⟨N⟩.⦇νx⦈P) | Ψ x M N P. x ♯ Ψ ∧ x ♯ M ∧ x ♯ N}"
let ?X2 = "{(Ψ, M⟨N⟩.⦇νx⦈P, ⦇νx⦈(M⟨N⟩.P)) | Ψ x M N P. x ♯ Ψ ∧ x ♯ M ∧ x ♯ N}"
let ?X = "?X1 ∪ ?X2"
have "eqvt ?X" by(rule_tac eqvtUnion) (force simp add: eqvt_def pt_fresh_bij[OF pt_name_inst, OF at_name_inst] eqvts)+
from ‹x ♯ Ψ› ‹x ♯ M› ‹x ♯ N› have "(Ψ, ⦇νx⦈(M⟨N⟩.P), M⟨N⟩.⦇νx⦈P) ∈ ?X" by auto
hence "Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ∼ M⟨N⟩.⦇νx⦈P"
proof(coinduct rule: bisimCoinduct)
case(cStatEq Ψ Q R)
thus ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
next
case(cSim Ψ Q R)
thus ?case using ‹eqvt ?X›
by(fastforce intro: outputPushResLeft outputPushResRight bisimReflexive)
next
case(cExt Ψ Q R Ψ')
show ?case
proof(case_tac "(Ψ, Q, R) ∈ ?X1")
assume "(Ψ, Q, R) ∈ ?X1"
then obtain x M N P where Qeq: "Q = ⦇νx⦈(M⟨N⟩.P)" and Req: "R = M⟨N⟩.⦇νx⦈P" and "x ♯ Ψ" and "x ♯ M" and "x ♯ N" by auto
obtain y::name where "y ♯ Ψ" and "y ♯ Ψ'" and "y ♯ M" and "y ♯ N" and "y ♯ P"
by(generate_fresh "name") (auto simp add: fresh_prod)
moreover hence "(Ψ ⊗ Ψ', ⦇νy⦈(M⟨N⟩.([(x, y)] ∙ P)), M⟨N⟩.⦇νy⦈([(x, y)] ∙ P)) ∈ ?X" by auto
moreover from Qeq ‹x ♯ M› ‹y ♯ M› ‹x ♯ N› ‹y ♯ N› ‹y ♯ P› have "Q = ⦇νy⦈(M⟨N⟩.([(x, y)] ∙ P))"
apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
moreover from Req ‹y ♯ P› have "R = M⟨N⟩.⦇νy⦈([(x, y)] ∙ P)"
apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
ultimately show ?case by blast
next
assume "(Ψ, Q, R) ∉ ?X1"
with ‹(Ψ, Q, R) ∈ ?X› have "(Ψ, Q, R) ∈ ?X2" by blast
then obtain x M N P where Req: "R = ⦇νx⦈(M⟨N⟩.P)" and Qeq: "Q = M⟨N⟩.⦇νx⦈P" and "x ♯ Ψ" and "x ♯ M" and "x ♯ N" by auto
obtain y::name where "y ♯ Ψ" and "y ♯ Ψ'" and "y ♯ M" and "y ♯ N" and "y ♯ P"
by(generate_fresh "name") (auto simp add: fresh_prod)
moreover hence "(Ψ ⊗ Ψ', ⦇νy⦈(M⟨N⟩.([(x, y)] ∙ P)), M⟨N⟩.⦇νy⦈([(x, y)] ∙ P)) ∈ ?X" by auto
moreover from Req ‹x ♯ M› ‹y ♯ M› ‹x ♯ N› ‹y ♯ N› ‹y ♯ P› have "R = ⦇νy⦈(M⟨N⟩.([(x, y)] ∙ P))"
apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
moreover from Qeq ‹y ♯ P› have "Q = M⟨N⟩.⦇νy⦈([(x, y)] ∙ P)"
apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
ultimately show ?case by blast
qed
next
case(cSym Ψ R Q)
thus ?case by blast
qed
}
moreover obtain y::name where "y ♯ Ψ" and "y ♯ M" and "y ♯ N" "y ♯ P"
by(generate_fresh "name") auto
ultimately have "Ψ ⊳ ⦇νy⦈(M⟨N⟩.([(x, y)] ∙ P)) ∼ M⟨N⟩.⦇νy⦈([(x, y)] ∙ P)" by auto
thus ?thesis using assms ‹y ♯ P› ‹y ♯ M› ‹y ♯ N›
apply(subst alphaRes[where x=x and y=y and P=P], auto)
by(subst alphaRes[where x=x and y=y and P="M⟨N⟩.P"]) auto
qed
lemma bisimInputPushRes:
fixes x :: name
and Ψ :: 'b
and M :: 'a
and xvec :: "name list"
and N :: 'a
and P :: "('a, 'b, 'c) psi"
assumes "x ♯ M"
and "x ♯ xvec"
and "x ♯ N"
shows "Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ∼ M⦇λ*xvec N⦈.⦇νx⦈P"
proof -
{
fix x::name and P::"('a, 'b, 'c) psi"
assume "x ♯ Ψ" and "x ♯ M" and "x ♯ N" and "x ♯ xvec"
let ?X1 = "{(Ψ, ⦇νx⦈(M⦇λ*xvec N⦈.P), M⦇λ*xvec N⦈.⦇νx⦈P) | Ψ x M xvec N P. x ♯ Ψ ∧ x ♯ M ∧ x ♯ xvec ∧ x ♯ N}"
let ?X2 = "{(Ψ, M⦇λ*xvec N⦈.⦇νx⦈P, ⦇νx⦈(M⦇λ*xvec N⦈.P)) | Ψ x M xvec N P. x ♯ Ψ ∧ x ♯ M ∧ x ♯ xvec ∧ x ♯ N}"
let ?X = "?X1 ∪ ?X2"
have "eqvt ?X" by(rule_tac eqvtUnion) (force simp add: eqvt_def pt_fresh_bij[OF pt_name_inst, OF at_name_inst] eqvts)+
from ‹x ♯ Ψ› ‹x ♯ M› ‹x ♯ xvec› ‹x ♯ N› have "(Ψ, ⦇νx⦈(M⦇λ*xvec N⦈.P), M⦇λ*xvec N⦈.⦇νx⦈P) ∈ ?X" by blast
hence "Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ∼ M⦇λ*xvec N⦈.⦇νx⦈P"
proof(coinduct rule: bisimCoinduct)
case(cStatEq Ψ Q R)
thus ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
next
case(cSim Ψ Q R)
thus ?case using ‹eqvt ?X›
by(fastforce intro: inputPushResLeft inputPushResRight bisimReflexive)
next
case(cExt Ψ Q R Ψ')
show ?case
proof(case_tac "(Ψ, Q, R) ∈ ?X1")
assume "(Ψ, Q, R) ∈ ?X1"
then obtain x M xvec N P where Qeq: "Q = ⦇νx⦈(M⦇λ*xvec N⦈.P)" and Req: "R = M⦇λ*xvec N⦈.⦇νx⦈P" and "x ♯ Ψ"
and "x ♯ M" and "x ♯ xvec" and "x ♯ N" by auto
obtain y::name where "y ♯ Ψ" and "y ♯ Ψ'" and "y ♯ M" and "y ♯ N" and "y ♯ P" and "y ♯ xvec"
by(generate_fresh "name") (auto simp add: fresh_prod)
moreover hence "(Ψ ⊗ Ψ', ⦇νy⦈(M⦇λ*xvec N⦈.([(x, y)] ∙ P)), M⦇λ*xvec N⦈.⦇νy⦈([(x, y)] ∙ P)) ∈ ?X" by fastforce
moreover from Qeq ‹x ♯ M› ‹y ♯ M› ‹x ♯ xvec› ‹y ♯ xvec› ‹x ♯ N› ‹y ♯ N› ‹y ♯ P› have "Q = ⦇νy⦈(M⦇λ*xvec N⦈.([(x, y)] ∙ P))"
apply auto by(subst alphaRes[of y]) (auto simp add: eqvts inputChainFresh)
moreover from Req ‹y ♯ P› have "R = M⦇λ*xvec N ⦈.⦇νy⦈([(x, y)] ∙ P)"
apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
ultimately show ?case by blast
next
assume "(Ψ, Q, R) ∉ ?X1"
with ‹(Ψ, Q, R) ∈ ?X› have "(Ψ, Q, R) ∈ ?X2" by blast
then obtain x M xvec N P where Req: "R = ⦇νx⦈(M⦇λ*xvec N⦈.P)" and Qeq: "Q = M⦇λ*xvec N⦈.⦇νx⦈P" and "x ♯ Ψ"
and "x ♯ M" and "x ♯ xvec" and "x ♯ N" by auto
obtain y::name where "y ♯ Ψ" and "y ♯ Ψ'" and "y ♯ M" and "y ♯ N" and "y ♯ P" and "y ♯ xvec"
by(generate_fresh "name") (auto simp add: fresh_prod)
moreover hence "(Ψ ⊗ Ψ', ⦇νy⦈(M⦇λ*xvec N⦈.([(x, y)] ∙ P)), M⦇λ*xvec N⦈.⦇νy⦈([(x, y)] ∙ P)) ∈ ?X" by fastforce
moreover from Req ‹x ♯ M› ‹y ♯ M› ‹x ♯ xvec› ‹y ♯ xvec› ‹x ♯ N› ‹y ♯ N› ‹y ♯ P› have "R = ⦇νy⦈(M⦇λ*xvec N⦈.([(x, y)] ∙ P))"
apply auto by(subst alphaRes[of y]) (auto simp add: eqvts inputChainFresh)
moreover from Qeq ‹y ♯ P› have "Q = M⦇λ*xvec N ⦈.⦇νy⦈([(x, y)] ∙ P)"
apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
ultimately show ?case by blast
qed
next
case(cSym Ψ R Q)
thus ?case by blast
qed
}
moreover obtain y::name where "y ♯ Ψ" and "y ♯ M" and "y ♯ N" and "y ♯ P" and "y ♯ xvec"
by(generate_fresh "name") auto
ultimately have "Ψ ⊳ ⦇νy⦈(M⦇λ*xvec N⦈.([(x, y)] ∙ P)) ∼ M⦇λ*xvec N⦈.⦇νy⦈([(x, y)] ∙ P)" by auto
thus ?thesis using assms ‹y ♯ P› ‹y ♯ M› ‹y ♯ N› ‹y ♯ xvec›
apply(subst alphaRes[where x=x and y=y and P=P], auto)
by(subst alphaRes[where x=x and y=y and P="M⦇λ*xvec N⦈.P"]) (auto simp add: inputChainFresh eqvts)
qed
lemma bisimCasePushRes:
fixes x :: name
and Ψ :: 'b
and Cs :: "('c × ('a, 'b, 'c) psi) list"
assumes "x ♯ (map fst Cs)"
shows "Ψ ⊳ ⦇νx⦈(Cases Cs) ∼ Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
proof -
{
fix x::name and Cs::"('c × ('a, 'b, 'c) psi) list"
assume "x ♯ Ψ" and "x ♯ (map fst Cs)"
let ?X1 = "{(Ψ, ⦇νx⦈(Cases Cs), Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)) | Ψ x Cs. x ♯ Ψ ∧ x ♯ (map fst Cs)}"
let ?X2 = "{(Ψ, Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs), ⦇νx⦈(Cases Cs)) | Ψ x Cs. x ♯ Ψ ∧ x ♯ (map fst Cs)}"
let ?X = "?X1 ∪ ?X2"
have "eqvt ?X" apply(rule_tac eqvtUnion)
apply(auto simp add: eqvt_def eqvts)
apply(rule_tac x="p ∙ x" in exI)
apply(rule_tac x="p ∙ Cs" in exI)
apply(perm_extend_simp)
apply(auto simp add: eqvts)
apply(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: eqvts)
apply(perm_extend_simp)
apply(simp add: eqvts)
apply(rule_tac x="p ∙ x" in exI)
apply(rule_tac x="p ∙ Cs" in exI)
apply auto
apply(perm_extend_simp)
apply(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: eqvts)
apply(perm_extend_simp)
by(simp add: eqvts)
from ‹x ♯ Ψ› ‹x ♯ map fst Cs› have "(Ψ, ⦇νx⦈(Cases Cs), Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)) ∈ ?X" by auto
hence "Ψ ⊳ ⦇νx⦈(Cases Cs) ∼ Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
proof(coinduct rule: bisimCoinduct)
case(cStatEq Ψ Q R)
thus ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
next
case(cSim Ψ Q R)
thus ?case using ‹eqvt ?X›
by(fastforce intro: casePushResLeft casePushResRight bisimReflexive)
next
case(cExt Ψ Q R Ψ')
show ?case
proof(case_tac "(Ψ, Q, R) ∈ ?X1")
assume "(Ψ, Q, R) ∈ ?X1"
then obtain x Cs where Qeq: "Q = ⦇νx⦈(Cases Cs)" and Req: "R = Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
and "x ♯ Ψ" and "x ♯ (map fst Cs)" by blast
obtain y::name where "y ♯ Ψ" and "y ♯ Ψ'" and "y ♯ Cs"
by(generate_fresh "name") (auto simp add: fresh_prod)
from ‹y ♯ Cs› ‹x ♯ (map fst Cs)› have "y ♯ map fst ([(x, y)] ∙ Cs)" by(induct Cs) (auto simp add: fresh_list_cons fresh_list_nil)
moreover with ‹y ♯ Ψ› ‹y ♯ Ψ'› have "(Ψ ⊗ Ψ', ⦇νy⦈(Cases ([(x, y)] ∙ Cs)), Cases(map (λ(φ, P). (φ, ⦇νy⦈P)) ([(x, y)] ∙ Cs))) ∈ ?X"
by auto
moreover from Qeq ‹y ♯ Cs› have "Q = ⦇νy⦈(Cases([(x, y)] ∙ Cs))"
apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
moreover from Req ‹y ♯ Cs› ‹x ♯ (map fst Cs)› have "R = Cases(map (λ(φ, P). (φ, ⦇νy⦈P)) ([(x, y)] ∙ Cs))"
by(induct Cs arbitrary: R) (auto simp add: fresh_list_cons fresh_prod alphaRes)
ultimately show ?case by blast
next
assume "(Ψ, Q, R) ∉ ?X1"
with ‹(Ψ, Q, R) ∈ ?X› have "(Ψ, Q, R) ∈ ?X2" by blast
then obtain x Cs where Req: "R = ⦇νx⦈(Cases Cs)" and Qeq: "Q = Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
and "x ♯ Ψ" and "x ♯ (map fst Cs)" by blast
obtain y::name where "y ♯ Ψ" and "y ♯ Ψ'" and "y ♯ Cs"
by(generate_fresh "name") (auto simp add: fresh_prod)
from ‹y ♯ Cs› ‹x ♯ (map fst Cs)› have "y ♯ map fst ([(x, y)] ∙ Cs)" by(induct Cs) (auto simp add: fresh_list_cons fresh_list_nil)
moreover with ‹y ♯ Ψ› ‹y ♯ Ψ'› have "(Ψ ⊗ Ψ', ⦇νy⦈(Cases ([(x, y)] ∙ Cs)), Cases(map (λ(φ, P). (φ, ⦇νy⦈P)) ([(x, y)] ∙ Cs))) ∈ ?X"
by auto
moreover from Req ‹y ♯ Cs› have "R = ⦇νy⦈(Cases([(x, y)] ∙ Cs))"
apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
moreover from Qeq ‹y ♯ Cs› ‹x ♯ (map fst Cs)› have "Q = Cases(map (λ(φ, P). (φ, ⦇νy⦈P)) ([(x, y)] ∙ Cs))"
by(induct Cs arbitrary: Q) (auto simp add: fresh_list_cons fresh_prod alphaRes)
ultimately show ?case by blast
qed
next
case(cSym Ψ R Q)
thus ?case by blast
qed
}
moreover obtain y::name where "y ♯ Ψ" and "y ♯ Cs" by(generate_fresh "name") auto
moreover from ‹x ♯ map fst Cs› have "y ♯ map fst([(x, y)] ∙ Cs)"
by(induct Cs) (auto simp add: fresh_left calc_atm)
ultimately have "Ψ ⊳ ⦇νy⦈(Cases ([(x, y)] ∙ Cs)) ∼ Cases(map (λ(φ, P). (φ, ⦇νy⦈P)) ([(x, y)] ∙ Cs))"
by auto
moreover from ‹y ♯ Cs› have "⦇νy⦈(Cases ([(x, y)] ∙ Cs)) = ⦇νx⦈(Cases Cs)"
by(simp add: alphaRes eqvts)
moreover from ‹x ♯ map fst Cs› ‹y ♯ Cs› have "Cases(map (λ(φ, P). (φ, ⦇νy⦈P)) ([(x, y)] ∙ Cs)) = Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
by(induct Cs) (auto simp add: alphaRes)
ultimately show ?thesis by auto
qed
lemma bangExt:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
assumes "guarded P"
shows "Ψ ⊳ !P ∼ P ∥ !P"
proof -
let ?X = "{(Ψ, !P, P ∥ !P) | Ψ P. guarded P} ∪ {(Ψ, P ∥ !P, !P) | Ψ P. guarded P}"
from ‹guarded P› have "(Ψ, !P, P ∥ !P) ∈ ?X" by auto
thus ?thesis
proof(coinduct rule: bisimCoinduct)
case(cStatEq Ψ Q R)
from ‹(Ψ, Q, R) ∈ ?X› obtain P where Eq: "(Q = !P ∧ R = P ∥ !P) ∨ (Q = P ∥ !P ∧ R = !P)" and "guarded P"
by auto
obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" by(rule freshFrame)
from FrP ‹guarded P› have "Ψ⇩P ≃ SBottom'" by(blast dest: guardedStatEq)
from ‹Ψ⇩P ≃ SBottom'› have "Ψ ⊗ SBottom' ≃ Ψ ⊗ Ψ⇩P ⊗ SBottom'" by(metis Identity Composition AssertionStatEqTrans Commutativity AssertionStatEqSym)
hence "⟨A⇩P, Ψ ⊗ SBottom'⟩ ≃⇩F ⟨A⇩P, Ψ ⊗ Ψ⇩P ⊗ SBottom'⟩"
by(force intro: frameResChainPres)
moreover from ‹A⇩P ♯* Ψ› have "⟨ε, Ψ ⊗ SBottom'⟩ ≃⇩F ⟨A⇩P, Ψ ⊗ SBottom'⟩"
by(rule_tac FrameStatEqSym) (fastforce intro: frameResFreshChain)
ultimately show ?case using Eq ‹A⇩P ♯* Ψ› FrP
by auto (blast dest: FrameStatEqTrans FrameStatEqSym)+
next
case(cSim Ψ Q R)
thus ?case by(auto intro: bangExtLeft bangExtRight bisimReflexive)
next
case(cExt Ψ Q R)
thus ?case by auto
next
case(cSym Ψ Q R)
thus ?case by auto
qed
qed
lemma bisimParPresSym:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes "Ψ ⊳ P ∼ Q"
shows "Ψ ⊳ R ∥ P ∼ R ∥ Q"
using assms
by(metis bisimParComm bisimParPres bisimTransitive)
lemma bisimScopeExtSym:
fixes x :: name
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
assumes "x ♯ Ψ"
and "x ♯ Q"
shows "Ψ ⊳ ⦇νx⦈(P ∥ Q) ∼ (⦇νx⦈P) ∥ Q"
using assms
by(metis bisimScopeExt bisimTransitive bisimParComm bisimSymmetric bisimResPres)
lemma bisimScopeExtChainSym:
fixes xvec :: "name list"
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
assumes "xvec ♯* Ψ"
and "xvec ♯* Q"
shows "Ψ ⊳ ⦇ν*xvec⦈(P ∥ Q) ∼ (⦇ν*xvec⦈P) ∥ Q"
using assms
by(induct xvec) (auto intro: bisimScopeExtSym bisimReflexive bisimTransitive bisimResPres)
lemma bisimParPresAuxSym:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes "Ψ ⊗ Ψ⇩R ⊳ P ∼ Q"
and "extractFrame R = ⟨A⇩R, Ψ⇩R⟩"
and "A⇩R ♯* Ψ"
and "A⇩R ♯* P"
and "A⇩R ♯* Q"
shows "Ψ ⊳ R ∥ P ∼ R ∥ Q"
using assms
by(metis bisimParComm bisimParPresAux bisimTransitive)
lemma bangDerivative:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and α :: "'a action"
and P' :: "('a, 'b, 'c) psi"
assumes "Ψ ⊳ !P ⟼α ≺ P'"
and "Ψ ⊳ P ∼ Q"
and "bn α ♯* Ψ"
and "bn α ♯* P"
and "bn α ♯* Q"
and "bn α ♯* subject α"
and "guarded Q"
obtains Q' R T where "Ψ ⊳ !Q ⟼α ≺ Q'" and "Ψ ⊳ P' ∼ R ∥ !P" and "Ψ ⊳ Q' ∼ T ∥ !Q" and "Ψ ⊳ R ∼ T"
and "((supp R)::name set) ⊆ supp P'" and "((supp T)::name set) ⊆ supp Q'"
proof -
from ‹Ψ ⊳ !P ⟼α ≺ P'› have "guarded P" apply - by(ind_cases "Ψ ⊳ !P ⟼α ≺ P'") (auto simp add: psi.inject)
assume "⋀Q' R T. ⟦Ψ ⊳ !Q ⟼α ≺ Q'; Ψ ⊳ P' ∼ R ∥ !P; Ψ ⊳ Q' ∼ T ∥ !Q; Ψ ⊳ R ∼ T; ((supp R)::name set) ⊆ supp P';
((supp T)::name set) ⊆ supp Q'⟧ ⟹ thesis"
moreover from ‹Ψ ⊳ !P ⟼α ≺ P'› ‹bn α ♯* subject α› ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹bn α ♯* Q› ‹Ψ ⊳ P ∼ Q› ‹guarded Q›
have "∃Q' T R . Ψ ⊳ !Q ⟼α ≺ Q' ∧ Ψ ⊳ P' ∼ R ∥ !P ∧ Ψ ⊳ Q' ∼ T ∥ !Q ∧ Ψ ⊳ R ∼ T ∧
((supp R)::name set) ⊆ supp P' ∧ ((supp T)::name set) ⊆ supp Q'"
proof(nominal_induct avoiding: Q rule: bangInduct')
case(cAlpha α P' p Q)
then obtain Q' T R where QTrans: "Ψ ⊳ !Q ⟼α ≺ Q'" and "Ψ ⊳ P' ∼ R ∥ (P ∥ !P)" and "Ψ ⊳ Q' ∼ T ∥ !Q" and "Ψ ⊳ R ∼ T"
and suppR: "((supp R)::name set) ⊆ supp P'" and suppT: "((supp T)::name set) ⊆ supp Q'"
by blast
from QTrans have "distinct(bn α)" by(rule boundOutputDistinct)
have S: "set p ⊆ set(bn α) × set(bn(p ∙ α))" by fact
from QTrans ‹bn(p ∙ α) ♯* Q› ‹bn(p ∙ α) ♯* α› ‹bn α ♯* subject α› ‹distinct(bn α)› have "bn(p ∙ α) ♯* Q'"
by(drule_tac freeFreshChainDerivative) simp+
with QTrans ‹bn(p ∙ α) ♯* α› S ‹bn α ♯* subject α› have "Ψ ⊳ !Q ⟼(p ∙ α) ≺ (p ∙ Q')"
by(force simp add: residualAlpha)
moreover from ‹Ψ ⊳ P' ∼ R ∥ (P ∥ !P)› have "(p ∙ Ψ) ⊳ (p ∙ P') ∼ (p ∙ (R ∥ (P ∥ !P)))"
by(rule bisimClosed)
with ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹bn(p ∙ α) ♯* Ψ› ‹bn(p ∙ α) ♯* P› S have "Ψ ⊳ (p ∙ P') ∼ (p ∙ R) ∥ (P ∥ !P)"
by(simp add: eqvts)
moreover from ‹Ψ ⊳ Q' ∼ T ∥ !Q› have "(p ∙ Ψ) ⊳ (p ∙ Q') ∼ (p ∙ (T ∥ !Q))"
by(rule bisimClosed)
with ‹bn α ♯* Ψ› ‹bn α ♯* Q› ‹bn(p ∙ α) ♯* Ψ› ‹bn(p ∙ α) ♯* Q› S have "Ψ ⊳ (p ∙ Q') ∼ (p ∙ T) ∥ !Q"
by(simp add: eqvts)
moreover from ‹Ψ ⊳ R ∼ T› have "(p ∙ Ψ) ⊳ (p ∙ R) ∼ (p ∙ T)"
by(rule bisimClosed)
with ‹bn α ♯* Ψ› ‹bn(p ∙ α) ♯* Ψ› S have "Ψ ⊳ (p ∙ R) ∼ (p ∙ T)"
by(simp add: eqvts)
moreover from suppR have "((supp(p ∙ R))::name set) ⊆ supp(p ∙ P')"
apply(erule_tac rev_mp)
by(subst subsetClosed[of p, symmetric]) (simp add: eqvts)
moreover from suppT have "((supp(p ∙ T))::name set) ⊆ supp(p ∙ Q')"
apply(erule_tac rev_mp)
by(subst subsetClosed[of p, symmetric]) (simp add: eqvts)
ultimately show ?case by blast
next
case(cPar1 α P' Q)
from ‹Ψ ⊳ P ∼ Q› ‹Ψ ⊳ P ⟼α ≺ P'› ‹bn α ♯* Ψ› ‹bn α ♯* Q›
obtain Q' where QTrans: "Ψ ⊳ Q ⟼α ≺ Q'" and "Ψ ⊳ P' ∼ Q'"
by(blast dest: bisimE simE)
from QTrans have "Ψ ⊗ SBottom' ⊳ Q ⟼α ≺ Q'" by(metis statEqTransition Identity AssertionStatEqSym)
hence "Ψ ⊳ Q ∥ !Q ⟼α ≺ (Q' ∥ !Q)" using ‹bn α ♯* Q› by(rule_tac Par1) (assumption | simp)+
hence "Ψ ⊳ !Q ⟼α ≺ (Q' ∥ !Q)" using ‹guarded Q› by(rule Bang)
moreover from ‹guarded P› have "Ψ ⊳ P' ∥ !P ∼ P' ∥ (P ∥ !P)" by(metis bangExt bisimParPresSym)
moreover have "Ψ ⊳ Q' ∥ !Q ∼ Q' ∥ !Q" by(rule bisimReflexive)
ultimately show ?case using ‹Ψ ⊳ P' ∼ Q'› by(force simp add: psi.supp)
next
case(cPar2 α P' Q)
then obtain Q' T R where QTrans: "Ψ ⊳ !Q ⟼α ≺ Q'" and "Ψ ⊳ P' ∼ R ∥ !P" and "Ψ ⊳ Q' ∼ T ∥ !Q" and "Ψ ⊳ R ∼ T"
and suppR: "((supp R)::name set) ⊆ supp P'" and suppT: "((supp T)::name set) ⊆ supp Q'"
by blast
note QTrans
from ‹Ψ ⊳ P' ∼ R ∥ !P› have "Ψ ⊳ P ∥ P' ∼ R ∥ (P ∥ !P)"
by(metis bisimParPresSym bisimParComm bisimTransitive bisimParAssoc)
with QTrans show ?case using ‹Ψ ⊳ Q' ∼ T ∥ !Q› ‹Ψ ⊳ R ∼ T› suppR suppT
by(force simp add: psi.supp)
next
case(cComm1 M N P' K xvec P'' Q)
from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊳ Q ↝[bisim] P" by(metis bisimE)
with ‹Ψ ⊳ P ⟼M⦇N⦈ ≺ P'› obtain Q' where QTrans: "Ψ ⊳ Q ⟼M⦇N⦈ ≺ Q'" and "Ψ ⊳ Q' ∼ P'"
by(force dest: simE)
from QTrans have "Ψ ⊗ SBottom' ⊳ Q ⟼M⦇N⦈ ≺ Q'" by(metis statEqTransition Identity AssertionStatEqSym)
moreover obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Q" and "A⇩Q ♯* M"
by(rule_tac C="(Ψ, Q, M)" in freshFrame) auto
note FrQ
moreover from FrQ ‹guarded Q› have "Ψ⇩Q ≃ SBottom'" by(blast dest: guardedStatEq)
from ‹Ψ ⊳ !P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P''› ‹xvec ♯* K› ‹Ψ ⊳ P ∼ Q› ‹xvec ♯* Ψ› ‹xvec ♯* P› ‹xvec ♯* Q› ‹guarded Q›
obtain Q'' T R where QTrans': "Ψ ⊳ !Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q''" and "Ψ ⊳ P'' ∼ R ∥ !P" and "Ψ ⊳ Q'' ∼ T ∥ !Q" and "Ψ ⊳ R ∼ T"
and suppR: "((supp R)::name set) ⊆ supp P''" and suppT: "((supp T)::name set) ⊆ supp Q''" using cComm1
by fastforce
from QTrans' ‹Ψ⇩Q ≃ SBottom'› have "Ψ ⊗ Ψ⇩Q ⊳ !Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q''"
by(metis statEqTransition Identity compositionSym AssertionStatEqSym)
moreover from ‹Ψ ⊢ M ↔ K› ‹Ψ⇩Q ≃ SBottom'› have "Ψ ⊗ Ψ⇩Q ⊗ SBottom' ⊢ M ↔ K" by(metis statEqEnt Identity compositionSym AssertionStatEqSym)
ultimately have "Ψ ⊳ Q ∥ !Q ⟼τ ≺ (⦇ν*xvec⦈(Q' ∥ Q''))" using ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* M› ‹xvec ♯* Q›
by(rule_tac Comm1) (assumption | simp)+
hence "Ψ ⊳ !Q ⟼τ ≺ (⦇ν*xvec⦈(Q' ∥ Q''))" using ‹guarded Q› by(rule Bang)
moreover from ‹Ψ ⊳ P'' ∼ R ∥ !P› ‹guarded P› ‹xvec ♯* Ψ› have "Ψ ⊳ ⦇ν*xvec⦈(P' ∥ P'') ∼ ⦇ν*xvec⦈((P' ∥ R) ∥ (P ∥ !P))"
by(metis bisimParPresSym bangExt bisimTransitive bisimParAssoc bisimSymmetric bisimResChainPres)
with ‹xvec ♯* Ψ› ‹xvec ♯* P› have "Ψ ⊳ ⦇ν*xvec⦈(P' ∥ P'') ∼ (⦇ν*xvec⦈(P' ∥ R)) ∥ (P ∥ !P)"
by(metis bisimScopeExtChainSym bisimTransitive psiFreshVec)
moreover from ‹Ψ ⊳ Q'' ∼ T ∥ !Q› ‹xvec ♯* Ψ› ‹xvec ♯* Q› have "Ψ ⊳ ⦇ν*xvec⦈(Q' ∥ Q'') ∼ (⦇ν*xvec⦈(Q' ∥ T)) ∥ !Q"
by(metis bisimParPresSym bisimTransitive bisimParAssoc bisimSymmetric bisimResChainPres bisimScopeExtChainSym psiFreshVec)
moreover from ‹Ψ ⊳ R ∼ T› ‹Ψ ⊳ Q' ∼ P'› ‹xvec ♯* Ψ› have "Ψ ⊳ ⦇ν*xvec⦈(P' ∥ R) ∼ ⦇ν*xvec⦈(Q' ∥ T)"
by(metis bisimParPresSym bisimTransitive bisimResChainPres bisimParComm bisimE(4))
moreover from suppR have "((supp(⦇ν*xvec⦈(P' ∥ R)))::name set) ⊆ supp((⦇ν*xvec⦈(P' ∥ P'')))"
by(auto simp add: psi.supp resChainSupp)
moreover from suppT have "((supp(⦇ν*xvec⦈(Q' ∥ T)))::name set) ⊆ supp((⦇ν*xvec⦈(Q' ∥ Q'')))"
by(auto simp add: psi.supp resChainSupp)
ultimately show ?case by blast
next
case(cComm2 M xvec N P' K P'' Q)
from ‹Ψ ⊳ P ∼ Q› ‹Ψ ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'› ‹xvec ♯* Ψ› ‹xvec ♯* Q›
obtain Q' where QTrans: "Ψ ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'" and "Ψ ⊳ P' ∼ Q'"
by(metis bisimE simE bn.simps)
from QTrans have "Ψ ⊗ SBottom' ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'" by(metis statEqTransition Identity AssertionStatEqSym)
moreover obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Q" and "A⇩Q ♯* M"
by(rule_tac C="(Ψ, Q, M)" in freshFrame) auto
note FrQ
moreover from FrQ ‹guarded Q› have "Ψ⇩Q ≃ SBottom'" by(blast dest: guardedStatEq)
from ‹Ψ ⊳ !P ⟼K⦇N⦈ ≺ P''› ‹Ψ ⊳ P ∼ Q› ‹guarded Q›
obtain Q'' T R where QTrans': "Ψ ⊳ !Q ⟼K⦇N⦈ ≺ Q''" and "Ψ ⊳ P'' ∼ R ∥ !P" and "Ψ ⊳ Q'' ∼ T ∥ !Q" and "Ψ ⊳ R ∼ T"
and suppR: "((supp R)::name set) ⊆ supp P''" and suppT: "((supp T)::name set) ⊆ supp Q''" using cComm2
by fastforce
from QTrans' ‹Ψ⇩Q ≃ SBottom'› have "Ψ ⊗ Ψ⇩Q ⊳ !Q ⟼K⦇N⦈ ≺ Q''"
by(metis statEqTransition Identity compositionSym AssertionStatEqSym)
moreover from ‹Ψ ⊢ M ↔ K› ‹Ψ⇩Q ≃ SBottom'› have "Ψ ⊗ Ψ⇩Q ⊗ SBottom' ⊢ M ↔ K" by(metis statEqEnt Identity compositionSym AssertionStatEqSym)
ultimately have "Ψ ⊳ Q ∥ !Q ⟼τ ≺ (⦇ν*xvec⦈(Q' ∥ Q''))" using ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* M› ‹xvec ♯* Q›
by(rule_tac Comm2) (assumption | simp)+
hence "Ψ ⊳ !Q ⟼τ ≺ (⦇ν*xvec⦈(Q' ∥ Q''))" using ‹guarded Q› by(rule Bang)
moreover from ‹Ψ ⊳ P'' ∼ R ∥ !P› ‹guarded P› ‹xvec ♯* Ψ› have "Ψ ⊳ ⦇ν*xvec⦈(P' ∥ P'') ∼ ⦇ν*xvec⦈((P' ∥ R) ∥ (P ∥ !P))"
by(metis bisimParPresSym bangExt bisimTransitive bisimParAssoc bisimSymmetric bisimResChainPres)
with ‹xvec ♯* Ψ› ‹xvec ♯* P› have "Ψ ⊳ ⦇ν*xvec⦈(P' ∥ P'') ∼ (⦇ν*xvec⦈(P' ∥ R)) ∥ (P ∥ !P)"
by(metis bisimScopeExtChainSym bisimTransitive psiFreshVec)
moreover from ‹Ψ ⊳ Q'' ∼ T ∥ !Q› ‹xvec ♯* Ψ› ‹xvec ♯* Q› have "Ψ ⊳ ⦇ν*xvec⦈(Q' ∥ Q'') ∼ (⦇ν*xvec⦈(Q' ∥ T)) ∥ !Q"
by(metis bisimParPresSym bisimTransitive bisimParAssoc bisimSymmetric bisimResChainPres bisimScopeExtChainSym psiFreshVec)
moreover from ‹Ψ ⊳ R ∼ T› ‹Ψ ⊳ P' ∼ Q'› ‹xvec ♯* Ψ› have "Ψ ⊳ ⦇ν*xvec⦈(P' ∥ R) ∼ ⦇ν*xvec⦈(Q' ∥ T)"
by(metis bisimParPresSym bisimTransitive bisimResChainPres bisimParComm)
moreover from suppR have "((supp(⦇ν*xvec⦈(P' ∥ R)))::name set) ⊆ supp((⦇ν*xvec⦈(P' ∥ P'')))"
by(auto simp add: psi.supp resChainSupp)
moreover from suppT have "((supp(⦇ν*xvec⦈(Q' ∥ T)))::name set) ⊆ supp((⦇ν*xvec⦈(Q' ∥ Q'')))"
by(auto simp add: psi.supp resChainSupp)
ultimately show ?case by blast
next
case(cBang α P' Q)
then obtain Q' T R where QTrans: "Ψ ⊳ !Q ⟼α ≺ Q'" and "Ψ ⊳ P' ∼ R ∥ (P ∥ !P)" and "Ψ ⊳ Q' ∼ T ∥ !Q" and "Ψ ⊳ R ∼ T"
and suppR: "((supp R)::name set) ⊆ supp P'" and suppT: "((supp T)::name set) ⊆ supp Q'"
by blast
from ‹Ψ ⊳ P' ∼ R ∥ (P ∥ !P)› ‹guarded P› have "Ψ ⊳ P' ∼ R ∥ !P" by(metis bangExt bisimParPresSym bisimTransitive bisimSymmetric)
with QTrans show ?case using ‹Ψ ⊳ Q' ∼ T ∥ !Q› ‹Ψ ⊳ R ∼ T› suppR suppT
by blast
qed
ultimately show ?thesis by blast
qed
lemma structCongBisim:
fixes P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
assumes "P ≡⇩s Q"
shows "P ∼ Q"
using assms
by(induct rule: structCong.induct)
(auto intro: bisimReflexive bisimSymmetric bisimTransitive bisimParComm bisimParAssoc bisimParNil bisimResNil bisimResComm bisimScopeExt bisimCasePushRes bisimInputPushRes bisimOutputPushRes bangExt)
lemma bisimBangPres:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
assumes "Ψ ⊳ P ∼ Q"
and "guarded P"
and "guarded Q"
shows "Ψ ⊳ !P ∼ !Q"
proof -
let ?X = "{(Ψ, R ∥ !P, R ∥ !Q) | Ψ P Q R. Ψ ⊳ P ∼ Q ∧ guarded P ∧ guarded Q}"
let ?Y = "{(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ ?X ∧ Ψ ⊳ Q' ∼ Q}"
from assms have "(Ψ, 𝟬 ∥ !P, 𝟬 ∥ !Q) ∈ ?X" by(blast intro: bisimReflexive)
moreover have "eqvt ?X"
apply(auto simp add: eqvt_def)
apply(drule_tac p=p in bisimClosed)
by fastforce
ultimately have "Ψ ⊳ 𝟬 ∥ !P ∼ 𝟬 ∥ !Q"
proof(coinduct rule: weakTransitiveCoinduct)
case(cStatEq Ψ P Q)
thus ?case by auto
next
case(cSim Ψ RP RQ)
from ‹(Ψ, RP, RQ) ∈ ?X› obtain P Q R where "Ψ ⊳ P ∼ Q" and "guarded P" and "guarded Q"
and "RP = R ∥ !P" and "RQ = R ∥ !Q"
by auto
note ‹Ψ ⊳ P ∼ Q›
moreover from ‹eqvt ?X› have "eqvt ?Y" by blast
moreover note ‹guarded P› ‹guarded Q› bisimE(2) bisimE(3) bisimE(4) statEqBisim bisimClosed bisimParAssoc[THEN bisimSymmetric]
bisimParPres bisimParPresAuxSym bisimResChainPres bisimScopeExtChainSym bisimTransitive
moreover have "⋀Ψ P Q R T. ⟦Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ ?Y; Ψ ⊳ R ∼ T⟧ ⟹ (Ψ, P, T) ∈ ?Y"
by auto (metis bisimTransitive)
moreover have "⋀Ψ P Q R. ⟦Ψ ⊳ P ∼ Q; guarded P; guarded Q⟧ ⟹ (Ψ, R ∥ !P, R ∥ !Q) ∈ ?Y" by(blast intro: bisimReflexive)
moreover have "⋀Ψ P α P' Q. ⟦Ψ ⊳ !P ⟼α ≺ P'; Ψ ⊳ P ∼ Q; bn α ♯* Ψ; bn α ♯* P; bn α ♯* Q; guarded Q; bn α ♯* subject α⟧ ⟹
∃Q' R T. Ψ ⊳ !Q ⟼α ≺ Q' ∧ Ψ ⊳ P' ∼ R ∥ !P ∧ Ψ ⊳ Q' ∼ T ∥ !Q ∧
Ψ ⊳ R ∼ T ∧ ((supp R)::name set) ⊆ supp P' ∧
((supp T)::name set) ⊆ supp Q'"
by(blast elim: bangDerivative)
ultimately have "Ψ ⊳ R ∥ !P ↝[?Y] R ∥ !Q"
by(rule bangPres)
with ‹RP = R ∥ !P› ‹RQ = R ∥ !Q› show ?case
by blast
next
case(cExt Ψ RP RQ Ψ')
thus ?case by(blast dest: bisimE)
next
case(cSym Ψ RP RQ)
thus ?case by(blast dest: bisimE)
qed
thus ?thesis
by(metis bisimTransitive bisimParNil bisimSymmetric bisimParComm)
qed
end
end