Theory Weak_Sim_Pres
theory Weak_Sim_Pres
imports Sim_Pres Weak_Simulation Weak_Stat_Imp
begin
context env begin
lemma weakInputPres:
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 M :: 'a
and xvec :: "name list"
and N :: 'a
assumes PRelQ: "⋀Tvec Ψ'. length xvec = length Tvec ⟹ (Ψ ⊗ Ψ', P[xvec::=Tvec], Q[xvec::=Tvec]) ∈ Rel"
shows "Ψ ⊳ M⦇λ*xvec N⦈.P ↝<Rel> M⦇λ*xvec N⦈.Q"
proof(induct rule: weakSimI2)
case(cAct Ψ' α Q')
from ‹Ψ ⊳ M⦇λ*xvec N⦈.Q ⟼α ≺ Q'› show ?case
proof(induct rule: inputCases)
case(cInput K Tvec)
from ‹Ψ ⊢ M ↔ K› ‹set xvec ⊆ supp N› ‹length xvec = length Tvec› ‹distinct xvec›
have "Ψ : (M⦇λ*xvec N⦈.Q) ⊳ M⦇λ*xvec N⦈.P ⟹K⦇(N[xvec::=Tvec])⦈ ≺ (P[xvec::=Tvec])"
by(rule_tac weakInput) auto
moreover have "Ψ ⊗ Ψ' ⊳ P[xvec::=Tvec] ⟹⇧^⇩τ P[xvec::=Tvec]" by simp
moreover from ‹length xvec = length Tvec› have "(Ψ ⊗ Ψ', P[xvec::=Tvec], Q[xvec::=Tvec]) ∈ Rel"
by(rule PRelQ)
ultimately show ?case by blast
qed
next
case(cTau Q')
from ‹Ψ ⊳ M⦇λ*xvec N⦈.Q ⟼τ ≺ Q'› have False by auto
thus ?case by simp
qed
lemma weakOutputPres:
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 M :: 'a
and N :: 'a
assumes PRelQ: "⋀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ Rel"
shows "Ψ ⊳ M⟨N⟩.P ↝<Rel> M⟨N⟩.Q"
proof(induct rule: weakSimI2)
case(cAct Ψ' α Q')
from ‹Ψ ⊳ M⟨N⟩.Q ⟼α ≺ Q'› show ?case
proof(induct rule: outputCases)
case(cOutput K)
from ‹Ψ ⊢ M ↔ K›
have "Ψ : (M⟨N⟩.Q) ⊳ M⟨N⟩.P ⟹K⟨N⟩ ≺ P" by(rule weakOutput) auto
moreover have "Ψ ⊗ Ψ' ⊳ P ⟹⇧^⇩τ P" by simp
moreover have "(Ψ ⊗ Ψ', P, Q) ∈ Rel" by(rule PRelQ)
ultimately show ?case by blast
qed
next
case(cTau Q')
from ‹Ψ ⊳ M⟨N⟩.Q ⟼τ ≺ Q'› have False by auto
thus ?case by simp
qed
lemma resTauCases[consumes 3, case_names cRes]:
fixes Ψ :: 'b
and x :: name
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
and C :: "'d::fs_name"
assumes Trans: "Ψ ⊳ ⦇νx⦈P ⟼τ ≺ P'"
and "x ♯ Ψ"
and "x ♯ P'"
and rScope: "⋀P'. ⟦Ψ ⊳ P ⟼τ ≺ P'⟧ ⟹ Prop (⦇νx⦈P')"
shows "Prop P'"
proof -
note Trans ‹x ♯ Ψ›
moreover have "x ♯ (τ)" by simp
moreover note ‹x ♯ P'›
moreover have "bn(τ) ♯* Ψ" and "bn(τ) ♯* P" and "bn(τ) ♯* subject(τ)" and "bn(τ) = []" by simp+
ultimately show ?thesis
by(induct rule: resCases) (auto intro: rScope)
qed
lemma weakResPres:
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 y. ⟦(Ψ', R, S) ∈ Rel; y ♯ Ψ'⟧ ⟹ (Ψ', ⦇νy⦈R, ⦇νy⦈S) ∈ Rel'"
shows "Ψ ⊳ ⦇νx⦈P ↝<Rel'> ⦇νx⦈Q"
proof -
note ‹eqvt Rel'› ‹x ♯ Ψ›
moreover have "x ♯ ⦇νx⦈P" and "x ♯ ⦇νx⦈Q" by(simp add: abs_fresh)+
ultimately show ?thesis
proof(induct rule: weakSimIFresh[of _ _ _ _ _ "()"])
case(cAct α Q' Ψ')
from ‹bn α ♯* ⦇νx⦈P› ‹bn α ♯* ⦇νx⦈Q› ‹x ♯ α› have "bn α ♯* P" and "bn α ♯* Q" by simp+
from ‹Ψ ⊳ ⦇νx⦈Q ⟼α ≺ Q'› ‹x ♯ Ψ› ‹x ♯ α› ‹x ♯ Q'› ‹bn α ♯* Ψ› ‹bn α ♯* Q› ‹bn α ♯* subject α› ‹bn α ♯* P› ‹x ♯ α›
show ?case
proof(induct rule: resCases)
case(cOpen M xvec1 xvec2 y N Q')
from ‹bn(M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩) ♯* P› have "xvec1 ♯* P" and "xvec2 ♯* P" and "y ♯ P" by simp+
from ‹x ♯ (M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩)› have "x ♯ xvec1" and "x ≠ y" and "x ♯ xvec2" and "x ♯ M" by simp+
from PSimQ ‹Ψ ⊳ Q ⟼M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ Q')› ‹xvec1 ♯* Ψ› ‹xvec2 ♯* Ψ› ‹xvec1 ♯* P› ‹xvec2 ♯* P› ‹α ≠ τ›
obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ P''"
and P''Chain: "Ψ ⊗ ([(x, y)] ∙ Ψ') ⊳ P'' ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ ⊗ ([(x, y)] ∙ Ψ'), P', ([(x, y)] ∙ Q')) ∈ Rel"
by (fastforce dest: weakSimE)
from PTrans have "([(x, y)] ∙ Ψ) : ([(x, y)] ∙ Q) ⊳ ([(x, y)] ∙ P) ⟹([(x, y)] ∙ (M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩)) ≺ ([(x, y)] ∙ P'')"
by(rule eqvts)
with ‹x ♯ Ψ› ‹y ♯ Ψ› ‹x ♯ M› ‹y ♯ M› ‹x ♯ xvec1› ‹y ♯ xvec1› ‹x ♯ xvec2› ‹y ♯ xvec2›
have "Ψ : ([(x, y)] ∙ Q) ⊳ ([(x, y)] ∙ P) ⟹M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ ([(x, y)] ∙ P'')"
by(simp add: eqvts)
hence "Ψ : ⦇νy⦈([(x, y)] ∙ Q) ⊳ ⦇νy⦈([(x, y)] ∙ P) ⟹M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ ([(x, y)] ∙ P'')"
using ‹y ∈ supp N› ‹y ♯ Ψ› ‹y ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2›
by(rule weakOpen)
with ‹y ♯ P› ‹y ♯ Q› have "Ψ : ⦇νx⦈Q ⊳ ⦇νx⦈P ⟹M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ ([(x, y)] ∙ P'')"
by(simp add: alphaRes)
moreover from P''Chain have "([(x, y)] ∙ (Ψ ⊗ ([(x, y)] ∙ Ψ'))) ⊳ ([(x, y)] ∙ P'') ⟹⇧^⇩τ ([(x, y)] ∙ P')"
by(rule eqvts)
with ‹x ♯ Ψ› ‹y ♯ Ψ› have "Ψ ⊗ Ψ' ⊳ ([(x, y)] ∙ P'') ⟹⇧^⇩τ ([(x, y)] ∙ P')" by(simp add: eqvts)
moreover from P'RelQ' ‹Rel ⊆ Rel'› have "(Ψ ⊗ ([(x, y)] ∙ Ψ'), P', ([(x, y)] ∙ Q')) ∈ Rel'" by auto
with ‹eqvt Rel'› have "([(x, y)] ∙ (Ψ ⊗ ([(x, y)] ∙ Ψ'), P', ([(x, y)] ∙ Q'))) ∈ Rel'" by(rule eqvtI)
with ‹x ♯ Ψ› ‹y ♯ Ψ› have " (Ψ ⊗ Ψ', [(x, y)] ∙ P', Q') ∈ Rel'" by(simp add: eqvts)
ultimately show ?case by blast
next
case(cRes Q')
from PSimQ ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹α ≠ τ›
obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹α ≺ P''"
and P''Chain: "Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ ⊗ Ψ', P', Q') ∈ Rel"
by(blast dest: weakSimE)
from PTrans ‹x ♯ Ψ› ‹x ♯ α› have "Ψ : ⦇νx⦈Q ⊳ ⦇νx⦈P ⟹α ≺ ⦇νx⦈P''"
by(rule_tac weakScope)
moreover from P''Chain ‹x ♯ Ψ› ‹x ♯ Ψ'› have "Ψ ⊗ Ψ' ⊳ ⦇νx⦈P'' ⟹⇧^⇩τ ⦇νx⦈P'"
by(rule_tac tauChainResPres) auto
moreover from P'RelQ' ‹x ♯ Ψ› ‹x ♯ Ψ'› have "(Ψ ⊗ Ψ', ⦇νx⦈P', ⦇νx⦈Q') ∈ Rel'"
apply(rule_tac C1) by(auto simp add: fresh_left calc_atm)
ultimately show ?case by blast
qed
next
case(cTau Q')
from ‹Ψ ⊳ ⦇νx⦈Q ⟼τ ≺ Q'› ‹x ♯ Ψ› ‹x ♯ Q'›
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: weakSimE)
from PChain ‹x ♯ Ψ› have "Ψ ⊳ ⦇νx⦈P ⟹⇧^⇩τ ⦇νx⦈P'" by(rule tauChainResPres)
moreover from P'RelQ' ‹x ♯ Ψ› have "(Ψ, ⦇νx⦈P', ⦇νx⦈Q') ∈ Rel'" by(rule C1)
ultimately show ?case by blast
qed
qed
qed
lemma weakResChainPres:
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 yvec. ⟦(Ψ', R, S) ∈ Rel; yvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*yvec⦈R, ⦇ν*yvec⦈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 yvec="[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 weakResPres)
thus ?case by simp
qed
lemma parTauCases[consumes 1, case_names cPar1 cPar2 cComm1 cComm2]:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
and C :: "'d::fs_name"
assumes Trans: "Ψ ⊳ P ∥ Q ⟼τ ≺ R"
and rPar1: "⋀P' A⇩Q Ψ⇩Q. ⟦Ψ ⊗ Ψ⇩Q ⊳ P ⟼τ ≺ P'; extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩; distinct A⇩Q;
A⇩Q ♯* Ψ; A⇩Q ♯* P; A⇩Q ♯* Q; A⇩Q ♯* C⟧ ⟹ Prop (P' ∥ Q)"
and rPar2: "⋀Q' A⇩P Ψ⇩P. ⟦Ψ ⊗ Ψ⇩P ⊳ Q ⟼τ ≺ Q'; extractFrame P = ⟨A⇩P, Ψ⇩P⟩; distinct A⇩P;
A⇩P ♯* Ψ; A⇩P ♯* P; A⇩P ♯* Q; A⇩P ♯* C⟧ ⟹ Prop (P ∥ Q')"
and rComm1: "⋀Ψ⇩Q M N P' A⇩P Ψ⇩P K xvec Q' A⇩Q.
⟦Ψ ⊗ Ψ⇩Q ⊳ P ⟼M⦇N⦈ ≺ P'; extractFrame P = ⟨A⇩P, Ψ⇩P⟩; distinct A⇩P;
Ψ ⊗ Ψ⇩P ⊳ Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'; extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩; distinct A⇩Q;
Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q ⊢ M ↔ K; distinct xvec;
A⇩P ♯* Ψ; A⇩P ♯* Ψ⇩Q; A⇩P ♯* P; A⇩P ♯* M; A⇩P ♯* N; A⇩P ♯* P'; A⇩P ♯* Q; A⇩P ♯* xvec; A⇩P ♯* Q'; A⇩P ♯* A⇩Q; A⇩P ♯* C;
A⇩Q ♯* Ψ; A⇩Q ♯* Ψ⇩P; A⇩Q ♯* P; A⇩Q ♯* K; A⇩Q ♯* N; A⇩Q ♯* P'; A⇩Q ♯* Q; A⇩Q ♯* xvec; A⇩Q ♯* Q'; A⇩Q ♯* C;
xvec ♯* Ψ; xvec ♯* Ψ⇩P; xvec ♯* P; xvec ♯* M; xvec ♯* K; xvec ♯* Q; xvec ♯* Ψ⇩Q; xvec ♯* C⟧ ⟹
Prop (⦇ν*xvec⦈(P' ∥ Q'))"
and rComm2: "⋀Ψ⇩Q M xvec N P' A⇩P Ψ⇩P K Q' A⇩Q.
⟦Ψ ⊗ Ψ⇩Q ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'; extractFrame P = ⟨A⇩P, Ψ⇩P⟩; distinct A⇩P;
Ψ ⊗ Ψ⇩P ⊳ Q ⟼K⦇N⦈ ≺ Q'; extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩; distinct A⇩Q;
Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q ⊢ M ↔ K; distinct xvec;
A⇩P ♯* Ψ; A⇩P ♯* Ψ⇩Q; A⇩P ♯* P; A⇩P ♯* M; A⇩P ♯* N; A⇩P ♯* P'; A⇩P ♯* Q; A⇩P ♯* xvec; A⇩P ♯* Q'; A⇩P ♯* A⇩Q; A⇩P ♯* C;
A⇩Q ♯* Ψ; A⇩Q ♯* Ψ⇩P; A⇩Q ♯* P; A⇩Q ♯* K; A⇩Q ♯* N; A⇩Q ♯* P'; A⇩Q ♯* Q; A⇩Q ♯* xvec; A⇩Q ♯* Q'; A⇩Q ♯* C;
xvec ♯* Ψ; xvec ♯* Ψ⇩P; xvec ♯* P; xvec ♯* M; xvec ♯* K; xvec ♯* Q; xvec ♯* Ψ⇩Q; xvec ♯* C⟧ ⟹
Prop (⦇ν*xvec⦈(P' ∥ Q'))"
shows "Prop R"
proof -
from Trans obtain α where "Ψ ⊳ P ∥ Q ⟼α ≺ R" and "bn α ♯* Ψ" and "bn α ♯* P" and "bn α ♯* Q" and "bn α ♯* subject α" and "α = τ" by auto
thus ?thesis using rPar1 rPar2 rComm1 rComm2
by(induct rule: parCases[where C=C]) (auto simp add: residualInject)
qed
lemma weakParPres:
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 PRelQ: "⋀A⇩R Ψ⇩R. ⟦extractFrame R = ⟨A⇩R, Ψ⇩R⟩; A⇩R ♯* Ψ; A⇩R ♯* P; A⇩R ♯* Q⟧ ⟹ (Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel"
and Eqvt: "eqvt Rel"
and Eqvt': "eqvt Rel'"
and Sim: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ Ψ' ⊳ S ↝<Rel> T"
and Sym: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ (Ψ', T, S) ∈ Rel"
and Ext: "⋀Ψ' S T Ψ'. ⟦(Ψ', S, T) ∈ Rel⟧ ⟹ (Ψ' ⊗ Ψ'', S, T) ∈ Rel"
and StatImp: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ Ψ' ⊳ S ⪅<Rel> T"
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 -
from Eqvt' show ?thesis
proof(induct rule: weakSimI[where C="()"])
case(cAct Ψ' α QR)
from ‹bn α ♯* (P ∥ R)› ‹bn α ♯* (Q ∥ R)›
have "bn α ♯* P" and "bn α ♯* Q" and "bn α ♯* R"
by simp+
from ‹Ψ ⊳ Q ∥ R ⟼α ≺ QR› ‹bn α ♯* Ψ› ‹bn α ♯* Q› ‹bn α ♯* R› ‹bn α ♯* subject α› ‹α ≠ τ› show ?case
proof(induct rule: parCases[where C="(P, R, Ψ')"])
case(cPar1 Q' A⇩R Ψ⇩R)
from ‹A⇩R ♯* (P, R, Ψ')› have "A⇩R ♯* P" and "A⇩R ♯* Ψ'" by simp+
have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
from ‹A⇩R ♯* α› ‹bn α ♯* R› FrR
have "bn α ♯* Ψ⇩R" by(drule_tac extractFrameFreshChain) auto
have QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼α ≺ Q'" by fact
from FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› have "Ψ ⊗ Ψ⇩R ⊳ P ↝<Rel> Q"
by(blast intro: PRelQ Sim)
then obtain P'' P' where PTrans: "Ψ ⊗ Ψ⇩R : Q ⊳ P ⟹α ≺ P''"
and P''Chain: "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'" and P'RelQ': "((Ψ ⊗ Ψ⇩R) ⊗ Ψ', P', Q') ∈ Rel"
using QTrans ‹bn α ♯* Ψ› ‹bn α ♯* Ψ⇩R› ‹bn α ♯* P› ‹bn α ♯* R› ‹A⇩R ♯* α› ‹α ≠ τ›
by(drule_tac Ψ'=Ψ' in weakSimE(1)) auto
from PTrans QTrans ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* α› ‹bn α ♯* subject α› ‹distinct(bn α)›
have "A⇩R ♯* P''" and "A⇩R ♯* Q'"
by(fastforce dest: weakFreshChainDerivative freeFreshChainDerivative)+
with P''Chain have "A⇩R ♯* P'" by(force dest: tauChainFreshChain)
from PTrans FrR ‹bn α ♯* R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* α› ‹A⇩R ♯* Q›
have "Ψ : Q ∥ R ⊳ P ∥ R ⟹α ≺ (P'' ∥ R)"
by(rule_tac weakPar1)
moreover from P''Chain have "(Ψ ⊗ Ψ') ⊗ Ψ⇩R ⊳ P'' ⟹⇧^⇩τ P'"
by(metis tauChainStatEq Associativity Commutativity Composition)
with FrR have "Ψ ⊗ Ψ' ⊳ P'' ∥ R ⟹⇧^⇩τ P' ∥ R" using ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ'› ‹A⇩R ♯* P''›
by(rule_tac tauChainPar1) auto
moreover from P'RelQ' have "((Ψ ⊗ Ψ') ⊗ Ψ⇩R, P', Q') ∈ Rel"
by(metis C3 compositionSym Associativity Commutativity)
hence "(Ψ ⊗ Ψ', P' ∥ R, Q' ∥ R) ∈ Rel'" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ'› ‹A⇩R ♯* P'› ‹A⇩R ♯* Q'›
by(rule_tac C1) auto
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" and "A⇩Q ♯* Ψ'" 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 ♯* α" 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
from FrP FrQ ‹bn α ♯* P› ‹bn α ♯* Q› ‹A⇩P ♯* α› ‹A⇩Q ♯* α›
have "bn α ♯* Ψ⇩P" and "bn α ♯* Ψ⇩Q"
by(force dest: extractFrameFreshChain)+
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 ♯* α" and "A⇩R ♯* R" and "A⇩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› ‹A⇩R ♯* α› ‹A⇩R ♯* Ψ'›
‹bn α ♯* Ψ› ‹bn α ♯* P› ‹bn α ♯* Q› ‹bn α ♯* R› ‹bn α ♯* subject α› ‹distinct(bn α)›
obtain p Ψ'' A⇩R' Ψ⇩R' where S: "set p ⊆ set(bn α) × set(bn(p ∙ α))" and "(p ∙ Ψ⇩R) ⊗ Ψ'' ≃ Ψ⇩R'"
and FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩"
and "bn(p ∙ α) ♯* Ψ" and "bn(p ∙ α) ♯* P" and "bn(p ∙ α) ♯* Q"
and "A⇩R' ♯* Ψ" and "A⇩R' ♯* P" and "A⇩R' ♯* Q" and "A⇩R' ♯* Ψ'" and "distinctPerm p"
by(rule_tac C="(Ψ, Ψ', P, Q)" and C'="(Ψ, P, Q)" in expandFrame) (assumption | simp)+
from FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q›
have "(Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel" by(rule PRelQ)
hence "(Ψ ⊗ Ψ⇩R, Q, P) ∈ Rel" by(rule Sym)
hence "Ψ ⊗ Ψ⇩R ⊳ Q ⪅<Rel> P" by(rule StatImp)
then 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 ∙ Ψ')) ⊳ P' ⟹⇧^⇩τ P''"
and P'RelQ: "((Ψ ⊗ Ψ⇩R) ⊗ ((p ∙ Ψ'') ⊗ (p ∙ Ψ')), Q, P'') ∈ Rel"
by(rule weakStatImpE)
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" and "A⇩P' ♯* α"
by(rule_tac C="(Ψ, Ψ⇩R, Ψ⇩Q, A⇩Q, R, A⇩R, α)" in freshFrame) auto
from PChain ‹A⇩R ♯* P› ‹A⇩Q ♯* P› ‹bn α ♯* P› have "A⇩Q ♯* P'" and "A⇩R ♯* P'" and "bn α ♯* 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 "insertAssertion (extractFrame(Q ∥ R)) Ψ ↪⇩F insertAssertion(extractFrame(P' ∥ R)) Ψ"
proof -
have "⟨A⇩Q, Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩"
by(metis Associativity Composition Commutativity AssertionStatEqTrans AssertionStatEqSym frameNilStatEq frameResChainPres)
moreover from QimpP' FrQ FrP' ‹A⇩Q ♯* Ψ⇩R› ‹A⇩P' ♯* Ψ⇩R› ‹A⇩P' ♯* Ψ› ‹A⇩Q ♯* Ψ›
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 Associativity Composition Commutativity AssertionStatEqTrans AssertionStatEqSym frameNilStatEq frameResChainPres)
ultimately have "⟨A⇩Q, Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P', Ψ ⊗ Ψ⇩P' ⊗ Ψ⇩R⟩"
by(rule FrameStatEqImpCompose)
hence "⟨(A⇩R@A⇩Q), Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R⟩ ↪⇩F ⟨(A⇩R@A⇩P'), Ψ ⊗ Ψ⇩P' ⊗ Ψ⇩R⟩"
by(force intro: frameImpResChainPres simp add: frameChainAppend)
with FrQ FrR FrP' ‹A⇩R ♯* A⇩Q› ‹A⇩P' ♯* A⇩R› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩R ♯* Ψ⇩Q› ‹A⇩R ♯* Ψ⇩P'› ‹A⇩P' ♯* Ψ⇩R›
‹A⇩P' ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩R ♯* Ψ›
show ?thesis
by(simp add: frameChainAppend) (metis frameImpChainComm FrameStatImpTrans)
qed
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⇩Q ♯* α›
‹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: transferFrame)
qed
hence "Ψ ⊳ P' ∥ R ⟼α ≺ (P' ∥ R')" using FrP' ‹bn α ♯* P'› ‹A⇩P' ♯* Ψ› ‹A⇩P' ♯* R› ‹A⇩P' ♯* α› ‹A⇩P' ♯* α›
by(rule_tac Par2)
ultimately have "Ψ : (Q ∥ R) ⊳ P ∥ R ⟹α ≺ (P' ∥ R')"
by(rule_tac weakTransitionI)
moreover from PChain P'Chain ‹bn α ♯* P'› ‹bn(p ∙ α) ♯* P› ‹A⇩R' ♯* P›
have "bn α ♯* P''" and "bn(p ∙ α) ♯* P'" and "bn(p ∙ α) ♯* P''" and "A⇩R' ♯* P'" and "A⇩R' ♯* P''"
by(metis tauChainFreshChain)+
from P'Chain have "(p ∙ ((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'') ⊗ (p ∙ Ψ'))) ⊳ (p ∙ P') ⟹⇧^⇩τ (p ∙ P'')"
by(rule eqvts)
with ‹bn α ♯* Ψ› ‹bn(p ∙ α) ♯* Ψ› ‹bn α ♯* P'› ‹bn(p ∙ α) ♯* P'› ‹bn α ♯* P''› ‹bn(p ∙ α) ♯* P''›
S ‹distinctPerm p›
have "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ'' ⊗ Ψ' ⊳ P' ⟹⇧^⇩τ P''"
by(simp add: eqvts)
hence "(Ψ ⊗ Ψ') ⊗ (p ∙ Ψ⇩R) ⊗ Ψ'' ⊳ P' ⟹⇧^⇩τ P''"
by(rule tauChainStatEq) (metis Associativity Commutativity Composition AssertionStatEqTrans)
with ‹(p ∙ Ψ⇩R) ⊗ Ψ'' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ') ⊗ Ψ⇩R' ⊳ P' ⟹⇧^⇩τ P''" by(metis tauChainStatEq compositionSym)
hence "Ψ ⊗ Ψ' ⊳ P' ∥ R' ⟹⇧^⇩τ P'' ∥ R'" using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* Ψ'› ‹A⇩R' ♯* P'› by(rule_tac tauChainPar1) auto
moreover from P'RelQ have "((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'') ⊗ (p ∙ Ψ'), P'', Q) ∈ Rel" by(rule Sym)
with ‹eqvt Rel› have "(p ∙ ((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'') ⊗ (p ∙ Ψ'), P'', Q)) ∈ Rel" by(rule eqvtI)
with ‹bn α ♯* Ψ› ‹bn(p ∙ α) ♯* Ψ› ‹bn α ♯* P''› ‹bn(p ∙ α) ♯* P''› ‹bn α ♯* Q› ‹bn(p ∙ α) ♯* Q› S ‹distinctPerm p›
have "((Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ'' ⊗ Ψ', P'', Q) ∈ Rel" by(simp add: eqvts)
with ‹(p ∙ Ψ⇩R) ⊗ Ψ'' ≃ Ψ⇩R'› have "((Ψ ⊗ Ψ') ⊗ Ψ⇩R', P'', Q) ∈ Rel"
by(rule_tac C3, auto) (metis Associativity Commutativity Composition AssertionStatEqTrans)
with FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* Ψ'› ‹A⇩R' ♯* P''› ‹A⇩R' ♯* Q›
have "(Ψ ⊗ Ψ', P'' ∥ R', Q ∥ R') ∈ Rel'" by(rule_tac C1) auto
ultimately show ?case by blast
next
case cComm1
from ‹τ ≠ τ› have False by simp
thus ?case by simp
next
case cComm2
from ‹τ ≠ τ› have False by simp
thus ?case by simp
qed
next
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(blast intro: PRelQ Sim)
moreover have QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼τ ≺ Q'" by fact
ultimately obtain P' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ ⊗ Ψ⇩R, P', Q') ∈ Rel"
by(force dest: weakSimE)
from PChain QTrans ‹A⇩R ♯* P› ‹A⇩R ♯* Q› have "A⇩R ♯* P'" and "A⇩R ♯* Q'"
by(force dest: freeFreshChainDerivative tauChainFreshChain)+
from PChain FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ (P' ∥ R)"
by(rule tauChainPar1)
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) ⊗ Ψ', Q, P'') ∈ Rel"
by(metis StatImp PRelQ Sym weakStatImpE)
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(rule tauChainStatEq) (metis Associativity)
with ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'› have "Ψ ⊗ Ψ⇩R' ⊳ P' ⟹⇧^⇩τ P''" by(metis tauChainStatEq compositionSym)
hence "Ψ ⊳ P' ∥ R' ⟹⇧^⇩τ P'' ∥ R'" using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P'› by(rule_tac tauChainPar1)
ultimately have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ (P'' ∥ R')"
by(fastforce dest: rtrancl_into_rtrancl)
moreover from P'RelQ ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ⇩R', P'', Q) ∈ Rel" by(blast intro: C3 Associativity compositionSym Sym)
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› ‹A⇩R ♯* N› ‹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› ‹xvec ♯* K› ‹distinct xvec› ‹A⇩R ♯* N›
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)
from FrR ‹(p ∙ A⇩R) ♯* Ψ› ‹(p ∙ A⇩R) ♯* P› ‹(p ∙ A⇩R) ♯* Q›
have "Ψ ⊗ (p ∙ Ψ⇩R) ⊳ P ↝<Rel> Q" by(force intro: Sim PRelQ)
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(auto dest: weakInputFreshChainDerivative inputFreshChainDerivative)
from PTrans FrQ RTrans FrR MeqK ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* P› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* R› ‹A⇩Q ♯* (p ∙ M)› ‹A⇩Q ♯* (p ∙ A⇩R)›
‹(p ∙ A⇩R) ♯* Ψ› ‹(p ∙ A⇩R) ♯* P› ‹(p ∙ A⇩R) ♯* Q› ‹(p ∙ A⇩R) ♯* R› ‹(p ∙ A⇩R) ♯* K› ‹xvec ♯* P› ‹distinct A⇩R›
have "Ψ ⊳ P ∥ R ⟹⇩τ ⦇ν*xvec⦈(P'' ∥ R')" apply(rule_tac weakComm1)
by(assumption | simp)+
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 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) (assumption | simp)+
from FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› have "Ψ ⊗ Ψ⇩R ⊳ P ↝<Rel> Q" by(force intro: Sim PRelQ)
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 have "A⇩R' ♯* P''" using ‹A⇩R' ♯* xvec› ‹xvec ♯* M› ‹distinct 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 tauActTauChain) 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
qed
no_notation relcomp (infixr "O" 75)
lemma weakSimBangPres:
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 "(Ψ, P, Q) ∈ Rel"
and "eqvt 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 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 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 cSim: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ Ψ' ⊳ S ↝<Rel> T"
and cExt: "⋀Ψ' S T Ψ''. (Ψ', S, T) ∈ Rel ⟹ (Ψ' ⊗ Ψ'', S, T) ∈ Rel"
and cExt': "⋀Ψ' S T Ψ''. (Ψ', S, T) ∈ Rel' ⟹ (Ψ' ⊗ Ψ'', S, T) ∈ Rel'"
and cSym: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ (Ψ', T, S) ∈ Rel"
and cSym': "⋀Ψ' S T. (Ψ', S, T) ∈ Rel' ⟹ (Ψ', T, S) ∈ Rel'"
and ParPres: "⋀Ψ' S T U. (Ψ', S, T) ∈ Rel ⟹ (Ψ', S ∥ U, T ∥ U) ∈ Rel"
and ParPres2: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ (Ψ', S ∥ S, T ∥ T) ∈ Rel"
and ParPres': "⋀Ψ' S T U. (Ψ', S, T) ∈ Rel' ⟹ (Ψ', U ∥ S, U ∥ 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"
using ‹eqvt Rel''›
proof(induct rule: weakSimI[where C="()"])
case(cAct Ψ' α RQ')
from ‹bn α ♯* (R ∥ !P)› ‹bn α ♯* (R ∥ !Q)› have "bn α ♯* P" and "bn α ♯* (!Q)" and "bn α ♯* Q" and "bn α ♯* R"
by simp+
from ‹Ψ ⊳ R ∥ !Q ⟼α ≺ RQ'› ‹bn α ♯* Ψ› ‹bn α ♯* R› ‹bn α ♯* !Q› ‹bn α ♯* subject α› ‹α ≠ τ› show ?case
proof(induct rule: parCases[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'› ‹bn α ♯* Ψ› ‹bn α ♯* P›
have "Ψ ⊳ R ∥ !P ⟼α ≺ (R' ∥ !P)" by(rule_tac Par1) (assumption | simp)+
hence "Ψ : R ∥ !Q ⊳ R ∥ !P ⟹α ≺ R' ∥ !P" by(rule_tac transitionWeakTransition) auto
moreover have "Ψ ⊗ Ψ' ⊳ R' ∥ !P ⟹⇧^⇩τ R' ∥ !P" by auto
moreover from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ', P, Q) ∈ Rel" by(rule cExt)
hence "(Ψ ⊗ Ψ', 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 ♯* Ψ'" and "A⇩R ♯* R" by simp+
have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
with ‹bn α ♯* R› ‹A⇩R ♯* α› have "bn α ♯* Ψ⇩R" by(auto dest: extractFrameFreshChain)
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› ‹bn α ♯* Q› ‹α ≠ τ› ‹bn α ♯* subject α›
obtain T where QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼α ≺ T" and "(𝟭, Q', T ∥ !Q) ∈ Rel'"
by(blast dest: rBangActE)
from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel" by(rule cExt)
with QTrans ‹bn α ♯* Ψ› ‹bn α ♯* Ψ⇩R› ‹bn α ♯* P› ‹α ≠ τ›
obtain P'' S where PTrans: "Ψ ⊗ Ψ⇩R : Q ⊳ P ⟹α ≺ P''"
and P''Chain: "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ S"
and SRelT: "((Ψ ⊗ Ψ⇩R) ⊗ Ψ', S, T) ∈ Rel"
by(blast dest: cSim weakSimE)
from PTrans have "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 : Q ⊳ P ⟹α ≺ P''"
by(metis weakTransitionStatEq Identity AssertionStatEqSym)
hence "Ψ ⊗ Ψ⇩R : Q ∥ !P ⊳ P ∥ !P ⟹α ≺ P'' ∥ !P" using ‹bn α ♯* P›
by(force intro: weakPar1)
hence "Ψ ⊗ Ψ⇩R : Q ∥ !P ⊳ !P ⟹α ≺ P'' ∥ !P" using ‹guarded P›
by(rule weakBang)
hence "Ψ : R ∥ (Q ∥ !P) ⊳ R ∥ !P ⟹α ≺ R ∥ (P'' ∥ !P)"
using FrR ‹bn α ♯* R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Q›‹A⇩R ♯* P› ‹A⇩R ♯* α› ‹A⇩R ♯* α›
by(rule_tac weakPar2) auto
moreover have "insertAssertion (extractFrame(R ∥ !Q)) Ψ ↪⇩F insertAssertion (extractFrame(R ∥ (Q ∥ !P))) Ψ"
proof -
have "insertAssertion (extractFrame(R ∥ !P)) Ψ = ⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ 𝟭⟩" using FrR ‹A⇩R ♯* Ψ›
by auto
moreover from ‹Ψ⇩Q ≃ 𝟭› have "⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ 𝟭⟩ ≃⇩F ⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩"
by(rule_tac frameResChainPres, auto) (metis Identity compositionSym AssertionStatEqTrans AssertionStatEqSym)
moreover have "⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩ ≃⇩F ⦇ν*A⇩Q⦈(⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩)" using ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩Q ♯* A⇩R› freshCompChain
by(subst frameResFreshChain[where xvec=A⇩Q, THEN FrameStatEqSym]) auto
moreover have "⦇ν*A⇩Q⦈(⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩) ≃⇩F ⦇ν*A⇩R⦈(⟨A⇩Q, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩)"
by(rule frameResChainComm)
moreover have "insertAssertion (extractFrame(R ∥ (Q ∥ !P))) Ψ = ⟨(A⇩R@A⇩Q), Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩"
using FrR FrQ ‹A⇩R ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* A⇩R› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩R ♯* Ψ⇩Q› freshCompChain
by auto
ultimately have "insertAssertion (extractFrame(R ∥ !P)) Ψ ≃⇩F insertAssertion (extractFrame(R ∥ (Q ∥ !P))) Ψ"
by(auto simp add: frameChainAppend) (blast dest: FrameStatEqTrans)
thus ?thesis by(simp add: FrameStatEq_def)
qed
ultimately have "Ψ : R ∥ !Q ⊳ R ∥ !P ⟹α ≺ R ∥ (P'' ∥ !P)"
by(rule weakTransitionFrameImp)
moreover from PTrans ‹A⇩R ♯* P› ‹A⇩R ♯* α› ‹bn α ♯* subject α› ‹distinct(bn α)›
have "A⇩R ♯* P''" by(force dest: weakFreshChainDerivative)
with P''Chain have "A⇩R ♯* S" by(force dest: tauChainFreshChain)
from ‹Ψ ⊗ Ψ⇩R ⊳ Q ⟼α ≺ T› ‹A⇩R ♯* Q› ‹A⇩R ♯* α› ‹bn α ♯* subject α› ‹distinct(bn α)› have "A⇩R ♯* T"
by(force dest: freeFreshChainDerivative)
from P''Chain have "((Ψ ⊗ Ψ') ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P'' ⟹⇧^⇩τ S"
by(rule tauChainStatEq) (metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym Identity)
hence "(Ψ ⊗ Ψ') ⊗ Ψ⇩R ⊳ P'' ∥ !P ⟹⇧^⇩τ S ∥ !P"
by(rule_tac tauChainPar1) auto
hence "Ψ ⊗ Ψ' ⊳ R ∥ (P'' ∥ !P) ⟹⇧^⇩τ R ∥ (S ∥ !P)" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ'› ‹A⇩R ♯* P''› ‹A⇩R ♯* P›
by(rule_tac tauChainPar2) auto
moreover have "(Ψ ⊗ Ψ', R ∥ (S ∥ !P), R ∥ Q') ∈ Rel''"
proof -
from ‹((Ψ ⊗ Ψ⇩R) ⊗ Ψ', S, T) ∈ Rel› have "((Ψ ⊗ Ψ') ⊗ Ψ⇩R, S, T) ∈ Rel"
by(rule StatEq) (metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym)
with FrR ‹A⇩R ♯* Ψ› ‹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)
moreover from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ', P, Q) ∈ Rel" by(rule cExt)
hence "(Ψ ⊗ Ψ', (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
from ‹τ ≠ τ› have False by simp
thus ?case by simp
next
case cComm2
from ‹τ ≠ τ› have False by simp
thus ?case by simp
qed
next
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› ‹guarded P› ‹guarded Q› have "(Ψ, R' ∥ !P, R' ∥ !Q) ∈ Rel''"
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 ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel" by(rule cExt)
hence "(Ψ ⊗ Ψ⇩R, P ∥ P, Q ∥ Q) ∈ Rel" by(rule ParPres2)
with QTrans
obtain S where PTrans: "Ψ ⊗ Ψ⇩R ⊳ P ∥ P ⟹⇧^⇩τ S" and SRelT: "(Ψ ⊗ Ψ⇩R, S, T) ∈ Rel"
by(blast dest: cSim weakSimE)
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: tauChainFreshChain)
from ‹Ψ ⊗ Ψ⇩R ⊳ !P ⟹⇧^⇩τ U› FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› have "Ψ ⊳ R ∥ !P ⟹⇧^⇩τ R ∥ U"
by(rule_tac tauChainPar2) auto
moreover from PTrans ‹A⇩R ♯* P› have "A⇩R ♯* S" by(force dest: tauChainFreshChain)
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 tauActTauChain)
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 tauActTauChain) 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 tauActTauChain)
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 tauActTauChain) 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