Theory Weak_Bisim_Subst

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

context env begin

abbreviation
  weakBisimSubstJudge ("_ ⊳ _ ≈⇩s _" [70, 70, 70] 65) where "Ψ ⊳ P ≈⇩s Q ≡ (Ψ, P, Q) ∈ closeSubst weakBisim"
abbreviation
  weakBisimSubstNilJudge ("_ ≈⇩s _" [70, 70] 65) where "P ≈⇩s Q ≡ 𝟭 ⊳ P ≈⇩s Q"

lemmas weakBisimSubstClosed[eqvt] = closeSubstClosed[OF weakBisimEqvt]
lemmas weakBisimEqvt[simp] = closeSubstEqvt[OF weakBisimEqvt]

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

  assumes "Ψ ⊳ P ∼⇩s Q"

  shows "Ψ ⊳ P ≈⇩s Q"
using assms
by(metis closeSubstI closeSubstE strongBisimWeakBisim)

lemma weakBisimSubstOutputPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   M :: 'a
  and   N :: 'a
  
  assumes "Ψ ⊳ P ≈⇩s Q"

  shows "Ψ ⊳ M⟨N⟩.P ≈⇩s M⟨N⟩.Q"
using assms
by(fastforce intro: closeSubstI closeSubstE weakBisimOutputPres)

lemma bisimSubstInputPres:
  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 ≈⇩s Q"
  and     "xvec ♯* Ψ"
  and     "distinct xvec"

  shows "Ψ ⊳ M⦇λ*xvec N⦈.P ≈⇩s M⦇λ*xvec N⦈.Q"
proof(rule_tac closeSubstI)
  fix σ :: "(name list × 'a list) list"
  assume "wellFormedSubst σ"
  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 ≈⇩s Q› have "(p ∙ Ψ) ⊳ (p ∙ P) ≈⇩s (p ∙ Q)"
    by(rule weakBisimSubstClosed)
  with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S have "Ψ ⊳ (p ∙ P) ≈⇩s (p ∙ Q)"
    by simp

  {
    fix Tvec' :: "'a list"
    assume "length (p ∙ xvec) = length Tvec'"
    with ‹wellFormedSubst σ› ‹distinct xvec› have "wellFormedSubst (σ @ [(p ∙ xvec,Tvec')])"
      by simp
    with ‹Ψ ⊳ (p ∙ P) ≈⇩s (p ∙ Q)› have "Ψ ⊳ (p ∙ P)[<(σ @ [(p ∙ xvec,Tvec')])>] ≈ (p ∙ Q)[<(σ @ [(p ∙ xvec,Tvec')])>]"
      by (rule closeSubstE)
    then have "Ψ ⊳ ((p ∙ P)[<σ>])[(p ∙ xvec)::=Tvec'] ≈ ((p ∙ Q)[<σ>])[(p ∙ xvec)::=Tvec']"
      by (metis seqSubsCons seqSubsNil seqSubsTermAppend)
  }

  then have "Ψ ⊳ M[<σ>]⦇λ*(p ∙ xvec) (p ∙ N)[<σ>]⦈.((p ∙ P)[<σ>]) ≈ M[<σ>]⦇λ*(p ∙ xvec) (p ∙ N)[<σ>]⦈.((p ∙ Q)[<σ>])"
    using weakBisimInputPres by metis
  with ‹(p ∙ xvec) ♯* σ› have "Ψ ⊳ (M⦇λ*(p ∙ xvec) (p ∙ N)⦈.(p ∙ P))[<σ>] ≈ (M⦇λ*(p ∙ xvec) (p ∙ N)⦈.(p ∙ Q))[<σ>]"
    by (metis seqSubstInputChain seqSubstSimps(3))
  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 "Ψ ⊳ (M⦇λ*xvec N⦈.P)[<σ>] ≈ (M⦇λ*xvec N⦈.Q)[<σ>]"
    by force
qed
(*
lemma bisimSubstCasePresAux:
  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 ∼⇩s Q"
  and     C2: "⋀φ Q. (φ, Q) mem CsQ ⟹ ∃P. (φ, P) mem CsP ∧ guarded P ∧ Ψ ⊳ P ∼⇩s Q"

  shows "Ψ ⊳ Cases CsP ∼⇩s Cases CsQ"
proof -
  {
    fix xvec :: "name list"
    and Tvec :: "'a list"

    assume "length xvec = length Tvec"
    and    "distinct xvec"

    have "Ψ ⊳ Cases(caseListSubst CsP xvec Tvec) ∼ Cases(caseListSubst CsQ xvec Tvec)"
    proof(rule bisimCasePres)
      fix φ P
      assume "(φ, P) mem (caseListSubst CsP xvec Tvec)"
      then obtain φ' P' where "(φ', P') mem CsP" and "φ = substCond φ' xvec Tvec" and PeqP': "P = (P'[xvec::=Tvec])"
        by(induct CsP) force+
      from `(φ', P') mem CsP` obtain Q' where "(φ', Q') mem CsQ" and "guarded Q'" and "Ψ ⊳ P' ∼⇩s Q'" by(blast dest: C1)
      from `(φ', Q') mem CsQ` `φ = substCond φ' xvec Tvec` obtain Q where "(φ, Q) mem (caseListSubst CsQ xvec Tvec)" and "Q = Q'[xvec::=Tvec]"
        by(induct CsQ) auto
      with PeqP' `guarded Q'` `Ψ ⊳ P' ∼⇩s Q'` `length xvec = length Tvec` `distinct xvec` show "∃Q. (φ, Q) mem (caseListSubst CsQ xvec Tvec) ∧ guarded Q ∧ Ψ ⊳ P ∼ Q"
        by(blast dest: bisimSubstE guardedSubst)
    next
      fix φ Q
      assume "(φ, Q) mem (caseListSubst CsQ xvec Tvec)"
      then obtain φ' Q' where "(φ', Q') mem CsQ" and "φ = substCond φ' xvec Tvec" and QeqQ': "Q = Q'[xvec::=Tvec]"
        by(induct CsQ) force+
      from `(φ', Q') mem CsQ` obtain P' where "(φ', P') mem CsP" and "guarded P'" and "Ψ ⊳ P' ∼⇩s Q'" by(blast dest: C2)
      from `(φ', P') mem CsP` `φ = substCond φ' xvec Tvec` obtain P where "(φ, P) mem (caseListSubst CsP xvec Tvec)" and "P = P'[xvec::=Tvec]"
        by(induct CsP) auto
      with QeqQ' `guarded P'` `Ψ ⊳ P' ∼⇩s Q'` `length xvec = length Tvec` `distinct xvec` show "∃P. (φ, P) mem (caseListSubst CsP xvec Tvec) ∧ guarded P ∧ Ψ ⊳ P ∼ Q"
        by(blast dest: bisimSubstE guardedSubst)
    qed
  }
  thus ?thesis
    by(rule_tac bisimSubstI) auto
qed
*)
lemma weakBisimSubstReflexive:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"

  shows "Ψ ⊳ P ≈⇩s P"
by(auto intro: closeSubstI weakBisimReflexive)

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

  assumes "Ψ ⊳ P ≈⇩s Q"
  and     "Ψ ⊳ Q ≈⇩s R"

  shows "Ψ ⊳ P ≈⇩s R"
using assms
by(auto intro: closeSubstI closeSubstE weakBisimTransitive)

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

  assumes "Ψ ⊳ P ≈⇩s Q"

  shows "Ψ ⊳ Q ≈⇩s P"
using assms
by(auto intro: closeSubstI closeSubstE weakBisimE)
(*
lemma bisimSubstCasePres:
  fixes Ψ   :: 'b
  and   CsP :: "('c × ('a, 'b, 'c) psi) list"
  and   CsQ :: "('c × ('a, 'b, 'c) psi) list"
  
  assumes "length CsP = length CsQ"
  and     C: "⋀(i::nat) φ P φ' Q. ⟦i <= length CsP; (φ, P) = nth CsP i; (φ', Q) = nth CsQ i⟧ ⟹ φ = φ' ∧ Ψ ⊳ P ∼ Q"

  shows "Ψ ⊳ Cases CsP ∼⇩s Cases CsQ"
proof -
  {
    fix φ 
    and P

    assume "(φ, P) mem CsP"

    with `length CsP = length CsQ` have "∃Q. (φ, Q) mem CsQ ∧ Ψ ⊳ P ∼⇩s Q"
      apply(induct n=="length CsP" arbitrary: CsP CsQ rule: nat.induct)
      apply simp
      apply simp
      apply auto

  }
using `length CsP = length CsQ`
proof(induct n=="length CsP" rule: nat.induct)
  case zero
  thus ?case by(fastforce intro: bisimSubstReflexive)
next
  case(Suc n)
next
apply auto
apply(blast intro: bisimSubstReflexive)
apply auto
apply(simp add: nth.simps)
apply(auto simp add: nth.simps)
apply blast
apply(rule_tac bisimSubstCasePresAux)
apply auto
*)
lemma weakBisimSubstParPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"
  
  assumes "Ψ ⊳ P ≈⇩s Q"

  shows "Ψ ⊳ P ∥ R ≈⇩s Q ∥ R"
using assms
by(fastforce intro: closeSubstI closeSubstE weakBisimParPres)

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

  assumes "Ψ ⊳ P ≈⇩s Q"
  and     "x ♯ Ψ"

  shows "Ψ ⊳ ⦇νx⦈P ≈⇩s ⦇νx⦈Q"
proof(rule closeSubstI)
  fix σ :: "(name list × 'a list) list"
  assume "wellFormedSubst σ"
  obtain y::name where "y ♯ Ψ" and "y ♯ P" and "y ♯ Q" and "y ♯ σ"
    by (generate_fresh "name") auto

  from ‹Ψ ⊳ P ≈⇩s Q› have "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ P) ≈⇩s ([(x, y)] ∙ Q)"
    by (rule weakBisimSubstClosed)
  with ‹x ♯ Ψ› ‹y ♯ Ψ› have "Ψ ⊳ ([(x, y)] ∙ P) ≈⇩s ([(x, y)] ∙ Q)"
    by simp
  hence "Ψ ⊳ ([(x, y)] ∙ P)[<σ>] ≈ ([(x, y)] ∙ Q)[<σ>]"
    using ‹wellFormedSubst σ› by (rule closeSubstE)
  hence "Ψ ⊳ ⦇νy⦈(([(x, y)] ∙ P)[<σ>]) ≈ ⦇νy⦈(([(x, y)] ∙ Q)[<σ>])"
    using ‹y ♯ Ψ› by (rule weakBisimResPres)
  with ‹y ♯ P› ‹y ♯ Q› ‹y ♯ σ› show "Ψ ⊳ (⦇νx⦈P)[<σ>] ≈ (⦇νx⦈Q)[<σ>]"
    by (simp add: alphaRes)
qed

(*
lemma bisimSubstBangPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
 
  assumes "Ψ ⊳ P ∼⇩s Q"
  and     "guarded P"
  and     "guarded Q"

  shows "Ψ ⊳ !P ∼⇩s !Q"
using assms
by(fastforce intro: bisimSubstI bisimSubstE bisimBangPres)
*)

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

  shows "Ψ ⊳ P ∥ 𝟬 ≈⇩s P"
by(metis strongBisimSubstWeakBisimSubst bisimSubstParNil) 

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

  shows "Ψ ⊳ P ∥ Q ≈⇩s Q ∥ P"
by(metis strongBisimSubstWeakBisimSubst bisimSubstParComm) 

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

  shows "Ψ ⊳ (P ∥ Q) ∥ R ≈⇩s P ∥ (Q ∥ R)"
by(metis strongBisimSubstWeakBisimSubst bisimSubstParAssoc) 

lemma weakBisimSubstResNil:
  fixes Ψ :: 'b
  and   x :: name

  shows "Ψ ⊳ ⦇νx⦈𝟬 ∼⇩s 𝟬"
by(metis strongBisimSubstWeakBisimSubst bisimSubstResNil) 

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

  assumes "x ♯ P"

  shows "Ψ ⊳ ⦇νx⦈(P ∥ Q) ≈⇩s P ∥ ⦇νx⦈Q" 
using assms
by(metis strongBisimSubstWeakBisimSubst bisimSubstScopeExt) 

lemma weakBisimSubstCasePushRes:
  fixes x  :: name
  and   Ψ  :: 'b
  and   Cs :: "('c × ('a, 'b, 'c) psi) list"

  assumes "x ♯ map fst Cs"

  shows "Ψ ⊳ ⦇νx⦈(Cases Cs) ≈⇩s Cases map (λ(φ, P). (φ, ⦇νx⦈P)) Cs"
using assms
by(metis strongBisimSubstWeakBisimSubst bisimSubstCasePushRes) 

lemma weakBisimSubstOutputPushRes:
  fixes x :: name
  and   Ψ :: 'b
  and   M :: 'a
  and   N :: 'a
  and   P :: "('a, 'b, 'c) psi"

  assumes "x ♯ Ψ"
  and     "x ♯ M"
  and     "x ♯ N"

  shows "Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ≈⇩s M⟨N⟩.⦇νx⦈P"
using assms
by(metis strongBisimSubstWeakBisimSubst bisimSubstOutputPushRes) 

lemma weakBisimSubstInputPushRes:
  fixes x    :: name
  and   Ψ    :: 'b
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a

  assumes "x ♯ M"
  and     "x ♯ xvec"
  and     "x ♯ N"

  shows "Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ≈⇩s M⦇λ*xvec N⦈.⦇νx⦈P"
using assms
by(metis strongBisimSubstWeakBisimSubst bisimSubstInputPushRes) 

lemma weakBisimSubstResComm:
  fixes x :: name
  and   y :: name

  shows "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ≈⇩s ⦇νy⦈(⦇νx⦈P)"
by(metis strongBisimSubstWeakBisimSubst bisimSubstResComm) 

lemma weakBisimSubstExtBang:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  
  assumes "guarded P"

  shows "Ψ ⊳ !P ≈⇩s P ∥ !P"
using assms
by(metis strongBisimSubstWeakBisimSubst bisimSubstExtBang) 

end

end