Defretgen
Generate some defret and defret-mutual forms for a set
of functions and mutual recursions.
This macro generates theorems based on the same kinds of rules as
defret-mutual-generate. However, instead of generating those theorems
for a single mutually-recursive clique, it generates them for a user-specified
list of functions and mutual recursions, which must be defined using define or defines respectively.
The syntax of defretgen works as follows:
(defretgen my-theorem-about-<fn>
;; rules to generate the theorems
:rules ((condition1 action1 ...)
(condition2 action2 ...)
...)
;; abbreviations that generate more rules
:formal-hyps ...
:return-concls ...
:function-keys ...
;; optional keywords
:hints top-level-hints-for-defret-mutual
:no-induction-hint nil ;; for defret-mutual
:otf-flg nil
;; specifies the set of functions for which to generate the theorems
:functions my-function-set)
See defretgen-rules for documentation on the :rules,
:formal-hyps, :return-concls, and :function-keys arguments. The
:hints, :no-induction-hint, and :otf-flg arguments are passed to
defret-mutual forms at the top level; hints for defret forms (both
standalone and within defret-mutual forms) may be specified by the :rules
and :function-keys arguments.
The argument to :functions must be a list of descriptors (described
below) or a single symbol, which is an abbreviation for the singleton list
containing that symbol. A descriptor may be a symbol or one of the following
kinds of pairs:
- (:fnset <name>) denotes a set of functions as defined by def-retgen-fnset.
- (:mutrec <name>) names a mutually-recursive clique of functions
defined using defines; note that <name> must be the name given to
the mutually-recursive clique as a whole (the first argument to defines,
which is not necessarily the name of one of the functions.
- (:function <name>) names a function defined using define.
If it is a symbol, it is treated as (:fnset <name>) if such a function
set exists, then (:mutrec <name>) if such a mutual recursion exists, then
(:function <name>) otherwise.
Subtopics
- Defretgen-rules
- Syntax and meaning of rules and abbreviations for defretgen
and defret-mutual-generate
- Defret-mutual-generate
- Generate a defret-mutual form using rules that produce hyps and
conclusion conjuncts based on define formal and return
specifiers.
- Def-retgen-fnset
- Give a name to a set of functions and mutual recursions that may be
used in defretgen.
