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, and double-containment.

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.

- Omaps
- A library of omaps (ordered maps), i.e. finite maps represented as strictly ordered alists.
- All-by-membership
- A way to quantify over sets.
- In
`(in a x)`determines ifa is a member of the setX .- Defset
- Generate a
fixtype of osets whose elements have a specified fixtype. - Primitives
- Replacements for
car ,cdr , etc., that respect the*non-set convention*. - Subset
`(subset x y)`determines ifX is a subset ofY .- Mergesort
`(mergesort x)`converts the listX into an ordered set.- Intersect
`(intersect x y)`constructs the intersection ofX andY .- Union
`(union x y)`constructs the union ofX andY .- Pick-a-point-subset-strategy
- Automatic pick-a-point proofs of subset.
- Delete
`(delete a x)`removes the elementa from the setX .- Difference
`(difference x y)`removes all members ofY fromX .- Cardinality
`(cardinality x)`computes the number of elements inX .- Set
- A fixtype of osets.
- Double-containment
- A strategy for proving sets are equal because they are subsets of one another.
- Intersectp
`(intersectp x y)`checks whetherX andY have any common members.