Download Refinement and Theorem Proving*

Suppose that we are defining recursive functions whose termination can be
shown with measure (len x), where x is the first argument to the function.
Instead of adding the required declarations to all of the functions under consideration, we might want to write a macro that generates the required defun.
Here is one way of doing this.
(defmacro defunm (name args body)
‘(defun ,name
,args
(declare (xargs :measure (len ,(first args))))
,body))
Notice that we define macros using defmacro, in a manner similar to function
definitions. Notice the use of what is called the backquote notation. The value
of a backquoted list is a list that has the same structure as the backquoted list
except that expressions preceded by a comma are replaced by their values. For
example, if the value of name is app, then the value of ‘(defun ,name) is (defun
app).
We can now use defunm as follows.
(defunm app (x y)
(if (consp x)
(cons (car x) (app (cdr x) y))
y))
This expands to the following.
(defun app (x y)
(declare (xargs :measure (len x)))
(if (consp x)
(cons (car x) (app (cdr x) y))
y))
When the above is processed, the result is that the function app is defined. In
more detail, the above macro is evaluated as follows. The macro formals name,
args, and body are bound to app, (x y), and (if (consp x) (cons (car x)
(app (cdr x) y)) y), respectively. Then, the macro body is evaluated. As per
the discussion on the backquote notation, the above expansion is produced.
We consider a final example to introduce ampersand markers. The example
is the list macro and its definition follows.
(defmacro list (&rest args)
(list-macro args))
Recall that (list 1 2) is an abbreviation for (cons 1 (cons 2 nil)). In addition, list can be called on an arbitrary number of arguments; this is accomplished with the use of the &rest ampersand marker. When this marker is used,
it results in the next formal, args, getting bound to the list of the remaining arguments. Thus, the value of (list 1 2) is the value of the expression
(list-macro ’(1 2)). In this way, an arbitrary number of objects are turned