(* 
   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