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
(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