Definition
Make a rule that acts like a function definition
See rule-classes for a general discussion of rule classes
and how they are used to build rules from formulas. An example :corollary formula from which a :definition rule might be built is:
Examples:
(defthm open-len-twice
(implies (true-listp x)
(equal (len x)
(if (null x)
0
(if (null (cdr x))
1
(+ 2 (len (cddr x)))))))
:rule-classes :definition)
; Same as above, with :controller-alist made explicit:
(defthm open-len-twice
(implies (true-listp x)
(equal (len x)
(if (null x)
0
(if (null (cdr x))
1
(+ 2 (len (cddr x)))))))
:rule-classes ((:definition :controller-alist ((len t)))))
General Form:
(implies hyp (equiv (fn a1 ... an) body))
where equiv is an equivalence relation and fn is a function
symbol other than if, hide, force or case-split. Such rules allow ``alternative'' definitions of fn to be
proved as theorems but used as definitions. These rules are not true
``definitions'' in the sense that they (a) cannot introduce new function
symbols and (b) do not have to be terminating recursion schemes. They are
just conditional rewrite rules that are controlled the same way we control
recursive definitions. We call these ``definition rules'' or ``generalized
definitions''.
Consider the general form above. Generalized definitions are stored much
as :rewrite rules for the function ``defined,'' fn above,
but the procedure for applying them is a little different. During rewriting,
instances of (fn a1 ... an) are replaced by corresponding instances of
body provided the hyps can be established, as for a :rewrite rule; but when applying a :definition rule, the result of
rewriting body must also satisfy the criteria for function expansion.
There are two primary criteria, either of which permits expansion. The first
is that the ``recursive'' calls of fn in the rewritten body have
arguments that already occur in the goal conjecture. The second is that the
``controlling'' arguments to fn are simpler in the rewritten body.
The notions of ``recursive call'' and ``controllers'' are complicated by
the provisions for mutually recursive definitions. Consider a ``clique'' of
mutually recursive definitions. Then a ``recursive call'' is a call to any
function defined in the clique and an argument is a ``controller'' if it is
involved in the measure that decreases in all recursive calls. These notions
are precisely defined by the definitional principle and do not necessarily
make sense in the context of generalized definitional equations as implemented
here.
But because the heuristics governing the use of generalized definitions
require these notions, it is generally up to the user to specify which calls
in body are to be considered recursive and what the controlling arguments are.
This information is specified in the :clique and :controller-alist
fields of the :definition rule class.
The :clique field is the list of function symbols to be considered
recursive calls of fn. In the case of a non-recursive definition, the
:clique field is empty; in a singly recursive definition, it should
consist of the singleton list containing fn; otherwise it should be a
list of all of the functions in the mutually recursive clique with this
definition of fn.
If the :clique field is not provided it defaults to nil if
fn does not occur as a function symbol in body and it defaults to
the singleton list containing fn otherwise. Thus, :clique must be
supplied by the user only when the generalized definition rule is to be
treated as one of several in a mutually recursive clique.
The :controller-alist is an alist that maps each function symbol in
the :clique to a mask specifying which arguments are considered
controllers. The mask for a given member of the clique, fn, must be a
list of t's and nil's of length equal to the arity of fn. A
t should be in each argument position that is considered a ``controller''
of the recursion. For a function admitted under the principle of definition,
an argument controls the recursion if it is one of the arguments measured in
the termination argument for the function. But in generalized definition
rules, the user is free to designate any subset of the arguments as
controllers. Failure to choose wisely may result in the ``infinite
expansion'' of definitional rules but cannot render ACL2 unsound since the
rule being misused is a theorem.
If the :controller-alist is omitted it can sometimes be defaulted
automatically by the system. If the :clique is nil, the
:controller-alist defaults to nil. If the :clique is a
singleton containing fn, the :controller-alist defaults to the
controller alist computed by (defun fn args body). (The user can obtain
some control over this analysis by setting the default ruler-extenders; see
rulers.) If the :clique contains more than one function, the user
must supply the :controller-alist specifying the controllers for each
function in the clique. This is necessary since the system cannot determine
and thus cannot analyze the other definitional equations to be included in the
clique.
For example, suppose fn1 and fn2 have been defined one way and it
is desired to make ``alternative'' mutually recursive definitions available to
the rewriter. Then one would prove two theorems and store each as a
:definition rule. These two theorems would exhibit equations
``defining'' fn1 and fn2 in terms of each other. No provision is
here made for exhibiting these two equations as a system of equations. One is
proved and then the other. It just so happens that the user intends them to
be treated as mutually recursive definitions. To achieve this end, both
:definition rules should specify the :clique (fn1 fn2) and
should specify a suitable :controller-alist. If, for example, the new
definition of fn1 is controlled by its first argument and the new
definition of fn2 is controlled by its second and third (and they each
take three arguments) then a suitable :controller-alist would be ((fn1
t nil nil) (fn2 nil t t)). The order of the pairs in the alist is
unimportant, but there must be a pair for each function in the clique.
Inappropriate heuristic advice via :clique and :controller-alist
can cause ``infinite expansion'' of generalized definitions, but cannot render
ACL2 unsound.
Note that the actual definition of fn1 has the runic name
(:definition fn1). The runic name of the alternative definition is
(:definition lemma), where lemma is the name given to the event that
created the generalized :definition rule. This allows theories to switch
between various ``definitions'' of the functions.
By default, a :definition rule establishes the so-called ``body'' of a
function. The body is used by :expand hints, and it is also used
heuristically by the theorem prover's preprocessing (the initial
simplification using ``simple'' rules that is controlled by the
preprocess symbol in :do-not hints), induction analysis, and
the determination for when to warn about non-recursive functions in rules.
The body is also used by some heuristics involving whether a function is
recursively defined, and by the expand, x, and x-dumb commands
of the interactive proof-builder.
See rule-classes for a discussion of the optional field
:install-body of :definition rules, which controls whether a
:definition rule is used as described in the paragraph above. Note that
even if :install-body nil is supplied, the rewriter will still rewrite
with the :definition rule; in that case, ACL2 just won't install a new
body for the top function symbol of the left-hand side of the rule, which for
example affects the application of :expand hints as described in the
preceding paragraph. Also see set-body and see show-bodies for
how to change the body of a function symbol.
Note only that if you prove a definition rule for function foo, say,
foo-new-def, you will need to refer to that definition as
foo-new-def or as (:DEFINITION foo-new-def). That is because a
:definition rule does not change the meaning of the symbol foo for
:use hints, nor does it change the meaning of the symbol foo
in theory expressions; see theories, in particular the discussion there
of runic designators. Similarly :pe foo and :pf foo will still show the original definition of foo.
The definitional principle, defun, actually adds :definition
rules. Thus the handling of generalized definitions is exactly the same as
for ``real'' definitions because no distinction is made in the implementation.
Suppose (fn x y) is defun'd to be body. Note that defun (or defuns or mutual-recursion) can compute the clique
for fn from the syntactic presentation and it can compute the controllers
from the termination analysis. Provided the definition is admissible, defun adds the :definition rule (equal (fn x y) body).
Subtopics
- Force
- Identity function used to force a hypothesis
- Syntaxp
- Attach a heuristic filter on a rule
- Bind-free
- To bind free variables of a rewrite, definition, or linear rule
- Case-split
- Like force but immediately splits the top-level goal on the hypothesis
- Simple
- :definition and :rewrite rules used in
preprocessing
- Set-body
- Set the definition body
- Show-bodies
- Show the potential definition bodies
