Changeset 2203 for src/Clight/Cexec.ma


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/Clight/Cexec.ma

    r2176 r2203  
    551551definition clight_fullexec : fullexec io_out io_in ≝
    552552  mk_fullexec ??? clight_exec make_global make_initial_state.
     553
     554
     555(* A few lemmas about the semantics. *)
     556
     557lemma cl_step_not_final : ∀ge,s1,tr,s2.
     558  exec_step ge s1 = OK … 〈tr,s2〉 →
     559  is_final s1 = None ?.
     560#ge * //
     561#r #tr #s2 #E
     562whd in E:(??%%);
     563destruct
     564qed.
     565
     566(* If you can step in Clight, then you aren't in a final state.  Hence we can
     567   give nicer constructors for plus. *)
     568lemma cl_plus_one : ∀ge,s1,tr,s2.
     569  exec_step ge s1 = OK … 〈tr,s2〉 →
     570  plus … clight_exec ge s1 tr s2.
     571#ge #s1 #tr #s2 #EX @(plus_one … EX) /2/
     572qed.
     573
     574lemma cl_plus_succ : ∀ge,s1,tr,s2,tr',s3.
     575    exec_step ge s1 = OK … 〈tr,s2〉 →
     576    plus … clight_exec ge s2 tr' s3 →
     577    plus … clight_exec ge s1 (tr⧺tr') s3.
     578#ge #s1 #tr #s2 #tr' #s3 #EX @plus_succ /2/ @EX
     579qed.
     580
Note: See TracChangeset for help on using the changeset viewer.