Theory Strong_Bisim

(* 
   Title: The Calculus of Communicating Systems   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Strong_Bisim
  imports Strong_Sim
begin

lemma monotonic:
  fixes P :: ccs
  and   A :: "(ccs × ccs) set"
  and   Q :: ccs
  and   B :: "(ccs × ccs) set"

  assumes "P ↝[A] Q"
  and     "A ⊆ B"

  shows "P ↝[B] Q"
using assms
by(fastforce simp add: simulation_def)

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

coinductive_set bisim :: "(ccs × ccs) set"
where
  "⟦P ↝[bisim] Q; (Q, P) ∈ bisim⟧ ⟹ (P, Q) ∈ bisim"
monos monoCoinduct

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

lemma bisimCoinductAux[consumes 1]:
  fixes P :: "ccs"
  and   Q :: "ccs"
  and   X :: "(ccs × ccs) set"

  assumes "(P, Q) ∈ X"
  and     "⋀P Q. (P, Q) ∈ X ⟹ P ↝[(X ∪ bisim)] Q ∧ (Q, P) ∈ X"

  shows "P ∼ Q"
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 cSim cSym]:
  fixes P :: "ccs"
  and   Q :: "ccs"
  and   X :: "(ccs × ccs) set"

  assumes "(P, Q) ∈ X"
  and     "⋀R S. (R, S) ∈ X ⟹ R ↝[(X ∪ bisim)] S"
  and     "⋀R S. (R, S) ∈ X ⟹ (S, R) ∈ X"

  shows "P ∼ Q"
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 P :: "ccs"
  and   Q :: "ccs"
  and   X :: "(ccs × ccs) set"

  assumes "(P, Q) ∈ X"
  and     "⋀R S. (R, S) ∈ X ⟹ R ↝[X] S ∧ (S, R) ∈ X" 

  shows "P ∼ Q"
using assms
by(coinduct rule: bisimCoinductAux) (blast intro: monotonic)

lemma bisimWeakCoinduct[consumes 1, case_names cSim cSym]:
  fixes P :: "ccs"
  and   Q :: "ccs"
  and   X :: "(ccs × ccs) set"

  assumes "(P, Q) ∈ X"
  and     "⋀P Q. (P, Q) ∈ X ⟹ P ↝[X] Q"
  and     "⋀P Q. (P, Q) ∈ X ⟹ (Q, P) ∈ X"

  shows "P ∼ Q"
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  :: "ccs"
  and   Q  :: "ccs"

  assumes "P ∼ Q"

  shows "P ↝[bisim] Q"
  and   "Q ∼ P"
using assms
by(auto simp add: intro: bisim.cases)

lemma bisimI:
  fixes P :: "ccs"
  and   Q :: "ccs"

  assumes "P ↝[bisim] Q"
  and     "Q ∼ P"

  shows "P ∼ Q"
using assms
by(auto intro: bisim.intros)

lemma reflexive: 
  fixes P :: ccs

  shows "P ∼ P"
proof -
  have "(P, P) ∈ Id" by blast
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: reflexive)
qed

lemma symmetric: 
  fixes P :: ccs
  and   Q :: ccs

  assumes "P ∼ Q"

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

lemma transitive: 
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes "P ∼ Q"
  and     "Q ∼ R"

  shows "P ∼ R"
proof -
  from assms have "(P, R) ∈ bisim O bisim" by auto
  thus ?thesis
    by(coinduct rule: bisimCoinduct) (auto intro: transitive dest: bisimE)
qed

lemma bisimTransCoinduct[consumes 1, case_names cSim cSym]:
  fixes P :: ccs
  and   Q :: ccs

  assumes "(P, Q) ∈ X"
  and     rSim: "⋀R S. (R, S) ∈ X ⟹ R ↝[(bisim O X O bisim)] S"
  and     rSym: "⋀R S. (R, S) ∈ X ⟹ (S, R) ∈ X"

  shows "P ∼ Q"
proof -
  from ‹(P, Q) ∈ X› have "(P, Q) ∈ bisim O X O bisim"
    by(auto intro: reflexive)
  thus ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cSim P Q)
    from ‹(P, Q) ∈ bisim O X O bisim›
    obtain R S where "P ∼ R" and "(R, S) ∈ X" and "S ∼ Q"
      by auto
    from ‹P ∼ R› have "P ↝[bisim] R" by(rule bisimE)
    moreover from ‹(R, S) ∈ X› have "R ↝[(bisim O X O bisim)] S"
      by(rule rSim)
    moreover have "bisim O (bisim O X O bisim) ⊆ bisim O X O bisim"
      by(auto intro: transitive)
    ultimately have "P ↝[(bisim O X O bisim)] S"
      by(rule Strong_Sim.transitive)
    moreover from ‹S ∼ Q› have "S ↝[bisim] Q" by(rule bisimE)
    moreover have "(bisim O X O bisim) O bisim ⊆ bisim O X O bisim"
      by(auto intro: transitive)
    ultimately show ?case by(rule Strong_Sim.transitive)
  next
    case(cSym P Q)
    thus ?case by(auto dest: symmetric rSym)
  qed
qed

end