Finite Set Theory based on Fully Ordered Lists |

This is a relatively minor release for efficiency improvements and minor tweaks to the reasoning strategy.

*Certain operations are now tail recursive.* Previously, functions
such as `fast-union`, `fast-intersect`,
`fast-difference`, were not implemented tail recursively. This could
cause overflows on very large lists. Thanks to David Rager for identifying
this problem and for submitting patches to make these functions tail
recursive, eliminating the problem. Also made `split-list` tail
recursive, at David Rager's suggestion.

*Cardinality has been given a speed boost.* The executable version
of cardinality now calls `length` instead of `len`.

*Subset is now enabled.* Disabling the subset function was causing
some problems in finishing pick a point proofs. It is now enabled by
default.

*Added :built-in-clause rules about the acl2-count of
head and tail.*

*Added the rule in-head, rewriting (in (head X) X) to
(not (empty X)).*

This is a major release.

*The library now requires ACL2 2.9.*

*The set order has been changed.* We now use the same
`<<` as the total-order book. Effectively, we make
fewer assumptions about the set order, no longer requiring that nil
be the greatest element. This change might allow us to consider
custom set orders in the future. This was a bit of an undertaking.
Many proofs in `membership.lisp` and `fast.lisp` have
been changed to avoid relying on `nil`'s maximality. There
are also some changes in other low level theorems, such as
`head-insert`. There should be little or no impact on user
theorems, unless you were reasoning "from first principles", e.g.,
for "fast" functions defined using `cons` and so forth.

*Computed hints are now automatically managed.*
Previously, the macros `enable/disable-set-reasoning` were
used to turn on the computed hint for conducting pick-a-point
proofs. These macros have been removed and are no longer necessary,
and pick-a-point proofs are automatically enabled. (To disable
them, disable the "tagging" theorem,
`pick-a-point-subset-strategy`, instead.) Thanks to Matt
Kaufmann for modifying ACL2 to permit this change.

* Membership.lisp has been cleaned up.* The
support for computed hints have been separated out and put into its
own package,

*A new package, INSTANCE, has been added to support
the new extensions.* Users should not need to use this package
directly.

*New extension: constructive quantification.* This
extension (in `quantify.lisp`) completely replaces typed sets
with a more general and powerful theory of constructive
quantification. Given a k-ary (k > 1) predicate `P`, you can
now quickly introduce a theory of quantification for that predicate
over sets and lists.

*New extension: mappings.* Building off the base provided
by constructive quantification, mappings allow you to discuss the
images of sets under some arbitrary k-ary function, F, where (k > 1).
As with constructive quantification, an elaborate rewriting strategy
is also introduced for reasoning about mappings. Mappings are also
implemented more efficiently (via MBE) than the naive implementation
using repeated insertion.

*Mergesort is easier to reason about.* `Mergesort`
now has a new logical definition via MBE, so that you can reason
about it as if it were a simple, recursive insert sort. Of course,
it still acts as an efficient mergesort under the hood. Thanks to
Serita Nelesen for pointing out the deficiencies with the previous
approach. I've also done away with the use of `member-equal`,
and instead a new `in-list` function has been added which
returns a boolean instead of part of the list.

*Cardinality reasoning has been improved.* This is
particularly true with regards to the cardinalities of
intersections. Added theorems `cardinality-zero-empty`,
`intersect-cardinality-non-subset`,
`intersect-cardinality-subset-2`, and
`intersect-cardinality-non-subset-2`. Also changed
`intersect-cardinality-subset` to also be a :rewrite rule in
addition to being :linear. Thanks to Robert Krug and Hanbing Liu
for their input in these changes.

*Subset reasoning has been improved.* Added the theorem
`subset-tail` at Hanbing Liu's suggestion, which is useful
for induction-style proofs of subset. Also, the theorems
`difference-preserves-subset` and `subset-delete`,
have been added at Omar El-Domeiri's suggestion. Finally,
`subset-insert` has been added, and parallels
`subset-delete`.

This is a minor release to merge the library with ACL2.

*Matt Kaufmann has integreated the library with ACL2.* The
library will now be part of the standard books released with ACL2.
The build system has been modified to work nicely with ACL2's
makefiles, changed the computed hints functions to be program mode
in order to fix some problems with the new, more stringent guard
checking in ACL2 2.8. He has also updated the README to be more
accurate about what is built, and cleaned up the stray parentheses
in membership.lisp. Thanks, Matt!

This is a significant release, involving significant cleanup work and a few new theorems.

*The build system has been significantly improved.* A file
`package.lisp` has been added, and now contains the defpkg
event for the set theory books, so you can now simply "ld" this file
to get the set theory package. The `.acl2` have been changed
so that they do not contain include-book events, and
`sets.lisp` now includes the other books locally and then
redefines events from those books. This approach makes loading
`sets.lisp` faster, allows us to export events in a better
order, and hides all of the local proofs. These changes have all
been made at the suggestion of Eric Smith. Thanks!

*A mergesort has been added.* This allows you to quickly
create a set from an unordered list which may contain duplicates,
and its performance seems quite good.

*Optional set order reasoning is now available.* The file
`set-order.lisp` has been added and can be optionally
included to help with reasoning about the set order. Of course,
this should only be done if you are arguing from "first principles"
that your functions create sets, and should otherwise generally be
avoided.

*Double containment is now a rewrite rule.* A new theorem,
double-containment, has been added in order to explicitly rewrite
equalities between sets into mutual subset statements. The computed
hints which previously performed double containment proofs have been
removed.

*Computed hints can now be easily disabled.* The macro
`disable-set-reasoning` has been added, and can be used to
turn off the pick-a-point proofs that enable-set-reasoning turns
on.

*Some new theorems help fill out the rewriting strategy.*
In particular, the theorems `difference-insert-X/Y` and
`difference-delete-X/Y` were added.

This is a minor release, mainly introducing a new extension.

*A new induction scheme is now used for insert.* This
induction scheme rephrases insert's operation in terms of membership
rather than the set order, allowing inductive proofs over the
definition of insert to avoid introducing the set order into
proofs.

*New extension: typed sets.* This extension allows you to
introduce a theory about sets which contain elements of a fixed
type, e.g., `integerp`.

This is the first publically available version of the set theory library.