Documentation

Cslib.Foundations.Semantics.LTS.Union

Union of LTSs #

Note: there is a nontrivial balance between ergonomics and generality here. These definitions might change in the future.

source
def Cslib.LTS.union {State : Type u} {Label : Type v} (lts1 lts2 : LTS State Label) :
LTS State Label

The union of two LTSs defined on the same types.

Equations
Instances For
    source
    def Cslib.LTS.unionSubtype {State : Type u} {Label : Type v} {S1 : State → Prop} {L1 : Label → Prop} {S2 : State → Prop} {L2 : Label → Prop} (lts1 : LTS (Subtype S1) (Subtype L1)) (lts2 : LTS (Subtype S2) (Subtype L2)) :
    LTS State Label

    The union of two LTSs that have common supertypes for states and labels.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Cslib.LTS.inl {State : Type u} {Label : Type v} {State' : Type u_1} (lts : LTS State Label) :
      LTS { x : State ⊕ State' // x.isLeft = true } { _label : Label // True }

      Lifting of an LTS State Label to LTS (State ⊕ State') Label.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Cslib.LTS.inr {State : Type u} {Label : Type v} {State' : Type u_1} (lts : LTS State Label) :
        LTS { x : State' ⊕ State // x.isRight = true } { _label : Label // True }

        Lifting of an LTS State Label to LTS (State' ⊕ State) Label.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Cslib.LTS.unionSum {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} (lts1 : LTS State1 Label) (lts2 : LTS State2 Label) :
          LTS (State1 ⊕ State2) Label

          Union of two LTSs with the same Label type. The result combines the original respective state types State1 and State2 into (State1 ⊕ State2).

          Equations
          Instances For
            source
            @[simp]
            theorem Cslib.LTS.unionSum_tr_inl_inl {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} {lts1 : LTS State1 Label} {lts2 : LTS State2 Label} {s s' : State1} {μ : Label} :
            (lts1.unionSum lts2).Tr (Sum.inl s) μ (Sum.inl s') ↔ lts1.Tr s μ s'
            source
            @[simp]
            theorem Cslib.LTS.unionSum_tr_inr_inr {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} {lts1 : LTS State1 Label} {lts2 : LTS State2 Label} {s s' : State2} {μ : Label} :
            (lts1.unionSum lts2).Tr (Sum.inr s) μ (Sum.inr s') ↔ lts2.Tr s μ s'
            source
            @[simp]
            theorem Cslib.LTS.unionSum_not_tr_inl_inr {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} {lts1 : LTS State1 Label} {lts2 : LTS State2 Label} {s : State1} {s' : State2} {μ : Label} :
            ¬(lts1.unionSum lts2).Tr (Sum.inl s) μ (Sum.inr s')
            source
            @[simp]
            theorem Cslib.LTS.unionSum_not_tr_inr_inl {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} {lts1 : LTS State1 Label} {lts2 : LTS State2 Label} {s : State2} {s' : State1} {μ : Label} :
            ¬(lts1.unionSum lts2).Tr (Sum.inr s) μ (Sum.inl s')
            source
            theorem Cslib.LTS.unionSum_mTr_inl {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} {lts1 : LTS State1 Label} {lts2 : LTS State2 Label} {s : State1} {μs : List Label} {y : State1 ⊕ State2} (h : (lts1.unionSum lts2).MTr (Sum.inl s) μs y) :
            ∃ (t : State1), y = Sum.inl t ∧ lts1.MTr s μs t

            A run of unionSum lts1 lts2 from a state of lts1 stays among the states of lts1, where it is a run of lts1.

            source
            theorem Cslib.LTS.unionSum_mTr_inr {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} {lts1 : LTS State1 Label} {lts2 : LTS State2 Label} {s : State2} {μs : List Label} {y : State1 ⊕ State2} (h : (lts1.unionSum lts2).MTr (Sum.inr s) μs y) :
            ∃ (t : State2), y = Sum.inr t ∧ lts2.MTr s μs t

            A run of unionSum lts1 lts2 from a state of lts2 stays among the states of lts2, where it is a run of lts2.

            source
            theorem Cslib.LTS.unionSum_mTr_inl_iff {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} {lts1 : LTS State1 Label} {lts2 : LTS State2 Label} {s t : State1} {μs : List Label} :
            (lts1.unionSum lts2).MTr (Sum.inl s) μs (Sum.inl t) ↔ lts1.MTr s μs t

            The runs of unionSum lts1 lts2 between states of lts1 are the runs of lts1.

            source
            theorem Cslib.LTS.unionSum_mTr_inr_iff {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} {lts1 : LTS State1 Label} {lts2 : LTS State2 Label} {s t : State2} {μs : List Label} :
            (lts1.unionSum lts2).MTr (Sum.inr s) μs (Sum.inr t) ↔ lts2.MTr s μs t

            The runs of unionSum lts1 lts2 between states of lts2 are the runs of lts2.