Finitary CCS: syntax and operational semantics

inductive CCS.Label (Name : Type u_1) : Type u_1

CCS labels: input or output on a name.

• inp {Name : Type u_1} : Name → Label Name
• out {Name : Type u_1} : Name → Label Name

def CCS.Label.co {Name : Type u_1} : Label Name → Label Name

Co-label: swap input/output.

Equations

• (CCS.Label.inp n).co = CCS.Label.out n
• (CCS.Label.out n).co = CCS.Label.inp n

@[simp]

theorem CCS.Label.co_co {Name : Type u_1} (a : Label Name) : a.co.co = a

def CCS.Label.map {Name : Type u_1} {Name' : Type u_2} (f : Name → Name') : Label Name → Label Name'

Rename the underlying name.

Equations

• CCS.Label.map f (CCS.Label.inp n) = CCS.Label.inp (f n)
• CCS.Label.map f (CCS.Label.out n) = CCS.Label.out (f n)

def CCS.Label.strip {Name : Type u_1} : Label (Option Name) → Option (Label Name)

Strip a label down to Name, failing on the bound name none.

Equations

• (CCS.Label.inp none).strip = none
• (CCS.Label.inp (some n)).strip = some (CCS.Label.inp n)
• (CCS.Label.out none).strip = none
• (CCS.Label.out (some n)).strip = some (CCS.Label.out n)

@[simp]

theorem CCS.Label.strip_map {Name : Type u_1} (a : Label Name) : (map some a).strip = some a

inductive CCS.Action (Name : Type u_1) : Type u_1

CCS actions: a visible label, or the internal action τ.

• vis {Name : Type u_1} : Label Name → Action Name
• tau {Name : Type u_1} : Action Name

def CCS.Action.map {Name : Type u_1} {Name' : Type u_2} (f : Name → Name') : Action Name → Action Name'

Rename the underlying name.

Equations

• CCS.Action.map f (CCS.Action.vis a) = CCS.Action.vis (CCS.Label.map f a)
• CCS.Action.map f CCS.Action.tau = CCS.Action.tau

def CCS.Action.strip {Name : Type u_1} : Action (Option Name) → Option (Action Name)

Strip an action down to Name, failing if it mentions the bound name.

Equations

• (CCS.Action.vis a).strip = Option.map CCS.Action.vis a.strip
• CCS.Action.tau.strip = some CCS.Action.tau

@[simp]

theorem CCS.Action.strip_map {Name : Type u_1} (α : Action Name) : (map some α).strip = some α

theorem CCS.Action.map_some_of_strip {Name : Type u_1} {b : Action (Option Name)} {a : Action Name} : b.strip = some a → b = map some a

strip inverts map some.

inductive CCS.Process : Type u → Type (u + 1)

Finitary CCS, well-scoped: res binds a name via Option.

• nil {Name : Type u} : Process Name
• pre {Name : Type u} : Action Name → Process Name → Process Name
• sum {Name : Type u} : Process Name → Process Name → Process Name
• par {Name : Type u} : Process Name → Process Name → Process Name
• res {Name : Type u} : Process (Option Name) → Process Name

inductive CCS.Step {Name : Type u_1} : Process Name → Action Name → Process Name → Prop

Operational semantics of CCS.

• pre {Name : Type u_1} {α : Action Name} {P : Process Name} : Step (Process.pre α P) α P
• sumL {Name : Type u_1} {P : Process Name} {α : Action Name} {P' Q : Process Name} : Step P α P' → Step (P.sum Q) α P'
• sumR {Name : Type u_1} {P Q : Process Name} {α : Action Name} {Q' : Process Name} : Step Q α Q' → Step (P.sum Q) α Q'
• parL {Name : Type u_1} {P : Process Name} {α : Action Name} {P' Q : Process Name} : Step P α P' → Step (P.par Q) α (P'.par Q)
• parR {Name : Type u_1} {P Q : Process Name} {α : Action Name} {Q' : Process Name} : Step Q α Q' → Step (P.par Q) α (P.par Q')
• parSync {Name : Type u_1} {P : Process Name} {a : Label Name} {P' Q Q' : Process Name} : Step P (Action.vis a) P' → Step Q (Action.vis a.co) Q' → Step (P.par Q) Action.tau (P'.par Q')
• res {Name : Type u_1} {P : Process (Option Name)} {α : Action Name} {P' : Process (Option Name)} : Step P (Action.map some α) P' → Step P.res α P'.res