Ignore:
Timestamp:
Jul 17, 2012, 6:57:40 PM (8 years ago)
Author:
campbell
Message:

A general result about simulations of executions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r2202 r2203  
    1919         repeat n' ?? exec g s1
    2020].
     21
     22(* We take care here to check that we're not at the final state.  It is not
     23   necessarily the case that a success step guarantees this (e.g., because
     24   there may be no way to stop a processor, so an infinite loop is used
     25   instead). *)
     26inductive plus (O) (I) (TS:trans_system O I) (ge:global … TS) : state … TS ge → trace → state … TS ge → Prop ≝
     27| plus_one : ∀s1,tr,s2.
     28    is_final … TS ge s1 = None ? →
     29    step … TS ge s1 = OK … 〈tr,s2〉 →
     30    plus … ge s1 tr s2
     31| plus_succ : ∀s1,tr,s2,tr',s3.
     32    is_final … TS ge s1 = None ? →
     33    step … TS ge s1 = OK … 〈tr,s2〉 →
     34    plus … ge s2 tr' s3 →
     35    plus … ge s1 (tr⧺tr') s3.
     36
     37lemma plus_not_final : ∀O,I,FE. ∀gl,s,tr,s'.
     38  plus O I FE gl s tr s' →
     39  is_final … FE gl s = None ?.
     40#O #I #FE #gl #s0 #tr0 #s0' * //
     41qed.
    2142
    2243let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
Note: See TracChangeset for help on using the changeset viewer.