Changeset 1535 for src/common

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:

• src/common/Identifiers.ma (modified) (1 diff)

src/common/Identifiers.ma

@@ -173 +173 @@
 λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
 cases H #H'  cases (H' (refl ??)) qed.
+
+lemma lookup_lookup_present : ∀tag,A,m,id,p.
+  lookup tag A m id = Some ? (lookup_present tag A m id p).
+#tag #A #m #id #p
+whd in p ⊢ (???(??%));
+cases (lookup tag A m id) in p ⊢ %;
+[ * #H @⊥ @H @refl
+| #a #H @refl
+] qed.
 
 definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝