Theory Weak_Bisim_Struct_Cong

(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Bisim_Struct_Cong
  imports Weak_Bisim_Pres Bisim_Struct_Cong
begin

context env begin

lemma weakBisimParComm:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  
  shows "Ψ ⊳ P ∥ Q ≈ Q ∥ P"
by(metis bisimParComm strongBisimWeakBisim)

lemma weakBisimResComm:
  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 strongBisimWeakBisim)

lemma weakBisimResComm':
  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' strongBisimWeakBisim)

lemma weakBisimScopeExt:
  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 strongBisimWeakBisim)

lemma weakBisimScopeExtChain:
  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 strongBisimWeakBisim)

lemma weakBisimParAssoc:
  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 strongBisimWeakBisim)

lemma weakBisimParNil:
  fixes P :: "('a, 'b, 'c) psi"

  shows "Ψ ⊳ P ∥ 𝟬 ≈ P"
by(metis bisimParNil strongBisimWeakBisim)

lemma weakBisimResNil:
  fixes x :: name
  and   Ψ :: 'b
  
  assumes "x ♯ Ψ"

  shows "Ψ ⊳ ⦇νx⦈𝟬 ≈ 𝟬"
using assms
by(metis bisimResNil strongBisimWeakBisim)

lemma weakBisimOutputPushRes:
  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 strongBisimWeakBisim)

lemma weakBisimInputPushRes:
  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 strongBisimWeakBisim)

lemma weakBisimCasePushRes:
  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 strongBisimWeakBisim)

lemma weakBangExt:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  
  assumes "guarded P"

  shows "Ψ ⊳ !P ≈ P ∥ !P"
using assms
by(metis bangExt strongBisimWeakBisim)

lemma weakBisimParSym:
  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 weakBisimParComm weakBisimParPres weakBisimTransitive)

lemma weakBisimScopeExtSym:
  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 weakBisimScopeExt weakBisimTransitive weakBisimParComm weakBisimE weakBisimResPres)

lemma weakBisimScopeExtChainSym:
  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: weakBisimScopeExtSym weakBisimReflexive weakBisimTransitive weakBisimResPres)

lemma weakBisimParPresAuxSym:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊗ Ψ⇩R ⊳ P ≈ Q"
  and     "extractFrame R = ⟨A⇩R, Ψ⇩R⟩"
  and     "A⇩R ♯* Ψ"
  and     "A⇩R ♯* P"
  and     "A⇩R ♯* Q"

  shows "Ψ ⊳ R ∥ P ≈ R ∥ Q"
using assms
by(metis weakBisimParComm weakBisimParPresAux weakBisimTransitive)

lemma weakBisimParPresSym:
  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 weakBisimParComm weakBisimParPres weakBisimTransitive)

lemma guardedFrameStatEq:
  fixes P :: "('a, 'b, 'c) psi"

  assumes "guarded P"

  shows "extractFrame P ≃⇩F ⟨ε, 𝟭⟩"
proof -
  obtain A⇩P Ψ⇩P where FrR: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩"
    by(rule freshFrame)

  with ‹guarded P› have "Ψ⇩P ≃ 𝟭" and "((supp Ψ⇩P)::name set) = {}"
    by(metis guardedStatEq)+
  from ‹supp Ψ⇩P = {}› have "A⇩P ♯* Ψ⇩P" by(auto simp add: fresh_star_def fresh_def)
  hence "⟨A⇩P, Ψ⇩P⟩ ≃⇩F ⟨[], Ψ⇩P⟩" by(force intro: frameResFreshChain)
  moreover from ‹Ψ⇩P ≃ 𝟭› have  "⟨[], Ψ⇩P⟩ ≃⇩F ⟨[], 𝟭⟩"
    by(simp add: FrameStatEq_def FrameStatImp_def AssertionStatEq_def AssertionStatImp_def)
  ultimately show ?thesis using FrR by(rule_tac FrameStatEqTrans) auto
qed

lemma guardedInsertAssertion:
  fixes P :: "('a, 'b, 'c) psi"
  and   Ψ :: 'b

  assumes "guarded P"

  shows "insertAssertion (extractFrame P) Ψ ≃⇩F ⟨ε, Ψ⟩"
proof -
  obtain A⇩P Ψ⇩P where FrR: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ"
    by(rule freshFrame)

  with ‹guarded P› have "Ψ⇩P ≃ 𝟭" and "((supp Ψ⇩P)::name set) = {}"
    by(metis guardedStatEq)+
  from ‹supp Ψ⇩P = {}› have "A⇩P ♯* Ψ⇩P" by(auto simp add: fresh_star_def fresh_def)
  hence "⟨A⇩P, Ψ ⊗ Ψ⇩P⟩ ≃⇩F ⟨[], Ψ ⊗ Ψ⇩P⟩" using ‹A⇩P ♯* Ψ› by(force intro: frameResFreshChain)
  moreover from ‹Ψ⇩P ≃ 𝟭› have  "⟨ε, Ψ ⊗ Ψ⇩P⟩ ≃⇩F ⟨ε, Ψ ⊗ 𝟭⟩" by(force intro: compositionSym)
  moreover have "⟨ε, Ψ ⊗ 𝟭⟩ ≃⇩F ⟨ε, Ψ⟩" by(force intro: Identity)
  ultimately show ?thesis using FrR ‹A⇩P ♯* Ψ›
    by(force intro: FrameStatEqTrans AssertionStatEqTrans)
qed

lemma insertDoubleAssertionStatEq':
  fixes F  :: "'b frame"
  and   Ψ  :: 'b
  and   Ψ' :: 'b

  shows "insertAssertion(insertAssertion F Ψ) Ψ' ≃⇩F (insertAssertion F) (Ψ' ⊗ Ψ)"
proof -
  obtain A⇩F Ψ⇩F where "F = ⟨A⇩F, Ψ⇩F⟩" and "A⇩F ♯* Ψ" and "A⇩F ♯* Ψ'" and "A⇩F ♯* (Ψ' ⊗ Ψ)"
    by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto
  thus ?thesis
    by auto (metis frameIntAssociativity FrameStatEqSym)
qed

lemma bangActE:
  assumes "Ψ ⊳ !P ⟼α ≺ P'"
  and     "bn α ♯* subject α"
  and     "guarded P"
  and     "α ≠ τ"
  and     "bn α ♯* P"

  obtains Q where "Ψ ⊳ P ⟼α ≺ Q" and "P' ∼ Q ∥ !P"
proof -
  assume "⋀Q. ⟦Ψ ⊳ P ⟼α ≺ Q; P' ∼ Q ∥ !P⟧ ⟹ thesis"
  moreover from ‹Ψ ⊳ !P ⟼α ≺ P'› ‹bn α ♯* subject α› ‹α ≠ τ› ‹bn α ♯* P›  have "∃Q. Ψ ⊳ P ⟼α ≺ Q ∧ P' ∼ Q ∥ !P"
  proof(nominal_induct rule: bangInduct')
    case(cAlpha α P' p)
    then obtain Q where "Ψ ⊳ P ⟼α ≺ Q" and "P' ∼ Q ∥ (P ∥ !P)" by fastforce
    from ‹Ψ ⊳ P ⟼α ≺ Q› have "distinct(bn α)" by(rule boundOutputDistinct)
    have S: "set p ⊆ set(bn α) × set(bn(p ∙ α))" by fact
    from ‹Ψ ⊳ P ⟼α ≺ Q› ‹bn(p ∙ α) ♯* α› ‹bn(p ∙ α) ♯* P› ‹bn α ♯* subject α› ‹distinct(bn α)›
    have "bn(p ∙ α) ♯* Q" by(force dest: freeFreshChainDerivative)
    with ‹Ψ ⊳ P ⟼α ≺ Q› ‹bn(p ∙ α) ♯* α› S ‹bn α ♯* subject α› ‹distinct(bn α)› have "Ψ ⊳ P ⟼(p ∙ α) ≺ (p ∙ Q)"
      by(fastforce simp add: residualAlpha)
    moreover from ‹P' ∼ Q ∥ (P ∥ !P)› have "(p ∙ 𝟭) ⊳ (p ∙ P') ∼ (p ∙ (Q ∥ (P ∥ !P)))"
      by(rule bisimClosed)
    with ‹(bn α) ♯* P› ‹bn(p ∙ α) ♯* P› S have "(p ∙ P') ∼ (p ∙ Q) ∥ (P ∥ !P)"
      by(simp add: eqvts)
    ultimately show ?case by blast
  next
    case(cPar1 α P')
    from ‹guarded P› have "P' ∥ !P ∼ P' ∥ (P ∥ !P)" by(metis bangExt bisimParPresSym)
    with ‹Ψ ⊳ P ⟼α ≺ P'› show ?case by blast
  next
    case(cPar2 α P')
    then obtain Q where PTrans: "Ψ ⊳ P ⟼α ≺ Q" and "P' ∼ Q ∥ !P" by blast
    from ‹P' ∼ Q ∥ !P› have "P ∥ P' ∼ Q ∥ (P ∥ !P)"
      by(metis bisimParPresSym bisimParAssoc bisimTransitive bisimParComm)
    with PTrans 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
  next
    case(cBang α P')
    then obtain Q where PTrans: "Ψ ⊳ P ⟼α ≺ Q" and "P' ∼ Q ∥ (P ∥ !P)" by blast
    from ‹P' ∼ Q ∥ (P ∥ !P)› ‹guarded P› have "P' ∼ Q ∥ !P" by(metis bisimTransitive bisimParPresSym bangExt bisimSymmetric)
    with PTrans show ?case by blast
  qed
  ultimately show ?thesis by blast
qed

lemma bangTauE:
  assumes "Ψ ⊳ !P ⟼τ ≺ P'"
  and     "guarded P"

  obtains Q where "Ψ ⊳ P ∥ P ⟼τ ≺ Q" and "P' ∼ Q ∥ !P"
using assms
proof -
  assume "⋀Q. ⟦Ψ ⊳ P ∥ P⟼τ ≺ Q; P' ∼ Q ∥ !P⟧ ⟹ thesis"
  moreover from assms have "∃Q. Ψ ⊳ P ∥ P ⟼τ ≺ Q ∧ P' ∼ Q ∥ !P"
  proof(nominal_induct rule: bangTauInduct)
    case(cPar1 P')
    obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "A⇩P ♯* P"
      by(rule_tac C="(Ψ, P)" in freshFrame) auto
    from ‹guarded P› FrP have "Ψ⇩P ≃ 𝟭" by(drule_tac guardedStatEq) auto
    with ‹Ψ ⊳ P ⟼τ ≺ P'› have "Ψ ⊗ Ψ⇩P ⊳ P ⟼τ ≺ P'"
      by(rule_tac statEqTransition, auto) (metis Identity AssertionStatEqSym compositionSym AssertionStatEqTrans)
    hence "Ψ ⊳ P ∥ P ⟼τ ≺ P' ∥ P" using FrP ‹A⇩P ♯* Ψ› ‹A⇩P ♯* P› by(rule_tac Par1) auto 
    moreover from ‹guarded P› have "P' ∥ !P ∼ (P' ∥ P) ∥ (P ∥ !P)"
      by(metis bisimParPresSym bisimParAssoc bisimTransitive bisimParComm bangExt)
    ultimately show ?case by blast
  next
    case(cPar2 P')
    then obtain n Q where PTrans: "Ψ ⊳ P ∥ P ⟼τ ≺ Q" and "P' ∼ Q ∥ !P" by blast
    from ‹P' ∼ Q ∥ !P› have "P ∥ P' ∼ Q ∥ (P ∥ !P)"
      by(metis bisimParPresSym bisimParAssoc bisimTransitive bisimParComm)
    with PTrans show ?case by blast
  next
    case(cComm1 M N P' K xvec P'')
    obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "A⇩P ♯* P" and "A⇩P ♯* M"
      by(rule_tac C="(Ψ, P, M)" in freshFrame) auto
    from ‹guarded P› FrP have "Ψ⇩P ≃ 𝟭" by(drule_tac guardedStatEq) auto
    obtain A⇩P' Ψ⇩P' where FrP': "extractFrame P = ⟨A⇩P', Ψ⇩P'⟩" and "A⇩P' ♯* Ψ" and "A⇩P' ♯* P" and "A⇩P' ♯* K" and "A⇩P' ♯* A⇩P"
      by(rule_tac C="(Ψ, P, K, A⇩P)" in freshFrame) auto
    from ‹guarded P› FrP' have "Ψ⇩P' ≃ 𝟭" by(drule_tac guardedStatEq) auto
    with ‹Ψ ⊳ P ⟼M⦇N⦈ ≺ P'› have "Ψ ⊗ Ψ⇩P' ⊳ P ⟼M⦇N⦈ ≺ P'"
      by(rule_tac statEqTransition, auto) (metis Identity AssertionStatEqSym compositionSym AssertionStatEqTrans)
    moreover from ‹Ψ ⊳ !P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P''› ‹guarded P› ‹xvec ♯* P› ‹xvec ♯* K›
    obtain Q where PTrans: "Ψ ⊳ P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q" and "P'' ∼ Q ∥ !P" 
      by(drule_tac bangActE) auto
    from PTrans ‹Ψ⇩P ≃ 𝟭› have "Ψ ⊗ Ψ⇩P ⊳ P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q"
      by(rule_tac statEqTransition, auto) (metis Identity AssertionStatEqSym compositionSym AssertionStatEqTrans)
    moreover from ‹Ψ ⊢ M ↔ K› ‹Ψ⇩P ≃ 𝟭› ‹Ψ⇩P' ≃ 𝟭› have "Ψ ⊗ Ψ⇩P ⊗ Ψ⇩P' ⊢ M ↔ K"
      by(rule_tac statEqEnt, auto) (metis Identity AssertionStatEqSym compositionSym AssertionStatEqTrans)
    ultimately have "Ψ ⊳ P ∥ P ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ Q)" using FrP FrP' ‹A⇩P ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩P ♯* M› ‹A⇩P' ♯* Ψ› ‹A⇩P' ♯* P› ‹A⇩P' ♯* K› ‹A⇩P' ♯* A⇩P› ‹xvec ♯* P›
      by(rule_tac Comm1) (assumption | simp)+
    moreover from ‹P'' ∼ Q ∥ !P› ‹guarded P› have "P' ∥ P'' ∼ (P' ∥ Q) ∥ (P ∥ !P)"
      by(metis bisimTransitive bangExt bisimParPresSym bisimParAssoc bisimSymmetric) 
    hence "⦇ν*xvec⦈(P' ∥ P'') ∼ ⦇ν*xvec⦈((P' ∥ Q) ∥ (P ∥ !P))" by(rule_tac bisimResChainPres) auto
    with ‹xvec ♯* P› ‹xvec ♯* Ψ› have "⦇ν*xvec⦈(P' ∥ P'') ∼ (⦇ν*xvec⦈(P' ∥ Q)) ∥ (P ∥ !P)"
      by(force intro: bisimTransitive bisimScopeExtChainSym)
    ultimately show ?case by blast
  next
    case(cComm2 M N P' K xvec P'')
    obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "A⇩P ♯* P" and "A⇩P ♯* M"
      by(rule_tac C="(Ψ, P, M)" in freshFrame) auto
    from ‹guarded P› FrP have "Ψ⇩P ≃ 𝟭" by(drule_tac guardedStatEq) auto
    obtain A⇩P' Ψ⇩P' where FrP': "extractFrame P = ⟨A⇩P', Ψ⇩P'⟩" and "A⇩P' ♯* Ψ" and "A⇩P' ♯* P" and "A⇩P' ♯* K" and "A⇩P' ♯* A⇩P"
      by(rule_tac C="(Ψ, P, K, A⇩P)" in freshFrame) auto
    from ‹guarded P› FrP' have "Ψ⇩P' ≃ 𝟭" by(drule_tac guardedStatEq) auto
    with ‹Ψ ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'› have "Ψ ⊗ Ψ⇩P' ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
      by(rule_tac statEqTransition, auto) (metis Identity AssertionStatEqSym compositionSym AssertionStatEqTrans)
    moreover from ‹Ψ ⊳ !P ⟼K⦇N⦈ ≺ P''› ‹guarded P›
    obtain Q where PTrans: "Ψ ⊳ P ⟼K⦇N⦈ ≺ Q" and "P'' ∼ Q ∥ !P" by(rule_tac bangActE) auto
    from PTrans ‹Ψ⇩P ≃ 𝟭› have "Ψ ⊗ Ψ⇩P ⊳ P ⟼K⦇N⦈ ≺ Q"
      by(rule_tac statEqTransition, auto) (metis Identity AssertionStatEqSym compositionSym AssertionStatEqTrans)
    moreover from ‹Ψ ⊢ M ↔ K› ‹Ψ⇩P ≃ 𝟭› ‹Ψ⇩P' ≃ 𝟭› have "Ψ ⊗ Ψ⇩P ⊗ Ψ⇩P' ⊢ M ↔ K"
      by(rule_tac statEqEnt, auto) (metis Identity AssertionStatEqSym compositionSym AssertionStatEqTrans)
    ultimately have "Ψ ⊳ P ∥ P ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ Q)" using FrP FrP' ‹A⇩P ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩P ♯* M› ‹A⇩P' ♯* Ψ› ‹A⇩P' ♯* P› ‹A⇩P' ♯* K› ‹A⇩P' ♯* A⇩P› ‹xvec ♯* P›
      by(rule_tac Comm2) (assumption | simp)+
    moreover from ‹P'' ∼ Q ∥ !P› ‹guarded P› have "P' ∥ P'' ∼ (P' ∥ Q) ∥ (P ∥ !P)"
      by(metis bisimTransitive bangExt bisimParPresSym bisimParAssoc bisimSymmetric) 
    hence "⦇ν*xvec⦈(P' ∥ P'') ∼ ⦇ν*xvec⦈((P' ∥ Q) ∥ (P ∥ !P))" by(rule_tac bisimResChainPres) auto
    with ‹xvec ♯* P› ‹xvec ♯* Ψ› have "⦇ν*xvec⦈(P' ∥ P'') ∼ (⦇ν*xvec⦈(P' ∥ Q)) ∥ (P ∥ !P)"
      by(force intro: bisimTransitive bisimScopeExtChainSym)
    ultimately show ?case by blast
  next
    case(cBang P')
    then obtain Q where PTrans: "Ψ ⊳ P ∥ P ⟼τ ≺ Q" and "P' ∼ Q ∥ (P ∥ !P)" by blast
    from ‹P' ∼ Q ∥ (P ∥ !P)› ‹guarded P› have "P' ∼ Q ∥ !P" by(metis bisimTransitive bisimParPresSym bangExt bisimSymmetric)
    with PTrans show ?case by blast
  qed
  ultimately show ?thesis by blast
qed

lemma tauBangI:
  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 rule: parTauCases[where C="()"])
    case(cPar1 P' A⇩P Ψ⇩P)
    from ‹Ψ ⊗ Ψ⇩P ⊳ P ⟼τ ≺ P'› have "(Ψ ⊗ Ψ⇩P) ⊗ 𝟭 ⊳ P ⟼τ ≺ P'" 
      by(rule statEqTransition) (metis Identity AssertionStatEqSym)
     hence "Ψ ⊗ Ψ⇩P ⊳ P ∥ !P ⟼τ ≺ P' ∥ !P" by(rule_tac Par1) auto
     hence "Ψ ⊗ Ψ⇩P ⊳ !P ⟼τ ≺ P' ∥ !P" using ‹guarded P› by(rule Bang)
     hence "Ψ ⊳ P ∥ !P ⟼τ ≺ P ∥ (P' ∥ !P)" using ‹extractFrame P = ⟨A⇩P, Ψ⇩P⟩› ‹A⇩P ♯* Ψ› ‹A⇩P ♯* P›
       by(rule_tac Par2) auto
     hence "Ψ ⊳ !P ⟼τ ≺ P ∥ (P' ∥ !P)" using ‹guarded P› by(rule Bang)
     moreover have "P ∥ (P' ∥ !P) ∼ P' ∥ P ∥ !P"
       by(metis bisimParAssoc bisimParComm bisimTransitive bisimSymmetric bisimParPres)
     ultimately show ?case by blast
   next
    case(cPar2 P' A⇩P Ψ⇩P)
    from ‹Ψ ⊗ Ψ⇩P ⊳ P ⟼τ ≺ P'› have "(Ψ ⊗ Ψ⇩P) ⊗ 𝟭 ⊳ P ⟼τ ≺ P'" 
      by(rule statEqTransition) (metis Identity AssertionStatEqSym)
     hence "Ψ ⊗ Ψ⇩P ⊳ P ∥ !P ⟼τ ≺ P' ∥ !P" by(rule_tac Par1) auto
     hence "Ψ ⊗ Ψ⇩P ⊳ !P ⟼τ ≺ P' ∥ !P" using ‹guarded P› by(rule Bang)
     hence "Ψ ⊳ P ∥ !P ⟼τ ≺ P ∥ (P' ∥ !P)" using ‹extractFrame P = ⟨A⇩P, Ψ⇩P⟩› ‹A⇩P ♯* Ψ› ‹A⇩P ♯* P›
       by(rule_tac Par2) auto
     hence "Ψ ⊳ !P ⟼τ ≺ P ∥ (P' ∥ !P)" using ‹guarded P› by(rule Bang)
     moreover have "P ∥ (P' ∥ !P) ∼ P ∥ P' ∥ !P"
       by(metis bisimParAssoc bisimSymmetric)
     ultimately show ?case by blast
   next
     case(cComm1 Ψ⇩P' M N P' A⇩P Ψ⇩P K xvec P'' A⇩P')
     from ‹extractFrame P = ⟨A⇩P', Ψ⇩P'⟩› ‹guarded P› have "Ψ⇩P' ≃ 𝟭" by(blast dest: guardedStatEq)
     with ‹Ψ ⊗ Ψ⇩P' ⊳ P ⟼M⦇N⦈ ≺ P'› have "Ψ ⊗ 𝟭 ⊳ P ⟼M⦇N⦈ ≺ P'"
       by(rule_tac statEqTransition, auto) (metis compositionSym AssertionStatEqSym)
     moreover note ‹extractFrame P = ⟨A⇩P, Ψ⇩P⟩›
     moreover from ‹Ψ ⊗ Ψ⇩P ⊳ P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P''› have "(Ψ ⊗ Ψ⇩P) ⊗ 𝟭 ⊳ P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P''"
       by(rule statEqTransition) (metis Identity AssertionStatEqSym)
     hence "Ψ ⊗ Ψ⇩P ⊳ P ∥ !P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ (P'' ∥ !P)" using ‹xvec ♯* P› by(force intro: Par1)
     hence "Ψ ⊗ Ψ⇩P ⊳ !P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ (P'' ∥ !P)" using ‹guarded P› by(rule Bang)
     moreover from ‹Ψ ⊗ Ψ⇩P ⊗ Ψ⇩P' ⊢ M ↔ K› ‹Ψ⇩P' ≃ 𝟭› have "Ψ ⊗ Ψ⇩P ⊗ 𝟭 ⊢ M ↔ K"
       by(rule_tac statEqEnt, auto) (metis compositionSym AssertionStatEqSym)
     ultimately have "Ψ ⊳ P ∥ !P ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ (P'' ∥ !P))"
       using ‹A⇩P ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩P ♯* M› ‹A⇩P ♯* A⇩P'› ‹A⇩P' ♯* Ψ› ‹A⇩P' ♯* P› ‹A⇩P' ♯* K› ‹xvec ♯* P›
       by(force intro: Comm1)
     hence "Ψ ⊳ !P ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ (P'' ∥ !P))" using ‹guarded P› by(rule Bang)
     moreover have "⦇ν*xvec⦈(P' ∥ (P'' ∥ !P)) ∼ (⦇ν*xvec⦈(P' ∥ P'')) ∥ !P" 
     proof -
       have "⦇ν*xvec⦈(P' ∥ (P'' ∥ !P)) ∼ ⦇ν*xvec⦈((P' ∥ P'') ∥ !P)"
         by(force intro: bisimResChainPres bisimParAssoc[THEN bisimSymmetric])
       moreover have "⦇ν*xvec⦈((P' ∥ P'') ∥ !P) ∼ (⦇ν*xvec⦈(P' ∥ P'')) ∥ !P" using ‹xvec ♯* P›
         by(rule_tac bisimScopeExtChainSym) auto
       ultimately show ?thesis by(rule bisimTransitive)
     qed
     ultimately show ?case by blast
   next
     case(cComm2 Ψ⇩P' M xvec N P' A⇩P Ψ⇩P K P'' A⇩P')
     from ‹extractFrame P = ⟨A⇩P', Ψ⇩P'⟩› ‹guarded P› have "Ψ⇩P' ≃ 𝟭" by(blast dest: guardedStatEq)
     with ‹Ψ ⊗ Ψ⇩P' ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩≺ P'› have "Ψ ⊗ 𝟭 ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
       by(rule_tac statEqTransition, auto) (metis compositionSym AssertionStatEqSym)
     moreover note ‹extractFrame P = ⟨A⇩P, Ψ⇩P⟩›
     moreover from ‹Ψ ⊗ Ψ⇩P ⊳ P ⟼K⦇N⦈ ≺ P''› have "(Ψ ⊗ Ψ⇩P) ⊗ 𝟭 ⊳ P ⟼K⦇N⦈ ≺ P''"
       by(rule statEqTransition) (metis Identity AssertionStatEqSym)
     hence "Ψ ⊗ Ψ⇩P ⊳ P ∥ !P ⟼K⦇N⦈ ≺ (P'' ∥ !P)" by(force intro: Par1)
     hence "Ψ ⊗ Ψ⇩P ⊳ !P ⟼K⦇N⦈ ≺ (P'' ∥ !P)" using ‹guarded P› by(rule Bang)
     moreover from ‹Ψ ⊗ Ψ⇩P ⊗ Ψ⇩P' ⊢ M ↔ K› ‹Ψ⇩P' ≃ 𝟭› have "Ψ ⊗ Ψ⇩P ⊗ 𝟭 ⊢ M ↔ K"
       by(rule_tac statEqEnt, auto) (metis compositionSym AssertionStatEqSym)
     ultimately have "Ψ ⊳ P ∥ !P ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ (P'' ∥ !P))"
       using ‹A⇩P ♯* Ψ› ‹A⇩P ♯* P› ‹A⇩P ♯* M› ‹A⇩P ♯* A⇩P'› ‹A⇩P' ♯* Ψ› ‹A⇩P' ♯* P› ‹A⇩P' ♯* K› ‹xvec ♯* P›
       by(force intro: Comm2)
     hence "Ψ ⊳ !P ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ (P'' ∥ !P))" using ‹guarded P› by(rule Bang)
     moreover have "⦇ν*xvec⦈(P' ∥ (P'' ∥ !P)) ∼ (⦇ν*xvec⦈(P' ∥ P'')) ∥ !P" 
     proof -
       have "⦇ν*xvec⦈(P' ∥ (P'' ∥ !P)) ∼ ⦇ν*xvec⦈((P' ∥ P'') ∥ !P)"
         by(force intro: bisimResChainPres bisimParAssoc[THEN bisimSymmetric])
       moreover have "⦇ν*xvec⦈((P' ∥ P'') ∥ !P) ∼ (⦇ν*xvec⦈(P' ∥ P'')) ∥ !P" using ‹xvec ♯* P›
         by(rule_tac bisimScopeExtChainSym) auto
       ultimately show ?thesis by(rule bisimTransitive)
     qed
     ultimately show ?case by blast
   qed
   ultimately show ?thesis by blast
qed

lemma tauChainBangI:
  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: tauChainInduct)
    case TauBase
    have "Ψ ⊳ !P ⟹⇧^⇩τ !P" by simp
    moreover have "Ψ ⊳ !P ∼ (P ∥ P) ∥ !P" using ‹guarded P›
      by(metis bisimParAssoc bisimTransitive bisimParPresSym bangExt bisimParComm)
    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: tauActTauChain)
    thus ?case using ‹Ψ ⊳ Q' ∼ R'' ∥ !P› by blast
  qed
  ultimately show ?thesis by blast
qed

lemma weakBisimBangPresAux:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ≈ Q"
  and     "guarded P"
  and     "guarded Q"

  shows   "Ψ ⊳ R ∥ !P ≈ R ∥ !Q"
proof -
  let ?X = "{(Ψ, R ∥ !P, R ∥ !Q) | Ψ R P Q. guarded P ∧ guarded Q ∧ Ψ ⊳ P ≈ Q}"
  let ?Y = "{(Ψ, P, Q) | Ψ P Q. ∃R S. Ψ ⊳ P ≈ R ∧ (Ψ, R, S) ∈ ?X ∧ Ψ ⊳ S ∼ Q}"

  from assms have "(Ψ, R ∥ !P, R ∥ !Q) ∈ ?X" by auto
  moreover have "eqvt ?X"
    by(fastforce simp add: eqvt_def intro: weakBisimClosed)
  ultimately show ?thesis
  proof(coinduct rule: weakTransitiveCoinduct2)
    case(cStatImp Ψ P Q)
    thus ?case by(force dest: weakBisimE(3) simp add: weakStatImp_def)
  next
    case(cSim Ψ P Q)
    moreover {
      fix Ψ P Q R
      assume "Ψ ⊳ P ≈ Q"
      moreover have "eqvt ?Y" 
        apply(auto simp add: eqvt_def)
        apply(rule_tac x="p ∙ (Ra ∥ !P)" in exI, auto)
        apply(fastforce dest: weakBisimClosed simp add: eqvts)
        apply(rule_tac x="(p ∙ Ra) ∥ !(p ∙ Q)" in exI, auto)
        apply(rule_tac x="p ∙ Ra" in exI)
        apply(rule_tac x="p ∙ P" in exI, auto)
        apply(rule_tac x="p ∙ Q" in exI, auto)
        apply(blast intro: weakBisimClosed)
        by(fastforce dest: bisimClosed simp add: eqvts)
      moreover assume "guarded P" and "guarded Q" 
      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 weakBisimParPres weakBisimParComm weakBisimE(4) weakBisimTransitive)
      moreover note bisimParPresSym
      moreover have "bisim ⊆ weakBisim" by(auto dest: strongBisimWeakBisim)
      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) ∈ ?Y; Ψ ⊳ S ∼ Q⟧ ⟹ (Ψ, P, Q) ∈ ?Y"
        by(blast dest: weakBisimTransitive bisimTransitive)
      moreover have "⋀Ψ P Q R. ⟦Ψ ⊳ P ≈ Q; guarded P; guarded Q⟧ ⟹ (Ψ, R ∥ !P, R ∥ !Q) ∈ ?Y"
        by(blast intro: bisimReflexive weakBisimReflexive)
      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 tauChainBangI have "⋀Ψ P P'. ⟦Ψ ⊳ P ∥ P ⟹⇧^⇩τ P'; guarded P⟧ ⟹ ∃Q. Ψ ⊳ !P ⟹⇧^⇩τ Q ∧ Ψ ⊳ Q ∼ P' ∥ !P"
        by blast
      ultimately have  "Ψ ⊳ R ∥ !P ↝<?Y> R ∥ !Q" 
        by(rule_tac weakSimBangPres)
    }
    ultimately show ?case by blast
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(blast dest: weakBisimE)
  next
    case(cSym Ψ P Q)
    thus ?case by(blast dest: weakBisimE)
  qed
qed


lemma weakBisimBangPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ≈ Q"
  and     "guarded P"
  and     "guarded Q"

  shows   "Ψ ⊳ !P ≈ !Q"
proof -
  from assms have "Ψ ⊳ 𝟬 ∥ !P ≈ 𝟬 ∥ !Q" by(rule weakBisimBangPresAux)
  thus ?thesis
    by(metis weakBisimParNil weakBisimParComm weakBisimTransitive weakBisimE(4))
qed

end

end