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 \<leadsto>[A] Q"
  and     "A ⊆ B"

  shows "P \<leadsto>[B] Q"
using assms
by(fastsimp simp add: simulation_def)

lemma monoCoinduct: "!!x y xa xb P Q.
                      x ≤ y ==>
                      (Q \<leadsto>[{(xb, xa). x xb xa}] P) -->
                     (Q \<leadsto>[{(xb, xa). y xb xa}] P)"
apply auto
apply(rule monotonic)
by(auto dest: le_funE)

coinductive_set bisim :: "(ccs × ccs) set"
where
  "[|P \<leadsto>[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 \<leadsto>[(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 \<leadsto>[(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 \<leadsto>[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 \<leadsto>[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 \<leadsto>[bisim] Q"
  and   "Q ∼ P"
using assms
by(auto simp add: intro: bisim.cases)

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

  assumes "P \<leadsto>[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 \<leadsto>[(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 \<leadsto>[bisim] R" by(rule bisimE)
    moreover from `(R, S) ∈ X` have "R \<leadsto>[(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 \<leadsto>[(bisim O X O bisim)] S"
      by(rule Strong_Sim.transitive)
    moreover from `S ∼ Q` have "S \<leadsto>[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