Theory Weak_Early_Bisim

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

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

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

abbreviation weakEarlyBisimJudge (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 ∪ weakBisim"

  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 weakBisimWeakCoinductAux[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)
  from step[OF this] show ?case using Weak_Early_Sim.monotonic by blast
qed

lemma weakBisimCoinduct[consumes 1, case_names cSim cSym]:
  fixes P :: pi
  and   Q :: pi
  and   X :: "(pi × pi) set"

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

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

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

lemma weakBisimE:
  fixes P :: pi
  and   Q :: pi

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

lemma weakBisimI:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ↝<weakBisim> Q"
  and     "Q ≈ P"

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

lemma eqvt[simp]:
  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_Early_Sim.eqvtI)
    qed

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

lemma eqvtI[eqvt]:
  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 strongBisimWeakBisim:
  fixes P :: pi
  and   Q :: pi

  assumes "P ∼ Q"

  shows "P ≈ Q"
proof -
  from ‹P ∼ Q› show ?thesis
  proof(coinduct rule: weakBisimWeakCoinduct)
    case(cSim P Q)
    from ‹P ∼ Q› have "P ↝[bisim] Q" by(rule bisimE)
    thus "P ↝<bisim> Q" by(rule strongSimWeakSim)
  next
    case(cSym P Q)
    thus ?case by(rule bisimE)
  qed
qed

lemma reflexive:
  fixes P :: pi

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

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

  shows "Q ≈ P"
using assms
by(auto dest: weakBisimE)

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

  assumes "P ≈ Q"
  and     "Q ≈ R"

  shows "P ≈ R"
proof -
  let ?X = "weakBisim O weakBisim"
  from assms have "(P, R) ∈ ?X" by blast
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim P R)
    from ‹(P, R) ∈ ?X› obtain Q where "P ≈ Q" and "Q ≈ R" by auto
    from ‹Q ≈ R› have "Q ↝<weakBisim> R" by(rule weakBisimE)
    moreover have "eqvt ?X" by auto
    moreover have "?X ⊆ ?X" by simp
    ultimately show "P ↝<(?X ∪ weakBisim)> R" using weakBisimE(1) ‹P ≈ Q›
      by(rule_tac Weak_Early_Sim.transitive) auto
  next
    case(cSym P R)
    thus ?case by(auto dest: symetric)
  qed
qed

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

  shows "P ≈ Q"
proof -
  let ?X = "weakBisim O X O weakBisim"
  let ?Y = "weakBisim O X O bisim"
  from  Eqvt eqvt have "eqvt ?X" by blast
  from Strong_Early_Bisim.eqvt Eqvt eqvt have "eqvt ?Y" by blast

  from ‹(P, Q) ∈ X› have "(P, Q) ∈ ?X" by(blast intro: Strong_Early_Bisim.reflexive reflexive)
  thus ?thesis
  proof(coinduct rule: weakBisimWeakCoinduct)
    case(cSim P Q)
    {
      fix P P' Q' Q
      assume "P ≈ P'" and "(P', Q') ∈ X" and "Q' ≈ Q"
      from ‹Q' ≈ Q› have "Q' ↝<weakBisim> Q" by(rule weakBisimE)
      moreover note ‹eqvt ?Y› ‹eqvt ?X›
      moreover have "?Y O weakBisim ⊆ ?X" by(blast dest: strongBisimWeakBisim transitive)
      moreover {
        fix P Q
        assume "(P, Q) ∈ ?Y"
        then obtain P' Q' where "P ≈ P'" and "(P', Q') ∈ X" and "Q' ∼ Q" by auto
        from ‹(P', Q') ∈ X› have "P' ↝<?Y> Q'" by(rule rSim)
        moreover from ‹Q' ∼ Q› have "Q' ↝[bisim] Q" by(rule bisimE)
        moreover note ‹eqvt ?Y›
        moreover have "?Y O bisim ⊆ ?Y" by(auto dest: Strong_Early_Bisim.transitive)
        ultimately have "P' ↝<?Y> Q" by(rule strongAppend)
        moreover note ‹P ≈ P'›
        moreover have "weakBisim O ?Y ⊆ ?Y" by(blast dest: transitive)
        ultimately have "P ↝<?Y> Q" using weakBisimE(1) eqvt ‹eqvt ?Y›
          by(rule_tac Weak_Early_Sim.transitive)
      }
      moreover from ‹(P', Q') ∈ X› have "(P', Q') ∈ ?Y" by(blast intro: reflexive Strong_Early_Bisim.reflexive)
      ultimately have "P' ↝<?X> Q" by(rule Weak_Early_Sim.transitive)
      moreover note ‹P ≈ P'›
      moreover have "weakBisim O ?X ⊆ ?X" by(blast dest: transitive)
      ultimately have "P ↝<?X> Q" using weakBisimE(1) eqvt ‹eqvt ?X›
        by(rule_tac Weak_Early_Sim.transitive)
    }
    with ‹(P, Q) ∈ ?X› show ?case by auto
  next
    case(cSym P Q)
    thus ?case 
      apply auto
      by(blast dest: bisimE rSym weakBisimE)
  qed
qed

lemma weakBisimUpto[case_names cSim cSym, consumes 1]:
  assumes p: "(P, Q) ∈ X"
  and Eqvt: "eqvt X"
  and rSim: "⋀R S. (R, S) ∈ X ⟹ R ↝<(weakBisim O (X ∪ weakBisim) O bisim)> S"
  and rSym: "⋀R S. (R, S) ∈ X ⟹ (S, R) ∈ X"

  shows "P ≈ Q"
proof -
  from p  have "(P, Q) ∈ X ∪ weakBisim" by simp
  thus ?thesis using Eqvt
    apply(coinduct rule: weakBisimWeakUpto)
    apply(auto dest: rSim rSym weakBisimE)
    apply(rule Weak_Early_Sim.monotonic)
    apply(blast dest: weakBisimE)
    apply(auto simp add: relcomp_unfold)
    by(metis reflexive Strong_Early_Bisim.reflexive transitive)
qed


lemma transitive_coinduct_weak[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) ∈ bisim O X O bisim"

  shows "P ≈ Q"
proof -
  let ?X = "bisim O X O bisim"
  from ‹(P, Q) ∈ X› have "(P, Q) ∈ ?X" by(blast intro: Strong_Early_Bisim.reflexive)
  thus ?thesis
  proof(coinduct rule: weakBisimWeakCoinduct)
    case(cSim P Q)
    {
      fix P P' Q' Q
      assume PBisimP': "P ∼ P'"
      assume P'SimQ': "P' ↝<?X> Q'"
      assume Q'SimQ: "Q' ↝[bisim] Q"
      
      have "P ↝<?X> Q"
      proof -
        have "P' ↝<?X> Q"
        proof -
          have "?X O bisim ⊆ ?X" by(blast intro: Strong_Early_Bisim.transitive)
          moreover from Strong_Early_Bisim.eqvt Eqvt have "eqvt ?X" by blast
          ultimately show ?thesis using P'SimQ' Q'SimQ 
            by(rule_tac strongAppend)
        qed
        moreover have "eqvt bisim" by(rule Strong_Early_Bisim.eqvt)
        moreover from Strong_Early_Bisim.eqvt Eqvt have "eqvt ?X" by blast
        moreover have "bisim O ?X ⊆ ?X" by(blast intro: Strong_Early_Bisim.transitive)
        moreover have "⋀P Q. P ∼ Q ⟹ P ↝<bisim> Q" by(blast dest: Strong_Early_Bisim.bisimE strongSimWeakSim)
        ultimately show ?thesis using PBisimP' by(rule Weak_Early_Sim.transitive)
      qed
    }
    thus ?case using ‹(P, Q) ∈ ?X› rSim by (blast dest: Strong_Early_Bisim.bisimE)
  next
    case(cSym P Q)
    {
      fix P P' Q' Q
      assume "P ∼ P'" and "(P', Q') ∈ X" and "Q' ∼ Q"
      from ‹(P', Q') ∈ X› have "(Q', P') ∈ ?X" by(rule rSym)
      with ‹P ∼ P'› ‹Q' ∼ Q› have "(Q, P) ∈ ?X" 
        apply auto
        apply(drule_tac Strong_Early_Bisim.bisimE(2))
        apply(drule Strong_Early_Bisim.transitive[where Q=P'])
        apply assumption
        apply(drule_tac Strong_Early_Bisim.bisimE(2))
        apply(drule Strong_Early_Bisim.transitive[where Q=Q'])
        apply assumption
        by auto
    }
    thus ?case using ‹(P, Q) ∈ ?X› by auto
  qed
qed

end