Theory Strong_Late_Bisim

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

lemma monoAux: "A ⊆ B ⟹ P ↝[A] Q ⟶ P ↝[B] Q"
by(auto intro: Strong_Late_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 monotonic': "mono(λS. {(P, Q) |P Q. P ↝[S] Q ∧ Q ↝[S] P})"
apply(rule monoI)
by(auto dest: monoAux)

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_Late_Sim.monotonic)


lemma bisimCoinduct[case_names cSim cSym , consumes 1]:
  assumes p: "(P, Q) ∈ X"
  and     rSim: "⋀R S. (R, S) ∈ X ⟹ R ↝[(X ∪ bisim)] S"
  and     rSym: "⋀R S. (R, S) ∈ X ⟹ (S, R) ∈ X"

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

  from p show ?thesis
    apply(coinduct, auto)
    apply(fastforce dest: rSim simp add: aux)
    by(fastforce dest: rSym)
qed

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

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

lemma bisimI:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ↝[bisim] Q"
  and     "Q ∼ P"

  shows "P ∼ Q"
using assms
by(rule bisim.intros)

definition old_bisim :: "(pi × pi) set ⇒ bool" where
  "old_bisim Rel ≡ ∀(P, Q) ∈ Rel. P ↝[Rel] Q ∧ (Q, P) ∈ Rel"

lemma oldBisimBisimEq:
  shows "(⋃{Rel. (old_bisim Rel)}) = bisim"  (is "?LHS = ?RHS")
proof
  show "?LHS ⊆ ?RHS"
  proof auto
    fix P Q Rel
    assume "(P, Q) ∈ Rel" and "old_bisim Rel"
    thus "P ∼ Q"
    proof(coinduct rule: bisimCoinduct)
      case(cSim P Q)
      with ‹old_bisim Rel› show ?case
        by(fastforce simp add: old_bisim_def intro: Strong_Late_Sim.monotonic)
    next
      case(cSym P Q)
      with ‹old_bisim Rel› show ?case
        by(auto simp add: old_bisim_def)
    qed
  qed
next
  show "?RHS ⊆ ?LHS"
  proof auto
    fix P Q
    assume "P ∼ Q"
    moreover hence "old_bisim bisim"
      by(auto simp add: old_bisim_def dest: bisim.cases)
    ultimately show "∃Rel. old_bisim Rel ∧ (P, Q) ∈ Rel"
      by blast
  qed
qed

lemma reflexive:
  fixes P :: pi

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

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

  shows "Q ∼ P"
using assms
by(auto dest: bisim.cases)

lemma bisimClosed:
  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 Q (p::name prm). P ∼ Q}"
  from ‹P ∼ Q› have  "(p ∙ P, p ∙ Q) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim pP pQ)
    from ‹(pP, pQ) ∈ ?X› obtain P Q p where "P ∼ Q" and "pP = (p::name prm) ∙ P" and "pQ = p ∙ Q"
      by auto
    from ‹P ∼ Q› have "P ↝[bisim] Q" by(rule bisimE)
    moreover have "bisim ⊆ ?X"
    proof 
      fix x
      assume "x ∈ bisim"
      moreover have "x = (([]::name prm) ∙ x)" by auto
      ultimately show "x ∈ ?X"
        apply(case_tac x)
        by(clarify, simp only: eqvts) metis
    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'. (∃(perm::name prm). perm1 ∙ perm2 ∙ P = perm ∙ P' ∧
                                                   perm1 ∙ perm2 ∙ Q = perm ∙ Q') ∧ P' ∼ Q'"
        by blast
    qed
    ultimately have "(p ∙ P) ↝[?X] (p ∙ Q)" 
      by(rule Strong_Late_Sim.eqvtI)
    with ‹pP = p ∙ P› ‹pQ = p ∙ Q› show ?case
      by(force intro: Strong_Late_Sim.monotonic)
  next
    case(cSym P Q)
    thus ?case by(auto intro: symmetric)
  qed
qed

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

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

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

  shows "P ∼ R"
proof -
  let ?X = "bisim O bisim"
  from assms have "(P, R) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim P R)
    thus ?case
      by(fastforce intro: Strong_Late_Sim.transitive dest: bisimE simp add: eqvtTrans)
  next
    case(cSym P R)
    thus ?case
      by(auto dest: symmetric)
  qed
qed

lemma bisimTransitiveCoinduct[case_names cSim cSym, case_conclusion bisim step, consumes 2]:
  assumes "(P, Q) ∈ X"
  and "eqvt X"
  and rSim: "⋀R S. (R, S) ∈ X ⟹ R ↝[(bisim O (X ∪ bisim) O bisim)] S"
  and rSym: "⋀R S. (R, S) ∈ X ⟹ (S, R) ∈ bisim O (X ∪ bisim) O bisim"

  shows "P ∼ Q"
proof -
  let ?X = "bisim O (X ∪ bisim) O bisim"
  from ‹(P, Q) ∈ X›  have "(P, Q) ∈ ?X" by(auto intro: reflexive)
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim P Q)
    {
      fix P P' Q' Q

      assume "P ∼ P'" and "(P', Q') ∈ X ∪ bisim" and "Q' ∼ Q"
      have "P ↝[(?X ∪ bisim)] Q"
      proof(cases "(P', Q') ∈ X")
        case True
        from ‹P ∼ P'› have "P ↝[bisim] P'" by(rule bisimE)
        moreover from ‹(P', Q') ∈ X› have "P' ↝[(?X)] Q'" by(rule rSim)
        moreover from ‹eqvt X› bisimEqvt have "eqvt(?X ∪ bisim)" by blast
        moreover have "bisim O ?X ⊆ ?X ∪ bisim" by(auto dest: transitive)
        ultimately have "P ↝[(?X ∪ bisim)] Q'" by(rule Strong_Late_Sim.transitive)
        moreover from ‹Q' ∼ Q› have "Q' ↝[bisim] Q" by(rule bisimE)
        moreover note ‹eqvt(?X ∪ bisim)›
        moreover have "(?X ∪ bisim) O bisim ⊆ ?X ∪ bisim"
          by auto (blast dest: transitive)+
        ultimately show ?thesis by(rule Strong_Late_Sim.transitive)
      next
        case False
        from ‹(P', Q') ∉ X› ‹(P', Q') ∈ X ∪ bisim› have "P' ∼ Q'" by simp
        with ‹P ∼ P'› ‹Q' ∼ Q› have "P ∼ Q" by(blast dest: transitive)
        hence "P ↝[bisim] Q" by(rule bisimE)
        moreover have "bisim ⊆ ?X ∪ bisim" by auto
        ultimately show ?thesis by(rule Strong_Late_Sim.monotonic)
      qed
    }
    with ‹(P, Q) ∈ ?X› show ?case by auto
    case(cSym P Q)
    {
      fix P P' Q' Q

      assume "P ∼ P'" and "(P', Q') ∈ X ∪ bisim" and "Q' ∼ Q"
      have "(Q, P) ∈ bisim O (X ∪ bisim) O bisim"
      proof(cases "(P', Q') ∈ X")
        case True
        from ‹(P', Q') ∈ X› have "(Q', P') ∈ ?X" by(rule rSym)
        then obtain Q'' P'' where "Q' ∼ Q''" and "(Q'', P'') ∈ X ∪ bisim" and "P'' ∼ P'"
          by auto
        from ‹Q' ∼ Q› ‹Q' ∼ Q''› have "Q ∼ Q''" by(metis transitive symmetric)
        moreover from ‹P ∼ P'› ‹P'' ∼ P'› have "P'' ∼ P" by(metis transitive symmetric)
        ultimately show ?thesis using ‹(Q'', P'') ∈ X ∪ bisim› by blast
      next
        case False
        from ‹(P', Q') ∉ X› ‹(P', Q') ∈ X ∪ bisim› have "P' ∼ Q'" by simp
        with ‹P ∼ P'› ‹Q' ∼ Q› have "Q ∼ P" by(metis transitive symmetric)
        thus ?thesis by(blast intro: reflexive)
      qed
    }
    with ‹(P, Q) ∈ ?X› show ?case by blast
  qed
qed

end