Changeset 2296 for src/RTLabs/Traces.ma

Timestamp:

Aug 13, 2012, 2:18:31 PM (7 years ago)

Author:

campbell

Message:

Tidy up some ill-placed definitions.

File:

• src/RTLabs/Traces.ma (modified) (5 diffs)

src/RTLabs/Traces.ma

@@ -4 +4 @@
 include "common/StructuredTraces.ma".
 include "common/Executions.ma".
+include "utilities/deqsets.ma".
 
 discriminator status_class.
@@ -146 +147 @@
 .
 
-(* TODO: move to pointers *)
-unification hint 0 ≔ ; D ≟ block_eq
-(*-----------------------------------------------------*)⊢
-block ≡ carr D.
-
 definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
 λx,y. match x with
@@ -161 +157 @@
 | rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
 ].
-
-(* TODO: move *)
-lemma eqb_elim : ∀D:DeqSet. ∀P:bool → Type[0]. ∀x,y:D.
-  (x = y → P true) →
-  (x ≠ y → P false) →
-  P (eqb D x y).
-#D #P #x #y #T #F lapply (eqb_true D x y) cases (eqb D x y) *
-[ #TT #_ @T @TT //
-| #_ #FF @F % #E destruct lapply (FF (refl ??)) #E destruct
-] qed.
 
 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).
 
-(* XXX move to semantics *)
-lemma final_cannot_move : ∀ge,s.
-  RTLabs_is_final s ≠ None ? →
-  ∃err. eval_statement ge s = Wrong ??? err.
-#ge *
-[ #f #fs #m * #F cases (F ?) @refl
-| #a #b #c #d #e * #F cases (F ?) @refl
-| #a #b #c #d * #F cases (F ?) @refl
-| #r #F % [2: @refl | skip ]
-] qed.
-
 let corec flat_traces_are_determined_by_starting_point ge s tr1
 : ∀tr2. equal_flat_traces ge s tr1 tr2 ≝ 
@@ -2403 +2378 @@
 qed.
 
-(* XXX move *)
-lemma step_not_final : ∀ge,s,tr,s'.
-  eval_statement ge s = Value … 〈tr,s'〉 →
-  RTLabs_is_final s = None ?.
-#ge #s #tr #s' #EX
-lapply (final_cannot_move ge s)
-cases (RTLabs_is_final s)
-[ // | #r #F cases (F ?) [ #m #E >E in EX; #EX destruct | % #E destruct ]
-qed.
-
 lemma tal_not_final : ∀ge,fl,s1,s2.
   ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.