Attach a heuristic filter on a rule

A call of `rewrite`, `definition`, or `linear` rule is treated
specially, as described below. Similar treatment is given to the evaluation
of a `meta` rule's hypothesis function call.

For example, consider the `rewrite` rule created from the
following formula.

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

The

General Form: (SYNTAXP test)

Note that the test of a

Note also that a `trans` to
display this internal representation.

There are two types of `rewrite`, `definition`, or
`linear` rule provided `meta` rules is similar to the above,
except that it applies to the result of applying the hypothesis metafunction.
(Later below we will describe the second type, an *extended* `state`.)

We illustrate the use of simple `rewrite`
rule:

(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 X) ==> (LXD (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. Thus, in order to relieve the first hypothesis above, we rewrite

(RATIONALP (trn a b)).

If this rewrites to true, we continue.

Of course, many users are aware of some exceptions to this general
description of the way we relieve hypotheses. 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. See free-variables. `Force`d
hypotheses are another exception to the general rule of how hypotheses are
relieved.

Hypotheses marked with

(NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).

This clearly evaluates to

The acute reader will have noticed something odd about the form

(NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).

When relieving the first hypothesis, `consp` and
if so, is its `car` the symbol `cons`, and then evaluating forms such
as

(AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM)) (AND (CONSP (trn a b)) (EQ (CAR (trn a b)) NORM)) (AND (CONSP (trn 'a 'b)) (EQ (CAR (trn 'a 'b)) NORM)) (AND (CONSP '(trn a b)) (EQ '(CAR (trn a b)) ''NORM))

at the top-level ACL2 prompt.

See syntaxp-examples for more examples of the use of

An extended `state`. See syntaxp-examples for an example of the use of these
extended

We conclude with an example illustrating an error that may occur if you
forget that a

(defstobj st (fld1 :type (signed-byte 3) :initially 0) fld2)

The following

ACL2 !>(defthm bad (implies (syntaxp (quotep (fld1 st))) (equal (stp st) (and (true-listp st) (equal (len st) 2) (fld1p (car st)))))) ACL2 Error in ( DEFTHM BAD ...): The form (QUOTEP (FLD1 ST)), from a SYNTAXP hypothesis, is not suitable for evaluation in an environment where its variables are bound to terms. See :DOC SYNTAXP. Here is further explanation: The form ST is being used, as an argument to a call of FLD1, where the single-threaded object of that name is required. But in the current context, the only declared stobj name is STATE. Note: this error occurred in the context (FLD1 ST). Summary Form: ( DEFTHM BAD ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( DEFTHM BAD ...): See :DOC failure. ******** FAILED ******** ACL2 !>

Presumably the intention was to rewrite the term

(defthm good (implies (and (equal f (fld1 st)) (syntaxp (quotep f))) (equal (stp st) (and (true-listp st) (equal (len st) 2) (fld1p (car st))))))

The event above is admitted by ACL2. We can see it in action by disabling
the definition of

(in-theory (disable stp))

Then the proof fails for the following, because the

(thm (stp st))

However, the proof succeeds for the next form, as we explain below.

(thm (stp (list 3 rest)))

Consider what happens in that case when rule

- Syntaxp-examples
- Examples pertaining to syntaxp hypotheses