Info file: acl2-doc-lemacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-lemacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.9 Copyright (C) 1997 Computational Logic, Inc. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. Written by: Matt Kaufmann and J Strother Moore Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, TX 78703-4776 U.S.A.  File: acl2-doc-lemacs.info, Node: LINEAR-ALIAS, Next: META, Prev: LINEAR, Up: RULE-CLASSES LINEAR-ALIAS make a rule to extend the applicability of linear arithmetic *Note 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 :linear-alias rule might be built is as follows. (Of course, the functions fix, plus, diff, and lessp would have to be defined first.) Example: (and (equal (fix (plus x y)) (plus x y)) (equal (fix (diff x y)) (diff x y)) (equal (fix (fix x)) (fix x)) (equal (lessp x y) (< (fix x) (fix y))) (equal (plus x y) (+ (fix x) (fix y))) (implies (not (lessp x y)) (equal (diff x y) (- (fix x) (fix y))))) :linear-alias rules are essentially a hack to allow the creation of the "NQTHM" package. We will be surprised if the casual user of ACL2 ever finds a use for them. They are not documented very thoroughly. General Forms: (equal lhs rhs) (implies hyps (equal lhs rhs)) where every variable that occurs in the rule must occur in the lhs. As for :rewrite rules, we strip the conjuncts out of the :corollary formula and generate one :linear-alias rule for each. Thus, it is possible to package together a complete set of :linear-alias rules under a single name. When linear arithmetic is applied to a term that is not "linearizable," i.e., a term that does not start with <, +, or -, it attempts to transduce the term to a linearizable one by applying all known :linear-alias rules as rewrite rules. This transduction is performed by the simple rewrite function rewrite-with-linear-aliases. Like the standard ACL2 rewriter, the linear alias rewriter applies linear alias rules exhaustively in the sense that if a rule applies then the rhs of the rule is recursively rewritten. Unlike :rewrite rules, :linear-alias rules are applied from outside in (!) and hypotheses are not relieved but merely collected. For example, rewriting (lessp (diff (plus a b) c) (diff u v)) with the rules generated from the conjunction above produces (< (+ (+ (fix a) (fix b)) (- (fix c))) (+ (fix u) (- (fix v)))) under the hypothesis that (not (lessp (plus a b) c)) and (not (lessp u v)). (Actually, the + and - operators shown above are really calls of binary-+ and unary--.) Think of :linear-alias rules as transforming a term from one theory to another, generating hypotheses in the first theory. Call the initial theory "nqthm" and the final one "acl2." One should strive to create a set of rules that transform from the nqthm to the acl2 theory while only generating hypotheses in the first theory. The restriction is motivated by the desire not to surprise the nqthm user by suddently introducing conditions that are not phrased in the nqthm theory. The purpose of the nqthm package is to emulate nqthm, so it simply represents a failure if acl2 suddenly produces a case split, say, in which some non-nqthm term appears, such as (rationalp (plus a b)). To this end, we offer some advice below. However, it is especially helpful to study how the outside-in rewrite strategy uses the rules above to achieve this goal. For example, (lessp (plus a b) (diff u v)) first steps to (< (fix (plus a b)) (fix (diff u v))), unconditionally. But plus and diff don't need fixing: (< (plus a b) (diff u v)). Rewriting further finishes with (< (+ (fix a) (fix b)) (+ (fix u) (- (fix v)))). Observe that had we rewritten inside-out the sequence would have been: (lessp (+ (fix a) (fix b)) (+ (fix u) (- (fix v)))) and then (< (fix (+ (fix a) (fix b))) (fix (+ (fix u) (- (fix v))))). Note that we now need to know that + doesn't need fixing if its arguments have been. But that is a more complicated rule than the simple one that plus doesn't need fixing. Perhaps a different set of rules would work well for inside-out rewriting, but I just used the ones that first leapt to mind. It is interesting to note that linearization proceeds outside in too. Here then is the advice. Rules should either transform nqthm terms to nqthm terms, e.g., (fix (plus x y)) to (plus x y), or should transform nqthm terms to acl2 terms, e.g., (lessp x y) to (< (fix x) (fix y)). When the rhs introduces an acl2 function symbol, the symbol should be outside of all nqthm terms in the rhs. Hypotheses should be expressed in the nqthm theory. No rule should rewrite an acl2 function symbol. If the transformation involves "fixers" then each operator should have two rules about it. The first, like (plus x y) = (+ (fix x) (fix y)), explains the nqthm function in terms of an acl2 function with fixed arguments. The second, like (fix (plus x y)) = (plus x y) eliminates the interior fixes generated by the first rule. These conventions mean that the rewriter, by going from outside in, always sees nqthm terms and instantiates the hypotheses of rules with nqthm terms. To violate these conventions might produce a set of rules that would cause a non-nqthm hypothesis to be generated. Finally, observe that the rules probably will introduce a "fixer", which is the function fix in the NQTHM package. The fixer tends to settle around the nonlinear leaves of the resultant linearizable term. It is important to have a :type-prescription rule establishing that the fixer produces a rational. When a :linear arithmetic rule is proved its conclusion is linearized to obtain the relevant polynomials. :linear-alias rules may kick in there; thus, a conclusion of the form (not (lessp (length str) (strpos pat str))) may be a legal :linear rule. Note however that its linearization is (not (< (fix (length str)) (fix (strpos pat str)))). The maximal term of this rule is (fix (strpos pat str)). However, we do not want to store such a linear rule under fix because that would result in all of the Nqthm proveall's linear rules being stored under the same symbol. We therefore note when the maximal term does not actually occur in the conclusion, is of the form (fix term), for some unary function fix, and term does occur in the conclusion. In that case, we call fix a "fixer" and we store a t under the property 'linear-alias-fixerp. We then store the rule with the maximal term term instead of (fix term). Later, when we are adding lemmas to the linear pot, we note that if we seek linear lemmas about (fix term), where fix is a fixer, we look for lemmas both stored under the function symbol of term and stored under the function symbol fix. In all cases, the maximal term of the rule contains as its top-most function symbol the symbol under which the rule is stored. Thus, if we seek lemmas about (fix (strpos pat str)) we will go to the property list of strpos and there find rules about (strpos pat str). We will instantiate their conclusions and linearize them, producing polynomials about (fix (strpos pat str)). This raises a subtle point. It could be that there is more than one fixer used in connection with strpos. Thus, some lemmas could linearize to polynomials about (rat (strpos pat str)). Therefore, when we create the linear rule with (strpos pat str) as its (fixed) maximal term, we store in the :fixer field of the rule the symbol fix to indicate that the linearization of this conclusion will (probably) produce (fix (strpos pat str)) terms. When looking for lemmas about (fix (strpos pat str)) we actually look for lemmas about strpos that have :fixer fix. Here is an extended example of the use of linear aliasing. First, we define some nqthm-level functions: (defun fix (x) (if (and (integerp x) (>= x 0)) x 0)) (defun lessp (x y) (< (fix x) (fix y))) (defun plus (x y) (+ (fix x) (fix y))) (defun diff (x y) (fix (- (fix x) (fix y)))) Note that (fix x) gets a :type-prescription rule that it is a nonnegative integer. Now we prove a :linear-alias rule, actually a package of the six rules above. (defthm nqthm-linear-arithmetic (and (equal (fix (plus x y)) (plus x y)) (equal (fix (diff x y)) (diff x y)) (equal (fix (fix x)) (fix x)) (equal (lessp x y) (< (fix x) (fix y))) (equal (plus x y) (+ (fix x) (fix y))) (implies (not (lessp x y)) (equal (diff x y) (- (fix x) (fix y))))) :rule-classes :linear-alias) To mimic Nqthm behavior, we need a :rewrite rule to dispatch the cases generated by the case split caused by linearizing diff-expressions. This is not, strictly speaking, part of linear aliasing. (defthm diff-0 (implies (lessp x y) (equal (diff x y) 0))) Now we disable the nqthm-level functions. Henceforth, we do not expect to see ACL2-level functions in proofs about these concepts. (in-theory (disable fix lessp plus diff)) Note that we can now prove such facts as (thm (implies (and (lessp a b) (lessp b c)) (lessp a c))) (thm (implies (lessp a (diff b c)) (lessp a b))) and that the proofs appeal to linear arithmetic! We can add new aliases (although they get new names). Note that we have to (a) define the function, (b) prove the :linear-alias rule --- probably enabling nqthm-level functions to do it, and (c) disable the new function so it survives rewriting and is around for linearization to de-alias. (defun add1 (x) (+ (fix x) 1)) ; (a) (defthm add1-linear ; (b) - see below (and (equal (add1 x) (+ (fix x) 1)) (equal (fix (add1 x)) (add1 x))) :rule-classes :linear-alias :hints (("Goal" :in-theory (enable fix)))) (in-theory (disable add1)) ; (c) (thm (lessp x (add1 x))) Observe that in (b) we prove two rules about add1: the one that relates it to + and the one that removes the fixes inserted by the first rule. Next we illustrate the use of :linear lemmas in the context of linear aliasing. Consider the function: (defun strpos (pat str) ; Find the position of pat in str. (cond ((atom str) 0) ((equal pat (car str)) 0) (t (add1 (strpos pat (cdr str)))))) (defun strlen (str) (cond ((atom str) 0) (t (add1 (strlen (cdr str)))))) We can prove and store the following :linear lemma about strpos. (defthm strpos-length (not (lessp (strlen str) (strpos pat str))) :rule-classes :linear) This event is interesting for two reasons. The proof illustrates linear aliasing. But the fact that this event is stored as a :linear lemma -- even though the conclusion is not about < -- also illustrates linear aliasing. In fact, this lemma is stored under (strpos pat str) with :fixer fix. We can illustrate the storage and retrieval of the lemma directly by proving: (thm (not (< (fix (strlen str)) (fix (strpos pat str))))) But more commonly we will be interested in proofs that reach out for facts about strpos (implicitly fixing them for us) as in: (thm (implies (lessp (strlen str) mx) (lessp (strpos pat str) mx))). This ends the extended example of linear aliasing lemmas.  File: acl2-doc-lemacs.info, Node: META, Next: REFINEMENT, Prev: LINEAR-ALIAS, Up: RULE-CLASSES META make a :meta rule (a hand-written simplifier) *Note RULE-CLASSES:: for a general discussion of rule classes and how they are used to build rules from formulas. 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. Example :corollary formulas from which :meta rules might be built are: Examples: (equal (ev x a) ; Modify the rewriter to use fn to (ev (fn x) a)) ; transform terms. The :trigger-fns ; of the :meta rule-class specify ; the top-most function symbols of ; those x that are candidates for ; this transformation. (implies (and (pseudo-termp x) ; As above, but this illustrates (alistp a)) ; that without loss of generality we (equal (ev x a) ; may restrict x to be shaped like a (ev (fn x) a))) ; term and a to be an alist. (implies (and (pseudo-termp x) ; As above (with or without the (alistp a) ; hypotheses on x and a) with the (ev (hyp-fn x) a)); additional restriction that the (equal (ev x a) ; meaning of (hyp-fn x) is true in (ev (fn x) a))) ; the current context. That is, the ; applicability of the transforma- ; tion may be dependent upon some ; computed hypotheses. A non-nil list of function symbols must be supplied as the value of the :trigger-fns field in a :meta rule class object. 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 (equiv (ev x a) (ev (fn x) a))) where equiv is a known equivalence relation, x and a are distinct variable names, and ev is an evaluator function (see below), and fn is a function symbol, as is hyp-fn when provided. Both fn and hyp-fn should take a single argument. If fn and/or hyp-fn are guarded, their guards should be (implied by) pseudo-termp. *Note PSEUDO-TERMP::. We say the theorem above is a "metatheorem" or "metalemma" and fn is a "metafunction", and hyp-fn is a "hypothesis metafunction". 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, x, of fn and hyp-fn as a "term." When these metafunctions are executed by the simplifier, they will be applied to (the quotations of) terms. But during the proof of the metatheorem itself, x may not be the quotation of a term. If the pseudo-termp hypothesis is omitted, x may be any object. Even with the pseudo-termp hypothesis, x may merely "look like a term" but use non-function symbols or function symbols of incorrect arity. In any case, the metatheorem is stronger than necessary to allow us to apply the metafunctions to terms, as we do in the discussion below. We return later to the question of proving the metatheorem. Suppose the general form of the metatheorem above is proved with the pseudo-termp and alistp hypotheses. Then when the simplifier encounters a term, (h t1 ... tn), that begins with a function symbol, h, listed in :trigger-fns, it applies the metafunction, fn, to the quotation of the term, i.e., it evaluates (fn '(h t1 ... tn)) to obtain some result, which can be written as 'val. If 'val is different from '(h t1 ... tn) and val is a term, then (h t1 ... tn) is replaced by val, which is then passed along for further rewriting. Because the metatheorem establishes the correctness of fn for all terms (even non-terms!), there is no restriction on which function symbols are listed in the :trigger-fns. Generally, of course, they should be the symbols that head up the terms simplified by the metafunction fn. *Note TERM-TABLE:: for how one obtains some assistance towards guaranteeing that val is indeed a term. The "evaluator" function, ev, is a function that can evaluate a certain class of expressions, namely, all of those composed of variables, constants, and applications of a fixed, finite set of function symbols, g1, ..., gk. Generally speaking, the set of function symbols handled by ev is chosen to be exactly the function symbols recognized and manipulated by the metafunctions being introduced. For example, if fn manipulates expressions in which 'equal and 'binary-append occur as function symbols, then ev is generally specified to handle equal and binary-append. The actual requirements on ev become clear when the metatheorem is proved. The standard way to introduce an evaluator is to use the ACL2 macro defevaluator, though this is not strictly necessary. *Note DEFEVALUATOR:: for details. Why are we justified in using metafunctions this way? Suppose (fn 'term1) is 'term2. What justifies replacing term1 by term2? The first step is to assert that term1 is (ev 'term1 a), where a is an alist that maps 'var to var, for each variable var in term1. This step is incorrect, because 'term1 may contain function symbols other than the ones, g1, ..., gk, that ev knows how to handle. But we can grow ev to a "larger" evaluator, ev*, an evaluator for all of the symbols that occur in term1 or term2. We can prove that ev* satisfies the constraints on ev. Hence, the metatheorem holds for ev* in place of ev, by functional instantiation. We can then carry out the proof of the equivalence of term1 and term2 as follows: Fix a to be an alist that maps the quotations of the variables of term1 and term2 to themselves. Then, 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 term1 is a term and a is an alist by construction. 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, (h t1 ... tn), where h is listed in :trigger-fns. This time, after it applies fn to '(h t1 ... tn) to obtain the quotation of some new term, 'val, it then applies the hypothesis metafunction, hyp-fn. That is, it evaluates (hyp-fn '(h t1 ... tn)) to obtain some result, which can be written as 'hyp-val. If hyp-val is not in fact a term, the metafunction is not used. Provided hyp-val is a term, the simplifier attempts to establish (by conventional backchaining) that this term is non-nil in the current context. If this attempt fails, then the meta rule is not applied. Otherwise, (h t1...tn) is replaced by val as in the previous case (where there was no hypothesis metafunction). 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 (new-fn x) is defined to be (list 'if (hyp-fn x) (fn x) x). (If we're careful, we realize that this argument depends on making an extension of ev to an evaluator ev* that handles if and the functions manipulated by hyp-fn.) If we write 'term for the quotation of the present term, and if (hyp-fn 'term) and (fn 'term) are both terms, say hyp1 and term1, then by the previous argument we know it is sound to rewrite term to (if hyp1 term1 term). But since we have established in the current context that hyp1 is non-nil, we may simplify (if hyp1 term1 term) to term1, as desired. We now discuss the role of the pseudo-termp hypothesis. (Pseudo-termp x) checks that x has the shape of a term. Roughly speaking, it insures that x is a symbol, a quoted constant, or a true list consisting of a lambda expression or symbol followed by some pseudo-terms. Among the properties of terms not checked by pseudo-termp are that variable symbols never begin with ampersand, lambda expressions are closed, and function symbols are applied to the correct number of arguments. *Note PSEUDO-TERMP::. 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 (*Note GUARDS-AND-EVALUATION::, especially the section on efficiency issues), (b) verify the guards of the metafunction (*Note VERIFY-GUARDS::), and (c) compile the metafunction (*Note COMP::). When these three steps have been taken the simplifier can evaluate (fn 'term1) by running the compiled "primary code" (*Note GUARDS-AND-EVALUATION::) for fn directly in Common Lisp. Before discussing efficiency issues further, let us review the for a moment the general case in which we wish to evaluate (fn `obj) for some :logic function. We must first ask whether the guards of fn have been verified. If not, we must evaluate fn by executing its logic definition. This effectively checks the guards of every subroutine and so can be slow. If, on the other hand, the guards of fn have been verified, then we can run the primary code for fn, provided 'obj satisfies the guard of fn. So we must next evaluate the guard of fn on 'obj. If the guard is met, then we run the primary code for fn, otherwise we run the logic code. 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 term1 is a term and hence 'term1 is a 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. Guard verification is also recommended.  File: acl2-doc-lemacs.info, Node: REFINEMENT, Next: REWRITE, Prev: META, Up: RULE-CLASSES REFINEMENT record that one equivalence relation refines another *Note 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 :refinement rule might be built is: Example: (implies (bag-equal x y) (set-equal y x)). Also *Note DEFREFINEMENT::. General Form: (implies (equiv1 x y) (equiv2 x y)) Equiv1 and equiv2 must be known equivalence relations. The effect of such a rule is to record that equiv1 is a refinement of equiv2. This means that equiv1 :rewrite rules may be used while trying to maintain equiv2. *Note EQUIVALENCE:: for a general discussion of the issues. The macro form (defrefinement equiv1 equiv2) is an abbreviation for a defthm of rule-class :refinement that establishes that equiv1 is a refinement of equiv2. *Note DEFREFINEMENT::. Suppose we have the :rewrite rule (bag-equal (append a b) (append b a)) which states that append is commutative modulo bag-equality. Suppose further we have established that bag-equality refines set-equality. Then when we are simplifying append expressions while maintaining set-equality we use append's commutativity property, even though it was proved for bag-equality. Equality is known to be a refinement of all equivalence relations. The transitive closure of the refinement relation is maintained, so if set-equality, say, is shown to be a refinement of some third sense of equivalence, then bag-equality will automatially be known as a refinement of that third equivalence. :refinement lemmas cannot be disabled. That is, once one equivalence relation has been shown to be a refinement of another, there is no way to prevent the system from using that information. Of course, individual :rewrite rules can be disabled. More will be written about this as we develop the techniques.  File: acl2-doc-lemacs.info, Node: REWRITE, Next: TYPE-PRESCRIPTION, Prev: REFINEMENT, Up: RULE-CLASSES REWRITE make some :rewrite rules (possibly conditional ones) *Note RULE-CLASSES:: for a general discussion of rule classes and how they are used to build rules from formulas. Example :corollary formulas from which :rewrite rules might be built are: Example: (equal (+ x y) (+ y x)) replace (+ a b) by (+ b a) provided certain heuristics approve the permutation. (implies (true-listp x) replace (append a nil) by a, if (equal (append x nil) x)) (true-listp a) rewrites to t (implies replace (member a (append b c)) by (and (eqlablep e) (member a (append c b)) in contexts (true-listp x) in which propositional equivalence (true-listp y)) is sufficient, provided (eqlablep a) (iff (member e (append x y)) (true-listp b) and (true-listp c) (member e (append y x)))) rewrite to t and the permutative heuristics approve General Form: (and ... (implies (and ...hi...) (implies (and ...hk...) (and ... (equiv lhs rhs) ...))) ...) Note: One :rewrite rule class object might create many rewrite rules from the :corollary formula. To create the rules, we first translate the formula (expanding all macros; also *Note TRANS::). Next, we eliminate all lambdas; one may think of this step as simply substituting away every let, let*, and mv-let in the formula. We then flatten the and and implies structure of the formula, transforming it into a conjunction of formulas, each of the form (implies (and h1 ... hn) concl) where no hypothesis is a conjunction and concl is neither a conjunction nor an implication. If necessary, the hypothesis of such a conjunct may be vacuous. We then further coerce each concl into the form (equiv lhs rhs), where equiv is a known equivalence relation, by replacing any concl not of that form by (iff concl t). A concl of the form (not term) is considered to be of the form (iff term nil). By these steps we reduce the given :corollary to a sequence of conjuncts, each of which is of the form (implies (and h1 ... hn) (equiv lhs rhs)) where equiv is a known equivalence relation. *Note EQUIVALENCE::for a general discussion of the introduction of new equivalence relations. We create a :rewrite rule for each such conjunct, if possible, and otherwise cause an error. It is possible to create a rewrite rule from such a conjunct provided lhs is not a variable, a quoted constant, a let-expression, a lambda application, or an if-expression. A :rewrite rule is used when any instance of the lhs occurs in a context in which the equivalence relation is operative. First, we find a substitution that makes lhs equal to the target term. Then we attempt to relieve the instantiated hypotheses of the rule. Hypotheses that are fully instantiated are relieved by recursive rewriting. Hypotheses that contain "free variables" (variables not assigned by the unifying substitution) are relieved by attempting to guess a suitable instance so as to make the hypothesis equal to some known assumption in the context of the target. If the hypotheses are relieved, and certain restrictions that prevent some forms of infinite regress are met (*Note LOOP-STOPPER::), the target is replaced by the instantiated rhs, which is then recursively rewritten. At the moment, the best description of how ACL2 :rewrite rules are used may be found in the discussion of "Replacement Rules" pp 234 of A Computational Logic Handbook.  File: acl2-doc-lemacs.info, Node: TYPE-PRESCRIPTION, Next: TYPE-SET-INVERTER, Prev: REWRITE, Up: RULE-CLASSES TYPE-PRESCRIPTION make a rule that specifies the type of a term *Note RULE-CLASSES:: for a general discussion of rule classes and how they are used to build rules from formulas. Some example :corollary formulas from which :type-prescription rules might be built are: Examples: (implies (nth n lst) is of type characterp (and (character-listp lst) provided the two hypotheses can (< n (length lst))) be established by type reasoning (characterp (nth n lst))). (implies (demodulize a lst 'value ans) is (and (atom a) either a nonnegative integer or (true-listp lst) of the same type as ans, provided (member-equal a lst)) the hyps can be established by type (or (and reasoning (integerp (demodulize a lst 'value ans)) (>= (demodulize a lst 'value ans) 0)) (equal (demodulize a lst 'value ans) ans))). To specify the term whose type (*Note TYPE-SET::) is described by the rule, provide that term as the value of the :typed-term field of the rule class object. General Form: (implies hyps (or type-restriction1-on-pat ... type-restrictionk-on-pat (equal pat var1) ... (equal pat varj))) where pat is the application of some function symbol to some arguments, each type-restrictioni-on-pat is a term involving pat and containing no variables outside of the occurrences of pat, and each vari is one of the variables of pat. Generally speaking, the type-restriction terms ought to be terms that inform us as to the type of pat. Ideally, they should be "primitive recognizing expressions" about pat; *Note COMPOUND-RECOGNIZER::. If the :typed-term is not provided in the rule class object, it is computed heuristically by looking for a term in the conclusion whose type is being restricted. An error is caused if no such term is found. Roughly speaking, the effect of adding such a rule is to inform the ACL2 typing mechanism that pat has the type described by the conclusion, when the hypotheses are true. In particular, the type of pat is within the union of the types described by the several disjuncts. The "type described by" (equal pat vari) is the type of vari. More operationally, when asked to determine the type of a term that is an instance of pat, ACL2 will first attempt to establish the hypotheses. *This is done by type reasoning alone, not rewriting!* Of course, if some hypothesis is to be forced, it is so treated; *Note FORCE::. Provided the hypotheses are established by type reasoning, ACL2 then unions the types described by the type-restrictioni-on-pat terms together with the types of those subexpressions of pat identified by the vari. The final type computed for a term is the intersection of the types implied by each applicable rule. Type prescription rules may be disabled. Because only type reasoning is used to establish the hypotheses of :type-prescription rules, some care must be taken with the hypotheses. Suppose, for example, that the non-recursive function my-statep is defined as (defun my-statep (x) (and (true-listp x) (equal (length x) 2))) and suppose (my-statep s) occurs as a hypothesis of a :type-prescription rule that is being considered for use in the proof attempt for a conjecture with the hypothesis (my-statep s). Since the hypothesis in the conjecture is rewritten, it will become the conjunction of (true-listp s) and (equal (length s) 2). Those two terms will be assumed to have type t in the context in which the :type-prescription rule is tried. But type reasoning will be unable to deduce that (my-statep s) has type t in this context. Thus, either my-statep should be disabled (*Note DISABLE::) during the proof attempt or else the occurrence of (my-statep s) in the :type-prescription rule should be replaced by the conjunction into which it rewrites. While this example makes it clear how non-recursive predicates can cause problems, non-recursive functions in general can cause problems. For example, if (mitigate x) is defined to be (if (rationalp x) (1- x) x) then the hypothesis (pred (mitigate s)) in the conjecture will rewrite, opening mitigate and splitting the conjecture into two subgoals, one in which (rationalp s) and (pred (1- x)) are assumed and the other in which (not (rationalp s)) and (pred x) are assumed. But (pred (mitigate s)) will not be typed as t in either of these contexts. The moral is: beware of non-recursive functions occuring in the hypotheses of :type-prescription rules. Because of the freedom one has in forming the conclusion of a type-prescription, we have to use heuristics to recover the pattern, pat, whose type is being specified. In some cases our heuristics may not identify the intended term and the :type-prescription rule will be rejected as illegal because the conclusion is not of the correct form. When this happens you may wish to specify the pat directly. This may be done by using a suitable rule class token. In particular, when the token :type-prescription is used it means ACL2 is to compute pat with its heuristics; otherwise the token should be of the form (:type-prescription :typed-term pat), where pat is the term whose type is being specified. The defun event may generate a :type-prescription rule. Suppose fn is the name of the function concerned. Then (:type-prescription fn) is the rune given to the type-prescription, if any, generated for fn by defun. (The trivial rule, saying fn has unknown type, is not stored, but defun still allocates the rune and the corollary of this rune is known to be t.)  File: acl2-doc-lemacs.info, Node: TYPE-SET-INVERTER, Next: WELL-FOUNDED-RELATION, Prev: TYPE-PRESCRIPTION, Up: RULE-CLASSES TYPE-SET-INVERTER exhibit a new decoding for an ACL2 type-set *Note RULE-CLASSES:: for a general discussion of rule classes and how they are used to build rules from formulas. Example Rule Class: (:type-set-inverter :corollary (equal (and (counting-number x) (not (equal x 0))) (and (integerp x) (< x 0))) :type-set 2) General Forms of Rule Class: :type-set-inverter, or (:type-set-inverter :type-set n) General Form of Theorem or Corollary: (EQUAL new-expr old-expr) where n is a type-set (*Note TYPE-SET::) and old-expr is the term containing x as a free variable that ACL2 currently uses to recognize type-set n. For a given n, the exact form of old-expr is generated by (convert-type-set-to-term 'x n (ens state) (w state) nil)]. If the :type-set field of the rule-class is omitted, we attempt to compute it from the right-hand side, old-expr, of the corollary. That computation is done by type-set-implied-by-term (*Note TYPE-SET::). However, it is possible that the type-set we compute from lhs does not have the required property that when inverted with convert-type-set-to-term the result is lhs. If you omit :type-set and an error is caused because lhs has the incorrect form, you should manually specify both :type-set and the lhs generated by convert-type-set-to-term. The rule generated will henceforth make new-expr be the term used by ACL2 to recognize type-set n. If this rule is created by a defthm event named name then the rune of the rule is (:type-set-inverter name) and by disabling that rune you can prevent its being used to decode type-sets. Type-sets are inverted when forced assumptions are turned into formulas to be proved. In their internal form, assumptions are essentially pairs consisting of a context and a goal term, which was forced. Abstractly a context is just a list of hypotheses which may be assumed while proving the goal term. But actually contexts are alists which pair terms with type-sets, encoding the current hypotheses. For example, if the original conjecture contained the hypothesis (integerp x) then the context used while working on that conjecture will include the assignment to x of the type-set *ts-integer*.  File: acl2-doc-lemacs.info, Node: WELL-FOUNDED-RELATION, Prev: TYPE-SET-INVERTER, Up: RULE-CLASSES WELL-FOUNDED-RELATION show that a relation is well-founded on a set *Note 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 :well-founded-relation rule might be built is as follows. (Of course, the functions pairp, lex2p, and ordinate would have to be defined first.) Example: (and (implies (pairp x) (e0-ordinalp (ordinate x))) (implies (and (pairp x) (pairp y) (lex2p x y)) (e0-ord-< (ordinate x) (ordinate y)))) The above example establishes that lex2p is a well-founded relation on pairps. We explain and give details below. Exactly two general forms are recognized: General Forms (AND (IMPLIES (mp x) (E0-ORDINALP (fn x))) ; Property 1 (IMPLIES (AND (mp x) ; Property 2 (mp y) (rel x y)) (E0-ORD-< (fn x) (fn y)))), or (AND (E0-ORDINALP (fn x)) ; Property 1 (IMPLIES (rel x y) ; Property 2 (E0-ORD-< (fn x) (fn y)))) where mp, fn, and rel are function symbols, x and y are distinct variable symbols, and no other :well-founded-relation theorem about fn has been proved. When the second general form is used, we act as though the first form were used with mp being the function that ignores its argument and returns t. The discussion below therefore considers only the first general form. Note: We are very rigid when checking that the submitted formula is of one of these forms. For example, in the first form, we insist that all the conjuncts appear in the order shown above. Thus, interchanging the two properties in the top-level conjunct or rearranging the hyptheses in the second conjunct both produce unrecognized forms. The requirement that each fn be proved well-founded at most once insures that for each well-founded relation, fn, there is a unique mp that recognizes the domain on which rel is well-founded. We impose this requirement simply so that rel can be used as a short-hand when specifying the well-founded relations to be used in definitions; otherwise the specification would have to indicate which mp was to be used. Mp is a predicate that recognizes the objects that are supposedly ordered in a well-founded way by rel. We call such an object an "mp-measure" or simply a "measure" when mp is understood. Property 1 tells us that every measure can be mapped into an ACL2 ordinal. (*Note E0-ORDINALP::.) This mapping is performed by fn. Property 2 tells us that if the measure x is smaller than the measure y according to rel then the image of x under fn is a smaller than that of y, according to the well-founded relation e0-ord-<. (*Note E0-ORD-<::.) Thus, the general form of a :well-founded-relation formula establishes that there exists a rel-order preserving embedding (namely via fn) of the mp-measures into the ordinals. We can thus conclude that rel is well-founded on mp-measures. Such well-founded relations are used in the admissibility test for recursive functions, in particular, to show that the recursion terminates. To illustrate how such information may be used, consider a generic function definition (defun g (x) (if (test x) (g (step x)) (base x))). If rel has been shown to be well-founded on mp-measures, then g's termination can be insured by finding a measure, (m x), with the property that m produces a measure: (mp (m x)), ; Defun-goal-1 and that the argument to g gets smaller (when measured by m and compared by rel) in the recursion, (implies (test x) (rel (m (step x)) (m x))). ; Defun-goal-2 If rel is selected as the :well-founded-relation to be used in the definition of g, the definitional principal will generate and attempt to prove defun-goal-1 and defun-goal-2 to justify g. We show later why these two goals are sufficient to establish the termination of g. Observe that neither the ordinals nor the embedding, fn, of the mp-measures into the ordinals is involved in the goals generated by the definitional principal. Suppose now that a :well-founded-relation theorem has been proved for mp and rel. How can rel be "selected as the :well-founded-relation" by defun? There are two ways. First, an xargs keyword to the defun event allows the specification of a :well-founded-relation. Thus, the definition of g above might be written (defun g (x) (declare (xargs :well-founded-relation (mp . rel))) (if (test x) (g (step x)) (base x))) Alternatively, rel may be specified as the :default-well-founded-relation in acl2-defaults-table by executing the event (set-default-well-founded-relation rel). When a defun event does not explicitly specify the relation in its xargs the default relation is used. When ACL2 is initialized, the default relation is e0-ord-<. Finally, though it is probably obvious, we now show that defun-goal-1 and defun-goal-2 are sufficient to insure the termination of g provided property-1 and property-2 of mp and rel have been proved. To this end, assume we have proved defun-goal-1 and defun-goal-2 as well as property-1 and property-2 and we show how to admit g under the primitive ACL2 definitional principal (i.e., using only the ordinals). In particular, consider the definition event (defun g (x) (declare (xargs :well-founded-relation e0-ord-< :measure (fn (m x)))) (if (test x) (g (step x)) (base x))) Proof that g is admissible: To admit the definition of g above we must prove (e0-ordinalp (fn (m x))) ; *1 and (implies (test x) ; *2 (e0-ord-< (fn (m (step x))) (fn (m x)))). But *1 can be proved by instantiating property-1 to get (implies (mp (m x)) (e0-ordinalp (fn (m x)))), and then relieving the hypothesis with defun-goal-1, (mp (m x)). Similarly, *2 can be proved by instantiating property-2 to get (implies (and (mp (m (step x))) (mp (m x)) (rel (m (step x)) (m x))) (e0-ord-< (fn (m (step x))) (fn (m x)))) and relieving the first two hypotheses by appealing to two instances of defun-goal-1, thus obtaining (implies (rel (m (step x)) (m x)) (e0-ord-< (fn (m (step x))) (fn (m x)))). By chaining this together with defun-goal-2, (implies (test x) (rel (m (step x)) (m x))) we obtain *2. Q.E.D.  File: acl2-doc-lemacs.info, Node: THEORIES, Prev: RULE-CLASSES, Up: Top THEORIES sets of runes to enable/disable in concert Example: '((:definition app) (:executable-counterpart app) rv (rv) assoc-of-app) See: * Menu: * CURRENT-THEORY:: currently enabled rules as of logical name * DISABLE:: deletes names from current theory * ENABLE:: adds names to current theory * EXECUTABLE-COUNTERPART-THEORY:: executable counterpart rules as of logical name * FUNCTION-THEORY:: function symbol rules as of logical name * GROUND-ZERO:: enabled rules in the startup theory * INCOMPATIBLE:: declaring that two rules should not both be enabled * INTERSECTION-THEORIES:: intersect two theories * RULE-NAMES:: How rules are named. * RUNE:: a rule name * SET-DIFFERENCE-THEORIES:: difference of two theories * THEORY:: retrieve named theory * THEORY-FUNCTIONS:: functions for obtaining or producing theories * UNION-THEORIES:: union two theories * UNIVERSAL-THEORY:: all rules as of logical name Related topics other than immediate subtopics: * DEFTHEORY:: define a theory (to enable or disable a set of rules) A theory is a list of "runic designators" as described below. Each runic designator denotes a set of "runes" (*Note RUNE::) and by unioning together the runes denoted by each member of a theory we define the set of runes corresponding to a theory. Theories are used to control which rules are "enabled," i.e., available for automatic application by the theorem prover. There is always a "current" theory. A rule is enabled precisely if its rune is an element of the set of runes corresponding to the current theory. At the top-level, the current theory is the theory selected by the most recent in-theory event, extended with the rule names introduced since then. Inside the theorem prover, the :in-theory hint (*Note HINTS::) can be used to select a particular theory as current during the proof attempt for a particular goal. Theories are generally constructed by "theory expressions." Formally, a theory expression is any term, containing at most the single free variable world, that when evaluated with world bound to the current ACL2 world (*Note WORLD::) produces a theory. ACL2 provides various functions for the convenient construction and manipulation of theories. These are called "theory functions" (*Note THEORY-FUNCTIONS::). For example, the theory function union-theories takes two theories and produces their union. The theory function universal-theory returns the theory containing all known rule names as of the introduction of a given logical name. But a theory expression can contain constants, e.g., '(assoc (assoc) (:rewrite car-cons) car-cdr-elim) and user-defined functions. The only important criterion is that a theory expression mention no variable freely except world and evaluate to a theory. More often than not, theory expressions typed by the user do not mention the variable world. This is because user-typed theory expressions are generally composed of applications of ACL2's theory functions. These "functions" are actually macros that expand into terms in which world is used freely and appropriately. Thus, the technical definition of "theory expression" should not mislead you into thinking that interestng theory expressions must mention world; they probably do and you just didn't know it! One aspect of this arrangement is that theory expressions cannot generally be evaluated at the top-level of ACL2, because world is not bound. To see the value of a theory expression, expr, at the top-level, type ACL2 !>(LET ((WORLD (W STATE))) expr). However, because the built-in theories are quite long, you may be sorry you printed the value of a theory expression! A theory is a true list of runic designators and to each theory there corresponds a set of runes, obtained by unioning together the sets of runes denoted by each runic designator. For example, the theory constant '(assoc (assoc) (:rewrite car-cons) car-cdr-elim) corresponds to the set of runes {(:definition assoc) (:executable-counterpart assoc) (:rewrite car-cons) (:rewrite car-cdr-elim) (:elim car-cdr-elim)} . Observe that the theory contains four elements but its runic correspondent contains five. That is because some designators denote sets of several runes. If the above theory were selected as current then the five rules named in its runic counterpart would be enabled and all other rules would be disabled. We now precisely define the runic designators and the set of runes denoted by each. o A rune is a runic designator and denotes the singleton set containing that rune. o If symb is a function symbol introduced with a defun (or defuns) event, then symb is a runic designator and denotes the singleton set containing the rune (:definition symb). o If symb is a function symbol introduced with a defun (or defuns) event, then (symb) is a runic designator and denotes the singleton set containing the rune (:executable-counterpart symb). o If symb is the name of a defthm (or defaxiom) event that introduced at least one rule, then symb is a runic designator and denotes the set of the names of all rules introduced by the named event. o If str is the string naming some defpkg event and symb is the symbol returned by (intern str "ACL2"), then symb is a runic designator and denotes the singleton set containing (:rewrite symb), which is the name of the rule stating the conditions under which the symbol-package-name of (intern x str) is str. o If symb is the name of a deftheory event, then symb is a runic designator and denotes the runic theory corresponding to symb. These conventions attempt to implement the Nqthm-1992 treatment of theories. For example, including a function name, e.g., assoc, in the current theory enables that function but does not enable the executable counterpart. Similarly, including (assoc) enables the executable counterpart (Nqthm's *1*assoc) but not the symbolic definition. And including the name of a proved lemma enables all of the rules added by the event. These conventions are entirely consistent with Nqthm usage. Of course, in ACL2 one can include explicitly the runes naming the rules in question and so can avoid entirely the use of non-runic elements in theories. Because a rune is a runic designator denoting the set containing that rune, a list of runes is a theory and denotes itself. We call such theories "runic theories." To every theory there corresponds a runic theory obtained by unioning together the sets denoted by each designator in the theory. When a theory is selected as "current" it is actually its runic correspondent that is effectively used. That is, a rune is enabled iff it is a member of the runic correspondent of the current theory. The value of a theory defined with deftheory is the runic correspondent of the theory computed by the defining theory expression. The theory manipulation functions, e.g., union-theories, actually convert their theory arguments to their runic correspondents before performing the required set operation. The manipulation functions always return runic theories. Thus, it is sometimes convenient to think of (non-runic) theories as merely abbreviations for their runic correspondents, abbreviations which are "expanded" at the first opportunity by theory manipulation functions and the "theory consumer" functions such as in-theory and deftheory.