Major Section: RELEASE-NOTES
Programming mode has been eliminated. Instead, all functions have a
``color'' which indicates what can be done with the function. For
:red functions can be executed but have no axioms
describing them. Thus,
:red functions can be introduced after
passing a simple syntactic check and they can be redefined without
undoing. But nothing of consequence can be proved about them. At
the other extreme are
:gold functions which can be executed and
which also have passed both the termination and the guard
verification proofs. The color of a function can be specified with
:color, which, if omitted defaults to the
global setting of
:red causes behavior similar to the old
:gold causes behavior similar to the old
:v-mode. It is possible to prototype your system in
:red and then
:red functions to :
blue individually by calling
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.,
(fn ...xk...), by maintaining another
equivalence relation while rewriting the
(see congruence). If
r has been shown to be an equivalence
relation and then
(implies hyps (r (foo x) (bar x))) is proved as a
rewrite rule, then instances of
(foo x) will be replaced by
corresponding instances of
(bar x) provided the instance occurs in a
slot where the maintainence of
r-equivalence is known to be
hyps can be established as usual.
In Version 1.2, rule-classes were simple keywords, e.g.,
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.
Rules used to be named by symbols, e.g.,
car-cons were the
names of rules. Unfortunately, this was ambiguous because there are
three rules associated with function symbols: the symbolic
definition, the executable counterpart, and the type-prescription;
many different rules might be associated with theorems, depending on
the rule classes. In Version 1.3 rules are named by ``runes''
(which is just short hand for ``rule names''). Example runes are
(:executable-counterpart car), and
(:type-prescription car . 1). Every rule added by an event has a
different name and you can enable and disable them independently.
See rune and see theories.
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
(force term), it simply
assumes it is true and goes on, delaying until later the
establishment of term. In particular, pushes a new subgoal to prove
term in the current context. When that subgoal is attacked, all of
the resources of the theorem prover, not just rewriting, are brought
to bear. Thus, for example, if you wish to prove the rule
(implies (good-statep s) (equal (exec s n) s')) and it is your
expectation that every time
exec appears its first argument is a
good-statep then you might write the rule as
(implies (force (good-statep s)) (equal (exec s n) s')). This
rule is essentially an unconditional rewrite of
(exec s n) to
s' that spawns the new goal
(good-statep s). See force.
Because you can now specify independently how a theorem is used as a
rule, you need not write the
force in the actual theorem proved.
Version 1.3 supports a facility similar to Nqthm's
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
(rationalp (foo a b c)) it is now
smart enough to try lemmas that match with
(integerp (foo a b c)).