### SYNTAXP-EXAMPLES

examples pertaining to syntaxp hypotheses
```Major Section:  SYNTAXP
```

See syntaxp for a basic discussion of the use of `syntaxp` to control rewriting.

A common syntactic restriction is

```(SYNTAXP (AND (CONSP X) (EQ (CAR X) 'QUOTE)))
```
or, equivalently,
```(SYNTAXP (QUOTEP X)).
```
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` prints as `(+ 11 12)` then the test evaluates to `nil` (because `(car x)` is the symbol `binary-+`). We see the use of this restriction in the rule
```(implies (and (syntaxp (quotep c))
(syntaxp (quotep d)))
(equal (+ c d x)
(+ (+ c d) x))).
```
If `c` and `d` are constants, then the `executable-counterpart` of `binary-+` will evaluate the sum of `c` and `d`. For instance, under the influence of this rule
```(+ 11 12 foo)
```
rewrites to
```(+ (+ 11 12) foo)
```
which in turn rewrites to `(+ 23 foo)`. Without the syntactic restriction, this rule would loop with the built-in rules `ASSOCIATIVITY-OF-+` or `COMMUTATIVITY-OF-+`.

We here recommend that the reader try the affects of entering expressions such as the following at the top level ACL2 prompt.

```(+ 11 23)
(+ '11 23)
(+ '11 '23)
(+ ''11 ''23)
:trans (+ 11 23)
:trans (+ '11 23)
:trans (+ ''11 23)
:trans (+ c d x)
:trans (+ (+ c d) x)
```
We also recommend that the reader verify our claim above about looping by trying the affect of each of the following rules individually.
```(defthm good
(implies (and (syntaxp (quotep c))
(syntaxp (quotep d)))
(equal (+ c d x)
(+ (+ c d) x))))

(implies (and (acl2-numberp c)
(acl2-numberp d))
(equal (+ c d x)
(+ (+ c d) x))))
```
on (the false) theorems:
```(thm
(equal (+ 11 12 x) y))

(thm
(implies (and (acl2-numberp c)
(acl2-numberp d)
(acl2-numberp x))
(equal (+ c d x) y))).
```
One can use `:``brr`, perhaps in conjunction with `cw-gstack`, to investigate any looping.

Here is a simple example showing the value of rule `good` above. Without `good`, the `thm` form below fails.

```(defstub foo (x) t)

(thm (equal (foo (+ 3 4 x)) (foo (+ 7 x))))
```

The next three examples further explore the use of `quote` in `syntaxp` hypotheses.

We continue the examples of `syntaxp` hypotheses with a rule from `books/finite-set-theory/set-theory.lisp`. We will not discuss here the meaning of this rule, but it is necessary to point out that `(ur-elementp nil)` is true in this book.

```(defthm scons-nil
(implies (and (syntaxp (not (equal a ''nil)))
(ur-elementp a))
(= (scons e a)
(scons e nil)))).
```
Here also, `syntaxp` is used to prevent looping. Without the restriction, `(scons e nil)` would be rewritten to itself since `(ur-elementp nil)` is true.
Question: Why the use of two quotes in `''nil`?
Hints: `Nil` is a constant just as 23 is. Try `:trans (cons a nil)`, `:trans (cons 'a 'nil)`, and `:trans (cons ''a ''nil)`. Also, don't forget that the arguments to a function are evaluated before the function is applied.

The next two rules move negative constants to the other side of an inequality.

```(defthm |(< (+ (- c) x) y)|
(implies (and (syntaxp (quotep c))
(syntaxp (< (cadr c) 0))
(acl2-numberp y))
(equal (< (+ c x) y)
(< (fix x) (+ (- c) y)))))

(defthm |(< y (+ (- c) x))|
(implies (and (syntaxp (quotep c))
(syntaxp (< (cadr c) 0))
(acl2-numberp y))
(equal (< y (+ c x))
(< (+ (- c) y) (fix x)))))
```
Questions: What would happen if `(< (cadr c) '0)` were used? What about `(< (cadr c) ''0)`?

One can also use `syntaxp` to restrict the application of a rule to a particular set of variable bindings as in the following taken from `books/ihs/quotient-remainder-lemmas.lisp`.

```(encapsulate ()

(local
(defthm floor-+-crock
(implies
(and (real/rationalp x)
(real/rationalp y)
(real/rationalp z)
(syntaxp (and (eq x 'x) (eq y 'y) (eq z 'z))))
(equal (floor (+ x y) z)
(floor (+ (+ (mod x z) (mod y z))
(* (+ (floor x z) (floor y z)) z)) z)))))

(defthm floor-+
(implies
(and (force (real/rationalp x))
(force (real/rationalp y))
(force (real/rationalp z))
(force (not (equal z 0))))
(equal (floor (+ x y) z)
(+ (floor (+ (mod x z) (mod y z)) z)
(+ (floor x z) (floor y z))))))

)
```
We recommend the use of `:``brr` to investigate the use of `floor-+-crock`.

Another useful restriction is defined by

```(defun rewriting-goal-literal (x mfc state)

;; Are we rewriting a top-level goal literal, rather than rewriting
;; to establish a hypothesis from a rewrite (or other) rule?

(declare (ignore x state))
(null (access metafunction-context mfc :ancestors))).
```
We use this restriction in the rule
```(defthm |(< (* x y) 0)|
(implies (and (syntaxp (rewriting-goal-literal x mfc state))
(rationalp x)
(rationalp y))
(equal (< (* x y) 0)
(cond ((equal x 0)
nil)
((equal y 0)
nil)
((< x 0)
(< 0 y))
((< 0 x)
(< y 0))))))
```
which has been found to be useful, but which also leads to excessive thrashing in the linear arithmetic package if used indiscriminately.

See extended-metafunctions for information on the use of `mfc` and `metafunction-context`.