Theory Weak_Early_Cong

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

definition weakCongruence :: "pi ⇒ pi ⇒ bool" (infixr ‹≃› 65)
where "P ≃ Q ≡ P ↝«weakBisim» Q ∧ Q ↝«weakBisim» P"

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

  assumes "Prop P Q"
  and     "⋀R S. Prop R S ⟹ Prop S R"
  and     "⋀R S. Prop R S ⟹ (F R) ↝«weakBisim» (F S)"

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

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

  assumes "P ≃ Q"
  and     "⋀R S. R ≃ S ⟹ (F R) ↝«weakBisim» (F S)"

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

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

  assumes "P ≃ Q"

  shows "P ↝«weakBisim» Q"
  and   "Q ↝«weakBisim» P"
using assms
by(auto simp add: weakCongruence_def)

lemma weakCongI:
  fixes P :: pi
  and   Q :: pi

  assumes "P ↝«weakBisim» Q"
  and     "Q ↝«weakBisim» P"

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

lemma eqvtI[eqvt]:
  fixes P :: pi
  and   Q :: pi
  and   p :: "name prm"

  assumes "P ≃ Q"

  shows "(p ∙ P) ≃ (p ∙ Q)"
using assms
by(auto simp add: weakCongruence_def intro: eqvtI)

lemma strongBisimWeakCong:
  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 Weak_Early_Step_Sim.strongSimWeakSim)
    moreover have "bisim ⊆ weakBisim"
      by(auto intro: strongBisimWeakBisim)
    ultimately show "P ↝«weakBisim» Q" by(rule Weak_Early_Step_Sim.monotonic)
  qed
  with assms show ?thesis
    by(blast intro: weakCongI dest: Strong_Early_Bisim.bisimE)
qed

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

  assumes "P ≃ Q"

  shows "P ≈ Q"
using assms
proof -
  let ?X = "{(P, Q) | P Q. P ≃ Q}"
  from assms have "(P, Q) ∈ ?X" by simp
  thus ?thesis 
  proof(induct rule: weakBisimCoinduct)
    case(cSim P Q) 
    {
      fix P Q
      assume "P ≃ Q"
      hence "P ↝«weakBisim» Q" by(simp add: weakCongruence_def)
      hence "P ↝«(?X ∪ weakBisim)» Q" by(rule_tac Weak_Early_Step_Sim.monotonic) auto
      hence "P ↝<(?X ∪ weakBisim)> Q" by(rule weakSimWeakEqSim)
    }
    with ‹(P, Q) ∈ ?X› show ?case by auto
  next
    case(cSym P Q)
    thus ?case by(auto simp add: weakCongruence_def)
  qed
qed

lemma reflexive:
  fixes P :: pi
  
  shows "P ≃ P"
proof -
  from Weak_Early_Bisim.reflexive have "⋀P. P ↝«weakBisim» P"
    by(blast intro: Weak_Early_Step_Sim.reflexive)
  thus ?thesis
    by(force simp add: substClosed_def weakCongruence_def)
qed

lemma symetric:
  fixes P :: pi
  and   Q :: pi
  
  assumes "P ≃ Q"
  
  shows "Q ≃ P"
using assms
by(force simp add: substClosed_def weakCongruence_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_Early_Bisim.eqvt Weak_Early_Bisim.weakBisimE Weak_Early_Bisim.transitive
    by(blast intro: Weak_Early_Step_Sim.transitive)
  from assms show ?thesis
    apply(simp add: weakCongruence_def) using assms
    by(blast intro: Goal dest: congruenceWeakBisim symetric)
qed

end