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

Tidy up some ill-placed definitions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.