Theory Bisim_Pres

theory Bisim_Pres
  imports Bisimulation Sim_Pres
begin

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

context env begin

lemma bisimInputPres:
  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 "⋀Tvec. length xvec = length Tvec ⟹ Ψ ⊳ P[xvec::=Tvec] ∼ Q[xvec::=Tvec]"

shows "Ψ ⊳ M⦇λ*xvec N⦈.P ∼ M⦇λ*xvec N⦈.Q"
proof -
  let ?X = "{(Ψ, M⦇λ*xvec N⦈.P, M⦇λ*xvec N⦈.Q) | Ψ M xvec N P Q. ∀Tvec. length xvec = length Tvec ⟶ Ψ ⊳ P[xvec::=Tvec] ∼ Q[xvec::=Tvec]}"

  from assms have "(Ψ, M⦇λ*xvec N⦈.P, M⦇λ*xvec N⦈.Q) ∈ ?X" by blast
  then show ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ P Q)
    then show ?case by auto
  next
    case(cSim Ψ P Q)
    then show ?case by(blast intro: inputPres)
  next
    case(cExt Ψ P Q Ψ')
    then show ?case by(blast dest: bisimE)
  next
    case(cSym Ψ P Q)
    then show ?case by(blast dest: bisimE)
  qed
qed

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

assumes "Ψ ⊳ P ∼ Q"

shows "Ψ ⊳ M⟨N⟩.P ∼ M⟨N⟩.Q"
proof -
  let ?X = "{(Ψ, M⟨N⟩.P, M⟨N⟩.Q) | Ψ M N P Q. Ψ ⊳ P ∼ Q}"
  from ‹Ψ ⊳ P ∼ Q› have "(Ψ, M⟨N⟩.P, M⟨N⟩.Q) ∈ ?X" by auto
  then show ?thesis
    by(coinduct rule: bisimCoinduct, auto) (blast intro: outputPres dest: bisimE)+
qed

lemma bisimCasePres:
  fixes Ψ   :: 'b
    and CsP :: "('c × ('a, 'b, 'c) psi) list"
    and CsQ :: "('c × ('a, 'b, 'c) psi) list"

assumes "⋀φ P. (φ, P) ∈ set CsP ⟹ ∃Q. (φ, Q) ∈ set CsQ ∧ guarded Q ∧ Ψ ⊳ P ∼ Q"
  and   "⋀φ Q. (φ, Q) ∈ set CsQ ⟹ ∃P. (φ, P) ∈ set CsP ∧ guarded P ∧ Ψ ⊳ P ∼ Q"

shows "Ψ ⊳ Cases CsP ∼ Cases CsQ"
proof -
  let ?X = "{(Ψ, Cases CsP, Cases CsQ) | Ψ CsP CsQ. (∀φ P. (φ, P) ∈ set CsP ⟶ (∃Q. (φ, Q) ∈ set CsQ ∧ guarded Q ∧ Ψ ⊳ P ∼ Q)) ∧
                                                     (∀φ Q. (φ, Q) ∈ set CsQ ⟶ (∃P. (φ, P) ∈ set CsP ∧ guarded P ∧ Ψ ⊳ P ∼ Q))}"
  from assms have "(Ψ, Cases CsP, Cases CsQ) ∈ ?X" by auto
  then show ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ P Q)
    then show ?case by auto
  next
    case(cSim Ψ CasesP CasesQ)
    then obtain CsP CsQ where C1: "⋀φ Q. (φ, Q) ∈ set CsQ ⟹ ∃P. (φ, P) ∈ set CsP ∧ guarded P ∧ Ψ ⊳ P ∼ Q"
      and A: "CasesP = Cases CsP" and B: "CasesQ = Cases CsQ"
      by auto
    note C1
    moreover have "⋀Ψ P Q. Ψ ⊳ P ∼ Q ⟹ Ψ ⊳ P ↝[bisim] Q" by(rule bisimE)
    moreover have "bisim ⊆ ?X ∪ bisim" by blast
    ultimately have "Ψ ⊳ Cases CsP ↝[(?X ∪ bisim)] Cases CsQ"
      by(rule casePres)
    then show ?case using A B by blast
  next
    case(cExt Ψ P Q)
    then show ?case by(blast dest: bisimE)
  next
    case(cSym Ψ P Q)
    then show ?case by(blast dest: bisimE)
  qed
qed

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

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

shows "Ψ ⊳ ⦇νx⦈P ∼ ⦇νx⦈Q"
proof -
  let ?X = "{(Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) | Ψ xvec P Q. Ψ ⊳ P ∼ Q ∧ xvec ♯* Ψ}"
  have "eqvt ?X" using bisimClosed pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst]
    by(auto simp add: eqvts eqvt_def) blast
  have "(Ψ, ⦇νx⦈P, ⦇νx⦈Q) ∈ ?X"
  proof -
    from ‹x ♯ Ψ› have "[x] ♯* Ψ"
      by auto
    with ‹Ψ ⊳ P ∼ Q› show ?thesis
      by (smt mem_Collect_eq resChain.base resChain.step)
  qed
  then show ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ xP xQ)
    from ‹(Ψ, xP, xQ) ∈ ?X› obtain xvec P Q where "Ψ ⊳ P ∼ Q" and "xvec ♯* Ψ" and "xP = ⦇ν*xvec⦈P" and "xQ = ⦇ν*xvec⦈Q"
      by auto
    moreover from ‹Ψ ⊳ P ∼ Q› have PeqQ: "insertAssertion(extractFrame P) Ψ ≃⇩F insertAssertion(extractFrame Q) Ψ"
      by(rule bisimE)
    ultimately show ?case by(auto intro: frameResChainPres)
  next
    case(cSim Ψ xP xQ)
    from ‹(Ψ, xP, xQ) ∈ ?X› obtain xvec P Q where "Ψ ⊳ P ∼ Q" and "xvec ♯* Ψ" and "xP = ⦇ν*xvec⦈P" and "xQ = ⦇ν*xvec⦈Q"
      by auto
    from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊳ P ↝[bisim] Q" by(rule bisimE)
    note ‹eqvt ?X›
    then have "eqvt(?X ∪ bisim)" by auto
    from ‹xvec ♯* Ψ›
    have "Ψ ⊳ ⦇ν*xvec⦈P ↝[(?X ∪ bisim)] ⦇ν*xvec⦈Q"
    proof(induct xvec)
      case Nil
      have "Ψ ⊳ ⦇ν*[]⦈P ↝[bisim] ⦇ν*[]⦈Q" using ‹Ψ ⊳ P ∼ Q›
        unfolding resChain.simps
        by(rule bisimE)
      then show ?case by(rule monotonic) auto
    next
      case(Cons x xvec)
      then have "x ♯ Ψ" and "xvec ♯* Ψ"
        by auto
      from ‹xvec ♯* Ψ› have "Ψ ⊳ ⦇ν*xvec⦈P ↝[(?X ∪ bisim)] ⦇ν*xvec⦈Q"
        by(rule Cons)
      moreover note ‹eqvt(?X ∪ bisim)›
      moreover note ‹x ♯ Ψ›
      moreover have "?X ∪ bisim ⊆ ?X ∪ bisim" by auto
      moreover have "⋀Ψ P Q xvec. ⟦(Ψ, P, Q) ∈ ?X ∪ bisim; xvec ♯* Ψ⟧ ⟹ (Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) ∈ ?X ∪ bisim"
        by (smt (verit, ccfv_threshold) Un_iff freshChainAppend mem_Collect_eq prod.inject resChainAppend)
      ultimately have "Ψ ⊳ ⦇νx⦈(⦇ν*xvec⦈P) ↝[(?X ∪ bisim)] ⦇νx⦈(⦇ν*xvec⦈Q)"
        by(rule resPres)
      then show ?case unfolding resChain.simps by -
    next
    qed
    with ‹xP = ⦇ν*xvec⦈P› ‹xQ = ⦇ν*xvec⦈Q› show ?case
      by simp
  next
    case(cExt Ψ xP xQ Ψ')
    from ‹(Ψ, xP, xQ) ∈ ?X› obtain xvec P Q where "Ψ ⊳ P ∼ Q" and "xvec ♯* Ψ" and xpe: "xP = ⦇ν*xvec⦈P" and xqe: "xQ = ⦇ν*xvec⦈Q"
      by auto
    obtain p::"name prm" where "(p∙xvec) ♯* Ψ" and "(p∙xvec) ♯* Ψ'" and "(p∙xvec) ♯* P" and "(p∙xvec) ♯* Q" and "(p∙xvec) ♯* xvec" and "distinctPerm p" and "set p ⊆ (set xvec) × (set (p∙xvec))"
      by(rule name_list_avoiding[where c="(Ψ,Ψ',P,Q,xvec)"]) auto
    from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊗ (p∙Ψ') ⊳ P ∼ Q"
      by(rule bisimE)
    moreover have "xvec ♯* (Ψ ⊗ (p∙Ψ'))" using ‹xvec ♯* Ψ› ‹(p∙xvec) ♯* Ψ'› ‹distinctPerm p›
      apply(intro freshCompChain)
       apply assumption
      apply(subst perm_bool[where pi=p,symmetric])
      by(simp add: eqvts)
    ultimately have "(Ψ ⊗ (p∙Ψ'),⦇ν*xvec⦈P,⦇ν*xvec⦈Q) ∈ ?X"
      by auto
    then have "(p∙(Ψ ⊗ (p∙Ψ'),⦇ν*xvec⦈P,⦇ν*xvec⦈Q)) ∈ ?X" using ‹eqvt ?X›
      by(intro eqvtI)
    then have "(Ψ ⊗ Ψ',⦇ν*(p∙xvec)⦈(p∙P),⦇ν*(p∙xvec)⦈(p∙Q)) ∈ ?X" using ‹distinctPerm p› ‹set p ⊆ (set xvec) × (set (p∙xvec))› ‹xvec ♯* Ψ› ‹(p∙xvec) ♯* Ψ›
      by(simp add: eqvts)
    then have "(Ψ ⊗ Ψ',⦇ν*xvec⦈P,⦇ν*xvec⦈Q) ∈ ?X" using ‹(p ∙ xvec) ♯* Q› ‹(p ∙ xvec) ♯* P› ‹set p ⊆ set xvec × set (p ∙ xvec)› ‹distinctPerm p›
      by(subst (1 2) resChainAlpha[where p=p]) auto
    then show ?case unfolding xpe xqe
      by blast
  next
    case(cSym Ψ P Q)
    then show ?case
      by(blast dest: bisimE)
  qed
qed

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

assumes "Ψ ⊳ P ∼ Q"
  and   "xvec ♯* Ψ"

shows "Ψ ⊳ ⦇ν*xvec⦈P ∼ ⦇ν*xvec⦈Q"
  using assms
  by(induct xvec) (auto intro: bisimResPres)

lemma bisimParPresAux:
  fixes Ψ  :: 'b
    and Ψ⇩R :: 'b
    and P  :: "('a, 'b, 'c) psi"
    and Q  :: "('a, 'b, 'c) psi"
    and R  :: "('a, 'b, 'c) psi"
    and A⇩R :: "name list"

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

shows "Ψ ⊳ P ∥ R ∼ Q ∥ R"
proof -
  let ?X = "{(Ψ, ⦇ν*xvec⦈(P ∥ R), ⦇ν*xvec⦈(Q ∥ R)) | xvec Ψ P Q R. xvec ♯* Ψ ∧ (∀A⇩R Ψ⇩R. (extractFrame R = ⟨A⇩R, Ψ⇩R⟩ ∧ A⇩R ♯* Ψ ∧ A⇩R ♯* P ∧ A⇩R ♯* Q) ⟶
                                                                                          Ψ ⊗ Ψ⇩R ⊳ P ∼ Q)}"
  {
    fix xvec :: "name list"
      and Ψ    :: 'b
      and P    :: "('a, 'b, 'c) psi"
      and Q    :: "('a, 'b, 'c) psi"
      and R    :: "('a, 'b, 'c) psi"

    assume "xvec ♯* Ψ"
      and  "⋀A⇩R Ψ⇩R. ⟦extractFrame R = ⟨A⇩R, Ψ⇩R⟩; A⇩R ♯* Ψ; A⇩R ♯* P; A⇩R ♯* Q⟧ ⟹ Ψ ⊗ Ψ⇩R ⊳ P ∼ Q"

    then have "(Ψ, ⦇ν*xvec⦈(P ∥ R), ⦇ν*xvec⦈(Q ∥ R)) ∈ ?X"
      by auto blast
  }

  note XI = this
  {
    fix xvec :: "name list"
      and Ψ    :: 'b
      and P    :: "('a, 'b, 'c) psi"
      and Q    :: "('a, 'b, 'c) psi"
      and R    :: "('a, 'b, 'c) psi"
      and C    :: "'d::fs_name"

    assume "xvec ♯* Ψ"
      and  A: "⋀A⇩R Ψ⇩R. ⟦extractFrame R = ⟨A⇩R, Ψ⇩R⟩; A⇩R ♯* Ψ; A⇩R ♯* P; A⇩R ♯* Q; A⇩R ♯* C⟧ ⟹ Ψ ⊗ Ψ⇩R ⊳ P ∼ Q"

    from ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈(P ∥ R), ⦇ν*xvec⦈(Q ∥ R)) ∈ ?X"
    proof(rule XI)
      fix A⇩R Ψ⇩R
      assume FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩"
      obtain p::"name prm" where "(p ∙ A⇩R) ♯* Ψ" and "(p ∙ A⇩R) ♯* P" and "(p ∙ A⇩R) ♯* Q" and "(p ∙ A⇩R) ♯* R" and "(p ∙ A⇩R) ♯* C"
        and "(p ∙ A⇩R) ♯* Ψ⇩R" and S: "(set p) ⊆ (set A⇩R) × (set(p ∙ A⇩R))" and "distinctPerm p"
        by(rule name_list_avoiding[where c="(Ψ, P, Q, R, Ψ⇩R, C)"]) auto
      from FrR ‹(p ∙ A⇩R) ♯* Ψ⇩R› S have "extractFrame R = ⟨(p ∙ A⇩R), p ∙ Ψ⇩R⟩" by(simp add: frameChainAlpha')

      moreover assume "A⇩R ♯* Ψ"
      then have "(p ∙ A⇩R) ♯* (p ∙ Ψ)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹A⇩R ♯* Ψ› ‹(p ∙ A⇩R) ♯* Ψ› S have "(p ∙ A⇩R) ♯* Ψ" by simp
      moreover assume "A⇩R ♯* P"
      then have "(p ∙ A⇩R) ♯* (p ∙ P)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹A⇩R ♯* P› ‹(p ∙ A⇩R) ♯* P› S have "(p ∙ A⇩R) ♯* P" by simp
      moreover assume "A⇩R ♯* Q"
      then have "(p ∙ A⇩R) ♯* (p ∙ Q)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹A⇩R ♯* Q› ‹(p ∙ A⇩R) ♯* Q› S have "(p ∙ A⇩R) ♯* Q" by simp
      ultimately have "Ψ ⊗ (p ∙ Ψ⇩R) ⊳ P ∼ Q" using ‹(p ∙ A⇩R) ♯* C› A by blast
      then have "(p ∙ (Ψ ⊗ (p ∙ Ψ⇩R))) ⊳ (p ∙ P) ∼ (p ∙ Q)" by(rule bisimClosed)
      with ‹A⇩R ♯* Ψ› ‹(p ∙ A⇩R) ♯* Ψ› ‹A⇩R ♯* P› ‹(p ∙ A⇩R) ♯* P› ‹A⇩R ♯* Q› ‹(p ∙ A⇩R) ♯* Q› S ‹distinctPerm p›
      show "Ψ ⊗ Ψ⇩R ⊳ P ∼ Q" by(simp add: eqvts)
    qed
  }
  note XI' = this

  have "eqvt ?X"
    unfolding eqvt_def
  proof
    fix x
    assume "x ∈ ?X"
    then obtain xvec Ψ P Q R where 1: "x = (Ψ, ⦇ν*xvec⦈P ∥ R, ⦇ν*xvec⦈Q ∥ R)" and 2: "xvec ♯* Ψ" and
      3: "∀A⇩R Ψ⇩R. extractFrame R = ⟨A⇩R, Ψ⇩R⟩ ∧ A⇩R ♯* Ψ ∧ A⇩R ♯* P ∧ A⇩R ♯* Q ⟶ Ψ ⊗ Ψ⇩R ⊳ P ∼ Q"
      by blast
    show "∀p::(name × name) list. p ∙ x ∈ ?X"
    proof
      fix p :: "(name × name) list"
      from 1 have "p ∙ x = (p ∙ Ψ, ⦇ν*p ∙ xvec⦈(p ∙ P) ∥ (p ∙ R), ⦇ν*p ∙ xvec⦈(p ∙ Q) ∥ (p ∙ R))"
        by (simp add: eqvts)
      moreover from 2 have "(p ∙ xvec) ♯* (p ∙ Ψ)"
        by (simp add: fresh_star_bij(2))
      moreover have "∀A⇩R Ψ⇩R. extractFrame (p ∙ R) = ⟨A⇩R, Ψ⇩R⟩ ∧ A⇩R ♯* (p ∙ Ψ) ∧ A⇩R ♯* (p ∙ P) ∧ A⇩R ♯* (p ∙ Q) ⟶ (p ∙ Ψ) ⊗ Ψ⇩R ⊳ (p ∙ P) ∼ (p ∙ Q)"
      proof (rule allI, rule allI, rule impI, (erule conjE)+)
        fix A⇩R Ψ⇩R
        assume exF: "extractFrame (p ∙ R) = ⟨A⇩R, Ψ⇩R⟩" and freshPsi: "A⇩R ♯* (p ∙ Ψ)" and freshP: "A⇩R ♯* (p ∙ P)" and freshQ: "A⇩R ♯* (p ∙ Q)"
        from exF have "extractFrame R = ⟨rev p ∙ A⇩R, rev p ∙ Ψ⇩R⟩"
          by (metis Chain.simps(5) extractFrameEqvt(1) frame.perm(1) frameResChainEqvt)
        moreover from freshPsi have "(rev p ∙ A⇩R) ♯* Ψ"
          by (metis fresh_star_bij(2) perm_pi_simp(1))
        moreover from freshP have "(rev p ∙ A⇩R) ♯* P"
          by (metis fresh_star_bij(2) perm_pi_simp(1))
        moreover from freshQ have "(rev p ∙ A⇩R) ♯* Q"
          by (metis fresh_star_bij(2) perm_pi_simp(1))
        ultimately show "(p ∙ Ψ) ⊗ Ψ⇩R ⊳ p ∙ P ∼ p ∙ Q"
          using 3 by (metis (no_types, opaque_lifting) bisimClosed perm_pi_simp(2) statEqvt')
      qed
      ultimately show "p ∙ x ∈ ?X"
        by blast
    qed
  qed

  moreover have Res: "⋀Ψ P Q x. ⟦(Ψ, P, Q) ∈ ?X ∪ bisim; x ♯ Ψ⟧ ⟹ (Ψ, ⦇νx⦈P, ⦇νx⦈Q) ∈ ?X ∪ bisim"
  proof -
    fix Ψ P Q x
    assume "(Ψ, P, Q) ∈ ?X ∪ bisim" and "(x::name) ♯ Ψ"
    show "(Ψ, ⦇νx⦈P, ⦇νx⦈Q) ∈ ?X ∪ bisim"
    proof(cases "(Ψ, P, Q) ∈ ?X")
      assume "(Ψ, P, Q) ∈ ?X"
      then obtain xvec P' Q' R where "P = ⦇ν*xvec⦈P' ∥ R" and "Q = ⦇ν*xvec⦈Q' ∥ R" and "xvec ♯* Ψ"
          and "∀A⇩R Ψ⇩R. extractFrame R = ⟨A⇩R, Ψ⇩R⟩ ∧ A⇩R ♯* Ψ ∧ A⇩R ♯* P' ∧ A⇩R ♯* Q' ⟶ Ψ ⊗ Ψ⇩R ⊳ P' ∼ Q'"
        by blast
      moreover have "⦇νx⦈(⦇ν*xvec⦈P' ∥ R) = ⦇ν*(x # xvec)⦈P' ∥ R"
        by simp
      moreover have "⦇νx⦈(⦇ν*xvec⦈Q' ∥ R) = ⦇ν*(x # xvec)⦈Q' ∥ R"
        by simp
      moreover from ‹x ♯ Ψ› ‹xvec ♯* Ψ› have "(x # xvec) ♯* Ψ"
        by simp
      ultimately have "(Ψ, ⦇νx⦈P, ⦇νx⦈Q) ∈ ?X"
        by blast
      then show ?thesis by simp
    next
      assume "¬(Ψ, P, Q) ∈ ?X"
      with ‹(Ψ, P, Q) ∈ ?X ∪ bisim› have "Ψ ⊳ P ∼ Q"
        by blast
      then have "Ψ ⊳ ⦇νx⦈P ∼ ⦇νx⦈Q" using ‹x ♯ Ψ›
        by(rule bisimResPres)
      then show ?thesis
        by simp
    qed
  qed
  have ResChain: "⋀Ψ P Q xvec. ⟦(Ψ, P, Q) ∈ ?X ∪ bisim; xvec ♯* Ψ⟧ ⟹ (Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) ∈ ?X ∪ bisim"
  proof -
    fix Ψ P Q
      and xvec::"name list"
    assume "(Ψ, P, Q) ∈ ?X ∪ bisim"
      and "xvec ♯* Ψ"
    then show "(Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) ∈ ?X ∪ bisim"
    proof(induct xvec)
      case Nil then show ?case by simp
    next
      case(Cons x xvec)
      then have "(Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) ∈ ?X ∪ bisim"
        by simp
      moreover have "x ♯ Ψ" using Cons by simp
      ultimately show ?case unfolding resChain.simps
        by(rule Res)
    qed
  qed
  have "(Ψ, P ∥ R, Q ∥ R) ∈ ?X"
  proof -
    {
      fix A⇩R' :: "name list"
        and Ψ⇩R' :: 'b

      assume FrR': "extractFrame R = ⟨A⇩R', Ψ⇩R'⟩"
        and  "A⇩R' ♯* Ψ"
        and  "A⇩R' ♯* P"
        and  "A⇩R' ♯* Q"

      obtain p where "(p ∙ A⇩R') ♯* A⇩R" and "(p ∙ A⇩R') ♯* Ψ⇩R'" and "(p ∙ A⇩R') ♯* Ψ" and "(p ∙ A⇩R') ♯* P" and "(p ∙ A⇩R') ♯* Q"
        and Sp: "(set p) ⊆ (set A⇩R') × (set(p ∙ A⇩R'))" and "distinctPerm p"
        by(rule name_list_avoiding[where c="(A⇩R, Ψ, Ψ⇩R', P, Q)"]) auto

      from FrR' ‹(p ∙ A⇩R') ♯*  Ψ⇩R'› Sp have "extractFrame R = ⟨(p ∙ A⇩R'), p ∙ Ψ⇩R'⟩"
        by(simp add: frameChainAlpha eqvts)
      with FrR ‹(p ∙ A⇩R') ♯* A⇩R› obtain q::"name prm"
        where Sq: "set q ⊆ set(p ∙ A⇩R') × set A⇩R" and "distinctPerm q" and "Ψ⇩R = q ∙ p ∙ Ψ⇩R'"
        by(force elim: frameChainEq)

      from ‹Ψ ⊗ Ψ⇩R ⊳ P ∼ Q› ‹Ψ⇩R = q ∙ p ∙ Ψ⇩R'› have "Ψ ⊗ (q ∙ p ∙ Ψ⇩R') ⊳ P ∼ Q" by simp
      then have "(q ∙ (Ψ ⊗ (q ∙ p ∙ Ψ⇩R'))) ⊳ (q ∙ P) ∼ (q ∙ Q)" by(rule bisimClosed)
      with Sq ‹A⇩R ♯* Ψ› ‹(p ∙ A⇩R') ♯* Ψ› ‹A⇩R ♯* P› ‹(p ∙ A⇩R') ♯* P› ‹A⇩R ♯* Q› ‹(p ∙ A⇩R') ♯* Q› ‹distinctPerm q›
      have "Ψ ⊗ (p ∙ Ψ⇩R') ⊳ P ∼ Q" by(simp add: eqvts)
      then have "(p ∙ (Ψ ⊗ (p ∙ Ψ⇩R'))) ⊳ (p ∙ P) ∼ (p ∙ Q)" by(rule bisimClosed)
      with Sp ‹A⇩R' ♯* Ψ› ‹(p ∙ A⇩R') ♯* Ψ› ‹A⇩R' ♯* P› ‹(p ∙ A⇩R') ♯* P› ‹A⇩R' ♯* Q› ‹(p ∙ A⇩R') ♯* Q› ‹distinctPerm p›
      have "Ψ ⊗ Ψ⇩R' ⊳ P ∼ Q" by(simp add: eqvts)
    }
    then show ?thesis
      apply clarsimp
      apply(rule exI[where x="[]"])
      by auto blast
  qed
  then show ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ PR QR)
    from ‹(Ψ, PR, QR) ∈ ?X›
    obtain xvec P Q R where PFrR: "PR = ⦇ν*xvec⦈(P ∥ R)" and QFrR: "QR = ⦇ν*xvec⦈(Q ∥ R)"
      and "xvec ♯* Ψ" and *: "∀A⇩R Ψ⇩R. extractFrame R = ⟨A⇩R, Ψ⇩R⟩ ∧ A⇩R ♯* Ψ ∧ A⇩R ♯* P ∧ A⇩R ♯* Q ⟶ Ψ ⊗ Ψ⇩R ⊳ P ∼ Q"
      by blast
    obtain A⇩R Ψ⇩R where FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" and fresh: "A⇩R ♯* (Ψ, P, Q, R)"
      using freshFrame by metis
    from fresh have "A⇩R ♯* Ψ" and "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* R"
      by auto
    with FrR have PSimQ: "Ψ ⊗ Ψ⇩R ⊳ P ∼ Q"
      using * by blast

    obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "A⇩P ♯* A⇩R" and "A⇩P ♯* Ψ⇩R"
      by(rule freshFrame[where C="(Ψ, A⇩R, Ψ⇩R)"]) auto
    obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* A⇩R" and "A⇩Q ♯* Ψ⇩R"
      by(rule freshFrame[where C="(Ψ, A⇩R, Ψ⇩R)"]) auto
    from ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩P ♯* A⇩R› ‹A⇩Q ♯* A⇩R› FrP FrQ have "A⇩R ♯* Ψ⇩P" and  "A⇩R ♯* Ψ⇩Q"
      by(force dest: extractFrameFreshChain)+

    have "⟨(A⇩P@A⇩R), Ψ ⊗ Ψ⇩P ⊗ Ψ⇩R⟩ ≃⇩F ⟨(A⇩Q@A⇩R), Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R⟩"
    proof -
      have "⟨A⇩P, Ψ ⊗ Ψ⇩P ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩P, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P⟩"
        by(metis frameResChainPres frameNilStatEq Associativity Commutativity AssertionStatEqTrans Composition)
      moreover from PSimQ have "insertAssertion(extractFrame P) (Ψ ⊗ Ψ⇩R) ≃⇩F insertAssertion(extractFrame Q) (Ψ ⊗ Ψ⇩R)"
        by(rule bisimE)
      with FrP FrQ freshCompChain ‹A⇩P ♯* Ψ› ‹A⇩P ♯* Ψ⇩R› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Ψ⇩R› have "⟨A⇩P, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P⟩ ≃⇩F ⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩"
        by auto
      moreover have "⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩ ≃⇩F ⟨A⇩Q, Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R⟩"
        by(metis frameResChainPres frameNilStatEq Associativity Commutativity AssertionStatEqTrans Composition)
      ultimately have "⟨A⇩P, Ψ ⊗ Ψ⇩P ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q, Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R⟩"
        by(blast intro: FrameStatEqTrans)
      then have "⟨(A⇩R@A⇩P), Ψ ⊗ Ψ⇩P ⊗ Ψ⇩R⟩ ≃⇩F ⟨(A⇩R@A⇩Q), Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R⟩"
        by(drule_tac frameResChainPres) (simp add: frameChainAppend)
      then show ?thesis
        apply(simp add: frameChainAppend)
        by(metis frameResChainComm FrameStatEqTrans)
    qed
    moreover from ‹A⇩P ♯* Ψ› ‹A⇩R ♯* Ψ› have "(A⇩P@A⇩R) ♯* Ψ" by simp
    moreover from ‹A⇩Q ♯* Ψ› ‹A⇩R ♯* Ψ› have "(A⇩Q@A⇩R) ♯* Ψ" by simp
    ultimately have PFrRQR: "insertAssertion(extractFrame(P ∥ R)) Ψ ≃⇩F insertAssertion(extractFrame(Q ∥ R)) Ψ"
      using FrP FrQ FrR ‹A⇩P ♯* A⇩R› ‹A⇩P ♯* Ψ⇩R› ‹A⇩Q ♯* A⇩R› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩R ♯* Ψ⇩P› ‹A⇩R ♯* Ψ⇩Q›
      by simp

    from ‹xvec ♯* Ψ› have "insertAssertion (extractFrame(⦇ν*xvec⦈P ∥ R)) Ψ ≃⇩F ⦇ν*xvec⦈(insertAssertion (extractFrame(P ∥ R)) Ψ)"
      by(rule insertAssertionExtractFrameFresh)
    moreover from PFrRQR have "⦇ν*xvec⦈(insertAssertion (extractFrame(P ∥ R)) Ψ) ≃⇩F ⦇ν*xvec⦈(insertAssertion (extractFrame(Q ∥ R)) Ψ)"
      by(induct xvec) (auto intro: frameResPres)
    moreover from ‹xvec ♯* Ψ› have "⦇ν*xvec⦈(insertAssertion (extractFrame(Q ∥ R)) Ψ) ≃⇩F insertAssertion (extractFrame(⦇ν*xvec⦈Q ∥ R)) Ψ"
      by(rule FrameStatEqSym[OF insertAssertionExtractFrameFresh])
    ultimately show ?case using PFrR QFrR
      by(blast intro: FrameStatEqTrans)
  next
    case(cSim Ψ PR QR)
    {
      fix Ψ P Q R xvec
      assume "⋀A⇩R Ψ⇩R. ⟦extractFrame R = ⟨A⇩R, Ψ⇩R⟩; A⇩R ♯* Ψ; A⇩R ♯* P; A⇩R ♯* Q⟧ ⟹ Ψ ⊗ Ψ⇩R ⊳ P ∼ Q"
      moreover have "eqvt bisim" by simp
      moreover from ‹eqvt ?X› have "eqvt(?X ∪ bisim)" by auto
      moreover from bisimE(1) have "⋀Ψ P Q. Ψ ⊳ P ∼ Q ⟹ insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P) Ψ" by(simp add: FrameStatEq_def)
      moreover note bisimE(2) bisimE(3)
      moreover
      {
        fix Ψ P Q A⇩R Ψ⇩R R
        assume PSimQ: "Ψ ⊗ Ψ⇩R ⊳ P ∼ Q"
          and FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩"
          and "A⇩R ♯* Ψ"
          and "A⇩R ♯* P"
          and "A⇩R ♯* Q"
        then have "(Ψ, P ∥ R, Q ∥ R) ∈ ?X"
        proof -
          have "P ∥ R = ⦇ν*[]⦈(P ∥ R)" by simp
          moreover have "Q ∥ R = ⦇ν*[]⦈(Q ∥ R)" by simp
          moreover have "([]::name list) ♯* Ψ" by simp
          moreover
          {
            fix A⇩R' Ψ⇩R'

            assume FrR': "extractFrame R = ⟨A⇩R', Ψ⇩R'⟩"
              and "A⇩R' ♯* Ψ"
              and "A⇩R' ♯* P"
              and "A⇩R' ♯* Q"
            obtain p where "(p ∙ A⇩R') ♯* A⇩R"
              and "(p ∙ A⇩R') ♯* Ψ⇩R'"
              and "(p ∙ A⇩R') ♯* Ψ"
              and "(p ∙ A⇩R') ♯* P"
              and "(p ∙ A⇩R') ♯* Q"
              and S: "(set p) ⊆ (set A⇩R') × (set(p ∙ A⇩R'))" and "distinctPerm p"
              by(rule name_list_avoiding[where c="(A⇩R, Ψ, Ψ⇩R', P, Q)"]) auto

            from ‹(p ∙ A⇩R') ♯* Ψ⇩R'› S have "⟨A⇩R', Ψ⇩R'⟩ = ⟨p ∙ A⇩R', p ∙ Ψ⇩R'⟩"
              by(simp add: frameChainAlpha)

            with FrR' have FrR'': "extractFrame R = ⟨p ∙ A⇩R', p ∙ Ψ⇩R'⟩" by simp
            with FrR ‹(p ∙ A⇩R') ♯* A⇩R›
            obtain q where "p ∙ Ψ⇩R' = (q::name prm) ∙ Ψ⇩R" and S': "set q ⊆ (set A⇩R) × set(p ∙ A⇩R')" and "distinctPerm q"
              apply clarsimp
              apply(drule sym)
              apply simp
              by(drule frameChainEq) auto
            from PSimQ have "(q ∙ (Ψ ⊗ Ψ⇩R)) ⊳ (q ∙ P) ∼ (q ∙ Q)"
              by(rule bisimClosed)
            with ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹(p ∙ A⇩R') ♯* Ψ› ‹(p ∙ A⇩R') ♯* P› ‹(p ∙ A⇩R') ♯* Q› S'
            have "Ψ ⊗ (q ∙ Ψ⇩R) ⊳ P ∼ Q" by(simp add: eqvts)
            then have "(p ∙ (Ψ ⊗ (q ∙ Ψ⇩R))) ⊳ (p ∙ P) ∼ (p ∙ Q)" by(rule bisimClosed)
            with ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P› ‹A⇩R' ♯* Q› ‹(p ∙ A⇩R') ♯* Ψ› ‹(p ∙ A⇩R') ♯* P› ‹(p ∙ A⇩R') ♯* Q› S ‹distinctPerm p› ‹(p ∙ Ψ⇩R') = q ∙ Ψ⇩R›
            have "Ψ ⊗ Ψ⇩R' ⊳ P ∼ Q"
              by(drule_tac sym) (simp add: eqvts)
          }
          ultimately show ?thesis
            by blast
        qed
        then have "(Ψ, P ∥ R, Q ∥ R) ∈ ?X ∪ bisim"
          by simp
      }
      moreover have "⋀Ψ P Q xvec. ⟦(Ψ, P, Q) ∈ ?X ∪ bisim; (xvec::name list) ♯* Ψ⟧ ⟹ (Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) ∈ ?X ∪ bisim"
      proof -
        fix Ψ P Q xvec
        assume "(Ψ, P, Q) ∈ ?X ∪ bisim"
        assume "(xvec::name list) ♯* Ψ"
        then show "(Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) ∈ ?X ∪ bisim"
        proof(induct xvec)
          case Nil
          then show ?case using ‹(Ψ, P, Q) ∈ ?X ∪ bisim› by simp
        next
          case(Cons x xvec)
          then show ?case by(simp only: resChain.simps) (rule Res, auto)
        qed
      qed
      ultimately have "Ψ ⊳ P ∥ R ↝[(?X ∪ bisim)] Q ∥ R" using statEqBisim
        by(rule parPres)
      moreover assume "(xvec::name list) ♯* Ψ"
      moreover from ‹eqvt ?X› have "eqvt(?X ∪ bisim)" by auto
      ultimately have "Ψ ⊳ ⦇ν*xvec⦈(P ∥ R) ↝[(?X ∪ bisim)] ⦇ν*xvec⦈(Q ∥ R)" using ResChain
        by(intro resChainPres)
    }
    with ‹(Ψ, PR, QR) ∈ ?X› show ?case by blast
  next
    case(cExt Ψ PR QR Ψ')

    from ‹(Ψ, PR, QR) ∈ ?X›
    obtain xvec P Q R A⇩R Ψ⇩R where PFrR: "PR = ⦇ν*xvec⦈(P ∥ R)" and QFrR: "QR = ⦇ν*xvec⦈(Q ∥ R)"
      and "xvec ♯* Ψ" and A: "∀A⇩R Ψ⇩R. (extractFrame R = ⟨A⇩R, Ψ⇩R⟩ ∧ A⇩R ♯* Ψ ∧ A⇩R ♯* P ∧ A⇩R ♯* Q) ⟶ Ψ ⊗ Ψ⇩R ⊳ P ∼ Q"
      by auto

    obtain p where "(p ∙ xvec) ♯* Ψ"
      and "(p ∙ xvec) ♯* P"
      and "(p ∙ xvec) ♯* Q"
      and "(p ∙ xvec) ♯* R"
      and "(p ∙ xvec) ♯* Ψ'"
      and S: "(set p) ⊆ (set xvec) × (set(p ∙ xvec))" and "distinctPerm p"
      by(rule name_list_avoiding[where c="(Ψ, P, Q, R, Ψ')"]) auto

    from ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* R› S have "⦇ν*xvec⦈(P ∥ R) = ⦇ν*(p ∙ xvec)⦈(p ∙ (P ∥ R))"
      by(subst resChainAlpha) auto
    then have PRAlpha: "⦇ν*xvec⦈(P ∥ R) = ⦇ν*(p ∙ xvec)⦈((p ∙ P) ∥ (p ∙ R))"
      by(simp add: eqvts)

    from ‹(p ∙ xvec) ♯* Q› ‹(p ∙ xvec) ♯* R› S have "⦇ν*xvec⦈(Q ∥ R) = ⦇ν*(p ∙ xvec)⦈(p ∙ (Q ∥ R))"
      by(subst resChainAlpha) auto
    then have QRAlpha: "⦇ν*xvec⦈(Q ∥ R) = ⦇ν*(p ∙ xvec)⦈((p ∙ Q) ∥ (p ∙ R))"
      by(simp add: eqvts)

    have "(Ψ ⊗ Ψ', ⦇ν*(p ∙ xvec)⦈((p ∙ P) ∥ (p ∙ R)), ⦇ν*(p ∙ xvec)⦈((p ∙ Q) ∥ (p ∙ R))) ∈ ?X"
    proof(rule XI'[where C2="(Ψ, (p ∙ P), (p ∙ Q), R, Ψ', xvec, p ∙ xvec)"])
      show "(p ∙ xvec) ♯* (Ψ ⊗ Ψ')"
        using ‹(p ∙ xvec) ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ'› by auto
    next
      fix A⇩R Ψ⇩R
      assume FrR: "extractFrame (p ∙ R) = ⟨A⇩R, Ψ⇩R⟩" and "A⇩R ♯* (Ψ ⊗ Ψ')" and "A⇩R ♯* (p ∙ P)" and "A⇩R ♯* (Ψ, p ∙ P, p ∙ Q, R, Ψ', xvec, p ∙ xvec)"
      then have "A⇩R ♯* Ψ" and "A⇩R ♯* (p ∙ Q)"
        by simp_all
      from FrR have "(p ∙ (extractFrame (p ∙ R))) = (p ∙ ⟨A⇩R, Ψ⇩R⟩)"
        by simp
      with ‹distinctPerm p› have "extractFrame R = ⟨p ∙ A⇩R, p ∙ Ψ⇩R⟩"
        by(simp add: eqvts)
      moreover 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
      moreover from ‹A⇩R ♯* (p ∙ P)› have "(p ∙ A⇩R) ♯* (p ∙ p ∙ P)"
        by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹distinctPerm p› have "(p ∙ A⇩R) ♯* P"
        by simp
      moreover from ‹A⇩R ♯* (p ∙ Q)› have "(p ∙ A⇩R) ♯* (p ∙ p ∙ Q)"
        by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹distinctPerm p› have "(p ∙ A⇩R) ♯* Q"
        by simp
      ultimately have "Ψ ⊗ (p ∙ Ψ⇩R) ⊳ P ∼ Q"
        using A by blast
      then have "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ (p ∙ Ψ') ⊳ P ∼ Q"
        by(rule bisimE)
      moreover have "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ (p ∙ Ψ') ≃ (Ψ ⊗ (p ∙ Ψ')) ⊗ (p ∙ Ψ⇩R)"
        by(metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym)
      ultimately have "(Ψ ⊗ (p ∙ Ψ')) ⊗ (p ∙ Ψ⇩R) ⊳ P ∼ Q"
        by(rule statEqBisim)
      then have "(p ∙ ((Ψ ⊗ (p ∙ Ψ')) ⊗ (p ∙ Ψ⇩R))) ⊳ (p ∙ P) ∼ (p ∙ Q)"
        by(rule bisimClosed)
      with ‹distinctPerm p› ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S show "(Ψ ⊗ Ψ') ⊗ Ψ⇩R ⊳ (p ∙ P) ∼ (p ∙ Q)"
        by(simp add: eqvts)
    qed
    with PFrR QFrR PRAlpha QRAlpha show ?case by simp
  next
    case(cSym Ψ PR QR)
    then show ?case by(blast dest: bisimE)
  qed
qed

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

assumes "Ψ ⊳ P ∼ Q"

shows "Ψ ⊳ P ∥ R ∼ Q ∥ R"
proof -
  obtain A⇩R Ψ⇩R where "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" and "A⇩R ♯* Ψ" and "A⇩R ♯* P" and "A⇩R ♯* Q"
    by(rule freshFrame[where C="(Ψ, P, Q)"]) auto
  moreover from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊗ Ψ⇩R ⊳ P ∼ Q" by(rule bisimE)
  ultimately show ?thesis by(intro bisimParPresAux)
qed

end

end