Theory Weak_Cong_Sim_Pres
theory Weak_Cong_Sim_Pres
imports Weak_Sim_Pres Weak_Cong_Simulation
begin
context env begin
lemma caseWeakSimPres:
fixes Ψ :: 'b
and CsP :: "('c × ('a, 'b, 'c) psi) list"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and CsQ :: "('c × ('a, 'b, 'c) psi) list"
and M :: 'a
and N :: 'a
assumes PRelQ: "⋀φ Q. (φ, Q) mem CsQ ⟹ ∃P. (φ, P) mem CsP ∧ guarded P ∧ Eq Ψ P Q"
and Sim: "⋀Ψ' P Q. (Ψ', P, Q) ∈ Rel ⟹ Ψ' ⊳ P ↝<Rel> Q"
and EqRel: "⋀Ψ' P Q. Eq Ψ' P Q ⟹ (Ψ', P, Q) ∈ Rel"
and EqSim: "⋀Ψ' P Q. Eq Ψ' P Q ⟹ Ψ' ⊳ P ↝«Rel» Q"
shows "Ψ ⊳ Cases CsP ↝<Rel> Cases CsQ"
proof(induct rule: weakSimI2)
case(cAct Ψ' α Q')
from ‹bn α ♯* (Cases CsP)› have "bn α ♯* CsP" by auto
from ‹Ψ ⊳ Cases CsQ ⟼α ≺ Q'›
show ?case
proof(induct rule: caseCases)
case(cCase φ Q)
from ‹(φ, Q) mem CsQ› obtain P where "(φ, P) mem CsP" and "guarded P" and "Eq Ψ P Q"
by(metis PRelQ)
from ‹Eq Ψ P Q› have "Ψ ⊳ P ↝<Rel> Q" by(metis EqRel Sim)
moreover note ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹bn α ♯* Ψ›
moreover from ‹bn α ♯* CsP› ‹(φ, P) mem CsP› have "bn α ♯* P" by(auto dest: memFreshChain)
ultimately obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹α ≺ P''"
and P''Chain: "Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ ⊗ Ψ', P', Q') ∈ Rel"
using ‹α ≠ τ›
by(blast dest: weakSimE)
note PTrans ‹(φ, P) mem CsP› ‹Ψ ⊢ φ› ‹guarded P›
moreover from ‹guarded Q› have "insertAssertion (extractFrame Q) Ψ ≃⇩F ⟨ε, Ψ ⊗ 𝟭⟩"
by(rule insertGuardedAssertion)
hence "insertAssertion (extractFrame(Cases CsQ)) Ψ ↪⇩F insertAssertion (extractFrame Q) Ψ"
by(auto simp add: FrameStatEq_def)
moreover from Identity have "insertAssertion (extractFrame(Cases CsQ)) Ψ ↪⇩F ⟨ε, Ψ⟩"
by(auto simp add: AssertionStatEq_def)
ultimately have "Ψ : (Cases CsQ) ⊳ Cases CsP ⟹α ≺ P''"
by(rule weakCase)
with P''Chain P'RelQ' show ?case by blast
qed
next
case(cTau Q')
from ‹Ψ ⊳ Cases CsQ ⟼τ ≺ Q'› show ?case
proof(induct rule: caseCases)
case(cCase φ Q)
from ‹(φ, Q) mem CsQ› obtain P where "(φ, P) mem CsP" and "guarded P" and "Eq Ψ P Q"
by(metis PRelQ)
from ‹Eq Ψ P Q› ‹Ψ ⊳ Q ⟼τ ≺ Q'›
obtain P' where PChain: "Ψ ⊳ P ⟹⇩τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
by(blast dest: EqSim weakCongSimE)
from PChain ‹(φ, P) mem CsP› ‹Ψ ⊢ φ› ‹guarded P› have "Ψ ⊳ Cases CsP ⟹⇩τ P'"
by(rule tauStepChainCase)
hence "Ψ ⊳ Cases CsP ⟹⇧^⇩τ P'" by(simp add: trancl_into_rtrancl)
with P'RelQ' show ?case by blast
qed
qed
lemma weakCongSimCasePres:
fixes Ψ :: 'b
and CsP :: "('c × ('a, 'b, 'c) psi) list"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and CsQ :: "('c × ('a, 'b, 'c) psi) list"
and M :: 'a
and N :: 'a
assumes PRelQ: "⋀φ Q. (φ, Q) mem CsQ ⟹ ∃P. (φ, P) mem CsP ∧ guarded P ∧ Eq Ψ P Q"
and EqSim: "⋀Ψ' P Q. Eq Ψ' P Q ⟹ Ψ' ⊳ P ↝«Rel» Q"
shows "Ψ ⊳ Cases CsP ↝«Rel» Cases CsQ"
proof(induct rule: weakCongSimI)
case(cTau Q')
from ‹Ψ ⊳ Cases CsQ ⟼τ ≺ Q'› show ?case
proof(induct rule: caseCases)
case(cCase φ Q)
from ‹(φ, Q) mem CsQ› obtain P where "(φ, P) mem CsP" and "guarded P" and "Eq Ψ P Q"
by(metis PRelQ)
from ‹Eq Ψ P Q› ‹Ψ ⊳ Q ⟼τ ≺ Q'›
obtain P' where PChain: "Ψ ⊳ P ⟹⇩τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
by(blast dest: EqSim weakCongSimE)
from PChain ‹(φ, P) mem CsP› ‹Ψ ⊢ φ› ‹guarded P› have "Ψ ⊳ Cases CsP ⟹⇩τ P'"
by(rule tauStepChainCase)
with P'RelQ' show ?case by blast
qed
qed
lemma weakCongSimResPres:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and x :: name
and Rel' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
assumes PSimQ: "Ψ ⊳ P ↝«Rel» Q"
and "eqvt Rel'"
and "x ♯ Ψ"
and "Rel ⊆ Rel'"
and C1: "⋀Ψ' R S x. ⟦(Ψ', R, S) ∈ Rel; x ♯ Ψ'⟧ ⟹ (Ψ', ⦇νx⦈R, ⦇νx⦈S) ∈ Rel'"
shows "Ψ ⊳ ⦇νx⦈P ↝«Rel'» ⦇νx⦈Q"
proof(induct rule: weakCongSimI)
case(cTau Q')
from ‹Ψ ⊳ ⦇νx⦈Q ⟼τ ≺ Q'› have "x ♯ Q'" by(auto dest: tauFreshDerivative simp add: abs_fresh)
with ‹Ψ ⊳ ⦇νx⦈Q ⟼τ ≺ Q'› ‹x ♯ Ψ› show ?case
proof(induct rule: resTauCases)
case(cRes Q')
from PSimQ ‹Ψ ⊳ Q ⟼τ ≺ Q'› obtain P' where PChain: "Ψ ⊳ P ⟹⇩τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
by(blast dest: weakCongSimE)
from PChain ‹x ♯ Ψ› have "Ψ ⊳ ⦇νx⦈P ⟹⇩τ ⦇νx⦈P'" by(rule tauStepChainResPres)
moreover from P'RelQ' ‹x ♯ Ψ› have "(Ψ, ⦇νx⦈P', ⦇νx⦈Q') ∈ Rel'" by(rule C1)
ultimately show ?case by blast
qed
qed
lemma weakCongSimResChainPres:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Q :: "('a, 'b, 'c) psi"
and xvec :: "name list"
assumes PSimQ: "Ψ ⊳ P ↝«Rel» Q"
and "eqvt Rel"
and "xvec ♯* Ψ"
and C1: "⋀Ψ' R S xvec. ⟦(Ψ', R, S) ∈ Rel; xvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*xvec⦈R, ⦇ν*xvec⦈S) ∈ Rel"
shows "Ψ ⊳ ⦇ν*xvec⦈P ↝«Rel» ⦇ν*xvec⦈Q"
using ‹xvec ♯* Ψ›
proof(induct xvec)
case Nil
from PSimQ show ?case by simp
next
case(Cons x xvec)
from ‹(x#xvec) ♯* Ψ› have "x ♯ Ψ" and "xvec ♯* Ψ" by simp+
from ‹xvec ♯* Ψ ⟹ Ψ ⊳ ⦇ν*xvec⦈P ↝«Rel» ⦇ν*xvec⦈Q› ‹xvec ♯* Ψ›
have "Ψ ⊳ ⦇ν*xvec⦈P ↝«Rel» ⦇ν*xvec⦈Q" by simp
moreover note ‹eqvt Rel› ‹x ♯ Ψ›
moreover have "Rel ⊆ Rel" by simp
moreover have "⋀Ψ P Q x. ⟦(Ψ, P, Q) ∈ Rel; x ♯ Ψ⟧ ⟹ (Ψ, ⦇ν*[x]⦈P, ⦇ν*[x]⦈Q) ∈ Rel"
by(rule_tac xvec="[x]" in C1) auto
hence "⋀Ψ P Q x. ⟦(Ψ, P, Q) ∈ Rel; x ♯ Ψ⟧ ⟹ (Ψ, ⦇νx⦈P, ⦇νx⦈Q) ∈ Rel"
by simp
ultimately have "Ψ ⊳ ⦇νx⦈(⦇ν*xvec⦈P) ↝«Rel» ⦇νx⦈(⦇ν*xvec⦈Q)"
by(rule weakCongSimResPres)
thus ?case by simp
qed
lemma weakCongSimParPres:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
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 PSimQ: "⋀Ψ'. Ψ' ⊳ P ↝«Rel» Q"
and PSimQ': "⋀Ψ'. Ψ' ⊳ P ↝<Rel> Q"
and StatImp: "⋀Ψ'. Ψ' ⊳ Q ⪅<Rel> P"
and "eqvt Rel"
and "eqvt Rel'"
and Sym: "⋀Ψ' S T. ⟦(Ψ', S, T) ∈ Rel⟧ ⟹ (Ψ', T, S) ∈ Rel"
and Ext: "⋀Ψ' S T Ψ''. ⟦(Ψ', S, T) ∈ Rel⟧ ⟹ (Ψ' ⊗ Ψ'', S, T) ∈ Rel"
and C1: "⋀Ψ' S T A⇩U Ψ⇩U U. ⟦(Ψ' ⊗ Ψ⇩U, S, T) ∈ Rel; extractFrame U = ⟨A⇩U, Ψ⇩U⟩; A⇩U ♯* Ψ'; A⇩U ♯* S; A⇩U ♯* T⟧ ⟹ (Ψ', S ∥ U, T ∥ U) ∈ Rel'"
and C2: "⋀Ψ' S T xvec. ⟦(Ψ', S, T) ∈ Rel'; xvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*xvec⦈S, ⦇ν*xvec⦈T) ∈ Rel'"
and C3: "⋀Ψ' S T Ψ''. ⟦(Ψ', S, T) ∈ Rel; Ψ' ≃ Ψ''⟧ ⟹ (Ψ'', S, T) ∈ Rel"
shows "Ψ ⊳ P ∥ R ↝«Rel'» Q ∥ R"
proof(induct rule: weakCongSimI)
case(cTau QR)
from ‹Ψ ⊳ Q ∥ R ⟼τ ≺ QR› show ?case
proof(induct rule: parTauCases[where C="(P, R)"])
case(cPar1 Q' A⇩R Ψ⇩R)
from ‹A⇩R ♯* (P, R)› have "A⇩R ♯* P"
by simp+
have FrR: " extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
with ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› have "Ψ ⊗ Ψ⇩R ⊳ P ↝«Rel» Q"
by(rule_tac PSimQ)
moreover have QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼τ ≺ Q'" by fact
ultimately obtain P' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇩τ P'" and P'RelQ': "(Ψ ⊗ Ψ⇩R, P', Q') ∈ Rel"
by(rule weakCongSimE)
from PChain QTrans ‹A⇩R ♯* P› ‹A⇩R ♯* Q› have "A⇩R ♯* P'" and "A⇩R ♯* Q'"
by(force dest: freeFreshChainDerivative tauStepChainFreshChain)+
from PChain FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› have "Ψ ⊳ P ∥ R ⟹⇩τ (P' ∥ R)"
by(rule tauStepChainPar1)
moreover from P'RelQ' FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P'› ‹A⇩R ♯* Q'› have "(Ψ, P' ∥ R, Q' ∥ R) ∈ Rel'" by(rule C1)
ultimately show ?case by blast
next
case(cPar2 R' A⇩Q Ψ⇩Q)
from ‹A⇩Q ♯* (P, R)› have "A⇩Q ♯* P" and "A⇩Q ♯* R" by simp+
obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* (Ψ, A⇩Q, Ψ⇩Q, R)"
by(rule freshFrame)
hence "A⇩P ♯* Ψ" and "A⇩P ♯* A⇩Q" and "A⇩P ♯* Ψ⇩Q" and "A⇩P ♯* R"
by simp+
have FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
from ‹A⇩Q ♯* P› FrP ‹A⇩P ♯* A⇩Q› have "A⇩Q ♯* Ψ⇩P"
by(drule_tac extractFrameFreshChain) auto
obtain A⇩R Ψ⇩R where FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" and "A⇩R ♯* (Ψ, P, Q, A⇩Q, A⇩P, Ψ⇩Q, Ψ⇩P, R)" and "distinct A⇩R"
by(rule freshFrame)
then have "A⇩R ♯* Ψ" and "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* A⇩Q" and "A⇩R ♯* A⇩P" and "A⇩R ♯* Ψ⇩Q" and "A⇩R ♯* Ψ⇩P"
and "A⇩R ♯* R"
by simp+
from ‹A⇩Q ♯* R› FrR ‹A⇩R ♯* A⇩Q› have "A⇩Q ♯* Ψ⇩R" by(drule_tac extractFrameFreshChain) auto
from ‹A⇩P ♯* R› ‹A⇩R ♯* A⇩P› FrR have "A⇩P ♯* Ψ⇩R" by(drule_tac extractFrameFreshChain) auto
moreover from ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼τ ≺ R'› FrR ‹distinct A⇩R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* R›
obtain Ψ' A⇩R' Ψ⇩R' where "Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'" and FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩"
and "A⇩R' ♯* Ψ" and "A⇩R' ♯* P" and "A⇩R' ♯* Q"
by(rule_tac C="(Ψ, P, Q, R)" in expandTauFrame) (assumption | simp)+
from FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q›
obtain P' P'' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇧^⇩τ P'"
and QimpP': "insertAssertion(extractFrame Q) (Ψ ⊗ Ψ⇩R) ↪⇩F insertAssertion(extractFrame P') (Ψ ⊗ Ψ⇩R)"
and P'Chain: "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P' ⟹⇧^⇩τ P''"
and P'RelQ: "((Ψ ⊗ Ψ⇩R) ⊗ Ψ', P'', Q) ∈ Rel"
by(metis StatImp weakStatImp_def Sym)
obtain A⇩P' Ψ⇩P' where FrP': "extractFrame P' = ⟨A⇩P', Ψ⇩P'⟩" and "A⇩P' ♯* Ψ" and "A⇩P' ♯* Ψ⇩R" and "A⇩P' ♯* Ψ⇩Q"
and "A⇩P' ♯* A⇩Q" and "A⇩P' ♯* R" and "A⇩P' ♯* A⇩R"
by(rule_tac C="(Ψ, Ψ⇩R, Ψ⇩Q, A⇩Q, R, A⇩R)" in freshFrame) auto
from PChain P'Chain ‹A⇩R ♯* P› ‹A⇩Q ♯* P› ‹A⇩R' ♯* P› have "A⇩Q ♯* P'" and "A⇩R ♯* P'" and "A⇩R' ♯* P'" and "A⇩R' ♯* P''"
by(force intro: tauChainFreshChain)+
from ‹A⇩R ♯* P'› ‹A⇩P' ♯* A⇩R› ‹A⇩Q ♯* P'› ‹A⇩P' ♯* A⇩Q› FrP' have "A⇩Q ♯* Ψ⇩P'" and "A⇩R ♯* Ψ⇩P'"
by(force dest: extractFrameFreshChain)+
from PChain FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ P' ∥ R" by(rule tauChainPar1)
moreover have RTrans: "Ψ ⊗ Ψ⇩P' ⊳ R ⟼τ ≺ R'"
proof -
have "Ψ ⊗ Ψ⇩Q ⊳ R ⟼τ ≺ R'" by fact
moreover have "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P', (Ψ ⊗ Ψ⇩P') ⊗ Ψ⇩R⟩"
proof -
have "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩"
by(metis frameIntAssociativity Commutativity FrameStatEqTrans frameIntCompositionSym FrameStatEqSym)
moreover with FrP' FrQ QimpP' ‹A⇩P' ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩P' ♯* Ψ⇩R› ‹A⇩Q ♯* Ψ⇩R›
have "⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩ ↪⇩F ⟨A⇩P', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'⟩" using freshCompChain
by simp
moreover have "⟨A⇩P', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'⟩ ≃⇩F ⟨A⇩P', (Ψ ⊗ Ψ⇩P') ⊗ Ψ⇩R⟩"
by(metis frameIntAssociativity Commutativity FrameStatEqTrans frameIntCompositionSym frameIntAssociativity[THEN FrameStatEqSym])
ultimately show ?thesis
by(rule FrameStatEqImpCompose)
qed
ultimately show ?thesis
using ‹A⇩P' ♯* Ψ› ‹A⇩P' ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Ψ⇩P'› ‹A⇩P' ♯* R› ‹A⇩Q ♯* R›
‹A⇩P' ♯* A⇩R› ‹A⇩R ♯* A⇩Q› ‹A⇩R ♯* Ψ⇩P'› ‹A⇩R ♯* Ψ⇩Q› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ⇩P'› ‹A⇩Q ♯* Ψ⇩P'› FrR ‹distinct A⇩R›
by(force intro: transferTauFrame)
qed
hence "Ψ ⊳ P' ∥ R ⟼τ ≺ (P' ∥ R')" using FrP' ‹A⇩P' ♯* Ψ› ‹A⇩P' ♯* R›
by(rule_tac Par2) auto
moreover from P'Chain have "Ψ ⊗ Ψ⇩R ⊗ Ψ' ⊳ P' ⟹⇧^⇩τ P''"
by(metis tauChainStatEq Associativity)
with ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'› have "Ψ ⊗ Ψ⇩R' ⊳ P' ⟹⇧^⇩τ P''"
by(rule_tac tauChainStatEq, auto) (metis compositionSym)
hence "Ψ ⊳ P' ∥ R' ⟹⇧^⇩τ P'' ∥ R'" using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P'› by(rule_tac tauChainPar1)
ultimately have "Ψ ⊳ P ∥ R ⟹⇩τ (P'' ∥ R')"
by(drule_tac tauActTauStepChain) auto
moreover from P'RelQ ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ⇩R', P'', Q) ∈ Rel" by(blast intro: C3 Associativity compositionSym)
with FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P''› ‹A⇩R' ♯* Q› have "(Ψ, P'' ∥ R', Q ∥ R') ∈ Rel'" by(rule_tac C1)
ultimately show ?case by blast
next
case(cComm1 Ψ⇩R M N Q' A⇩Q Ψ⇩Q K xvec R' A⇩R)
have FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
from ‹A⇩Q ♯* (P, R)› have "A⇩Q ♯* P" and "A⇩Q ♯* R" by simp+
have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
from ‹A⇩R ♯* (P, R)› have "A⇩R ♯* P" and "A⇩R ♯* R" by simp+
from ‹xvec ♯* (P, R)› have "xvec ♯* P" and "xvec ♯* R" by simp+
have QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼M⦇N⦈ ≺ Q'" and RTrans: "Ψ ⊗ Ψ⇩Q ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'"
and MeqK: "Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R ⊢ M ↔K" by fact+
from RTrans FrR ‹distinct A⇩R› ‹A⇩R ♯* R› ‹A⇩R ♯* xvec› ‹xvec ♯* R› ‹xvec ♯* Q› ‹xvec ♯* Ψ› ‹xvec ♯* Ψ⇩Q› ‹A⇩R ♯* Q›
‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ⇩Q› ‹xvec ♯* K› ‹A⇩R ♯* K› ‹A⇩R ♯* R› ‹xvec ♯* R› ‹A⇩R ♯* P› ‹xvec ♯* P›
‹A⇩Q ♯* A⇩R› ‹A⇩Q ♯* xvec› ‹A⇩R ♯* K› ‹A⇩R ♯* N› ‹xvec ♯* K› ‹distinct xvec›
obtain p Ψ' A⇩R' Ψ⇩R' where S: "set p ⊆ set xvec × set(p ∙ xvec)" and FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩"
and "(p ∙ Ψ⇩R) ⊗ Ψ' ≃ Ψ⇩R'" and "A⇩R' ♯* Q" and "A⇩R' ♯* Ψ" and "(p ∙ xvec) ♯* Ψ"
and "(p ∙ xvec) ♯* Q" and "(p ∙ xvec) ♯* Ψ⇩Q" and "(p ∙ xvec) ♯* K" and "(p ∙ xvec) ♯* R"
and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* A⇩Q" and "A⇩R' ♯* P" and "A⇩R' ♯* N"
by(rule_tac C="(Ψ, Q, Ψ⇩Q, K, R, P, A⇩Q)" and C'="(Ψ, Q, Ψ⇩Q, K, R, P, A⇩Q)" in expandFrame) (assumption | simp)+
from ‹A⇩R ♯* Ψ› have "(p ∙ A⇩R) ♯* (p ∙ Ψ)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S have "(p ∙ A⇩R) ♯* Ψ" by simp
from ‹A⇩R ♯* P› have "(p ∙ A⇩R) ♯* (p ∙ P)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› S have "(p ∙ A⇩R) ♯* P" by simp
from ‹A⇩R ♯* Q› have "(p ∙ A⇩R) ♯* (p ∙ Q)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› S have "(p ∙ A⇩R) ♯* Q" by simp
from ‹A⇩R ♯* R› have "(p ∙ A⇩R) ♯* (p ∙ R)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹xvec ♯* R› ‹(p ∙ xvec) ♯* R› S have "(p ∙ A⇩R) ♯* R" by simp
from ‹A⇩R ♯* K› have "(p ∙ A⇩R) ♯* (p ∙ K)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
with ‹xvec ♯* K› ‹(p ∙ xvec) ♯* K› S have "(p ∙ A⇩R) ♯* K" by simp
from ‹A⇩Q ♯* xvec› ‹(p ∙ xvec) ♯* A⇩Q› ‹A⇩Q ♯* M› S have "A⇩Q ♯* (p ∙ M)" by(simp add: freshChainSimps)
from ‹A⇩Q ♯* xvec› ‹(p ∙ xvec) ♯* A⇩Q› ‹A⇩Q ♯* A⇩R› S have "A⇩Q ♯* (p ∙ A⇩R)" by(simp add: freshChainSimps)
from QTrans S ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› have "(p ∙ (Ψ ⊗ Ψ⇩R)) ⊳ Q ⟼ (p ∙ M)⦇N⦈ ≺ Q'"
by(rule_tac inputPermFrameSubject) (assumption | auto simp add: fresh_star_def)+
with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S have QTrans: "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊳ Q ⟼ (p ∙ M)⦇N⦈ ≺ Q'"
by(simp add: eqvts)
from FrR have "(p ∙ extractFrame R) = p ∙ ⟨A⇩R, Ψ⇩R⟩" by simp
with ‹xvec ♯* R› ‹(p ∙ xvec) ♯* R› S have FrR: "extractFrame R = ⟨(p ∙ A⇩R), (p ∙ Ψ⇩R)⟩"
by(simp add: eqvts)
from MeqK have "(p ∙ (Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R)) ⊢ (p ∙ M) ↔ (p ∙ K)" by(rule chanEqClosed)
with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* Ψ⇩Q› ‹(p ∙ xvec) ♯* Ψ⇩Q› ‹xvec ♯* K› ‹(p ∙ xvec) ♯* K› S
have MeqK: "Ψ ⊗ Ψ⇩Q ⊗ (p ∙ Ψ⇩R) ⊢ (p ∙ M) ↔ K" by(simp add: eqvts)
have "Ψ ⊗ (p ∙ Ψ⇩R) ⊳ P ↝<Rel> Q" by(rule PSimQ')
with QTrans obtain P' P'' where PTrans: "Ψ ⊗ (p ∙ Ψ⇩R) : Q ⊳ P ⟹(p ∙ M)⦇N⦈ ≺ P''"
and P''Chain: "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'"
and P'RelQ': "((Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ', P', Q') ∈ Rel"
by(fastforce dest: weakSimE)
from PTrans QTrans ‹A⇩R' ♯* P› ‹A⇩R' ♯* Q› ‹A⇩R' ♯* N› have "A⇩R' ♯* P''" and "A⇩R' ♯* Q'"
by(blast dest: weakInputFreshChainDerivative inputFreshChainDerivative)+
from PTrans obtain P''' where PChain: "Ψ ⊗ (p ∙ Ψ⇩R) ⊳ P ⟹⇧^⇩τ P'''"
and QimpP''': "insertAssertion (extractFrame Q) (Ψ ⊗ (p ∙ Ψ⇩R)) ↪⇩F insertAssertion (extractFrame P''') (Ψ ⊗ (p ∙ Ψ⇩R))"
and P'''Trans: "Ψ ⊗ (p ∙ Ψ⇩R) ⊳ P''' ⟼(p ∙ M)⦇N⦈ ≺ P''"
by(rule weakTransitionE)
from PChain ‹xvec ♯* P› ‹(p ∙ A⇩R) ♯* P› ‹A⇩R' ♯* P› have "xvec ♯* P'''" and "(p ∙ A⇩R) ♯* P'''" and "A⇩R' ♯* P'''"
by(force intro: tauChainFreshChain)+
from P'''Trans ‹A⇩R' ♯* P'''› ‹A⇩R' ♯* N› have "A⇩R' ♯* P''" by(force dest: inputFreshChainDerivative)
obtain A⇩P''' Ψ⇩P''' where FrP''': "extractFrame P''' = ⟨A⇩P''', Ψ⇩P'''⟩" and "A⇩P''' ♯* (Ψ, A⇩Q, Ψ⇩Q, p ∙ A⇩R, p ∙ Ψ⇩R, p ∙ M, N, K, R, P''', xvec)" and "distinct A⇩P'''"
by(rule freshFrame)
hence "A⇩P''' ♯* Ψ" and "A⇩P''' ♯* A⇩Q" and "A⇩P''' ♯* Ψ⇩Q" and "A⇩P''' ♯* (p ∙ M)" and "A⇩P''' ♯* R"
and "A⇩P''' ♯* N" and "A⇩P''' ♯* K" and "A⇩P''' ♯* (p ∙ A⇩R)" and "A⇩P''' ♯* P'''" and "A⇩P''' ♯* xvec" and "A⇩P''' ♯* (p ∙ Ψ⇩R)"
by simp+
have "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ (p ∙ Ψ⇩R)⟩ ≃⇩F ⟨A⇩Q, (Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ⇩Q⟩"
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
moreover with QimpP''' FrP''' FrQ ‹A⇩P''' ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩P''' ♯* (p ∙ Ψ⇩R)› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩Q ♯* xvec› ‹(p ∙ xvec) ♯* A⇩Q› S
have "⟨A⇩Q, (Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ⇩Q⟩ ↪⇩F ⟨A⇩P''', (Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ⇩P'''⟩" using freshCompChain
by(simp add: freshChainSimps)
moreover have "⟨A⇩P''', (Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ⇩P'''⟩ ≃⇩F ⟨A⇩P''', (Ψ ⊗ Ψ⇩P''') ⊗ (p ∙ Ψ⇩R)⟩"
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
ultimately have QImpP''': "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ (p ∙ Ψ⇩R)⟩ ↪⇩F ⟨A⇩P''', (Ψ ⊗ Ψ⇩P''') ⊗ (p ∙ Ψ⇩R)⟩"
by(rule FrameStatEqImpCompose)
from PChain FrR ‹(p ∙ A⇩R) ♯* Ψ› ‹(p ∙ A⇩R) ♯* P› have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ P''' ∥ R" by(rule tauChainPar1)
moreover from RTrans FrR P'''Trans MeqK QImpP''' FrP''' FrQ ‹distinct A⇩P'''› ‹distinct A⇩R› ‹A⇩P''' ♯* (p ∙ A⇩R)› ‹A⇩Q ♯* (p ∙ A⇩R)›
‹(p ∙ A⇩R) ♯* Ψ› ‹(p ∙ A⇩R) ♯* P'''› ‹(p ∙ A⇩R) ♯* Q› ‹(p ∙ A⇩R) ♯* R› ‹(p ∙ A⇩R) ♯* K› ‹A⇩P''' ♯* Ψ› ‹A⇩P''' ♯* R›
‹A⇩P''' ♯* P'''› ‹A⇩P''' ♯* (p ∙ M)› ‹A⇩Q ♯* R› ‹A⇩Q ♯* (p ∙ M)›
obtain K' where "Ψ ⊗ Ψ⇩P''' ⊳ R ⟼K'⦇ν*xvec⦈⟨N⟩ ≺ R'" and "Ψ ⊗ Ψ⇩P''' ⊗ (p ∙ Ψ⇩R) ⊢ (p ∙ M) ↔ K'" and "(p ∙ A⇩R) ♯* K'"
by(rule_tac comm1Aux) (assumption | simp)+
with P'''Trans FrP''' have "Ψ ⊳ P''' ∥ R ⟼τ ≺ ⦇ν*xvec⦈(P'' ∥ R')" using FrR ‹(p ∙ A⇩R) ♯* Ψ› ‹(p ∙ A⇩R) ♯* P'''› ‹(p ∙ A⇩R) ♯* R›
‹xvec ♯* P'''› ‹A⇩P''' ♯* Ψ› ‹A⇩P''' ♯* P'''› ‹A⇩P''' ♯* R› ‹A⇩P''' ♯* (p ∙ M)› ‹(p ∙ A⇩R) ♯* K'› ‹A⇩P''' ♯* (p ∙ A⇩R)›
by(rule_tac Comm1)
moreover from P''Chain ‹A⇩R' ♯* P''› have "A⇩R' ♯* P'" by(rule tauChainFreshChain)
from ‹(p ∙ Ψ⇩R) ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ' ≃ Ψ ⊗ Ψ⇩R'"
by(metis Associativity AssertionStatEqTrans AssertionStatEqSym compositionSym)
with P''Chain have "Ψ ⊗ Ψ⇩R' ⊳ P'' ⟹⇧^⇩τ P'" by(rule tauChainStatEq)
hence "Ψ ⊳ P'' ∥ R' ⟹⇧^⇩τ P' ∥ R'" using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P''› by(rule tauChainPar1)
hence "Ψ ⊳ ⦇ν*xvec⦈(P'' ∥ R') ⟹⇧^⇩τ ⦇ν*xvec⦈(P' ∥ R')" using ‹xvec ♯* Ψ› by(rule tauChainResChainPres)
ultimately have "Ψ ⊳ P ∥ R ⟹⇩τ ⦇ν*xvec⦈(P' ∥ R')"
by(drule_tac tauActTauStepChain) auto
moreover from P'RelQ' ‹(p ∙ Ψ⇩R) ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ⇩R', P', Q') ∈ Rel" by(metis C3 Associativity compositionSym)
with FrR' ‹A⇩R' ♯* P'› ‹A⇩R' ♯* Q'› ‹A⇩R' ♯* Ψ› have "(Ψ, P' ∥ R', Q' ∥ R') ∈ Rel'" by(rule_tac C1)
with ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈(P' ∥ R'), ⦇ν*xvec⦈(Q' ∥ R')) ∈ Rel'"
by(rule_tac C2)
ultimately show ?case by blast
next
case(cComm2 Ψ⇩R M xvec N Q' A⇩Q Ψ⇩Q K R' A⇩R)
have FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
from ‹A⇩Q ♯* (P, R)› have "A⇩Q ♯* P" and "A⇩Q ♯* R" by simp+
have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
from ‹A⇩R ♯* (P, R)› have "A⇩R ♯* P" and "A⇩R ♯* R" by simp+
from ‹xvec ♯* (P, R)› have "xvec ♯* P" and "xvec ♯* R" by simp+
have QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'" and RTrans: "Ψ ⊗ Ψ⇩Q ⊳ R ⟼K⦇N⦈ ≺ R'"
and MeqK: "Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R ⊢ M ↔K" by fact+
from RTrans FrR ‹distinct A⇩R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* Q'› ‹A⇩R ♯* N› ‹A⇩R ♯* P› ‹A⇩R ♯* xvec› ‹A⇩R ♯* K›
obtain Ψ' A⇩R' Ψ⇩R' where ReqR': "Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'" and FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩"
and "A⇩R' ♯* Ψ" and "A⇩R' ♯* P" and "A⇩R' ♯* Q'" and "A⇩R' ♯* N" and "A⇩R' ♯* xvec"
by(rule_tac C="(Ψ, P, Q', N, xvec)" and C'="(Ψ, P, Q', N, xvec)" in expandFrame) auto
have "Ψ ⊗ Ψ⇩R ⊳ P ↝<Rel> Q" by(rule PSimQ')
with QTrans ‹xvec ♯* Ψ› ‹xvec ♯* Ψ⇩R› ‹xvec ♯* P›
obtain P'' P' where PTrans: "Ψ ⊗ Ψ⇩R : Q ⊳ P ⟹M⦇ν*xvec⦈⟨N⟩ ≺ P''"
and P''Chain: "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'"
and P'RelQ': "((Ψ ⊗ Ψ⇩R) ⊗ Ψ', P', Q') ∈ Rel"
by(fastforce dest: weakSimE)
from PTrans obtain P''' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇧^⇩τ P'''"
and QimpP''': "insertAssertion (extractFrame Q) (Ψ ⊗ Ψ⇩R) ↪⇩F insertAssertion (extractFrame P''') (Ψ ⊗ Ψ⇩R)"
and P'''Trans: "Ψ ⊗ Ψ⇩R ⊳ P''' ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P''"
by(rule weakTransitionE)
from PChain ‹A⇩R ♯* P› have "A⇩R ♯* P'''" by(rule tauChainFreshChain)
obtain A⇩P''' Ψ⇩P''' where FrP''': "extractFrame P''' = ⟨A⇩P''', Ψ⇩P'''⟩" and "A⇩P''' ♯* (Ψ, A⇩Q, Ψ⇩Q, A⇩R, Ψ⇩R, M, N, K, R, P''', xvec)" and "distinct A⇩P'''"
by(rule freshFrame)
hence "A⇩P''' ♯* Ψ" and "A⇩P''' ♯* A⇩Q" and "A⇩P''' ♯* Ψ⇩Q" and "A⇩P''' ♯* M" and "A⇩P''' ♯* R"
and "A⇩P''' ♯* N" and "A⇩P''' ♯* K" and "A⇩P''' ♯* A⇩R" and "A⇩P''' ♯* P'''" and "A⇩P''' ♯* xvec" and "A⇩P''' ♯* Ψ⇩R"
by simp+
have "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩"
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
moreover with QimpP''' FrP''' FrQ ‹A⇩P''' ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩P''' ♯* Ψ⇩R› ‹A⇩Q ♯* Ψ⇩R›
have "⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩ ↪⇩F ⟨A⇩P''', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'''⟩" using freshCompChain
by simp
moreover have "⟨A⇩P''', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'''⟩ ≃⇩F ⟨A⇩P''', (Ψ ⊗ Ψ⇩P''') ⊗ Ψ⇩R⟩"
by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
ultimately have QImpP''': "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P''', (Ψ ⊗ Ψ⇩P''') ⊗ Ψ⇩R⟩"
by(rule FrameStatEqImpCompose)
from PChain FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ P''' ∥ R" by(rule tauChainPar1)
moreover from RTrans FrR P'''Trans MeqK QImpP''' FrP''' FrQ ‹distinct A⇩P'''› ‹distinct A⇩R› ‹A⇩P''' ♯* A⇩R› ‹A⇩Q ♯* A⇩R›
‹A⇩R ♯* Ψ› ‹A⇩R ♯* P'''› ‹A⇩R ♯* Q› ‹A⇩R ♯* R› ‹A⇩R ♯* K› ‹A⇩P''' ♯* Ψ› ‹A⇩P''' ♯* R›
‹A⇩P''' ♯* P'''› ‹A⇩P''' ♯* M› ‹A⇩Q ♯* R› ‹A⇩Q ♯* M› ‹A⇩R ♯* xvec› ‹xvec ♯* M›
obtain K' where "Ψ ⊗ Ψ⇩P''' ⊳ R ⟼K'⦇N⦈ ≺ R'" and "Ψ ⊗ Ψ⇩P''' ⊗ Ψ⇩R ⊢ M ↔ K'" and "A⇩R ♯* K'"
by(rule_tac comm2Aux) (assumption | simp)+
with P'''Trans FrP''' have "Ψ ⊳ P''' ∥ R ⟼τ ≺ ⦇ν*xvec⦈(P'' ∥ R')" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P'''› ‹A⇩R ♯* R›
‹xvec ♯* R› ‹A⇩P''' ♯* Ψ› ‹A⇩P''' ♯* P'''› ‹A⇩P''' ♯* R› ‹A⇩P''' ♯* M› ‹A⇩R ♯* K'› ‹A⇩P''' ♯* A⇩R›
by(rule_tac Comm2)
moreover from P'''Trans ‹A⇩R ♯* P'''› ‹A⇩R ♯* xvec› ‹xvec ♯* M› ‹distinct xvec› have "A⇩R ♯* P''"
by(rule_tac outputFreshChainDerivative) auto
from PChain ‹A⇩R' ♯* P› have "A⇩R' ♯* P'''" by(rule tauChainFreshChain)
with P'''Trans ‹xvec ♯* M› ‹distinct xvec› have "A⇩R' ♯* P''" using ‹A⇩R' ♯* xvec›
by(rule_tac outputFreshChainDerivative) auto
with P''Chain have "A⇩R' ♯* P'" by(rule tauChainFreshChain)
from ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ≃ Ψ ⊗ Ψ⇩R'"
by(metis Associativity AssertionStatEqTrans AssertionStatEqSym compositionSym)
with P''Chain have "Ψ ⊗ Ψ⇩R' ⊳ P'' ⟹⇧^⇩τ P'" by(rule tauChainStatEq)
hence "Ψ ⊳ P'' ∥ R' ⟹⇧^⇩τ P' ∥ R'" using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P''›
by(rule tauChainPar1)
hence "Ψ ⊳ ⦇ν*xvec⦈(P'' ∥ R') ⟹⇧^⇩τ ⦇ν*xvec⦈(P' ∥ R')"
using ‹xvec ♯* Ψ› by(rule tauChainResChainPres)
ultimately have "Ψ ⊳ P ∥ R ⟹⇩τ ⦇ν*xvec⦈(P' ∥ R')" by(drule_tac tauActTauStepChain) auto
moreover from P'RelQ' ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ⇩R', P', Q') ∈ Rel" by(metis C3 Associativity compositionSym)
with FrR' ‹A⇩R' ♯* P'› ‹A⇩R' ♯* Q'› ‹A⇩R' ♯* Ψ› have "(Ψ, P' ∥ R', Q' ∥ R') ∈ Rel'" by(rule_tac C1)
with ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈(P' ∥ R'), ⦇ν*xvec⦈(Q' ∥ R')) ∈ Rel'"
by(rule_tac C2)
ultimately show ?case by blast
qed
qed
no_notation relcomp (infixr "O" 75)
lemma weakCongSimBangPres:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Rel' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
and Rel'' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
assumes PEqQ: "Eq P Q"
and PRelQ: "(Ψ, P, Q) ∈ Rel"
and "guarded P"
and "guarded Q"
and Rel'Rel: "Rel' ⊆ Rel"
and FrameParPres: "⋀Ψ' Ψ⇩U S T U A⇩U. ⟦(Ψ' ⊗ Ψ⇩U, S, T) ∈ Rel; extractFrame U = ⟨A⇩U, Ψ⇩U⟩; A⇩U ♯* Ψ'; A⇩U ♯* S; A⇩U ♯* T⟧ ⟹
(Ψ', U ∥ S, U ∥ T) ∈ Rel"
and C1: "⋀Ψ' S T U. ⟦(Ψ', S, T) ∈ Rel; guarded S; guarded T⟧ ⟹ (Ψ', U ∥ !S, U ∥ !T) ∈ Rel''"
and Closed: "⋀Ψ' S T p. (Ψ', S, T) ∈ Rel ⟹ ((p::name prm) ∙ Ψ', p ∙ S, p ∙ T) ∈ Rel"
and Closed': "⋀Ψ' S T p. (Ψ', S, T) ∈ Rel' ⟹ ((p::name prm) ∙ Ψ', p ∙ S, p ∙ T) ∈ Rel'"
and StatEq: "⋀Ψ' S T Ψ''. ⟦(Ψ', S, T) ∈ Rel; Ψ' ≃ Ψ''⟧ ⟹ (Ψ'', S, T) ∈ Rel"
and StatEq': "⋀Ψ' S T Ψ''. ⟦(Ψ', S, T) ∈ Rel'; Ψ' ≃ Ψ''⟧ ⟹ (Ψ'', S, T) ∈ Rel'"
and Trans: "⋀Ψ' S T U. ⟦(Ψ', S, T) ∈ Rel; (Ψ', T, U) ∈ Rel⟧ ⟹ (Ψ', S, U) ∈ Rel"
and Trans': "⋀Ψ' S T U. ⟦(Ψ', S, T) ∈ Rel'; (Ψ', T, U) ∈ Rel'⟧ ⟹ (Ψ', S, U) ∈ Rel'"
and EqSim: "⋀Ψ' S T. Eq S T ⟹ Ψ' ⊳ S ↝«Rel» T"
and cSim: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ Ψ' ⊳ S ↝<Rel> T"
and cSym: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ (Ψ', T, S) ∈ Rel"
and cSym': "⋀Ψ' S T. (Ψ', S, T) ∈ Rel' ⟹ (Ψ', T, S) ∈ Rel'"
and cExt: "⋀Ψ' S T Ψ''. (Ψ', S, T) ∈ Rel ⟹ (Ψ' ⊗ Ψ'', S, T) ∈ Rel"
and cExt': "⋀Ψ' S T Ψ''. (Ψ', S, T) ∈ Rel' ⟹ (Ψ' ⊗ Ψ'', S, T) ∈ Rel'"
and ParPres: "⋀Ψ' S T U. (Ψ', S, T) ∈ Rel ⟹ (Ψ', S ∥ U, T ∥ U) ∈ Rel"
and ParPres': "⋀Ψ' S T U. (Ψ', S, T) ∈ Rel' ⟹ (Ψ', U ∥ S, U ∥ T) ∈ Rel'"
and ParPres2: "⋀Ψ' S T. Eq S T ⟹ Eq (S ∥ S) (T ∥ T)"
and ResPres: "⋀Ψ' S T xvec. ⟦(Ψ', S, T) ∈ Rel; xvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*xvec⦈S, ⦇ν*xvec⦈T) ∈ Rel"
and ResPres': "⋀Ψ' S T xvec. ⟦(Ψ', S, T) ∈ Rel'; xvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*xvec⦈S, ⦇ν*xvec⦈T) ∈ Rel'"
and Assoc: "⋀Ψ' S T U. (Ψ', S ∥ (T ∥ U), (S ∥ T) ∥ U) ∈ Rel"
and Assoc': "⋀Ψ' S T U. (Ψ', S ∥ (T ∥ U), (S ∥ T) ∥ U) ∈ Rel'"
and ScopeExt: "⋀xvec Ψ' T S. ⟦xvec ♯* Ψ'; xvec ♯* T⟧ ⟹ (Ψ', ⦇ν*xvec⦈(S ∥ T), (⦇ν*xvec⦈S) ∥ T) ∈ Rel"
and ScopeExt': "⋀xvec Ψ' T S. ⟦xvec ♯* Ψ'; xvec ♯* T⟧ ⟹ (Ψ', ⦇ν*xvec⦈(S ∥ T), (⦇ν*xvec⦈S) ∥ T) ∈ Rel'"
and Compose: "⋀Ψ' S T U O. ⟦(Ψ', S, T) ∈ Rel; (Ψ', T, U) ∈ Rel''; (Ψ', U, O) ∈ Rel'⟧ ⟹ (Ψ', S, O) ∈ Rel''"
and rBangActE: "⋀Ψ' S α S'. ⟦Ψ' ⊳ !S ⟼α ≺ S'; guarded S; bn α ♯* S; α ≠ τ; bn α ♯* subject α⟧ ⟹ ∃T. Ψ' ⊳ S ⟼α ≺ T ∧ (𝟭, S', T ∥ !S) ∈ Rel'"
and rBangTauE: "⋀Ψ' S S'. ⟦Ψ' ⊳ !S ⟼τ ≺ S'; guarded S⟧ ⟹ ∃T. Ψ' ⊳ S ∥ S ⟼τ ≺ T ∧ (𝟭, S', T ∥ !S) ∈ Rel'"
and rBangTauI: "⋀Ψ' S S'. ⟦Ψ' ⊳ S ∥ S ⟹⇩τ S'; guarded S⟧ ⟹ ∃T. Ψ' ⊳ !S ⟹⇩τ T ∧ (Ψ', T, S' ∥ !S) ∈ Rel'"
shows "Ψ ⊳ R ∥ !P ↝«Rel''» R ∥ !Q"
proof(induct rule: weakCongSimI)
case(cTau RQ')
from ‹Ψ ⊳ R ∥ !Q ⟼τ ≺ RQ'› show ?case
proof(induct rule: parTauCases[where C="(P, Q, R)"])
case(cPar1 R' A⇩Q Ψ⇩Q)
from ‹extractFrame (!Q) = ⟨A⇩Q, Ψ⇩Q⟩› have "A⇩Q = []" and "Ψ⇩Q = SBottom'" by simp+
with ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼τ ≺ R'› ‹Ψ⇩Q = SBottom'›
have "Ψ ⊳ R ∥ !P ⟼τ ≺ (R' ∥ !P)" by(rule_tac Par1) (assumption | simp)+
hence "Ψ ⊳ R ∥ !P ⟹⇩τ R' ∥ !P" by auto
moreover from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ, R' ∥ !P, R' ∥ !Q) ∈ Rel''" using ‹guarded P› ‹guarded Q›
by(rule C1)
ultimately show ?case by blast
next
case(cPar2 Q' A⇩R Ψ⇩R)
from ‹A⇩R ♯* (P, Q, R)› have "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* R" by simp+
have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Ψ⇩R" and "A⇩Q ♯* A⇩R"
by(rule_tac C="(Ψ, Ψ⇩R, A⇩R)" in freshFrame) auto
from FrQ ‹guarded Q› have "Ψ⇩Q ≃ 𝟭" and "supp Ψ⇩Q = ({}::name set)" by(blast dest: guardedStatEq)+
hence "A⇩R ♯* Ψ⇩Q" and "A⇩Q ♯* Ψ⇩Q" by(auto simp add: fresh_star_def fresh_def)
from ‹Ψ ⊗ Ψ⇩R ⊳ !Q ⟼τ ≺ Q'› ‹guarded Q›
obtain T where QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ∥ Q ⟼τ ≺ T" and "(𝟭, Q', T ∥ !Q) ∈ Rel'"
by(blast dest: rBangTauE)
from ‹Eq P Q› have "Eq (P ∥ P) (Q ∥ Q)" by(rule ParPres2)
with QTrans
obtain S where PTrans: "Ψ ⊗ Ψ⇩R ⊳ P ∥ P ⟹⇩τ S" and SRelT: "(Ψ ⊗ Ψ⇩R, S, T) ∈ Rel"
by(blast dest: EqSim weakCongSimE)
from PTrans ‹guarded P› obtain U where PChain: "Ψ ⊗ Ψ⇩R ⊳ !P ⟹⇩τ U" and "(Ψ ⊗ Ψ⇩R, U, S ∥ !P) ∈ Rel'"
by(blast dest: rBangTauI)
from PChain ‹A⇩R ♯* P› have "A⇩R ♯* U" by(force dest: tauStepChainFreshChain)
from ‹Ψ ⊗ Ψ⇩R ⊳ !P ⟹⇩τ U› FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› have "Ψ ⊳ R ∥ !P ⟹⇩τ R ∥ U"
by(rule_tac tauStepChainPar2) auto
moreover from PTrans ‹A⇩R ♯* P› have "A⇩R ♯* S" by(force dest: tauStepChainFreshChain)
from QTrans ‹A⇩R ♯* Q› have "A⇩R ♯* T" by(force dest: tauFreshChainDerivative)
have "(Ψ, R ∥ U, R ∥ Q') ∈ Rel''"
proof -
from ‹(Ψ ⊗ Ψ⇩R, U, S ∥ !P) ∈ Rel'› Rel'Rel have "(Ψ ⊗ Ψ⇩R, U, S ∥ !P) ∈ Rel"
by auto
hence "(Ψ, R ∥ U, R ∥ (S ∥ !P)) ∈ Rel" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* U› ‹A⇩R ♯* S› ‹A⇩R ♯* P›
by(rule_tac FrameParPres) auto
moreover from ‹(Ψ ⊗ Ψ⇩R, S, T) ∈ Rel› FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* S› ‹A⇩R ♯* T› have "(Ψ, R ∥ S, R ∥ T) ∈ Rel"
by(rule_tac FrameParPres) auto
hence "(Ψ, R ∥ T, R ∥ S) ∈ Rel" by(rule cSym)
hence "(Ψ, (R ∥ T) ∥ !P, (R ∥ S) ∥ !P) ∈ Rel" by(rule ParPres)
hence "(Ψ, (R ∥ S) ∥ !P, (R ∥ T) ∥ !P) ∈ Rel" by(rule cSym)
hence "(Ψ, R ∥ (S ∥ !P), (R ∥ T) ∥ !P) ∈ Rel" by(metis Trans Assoc)
ultimately have "(Ψ, R ∥ U, (R ∥ T) ∥ !P) ∈ Rel" by(rule Trans)
moreover from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ, (R ∥ T) ∥ !P, (R ∥ T) ∥ !Q) ∈ Rel''" using ‹guarded P› ‹guarded Q› by(rule C1)
moreover from ‹(𝟭, Q', T ∥ !Q) ∈ Rel'› have "(𝟭 ⊗ Ψ, Q', T ∥ !Q) ∈ Rel'" by(rule cExt')
hence "(Ψ, Q', T ∥ !Q) ∈ Rel'"
by(rule StatEq') (metis Identity AssertionStatEqSym Commutativity AssertionStatEqTrans)
hence "(Ψ, R ∥ Q', R ∥ (T ∥ !Q)) ∈ Rel'" by(rule ParPres')
hence "(Ψ, R ∥ Q', (R ∥ T) ∥ !Q) ∈ Rel'" by(metis Trans' Assoc')
hence "(Ψ, (R ∥ T) ∥ !Q, R ∥ Q') ∈ Rel'" by(rule cSym')
ultimately show ?thesis by(rule_tac Compose)
qed
ultimately show ?case by blast
next
case(cComm1 Ψ⇩Q M N R' A⇩R Ψ⇩R K xvec Q' A⇩Q)
from ‹A⇩R ♯* (P, Q, R)› have "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* R" by simp+
from ‹xvec ♯* (P, Q, R)› have "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* R" by simp+
have FrQ: "extractFrame(!Q) = ⟨A⇩Q, Ψ⇩Q⟩" by fact
have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
from ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇N⦈ ≺ R'› FrR ‹distinct A⇩R› ‹A⇩R ♯* R› ‹A⇩R ♯* N› ‹A⇩R ♯* xvec› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* M›
obtain A⇩R' Ψ⇩R' Ψ' where FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩" and "Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'" and "A⇩R' ♯* xvec" and "A⇩R' ♯* P" and "A⇩R' ♯* Q" and "A⇩R' ♯* Ψ"
by(rule_tac C="(Ψ, xvec, P, Q)" and C'="(Ψ, xvec, P, Q)" in expandFrame) auto
from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel" by(rule cExt)
moreover from ‹Ψ ⊗ Ψ⇩R ⊳ !Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'› ‹guarded Q› ‹xvec ♯* Q› ‹xvec ♯* K›
obtain S where QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ S" and "(𝟭, Q', S ∥ !Q) ∈ Rel'"
by(fastforce dest: rBangActE)
ultimately obtain P' T where PTrans: "Ψ ⊗ Ψ⇩R : Q ⊳ P ⟹K⦇ν*xvec⦈⟨N⟩ ≺ P'" and P'Chain: "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P' ⟹⇧^⇩τ T" and "((Ψ ⊗ Ψ⇩R) ⊗ Ψ', T, S) ∈ Rel"
using ‹xvec ♯* Ψ› ‹xvec ♯* Ψ⇩R› ‹xvec ♯* P›
by(fastforce dest: cSim weakSimE)
from PTrans ‹A⇩R ♯* P› ‹A⇩R ♯* xvec› ‹A⇩R' ♯* P› ‹A⇩R' ♯* xvec› ‹xvec ♯* K› ‹distinct xvec›
have "A⇩R ♯* P'" and "A⇩R' ♯* P'"
by(force dest: weakOutputFreshChainDerivative)+
with P'Chain have "A⇩R' ♯* T" by(force dest: tauChainFreshChain)+
from QTrans ‹A⇩R' ♯* Q› ‹A⇩R' ♯* xvec› ‹xvec ♯* K› ‹distinct xvec›
have "A⇩R' ♯* S" by(force dest: outputFreshChainDerivative)
obtain A⇩Q' Ψ⇩Q' where FrQ': "extractFrame Q = ⟨A⇩Q', Ψ⇩Q'⟩" and "A⇩Q' ♯* Ψ" and "A⇩Q' ♯* Ψ⇩R" and "A⇩Q' ♯* A⇩R" and "A⇩Q' ♯* M" and "A⇩Q' ♯* R" and "A⇩Q' ♯* K"
by(rule_tac C="(Ψ, Ψ⇩R, A⇩R, K, M, R)" in freshFrame) auto
from FrQ' ‹guarded Q› have "Ψ⇩Q' ≃ 𝟭" and "supp Ψ⇩Q' = ({}::name set)" by(blast dest: guardedStatEq)+
hence "A⇩Q' ♯* Ψ⇩Q'" by(auto simp add: fresh_star_def fresh_def)
from PTrans obtain P'' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇧^⇩τ P''"
and NilImpP'': "⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩ ↪⇩F insertAssertion (extractFrame P'') (Ψ ⊗ Ψ⇩R)"
and P''Trans: "Ψ ⊗ Ψ⇩R ⊳ P'' ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P'"
using FrQ' ‹A⇩Q' ♯* Ψ› ‹A⇩Q' ♯* Ψ⇩R› freshCompChain
by(drule_tac weakTransitionE) auto
from PChain have "Ψ ⊳ R ∥ !P ⟹⇩τ ⦇ν*xvec⦈(R' ∥ (P' ∥ !P))"
proof(induct rule: tauChainCases)
case TauBase
from ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇N⦈ ≺ R'› FrQ have "Ψ ⊗ 𝟭 ⊳ R ⟼M⦇N⦈ ≺ R'" by simp
moreover note FrR
moreover from P''Trans ‹P = P''› have "Ψ ⊗ Ψ⇩R ⊳ P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P'" by simp
hence "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P'" by(rule statEqTransition) (metis Identity AssertionStatEqSym)
hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ !P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ (P' ∥ !P)" using ‹xvec ♯* Ψ› ‹xvec ♯* Ψ⇩R› ‹xvec ♯* P›
by(force intro: Par1)
hence "Ψ ⊗ Ψ⇩R ⊳ !P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ (P' ∥ !P)" using ‹guarded P› by(rule Bang)
moreover from ‹Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊢ M ↔ K› FrQ have "Ψ ⊗ Ψ⇩R ⊗ 𝟭 ⊢ M ↔ K" by simp
ultimately have "Ψ ⊳ R ∥ !P ⟼τ ≺ ⦇ν*xvec⦈(R' ∥ (P' ∥ !P))" using ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* P› ‹A⇩R ♯* M› ‹xvec ♯* R›
by(force intro: Comm1)
thus ?case by(rule tauActTauStepChain)
next
case TauStep
obtain A⇩P'' Ψ⇩P'' where FrP'': "extractFrame P'' = ⟨A⇩P'', Ψ⇩P''⟩" and "A⇩P'' ♯* Ψ" and "A⇩P'' ♯* K" and "A⇩P'' ♯* Ψ⇩R" and "A⇩P'' ♯* R" and "A⇩P'' ♯* P''" and "A⇩P'' ♯* P"
and "A⇩P'' ♯* A⇩R" and "distinct A⇩P''"
by(rule_tac C="(Ψ, K, A⇩R, Ψ⇩R, R, P'', P)" in freshFrame) auto
from PChain ‹A⇩R ♯* P› have "A⇩R ♯* P''" by(drule_tac tauChainFreshChain) auto
with FrP'' ‹A⇩P'' ♯* A⇩R› have "A⇩R ♯* Ψ⇩P''" by(drule_tac extractFrameFreshChain) auto
from ‹Ψ ⊗ Ψ⇩R ⊳ P ⟹⇩τ P''› have "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P ⟹⇩τ P''" by(rule tauStepChainStatEq) (metis Identity AssertionStatEqSym)
hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ !P ⟹⇩τ P'' ∥ !P" by(rule_tac tauStepChainPar1) auto
hence "Ψ ⊗ Ψ⇩R ⊳ !P ⟹⇩τ P'' ∥ !P" using ‹guarded P› by(rule tauStepChainBang)
hence "Ψ ⊳ R ∥ !P ⟹⇩τ R ∥ (P'' ∥ !P)" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P›
by(rule_tac tauStepChainPar2) auto
moreover have "Ψ ⊳ R ∥ (P'' ∥ !P) ⟼τ ≺ ⦇ν*xvec⦈(R' ∥ (P' ∥ !P))"
proof -
from FrQ ‹Ψ⇩Q' ≃ 𝟭› ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇N⦈ ≺ R'› have "Ψ ⊗ Ψ⇩Q' ⊳ R ⟼M⦇N⦈ ≺ R'"
by simp (metis statEqTransition AssertionStatEqSym compositionSym)
moreover from P''Trans have "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P'' ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P'"
by(rule statEqTransition) (metis Identity AssertionStatEqSym)
hence P''PTrans: "Ψ ⊗ Ψ⇩R ⊳ P'' ∥ !P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ (P' ∥ !P)" using ‹xvec ♯* P›
by(rule_tac Par1) auto
moreover from FrP'' have FrP''P: "extractFrame(P'' ∥ !P) = ⟨A⇩P'', Ψ⇩P'' ⊗ 𝟭⟩"
by auto
moreover from FrQ ‹Ψ⇩Q' ≃ 𝟭› ‹Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊢ M ↔ K› have "Ψ ⊗ Ψ⇩Q' ⊗ Ψ⇩R ⊢ M ↔ K"
by simp (metis statEqEnt Composition AssertionStatEqSym Commutativity)
hence "Ψ ⊗ Ψ⇩Q' ⊗ Ψ⇩R ⊢ K ↔ M" by(rule chanEqSym)
moreover have "⟨A⇩Q', (Ψ ⊗ Ψ⇩Q') ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭)) ⊗ Ψ⇩R⟩"
proof -
have "⟨A⇩Q', (Ψ ⊗ Ψ⇩Q') ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩"
by(rule_tac frameResChainPres, simp)
(metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym)
moreover from NilImpP'' FrQ FrP'' ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* Ψ⇩R› freshCompChain have "⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P''⟩"
by auto
moreover have "⟨A⇩P'', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P''⟩ ≃⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R⟩"
by(rule frameResChainPres, simp)
(metis Identity AssertionStatEqSym Associativity Commutativity Composition AssertionStatEqTrans)
ultimately show ?thesis by(rule FrameStatEqImpCompose)
qed
ultimately obtain M' where RTrans: "Ψ ⊗ Ψ⇩P'' ⊗ 𝟭 ⊳ R ⟼M'⦇N⦈ ≺ R'" and "Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ K ↔ M'" and "A⇩R ♯* M'"
using FrR FrQ' ‹distinct A⇩R› ‹distinct A⇩P''› ‹A⇩P'' ♯* A⇩R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P''› ‹A⇩R ♯* Q› ‹A⇩R ♯* R› ‹A⇩R ♯* M› ‹A⇩Q' ♯* R› ‹A⇩Q' ♯* K› ‹A⇩Q' ♯* A⇩R› ‹A⇩R ♯* P› ‹A⇩P'' ♯* P› ‹A⇩R ♯* xvec›
‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* R› ‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* K› ‹xvec ♯* K› ‹distinct xvec›
by(rule_tac A⇩Q="A⇩Q'" and Q="Q" in comm2Aux) (assumption | simp)+
note RTrans FrR P''PTrans FrP''P
moreover from ‹Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ K ↔ M'› have "Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ M' ↔ K" by(rule chanEqSym)
hence "Ψ ⊗ Ψ⇩R ⊗ Ψ⇩P'' ⊗ 𝟭 ⊢ M' ↔ K" by(metis statEqEnt Composition AssertionStatEqSym Commutativity)
ultimately show ?thesis using ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* P''› ‹A⇩R ♯* P› ‹A⇩R ♯* M'› ‹A⇩P'' ♯* A⇩R› ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* R› ‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* P› ‹A⇩P'' ♯* K› ‹xvec ♯* R›
by(rule_tac Comm1) (assumption | simp)+
qed
ultimately show ?thesis
by(drule_tac tauActTauStepChain) auto
qed
moreover from P'Chain have "((Ψ ⊗ Ψ⇩R) ⊗ Ψ') ⊗ 𝟭 ⊳ P' ⟹⇧^⇩τ T"
by(rule tauChainStatEq) (metis Identity AssertionStatEqSym)
hence "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P' ∥ !P ⟹⇧^⇩τ T ∥ !P"
by(rule_tac tauChainPar1) auto
hence "Ψ ⊗ Ψ⇩R ⊗ Ψ' ⊳ P' ∥ !P ⟹⇧^⇩τ T ∥ !P"
by(rule tauChainStatEq) (metis Associativity)
hence "Ψ ⊗ Ψ⇩R' ⊳ P' ∥ !P⟹⇧^⇩τ T ∥ !P" using ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'›
by(rule_tac tauChainStatEq) (auto intro: compositionSym)
hence "Ψ ⊳ R' ∥ (P' ∥ !P) ⟹⇧^⇩τ R' ∥ (T ∥ !P)" using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P› ‹A⇩R' ♯* P'›
by(rule_tac tauChainPar2) auto
hence "Ψ ⊳ ⦇ν*xvec⦈(R' ∥ (P' ∥ !P)) ⟹⇧^⇩τ ⦇ν*xvec⦈(R' ∥ (T ∥ !P))" using ‹xvec ♯* Ψ›
by(rule tauChainResChainPres)
ultimately have "Ψ ⊳ R ∥ !P ⟹⇩τ ⦇ν*xvec⦈(R' ∥ (T ∥ !P))"
by auto
moreover have "(Ψ, ⦇ν*xvec⦈(R' ∥ (T ∥ !P)), ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel''"
proof -
from ‹((Ψ ⊗ Ψ⇩R) ⊗ Ψ', T, S) ∈ Rel› have "(Ψ ⊗ Ψ⇩R ⊗ Ψ', T, S) ∈ Rel"
by(rule StatEq) (metis Associativity)
hence "(Ψ ⊗ Ψ⇩R', T, S) ∈ Rel" using ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'›
by(rule_tac StatEq) (auto dest: compositionSym)
with FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* S› ‹A⇩R' ♯* T› have "(Ψ, R' ∥ T, R' ∥ S) ∈ Rel"
by(rule_tac FrameParPres) auto
hence "(Ψ, (R' ∥ T) ∥ !P, (R' ∥ S) ∥ !P) ∈ Rel" by(rule ParPres)
hence "(Ψ, ⦇ν*xvec⦈((R' ∥ T) ∥ !P), ⦇ν*xvec⦈((R' ∥ S) ∥ !P)) ∈ Rel" using ‹xvec ♯* Ψ›
by(rule ResPres)
hence "(Ψ, ⦇ν*xvec⦈(R' ∥ T) ∥ !P, (⦇ν*xvec⦈(R' ∥ S)) ∥ !P) ∈ Rel" using ‹xvec ♯* Ψ› ‹xvec ♯* P›
by(force intro: Trans ScopeExt)
hence "(Ψ, ⦇ν*xvec⦈(R' ∥ (T ∥ !P)), (⦇ν*xvec⦈(R' ∥ S)) ∥ !P) ∈ Rel" using ‹xvec ♯* Ψ›
by(force intro: Trans ResPres Assoc)
moreover from ‹(Ψ, P, Q) ∈ Rel› ‹guarded P› ‹guarded Q› have "(Ψ, (⦇ν*xvec⦈(R' ∥ S)) ∥ !P, (⦇ν*xvec⦈(R' ∥ S)) ∥ !Q) ∈ Rel''"
by(rule C1)
moreover from ‹(𝟭, Q', S ∥ !Q) ∈ Rel'› have "(𝟭 ⊗ Ψ, Q', S ∥ !Q) ∈ Rel'" by(rule cExt')
hence "(Ψ, Q', S ∥ !Q) ∈ Rel'"
by(rule StatEq') (metis Identity AssertionStatEqSym Commutativity AssertionStatEqTrans)
hence "(Ψ, R' ∥ Q', R' ∥ (S ∥ !Q)) ∈ Rel'" by(rule ParPres')
hence "(Ψ, R' ∥ Q', (R' ∥ S) ∥ !Q) ∈ Rel'" by(metis Trans' Assoc')
hence "(Ψ, (R' ∥ S) ∥ !Q, R' ∥ Q') ∈ Rel'" by(rule cSym')
hence "(Ψ, ⦇ν*xvec⦈((R' ∥ S) ∥ !Q), ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel'" using ‹xvec ♯* Ψ›
by(rule ResPres')
hence "(Ψ, (⦇ν*xvec⦈(R' ∥ S)) ∥ !Q, ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel'" using ‹xvec ♯* Ψ› ‹xvec ♯* Q›
by(force intro: Trans' ScopeExt'[THEN cSym'])
ultimately show ?thesis by(rule_tac Compose)
qed
ultimately show ?case by blast
next
case(cComm2 Ψ⇩Q M xvec N R' A⇩R Ψ⇩R K Q' A⇩Q)
from ‹A⇩R ♯* (P, Q, R)› have "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* R" by simp+
from ‹xvec ♯* (P, Q, R)› have "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* R" by simp+
have FrQ: "extractFrame(!Q) = ⟨A⇩Q, Ψ⇩Q⟩" by fact
have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
from ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇ν*xvec⦈⟨N⟩ ≺ R'› FrR ‹distinct A⇩R› ‹A⇩R ♯* R› ‹A⇩R ♯* N› ‹A⇩R ♯* xvec› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* Ψ› ‹xvec ♯* R› ‹xvec ♯* Ψ› ‹xvec ♯* P› ‹xvec ♯* Q› ‹xvec ♯* M› ‹distinct xvec› ‹A⇩R ♯* M›
obtain p A⇩R' Ψ⇩R' Ψ' where FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩" and "(p ∙ Ψ⇩R) ⊗ Ψ' ≃ Ψ⇩R'" and "A⇩R' ♯* xvec" and "A⇩R' ♯* P" and "A⇩R' ♯* Q" and "A⇩R' ♯* Ψ" and S: "set p ⊆ set xvec × set(p ∙ xvec)" and "distinctPerm p" and "(p ∙ xvec) ♯* N" and "(p ∙ xvec) ♯* Q" and "(p ∙ xvec) ♯* R'" and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Ψ" and "A⇩R' ♯* N" and "A⇩R' ♯* xvec" and "A⇩R' ♯* (p ∙ xvec)"
by(rule_tac C="(Ψ, P, Q)" and C'="(Ψ, P, Q)" in expandFrame) (assumption | simp)+
from ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇ν*xvec⦈⟨N⟩ ≺ R'› S ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* R'›
have RTrans: "Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ R')"
by(simp add: boundOutputChainAlpha'' residualInject)
from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel" by(rule cExt)
moreover from ‹Ψ ⊗ Ψ⇩R ⊳ !Q ⟼K⦇N⦈ ≺ Q'› S ‹(p ∙ xvec) ♯* Q› ‹xvec ♯* Q› ‹distinctPerm p›
have "Ψ ⊗ Ψ⇩R ⊳ !Q ⟼K⦇(p ∙ N)⦈ ≺ (p ∙ Q')" by(rule_tac inputAlpha) auto
then obtain S where QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼K⦇(p ∙ N)⦈ ≺ S" and "(𝟭, (p ∙ Q'), S ∥ !Q) ∈ Rel'"
using ‹guarded Q›
by(fastforce dest: rBangActE)
ultimately obtain P' T where PTrans: "Ψ ⊗ Ψ⇩R : Q ⊳ P ⟹K⦇(p ∙ N)⦈ ≺ P'"
and P'Chain: "(Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ') ⊳ P' ⟹⇧^⇩τ T"
and "((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'), T, S) ∈ Rel"
by(fastforce dest: cSim weakSimE)
from ‹A⇩R' ♯* N› ‹A⇩R' ♯* xvec› ‹A⇩R' ♯* (p ∙ xvec)› S have "A⇩R' ♯* (p ∙ N)"
by(simp add: freshChainSimps)
with PTrans ‹A⇩R' ♯* P› have "A⇩R' ♯* P'" by(force dest: weakInputFreshChainDerivative)
with P'Chain have "A⇩R' ♯* T" by(force dest: tauChainFreshChain)+
from QTrans ‹A⇩R' ♯* Q› ‹A⇩R' ♯* (p ∙ N)› have "A⇩R' ♯* S" by(force dest: inputFreshChainDerivative)
obtain A⇩Q' Ψ⇩Q' where FrQ': "extractFrame Q = ⟨A⇩Q', Ψ⇩Q'⟩" and "A⇩Q' ♯* Ψ" and "A⇩Q' ♯* Ψ⇩R" and "A⇩Q' ♯* A⇩R" and "A⇩Q' ♯* M" and "A⇩Q' ♯* R" and "A⇩Q' ♯* K"
by(rule_tac C="(Ψ, Ψ⇩R, A⇩R, K, M, R)" in freshFrame) auto
from FrQ' ‹guarded Q› have "Ψ⇩Q' ≃ 𝟭" and "supp Ψ⇩Q' = ({}::name set)" by(blast dest: guardedStatEq)+
hence "A⇩Q' ♯* Ψ⇩Q'" by(auto simp add: fresh_star_def fresh_def)
from PTrans obtain P'' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇧^⇩τ P''"
and NilImpP'': "⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩ ↪⇩F insertAssertion (extractFrame P'') (Ψ ⊗ Ψ⇩R)"
and P''Trans: "Ψ ⊗ Ψ⇩R ⊳ P'' ⟼K⦇(p ∙ N)⦈ ≺ P'"
using FrQ' ‹A⇩Q' ♯* Ψ› ‹A⇩Q' ♯* Ψ⇩R› freshCompChain
by(drule_tac weakTransitionE) auto
from ‹(p ∙ xvec) ♯* P› ‹xvec ♯* P› PChain have "(p ∙ xvec) ♯* P''" and "xvec ♯* P''"
by(force dest: tauChainFreshChain)+
from ‹(p ∙ xvec) ♯* N› ‹distinctPerm p› have "xvec ♯* (p ∙ N)"
by(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, where pi=p, symmetric]) simp
with P''Trans ‹xvec ♯* P''› have "xvec ♯* P'" by(force dest: inputFreshChainDerivative)
hence "(p ∙ xvec) ♯* (p ∙ P')" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
from PChain have "Ψ ⊳ R ∥ !P ⟹⇩τ ⦇ν*(p ∙ xvec)⦈((p ∙ R') ∥ (P' ∥ !P))"
proof(induct rule: tauChainCases)
case TauBase
from RTrans FrQ have "Ψ ⊗ 𝟭 ⊳ R ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ R')" by simp
moreover note FrR
moreover from P''Trans ‹P = P''› have "Ψ ⊗ Ψ⇩R ⊳ P ⟼K⦇(p ∙ N)⦈≺ P'" by simp
hence "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P ⟼K⦇(p ∙ N)⦈ ≺ P'"
by(rule statEqTransition) (metis Identity AssertionStatEqSym)
hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ !P ⟼K⦇(p ∙ N)⦈ ≺ (P' ∥ !P)" by(force intro: Par1)
hence "Ψ ⊗ Ψ⇩R ⊳ !P ⟼K⦇(p ∙ N)⦈ ≺ (P' ∥ !P)" using ‹guarded P› by(rule Bang)
moreover from ‹Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊢ M ↔ K› FrQ have "Ψ ⊗ Ψ⇩R ⊗ 𝟭 ⊢ M ↔ K" by simp
ultimately have "Ψ ⊳ R ∥ !P ⟼τ ≺ ⦇ν*(p ∙ xvec)⦈((p ∙ R') ∥ (P' ∥ !P))" using ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* P› ‹A⇩R ♯* M› ‹(p ∙ xvec) ♯* P›
by(force intro: Comm2)
thus ?case by(rule tauActTauStepChain)
next
case TauStep
obtain A⇩P'' Ψ⇩P'' where FrP'': "extractFrame P'' = ⟨A⇩P'', Ψ⇩P''⟩" and "A⇩P'' ♯* Ψ" and "A⇩P'' ♯* K" and "A⇩P'' ♯* Ψ⇩R" and "A⇩P'' ♯* R" and "A⇩P'' ♯* P''" and "A⇩P'' ♯* P"
and "A⇩P'' ♯* A⇩R" and "distinct A⇩P''"
by(rule_tac C="(Ψ, K, A⇩R, Ψ⇩R, R, P'', P)" in freshFrame) auto
from PChain ‹A⇩R ♯* P› have "A⇩R ♯* P''" by(drule_tac tauChainFreshChain) auto
with FrP'' ‹A⇩P'' ♯* A⇩R› have "A⇩R ♯* Ψ⇩P''" by(drule_tac extractFrameFreshChain) auto
from ‹Ψ ⊗ Ψ⇩R ⊳ P ⟹⇩τ P''› have "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P ⟹⇩τ P''" by(rule tauStepChainStatEq) (metis Identity AssertionStatEqSym)
hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ !P ⟹⇩τ P'' ∥ !P" by(rule_tac tauStepChainPar1) auto
hence "Ψ ⊗ Ψ⇩R ⊳ !P ⟹⇩τ P'' ∥ !P" using ‹guarded P› by(rule tauStepChainBang)
hence "Ψ ⊳ R ∥ !P ⟹⇩τ R ∥ (P'' ∥ !P)" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P›
by(rule_tac tauStepChainPar2) auto
moreover have "Ψ ⊳ R ∥ (P'' ∥ !P) ⟼τ ≺ ⦇ν*(p ∙ xvec)⦈((p ∙ R') ∥ (P' ∥ !P))"
proof -
from FrQ ‹Ψ⇩Q' ≃ 𝟭› RTrans have "Ψ ⊗ Ψ⇩Q' ⊳ R ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ R')"
by simp (metis statEqTransition AssertionStatEqSym compositionSym)
moreover from P''Trans have "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P'' ⟼K⦇(p ∙ N)⦈ ≺ P'"
by(rule statEqTransition) (metis Identity AssertionStatEqSym)
hence P''PTrans: "Ψ ⊗ Ψ⇩R ⊳ P'' ∥ !P ⟼K⦇(p ∙ N)⦈ ≺ (P' ∥ !P)"
by(rule_tac Par1) auto
moreover from FrP'' have FrP''P: "extractFrame(P'' ∥ !P) = ⟨A⇩P'', Ψ⇩P'' ⊗ 𝟭⟩"
by auto
moreover from FrQ ‹Ψ⇩Q' ≃ 𝟭› ‹Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊢ M ↔ K› have "Ψ ⊗ Ψ⇩Q' ⊗ Ψ⇩R ⊢ M ↔ K"
by simp (metis statEqEnt Composition AssertionStatEqSym Commutativity)
hence "Ψ ⊗ Ψ⇩Q' ⊗ Ψ⇩R ⊢ K ↔ M" by(rule chanEqSym)
moreover have "⟨A⇩Q', (Ψ ⊗ Ψ⇩Q') ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭)) ⊗ Ψ⇩R⟩"
proof -
have "⟨A⇩Q', (Ψ ⊗ Ψ⇩Q') ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩"
by(rule_tac frameResChainPres, simp)
(metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym)
moreover from NilImpP'' FrQ FrP'' ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* Ψ⇩R› freshCompChain have "⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P''⟩"
by auto
moreover have "⟨A⇩P'', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P''⟩ ≃⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R⟩"
by(rule frameResChainPres, simp)
(metis Identity AssertionStatEqSym Associativity Commutativity Composition AssertionStatEqTrans)
ultimately show ?thesis by(rule FrameStatEqImpCompose)
qed
ultimately obtain M' where RTrans: "Ψ ⊗ Ψ⇩P'' ⊗ 𝟭 ⊳ R ⟼M'⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ R')" and "Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ K ↔ M'" and "A⇩R ♯* M'"
using FrR FrQ' ‹distinct A⇩R› ‹distinct A⇩P''› ‹A⇩P'' ♯* A⇩R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P''› ‹A⇩R ♯* Q› ‹A⇩R ♯* R› ‹A⇩R ♯* M› ‹A⇩Q' ♯* R› ‹A⇩Q' ♯* K› ‹A⇩Q' ♯* A⇩R› ‹A⇩R ♯* P› ‹A⇩P'' ♯* P›
‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* R› ‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* K›
by(rule_tac A⇩Q="A⇩Q'" and Q="Q" in comm1Aux) (assumption | simp)+
note RTrans FrR P''PTrans FrP''P
moreover from ‹Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ K ↔ M'› have "Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ M' ↔ K" by(rule chanEqSym)
hence "Ψ ⊗ Ψ⇩R ⊗ Ψ⇩P'' ⊗ 𝟭 ⊢ M' ↔ K" by(metis statEqEnt Composition AssertionStatEqSym Commutativity)
ultimately show ?thesis using ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* P''› ‹A⇩R ♯* P› ‹A⇩R ♯* M'› ‹A⇩P'' ♯* A⇩R› ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* R› ‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* P› ‹A⇩P'' ♯* K› ‹(p ∙ xvec) ♯* P''› ‹(p ∙ xvec) ♯* P›
by(rule_tac Comm2) (assumption | simp)+
qed
ultimately show ?thesis
by(drule_tac tauActTauStepChain) auto
qed
hence "Ψ ⊳ R ∥ !P ⟹⇩τ ⦇ν*xvec⦈(R' ∥ ((p ∙ P') ∥ !P))"
using ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* (p ∙ P')› ‹(p ∙ xvec) ♯* R'› S ‹distinctPerm p›
by(subst resChainAlpha[where p=p]) auto
moreover from P'Chain have "(p ∙ ((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'))) ⊳ (p ∙ P') ⟹⇧^⇩τ (p ∙ T)"
by(rule tauChainEqvt)
with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S ‹distinctPerm p›
have "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ' ⊳ (p ∙ P') ⟹⇧^⇩τ (p ∙ T)" by(simp add: eqvts)
hence "((Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ') ⊗ 𝟭 ⊳ (p ∙ P') ⟹⇧^⇩τ (p ∙ T)"
by(rule tauChainStatEq) (metis Identity AssertionStatEqSym)
hence "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ' ⊳ (p ∙ P') ∥ !P ⟹⇧^⇩τ (p ∙ T) ∥ !P"
by(rule_tac tauChainPar1) auto
hence "Ψ ⊗ (p ∙ Ψ⇩R) ⊗ Ψ' ⊳ (p ∙ P') ∥ !P ⟹⇧^⇩τ (p ∙ T) ∥ !P"
by(rule tauChainStatEq) (metis Associativity)
hence "Ψ ⊗ Ψ⇩R' ⊳ (p ∙ P') ∥ !P ⟹⇧^⇩τ (p ∙ T) ∥ !P" using ‹(p ∙ Ψ⇩R) ⊗ Ψ' ≃ Ψ⇩R'›
by(rule_tac tauChainStatEq) (auto intro: compositionSym)
hence "Ψ ⊳ R' ∥ ((p ∙ P') ∥ !P) ⟹⇧^⇩τ R' ∥ ((p ∙ T) ∥ !P)"
using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P› ‹A⇩R' ♯* P'› ‹A⇩R' ♯* xvec› ‹A⇩R' ♯* (p ∙ xvec)› S
by(rule_tac tauChainPar2) (auto simp add: freshChainSimps)
hence "Ψ ⊳ ⦇ν*xvec⦈(R' ∥ ((p ∙ P') ∥ !P)) ⟹⇧^⇩τ ⦇ν*xvec⦈(R' ∥ ((p ∙ T) ∥ !P))" using ‹xvec ♯* Ψ›
by(rule tauChainResChainPres)
ultimately have "Ψ ⊳ R ∥ !P ⟹⇩τ ⦇ν*xvec⦈(R' ∥ ((p ∙ T) ∥ !P))"
by auto
moreover have "(Ψ, ⦇ν*xvec⦈(R' ∥ ((p ∙ T) ∥ !P)), ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel''"
proof -
from ‹((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'), T, S) ∈ Rel›
have "(p ∙ ((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ')), (p ∙ T), (p ∙ S)) ∈ Rel"
by(rule Closed)
with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹distinctPerm p› S
have "((Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ', p ∙ T, p ∙ S) ∈ Rel"
by(simp add: eqvts)
hence "(Ψ ⊗ (p ∙ Ψ⇩R) ⊗ Ψ', p ∙ T, p ∙ S) ∈ Rel"
by(rule StatEq) (metis Associativity)
hence "(Ψ ⊗ Ψ⇩R', p ∙ T, p ∙ S) ∈ Rel" using ‹(p ∙ Ψ⇩R) ⊗ Ψ' ≃ Ψ⇩R'›
by(rule_tac StatEq) (auto dest: compositionSym)
moreover from ‹A⇩R' ♯* S› ‹A⇩R' ♯* T› ‹A⇩R' ♯* xvec› ‹A⇩R' ♯* (p ∙ xvec)› S
have "A⇩R' ♯* (p ∙ S)" and "A⇩R' ♯* (p ∙ T)"
by(simp add: freshChainSimps)+
ultimately have "(Ψ, R' ∥ (p ∙ T), R' ∥ (p ∙ S)) ∈ Rel" using FrR' ‹A⇩R' ♯* Ψ›
by(rule_tac FrameParPres) auto
hence "(Ψ, (R' ∥ (p ∙ T)) ∥ !P, (R' ∥ (p ∙ S)) ∥ !P) ∈ Rel" by(rule ParPres)
hence "(Ψ, ⦇ν*xvec⦈((R' ∥ (p ∙ T)) ∥ !P), ⦇ν*xvec⦈((R' ∥ (p ∙ S)) ∥ !P)) ∈ Rel"
using ‹xvec ♯* Ψ›
by(rule ResPres)
hence "(Ψ, ⦇ν*xvec⦈(R' ∥ (p ∙ T)) ∥ !P, (⦇ν*xvec⦈(R' ∥ (p ∙ S))) ∥ !P) ∈ Rel"
using ‹xvec ♯* Ψ› ‹xvec ♯* P›
by(force intro: Trans ScopeExt)
hence "(Ψ, ⦇ν*xvec⦈(R' ∥ ((p ∙ T) ∥ !P)), (⦇ν*xvec⦈(R' ∥ (p ∙ S))) ∥ !P) ∈ Rel"
using ‹xvec ♯* Ψ›
by(force intro: Trans ResPres Assoc)
moreover from ‹(Ψ, P, Q) ∈ Rel› ‹guarded P› ‹guarded Q›
have "(Ψ, (⦇ν*xvec⦈(R' ∥ (p ∙ S))) ∥ !P, (⦇ν*xvec⦈(R' ∥ (p ∙ S))) ∥ !Q) ∈ Rel''"
by(rule C1)
moreover from ‹(𝟭, (p ∙ Q'), S ∥ !Q) ∈ Rel'›
have "(p ∙ 𝟭, p ∙ p ∙ Q', p ∙ (S ∥ !Q)) ∈ Rel'" by(rule Closed')
with ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› S ‹distinctPerm p›
have "(𝟭, Q', (p ∙ S) ∥ !Q) ∈ Rel'" by(simp add: eqvts)
hence "(𝟭 ⊗ Ψ, Q', (p ∙ S) ∥ !Q) ∈ Rel'" by(rule cExt')
hence "(Ψ, Q', (p ∙ S) ∥ !Q) ∈ Rel'"
by(rule StatEq') (metis Identity AssertionStatEqSym Commutativity AssertionStatEqTrans)
hence "(Ψ, R' ∥ Q', R' ∥ ((p ∙ S) ∥ !Q)) ∈ Rel'" by(rule ParPres')
hence "(Ψ, R' ∥ Q', (R' ∥ (p ∙ S)) ∥ !Q) ∈ Rel'" by(metis Trans' Assoc')
hence "(Ψ, (R' ∥ (p ∙ S)) ∥ !Q, R' ∥ Q') ∈ Rel'" by(rule cSym')
hence "(Ψ, ⦇ν*xvec⦈((R' ∥ (p ∙ S)) ∥ !Q), ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel'" using ‹xvec ♯* Ψ›
by(rule ResPres')
hence "(Ψ, (⦇ν*xvec⦈(R' ∥ (p ∙ S))) ∥ !Q, ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel'" using ‹xvec ♯* Ψ› ‹xvec ♯* Q›
by(force intro: Trans' ScopeExt'[THEN cSym'])
ultimately show ?thesis by(rule_tac Compose)
qed
ultimately show ?case by blast
qed
qed
notation relcomp (infixr "O" 75)
end
end