Major Section: PROOF-CHECKER
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-checker-commands for documentation of the command
then, which is itself a pc-macro command, and commands
bash.) Rather than issuing
(then induct bash), or worse yet issuing
inductand then issuing
bashfor each resulting goals, the above definition of
ibwould let you issue
iband get the same effect.
General Form: (define-pc-macro cmd args doc-string dcl ... dcl body)where
cmdis the name of the pc-macro than you want to define,
argsis its list of formal parameters.
Argsmay include lambda-list keywords
&rest; see macro-args, but note that here,
argsmay not include
The value of
body should be an ACL2 ``error triple,'' i.e., have the
(mv erp xxx state) for some
xxx is handed off to the proof-checker's instruction
interpreter. Otherwise, evaluation typically halts. We may write
more on the full story later if there is interest in reading it.