ACL2 Version 3.5(r) (May, 2009) Notes

Please also see note-3-5 for changes in Version 3.5 of ACL2.

This release incorporates improvements from Ruben Gamboa in support for non-standard analysis in ACL2(r), in the following ways:

ACL2(r) now supports non-classical objects that are not also numeric, e.g.,
non-classical cons pairs. Consequently, the built-in `standardp`.

If

(defthm-std sqrt-2-rational (standardp (acl2-sqrt 2)))

More generally, the expression

(defthm-std sqrt-x-rational (implies (standardp x) (standardp (acl2-sqrt x))))

A potential soundness bug in `encapsulate` was fixed. Specifically,
when a classical, constrained function is instantiated with a lambda
expression containing free variables, it may produce non-standard values
depending on the values of the free variables. This means that the functional
instantiation cannot be used to justify a non-classical theorem. For example,
consider the following sequence:

(encapsulate ((f (x) t)) (local (defun f (x) x))) (defthm-std f-x-standard (implies (standardp x) (standardp (f x)))) (defthm plus-x-standard (implies (standardp x) (standardp (+ x y))) :hints (("Goal" :use ((:functional-instance f-x-standard (f (lambda (x) (+ x y)))))))) (defthm plus-x-eps-not-standard (implies (standardp x) (not (standardp (+ x (/ (i-large-integer))))))) (defthm nil-iff-t nil :hints (("Goal" :use ((:instance plus-x-standard (y (/ (i-large-integer)))) (:instance plus-x-eps-not-standard)))))

ACL2(r) also supports the introduction of non-classical functions with
`defchoose`. These behave just as normal functions introduced with
`defchoose`, but they have a non-classical choice property.

Finally, ACL2(r) now comes with a revamped library supporting non-standard
analysis, still distributed separately as `defchoose` to state more natural and useful versions of the IVT,
MVT, etc. It also supports the introduction of inverse functions, e.g.,
logarithms. Finally, the library has much more extensive support for
differentiation.