Theory Weak_Bisim_Pres

(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Bisim_Pres
  imports Weak_Bisimulation Weak_Sim_Pres Weak_Stat_Imp_Pres
begin

context env begin

lemma weakBisimInputPres:
  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: weakBisimCoinduct)
    case(cStatImp Ψ P Q)
    thus ?case by(fastforce intro: weakStatImpInputPres dest: weakBisimE(3))
  next
    case(cSim Ψ P Q)
    thus ?case
      by auto (blast intro: weakInputPres dest: weakBisimE)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(blast dest: weakBisimE)
  next
    case(cSym Ψ P Q)
    thus ?case by(blast dest: weakBisimE)
  qed
qed
  
lemma weakBisimOutputPres:
  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 ≈ Q"

  shows "Ψ ⊳ M⟨N⟩.P ≈ M⟨N⟩.Q"
proof -
  let ?X = "{(Ψ, M⟨N⟩.P, M⟨N⟩.Q) | Ψ M N P Q. Ψ ⊳ P ≈ Q}"

  from assms have "(Ψ, M⟨N⟩.P, M⟨N⟩.Q) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cStatImp Ψ P Q)
    thus ?case by auto (blast intro: weakStatImpOutputPres dest: weakBisimE(3))
  next
    case(cSim Ψ P Q)
    thus ?case
      by(auto intro: weakOutputPres dest: weakBisimE)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(blast dest: weakBisimE)
  next
    case(cSym Ψ P Q)
    thus ?case by(blast dest: weakBisimE)
  qed
qed

lemma weakBisimResPres:
  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: weakBisimCoinduct)
    case(cStatImp Ψ xP xQ)
    {
      fix Ψ P Q x
      assume "Ψ ⊳ P ≈ Q"
      hence "Ψ ⊳ P ⪅<weakBisim> Q" by(rule weakBisimE)
      moreover have "eqvt weakBisim" by auto
      moreover assume "(x::name) ♯ Ψ"
      moreover have "⋀Ψ P Q x. ⟦(Ψ, P, Q) ∈ weakBisim; x ♯ Ψ⟧ ⟹ (Ψ, ⦇νx⦈P, ⦇νx⦈Q) ∈ ?X ∪ weakBisim"
        by auto
      ultimately have "Ψ ⊳ ⦇νx⦈P ⪅<(?X ∪ weakBisim)> ⦇νx⦈Q"
        by(rule weakStatImpResPres)
    }
    with ‹(Ψ, xP, xQ) ∈ ?X› show ?case by auto
  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 ↝<weakBisim> Q" by(rule weakBisimE)
    moreover have "eqvt ?X"
      by(force simp add: eqvt_def weakBisimClosed pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
    hence "eqvt(?X ∪ weakBisim)" by auto
    moreover note ‹x ♯ Ψ›
    moreover have "weakBisim ⊆ ?X ∪ weakBisim" by auto
    moreover have "⋀Ψ P Q x. ⟦(Ψ, P, Q) ∈ weakBisim; x ♯ Ψ⟧ ⟹ (Ψ, ⦇νx⦈P, ⦇νx⦈Q) ∈ ?X ∪ weakBisim"
      by auto
    ultimately have "Ψ ⊳ ⦇νx⦈P ↝<(?X ∪ weakBisim)> ⦇νx⦈Q"
      by(rule weakResPres)
    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 weakBisimE)
   hence "([(x, y)] ∙ (Ψ ⊗ ([(x, y)] ∙ Ψ'))) ⊳ ([(x, y)] ∙ P) ≈ ([(x, y)] ∙ Q)"
     by(rule weakBisimClosed)
   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: weakBisimE)
  qed
qed

lemma weakBisimResChainPres:
  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: weakBisimResPres)

lemma weakBisimParPresAux:
  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"
      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 weakBisimClosed)
      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 weakBisimClosed)
    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 ∪ weakBisim; x ♯ Ψ⟧ ⟹ (Ψ, ⦇νx⦈P, ⦇νx⦈Q) ∈ ?X ∪ weakBisim"
  proof -
    fix Ψ P Q x
    assume "(Ψ, P, Q) ∈ ?X ∪ weakBisim" and "(x::name) ♯ Ψ"
    show "(Ψ, ⦇νx⦈P, ⦇νx⦈Q) ∈ ?X ∪ weakBisim"
    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 ∪ weakBisim› have "Ψ ⊳ P ≈ Q"
        by blast
      hence "Ψ ⊳ ⦇νx⦈P ≈ ⦇νx⦈Q" using ‹x ♯ Ψ›
        by(rule weakBisimResPres)
      thus ?thesis
        by simp
    qed
  qed

  {
    fix Ψ  :: 'b
      and P  :: "('a, 'b, 'c) psi"
      and Q  :: "('a, 'b, 'c) psi"
      and Ψ' :: 'b

    assume "Ψ ⊳ P ≈ Q"

    hence "Ψ ⊳ Q ≈ P" by(rule weakBisimE)
    then obtain P' P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P'"
                         and QimpP': "insertAssertion(extractFrame Q) Ψ ↪⇩F insertAssertion(extractFrame P') Ψ"
                         and P'Chain: "Ψ ⊗ Ψ' ⊳ P' ⟹⇧^⇩τ P''"   
                         and "Ψ ⊗ Ψ' ⊳ Q ≈ P''" using weakStatImp_def
      by(blast dest: weakBisimE)
    note PChain QimpP' P'Chain
    moreover from ‹Ψ ⊗ Ψ' ⊳ Q ≈ P''› have "Ψ ⊗ Ψ' ⊳ P'' ≈ Q" by(rule weakBisimE)
    ultimately have "∃P' P''. Ψ ⊳ P ⟹⇧^⇩τ P' ∧ insertAssertion(extractFrame Q) Ψ ↪⇩F insertAssertion(extractFrame P') Ψ ∧
                              Ψ ⊗ Ψ' ⊳ P' ⟹⇧^⇩τ P'' ∧ Ψ ⊗ Ψ' ⊳ P'' ≈ Q"
      by blast
  }
  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 weakBisimClosed)
        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 weakBisimClosed)
        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 ∪ weakBisim"
      by simp
  }
  note C1 = this

  have C2: "⋀Ψ P Q xvec. ⟦(Ψ, P, Q) ∈ ?X ∪ weakBisim; (xvec::name list) ♯* Ψ⟧ ⟹ (Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) ∈ ?X ∪ weakBisim"
  proof -
    fix Ψ P Q xvec
    assume "(Ψ, P, Q) ∈ ?X ∪ weakBisim"
    assume "(xvec::name list) ♯* Ψ"
    thus "(Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) ∈ ?X ∪ weakBisim"
    proof(induct xvec)
      case Nil
      thus ?case using ‹(Ψ, P, Q) ∈ ?X ∪ weakBisim› by simp
    next
      case(Cons x xvec)
      thus ?case by(simp only: resChain.simps) (rule_tac Res, auto)
    qed
  qed

  {
    fix Ψ :: 'b
    and P :: "('a, 'b, 'c) psi"
    and Q :: "('a, 'b, 'c) psi"
    and R :: "('a, 'b, 'c) psi"
    and A⇩R :: "name list"
    and Ψ⇩R :: 'b

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

    
    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 weakBisimClosed)
        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 weakBisimClosed)
        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
  }
  note Goal = this
  with assms have "(Ψ, P ∥ R, Q ∥ R) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cStatImp Ψ PR QR)
    {
      fix xvec :: "name list"
      fix P Q R 
      assume A: "∀A⇩R Ψ⇩R. extractFrame R = ⟨A⇩R, Ψ⇩R⟩ ∧ A⇩R ♯* Ψ ∧ A⇩R ♯* P ∧ A⇩R ♯* Q ⟶ Ψ ⊗ Ψ⇩R ⊳ P ≈ Q"
      {
        fix A⇩R Ψ⇩R
        assume "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" and "A⇩R ♯* Ψ" and "A⇩R ♯* P" and "A⇩R ♯* Q"
        with A have "Ψ ⊗ Ψ⇩R ⊳ P ⪅<weakBisim> Q" by(auto dest: weakBisimE)
      }
      moreover assume "xvec ♯* Ψ"
      moreover have "eqvt weakBisim" by auto
      moreover note C1 C2 statEqWeakBisim
      ultimately have "Ψ ⊳ ⦇ν*xvec⦈(P ∥ R) ⪅<(?X ∪ weakBisim)> ⦇ν*xvec⦈(Q ∥ R)" 
        by(rule weakStatImpParPres)
    }
    with ‹(Ψ, PR, QR) ∈ ?X› show ?case by auto
  next
    case(cSim Ψ 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 ♯* Ψ"
      by auto
    with ‹(Ψ, PR, QR) ∈ ?X› have "(Ψ, ⦇ν*xvec⦈(P ∥ R), ⦇ν*xvec⦈(Q ∥ R)) ∈ ?X" by simp
    hence "Ψ ⊳ ⦇ν*xvec⦈(P ∥ R) ↝<(?X ∪ weakBisim)> ⦇ν*xvec⦈(Q ∥ R)" using ‹xvec ♯* Ψ›
    proof(induct xvec)
      case Nil
      from ‹(Ψ, ⦇ν*[]⦈(P ∥ R), ⦇ν*[]⦈(Q ∥ R)) ∈ ?X› have PRQR: "(Ψ, P ∥ R, Q ∥ R) ∈ ?X" by simp
      from PRQR have "⋀A⇩R Ψ⇩R. ⟦extractFrame R = ⟨A⇩R, Ψ⇩R⟩; A⇩R ♯* Ψ;  A⇩R ♯* P;  A⇩R ♯* Q⟧ ⟹ (Ψ ⊗ Ψ⇩R, P, Q) ∈ weakBisim"
        by auto
      moreover note weakBisimEqvt
      moreover from ‹eqvt ?X› have "eqvt(?X ∪ weakBisim)" by auto
      moreover note weakBisimE(2) weakBisimE(4) weakBisimE(3) weakBisimE(1)
      moreover note C1 C2 
      ultimately have "Ψ ⊳ P ∥ R ↝<(?X ∪ weakBisim)> Q ∥ R" using statEqWeakBisim
        by(rule weakParPres)
      thus ?case by simp
    next
      case(Cons x xvec')
      from ‹(x#xvec') ♯* Ψ› have "x ♯ Ψ" and "xvec' ♯* Ψ" by simp+
      with ‹(Ψ, ⦇ν*(x#xvec')⦈P ∥ R, ⦇ν*(x#xvec')⦈Q ∥ R) ∈ ?X›
      have "(Ψ, ⦇ν*(xvec')⦈P ∥ R, ⦇ν*(xvec')⦈Q ∥ R) ∈ ?X"
        apply auto
        apply(subgoal_tac "∃y yvec. xvec=y#yvec")
        apply(clarify)
        apply simp
        apply(simp add: psi.inject alpha)
        apply(clarify)
        apply(erule disjE)
        apply(erule disjE)
        apply(clarify)
        apply blast
        apply(clarify)
        apply(clarify)
        apply(simp add: eqvts)
        apply(rule_tac x="[(x, y)] ∙ yvec" in exI)
        apply(rule_tac x="[(x, y)] ∙ P" in exI)
        apply(rule_tac x="[(x, y)] ∙ Q" in exI)
        apply(rule_tac x="[(x, y)] ∙ R" in exI)
        apply(clarsimp)
        apply(rule conjI)
        apply(subst pt_fresh_star_bij[OF pt_name_inst,OF at_name_inst, of "[(x, y)]", THEN sym])
        apply simp
        apply(clarify)
        apply(erule_tac x="[(x, y)] ∙ A⇩R" in allE)
        apply(erule_tac x="[(x, y)] ∙ Ψ⇩R" in allE)
        apply(drule mp)
        apply(rule conjI)
        apply(rule_tac pi="[(x, y)]" in pt_bij4[OF pt_name_inst, OF at_name_inst])
        apply(simp add: eqvts)
        apply(rule conjI)
        apply(subst pt_fresh_star_bij[OF pt_name_inst,OF at_name_inst, of "[(x, y)]", THEN sym])
        apply simp
        apply(rule conjI)
        apply(subst pt_fresh_star_bij[OF pt_name_inst,OF at_name_inst, of "[(x, y)]", THEN sym])
        apply simp
        apply(subst pt_fresh_star_bij[OF pt_name_inst,OF at_name_inst, of "[(x, y)]", THEN sym])
        apply simp
        apply(drule_tac p="[(x, y)]" in weakBisimClosed)
        apply(simp add: eqvts)
        by(case_tac xvec) auto
      
      with ‹⟦(Ψ, ⦇ν*xvec'⦈(P ∥ R), ⦇ν*xvec'⦈(Q ∥ R)) ∈ ?X; xvec' ♯* Ψ⟧ ⟹ Ψ ⊳ ⦇ν*xvec'⦈(P ∥ R) ↝<(?X ∪ weakBisim)> ⦇ν*xvec'⦈(Q ∥ R)› ‹xvec' ♯* Ψ›
      have "Ψ ⊳ ⦇ν*xvec'⦈(P ∥ R) ↝<(?X ∪ weakBisim)> ⦇ν*xvec'⦈(Q ∥ R)" by blast
      moreover note ‹eqvt ?X› 
      moreover from ‹eqvt ?X› have "eqvt(?X ∪ weakBisim)" by auto
      moreover note ‹x ♯ Ψ›
      moreover have "?X ∪ weakBisim ⊆ ?X ∪ weakBisim" by simp
      ultimately have "Ψ ⊳ ⦇νx⦈(⦇ν*xvec'⦈(P ∥ R)) ↝<(?X ∪ weakBisim)> ⦇νx⦈(⦇ν*xvec'⦈(Q ∥ R))" using Res
        by(rule_tac weakResPres)
      thus ?case
        by simp
    qed
    with PFrR QFrR show ?case
      by simp
  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 weakBisimE)
      moreover have "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ (p ∙ Ψ') ≃ (Ψ ⊗ (p ∙ Ψ')) ⊗ (p ∙ Ψ⇩R)"
        by(metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym)
      ultimately have "(Ψ ⊗ (p ∙ Ψ')) ⊗ (p ∙ Ψ⇩R) ⊳ P ≈ Q" 
        by(rule statEqWeakBisim)
      hence "(p ∙ ((Ψ ⊗ (p ∙ Ψ')) ⊗ (p ∙ Ψ⇩R))) ⊳ (p ∙ P) ≈ (p ∙ Q)"
        by(rule weakBisimClosed)
      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: weakBisimE)
  qed
qed

lemma weakBisimParPres:
  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 weakBisimE)
  ultimately show ?thesis by(rule_tac weakBisimParPresAux)
qed

end

end