Theory Bisimulation

theory Bisimulation
  imports Simulation
begin

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

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(rule impI)
  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
  then show ?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
  then show ?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 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(clarsimp simp add: eqvt_def)
        by (metis (no_types, opaque_lifting) pt_name2)
      moreover assume "Ψ ⊳ P ↝[bisim] Q"
      then have "Ψ ⊳ P ↝[?X] Q"
        apply(rule monotonic[where A=bisim], auto)
        by(rule exI[where x="[]::name prm"]) auto
      ultimately have "((p::name prm) ∙ Ψ) ⊳ (p ∙ P) ↝[?X] (p ∙ Q)"
        by(rule 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"
      then have "((p ∙ Ψ) ⊗ Ψ', p ∙ P, p ∙ Q) ∈ ?X"
        apply(clarsimp)
        apply(rule exI[where x=p])
        apply(rule exI[where x="Ψ ⊗ (rev p ∙ Ψ')"])
        by(auto simp add: eqvts)
    }
    with ‹(Ψ, P, Q) ∈ ?X› show ?case
      by(blast dest: bisimE)
  next
    case(cSym Ψ P Q)
    then show ?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
  then show ?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 freshFrame[where C="(Ψ, Ψ')"]) auto
    obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Ψ'"
      by(rule freshFrame[where C="(Ψ, Ψ')"]) 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)
    then have "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)
    then show ?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
  then show ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ P R)
    then show ?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 Ψ')
    then show ?case by(blast dest: bisimE)
  next
    case(cSym Ψ P R)
    then show ?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)
  then show ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cStatEq Ψ P Q)
    then show ?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"
      then have "Ψ ⊳ P' ↝[?X] Q'" by(rule rSim)
      moreover from ‹eqvt X› P'RelQ' have "eqvt ?X"
        apply(clarsimp simp add: eqvt_def)
        apply(drule bisimClosed)
        apply(drule bisimClosed)
        apply(rule exI)
        apply(rule conjI)
         apply assumption
        apply(rule exI)
        by 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 Ψ')
    then show ?case by(blast dest: bisimE intro: rExt)
  next
    case(cSym Ψ P Q)
    then show ?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)
  then show ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cStatEq Ψ P Q)
    then show ?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"
      then have "Ψ ⊳ P' ↝[?X] Q'" by(rule rSim)
      moreover from ‹eqvt X› P'RelQ' have "eqvt ?X"
        apply(clarsimp simp add: eqvt_def)
        apply(drule bisimClosed)
        apply(drule bisimClosed)
        apply(rule exI)
        apply(rule conjI)
         apply assumption
        apply(rule exI)
        by 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 Ψ')
    then show ?case by(blast dest: bisimE intro: rExt)
  next
    case(cSym Ψ P Q)
    then show ?case
      apply clarsimp
      apply(drule rSym)
      apply clarsimp
      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)
  then show ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cStatEq Ψ P Q)
    then show ?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"
      then have "Ψ ⊳ P' ↝[?X] Q'" by(rule rSim)
      moreover from ‹eqvt X› P'RelQ' have "eqvt ?X"
        apply(clarsimp simp add: eqvt_def)
        apply(drule bisimClosed)
        apply(drule bisimClosed)
        apply(rule exI)
        apply(rule conjI)
         apply assumption
        apply(rule exI)
        by 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 Ψ')
    then show ?case by(rule rExt)
  next
    case(cSym Ψ P Q)
    then show ?case by(rule 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)
    then show ?case
      by(blast intro: rStatEq dest: bisimE)
  next
    case(cSim Ψ P Q)
    then show ?case
      apply clarsimp
      apply (erule disjE)
       apply(blast intro: rSim)
      apply(drule bisimE(2))
      apply(rule monotonic, simp)
      by(force intro: bisimReflexive)
  next
    case(cExt Ψ P Q Ψ')
    then show ?case
      by(blast dest: bisimE rExt)
  next
    case(cSym Ψ P Q)
    then show ?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)
    then show ?case
      by(blast intro: rStatEq dest: bisimE)
  next
    case(cSim Ψ P Q)
    then show ?case
      apply -
      apply(cases "(Ψ, P, Q) ∈ X")
       apply(rule rSim)
       apply simp
      apply(clarify)
      apply(drule bisimE(2))
      apply(rule monotonic, simp)
      by(force intro: bisimReflexive)
  next
    case(cExt Ψ P Q Ψ')
    then show ?case
      by(blast dest: bisimE rExt)
  next
    case(cSym Ψ P Q)
    then show ?case
      apply clarsimp
      apply (erule disjE)
       apply(drule rSym)
       apply clarsimp
      apply(rule exI[where x=Q])
      apply(simp add: bisimReflexive)
      apply(rule 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(clarsimp simp add: eqvt_def)
  apply(erule disjE)
   using ballE bisimClosed apply fastforce
  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(clarsimp simp add: eqvt_def)
  using ballE bisimClosed by fastforce

inductive_set
  rel_trancl :: "('b × ('a,'b,'c) psi × ('a,'b,'c) psi) set ⇒ ('b × ('a,'b,'c) psi × ('a,'b,'c) psi) set"  (‹(_⇧⋆)› [1000] 999)
  for r :: "('b × ('a,'b,'c) psi × ('a,'b,'c) psi) set"
  where
    r_into_rel_trancl [intro, Pure.intro]: "(Ψ, P,Q) : r ==> (Ψ,P,Q) : r⇧⋆"
  | rel_trancl_into_rel_trancl [Pure.intro]: "(Ψ,P,Q) : r⇧⋆ ==> (Ψ,Q,R) : r ==> (Ψ,P,R) : r⇧⋆"

lemma rel_trancl_transitive:
  assumes "(Ψ,P,Q) ∈ Rel⇧⋆"
    and   "(Ψ,Q,R) ∈ Rel⇧⋆"
  shows   "(Ψ,P,R) ∈ Rel⇧⋆"
  using ‹(Ψ,Q,R) ∈ Rel⇧⋆› ‹(Ψ,P,Q) ∈ Rel⇧⋆›
  by(induct rule: rel_trancl.induct) (auto intro: rel_trancl_into_rel_trancl)

lemma rel_trancl_eqvt:
  assumes "eqvt X"
  shows   "eqvt(X⇧⋆)"
proof -
  {
    fix  p::"name prm"
      and Ψ P Q
    assume "(Ψ,P,Q) ∈ X⇧⋆"
    then have   "(p∙(Ψ,P,Q)) ∈ X⇧⋆"
    proof(induct rule: rel_trancl.induct)
      case(r_into_rel_trancl Ψ P Q)
      with ‹eqvt X› have "(p∙(Ψ, P, Q)) ∈ X"
        unfolding eqvt_def by auto
      then show ?case by auto
    next
      case(rel_trancl_into_rel_trancl Ψ P Q R)
      from ‹(Ψ, Q, R) ∈ X› ‹eqvt X› have "(p∙(Ψ, Q, R)) ∈ X"
        unfolding eqvt_def by auto
      then have "(p∙(Ψ, Q, R)) ∈ X⇧⋆"
        by auto
      with ‹p ∙ (Ψ, P, Q) ∈ X⇧⋆› show ?case by(auto dest: rel_trancl_transitive)
    qed
  }
  then show ?thesis unfolding eqvt_def
    by auto
qed

lemma bisimStarWeakCoinduct[consumes 2, 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   "eqvt X"
  and   rStatEq: "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ insertAssertion (extractFrame R) Ψ' ≃⇩F insertAssertion (extractFrame S) Ψ'"
  and   rSim: "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ Ψ' ⊳ R ↝[X⇧⋆] S"
  and   rExt: "⋀Ψ' R S Ψ''. (Ψ', R, S) ∈ X ⟹ (Ψ' ⊗ Ψ'', R, S) ∈ X"
  and   rSym: "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ (Ψ', S, R) ∈ X"

shows "(Ψ, P, Q) ∈ bisim"
proof -
  have "eqvt(X⇧⋆)" using ‹eqvt X›
    by(rule rel_trancl_eqvt)
  from ‹(Ψ, P, Q) ∈ X›
  have "(Ψ, P, Q) ∈ X⇧⋆"
    by force
  then show ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cSim Ψ' R S)
    then show ?case
    proof(induct rule: rel_trancl.induct)
      case(r_into_rel_trancl Ψ P Q)
      then show ?case
        by(rule rSim)
    next
      case(rel_trancl_into_rel_trancl Ψ P Q R)
      note ‹Ψ ⊳ P ↝[X⇧⋆] Q›
      moreover from ‹(Ψ, Q, R) ∈ X› have "Ψ ⊳ Q ↝[X⇧⋆] R"
        by(rule rSim)
      moreover note ‹eqvt(X⇧⋆)›
      moreover have "{(Ψ, P, R) |Ψ P R. ∃Q. (Ψ, P, Q) ∈ X⇧⋆ ∧ (Ψ, Q, R) ∈ X⇧⋆} ⊆ X⇧⋆"
        by(blast intro: rel_trancl_transitive)
      ultimately show ?case
        using transitive by meson
    qed
  next
    case (cStatEq Ψ P Q)
    then show ?case
    proof(induct rule: rel_trancl.induct)
      case(r_into_rel_trancl Ψ P Q)
      then show ?case
        by(rule rStatEq)
    next
      case(rel_trancl_into_rel_trancl Ψ P Q R)
      from ‹(Ψ, Q, R) ∈ X› have "insertAssertion (extractFrame Q) Ψ ≃⇩F insertAssertion (extractFrame R) Ψ"
        by(rule rStatEq)
      with ‹insertAssertion (extractFrame P) Ψ ≃⇩F insertAssertion (extractFrame Q) Ψ›
      show ?case
        by(rule FrameStatEqTrans)
    qed
  next
    case(cExt Ψ P Q Ψ')
    then show ?case
    proof(induct rule: rel_trancl.induct)
      case(r_into_rel_trancl Ψ P Q)
      then have "(Ψ ⊗ Ψ', P, Q) ∈ X" by(rule rExt)
      then show ?case
        by force
    next
      case(rel_trancl_into_rel_trancl Ψ P Q R)
      from ‹(Ψ, Q, R) ∈ X› have "(Ψ ⊗ Ψ', Q, R) ∈ X" by(rule rExt)
      then have "(Ψ ⊗ Ψ', Q, R) ∈ X⇧⋆" by force
      with ‹(Ψ ⊗ Ψ', P, Q) ∈ X⇧⋆›
      show ?case
        by(rule rel_trancl_transitive)
    qed
  next
    case(cSym Ψ P Q)
    then show ?case
    proof(induct rule: rel_trancl.induct)
      case(r_into_rel_trancl Ψ P Q)
      then have "(Ψ, Q, P) ∈ X" by(rule rSym)
      then show ?case
        by force
    next
      case(rel_trancl_into_rel_trancl Ψ P Q R)
      from ‹(Ψ, Q, R) ∈ X› have "(Ψ, R, Q) ∈ X" by(rule rSym)
      then have "(Ψ, R, Q) ∈ X⇧⋆" by force
      then show ?case using ‹(Ψ, Q, P) ∈ X⇧⋆›
        by(rule rel_trancl_transitive)
    qed
  qed
qed

lemma weakTransitiveStarCoinduct[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)
  moreover from ‹eqvt X› have "eqvt ?X" by auto
  ultimately show ?thesis
  proof(coinduct rule: bisimStarWeakCoinduct)
    case(cStatEq Ψ P Q)
    then show ?case
      by(blast dest: rStatEq bisimE FrameStatEqTrans)
  next
    case(cSim Ψ P Q)
    then obtain P' Q' where "Ψ ⊳ P ∼ P'" and "(Ψ, P', Q') ∈ X" and "Ψ ⊳ Q' ∼ Q"
      by blast
    then have "Ψ ⊳ P ↝[bisim] P'" and "Ψ ⊳ Q' ↝[bisim] Q"
      by(auto dest: bisimE)
    {
      fix Ψ P Q
        and Q'::"('a,'b,'c) psi"
      assume "Ψ ⊳ P ∼ Q"
        and  "(Ψ,Q,Q') ∈ ?X⇧⋆"
      note ‹(Ψ,Q,Q') ∈ ?X⇧⋆› ‹Ψ ⊳ P ∼ Q›
      then have "(Ψ,P,Q') ∈ ?X⇧⋆"
      proof(induct rule: rel_trancl.inducts)
        case(r_into_rel_trancl Ψ Q Q') then show ?case
          by(blast dest: bisimTransitive)
      next
        case(rel_trancl_into_rel_trancl Ψ P' Q Q')
        then show ?case
          by(blast dest: rel_trancl_transitive)
      qed
    }
    note tonic = this
    {
      fix Ψ P Q
        and Q'::"('a,'b,'c) psi"
      assume "(Ψ,P,Q) ∈ ?X⇧⋆"
        and  "Ψ ⊳ Q ∼ Q'"
      then have "(Ψ,P,Q') ∈ ?X⇧⋆"
      proof(induct arbitrary: Q' rule: rel_trancl.inducts)
        case(r_into_rel_trancl Ψ P Q) then show ?case
          by(blast dest: bisimTransitive)
      next
        case(rel_trancl_into_rel_trancl Ψ P P' Q)
        from ‹(Ψ, P', Q) ∈ ?X› ‹Ψ ⊳ Q ∼ Q'› have "(Ψ, P', Q') ∈ ?X"
          by(blast dest: bisimTransitive)
        then have "(Ψ, P', Q') ∈ ?X⇧⋆"
          by blast
        with ‹(Ψ, P, P') ∈ ?X⇧⋆›
        show ?case
          by(rule rel_trancl_transitive)
      qed
    }
    note tonic2 = this
    from ‹(Ψ, P', Q') ∈ X› have "Ψ ⊳ P' ↝[?X⇧⋆] Q'"
      by(rule rSim)
    with ‹Ψ ⊳ P ↝[bisim] P'› have "Ψ ⊳ P ↝[?X⇧⋆] Q'"
      apply -
      apply(rule transitive)
         apply assumption
        apply assumption
       apply(rule rel_trancl_eqvt)
       apply(rule ‹eqvt ?X›)
      by(blast intro: tonic)
    with ‹Ψ ⊳ Q' ↝[bisim] Q› show ?case
      apply -
      apply(rule transitive)
         apply assumption
        apply assumption
       apply(rule rel_trancl_eqvt)
       apply(rule ‹eqvt ?X›)
      by(blast intro: tonic2)
  next
    case(cExt Ψ P Q Ψ')
    then show ?case by(blast dest: bisimE intro: rExt)
  next
    case(cSym Ψ P Q)
    then show ?case by(blast dest: bisimE intro: rSym)
  qed
qed

lemma weakTransitiveStarCoinduct'[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)
  moreover from ‹eqvt X› have "eqvt ?X" by auto
  ultimately show ?thesis
  proof(coinduct rule: bisimStarWeakCoinduct)
    case(cStatEq Ψ P Q)
    then show ?case
      by(blast dest: rStatEq bisimE FrameStatEqTrans)
  next
    case(cSim Ψ P Q)
    then obtain P' Q' where "Ψ ⊳ P ∼ P'" and "(Ψ, P', Q') ∈ X" and "Ψ ⊳ Q' ∼ Q"
      by blast
    then have "Ψ ⊳ P ↝[bisim] P'" and "Ψ ⊳ Q' ↝[bisim] Q"
      by(auto dest: bisimE)
    {
      fix Ψ P Q
        and Q'::"('a,'b,'c) psi"
      assume "Ψ ⊳ P ∼ Q"
        and  "(Ψ,Q,Q') ∈ ?X⇧⋆"
      note ‹(Ψ,Q,Q') ∈ ?X⇧⋆› ‹Ψ ⊳ P ∼ Q›
      then have "(Ψ,P,Q') ∈ ?X⇧⋆"
      proof(induct rule: rel_trancl.inducts)
        case(r_into_rel_trancl Ψ Q Q') then show ?case
          by(blast dest: bisimTransitive)
      next
        case(rel_trancl_into_rel_trancl Ψ P' Q Q')
        then show ?case
          by(blast dest: rel_trancl_transitive)
      qed
    }
    note tonic = this
    {
      fix Ψ P Q
        and Q'::"('a,'b,'c) psi"
      assume "(Ψ,P,Q) ∈ ?X⇧⋆"
        and  "Ψ ⊳ Q ∼ Q'"
      then have "(Ψ,P,Q') ∈ ?X⇧⋆"
      proof(induct arbitrary: Q' rule: rel_trancl.inducts)
        case(r_into_rel_trancl Ψ P Q) then show ?case
          by(blast dest: bisimTransitive)
      next
        case(rel_trancl_into_rel_trancl Ψ P P' Q)
        from ‹(Ψ, P', Q) ∈ ?X› ‹Ψ ⊳ Q ∼ Q'› have "(Ψ, P', Q') ∈ ?X"
          by(blast dest: bisimTransitive)
        then have "(Ψ, P', Q') ∈ ?X⇧⋆"
          by blast
        with ‹(Ψ, P, P') ∈ ?X⇧⋆›
        show ?case
          by(rule rel_trancl_transitive)
      qed
    }
    note tonic2 = this
    from ‹(Ψ, P', Q') ∈ X› have "Ψ ⊳ P' ↝[?X⇧⋆] Q'"
      by(rule rSim)
    with ‹Ψ ⊳ P ↝[bisim] P'› have "Ψ ⊳ P ↝[?X⇧⋆] Q'"
      apply -
      apply(rule transitive)
         apply assumption
        apply assumption
       apply(rule rel_trancl_eqvt)
       apply(rule ‹eqvt ?X›)
      by(blast intro: tonic)
    with ‹Ψ ⊳ Q' ↝[bisim] Q› show ?case
      apply -
      apply(rule transitive)
         apply assumption
        apply assumption
       apply(rule rel_trancl_eqvt)
       apply(rule ‹eqvt ?X›)
      by(blast intro: tonic2)
  next
    case(cExt Ψ P Q Ψ')
    then show ?case by(blast dest: bisimE intro: rExt)
  next
    case(cSym Ψ P Q)
    then show ?case
      apply clarsimp
      apply(drule rSym)
      apply clarsimp
      by(metis bisimTransitive bisimE(4))
  qed
qed

lemma transitiveStarCoinduct[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: weakTransitiveStarCoinduct')
    case(cStatEq Ψ P Q)
    then show ?case
      by(blast intro: rStatEq dest: bisimE)
  next
    case(cSim Ψ P Q)
    then show ?case
      apply clarsimp
      apply (erule disjE)
       apply(blast intro: rSim)
      apply(drule bisimE(2))
      apply(rule monotonic, simp)
      by(force intro: bisimReflexive)
  next
    case(cExt Ψ P Q Ψ')
    then show ?case
      by(blast dest: bisimE rExt)
  next
    case(cSym Ψ P Q)
    then show ?case by(blast dest: bisimE rSym intro: bisimReflexive)
  qed
qed

end

end