Theory Bisim_Subst

theory Bisim_Subst
  imports Bisim_Struct_Cong "Psi_Calculi.Close_Subst"
begin

text ‹This file is a (heavily modified) variant of the theory {\it Psi\_Calculi.Bisim\_Subst}
from~\cite{DBLP:journals/afp/Bengtson12}.›

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 closeSubstI closeSubstE bisimOutputPres by force


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 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 name_list_avoiding[where c="(σ, P, Q, Ψ, N)"]) 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]"
      apply -
      by(drule 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) ∈ set CsP ⟹ ∃Q. (φ, Q) ∈ set CsQ ∧ guarded Q ∧ Ψ ⊳ P ∼⇩s Q"
  and   C2: "⋀φ Q. (φ, Q) ∈ set CsQ ⟹ ∃P. (φ, P) ∈ set 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) ∈ set (caseListSeqSubst CsP σ)"
      then obtain φ' P' where "(φ', P') ∈ set CsP" and "φ = substCond.seqSubst φ' σ" and PeqP': "P = (P'[<σ>])"
        by(induct CsP) force+
      from ‹(φ', P') ∈ set CsP› obtain Q' where "(φ', Q') ∈ set CsQ" and "guarded Q'" and "Ψ ⊳ P' ∼⇩s Q'" by(blast dest: C1)
      from ‹(φ', Q') ∈ set CsQ› ‹φ = substCond.seqSubst φ' σ› obtain Q where "(φ, Q) ∈ set (caseListSeqSubst CsQ σ)" and "Q = Q'[<σ>]"
        by(induct CsQ) auto
      with PeqP' ‹guarded Q'› ‹Ψ ⊳ P' ∼⇩s Q'› ‹wellFormedSubst σ› show "∃Q. (φ, Q) ∈ set (caseListSeqSubst CsQ σ) ∧ guarded Q ∧ Ψ ⊳ P ∼ Q"
        by(blast dest: closeSubstE guardedSeqSubst)
    next
      fix φ Q
      assume "(φ, Q) ∈ set (caseListSeqSubst CsQ σ)"
      then obtain φ' Q' where "(φ', Q') ∈ set CsQ" and "φ = substCond.seqSubst φ' σ" and QeqQ': "Q = Q'[<σ>]"
        by(induct CsQ) force+
      from ‹(φ', Q') ∈ set CsQ› obtain P' where "(φ', P') ∈ set CsP" and "guarded P'" and "Ψ ⊳ P' ∼⇩s Q'" by(blast dest: C2)
      from ‹(φ', P') ∈ set CsP› ‹φ = substCond.seqSubst φ' σ› obtain P where "(φ, P) ∈ set (caseListSeqSubst CsP σ)" and "P = P'[<σ>]"
        by(induct CsP) auto
      with QeqQ' ‹guarded P'› ‹Ψ ⊳ P' ∼⇩s Q'› ‹wellFormedSubst σ›  show "∃P. (φ, P) ∈ set (caseListSeqSubst CsP σ) ∧ guarded P ∧ Ψ ⊳ P ∼ Q"
        by(blast dest: closeSubstE guardedSeqSubst)
    qed
  }
  then show ?thesis
    by(intro 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 ∼⇩s Q ∧ guarded P ∧ guarded Q"

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

    assume "(φ, P) ∈ set CsP"

    with ‹length CsP = length CsQ› have "∃Q. (φ, Q) ∈ set CsQ ∧ guarded Q ∧ Ψ ⊳ P ∼⇩s Q" using C
    proof(induct n=="length CsP" arbitrary: CsP CsQ rule: nat.induct)
      case zero then show ?case by simp
    next
      case(Suc n) then show ?case
      proof(cases CsP)
        case Nil then show ?thesis using ‹Suc n = length CsP› by simp
      next
        case(Cons P'φ CsP')
        note CsPdef = this
        then show ?thesis
        proof(cases CsQ)
          case Nil then show ?thesis using CsPdef ‹length CsP = length CsQ›
            by simp
        next
          case(Cons Q'φ CsQ')
          obtain Q' φ' where Q'phi: "Q'φ=(φ',Q')"
            by(induct Q'φ) auto
          show ?thesis
          proof(cases "P'φ = (φ,P)")
            case True
            have "0 <= length CsP" unfolding CsPdef
              by simp
            moreover from True have "(φ, P) = nth CsP 0" using ‹(φ, P) ∈ set CsP› unfolding CsPdef
              by simp
            moreover have "(φ', Q') = nth CsQ 0" unfolding Cons Q'phi by simp
            ultimately have "φ = φ' ∧ Ψ ⊳ P ∼⇩s Q' ∧ guarded P ∧ guarded Q'"
              by(rule Suc)
            then show ?thesis unfolding Cons Q'phi
              by(intro exI[where x=Q']) auto
          next
            case False
            have "n = length CsP'" using ‹Suc n = length CsP› unfolding CsPdef
              by simp
            moreover have "length CsP' = length CsQ'" using ‹length CsP = length CsQ› unfolding CsPdef Cons by simp
            moreover from ‹(φ,P) ∈ set CsP› False have "(φ, P) ∈ set CsP'" unfolding CsPdef by simp
            moreover
            {
              fix   i::nat
                and φ::'c
                and φ'::'c
                and P::"('a,'b,'c) psi"
                and Q::"('a,'b,'c) psi"
              assume "i ≤ length CsP'"
                and  "(φ, P) = CsP' ! i"
                and  "(φ', Q) = CsQ' ! i"
              then have "(i+1) ≤ length CsP"
                and "(φ, P) = CsP ! (i+1)"
                and "(φ', Q) = CsQ ! (i+1)"
                unfolding CsPdef Cons
                by simp+
              then have "φ = φ' ∧ Ψ ⊳ P ∼⇩s Q ∧ guarded P ∧ guarded Q"
                by(rule Suc)
            }
            note this
            ultimately have "∃Q. (φ, Q) ∈ set CsQ' ∧ guarded Q ∧ Ψ ⊳ P ∼⇩s Q"
              by(rule Suc)
            then show ?thesis unfolding Cons by auto
          qed
        qed
      qed
    qed
  }
  note this
  moreover
  {
    fix φ
      and Q

    assume "(φ, Q) ∈ set CsQ"

    with ‹length CsP = length CsQ› have "∃P. (φ, P) ∈ set CsP ∧ guarded P ∧ Ψ ⊳ P ∼⇩s Q" using C
    proof(induct n=="length CsQ" arbitrary: CsP CsQ rule: nat.induct)
      case zero then show ?case by simp
    next
      case(Suc n) then show ?case
      proof(cases CsQ)
        case Nil then show ?thesis using ‹Suc n = length CsQ› by simp
      next
        case(Cons Q'φ CsQ')
        note CsPdef = this
        then show ?thesis
        proof(cases CsP)
          case Nil then show ?thesis using CsPdef ‹length CsP = length CsQ›
            by simp
        next
          case(Cons P'φ CsP')
          obtain P' φ' where P'phi: "P'φ=(φ',P')"
            by(induct P'φ) auto
          show ?thesis
          proof(cases "Q'φ = (φ,Q)")
            case True
            have "0 <= length CsP" unfolding CsPdef
              by simp
            moreover have "(φ', P') = nth CsP 0" unfolding Cons P'phi by simp
            moreover from True have "(φ, Q) = nth CsQ 0" using ‹(φ, Q) ∈ set CsQ› unfolding CsPdef
              by simp
            ultimately have "φ' = φ ∧ Ψ ⊳ P' ∼⇩s Q ∧ guarded P' ∧ guarded Q"
              by(rule Suc)
            then show ?thesis unfolding Cons P'phi
              by(intro exI[where x=P']) auto
          next
            case False
            have "n = length CsQ'" using ‹Suc n = length CsQ› unfolding CsPdef
              by simp
            moreover have "length CsP' = length CsQ'" using ‹length CsP = length CsQ› unfolding CsPdef Cons by simp
            moreover from ‹(φ,Q) ∈ set CsQ› False have "(φ, Q) ∈ set CsQ'" unfolding CsPdef by simp
            moreover
            {
              fix   i::nat
                and φ::'c
                and φ'::'c
                and P::"('a,'b,'c) psi"
                and Q::"('a,'b,'c) psi"
              assume "i ≤ length CsP'"
                and  "(φ, P) = CsP' ! i"
                and  "(φ', Q) = CsQ' ! i"
              then have "(i+1) ≤ length CsP"
                and "(φ, P) = CsP ! (i+1)"
                and "(φ', Q) = CsQ ! (i+1)"
                unfolding CsPdef Cons
                by simp+
              then have "φ = φ' ∧ Ψ ⊳ P ∼⇩s Q ∧ guarded P ∧ guarded Q"
                by(rule Suc)
            }
            note this
            ultimately have "∃P. (φ, P) ∈ set CsP' ∧ guarded P ∧ Ψ ⊳ P ∼⇩s Q"
              by(rule Suc)
            then show ?thesis unfolding Cons by auto
          qed
        qed
      qed
    qed
  }
  ultimately show ?thesis
    by(rule bisimSubstCasePresAux)
qed

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 closeSubstI closeSubstE bisimParPres by force

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 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
  then have "Ψ ⊳ ([(x, y)] ∙ P)[<σ>] ∼ ([(x, y)] ∙ Q)[<σ>]" using ‹wellFormedSubst σ›
    by(rule closeSubstE)
  then have "Ψ ⊳ ⦇ν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 closeSubstI closeSubstE bisimBangPres guardedSeqSubst by force

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(auto 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"
  by(auto 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)"
  by(auto 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)
  then have "Ψ ⊳ ⦇ν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 ♯ σ"

    then have "(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"

    then have "(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)
  then have "Ψ ⊳ ⦇ν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 name_list_avoiding[where c="(N, P, x, y, σ)"]) 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(cases "x = y")
  assume "x = y"
  then show ?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 closeSubstI bangExt guardedSeqSubst by force

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