Theory Weak_Psi_Congruence

(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Psi_Congruence
  imports Weak_Cong_Simulation Weak_Bisimulation
begin

context env begin

definition weakPsiCongruence :: "'b ⇒ ('a, 'b, 'c) psi ⇒ ('a, 'b, 'c) psi ⇒ bool" (‹_ ⊳ _ ≐ _› [70, 70, 70] 65)
where 
  "Ψ ⊳ P ≐ Q ≡ Ψ ⊳ P ≈ Q ∧ Ψ ⊳ P ↝«weakBisim» Q ∧ Ψ ⊳ Q ↝«weakBisim» P"

abbreviation
  weakPsiCongNilJudge (‹_ ≐ _› [70, 70] 65) where "P ≐ Q ≡ 𝟭 ⊳ P ≐ Q"

lemma weakPsiCongSym:
  fixes Ψ  :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   Q  :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ≐ Q"

  shows "Ψ ⊳ Q ≐ P"
using assms
by(auto simp add: weakPsiCongruence_def weakBisimE)

lemma weakPsiCongE:
  fixes Ψ   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"
  and   Ψ'  :: 'b


  assumes "Ψ ⊳ P ≐ Q"

  shows "Ψ ⊳ P ≈ Q"
  and   "Ψ ⊳ P ↝«weakBisim» Q"
  and   "Ψ ⊳ Q ↝«weakBisim» P"
using assms
by(auto simp add: weakPsiCongruence_def)

lemma weakPsiCongI[case_names cWeakBisim cSimLeft cSimRight]:
  fixes Ψ  :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"
  and   Ψ' :: 'b

  assumes "Ψ ⊳ P ≈ Q"
  and     "Ψ ⊳ P ↝«weakBisim» Q"
  and     "Ψ ⊳ Q ↝«weakBisim» P"

  shows "Ψ ⊳ P ≐ Q"
using assms
by(auto simp add: weakPsiCongruence_def)

lemma weakPsiCongSymI[consumes 1, case_names cSym cWeakBisim cSim]:
  fixes Ψ  :: 'b
  and   P   :: "'d::fs_name"
  and   Q   :: 'd
  and   Ψ' :: 'b

  assumes "Prop P Q"
  and     "⋀P Q. Prop P Q ⟹ Prop Q P"

  and     "⋀P Q. Prop P Q ⟹ Ψ ⊳ (C P) ≈ (C Q)"

  and     "⋀P Q. Prop P Q ⟹ Ψ ⊳ (C P) ↝«weakBisim» (C Q)"

  shows "Ψ ⊳ (C P) ≐ (C Q)"
using assms
by(rule_tac weakPsiCongI) auto

lemma weakPsiCongSym2[consumes 1, case_names cWeakBisim cSim]:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b

  assumes "Ψ ⊳ P ≐ Q"

  and     "⋀P Q. Ψ ⊳ P ≐ Q ⟹ Ψ ⊳ (C P) ≈ (C Q)"

  and     "⋀P Q. Ψ ⊳ P ≐ Q ⟹ Ψ ⊳ (C P) ↝«weakBisim» (C Q)"

  shows "Ψ ⊳ (C P) ≐ (C Q)"
using assms
apply(rule_tac weakPsiCongSymI[where C=C])
apply assumption
by(auto simp add: weakPsiCongruence_def dest: weakBisimE)

lemma statEqWeakCong:
  fixes Ψ  :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   Q  :: "('a, 'b, 'c) psi"
  and   Ψ' :: 'b
  
  assumes "Ψ ⊳ P ≐ Q"
  and     "Ψ ≃ Ψ'"

  shows "Ψ' ⊳ P ≐ Q"
proof -
  let ?Prop = "λP Q. Ψ ⊳ P ≐ Q ∧ Ψ ≃ Ψ'"
  from assms have "?Prop P Q" by auto
  thus ?thesis
  proof(induct rule: weakPsiCongSymI)
    case(cSym P Q)
    thus ?case by(blast dest: weakPsiCongSym)
  next
    case(cSim P Q)
    from ‹Ψ ⊳ P ≐ Q ∧ Ψ ≃ Ψ'› have "Ψ ⊳ P ≐ Q" and "Ψ ≃ Ψ'" by simp+
    from ‹Ψ ⊳ P ≐ Q› have "Ψ ⊳ P ↝«weakBisim» Q" by(rule weakPsiCongE)
    with ‹Ψ ≃ Ψ'› show ?case using statEqWeakBisim
      by(rule_tac weakCongSimStatEq) auto
  next
    case(cWeakBisim P Q)
    from ‹Ψ ⊳ P ≐ Q ∧ Ψ ≃ Ψ'›
    have "Ψ ⊳ P ≈ Q" and "Ψ ≃ Ψ'" by(auto dest: weakPsiCongE)
    thus ?case by(rule statEqWeakBisim)
  qed
qed

lemma weakPsiCongReflexive:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"


  shows "Ψ ⊳ P ≐ P"
by(fastforce intro: weakPsiCongI weakCongSimReflexive weakBisimReflexive)

lemma weakPsiCongClosed:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   p :: "name prm"
  
  assumes "Ψ ⊳ P ≐ Q"

  shows "(p ∙ Ψ) ⊳  (p ∙ P) ≐ (p ∙ Q)"
using assms
proof(induct rule: weakPsiCongSymI)
  case(cSym P Q)
  thus ?case by(rule weakPsiCongSym)
next
  case(cSim P Q)
  from ‹Ψ ⊳ P ≐ Q› have "Ψ ⊳ P ↝«weakBisim» Q" by(rule weakPsiCongE)
  thus ?case by(drule_tac p=p in weakCongSimClosed(1)[OF weakBisimEqvt]) (simp add: eqvts)
next
  case(cWeakBisim P Q)
  from ‹Ψ ⊳ P ≐ Q› have "Ψ ⊳ P ≈ Q" by(rule weakPsiCongE)
  thus ?case by(rule weakBisimClosed)
qed

lemma weakPsiCongTransitive:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ≐ Q"
  and     "Ψ ⊳ Q ≐ R"

  shows "Ψ ⊳ P ≐ R"
proof -
  from assms have "Ψ ⊳ P ≐ Q ∧ Ψ ⊳ Q ≐ R"  by auto
  thus ?thesis
  proof(induct rule: weakPsiCongSymI)
    case(cSym P R)
    thus ?case by(auto dest: weakPsiCongSym)
  next
    case(cSim P R)
    hence "Ψ ⊳ P ≐ Q" and  "Ψ ⊳ Q ≐ R"  by auto
    moreover from ‹Ψ ⊳ P ≐ Q› have "Ψ ⊳ P ≈ Q" by(metis weakBisimE weakPsiCongE)
    moreover from ‹Ψ ⊳ P ≐ Q› have "Ψ ⊳ P ↝«weakBisim» Q" by(rule weakPsiCongE)
    moreover from ‹Ψ ⊳ Q ≐ R› have "Ψ ⊳ Q ↝«weakBisim» R" by(rule weakPsiCongE)
    moreover have "{(Ψ, P, R) | Ψ P R. ∃Q. Ψ ⊳ P ≈ Q ∧ Ψ ⊳ Q ≈ R} ⊆ weakBisim"
      by(auto dest: weakBisimTransitive)
    ultimately show ?case using weakBisimE(2) by(rule_tac weakCongSimTransitive)
  next
    case(cWeakBisim P R)
    thus ?case by(auto dest: weakBisimTransitive weakPsiCongE)
  qed
qed

lemma strongBisimWeakPsiCong:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ∼ Q"

  shows "Ψ ⊳ P ≐ Q"
using assms
proof(induct rule: weakPsiCongSymI)
  case(cSym P Q)
  from ‹Ψ ⊳ P ∼ Q› show ?case by(rule bisimE)
next
  case(cSim P Q)
  from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊳ P ↝[bisim] Q" by(rule bisimE)
  thus "Ψ ⊳ P ↝«weakBisim» Q" using strongBisimWeakBisim
    by(rule_tac strongSimWeakCongSim) auto
next
  case(cWeakBisim P Q)
  thus ?case by(rule strongBisimWeakBisim)
qed

lemma structCongWeakPsiCong:
  fixes P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "P ≡⇩s Q"

  shows "P ≐ Q"
using assms
by(metis structCongBisim strongBisimWeakPsiCong)

end

end