Changeset 1092


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

Some minor definitions for identifiers and lists.

Location:
src
Files:
2 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.
  • src/utilities/lists.ma

    r816 r1092  
    99let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
    1010match l with
    11 [ nil ⇒ False
     11[ nil ⇒ True
    1212| cons h t ⇒ P h ∧ All A P t
    1313].
     14
     15lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
     16#A #P #Q #H #l elim l normalize //
     17#h #t #IH * /3/
     18qed.
    1419
    1520let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
     
    1823| cons h t ⇒ orb (p h) (exists A p t)
    1924].
     25
     26let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
     27match l with
     28[ nil ⇒ False
     29| cons h t ⇒ (P h) ∨ (Exists A P t)
     30].
     31
     32lemma Exists_append : ∀A,P,l1,l2.
     33  Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
     34#A #P #l1 elim l1
     35[ normalize /2/
     36| #h #t #IH #l2 *
     37  [ #H /3/
     38  | #H cases (IH l2 H) /3/
     39  ]
     40] qed.
     41
     42lemma map_append : ∀A,B,f,l1,l2.
     43  (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
     44#A #B #f #l1 elim l1
     45[ #l2 @refl
     46| #h #t #IH #l2 normalize //
     47] qed.
Note: See TracChangeset for help on using the changeset viewer.