Changeset 1562 for src/common/Identifiers.ma

Timestamp:

Nov 25, 2011, 1:20:41 PM (9 years ago)

Author:

mulligan

Message:

new version of assembly, fixed conflict in positivemap.ma, changed erroneous axiom in identifiers.ma

File:

• src/common/Identifiers.ma (modified) (3 diffs)

src/common/Identifiers.ma

@@ -59 +59 @@
 qed.
 
+axiom eq_identifier_sym:
+  ∀tag: String.
+  ∀l  : identifier tag.
+  ∀r  : identifier tag.
+    eq_identifier tag l r = eq_identifier tag r l.
+
 lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
 #tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/
@@ -105 +111 @@
 qed.
 
+lemma lookup_def_add_hit : ∀tag,A,m,i,a,d.
+  lookup_def tag A (add tag A m i a) i d = a.
+#tag #A * #m * #i #a #d
+@lookup_insert_hit
+qed.
+
 lemma lookup_add_miss : ∀tag,A,m,i,j,a.
   i ≠ j →
@@ -111 +123 @@
 @lookup_opt_insert_miss /2/
 qed.
+
+axiom lookup_def_add_miss : ∀tag,A,m,i,j,a,d.
+  i ≠ j →
+  lookup_def tag A (add tag A m j a) i d = lookup_def tag A m i d.
 
 lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.