make a rule that acts like a function definition Major Section:
RULE-CLASSES  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 :definition rule might
be built is:  (implies (true-listp x)          (equal (len x)
(if (null x)                     (if (null (cdr x))
(+ 2 (len (cddr x)))))))  General Form: (implies hyp (equiv (fn
a1 ... an) body))  where equiv is an equivalence relation and fn
is a function symbol other than if, hide, force or case-split.
Such rules allow ``alternative'' definitions of fn to be proved
as theorems but used as definitions. These rules are not true
``definitions'' in the sense that they (a) cannot introduce new
function symbols and (b) do not have to be terminating recursion
schemes. They are just conditional rewrite rules that are
controlled the same way we control recursive definitions. We
call these ``definition rules'' or ``generalized