(* 
   Title: The Calculus of Communicating Systems   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Struct_Cong
  imports Agent
begin

inductive structCong :: "ccs → ccs → bool" (‹_ ≡_s _›)
  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 ∥ 0 ≡_s P"

| SumComm: "P ⊕ Q ≡_s Q ⊕ P"
| SumAssoc: "(P ⊕ Q) ⊕ R ≡_s P ⊕ (Q ⊕ R)"
| SumId: "P ⊕ 0 ≡_s P"

| ResNil: "(νx)0 ≡_s 0"
| ScopeExtPar: "x ♯ P ==> (νx)(P ∥ Q) ≡_s P ∥ (νx)Q"
| ScopeExtSum: "x ♯ P ==> (νx)(P ⊕ Q) ≡_s P ⊕ (νx)Q"
| ScopeAct: "x ♯ α ==> (νx)(α.(P)) ≡_s α.((νx)P)"
| ScopeCommAux: "x ≠ y ==> (νx)((νy)P) ≡_s (νy)((νx)P)"

| BangUnfold: "!P ≡_s P ∥ !P"
equivariance structCong
nominal_inductive structCong
by(auto simp add: abs_fresh)

lemma ScopeComm:
  fixes x :: name
  and   y :: name
  and   P :: ccs

  shows "(νx)((νy)P) ≡_s (νy)((νx)P)"
by(cases "x=y") (auto intro: Refl ScopeCommAux)

end