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' }.