Major Section: MISCELLANEOUS

A calls of `syntaxp`

in the hypothesis of a `:`

`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

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

.
### SYNTAXP-EXAMPLES -- examples pertaining to syntaxp hypotheses

General Form: (SYNTAXP test)

`Syntaxp`

always returns `t`

and so may be added as a vacuous hypothesis.
However, when relieving the hypothesis, 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.Note that the test of a `syntaxp`

hypothesis does not, in general, deal
with the meaning or semantics or values of the terms, but rather 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 `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`

unless it has already been `norm`

ed.''

Note also that a `syntaxp`

hypothesis deals with the syntactic form used
internally by ACL2, rather than that seen by the user. In some cases these
are the same, but there can be subtle differences with which the writer of a
`syntaxp`

hypothesis must be aware. You can use `:`

`trans`

to
display this internal representation.

There are two types of `syntaxp`

hypotheses. The simpler type may be a
hypothesis of a `:`

`rewrite`

, `:`

`definition`

, or
`:`

`linear`

rule provided `test`

contains at least one variable but
no free variables (see free-variables). In particular, `test`

may not use
stobjs; any stobj name will be treated as an ordinary variable. The
case of `:`

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

hypothesis, which may
use `state`

.)

We illustrate the use of simple `syntaxp`

hypotheses by slightly
elaborating the example given above. Consider a `:`

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

.
(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 `syntaxp`

, as in `(syntaxp test)`

, are also
exceptions. We instantiate such a hypothesis; but instead of rewriting the
instantiated instance, we evaluate the instantiated `test`

. More
precisely, 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. So in the case in point, we (in
essence) evaluate

(NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).This clearly evaluates to

`t`

. When a `syntaxp`

test evaluates to true,
we consider the `syntaxp`

hypothesis to have been established; this is
sound because logically `(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.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,

`(RATIONALP X)`

, we substituted
`(trn a b)`

for `X`

; but when relieving the second hypothesis,
`(SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM))))`

, we substituted the
quotation of `(trn a b)`

for `X`

. Why the difference? Remember that in
the first hypothesis we are talking about the value of `(trn a b)`

-- is
it rational -- while in the second one we are talking about its syntactic
form. Remember also that Lisp, and hence ACL2, evaluates the arguments to a
function before applying the function to the resulting values. Thus, we are
asking ``Is the list `(trn a b)`

a `consp`

and if so, is its `car`

the symbol `NORM`

?'' The `quote`

s on both `(trn a b)`

and `NORM`

are
therefore necessary. One can verify this by defining `trn`

to be, say
`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 `syntaxp`

.

An extended `syntaxp`

hypothesis is similar to the simple type described
above, but it uses two additional variables, `mfc`

and `state`

, which
must not be bound by the left hand side or an earlier hypothesis of the rule.
They must be the last two variables mentioned by `form`

; first `mfc`

,
then `state`

. These two variables give access to the functions
`mfc-`

xxx; see extended-metafunctions. As described there, `mfc`

is
bound to the so-called metafunction-context and `state`

to ACL2's
`state`

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

hypotheses.

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

hypothesis will be evaluated in an environment
where variables are bound to syntactic terms, not to values. Consider the
following stobj introduction (see defstobj).

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

`syntaxp`

hypothesis is ill-formed for evaluation. Indeed,
ACL2 causes an error because it anticipates that when trying to relieve the
`syntaxp`

hypothesis of this rule, ACL2 would be evaluating `(fld1 st)`

where `st`

is bound to a term, not to an actual `stobj`

as required by
the function `fld1`

. The error message is intended to explain this
problem.
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

`(stp st)`

when the
`fld1`

component of `st`

is seen to be an explicit constant. As
explained elsewhere (see free-variables), we can obtain the result of
rewriting `(fld1 st)`

by binding a fresh variable to that term using
`EQUAL`

, as follows.
(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

`stp`

so that only the rule above, `good`

, is available
for reasoning about `stp`

.
(in-theory (disable stp))Then the proof fails for the following, because the

`syntaxp`

hypothesis of
the rule, `good`

, fails: `(quotep f)`

evaluates to `nil`

when `f`

is
bound to the term `(fld1 st)`

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

`good`

is applied to the term
`(stp (list 3 rest))`

. (See free-variables for relevant background.) The
first hypothesis of `good`

binds the variable `f`

to the result of
rewriting `(fld1 st)`

, where `st`

is bound to the (internal form of) the
term `(list 3 rest)`

-- and that result is clearly the term, `'3`

.
Then the `syntaxp`

hypothesis is successfully relieved, because the
evaluation of `(quotep f)`

returns `t`

in the environment that binds
`f`

to `'3`

.