Theory Bisim_Subst

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

context env begin

abbreviation
  bisimSubstJudge (‹_ ⊳ _ ∼⇩s _› [70, 70, 70] 65) where "Ψ ⊳ P ∼⇩s Q ≡ (Ψ, P, Q) ∈ closeSubst bisim"
abbreviation
  bisimSubstNilJudge (‹_ ∼⇩s _› [70, 70] 65) where "P ∼⇩s Q ≡ SBottom' ⊳ P ∼⇩s Q"

lemmas bisimSubstClosed[eqvt] = closeSubstClosed[OF bisimEqvt]
lemmas bisimSubstEqvt[simp] = closeSubstEqvt[OF bisimEqvt]

lemma bisimSubstOutputPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   M :: 'a
  and   N :: 'a
  
  assumes "Ψ ⊳ P ∼⇩s Q"

  shows "Ψ ⊳ M⟨N⟩.P ∼⇩s M⟨N⟩.Q"
using assms
by(fastforce intro: closeSubstI closeSubstE bisimOutputPres)


lemma seqSubstInputChain[simp]:
  fixes xvec :: "name list"
  and   N    :: "'a"
  and   P    :: "('a, 'b, 'c) psi"
  and   σ    :: "(name list × 'a list) list"

  assumes "xvec ♯* σ"

  shows "seqSubs' (inputChain xvec N P) σ = inputChain xvec (substTerm.seqSubst N σ) (seqSubs P σ)"
using assms
by(induct xvec) auto

lemma bisimSubstInputPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a

  assumes "Ψ ⊳ P ∼⇩s Q"
  and     "xvec ♯* Ψ"
  and     "distinct xvec"

  shows "Ψ ⊳ M⦇λ*xvec N⦈.P ∼⇩s M⦇λ*xvec N⦈.Q"
proof(rule_tac closeSubstI)
  fix σ
  assume "wellFormedSubst(σ::(name list × 'a list) list)"
  obtain p where "(p ∙ xvec) ♯* σ"
             and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Q" and "(p ∙ xvec) ♯* Ψ" and "(p ∙ xvec) ♯* N"
             and S: "set p ⊆ set xvec × set (p ∙ xvec)"
      by(rule_tac c="(σ, P, Q, Ψ, N)" in name_list_avoiding) auto
    
  from ‹Ψ ⊳ P ∼⇩s Q› have "(p ∙ Ψ) ⊳ (p ∙ P) ∼⇩s (p ∙ Q)"
    by(rule bisimSubstClosed)
  with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S have "Ψ ⊳ (p ∙ P) ∼⇩s (p ∙ Q)"
    by simp

  {
    fix Tvec :: "'a list"
    from ‹Ψ ⊳ (p ∙ P) ∼⇩s (p ∙ Q)› ‹wellFormedSubst σ› have "Ψ ⊳ (p ∙ P)[<σ>] ∼⇩s (p ∙ Q)[<σ>]"
      by(rule closeSubstUnfold)
    moreover assume "length xvec = length Tvec" and "distinct xvec"
    ultimately have "Ψ ⊳ ((p ∙ P)[<σ>])[(p ∙ xvec)::=Tvec] ∼ ((p ∙ Q)[<σ>])[(p ∙ xvec)::=Tvec]" 
      by(drule_tac closeSubstE[where σ="[((p ∙ xvec), Tvec)]"]) auto
  }

  with ‹(p ∙ xvec) ♯* σ› ‹distinct xvec›
  have "Ψ ⊳ (M⦇λ*(p ∙ xvec) (p ∙ N)⦈.(p ∙ P))[<σ>] ∼ (M⦇λ*(p ∙ xvec) (p ∙ N)⦈.(p ∙ Q))[<σ>]"
    by(force intro: bisimInputPres)
  moreover from ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* P› S have "M⦇λ*(p ∙ xvec) (p ∙ N)⦈.(p ∙ P) = M⦇λ*xvec N⦈.P" 
    apply(simp add: psi.inject) by(rule inputChainAlpha[symmetric]) auto
  moreover from ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* Q› S have "M⦇λ*(p ∙ xvec) (p ∙ N)⦈.(p ∙ Q) = M⦇λ*xvec N⦈.Q"
    apply(simp add: psi.inject) by(rule inputChainAlpha[symmetric]) auto
  ultimately show "Ψ ⊳ (M⦇λ*xvec N⦈.P)[<σ>] ∼ (M⦇λ*xvec N⦈.Q)[<σ>]"
    by force
qed

lemma bisimSubstCasePresAux:
  fixes Ψ   :: 'b
  and   CsP :: "('c × ('a, 'b, 'c) psi) list"
  and   CsQ :: "('c × ('a, 'b, 'c) psi) list"
  
  assumes C1: "⋀φ P. (φ, P) mem CsP ⟹ ∃Q. (φ, Q) mem CsQ ∧ guarded Q ∧ Ψ ⊳ P ∼⇩s Q"
  and     C2: "⋀φ Q. (φ, Q) mem CsQ ⟹ ∃P. (φ, P) mem CsP ∧ guarded P ∧ Ψ ⊳ P ∼⇩s Q"

  shows "Ψ ⊳ Cases CsP ∼⇩s Cases CsQ"
proof -
  {
    fix σ :: "(name list × 'a list) list"

    assume "wellFormedSubst σ"

    have "Ψ ⊳ Cases(caseListSeqSubst CsP σ) ∼ Cases(caseListSeqSubst CsQ σ)"
    proof(rule bisimCasePres)
      fix φ P
      assume "(φ, P) mem (caseListSeqSubst CsP σ)"
      then obtain φ' P' where "(φ', P') mem CsP" and "φ = substCond.seqSubst φ' σ" and PeqP': "P = (P'[<σ>])"
        by(induct CsP) force+
      from ‹(φ', P') mem CsP› obtain Q' where "(φ', Q') mem CsQ" and "guarded Q'" and "Ψ ⊳ P' ∼⇩s Q'" by(blast dest: C1)
      from ‹(φ', Q') mem CsQ› ‹φ = substCond.seqSubst φ' σ› obtain Q where "(φ, Q) mem (caseListSeqSubst CsQ σ)" and "Q = Q'[<σ>]"
        by(induct CsQ) auto
      with PeqP' ‹guarded Q'› ‹Ψ ⊳ P' ∼⇩s Q'› ‹wellFormedSubst σ› show "∃Q. (φ, Q) mem (caseListSeqSubst CsQ σ) ∧ guarded Q ∧ Ψ ⊳ P ∼ Q"
        by(blast dest: closeSubstE guardedSeqSubst)
    next
      fix φ Q
      assume "(φ, Q) mem (caseListSeqSubst CsQ σ)"
      then obtain φ' Q' where "(φ', Q') mem CsQ" and "φ = substCond.seqSubst φ' σ" and QeqQ': "Q = Q'[<σ>]"
        by(induct CsQ) force+
      from ‹(φ', Q') mem CsQ› obtain P' where "(φ', P') mem CsP" and "guarded P'" and "Ψ ⊳ P' ∼⇩s Q'" by(blast dest: C2)
      from ‹(φ', P') mem CsP› ‹φ = substCond.seqSubst φ' σ› obtain P where "(φ, P) mem (caseListSeqSubst CsP σ)" and "P = P'[<σ>]"
        by(induct CsP) auto
      with QeqQ' ‹guarded P'› ‹Ψ ⊳ P' ∼⇩s Q'› ‹wellFormedSubst σ›  show "∃P. (φ, P) mem (caseListSeqSubst CsP σ) ∧ guarded P ∧ Ψ ⊳ P ∼ Q"
        by(blast dest: closeSubstE guardedSeqSubst)
    qed
  }
  thus ?thesis
    by(rule_tac closeSubstI) auto
qed

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

  shows "Ψ ⊳ P ∼⇩s P"
by(auto intro: closeSubstI bisimReflexive)

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

  assumes "Ψ ⊳ P ∼⇩s Q"
  and     "Ψ ⊳ Q ∼⇩s R"

  shows "Ψ ⊳ P ∼⇩s R"
using assms
by(auto intro: closeSubstI closeSubstE bisimTransitive)

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

  assumes "Ψ ⊳ P ∼⇩s Q"

  shows "Ψ ⊳ Q ∼⇩s P"
using assms
by(auto intro: closeSubstI closeSubstE bisimE)
(*
lemma bisimSubstCasePres:
  fixes Ψ   :: 'b
  and   CsP :: "('c × ('a, 'b, 'c) psi) list"
  and   CsQ :: "('c × ('a, 'b, 'c) psi) list"
  
  assumes "length CsP = length CsQ"
  and     C: "⋀(i::nat) φ P φ' Q. ⟦i <= length CsP; (φ, P) = nth CsP i; (φ', Q) = nth CsQ i⟧ ⟹ φ = φ' ∧ Ψ ⊳ P ∼ Q"

  shows "Ψ ⊳ Cases CsP ∼⇩s Cases CsQ"
proof -
  {
    fix φ 
    and P

    assume "(φ, P) mem CsP"

    with `length CsP = length CsQ` have "∃Q. (φ, Q) mem CsQ ∧ Ψ ⊳ P ∼⇩s Q"
      apply(induct n=="length CsP" arbitrary: CsP CsQ rule: nat.induct)
      apply simp
      apply simp
      apply auto

  }
using `length CsP = length CsQ`
proof(induct n=="length CsP" rule: nat.induct)
  case zero
  thus ?case by(fastforce intro: bisimSubstReflexive)
next
  case(Suc n)
next
apply auto
apply(blast intro: bisimSubstReflexive)
apply auto
apply(simp add: nth.simps)
apply(auto simp add: nth.simps)
apply blast
apply(rule_tac bisimSubstCasePresAux)
apply auto
*)
lemma bisimSubstParPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"
  
  assumes "Ψ ⊳ P ∼⇩s Q"

  shows "Ψ ⊳ P ∥ R ∼⇩s Q ∥ R"
using assms
by(fastforce intro: closeSubstI closeSubstE bisimParPres)

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

  assumes "Ψ ⊳ P ∼⇩s Q"
  and     "x ♯ Ψ"

  shows "Ψ ⊳ ⦇νx⦈P ∼⇩s ⦇νx⦈Q"
proof(rule_tac closeSubstI)
  fix σ :: "(name list × 'a list) list"

  assume "wellFormedSubst σ"
  obtain y::name where "y ♯ Ψ" and "y ♯ P" and "y ♯ Q" and "y ♯ σ"
    by(generate_fresh "name") (auto simp add: fresh_prod)

  from ‹Ψ ⊳ P ∼⇩s Q› have "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ P) ∼⇩s ([(x, y)] ∙ Q)"
    by(rule bisimSubstClosed)
  with ‹x ♯ Ψ› ‹y ♯ Ψ› have "Ψ ⊳ ([(x, y)] ∙ P) ∼⇩s ([(x, y)] ∙ Q)"
    by simp
  hence "Ψ ⊳ ([(x, y)] ∙ P)[<σ>] ∼ ([(x, y)] ∙ Q)[<σ>]" using ‹wellFormedSubst σ› 
    by(rule closeSubstE)
  hence "Ψ ⊳ ⦇νy⦈(([(x, y)] ∙ P)[<σ>]) ∼ ⦇νy⦈(([(x, y)] ∙ Q)[<σ>])" using ‹y ♯ Ψ›
    by(rule bisimResPres)
  with ‹y ♯ P› ‹y ♯ Q› ‹y ♯ σ›
  show "Ψ ⊳ (⦇νx⦈P)[<σ>] ∼ (⦇νx⦈Q)[<σ>]"
    by(simp add: alphaRes)
qed

lemma bisimSubstBangPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
 
  assumes "Ψ ⊳ P ∼⇩s Q"
  and     "guarded P"
  and     "guarded Q"

  shows "Ψ ⊳ !P ∼⇩s !Q"
using assms
by(fastforce intro: closeSubstI closeSubstE bisimBangPres guardedSeqSubst)

lemma substNil[simp]:
  fixes xvec :: "name list"
  and   Tvec :: "'a list"

  assumes "wellFormedSubst σ"
  and     "distinct xvec"

  shows "(𝟬[<σ>]) = 𝟬"
using assms
by simp

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

  shows "Ψ ⊳ P ∥ 𝟬 ∼⇩s P" 
by(fastforce intro: closeSubstI bisimParNil)

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

  shows "Ψ ⊳ P ∥ Q ∼⇩s Q ∥ P"
apply(rule closeSubstI)
by(fastforce intro: closeSubstI bisimParComm)

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

  shows "Ψ ⊳ (P ∥ Q) ∥ R ∼⇩s P ∥ (Q ∥ R)"
apply(rule closeSubstI)
by(fastforce intro: closeSubstI bisimParAssoc)

lemma bisimSubstResNil:
  fixes Ψ :: 'b
  and   x :: name

  shows "Ψ ⊳ ⦇νx⦈𝟬 ∼⇩s 𝟬"
proof(rule closeSubstI)
  fix σ:: "(name list × 'a list) list"

  assume "wellFormedSubst σ"
  obtain y::name where "y ♯ Ψ" and "y ♯ σ"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  have "Ψ ⊳ ⦇νy⦈𝟬 ∼ 𝟬" by(rule bisimResNil)
  with ‹y ♯ σ› ‹wellFormedSubst σ›  show "Ψ ⊳ (⦇νx⦈𝟬)[<σ>] ∼ 𝟬[<σ>]"
    by(subst alphaRes[of y]) auto
qed

lemma seqSubst2:
  fixes x :: name
  and   P :: "('a, 'b, 'c) psi"

  assumes "wellFormedSubst σ"
  and     "x ♯ σ"
  and     "x ♯ P"

  shows "x ♯ P[<σ>]"
using assms
by(induct σ arbitrary: P, auto) (blast dest: subst2)

notation substTerm.seqSubst (‹_[<_>]› [100, 100] 100)

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

  assumes "x ♯ P"

  shows "Ψ ⊳ ⦇νx⦈(P ∥ Q) ∼⇩s P ∥ ⦇νx⦈Q" 
proof(rule closeSubstI)
  fix σ:: "(name list × 'a list) list"

  assume "wellFormedSubst σ"
  obtain y::name where "y ♯ Ψ" and "y ♯ σ" and "y ♯ P" and "y ♯ Q"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  moreover from ‹wellFormedSubst σ›  ‹y ♯ σ› ‹y ♯ P› have "y ♯ P[<σ>]"
    by(rule seqSubst2)
  hence "Ψ ⊳ ⦇νy⦈((P[<σ>]) ∥ (([(x, y)] ∙ Q)[<σ>])) ∼ (P[<σ>]) ∥ ⦇νy⦈(([(x, y)] ∙ Q)[<σ>])"
    by(rule bisimScopeExt)
  with ‹x ♯ P› ‹y ♯ P› ‹y ♯ Q› ‹y ♯ σ› show "Ψ ⊳ (⦇νx⦈(P ∥ Q))[<σ>] ∼ (P ∥ ⦇νx⦈Q)[<σ>]"
    apply(subst alphaRes[of y], simp)
    apply(subst alphaRes[of y Q], simp)
    by(simp add: eqvts)
qed  

lemma bisimSubstCasePushRes:
  fixes x  :: name
  and   Ψ  :: 'b
  and   Cs :: "('c × ('a, 'b, 'c) psi) list"

  assumes "x ♯ map fst Cs"

  shows "Ψ ⊳ ⦇νx⦈(Cases Cs) ∼⇩s Cases map (λ(φ, P). (φ, ⦇νx⦈P)) Cs"
proof(rule closeSubstI)
  fix σ:: "(name list × 'a list) list"

  assume "wellFormedSubst σ"
  obtain y::name where "y ♯ Ψ" and "y ♯ σ" and "y ♯ Cs"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  
  {
    fix x    :: name
    and Cs   :: "('c × ('a, 'b, 'c) psi) list"
    and σ    :: "(name list × 'a list) list"

    assume "x ♯ σ"

    hence "(Cases map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)[<σ>] = Cases map (λ(φ, P). (φ, ⦇νx⦈P)) (caseListSeqSubst Cs σ)"
      by(induct Cs) auto
  }
  note C1 = this

  {
    fix x    :: name
    and y    :: name
    and Cs   :: "('c × ('a, 'b, 'c) psi) list"

    assume "x ♯ map fst Cs"
    and    "y ♯ map fst Cs"
    and    "y ♯ Cs"

    hence "(Cases map (λ(φ, P). (φ, ⦇νx⦈P)) Cs) = Cases map (λ(φ, P). (φ, ⦇νy⦈P)) ([(x, y)] ∙ Cs)"
      by(induct Cs) (auto simp add: fresh_list_cons alphaRes)
  }
  note C2 = this

  from ‹y ♯ Cs› have "y ♯ map fst Cs" by(induct Cs) (auto simp add: fresh_list_cons fresh_list_nil)
  from ‹y ♯ Cs› ‹y ♯ σ› ‹x ♯ map fst Cs› ‹wellFormedSubst σ›  have "y ♯ map fst (caseListSeqSubst ([(x, y)] ∙ Cs) σ)"
    by(induct Cs) (auto intro: substCond.seqSubst2 simp add: fresh_list_cons fresh_list_nil fresh_prod)
  hence "Ψ ⊳ ⦇νy⦈(Cases(caseListSeqSubst ([(x, y)] ∙ Cs) σ)) ∼ Cases map (λ(φ, P). (φ, ⦇νy⦈P)) (caseListSeqSubst ([(x, y)] ∙ Cs) σ)"
    by(rule bisimCasePushRes)

  with ‹y ♯ Cs› ‹x ♯ map fst Cs› ‹y ♯ map fst Cs› ‹y ♯ σ› ‹wellFormedSubst σ› 
  show "Ψ ⊳ (⦇νx⦈(Cases Cs))[<σ>] ∼ (Cases map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)[<σ>]"
    apply(subst C2[of x Cs y])
    apply assumption+
    apply(subst C1)
    apply assumption+
    apply(subst alphaRes[of y], simp)
    by(simp add: eqvts)
qed

lemma bisimSubstOutputPushRes:
  fixes x :: name
  and   Ψ :: 'b
  and   M :: 'a
  and   N :: 'a
  and   P :: "('a, 'b, 'c) psi"

  assumes "x ♯ M"
  and     "x ♯ N"

  shows "Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ∼⇩s M⟨N⟩.⦇νx⦈P"
proof(rule closeSubstI)
  fix σ:: "(name list × 'a list) list"

  assume "wellFormedSubst σ"
  obtain y::name where "y ♯ Ψ" and "y ♯ σ" and "y ♯ P" and "y ♯ M" and "y ♯ N"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from ‹wellFormedSubst σ›  ‹y ♯ M› ‹y ♯ σ› have "y ♯ M[<σ>]" by auto
  moreover from ‹wellFormedSubst σ›  ‹y ♯ N› ‹y ♯ σ› have "y ♯ N[<σ>]" by auto
  ultimately have "Ψ ⊳ ⦇νy⦈((M[<σ>])⟨(N[<σ>])⟩.(([(x, y)] ∙ P)[<σ>])) ∼ (M[<σ>])⟨(N[<σ>])⟩.(⦇νy⦈(([(x, y)] ∙ P)[<σ>]))"
    by(rule bisimOutputPushRes)
  with ‹y ♯ M› ‹y ♯ N› ‹y ♯ P› ‹x ♯ M› ‹x ♯ N› ‹y ♯ σ› ‹wellFormedSubst σ› 
  show "Ψ ⊳ (⦇νx⦈(M⟨N⟩.P))[<σ>] ∼ (M⟨N⟩.⦇νx⦈P)[<σ>]"
    apply(subst alphaRes[of y], simp)
    apply(subst alphaRes[of y P], simp)
    by(simp add: eqvts)
qed

lemma bisimSubstInputPushRes:
  fixes x    :: name
  and   Ψ    :: 'b
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a

  assumes "x ♯ M"
  and     "x ♯ xvec"
  and     "x ♯ N"

  shows "Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ∼⇩s M⦇λ*xvec N⦈.⦇νx⦈P"
proof(rule closeSubstI)
  fix σ:: "(name list × 'a list) list"

  assume "wellFormedSubst σ"
  obtain y::name where "y ♯ Ψ" and "y ♯ σ" and "y ♯ P" and "y ♯ M" and "y ♯ xvec" and "y ♯ N"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  obtain p::"name prm" where "(p ∙ xvec) ♯* N" and  "(p ∙ xvec) ♯* P" and "x ♯ (p ∙ xvec)" and "y ♯ (p ∙ xvec)" and "(p ∙ xvec) ♯* σ"
                         and S: "set p ⊆ set xvec × set(p ∙ xvec)"
   by(rule_tac c="(N, P, x, y, σ)" in name_list_avoiding) auto
    
  from ‹wellFormedSubst σ› ‹y ♯ M› ‹y ♯ σ › have "y ♯ M[<σ>]" by auto
  moreover note ‹y ♯ (p ∙ xvec)›
  moreover from ‹y ♯ N› have "(p ∙ y) ♯ (p ∙ N)" by(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
  with ‹y ♯ xvec› ‹y ♯ (p ∙ xvec)› S have "y ♯ p ∙ N" by simp
  with ‹wellFormedSubst σ› have "y ♯ (p ∙ N)[<σ>]" using ‹y ♯ σ› by auto
  ultimately have "Ψ ⊳ ⦇νy⦈((M[<σ>])⦇λ*(p ∙ xvec) ((p ∙ N)[<σ>])⦈.(([(x, y)] ∙ (p ∙ P))[<σ>])) ∼ (M[<σ>])⦇λ*(p ∙ xvec) ((p ∙ N)[<σ>])⦈.(⦇νy⦈(([(x, y)] ∙ p ∙ P)[<σ>]))"
    by(rule bisimInputPushRes)
  with ‹y ♯ M› ‹y ♯ N› ‹y ♯ P› ‹x ♯ M› ‹x ♯ N› ‹y ♯ xvec› ‹x ♯ xvec› ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* P› 
       ‹x ♯ (p ∙ xvec)› ‹y ♯ (p ∙ xvec)› ‹y ♯ σ› ‹(p ∙ xvec) ♯* σ› S ‹wellFormedSubst σ›
  show "Ψ ⊳ (⦇νx⦈(M⦇λ*xvec N⦈.P))[<σ>] ∼ (M⦇λ*xvec N⦈.⦇νx⦈P)[<σ>]"
    apply(subst inputChainAlpha')
    apply assumption+
    apply(subst inputChainAlpha'[of p xvec])
    apply(simp add: abs_fresh_star)
    apply assumption+
    apply(simp add: eqvts)
    apply(subst alphaRes[of y], simp)
    apply(simp add: inputChainFresh)
    apply(simp add: freshChainSimps)
    apply(subst alphaRes[of y "(p ∙ P)"])
    apply(simp add: freshChainSimps)
    by(simp add: freshChainSimps eqvts)
qed

lemma bisimSubstResComm:
  fixes x :: name
  and   y :: name

  shows "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ∼⇩s ⦇νy⦈(⦇νx⦈P)"
proof(case_tac "x = y")
  assume "x = y"
  thus ?thesis by(force intro: bisimSubstReflexive)
next
  assume "x ≠ y"
  show ?thesis
  proof(rule closeSubstI)
  fix σ:: "(name list × 'a list) list"
  assume "wellFormedSubst σ"


    obtain x'::name where "x' ♯  Ψ" and "x' ♯ σ" and "x' ♯ P" and "x ≠ x'" and "y ≠ x'"
      by(generate_fresh "name") (auto simp add: fresh_prod)
    obtain y'::name where "y' ♯  Ψ" and "y' ♯ σ" and "y' ♯ P" and "x ≠ y'" and "y ≠ y'" and "x' ≠ y'"
      by(generate_fresh "name") (auto simp add: fresh_prod)

    have "Ψ ⊳ ⦇νx'⦈(⦇νy'⦈(([(x, x')] ∙ [(y, y')] ∙ P)[<σ>])) ∼ ⦇νy'⦈(⦇νx'⦈(([(x, x')] ∙ [(y, y')] ∙ P)[<σ>]))"
      by(rule bisimResComm)
    moreover from ‹x' ♯ P› ‹y' ♯ P› ‹x ≠ y'› ‹x' ≠ y'› have "⦇νx⦈(⦇νy⦈P) = ⦇νx'⦈(⦇νy'⦈(([(x, x')] ∙ [(y, y')] ∙ P)))"
      apply(subst alphaRes[of y' P], simp)
      by(subst alphaRes[of x']) (auto simp add: abs_fresh fresh_left calc_atm eqvts)
    moreover from ‹x' ♯ P› ‹y' ♯ P› ‹y ≠ x'› ‹x ≠ y'› ‹x' ≠ y'› ‹x ≠ x'› ‹x ≠ y› have "⦇νy⦈(⦇νx⦈P) = ⦇νy'⦈(⦇νx'⦈(([(x, x')] ∙ [(y, y')] ∙ P)))"
      apply(subst alphaRes[of x' P], simp)
      apply(subst alphaRes[of y'], simp add: abs_fresh fresh_left calc_atm) 
      apply(simp add: eqvts calc_atm)
      by(subst perm_compose) (simp add: calc_atm)

    ultimately show "Ψ ⊳ (⦇νx⦈(⦇νy⦈P))[<σ>] ∼ (⦇νy⦈(⦇νx⦈P))[<σ>]" 
      using ‹wellFormedSubst σ›  ‹x' ♯ σ› ‹y' ♯ σ›
      by simp
  qed
qed

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

  shows "Ψ ⊳ !P ∼⇩s P ∥ !P"
using assms
by(fastforce intro: closeSubstI bangExt guardedSeqSubst)

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

  assumes "P ≡⇩s Q"

  shows "P ∼⇩s Q"
using assms
by(induct rule: structCong.induct)
  (auto intro: bisimSubstReflexive bisimSubstSymmetric bisimSubstTransitive bisimSubstParComm bisimSubstParAssoc bisimSubstParNil bisimSubstResNil bisimSubstResComm bisimSubstScopeExt bisimSubstCasePushRes bisimSubstInputPushRes bisimSubstOutputPushRes bisimSubstExtBang)

end

end