		Search-engine friendly clone of the ACL2 documentation.

Xargs

Normalize

Storing simplified definition bodies and guards

By default, when you submit a defun form, the body is simplified for certain later uses. This simplification is sometimes called ``normalization''; the ACL2 system function that accomplishes this task is normalize. Consider the following examples, where we make two definitions and then show their bodies using :pf..

ACL2 !>(defun f1 (x y)
         (cons (implies x y) (integerp 3)))
[.. output omitted ..]
 F1
ACL2 !>(defun f2 (x y)
         (declare (xargs :normalize nil))
         (cons (implies x y) (integerp 3)))
[.. output omitted ..]
 F2
ACL2 !>:pf f1
(EQUAL (F1 X Y) (IF X (IF Y '(T . T) '(NIL . T)) '(T . T)))
ACL2 !>:pf f2
(EQUAL (F2 X Y) (CONS (IMPLIES X Y) (INTEGERP 3)))
ACL2 !>

We see that the body of f1 has undergone the default simplification (with normalize), while the body of f2 has not because of the xargs in its defun form.

The example above illustrates that normalization consists of the following three parts:

propagation upward of if tests;
potential simplification with type reasoning; and
the expansion of calls of a few built-in functions like implies (the full list is the value of the constant, *expandable-boot-strap-non-rec-fns*).

We have seen an example where type reasoning can be expensive. So when ACL2 normalizes definition bodies and guards, it establishes a backchain-limit for type-set reasoning of 1, unless that limit is currently 0. (The global default is to have no limit.)

Also see the community-books utility install-not-normalized.