Finite Set Theory based on Fully Ordered Lists

SetsOrdered Sets

This is a finite set theory implementation for ACL2 based on fully ordered lists.

  • Set equality is just equal.
  • Pick-a-point approaches are automatically suggested during proofs of subset relations.

The set operations have been efficiently implemented with MBE and Guards.

  • Subset, union, intersect, and difference are linear time.
  • An efficient mergesort has been provided.
  • Set operations are tail recursive.

The library is freely available under the terms of the GNU General Public License.


Download Version 0.91 is now available.
BZipped Tar File; 53 KB
Note: You may already have this library installed. It is distributed in the books/finite-set-theory/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 (include-book "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 non-sets.

  • (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.

  • (in-list 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.


If you want to use the sets library to do non-trivial things, you will probably want to read some more thorough documentation of it.

PDF Finite Set Theory based on Fully Ordered Lists
Published in ACL2 '04.
PDF; 144 KB
This paper discussed the library's organization and design, and is probably the best thing to read to learn about the library.


PDF ACL2 '04 Presentation Slides
November 2004; PDF; 521 KB
PDF Feb 04 ACL2 Seminar Slides
February 2004; PDF; 220 KB
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

Code Browse Source (stable version)
This just gives you the Apache file listing.
Code Browse Subversion (development version)
Note that this viewer can be pretty slow.
Anonymous SVN access is also available. Run svn checkout svn:// osets