Theory Strong_Early_Bisim

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Strong_Early_Bisim
  imports Strong_Early_Sim
begin

lemma monoAux: "A ⊆ B ⟹ P ↝[A] Q ⟶ P ↝[B] Q"
by(auto intro: Strong_Early_Sim.monotonic)

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

abbreviation strongBisimJudge (infixr "∼" 65) where "P ∼ Q ≡ (P, Q) ∈ bisim"


lemma bisimCoinductAux[case_names bisim, case_conclusion StrongBisim step, consumes 1]:
  assumes p: "(P, Q) ∈ X"
  and step:  "⋀P Q. (P, Q) ∈ X ⟹ P ↝[(X ∪ bisim)] Q ∧ (Q, P) ∈ bisim ∪ X"

  shows "P ∼ Q"
proof -
  have aux: "X ∪ bisim = {(P, Q). (P, Q) ∈ X ∨ P ∼ Q}" by blast

  from p show ?thesis
    by(coinduct, force dest: step simp add: aux)
qed

lemma bisimCoinduct[consumes 1, case_names cSim cSym]:
  fixes P :: pi
  and   Q :: pi
  
  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"
using assms
by(coinduct rule: bisimCoinductAux) auto

lemma weak_coinduct[case_names bisim, case_conclusion StrongBisim step, consumes 1]:
  assumes p: "(P, Q) ∈ X"
  and step:  "⋀P Q. (P, Q) ∈ X ⟹ P ↝[X] Q ∧ (Q, P) ∈ X"
 
  shows "P ∼ Q"
using p
proof(coinduct rule: bisimCoinductAux)
  case (bisim P)
  from step[OF this] show ?case using Strong_Early_Sim.monotonic by blast
qed

lemma bisimWeakCoinduct[consumes 1, case_names cSim cSym]:
  fixes P :: pi
  and   Q :: pi
  
  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"
using assms
by(coinduct rule: weak_coinduct) auto

lemma monotonic: "mono(λp x1 x2.
        ∃P Q. x1 = P ∧
              x2 = Q ∧ P ↝[{(xa, x). p xa x}] Q ∧ Q ↝[{(xa, x). p xa x}] P)"
apply(rule monoI)
by(auto intro: Strong_Early_Sim.monotonic)

lemma bisimE:
  fixes P :: pi
  and   Q :: pi

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

lemma bisimClosed[eqvt]:
  fixes P :: pi
  and   Q :: pi
  and   p :: "name prm"

  assumes "P ∼ Q"

  shows "(p ∙ P) ∼ (p ∙ Q)"
proof -
  let ?X = "{(p ∙ P, p ∙ Q) | (p::name prm) P Q. P ∼ Q}"
  from assms have "(p ∙ P, p ∙ Q) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cSim P Q)
    moreover {
      fix P Q
      fix p::"name prm"
      assume "P ↝[bisim] Q"

      moreover have "bisim ⊆ ?X"
        by(auto, rule_tac x="[]" in exI) auto
      moreover have "eqvt ?X"
        by(auto simp add: eqvt_def pt2[OF pt_name_inst, THEN sym]) blast
      ultimately have "(p ∙ P) ↝[?X] (p ∙ Q)"
        by(rule Strong_Early_Sim.eqvtI)
    }
    ultimately show ?case by(blast dest: bisimE)
  next
    case(cSym P Q)
    thus ?case by(blast dest: bisimE)
  qed
qed

lemma eqvt[simp]:
  shows "eqvt bisim"
by(auto simp add: eqvt_def eqvts)

lemma reflexive:
  fixes P :: pi

  shows "P ∼ P"
proof -
  have "(P, P) ∈ Id" by simp
  then show ?thesis
    by(coinduct rule: bisimWeakCoinduct) (auto intro: Strong_Early_Sim.reflexive)
qed

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

  assumes PBiSimQ: "P ∼ Q"
  and     QBiSimR: "Q ∼ R"

  shows "P ∼ R"
proof -
  let ?X = "bisim O bisim"
  from assms have "(P, R) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cSim P Q)
    moreover {
      fix P Q R
      assume "P ∼ Q" and "Q ∼ R"
      hence "P ↝[bisim] Q" and "Q ↝[bisim] R"
        by(metis bisimE)+
      moreover from eqvt have "eqvt ?X" by(auto simp add: eqvtTrans)
      moreover have "bisim O bisim ⊆ ?X" by auto

      ultimately have "P ↝[?X] R"
        by(rule Strong_Early_Sim.transitive)
    }
    ultimately show ?case by auto
  next
    case(cSym P Q)
    thus ?case by(auto dest: bisimE)
  qed
qed

end