Theory Structural_Congruence

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


inductive structCong :: "(('a::fs_name), ('b::fs_name), ('c::fs_name)) psi ⇒ ('a, 'b, 'c) psi ⇒ bool" ("_ ≡⇩s _" [70, 70] 70)
where
  Refl: "P ≡⇩s P"
| Sym:  "P ≡⇩s Q ⟹ Q ≡⇩s P"
| Trans: "⟦P ≡⇩s Q; Q ≡⇩s R⟧ ⟹ P ≡⇩s R"

| ParComm: "P ∥ Q ≡⇩s Q ∥ P"
| ParAssoc: "(P ∥ Q) ∥ R ≡⇩s P ∥ (Q ∥ R)"
| ParId: "P ∥ 𝟬 ≡⇩s P"

| ResNil: "⦇νx⦈𝟬 ≡⇩s 𝟬"
| ResComm: "⦇νx⦈(⦇νy⦈P) ≡⇩s ⦇νy⦈(⦇νx⦈P)"
| ScopeExtPar: "x ♯ P ⟹ ⦇νx⦈(P ∥ Q) ≡⇩s P ∥ ⦇νx⦈Q"
| InputRes: "⟦x ♯ M; x ♯ xvec; x ♯ N⟧ ⟹ ⦇νx⦈(M⦇λ*xvec N⦈.P) ≡⇩s M⦇λ*xvec N⦈.(⦇νx⦈P)"
| OutputRes: "⟦x ♯ M; x ♯ N⟧ ⟹ ⦇νx⦈(M⟨N⟩.P) ≡⇩s M⟨N⟩.(⦇νx⦈P)"
| CaseRes: "x ♯ (map fst Cs) ⟹ ⦇νx⦈(Cases Cs) ≡⇩s Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"

| BangUnfold: "guarded P ⟹ !P ≡⇩s P ∥ !P"

end