include "extralib.ma".
include "IOMonad.ma".
include "Integers.ma".
include "Events.ma".

nrecord execstep : Type[1] ≝
{ genv  : Type
; state : Type
; io : interaction
; initial : state → Prop
; final : state → int → Prop
; step : genv → state → IO io (trace×state)
}.

nlet rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec)
 : IO (io exec) (trace × (state exec)) ≝
match n with
[ O ⇒ Value ?? 〈E0, s〉
| S n' ⇒ ! 〈t1,s1〉 ← step exec g s;:
         repeat n' exec g s1
].

alias symbol "and" (instance 2) = "logical and".
nrecord related_semantics : Type[1] ≝
{ sem1 : execstep
; sem2 : execstep
; ge1 : genv sem1
; ge2 : genv sem2
; match_states : state sem1 → state sem2 → Prop
; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2
; match_final_states : ∀st1,st2,r. match_states st1 st2 → (final sem1) st1 r → (final sem2) st2 r
}.



nrecord simulation : Type[1] ≝ 
{ sems :> related_semantics
; sim : ∀st1,st2,t,st1'.
        P_io' (io (sem1 sems)) (trace × (state (sem1 sems))) (λr. r = 〈t,st1'〉) (step (sem1 sems) (ge1 sems) st1) →
        match_states sems st1 st2 → 
        ∃st2':(state (sem2 sems)).(∃n:nat.P_io' (io (sem2 sems)) (trace × (state (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n (sem2 sems) (ge2 sems) st2)) ∧
          match_states sems st1' st2'
}.