Ignore:
Timestamp:
Nov 23, 2011, 12:07:01 PM (9 years ago)
Author:
campbell
Message:

Make RTLabs semantics use knowledge that the next instruction always
exists. (Makes statements involving RTLabs execution easier.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1516 r1535  
    173173λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
    174174cases H #H'  cases (H' (refl ??)) qed.
     175
     176lemma lookup_lookup_present : ∀tag,A,m,id,p.
     177  lookup tag A m id = Some ? (lookup_present tag A m id p).
     178#tag #A #m #id #p
     179whd in p ⊢ (???(??%));
     180cases (lookup tag A m id) in p ⊢ %;
     181[ * #H @⊥ @H @refl
     182| #a #H @refl
     183] qed.
    175184
    176185definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
Note: See TracChangeset for help on using the changeset viewer.