Guarantee that a metafunction or clause-processor returns a well-formed answer

A `meta` and `clause-processor` `rule-classes`. By default, when a metafunction or clause processor is
applied, ACL2 checks that the output is well-formed (and does not contain
certain ``forbidden'' functions; see `set-skip-meta-termp-checks`). By
providing a

This is considered an advanced feature that requires that you prove certain theorems; this is probably only worthwhile if your metafunctions or clause processors produce very large terms. Henceforth, we assume you are familiar with metafunctions and clause processors.

This topic first exhibits a simple example of a well-formedness guarantee
for a metafunction. This example is really an outline; a self-contained,
runnable example may be found in the community-books in file

Suppose that `arity` 1. The event storing

(defthm fn-is-correct (implies (and (pseudo-termp x) (alistp a)) (equal (evl x a) (evl (fn x) a))) :rule-classes ((:meta :trigger-fns (TARGET))))where

**Function: **

(defun logic-termp (x wrld) (declare (xargs :guard (plist-worldp-with-formals wrld))) (and (termp x wrld) (logic-fnsp x wrld)))

The

(defthm fn-is-well-formed (implies (and (logic-termp x w) (arities-okp '((TARGET . 1) (CONS . 2) (IF . 3)) w)) (logic-termp (fn x) w)) :rule-classes nil)and then you store

(defthm fn-is-correct (implies (and (pseudo-termp x) (alistp a)) (equal (evl x a) (evl (fn x) a))) :rule-classes ((:meta :trigger-fns (TARGET) :well-formedness-guarantee fn-is-well-formed)))

Now we describe the values you may provide with the

General Forms: :well-formedness-guarantee thm-name1 :well-formedness-guarantee (thm-name1) :well-formedness-guarantee (thm-name1 thm-name2)where both

Each well-formedness theorem provides an ``arity alist'' that specifies the
assumed arities of the function symbols known to the metafunction or clause
processor. The arities shown for the function symbols listed in that alist
must be the same as the arities of those functions in the actual ACL2 logical
world current at the time the `logic` mode.

Furthermore, none of the function symbols in the arity alists should be
``forbidden'' function symbols as explained in `set-skip-meta-termp-checks`.

When the `push-untouchable`.

The only way a function's arity or forbidden status can change, or that a
function can transition out of

Theorems must be proved to establish that metafunctions and clause
processors return well-formed results. These are called ``well-formedness
theorems.'' Note: To say a theorem is a ``well-formedness theorem'' is a
remark about the shape of the formula, not its rule-class. There is no
`rule-classes` that accept the syntax of the
formula or as

Well-formedness theorems for metafunctions and clause processors are
similar but slightly different. We deal with metafunctions and their
corresponding hypothesis metafunctions (if any) first. The shapes of the
well-formedness theorems for a metafunction and hypothesis metafunction are
identical, but remember that you must prove a well-formedness theorem for both
the metafunction and the associated hypothesis metafunction. So suppose
`termp` when given one, provided the arities of certain
function symbols are as expected:

General Form of Well-Formedness Theorem for a Metafunction: (implies (and (logic-termp x w) (arities-okp '<alist> w)) (logic-termp (fn x ...) w))where

An example of `termp` you
will see that it uses `arities-okp` hypothesis restricts `logic`-mode. For example, given the `arity` and `arities-okp` are
disabled; and the following rewrite rules, which are part of ACL2's initial
world, will take care of calls like

**Theorem: **

(defthm arities-okp-implies-arity (implies (and (arities-okp user-table w) (assoc fn user-table)) (equal (arity fn w) (cdr (assoc fn user-table)))))

**Theorem: **

(defthm arities-okp-implies-logicp (implies (and (arities-okp user-table w) (assoc fn user-table)) (logicp fn w)))

Now we turn to the well-formedness theorem for a clause processor,
`logic-term-listp` and
the recognizer for a list of clauses is `logic-term-list-listp`:

General Forms of Well-Formedness Theorem for a Clause Processor (implies (and (logic-term-listp x w) (arities-okp '<alist> w)) (logic-term-list-listp (cl-proc x ...) w)) (implies (and (logic-term-listp x w) (arities-okp '<alist> w)) (logic-term-list-listp (clauses-result (cl-proc x ...)) w))

The first form above is for a

The discussion about metafunctions, above, applies here as well.

In the absence of a

If

When a