Download

 Note: You may already have this library installed. It is distributed
in the books/finitesettheory/osets directory of ACL2 2.9.3
through 3.0.
 This version mainly includes speed enhancements over Version 0.9. See
the Changelog for
details.
Quick Guide
When you run (includebook "sets"), you will have
the following functions. Note that all of these functions are
in the SETS package!
 (setp X)  test for if X is a set or not.
 (sfix X)  identity on sets, nil on nonsets.
 (empty X)  is X an empty set?
 (head X)  "smallest" element in a set (think of car)
 (tail X)  "all but smallest" elements of a set (think of
cdr)
 (insert a X)  insert a into X.
 (delete a X)  delete a from X.
 (in a X)  test if a is in X.
 (subset X Y)  test if X is a subset of
Y.
 (union X Y)  union of X and Y.
 (intersect X Y)  intersection of X and Y.
 (difference X Y)  difference of X and Y.
 (cardinality X)  number of elements in X.
 (inlist a x)  returns t if a is a member of
the list x, or nil otherwise.
 (mergesort x)  create a set with all elements in list
x.
There are also some optional extensions to the library. You can include
quantify.lisp to introduce notions
of quantifying over set elements. You can also include
map.lisp to introduce mappings between
sets and lists. Putting these ideas together can be fairly powerful,
as this simple graph.lisp script observes.
Documentation
If you want to use the sets library to do nontrivial things, you
will probably want to read some more thorough documentation of it.

 This paper discussed the library's organization and design, and is
probably the best thing to read to learn about the library.
Presentations


 These are a little dated, but still fairly accurate. There was
some confusion about nested sets during this talk, so I have also
written some Notes on Nested Sets
which compares J's unordered sets library with osets with respect
to handling nested sets.
Source Code

Browse Source (stable version)
This just gives you the Apache file listing.

 Anonymous SVN access is also available. Run svn
checkout svn://dimebox.cs.utexas.edu/u/jared/Subversion/osets/trunk
osets