Built-in-theorems
Built-in theorems.
The ACL2 source file axioms.lisp provides a number of theorems.
Here we mean `theorem' in the logical sense,
introduced not only via defthm but also via defaxiom
(logically, axioms are easy-to-prove theorems).
This documentation topic (and subtopics)
collects and display these theorems,
organized according to the built-in functions and values that they involve.
These theorems may be easier to read and analyze here
than in the ACL2 source files, which contain additional code.
The current organization of these theorems in subtopics
may be improved in the future.
It may even make sense to repeat certain theorems under certin subtopics,
when they are relevant to multiple subtopics.
We use the XDOC preprocessor directive @(def ...)
to list the theorems automatically,
without copying the forms (just the names).
Thus, the only way in which this documentation topic may get out of sync
is when some built-in theorem is added or removed,
which may be a rare occurrence.
For now we only include the theorems of ``plain'' ACL2, not ACL2(r).
We omit theorems about ``internal'' functions,
i.e. functions not documented in the manual.
An example is
the theorem that rewrites member-eq-exec to member-equal:
member-eq-exec is internal, and in fact
the purpose of the aforementioned rewrite rule is to rewrite it away.
Subtopics
- Built-in-theorems-about-arithmetic
- Built-in theorems about arithmetic.
- Built-in-theorems-about-symbols
- Built-in theorems about symbols.
- Built-in-theorems-about-characters
- Built-in theorems about characters.
- Built-in-theorems-about-lists
- Built-in theorems about lists.
- Built-in-theorems-about-arrays
- Built-in theorems about arrays.
- Built-in-theorems-about-strings
- Built-in theorems about strings.
- Built-in-theorems-about-alists
- Built-in theorems about alists.
- Built-in-theorems-about-total-order
- Built-in theorems about the total order on values.
- Built-in-theorems-about-system-utilities
- Built-in theorems about system utilities.
- Built-in-theorems-about-cons-pairs
- Built-in theorems about cons pairs.
- Built-in-theorems-for-tau
- Built-in theorems specifically for the tau system.
- Built-in-theorems-about-bad-atoms
- Built-in theorems about bad atoms.
- Built-in-theorems-about-logical-connectives
- Built-in-theorems about logical connectives.
- Built-in-theorems-about-booleans
- Built-in-theorems about booleans.
- Built-in-theorems-about-random$
- Built-in theorems about random$.
- Built-in-theorems-about-eqlables
- Built-in theorems about eqlables.
