Ignore:
Timestamp:
Nov 7, 2012, 4:42:02 PM (8 years ago)
Author:
campbell
Message:

Get a proper reverse mapping of function blocks to identifiers by getting
rid of shadowing.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2420 r2439  
    326326  ].
    327327
     328(* Remove an entry from a map (and leave it equivalent, otherwise) *)
     329definition remove : ∀tag,A. identifier_map tag A → identifier tag → identifier_map tag A ≝
     330λtag,A,m,id. an_id_map tag A (pm_set A (match id with [ an_identifier p ⇒ p ]) (None ?)
     331                                       (match m with [ an_id_map m ⇒ m ])).
     332
     333lemma lookup_remove_hit : ∀tag,A,m,id.
     334  lookup tag A (remove tag A m id) id = None ?.
     335#tag #A * #m * #id @lookup_opt_pm_set_hit
     336qed.
     337
     338lemma lookup_remove_miss : ∀tag,A,m,id,id'.
     339  id ≠ id' →
     340  lookup tag A (remove tag A m id') id = lookup tag A m id.
     341#tag #A * #m * #id * #id' #NE
     342@lookup_opt_pm_set_miss
     343/2/
     344qed.
     345
    328346(* Fold over the entries in a map.  There are some lemmas to help reason about
    329347   this near the bottom of the file (they require sets). *)
     
    365383| * #id' #a' normalize #E destruct %
    366384] qed.
     385
     386lemma find_none : ∀tag,A,m,p,id,a.
     387  find tag A m p = None ? →
     388  lookup … m id = Some ? a →
     389  ¬ p id a.
     390#tag #A * #m #p * #id #a #FIND
     391@(pm_find_none A m (λid. p (an_identifier tag id)))
     392whd in FIND:(??%?); cases (pm_find ???) in FIND ⊢ %;
     393[ normalize #E destruct %
     394| * #id' #a' normalize #E destruct
     395] qed.
     396
    367397
    368398lemma find_predicate : ∀tag,A,m,p,id,a.
Note: See TracChangeset for help on using the changeset viewer.