Theory Bisimulation

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

context env begin

lemma monoCoinduct: "⋀x y xa xb xc P Q Ψ.
                      x ≤ y ⟹
                      (Ψ ⊳ Q ↝[{(xc, xb, xa). x xc xb xa}] P) ⟶
                     (Ψ ⊳ Q ↝[{(xb, xa, xc). y xb xa xc}] P)"
apply auto
apply(rule monotonic)
by(auto dest: le_funE)

coinductive_set bisim :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set" 
where
  step: "⟦(insertAssertion (extractFrame P)) Ψ ≃⇩F (insertAssertion (extractFrame Q) Ψ);
          Ψ ⊳ P ↝[bisim] Q;
          ∀Ψ'. (Ψ ⊗ Ψ',  P, Q) ∈ bisim; (Ψ, Q, P) ∈ bisim⟧ ⟹ (Ψ, P, Q) ∈ bisim"
monos monoCoinduct

abbreviation
  bisimJudge (‹_ ⊳ _ ∼ _› [70, 70, 70] 65) where "Ψ ⊳ P ∼ Q ≡ (Ψ, P, Q) ∈ bisim"
abbreviation
  bisimNilJudge (‹_ ∼ _› [70, 70] 65) where "P ∼ Q ≡ SBottom' ⊳ P ∼ Q"

lemma bisimCoinductAux[consumes 1]:
  fixes F :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "(Ψ, P, Q) ∈ X"
  and     "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ ∧
                                    (Ψ ⊳ P ↝[(X ∪ bisim)] Q) ∧
                                    (∀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ X ∨ (Ψ ⊗ Ψ', P, Q) ∈ bisim) ∧
                                    ((Ψ, Q, P) ∈ X ∨ (Ψ, Q, P) ∈ bisim)"

  shows "(Ψ, P, Q) ∈ bisim"
proof -
  have "X ∪ bisim = {(Ψ, P, Q). (Ψ, P, Q) ∈ X ∨ (Ψ, P, Q) ∈ bisim}" by auto
  with assms show ?thesis
    by coinduct simp
qed

lemma bisimCoinduct[consumes 1, case_names cStatEq cSim cExt cSym]:
  fixes F :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "(Ψ, P, Q) ∈ X"
  and     "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ insertAssertion (extractFrame R) Ψ' ≃⇩F insertAssertion (extractFrame S) Ψ'"
  and     "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ Ψ' ⊳ R ↝[(X ∪ bisim)] S"
  and     "⋀Ψ' R S Ψ''. (Ψ', R, S) ∈ X ⟹ (Ψ' ⊗ Ψ'', R, S) ∈ X ∨ (Ψ' ⊗ Ψ'', R, S) ∈ bisim"
  and     "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ (Ψ', S, R) ∈ X ∨ (Ψ', S, R) ∈ bisim"

  shows "(Ψ, P, Q) ∈ bisim"
proof -
  have "X ∪ bisim = {(Ψ, P, Q). (Ψ, P, Q) ∈ X ∨ (Ψ, P, Q) ∈ bisim}" by auto
  with assms show ?thesis
    by coinduct simp
qed

lemma bisimWeakCoinductAux[consumes 1]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "(Ψ, P, Q) ∈ X"
  and     "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ ∧
                                     Ψ ⊳ P ↝[X] Q ∧
                                    (∀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ X) ∧ (Ψ, Q, P) ∈ X" 

  shows "(Ψ, P, Q) ∈ bisim"
using assms
by(coinduct rule: bisimCoinductAux) (blast intro: monotonic)

lemma bisimWeakCoinduct[consumes 1, case_names cStatEq cSim cExt cSym]:
  fixes F :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "(Ψ, P, Q) ∈ X"
  and     "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ"
  and     "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ↝[X] Q"
  and     "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ X ⟹ (Ψ ⊗ Ψ', P, Q) ∈ X"
  and     "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ (Ψ, Q, P) ∈ X"

  shows "(Ψ, P, Q) ∈ bisim"
proof -
  have "X ∪ bisim = {(Ψ, P, Q). (Ψ, P, Q) ∈ X ∨ (Ψ, P, Q) ∈ bisim}" by auto
  with assms show ?thesis
  by(coinduct rule: bisimCoinduct) (blast intro: monotonic)+
qed

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

  assumes "(Ψ, P, Q) ∈ bisim"

  shows "insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ"
  and   "Ψ ⊳ P ↝[bisim] Q"
  and   "(Ψ ⊗ Ψ', P, Q) ∈ bisim"
  and   "(Ψ, Q, P) ∈ bisim"
using assms
by(auto simp add: intro: bisim.cases)

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

  assumes "insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ"
  and     "Ψ ⊳ P ↝[bisim] Q"
  and     "∀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ bisim"
  and     "(Ψ, Q, P) ∈ bisim"

  shows "(Ψ, P, Q) ∈ bisim"
using assms
by(auto intro: bisim.step)

lemma bisimReflexive:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"


  shows "Ψ ⊳ P ∼ P"
proof -
  let ?X = "{(Ψ, P, P) | Ψ P. True}"
  have "(Ψ, P, P) ∈ ?X" by simp
  thus ?thesis
    by(coinduct rule: bisimWeakCoinduct, auto intro: reflexive)
qed

lemma bisimClosed:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   p :: "name prm"
  
  assumes PBisimQ: "Ψ ⊳ P ∼ Q"

  shows "(p ∙ Ψ) ⊳  (p ∙ P) ∼ (p ∙ Q)"
proof -
  let ?X = "{(p ∙ Ψ, p ∙ P, p ∙ Q) | (p::name prm) Ψ  P Q. Ψ ⊳ P ∼ Q}"
  from PBisimQ have "(p ∙ Ψ, p ∙ P, p ∙ Q) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cStatEq Ψ P Q)
    have "⋀Ψ P Q (p::name prm). insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ ⟹
          insertAssertion (extractFrame(p ∙ P)) (p ∙ Ψ) ≃⇩F insertAssertion (extractFrame(p ∙ Q))  (p ∙ Ψ)"
      by(drule_tac p = p in FrameStatEqClosed) (simp add: eqvts)
      
    with ‹(Ψ, P, Q) ∈ ?X› show ?case by(blast dest: bisimE)
  next
    case(cSim Ψ P Q)
    {
      fix p :: "name prm"
      fix Ψ P Q
      have "eqvt ?X"
        apply(auto simp add: eqvt_def)
        apply(rule_tac x="pa@p" in exI)
        by(auto simp add: pt2[OF pt_name_inst])
      moreover assume "Ψ ⊳ P ↝[bisim] Q"
      hence "Ψ ⊳ P ↝[?X] Q"
        apply(rule_tac A=bisim in monotonic, auto)
        by(rule_tac x="[]::name prm" in exI) auto
      ultimately have "((p::name prm) ∙ Ψ) ⊳ (p ∙ P) ↝[?X] (p ∙ Q)"
        by(rule_tac simClosed)
    }
    with ‹(Ψ, P, Q) ∈ ?X› show ?case
      by(blast dest: bisimE)
  next
    case(cExt Ψ P Q Ψ')
    {
      fix p :: "name prm"
      fix Ψ P Q Ψ'
      assume "∀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ bisim"
      hence "((p ∙ Ψ) ⊗ Ψ', p ∙ P, p ∙ Q) ∈ ?X"  
        apply(auto, rule_tac x=p in exI)
        apply(rule_tac x="Ψ ⊗ (rev p ∙ Ψ')" in exI)
        by(auto simp add: eqvts)
    }
    with ‹(Ψ, P, Q) ∈ ?X› show ?case
      by(blast dest: bisimE)
  next
    case(cSym Ψ P Q)
    thus ?case
      by(blast dest: bisimE)
  qed
qed

lemma bisimEqvt[simp]:
  shows "eqvt bisim"
by(auto simp add: eqvt_def bisimClosed)

lemma statEqBisim:
  fixes Ψ  :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   Q  :: "('a, 'b, 'c) psi"
  and   Ψ' :: 'b
  
  assumes "Ψ ⊳ P ∼ Q"
  and     "Ψ ≃ Ψ'"

  shows "Ψ' ⊳ P ∼ Q"
proof -
  let ?X = "{(Ψ', P, Q) | Ψ P Q Ψ'. Ψ ⊳ P ∼ Q ∧ Ψ ≃ Ψ'}"
  from ‹Ψ ⊳ P ∼ Q› ‹Ψ ≃ Ψ'› have "(Ψ', P, Q) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ' P Q)
    from ‹(Ψ', P, Q) ∈ ?X› obtain Ψ where "Ψ ⊳ P ∼ Q" and "Ψ ≃ Ψ'"
      by auto
    from ‹Ψ ⊳ P ∼ Q› have PeqQ: "insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ"
      by(rule bisimE)

    obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "A⇩P ♯* Ψ'"
      by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto
    obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Ψ'"
      by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto

    from PeqQ FrP FrQ ‹A⇩P ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹Ψ ≃ Ψ'›
    have "⟨A⇩P, Ψ' ⊗ Ψ⇩P⟩ ≃⇩F ⟨A⇩Q, Ψ' ⊗ Ψ⇩Q⟩"
      by simp (metis frameIntComposition FrameStatEqTrans FrameStatEqSym)
    with FrP FrQ ‹A⇩P ♯* Ψ'› ‹A⇩Q ♯* Ψ'› show ?case by simp
  next
    case(cSim Ψ' P Q)
    from ‹(Ψ', P, Q) ∈ ?X› obtain Ψ where "Ψ ⊳ P ∼ Q" and "Ψ ≃ Ψ'"
      by auto
    from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊳ P ↝[bisim] Q" by(blast dest: bisimE)
    moreover have "eqvt ?X"
      by(auto simp add: eqvt_def) (metis bisimClosed AssertionStatEqClosed)
    hence "eqvt(?X ∪ bisim)" by auto
    moreover note ‹Ψ ≃ Ψ'›
    moreover have "⋀Ψ P Q Ψ'. ⟦Ψ ⊳ P ∼ Q; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?X ∪ bisim"
      by auto
    ultimately show ?case
      by(rule statEqSim)
  next
    case(cExt Ψ' P Q Ψ'')
    from ‹(Ψ', P, Q) ∈ ?X› obtain Ψ where "Ψ ⊳ P ∼ Q" and "Ψ ≃ Ψ'"
      by auto
    from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊗ Ψ'' ⊳ P ∼ Q" by(rule bisimE)
    moreover from ‹Ψ ≃ Ψ'› have "Ψ ⊗ Ψ'' ≃ Ψ' ⊗ Ψ''" by(rule Composition)
    ultimately show ?case by blast
  next
    case(cSym Ψ' P Q)
    from ‹(Ψ', P, Q) ∈ ?X› obtain Ψ where "Ψ ⊳ P ∼ Q" and "Ψ ≃ Ψ'"
      by auto
    from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊳ Q ∼ P" by(rule bisimE)
    thus ?case using ‹Ψ ≃ Ψ'› by auto
  qed
qed

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

  assumes PQ: "Ψ ⊳ P ∼ Q"
  and     QR: "Ψ ⊳ Q ∼ R"

  shows "Ψ ⊳ P ∼ R"
proof -
  let ?X = "{(Ψ, P, R) | Ψ P Q R. Ψ ⊳ P ∼ Q ∧ Ψ ⊳ Q ∼ R}" 
  from PQ QR have "(Ψ, P, R) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ P R)
    thus ?case by(blast dest: bisimE FrameStatEqTrans)
  next
    case(cSim Ψ P R)
    {
      fix Ψ P Q R
      assume "Ψ ⊳ P ↝[bisim] Q" and "Ψ ⊳ Q ↝[bisim] R"
      moreover have "eqvt ?X"
        by(force simp add: eqvt_def dest: bisimClosed)
      with bisimEqvt have "eqvt (?X ∪ bisim)" by blast
      moreover have "?X ⊆ ?X ∪ bisim" by auto
      ultimately have "Ψ ⊳ P ↝[(?X ∪ bisim)] R"
        by(force intro: transitive)
    }
    with ‹(Ψ, P, R) ∈ ?X› show ?case
      by(blast dest: bisimE)
  next
    case(cExt Ψ P R Ψ')
    thus ?case by(blast dest: bisimE)
  next
    case(cSym Ψ P R)
    thus ?case by(blast dest: bisimE)
  qed
qed

lemma weakTransitiveCoinduct[case_names cStatEq cSim cExt cSym, case_conclusion bisim step, consumes 2]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes p: "(Ψ, P, Q) ∈ X"
  and Eqvt: "eqvt X"
  and rStatEq: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ"
  and rSim: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ↝[({(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧
                                                                        (Ψ, P', Q') ∈ X ∧
                                                                        Ψ ⊳ Q' ∼ Q})] Q"
  and rExt: "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ X ⟹ (Ψ ⊗ Ψ', P, Q) ∈ X"
  and rSym: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ (Ψ, Q, P) ∈ X"

  shows "Ψ ⊳ P ∼ Q"
proof -
  let ?X = "{(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q}"
  from p have "(Ψ, P, Q) ∈ ?X"
    by(blast intro: bisimReflexive)
  thus ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cStatEq Ψ P Q)
    thus ?case
      by(blast dest: rStatEq bisimE FrameStatEqTrans)
  next
    case(cSim Ψ P Q)
    {
      fix Ψ P P' Q' Q
      assume "Ψ ⊳ P ↝[bisim] P'"
      moreover assume P'RelQ': "(Ψ, P', Q') ∈ X"
      hence "Ψ ⊳ P' ↝[?X] Q'" by(rule rSim)
      moreover from ‹eqvt X› P'RelQ' have "eqvt ?X"
        apply(auto simp add: eqvt_def)
        apply(drule_tac p=p in bisimClosed)
        apply(drule_tac p=p in bisimClosed)
        apply(rule_tac x="p ∙ P'a" in exI, simp)
        by(rule_tac x="p ∙ Q'a" in exI, auto)
      ultimately have "Ψ ⊳ P ↝[?X] Q'"
        by(force intro: transitive dest: bisimTransitive)
      moreover assume "Ψ ⊳ Q' ↝[bisim] Q"
      ultimately have "Ψ ⊳ P ↝[?X] Q" using ‹eqvt ?X›
        by(force intro: transitive dest: bisimTransitive)
    }
    with ‹(Ψ, P, Q) ∈ ?X› show ?case
      by(blast dest: bisimE)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(blast dest: bisimE intro: rExt)
  next
    case(cSym Ψ P Q)
    thus ?case by(blast dest: bisimE intro: rSym)
  qed
qed

lemma weakTransitiveCoinduct'[case_names cStatEq cSim cExt cSym, case_conclusion bisim step, consumes 2]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes p: "(Ψ, P, Q) ∈ X"
  and Eqvt: "eqvt X"
  and rStatEq: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ"
  and rSim: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ↝[({(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧
                                                                        (Ψ, P', Q') ∈ X ∧
                                                                        Ψ ⊳ Q' ∼ Q})] Q"
  and rExt: "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ X ⟹ (Ψ ⊗ Ψ', P, Q) ∈ X"
  and rSym: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹
                      (Ψ, Q, P) ∈ {(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q}"

  shows "Ψ ⊳ P ∼ Q"
proof -
  let ?X = "{(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q}"
  from p have "(Ψ, P, Q) ∈ ?X"
    by(blast intro: bisimReflexive)
  thus ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cStatEq Ψ P Q)
    thus ?case
      by(blast dest: rStatEq bisimE FrameStatEqTrans)
  next
    case(cSim Ψ P Q)
    {
      fix Ψ P P' Q' Q
      assume "Ψ ⊳ P ↝[bisim] P'"
      moreover assume P'RelQ': "(Ψ, P', Q') ∈ X"
      hence "Ψ ⊳ P' ↝[?X] Q'" by(rule rSim)
      moreover from ‹eqvt X› P'RelQ' have "eqvt ?X"
        apply(auto simp add: eqvt_def)
        apply(drule_tac p=p in bisimClosed)
        apply(drule_tac p=p in bisimClosed)
        apply(rule_tac x="p ∙ P'a" in exI, simp)
        by(rule_tac x="p ∙ Q'a" in exI, auto)
      ultimately have "Ψ ⊳ P ↝[?X] Q'"
        by(force intro: transitive dest: bisimTransitive)
      moreover assume "Ψ ⊳ Q' ↝[bisim] Q"
      ultimately have "Ψ ⊳ P ↝[?X] Q" using ‹eqvt ?X›
        by(force intro: transitive dest: bisimTransitive)
    }
    with ‹(Ψ, P, Q) ∈ ?X› show ?case
      by(blast dest: bisimE)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(blast dest: bisimE intro: rExt)
  next
    case(cSym Ψ P Q)
    thus ?case
      apply auto
      apply(drule rSym)
      apply auto
      by(metis bisimTransitive bisimE(4))
  qed
qed

lemma weakTransitiveCoinduct''[case_names cStatEq cSim cExt cSym, case_conclusion bisim step, consumes 2]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes p: "(Ψ, P, Q) ∈ X"
  and Eqvt: "eqvt X"
  and rStatEq: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ"
  and rSim: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ↝[({(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧
                                                                        (Ψ, P', Q') ∈ X ∧
                                                                        Ψ ⊳ Q' ∼ Q})] Q"
  and rExt: "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ {(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q} ⟹ 
                         (Ψ ⊗ Ψ', P, Q) ∈ {(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q}"
  and rSym: "⋀Ψ P Q. (Ψ, P, Q) ∈ {(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q} ⟹ 
                      (Ψ, Q, P) ∈ {(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q}"

  shows "Ψ ⊳ P ∼ Q"
proof -
  let ?X = "{(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q}"
  from p have "(Ψ, P, Q) ∈ ?X"
    by(blast intro: bisimReflexive)
  thus ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cStatEq Ψ P Q)
    thus ?case
      by(blast dest: rStatEq bisimE FrameStatEqTrans)
  next
    case(cSim Ψ P Q)
    {
      fix Ψ P P' Q' Q
      assume "Ψ ⊳ P ↝[bisim] P'"
      moreover assume P'RelQ': "(Ψ, P', Q') ∈ X"
      hence "Ψ ⊳ P' ↝[?X] Q'" by(rule rSim)
      moreover from ‹eqvt X› P'RelQ' have "eqvt ?X"
        apply(auto simp add: eqvt_def)
        apply(drule_tac p=p in bisimClosed)
        apply(drule_tac p=p in bisimClosed)
        apply(rule_tac x="p ∙ P'a" in exI, simp)
        by(rule_tac x="p ∙ Q'a" in exI, auto)
      ultimately have "Ψ ⊳ P ↝[?X] Q'"
        by(force intro: transitive dest: bisimTransitive)
      moreover assume "Ψ ⊳ Q' ↝[bisim] Q"
      ultimately have "Ψ ⊳ P ↝[?X] Q" using ‹eqvt ?X›
        by(force intro: transitive dest: bisimTransitive)
    }
    with ‹(Ψ, P, Q) ∈ ?X› show ?case
      by(blast dest: bisimE)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(rule_tac rExt)
  next
    case(cSym Ψ P Q)
    thus ?case by(rule_tac rSym)
  qed
qed

lemma transitiveCoinduct[case_names cStatEq cSim cExt cSym, case_conclusion bisim step, consumes 2]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes p: "(Ψ, P, Q) ∈ X"
  and Eqvt: "eqvt X"
  and rStatEq: "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ insertAssertion (extractFrame R) Ψ' ≃⇩F insertAssertion (extractFrame S) Ψ'"
  and rSim: "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ Ψ' ⊳ R ↝[({(Ψ', R, S) | Ψ' R R' S' S. Ψ' ⊳ R ∼ R' ∧
                                                                        ((Ψ', R', S') ∈ X ∨ Ψ' ⊳ R' ∼ S') ∧
                                                                        Ψ' ⊳ S' ∼ S})] S"
  and rExt: "⋀Ψ' R S Ψ''. (Ψ', R, S) ∈ X ⟹ (Ψ' ⊗ Ψ'', R, S) ∈ X ∨ Ψ' ⊗ Ψ'' ⊳ R ∼ S"
  and rSym: "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ (Ψ', S, R) ∈ X ∨ Ψ' ⊳ S ∼ R"


  shows "Ψ ⊳ P ∼ Q"
proof -
  from p have "(Ψ, P, Q) ∈ (X ∪ bisim)"
    by blast
  moreover from ‹eqvt X› bisimEqvt have "eqvt (X ∪ bisim)"
    by auto
  ultimately show ?thesis
  proof(coinduct rule: weakTransitiveCoinduct')
    case(cStatEq Ψ P Q)
    thus ?case
      by(blast intro: rStatEq dest: bisimE)
  next
    case(cSim Ψ P Q)
    thus ?case
      apply auto
      apply(blast intro: rSim)
      apply(drule bisimE(2))
      apply(rule_tac A=bisim in monotonic, simp)
      by(force intro: bisimReflexive)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case
      by(blast dest: bisimE rExt)
  next
    case(cSym Ψ P Q)
    thus ?case by(blast dest: bisimE rSym intro: bisimReflexive)
  qed
qed

lemma transitiveCoinduct'[case_names cStatEq cSim cExt cSym, case_conclusion bisim step, consumes 2]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   X :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes p: "(Ψ, P, Q) ∈ X"
  and Eqvt: "eqvt X"
  and rStatEq: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ"
  and rSim: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ↝[({(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧
                                                                        (Ψ, P', Q') ∈ (X ∪ bisim) ∧
                                                                        Ψ ⊳ Q' ∼ Q})] Q"
  and rExt: "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ X ⟹ (Ψ ⊗ Ψ', P, Q) ∈ X ∨ Ψ ⊗ Ψ' ⊳ P ∼ Q"
  and rSym: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹
                      (Ψ, Q, P) ∈ {(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ ((Ψ, P', Q') ∈ (X ∪ bisim)) ∧ Ψ ⊳ Q' ∼ Q}"

  shows "Ψ ⊳ P ∼ Q"
proof -
  from p have "(Ψ, P, Q) ∈ (X ∪ bisim)"
    by blast
  moreover from ‹eqvt X› bisimEqvt have "eqvt (X ∪ bisim)"
    by auto
  ultimately show ?thesis
  proof(coinduct rule: weakTransitiveCoinduct')
    case(cStatEq Ψ P Q)
    thus ?case
      by(blast intro: rStatEq dest: bisimE)
  next
    case(cSim Ψ P Q)
    thus ?case
      apply -
      apply(case_tac "(Ψ, P, Q) ∈ X" for X)
      apply(rule_tac rSim)
      apply simp
      apply(clarify)
      apply(drule bisimE(2))
      apply(rule_tac A=bisim in monotonic, simp)
      by(force intro: bisimReflexive)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case
      by(blast dest: bisimE rExt)
  next
    case(cSym Ψ P Q)
    thus ?case
      apply auto
      apply(drule rSym)
      apply auto
      apply(rule_tac x=Q in exI)
      apply(auto intro: bisimReflexive)
      apply(rule_tac x=P in exI)
      by(auto intro: bisimReflexive dest: bisimE(4))
  qed
qed

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

  assumes "Ψ ⊳ P ∼ Q"
  
  shows "Ψ ⊳ Q ∼ P"
using assms
by(rule bisimE)

lemma eqvtTrans[intro]:
  assumes "eqvt X"

  shows "eqvt {(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ ((Ψ, P', Q') ∈ X ∨ Ψ ⊳ P' ∼ Q') ∧ Ψ ⊳ Q' ∼ Q}"
using assms
apply(auto simp add: eqvt_def eqvts)
apply(erule_tac x="(a, P', Q')" in ballE, auto)
by(blast dest: bisimClosed)+

lemma eqvtWeakTrans[intro]:
  assumes "eqvt X"

  shows "eqvt {(Ψ, P, Q) | Ψ P P' Q' Q. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q}"
using assms
apply(auto simp add: eqvt_def eqvts)
apply(erule_tac x="(a, P', Q')" in ballE, auto)
by(blast dest: bisimClosed)+

end

end