Define-pc-macro
Define a proof-builder macro command
A call of define-pc-macro defines a sort of macro, which is a
tactic that generates proof-builder instructions. This topic contains
basic information about how to use this utility. For somewhat sophisticated,
but commented, examples, see the community-book
books/kestrel/utilities/proof-builder-macros.lisp and associated tests in
the same directory, proof-builder-macros-tests.lisp.
We begin with the following example.
(define-pc-macro ib (&optional term)
(value
(if term
`(then (induct ,term) bash)
`(then induct bash))))
The example above captures a common paradigm: one attempts to prove the
current goal by inducting and then simplifying the resulting goals. (See
proof-builder-commands for documentation of the command then,
which is itself a pc-macro command, and commands induct and bash.)
Rather than issuing (then induct bash), or worse yet issuing induct
and then issuing bash for each resulting goal, the above definition of
ib would let you issue ib and get the same effect.
General Form:
(define-pc-macro cmd args dcl ... dcl body)
where cmd is the name of the pc-macro that you want to define,
args is its list of formal parameters. Args may include lambda-list
keywords &optional and &rest; see macro-args, but note that
here, args may not include &key or &whole.
The value of body should be an error-triple, of the form (mv
erp xxx state) for some erp and xxx. If erp is nil,
then xxx is handed off to the interactive proof-builder's instruction
interpreter. Otherwise, evaluation typically halts.
