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
example, :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
the new xargs keyword, :color, which, if omitted defaults to the
global setting of ld-color. Ld-color replaces load-mode. Setting
ld-color to :red causes behavior similar to the old :g-mode.
Setting ld-color to :gold causes behavior similar to the old
:v-mode. It is possible to prototype your system in :red and then
convert :red functions to :blue individually by calling
verify-termination on them. They can then be converted to :gold
with 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 kth argument
(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
sufficient and hyps can be established as usual.
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 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
(:definition car), (: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.
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 (rationalp (foo a b c)) it is now
smart enough to try lemmas that match with (integerp (foo a b c)).