Theory Weak_Cong

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

definition weakCongruence :: "ccs => ccs => bool" ("_ ≅ _" [70, 70] 65)
where
  "P ≅ Q ≡ P \<leadsto><weakBisimulation> Q ∧ Q \<leadsto><weakBisimulation> P"

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

  assumes "P ≅ Q"

  shows "P \<leadsto><weakBisimulation> Q"
  and   "Q \<leadsto><weakBisimulation> P"
using assms
by(auto simp add: weakCongruence_def)

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

  assumes "P \<leadsto><weakBisimulation> Q"
  and     "Q \<leadsto><weakBisimulation> P"

  shows "P ≅ Q"
using assms
by(auto simp add: weakCongruence_def)

lemma weakCongISym[consumes 1, case_names cSym cSim]:
  fixes P :: ccs
  and   Q :: ccs

  assumes "Prop P Q"
  and     "!!P Q. Prop P Q ==> Prop Q P"
  and     "!!P Q. Prop P Q ==> (F P) \<leadsto><weakBisimulation> (F Q)"

  shows "F P ≅ F Q"
using assms
by(auto simp add: weakCongruence_def)

lemma weakCongISym2[consumes 1, case_names cSim]:
  fixes P :: ccs
  and   Q :: ccs

  assumes "P ≅ Q"
  and     "!!P Q. P ≅ Q ==> (F P) \<leadsto><weakBisimulation> (F Q)"

  shows "F P ≅ F Q"
using assms
by(auto simp add: weakCongruence_def)

lemma reflexive: 
  fixes P :: ccs

  shows "P ≅ P"
by(auto intro: weakCongruenceI Weak_Bisim.reflexive Weak_Cong_Sim.reflexive)

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

  assumes "P ≅ Q"

  shows "Q ≅ P"
using assms  
by(auto simp add: weakCongruence_def)

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

  assumes "P ≅ Q"
  and     "Q ≅ R"

  shows "P ≅ R"
proof -
  let ?Prop = "λP R. ∃Q. P ≅ Q ∧ Q ≅ R"
  from assms have "?Prop P R" by auto
  thus ?thesis
  proof(induct rule: weakCongISym)
    case(cSym P R)
    thus ?case by(auto dest: symmetric)
  next
    case(cSim P R)
    from `?Prop P R` obtain Q where "P ≅ Q" and "Q ≅ R"
      by auto
    from `P ≅ Q` have "P \<leadsto><weakBisimulation> Q" by(rule weakCongruenceE)
    moreover from `Q ≅ R` have "Q \<leadsto><weakBisimulation> R" by(rule weakCongruenceE)
    moreover from Weak_Bisim.transitive have "weakBisimulation O weakBisimulation ⊆ weakBisimulation"
      by auto
    ultimately show ?case using weakBisimulationE(1)
      by(rule Weak_Cong_Sim.transitive)
  qed
qed

lemma bisimWeakCongruence:
  fixes P :: ccs
  and   Q :: ccs
  
  assumes "P ∼ Q"

  shows "P ≅ Q"
using assms
proof(induct rule: weakCongISym)
  case(cSym P Q)
  thus ?case by(rule bisimE)
next
  case(cSim P Q)
  from `P ∼ Q` have "P \<leadsto>[bisim] Q" by(rule bisimE)
  hence "P \<leadsto>[weakBisimulation] Q" using bisimWeakBisimulation 
    by(rule_tac monotonic) auto
  thus ?case by(rule simWeakSim)
qed

lemma structCongWeakCongruence:
  fixes P :: ccs
  and   Q :: ccs

  assumes "P ≡⇩s Q"

  shows "P ≅ Q"
using assms
by(auto intro: bisimWeakCongruence bisimStructCong)

lemma weakCongruenceWeakBisimulation:
  fixes P :: ccs
  and   Q :: ccs
  
  assumes "P ≅ Q"

  shows "P ≈ Q"
proof -
  let ?X = "{(P, Q) | P Q. P ≅ Q}"
  from assms have "(P, Q) ∈ ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimulationCoinduct)
    case(cSim P Q)
    from `(P, Q) ∈ ?X` have "P ≅ Q" by auto
    hence "P \<leadsto><weakBisimulation> Q" by(rule Weak_Cong.weakCongruenceE)
    hence "P \<leadsto><(?X ∪ weakBisimulation)> Q" by(force intro: Weak_Cong_Sim.weakMonotonic)
    thus ?case by(rule weakCongSimWeakSim)
  next
    case(cSym P Q)
    from `(P, Q) ∈ ?X` show ?case by(blast dest: symmetric)
  qed
qed


end