Changeset 2296 for src/RTLabs
 Timestamp:
 Aug 13, 2012, 2:18:31 PM (7 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2295 r2296 4 4 include "common/StructuredTraces.ma". 5 5 include "common/Executions.ma". 6 include "utilities/deqsets.ma". 6 7 7 8 discriminator status_class. … … 146 147 . 147 148 148 (* TODO: move to pointers *)149 unification hint 0 ≔ ; D ≟ block_eq150 (**)⊢151 block ≡ carr D.152 153 149 definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝ 154 150 λx,y. match x with … … 161 157  rapc_fin ⇒ match y with [ rapc_fin ⇒ true  _ ⇒ false ] 162 158 ]. 163 164 (* TODO: move *)165 lemma eqb_elim : ∀D:DeqSet. ∀P:bool → Type[0]. ∀x,y:D.166 (x = y → P true) →167 (x ≠ y → P false) →168 P (eqb D x y).169 #D #P #x #y #T #F lapply (eqb_true D x y) cases (eqb D x y) *170 [ #TT #_ @T @TT //171  #_ #FF @F % #E destruct lapply (FF (refl ??)) #E destruct172 ] qed.173 159 174 160 definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?. … … 2213 2199  eft_step : ∀s,tr,s',EX,tr1,tr2. equal_flat_traces ge s' tr1 tr2 → equal_flat_traces ge s (ft_step … EX tr1) (ft_step … s tr s' EX tr2). 2214 2200 2215 (* XXX move to semantics *)2216 lemma final_cannot_move : ∀ge,s.2217 RTLabs_is_final s ≠ None ? →2218 ∃err. eval_statement ge s = Wrong ??? err.2219 #ge *2220 [ #f #fs #m * #F cases (F ?) @refl2221  #a #b #c #d #e * #F cases (F ?) @refl2222  #a #b #c #d * #F cases (F ?) @refl2223  #r #F % [2: @refl  skip ]2224 ] qed.2225 2226 2201 let corec flat_traces_are_determined_by_starting_point ge s tr1 2227 2202 : ∀tr2. equal_flat_traces ge s tr1 tr2 ≝ … … 2403 2378 qed. 2404 2379 2405 (* XXX move *)2406 lemma step_not_final : ∀ge,s,tr,s'.2407 eval_statement ge s = Value … 〈tr,s'〉 →2408 RTLabs_is_final s = None ?.2409 #ge #s #tr #s' #EX2410 lapply (final_cannot_move ge s)2411 cases (RTLabs_is_final s)2412 [ //  #r #F cases (F ?) [ #m #E >E in EX; #EX destruct  % #E destruct ]2413 qed.2414 2415 2380 lemma tal_not_final : ∀ge,fl,s1,s2. 2416 2381 ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2. 
src/RTLabs/semantics.ma
r2295 r2296 352 352 ] qed. 353 353 354 lemma final_cannot_move : ∀ge,s. 355 RTLabs_is_final s ≠ None ? → 356 ∃err. eval_statement ge s = Wrong ??? err. 357 #ge * 358 [ #f #fs #m * #F cases (F ?) @refl 359  #a #b #c #d #e * #F cases (F ?) @refl 360  #a #b #c #d * #F cases (F ?) @refl 361  #r #F % [2: @refl  skip ] 362 ] qed. 363 364 lemma step_not_final : ∀ge,s,tr,s'. 365 eval_statement ge s = Value … 〈tr,s'〉 → 366 RTLabs_is_final s = None ?. 367 #ge #s #tr #s' #EX 368 lapply (final_cannot_move ge s) 369 cases (RTLabs_is_final s) 370 [ //  #r #F cases (F ?) [ #m #E >E in EX; #EX destruct  % #E destruct ] 371 qed. 354 372 355 373 lemma initial_state_is_not_final : ∀p,s.
Note: See TracChangeset
for help on using the changeset viewer.