```------------------------------------------------------------------------
-- A formalisation of CBS, close to "A calculus of broadcasting
-- systems" by K.V.S. Prasad, but using mixed induction and
-- coinduction instead of explicit guarded definitions
------------------------------------------------------------------------

module CBS where

open import Coinduction
open import Data.Product
open import Function.Equality
open import Function.Equivalence
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Sets with decidable propositional equality

record Data : Set₁ where
field
El     : Set
⟨_⟩_≟_ : Decidable (_≡_ {A = El})

open Data public

------------------------------------------------------------------------
-- Processes

-- Messages; τ stands for a silent message.

data Msg α : Set where
msg : (v : El α) → Msg α
τ   : Msg α

-- Processes. Instead of explicit guarded definitions I have used
-- mixed induction and coinduction.

infix 5 _&⟨_,_⟩ _∣_ _[_]

data Proc (α : Data) : Set₁ where
¿       : (f : El α → ∞ (Proc α)) → Proc α
_&⟨_,_⟩ : (f : El α → ∞ (Proc α)) (w : Msg α) (p : ∞ (Proc α)) → Proc α
_∣_     : (p₁ p₂ : Proc α) → Proc α
_[_]    : ∀ {β} (ϕ : El α ⇔ El β) (p : Proc β) → Proc α

------------------------------------------------------------------------
-- Some derived operators

∅ : ∀ {α} → Proc α
∅ = ¿ λ _ → ♯ ∅

-- Swallows messages until it gets a chance to send.

_¡_ : ∀ {α} → Msg α → Proc α → Proc α
w ¡ p = (λ _ → ♯ (w ¡ p)) &⟨ w , ♯ p ⟩

------------------------------------------------------------------------
-- Single-step semantics

-- Application of translation functions.

infixr 5 _↑_ _↓_

_↑_ : ∀ {α β} → El α ⇔ El β → Msg β → Msg α
ϕ ↑ msg x = msg (Equivalence.from ϕ ⟨\$⟩ x)
ϕ ↑ τ     = τ

_↓_ : ∀ {α β} → El α ⇔ El β → Msg α → Msg β
ϕ ↓ msg x = msg (Equivalence.to ϕ ⟨\$⟩ x)
ϕ ↓ τ     = τ

-- Actions are messages along with information about whether they are

data SendRecv : Set where
! : SendRecv
¿ : SendRecv

Action : Data → Set
Action α = Msg α × SendRecv

-- Two processes cannot simultaneously send something.

infix 4 _·_≡_

data _·_≡_ : SendRecv → SendRecv → SendRecv → Set where
!¿ : ! · ¿ ≡ !
¿! : ¿ · ! ≡ !
¿¿ : ¿ · ¿ ≡ ¿

-- The single-step relation.

infix 4 _[_]⟶_

data _[_]⟶_ {α} : Proc α → Action α → Proc α → Set₁ where
τ          : ∀ {p}       → p            [ τ     , ¿ ]⟶ p
¿-recv     : ∀ {f     v} → ¿ f          [ msg v , ¿ ]⟶ ♭ (f v)
&-recv     : ∀ {f w p v} → f &⟨ w , p ⟩ [ msg v , ¿ ]⟶ ♭ (f v)
&-send     : ∀ {f w p}   → f &⟨ w , p ⟩ [ w     , ! ]⟶ ♭ p
compose    : ∀ {p₁ p₁′ p₂ p₂′ ♮₁ ♮₂ ♮₃ w}
(¬‼     : ♮₁ · ♮₂ ≡ ♮₃)
(p₁⟶p₁′ : p₁ [ w , ♮₁ ]⟶ p₁′)
(p₂⟶p₂′ : p₂ [ w , ♮₂ ]⟶ p₂′) →
p₁ ∣ p₂ [ w , ♮₃ ]⟶ p₁′ ∣ p₂′
trans-send : ∀ {β} {p p′ : Proc β} {ϕ u} (p⟶p′ : p [ u     , ! ]⟶ p′) → ϕ [ p ] [ ϕ ↑ u , ! ]⟶ ϕ [ p′ ]
trans-recv : ∀ {β} {p p′ : Proc β} {ϕ w} (p⟶p′ : p [ ϕ ↓ w , ¿ ]⟶ p′) → ϕ [ p ] [ w     , ¿ ]⟶ ϕ [ p′ ]

------------------------------------------------------------------------
-- Strong bisimulation

-- The largest strong bisimulation.

infix 4 _∼_

record _∼_ {α} (p₁ p₂ : Proc α) : Set₁ where
inductive
field
⇒ : ∀ {p₁′ w ♮} → p₁ [ w , ♮ ]⟶ p₁′ →
∃ λ p₂′ → p₂ [ w , ♮ ]⟶ p₂′ × ∞ (p₁′ ∼ p₂′)

⇐ : ∀ {p₂′ w ♮} → p₂ [ w , ♮ ]⟶ p₂′ →
∃ λ p₁′ → p₁ [ w , ♮ ]⟶ p₁′ × ∞ (p₁′ ∼ p₂′)
```