ACL2 is a first-order, essentially quantifier free logic of computable
recursive functions based on an applicative subset of Common Lisp. It
supports lists as a primitive data structure. We describe how we have
formalized a practical finite set theory for ACL2. Our finite set theory
``book'' includes set equality, set membership, the subset relation, set
manipulation functions such as `union`

, `intersection`

,
etc., a choice function, a representation of finite functions as sets of
ordered pairs and a collection of useful functions for manipulating them
(e.g., domain, range, apply) and others. The book provides many lemmas about
these primitives, as well as macros for dealing with set comprehension and
some other ``higher order'' features of set theory, and various strategies or
tactics for proving theorems in set theory. The goal of this work is not to
provide ``heavy duty set theory'' -- a task more suited to other logics --
but to allow the ACL2 user to use sets in a ``light weight'' fashion in
specifications, while continuing to exploit ACL2's efficient executability,
built in proof techniques for certain domains, and extensive lemma libraries.

**Note:** This paper was accepted for *The 14th International
Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001)* and
will appear in the associated LNCS volume.

- paper (76 KB gzipped postscript)
- paper (114 KB gzipped pdf)
`books.tar`

(154 tar file): the source files for all the ACL2 books and the scripts needed to re-certify them.- Source files in
`books.tar`

`Makefile`

: A Unix makefile that will re-certify all of the relevant books.`total-ordering.lisp`

: a book defining a total ordering on ACL2 objects, used in the canonicalization of sets.`defpkg.lisp`

: the definition of the`"S"`

symbol package.`set-theory.lisp`

: the main set-theory book.`set-theory.acl2`

: the file that tells the`Makefile`

how to certify`set-theory.lisp`

.`powerset-examples.lisp`

`powerset-examples.acl2`

: the file that tells the`Makefile`

how to certify`powerset-examples.lisp`

.`set-count.lisp`

`set-count.acl2`

: the file that tells the`Makefile`

how to certify`set-count.lisp`

.`recursion-by-choose.lisp`

`recursion-by-choose.acl2`

: the file that tells the`Makefile`

how to certify`recursion-by-choose.lisp`

.

- Create some directory,
*dir*. - Download
`books.tar`

to*dir*and then invoke

`tar xvf books.tar`

or, equivalently, download all the source files to*dir*. - In both
`Makefile`

and`set-theory.lisp`

, change the path`/projects/acl2/v2-5/books/`

to the pathname identifying ACL2's distribution book directory on your local system. - While standing on directory
*dir*, type

`make ACL2=`

*acl2*

where*acl2*is the command to invoke ACL2 on your system.