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