chore: move Relation- and Trans-related defs about LTS upwards

Cslib/Foundations/Semantics/LTS/Basic.lean

@@ -57,6 +57,15 @@ structure LTS (State : Type u) (Label : Type v) where
   /-- The transition relation. -/
   Tr : State → Label → State → Prop
 
+/-- Returns the relation that relates all states `s1` and `s2` via a fixed transition label `μ`. -/
+def LTS.Tr.toRelation (lts : LTS State Label) (μ : Label) : State → State → Prop :=
+  fun s1 s2 => lts.Tr s1 μ s2
+
+/-- Any homogeneous relation can be seen as an LTS where all transitions have the same label. -/
+def Relation.toLTS [DecidableEq Label] (r : State → State → Prop) (μ : Label) :
+  LTS State Label where
+  Tr := fun s1 μ' s2 => if μ' = μ then r s1 s2 else False
+
 section MultiStep
 
 /-! ## Multi-step transitions -/
@@ -158,6 +167,57 @@ theorem LTS.CanReach.refl (s : State) : lts.CanReach s s := by
 def LTS.generatedBy (s : State) : LTS {s' : State // lts.CanReach s s'} Label where
   Tr := fun s1 μ s2 => lts.CanReach s s1 ∧ lts.CanReach s s2 ∧ lts.Tr s1 μ s2
 
+/-- Returns the relation that relates all states `s1` and `s2` via a fixed list of transition
+labels `μs`. -/
+def LTS.MTr.toRelation (lts : LTS State Label) (μs : List Label) : State → State → Prop :=
+  fun s1 s2 => lts.MTr s1 μs s2
+
+/-! ### Calc tactic support for MTr -/
+
+/-- Transitions can be chained. -/
+instance (lts : LTS State Label) :
+  Trans
+    (LTS.Tr.toRelation lts μ1)
+    (LTS.Tr.toRelation lts μ2)
+    (LTS.MTr.toRelation lts [μ1, μ2]) where
+  trans := by
+    intro s1 s2 s3 htr1 htr2
+    apply LTS.MTr.single at htr1
+    apply LTS.MTr.single at htr2
+    apply LTS.MTr.comp lts htr1 htr2
+
+/-- Transitions can be chained with multi-step transitions. -/
+instance (lts : LTS State Label) :
+  Trans
+    (LTS.Tr.toRelation lts μ)
+    (LTS.MTr.toRelation lts μs)
+    (LTS.MTr.toRelation lts (μ :: μs)) where
+  trans := by
+    intro s1 s2 s3 htr1 hmtr2
+    apply LTS.MTr.single at htr1
+    apply LTS.MTr.comp lts htr1 hmtr2
+
+/-- Multi-step transitions can be chained with transitions. -/
+instance (lts : LTS State Label) :
+  Trans
+    (LTS.MTr.toRelation lts μs)
+    (LTS.Tr.toRelation lts μ)
+    (LTS.MTr.toRelation lts (μs ++ [μ])) where
+  trans := by
+    intro s1 s2 s3 hmtr1 htr2
+    apply LTS.MTr.single at htr2
+    apply LTS.MTr.comp lts hmtr1 htr2
+
+/-- Multi-step transitions can be chained. -/
+instance (lts : LTS State Label) :
+  Trans
+    (LTS.MTr.toRelation lts μs1)
+    (LTS.MTr.toRelation lts μs2)
+    (LTS.MTr.toRelation lts (μs1 ++ μs2)) where
+  trans := by
+    intro s1 s2 s3 hmtr1 hmtr2
+    apply LTS.MTr.comp lts hmtr1 hmtr2
+
 end MultiStep
 
 section Termination
@@ -580,74 +640,6 @@ class LTS.DivergenceFree [HasTau Label] (lts : LTS State Label) where
 
 end Divergence
 
-section Relation
-
-/-- Returns the relation that relates all states `s1` and `s2` via a fixed transition label `μ`. -/
-def LTS.Tr.toRelation (lts : LTS State Label) (μ : Label) : State → State → Prop :=
-  fun s1 s2 => lts.Tr s1 μ s2
-
-/-- Returns the relation that relates all states `s1` and `s2` via a fixed list of transition
-labels `μs`. -/
-def LTS.MTr.toRelation (lts : LTS State Label) (μs : List Label) : State → State → Prop :=
-  fun s1 s2 => lts.MTr s1 μs s2
-
-/-- Any homogeneous relation can be seen as an LTS where all transitions have the same label. -/
-def Relation.toLTS [DecidableEq Label] (r : State → State → Prop) (μ : Label) :
-  LTS State Label where
-  Tr := fun s1 μ' s2 => if μ' = μ then r s1 s2 else False
-
-end Relation
-
-section Trans
-
-/-! ## Support for the calc tactic -/
-
-/-- Transitions can be chained. -/
-instance (lts : LTS State Label) :
-  Trans
-    (LTS.Tr.toRelation lts μ1)
-    (LTS.Tr.toRelation lts μ2)
-    (LTS.MTr.toRelation lts [μ1, μ2]) where
-  trans := by
-    intro s1 s2 s3 htr1 htr2
-    apply LTS.MTr.single at htr1
-    apply LTS.MTr.single at htr2
-    apply LTS.MTr.comp lts htr1 htr2
-
-/-- Transitions can be chained with multi-step transitions. -/
-instance (lts : LTS State Label) :
-  Trans
-    (LTS.Tr.toRelation lts μ)
-    (LTS.MTr.toRelation lts μs)
-    (LTS.MTr.toRelation lts (μ :: μs)) where
-  trans := by
-    intro s1 s2 s3 htr1 hmtr2
-    apply LTS.MTr.single at htr1
-    apply LTS.MTr.comp lts htr1 hmtr2
-
-/-- Multi-step transitions can be chained with transitions. -/
-instance (lts : LTS State Label) :
-  Trans
-    (LTS.MTr.toRelation lts μs)
-    (LTS.Tr.toRelation lts μ)
-    (LTS.MTr.toRelation lts (μs ++ [μ])) where
-  trans := by
-    intro s1 s2 s3 hmtr1 htr2
-    apply LTS.MTr.single at htr2
-    apply LTS.MTr.comp lts hmtr1 htr2
-
-/-- Multi-step transitions can be chained. -/
-instance (lts : LTS State Label) :
-  Trans
-    (LTS.MTr.toRelation lts μs1)
-    (LTS.MTr.toRelation lts μs2)
-    (LTS.MTr.toRelation lts (μs1 ++ μs2)) where
-  trans := by
-    intro s1 s2 s3 hmtr1 hmtr2
-    apply LTS.MTr.comp lts hmtr1 hmtr2
-
-end Trans
-
 open Lean Elab Meta Command Term
 
 /-- A command to create an `LTS` from a labelled transition `α → β → α → Prop`, robust to use of