Theory Weak_Late_Cong

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

definition congruence :: "(pi × pi) set" where 
  "congruence ≡ {(P, Q) |P Q. P ↝<weakBisim> Q ∧ Q ↝<weakBisim> P}"
abbreviation congruenceJudge (infixr ‹≃› 65) where "P ≃ Q ≡ (P, Q) ∈ congruence"

lemma unfoldE:
  fixes P :: pi
  and   Q :: pi
  and   s :: "(name × name) list"

  assumes "P ≃ Q"

  shows "P ↝<weakBisim> Q"
  and   "Q ↝<weakBisim> P"
proof -
  from assms show "P ↝<weakBisim> Q" by(force simp add: congruence_def)
next
  from assms show "Q ↝<weakBisim> P" by(force simp add: congruence_def)
qed

lemma unfoldI:
  fixes P :: pi
  and   Q :: pi

  assumes "P ↝<weakBisim> Q"
  and     "Q ↝<weakBisim> P"

  shows "P ≃ Q"
using assms by(force simp add: congruence_def)


lemma eqvt:
  shows "eqvt congruence"
proof -
  have "⋀P Q (perm::name prm). P ↝<weakBisim> Q ⟹ (perm ∙ P) ↝<weakBisim> (perm ∙ Q)"
  proof -
    fix P Q perm
    assume "P ↝<weakBisim> Q"
    thus "((perm::name prm) ∙ P) ↝<weakBisim> (perm ∙ Q)"
      apply -
      by(blast intro: Weak_Late_Step_Sim.eqvtI Weak_Late_Bisim.eqvt)
  qed
  thus ?thesis
    by(simp add: congruence_def eqvt_def)
qed

lemma eqvtI:
  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 strongBisimWeakEq:
  fixes P :: pi
  and   Q :: pi

  assumes "P ∼ Q"

  shows "P ≃ Q"
proof -
  have "⋀P Q. P ↝[bisim] Q ⟹ P ↝<weakBisim> Q"
  proof -
    fix P Q
    assume "P ↝[bisim] Q"
    hence "P ↝<bisim> Q" by(rule strongSimWeakEqSim)
    moreover have "bisim ⊆ weakBisim"
      by(auto intro: strongBisimWeakBisim)
    ultimately show "P ↝<weakBisim> Q" by(rule Weak_Late_Step_Sim.monotonic)
  qed
  with assms show ?thesis
    by(blast intro: unfoldI dest: Strong_Late_Bisim.bisimE Strong_Late_Bisim.symmetric)
qed

lemma congruenceWeakBisim:
  fixes P :: pi
  and   Q :: pi

  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: weakBisimCoinduct)
    case(cSim P Q)
    {
      fix P Q
      assume "P ≃ Q"
      hence "P ↝<weakBisim> Q" by(simp add: congruence_def)
      hence "P ↝<(?X ∪ weakBisim)> Q" by(rule_tac Weak_Late_Step_Sim.monotonic) auto
      hence "P ↝⇧^<(?X ∪ weakBisim)> Q" by(rule Weak_Late_Step_Sim.weakSimWeakEqSim)
    }
    with ‹(P, Q) ∈ ?X› show ?case by auto
  next
    case(cSym P Q)
    thus ?case by(auto simp add: congruence_def)
  qed 
qed

lemma congruenceSubsetWeakBisim:
  shows "congruence ⊆ weakBisim"
by(auto intro: congruenceWeakBisim)

lemma reflexive:
  fixes P :: pi
  
  shows "P ≃ P"
proof -
  from Weak_Late_Bisim.reflexive have "⋀P. P ↝<weakBisim> P"
    by(blast intro: Weak_Late_Step_Sim.reflexive)
  thus ?thesis
    by(force simp add: substClosed_def congruence_def)
qed

lemma symetric:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ≃ Q"
  
  shows "Q ≃ P"
using assms
by(force simp add: substClosed_def congruence_def)

lemma transitive:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi
  
  assumes "P ≃ Q"
  and     "Q ≃ R"
  
  shows "P ≃ R"
proof -
  have Goal: "⋀P Q R. ⟦P ↝<weakBisim> Q; Q ↝<weakBisim> R; P ≈ Q⟧ ⟹ P ↝<weakBisim> R"
    using Weak_Late_Bisim.eqvt Weak_Late_Bisim.unfoldE Weak_Late_Bisim.transitive
    by(blast intro: Weak_Late_Step_Sim.transitive)
  from assms show ?thesis
    apply(simp add: congruence_def) using assms
    by(blast intro: Goal dest: congruenceWeakBisim symetric)
qed

end