NOTE-2-8-RULES

ACL2 Version 2.8 Notes on Changes in Rules, Definitions, and Constants
Major Section:  NOTE-2-8

The theory minimal-theory has been changed by adding the definition rune for mv-nth to the theory. A corresponding change has been made to the theory warning mechanism, which was failing to warn if the definition of mv-nth is disabled, even though calls of mv-nth can be expanded by special-purpose code in the rewriter. Thanks to Serita Van Groningen for pointing out this problem with the theory warning mechanism.

The defevaluator event has been modified so that in the body of the evaluator function, to add a new case (ATOM X) (returning nil) has been inserted immediately after the case (EQ (CAR X) 'QUOTE). This is a no-op semantically but may speed up proofs. Thanks to Warren Hunt for suggesting this change.

A new form of :compound-recognizer rule is now allowed:

(if (fn x) concl1 concl2)
This is equivalent to an existing form:
(and (implies (fn x) concl1)
     (implies (not (fn x)) concl2))
Thanks to Josh Purinton for bringing this to our attention.

Rewrite rules realpart-+ and imagpart-+ have been added in order to simplify the realpart and imagpart (respectively) of a sum. They follow from a theorem add-def-complex that equates a sum with the complex number formed by adding real and imaginary parts. All three of these theorems may be found in source file axioms.lisp. Thanks to Eric Smith for raising a question leading to these additions, as well as to Joe Hendrix and Vernon Austel for helpful suggestions.