Examples pertaining to syntaxp hypotheses

See syntaxp for a basic discussion of the use of

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 `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 `executable-counterpart`
of `binary-+` will evaluate the sum of

(+ 11 12 foo)

rewrites to

(+ (+ 11 12) foo)

which in turn rewrites to

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)))) (defthm bad (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

(defstub foo (x) t) (thm (equal (foo (+ 3 4 x)) (foo (+ 7 x))))

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

We continue the examples of `syntaxp` hypotheses with a rule from
community 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,

Question: Why the use of two quotes in

Hints:

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

One can also use

(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

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