		Search-engine friendly clone of the ACL2 documentation.

Defines

A very fine alternative to mutual-recursion.

Defines is a sophisticated macro for introducing mutually recursive functions using define. It gives you:

The usual benefits of define—extended-formals, concise xargs syntax, returns-specifiers, xdoc integration, easy inlining, and so on.
Automatic ACL2::make-flag integration, so you can easily prove inductive theorems about your new definitions.

Examples

  (defines terms
    :parents (syntax)
    :short "Example of terms in some simple, numeric language."

    (define my-termp (x)
      (if (atom x)
          (natp x)
        (and (symbolp (car x))
             (my-term-listp (cdr x))))
      ///
      (defthm natp-when-my-termp
        (implies (atom x)
                 (equal (my-termp x)
                        (natp x))))
      (defthm my-termp-of-cons
        (equal (my-termp (cons fn args))
               (and (symbolp fn)
                    (my-term-listp args)))))

    (define my-term-listp (x)
      (if (atom x)
          t
        (and (my-termp (car x))
             (my-term-listp (cdr x))))
      ///
      (deflist my-term-listp (x)
        (my-termp x)
        :already-definedp t)))

(defines flattening
  :parents (terms)
  :short "Collect up the arguments of terms."

  (define my-flatten-term ((x my-termp))
    :flag term
    :returns (numbers true-listp :rule-classes :type-prescription)
    (if (atom x)
        (list x)
      (my-flatten-term-list (cdr x))))

  (define my-flatten-term-list ((x my-term-listp))
    :flag list
    :returns (numbers true-listp :rule-classes :type-prescription)
    (if (atom x)
        nil
      (append (my-flatten-term (car x))
              (my-flatten-term-list (cdr x)))))
  ///
  (defthm-flattening-flag
    (defthm nat-listp-of-my-flatten-term
      (implies (my-termp x)
               (nat-listp (my-flatten-term x)))
      :flag term)
    (defthm nat-listp-of-my-flatten-term-list
      (implies (my-term-listp x)
               (nat-listp (my-flatten-term-list x)))
      :flag list)))

Usage

The general form of defines is:

(defines clique-name
  [global options]
  (define f1 ...)
  ...
  (define fN ...)
  [/// other-events])

The clique-name may be any symbol—we often just use the name of the first function in the clique, but this is not required. The name is used for documentation purposes, and also (by default) is used to name the flag function that will be introduced by ACL2::make-flag.

The global options each have the form :name value, and we describe these options below. We usually prefer to put these options at the front of the defines form, as shown above, but the options can be put anywhere until the /// form.

There must be at least two define forms. These can use the usual define syntax, and mostly this all works out naturally. The most significant caveats have to do with how we try to prove the theorems for :returns specifiers (see below).

The other-events are a structuring device that allow you to associate any arbitrary events. These events are submitted after the definitions, flag function, etc., have been processed. All of the functions in the clique are left enabled while processing these events.

Note that individual defines can have their own other-events. All of these individual sections are processed (with their own local scopes) before any global other-events.

Global Options

:verbosep bool: Normally most output is suppressed, but this can make it hard to understand failures. You can enable :verbosep t for better debugging.
:mode
:guard-hints, :guard-debug
:verify-guards val: The value val may be one of the following: t, nil, or :after-returns. The first two correspond to what is described in xargs. The keyword :after-returns indicates that the guards of the functions are to be verified after the returns-specifiers.
:well-founded-relation, :measure-debug, :hints, :otf-flg
:ruler-extenders: In an ordinary mutual-recursion, each of these xargs style options can be attached to any defun in the clique. But we usually think of these as global options to the whole clique, so we make them available as top-level options to the defines form. In the implementation, we just attach these options to the first defun form generated, except for :ruler-extenders, which we apply to all of the defuns.
:prepwork: Arbitrary events to be submitted before the definitions. Typically this might include in-theory calls, one-off supporting lemmas, etc. Prepwork is not automatically local, so lemmas and theory changes should usually be explicitly made local.; Note that each individual define may have its own :prepwork section. All of these sections will be appended together in order, with the global :prepwork coming first, and submitted before the definitions.
:returns-hints hints
:returns-no-induct bool: You can give hints for the inductive :returns theorem. Alternately, if you know you don't need to prove the returns theorems inductively, you can set :returns-no-induct t, which may improve performance.
:parents, :short, :long: These are global xdoc options that will be associated with the clique-name for this defines.; Note that each individual define may separately have its own documentation and rest-events. As a convenience, if global documentation is provided while individual documentation is not, a basic topic will be created whose :parents point at the clique-name.; A corner case is when the clique-name agrees with an individual function's name. In this case we try to grab the documentation from either the named function or the global options. To prevent confusion, we cause an error if documentation is provided in both places.
:ignore-ok val
:irrelevant-formals-ok val
:bogus-ok val: Submit set-ignore-ok, set-irrelevant-formals-ok, and/or set-bogus-mutual-recursion-ok forms before the definitions. These options are local to the definitions; they do not affect the other-events or any later events.
:flag name: You can also use :flag nil to suppress the creation of a flag function. Alternately, you can use this option to customize the name of the flag function. The default is inferred from the clique-name, i.e., it will look like <clique-name>-flag.
:flag-var var
:flag-defthm-macro name
:flag-hints hints: Control the flag variable name, flag macro name, and hints for ACL2::make-flag.
:flag-local bool: By default the flag function is created locally. This generally improves performance when later including your book, and is appropriate when all of your flag-based reasoning about the function is done in :returns specifiers and in the /// section. If you need the flag function and its macros to exist beyond the defines form, set :flag-local nil.
:progn bool: By default everything is submitted in an (encapsulate nil ...). If you set :progn t, then we will instead submit everything in a progn. This mainly affects what local means within the /// section. This may slightly improve performance by avoiding the overhead of encapsulate, and is mainly meant as a tool for macro developers.