Theory Struct_Cong

(* 
   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 ∥ 𝟬 ≡⇩s P"

| SumComm: "P ⊕ Q ≡⇩s Q ⊕ P"
| SumAssoc: "(P ⊕ Q) ⊕ R ≡⇩s P ⊕ (Q ⊕ R)"
| SumId: "P ⊕ 𝟬 ≡⇩s P"

| ResNil: "⦇νx⦈𝟬 ≡⇩s 𝟬"
| 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