Undoing and perhaps redefining

This topic provides a high-level view of how one can undo a definition, perhaps replacing it with a new definition. We begin with some background.

ACL2 maintains a stack of commands. For example, suppose we submit the following events in a new session.

(defun f (x) x) (defun g (x) (* x x)) (defthm f^2-is-g (equal (expt (f x) 2) (g x)) :hints (("Goal" :expand ((expt x 2)))))

Then we can see the stack of commands by using `pcb` (``Print
Command Block'') back to command 0, that is back to the start.

ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN F (X) ...) L 2 (DEFUN G (X) ...) 3:x(DEFTHM F^2-IS-G ...) ACL2 !>

Now suppose that we want to redefine `ubt` (``Undo Back Through'') all the way
back through (and including)

ACL2 !>:ubt g L 1:x(DEFUN F (X) ...) ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1:x(DEFUN F (X) ...) ACL2 !>

Now we can define

ACL2 !>(defun g (x) (expt x 2)) [[.. output omitted here ..]] G ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN F (X) ...) L 2:x(DEFUN G (X) ...) ACL2 !>(defthm f^2-is-g (equal (expt (f x) 2) (g x))) [[.. output omitted here ..]] F^2-IS-G ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN F (X) ...) L 2 (DEFUN G (X) ...) 3:x(DEFTHM F^2-IS-G ...) ACL2 !>

See ubt for more information, including variants such as

It can occasionally be inconvenient to undo a large number of commands when
one's goal is only to redefine a single function. In such cases one might
wish to enable redefinition, even though it can be unsafe. Here is an
example (admittedly contrived) for how to continue the session above. Note
that there are variants of

ACL2 !>:redef (:QUERY . :OVERWRITE) ACL2 !>(defun f (x) (+ 10 x)) ACL2 Query (:REDEF): The name F is in use as a function. Its current defun-mode is :logic. Do you want to redefine it? (N, Y, E, O or ?): y Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (ACL2-NUMBERP (F X)). We used primitive type reasoning. Summary Form: ( DEFUN F ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN F (X) ...) L 2 (DEFUN G (X) ...) 3 (DEFTHM F^2-IS-G ...) L 4:x(DEFUN F (X) ...) ACL2 !>

Notice that the ``theorem''

You can inspect both commands that introduce a definition for

ACL2 !>:pcb! 1 L 1 (DEFUN F (X) X) ACL2 !>:pcb! 3 L 3:x(DEFUN F (X) (CAR (CONS X X))) ACL2 !>

- Ubt
- Undo the commands back through a command descriptor
- Ubu
- Undo the commands back up to (not including) a command descriptor
- Ubt!
- Undo commands, without a query or an error
- U
- Undo last command, without a query
- Ubu!
- Undo commands, without a query or an error
- Ubu?
- Undo commands, with queries as appropriate
- Ubt?
- Undo commands, with queries as appropriate
- Ubt-prehistory
- Undo the commands back through the last
`reset-prehistory`event