def isConf {L : Type u_1} (es : PES L) (X : Set es.Event) : Prop

A set of events is a configuration if it is conflict-free and downward closed.

Equations

• isConf es X = ((∀ {e₁ e₂ : es.Event}, e₁ ∈ X → e₂ ∈ X → ¬es.conflict e₁ e₂) ∧ ∀ {e e' : es.Event}, e ∈ X → e' ≤ e → e' ∈ X)

def Conf {L : Type u_1} (es : PES L) : Type

Type of all configurations of an event structure.

Equations

• Conf es = { X : Set es.Event // isConf es X }

def FinConf {L : Type u_1} (es : PES L) : Type

Type of all finite configurations of an event structure.

Equations

• FinConf es = { X : Finset es.Event // isConf es ↑X }

def Configuration.enables {L : Type u_1} (es : PES L) (c : Set es.Event) (e : es.Event) : Prop

c enables e if e is consistent with c, and the past of e lies in c.

Equations

• Configuration.enables es c e = (isConf es c ∧ (∀ e' ∈ c, es.consistent e e') ∧ es.past e ⊆ c)

theorem Configuration.enables_extension {L : Type u_1} (es : PES L) {c : Set es.Event} {e : es.Event} (h : enables es c e) : isConf es (c ∪ {e})

If a configuration c enables an event e, then c ∪ {e} is also a configuration.

theorem Configuration.isConf_empty {L : Type u_1} (es : PES L) : isConf es ∅

Configurations of ∅.

structure Emb {L : Type u_2} (E : PES L) (F : PES L) : Type (max u_3 u_4)

An injective, monotone, conflict-reflecting map of event structures.

• f : E.Event → F.Event
• inj : Function.Injective self.f
• mono {x y : E.Event} : x ≤ y → self.f x ≤ self.f y
• smono {x y : E.Event} : x < y → self.f x < self.f y
• conf {x y : E.Event} : E.conflict x y → F.conflict (self.f x) (self.f y)

theorem Emb.finite {L : Type u_2} {E : PES L} {F : PES L} (ι : Emb E F) {c : Set F.Event} (h : c.Finite) : {y : E.Event | ι.f y ∈ c}.Finite

theorem Emb.conf_restrict {L : Type u_2} {E : PES L} {F : PES L} (ι : Emb E F) {c : Set F.Event} (h : isConf F c) : isConf E {y : E.Event | ι.f y ∈ c}

theorem Emb.enables_restrict {L : Type u_2} {E : PES L} {F : PES L} (ι : Emb E F) {c : Set F.Event} {x : E.Event} (hc : isConf F c) (h : Configuration.enables F c (ι.f x)) : Configuration.enables E {y : E.Event | ι.f y ∈ c} x

theorem preimage_insert {α : Type u_2} {β : Type u_3} {ι : α → β} (hι : Function.Injective ι) (c : Set β) (x : α) : {y : α | ι y ∈ c ∪ {ι x}} = {y : α | ι y ∈ c} ∪ {x}

Restricting along an injection commutes with adding one event.

Bridge to configuration families

def PES.toFamily {L : Type u_2} (P : PES L) : ConfFamily L

A prime event structure gives a configuration family.

Equations

• P.toFamily = { Event := P.Event, Config := isConf P, label := P.label, empty_mem := ⋯, secured := ⋯ }

@[simp]

theorem PES.toFamily_Event {L : Type u_2} (P : PES L) : P.toFamily.Event = P.Event

@[simp]

theorem PES.toFamily_Config {L : Type u_2} (P : PES L) : P.toFamily.Config = isConf P

@[simp]

theorem PES.enables_iff {L : Type u_2} (P : PES L) {c : Set P.Event} {e : P.Event} : P.toFamily.enables c e ↔ Configuration.enables P c e

The family enabling relation agrees with the prime one.

theorem PES.indep_iff_concurrent {L : Type u_2} (P : PES L) {c : Set P.Event} {e₁ e₂ : P.Event} (h₁ : Configuration.enables P c e₁) (h₂ : Configuration.enables P c e₂) (hf₁ : e₁ ∉ c) (hf₂ : e₂ ∉ c) : P.toFamily.Indep c e₁ e₂ ↔ P.concurrent e₁ e₂

Derived independence coincides with concurrency, for distinct fresh events.