Changeset 2314 for src/common


Ignore:
Timestamp:
Aug 31, 2012, 4:12:35 PM (7 years ago)
Author:
campbell
Message:

Move generic definitions from recent commit to appropriate places.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2307 r2314  
    347347] qed.
    348348
     349lemma present_member : ∀tag,A,m,id.
     350  present tag A m id → member tag A m id.
     351#tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??))
     352qed.
     353
    349354definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
    350355λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
     
    988993qed.
    989994 
    990 
     995(* Link a map with the set consisting of its domain. *)
     996
     997definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
     998λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])).
     999
     1000lemma id_set_of_map_subset : ∀tag,A,m.
     1001  id_set_of_map tag A m ⊆ m.
     1002#tag #A * #m * #id normalize
     1003>lookup_opt_map normalize cases (lookup_opt ???) //
     1004qed.
     1005
     1006lemma id_set_of_map_present : ∀tag,A,m,id.
     1007  present tag A m id ↔ present tag unit (id_set_of_map … m) id.
     1008#tag #A * #m * #id %
     1009normalize @not_to_not
     1010>lookup_opt_map cases (lookup_opt ???) normalize //
     1011#a #E destruct
     1012qed.
     1013
     1014lemma id_set_of_map_card : ∀tag,A,m.
     1015  |m| = |id_set_of_map tag A m|.
     1016#tag #A * #m whd in ⊢ (??%%); >map_size //
     1017qed.
     1018
     1019
     1020
Note: See TracChangeset for help on using the changeset viewer.