Theory Bisim_Pres

(* 
   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