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