Acl2 Version 1.3 Notes

Programming mode has been eliminated. Instead, all
functions have a ``color'' which indicates what can be done with the function.
For example, `xargs` keyword, `verify-termination` on them. They can then be
converted to `verify-guards`. This allows us to
undertake to verify the termination and guards of system functions.
See `doc` color for an introduction to the use of colors.

Type prescription rules have been added. Recall that in Nqthm, some `rewrite` rules were actually stored as ``type-prescriptions.'' Such
rules allow the user to inform Nqthm's primitive type mechanism as to the
kinds of shells returned by a function. Earlier versions of Acl2 did not have
an analogous kind of rule because Acl2's type mechanism is complicated by
guards. Version 1.3 supports `type-prescription` rules. See
type-prescription.

Three more new rule-classes implement congruence-based rewriting.
It is possible to identify a binary relation as an equivalence relation (see
equivalence), to show that one equivalence relation refines another
(see refinement) and to show that a given equivalence relation is
maintained when rewriting a given function call, e.g., `rewrite` rule, then instances of

In Version 1.2, rule-classes were simple keywords, e.g.,
`rewrite` or `elim`. In Version 1.3, rule-classes have been elaborated to allow you to specify how the theorem
ought to be used as a rule. That is, the new rule-classes allows you
to separate the mathematical statement of the formula from its interpretation
as a rule. See rule-classes.

Rules used to be named by symbols, e.g., `car` and

The identity function `force`, of one argument, has been added and
given a special interpretation by the functions responsible for establishing
hypotheses in backchaining: When the system fails to establish some hypothesis
of the form `(implies
(good-statep s) (equal (exec s n) s'))` and it is your expectation that
every time `(implies (force (good-statep s)) (equal (exec s n)
s'))`. This rule is essentially an unconditional rewrite of `force` in the actual theorem proved. See
rule-classes.

Version 1.3 supports a facility similar to Nqthm's `break-lemma`.
See break-rewrite. You can install ``monitors'' on runes
that will cause interactive breaks under certain conditions.

Acl2 also provides ``wormholes'' which allow you to write functions
that cause interaction with the user but which do not require that you have
access to `state`. See wormhole.

The rewriter now automatically backchains to stronger recognizers. There
is no user hook to this feature but it may simplify some proofs with which
older versions of Acl2 had trouble. For example, if the rewriter is trying to
prove