Major Section: MISCELLANEOUS

It is illegal for one of the functions introduced in the signature
of an `encapsulate`

event to be involved in the induction scheme
suggested by a non-`local`

ly defined recursive function in that
`encapsulate`

. Such recursive functions can give rise to so-called
``subversive'' induction schemes in the sense that when used outside
the `encapsulate`

the scheme is unsound. Normally, the induction
suggested by a function is justified by the termination proof for
the recursion. But in the case of recursive functions defined
within encapsulations, the termination proof is constructed in a
context in which the functions are to be viewed as ``constrained.''
The termination proof might therefore take advantage of properties
of the witnesses that are not exported from the `encapsulate`

.
Hence, crucial restrictions on the constrained functions may be
lost. We give examples and advice below.

The following (illegal) event illustrates the problem posed by subversive inductions.

(encapsulate ((test (x) t) (d (x) t) (p (x) t))Consider just the first three events above: the local definitions of(local (defun test (x) (consp x)))

(local (defun d (x) (declare (xargs :mode :logic)) (cdr x)))

(defun foo (x) (declare (xargs :mode :logic)) (if (test x) (foo (d x)) t))

(local (defun p (x) (declare (ignore x)) t))

(defthm base-case (implies (not (test x)) (p x)))

(defthm induction-step (implies (and (test x) (p (d x))) (p x))))

`test`

and `d`

and the non-local recursive function `foo`

. `Test`

and `d`

will be constrained to have certain properties, but within the
`encapsulate`

they are locally witnessed by `consp`

and `cdr`

,
respectively. Observe that `foo`

recurses by stepping from `x`

to `(d x)`

when `(test x)`

is true. This recursion terminates because of
properties of the witnesses for `test`

and `d`

. These properties need
not be exported from the encapsulation. But when `foo`

is exported
from the encapsulation, it suggests that it is permissible to
recur/induct by stepping ``down'' to `(d x)`

from `x`

when `(test x)`

is
true. Since we do not constrain `(d x)`

to be smaller than `x`

when
`(test x)`

the induction suggestion by `foo`

can be used to prove
non-theorems. Because `foo`

uses `test`

and `d`

in its recursion we say
the induction suggested by `foo`

is ``subversive'' outside the
encapsulation and do not permit such a `foo`

to be defined
non-locally. That is, the attempt to submit the encapsulate event
above will cause an error and complain about `foo`

.
We give some advice below on how to carry out such encapsulations as
might have been intended by that above. But first we show how an
inconsistency can be deduced when the above `encapsulate`

is
permitted.

Note that the `encapsulate`

introduced one other function symbol, `p`

.
Furthermore, the only constraints on `test`

, `d`

, and `p`

are the last
two theorems above. These theorems are the base case and induction
step for a proof of `(p x)`

based on the induction suggested by `foo`

.
We arrange for these theorems to be provable simply by defining `p`

locally to be `t`

.

Once outside the encapsulate we can prove `(p x)`

by the spurious
induction suggested by `foo`

.

(defthm p-true (p x) :hints (("Goal" :induct (foo x))))The proof is immediate given the two theorems exported from the

`encapsulate`

.
But then we can functionally instantiate `p`

in the theorem above to
be `nil`

! We must, of course, satisfy the constraints on `p`

, namely
the two theorems about `test`

, `d`

, and `p`

exported from the `encapsulate`

.
We can satisfy the constraints by choosing `test`

to be always `t`

.

(defthm subversion! nil :hints (("Goal" :use (:functional-instance p-true (test (lambda (x) t)) (p (lambda (x) nil))))) :rule-classes nil)This concludes our illustration of what can go wrong were we to permit recursive functions in encapsulations to use the constrained functions in their recursions. We now move on to our advice about how to achieve the (non-nefarious) ends intended by the disallowed encapsulations.

One often desires to define recursive functions such as `foo`

, i.e.,
functions that use constrained functions in their recursion.
However, one should not try to introduce such functions within the
same encapsulation as the constrained functions. Instead, introduce
the constrained functions, including among their constraints the
measure theorems sufficient to justify the intended recursive uses,
and define the recursive functions outside the encapsulation
environment. Thus, the following pair of events achieves, perhaps,
the intended effect of the original encapsulation:

(encapsulate ((test (x) t) (d (x) t)) (local (defun test (x) (consp x))) (local (defun d (x) (declare (xargs :mode :logic)) (cdr x))) (defthm d-decreases (implies (test x) (< (acl2-count (d x)) (acl2-count x)))))Another alternative, depending on one's original intentions, is to include the definition of(defun foo (x) (if (test x) (foo (d x)) t))

`foo`

in the encapsulation but to make it
local. This allows `foo`

to be used in other local events of that
encapsulation but does not export it and its subversive induction
scheme.
Finally, it may be that `foo`

is needed outside the encapsulation
environment but the user does not intend for `foo`

to suggest any
induction schemes. If this is the case, one should include `foo`

in the signature of the encapsulate (and so make its definition
local) and prove a non-local `:`

`definition`

rule which states the
recurrence equation for `foo`

without requiring a termination
argument. The `:clique`

and `:controller-alist`

fields for the
`:`

`definition`

rule should be those for the recursive definition of
`foo`

. See definition.

Note that the functions introduced in the signature may not even
occur ancestrally in the induction scheme suggested by a
non-`local`

ly defined recursive function in the `encapsulate`

.
That is, they may not occur in definitions of, or constraints on,
functions that occur in such induction schemes; and **those**
functions may not occur in such induction schemes; and so on.

Major Section: MISCELLANEOUS

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 term.

`:`

`rewrite`

rule
Major Section: MISCELLANEOUS

Example: Consider the :REWRITE rule created fromThe(IMPLIES (SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))) (EQUAL (LXD X) (LXD (NORM X)))).

`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. `Force`

d 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 `norm`

ed.''

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.
Major Section: MISCELLANEOUS

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 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 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 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 trans and also
see 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.

Major Section: MISCELLANEOUS

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 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 trans.

`Term1`

comes before `term2`

in the term order iff

The function(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.

`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
`cdr`

s being compared only if the `car`

s 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.

Major Section: MISCELLANEOUS

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)`

.

Major Section: MISCELLANEOUS

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 trans
and see 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 valueThus, the type-set*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

`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`

.
Major Section: MISCELLANEOUS

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:

### 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

Major Section: MISCELLANEOUS

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-hintprovided 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 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))