Theory Sim_Struct_Cong
theory Sim_Struct_Cong
imports Simulation
begin
lemma partitionListLeft:
assumes "xs@ys=xs'@y#ys'"
and "y mem xs"
and "distinct(xs@ys)"
obtains zs where "xs = xs'@y#zs" and "ys'=zs@ys"
using assms
by(auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
lemma partitionListRight:
assumes "xs@ys=xs'@y#ys'"
and "y mem ys"
and "distinct(xs@ys)"
obtains zs where "xs' = xs@zs" and "ys=zs@y#ys'"
using assms
by(force simp add: append_eq_append_conv2 append_eq_Cons_conv)
context env begin
lemma resComm:
fixes Ψ :: 'b
and x :: name
and y :: name
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and P :: "('a, 'b, 'c) psi"
assumes "x ♯ Ψ"
and "y ♯ Ψ"
and "eqvt Rel"
and R1: "⋀Ψ' Q. (Ψ', Q, Q) ∈ Rel"
and R2: "⋀Ψ' a b Q. ⟦a ♯ Ψ'; b ♯ Ψ'⟧ ⟹ (Ψ', ⦇νa⦈(⦇νb⦈Q), ⦇νb⦈(⦇νa⦈Q)) ∈ Rel"
shows "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ↝[Rel] ⦇νy⦈(⦇νx⦈P)"
proof(case_tac "x=y")
assume "x = y"
thus ?thesis using R1
by(force intro: reflexive)
next
assume "x ≠ y"
note ‹eqvt Rel›
moreover from ‹x ♯ Ψ› ‹y ♯ Ψ› have "[x, y] ♯* Ψ" by(simp add: fresh_star_def)
moreover have "[x, y] ♯* ⦇νx⦈(⦇νy⦈P)" by(simp add: abs_fresh)
moreover have "[x, y] ♯* ⦇νy⦈(⦇νx⦈P)" by(simp add: abs_fresh)
ultimately show ?thesis
proof(induct rule: simIChainFresh[where C="(x, y)"])
case(cSim α P')
from ‹bn α ♯* (x, y)› ‹bn α ♯* (⦇νx⦈(⦇νy⦈P))› have "x ♯ bn α" and "y ♯ bn α" and "bn α ♯* P" by simp+
from ‹[x, y] ♯* α› have "x ♯ α" and "y ♯ α" by simp+
from ‹[x, y] ♯* P'› have "x ♯ P'" and "y ♯ P'" by simp+
from ‹bn α ♯* P› ‹x ♯ α› have "bn α ♯* ⦇νx⦈P" by(simp add: abs_fresh)
with ‹Ψ ⊳ ⦇νy⦈(⦇νx⦈P) ⟼α ≺ P'› ‹y ♯ Ψ› ‹y ♯ α› ‹y ♯ P'› ‹bn α ♯* Ψ›
show ?case using ‹bn α ♯* subject α› ‹x ♯ α› ‹x ♯ P'› ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹bn α ♯* subject α› ‹y ♯ α›
proof(induct rule: resCases')
case(cOpen M yvec1 yvec2 y' N P')
from ‹yvec1 ♯* yvec2› ‹distinct yvec1› ‹distinct yvec2› have "distinct(yvec1@yvec2)" by auto
from ‹x ♯ M⦇ν*(yvec1 @ y' # yvec2)⦈⟨N⟩› have "x ♯ M" and "x ♯ yvec1" and "x ≠ y'" and "x ♯ yvec2" and "x ♯ N"
by simp+
from ‹y ♯ M⦇ν*(yvec1 @ y' # yvec2)⦈⟨N⟩› have "y ♯ M" and "y ♯ yvec1" and "y ♯ yvec2"
by simp+
from ‹Ψ ⊳ ([(y, y')] ∙ ⦇νx⦈P) ⟼M⦇ν*(yvec1@yvec2)⦈⟨N⟩ ≺ P'› ‹x ≠ y› ‹x ≠ y'›
have "Ψ ⊳ ⦇νx⦈([(y, y')] ∙ P) ⟼M⦇ν*(yvec1@yvec2)⦈⟨N⟩ ≺ P'" by(simp add: eqvts)
moreover note ‹x ♯ Ψ›
moreover from ‹x ♯ N› ‹x ♯ yvec1› ‹x ♯ yvec2› ‹x ♯ M› have "x ♯ M⦇ν*(yvec1@yvec2)⦈⟨N⟩" by simp
moreover note ‹x ♯ P'›
moreover from ‹yvec1 ♯* Ψ› ‹yvec2 ♯* Ψ› have "bn(M⦇ν*(yvec1@yvec2)⦈⟨N⟩) ♯* Ψ" by simp
moreover from ‹yvec1 ♯* ⦇νx⦈P› ‹yvec2 ♯* ⦇νx⦈P› ‹y ♯ yvec1› ‹y' ♯ yvec1› ‹y ♯ yvec2› ‹y' ♯ yvec2› ‹x ♯ yvec1› ‹x ♯ yvec2›
have "bn(M⦇ν*(yvec1@yvec2)⦈⟨N⟩) ♯* ([(y, y')] ∙ P)" by simp
moreover from ‹yvec1 ♯* M› ‹yvec2 ♯* M› have "bn(M⦇ν*(yvec1 @ yvec2)⦈⟨N⟩) ♯* subject(M⦇ν*(yvec1 @ yvec2)⦈⟨N⟩)"
by simp
moreover have "bn(M⦇ν*(yvec1 @ yvec2)⦈⟨N⟩) = yvec1@yvec2" by simp
moreover have "subject(M⦇ν*(yvec1 @ yvec2)⦈⟨N⟩) = Some M" by simp
moreover have "object(M⦇ν*(yvec1 @ yvec2)⦈⟨N⟩) = Some N" by simp
ultimately show ?case
proof(induct rule: resCases')
case(cOpen M' xvec1 xvec2 x' N' P')
from ‹bn(M'⦇ν*(xvec1 @ x' # xvec2)⦈⟨N'⟩) = yvec1 @ yvec2› have "yvec1@yvec2 = xvec1@x'#xvec2" by simp
from ‹subject(M'⦇ν*(xvec1 @ x' # xvec2)⦈⟨N'⟩) = Some M› have "M = M'" by simp
from ‹object(M'⦇ν*(xvec1 @ x' # xvec2)⦈⟨N'⟩) = Some N› have "N = N'" by simp
from ‹x ♯ yvec1› ‹x ♯ yvec2› ‹y' ♯ yvec1› ‹y' ♯ yvec2› ‹y ♯ yvec1› ‹y ♯ yvec2›
have "x ♯ (yvec1@yvec2)" and "y ♯ (yvec1@yvec2)" and "y' ♯ (yvec1@yvec2)" by simp+
with ‹yvec1@yvec2 = xvec1@x'#xvec2›
have "x ♯ xvec1" and "x ≠ x'" and "x ♯ xvec2" and "y ♯ xvec1" and "y ≠ x'" and "y ♯ xvec2"
and "y' ♯ xvec1" and "x' ≠ y'" and "y' ♯ xvec2"
by auto
show ?case
proof(case_tac "x' mem yvec1")
assume "x' mem yvec1"
with ‹yvec1@yvec2 = xvec1@x'#xvec2› ‹distinct (yvec1@yvec2)›
obtain xvec2' where Eq1: "yvec1=xvec1@x'#xvec2'"
and Eq: "xvec2=xvec2'@yvec2"
by(rule_tac partitionListLeft)
from ‹Ψ ⊳ ([(x, x')] ∙ [(y, y')] ∙ P) ⟼M'⦇ν*(xvec1@xvec2)⦈⟨N'⟩ ≺ P'› ‹y' ∈ supp N› ‹y' ♯ Ψ› ‹y' ♯ M› ‹y' ♯ xvec1› ‹y' ♯ xvec2› Eq ‹M=M'› ‹N = N'›
have "Ψ ⊳ ⦇νy'⦈([(x, x')] ∙ [(y, y')] ∙ P) ⟼M'⦇ν*((xvec1@xvec2')@y'#yvec2)⦈⟨N'⟩ ≺ P'"
by(rule_tac Open) auto
then have "Ψ ⊳ ⦇νx'⦈(⦇νy'⦈([(x, x')] ∙ [(y, y')] ∙ P)) ⟼M⦇ν*(xvec1@x'#xvec2'@y'#yvec2)⦈⟨N⟩ ≺ P'"
using ‹x' ∈ supp N'› ‹x' ♯ Ψ› ‹x' ♯ M'› ‹x' ♯ xvec1› ‹x' ♯ xvec2› ‹x' ≠ y'› Eq ‹M=M'› ‹N=N'›
by(rule_tac Open) auto
with ‹x' ≠ y'› ‹x ≠ y'› ‹x' ♯ [(y, y')] ∙ P›
have "Ψ ⊳ ⦇νx⦈(⦇νy'⦈([(y, y')] ∙ P)) ⟼M⦇ν*(xvec1@x'#xvec2'@y'#yvec2)⦈⟨N⟩ ≺ P'"
by(subst alphaRes[where y=x']) (simp add: calc_atm eqvts abs_fresh)+
with Eq1 ‹y' ♯ ⦇νx⦈P› ‹x ≠ y'› R1 show ?case
by(fastforce simp add: alphaRes abs_fresh)
next
assume "¬x' mem yvec1"
hence "x' ♯ yvec1" by(simp add: fresh_def)
from ‹¬x' mem yvec1› ‹yvec1@yvec2 = xvec1@x'#xvec2›
have "x' mem yvec2"
by(fastforce simp add: append_eq_append_conv2 append_eq_Cons_conv
fresh_list_append fresh_list_cons)
with ‹yvec1@yvec2 = xvec1@x'#xvec2› ‹distinct (yvec1@yvec2)›
obtain xvec2' where Eq: "xvec1=yvec1@xvec2'"
and Eq1: "yvec2=xvec2'@x'#xvec2"
by(rule_tac partitionListRight)
from ‹Ψ ⊳ ([(x, x')] ∙ [(y, y')] ∙ P) ⟼M'⦇ν*(xvec1@xvec2)⦈⟨N'⟩ ≺ P'› ‹y' ∈ supp N› ‹y' ♯ Ψ› ‹y' ♯ M› ‹y' ♯ xvec1› ‹y' ♯ xvec2› Eq ‹M=M'› ‹N = N'›
have "Ψ ⊳ ⦇νy'⦈([(x, x')] ∙ [(y, y')] ∙ P) ⟼M'⦇ν*(yvec1@y'#xvec2'@xvec2)⦈⟨N'⟩ ≺ P'"
by(rule_tac Open) (assumption | simp)+
then have "Ψ ⊳ ⦇νx'⦈(⦇νy'⦈([(x, x')] ∙ [(y, y')] ∙ P)) ⟼M⦇ν*((yvec1@y'#xvec2')@x'#xvec2)⦈⟨N⟩ ≺ P'"
using ‹x' ∈ supp N'› ‹x' ♯ Ψ› ‹x' ♯ M'› ‹x' ♯ xvec1› ‹x' ♯ xvec2› ‹x' ≠ y'› Eq ‹M=M'› ‹N=N'›
by(rule_tac Open) auto
with ‹x' ≠ y'› ‹x ≠ y'› ‹x' ♯ [(y, y')] ∙ P›
have "Ψ ⊳ ⦇νx⦈(⦇νy'⦈([(y, y')] ∙ P)) ⟼M⦇ν*((yvec1@y'#xvec2')@x'#xvec2)⦈⟨N⟩ ≺ P'"
by(subst alphaRes[where y=x']) (simp add: calc_atm eqvts abs_fresh)+
with Eq1 ‹y' ♯ ⦇νx⦈P› ‹x ≠ y'› R1 show ?case
by(fastforce simp add: alphaRes abs_fresh)
qed
next
case(cRes P')
from ‹Ψ ⊳ ([(y, y')] ∙ P) ⟼M⦇ν*(yvec1@yvec2)⦈⟨N⟩ ≺ P'› ‹y' ∈ supp N› ‹y' ♯ Ψ› ‹y' ♯ M› ‹y' ♯ yvec1› ‹y' ♯ yvec2›
have "Ψ ⊳ ⦇νy'⦈([(y, y')] ∙ P) ⟼M⦇ν*(yvec1@y'#yvec2)⦈⟨N⟩ ≺ P'" by(rule Open)
with ‹y' ♯ ⦇νx⦈P› ‹x ≠ y'›have "Ψ ⊳ ⦇νy⦈P ⟼M⦇ν*(yvec1@y'#yvec2)⦈⟨N⟩ ≺ P'" by(simp add: alphaRes abs_fresh)
hence "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ⟼M⦇ν*(yvec1@y'#yvec2)⦈⟨N⟩ ≺ ⦇νx⦈P'" using ‹x ♯ Ψ› ‹x ♯ M› ‹x ♯ yvec1› ‹x ≠ y'› ‹x ♯ yvec2› ‹x ♯ N›
by(rule_tac Scope) auto
moreover have "(Ψ, ⦇νx⦈P', ⦇νx⦈P') ∈ Rel" by(rule R1)
ultimately show ?case by blast
qed
next
case(cRes P')
from ‹x ♯ ⦇νy⦈P'› ‹x ≠ y› have "x ♯ P'" by(simp add: abs_fresh)
with ‹Ψ ⊳ ⦇νx⦈P ⟼α ≺ P'› ‹x ♯ Ψ› ‹x ♯ α›
show ?case using ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹bn α ♯* subject α› ‹y ♯ α›
proof(induct rule: resCases')
case(cOpen M xvec1 xvec2 x' N P')
from ‹y ♯ M⦇ν*(xvec1@x'#xvec2)⦈⟨N⟩› have "y ≠ x'" and "y ♯ M⦇ν*(xvec1@xvec2)⦈⟨N⟩" by simp+
from ‹Ψ ⊳ ([(x, x')] ∙ P) ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ P'› ‹y ♯ Ψ› ‹y ♯ M⦇ν*(xvec1@xvec2)⦈⟨N⟩›
have "Ψ ⊳ ⦇νy⦈([(x, x')] ∙ P) ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ ⦇νy⦈P'"
by(rule Scope)
hence "Ψ ⊳ ⦇νx'⦈(⦇νy⦈([(x, x')] ∙ P)) ⟼M⦇ν*(xvec1@x'#xvec2)⦈⟨N⟩ ≺ ⦇νy⦈P'"
using ‹x' ∈ supp N› ‹x' ♯ Ψ› ‹x' ♯ M› ‹x' ♯ xvec1› ‹x' ♯ xvec2›
by(rule Open)
with ‹y ≠ x'› ‹x ≠ y› ‹x' ♯ P› have "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ⟼M⦇ν*(xvec1@x'#xvec2)⦈⟨N⟩ ≺ ⦇νy⦈P'"
by(subst alphaRes[where y=x']) (simp add: abs_fresh eqvts calc_atm)+
moreover have "(Ψ, ⦇νy⦈P', ⦇νy⦈P') ∈ Rel" by(rule R1)
ultimately show ?case by blast
next
case(cRes P')
from ‹Ψ ⊳ P ⟼α ≺ P'› ‹y ♯ Ψ› ‹y ♯ α›
have "Ψ ⊳ ⦇νy⦈P ⟼α ≺ ⦇νy⦈P'" by(rule Scope)
hence "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ⟼α ≺ ⦇νx⦈(⦇νy⦈P')" using ‹x ♯ Ψ› ‹x ♯ α›
by(rule Scope)
moreover from ‹x ♯ Ψ› ‹y ♯ Ψ› have "(Ψ, ⦇νx⦈(⦇νy⦈P'), ⦇νy⦈(⦇νx⦈P')) ∈ Rel"
by(rule R2)
ultimately show ?case by blast
qed
qed
qed
qed
lemma parAssocLeft:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
assumes "eqvt Rel"
and C1: "⋀Ψ' S T U. (Ψ, (S ∥ T) ∥ U, S ∥ (T ∥ U)) ∈ Rel"
and C2: "⋀xvec Ψ' S T U. ⟦xvec ♯* Ψ'; xvec ♯* S⟧ ⟹ (Ψ', ⦇ν*xvec⦈((S ∥ T) ∥ U), S ∥ (⦇ν*xvec⦈(T ∥ U))) ∈ Rel"
and C3: "⋀xvec Ψ' S T U. ⟦xvec ♯* Ψ'; xvec ♯* U⟧ ⟹ (Ψ', (⦇ν*xvec⦈(S ∥ T)) ∥ U, ⦇ν*xvec⦈(S ∥ (T ∥ U))) ∈ Rel"
and C4: "⋀Ψ' S T xvec. ⟦(Ψ', S, T) ∈ Rel; xvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*xvec⦈S, ⦇ν*xvec⦈T) ∈ Rel"
shows "Ψ ⊳ (P ∥ Q) ∥ R ↝[Rel] P ∥ (Q ∥ R)"
using ‹eqvt Rel›
proof(induct rule: simI[of _ _ _ _ "()"])
case(cSim α PQR)
from ‹bn α ♯* (P ∥ Q ∥ R)› have "bn α ♯* P" and "bn α ♯* Q" and "bn α ♯* R" by simp+
hence "bn α ♯* (Q ∥ R)" by simp
with ‹Ψ ⊳ P ∥ (Q ∥ R) ⟼α ≺ PQR› ‹bn α ♯* Ψ› ‹bn α ♯* P›
show ?case using ‹bn α ♯* subject α›
proof(induct rule: parCases[where C = "(Ψ, P, Q, R, α)"])
case(cPar1 P' A⇩Q⇩R Ψ⇩Q⇩R)
from ‹A⇩Q⇩R ♯* (Ψ, P, Q, R, α)› have "A⇩Q⇩R ♯* Q" and "A⇩Q⇩R ♯* R"
by simp+
with ‹extractFrame(Q ∥ R) = ⟨A⇩Q⇩R, Ψ⇩Q⇩R⟩› ‹distinct A⇩Q⇩R›
obtain A⇩Q Ψ⇩Q A⇩R Ψ⇩R where "A⇩Q⇩R = A⇩Q@A⇩R" and "Ψ⇩Q⇩R = Ψ⇩Q ⊗ Ψ⇩R" and FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩"
and "A⇩Q ♯* Ψ⇩R" and "A⇩R ♯* Ψ⇩Q"
by(rule_tac mergeFrameE) (auto dest: extractFrameFreshChain)
from ‹A⇩Q⇩R = A⇩Q@A⇩R› ‹A⇩Q⇩R ♯* Ψ› ‹A⇩Q⇩R ♯* P› ‹A⇩Q⇩R ♯* Q› ‹A⇩Q⇩R ♯* α›
have "A⇩Q ♯* Ψ" and "A⇩R ♯* Ψ" and "A⇩Q ♯* P" and "A⇩R ♯* P" and "A⇩Q ♯* Q" and "A⇩R ♯* Q" and "A⇩Q ♯* α" and "A⇩R ♯* α"
by simp+
from ‹Ψ ⊗ Ψ⇩Q⇩R ⊳ P ⟼α ≺ P'› ‹Ψ⇩Q⇩R = Ψ⇩Q ⊗ Ψ⇩R› have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q ⊳ P ⟼α ≺ P'"
by(metis statEqTransition Associativity Commutativity Composition)
hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ Q ⟼α ≺ (P' ∥ Q)" using FrQ ‹bn α ♯* Q› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩Q ♯* P› ‹A⇩Q ♯* α›
by(rule_tac Par1) auto
hence "Ψ ⊳ (P ∥ Q) ∥ R ⟼α ≺ ((P' ∥ Q) ∥ R)" using FrR ‹bn α ♯* R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* α›
by(rule_tac Par1) auto
moreover have "(Ψ, (P' ∥ Q) ∥ R, P' ∥ (Q ∥ R)) ∈ Rel" by(rule C1)
ultimately show ?case by blast
next
case(cPar2 QR A⇩P Ψ⇩P)
from ‹A⇩P ♯* (Ψ, P, Q, R, α)› have "A⇩P ♯* Q" and "A⇩P ♯* R" and "A⇩P ♯* α"
by simp+
have FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" by fact
with ‹bn α ♯* P› ‹A⇩P ♯* α› have "bn α ♯* Ψ⇩P" by(auto dest: extractFrameFreshChain)
with ‹bn α ♯* Ψ› have "bn α ♯* (Ψ ⊗ Ψ⇩P)" by force
with ‹Ψ ⊗ Ψ⇩P ⊳ Q ∥ R ⟼α ≺ QR›
show ?case using ‹bn α ♯* Q› ‹bn α ♯* R› ‹bn α ♯* subject α› ‹A⇩P ♯* Q› ‹A⇩P ♯* R›
proof(induct rule: parCasesSubject[where C = "(A⇩P, Ψ⇩P, P, Q, R, Ψ)"])
case(cPar1 Q' A⇩R Ψ⇩R)
from ‹A⇩R ♯* (A⇩P, Ψ⇩P, P, Q, R, Ψ)› have "A⇩R ♯* A⇩P" and "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* Ψ⇩P" and "A⇩R ♯* Ψ"
by simp+
from ‹A⇩P ♯* R› ‹extractFrame R = ⟨A⇩R, Ψ⇩R⟩› ‹A⇩R ♯* A⇩P› have "A⇩P ♯* Ψ⇩R"
by(drule_tac extractFrameFreshChain) auto
from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩R ⊳ Q ⟼α ≺ Q'› have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P ⊳ Q ⟼α ≺ Q'"
by(metis statEqTransition Associativity Commutativity Composition)
hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ Q ⟼α ≺ (P ∥ Q')"
using FrP ‹bn α ♯* P› ‹A⇩P ♯* Ψ› ‹A⇩P ♯* Ψ⇩R› ‹A⇩P ♯* Q› ‹A⇩P ♯* α›
by(rule_tac Par2) (assumption | force)+
hence "Ψ ⊳ (P ∥ Q) ∥ R ⟼α ≺ ((P ∥ Q') ∥ R)"
using ‹extractFrame R = ⟨A⇩R, Ψ⇩R⟩› ‹bn α ♯* R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* α›
by(rule_tac Par1) (assumption | simp)+
moreover have "(Ψ, (P ∥ Q') ∥ R, P ∥ (Q' ∥ R)) ∈ Rel" by(rule C1)
ultimately show ?case by blast
next
case(cPar2 R' A⇩Q Ψ⇩Q)
from ‹A⇩Q ♯* (A⇩P, Ψ⇩P, P, Q, R, Ψ)› have "A⇩Q ♯* A⇩P" and "A⇩Q ♯* R" and "A⇩Q ♯* Ψ⇩P" and "A⇩Q ♯* Ψ"
by simp+
have FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
from ‹A⇩P ♯* Q› FrQ ‹A⇩Q ♯* A⇩P› have "A⇩P ♯* Ψ⇩Q"
by(drule_tac extractFrameFreshChain) auto
from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q ⊳ R ⟼α ≺ R'›
have "Ψ ⊗ (Ψ⇩P ⊗ Ψ⇩Q) ⊳ R ⟼α ≺ R'"
by(blast intro: statEqTransition Associativity)
moreover from FrP FrQ ‹A⇩Q ♯* A⇩P› ‹A⇩P ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ⇩P›
have "extractFrame(P ∥ Q) = ⟨(A⇩P@A⇩Q), Ψ⇩P ⊗ Ψ⇩Q⟩ " by simp
moreover from ‹bn α ♯* P› ‹bn α ♯* Q› have "bn α ♯* (P ∥ Q)" by simp
moreover from ‹A⇩P ♯* Ψ› ‹A⇩Q ♯* Ψ› have "(A⇩P@A⇩Q) ♯* Ψ" by simp
moreover from ‹A⇩P ♯* R› ‹A⇩Q ♯* R› have "(A⇩P@A⇩Q) ♯* R" by simp
moreover from ‹A⇩P ♯* α› ‹A⇩Q ♯* α› have "(A⇩P@A⇩Q) ♯* α" by simp
ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼α ≺ ((P ∥ Q) ∥ R')"
by(rule Par2)
moreover have "(Ψ, (P ∥ Q) ∥ R', P ∥ (Q ∥ R')) ∈ Rel" by(rule C1)
ultimately show ?case by blast
next
case(cComm1 Ψ⇩R M N Q' A⇩Q Ψ⇩Q K xvec R' A⇩R)
from ‹A⇩Q ♯* (A⇩P, Ψ⇩P, P, Q, R, Ψ)›
have "A⇩Q ♯* P" and "A⇩Q ♯* Q" and "A⇩Q ♯* R" and "A⇩Q ♯* A⇩P" and "A⇩Q ♯* Ψ⇩P" and "A⇩Q ♯* Ψ" by simp+
from ‹A⇩R ♯* (A⇩P, Ψ⇩P, P, Q, R, Ψ)› have "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* R" and "A⇩R ♯* A⇩P" and "A⇩R ♯* Ψ" by simp+
from ‹xvec ♯* (A⇩P, Ψ⇩P, P, Q, R, Ψ)› have "xvec ♯* A⇩P" and "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* Ψ" by simp+
have FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
with ‹A⇩P ♯* Q› ‹A⇩Q ♯* A⇩P› have "A⇩P ♯* Ψ⇩Q"
by(drule_tac extractFrameFreshChain) auto
have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
with ‹A⇩P ♯* R› ‹A⇩R ♯* A⇩P› have "A⇩P ♯* Ψ⇩R"
by(drule_tac extractFrameFreshChain) auto
from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'› ‹A⇩P ♯* R› ‹xvec ♯* A⇩P› ‹xvec ♯* K› ‹distinct xvec› have "A⇩P ♯* N"
by(rule_tac outputFreshChainDerivative) auto
from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩R ⊳ Q ⟼M⦇N⦈ ≺ Q'› have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P ⊳ Q ⟼M⦇N⦈ ≺ Q'"
by(metis statEqTransition Associativity Commutativity Composition)
hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ Q ⟼M⦇N⦈ ≺ (P ∥ Q')" using FrP ‹A⇩P ♯* Ψ› ‹A⇩P ♯* Ψ⇩R› ‹A⇩P ♯* Q› ‹A⇩P ♯* M› ‹A⇩P ♯* N›
by(rule_tac Par2) auto
moreover from FrP FrQ ‹A⇩P ♯* Ψ⇩Q› ‹A⇩Q ♯* A⇩P› ‹A⇩Q ♯* Ψ⇩P› have "extractFrame(P ∥ Q) = ⟨(A⇩P@A⇩Q), Ψ⇩P ⊗ Ψ⇩Q⟩"
by simp
moreover from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'› have "Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'"
by(metis statEqTransition Associativity)
moreover note ‹extractFrame R = ⟨A⇩R, Ψ⇩R⟩›
moreover from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q ⊗ Ψ⇩R ⊢ M ↔ K› have "Ψ ⊗ (Ψ⇩P ⊗ Ψ⇩Q) ⊗ Ψ⇩R ⊢ M ↔ K"
by(metis statEqEnt Associativity Commutativity Composition)
ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ ⦇ν*xvec⦈((P ∥ Q') ∥ R')"
using ‹A⇩P ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩R ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩Q ♯* P› ‹A⇩R ♯* P› ‹A⇩P ♯* Q› ‹A⇩Q ♯* Q› ‹A⇩R ♯* Q› ‹A⇩P ♯* R› ‹A⇩Q ♯* R› ‹A⇩R ♯* R›
‹A⇩P ♯* M› ‹A⇩Q ♯* M› ‹A⇩R ♯* K› ‹A⇩R ♯* A⇩P› ‹A⇩Q ♯* A⇩R› ‹xvec ♯* P› ‹xvec ♯* Q›
by(rule_tac Comm1) (assumption | simp)+
moreover from ‹xvec ♯* Ψ› ‹xvec ♯* P› have "(Ψ, ⦇ν*xvec⦈((P ∥ Q') ∥ R'), P ∥ (⦇ν*xvec⦈(Q' ∥ R'))) ∈ Rel"
by(rule C2)
ultimately show ?case by blast
next
case(cComm2 Ψ⇩R M xvec N Q' A⇩Q Ψ⇩Q K R' A⇩R)
from ‹A⇩Q ♯* (A⇩P, Ψ⇩P, P, Q, R, Ψ)›
have "A⇩Q ♯* P" and "A⇩Q ♯* Q" and "A⇩Q ♯* R" and "A⇩Q ♯* A⇩P" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Ψ⇩P" by simp+
from ‹A⇩R ♯* (A⇩P, Ψ⇩P, P, Q, R, Ψ)› have "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* R" and "A⇩R ♯* A⇩P"and "A⇩R ♯* Ψ" by simp+
from ‹xvec ♯* (A⇩P, Ψ⇩P, P, Q, R, Ψ)› have "xvec ♯* A⇩P" and "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* Ψ" by simp+
have FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
with ‹A⇩P ♯* Q› ‹A⇩Q ♯* A⇩P› have "A⇩P ♯* Ψ⇩Q"
by(drule_tac extractFrameFreshChain) auto
have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
with ‹A⇩P ♯* R› ‹A⇩R ♯* A⇩P› have "A⇩P ♯* Ψ⇩R"
by(drule_tac extractFrameFreshChain) auto
from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩R ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'› ‹A⇩P ♯* Q› ‹xvec ♯* A⇩P› ‹xvec ♯* M› ‹distinct xvec› have "A⇩P ♯* N"
by(rule_tac outputFreshChainDerivative) auto
from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩R ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'› have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'"
by(metis statEqTransition Associativity Commutativity Composition)
hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ (P ∥ Q')" using FrP ‹A⇩P ♯* Ψ› ‹A⇩P ♯* Ψ⇩R› ‹A⇩P ♯* Q› ‹A⇩P ♯* M› ‹A⇩P ♯* N› ‹xvec ♯* P› ‹xvec ♯* A⇩P›
by(rule_tac Par2) auto
moreover from FrP FrQ ‹A⇩P ♯* Ψ⇩Q› ‹A⇩Q ♯* A⇩P› ‹A⇩Q ♯* Ψ⇩P› have "extractFrame(P ∥ Q) = ⟨(A⇩P@A⇩Q), Ψ⇩P ⊗ Ψ⇩Q⟩"
by simp+
moreover from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q ⊳ R ⟼K⦇N⦈ ≺ R'› have "Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q ⊳ R ⟼K⦇N⦈ ≺ R'"
by(metis statEqTransition Associativity)
moreover note ‹extractFrame R = ⟨A⇩R, Ψ⇩R⟩›
moreover from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q ⊗ Ψ⇩R ⊢ M ↔ K› have "Ψ ⊗ (Ψ⇩P ⊗ Ψ⇩Q) ⊗ Ψ⇩R ⊢ M ↔ K"
by(metis statEqEnt Associativity Commutativity Composition)
ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ ⦇ν*xvec⦈((P ∥ Q') ∥ R')"
using ‹A⇩P ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩R ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩Q ♯* P› ‹A⇩R ♯* P› ‹A⇩P ♯* Q› ‹A⇩Q ♯* Q› ‹A⇩R ♯* Q› ‹A⇩P ♯* R› ‹A⇩Q ♯* R› ‹A⇩R ♯* R›
‹A⇩P ♯* M› ‹A⇩Q ♯* M› ‹A⇩R ♯* K› ‹A⇩R ♯* A⇩P› ‹A⇩Q ♯* A⇩R› ‹xvec ♯* R›
by(rule_tac Comm2) (assumption | simp)+
moreover from ‹xvec ♯* Ψ› ‹xvec ♯* P› have "(Ψ, ⦇ν*xvec⦈((P ∥ Q') ∥ R'), P ∥ (⦇ν*xvec⦈(Q' ∥ R'))) ∈ Rel"
by(rule C2)
ultimately show ?case by blast
qed
next
case(cComm1 Ψ⇩Q⇩R M N P' A⇩P Ψ⇩P K xvec QR' A⇩Q⇩R)
from ‹xvec ♯* (Ψ, P, Q, R, α)› have "xvec ♯* Q" and "xvec ♯* R" by simp+
from ‹A⇩Q⇩R ♯* (Ψ, P, Q, R, α)› have "A⇩Q⇩R ♯* Q" and "A⇩Q⇩R ♯* R" and "A⇩Q⇩R ♯* Ψ" by simp+
from ‹A⇩P ♯* (Q ∥ R)› have "A⇩P ♯* Q" and "A⇩P ♯* R" by simp+
have PTrans: "Ψ ⊗ Ψ⇩Q⇩R ⊳ P ⟼M⦇N⦈ ≺ P'" and FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and MeqK: "Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q⇩R ⊢ M ↔ K" by fact+
note ‹Ψ ⊗ Ψ⇩P ⊳ Q ∥ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ QR'›
moreover from ‹xvec ♯* Ψ› ‹xvec ♯* Ψ⇩P› have "xvec ♯* (Ψ ⊗ Ψ⇩P)" by force
moreover note ‹xvec ♯* Q›‹xvec ♯* R› ‹xvec ♯* K›
‹extractFrame(Q ∥ R) = ⟨A⇩Q⇩R, Ψ⇩Q⇩R⟩› ‹distinct A⇩Q⇩R›
moreover from ‹A⇩Q⇩R ♯* Ψ› ‹A⇩Q⇩R ♯* Ψ⇩P› have "A⇩Q⇩R ♯* (Ψ ⊗ Ψ⇩P)" by force
ultimately show ?case using ‹A⇩Q⇩R ♯* Q› ‹A⇩Q⇩R ♯* R› ‹A⇩Q⇩R ♯* K›
proof(induct rule: parCasesOutputFrame)
case(cPar1 Q' A⇩Q Ψ⇩Q A⇩R Ψ⇩R)
have Aeq: "A⇩Q⇩R = A⇩Q@A⇩R" and Ψeq: "Ψ⇩Q⇩R = Ψ⇩Q ⊗ Ψ⇩R" by fact+
from PTrans Ψeq have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q ⊳ P ⟼M⦇N⦈ ≺ P'"
by(metis statEqTransition Associativity Commutativity Composition)
moreover note FrP
moreover from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩R ⊳ Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'› have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P ⊳ Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'"
by(metis statEqTransition Associativity Commutativity Composition)
moreover note ‹extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩›
moreover from MeqK Ψeq have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P ⊗ Ψ⇩Q ⊢ M ↔ K"
by(metis statEqEnt Associativity Commutativity Composition)
moreover from ‹A⇩P ♯* R› ‹A⇩P ♯* A⇩Q⇩R› Aeq ‹extractFrame R = ⟨A⇩R, Ψ⇩R⟩› have "A⇩P ♯* A⇩Q" and "A⇩P ♯* Ψ⇩R"
by(auto dest: extractFrameFreshChain)
moreover from ‹A⇩Q⇩R ♯* P› ‹A⇩Q⇩R ♯* Ψ› Aeq have "A⇩Q ♯* P" and "A⇩Q ♯* Ψ" by simp+
ultimately have "Ψ ⊗ Ψ⇩R ⊳ P ∥ Q ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ Q')"
using ‹A⇩P ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩P ♯* Q› ‹A⇩P ♯* M› ‹A⇩P ♯* A⇩Q› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩Q ♯* P› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* K› ‹xvec ♯* P›
by(rule_tac Comm1) (assumption | force)+
moreover from ‹A⇩Q⇩R ♯* Ψ› Aeq have "A⇩R ♯* Ψ" by simp
moreover from ‹A⇩Q⇩R ♯* P› Aeq have "A⇩R ♯* P" by simp
ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ (⦇ν*xvec⦈(P' ∥ Q')) ∥ R" using ‹extractFrame R = ⟨A⇩R, Ψ⇩R⟩› ‹A⇩R ♯* Q›
by(rule_tac Par1) (assumption | simp)+
moreover from ‹xvec ♯* Ψ› ‹xvec ♯* R› have "(Ψ, (⦇ν*xvec⦈(P' ∥ Q')) ∥ R, ⦇ν*xvec⦈(P' ∥ (Q' ∥ R))) ∈ Rel"
by(rule C3)
ultimately show ?case by blast
next
case(cPar2 R' A⇩Q Ψ⇩Q A⇩R Ψ⇩R)
have Aeq: "A⇩Q⇩R = A⇩Q@A⇩R" and Ψeq: "Ψ⇩Q⇩R = Ψ⇩Q ⊗ Ψ⇩R" by fact+
from ‹A⇩Q⇩R ♯* Ψ› ‹A⇩Q⇩R ♯* P› ‹A⇩Q⇩R ♯* Ψ⇩P› ‹A⇩P ♯* A⇩Q⇩R› Aeq have "A⇩R ♯* Ψ" and "A⇩R ♯* Ψ⇩P" and "A⇩P ♯* A⇩R" and "A⇩P ♯* A⇩Q" and "A⇩R ♯* P" by simp+
from ‹A⇩Q⇩R ♯* Ψ› Aeq have "A⇩Q ♯* Ψ" by simp
from ‹A⇩Q⇩R ♯* P› ‹A⇩P ♯* A⇩Q⇩R› Aeq FrP have "A⇩Q ♯* Ψ⇩P" by(auto dest: extractFrameFreshChain)
from ‹A⇩P ♯* A⇩Q⇩R› ‹extractFrame R = ⟨A⇩R, Ψ⇩R⟩› ‹extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩› Aeq ‹A⇩P ♯* Q› ‹A⇩P ♯* R› have "A⇩P ♯* Ψ⇩Q" and "A⇩P ♯* Ψ⇩R" by(auto dest: extractFrameFreshChain)
have RTrans: "(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'" and FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact+
then obtain K' where KeqK': "((Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q) ⊗ Ψ⇩R ⊢ K ↔ K'" and "A⇩P ♯* K'" and "A⇩Q ♯* K'"
using ‹A⇩P ♯* R› ‹A⇩Q ♯* R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ⇩P› ‹A⇩R ♯* Ψ⇩Q› ‹A⇩Q ♯* A⇩R› ‹A⇩P ♯* A⇩R› ‹A⇩R ♯* R› ‹A⇩R ♯* R› ‹A⇩R ♯* K› ‹distinct A⇩R› ‹xvec ♯* K› ‹distinct xvec›
by(rule_tac B="A⇩P@A⇩Q" in obtainPrefix) (assumption | force)+
from PTrans Ψeq have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q ⊳ P ⟼M⦇N⦈ ≺ P'"
by(metis statEqTransition Associativity Commutativity Composition)
moreover from MeqK KeqK' Ψeq have MeqK': "((Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q) ⊗ Ψ⇩P ⊢ M ↔ K'"
by(metis statEqEnt Associativity Commutativity Composition chanEqTrans)
ultimately have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q ⊳ P ⟼K'⦇N⦈ ≺ P'" using FrP ‹distinct A⇩P› ‹A⇩P ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩P ♯* M› ‹A⇩P ♯* K'› ‹A⇩P ♯* Ψ⇩Q› ‹A⇩P ♯* Ψ⇩R›
by(rule_tac inputRenameSubject) auto
moreover from ‹A⇩Q⇩R ♯* P› ‹A⇩Q⇩R ♯* N› Aeq have "A⇩Q ♯* P" and "A⇩Q ♯* N" by simp+
ultimately have "Ψ ⊗ Ψ⇩R ⊳ P ∥ Q ⟼K'⦇N⦈ ≺ P' ∥ Q" using ‹extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩Q ♯* K'› ‹A⇩Q ♯* Ψ›
by(rule_tac Par1) (assumption | force)+
moreover from FrP ‹extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩› ‹A⇩P ♯* A⇩Q› ‹A⇩P ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ⇩P›
have "extractFrame(P ∥ Q) = ⟨(A⇩P@A⇩Q), Ψ⇩P ⊗ Ψ⇩Q⟩" by simp+
moreover from RTrans have "Ψ ⊗ (Ψ⇩P ⊗ Ψ⇩Q) ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'" by(metis Associativity statEqTransition)
moreover note FrR
moreover from MeqK' KeqK' have "Ψ ⊗ (Ψ⇩P ⊗ Ψ⇩Q) ⊗ Ψ⇩R ⊢ K' ↔ K"
by(metis statEqEnt Associativity Commutativity Composition chanEqTrans chanEqSym)
ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ ⦇ν*xvec⦈((P' ∥ Q) ∥ R')"
using ‹A⇩P ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩Q ♯* P› ‹A⇩P ♯* Q› ‹A⇩Q ♯* Q› ‹A⇩P ♯* R› ‹A⇩Q ♯* R› ‹A⇩P ♯* K'› ‹A⇩Q ♯* K'› ‹A⇩P ♯* A⇩R› ‹A⇩Q ♯* A⇩R›
‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* R› ‹A⇩R ♯* K› ‹xvec ♯* P› ‹xvec ♯* Q›
by(rule_tac Comm1) (assumption | simp)+
moreover from ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈((P' ∥ Q) ∥ R'), ⦇ν*xvec⦈(P' ∥ (Q ∥ R'))) ∈ Rel"
by(metis C1 C4)
ultimately show ?case by blast
qed
next
case(cComm2 Ψ⇩Q⇩R M xvec N P' A⇩P Ψ⇩P K QR' A⇩Q⇩R)
from ‹A⇩Q⇩R ♯* (Ψ, P, Q, R, α)› have "A⇩Q⇩R ♯* Q" and "A⇩Q⇩R ♯* R" and "A⇩Q⇩R ♯* Ψ" by simp+
from ‹A⇩P ♯* (Q ∥ R)› ‹xvec ♯* (Q ∥ R)› have "A⇩P ♯* Q" and "A⇩P ♯* R" and "xvec ♯* Q" and "xvec ♯* R" by simp+
have PTrans: "Ψ ⊗ Ψ⇩Q⇩R ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'" and FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and MeqK: "Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q⇩R ⊢ M ↔ K" by fact+
note ‹Ψ ⊗ Ψ⇩P ⊳ Q ∥ R ⟼K⦇N⦈ ≺ QR'› ‹extractFrame(Q ∥ R) = ⟨A⇩Q⇩R, Ψ⇩Q⇩R⟩› ‹distinct A⇩Q⇩R›
moreover from ‹A⇩Q⇩R ♯* Ψ› ‹A⇩Q⇩R ♯* Ψ⇩P› have "A⇩Q⇩R ♯* (Ψ ⊗ Ψ⇩P)" by force
ultimately show ?case using ‹A⇩Q⇩R ♯* Q› ‹A⇩Q⇩R ♯* R› ‹A⇩Q⇩R ♯* K›
proof(induct rule: parCasesInputFrame)
case(cPar1 Q' A⇩Q Ψ⇩Q A⇩R Ψ⇩R)
have Aeq: "A⇩Q⇩R = A⇩Q@A⇩R" and Ψeq: "Ψ⇩Q⇩R = Ψ⇩Q ⊗ Ψ⇩R" by fact+
from PTrans Ψeq have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
by(metis statEqTransition Associativity Commutativity Composition)
moreover note FrP
moreover from ‹(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩R ⊳ Q ⟼K⦇N⦈ ≺ Q'› have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P ⊳ Q ⟼K⦇N⦈ ≺ Q'"
by(metis statEqTransition Associativity Commutativity Composition)
moreover note ‹extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩›
moreover from MeqK Ψeq have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P ⊗ Ψ⇩Q ⊢ M ↔ K"
by(metis statEqEnt Associativity Commutativity Composition)
moreover from ‹A⇩P ♯* Q› ‹A⇩P ♯* R› ‹A⇩P ♯* A⇩Q⇩R› Aeq ‹extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩› ‹extractFrame R = ⟨A⇩R, Ψ⇩R⟩›
have "A⇩P ♯* A⇩Q" and "A⇩P ♯* Ψ⇩R" by(auto dest: extractFrameFreshChain)
moreover from ‹A⇩Q⇩R ♯* Ψ› ‹A⇩Q⇩R ♯* P› Aeq have "A⇩Q ♯* Ψ" and "A⇩Q ♯* P" by simp+
ultimately have "Ψ ⊗ Ψ⇩R ⊳ P ∥ Q ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ Q')"
using ‹A⇩P ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩P ♯* Q› ‹A⇩P ♯* M› ‹A⇩P ♯* A⇩Q› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩Q ♯* P› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* K› ‹xvec ♯* Q›
by(rule_tac Comm2) (assumption | force)+
moreover from ‹A⇩Q⇩R ♯* Ψ› ‹A⇩Q⇩R ♯* P› Aeq have "A⇩R ♯* Ψ" and "A⇩R ♯* P" by simp+
ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ (⦇ν*xvec⦈(P' ∥ Q')) ∥ R" using ‹extractFrame R = ⟨A⇩R, Ψ⇩R⟩› ‹A⇩R ♯* Q›
by(rule_tac Par1) (assumption | simp)+
moreover from ‹xvec ♯* Ψ› ‹xvec ♯* R› have "(Ψ, (⦇ν*xvec⦈(P' ∥ Q')) ∥ R, ⦇ν*xvec⦈(P' ∥ (Q' ∥ R))) ∈ Rel"
by(rule C3)
ultimately show ?case by blast
next
case(cPar2 R' A⇩Q Ψ⇩Q A⇩R Ψ⇩R)
have Aeq: "A⇩Q⇩R = A⇩Q@A⇩R" and Ψeq: "Ψ⇩Q⇩R = Ψ⇩Q ⊗ Ψ⇩R" by fact+
from ‹A⇩Q⇩R ♯* Ψ› ‹A⇩Q⇩R ♯* P› ‹A⇩Q⇩R ♯* Ψ⇩P› ‹A⇩P ♯* A⇩Q⇩R› Aeq
have "A⇩R ♯* Ψ" and "A⇩R ♯* Ψ⇩P" and "A⇩P ♯* A⇩R" and "A⇩P ♯* A⇩Q" and "A⇩R ♯* P" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Ψ⇩P" by simp+
have RTrans: "(Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q ⊳ R ⟼K⦇N⦈ ≺ R'" and FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact+
then obtain K' where KeqK': "((Ψ ⊗ Ψ⇩P) ⊗ Ψ⇩Q) ⊗ Ψ⇩R ⊢ K ↔ K'" and "A⇩P ♯* K'" and "A⇩Q ♯* K'"
using ‹A⇩P ♯* R› ‹A⇩Q ♯* R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ⇩P› ‹A⇩R ♯* Ψ⇩Q› ‹A⇩Q ♯* A⇩R› ‹A⇩P ♯* A⇩R› ‹A⇩R ♯* R› ‹A⇩R ♯* R› ‹A⇩R ♯* K› ‹distinct A⇩R›
by(rule_tac B="A⇩P@A⇩Q" in obtainPrefix) (assumption | force)+
from PTrans Ψeq have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
by(metis statEqTransition Associativity Commutativity Composition)
moreover from MeqK KeqK' Ψeq have MeqK': "((Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q) ⊗ Ψ⇩P ⊢ M ↔ K'"
by(metis statEqEnt Associativity Commutativity Composition chanEqTrans)
moreover from ‹A⇩P ♯* R› ‹A⇩P ♯* Q› ‹A⇩P ♯* A⇩Q⇩R› FrR ‹extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩› Aeq have "A⇩P ♯* Ψ⇩Q" and "A⇩P ♯* Ψ⇩R"
by(auto dest: extractFrameFreshChain)
ultimately have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q ⊳ P ⟼K'⦇ν*xvec⦈⟨N⟩ ≺ P'" using FrP ‹distinct A⇩P› ‹A⇩P ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩P ♯* M› ‹A⇩P ♯* K'›
by(rule_tac outputRenameSubject) auto
moreover from ‹A⇩Q⇩R ♯* P› ‹A⇩Q⇩R ♯* N› ‹A⇩Q⇩R ♯* xvec› Aeq have "A⇩Q ♯* P" and "A⇩Q ♯* N" and "A⇩Q ♯* xvec" by simp+
ultimately have "Ψ ⊗ Ψ⇩R ⊳ P ∥ Q ⟼K'⦇ν*xvec⦈⟨N⟩ ≺ (P' ∥ Q)" using ‹extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩Q ♯* K'› ‹xvec ♯* Q› ‹A⇩Q ♯* Ψ›
by(rule_tac Par1) (assumption | force)+
moreover from FrP ‹extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩› ‹A⇩P ♯* A⇩Q› ‹A⇩P ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ⇩P›
have "extractFrame(P ∥ Q) = ⟨(A⇩P@A⇩Q), Ψ⇩P ⊗ Ψ⇩Q⟩" by simp+
moreover from RTrans have "Ψ ⊗ (Ψ⇩P ⊗ Ψ⇩Q) ⊳ R ⟼K⦇N⦈ ≺ R'" by(metis Associativity statEqTransition)
moreover note FrR
moreover from MeqK' KeqK' have "Ψ ⊗ (Ψ⇩P ⊗ Ψ⇩Q) ⊗ Ψ⇩R ⊢ K' ↔ K"
by(metis statEqEnt Associativity Commutativity Composition chanEqTrans chanEqSym)
ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ ⦇ν*xvec⦈((P' ∥ Q) ∥ R')"
using ‹A⇩P ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩Q ♯* P› ‹A⇩P ♯* Q› ‹A⇩Q ♯* Q› ‹A⇩P ♯* R› ‹A⇩Q ♯* R› ‹A⇩P ♯* K'› ‹A⇩Q ♯* K'› ‹A⇩P ♯* A⇩R› ‹A⇩Q ♯* A⇩R›
‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* R› ‹A⇩R ♯* K› ‹xvec ♯* R›
by(rule_tac Comm2) (assumption | simp)+
moreover from ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈((P' ∥ Q) ∥ R'), ⦇ν*xvec⦈(P' ∥ (Q ∥ R'))) ∈ Rel"
by(metis C1 C4)
ultimately show ?case by blast
qed
qed
qed
lemma parNilLeft:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
assumes "eqvt Rel"
and C1: "⋀Q. (Ψ, Q ∥ 𝟬, Q) ∈ Rel"
shows "Ψ ⊳ (P ∥ 𝟬) ↝[Rel] P"
using ‹eqvt Rel›
proof(induct rule: simI[of _ _ _ _ "()"])
case(cSim α P')
from ‹Ψ ⊳ P ⟼α ≺ P'› have "Ψ ⊗ SBottom' ⊳ P ⟼α ≺ P'"
by(metis statEqTransition Identity AssertionStatEqSym)
hence "Ψ ⊳ (P ∥ 𝟬) ⟼α ≺ (P' ∥ 𝟬)"
by(rule_tac Par1) auto
moreover have "(Ψ, P' ∥ 𝟬, P') ∈ Rel" by(rule C1)
ultimately show ?case by blast
qed
lemma parNilRight:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
assumes "eqvt Rel"
and C1: "⋀Q. (Ψ, Q, (Q ∥ 𝟬)) ∈ Rel"
shows "Ψ ⊳ P ↝[Rel] (P ∥ 𝟬)"
using ‹eqvt Rel›
proof(induct rule: simI[of _ _ _ _ "()"])
case(cSim α P')
note ‹Ψ ⊳ P ∥ 𝟬 ⟼α ≺ P'› ‹bn α ♯* Ψ› ‹bn α ♯* P›
moreover have "bn α ♯* 𝟬" by simp
ultimately show ?case using ‹bn α ♯* subject α›
proof(induct rule: parCases[where C="()"])
case(cPar1 P' A⇩Q Ψ⇩Q)
from ‹extractFrame(𝟬) = ⟨A⇩Q, Ψ⇩Q⟩› have "Ψ⇩Q = SBottom'" by auto
with ‹Ψ ⊗ Ψ⇩Q ⊳ P ⟼α ≺ P'› have "Ψ ⊳ P ⟼α ≺ P'"
by(metis statEqTransition Identity)
moreover have "(Ψ, P', P' ∥ 𝟬) ∈ Rel" by(rule C1)
ultimately show ?case by blast
next
case(cPar2 Q' A⇩P Ψ⇩P)
from ‹Ψ ⊗ Ψ⇩P ⊳ 𝟬 ⟼α ≺ Q'› have False
by auto
thus ?case by simp
next
case(cComm1 Ψ⇩Q M N P' A⇩P Ψ⇩P K xvec Q' A⇩Q)
from ‹Ψ ⊗ Ψ⇩P ⊳ 𝟬 ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'› have False by auto
thus ?case by simp
next
case(cComm2 Ψ⇩Q M xvec N P' A⇩P Ψ⇩P K Q' A⇩Q)
from ‹Ψ ⊗ Ψ⇩P ⊳ 𝟬 ⟼K⦇N⦈ ≺ Q'› have False
by auto
thus ?case by simp
qed
qed
lemma resNilLeft:
fixes x :: name
and Ψ :: 'b
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
shows "Ψ ⊳ ⦇νx⦈𝟬 ↝[Rel] 𝟬"
by(auto simp add: simulation_def)
lemma resNilRight:
fixes x :: name
and Ψ :: 'b
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
shows "Ψ ⊳ 𝟬 ↝[Rel] ⦇νx⦈𝟬"
apply(auto simp add: simulation_def)
by(cases rule: semantics.cases) (auto simp add: psi.inject alpha')
lemma inputPushResLeft:
fixes Ψ :: 'b
and x :: name
and M :: 'a
and xvec :: "name list"
and N :: 'a
and P :: "('a, 'b, 'c) psi"
assumes "eqvt Rel"
and "x ♯ Ψ"
and "x ♯ M"
and "x ♯ xvec"
and "x ♯ N"
and C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"
shows "Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ↝[Rel] M⦇λ*xvec N⦈.⦇νx⦈P"
proof -
note ‹eqvt Rel› ‹x ♯ Ψ›
moreover have "x ♯ ⦇νx⦈(M⦇λ*xvec N⦈.P)" by(simp add: abs_fresh)
moreover from ‹x ♯ M› ‹x ♯ N› have "x ♯ M⦇λ*xvec N⦈.⦇νx⦈P"
by(auto simp add: inputChainFresh abs_fresh)
ultimately show ?thesis
proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
case(cSim α P')
from ‹Ψ ⊳ M⦇λ*xvec N⦈.⦇νx⦈P ⟼α ≺ P'› ‹x ♯ α› show ?case
proof(induct rule: inputCases)
case(cInput K Tvec)
from ‹x ♯ K⦇N[xvec::=Tvec]⦈› have "x ♯ K" and "x ♯ N[xvec::=Tvec]" by simp+
from ‹Ψ ⊢ M ↔ K› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹length xvec = length Tvec›
have "Ψ ⊳ M⦇λ*xvec N⦈.P ⟼K⦇(N[xvec::=Tvec])⦈ ≺ P[xvec::=Tvec]"
by(rule Input)
hence "Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ⟼K⦇(N[xvec::=Tvec])⦈ ≺ ⦇νx⦈(P[xvec::=Tvec])" using ‹x ♯ Ψ› ‹x ♯ K› ‹x ♯ N[xvec::=Tvec]›
by(rule_tac Scope) auto
moreover from ‹length xvec = length Tvec› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹x ♯ N[xvec::=Tvec]› have "x ♯ Tvec"
by(rule substTerm.subst3)
with ‹x ♯ xvec› have "(Ψ, ⦇νx⦈(P[xvec::=Tvec]), (⦇νx⦈P)[xvec::=Tvec]) ∈ Rel"
by(force intro: C1)
ultimately show ?case by blast
qed
qed
qed
lemma inputPushResRight:
fixes Ψ :: 'b
and x :: name
and M :: 'a
and xvec :: "name list"
and N :: 'a
and P :: "('a, 'b, 'c) psi"
assumes "eqvt Rel"
and "x ♯ Ψ"
and "x ♯ M"
and "x ♯ xvec"
and "x ♯ N"
and C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"
shows "Ψ ⊳ M⦇λ*xvec N⦈.⦇νx⦈P ↝[Rel] ⦇νx⦈(M⦇λ*xvec N⦈.P)"
proof -
note ‹eqvt Rel› ‹x ♯ Ψ›
moreover from ‹x ♯ M› ‹x ♯ N› have "x ♯ M⦇λ*xvec N⦈.⦇νx⦈P"
by(auto simp add: inputChainFresh abs_fresh)
moreover have "x ♯ ⦇νx⦈(M⦇λ*xvec N⦈.P)" by(simp add: abs_fresh)
ultimately show ?thesis
proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
case(cSim α P')
note ‹Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ⟼α ≺ P'› ‹x ♯ Ψ› ‹x ♯ α› ‹x ♯ P'› ‹bn α ♯* Ψ›
moreover from ‹bn α ♯* (⦇νx⦈(M⦇λ*xvec N⦈.P))› ‹x ♯ α› have "bn α ♯* (M⦇λ*xvec N⦈.P)"
by simp
ultimately show ?case using ‹bn α ♯* subject α›
proof(induct rule: resCases)
case(cRes P')
from ‹Ψ ⊳ M⦇λ*xvec N⦈.P ⟼α ≺ P'› ‹x ♯ α› show ?case
proof(induct rule: inputCases)
case(cInput K Tvec)
from ‹x ♯ K⦇N[xvec::=Tvec]⦈› have "x ♯ K" and "x ♯ N[xvec::=Tvec]" by simp+
from ‹Ψ ⊢ M ↔ K› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹length xvec = length Tvec›
have "Ψ ⊳ M⦇λ*xvec N⦈.(⦇νx⦈P) ⟼K⦇(N[xvec::=Tvec])⦈ ≺ (⦇νx⦈P)[xvec::=Tvec]"
by(rule Input)
moreover from ‹length xvec = length Tvec› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹x ♯ N[xvec::=Tvec]› have "x ♯ Tvec"
by(rule substTerm.subst3)
with ‹x ♯ xvec› have "(Ψ, (⦇νx⦈P)[xvec::=Tvec], ⦇νx⦈(P[xvec::=Tvec])) ∈ Rel"
by(force intro: C1)
ultimately show ?case by blast
qed
next
case cOpen
then have False by auto
thus ?case by simp
qed
qed
qed
lemma outputPushResLeft:
fixes Ψ :: 'b
and x :: name
and M :: 'a
and N :: 'a
and P :: "('a, 'b, 'c) psi"
assumes "eqvt Rel"
and "x ♯ Ψ"
and "x ♯ M"
and "x ♯ N"
and C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"
shows "Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ↝[Rel] M⟨N⟩.⦇νx⦈P"
proof -
note ‹eqvt Rel› ‹x ♯ Ψ›
moreover have "x ♯ ⦇νx⦈(M⟨N⟩.P)" by(simp add: abs_fresh)
moreover from ‹x ♯ M› ‹x ♯ N› have "x ♯ M⟨N⟩.⦇νx⦈P"
by(auto simp add: abs_fresh)
ultimately show ?thesis
proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
case(cSim α P')
from ‹Ψ ⊳ M⟨N⟩.⦇νx⦈P ⟼α ≺ P'› ‹x ♯ α›
show ?case
proof(induct rule: outputCases)
case(cOutput K)
from ‹Ψ ⊢ M ↔ K› have "Ψ ⊳ M⟨N⟩.P ⟼K⟨N⟩ ≺ P"
by(rule Output)
hence "Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ⟼K⟨N⟩ ≺ ⦇νx⦈P" using ‹x ♯ Ψ› ‹x ♯ K⟨N⟩›
by(rule Scope)
moreover have "(Ψ, ⦇νx⦈P, ⦇νx⦈P) ∈ Rel" by(rule C1)
ultimately show ?case by blast
qed
qed
qed
lemma outputPushResRight:
fixes Ψ :: 'b
and x :: name
and M :: 'a
and N :: 'a
and P :: "('a, 'b, 'c) psi"
assumes "eqvt Rel"
and "x ♯ Ψ"
and "x ♯ M"
and "x ♯ N"
and C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"
shows "Ψ ⊳ M⟨N⟩.⦇νx⦈P ↝[Rel] ⦇νx⦈(M⟨N⟩.P)"
proof -
note ‹eqvt Rel› ‹x ♯ Ψ›
moreover from ‹x ♯ M› ‹x ♯ N› have "x ♯ M⟨N⟩.⦇νx⦈P"
by(auto simp add: abs_fresh)
moreover have "x ♯ ⦇νx⦈(M⟨N⟩.P)" by(simp add: abs_fresh)
ultimately show ?thesis
proof(induct rule: simIFresh[of _ _ _ _ _ "(M, N)"])
case(cSim α P')
note ‹Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ⟼α ≺ P'› ‹x ♯ Ψ› ‹x ♯ α› ‹x ♯ P'› ‹bn α ♯* Ψ›
moreover from ‹bn α ♯* (⦇νx⦈(M⟨N⟩.P))› ‹x ♯ α› have "bn α ♯* (M⟨N⟩.P)" by simp
ultimately show ?case using ‹bn α ♯* subject α› ‹bn α ♯* (M, N)› ‹x ♯ α›
proof(induct rule: resCases)
case(cOpen K xvec1 xvec2 y N' P')
from ‹bn(K⦇ν*(xvec1@y#xvec2)⦈⟨N'⟩) ♯* (M, N)› have "y ♯ N" by simp+
from ‹Ψ ⊳ M⟨N⟩.P ⟼K⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N')⟩ ≺ ([(x, y)] ∙ P')›
have "N = ([(x, y)] ∙ N')"
apply -
by(ind_cases "Ψ ⊳ M⟨N⟩.P ⟼K⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N')⟩ ≺ ([(x, y)] ∙ P')")
(auto simp add: residualInject psi.inject)
with ‹x ♯ N› ‹y ♯ N› ‹x ≠ y› have "N = N'"
by(subst pt_bij[OF pt_name_inst, OF at_name_inst, symmetric, where pi="[(x, y)]"])
(simp add: fresh_left calc_atm)
with ‹y ∈ supp N'› ‹y ♯ N› have False by(simp add: fresh_def)
thus ?case by simp
next
case(cRes P')
from ‹Ψ ⊳ M⟨N⟩.P ⟼α ≺ P'› show ?case
proof(induct rule: outputCases)
case(cOutput K)
from ‹Ψ ⊢ M ↔ K› have "Ψ ⊳ M⟨N⟩.(⦇νx⦈P) ⟼K⟨N⟩ ≺ ⦇νx⦈P"
by(rule Output)
moreover have "(Ψ, ⦇νx⦈P, ⦇νx⦈P) ∈ Rel" by(rule C1)
ultimately show ?case by force
qed
qed
qed
qed
lemma casePushResLeft:
fixes Ψ :: 'b
and x :: name
and Cs :: "('c × ('a, 'b, 'c) psi) list"
assumes "eqvt Rel"
and "x ♯ Ψ"
and "x ♯ map fst Cs"
and C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"
shows "Ψ ⊳ ⦇νx⦈(Cases Cs) ↝[Rel] Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
proof -
note ‹eqvt Rel› ‹x ♯ Ψ›
moreover have "x ♯ ⦇νx⦈(Cases Cs)" by(simp add: abs_fresh)
moreover from ‹x ♯ map fst Cs› have "x ♯ Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
by(induct Cs) (auto simp add: abs_fresh)
ultimately show ?thesis
proof(induct rule: simIFresh[of _ _ _ _ _ Cs])
case(cSim α P'')
from ‹Ψ ⊳ Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs) ⟼α ≺ P''›
show ?case
proof(induct rule: caseCases)
case(cCase φ P')
from ‹(φ, P') mem (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)›
obtain P where "(φ, P) mem Cs" and "P' = ⦇νx⦈P"
by(induct Cs) auto
from ‹guarded P'› ‹P' = ⦇νx⦈P› have "guarded P" by simp
from ‹Ψ ⊳ P' ⟼α ≺ P''› ‹P' = ⦇νx⦈P› have "Ψ ⊳ ⦇νx⦈P ⟼α ≺ P''"
by simp
moreover note ‹x ♯ Ψ› ‹x ♯ α› ‹x ♯ P''› ‹bn α ♯* Ψ›
moreover from ‹bn α ♯* Cs› ‹(φ, P) mem Cs›
have "bn α ♯* P" by(auto dest: memFreshChain)
ultimately show ?case using ‹bn α ♯* subject α› ‹x ♯ α› ‹bn α ♯* Cs›
proof(induct rule: resCases)
case(cOpen M xvec1 xvec2 y N P')
from ‹x ♯ M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩› have "x ♯ xvec1" and "x ♯ xvec2" and "x ♯ M" by simp+
from ‹bn(M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩) ♯* Cs› have "y ♯ Cs" by simp
from ‹Ψ ⊳ P ⟼M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')› ‹(φ, P) mem Cs› ‹Ψ ⊢ φ› ‹guarded P›
have "Ψ ⊳ Cases Cs ⟼M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')" by(rule Case)
hence "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ (Cases Cs)) ⟼([(x, y)] ∙ (M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')))"
by(rule semantics.eqvt)
with ‹x ♯ Ψ› ‹x ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2› ‹y ♯ Ψ› ‹y ♯ M› ‹x ♯ xvec1› ‹x ♯ xvec2›
have "Ψ ⊳ ([(x, y)] ∙ (Cases Cs)) ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ P'" by(simp add: eqvts)
hence "Ψ ⊳ ⦇νy⦈([(x, y)] ∙ (Cases Cs)) ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ P'" using ‹y ∈ supp N› ‹y ♯ Ψ› ‹y ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2›
by(rule Open)
hence "Ψ ⊳ ⦇νx⦈(Cases Cs) ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ P'" using ‹y ♯ Cs›
by(simp add: alphaRes)
moreover have "(Ψ, P', P') ∈ Rel" by(rule C1)
ultimately show ?case by blast
next
case(cRes P')
from ‹Ψ ⊳ P ⟼α ≺ P'› ‹(φ, P) mem Cs› ‹Ψ ⊢ φ› ‹guarded P›
have "Ψ ⊳ Cases Cs ⟼α ≺ P'" by(rule Case)
hence "Ψ ⊳ ⦇νx⦈(Cases Cs) ⟼α ≺ ⦇νx⦈P'" using ‹x ♯ Ψ› ‹x ♯ α›
by(rule Scope)
moreover have "(Ψ, ⦇νx⦈P', ⦇νx⦈P') ∈ Rel" by(rule C1)
ultimately show ?case by blast
qed
qed
qed
qed
lemma casePushResRight:
fixes Ψ :: 'b
and x :: name
and Cs :: "('c × ('a, 'b, 'c) psi) list"
assumes "eqvt Rel"
and "x ♯ Ψ"
and "x ♯ map fst Cs"
and C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"
shows "Ψ ⊳ Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs) ↝[Rel] ⦇νx⦈(Cases Cs)"
proof -
note ‹eqvt Rel› ‹x ♯ Ψ›
moreover from ‹x ♯ map fst Cs› have "x ♯ Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
by(induct Cs) (auto simp add: abs_fresh)
moreover have "x ♯ ⦇νx⦈(Cases Cs)" by(simp add: abs_fresh)
ultimately show ?thesis
proof(induct rule: simIFresh[of _ _ _ _ _ Cs])
case(cSim α P'')
note ‹Ψ ⊳ ⦇νx⦈(Cases Cs) ⟼α ≺ P''› ‹x ♯ Ψ› ‹x ♯ α› ‹x ♯ P''› ‹bn α ♯* Ψ›
moreover from ‹bn α ♯* ⦇νx⦈(Cases Cs)› ‹x ♯ α› have "bn α ♯* (Cases Cs)" by simp
ultimately show ?case using ‹bn α ♯* subject α› ‹x ♯ α› ‹bn α ♯* Cs›
proof(induct rule: resCases)
case(cOpen M xvec1 xvec2 y N P')
from ‹x ♯ M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩› have "x ♯ xvec1" and "x ♯ xvec2" and "x ♯ M" by simp+
from ‹bn(M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩) ♯* Cs› have "y ♯ Cs" by simp
from ‹Ψ ⊳ Cases Cs ⟼M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')›
show ?case
proof(induct rule: caseCases)
case(cCase φ P)
from ‹Ψ ⊳ P ⟼M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')›
have "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ P) ⟼([(x, y)] ∙ (M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')))"
by(rule semantics.eqvt)
with ‹x ♯ Ψ› ‹x ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2› ‹y ♯ Ψ› ‹y ♯ M› ‹x ♯ xvec1› ‹x ♯ xvec2›
have "Ψ ⊳ ([(x, y)] ∙ P) ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ P'" by(simp add: eqvts)
hence "Ψ ⊳ ⦇νy⦈([(x, y)] ∙ P) ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ P'" using ‹y ∈ supp N› ‹y ♯ Ψ› ‹y ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2›
by(rule Open)
hence "Ψ ⊳ ⦇νx⦈P ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ P'" using ‹y ♯ Cs› ‹(φ, P) mem Cs›
by(subst alphaRes, auto dest: memFresh)
moreover from ‹(φ, P) mem Cs› have "(φ, ⦇νx⦈P) mem (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
by(induct Cs) auto
moreover note ‹Ψ ⊢ φ›
moreover from ‹guarded P› have "guarded(⦇νx⦈P)" by simp
ultimately have "Ψ ⊳ (Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)) ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ P'"
by(rule Case)
moreover have "(Ψ, P', P') ∈ Rel" by(rule C1)
ultimately show ?case by blast
qed
next
case(cRes P')
from ‹Ψ ⊳ Cases Cs ⟼α ≺ P'›
show ?case
proof(induct rule: caseCases)
case(cCase φ P)
from ‹Ψ ⊳ P ⟼α ≺ P'› ‹x ♯ Ψ› ‹x ♯ α›
have "Ψ ⊳ ⦇νx⦈P ⟼α ≺ ⦇νx⦈P'" by(rule Scope)
moreover from ‹(φ, P) mem Cs› have "(φ, ⦇νx⦈P) mem (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
by(induct Cs) auto
moreover note ‹Ψ ⊢ φ›
moreover from ‹guarded P› have "guarded(⦇νx⦈P)" by simp
ultimately have "Ψ ⊳ (Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)) ⟼α ≺ ⦇νx⦈P'"
by(rule Case)
moreover have "(Ψ, ⦇νx⦈P', ⦇νx⦈P') ∈ Rel" by(rule C1)
ultimately show ?case by blast
qed
qed
qed
qed
lemma resInputCases[consumes 5, case_names cRes]:
fixes Ψ :: 'b
and x :: name
and P :: "('a, 'b, 'c) psi"
and M :: 'a
and N :: 'a
and P' :: "('a, 'b, 'c) psi"
and C :: "'d::fs_name"
assumes Trans: "Ψ ⊳ ⦇νx⦈P ⟼M⦇N⦈ ≺ P'"
and "x ♯ Ψ"
and "x ♯ M"
and "x ♯ N"
and "x ♯ P'"
and rScope: "⋀P'. ⟦