Documentation

Cslib.Foundations.Semantics.LTS.Reverse

Reverse operation for LTS #

This file defines Cslib.LTS.reverse, which reverses every transition of an LTS. reverse_canReach, reverse_unlabelledTr, reverse_image, reverse_imageMultistep, reverse_hasOutLabel and reverse_boundedUpTo each state a property about lts.reverse in terms of lts.

reverse_mTr states that the multistep transitions of lts.reverse are the reversed multistep transitions of lts. reverse_execution is the same statement for executions, and is derived from Execution.reverse.

source
def Cslib.LTS.reverse {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) :
LTS State Label

Constructs an LTS by reversing the transitions of an existing LTS.

Equations
  • lts.reverse = { Tr := fun (s : State) (μ : Label) (s' : State) => lts.Tr s' μ s }
Instances For
    source
    @[simp]
    theorem Cslib.LTS.reverse_tr {State : Type u_1} {Label : Type u_2} {s : State} {μ : Label} {s' : State} {lts : LTS State Label} :
    lts.reverse.Tr s μ s' ↔ lts.Tr s' μ s

    The transitions of lts.reverse are exactly the reversed transitions of lts.

    source
    @[simp]
    theorem Cslib.LTS.reverse_reverse {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) :
    lts.reverse.reverse = lts

    Reversing an LTS twice gives back the original LTS.

    source
    theorem Cslib.LTS.reverse_involutive {State : Type u_1} {Label : Type u_2} :
    Function.Involutive reverse

    Reversal of an LTS is an involution.

    source
    @[simp]
    theorem Cslib.LTS.reverse_mTr {State : Type u_1} {Label : Type u_2} {s' : State} {μs : List Label} {s : State} {lts : LTS State Label} :
    lts.reverse.MTr s' μs s ↔ lts.MTr s μs.reverse s'

    The multistep transitions of lts.reverse are exactly the reversed multistep transitions of lts.

    source
    @[simp]
    theorem Cslib.LTS.reverse_canReach {State : Type u_1} {Label : Type u_2} {s s' : State} {lts : LTS State Label} :
    lts.reverse.CanReach s s' ↔ lts.CanReach s' s

    lts.reverse can reach s' from s iff lts can reach s from s'.

    source
    @[simp]
    theorem Cslib.LTS.reverse_unlabelledTr {State : Type u_1} {Label : Type u_2} {s s' : State} {lts : LTS State Label} :
    lts.reverse.UnlabelledTr s s' ↔ lts.UnlabelledTr s' s

    The unlabelled transitions of lts.reverse are those of lts with the endpoints swapped.

    source
    @[simp]
    theorem Cslib.LTS.reverse_image {State : Type u_1} {Label : Type u_2} {s : State} {μ : Label} {lts : LTS State Label} :
    lts.reverse.image s μ = {s' : State | lts.Tr s' μ s}

    The μ-image of a state in lts.reverse is its μ-preimage in lts.

    source
    theorem Cslib.LTS.mem_reverse_image {State : Type u_1} {Label : Type u_2} {s : State} {μ : Label} {s' : State} {lts : LTS State Label} :
    s' ∈ lts.reverse.image s μ ↔ s ∈ lts.image s' μ

    Membership form of reverse_image.

    source
    @[simp]
    theorem Cslib.LTS.reverse_imageMultistep {State : Type u_1} {Label : Type u_2} {s : State} {μs : List Label} {lts : LTS State Label} :
    lts.reverse.imageMultistep s μs = {s' : State | lts.MTr s' μs.reverse s}

    The μs-image of a state in lts.reverse is its μs.reverse-preimage in lts.

    source
    theorem Cslib.LTS.mem_reverse_imageMultistep {State : Type u_1} {Label : Type u_2} {s : State} {μs : List Label} {s' : State} {lts : LTS State Label} :
    s' ∈ lts.reverse.imageMultistep s μs ↔ s ∈ lts.imageMultistep s' μs.reverse

    Membership version of reverse_imageMultistep.

    source
    @[simp]
    theorem Cslib.LTS.reverse_hasOutLabel {State : Type u_1} {Label : Type u_2} {s : State} {μ : Label} {lts : LTS State Label} :
    lts.reverse.HasOutLabel s μ ↔ ∃ (s' : State), lts.Tr s' μ s

    A state has μ as an outgoing label in lts.reverse iff it has μ as an incoming label in lts.

    source
    @[simp]
    theorem Cslib.LTS.reverse_boundedUpTo {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {n : ℕ} :
    lts.reverse.BoundedUpTo n ↔ lts.BoundedUpTo n

    lts.reverse is bounded up to n iff lts is.

    source
    theorem Cslib.LTS.Execution.reverse {State : Type u_1} {Label : Type u_2} {s : State} {μs : List Label} {s' : State} {ss : List State} {lts : LTS State Label} (h : lts.Execution s μs s' ss) :
    lts.reverse.Execution s' μs.reverse s ss.reverse

    Reversing an execution of lts gives an execution of lts.reverse, with the labels, states and endpoints reversed.

    source
    @[simp]
    theorem Cslib.LTS.reverse_execution {State : Type u_1} {Label : Type u_2} {s : State} {μs : List Label} {s' : State} {ss : List State} {lts : LTS State Label} :
    lts.reverse.Execution s μs s' ss ↔ lts.Execution s' μs.reverse s ss.reverse

    An execution of lts.reverse is an execution of lts with the labels, states and endpoints reversed.