Make a

See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description.

Meta rules extend the ACL2 simplifier with hand-written code to transform
certain terms to equivalent ones. To add a meta rule, the `corollary` formula must establish that the hand-written ``metafunction''
preserves the meaning of the transformed term.

Examples: (defthm fn-correct-1 ; Modify the rewriter to use fn to (equal (evl x a) ; transform terms that are calls of (evl (fn x) a)) ; nth or of foo. :rule-classes ((:meta :trigger-fns (nth foo)))) (defthm fn-correct-2 ; As above, but this illustrates (implies (and (pseudo-termp x) ; that without loss of generality we (alistp a)) ; may restrict x to be shaped like a (equal (evl x a) ; term and a to be an alist. (evl (fn x) a))) :rule-classes ((:meta :trigger-fns (nth foo)))) (defthm fn-correct-3 ; As above (with or without the (implies (and (pseudo-termp x) ; hypotheses on x and a), with the (alistp a) ; additional restriction that the (evl (hyp-fn x) a)) ; meaning of (hyp-fn x) is true in (equal (evl x a) ; the current context. That is, the (evl (fn x) a))) ; applicability of the transformation :rule-classes ; may be dependent upon some computed ((:meta :trigger-fns (nth foo)))) ; hypotheses.

While our intention is that the set of ACL2 documentation topics is self-contained, readers might find it useful to see the following paper for an introduction to meta reasoning in ACL2.

W. A. Hunt, Jr., R. B. Krug, M. Kaufmann, J S. Moore and E. W. Smith, ``Meta Reasoning in ACL2.'' TPHOLs 2005, ed. J. Hurd and T. F. Melham, LNCS 3603, Springer-Verlag, Berlin, 2005, pp. 163–178.

A non-

General Forms: (implies (and (pseudo-termp x) ; this hyp is optional (alistp a) ; this hyp is optional (ev (hyp-fn x ...) a) ; this hyp is optional ; meta-extract hyps may also be included (see below) ) (equiv (ev x a) (ev (fn x ...) a)))

where `pseudo-termp`. We say the
theorem above is a ``metatheorem'' or ``metalemma'' and

If ```state` and context sensitive information to compute their results, within
certain limits. We discuss vanilla metafunctions here and recommend a
thorough understanding of them before proceeding (at which time see extended-metafunctions).

If a metafunction application to a term,

Additional hypotheses are supported, called ``meta-extract hypotheses''. These allow metafunctions to depend on the validity of certain terms extracted from the context or the logical world. These hypotheses provide a relatively advanced form of metatheorem so we explain them elsewhere; see meta-extract.

One might think that metafunctions and (if supplied) hypothesis
metafunctions must be executable: that is, not constrained (i.e., introduced
in the signature of `encapsulate` events), and not declared `non-executable`. After all, there is no point in
installing a simplifier that cannot be run! However, such a restriction is
not enforced, because one could introduce a metafunction using `encapsulate` and then use `defattach` to attach it to an executable
function; see defattach.

We defer discussion of the case in which there is a hypothesis metafunction and for now address the case in which the other two hypotheses are present.

In the discussion below, we refer to the argument, `pseudo-termp` hypothesis is omitted, `pseudo-termp` hypothesis,

Suppose the general form of the metatheorem above is proved with the `pseudo-termp` and `alistp` hypotheses. Then when the simplifier
encounters a term,

Note that the result of applying a metafunction (or a hypothesis
metafunction) must be a term, i.e., must satisfy the predicate `termp`
in the current logical world. If not, then an error occurs. See term-table for how one obtains some assistance towards testing that `set-skip-meta-termp-checks`. Both of these runtime checks can be avoided by
proving that the metafunction (and the corresponding hypothesis metafunction,
if any) always produces an acceptable term. See well-formedness-guarantee. Alternatively, with an active trust tag (see
defttag) you can tell ACL2 to skip these tests; see `set-skip-meta-termp-checks`.

The ``evaluator'' function, `equal` and `binary-append` occur as function symbols, then `equal` and `binary-append`. The actual requirements on
`defevaluator`, though
this is not strictly necessary. See defevaluator if you want
details.

[Aside for the logic-minded.] Why are we justified in using metafunctions
this way? Suppose `defaxiom` events are adding
constraints to

term1 = (ev* 'term1 a) ; (1) by construction of ev* and a = (ev* (fn 'term1) a) ; (2) by the metatheorem for ev* = (ev* 'term2 a) ; (3) by evaluation of fn = term2 ; (4) by construction of ev* and a

Note that in line (2) above, where we appeal to the (functional
instantiation of the) metatheorem, we can relieve its (optional) `pseudo-termp` and `alistp` hypotheses by appealing to the facts that

There are subtleties related to the notion of ``growing''

Finally, we turn to the second case, in which there is a hypothesis
metafunction. In that case, consider as before what happens when the
simplifier encounters a term, `force`, `case-split`, `syntaxp`, and `bind-free`. If this attempt to
establish this term fails, then the meta rule is not applied. Otherwise,

Why is it justified to make this extension to the case of hypothesis metafunctions? First, note that the rule

(implies (and (pseudo-termp x) (alistp a) (ev (hyp-fn x) a)) (equal (ev x a) (ev (fn x) a)))

is logically equivalent to the rule

(implies (and (pseudo-termp x) (alistp a)) (equal (ev x a) (ev (new-fn x) a)))

where `if` and the
functions manipulated by

We now discuss the role of the `pseudo-termp` hypothesis.
`pseudo-termp` are that variable symbols never begin with ampersand,

There are two possible roles for `pseudo-termp` in the development of
a metatheorem: it may be used as the guard of the metafunction and/or
hypothesis metafunction and it may be used as a hypothesis of the metatheorem.
Generally speaking, the `pseudo-termp` hypothesis is included in a
metatheorem only if it makes it easier to prove. The choice is yours. (An
extreme example of this is when the metatheorem is invalid without the
hypothesis!) We therefore address ourselves the question: should a
metafunction have a `pseudo-termp` guard? A `pseudo-termp`
guard for a metafunction, in connection with other considerations
described below, improves the efficiency with which the metafunction is used
by the simplifier.

To make a metafunction maximally efficient you should (a) provide it with a
`pseudo-termp` guard and exploit the guard when possible
in coding the body of the function (see guards-and-evaluation,
especially the section on efficiency issues), (b) verify the guards of
the metafunction (see verify-guards), and (c) compile the metafunction
(see comp). When these three steps have been taken the simplifier can
evaluate

Before discussing efficiency issues further, let us review for a moment the
general case in which we wish to evaluate `logic` function. We must first ask whether the guards of

Now in the case of a metafunction for which the three steps above have been
followed, we know the guard is (implied by) `pseudo-termp` and
that it has been verified. Furthermore, we know without checking that the
guard is met (because `pseudo-termp`). Hence, we can use the compiled primary code
directly.

We strongly recommend that you compile your metafunctions, as well as all their subroutines (unless explicit compilation is suppressed; see compilation). Guard verification is also recommended.

Finally, we present a very simple example of the use of `hide`, which in turn is inside a call of a user-defined ``unhiding'' function,

(defun unhide (x) (declare (xargs :guard t)) x) (defthm unhide-hide (equal (unhide (hide x)) x) :hints (("Goal" :expand ((hide x))))) (in-theory (disable unhide)) (defun my-plus (x y) (+ x y)) (in-theory (disable my-plus)) (defevaluator evl evl-list ((my-plus x y) (binary-+ x y) (unhide x) (hide x))) (defun meta-fn (term) (declare (xargs :guard (pseudo-termp term))) (if (and (consp term) (equal (length term) 3) (equal (car term) 'my-plus)) `(UNHIDE (HIDE (BINARY-+ ,(cadr term) ,(caddr term)))) term)) (defthm my-meta-lemma (equal (evl term a) (evl (meta-fn term) a)) :hints (("Goal" :in-theory (enable my-plus))) :rule-classes ((:meta :trigger-fns (my-plus))))

Notice that in the following (silly) conjecture, ACL2 initially does only
does the simplification directed by the metafunction; a second goal is
generated before the commutativity of addition can be applied. If the above
calls of

ACL2 !>(thm (equal (my-plus b a) ccc)) This simplifies, using the :meta rule MY-META-LEMMA and the :rewrite rule UNHIDE-HIDE, to Goal' (EQUAL (+ B A) CCC). This simplifies, using the :rewrite rule COMMUTATIVITY-OF-+, to Goal'' (EQUAL (+ A B) CCC).

The discussion above probably suffices to make good use of this `thm` form above.

(trace$ (rewrite :entry (list (take 2 arglist)) :exit (list (car values))) (rewrite-with-lemma :entry (list (take 2 arglist)) :exit (take 2 values)))

The following annotated subset of the trace output (which may appear a bit different depending on the underlying Common Lisp implementation) explains how the trick works.

2> (REWRITE ((MY-PLUS B A) NIL))> 3> (REWRITE-WITH-LEMMA ((MY-PLUS B A) (REWRITE-RULE (:META MY-META-LEMMA) 1822 NIL EQUAL META-FN NIL META NIL NIL)))> We apply the meta rule, then recursively rewrite the result, which is the (UNHIDE (HIDE ...)) term shown just below. 4> (REWRITE ((UNHIDE (HIDE (BINARY-+ B A))) ((A . A) (B . B))))> 5> (REWRITE ((HIDE (BINARY-+ B A)) ((A . A) (B . B))))> The HIDE protects its argument from being touched by the rewriter. <5 (REWRITE (HIDE (BINARY-+ B A)))> 5> (REWRITE-WITH-LEMMA ((UNHIDE (HIDE (BINARY-+ B A))) (REWRITE-RULE (:REWRITE UNHIDE-HIDE) 1806 NIL EQUAL (UNHIDE (HIDE X)) X ABBREVIATION NIL NIL)))> Now we apply UNHIDE-HIDE, then recursively rewrite its right-hand side in an environment where X is bound to (BINARY-+ B A). 6> (REWRITE (X ((X BINARY-+ B A))))> Notice that at this point X is cached, so REWRITE just returns (BINARY-+ B A). <6 (REWRITE (BINARY-+ B A))> <5 (REWRITE-WITH-LEMMA T (BINARY-+ B A))> <4 (REWRITE (BINARY-+ B A))> <3 (REWRITE-WITH-LEMMA T (BINARY-+ B A))> <2 (REWRITE (BINARY-+ B A))>

- Force
- Identity function used to force a hypothesis
- Syntaxp
- Attach a heuristic filter on a rule
- Extended-metafunctions
- State and context sensitive metafunctions
- Meta-extract
- Meta reasoning using valid terms extracted from context or world
- Backchain-limit
- Limiting the effort expended on relieving hypotheses
- Magic-ev-fncall
- Call the named function on the given arguments and return the value.
- Evaluator-restrictions
- Some restrictions on the use of evaluators in meta-level rules
- Meta-implicit-hypothesis
- A potentially more efficient way of coding a hypothesis metafunction
- Transparent-functions
- Working around restrictions on the use of evaluators in meta-level rules
- Set-skip-meta-termp-checks
- Skip output checks for meta functions and clause-processors
- Case-split
- Like force but immediately splits the top-level goal on the hypothesis
- Term-table
- A table used to validate meta rules
- Magic-ev
- Evaluate a term under a ground substitution using magic-ev-fncall.
- Meta-lemmas
- A book of general purpose meta lemmas.
- Set-skip-meta-termp-checks!
- Skip output checks non-locally for meta functions and clause-processors