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(