Changeset 2203 for src/Clight/Cexec.ma
 Timestamp:
 Jul 17, 2012, 6:57:40 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Cexec.ma
r2176 r2203 551 551 definition clight_fullexec : fullexec io_out io_in ≝ 552 552 mk_fullexec ??? clight_exec make_global make_initial_state. 553 554 555 (* A few lemmas about the semantics. *) 556 557 lemma 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 562 whd in E:(??%%); 563 destruct 564 qed. 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. *) 568 lemma 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/ 572 qed. 573 574 lemma 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 579 qed. 580
Note: See TracChangeset
for help on using the changeset viewer.