DEFUN-SK

Parent topic:  EVENTS
Home

Examples:
(defun-sk forall-x-p-and-q (y z)
  (forall x
          (and (p x y z)
               (q x y z))))


(defun-sk forall-x-p-and-q (y z) ; equivalent to the above
  (forall (x)
          (and (p x y z)
               (q x y z))))


(defun-sk some-x-y-p-and-q (z)
  (exists (x y)
          (and (p x y z)
               (q x y z))))

• EXISTS -- existential quantifier

• FORALL -- universal quantifier

(defun-sk fn (var1 ... varn) body
  &key doc quant-ok skolem-name thm-name)

The third argument, body, must be of the form

(Q bound-vars term)

The result of this event is to introduce a ``Skolem function,'' whose name is the keyword argument skolem-name if that is supplied, and otherwise is the result of modifying fn by suffixing "-WITNESS" to its name. The following definition and and of the following two theorems are introduced for skolem-name and fn in the case that bound-vars (see above) is a single variable v. The name of the defthm event may be supplied as the value of the keyword argument :thm-name; if it is not supplied, then it is the result of modifying fn by suffixing "-SUFF" to its name in the case that the quantifier is exists, and "-NECC" in the case that the quantifier is forall.

(defun fn (var1 ... varn)
  (let ((v (skolem-name var1 ... varn)))
    body))


(defthm fn-suff ;in case the quantifier is EXISTS
  (implies body
           (fn var1 ... varn)))


(defthm fn-necc ;in case the quantifier is FORALL
  (implies (not body)
           (not (fn var1 ... varn))))

(defun fn (var1 ... varn)
  (mv-let (bv1 ... bvk)
          (skolem-name var1 ... varn)
          body))

In order to emphasize that the last element of the list body is a term, defun-sk checks that the symbols forall and exists do not appear anywhere in it. However, on rare occasions one might deliberately choose to violate this convention, presumably because forall or exists is being used as a variable or because a macro call will be eliminating ``calls of'' forall and exists. In these cases, the keyword argument quant-ok may be supplied a non-nil value. Then defun-sk will permit forall and exists in the body, but it will still cause an error if there is a real attempt to use these symbols as quantifiers.

Those who want a more flexible version of defun-sk that allows nested quantifiers, should contact the implementors. In the meantime, if you want to represent nested quantifiers, you have to manage that yourself. For example, in order to represent

(forall x (exists y (p x y z)))

(defun-sk exists-y-p (x z)
  (exists y (p x y z)))


(defun-sk forall-x-exists-y-p (z)
  (forall x (exists-y-p x z)))

Some distracting and unimportant warnings are inhibited during defun-sk.

Defun-sk is implemented using defchoose, and hence should only be executed in defun-mode :logic; see defun-mode and see defchoose.

Note that this way of implementing quantifiers is not a new idea. Hilbert was certainly aware of it 60 years ago! The ``story'' (see bibliography) explains why our use of defchoose is appropriate, even in the presence of epsilon-0 induction.

EXISTS

Parent topic:  DEFUN-SK
Home

The symbol exists (in the ACL2 package) represents existential quantification in the context of a defun-sk form. See defun-sk and see forall.

FORALL

Parent topic:  DEFUN-SK
Home

The symbol forall (in the ACL2 package) represents universal quantification in the context of a defun-sk form. See defun-sk and see exists.

ENCAPSULATE

Parent topic:  EVENTS
Home

Examples:
(encapsulate ((an-element (lst) t))
  (local (defun an-element (lst)
           (if (consp lst) (car lst) nil)))
  (local (defthm member-equal-car
            (implies (and lst (true-listp lst))
                     (member-equal (car lst) lst))))
  (defthm thm1
     (implies (null lst) (null (an-element lst))))
  (defthm thm2
     (implies (and (true-listp lst)
                   (not (null lst)))
              (member-equal (an-element lst) lst))))


(encapsulate
 ()


 (local (defthm hack
          (implies (and (syntaxp (quotep x))
                        (syntaxp (quotep y)))
                   (equal (+ x y z)
                          (+ (+ x y) z)))))


 (defthm nthcdr-add1-conditional
   (implies (not (zp (1+ n)))
            (equal (nthcdr (1+ n) x)
                   (nthcdr n (cdr x))))))

General Form:
(encapsulate (signature ... signature)
  ev1
  ...
  evn)

To be well-formed, an encapsulate event must have the properties that each event in the body (including the local ones) can be successfully executed in sequence and that in the resulting theory, each function mentioned among the signatures was introduced via a local event and has the signature listed. In addition, the body may contain no ``local incompatibilities'' which, roughly stated, means that the events that are not local must not syntactically require symbols defined by local events, except for the functions listed in the signatures. See local-incompatibility. Finally, no non-local recursive definition in the body may involve in its suggested induction scheme any function symbol listed among the signatures. See subversive-inductions.

The result of an encapsulate event is an extension of the logic in which, roughly speaking, the functions listed in the signatures are constrained to have the signatures listed and to satisfy the non-local theorems proved about them. In fact, other functions introduced in the encapsulate event may be considered to have ``constraints'' as well. (See constraint for details, which are only relevant to functional instantiation.) Since the constraints were all theorems in the ``ephemeral'' or ``local'' theory, we are assured that the extension produced by encapsulate is sound. In essence, the local definitions of the constrained functions are just ``witness functions'' that establish the consistency of the constraints. Because those definitions are local, they are not present in the theory produced by encapsulation. Encapsulate also exports all rules generated by its non-local events, but rules generated by local events are not exported.

The default-defun-mode for the first event in an encapsulation is the default defun-mode ``outside'' the encapsulation. But since events changing the defun-mode are permitted within the body of an encapsulate, the default defun-mode may be changed. However, defun-mode changes occurring within the body of the encapsulate are not exported. In particular, the acl2-defaults-table after an encapsulate is always the same as it was before the encapsulate, even though the encapsulate body might contain defun-mode changing events, :program and :logic. See defun-mode. More generally, after execution of an encapsulate event, the value of acl2-defaults-table is restored to what it was immediately before that event was executed. See acl2-defaults-table.

Theorems about the constrained function symbols may then be proved -- theorems whose proofs necessarily employ only the constraints. Thus, those theorems may be later functionally instantiated, as with the :functional-instance lemma instance (see lemma-instance), to derive analogous theorems about different functions, provided the constraints (see constraint) can be proved about the new functions.

Observe that if the signatures list is empty, encapsulate may still be useful for deriving theorems to be exported whose proofs require lemmas you prefer to hide (i.e., made local).

The order of the events in the vicinity of an encapsulate is confusing. We discuss it in some detail here because when logical names are being used with theory functions to compute sets of rules, it is sometimes important to know the order in which events were executed. (See logical-name and see theory-functions.) What, for example, is the set of function names extant in the middle of an encapsulation?

If the most recent event is previous and then you execute an encapsulate constraining an-element with two non-local events in its body, thm1 and thm2, then the order of the events after the encapsulation is (reading chronologically forward): previous, thm1, thm2, an-element (the encapsulate itself). Actually, between previous and thm1 certain extensions were made to the world by the superior encapsulate, to permit an-element to be used as a function symbol in thm1.

Finally, we note that an encapsulate event is redundant if and only if a syntactically identical encapsulate has already been executed under the same default-defun-mode. See redundant-events.

IN-THEORY

Parent topic:  EVENTS
Home

Example:
(in-theory (set-difference-theories
             (universal-theory :here)
             '(flatten (:executable-counterpart flatten))))

General Form:
(in-theory term :doc doc-string)

Because no unique name is associated with an in-theory event, there is no way we can store the documentation string doc-string in our documentation data base. Hence, we actually prohibit doc-string from having the form of an ACL2 documentation string; see doc-string.

INCLUDE-BOOK

Parent topic:  EVENTS
Home

Examples:
(include-book "my-arith")
(include-book (:RELATIVE "my-arith"))
(include-book "/home/smith/my-arith")
(include-book (:ABSOLUTE "home" "smith" "my-arith"))

General Form:
(include-book file :load-compiled-file action :doc doc-string)

If there is a compiled file for the book that was created more recently than the book itself and the value action of the :load-compiled-file argument is not nil, or is omitted, then the compiled file is automatically loaded; otherwise it is not loaded. If action is t then the compiled file must be loaded or an error will occur, while if action is :warn (the default) then a warning will be printed. Certify-book can be used to compile a book. The effect of compilation is to speed up the execution of the functions defined within the book when those functions are applied to specific values. The presence of compiled code for the functions in the book should not otherwise affect the performance of ACL2. See guard for a discussion.

Include-book is similar in spirit to encapsulate in that it is a single event that ``contains'' other events, in this case the events listed in the file named. Include-book processes the non-local event forms in the file, assuming that each is admissible. Local events in the file are ignored. You may use include-book to load multiple books, creating the logical world that contains the definitions and theorems of all of them.

If any non-local event of the book attempts to define a name that has already been defined -- and the book's definition is not syntactically identical to the existing definition -- the attempt to include the book fails, an error message is printed, and no change to the logical world occurs. See redundant-events for the details.

When a book is included, the default defun-mode (see default-defun-mode) for the first event is always :logic. That is, the default defun-mode ``outside'' the book -- in the environment in which include-book was called -- is irrelevant to the book. Events that change the defun-mode are permitted within a book (provided they are not in local forms). However, such changes within a book are not exported, i.e., at the conclusion of an include-book, the ``outside'' default defun-mode is always the same as it was before the include-book.

Unlike every other event in ACL2, include-book puts a burden on you. Used improperly, include-book can be unsound in the sense that it can create an inconsistent extension of a consistent logical world. A certification mechanism is available to help you carry this burden -- but it must be understood up front that even certification is no guarantee against inconsistency here. The fundamental problem is one of file system security. See certificate for a discussion of the security issues.

After execution of an include-book form, the value of acl2-defaults-table is restored to what it was immediately before that include-book form was executed. See acl2-defaults-table.

This concludes the guided tour through books. See set-compile-fns for a subtle point about the interaction between include-book and on-the-fly compilation. See certify-book for a discussion of how to certify a book.

LOCAL

Parent topic:  EVENTS
Home

Examples:
(local (defthm hack1
         (implies (and (acl2-numberp x)
                       (acl2-numberp y)
                       (equal (* x y) 1))
                  (equal y (/ x)))))


(local (defun double-naturals-induction (a b)
         (cond ((and (integerp a) (integerp b) (< 0 a) (< 0 b))
                (double-naturals-induction (1- a) (1- b)))
               (t (list a b)))))

General Form:
(local ev)

Note that events that change the default defun-mode, and in fact any events that set the acl2-defaults-table, are disallowed inside the scope of local. See embedded-event-form.

LOGIC

Parent topic:  EVENTS
Home

Example:
ACL2 p!>:logic
ACL2 !>

Functions defined in :logic mode are logically defined. See defun-mode.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

See defun-mode for a discussion of the defun-modes available and what their effects on the logic are. See default-defun-mode for a discussion of how the default defun-mode is used. This event is equivalent to (table acl2-defaults-table :defun-mode :logic). See acl2-defaults-table.

Recall that the top-level form :logic is equivalent to (logic); see keyword-commands. Thus, to change the default defun-mode to :logic in a book, use (logic), which is an embedded event form, rather than :logic, which is not a legal form for books. See embedded-event-form.

MACRO-ALIASES-TABLE

Parent topic:  EVENTS
Home

Example:
(table macro-aliases-table 'append 'binary-append)

(in-theory (disable append))

(in-theory (disable binary-append))

(in-theory (set-difference-theories (current-theory :here)
                                    '(binary-append)))

General Form:
 
(table macro-aliases-table 'macro-name 'function-name)

(table macro-aliases-table macro-name-form function-name-form)

The table macro-aliases-table is an alist that associates macro symbols with function symbols, so that macro names may be used as runic designators (see theories). For a convenient way to add entries to this table, see add-macro-alias. To remove entries from the table with ease, see remove-macro-alias.

This table is used by the theory functions. For example, in order that (disable append) be interpreted as (disable binary-append), it is necessary that the example form above has been executed. In fact, this table does indeed associate many of the macros provided by the ACL2 system, including append, with function symbols. Loosely speaking, it only does so when the macro is ``essentially the same thing as'' a corresponding function; for example, (append x y) and (binary-append x y) represent the same term, for any expressions x and y.

MUTUAL-RECURSION

Parent topic:  EVENTS
Home

Example:
(mutual-recursion
 (defun evenlp (x)
   (if (consp x) (oddlp (cdr x)) t))
 (defun oddlp (x)
   (if (consp x) (evenlp (cdr x)) nil)))

General Form:
(mutual-recursion def1 ... defn)
where each defi is a DEFUN form.

The guard analysis must also be done for all of the functions at the same time. If any one of the defuns specifies the :verify-guards xarg to be nil, then guard verification is omitted for all of the functions.

Technical Note: Each defi above must be of the form (defun ...). In particular, it is not permitted for a defi to be a form that will macroexpand into a defun form. This is because mutual-recursion is itself a macro, and since macroexpansion occurs from the outside in, at the time (mutual-recursion def1 ... defk) is expanded the defi have not yet been. But mutual-recursion must decompose the defi. We therefore insist that they be explicitly presented as defuns.

Suppose you have defined your own defun-like macro and wish to use it in a mutual-recursion expression. Well, you can't. (!) But you can define your own version of mutual-recursion that allows your defun-like form. Here is an example. Suppose you define

(defmacro my-defun (&rest args) (my-defun-fn args))

(my-mutual-recursion (my-defun ...) ... (my-defun ...))

(defun my-mutual-recursion-fn (lst) 
  (declare (xargs :guard (alistp lst)))


; Each element of lst must be a consp (whose car, we assume, is always
; MY-DEFUN).  We apply my-defun-fn to the arguments of each element and
; collect the resulting list of DEFUNs.


  (cond ((atom lst) nil)
        (t (cons (my-defun-fn (cdr (car lst)))
                 (my-mutual-recursion-fn (cdr lst))))))


(defmacro my-mutual-recursion (&rest lst)


; Each element of lst must be a consp (whose car, we assume, is always
; MY-DEFUN).  We obtain the DEFUN corresponding to each and list them
; all inside a MUTUAL-RECURSION form.


  (declare (xargs :guard (alistp lst)))
  (cons 'mutual-recursion (my-mutual-recursion-fn lst))).

PROGRAM

Parent topic:  EVENTS
Home

Example:
ACL2 !>:program
ACL2 p!>

Functions defined in :program mode are logically undefined but can be executed on constants outside of deductive contexts. See defun-mode.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

See defun-mode for a discussion of the defun-modes available and what their effects on the logic are. See default-defun-mode for a discussion of how the default defun-mode is used. This event is equivalent to (table acl2-defaults-table :defun-mode :program). See acl2-defaults-table.

Recall that the top-level form :program is equivalent to (program); see keyword-commands. Thus, to change the default defun-mode to :program in a book, use (program), which is an embedded event form, rather than :program, which is not a legal form for books. See embedded-event-form.

REMOVE-MACRO-ALIAS

Parent topic:  EVENTS
Home

Example:
(remove-macro-alias append)

General Form:
(remove-macro-alias macro-name)

SET-COMPILE-FNS

Parent topic:  EVENTS
Home

Example Forms:
(set-compile-fns t)    ; new functions compiled after DEFUN
(set-compile-fns nil)  ; new functions not compiled after DEFUN

Also see comp, because it may be more efficient in some Common Lisps to compile many functions at once rather than to compile each one as you go along.

General Form:
(set-compile-fns term)

(table acl2-defaults-table :compile-fns term).

Set-compile-fns may be thought of as an event that merely sets a flag to t or nil. The flag's effect is felt when functions are defined, as with defun. If the flag is t, functions are automatically compiled after they are defined, as are their executable counterparts (see executable-counterpart). Otherwise, functions are not automatically compiled. Because set-compile-fns is an event, the old value of the flag is restored when a set-compile-fns event is undone.

Even when :set-compile-fns t has been executed, functions are not individually compiled when processing an include-book event. If you wish to include a book of compiled functions, we suggest that you first certify it with the compilation flag set; see certify-book. More generally, compilation via set-compile-fns is suppressed when the state global variable ld-skip-proofsp has value 'include-book.

SET-IGNORE-OK

Parent topic:  EVENTS
Home

Examples:
(set-ignore-ok t)
(set-ignore-ok nil)
(set-ignore-ok :warn)

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

General Form:
(set-ignore-ok flg)

One might find this event useful when one is generating function definitions by an automated procedure, when that procedure does not take care to make sure that all formals are actually used in the definitions that it generates.

SET-INHIBIT-WARNINGS

Parent topic:  EVENTS
Home

Examples:
(set-inhibit-warnings "theory" "use")

General Form:
(set-inhibit-warnings string1 string2 ...)

The effect of this event is to suppress any warning whose label is a member of this list (where again, case is ignored). For example, the warning

  ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE ....

Of course, if warnings are inhibited overall -- see set-inhibit-output-lst -- then the value of :inhibit-warnings is entirely irrelevant.

SET-INVISIBLE-FNS-ALIST

Parent topic:  EVENTS
Home

Examples:
(set-invisible-fns-alist ((binary-+ unary--)
                          (binary-* unary-/)
                          (unary-- unary--)
                          (unary-/ unary-/)))

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

General Form:
(set-invisible-fns-alist alist)

(table acl2-defaults-table :invisible-fns-alist 'alist),

The ``invisible functions alist'' is an alist that associates with certain function symbols, e.g., fn above, a set of unary functions, e.g., the ufni above. The ufni associated with fn in the invisible functions alist are said to be ``invisible with respect to fn.'' If fn is not the car of any pair on the invisible functions alist, then no function is invisible for it. Thus, setting the invisible functions alist to nil completely eliminates the consideration of invisibility.

The notion of invisibility is involved in the use of the :loop-stopper field of :rewrite rules to prevent the indefinite application of permutative rewrite rules. Roughly speaking, if rewrite rules are being used to permute arg and (ufni arg) inside of a nest of fn calls, and ufni is invisible with respect to fn, then arg and (ufni arg) are considered to have the same ``weight'' and will be permuted so as to end up as adjacent tips in the fn nest. See loop-stopper.

SET-IRRELEVANT-FORMALS-OK

Parent topic:  EVENTS
Home

Examples:
(set-irrelevant-formals-ok t)
(set-irrelevant-formals-ok nil)
(set-irrelevant-formals-ok :warn)

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

General Form:
(set-irrelevant-formals-ok flg)