Make a rule that specifies the type of a term

See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description. Also see type-reasoning for basic background on type reasoning in ACL2.

In this topic we focus on user-defined type-prescription rules, but note
that ACL2 also introduces type-prescription rules when introducing a function
with `defun`; see type-prescription-debugging for discussion of
how to influence the generation of such rules.

Examples: (defthm integerp-foo ; Assumes that foo has been (integerp (foo x y)) ; defined; then, states that :rule-classes :type-prescription) ; (foo x y) is of type integer. (defthm characterp-nth-type-prescription ; (Nth n lst) is of type character (implies ; provided the hypotheses can be (and (character-listp lst) ; established by type reasoning. (<= 0 n) (< n (len lst))) (characterp (nth n lst))) :rule-classes :type-prescription) (defthm characterp-nth-type-prescription-alt ; equivalent to the above (implies (and (character-listp lst) (<= 0 n) (< n (len lst))) (characterp (nth n lst))) :rule-classes ((:type-prescription :typed-term (nth n lst)))) (defthm demodulize-type-for-quote-value ; (Demodulize a lst 'value ans) is (implies ; either a nonnegative integer or (and (atom a) ; of the same type as ans, provided (true-listp lst) ; the hyps can be established by type (member-equal a lst)) ; reasoning ; (or (and (integerp (demodulize a lst 'value ans)) (>= (demodulize a lst 'value ans) 0)) (equal (demodulize a lst 'value ans) ans))) :rule-classes :type-prescription)

To specify the term whose type (see type-set) is described by the
rule, provide that term as the value of the

General Form (after preprocessing; see below): (implies hyps (or type-restriction1-on-pat ... type-restrictionk-on-pat (equal pat var1) ... (equal pat varj)))

where

If the

Roughly speaking, the effect of adding such a rule is to inform the ACL2
typing mechanism that

More operationally, when asked to determine the type of a term that is an
instance of **This is done by type reasoning alone, not rewriting!** However, if some
hypothesis is a call of `force`, then forcing may occur, which may
ultimately invoke the rewriter; see force and see case-split.
So-called free variables in hypotheses are treated specially; see free-variables. Provided the hypotheses are established by type reasoning,
ACL2 then unions the types described by the

You can limit the recursive establishment of hypotheses of rules; see set-backchain-limit.

Because only type reasoning is used to establish the hypotheses of

(defun my-statep (x) (and (true-listp x) (equal (len x) 2)))

and suppose

While this example makes it clear how non-recursive predicates can cause
problems, non-recursive functions in general can cause problems. For example,
if

Because of the freedom one has in forming the conclusion of a
type-prescription, we have to use heuristics to recover the pattern,

The defun event may generate a `defun`. (The trivial rule, saying `defun` still allocates the rune and the corollary of
this rune is known to be

We close with a discussion of how, before a term is parsed into a

(defthm append-tp-example (let ((result (append x y))) (implies (nat-listp x) (implies (let ((second-hyp (integer-listp y))) second-hyp) (true-listp result)))) :rule-classes :type-prescription)

This theorem is parsed into a type-prescription rule with the following hypotheses and conclusion.

(nat-listp x) ; first hypothesis ((lambda (second-hyp) second-hyp) (integer-listp y)) ; second hypothesis (true-listp (binary-append x y)) ; conclusion

Notice that the top-level `let` was expanded, i.e., `append` is a macro that
abbreviates `binary-append`. Also notice that the two hypotheses were
``flattened'' in the sense that they were gathered up into a list. Finally,
notice that the `let` in the second hypothesis was not expanded (it was
merely translated to internal form, using

Here is the detail promised above, for parsing a term into a
`let`, `let*`, and `mv-let`
expressions) and flattening the `implies` structure, until the
conclusion is exposed; then the conclusion's `pe`

- Force
- Identity function used to force a hypothesis
- Backchain-limit
- Limiting the effort expended on relieving hypotheses
- Case-split
- Like force but immediately splits the top-level goal on the hypothesis
- Type-prescription-debugging
- Improve a built-in type-prescription rule