Theory Weak_Cong_Struct_Cong
theory Weak_Cong_Struct_Cong
imports Weak_Cong_Pres Weak_Bisim_Struct_Cong
begin
context env begin
lemma weakPsiCongParComm:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
shows "Ψ ⊳ P ∥ Q ≐ Q ∥ P"
by(metis bisimParComm strongBisimWeakPsiCong)
lemma weakPsiCongResComm:
fixes x :: name
and Ψ :: 'b
and y :: name
and P :: "('a, 'b, 'c) psi"
assumes "x ♯ Ψ"
and "y ♯ Ψ"
shows "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ≐ ⦇νy⦈(⦇νx⦈P)"
using assms
by(metis bisimResComm strongBisimWeakPsiCong)
lemma weakPsiCongResComm':
fixes x :: name
and Ψ :: 'b
and xvec :: "name list"
and P :: "('a, 'b, 'c) psi"
assumes "x ♯ Ψ"
and "xvec ♯* Ψ"
shows "Ψ ⊳ ⦇νx⦈(⦇ν*xvec⦈P) ≐ ⦇ν*xvec⦈(⦇νx⦈P)"
using assms
by(metis bisimResComm' strongBisimWeakPsiCong)
lemma weakPsiCongScopeExt:
fixes x :: name
and Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
assumes "x ♯ Ψ"
and "x ♯ P"
shows "Ψ ⊳ ⦇νx⦈(P ∥ Q) ≐ P ∥ ⦇νx⦈Q"
using assms
by(metis bisimScopeExt strongBisimWeakPsiCong)
lemma weakPsiCongScopeExtChain:
fixes xvec :: "name list"
and Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
assumes "xvec ♯* Ψ"
and "xvec ♯* P"
shows "Ψ ⊳ ⦇ν*xvec⦈(P ∥ Q) ≐ P ∥ (⦇ν*xvec⦈Q)"
using assms
by(metis bisimScopeExtChain strongBisimWeakPsiCong)
lemma weakPsiCongParAssoc:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
shows "Ψ ⊳ (P ∥ Q) ∥ R ≐ P ∥ (Q ∥ R)"
by(metis bisimParAssoc strongBisimWeakPsiCong)
lemma weakPsiCongParNil:
fixes P :: "('a, 'b, 'c) psi"
shows "Ψ ⊳ P ∥ 𝟬 ≐ P"
by(metis bisimParNil strongBisimWeakPsiCong)
lemma weakPsiCongResNil:
fixes x :: name
and Ψ :: 'b
assumes "x ♯ Ψ"
shows "Ψ ⊳ ⦇νx⦈𝟬 ≐ 𝟬"
using assms
by(metis bisimResNil strongBisimWeakPsiCong)
lemma weakPsiCongOutputPushRes:
fixes x :: name
and Ψ :: 'b
and M :: 'a
and N :: 'a
and P :: "('a, 'b, 'c) psi"
assumes "x ♯ Ψ"
and "x ♯ M"
and "x ♯ N"
shows "Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ≐ M⟨N⟩.⦇νx⦈P"
using assms
by(metis bisimOutputPushRes strongBisimWeakPsiCong)
lemma weakPsiCongInputPushRes:
fixes x :: name
and Ψ :: 'b
and M :: 'a
and xvec :: "name list"
and N :: 'a
and P :: "('a, 'b, 'c) psi"
assumes "x ♯ Ψ"
and "x ♯ M"
and "x ♯ xvec"
and "x ♯ N"
shows "Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ≐ M⦇λ*xvec N⦈.⦇νx⦈P"
using assms
by(metis bisimInputPushRes strongBisimWeakPsiCong)
lemma weakPsiCongCasePushRes:
fixes x :: name
and Ψ :: 'b
and Cs :: "('c × ('a, 'b, 'c) psi) list"
assumes "x ♯ Ψ"
and "x ♯ (map fst Cs)"
shows "Ψ ⊳ ⦇νx⦈(Cases Cs) ≐ Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
using assms
by(metis bisimCasePushRes strongBisimWeakPsiCong)
lemma weakBangExt:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
assumes "guarded P"
shows "Ψ ⊳ !P ≐ P ∥ !P"
using assms
by(metis bangExt strongBisimWeakPsiCong)
lemma weakPsiCongParSym:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes "∀Ψ. Ψ ⊳ P ≐ Q"
shows "Ψ ⊳ R ∥ P ≐ R ∥ Q"
using assms
by(metis weakPsiCongParComm weakPsiCongParPres weakPsiCongTransitive)
lemma weakPsiCongScopeExtSym:
fixes x :: name
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
assumes "x ♯ Ψ"
and "x ♯ Q"
shows "Ψ ⊳ ⦇νx⦈(P ∥ Q) ≐ (⦇νx⦈P) ∥ Q"
using assms
by(metis weakPsiCongScopeExt weakPsiCongTransitive weakPsiCongParComm weakPsiCongE weakPsiCongResPres)
lemma weakPsiCongScopeExtChainSym:
fixes xvec :: "name list"
and Q :: "('a, 'b, 'c) psi"
and P :: "('a, 'b, 'c) psi"
assumes "xvec ♯* Ψ"
and "xvec ♯* Q"
shows "Ψ ⊳ ⦇ν*xvec⦈(P ∥ Q) ≐ (⦇ν*xvec⦈P) ∥ Q"
using assms
by(induct xvec) (auto intro: weakPsiCongScopeExtSym weakPsiCongReflexive weakPsiCongTransitive weakPsiCongResPres)
lemma weakPsiCongParPresSym:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes "⋀Ψ. Ψ ⊳ P ≐ Q"
shows "Ψ ⊳ R ∥ P ≐ R ∥ Q"
using assms
by(metis weakPsiCongParComm weakPsiCongParPres weakPsiCongTransitive)
lemma tauCongChainBangI:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and P' :: "('a, 'b, 'c) psi"
assumes "Ψ ⊳ P ∥ P ⟹⇩τ P'"
and "guarded P"
obtains Q where "Ψ ⊳ !P ⟹⇩τ Q" and "Ψ ⊳ Q ∼ P' ∥ !P"
proof -
assume "⋀Q. ⟦Ψ ⊳ !P ⟹⇩τ Q; Ψ ⊳ Q ∼ P' ∥ !P⟧ ⟹ thesis"
moreover from ‹Ψ ⊳ P ∥ P ⟹⇩τ P'› have "∃Q. Ψ ⊳ !P ⟹⇩τ Q ∧ Ψ ⊳ Q ∼ P' ∥ !P"
proof(induct x1=="P ∥ P" P' rule: tauStepChainInduct)
case(TauBase R')
from ‹Ψ ⊳ P ∥ P ⟼τ ≺ R'›
obtain Q where "Ψ ⊳ !P ⟼τ ≺ Q" and "Q ∼ R' ∥ !P" using ‹guarded P›
by(rule tauBangI)
from ‹Ψ ⊳ !P ⟼τ ≺ Q› have "Ψ ⊳ !P ⟹⇩τ Q" by auto
moreover from ‹Q ∼ R' ∥ !P› have "Ψ ⊳ Q ∼ R' ∥ !P"
apply(drule_tac bisimE(3)[where Ψ'=Ψ])
by(rule_tac statEqBisim, assumption) (metis Identity AssertionStatEqSym AssertionStatEqTrans Commutativity)
ultimately show ?case by blast
next
case(TauStep R' R'')
then obtain Q where PChain: "Ψ ⊳ !P ⟹⇩τ Q" and "Ψ ⊳ Q ∼ R' ∥ !P" by auto
from ‹Ψ ⊳ R' ⟼τ ≺ R''› have "Ψ ⊗ 𝟭 ⊳ R' ⟼τ ≺ R''" by(rule statEqTransition) (metis Identity AssertionStatEqSym)
hence "Ψ ⊳ R' ∥ !P ⟼τ ≺ R'' ∥ !P" by(rule_tac Par1) auto
with ‹Ψ ⊳ Q ∼ R' ∥ !P› obtain Q' where QTrans: "Ψ ⊳ Q ⟼τ ≺ Q'" and "Ψ ⊳ Q' ∼ R'' ∥ !P"
by(force dest: bisimE(2) simE)
from PChain QTrans have "Ψ ⊳ !P ⟹⇩τ Q'" by(auto dest: tauActTauStepChain)
thus ?case using ‹Ψ ⊳ Q' ∼ R'' ∥ !P› by blast
qed
ultimately show ?thesis by blast
qed
lemma weakPsiCongBangPres:
fixes Ψ :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
assumes PeqQ: "∀Ψ. Ψ ⊳ P ≐ Q"
and "guarded P"
and "guarded Q"
shows "Ψ ⊳ !P ≐ !Q"
proof -
from assms have "(∀Ψ. Ψ ⊳ P ≐ Q) ∧ guarded P ∧ guarded Q" by auto
hence "Ψ ⊳ 𝟬 ∥ !P ≐ 𝟬 ∥ !Q"
proof(induct rule: weakPsiCongSymI[where C="λP. 𝟬 ∥ !P"])
case(cSym P Q)
thus ?case by(auto dest: weakPsiCongSym)
next
case(cWeakBisim P Q)
thus ?case by(metis weakPsiCongE weakBisimBangPresAux)
next
case(cSim P Q)
then have "∀Ψ. Ψ ⊳ P ≐ Q" and "guarded P" and "guarded Q" by auto
moreover hence "Ψ ⊳ P ≈ Q" by(metis weakPsiCongE weakBisimE)
moreover have "⋀Ψ P Q. (∀Ψ. (Ψ ⊳ P ≐ Q)) ⟹ Ψ ⊳ P ↝«weakBisim» Q"
by(blast dest: weakPsiCongE)
moreover note weakBisimClosed bisimClosed weakBisimE(3) bisimE(3) weakBisimE(2)
weakBisimE(4) bisimE(4) statEqWeakBisim statEqBisim weakBisimTransitive bisimTransitive weakBisimParAssoc[THEN weakBisimE(4)]
bisimParAssoc[THEN bisimE(4)] weakBisimParPres
moreover have "⋀P Q. ∀Ψ. Ψ ⊳ P ≐ Q ⟹ ∀Ψ. Ψ ⊳ P ∥ P ≐ Q ∥ Q"
by(metis weakPsiCongParPres weakPsiCongParComm weakPsiCongSym weakPsiCongTransitive)
moreover note bisimParPresSym
moreover from strongBisimWeakBisim have "bisim ⊆ weakBisim" by auto
moreover have "⋀Ψ Ψ⇩R P Q R A⇩R. ⟦Ψ ⊗ Ψ⇩R ⊳ P ≈ Q; extractFrame R = ⟨A⇩R, Ψ⇩R⟩; A⇩R ♯* Ψ; A⇩R ♯* P; A⇩R ♯* Q⟧ ⟹ Ψ ⊳ R ∥ P ≈ R ∥ Q"
by(metis weakBisimParComm weakBisimTransitive weakBisimParPresAux)
moreover note weakBisimResChainPres bisimResChainPres weakBisimScopeExtChainSym bisimScopeExtChainSym
moreover have "⋀Ψ P R S Q. ⟦Ψ ⊳ P ≈ R; Ψ ⊳ R ≈ S; Ψ ⊳ S ∼ Q⟧ ⟹ Ψ ⊳ P ≈ Q"
by(blast dest: weakBisimTransitive strongBisimWeakBisim)
moreover note weakBisimBangPresAux
moreover from bangActE have "⋀Ψ P α P'. ⟦Ψ ⊳ !P ⟼α ≺ P'; bn α ♯* P; guarded P; α ≠ τ; bn α ♯* subject α⟧ ⟹ ∃Q. Ψ ⊳ P ⟼α ≺ Q ∧ P' ∼ Q ∥ !P"
by blast
moreover from bangTauE have "⋀Ψ P P'. ⟦Ψ ⊳ !P ⟼τ ≺ P'; guarded P⟧ ⟹ ∃Q. Ψ ⊳ P ∥ P ⟼τ ≺ Q ∧ P' ∼ Q ∥ !P"
by blast
moreover from tauCongChainBangI have "⋀Ψ P P'. ⟦Ψ ⊳ P ∥ P ⟹⇩τ P'; guarded P⟧ ⟹ ∃Q. Ψ ⊳ !P ⟹⇩τ Q ∧ Ψ ⊳ Q ∼ P' ∥ !P"
by blast
ultimately show ?case
by(rule_tac weakCongSimBangPres[where Rel=weakBisim and Rel'=bisim and Rel''=weakBisim and Eq="λP Q. ∀Ψ. Ψ ⊳ P ≐ Q"])
qed
thus ?thesis
by(metis weakPsiCongParNil weakPsiCongParComm weakPsiCongTransitive weakPsiCongSym)
qed
end
end