Theory Weak_Congruence

(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Congruence
  imports Weak_Cong_Struct_Cong Bisim_Subst
begin

context env begin

definition weakCongruence :: "('a, 'b, 'c) psi ⇒ ('a, 'b, 'c) psi ⇒ bool" ("_ ≐⇩c _" [70, 70] 65)
where 
  "P ≐⇩c Q ≡ ∀Ψ σ. wellFormedSubst σ ⟶ Ψ ⊳ P[<σ>] ≐ Q[<σ>]"

lemma weakCongE:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   σ :: "(name list × 'a list) list"

  assumes "P ≐⇩c Q"
  "wellFormedSubst σ"

  shows "Ψ ⊳ P[<σ>] ≐ Q[<σ>]"
using assms
by(auto simp add: weakCongruence_def)

lemma weakCongI[case_names cWeakPsiCong]:
  fixes P   :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"

  assumes "⋀Ψ σ. wellFormedSubst σ ⟹ Ψ ⊳ P[<σ>] ≐ Q[<σ>]"

  shows "P ≐⇩c Q"
using assms
by(auto simp add: weakCongruence_def)

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

  shows "(p ∙ P) ≐⇩c (p ∙ Q)"
proof(induct rule: weakCongI)
  case(cWeakPsiCong Ψ σ)
  note ‹P ≐⇩c Q›
  moreover from ‹wellFormedSubst σ› have "wellFormedSubst (rev p ∙ σ)" by simp
  ultimately have "((rev p) ∙ Ψ) ⊳ P[<(rev p ∙ σ)>] ≐  Q[<(rev p ∙ σ)>]"
    by(rule weakCongE)
  thus ?case by(drule_tac p=p in weakPsiCongClosed) (simp add: eqvts)
qed

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

  shows "P ≐⇩c P"
by(auto intro: weakCongI weakPsiCongReflexive)

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

  assumes "P ≐⇩c Q"

  shows "Q ≐⇩c P"
using assms
by(auto simp add: weakCongruence_def weakPsiCongSym)

lemma weakCongTransitive:
  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"
using assms
by(auto intro: weakCongI weakPsiCongTransitive dest: weakCongE)

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

  assumes "P ≐⇩c Q"

  shows "Ψ ⊳ P ≈ Q"
using assms
apply(drule_tac σ="[]" in weakCongE)
by(auto dest: weakPsiCongE)

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

  assumes "P ≐⇩c Q"

  shows "Ψ ⊳ P ≐ Q"
using assms
by(drule_tac weakCongE[where Ψ=Ψ and σ="[]"]) auto

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

  assumes "P ∼⇩s Q"

  shows "P ≐⇩c Q"
proof(induct rule: weakCongI)
  case(cWeakPsiCong Ψ σ)
  from assms ‹wellFormedSubst σ› have "P[<σ>] ∼ Q[<σ>]"
    by(rule closeSubstE)
  hence "Ψ ⊳ P[<σ>] ∼ Q[<σ>]" by(metis bisimE(3) statEqBisim Identity Commutativity)
  thus ?case by(rule strongBisimWeakPsiCong)
qed

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

  assumes "P ≡⇩s Q"

  shows "P ≐⇩c Q"
using assms
by(metis strongBisimWeakCong structCongBisimSubst)

lemma weakCongUnfold:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   σ :: "(name list × 'a list) list"

  assumes "P ≐⇩c Q"
  and     "wellFormedSubst σ"

  shows "P[<σ>] ≐⇩c Q[<σ>]"
proof(induct rule: weakCongI)
  case(cWeakPsiCong Ψ σ')
  with ‹wellFormedSubst σ› ‹wellFormedSubst σ'› have "wellFormedSubst(σ@σ')" by simp
  with ‹P ≐⇩c Q› have "Ψ ⊳ P[<(σ@σ')>] ≐ Q[<(σ@σ')>]"
    by(rule weakCongE)
  thus "Ψ ⊳ P[<σ>][<σ'>] ≐ Q[<σ>][<σ'>]"
    by simp
qed

lemma weakCongOutputPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   M :: 'a
  and   N :: 'a
  
  assumes "P ≐⇩c Q"

  shows "M⟨N⟩.P ≐⇩c M⟨N⟩.Q"
using assms
by(fastforce intro: weakCongI weakCongE weakPsiCongOutputPres)

lemma weakCongInputPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a

  assumes "P ≐⇩c Q"
  and     "distinct xvec"

  shows "M⦇λ*xvec N⦈.P ≐⇩c M⦇λ*xvec N⦈.Q"
proof(induct rule: weakCongI)
  case(cWeakPsiCong Ψ σ)
  obtain p where "(p ∙ xvec) ♯* σ"
             and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Q" and "(p ∙ xvec) ♯* Ψ" and "(p ∙ xvec) ♯* N"
             and S: "set p ⊆ set xvec × set (p ∙ xvec)"
      by(rule_tac c="(σ, P, Q, Ψ, N)" in name_list_avoiding) auto
    
  from ‹P ≐⇩c Q› have "(p ∙ P) ≐⇩c (p ∙ Q)"
    by(rule weakCongClosed)
  {
    fix Tvec :: "'a list"
    from ‹(p ∙ P) ≐⇩c (p ∙ Q)› ‹wellFormedSubst σ› have "(p ∙ P)[<σ>] ≐⇩c (p ∙ Q)[<σ>]"
      by(rule weakCongUnfold)
    moreover assume "length xvec = length Tvec" and "distinct xvec"
    ultimately have "Ψ ⊳ ((p ∙ P)[<σ>])[(p ∙ xvec)::=Tvec] ≐ ((p ∙ Q)[<σ>])[(p ∙ xvec)::=Tvec]" 
      by(drule_tac weakCongE[where σ="[((p ∙ xvec), Tvec)]"]) auto
    hence "Ψ ⊳ ((p ∙ P)[<σ>])[(p ∙ xvec)::=Tvec] ≈ ((p ∙ Q)[<σ>])[(p ∙ xvec)::=Tvec]"
      by(rule weakPsiCongE)
  }

  with ‹(p ∙ xvec) ♯* σ› ‹distinct xvec›
  have "Ψ ⊳ (M⦇λ*(p ∙ xvec) (p ∙ N)⦈.(p ∙ P))[<σ>] ≐ (M⦇λ*(p ∙ xvec) (p ∙ N)⦈.(p ∙ Q))[<σ>]"
    by(force intro: weakPsiCongInputPres)
  moreover from ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* P› S have "M⦇λ*(p ∙ xvec) (p ∙ N)⦈.(p ∙ P) = M⦇λ*xvec N⦈.P" 
    apply(simp add: psi.inject) by(rule inputChainAlpha[symmetric]) auto
  moreover from ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* Q› S have "M⦇λ*(p ∙ xvec) (p ∙ N)⦈.(p ∙ Q) = M⦇λ*xvec N⦈.Q"
    apply(simp add: psi.inject) by(rule inputChainAlpha[symmetric]) auto
  ultimately show ?case by force
qed

lemma weakCongCasePresAux:
  fixes Ψ   :: 'b
  and   CsP :: "('c × ('a, 'b, 'c) psi) list"
  and   CsQ :: "('c × ('a, 'b, 'c) psi) list"
  
  assumes C1: "⋀φ P. (φ, P) mem CsP ⟹ ∃Q. (φ, Q) mem CsQ ∧ guarded Q ∧ P ≐⇩c Q"
  and     C2: "⋀φ Q. (φ, Q) mem CsQ ⟹ ∃P. (φ, P) mem CsP ∧ guarded P ∧ P ≐⇩c Q"

  shows "Cases CsP ≐⇩c Cases CsQ"
proof -
  {
    fix Ψ :: 'b
    fix σ :: "(name list × 'a list) list"

    assume "wellFormedSubst σ"
    have "Ψ ⊳ Cases(caseListSeqSubst CsP σ) ≐ Cases(caseListSeqSubst CsQ σ)"
    proof(rule weakPsiCongCasePres)
      fix φ P
      assume "(φ, P) mem (caseListSeqSubst CsP σ)"
      then obtain φ' P' where "(φ', P') mem CsP" and "φ = substCond.seqSubst φ' σ" and PeqP': "P = (P'[<σ>])"
        by(induct CsP) force+
      from ‹(φ', P') mem CsP› obtain Q' where "(φ', Q') mem CsQ" and "guarded Q'" and "P' ≐⇩c Q'" by(blast dest: C1)
      from ‹(φ', Q') mem CsQ› ‹φ = substCond.seqSubst φ' σ› obtain Q where "(φ, Q) mem (caseListSeqSubst CsQ σ)" and "Q = Q'[<σ>]"
        by(induct CsQ) auto
      with PeqP' ‹guarded Q'› ‹P' ≐⇩c Q'› ‹wellFormedSubst σ› show "∃Q. (φ, Q) mem (caseListSeqSubst CsQ σ) ∧ guarded Q ∧ (∀Ψ. Ψ ⊳ P ≐ Q)"
        by(blast dest: weakCongE guardedSeqSubst)
    next
      fix φ Q
      assume "(φ, Q) mem (caseListSeqSubst CsQ σ)"
      then obtain φ' Q' where "(φ', Q') mem CsQ" and "φ = substCond.seqSubst φ' σ" and QeqQ': "Q = Q'[<σ>]"
        by(induct CsQ) force+
      from ‹(φ', Q') mem CsQ› obtain P' where "(φ', P') mem CsP" and "guarded P'" and "P' ≐⇩c Q'" by(blast dest: C2)
      from ‹(φ', P') mem CsP› ‹φ = substCond.seqSubst φ' σ› obtain P where "(φ, P) mem (caseListSeqSubst CsP σ)" and "P = P'[<σ>]"
        by(induct CsP) auto
      with QeqQ' ‹guarded P'› ‹P' ≐⇩c Q'› ‹wellFormedSubst σ›
      show "∃P. (φ, P) mem (caseListSeqSubst CsP σ) ∧ guarded P ∧ (∀Ψ. Ψ ⊳ P ≐ Q)"
        by(blast dest: weakCongE guardedSeqSubst)
    qed
  }
  thus ?thesis
    by(rule_tac weakCongI) auto
qed

lemma weakCongParPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"
  
  assumes "P ≐⇩c Q"

  shows "P ∥ R ≐⇩c Q ∥ R"
using assms
by(fastforce intro: weakCongI weakCongE weakPsiCongParPres)

lemma weakCongResPres:
  fixes P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   x :: name

  assumes "P ≐⇩c Q"

  shows "⦇νx⦈P ≐⇩c ⦇νx⦈Q"
proof(induct rule: weakCongI)
  case(cWeakPsiCong Ψ σ)
  obtain y::name where "y ♯ (Ψ::'b)" and "y ♯ P" and "y ♯ Q" and "y ♯ σ"
    by(generate_fresh "name") (auto simp add: fresh_prod)

  from ‹P ≐⇩c Q› have "([(x, y)] ∙ P) ≐⇩c ([(x, y)] ∙ Q)" by(rule weakCongClosed)
  hence "Ψ ⊳ ([(x, y)] ∙ P)[<σ>] ≐ ([(x, y)] ∙ Q)[<σ>]" using ‹wellFormedSubst σ›
    by(rule weakCongE)
  hence "Ψ ⊳ ⦇νy⦈(([(x, y)] ∙ P)[<σ>]) ≐ ⦇νy⦈(([(x, y)] ∙ Q)[<σ>])" using ‹y ♯ Ψ›
    by(rule weakPsiCongResPres)
  with ‹y ♯ P› ‹y ♯ Q›  ‹y ♯ σ›
  show "Ψ ⊳ (⦇νx⦈P)[<σ>] ≐ (⦇νx⦈Q)[<σ>]"
    by(simp add: alphaRes)
qed

lemma weakCongBangPres:
  fixes P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
 
  assumes "P ≐⇩c Q"
  and     "guarded P"
  and     "guarded Q"

  shows "!P ≐⇩c !Q"
using assms
by(fastforce intro: weakCongI weakCongE weakPsiCongBangPres  guardedSeqSubst)

end

end