(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Bisim_Pres
  imports Bisimulation Sim_Pres
begin

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
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ P Q)
    thus ?case by auto
  next
    case(cSim Ψ P Q)
    thus ?case by(blast intro: inputPres)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(blast dest: bisimE)
  next
    case(cSym Ψ P Q)
    thus ?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
  thus ?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) mem CsP ==> ∃Q. (φ, Q) mem CsQ ∧ guarded Q ∧ Ψ ⊳ P ∼ Q"
  and     "∧φ Q. (φ, Q) mem CsQ ==> ∃P. (φ, P) mem CsP ∧ guarded P ∧ Ψ ⊳ P ∼ Q"

  shows "Ψ ⊳ Cases CsP ∼ Cases CsQ"
proof -
  let ?X = "{(Ψ, Cases CsP, Cases CsQ) | Ψ CsP CsQ. (∀φ P. (φ, P) mem CsP ⟶ (∃Q. (φ, Q) mem CsQ ∧ guarded Q ∧ Ψ ⊳ P ∼ Q)) ∧
                                                     (∀φ Q. (φ, Q) mem CsQ ⟶ (∃P. (φ, P) mem CsP ∧ guarded P ∧ Ψ ⊳ P ∼ Q))}"
  from assms have "(Ψ, Cases CsP, Cases CsQ) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ P Q)
    thus ?case by auto
  next
    case(cSim Ψ CasesP CasesQ)
    then obtain CsP CsQ where C1: "∧φ Q. (φ, Q) mem CsQ ==> ∃P. (φ, P) mem 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)
    thus ?case using A B by blast
  next
    case(cExt Ψ P Q)
    thus ?case by(blast dest: bisimE)
  next
    case(cSym Ψ P Q)
    thus ?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 = "{(Ψ, (νx)P, (νx)Q) | Ψ x P Q. Ψ ⊳ P ∼ Q ∧ x ♯ Ψ}"
  
  from assms have "(Ψ, (νx)P, (νx)Q) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ xP xQ)
    from ‹(Ψ, xP, xQ) ∈ ?X› obtain x P Q where "Ψ ⊳ P ∼ Q" and "x ♯ Ψ" and "xP = (νx)P" and "xQ = (νx)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: frameResPres)
  next
    case(cSim Ψ xP xQ)
    from ‹(Ψ, xP, xQ) ∈ ?X› obtain x P Q where "Ψ ⊳ P ∼ Q" and "x ♯ Ψ" and "xP = (νx)P" and "xQ = (νx)Q"
      by auto
    from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊳ P ↝[bisim] Q" by(rule bisimE)
    moreover have "eqvt ?X"
      by(force simp add: eqvt_def bisimClosed pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
    hence "eqvt(?X ∪ bisim)" by auto
    moreover note ‹x ♯ Ψ›
    moreover have "bisim ⊆ ?X ∪ bisim" by auto
    moreover have "∧Ψ P Q x. [(Ψ, P, Q) ∈ bisim; x ♯ Ψ] ==> (Ψ, (νx)P, (νx)Q) ∈ ?X ∪ bisim"
      by auto
    ultimately have "Ψ ⊳ (νx)P ↝[(?X ∪ bisim)] (νx)Q"
      by(rule resPres)
    with ‹xP = (νx)P› ‹xQ = (νx)Q› show ?case
      by simp
  next
    case(cExt Ψ xP xQ Ψ')
    from ‹(Ψ, xP, xQ) ∈ ?X› obtain x P Q where "Ψ ⊳ P ∼ Q" and "x ♯ Ψ" and "xP = (νx)P" and "xQ = (νx)Q"
      by auto
    obtain y::name where "y ♯ P" and "y ♯ Q" and "y ♯ Ψ" and "y ♯ Ψ'"
     by(generate_fresh "name", auto simp add: fresh_prod)
   from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊗ ([(x, y)] ∙ Ψ') ⊳ P ∼ Q"
     by(rule bisimE)
   hence "([(x, y)] ∙ (Ψ ⊗ ([(x, y)] ∙ Ψ'))) ⊳ ([(x, y)] ∙ P) ∼ ([(x, y)] ∙ Q)"
     by(rule bisimClosed)
   with ‹x ♯ Ψ› ‹y ♯ Ψ› have "Ψ ⊗ Ψ' ⊳ ([(x, y)] ∙ P) ∼ ([(x, y)] ∙ Q)"
     by(simp add: eqvts)
   with ‹y ♯ Ψ› ‹y ♯ Ψ'› have "(Ψ ⊗ Ψ', (νy)([(x, y)] ∙ P), (νy)([(x, y)] ∙ Q)) ∈ ?X"
     by auto
   moreover from ‹y ♯ P› ‹y ♯ Q› have "(νx)P = (νy)([(x, y)] ∙ P)" and "(νx)Q = (νy)([(x, y)] ∙ Q)"
     by(simp add: alphaRes)+
   ultimately show ?case using ‹xP = (νx)P› ‹xQ = (νx)Q› by simp
 next
    case(cSym Ψ P Q)
    thus ?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"

    hence "(Ψ, (ν*xvec)(P ∥ R), (ν*xvec)(Q ∥ R)) ∈ ?X"
      apply auto
      by 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_tac c="(Ψ, P, Q, R, Ψ_R, C)" in name_list_avoiding) auto
      from FrR ‹(p ∙ A_R) ♯* Ψ_R› S have "extractFrame R = ⟨(p ∙ A_R), p ∙ Ψ_R⟩" by(simp add: frameChainAlpha')

      moreover assume "A_R ♯* Ψ"
      hence "(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"
      hence "(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"
      hence "(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
      hence "(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"
    apply(auto simp add: eqvt_def)
    apply(rule_tac x="p ∙ xvec" in exI)
    apply(rule_tac x="p ∙ P" in exI)
    apply(rule_tac x="p ∙ Q" in exI)
    apply(rule_tac x="p ∙ R" in exI)
    apply(simp add: eqvts)
    apply(simp add: fresh_star_bij)
    apply(clarify)
    apply(erule_tac x="(rev p) ∙ A_R" in allE)
    apply(erule_tac x="(rev p) ∙ Ψ_R" in allE)
    apply(drule mp)
    apply(rule conjI)
    apply(rule_tac pi=p in pt_bij4[OF pt_name_inst, OF at_name_inst])
    apply(simp add: eqvts)
    defer
    apply(drule_tac p=p in bisimClosed)
    apply(simp add: eqvts)
    apply(subst pt_fresh_star_bij[OF pt_name_inst,OF at_name_inst, of p, THEN sym])
    apply simp
    apply(subst pt_fresh_star_bij[OF pt_name_inst,OF at_name_inst, of p, THEN sym])
    apply simp
    apply(subst pt_fresh_star_bij[OF pt_name_inst,OF at_name_inst, of p, THEN sym])
    by simp

  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(case_tac "(Ψ, P, Q) ∈ ?X")
      assume "(Ψ, P, Q) ∈ ?X"
      with ‹x ♯ Ψ› have "(Ψ, (νx)P, (νx)Q) ∈ ?X"
        apply auto
        by(rule_tac x="x#xvec" in exI) auto
      thus ?thesis by simp
    next
      assume "¬(Ψ, P, Q) ∈ ?X"
      with ‹(Ψ, P, Q) ∈ ?X ∪ bisim› have "Ψ ⊳ P ∼ Q"
        by blast
      hence "Ψ ⊳ (νx)P ∼ (νx)Q" using ‹x ♯ Ψ›
        by(rule bisimResPres)
      thus ?thesis
        by simp
    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_tac c="(A_R, Ψ, Ψ_R', P, Q)" in name_list_avoiding) 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
      hence "(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)
      hence "(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)
    }
    thus ?thesis
      apply auto
      apply(rule_tac x="[]" in exI)
      by auto blast
  qed
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ 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 FrR: "extractFrame R = ⟨A_R, Ψ_R⟩" and PSimQ: "Ψ ⊗ Ψ_R ⊳ P ∼ Q"
                              and "A_R ♯* xvec" and "A_R ♯* Ψ" and "A_R ♯* P" and "A_R ♯* Q" and "A_R ♯* R"
      apply auto
      apply(subgoal_tac "∃A_R Ψ_R. extractFrame R = ⟨A_R, Ψ_R⟩ ∧ A_R ♯* (xvec, Ψ, P, Q, R)")
      apply auto
      apply(rule_tac F="extractFrame R" and C="(xvec, Ψ, P, Q, R)" in freshFrame)
      by auto

    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_tac C="(Ψ, A_R, Ψ_R)" in freshFrame) 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_tac C="(Ψ, A_R, Ψ_R)" in freshFrame) 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)
      hence "⟨(A_R@A_P), Ψ ⊗ Ψ_P ⊗ Ψ_R⟩ ≃_F ⟨(A_R@A_Q), Ψ ⊗ Ψ_Q ⊗ Ψ_R⟩"
        by(drule_tac frameResChainPres) (simp add: frameChainAppend)
      thus ?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"
        hence "(Ψ, 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_tac c="(A_R, Ψ, Ψ_R', P, Q)" in name_list_avoiding) 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 auto
              apply(drule_tac sym) apply simp
              by(drule_tac 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)
            hence "(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
        hence "(Ψ, 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) ♯* Ψ"
        thus "(Ψ, (ν*xvec)P, (ν*xvec)Q) ∈ ?X ∪ bisim"
        proof(induct xvec)
          case Nil
          thus ?case using ‹(Ψ, P, Q) ∈ ?X ∪ bisim› by simp
        next
          case(Cons x xvec)
          thus ?case by(simp only: resChain.simps) (rule_tac 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 Res
        by(rule_tac 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_tac c="(Ψ, P, Q, R, Ψ')" in name_list_avoiding) auto

    from ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* R› S have "(ν*xvec)(P ∥ R) = (ν*(p ∙ xvec))(p ∙ (P ∥ R))"
      by(subst resChainAlpha) auto
    hence 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
    hence QRAlpha: "(ν*xvec)(Q ∥ R) = (ν*(p ∙ xvec))((p ∙ Q) ∥ (p ∙ R))"
      by(simp add: eqvts)

    from ‹(p ∙ xvec) ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ'› have "(Ψ ⊗ Ψ', (ν*(p ∙ xvec))((p ∙ P) ∥ (p ∙ R)), (ν*(p ∙ xvec))((p ∙ Q) ∥ (p ∙ R))) ∈ ?X"
    proof(rule_tac C2="(Ψ, (p ∙ P), (p ∙ Q), R, Ψ', xvec, p ∙ xvec)" in XI', auto)
      fix A_R Ψ_R
      assume FrR: "extractFrame (p ∙ R) = ⟨A_R, Ψ_R⟩" and "A_R ♯* Ψ" and "A_R ♯* Ψ'" and "A_R ♯* (p ∙ P)" and "A_R ♯* (p ∙ Q)"
      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
      hence "(Ψ ⊗ (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)
      hence "(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)
    thus ?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_tac C="(Ψ, P, Q)" in freshFrame) auto
  moreover from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊗ Ψ_R ⊳ P ∼ Q" by(rule bisimE)
  ultimately show ?thesis by(rule_tac bisimParPresAux)
qed

end

end