Changeset 2685 for src/common/SmallstepExec.ma
 Timestamp:
 Feb 21, 2013, 11:38:36 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/SmallstepExec.ma
r2682 r2685 540 540 qed. 541 541 542 lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'. 543 exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 → 544 s = s1. 545 #n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC 546 lapply (exec_steps_length … EXEC) #E normalize in E; destruct 547 cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct 548 % 549 qed. 550 542 551 lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P. 543 552 after_n_steps n O I fx g s inv P → 544 ∃trace,s'. exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ P (gather_trace ? trace) s'. 553 ∃trace,s'. 554 exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ 555 bool_to_Prop (all ? (λstr. inv (\fst str)) (tail … trace)) ∧ 556 P (gather_trace ? trace) s'. 545 557 #n elim n 546 [ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} % {(refl ??)} @AFTER558 [ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} % [ %{(refl ??)} %  @AFTER ] 547 559  #m #IH #O #I #fx #g #s #inv #P #AFTER 548 560 cases (after_1_of_n_steps … AFTER) 549 561 #tr1 * #s1 * * * #NF #STEP #INV #AFTER' 550 562 cases (IH … AFTER') 551 #tl * #s' * #STEPS#p563 #tl * #s' * * #STEPS #INV' #p 552 564 %{(〈s,tr1〉::tl)} %{s'} % 553 [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS %  // ] 565 [ % 566 [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % 567  cases tl in STEPS INV INV' ⊢ %; [ //  * #sx #trx #t #STEPS #INV #INV' 568 <(exec_steps_first … STEPS) whd in ⊢ (?%); >INV // 569 >(exec_steps_length … STEPS) % 570 ] 571 ] 572  // ] 554 573 ] qed. 555 574 … … 588 607 destruct % 589 608 ] qed. 590 591 lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'.592 exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 →593 s = s1.594 #n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC595 lapply (exec_steps_length … EXEC) #E normalize in E; destruct596 cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct597 %598 qed.599 609 600 610 (* Show that it corresponds to split_trace … (exec_inf …).
Note: See TracChangeset
for help on using the changeset viewer.