Images of sets of states

The image of a set of states of an LTS along a label and along a list of labels, with lemmas on membership, singletons, the empty set and the empty list, unions, monotonicity and concatenation.

Main definitions

• LTS.setImage: the μ-image of a set of states.
• LTS.setImageMultistep: the μs-image of a set of states, for a list of labels μs.

Main statements

• LTS.mem_setImage, LTS.mem_setImageMultistep: membership through Tr and MTr.
• LTS.setImageMultistep_foldl_setImage: the multistep image is a left fold of setImage.
• LTS.setImage_union, LTS.setImageMultistep_union: images distribute over unions.
• LTS.setImageMultistep_append: the image along μs₁ ++ μs₂ is the image along μs₂ of the image along μs₁.

def Cslib.LTS.setImage {State : Type u} {Label : Type v} (lts : LTS State Label) (S : Set State) (μ : Label) : Set State

The μ-image of a set of states S is the union of all μ-images of the states in S.

Equations

• lts.setImage S μ = ⋃ s ∈ S, lts.image s μ

def Cslib.LTS.setImageMultistep {State : Type u} {Label : Type v} (lts : LTS State Label) (S : Set State) (μs : List Label) : Set State

The μs-image of a set of states S, where μs is a list of labels, is the union of all μs-images of the states in S.

Equations

• lts.setImageMultistep S μs = ⋃ s ∈ S, lts.imageMultistep s μs

theorem Cslib.LTS.mem_setImage {State : Type u} {Label : Type v} {S : Set State} {μ : Label} {s' : State} {lts : LTS State Label} : s' ∈ lts.setImage S μ ↔ ∃ s ∈ S, lts.Tr s μ s'

Characterisation of setImage wrt Tr.

theorem Cslib.LTS.tr_setImage {State : Type u} {Label : Type v} {S : Set State} {s : State} {μ : Label} {s' : State} {lts : LTS State Label} (hs : s ∈ S) (htr : lts.Tr s μ s') : s' ∈ lts.setImage S μ

theorem Cslib.LTS.mem_setImageMultistep {State : Type u} {Label : Type v} {S : Set State} {μs : List Label} {s' : State} {lts : LTS State Label} : s' ∈ lts.setImageMultistep S μs ↔ ∃ s ∈ S, lts.MTr s μs s'

Characterisation of setImageMultistep with MTr.

theorem Cslib.LTS.mTr_setImage {State : Type u} {Label : Type v} {S : Set State} {s : State} {μs : List Label} {s' : State} {lts : LTS State Label} (hs : s ∈ S) (htr : lts.MTr s μs s') : s' ∈ lts.setImageMultistep S μs

theorem Cslib.LTS.setImage_empty {State : Type u} {Label : Type v} {μ : Label} (lts : LTS State Label) : lts.setImage ∅ μ = ∅

The image of the empty set is always the empty set.

theorem Cslib.LTS.setImageMultistep_setImage_head {State : Type u} {Label : Type v} {S : Set State} {μ : Label} {μs : List Label} (lts : LTS State Label) : lts.setImageMultistep S (μ :: μs) = lts.setImageMultistep (lts.setImage S μ) μs

theorem Cslib.LTS.setImageMultistep_foldl_setImage {State : Type u} {Label : Type v} (lts : LTS State Label) : lts.setImageMultistep = List.foldl lts.setImage

Characterisation of setImageMultistep as List.foldl on setImage.

theorem Cslib.LTS.mem_foldl_setImage {State : Type u} {Label : Type v} {S : Set State} {μs : List Label} {s' : State} (lts : LTS State Label) : s' ∈ List.foldl lts.setImage S μs ↔ ∃ s ∈ S, lts.MTr s μs s'

Characterisation of membership in List.foldl lts.setImage with MTr.

@[simp]

theorem Cslib.LTS.setImage_singleton {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) (μ : Label) : lts.setImage {s} μ = lts.image s μ

The image of a singleton is the image of its element.

@[simp]

theorem Cslib.LTS.setImage_union {State : Type u} {Label : Type v} (lts : LTS State Label) (S T : Set State) (μ : Label) : lts.setImage (S ∪ T) μ = lts.setImage S μ ∪ lts.setImage T μ

Images of sets distribute over binary unions.

@[simp]

theorem Cslib.LTS.setImage_iUnion {State : Type u} {Label : Type v} (lts : LTS State Label) {ι : Sort u_1} (S : ι → Set State) (μ : Label) : lts.setImage (⋃ (i : ι), S i) μ = ⋃ (i : ι), lts.setImage (S i) μ

Images of sets distribute over indexed unions.

theorem Cslib.LTS.setImage_mono {State : Type u} {Label : Type v} (lts : LTS State Label) {S T : Set State} (h : S ⊆ T) (μ : Label) : lts.setImage S μ ⊆ lts.setImage T μ

Taking the image of a set is monotone.

@[simp]

theorem Cslib.LTS.setImageMultistep_nil {State : Type u} {Label : Type v} (lts : LTS State Label) (S : Set State) : lts.setImageMultistep S [] = S

The multistep image of a set along the empty list is the set itself.

@[simp]

theorem Cslib.LTS.setImageMultistep_empty {State : Type u} {Label : Type v} (lts : LTS State Label) (μs : List Label) : lts.setImageMultistep ∅ μs = ∅

The multistep image of the empty set is empty.

@[simp]

theorem Cslib.LTS.setImageMultistep_singleton {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) (μs : List Label) : lts.setImageMultistep {s} μs = lts.imageMultistep s μs

The multistep image of a singleton is the multistep image of its element.

@[simp]

theorem Cslib.LTS.setImageMultistep_union {State : Type u} {Label : Type v} (lts : LTS State Label) (S T : Set State) (μs : List Label) : lts.setImageMultistep (S ∪ T) μs = lts.setImageMultistep S μs ∪ lts.setImageMultistep T μs

Multistep images of sets distribute over binary unions.

@[simp]

theorem Cslib.LTS.setImageMultistep_iUnion {State : Type u} {Label : Type v} (lts : LTS State Label) {ι : Sort u_1} (S : ι → Set State) (μs : List Label) : lts.setImageMultistep (⋃ (i : ι), S i) μs = ⋃ (i : ι), lts.setImageMultistep (S i) μs

Multistep images of sets distribute over indexed unions.

theorem Cslib.LTS.setImageMultistep_mono {State : Type u} {Label : Type v} (lts : LTS State Label) {S T : Set State} (h : S ⊆ T) (μs : List Label) : lts.setImageMultistep S μs ⊆ lts.setImageMultistep T μs

Taking the multistep image of a set is monotone.

@[simp]

theorem Cslib.LTS.setImageMultistep_append {State : Type u} {Label : Type v} (lts : LTS State Label) (S : Set State) (μs₁ μs₂ : List Label) : lts.setImageMultistep S (μs₁ ++ μs₂) = lts.setImageMultistep (lts.setImageMultistep S μs₁) μs₂

The multistep image along μs₁ ++ μs₂ is the multistep image along μs₂ of the multistep image along μs₁.