Changeset 1092 for src/common


Ignore:
Timestamp:
Jul 28, 2011, 12:14:37 PM (8 years ago)
Author:
campbell
Message:

Some minor definitions for identifiers and lists.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1077 r1092  
    139139  ].
    140140
    141 axiom foldi:
     141definition foldi:
    142142  ∀A, B: Type[0].
    143143  ∀tag: String.
    144   (identifier tag -> A -> B -> B) -> identifier_map tag A -> B -> B.
     144  (identifier tag -> A -> B -> B) -> identifier_map tag A -> B -> B ≝
     145λA,B,tag,f,m,b.
     146  match m with
     147  [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ].
    145148
    146149(* Sets *)
     
    152155λtag. an_id_set tag (Stub unit 16).
    153156
    154 definition add_set : ∀tag:String. identifier_set tag → identifier tag → identifier_set tag ≝
    155 λtag,s,i. an_id_set tag (insert unit 16 (match i with [ an_identifier i' ⇒ i' ])
    156                                      it (match s with [ an_id_set s' ⇒ s' ])).
     157let rec add_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : identifier_set tag ≝
     158  an_id_set tag (insert unit 16 (match i with [ an_identifier i' ⇒ i' ])
     159                             it (match s with [ an_id_set s' ⇒ s' ])).
    157160
    158161definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
    159162λtag,i. add_set tag (empty_set tag) i.
    160163
    161 definition mem_set : ∀tag:String. identifier_set tag → identifier tag → bool ≝
    162 λtag,s,i. match lookup_opt ? 16 (match i with [ an_identifier i' ⇒ i' ])
    163                                 (match s with [ an_id_set s' ⇒ s' ]) with
    164           [ None ⇒ false
    165           | Some _ ⇒ true
    166           ].
     164let rec mem_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : bool ≝
     165  match lookup_opt ? 16 (match i with [ an_identifier i' ⇒ i' ])
     166                        (match s with [ an_id_set s' ⇒ s' ]) with
     167  [ None ⇒ false
     168  | Some _ ⇒ true
     169  ].
    167170
    168 definition union_set : ∀tag:String. identifier_set tag → identifier_set tag → identifier_set tag ≝
    169 λtag,s,s'. an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
    170                                         (match s' with [ an_id_set s1 ⇒ s1 ])).
     171let rec union_set (tag:String) (s:identifier_set tag) (s':identifier_set tag) on s : identifier_set tag ≝
     172  an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
     173                               (match s' with [ an_id_set s1 ⇒ s1 ])).
    171174
    172175interpretation "identifier set union" 'union a b = (union_set ? a b).
     
    174177interpretation "empty identifier set" 'empty = (empty_set ?).
    175178interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
     179interpretation "identifier set membership" 'mem a b = (mem_set ? b a).
     180
     181lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
     182#tag * //
     183qed.
     184
     185lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
     186#tag * #s cases (BitVectorTrie_Sn … s)
     187[ * #x * #y #E >E //
     188| #E >E //
     189] qed.
Note: See TracChangeset for help on using the changeset viewer.