Changeset 2296 for src/RTLabs


Ignore:
Timestamp:
Aug 13, 2012, 2:18:31 PM (7 years ago)
Author:
campbell
Message:

Tidy up some ill-placed definitions.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2295 r2296  
    44include "common/StructuredTraces.ma".
    55include "common/Executions.ma".
     6include "utilities/deqsets.ma".
    67
    78discriminator status_class.
     
    146147.
    147148
    148 (* TODO: move to pointers *)
    149 unification hint 0 ≔ ; D ≟ block_eq
    150 (*-----------------------------------------------------*)⊢
    151 block ≡ carr D.
    152 
    153149definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
    154150λx,y. match x with
     
    161157| rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
    162158].
    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 destruct
    172 ] qed.
    173159
    174160definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.
     
    22132199| 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).
    22142200
    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 ?) @refl
    2221 | #a #b #c #d #e * #F cases (F ?) @refl
    2222 | #a #b #c #d * #F cases (F ?) @refl
    2223 | #r #F % [2: @refl | skip ]
    2224 ] qed.
    2225 
    22262201let corec flat_traces_are_determined_by_starting_point ge s tr1
    22272202: ∀tr2. equal_flat_traces ge s tr1 tr2 ≝
     
    24032378qed.
    24042379
    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' #EX
    2410 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 
    24152380lemma tal_not_final : ∀ge,fl,s1,s2.
    24162381  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
  • src/RTLabs/semantics.ma

    r2295 r2296  
    352352] qed.
    353353
     354lemma 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
     364lemma 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
     368lapply (final_cannot_move ge s)
     369cases (RTLabs_is_final s)
     370[ // | #r #F cases (F ?) [ #m #E >E in EX; #EX destruct | % #E destruct ]
     371qed.
    354372
    355373lemma initial_state_is_not_final : ∀p,s.
Note: See TracChangeset for help on using the changeset viewer.