Theory Weak_Bisim

(* 
   Title: The Calculus of Communicating Systems   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Bisim
  imports Weak_Sim Strong_Bisim_SC Struct_Cong
begin

lemma weakMonoCoinduct: "x y xa xb P Q.
                         x  y 
                         (Q ^<{(xb, xa). x xb xa}> P) 
                        (Q ^<{(xb, xa). y xb xa}> P)"
apply auto
apply(rule weakMonotonic)
by(auto dest: le_funE)

coinductive_set weakBisimulation :: "(ccs × ccs) set"
where
  "P ^<weakBisimulation> Q; (Q, P)  weakBisimulation  (P, Q)  weakBisimulation"
monos weakMonoCoinduct

abbreviation
  weakBisimJudge ("_  _" [70, 70] 65) where "P  Q  (P, Q)  weakBisimulation"

lemma weakBisimulationCoinductAux[consumes 1]:
  fixes P :: "ccs"
  and   Q :: "ccs"
  and   X :: "(ccs × ccs) set"

  assumes "(P, Q)  X"
  and     "P Q. (P, Q)  X  P ^<(X  weakBisimulation)> Q  (Q, P)  X"

  shows "P  Q"
proof -
  have "X  weakBisimulation = {(P, Q). (P, Q)  X  (P, Q)  weakBisimulation}" by auto
  with assms show ?thesis
    by coinduct simp
qed

lemma weakBisimulationCoinduct[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 ^<(X  weakBisimulation)> S"
  and     "R S. (R, S)  X  (S, R)  X"

  shows "P  Q"
proof -
  have "X  weakBisimulation = {(P, Q). (P, Q)  X  (P, Q)  weakBisimulation}" by auto
  with assms show ?thesis
    by coinduct simp
qed

lemma weakBisimWeakCoinductAux[consumes 1]:
  fixes P :: "ccs"
  and   Q :: "ccs"
  and   X :: "(ccs × ccs) set"

  assumes "(P, Q)  X"
  and     "P Q. (P, Q)  X  P ^<X> Q  (Q, P)  X" 

  shows "P  Q"
using assms
by(coinduct rule: weakBisimulationCoinductAux) (blast intro: weakMonotonic)

lemma weakBisimWeakCoinduct[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 ^<X> Q"
  and     "P Q. (P, Q)  X  (Q, P)  X"

  shows "P  Q"
proof -
  have "X  weakBisim = {(P, Q). (P, Q)  X  (P, Q)  weakBisim}" by auto
  with assms show ?thesis
  by(coinduct rule: weakBisimulationCoinduct) (blast intro: weakMonotonic)+
qed

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

  assumes "P  Q"

  shows "P ^<weakBisimulation> Q"
  and   "Q  P"
using assms
by(auto simp add: intro: weakBisimulation.cases)

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

  assumes "P ^<weakBisimulation> Q"
  and     "Q  P"

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

lemma reflexive: 
  fixes P :: ccs

  shows "P  P"
proof -
  have "(P, P)  Id" by blast
  thus ?thesis
    by(coinduct rule: weakBisimulationCoinduct) (auto intro: Weak_Sim.reflexive)
qed

lemma symmetric: 
  fixes P :: ccs
  and   Q :: ccs

  assumes "P  Q"

  shows "Q  P"
using assms  
by(rule weakBisimulationE)

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)  weakBisimulation O weakBisimulation" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimulationCoinduct)
    case(cSim P R)
    from (P, R)  weakBisimulation O weakBisimulation
    obtain Q where "P  Q" and "Q  R" by auto
    note P  Q
    moreover from Q  R have "Q ^<weakBisimulation> R" by(rule weakBisimulationE)
    moreover have "weakBisimulation O weakBisimulation  (weakBisimulation O weakBisimulation)  weakBisimulation"
      by auto
    moreover note weakBisimulationE(1)
    ultimately show ?case by(rule Weak_Sim.transitive)
  next
    case(cSym P R)
    thus ?case by(blast dest: symmetric)
  qed
qed

lemma bisimWeakBisimulation:
  fixes P :: ccs
  and   Q :: ccs
  
  assumes "P  Q"

  shows "P  Q"
using assms
by(coinduct rule: weakBisimWeakCoinduct[where X=bisim])
  (auto dest: bisimE simWeakSim)

lemma structCongWeakBisimulation:
  fixes P :: ccs
  and   Q :: ccs

  assumes "P s Q"

  shows "P  Q"
using assms

by(auto intro: bisimWeakBisimulation bisimStructCong)

lemma strongAppend:
  fixes P     :: ccs
  and   Q     :: ccs
  and   R     :: ccs
  and   Rel   :: "(ccs × ccs) set"
  and   Rel'  :: "(ccs × ccs) set"
  and   Rel'' :: "(ccs × ccs) set"

  assumes PSimQ: "P ^<Rel> Q"
  and     QSimR: "Q ↝[Rel'] R"
  and     Trans: "Rel O Rel'  Rel''"

  shows "P ^<Rel''> R"
using assms
by(simp add: weakSimulation_def simulation_def) blast

lemma weakBisimWeakUpto[case_names cSim cSym, consumes 1]:
  assumes p: "(P, Q)  X"
  and rSim: "P Q. (P, Q)  X  P ^<(weakBisimulation O X O bisim)> Q"
  and rSym: " P Q. (P, Q)  X  (Q, P)  X"

  shows "P  Q"
proof -
  let ?X = "weakBisimulation O X O weakBisimulation"
  let ?Y = "weakBisimulation O X O bisim"
  from (P, Q)  X have "(P, Q)  ?X" by(blast intro: Strong_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 (P', Q')  X have "(P', Q')  ?Y" by(blast intro: reflexive Strong_Bisim.reflexive)
      moreover from Q'  Q have "Q' ^<weakBisimulation> Q" by(rule weakBisimulationE)
      moreover have "?Y O weakBisimulation  ?X" by(blast dest: bisimWeakBisimulation 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 have "?Y O bisim  ?Y" by(auto dest: Strong_Bisim.transitive)
        ultimately have "P' ^<?Y> Q" by(rule strongAppend)
        moreover note P  P'
        moreover have "weakBisimulation O ?Y  ?Y" by(blast dest: transitive)
        ultimately have "P ^<?Y> Q" using weakBisimulationE(1)
          by(rule_tac Weak_Sim.transitive)
      }
      ultimately have "P' ^<?X> Q" by(rule Weak_Sim.transitive)
      moreover note P  P'
      moreover have "weakBisimulation O ?X  ?X" by(blast dest: transitive)
      ultimately have "P ^<?X> Q" using weakBisimulationE(1)
        by(rule_tac Weak_Sim.transitive)
    }
    with (P, Q)  ?X show ?case by auto
  next
    case(cSym P Q)
    thus ?case 
      apply auto
      by(blast dest: bisimE rSym weakBisimulationE)
  qed
qed

lemma weakBisimUpto[case_names cSim cSym, consumes 1]:
  assumes p: "(P, Q)  X"
  and rSim: "R S. (R, S)  X  R ^<(weakBisimulation O (X  weakBisimulation) O bisim)> S"
  and rSym: "R S. (R, S)  X  (S, R)  X"

  shows "P  Q"
proof -
  from p have "(P, Q)  X  weakBisimulation" by simp
  thus ?thesis
    apply(coinduct rule: weakBisimWeakUpto)
    apply(auto dest: rSim rSym weakBisimulationE)
    apply(rule weakMonotonic)
    apply(blast dest: weakBisimulationE)
    apply(auto simp add: relcomp_unfold)
    by(metis reflexive Strong_Bisim.reflexive transitive)
qed

end