NOTE-3-5(R)

ACL2 Version 3.5(r) (May, 2009) Notes 
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.