Theory Weak_Late_Bisim

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

lemma monoAux: "A ⊆ B ⟹ P ↝⇧^<A> Q ⟶ P ↝⇧^<B> Q"
by(auto intro: Weak_Late_Sim.monotonic)

coinductive_set weakBisim :: "(pi × pi) set"
where
  step: "⟦P ↝⇧^<weakBisim> Q; (Q, P) ∈ weakBisim⟧ ⟹ (P, Q) ∈ weakBisim"
monos monoAux

abbreviation
  "weakBisimJudge" (infixr ‹≈› 65)  where "P ≈ Q ≡ (P, Q) ∈ weakBisim"

lemma weakBisimCoinductAux[case_names weakBisim, case_conclusion weakBisim step, consumes 1]:
  assumes p: "(P, Q) ∈ X"
  and step:  "⋀P Q. (P, Q) ∈ X ⟹ P ↝⇧^<(X ∪ weakBisim)> Q ∧ ((Q, P) ∈ X ∨ Q ≈ P)"

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

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

lemma weakBisimCoinduct[consumes 1, case_names cSim cSym]:
  fixes P :: pi
  and   Q :: pi

  assumes "(P, Q) ∈ X"
  and     "⋀P Q. (P, Q) ∈ X ⟹ P ↝⇧^<(X ∪ weakBisim)> Q"
  and     "⋀P Q. (P, Q) ∈ X ⟹ (Q, P) ∈ X"

  shows "P ≈ Q"
using assms
by(coinduct rule: weakBisimCoinductAux) auto

lemma weak_coinduct[case_names weakBisim, case_conclusion weakBisim 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: weakBisimCoinductAux)
  case (weakBisim P Q)
  from step[OF this] show ?case using Weak_Late_Sim.monotonic by blast
qed

lemma weakBisimWeakCoinduct[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)"
by(auto intro: monoI Weak_Late_Sim.monotonic)

lemma unfoldE:
  fixes P :: pi
  and   Q :: pi

  assumes "P ≈ Q"
  
  shows "P ↝⇧^<weakBisim> Q"
  and   "Q ≈ P"
using assms
by(auto intro: weakBisim.cases)

lemma unfoldI:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ↝⇧^<weakBisim> Q"
  and     "Q ≈ P"

  shows "P ≈ Q"
using assms
by(auto intro: weakBisim.cases)

lemma eqvt:
  shows "eqvt weakBisim"
proof(auto simp add: eqvt_def)
  let ?X = "{x. ∃P Q (perm::name prm). P ≈ Q ∧ x = (perm ∙ P, perm ∙ Q)}"
  fix P Q
  fix perm::"name prm"
  assume PBiSimQ: "P ≈ Q"

  hence "(perm ∙ P, perm ∙ Q) ∈ ?X" by blast
  moreover have "⋀P Q perm::name prm. ⟦P ↝⇧^<weakBisim> Q⟧ ⟹ (perm ∙ P) ↝⇧^<?X> (perm ∙ Q)"
  proof -
    fix P Q
    fix perm::"name prm"
    assume "P ↝⇧^<weakBisim> Q"

    moreover have "weakBisim ⊆ ?X"
    proof(auto)
      fix P Q
      assume "P ≈ Q"
      moreover have "P = ([]::name prm) ∙ P" and "Q = ([]::name prm) ∙ Q" by auto
      ultimately show "∃P' Q'. P' ≈ Q' ∧ (∃(perm::name prm). P = perm ∙ P' ∧ Q = perm ∙ Q')"
        by blast
    qed

    moreover have "eqvt ?X"
    proof(auto simp add: eqvt_def)
      fix P Q
      fix perm1::"name prm"
      fix perm2::"name prm"

      assume "P ≈ Q"
      moreover have "perm1 ∙ perm2 ∙ P = (perm1 @ perm2) ∙ P" by(simp add: pt2[OF pt_name_inst])
      moreover have "perm1 ∙ perm2 ∙ Q = (perm1 @ perm2) ∙ Q" by(simp add: pt2[OF pt_name_inst])

      ultimately show "∃P' Q'. P' ≈ Q' ∧ (∃(perm::name prm). perm1 ∙ perm2 ∙ P = perm ∙ P' ∧
                                                              perm1 ∙ perm2 ∙ Q = perm ∙ Q')"
        by blast
    qed

    ultimately show "(perm ∙ P) ↝⇧^<?X> (perm ∙ Q)"
      by(rule Weak_Late_Sim.eqvtI)
    qed

    ultimately show "(perm ∙ P) ≈ (perm ∙ Q)" by(coinduct rule: weak_coinduct, blast dest: unfoldE)
qed

lemma eqvtI:
  fixes P :: pi
  and   Q :: pi
  and   perm :: "name prm"

  assumes "P ≈ Q"

  shows "(perm ∙ P) ≈ (perm ∙ Q)"
using assms
by(rule eqvtRelI[OF eqvt])

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

lemma strongBisimWeakBisim:
  fixes P :: pi
  and   Q :: pi

  assumes PSimQ: "P ∼ Q"

  shows "P ≈ Q"
proof -
  have "⋀P Q. P ↝[bisim] Q ⟹ P ↝⇧^<(bisim ∪ weakBisim)> Q"
  proof -
    fix P Q
    assume "P ↝[bisim] Q"
    hence "P ↝⇧^<bisim> Q" by(rule strongSimWeakSim)
    thus "P ↝⇧^<(bisim ∪ weakBisim)> Q"
      by(blast intro: Weak_Late_Sim.monotonic)
  qed

  with PSimQ show ?thesis
    by(coinduct rule: weakBisimCoinductAux, force dest: Strong_Late_Bisim.bisimE symmetric)
qed

lemma reflexive:
  fixes P :: pi

  shows "P ≈ P"
proof -
  have "(P, P) ∈ Id" by simp
  then show ?thesis

  proof (coinduct rule: weak_coinduct)
    case (weakBisim P Q)
    have "(P, Q) ∈ Id" by fact
    thus ?case by(auto intro: Weak_Late_Sim.reflexive)
  qed
qed

lemma symmetric:
  fixes P :: pi
  and   Q :: pi
   
  assumes "P ≈ Q"

  shows "Q ≈ P"
using assms
by(auto dest: unfoldE intro: unfoldI)

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 = "weakBisim O weakBisim"
  from assms have "(P, R) ∈ ?X" by blast
  moreover have "⋀P Q R. ⟦Q ↝⇧^<weakBisim> R; P ≈ Q⟧ ⟹
                          P ↝⇧^<(?X ∪ weakBisim)> R"
  proof -
    fix P Q R
    assume PBiSimQ: "P ≈ Q"
    assume "Q ↝⇧^<weakBisim> R"
    moreover have "eqvt weakBisim" by(rule eqvt)
    moreover from eqvt have "eqvt (?X ∪ weakBisim)" by(auto simp add: eqvtTrans)
    moreover have "weakBisim O weakBisim ⊆ ?X ∪ weakBisim" by auto
    moreover have "⋀P Q. P ≈ Q ⟹ P ↝⇧^<weakBisim> Q" by(rule unfoldE)

    ultimately show "P ↝⇧^<(?X ∪ weakBisim)> R" using PBiSimQ
      by(rule Weak_Late_Sim.transitive)
  qed

  ultimately show ?thesis
    apply(coinduct rule: weakBisimCoinduct, auto)
    by(blast dest: unfoldE symmetric)+
qed


lemma transitive_coinduct_weak[case_names WeakBisimEarly, case_conclusion WeakBisimEarly step, consumes 2]:
  assumes p: "(P, Q) ∈ X"
  and Eqvt: "eqvt X"
  and step: "⋀P Q. (P, Q) ∈ X ⟹ P ↝⇧^<(bisim O X O bisim)> Q ∧ (Q, P) ∈ X"

  shows "P ≈ Q"
proof -
  let ?X = "bisim O X O bisim"

  have Sim: "⋀P P' Q' Q. ⟦P ∼ P'; P'↝⇧^<?X> Q'; Q' ↝[bisim] Q⟧ ⟹
                          P ↝⇧^<?X> Q"
  proof -
    fix P P' Q' Q
    assume PBisimP': "P ∼ P'"
    assume P'SimQ': "P' ↝⇧^<?X> Q'"
    assume Q'SimQ: "Q' ↝[bisim] Q"

    show "P ↝⇧^<?X> Q"
    proof -
      have "P' ↝⇧^<?X> Q"
      proof -
        have "?X O bisim ⊆ ?X" by(blast intro: Strong_Late_Bisim.transitive)
        moreover from Strong_Late_Bisim.bisimEqvt Eqvt have "eqvt ?X" by blast
        ultimately show ?thesis using P'SimQ' Q'SimQ by(blast intro: strongAppend)
      qed
      moreover have "eqvt bisim" by(rule Strong_Late_Bisim.bisimEqvt)
      moreover from Strong_Late_Bisim.bisimEqvt Eqvt have "eqvt ?X" by blast
      moreover have "bisim O ?X ⊆ ?X" by(blast intro: Strong_Late_Bisim.transitive)
      moreover have "⋀P Q. P ∼ Q ⟹ P ↝⇧^<bisim> Q" by(blast dest: Strong_Late_Bisim.bisimE strongSimWeakSim)
      ultimately show ?thesis using PBisimP' by(rule Weak_Late_Sim.transitive)
    qed
  qed

  from p have "(P, Q) ∈ ?X" by(blast intro: Strong_Late_Bisim.reflexive)
  moreover from step Sim have "⋀P Q. (P, Q) ∈ ?X ⟹ P ↝⇧^<?X> Q ∧ (Q, P) ∈ ?X"
    by(blast dest: Strong_Late_Bisim.bisimE Strong_Late_Bisim.symmetric)

  ultimately show ?thesis by(rule weak_coinduct)
qed

lemma weakBisimTransitiveCoinduct[case_names cSim cSym, consumes 2]:
  assumes p: "(P, Q) ∈ X"
  and Eqvt: "eqvt X"
  and rSim: "⋀P Q. (P, Q) ∈ X ⟹ P ↝⇧^<(bisim O X O bisim)> Q"
  and rSym: "⋀P Q. (P, Q) ∈ X ⟹ (Q, P) ∈ X"

  shows "P ≈ Q"
using assms
by(coinduct rule: transitive_coinduct_weak) auto

end