Ignore:
Timestamp:
Apr 8, 2011, 11:51:38 AM (9 years ago)
Author:
mulligan
Message:

Changes to bitvectortrieset: equality on sets. Added new file for translation of variable set functor. other small changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/BitVectorTrieSet.ma

    r698 r746  
    11include "ASM/BitVectorTrie.ma".
     2include "ASM/Util.ma".
    23
    34definition BitVectorTrieSet ≝ BitVectorTrie unit.
     
    5051qed.
    5152
     53let rec set_eq (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: bool ≝
     54  match b return λh. λ_. n = h → bool with
     55  [ Stub s ⇒
     56    match c with
     57    [ Stub s' ⇒ λ_. eq_nat s s'
     58    | _ ⇒ λ_. false
     59    ]
     60  | Leaf l ⇒
     61    match c with
     62    [ Leaf l' ⇒ λ_. true (* dpm: l and l' both unit *)
     63    | _ ⇒ λ_. false
     64    ]
     65  | Node h l r ⇒
     66    match c with
     67    [ Node h' l' r' ⇒ λprf. andb (set_eq h l ?) (set_eq h r ?)
     68    | _ ⇒ λ_. false
     69    ]
     70  ] (refl ? n).
     71  [ 1: @ r
     72  | 2: lapply (injective_S … prf)
     73       # H
     74       < H
     75       @ r'
     76  ]
     77qed.
     78
     79(*
     80let rec set_diff (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: BitVectorTrieSet n ≝
     81  match b with
     82  [ Stub ⇒
     83*)
     84
    5285definition set_insert ≝
    5386  λn: nat.
     
    5790
    5891definition set_empty ≝ λn. Stub unit n.
     92
     93definition set_singleton ≝
     94  λn: nat.
     95  λb: BitVector n.
     96    insert unit n b it (set_empty ?).
Note: See TracChangeset for help on using the changeset viewer.