Make a rule that acts like a function definition

See rule-classes for a general discussion of rule classes
and how they are used to build rules from formulas. An example `corollary` formula from which a

Examples: (defthm open-len-twice (implies (true-listp x) (equal (len x) (if (null x) 0 (if (null (cdr x)) 1 (+ 2 (len (cddr x))))))) :rule-classes :definition) ; Same as above, with :controller-alist made explicit: (defthm open-len-twice (implies (true-listp x) (equal (len x) (if (null x) 0 (if (null (cdr x)) 1 (+ 2 (len (cddr x))))))) :rule-classes ((:definition :controller-alist ((len t))))) General Form: (implies hyp (equiv (fn a1 ... an) body))

where `if`, `hide`, `force` or `case-split`. Such rules allow ``alternative'' definitions of

Consider the general form above. Generalized definitions are stored among
the `rewrite` rules for the function ``defined,'' `rewrite` rule and the result of rewriting

The notions of ``recursive call'' and ``controllers'' are complicated by the provisions for mutually recursive definitions. Consider a ``clique'' of mutually recursive definitions. Then a ``recursive call'' is a call to any function defined in the clique and an argument is a ``controller'' if it is involved in the measure that decreases in all recursive calls. These notions are precisely defined by the definitional principle and do not necessarily make sense in the context of generalized definitional equations as implemented here.

But because the heuristics governing the use of generalized definitions
require these notions, it is generally up to the user to specify which calls
in body are to be considered recursive and what the controlling arguments are.
This information is specified in the

The

If the

The

If the

For example, suppose

Inappropriate heuristic advice via

Note that the actual definition of

By default, a

See rule-classes for a discussion of the optional field

Note only that if you prove a definition rule for function `pe` `pf`

The definitional principle, `defun`, actually adds `defun`'d to be `defun` (or `defuns` or `mutual-recursion`) can compute the clique
for `defun` adds the

- Force
- Identity function used to force a hypothesis
- Syntaxp
- Attach a heuristic filter on a rule
- Bind-free
- To bind free variables of a rewrite, definition, or linear rule
- Case-split
- Like force but immediately splits the top-level goal on the hypothesis
- Simple
: `definition`and: `rewrite`rules used in preprocessing- Set-body
- Set the definition body
- Show-bodies
- Show the potential definition bodies