General event structures

Consistency is n-ary and causality is disjunctive.

structure GES (Label : Type u_1) : Type (max u_1 (u_2 + 1))

Events, an n-ary consistency predicate, and an enabling relation.

• Event : Type u_2
• Con : Finset self.Event → Prop
• enable : Finset self.Event → self.Event → Prop
• label : self.Event → Label
• con_empty : self.Con ∅
• con_subset {X Y : Finset self.Event} : self.Con Y → X ⊆ Y → self.Con X
• enable_mono {X Y : Finset self.Event} {e : self.Event} : self.enable X e → X ⊆ Y → self.Con Y → self.enable Y e

def GES.secApprox {L : Type u_1} (G : GES L) (x : Set G.Event) : ℕ → Set G.Event

Events of x secured in at most n steps.

Equations

• G.secApprox x 0 = ∅
• G.secApprox x n.succ = {e : G.Event | e ∈ x ∧ ∃ (X : Finset G.Event), ↑X ⊆ G.secApprox x n ∧ G.enable X e}

theorem GES.secApprox_subset {L : Type u_1} {G : GES L} {x : Set G.Event} (n : ℕ) : G.secApprox x n ⊆ x

theorem GES.secApprox_succ {L : Type u_1} {G : GES L} {x : Set G.Event} (n : ℕ) : G.secApprox x n ⊆ G.secApprox x (n + 1)

theorem GES.secApprox_mono {L : Type u_1} {G : GES L} {x : Set G.Event} {m n : ℕ} (h : m ≤ n) : G.secApprox x m ⊆ G.secApprox x n

theorem GES.secApprox_mono_set {L : Type u_1} {G : GES L} {x y : Set G.Event} (hxy : x ⊆ y) (n : ℕ) : G.secApprox x n ⊆ G.secApprox y n

Securedness only ever grows with the ambient set.

def GES.Consistent {L : Type u_1} (G : GES L) (s : Set G.Event) : Prop

Every finite subset is consistent.

Equations

• G.Consistent s = ∀ (X : Finset G.Event), ↑X ⊆ s → G.Con X

def GES.isConf {L : Type u_1} (G : GES L) (x : Set G.Event) : Prop

Consistent, and every event secured inside it.

Equations

• G.isConf x = (G.Consistent x ∧ ∀ e ∈ x, ∃ (n : ℕ), e ∈ G.secApprox x n)

noncomputable def GES.rank {L : Type u_1} (G : GES L) (x : Set G.Event) (e : G.Event) : ℕ

The least number of steps securing e in x.

Equations

• G.rank x e = sInf {n : ℕ | e ∈ G.secApprox x n}

theorem GES.rank_mem {L : Type u_1} {G : GES L} {x : Set G.Event} {e : G.Event} (h : ∃ (n : ℕ), e ∈ G.secApprox x n) : e ∈ G.secApprox x (G.rank x e)

theorem GES.rank_le {L : Type u_1} {G : GES L} {x : Set G.Event} {e : G.Event} {n : ℕ} (h : e ∈ G.secApprox x n) : G.rank x e ≤ n

theorem GES.exists_bound {L : Type u_1} {G : GES L} {x : Set G.Event} {X : Finset G.Event} (h : ∀ g ∈ X, ∃ (n : ℕ), g ∈ G.secApprox x n) : ∃ (N : ℕ), ↑X ⊆ G.secApprox x N

A finite set of secured events is secured uniformly.

theorem GES.exists_enabling {L : Type u_1} {G : GES L} {x : Set G.Event} (hx : G.isConf x) {e : G.Event} (he : e ∈ x) : ∃ (Y : Finset G.Event), G.enable Y e ∧ ↑Y ⊆ x

Every event of a configuration has an enabling set inside it.

theorem GES.isConf_empty {L : Type u_1} (G : GES L) : G.isConf ∅

The empty set is a configuration.

theorem GES.isConf_secured {L : Type u_1} (G : GES L) {x y : Set G.Event} (hx : G.isConf x) (hy : G.isConf y) (hsub : y ⊆ x) (hfin : (x \ y).Finite) (hne : x ≠ y) : ∃ e ∈ x \ y, G.isConf (x \ {e})

An event of the gap of greatest rank can be removed.

theorem GES.isConf_rank_lt {L : Type u_1} (G : GES L) {c : Set G.Event} (hc : G.isConf c) {x : G.Event} (hx : x ∈ c) : G.isConf ({z : G.Event | z ∈ c ∧ G.rank c z < G.rank c x} ∪ {x})

The events of c of rank strictly below that of x, together with x, form a configuration.

def GES.pmapSet {L : Type u_1} {L' : Type u_2} {G : GES L} {H : GES L'} (φ : G.Event → Option H.Event) (c : Set G.Event) : Set H.Event

The image of a set under a partial map on events.

Equations

• GES.pmapSet φ c = {x : H.Event | ∃ u ∈ c, φ u = some x}

theorem GES.subset_pmapSet {L : Type u_1} {L' : Type u_2} {G : GES L} {H : GES L'} {φ : G.Event → Option H.Event} {c : Set G.Event} {u : G.Event} {x : H.Event} (hu : u ∈ c) (hx : φ u = some x) : x ∈ pmapSet φ c

theorem GES.pmapSet_mono {L : Type u_1} {L' : Type u_2} {G : GES L} {H : GES L'} {φ : G.Event → Option H.Event} {c d : Set G.Event} (h : c ⊆ d) : pmapSet φ c ⊆ pmapSet φ d

theorem GES.isConf_pmap {L : Type u_1} {L' : Type u_2} {G : GES L} {H : GES L'} (φ : G.Event → Option H.Event) (hcon : ∀ {c : Set G.Event}, G.Consistent c → H.Consistent (pmapSet φ c)) (hen : ∀ {X : Finset G.Event} {u : G.Event} {x : H.Event}, G.enable X u → φ u = some x → ∃ (Y : Finset H.Event), (∀ y ∈ Y, y ∈ pmapSet φ ↑X) ∧ H.enable Y x) {c : Set G.Event} (hc : G.isConf c) : H.isConf (pmapSet φ c)

Configurations transfer along a partial map that carries enabling sets to enabling sets.

theorem GES.isConf_insert_pmap {L : Type u_1} {L' : Type u_2} {G : GES L} {H : GES L'} (φ : G.Event → Option H.Event) {c : Set G.Event} {u : G.Event} {x : H.Event} (hc : G.isConf c) (hφ : φ u = some x) (hcon : G.Consistent (c ∪ {u})) (hback : ∀ (Y : Finset H.Event), (∀ y ∈ Y, y ∈ pmapSet φ c) → H.enable Y x → ∃ (X : Finset G.Event), ↑X ⊆ c ∧ G.enable X u) (hx : H.isConf (pmapSet φ c ∪ {x})) : G.isConf (c ∪ {u})

Conversely, an event whose image is enabled extends a configuration, provided enabling sets pull back.

def GES.toFamily {L : Type u_1} (G : GES L) : ConfFamily L

The configuration family of a general event structure.

Equations

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

@[simp]

theorem GES.toFamily_Event {L : Type u_1} (G : GES L) : G.toFamily.Event = G.Event

@[simp]

theorem GES.toFamily_Config {L : Type u_1} (G : GES L) : G.toFamily.Config = G.isConf