Changeset 2418 for src/common


Ignore:
Timestamp:
Oct 29, 2012, 6:19:56 PM (7 years ago)
Author:
campbell
Message:

Add a checking function for the uniqueness of cost labels in RTLabs
programs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2415 r2418  
    494494lemma present_add_miss:
    495495  ∀tag, a, map, k, k', v.
    496     k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'.
    497   #tag #a #map #k #k' #v #neq_assm #present_assm
    498   whd >lookup_add_miss assumption
    499 qed.
     496    present tag a map k' → present tag a (add tag a map k v) k'.
     497  #tag #a #map #k #k' #v #present_assm
     498  whd @lookup_add_oblivious assumption
     499qed.
     500
     501lemma present_add_cases: ∀tag,A,map,k,v,k'.
     502  present tag A (add tag A map k v) k' →
     503  k = k' ∨ (k ≠ k' ∧ present tag A map k').
     504#tag #A #map #k #v #k' normalize
     505cases (identifier_eq ? k k')
     506[ #E /2/
     507| #NE >lookup_add_miss /3/
     508] qed.
    500509
    501510
Note: See TracChangeset for help on using the changeset viewer.