Simulation

Conjectura.Defs.ComputerScience.Semantics.Simulation

/-
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Fabrizio Montesi
-/
import Conjectura.Defs.ComputerScience.Semantics.LabelledTransitionSystem

/-! # Simulation

## Source

Adapted for Conjectura from [cslib](https://github.com/leanprover/cslib), `Cslib/Foundations/Semantics/Lts/Simulation.lean`, split into one concept per module. Released by its authors under Apache 2.0.
-/

namespace Conjectura.Semantics

/-- A relation is a **simulation** when, whenever it relates two states, every transition of
the first can be matched by the second with the results still related — the second system can
do everything the first can. -/
def IsSimulation {S₁ S₂ Label : Type*}
    (lts₁ : LTS S₁ Label) (lts₂ : LTS S₂ Label) (r : S₁ → S₂ → Prop) : Prop :=
  ∀ ⦃s₁ s₂⦄, r s₁ s₂ → ∀ μ, ∀ t₁, lts₁.Tr s₁ μ t₁ → ∃ t₂, lts₂.Tr s₂ μ t₂ ∧ r t₁ t₂

end Conjectura.Semantics