THEORIES-AND-PRIMITIVES

Major Section:  THEORIES

When you disable the definition or executable-counterpart of a built-in function, you may see a warning, for example as follows.

  ACL2 !>(in-theory (disable mv-nth))

  ACL2 Warning [Theory] in ( IN-THEORY (DISABLE ...)):  Although the
  theory expression (DISABLE MV-NTH) disables the :DEFINITION rule for
  MV-NTH, some expansions involving this function may still occur.  See
  :DOC theories-and-primitives.

This warning can be eliminated by turning off all theory warnings (see set-inhibit-warnings) or simply by evaluating the following form.

  (assign verbose-theory-warning nil)

First consider the following example, evaluated after the in-theory event displayed above.

  ACL2 !>(thm (equal (mv-nth 2 (list a b c d e)) c))

  Q.E.D.

  Summary
  Form:  ( THM ...)
  Rules: ((:DEFINITION MV-NTH)
          (:FAKE-RUNE-FOR-TYPE-SET NIL))
  Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
  Prover steps counted:  19

  Proof succeeded.
  ACL2 !>

Note that even though the definition of mv-nth had been disabled, nevertheless its definition rule was used in proving this theorem. It is as though mv-nth had not been been disabled after all! The warning is intended to indicate that expansion of mv-nth calls may be made by the theorem prover even when mv-nth is disabled. Indeed, the prover has special-purpose code for simplifying certain mv-nth calls.

A similar issue can arise for executable-counterpart rules, as the following log illustrates.

  ACL2 !>(in-theory (disable (:executable-counterpart symbolp)))

  ACL2 Warning [Theory] in ( IN-THEORY (DISABLE ...)):  Although the
  theory expression (DISABLE (:EXECUTABLE-COUNTERPART SYMBOLP)) disables
  the :EXECUTABLE-COUNTERPART rule for SYMBOLP, some calls involving
  this function may still be made.  See :DOC theories-and-primitives.


  Summary
  Form:  ( IN-THEORY (DISABLE ...))
  Rules: NIL
  Warnings:  Theory
  Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
   2921
  ACL2 !>(thm (symbolp 'a))

  Q.E.D.

  Summary
  Form:  ( THM ...)
  Rules: NIL
  Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

  Proof succeeded.
  ACL2 !>

In general, ACL2 warns when in-theory events or hints leave you in a theory where a rule for a built-in function is disabled but may be applied in some cases nonetheless, because of special-purpose prover code for handling calls of that function. The built-in function symbols with such definition rules or executable-counterpart rules are those in the following two lists, respectively.

  ACL2 !>*definition-minimal-theory*
  (MV-NTH IFF NOT
          IMPLIES EQ ATOM EQL = /= NULL ENDP ZEROP
          SYNP PLUSP MINUSP LISTP RETURN-LAST
          MV-LIST THE-CHECK WORMHOLE-EVAL
          FORCE CASE-SPLIT DOUBLE-REWRITE)
  ACL2 !>*built-in-executable-counterparts*
  (ACL2-NUMBERP BINARY-* BINARY-+ UNARY-- UNARY-/
                < CAR CDR CHAR-CODE CHARACTERP CODE-CHAR
                COMPLEX COMPLEX-RATIONALP COERCE
                CONS CONSP DENOMINATOR EQUAL IF IMAGPART
                INTEGERP INTERN-IN-PACKAGE-OF-SYMBOL
                NUMERATOR PKG-WITNESS PKG-IMPORTS
                RATIONALP REALPART STRINGP SYMBOL-NAME
                SYMBOL-PACKAGE-NAME SYMBOLP NOT)
  ACL2 !>