To bind free variables of a rewrite, definition, or linear rule

Examples: (IMPLIES (AND (RATIONALP LHS) (RATIONALP RHS) (BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X))) (EQUAL (EQUAL LHS RHS) (EQUAL (+ (- X) LHS) (+ (- X) RHS)))) (IMPLIES (AND (BIND-FREE (FIND-RATIONAL-MATCH-IN-TIMES-NESTS LHS RHS MFC STATE) (X)) (RATIONALP X) (CASE-SPLIT (NOT (EQUAL X 0)))) (EQUAL (< LHS RHS) (IF (< 0 X) (< (* (/ X) LHS) (* (/ X) RHS)) (< (* (/ X) RHS) (* (/ X) LHS)))))

General Forms:

(BIND-FREE term var-list) (BIND-FREE term t) (BIND-FREE term)

A rule which uses a `syntaxp` hypothesis and to a `meta` rule.
`syntaxp`, in that it logically always returns
`rewrite`, `rewrite-quoted-constant`, `definition`, or `linear`
rule when it is called at the top-level of a hypothesis. It is like a
`meta` rule, in that it allows the user to perform transformations
of terms under programmatic control.

Note that a `syntaxp` and the internal form that ACL2 uses
for terms. This internal form is similar to what the user sees, but there are
subtle and important differences. `Trans` can be used to view this
internal form.

Just as for a `syntaxp` hypothesis, there are two basic types of
`rewrite`, `definition`, or `linear` rule whose `corollary` is
*extended* `state` and `mfc`.
Whether simple or extended, a

We begin our description of

We wish to write a rule which will cancel ``like'' addends from both sides of an equality. Clearly, one could write a series of rules such as

(DEFTHM THE-HARD-WAY-2-1 (EQUAL (EQUAL (+ A X B) (+ X C)) (EQUAL (+ A B) (FIX C))))

with one rule for each combination of positions the matching addends might be found in (if one knew before-hand the maximum number of addends that would appear in a sum). But there is a better way. (In what follows, we assume the presence of an appropriate set of rules for simplifying sums.)

Consider the following definitions and theorem:

(DEFUN INTERSECTION-EQUAL (X Y) (COND ((ENDP X) NIL) ((MEMBER-EQUAL (CAR X) Y) (CONS (CAR X) (INTERSECTION-EQUAL (CDR X) Y))) (T (INTERSECTION-EQUAL (CDR X) Y)))) (DEFUN PLUS-LEAVES (TERM) (IF (EQ (FN-SYMB TERM) 'BINARY-+) (CONS (FARGN TERM 1) (PLUS-LEAVES (FARGN TERM 2))) (LIST TERM))) (DEFUN FIND-MATCH-IN-PLUS-NESTS (LHS RHS) (IF (AND (EQ (FN-SYMB LHS) 'BINARY-+) (EQ (FN-SYMB RHS) 'BINARY-+)) (LET ((COMMON-ADDENDS (INTERSECTION-EQUAL (PLUS-LEAVES LHS) (PLUS-LEAVES RHS)))) (IF COMMON-ADDENDS (LIST (CONS 'X (CAR COMMON-ADDENDS))) NIL)) NIL)) (DEFTHM CANCEL-MATCHING-ADDENDS-EQUAL (IMPLIES (AND (RATIONALP LHS) (RATIONALP RHS) (BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X))) (EQUAL (EQUAL LHS RHS) (EQUAL (+ (- X) LHS) (+ (- X) RHS)))))

How is this rule applied to the following term?

(equal (+ 3 (expt a n) (foo a c)) (+ (bar b) (expt a n)))

As mentioned above, the internal form of an ACL2 term is not always what
one sees printed out by ACL2. In this case, by using `trans` one
can see that the term is stored internally as

(equal (binary-+ '3 (binary-+ (expt a n) (foo a c))) (binary-+ (bar b) (expt a n))).

When ACL2 attempts to apply

((LHS . (binary-+ '3 (binary-+ (expt a n) (foo a c)))) (RHS . (binary-+ (bar b) (expt a n)))).

ACL2 then attempts to relieve the hypotheses in the order they were given. 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, we rewrite:

(RATIONALP (binary-+ '3 (binary-+ (expt a n) (foo a c)))).

Let us assume that the first two hypotheses rewrite to `syntaxp`
hypothesis, ACL2 evaluates

(FIND-MATCH-IN-PLUS-NESTS '(binary-+ '3 (binary-+ (expt a n) (foo a c))) '(binary-+ (bar b) (expt a n))).

Observe that, just as in the case of a `syntaxp` hypothesis, we
substitute the quotation of the variables bindings into the term to be
evaluated. See syntaxp for the reasons for this. The result of this
evaluation,

((X . (EXPT A N)) (LHS . (binary-+ '3 (binary-+ (expt a n) (foo a c)))) (RHS . (binary-+ (bar b) (expt a n)))),

and this extended substitution determines

(EQUAL (+ (- X) LHS) (+ (- X) RHS)) ==> (EQUAL (+ (- (EXPT A N)) 3 (EXPT A N) (FOO A C)) (+ (- (EXPT A N)) (BAR B) (EXPT A N))).

Question: What is the internal form of this result?

Hint: Use `trans`.

When this rule fires, it adds the negation of a common term to both sides
of the equality by selecting a binding for the otherwise-free variable

Just as for a `syntaxp` test, a `syntaxp` test signals success
by returning true, a

There is also a second, optional,

An extended `state`. See bind-free-examples for
examples of the use of these extended

**SECTION**: Returning a list of alists.

As promised above, we conclude with a discussion of the case that
evaluation of the

We illustrate with a simple pedagogical example. First introduce functions

(defstub p1 (x) t) (defstub p2 (x y) t) (defaxiom p2-implies-p1 (implies (p2 x y) (p1 x)))

If we add the following axiom, then

(defaxiom p2-instance (p2 v (cons v 4)))

Unfortunately, evaluation of

Let's define a function that produces a list of alists, each binding the
variable

(defun my-alists (x) (list (list (cons 'y (fcons-term* 'cons x ''3))) (list (cons 'y (fcons-term* 'cons x ''4))) (list (cons 'y (fcons-term* 'cons x ''5)))))

The following rewrite rule uses

(defthm p2-implies-p1-better (implies (and (bind-free (my-alists x) (y)) ; the second argument, (y), is optional (p2 x y)) (p1 x)))

Now the proof succeeds for

ACL2 !>(thm (p1 a)) 1> (ACL2_*1*_ACL2::MY-ALISTS A) <1 (ACL2_*1*_ACL2::MY-ALISTS (((Y CONS A '3)) ((Y CONS A '4)) ((Y CONS A '5)))) Q.E.D.

The first alist, binding

- Bind-free-examples
- Examples pertaining to
`bind-free`hypotheses