A finite set theory implementation for ACL2 based on fully ordered
lists. Some major features of this approach are that set equality is just
equal, and set operations like union, intersect, and so
forth have O(n) implementations.
Osets mostly hides the fact that sets are represented as ordered
lists. You should not have to reason about the set order unless you are trying
to exploit it to make some function faster. Instead, we generally try to
reason about sets with a membership-based approach, via in and subset.
The osets library offers some automation for pick-a-point style reasoning,
see for instance all-by-membership, pick-a-point-subset-strategy,
You can load the library with:
(include-book "std/osets/top" :dir :system)
The definitions of the main set-manipulation functions are disabled, but are
in a ruleset and may be enabled using:
(in-theory (acl2::enable* set::definitions))
Some potentially useful (but potentially expensive) rules are also left
disabled and may be enabled using:
(in-theory (acl2::enable* set::expensive-rules))
Besides this ACL2::xdoc documentation, you may be interested in the
2004 ACL2 workshop paper, Finite
Set Theory based on Fully Ordered Lists, and see also the slides
from the accompanying talk.
- A library of omaps (ordered maps),
i.e. finite maps represented as strictly ordered alists.
- A way to quantify over sets.
- Generate a fixtype
whose elements have a specified fixtype.
- (in a x) determines if a is a member of the set X.
- Replacements for car, cdr, etc., that respect the
- (subset x y) determines if X is a subset of Y.
- (mergesort x) converts the list X into an ordered set.
- (intersect x y) constructs the intersection of X and Y.
- (union x y) constructs the union of X and Y.
- Automatic pick-a-point proofs of subset.
- (delete a x) removes the element a from the set X.
- (difference x y) removes all members of Y from X.
- (cardinality x) computes the number of elements in X.
- A fixtype of osets.
- A strategy for proving sets are equal because they are subsets
of one another.
- (intersectp x y) checks whether X and Y have any common