Major Section: RELEASE-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 `standard-numberp`

has been replaced with `standardp`

.

If `f`

is a classical function, the value `(f x1 ... xn)`

is guaranteed
to be standard when the `xi`

are standard. ACL2(r) can now recognize this
fact automatically, using `defun-std`

. For example, the following can be
used to assert that the square root of 2 is a standard value.

(defthm-std sqrt-2-rational (standardp (acl2-sqrt 2)))More generally, the expression

`(f x1 ... xn)`

can contain free variables,
but the result is guaranteed to be standard when the variables take on
standard variables, as in the following:
(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 `books/nonstd/`

. The new library
uses `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.