Theory-management
Recommendations related to enabling and disabling functions and
theorems.
The best practices depend somewhat on the kind of book you are
writing. We distinguish between Widget Libraries and Core
Libraries.
Widget Libraries
Scenario: your library describes a particular kind of "Widget:" it defines
what Widgets are, provides some useful algorithms for operating on Widgets, and
proves some theorems about the properties of Widgets and these algorithms.
Recommendations
- Avoid any non-local inclusion of arithmetic libraries
- Avoid any non-local (in-theory ...) events that involve built-in ACL2
functions. For instance, do not do: (in-theory (enable append)).
- Try to respect the ACL2 namespace, e.g., do not define new functions in the
ACL2 package, especially with short or generic names, etc.
Rationale
- You would expect that loading a Widget library should generally just give
you definitions and lemmas that are about Widgets.
- You would not expect a Widget library to change how you reason about other
concepts that are unrelated to Widgets.
- Non-local arithmetic includes may make your Widget library incompatible
with other arithmetic libraries.
Core Libraries
Scenario: your library is meant to assist with reasoning about built-in ACL2
functions, for instance:
- arithmetic functions like +, -, *, /, floor, mod, logand;
- list functions like append, len, nth, member, subsetp;
- string functions like coerce, concatenate, subseq;
- system functions like io routines and state updates;
- meta functions like pseudo-termp, disjoin, conjoin-clauses;
Since your library is inherently about existing ACL2 functions rather than
new definitions, the Widget-library recommendations do not necessarily
apply.
