Theory Weak_Bisimulation

(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Bisimulation
  imports Weak_Simulation Weak_Stat_Imp Bisim_Struct_Cong
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 weakSimMonotonic)
by(auto dest: le_funE)

lemma monoCoinduct2: "⋀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 weakStatImpMonotonic)
by(auto dest: le_funE)

coinductive_set weakBisim :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set" 
where
  step: "⟦Ψ ⊳ P ⪅<weakBisim> Q; Ψ ⊳ P ↝<weakBisim> Q;
          ∀Ψ'. (Ψ ⊗ Ψ',  P, Q) ∈ weakBisim; (Ψ, Q, P) ∈ weakBisim⟧ ⟹ (Ψ, P, Q) ∈ weakBisim"
monos monoCoinduct monoCoinduct2

abbreviation
  weakBisimJudge (‹_ ⊳ _ ≈ _› [70, 70, 70] 65) where "Ψ ⊳ P ≈ Q ≡ (Ψ, P, Q) ∈ weakBisim"
abbreviation
  weakBisimNilJudge (‹_ ≈ _› [70, 70] 65) where "P ≈ Q ≡ 𝟭 ⊳ P ≈ Q"

lemma weakBisimCoinductAux[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 ⟹ (Ψ ⊳ P ⪅<(X ∪ weakBisim)> Q) ∧
                                      (Ψ ⊳ P ↝<(X ∪ weakBisim)> Q) ∧
                                      (∀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ X ∨ (Ψ ⊗ Ψ', P, Q) ∈ weakBisim) ∧
                                      ((Ψ, Q, P) ∈ X ∨ (Ψ, Q, P) ∈ weakBisim)"

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

lemma weakBisimCoinduct[consumes 1, case_names cStatImp 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 ⟹ Ψ' ⊳ R ⪅<(X ∪ weakBisim)> S"
  and     "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ Ψ' ⊳ R ↝<(X ∪ weakBisim)> S"
  and     "⋀Ψ' R S Ψ''. (Ψ', R, S) ∈ X ⟹ (Ψ' ⊗ Ψ'', R, S) ∈ X ∨ Ψ' ⊗ Ψ'' ⊳ R ≈ S"
  and     "⋀Ψ' R S. (Ψ', R, S) ∈ X ⟹ (Ψ', S, R) ∈ X ∨ Ψ' ⊳ S ≈ R"

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

lemma weakBisimWeakCoinductAux[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 ⟹ Ψ ⊳ P ⪅<X> Q ∧ Ψ ⊳ P ↝<X> Q ∧
                                      (∀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ X) ∧ (Ψ, Q, P) ∈ X" 

  shows "Ψ ⊳ P ≈ Q"
using assms
by(coinduct rule: weakBisimCoinductAux) (blast intro: weakSimMonotonic weakStatImpMonotonic)

lemma weakBisimWeakCoinduct[consumes 1, case_names cStatImp 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 ⟹ Ψ ⊳ P ⪅<X> 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) ∈ weakBisim"
proof -
  have "X ∪ weakBisim = {(Ψ, P, Q). (Ψ, P, Q) ∈ X ∨ (Ψ, P, Q) ∈ weakBisim}" by auto
  with assms show ?thesis
    by(coinduct rule: weakBisimWeakCoinductAux) blast
qed

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

  assumes "Ψ ⊳ P ≈ Q"

  shows "Ψ ⊳ P ⪅<weakBisim> Q"
  and   "Ψ ⊳ P ↝<weakBisim> Q"
  and   "Ψ ⊗ Ψ' ⊳  P ≈ Q"
  and   "Ψ ⊳ Q ≈ P"
using assms
by(auto intro: weakBisim.cases simp add: rtrancl_def)

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

  assumes "Ψ ⊳ P ⪅<weakBisim> Q"
  and     "Ψ ⊳ P ↝<weakBisim> Q"
  and     "∀Ψ'. Ψ ⊗ Ψ' ⊳ P ≈ Q"
  and     "Ψ ⊳ Q ≈ P"

  shows "Ψ ⊳ P ≈ Q"
using assms
by(rule_tac weakBisim.step) (auto simp add: rtrancl_def)

lemma weakBisimReflexive:
  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: weakBisimWeakCoinduct, auto intro: weakSimReflexive weakStatImpReflexive)
qed

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

  shows "(p ∙ Ψ) ⊳  (p ∙ P) ≈ (p ∙ Q)"
proof -
  let ?X = "{(p ∙ Ψ, p ∙ P, p ∙ Q) | (p::name prm) Ψ  P Q. Ψ ⊳ 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])
  from ‹Ψ ⊳ P ≈ Q› have "(p ∙ Ψ, p ∙ P, p ∙ Q) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: weakBisimWeakCoinduct)
    case(cStatImp Ψ P Q)
    {
      fix Ψ P Q p
      assume "Ψ ⊳ P ≈ (Q::('a, 'b, 'c) psi)"
      hence "Ψ ⊳ P ⪅<weakBisim> Q" by(rule weakBisimE)
      hence "Ψ ⊳ P ⪅<?X> Q"
        apply(rule_tac A=weakBisim in weakStatImpMonotonic, auto)
        by(rule_tac x="[]::name prm" in exI) auto
      with ‹eqvt ?X› have "((p::name prm) ∙ Ψ) ⊳ (p ∙ P) ⪅<?X> (p ∙ Q)"
        by(rule weakStatImpClosed)
    }
    with ‹(Ψ, P, Q) ∈ ?X› show ?case by blast
  next
    case(cSim Ψ P Q)
    {
      fix p :: "name prm"
      fix Ψ P Q
      assume "Ψ ⊳ P ↝<weakBisim> Q"
      hence "Ψ ⊳ P ↝<?X> Q"
        apply(rule_tac A=weakBisim in weakSimMonotonic, auto)
        by(rule_tac x="[]::name prm" in exI) auto
      with ‹eqvt ?X› have "((p::name prm) ∙ Ψ) ⊳ (p ∙ P) ↝<?X> (p ∙ Q)"
        by(rule_tac weakSimClosed)
    }
    with ‹(Ψ, P, Q) ∈ ?X› show ?case
      by(blast dest: weakBisimE)
  next
    case(cExt Ψ P Q Ψ')
    {
      fix p :: "name prm"
      fix Ψ P Q Ψ'
      assume "∀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ weakBisim"
      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: weakBisimE)
  next
    case(cSym Ψ P Q)
    thus ?case
      by(blast dest: weakBisimE)
  qed
qed

lemma weakBisimEqvt[simp]:
  shows "eqvt weakBisim"
by(auto simp add: eqvt_def weakBisimClosed)

lemma statEqWeakBisim:
  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: weakBisimCoinduct)
    case(cStatImp Ψ' P Q)
    from ‹(Ψ', P, Q) ∈ ?X› obtain Ψ where "Ψ ⊳ P ≈ Q" and "Ψ ≃ Ψ'"
      by auto
    from ‹Ψ ⊳ P ≈ Q› have "Ψ ⊳ P ⪅<weakBisim> Q" by(rule weakBisimE)
    moreover note ‹Ψ ≃ Ψ'›
    moreover have "⋀Ψ P Q Ψ'. ⟦Ψ ⊳ P ≈ Q; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?X ∪ weakBisim"
      by auto
    ultimately show ?case by(rule weakStatImpStatEq)
  next
    case(cSim Ψ' P Q)
    from ‹(Ψ', P, Q) ∈ ?X› obtain Ψ where "Ψ ⊳ P ≈ Q" and "Ψ ≃ Ψ'"
      by auto
    from ‹Ψ ⊳ P ≈ Q› have "Ψ ⊳ P ↝<weakBisim> Q" by(blast dest: weakBisimE)
    moreover have "eqvt ?X"
      by(auto simp add: eqvt_def) (metis weakBisimClosed AssertionStatEqClosed)
    hence "eqvt(?X ∪ weakBisim)" by auto
    moreover note ‹Ψ ≃ Ψ'›
    moreover have "⋀Ψ P Q Ψ'. ⟦Ψ ⊳ P ≈ Q; Ψ ≃ Ψ'⟧ ⟹ (Ψ', P, Q) ∈ ?X ∪ weakBisim"
      by auto
    ultimately show ?case by(rule weakSimStatEq)
  next
    case(cExt Ψ' P Q Ψ'')
    from ‹(Ψ', P, Q) ∈ ?X› obtain Ψ where "Ψ ⊳ P ≈ Q" and "Ψ ≃ Ψ'"
      by auto
    from ‹Ψ ⊳ P ≈ Q› have "Ψ ⊗ Ψ'' ⊳ P ≈ Q" by(rule weakBisimE)
    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 weakBisimE)
    thus ?case using ‹Ψ ≃ Ψ'› by auto
  qed
qed

lemma weakBisimTransitive:
  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 R. ∃Q. Ψ ⊳ P ≈ Q ∧ Ψ ⊳ Q ≈ R}" 
  from PQ QR have "(Ψ, P, R) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cStatImp Ψ P R)
    from ‹(Ψ, P, R) ∈ ?X› obtain Q where "Ψ ⊳ P ≈ Q" and  "Ψ ⊳ Q ≈ R" by blast
    from ‹Ψ ⊳ P ≈ Q› have "Ψ ⊳ P ⪅<weakBisim> Q" by(rule weakBisimE)
    moreover note ‹Ψ ⊳ Q ≈ R›
    moreover have "?X ⊆ ?X ∪ weakBisim" by auto
    moreover note weakBisimE(1)
    moreover from weakBisimE(2) have "⋀Ψ P Q P'. ⟦Ψ ⊳ P ≈ Q; Ψ ⊳ P ⟹⇧^⇩τ P'⟧ ⟹ ∃Q'. Ψ ⊳ Q ⟹⇧^⇩τ Q' ∧ Ψ ⊳ P' ≈ Q'"
      by(metis weakBisimE(4) weakSimTauChain)
    ultimately show ?case by(rule weakStatImpTransitive)
  next
    case(cSim Ψ P R)
    {
      fix Ψ P Q R
      assume "Ψ ⊳ P ≈ Q" and "Ψ ⊳ Q ↝<weakBisim> R"
      moreover have "eqvt ?X"
        by(force simp add: eqvt_def dest: weakBisimClosed)
      with weakBisimEqvt have "eqvt (?X ∪ weakBisim)" by blast
      moreover have "?X ⊆ ?X ∪ weakBisim" by auto
      moreover note weakBisimE(2)
      ultimately have "Ψ ⊳ P ↝<(?X ∪ weakBisim)> R"
        by(rule_tac weakSimTransitive) auto
    }
    with ‹(Ψ, P, R) ∈ ?X› show ?case
      by(blast dest: weakBisimE)
  next
    case(cExt Ψ P R Ψ')
    thus ?case by(blast dest: weakBisimE)
  next
    case(cSym Ψ P R)
    thus ?case by(blast dest: weakBisimE)
  qed
qed

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

  assumes "Ψ ⊳ P ∼ Q"

  shows "Ψ ⊳ P ≈ Q"
proof -
  from ‹Ψ ⊳ P ∼ Q›
  show ?thesis
  proof(coinduct rule: weakBisimWeakCoinduct)
    case(cStatImp Ψ P Q)
    from ‹Ψ ⊳ P ∼ Q› have "insertAssertion(extractFrame P) Ψ ↪⇩F insertAssertion(extractFrame Q) Ψ"
      by(metis bisimE FrameStatEq_def)
    moreover from ‹Ψ ⊳ P ∼ Q› have "⋀Ψ'. Ψ ⊗ Ψ' ⊳ P ∼ Q" by(rule bisimE)
    ultimately show ?case by(rule statImpWeakStatImp)
  next
    case(cSim Ψ P Q)
    note ‹Ψ ⊳ P ∼ Q›
    moreover have "⋀Ψ P Q. Ψ ⊳ P ∼ Q ⟹ insertAssertion(extractFrame Q) Ψ ↪⇩F insertAssertion(extractFrame P) Ψ"
      by(drule_tac bisimE) (simp add: FrameStatEq_def)
    ultimately show ?case using bisimE(2) bisimE(3)
      by(rule strongSimWeakSim)
  next
    case(cExt Ψ P Q Ψ')
    from ‹Ψ ⊳ P ∼ Q› show ?case
      by(rule bisimE)
  next
    case(cSym Ψ P Q)
    from ‹Ψ ⊳ P ∼ Q› show ?case
      by(rule bisimE)
  qed
qed

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

  assumes "P ≡⇩s Q"

  shows "P ≈ Q"
using assms
by(metis structCongBisim strongBisimWeakBisim)

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

  assumes "(Ψ, P, Q) ∈ Rel"
  and     "Ψ ⊳ Q ⟹⇧^⇩τ Q'"
  and     Sim: "⋀Ψ P Q. (Ψ, P, Q) ∈ Rel ⟹ Ψ ⊳ P ↝[Rel] Q"
  
  obtains P' where "Ψ ⊳ P ⟹⇧^⇩τ P'" and "(Ψ, P', Q') ∈ Rel"
proof -
  assume A: "⋀P'. ⟦Ψ ⊳ P ⟹⇧^⇩τ P'; (Ψ, P', Q') ∈ Rel⟧ ⟹ thesis"
  from ‹Ψ ⊳ Q ⟹⇧^⇩τ Q'› ‹(Ψ, P, Q) ∈ Rel› A show ?thesis
  proof(induct arbitrary: P thesis rule: tauChainInduct)
    case(TauBase Q P)
    moreover have "Ψ ⊳ P ⟹⇧^⇩τ P" by simp
    ultimately show ?case by blast
  next
    case(TauStep Q Q' Q'' P)
    from ‹(Ψ, P, Q) ∈ Rel› obtain P' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P'" and "(Ψ, P', Q') ∈ Rel"
      by(rule TauStep)
    from ‹(Ψ, P', Q') ∈ Rel› have "Ψ ⊳ P' ↝[Rel] Q'" by(rule Sim)
    then obtain P'' where P'Chain: "Ψ ⊳ P' ⟼τ ≺ P''" and "(Ψ, P'', Q'') ∈ Rel"
      using ‹Ψ ⊳ Q' ⟼τ ≺ Q''› by(drule_tac simE) auto
    from PChain P'Chain have "Ψ ⊳ P ⟹⇧^⇩τ P''" by(auto dest: tauActTauChain)
    thus ?case using ‹(Ψ, P'', Q'') ∈ Rel› by(rule TauStep)
  qed
qed

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

  assumes "quiet P"

  shows "Ψ ⊳ P ≈ 𝟬"
proof -
  let ?X = "{(Ψ, 𝟬, P) | Ψ P. quiet P} ∪ {(Ψ, P, 𝟬) | Ψ P. quiet P}"

  from ‹quiet P› have "(Ψ, P, 𝟬) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimWeakCoinduct)
    case(cStatImp Ψ P Q)
    thus ?case
      apply(simp add: weakStatImp_def)
      apply(rule allI)
      apply(rule_tac x=Q in exI)
      apply auto
      apply(drule_tac Ψ=Ψ in quietFrame)
      apply(rule_tac G="⟨ε, Ψ⟩" in FrameStatImpTrans)
      using Identity
      apply(simp add: AssertionStatEq_def)
      apply(simp add: FrameStatEq_def)
      apply(drule_tac Ψ=Ψ in quietFrame)
      apply(rule_tac G="⟨ε, Ψ⟩" in FrameStatImpTrans)
      apply auto
      defer
      using Identity
      apply(simp add: AssertionStatEq_def)
      apply(simp add: FrameStatEq_def)
      done
  next
    case(cSim Ψ P Q)
    moreover have "eqvt ?X" by(auto simp add: eqvt_def intro: quietEqvt)
    ultimately show ?case
      apply auto
      apply(rule quietSim)
      apply auto
      apply(auto simp add: weakSimulation_def)
      done
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by blast
  next
    case(cSym Ψ P Q)
    thus ?case by blast
  qed
qed

lemma weakTransitiveWeakCoinduct[case_names cStatImp 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 rStatImp: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ⪅<X> Q"
  and rSim: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ↝<({(Ψ, P, Q) | Ψ P Q. ∃P' 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 Q. ∃P' Q'. Ψ ⊳ P ∼ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q}"
  from p have "(Ψ, P, Q) ∈ ?X"
    by(blast intro: bisimReflexive)
  thus ?thesis
  proof(coinduct rule: weakBisimWeakCoinduct)
    case(cStatImp Ψ P Q)
    {
      fix Ψ'
      from ‹(Ψ , P, Q) ∈ ?X› obtain P' Q' where "Ψ ⊳ P ∼ P'" and "(Ψ, P', Q') ∈ X" and "Ψ ⊳ Q' ∼ Q" by auto
      from ‹(Ψ, P', Q') ∈ X› obtain Q'' Q''' where Q'Chain: "Ψ ⊳ Q' ⟹⇧^⇩τ Q''"
                                               and PImpQ: "insertAssertion (extractFrame P') Ψ ↪⇩F insertAssertion (extractFrame Q'') Ψ"
                                               and Q''Chain: "Ψ ⊗ Ψ' ⊳ Q'' ⟹⇧^⇩τ Q'''" and "(Ψ ⊗ Ψ', P', Q''') ∈ X"
        apply(drule_tac rStatImp) by(auto simp add: weakStatImp_def) blast
      from ‹Ψ ⊳ Q' ∼ Q› have "Ψ ⊳ Q ∼ Q'" by(rule bisimE)
      then obtain Q'''' where "Ψ ⊳ Q ⟹⇧^⇩τ Q''''" and "Ψ ⊳ Q'''' ∼ Q''" using  ‹Ψ ⊳ Q' ⟹⇧^⇩τ Q''› bisimE(2)
        by(rule simTauChain)
      note ‹Ψ ⊳ Q ⟹⇧^⇩τ Q''''›
      moreover have "insertAssertion (extractFrame P) Ψ ↪⇩F insertAssertion (extractFrame Q'''') Ψ"
      proof -
        from ‹Ψ ⊳ P ∼ P'› have "insertAssertion (extractFrame P) Ψ ↪⇩F insertAssertion (extractFrame P') Ψ"
          by(drule_tac bisimE) (simp add: FrameStatEq_def)
        moreover from ‹Ψ ⊳ Q'''' ∼ Q''› have "insertAssertion (extractFrame Q'') Ψ ↪⇩F insertAssertion (extractFrame Q'''') Ψ"
          by(drule_tac bisimE) (simp add: FrameStatEq_def)
        ultimately show ?thesis using PImpQ by(blast intro: FrameStatImpTrans)
      qed
      moreover from ‹Ψ ⊳ Q'''' ∼ Q''› have "Ψ ⊗ Ψ' ⊳ Q'''' ∼ Q''" by(metis bisimE)
      then obtain Q''''' where Q''''Chain: "Ψ ⊗ Ψ' ⊳ Q'''' ⟹⇧^⇩τ Q'''''" and "Ψ ⊗ Ψ' ⊳ Q''''' ∼ Q'''" using Q''Chain bisimE(2)
        by(rule simTauChain)
      moreover from ‹Ψ ⊳ P ∼ P'› ‹(Ψ ⊗ Ψ' , P', Q''') ∈ X› ‹Ψ ⊗ Ψ' ⊳ Q''''' ∼ Q'''› have "(Ψ ⊗ Ψ', P, Q''''') ∈ ?X" by(auto dest: bisimE)
      ultimately have "∃Q' Q''. Ψ ⊳ Q ⟹⇧^⇩τ Q'' ∧ insertAssertion (extractFrame P) Ψ ↪⇩F insertAssertion (extractFrame Q'') Ψ ∧ Ψ ⊗ Ψ' ⊳ Q'' ⟹⇧^⇩τ Q' ∧ (Ψ ⊗ Ψ', P, Q') ∈ ?X" by blast
    }
    with ‹(Ψ, P, Q) ∈ ?X› show ?case by(simp add: weakStatImp_def) blast
  next
    case(cSim Ψ P Q)
    from ‹(Ψ, P, Q) ∈ ?X› obtain P' Q' where "Ψ ⊳ P ∼ P'" and "(Ψ, P', Q') ∈ X" and "Ψ ⊳ Q' ∼ Q" by auto
    from ‹(Ψ, P', Q') ∈ X› have "Ψ ⊳ P' ↝<?X> Q'" 
      by(rule rSim)
    moreover from ‹Ψ ⊳ Q' ∼ Q› have "Ψ ⊳ Q' ↝[bisim] Q" by(rule bisimE)
    moreover from ‹eqvt X› 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'" in exI, simp)
      by(rule_tac x="p ∙ Q'" in exI, auto)
    moreover from ‹Ψ ⊳ Q' ∼ Q› have "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame Q') Ψ"
      by(drule_tac bisimE) (simp add: FrameStatEq_def)
    moreover have "{(Ψ, P, R) | Ψ P R. ∃Q. (Ψ, P, Q) ∈ ?X ∧ Ψ ⊳ Q ∼ R} ⊆ ?X"
      by(blast intro: bisimTransitive)
    moreover note bisimE(3)
    ultimately have "Ψ ⊳ P' ↝<?X> Q" by(rule strongAppend) 
    moreover have "{(Ψ, P, R) | Ψ P R. ∃Q. Ψ ⊳ P ∼ Q ∧ (Ψ, Q, R) ∈ ?X} ⊆ ?X"
      by(blast intro: bisimTransitive)
    moreover {
      fix Ψ P Q

      assume "Ψ ⊳ P ∼ Q"
      moreover have "⋀Ψ P Q. Ψ ⊳ P ∼ Q ⟹ insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P) Ψ"
        by(drule_tac bisimE) (simp add: FrameStatEq_def)
      ultimately have "Ψ ⊳ P ↝<bisim> Q" using bisimE(2) bisimE(3)
        by(rule strongSimWeakSim)
    }
    ultimately show ?case using ‹Ψ ⊳ P ∼ P'› ‹eqvt ?X›
      by(rule_tac weakSimTransitive)
  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 cStatImp 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 rStatImp: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ⪅<(X ∪ weakBisim)> Q"
  and rSim: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ↝<({(Ψ, P, Q) | Ψ P Q. ∃P' Q'. Ψ ⊳ P ∼ P' ∧
                                                                        (Ψ, P', Q') ∈ (X ∪ weakBisim) ∧
                                                                        Ψ ⊳ Q' ∼ Q})> Q"
  and rExt: "⋀Ψ P Q Ψ'. (Ψ, P, Q) ∈ X ⟹ (Ψ ⊗ Ψ', P, Q) ∈ X ∪ weakBisim"
  and rSym: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ (Ψ, Q, P) ∈ X ∪ weakBisim"

  shows "Ψ ⊳ P ≈ Q"
proof -
  from p have "(Ψ, P, Q) ∈ X ∪ weakBisim" by auto
  moreover from ‹eqvt X› have "eqvt(X ∪ weakBisim)" by auto
  ultimately show ?thesis
  proof(coinduct rule: weakTransitiveWeakCoinduct)
    case(cStatImp Ψ P Q)
    thus ?case by(blast dest: rStatImp weakBisimE(1) weakStatImpMonotonic)
  next
    case(cSim Ψ P Q)
    thus ?case by(fastforce intro: rSim weakBisimE(2) weakSimMonotonic bisimReflexive)
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(blast dest: weakBisimE rExt) 
  next
    case(cSym Ψ P Q)
    thus ?case by(blast dest: weakBisimE rSym)
  qed
qed

lemma weakTransitiveCoinduct2[case_names cStatImp 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 rStatImp: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ⪅<X> Q"
  and rSim: "⋀Ψ P Q. (Ψ, P, Q) ∈ X ⟹ Ψ ⊳ P ↝<({(Ψ, P, Q) | Ψ P Q. ∃P' 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 Q. ∃P' Q'. Ψ ⊳ P ≈ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ∼ Q}"
  let ?Y = "{(Ψ, P, Q) | Ψ P Q. ∃P' Q'. Ψ ⊳ P ≈ P' ∧ (Ψ, P', Q') ∈ X ∧ Ψ ⊳ Q' ≈ Q}"

  from ‹eqvt X› have "eqvt ?X"
    apply(auto simp add: eqvt_def)
    apply(drule_tac p=p in bisimClosed)
    apply(drule_tac p=p in weakBisimClosed)
    apply(rule_tac x="p ∙ P'" in exI, simp)
    by(rule_tac x="p ∙ Q'" in exI, auto)
  from ‹eqvt X› have "eqvt ?Y"
    apply(auto simp add: eqvt_def)
    apply(drule_tac p=p in weakBisimClosed)
    apply(drule_tac p=p in weakBisimClosed)
    apply(rule_tac x="p ∙ P'" in exI, simp)
    by(rule_tac x="p ∙ Q'" in exI, auto)

  {
    fix Ψ P Q
    assume "(Ψ, P, Q) ∈ ?X"
    then obtain P' Q' where "Ψ ⊳ P ≈ P'" and "(Ψ, P', Q') ∈ X" and "Ψ ⊳ Q' ∼ Q"
      by auto
    note ‹Ψ ⊳ P ≈ P'›
    moreover from ‹(Ψ, P', Q') ∈ X› have "Ψ ⊳ P' ↝<?X> Q'" by(rule rSim)
    moreover note ‹eqvt ?X›
    moreover have "{(Ψ, P, R) | Ψ P R. ∃Q. Ψ ⊳ P ≈ Q ∧ (Ψ, Q, R) ∈ ?X} ⊆ ?X"
      by(blast intro: weakBisimTransitive)
    ultimately have "Ψ ⊳ P ↝<?X> Q'" using weakBisimE(2) by(rule weakSimTransitive)
    moreover from ‹Ψ ⊳ Q' ∼ Q› have "Ψ ⊳ Q' ↝[bisim] Q" by(rule bisimE)
    moreover note ‹eqvt ?X›
    moreover from ‹Ψ ⊳ Q' ∼ Q› have "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame Q') Ψ"
      by(drule_tac bisimE) (simp add: FrameStatEq_def)
    moreover have "{(Ψ, P, R) | Ψ P R. ∃Q. (Ψ, P, Q) ∈ ?X ∧ Ψ ⊳ Q ∼ R} ⊆ ?X"
      by(blast dest: bisimTransitive)
    moreover note bisimE(3)
    ultimately have "Ψ ⊳ P ↝<?X> Q" by(rule_tac strongAppend) 
  }
  note Goal = this

  from p have "(Ψ, P, Q) ∈ ?Y" by(blast intro: weakBisimReflexive bisimReflexive rSym)
  thus ?thesis
  proof(coinduct rule: weakBisimWeakCoinduct)
  next
    case(cStatImp Ψ P Q)
    {
      fix Ψ'

      from ‹(Ψ, P, Q) ∈ ?Y› obtain R S where "Ψ ⊳ P ≈ R" and "(Ψ, R, S) ∈ X" and "Ψ ⊳ S ≈ Q" by auto
      from ‹Ψ ⊳ P ≈ R› obtain R'' R' 
        where RChain: "Ψ ⊳ R ⟹⇧^⇩τ R''" 
          and PImpR'': "insertAssertion (extractFrame P) Ψ ↪⇩F insertAssertion (extractFrame R'') Ψ"
          and R''Chain: "Ψ ⊗ Ψ' ⊳ R'' ⟹⇧^⇩τ R'" 
          and "Ψ ⊗ Ψ' ⊳ P ≈ R'"
        apply(drule_tac weakBisimE) by(simp add: weakStatImp_def) blast

      from ‹(Ψ, R, S) ∈ X› have "(Ψ, S, R) ∈ ?X" by(blast intro: weakBisimReflexive bisimReflexive rSym)
      with RChain obtain S'' where SChain: "Ψ ⊳ S ⟹⇧^⇩τ S''" and "(Ψ, S'', R'') ∈ ?X" using Goal
        by(rule weakSimTauChain)

      from ‹(Ψ, S'', R'') ∈ ?X› obtain T U where "Ψ ⊳ S'' ≈ T" and "(Ψ, T, U) ∈ X" and "Ψ ⊳ U ∼ R''"
        by auto
      from ‹Ψ ⊳ U ∼ R''› have R''ImpU: "insertAssertion (extractFrame R'') Ψ ↪⇩F insertAssertion (extractFrame U) Ψ"
        by(drule_tac bisimE) (simp add: FrameStatEq_def)
      
      from ‹(Ψ, T, U) ∈ X› weakStatImp_def
      obtain T'' T' where TChain: "Ψ ⊳ T ⟹⇧^⇩τ T''"
                      and UImpT'': "insertAssertion (extractFrame U) Ψ ↪⇩F insertAssertion (extractFrame T'') Ψ"
                      and T''Chain: "Ψ ⊗ Ψ' ⊳ T'' ⟹⇧^⇩τ T'" 
                      and "(Ψ ⊗ Ψ', U, T') ∈ X"
        by(blast dest: rStatImp rSym)

      from TChain ‹Ψ ⊳ S'' ≈ T› weakBisimE(2) obtain S''' where S''Chain: "Ψ ⊳ S'' ⟹⇧^⇩τ S'''" and "Ψ ⊳ S''' ≈ T''"
        by(rule weakSimTauChain)

      from ‹Ψ ⊳ S''' ≈ T''› weakStatImp_def
      obtain S''''' S'''' where S'''Chain: "Ψ ⊳ S''' ⟹⇧^⇩τ S'''''"
                            and T''ImpS''''': "insertAssertion (extractFrame T'') Ψ ↪⇩F insertAssertion (extractFrame S''''') Ψ"
                            and S'''''Chain: "Ψ ⊗ Ψ' ⊳ S''''' ⟹⇧^⇩τ S''''" 
                            and "Ψ ⊗ Ψ' ⊳ T'' ≈ S''''"
        by(metis weakBisimE)
      
      from SChain S''Chain S'''Chain have "Ψ ⊳ S ⟹⇧^⇩τ S'''''" by auto
      moreover from ‹Ψ ⊳ S ≈ Q› have "Ψ ⊳ Q ≈ S" by(rule weakBisimE)
      ultimately obtain Q''' where QChain: "Ψ ⊳ Q ⟹⇧^⇩τ Q'''" and "Ψ ⊳ Q''' ≈ S'''''" using weakBisimE(2)
        by(rule weakSimTauChain)
      from ‹Ψ ⊳ Q''' ≈ S'''''› have "Ψ ⊳ S''''' ≈ Q'''" by(rule weakBisimE)
      then obtain Q'' Q' where Q'''Chain: "Ψ ⊳ Q''' ⟹⇧^⇩τ Q''"
                           and S'''''ImpQ'': "insertAssertion (extractFrame S''''') Ψ ↪⇩F insertAssertion (extractFrame Q'') Ψ"
                           and Q''Chain: "Ψ ⊗ Ψ' ⊳ Q'' ⟹⇧^⇩τ Q'" 
                           and "Ψ ⊗ Ψ' ⊳ S''''' ≈ Q'" using weakStatImp_def
        by(metis weakBisimE)

      from QChain Q'''Chain have "Ψ ⊳ Q ⟹⇧^⇩τ Q''" by auto
      moreover from PImpR'' R''ImpU UImpT'' T''ImpS''''' S'''''ImpQ''
      have "insertAssertion (extractFrame P) Ψ ↪⇩F insertAssertion (extractFrame Q'') Ψ"
        by(blast dest: FrameStatImpTrans)

      moreover from ‹Ψ ⊳ U ∼ R''› have "Ψ ⊗ Ψ' ⊳ U ≈ R''" by(metis weakBisimE strongBisimWeakBisim)
      with R''Chain obtain U' where UChain: "Ψ ⊗ Ψ' ⊳ U ⟹⇧^⇩τ U'" and "Ψ ⊗ Ψ' ⊳ U' ≈ R'" using weakBisimE(2)
        by(rule weakSimTauChain)
      from ‹Ψ ⊗ Ψ' ⊳ U' ≈ R'› have "Ψ ⊗ Ψ' ⊳ R' ≈ U'" by(rule weakBisimE)
      from ‹(Ψ ⊗ Ψ', U, T') ∈ X› have "(Ψ ⊗ Ψ', T', U) ∈ ?X" by(blast intro: rSym weakBisimReflexive bisimReflexive)
      with UChain obtain T''' where T'Chain: "Ψ ⊗ Ψ' ⊳ T' ⟹⇧^⇩τ T'''" and "(Ψ ⊗ Ψ', T''', U') ∈ ?X" using Goal
        by(rule weakSimTauChain)
      from ‹(Ψ ⊗ Ψ', T''', U') ∈ ?X› have "(Ψ ⊗ Ψ', U', T''') ∈ ?Y" 
        by(blast dest: weakBisimE rSym strongBisimWeakBisim)
      from T''Chain T'Chain have "Ψ ⊗ Ψ' ⊳ T'' ⟹⇧^⇩τ T'''" by auto
      then obtain S'''''' where S''''Chain: "Ψ ⊗ Ψ' ⊳ S'''' ⟹⇧^⇩τ S''''''" and "Ψ ⊗ Ψ' ⊳ T''' ≈ S''''''" 
        using  ‹Ψ ⊗ Ψ' ⊳ T'' ≈ S''''› weakBisimE(2)
        apply(drule_tac weakBisimE(4))
        by(rule weakSimTauChain) (auto dest: weakBisimE(4))
      from S'''''Chain S''''Chain have "Ψ ⊗ Ψ' ⊳ S''''' ⟹⇧^⇩τ S''''''" by auto

      with ‹Ψ ⊗ Ψ' ⊳ S''''' ≈ Q'›
      obtain Q'''' where Q'Chain: "Ψ ⊗ Ψ' ⊳ Q' ⟹⇧^⇩τ Q''''" and "Ψ ⊗ Ψ' ⊳ S'''''' ≈ Q''''" using weakBisimE(2)
        apply(drule_tac weakBisimE(4))
        by(rule weakSimTauChain) (auto dest: weakBisimE(4))

      from Q''Chain Q'Chain have "Ψ ⊗ Ψ' ⊳ Q'' ⟹⇧^⇩τ Q''''" by auto
      moreover from ‹Ψ ⊗ Ψ' ⊳ P ≈ R'› ‹Ψ ⊗ Ψ' ⊳ R' ≈ U'› ‹(Ψ ⊗ Ψ', U', T''') ∈ ?Y› ‹Ψ ⊗ Ψ' ⊳ T''' ≈ S''''''›
                    ‹Ψ ⊗ Ψ' ⊳ S'''''' ≈ Q''''›
      have "(Ψ ⊗ Ψ', P, Q'''') ∈ ?Y"
        by auto (blast dest: weakBisimTransitive)
      ultimately have "∃Q'' Q'. Ψ ⊳ Q ⟹⇧^⇩τ Q'' ∧ insertAssertion (extractFrame P) Ψ ↪⇩F insertAssertion (extractFrame Q'') Ψ ∧ Ψ ⊗ Ψ' ⊳ Q'' ⟹⇧^⇩τ Q' ∧ (Ψ ⊗ Ψ', P, Q') ∈ ?Y"
        by blast
    }
    thus ?case by(simp add: weakStatImp_def)
  next
    case(cSim Ψ P Q)
    moreover {
      fix Ψ P P' Q' Q
      assume "Ψ ⊳ P ≈ P'" and "(Ψ, P', Q') ∈ X" and "Ψ ⊳ Q' ≈ Q"
      from ‹(Ψ, P', Q') ∈ X› have "(Ψ, P', Q') ∈ ?X"
        by(blast intro: weakBisimReflexive bisimReflexive)
      moreover from ‹Ψ ⊳ Q' ≈ Q› have "Ψ ⊳ Q' ↝<weakBisim> Q" by(rule weakBisimE)
      moreover note ‹eqvt ?Y›
      moreover have "{(Ψ, P, R) | Ψ P R. ∃Q. (Ψ, P, Q) ∈ ?X ∧ Ψ ⊳ Q ≈ R} ⊆ ?Y"
        by(blast dest: weakBisimTransitive strongBisimWeakBisim)
      ultimately have "Ψ ⊳ P' ↝<?Y> Q" using Goal
        by(rule weakSimTransitive)
      note ‹Ψ ⊳ P ≈ P'› this ‹eqvt ?Y›
      moreover have "{(Ψ, P, R) | Ψ P R. ∃Q. Ψ ⊳ P ≈ Q ∧ (Ψ, Q, R) ∈ ?Y} ⊆ ?Y"
        by(blast dest: weakBisimTransitive)
      ultimately have "Ψ ⊳ P ↝<?Y> Q" using weakBisimE(2)
        by(rule weakSimTransitive)
    }      
    ultimately show ?case by auto
  next
    case(cExt Ψ P Q Ψ')
    thus ?case by(blast dest: bisimE weakBisimE intro: rExt)
  next
    case(cSym Ψ P Q) 
    thus ?case by(blast dest: bisimE(4) weakBisimE(4) rSym)
  qed
qed

end

end