Theory Psi_Calculi.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(⦇νyP) s ⦇νy(⦇νxP)"
| ScopeExtPar: "x  P  ⦇νx(P  Q) s P  ⦇νxQ"
| InputRes: "x  M; x  xvec; x  N  ⦇νx(M⦇λ*xvec N⦈.P) s M⦇λ*xvec N⦈.(⦇νxP)"
| OutputRes: "x  M; x  N  ⦇νx(MN⟩.P) s MN⟩.(⦇νxP)"
| CaseRes: "x  (map fst Cs)  ⦇νx(Cases Cs) s Cases(map (λ(φ, P). (φ, ⦇νxP)) Cs)"

| BangUnfold: "guarded P  !P s P  !P"

end