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 \<parallel> Q ≡⇩s Q \<parallel> P"
| ParAssoc: "(P \<parallel> Q) \<parallel> R ≡⇩s P \<parallel> (Q \<parallel> R)"
| ParId: "P \<parallel> \<zero> ≡⇩s P"

| SumComm: "P ⊕ Q ≡⇩s Q ⊕ P"
| SumAssoc: "(P ⊕ Q) ⊕ R ≡⇩s P ⊕ (Q ⊕ R)"
| SumId: "P ⊕ \<zero> ≡⇩s P"

| ResNil: "(|νx|)),\<zero> ≡⇩s \<zero>"
| ScopeExtPar: "x \<sharp> P ==> (|νx|)),(P \<parallel> Q) ≡⇩s P \<parallel> (|νx|)),Q"
| ScopeExtSum: "x \<sharp> P ==> (|νx|)),(P ⊕ Q) ≡⇩s P ⊕ (|νx|)),Q"
| ScopeAct: "x \<sharp> α ==> (|νx|)),(α.(P)) ≡⇩s α.((|νx|)),P)"
| ScopeCommAux: "x ≠ y ==> (|νx|)),((|νy|)),P) ≡⇩s (|νy|)),((|νx|)),P)"

| BangUnfold: "!P ≡⇩s P \<parallel> !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