Changeset 2118 for src/common
 Timestamp:
 Jun 27, 2012, 12:04:27 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/SmallstepExec.ma
r1599 r2118 80 80 *) 81 81 82 lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r. 83 exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' → 84 step … ge s = Value … 〈tr, s'〉 ∧ 85 is_final … s' = Some ? r. 86 #O #I #TS #ge #s #s' #tr #r 87 >exec_inf_aux_unfold 88 cases (step … ge s) 89 [ 1,3: normalize #H1 #H2 try #H3 destruct 90  * #tr' #s'' 91 whd in ⊢ (??%? → ?); 92 lapply (refl ? (is_final … s'')) 93 cases (is_final … s'') in ⊢ (???% → %); 94 [ #_ whd in ⊢ (??%? → ?); #E destruct 95  #r' #E1 #E2 whd in E2:(??%?); destruct % // 96 ] 97 ] qed. 98 99 lemma extract_step : ∀O,I,TS,ge,s,s',tr,e. 100 exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e → 101 step … ge s = Value … 〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s'). 102 #O #I #TS #ge #s #s' #tr #e 103 >exec_inf_aux_unfold 104 cases (step … s) 105 [ 1,3: normalize #H1 #H2 try #H3 destruct 106  * #tr' #s'' 107 whd in ⊢ (??%? → ?); 108 cases (is_final … s'') 109 [ #E normalize in E; destruct /2/ 110  #r #E normalize in E; destruct 111 ] 112 ] qed. 113 114 lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e. 115 exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e → 116 is_final … s' = None ?. 117 #O #I #TS #ge #s #s' #tr #e 118 >exec_inf_aux_unfold 119 cases (step … s) 120 [ 1,3: normalize #H1 #H2 try #H3 destruct 121  * #tr' #s'' 122 whd in ⊢ (??%? → ?); 123 lapply (refl ? (is_final … s'')) 124 cases (is_final … s'') in ⊢ (???% → %); 125 [ #F whd in ⊢ (??%? → ?); #E destruct @F 126  #r' #_ #E whd in E:(??%?); destruct 127 ] 128 ] qed. 129 130 131 82 132 record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝ 83 133 { program : Type[0]
Note: See TracChangeset
for help on using the changeset viewer.