Info file: acl2-doc-emacs.info,    -*-Text-*-
produced by `texinfo-format-buffer'
from file `acl2-doc-emacs.texinfo'
using `texinfmt.el' version 2.32 of 19 November 1993.



This is documentation for ACL2 Version 1.9 Copyright (C) 1997
Computational Logic, Inc.

This program is free software; you can redistribute it and/or modify it
under the terms of the GNU General Public License as published by the
Free Software Foundation; either version 2 of the License, or (at your
option) any later version.

This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
General Public License for more details.

You should have received a copy of the GNU General Public License along
with this program; if not, write to the Free Software Foundation, Inc.,
675 Mass Ave, Cambridge, MA 02139, USA.

Written by: Matt Kaufmann and J Strother Moore Computational Logic, Inc.
1717 West Sixth Street, Suite 290 Austin, TX 78703-4776 U.S.A.






File: acl2-doc-emacs.info, Node: SYNTAX, Next: SYNTAXP, Prev: SUBVERSIVE-INDUCTIONS, Up: MISCELLANEOUS

SYNTAX    the syntax of ACL2 is that of Common Lisp

For the details of ACL2 syntax, see CLTL.  For examples of ACL2 syntax,
use :pe to print some of the ACL2 system code.  For example:

     :pe assoc-equal
     :pe dumb-occur
     :pe fn-var-count
     :pe add-linear-variable-to-alist


There is no comprehensive description of the ACL2 syntax yet, except
that found in CLTL.  Also see *Note TERM::.




File: acl2-doc-emacs.info, Node: SYNTAXP, Next: TERM, Prev: SYNTAX, Up: MISCELLANEOUS

SYNTAXP    to attach a heuristic filter on a :rewrite rule


     Example:
     Consider the :REWRITE rule created from

     (IMPLIES (SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM))))
              (EQUAL (LXD X) (LXD (NORM X)))).

The syntaxp hypothesis in this rule will allow the rule to be applied to
(lxd (trn a b)) but will not allow it to be applied to (lxd (norm a)).


     General Form:
     (SYNTAXP test)

may be used as the nth hypothesis in a :rewrite rule whose :corollary is
(implies (and hyp1 ... hypn ... hypk) (equiv lhs rhs)) provided test is
a term, test contains at least one variable, and every variable occuring
freely in test occurs freely in lhs or in some hypi, i<n.  Formally,
syntaxp is a function of one argument; syntaxp always returns t and so
may be added as a vacuous hypothesis.  However, the test "inside" the
syntaxp form is actually treated as a meta-level proposition about the
proposed instantiation of the rule's variables and that proposition must
evaluate to true (non-nil) to "establish" the syntaxp hypothesis.

We illustrate this by slightly elaborating the example given above.
Consider a :rewrite rule whose :corollary is:

     (IMPLIES (AND (RATIONALP X)
                   (SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))))
              (EQUAL (LXD X) (LXD (NORM X))))

How is this rule applied to (lxd (trn a b))?  First, we form a
substitution that instantiates the left-hand side of the conclusion of
the rule so that it is identical to the target term.  In the present
case, the substitution replaces x with (trn a b).  Then we backchain to
establish the hypotheses, in order.  Ordinarily this means that we
instantiate each hypothesis with our substitution and then attempt to
rewrite the resulting instance to true.  Of course, most users are aware
of some exceptions to this general rule.  For example, if a hypothesis
contains a "free-variable" -- one not bound by the current substitution
-- we attempt to extend the substitution by searching for an instance of
the hypothesis among known truths.  Forced hypotheses are another
exception to the general rule of how hypotheses are relieved.
Hypotheses marked with syntaxp, as in (syntaxp test), are also
exceptions.  Instead of instantiating the hypothesis and trying to
establish it, we evaluate test in an environment in which its variable
symbols are bound to the quotations of the terms to which those
variables are bound in the instantiating substitution.  In the case in
point, we evaluate the test

      (NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))

in an environment where x is bound to '(trn a b), i.e., the list of
length three whose car is the symbol 'trn.  Thus, the test returns t
because x is a consp and its car is not the symbol 'norm.  When the
syntaxp test evaluates to t, we consider the syntaxp hypothesis to have
been established; this is sound because (syntaxp test) is t regardless
of test.  If the test evaluates to nil (or fails to evaluate because of
guard violations) we act as though we cannot establish the hypothesis
and abandon the attempt to apply the rule; it is always sound to give
up.

Note that the test of a syntaxp hypothesis does not deal with the
meaning or semantics or values of the terms but with their syntactic
forms.  In the example above, the syntaxp hypothesis allows the rule to
be applied to every target of the form (lxd u), provided (rationalp u)
can be established and u is not of the form (norm v).  Observe that
without this syntactic restriction the rule above could loop producing a
sequence of increasingly complex targets (lxd a), (lxd (norm a)), (lxd
(norm (norm a))), etc.  An intuitive reading of the rule might be "norm
the argument of lxd (when it is rationalp) unless it has already been
normed."

Another common syntactic restriction is

       (SYNTAXP (AND (CONSP X) (EQ (CAR X) 'QUOTE))).

A rule with such a hypothesis can be applied only if x is bound to a
specific constant.  Thus, if x is 23 (which is actually represented
internally as (quote 23)), the test evaluates to t; but if x is (+ 11
12) it evaluates to nil (because (car x) is the symbol '+).  It is often
desirable to delay the application of a rule until certain subterms are
in some kind of normal form so that the application doesn't produce
excessive case splits.




File: acl2-doc-emacs.info, Node: TERM, Next: TERM-ORDER, Prev: SYNTAXP, Up: MISCELLANEOUS

TERM    the three senses of well-formed ACL2 expressions or formulas


     Examples of Terms:
     (cond ((caar x) (cons t x)) (t 0))   ; an untranslated term

     (if (car (car x)) (cons 't x) '0)    ; a translated term

     (car (cons x y) 'nil v)              ; a pseudo-term


In traditional first-order predicate calculus a "term" is a syntactic
entity denoting some object in the universe of individuals.  Often, for
example, the syntactic characterization of a term is that it is either a
variable symbol or the application of a function symbol to the
appropriate number of argument terms.  Traditionally, "atomic formulas"
are built from terms with predicate symbols such as "equal" and
"member;" "formulas" are then built from atomic formulas with
propositional "operators" like "not," "and," and "implies." Theorems are
formulas.  Theorems are "valid" in the sense that the value of a theorem
is true, in any model of the axioms and under all possible assignments
of individuals to variables.

However, in ACL2, terms are used in place of both atomic formulas and
formulas.  ACL2 does not have predicate symbols or propositional
operators as distinguished syntactic entities.  The ACL2 universe of
individuals includes a "true" object (denoted by t) and a "false" object
(denoted by nil), predicates and propositional operators are functions
that return these objects.  Theorems in ACL2 are terms and the
"validity" of a term means that, under no assignment to the variables
does the term evaluate to nil.

We use the word "term" in ACL2 in three distinct senses.  We will speak
of "translated" terms, "untranslated" terms, and "pseudo-" terms.

*Translated Terms:  The Strict Sense and Internal Form*

In its most strict sense, a "term" is either a legal variable symbol, a
quoted constant, or the application of an n-ary function symbol or
closed lambda expression to a true list of n terms.

The legal variable symbols are symbols other than t or nil which are not
in the keyword package, do not start with ampersand, do not start and
end with asterisks, and if in the main Lisp package, do not violate an
appropriate restriction (see *Note NAME::).

Quoted constants are expressions of the form (quote x), where x is any
ACL2 object.  Such expressions may also be written 'x.

Closed lambda expressions are expressions of the form (lambda (v1
... vn) body) where the vi are distinct legal variable symbols, body is
a term, and the only free variables in body are among the vi.

The function termp, which takes two arguments, an alleged term x and a
logical world w (see *Note WORLD::), recognizes terms of a given
extension of the logic.  Termp is defined in :program mode.  Its
definition may be inspected with :pe termp for a complete specification
of what we mean by "term" in the most strict sense.  Most ACL2
term-processing functions deal with terms in this strict sense and use
termp as a guard.  That is, the "internal form" of a term satisfies
termp, the strict sense of the word "term."

*Untranslated Terms:  What the User Types*

While terms in the strict sense are easy to explore (because their
structure is so regular and simple) they can be cumbersome to type.
Thus, ACL2 supports a more sugary syntax that includes uses of macros
and constant symbols.  Very roughly speaking, macros are functions that
produce terms as their results.  Constants are symbols that are
associated with quoted objects.  Terms in this sugary syntax are
"translated" to terms in the strict sense; the sugary syntax is more
often called "untranslated."  Roughly speaking, translation just
implements macroexpansion, the replacement of constant symbols by their
quoted values, and the checking of all the rules governing the strict
sense of "term."

More precisely, macro symbols are as described in the documentation for
defmacro.  A macro, mac, can be thought of as a function, mac-fn, from
ACL2 objects to an ACL2 object to be treated as an untranslated term.
For example, caar is defined as a macro symbol; the associated macro
function maps the object x into the object (car (car x)).  A macro form
is a "call" of a macro symbol, i.e., a list whose car is the macro
symbol and whose cdr is an arbitrary true list of objects, used as a
term.  Macroexpansion is the process of replacing in an untranslated
term every occurrence of a macro form by the result of applying the
macro function to the appropriate arguments.  The "appropriate"
arguments are determined by the exact form of the definition of the
macro; macros support positional, keyword, optional and other kinds of
arguments.  See *Note DEFMACRO::.

In addition to macroexpansion and constant symbol dereferencing,
translation implements the mapping of let and let* forms into
applications of lambda expressions and closes lambda expressions
containing free variables.  Thus, the translation of

     (let ((x (1+ i))) (cons x k))

can be seen as a two-step process that first produces

     ((lambda (x) (cons x k)) (1+ i))

and then

     ((lambda (x k) (cons x k)) (1+ i) k) .

Observe that the body of the let and of the first lambda expression
contains a free k which is finally bound and passed into the second
lambda expression.

When we say, of an event-level function such as defun or defthm, that
some argument "must be a term" we mean an untranslated term.  The event
functions translate their term-like arguments.

To better understand the mapping between untranslated terms and
translated terms it is convenient to use the keyword command :trans to
see examples of translations.  See *Note TRANS:: and also see *Note
TRANS1::.

*Pseudo-Terms:  A Common Guard for Metafunctions*

Because termp is defined in :program mode, it cannot be used effectively
in conjectures to be proved.  Furthermore, from the perspective of
merely guarding a term processing function, termp often checks more than
is required.  Finally, because termp requires the logical world as one
of its arguments it is impossible to use termp as a guard in places
where the logical world is not itself one of the arguments.

For these reasons we support the idea of "pseudo-terms."  A pseudo-term
is either a symbol (but not necessarily one having the syntax of a legal
variable symbol), a true list beginning with quote (but not necessarily
well-formed), or the "application of" a symbol or pseudo lambda
expression to a true list of pseudo-terms.  A pseudo lambda expression
is an expression of the form (lambda (v1 ... vn) body) where the vi are
all symbols and body is a pseudo-term.

Pseudo-terms are recognized by the unary function pseudo-termp.  If
(termp x w) is true, then (pseudo-termp x) is true.  However, if x fails
to be a (strict) term it may nevertheless still be a pseudo-term.  For
example, (car a b) is not a term, because car is applied to the wrong
number of arguments, but it is a pseudo-term.

The structures recognized by pseudo-termp can be recursively explored
with the same simplicity that terms can be.  In particular, if x is not
a variablep or an fquotep, then (ffn-symb x) is the function (symbol or
lambda expression) and (fargs x) is the list of argument pseudo-terms.
A metafunction may use pseudo-termp as the guard.




File: acl2-doc-emacs.info, Node: TERM-ORDER, Next: TTREE, Prev: TERM, Up: MISCELLANEOUS

TERM-ORDER    the ordering relation on terms used by ACL2

ACL2 must occasionally choose which of two terms is syntactically
smaller.  The need for such a choice arises, for example, when using
equality hypotheses in conjectures (the smaller term is substituted for
the larger elsewhere in the formula), in stopping loops in permutative
rewrite rules (see *Note LOOP-STOPPER::), and in choosing the order in
which to try to cancel the addends in linear arithmetic inequalities.
When this notion of syntactic size is needed, ACL2 uses "term order."
Popularly speaking, term order is just a lexicographic ordering on
terms.  But the situation is actually more complicated.

We define term order only with respect to terms in translated form.  See
*Note TRANS::.

Term1 comes before term2 in the term order iff

     (a) the number of variable occurrences in term1 is less than that
     in term2, or

     (b) the numbers of variable occurrences in the two terms are equal
     but the number of function applications in term1 is less than that
     in term2, or

     (c) the numbers of variable occurrences in the two terms are equal,
     the numbers of functions applications in the two terms are equal,
     and term1 comes before term2 in a certain lexicographic ordering
     based their structure as Lisp objects.


The function term-order, when applied to the translations of two ACL2
terms, returns t iff the first is "less than or equal" to the second in
the term order.

By "number of variable occurrences" we do not mean "number of distinct
variables" but "number of times a variable symbol is mentioned."  (cons
x x) has two variable occurrences, not one.  Thus, perhaps
counterintuitively, a large term that contains only one variable
occurrence, e.g., (standard-char-p (car (reverse x))) comes before (cons
x x) in the term order.

Since constants contain no variable occurrences and non-constant
expressions must contain at least one variable occurrence, constants
come before non-constants in the term order, no matter how large the
constants.  For example, the list constant

     '(monday tuesday wednesday thursday friday)

comes before x in the term order.  Because term order is involved in the
control of permutative rewrite rules and used to shift smaller terms to
the left, a set of permutative rules designed to allow the permutation
of any two tips in a tree representing the nested application of some
function will always move the constants into the left-most tips.  Thus,

     (+ x 3 (car (reverse klst)) (dx i j)) ,

which in translated form is

     (binary-+ x
               (binary-+ '3
                         (binary-+ (dx i j)
                                   (car (reverse klst))))),

will be permuted under the built-in commutativity rules to

     (binary-+ '3
               (binary-+ x
                         (binary-+ (car (reverse klst))
                                   (dx i j))))

or

     (+ 3 x (car (reverse klst)) (dx i j)).

Clearly, two constants are ordered using cases (b) and (c) of term
order, since they each contain 0 variable occurrences.  This raises the
question "How many function applications are in a constant?"  Because we
regard the number of function applications as a more fundamental measure
of the size of a constant than lexicographic considerations, we decided
that for the purposes of term order, constants would be seen as being
built by primitive constructor functions.  These constructor functions
are not actually defined in ACL2 but merely imagined for the purposes of
term order.  We here use suggestive names for these imagined functions,
ignoring entirely the prior use of these names within ACL2.

The constant function z constructs 0.  Positive integers are constructed
from (z) by the successor function, s.  Thus 2 is (s (s (z))) and
contains three function applications.  100 contains one hundred and one
applications.  Negative integers are constructed from their positive
counterparts by -.  Thus, -2 is (- (s (s (z)))) and has four
applications.  Ratios are constructed by the dyadic function /.  Thus,
-1/2 is

     (/ (- (s (z))) (s (s (z))))

and contains seven applications.  Complex rationals are similarly
constructed from rationals.  All character objects are considered
primitive and are constructed by constant functions of the same name.
Thus #\a and #\b both contain one application.  Strings are built from
the empty string, (o) by the "string-cons" function written cs.  Thus
"AB" is (cs (#\a) (cs (#\b) (o))) and contains five applications.
Symbols are obtained from strings by "packing" the symbol-name with the
unary function p.  Thus 'ab is

     (p (cs (#\a) (cs (#\b) (o))))

and has six applications.  Note that packages are here ignored and thus
'acl2::ab and 'my-package::ab each contain just six applications.
Finally, conses are built with cons, as usual.  So '(1 . 2) is (cons '1
'2) and contains six applications, since '1 contains two and '2 contains
three.  This, for better or worse, answers the question "How many
function applications are in a constant?"

Two terms with the same numbers of variable occurrences and function
applications are ordered by lexicographic means, based on their
structures.  In the lexicographic ordering, two atoms are ordered
"alphabetically" as described below, an atom and a cons are ordered so
that the atom comes first, and two conses are ordered so that the one
with the recursively smaller car comes first, with the cdrs being
compared only if the cars are equal.  Thus, if two terms (member ...)
and (reverse ...) contain the same numbers of variable occurrences and
function applications, then the member term is first in the term order
because member comes before reverse in the term order (which is here
reduced to alphabetic ordering).

It remains only to define what we mean by the alphabetic ordering on
Lisp atoms.  Within a single type, numbers are compared arithmetically,
characters are compared via their (char) codes, and strings and symbols
are compared with the conventional alphabetic ordering on sequences of
characters.  Across types, numbers come before characters, characters
before strings, and strings before symbols.




File: acl2-doc-emacs.info, Node: TTREE, Next: TYPE-SET, Prev: TERM-ORDER, Up: MISCELLANEOUS

TTREE    tag trees

Many low-level ACL2 functions take and return "tag trees" or "ttrees"
(pronounced "tee-trees") which contain various useful bits of
information such as the lemmas used, the linearize assumptions made,
etc.

Let a "tagged pair" be a list whose car is a symbol, called the "tag,"
and whose cdr is an arbitrary object, called the "tagged object."  A
"tag tree" is either nil, a tagged pair consed onto a tag tree, or a
non-nil tag tree consed onto a tag tree.

Abstractly a tag tree represents a list of sets, each member set having
a name given by one of the tags occurring in the ttree.  The elements of
the set named tag are all of the objects tagged tag in the tree.  To
cons a tagged pair (tag . obj) onto a tree is to add-to-set-equal obj to
the set corresponding to tag.  To cons two tag trees together is to
union-equal the corresponding sets.  The concrete representation of the
union so produced has duplicates in it, but we feel free to ignore or
delete duplicates.

The beauty of this definition is that to combine two non-nil tag trees
you need do only one cons.

The following function accumulates onto ans the set associated with a
given tag in a ttree:

     (defun tagged-objects (tag ttree ans)
      (cond
       ((null ttree) ans)
       ((symbolp (caar ttree))             ; ttree = ((tag . obj) . ttree)
        (tagged-objects tag (cdr ttree)
                        (cond ((eq (caar ttree) tag)
                               (add-to-set-equal (cdar ttree) ans))
                              (t ans))))
       (t                                  ; ttree = (ttree . ttree)
          (tagged-objects tag (cdr ttree)
                              (tagged-objects tag (car ttree) ans)))))

This function is defined as a :PROGRAM mode function in ACL2.

The rewriter, for example, takes a term and a ttree (among other
things), and returns a new term, term', and new ttree, ttree'.  Term' is
equivalent to term (under the current assumptions) and the ttree' is an
extension of ttree.  If we focus just on the set associated with the tag
LEMMA in the ttrees, then the set for ttree' is the extension of that
for ttree obtained by unioning into it all the runes used by the
rewrite.  The set associated with LEMMA can be obtained by
(tagged-objects 'LEMMA ttree nil).




File: acl2-doc-emacs.info, Node: TYPE-SET, Next: USING-COMPUTED-HINTS, Prev: TTREE, Up: MISCELLANEOUS

TYPE-SET    how type information is encoded in ACL2

To help you experiment with type-sets we briefly note the following
utility functions.

(type-set-quote x) will return the type-set of the object x.  For
example, (type-set-quote "test") is 2048 and (type-set-quote '(a b c))
is 512.

(type-set 'term nil nil nil nil (ens state) (w state) nil) will return
the type-set of term.  For example,

     (type-set '(integerp x) nil nil nil nil (ens state) (w state) nil)

will return (mv 192 nil).  192, otherwise known as *ts-boolean*, is the
type-set containing t and nil.  The second result may be ignored in
these experiments.  Term must be in the translated, internal form shown
by :trans.  See *Note TRANS::and see *Note TERM::.

(type-set-implied-by-term 'x nil 'term (ens state)(w state) nil) will
return the type-set deduced for the variable symbol x assuming the
translated term, term, true.  The second result may be ignored in these
experiments.  For example,

     (type-set-implied-by-term 'v nil '(integerp v)
                               (ens state) (w state) nil)

returns 11.

(convert-type-set-to-term 'x ts (ens state) (w state) nil) will return a
term whose truth is equivalent to the assertion that the term x has
type-set ts.  The second result may be ignored in these experiments.
For example

     (convert-type-set-to-term 'v 523 (ens state) (w state) nil)

returns a term expressing the claim that v is either an integer or a
non-nil true-list.  523 is the logical-or of 11 (which denotes the
integers) with 512 (which denotes the non-nil true-lists).

The "actual primitive types" of ACL2 are listed in
*actual-primitive-types*.  These primitive types include such types
as *ts-zero*, *ts-positive-integer*, *ts-nil* and *ts-proper-consp*.
Each actual primitive type denotes a set -- sometimes finite and
sometimes not -- of ACL2 objects and these sets are pairwise
disjoint.  For example, *ts-zero* denotes the set containing 0 while
*ts-positive-integer* denotes the set containing all of the positive
integers.

The actual primitive types were chosen by us to make theorem proving
convenient.  Thus, for example, the actual primitive type *ts-nil*
contains just nil so that we can encode the hypothesis "x is nil"
by saying "x has type *ts-nil*" and the hypothesis "x is
non-nil" by saying "x has type complement of *ts-nil*."  We
similarly devote a primitive type to t, *ts-t*, and to a third type,
*ts-non-t-non-nil-symbol*, to contain all the other ACL2 symbols.

Let *ts-other* denote the set of all Common Lisp objects other than
those in the actual primitive types.  Thus, *ts-other* includes such
things as floating point numbers and CLTL array objects.  The actual
primitive types together with *ts-other* constitute what we call
*universe*.  Note that *universe* is a finite set containing one
more object than there are actual primitive types; that is, here we are
using *universe* to mean the finite set of primitive types, not the
infinite set of all objects in all of those primitive types.
*Universe* is a partitioning of the set of all Common Lisp objects:
every object belongs to exactly one of the sets in
*universe*.

Abstractly, a "type-set" is a subset of *universe*.  To say that a term,
x, "has type-set ts" means that under all possible assignments to the
variables in x, the value of x is a member of some member of ts.  Thus,
(cons x y) has type-set {*ts-proper-cons* *ts-improper-cons*}.  A term
can have more than one type-set.  For example, (cons x y) also has the
type-set {*ts-proper-cons* *ts-improper-cons* *ts-nil*}.  Extraneous
types can be added to a type-set without invalidating the claim that a
term "has" that type-set.  Generally we are interested in the smallest
type-set a term has, but because the entire theorem-proving problem for
ACL2 can be encoded as a type-set question, namely, "Does p have
type-set complement of *ts-nil*?," finding the smallest type-set for a
term is an undecidable problem.  When we speak informally of "the"
type-set we generally mean "the type-set found by our heuristics" or
"the type-set assumed in the current context."

Note that if a type-set, ts, does not contain *ts-other* as an
element then it is just a subset of the actual primitive types.  If
it does contain *ts-other* it can be obtained by subtracting from
*universe* the complement of ts.  Thus, every type-set can be
written as a (possibly complemented) subset of the actual primitive
types.

By assigning a unique bit position to each actual primitive type we
can encode every subset, s, of the actual primitive types by the
nonnegative integer whose ith bit is on precisely if s contains the
ith actual primitive type.  The type-sets written as the complement
of s are encoded as the twos-complement of the encoding of s.  Those
type-sets are thus negative integers.  The bit positions assigned to
the actual primitive types are enumerated from 0 in the same order
as the types are listed in *actual-primitive-types*.  At the
concrete level, a type-set is an integer between *min-type-set* and
*max-type-set*, inclusive.

For example, *ts-nil* has bit position 6.  The type-set containing just
*ts-nil* is thus represented by 64.  If a term has type-set 64 then the
term is always equal to nil.  The type-set containing everything but
*ts-nil* is the twos-complement of 64, which is -65.  If a term has
type-set -65, it is never equal to nil.  By "always" and "never" we mean
under all, or under no, assignments to the variables, respectively.

Here is a more complicated example.  Let s be the type-set containing
all of the symbols and the natural numbers.  The relevant actual
primitive types, their bit positions and their encodings are:

     actual primitive type       bit    value

     *ts-zero*                    0       1
     *ts-positive-integer*        1       2
     *ts-nil*                     6      64
     *ts-t*                       7     128
     *ts-non-t-non-nil-symbol*    8     256

Thus, the type-set s is represented by (+ 1 2 64 128 256) = 451.  The
complement of s, i.e., the set of all objects other than the natural
numbers and the symbols, is -452.




File: acl2-doc-emacs.info, Node: USING-COMPUTED-HINTS, Next: USING-COMPUTED-HINTS-1, Prev: TYPE-SET, Up: MISCELLANEOUS

USING-COMPUTED-HINTS    how to use computed hints

Computed hints are extraordinarily powerful.  We show a few examples
here to illustrate their use.  We recommend that these be read in the
following sequence:



* Menu:


Related topics other than immediate subtopics:
* USING-COMPUTED-HINTS-1:: Driving Home the Basics

* USING-COMPUTED-HINTS-2:: One Hint to Every Top-Level Goal in a Forcing Round

* USING-COMPUTED-HINTS-3:: Hints as a Function of the Goal (not its Name)

* USING-COMPUTED-HINTS-4:: Computing the Hints

* USING-COMPUTED-HINTS-5:: Debugging Computed Hints

* USING-COMPUTED-HINTS-6:: Some Final Comments







File: acl2-doc-emacs.info, Node: USING-COMPUTED-HINTS-1, Next: USING-COMPUTED-HINTS-2, Prev: USING-COMPUTED-HINTS, Up: MISCELLANEOUS

USING-COMPUTED-HINTS-1    Driving Home the Basics

The common hint

     ("Subgoal 3.2.1"" :use lemma42)

has the same effect as the computed hint

     (if (equal id '((0) (3 2 1) . 2))
         '(:use lemma42)
         nil)

which, of course, is equivalent to

     (and (equal id '((0) (3 2 1) . 2))
          '(:use lemma42))

which is also equivalent to the computed hint

     my-special-hint

provided the following defun has first been executed

     (defun my-special-hint (id clause world)
       (declare (xargs :mode :program)
                (ignore clause world))
       (if (equal id '((0) (3 2 1) . 2))
           '(:use lemma42)
           nil))

It is permitted for the defun to be in :LOGIC mode (see *Note
DEFUN-MODE::) also.

Just to be concrete, the following three events all behave the same way
(if my-special-hint is as above):


     (defthm main (big-thm a b c)
       :hints (("Subgoal 3.2.1"" :use lemma42)))

     (defthm main (big-thm a b c)
       :hints ((and (equal id '((0) (3 2 1) . 2)) '(:use lemma42))))

     (defthm main (big-thm a b c)
       :hints (my-special-hint))





File: acl2-doc-emacs.info, Node: USING-COMPUTED-HINTS-2, Next: USING-COMPUTED-HINTS-3, Prev: USING-COMPUTED-HINTS-1, Up: MISCELLANEOUS

USING-COMPUTED-HINTS-2    One Hint to Every Top-Level Goal in a Forcing Round

Suppose the main proof completes with a forcing round on three subgoals,
"[1]Subgoal 3", "[1]Subgoal 2", and "[1]Subgoal 1".  Suppose you wish to
:use lemma42 in all top-level goals of the first forcing round.  This
can be done supplying the hint

     (if test '(:use lemma42) nil),

where test is an expression that returns t when ID is one of the clause
ids in question.

         goal-spec     (parse-clause-id goal-spec)

     "[1]Subgoal 3"        ((1) (3) . 0)
     "[1]Subgoal 2"        ((1) (2) . 0)
     "[1]Subgoal 1"        ((1) (1) . 0)

Recall (see *Note CLAUSE-IDENTIFIER::) that parse-clause-id maps from a
goal spec to a clause id, so you can use that function on the goal specs
printed in the failed proof attempt to determine the clause ids in
question.

So one acceptable test is

     (member-equal id '(((1) (3) . 0) 
                        ((1) (2) . 0)
                        ((1) (1) . 0)))

or you could use parse-clause-id in your computed hint if you don't want
to see clause ids in your script:

     (or (equal id (parse-clause-id "[1]Subgoal 3"))
         (equal id (parse-clause-id "[1]Subgoal 2"))
         (equal id (parse-clause-id "[1]Subgoal 1")))

or you could use the inverse function (see *Note CLAUSE-IDENTIFIER::):

     (member-equal (string-for-tilde-@-clause-id-phrase id)
                   '("[1]Subgoal 3"
                     "[1]Subgoal 2"
                     "[1]Subgoal 1"))


Recall that what we've shown above are the tests to use in the computed
hint.  The hint itself is (if test '(:use lemma42) nil) or something
equivalent like (and test '(:use lemma42)).

The three tests above are all equivalent.  They suffer from the problem
of requiring the explicit enumeration of all the goal specs in the first
forcing round.  A change in the script might cause more forced subgoals
and the ones other than those enumerated would not be given the hint.

You could write a test that recognizes all first round top-level
subgoals no matter how many there are.  Just think of the programming
problem: how do I recognize all the clause id's of the form ((1) (n)
. 0)?  Often you can come to this formulation of the problem by using
parse-clause-id on a few of the candidate goal-specs to see the common
structure.  A suitable test in this case is:

     (and (equal (car id) '(1))     ; forcing round 1, top-level (pre-induction)
          (equal (len (cadr id)) 1) ; Subgoal n (not Subgoal n.i ...)
          (equal (cddr id) 0))      ; no primes


The test above is "overkill" because it recognizes precisely the clause
ids in question.  But recall that once a computed hint is used, it is
removed from the hints available to the children of the clause.  Thus,
we can widen the set of clause ids recognized to include all the
children without worrying that the hint will be applied to those
children.

In particular, the following test supplies the hint to every top-level
goal of the first forcing round:

     (equal (car id) '(1))

You might worry that it would also supply the hint to the subgoal
produced by the hint -- the cases we ruled out by the "overkill" above.
But that doesn't happen since the hint is unavailable to the children.
You could even write:

     (equal (car (car id)) 1)

which would supply the hint to every goal of the form "[1]Subgoal ..."
and again, because we see and fire on the top-level goals first, we will
not fire on, say, "[1]Subgoal *1.3/2", i.e., the id '((1 1 3) (2) . 0)
even though the test recognizes that id.

Finally, the following test supplies the hint to every top-level goal of
every forcing round (except the 0th, which is the "gist" of the proof,
not "really" a forcing round):

     (not (equal (car (car id)) 0))


Recall again that in all the examples above we have exhibited the test
in a computed hint of the form (if test '(:key1 val1 ...) nil).




File: acl2-doc-emacs.info, Node: USING-COMPUTED-HINTS-3, Next: USING-COMPUTED-HINTS-4, Prev: USING-COMPUTED-HINTS-2, Up: MISCELLANEOUS

USING-COMPUTED-HINTS-3    Hints as a Function of the Goal (not its Name)

Sometimes it is desirable to supply a hint whenever a certain term
arises in a conjecture.  For example, suppose we have proved

     (defthm all-swaps-have-the-property
        (the-property (swap x))
        :rule-classes nil)

and suppose that whenever (SWAP A) occurs in a goal, we wish to add the
additional hypothesis that (THE-PROPERTY (SWAP A)).  Note that this is
equivalent supplying the hint

     (if test
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

where test answers the question "does the clause contain (SWAP A)?"
That question can be asked with (occur-lst '(SWAP A) clause).  Briefly,
occur-lst takes the representation of a translated term, x, and a list
of translated terms, y, and determines whether x occurs as a subterm of
any term in y.  (By "subterm" here we mean proper or improper, e.g., the
subterms of (CAR X) are X and (CAR X).)

Thus, the computed hint:

     (if (occur-lst '(swap a) clause)
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

will add the hypothesis (THE-PROPERTY (SWAP A)) to every goal containing
(SWAP A) -- except the children of goals to which the hypothesis was
added.

A COMMON MISTAKE users are likely to make is to forget that they are
dealing with translated terms.  For example, suppose we wished to look
for (SWAP (LIST 1 A)) with occur-lst.  We would never find it with

     (occur-lst '(SWAP (LIST 1 A)) clause)

because that presentation of the term contains macros and other
abbreviations.  By using :trans (see *Note TRANS::) we can obtain the
translation of the target term.  Then we can look for it with:

     (occur-lst '(SWAP (CONS '1 (CONS A 'NIL))) clause)

Note in particular that you must

     * eliminate all macros and
     * explicitly quote all constants.

We recommend using :trans to obtain the translated form of the terms in
which you are interested, before programming your hints.

An alternative is to use the expression (prettyify-clause clause) in
your hint to convert the current goal clause into the s-expression that
is actually printed.  For example, the clause

     ((NOT (CONSP X)) (SYMBOLP Y) (EQUAL (CONS '1 (CAR X)) Y)) 

"prettyifies" to

     (IMPLIES (AND (CONSP X)
                   (NOT (SYMBOLP Y)))
              (EQUAL (CONS 1 (CAR X)) Y))

which is what you would see printed by ACL2 when the goal clause is that
shown.

However, if you choose to convert your clauses to prettyified form, you
will have to write your own explorers (like our occur-lst), because all
of the ACL2 term processing utilities work on translated and/or clausal
forms.  This should not be taken as a terrible burden.  You will, at
least, gain the benefit of knowing what you are really looking for,
because your explorers will be looking at exactly the s-expressions you
see at your terminal.  And you won't have to wade through our still
undocumented term/clause utilities.  The approach will slow things down
a little, since you will be paying the price of independently consing up
the prettyified term.

We make one more note on this example.  We said above that the computed
hint:

     (if (occur-lst '(swap a) clause)
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

will add the hypothesis (THE-PROPERTY (SWAP A)) to every goal containing
(SWAP A) -- except the children of goals to which the hypothesis was
added.

It bears noting that the subgoals produced by induction and top-level
forcing round goals are not children.  For example, suppose the hint
above fires on "Subgoal 3" and produces, say, "Subgoal 3'".  Then the
hint will not fire on "Subgoal 3'" even though it (still) contains (SWAP
A) because "Subgoal 3'" is a child of a goal on which the hint fired.

But now suppose that "Subgoal 3'" is pushed for induction.  Then the
goals created by that induction, i.e., the base case and induction step,
are not considered children of "Subgoal 3'".  All of the original hints
are available.

Alternatively, suppose that "Subgoal 3' is proved but forces some other
subgoal, "[1]Subgoal 1" which is attacked in Forcing Round 1.  That
top-level forced subgoal is not a child.  All the original hints are
available to it.  Thus, if it contains (SWAP A), the hint will fire and
supply the hypothesis, producing "[1]Subgoal 1'".  This may be
unnecessary, as the hypothesis might already be present in "[1]Subgoal
1".  In this case, no harm is done.  The hint won't fire on "[1]Subgoal
1" because it is a child of "[1]Subgoal 1" and the hint fired on that.




File: acl2-doc-emacs.info, Node: USING-COMPUTED-HINTS-4, Next: USING-COMPUTED-HINTS-5, Prev: USING-COMPUTED-HINTS-3, Up: MISCELLANEOUS

USING-COMPUTED-HINTS-4    Computing the Hints

So far we have used computed hints only to compute when a fixed set of
keys and values are to be used as a hint.  But computed hints can, of
course, compute the set of keys and values.  You might, for example,
write a hint that recognizes when a clause "ought" to be provable by a
:BDD hint and generate the appropriate hint.  You might build in a set
of useful lemmas and check to see if the clause is proveable :BY one of
them.  You can keep all function symbols disabled and use computed hints
to compute which ones you want to :EXPAND.  In general, you can write a
theorem prover for use in your hints, provided you can get it do its job
by directing our theorem prover.

Suppose for example we wish to find every occurrence of an instance of
(SWAP x) and provide the corresponding instance of
ALL-SWAPS-HAVE-THE-PROPERTY.  Obviously, we must explore the clause
looking for instances of (SWAP x) and build the appropriate instances of
the lemma.  We could do this in many different ways, but below we show a
general purpose set of utilities for doing it.  The functions are not
defined in ACL2 but could be defined as shown.

Our plan is: (1) Find all instances of a given pattern (term) in a
clause, obtaining a set of substitutions.  (2) Build a set of :instance
expressions for a given lemma name and set of substitutions.  (3)
Generate a :use hint for those instances when instances are found.

The pair of functions below find all instances of a given pattern term
in either a term or a list of terms.  The functions each return a list
of substitutions, each substitution accounting for one of the matches of
pat to a subterm.  At this level in ACL2 substitutions are lists of
pairs of the form (var . term).  All terms mentioned here are presumed
to be in translated form.

The functions take as their third argument a list of substitutions
accumulated to date and add to it the substitutions produced by matching
pat to the subterms of the term.  We intend this accumulator to be nil
initially.  If the returned value is nil, then no instances of pat
occurred.


     (mutual-recursion
 
     (defun find-all-instances (pat term alists)
      (declare (xargs :mode :program))
      (mv-let
       (instancep alist)
       (one-way-unify pat term)
       (let ((alists (if instancep (add-to-set-equal alist alists) alists)))
         (cond
          ((variablep term) alists)
          ((fquotep term) alists)
          ((flambdap (ffn-symb term))
           (find-all-instances pat
                               (lambda-body (ffn-symb term))
                               (find-all-instances-list pat (fargs term) alists)))
          (t (find-all-instances-list pat (fargs term) alists))))))

     (defun find-all-instances-list (pat list-of-terms alists)
      (declare (xargs :mode :program))
      (cond
       ((null list-of-terms) alists)
       (t (find-all-instances pat
                              (car list-of-terms)
                              (find-all-instances-list pat
                                                       (cdr list-of-terms)
                                                       alists))))))


We now turn our attention to converting a list of substitutions into a
list of lemma instances, each of the form

     (:INSTANCE name (var1 term1) ... (vark termk))

as written in :use hints.  In the code shown above, substitutions are
lists of pairs of the form (var . term), but in lemma instances we must
write "doublets."  So here we show how to convert from one to the other:

     (defun pairs-to-doublets (alist)
       (declare (xargs :mode :program))
       (cond ((null alist) nil)
             (t (cons (list (caar alist) (cdar alist))
                      (pairs-to-doublets (cdr alist))))))


Now we can make a list of lemma instances:

     (defun make-lemma-instances (name alists)
       (declare (xargs :mode :program))
       (cond
        ((null alists) nil)
        (t (cons (list* :instance name (pairs-to-doublets (car alists)))
                 (make-lemma-instances name (cdr alists))))))


Finally, we can package it all together into a hint function.  The
function takes a pattern, pat, which must be a translated term, the name
of a lemma, name, and a clause.  If some instances of pat occur in
clause, then the corresponding instances of name are :USEd in the
computed hint.  Otherwise, the hint does not apply.

     (defun add-corresponding-instances (pat name clause)
       (declare (xargs :mode :program))
       (let ((alists (find-all-instances-list pat clause nil)))
         (cond
          ((null alists) nil)
          (t (list :use (make-lemma-instances name alists))))))

The design of this particular hint function makes it important that the
variables of the pattern be the variables of the named lemma and that
all of the variables we wish to instantiate occur in the pattern.  We
could, of course, redesign it to allow "free variables" or some sort of
renaming.

We could now use this hint as shown below:

     (defthm ... ...
       :hints ((add-corresponding-instances
                '(SWAP x)
                'ALL-SWAPS-HAVE-THE-PROPERTY
                clause)))

The effect of the hint above is that any time a clause arises in which
any instance of (SWAP x) appears, we add the corresponding instance of
ALL-SWAPS-HAVE-THE-PROPERTY.  So for example, if Subgoal *1/3.5 contains
the subterm (SWAP (SWAP A)) then this hint fires and makes the system
behave as though the hint:

     ("Subgoal *1/3.5"
      :USE ((:INSTANCE ALL-SWAPS-HAVE-THE-PROPERTY (X A))
            (:INSTANCE ALL-SWAPS-HAVE-THE-PROPERTY (X (SWAP A)))))

had been present.




File: acl2-doc-emacs.info, Node: USING-COMPUTED-HINTS-5, Next: USING-COMPUTED-HINTS-6, Prev: USING-COMPUTED-HINTS-4, Up: MISCELLANEOUS

USING-COMPUTED-HINTS-5    Debugging Computed Hints

We have found that it is sometimes helpful to define hints so that they
print out messages to the terminal when they fire, so you can see what
hint was generated and which of your computed hints did it.

To that end we have defined a macro we sometimes use.  Suppose you have
a :hints specification such as:

     :hints (computed-hint-fn (hint-expr id))

If you defmacro the macro below you could then write instead:

     :hints ((show-hint computed-hint-fn 1)
             (show-hint (hint-expr id) 2))

with the effect that whenever either hint is fired (i.e., returns
non-nil), a message identifying the hint by the marker (1 or 2, above)
and the non-nil value is printed.


     (defmacro show-hint (hint &optional marker)
       (cond
        ((and (consp hint)
              (stringp (car hint)))
         hint)
        (t
         `(let ((marker ,marker)
                (ans ,(if (symbolp hint)
                          `(,hint id clause world)
                        hint)))
            (if ans
                (prog2$
                 (cw "~%***** Computed Hint~#0~[~/ (from hint ~x1)~]~%~x2~%~%"
                     (if (null marker) 0 1)
                     marker
                     (cons (string-for-tilde-@-clause-id-phrase id)
                           ans))
                 ans)
              nil)))))

Putting a show-hint around a common hint has no effect.  If you find
yourself using this utility let us know and we'll consider putting it
into the system itself.  But it does illustrate that you can use
computed hints to do unusual things.




File: acl2-doc-emacs.info, Node: USING-COMPUTED-HINTS-6, Next: VERSION, Prev: USING-COMPUTED-HINTS-5, Up: MISCELLANEOUS

USING-COMPUTED-HINTS-6    Some Final Comments

None of the examples show the use of the variable WORLD, which is
allowed in computed hints.  There are some (undocumented) ACL2 utilities
that might be useful in programming hints, but these utilities need
access to the ACL2 logical world (see *Note WORLD::).

Using these utilities to look at the WORLD one can, for example,
determine whether a symbol is defined recursively or not, get the body
and formals of a defined function, or fetch the statement of a given
lemma.  Because these utilities are not yet documented, we do not expect
users to employ WORLD in computed hints.  But experts might and it might
lead to the formulation of a more convenient language for computed
hints.

If you start using computed hints extensively, please contact the
developers of ACL2 and let us know what you are doing with them and how
we can help.




File: acl2-doc-emacs.info, Node: VERSION, Next: WHY-BRR, Prev: USING-COMPUTED-HINTS-6, Up: MISCELLANEOUS

VERSION    ACL2 Version Number

To determine the version number of your copy of ACL2, evaluate the ACL2
constant *acl2-version*.  The value will be a string.  For example,

     ACL2 !>*acl2-version*
     "ACL2 Version 1.9"



Books are considered certified only in the same version of ACL2 in which
the certification was done.  The certificate file records the version
number of the certifying ACL2 and include-book considers the book
uncertified if that does not match the current version number.  Thus,
each time we release a new version of ACL2, previously certified books
must be recertified.

One reason for this is immediately obvious from the fact that the
version number is a logical constant in the ACL2 theory: changing the
version number changes the axioms!  For example, in version 1.8 you can
prove

     (defthm version-8
       (equal *acl2-version* "ACL2 Version 1.8"))

while in version 1.9 you can prove

     (defthm version-9
       (equal *acl2-version* "ACL2 Version 1.9"))

Thus, if a book containing the former were included into version 1.9,
one could prove a contradiction.

We could eliminate this particular threat of unsoundness by not
making the version number part of the axioms.  But there are over
150 constants in the system, most having to do with the fact that
ACL2 is coded in ACL2, and "version number inconsistency" is just
the tip of the iceberg.  Other likely-to-change constants include
*common-lisp-specials-and-constants*, which may change when we
port ACL2 to some new implementation of Common Lisp, and
*acl2-exports*, which lists commonly used ACL2 command names
users are likely to import into new packages.  Furthermore, it is
possible that from one version of the system to another we might change,
say, the default values on some system function or otherwise make
"intentional" changes to the axioms.  It is even possible one version of
the system is discovered to be unsound and we release a new version to
correct our error.

Therefore we adopted the draconian policy that books are certified by a
given version of ACL2 and must be recertified to be used in other
versions.  While there are less draconian solutions to the problems
illustrated above, we thought this was the simplest.




File: acl2-doc-emacs.info, Node: WHY-BRR, Next: WORLD, Prev: VERSION, Up: MISCELLANEOUS

WHY-BRR    an explanation of why ACL2 has an explicit brr mode

Why isn't brr mode automatically disabled when there are no monitored
runes?  The reason is that the list of monitored runes is kept in a
wormhole state.

See *Note WORMHOLE:: for more information on wormholes in general.  But
the fundamental property of the wormhole function is that it is a
logical no-op, a constant function that does not take state as an
argument.  When entering a wormhole, arbitrary information can be passed
in (including the external state).  That information is used to
construct a near copy of the external state and that "wormhole state" is
the one with respect to which interactions occur during breaks.  But no
information is carried by ACL2 out of a wormhole --- if that were
allowed wormholes would not be logical no-ops.  The only information
carried out of a wormhole is in the user's head.

Break-rewrite interacts with the user in a wormhole state because the
signature of the ACL2 rewrite function does not permit it to modify
state.  Hence, only wormhole interaction is possible.  (This has the
additional desirable property that the correctness of the rewriter does
not depend on what the user does during interactive breaks within it;
indeed, it is logically impossible for the user to affect the course of
rewrite.)

Now consider the list of monitored runes.  Is that kept in the external
state as a normal state global or is it kept in the wormhole state?  If
it is in the external state then it can be inspected within the wormhole
but not changed.  This is unacceptable; it is common to change the
monitored rules as the proof attempt progresses, installing monitors
when certain rules are about to be used in certain contexts.  Thus, the
list of monitored runes must be kept as a wormhole variable.  Hence, its
value cannot be determined outside the wormhole, where the proof attempt
is ongoing.

This raises another question: If the list of monitored runes is unknown
to the rewriter operating on the external state, how does the rewriter
know when to break?  The answer is simple: it breaks every time, for
every rune, if brr mode is enabled.  The wormhole is entered (silently),
computations are done within the wormhole state to determine if the user
wants to see the break, and if so, interactions begin.  For unmonitored
runes and runes with false break conditions, the silent wormhole entry
is followed by a silent wormhole exit and the user perceives no break.

Thus, the penalty for running with brr mode enabled when there are no
monitored runes is high: a wormhole is entered on every application of
every rune and the user is simply unware of it.  The user who has
finally unmonitored all runes is therefore strongly advised to carry
this information out of the wormhole and to do :brr nil in the external
state when the next opportunity arises.