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.8 Copyright (C) 1989-95 Computational Logic, Inc. (CLI). All rights reserved.  File: acl2-doc-lemacs.info, Node: NOTE7, Next: NOTE8, Prev: NOTE6, Up: RELEASE-NOTES NOTE7 ACL2 Version 1.7 (released October 1994) Notes Include-book now takes (optionally) an additional keyword argument, indicating whether a compiled file is to be loaded. The default behavior is unchanged, except that a warning is printed when a compiled file is not loaded. *Note INCLUDE-BOOK::. A markup language for documentation strings has been implemented, and many of the source files have been marked up using this language (thanks largely to the efforts of Laura Lawless). *Note MARKUP::. Moreover, there are translators that we have used to provide versions of the ACL2 documentation in info (for use in emacs), html (for Mosaic), and tex (for hardcopy) formats. A new event defdoc has been implemented. It is like deflabel, but allows redefinition of doc strings and has other advantages. *Note DEFDOC::. We used to ignore corollaries when collecting up the axioms introduced about constrained functions. That bug has been fixed. We thank John Cowles for bringing this bug to our attention. The macro defstub now allows a :doc keyword argument, so that documentation may be attached to the name being introduced. A new command nqthm-to-acl2 has been added to help Nqthm users to make the transition to ACL2. *Note NQTHM-TO-ACL2::, which also includes a complete listing of the relevant tables. Many function names, especially of the form "foo-lst", have been changed in order to support the following convention, for any "foo": (foo-listp lst) represents the notion (for x in lst always foop x). A complete list of these changes may be found at the end of this note. All of them except symbolp-listp and list-of-symbolp-listp have the string "-lst" in their names. Note also that keyword-listp has been renamed keyword-value-listp. Accumulated persistence has been implemented. It is not connected to :brr or rule monitoring. *Note ACCUMULATED-PERSISTENCE::. :Trigger-terms has been added for :linear rule classes, so you can hang a linear rule under any addend you want. *Note LINEAR::, which has been improved and expanded. ACL2 now accepts 256 characters and includes the Common Lisp functions code-char and char-code. However, ACL2 controls the lisp reader so that #\c may only be used when c is a single standard character or one of Newline, Space, Page, Rubout, Tab. If you want to enter other characters use code-char, e.g., (coerce (list (code-char 7) (code-char 240) #a) 'string). *Note CHARACTERS::. Note: our current handling of characters makes the set of theorems different under Macintosh Common Lisp (MCL) than under other Common Lisps. We hope to rectify this situation before the final release of ACL2. A new table, macro-aliases-table, has been implemented, that associates macro names with function names. So for example, since append is associated with binary-append, the form (disable append) it is interpreted as though it were (disable binary-append). *Note MACRO-ALIASES-TABLE::, *Note ADD-MACRO-ALIAS:: and *Note REMOVE-MACRO-ALIAS::. The implementation of conditional metalemmas has been modified so that the metafunction is applied before the hypothesis metafunction is applied. *Note META::. The Common Lisp functions acons and endp have been defined in the ACL2 logic. We have added the symbol declare to the list *acl2-exports*, and hence to the package "ACL2-USER". A new hint, :restrict, has been implemented. *Note HINTS::. It used to be that if :ubt were given a number that is greater than the largest current command number, it treated that number the same as :max. Now, an error is caused. The table :force-table has been eliminated. A command :disabledp (and macro disabledp) has been added; *Note DISABLEDP::. Compilation via :set-compile-fns is now suppressed during include-book. In fact, whenever the state global variable ld-skip-proofsp has value 'include-book. Here are some less important changes, additions, and so on. Unlike previous releases, we have not proved all the theorems in axioms.lisp; instead we have simply assumed them. We have deferred such proofs because we anticipate a fairly major changed in Version 1.8 in how we deal with guards. We used to (accidentally) prohibit the "redefinition" of a table as a function. That is no longer the case. The check for whether a corollary follows tautologically has been sped up, at the cost of making the check less "smart" in the following sense: no longer do we expand primitive functions such as implies before checking this propositional implication. The command ubt! has been modified so that it never causes or reports an error. *Note UBT!::. ACL2 now works in Harlequin Lispworks. The user can now specify the :trigger-terms for :linear rules. *Note LINEAR::. The name of the system is now "ACL2"; no longer is it "Acl2". The raw lisp counterpart of theory-invariant is now defined to be a no-op as is consistent with the idea that it is just a call of table. A bug was fixed that caused proof-checker instructions to be executed when ld-skip-proofsp was t. The function rassoc has been added, along with a corresponding function used in its guard, r-eqlable-alistp. The in-theory event and hint now print a warning not only when certain "primitive" :definition rules are disabled, but also when certain "primitive" :executable-counterpart rules are disabled. The modified version of trace provided by ACL2, for use in raw Lisp, has been modified so that the lisp special variable *trace-alist* is consulted. This alist associates, using eq, values with their print representations. For example, initially *trace-alist* is a one-element list containing the pair (cons state '|*the-live-state*|). The system now prints an observation when a form is skipped because the default color is :red or :pink. (Technically: when-cool has been modified.) Additional protection exists when you submit a form to raw Common Lisp that should only be submitted inside the ACL2 read-eval-print loop. Here is a complete list of the changes in function names described near the top of this note, roughly of the form foo-lst --> foo-listp meaning: the name "foo-lst" has been changed to "foo-listp." symbolp-listp --> symbol-listp list-of-symbolp-listp --> symbol-list-listp {for consistency with change to symbol-listp} rational-lst --> rational-listp {which in fact was already defined as well} integer-lst --> integer-listp character-lst --> character-listp stringp-lst --> string-listp 32-bit-integer-lst --> 32-bit-integer-listp typed-io-lst --> typed-io-listp open-channel-lst --> open-channel-listp readable-files-lst --> readable-files-listp written-file-lst --> written-file-listp read-file-lst --> read-file-listp writeable-file-lst --> writable-file-listp {note change in spelling of "writable"} writeable-file-lst1 --> writable-file-listp1 pseudo-termp-lst --> pseudo-term-listp hot-termp-lst --> hot-term-listp {by analogy with pseudo-term-listp} weak-termp-lst --> weak-term-listp weak-termp-lst-lst --> weak-termp-list-listp ts-builder-case-lstp -> ts-builder-case-listp quotep-lst --> quote-listp termp-lst --> term-listp instr-lst --> instr-listp spliced-instr-lst --> spliced-instr-listp rewrite-fncallp-lst --> rewrite-fncallp-listp every-occurrence-equiv-hittablep1-lst --> every-occurrence-equiv-hittablep1-listp some-occurrence-equiv-hittablep1-lst --> some-occurrence-equiv-hittablep1-listp {by analogy with the preceding, even though it's a "some" instead of "all" predicate] almost-quotep1-lst --> almost-quotep1-listp ffnnames-subsetp-lst --> ffnnames-subsetp-listp boolean-lstp --> boolean-listp subst-expr1-lst-okp --> subst-expr1-ok-listp  File: acl2-doc-lemacs.info, Node: NOTE8, Next: NOTE8-UPDATE, Prev: NOTE7, Up: RELEASE-NOTES NOTE8 ACL2 Version 1.8 (May, 1995) Notes *Note NOTE8-UPDATE:: for yet more recent changes. Guards have been eliminated from the ACL2 logic. A summary is contained in this brief note. Also *Note DEFUN-MODE:: and *Note SET-GUARD-CHECKING::. Guards may be included in defuns as usual but are ignored from the perspective of admission to the logic: functions must terminate on all arguments. As in Nqthm, primitive functions, e.g., + and car, logically default unexpected arguments to convenient values. Thus, (+ 'abc 3) is 3 and (car 'abc) is nil. *Note PROGRAMMING::, and see the documentation for the individual primitive functions. In contrast to earlier versions of ACL2, Version 1.8 logical functions are executed at Nqthm speeds even when guards have not been verified. In versions before 1.8, such functions were interpreted by ACL2. Colors have been eliminated. Two "defun-modes" are supported, :program and :logic. Roughly speaking, :program does what :red used to do, namely, allow you to prototype functions for execution without any proof burdens. :Logic mode does what :blue used to do, namely, allow you to add a new definitional axiom to the logic. A global default-defun-mode is comparable to the old default color. The system comes up in :logic mode. To change the global defun-mode, type :program or :logic at the top-level. To specify the defun-mode of a defun locally use (declare (xargs :mode mode)). The prompt has changed. The initial prompt, indicating :logic mode, is ACL2 !> If you change to :program mode the prompt becomes ACL2 p!> Guards can be seen as having either of two roles: (a) they are a specification device allowing you to characterize the kinds of inputs a function "should" have, or (b) they are an efficiency device allowing logically defined functions to be executed directly in Common Lisp. If a guard is specified, as with xargs :guard, then it is "verified" at defun-time (unless you also specify xargs :verify-guards nil). Guard verification means what it always has: the input guard is shown to imply the guards on all subroutines in the body. If the guards of a function are verified, then a call of the function on inputs satisfying the guard can be computed directly by Common Lisp. Thus, verifying the guards on your functions will allow them to execute more efficiently. But it does not affect their logical behavior and since you will automatically get Nqthm speeds on unverified logical definitions, most users will probably use guards either as a specification device or only use them when execution efficiency is extremely important. Given the presence of guards in the system, two issues are unavoidable. Are guards verified as part of the defun process? And are guards checked when terms are evaluated? We answer both of those questions below. Roughly speaking, in its initial state the system will try to verify the guards of a defun if a :guard is supplied in the xargs and will not try otherwise. However, guard verification in defun can be inhibited "locally" by supplying the xargs :verify-guards nil. "Global" inhibition can be obtained via the :set-verify-guards-eagerness. If you do not use the :guard xargs, you will not need to think about guard verification. We now turn to the evaluation of expressions. Even if your functions contain no guards, the primitive functions do and hence you have the choice: when you submit an expression for evaluation do you mean for guards to be checked at runtime or not? Put another way, do you mean for the expression to be evaluated in Common Lisp (if possible) or in the logic? Note: If Common Lisp delivers an answer, it will be the same as in the logic, but it might be erroneous to execute the form in Common Lisp. For example, should (car 'abc) cause a guard violation error or return nil? The top-level ACL2 loop has a variable which controls which sense of execution is provided. To turn "guard checking on," by which we mean that guards are checked at runtime, execute the top-level form :set-guard-checking t. To turn it off, do :set-guard-checking nil. The status of this variable is reflected in the prompt. ACL2 !> means guard checking is on and ACL2 > means guard checking is off. The exclamation mark can be thought of as "barring" certain computations. The absence of the mark suggests the absence of error messages or unbarred access to the logical axioms. Thus, for example ACL2 !>(car 'abc) will signal an error, while ACL2 >(car 'abc) will return nil. Note that whether or not guards are checked at runtime is independent of whether you are operating in :program mode or :logic mode and whether theorems are being proved or not. (Although it must be added that functions defined in :program mode cannot help but check their guards because no logical definition exists.) Version 1.8 permits the verification of the guards of theorems, thus insuring that all instances of the theorem will evaluate without error in Common Lisp. To verify the guards of a theorem named name execute the event (verify-guards name). If a theorem's guards have been verified, the theorem is guaranteed to evaluate without error to non-nil in Common Lisp (provided resource errors do not arise). Caveat about verify-guards: implies is a function symbol, so in the term (implies p q), p cannot be assumed true when q is evaluated; they are both evaluated "outside." Hence, you cannot generally verify the guards on a theorem if implies is used to state the hypotheses. Use if instead. In a future version of ACL2, implies will likely be a macro. See sum-list-example.lisp for a nice example of the use of Version 1.8. This is roughly the same as the documentation for guard-example. We have removed the capability to do "old-style-forcing" as existed before Version 1.5. *Note NOTE5::. NOTE: Some low level details have, of course, changed. One such change is that there are no longer two distinct type prescriptions stored when a function is admitted with its guards verified. So for example, the type prescription rune for binary-append is now (:type-prescription binary-append) while in Versions 1.7 and earlier, there were two such runes: (:type-prescription binary-append . 1) (:type-prescription binary-append . 2) Nqthm-style forcing on linear arithmetic assumptions is no longer executed when forcing is disabled. Functional instantiation now benefits from a trick also used in Nqthm: once a constraint generated by a :functional-instance lemma instance (*Note LEMMA-INSTANCE::) has been proved on behalf of a successful event, it will not have to be re-proved on behalf of a later event. 1+ and 1- are now macros in the logic, not functions. Hence, for example, it is "safe" to use them on left-hand sides of rewrite rules, without invoking the common warning about the presence of nonrecursive function symbols. A new documentation section file-reading-example illustrates how to process forms in a file. A new proof-checker command forwardchain has been added; *Note ACL2-PC::FORWARDCHAIN::. It is now possible to use quantifiers. *Note DEFUN-SK:: and *Note DEFCHOOSE::. There is a new event set-inhibit-warnings, which allows the user to turn off warnings of various types. *Note SET-INHIBIT-WARNINGS::. An unsoundness relating encapsulate and :functional-instance hints has been remedied, with a few small effects visible at the user level. The main observable effect is that defaxiom and non-local include-book events are no longer allowed in the scope of any encapsulate event that has a non-empty signature. When certify-book is called, we now require that the default defun-mode (*Note DEFAULT-DEFUN-MODE::) be :logic. On a related note, the default defun-mode is irrelevant to include-book; the mode is always set to :logic initially, though it may be changed within the book and reverts to its original value at the conclusion of the include-book. A bug in include-book prevented it from acting this way even though the documentation said otherwise. The documentation has been substantially improved. A new section "Programming" contains documentation of many useful functions provided by ACL2; *Note PROGRAMMING::. Also, the documentation has been "marked up" extensively. Thus in particular, users of Mosaic will find many links in the documentation. The symbols force, mv-nth, and acl2-count have been added to the list *acl2-exports*. We now permit most names from the main Lisp package to be used as names, except for names that define functions, macros, or constants. *Note NAME::. We have changed the list of imports from the Common Lisp package to ACL2, i.e., the list *common-lisp-symbols-from-main-lisp-package*, to be exactly those external symbols of the Common Lisp package as specified by the draft Common Lisp standard. In order to accommodate this change, we have renamed some ACL2 functions as shown below, but these and other ramifications of this change should be transparent to most ACL2 users. warning --> warning$ print-object --> print-object$ Proof trees are no longer enabled by default. To start them up, :start-proof-tree. We have added the capability of building smaller images. The easiest way to do this on a Unix (trademark of AT&T) system is: make small. Here we will put some less important changes, additions, and so on. We have added definitions for the Common Lisp function position (for the test eql), as well as corresponding versions position-equal and position-eq that use tests equal and eq, respectively. *Note POSITION::, *Note POSITION-EQUAL::, and *Note POSITION-EQ::. The defthm event rational-listp-implies-rationalp-car no longer exists. We fixed a bug in the hint mechanism that applied :by, :cases, and :use hints to the first induction goal when the prover reverted to proving the original goal by induction. We fixed a bug in the handling of (set-irrelevant-formals-ok :warn). In support of removing the old-style forcing capability, we deleted the initialization of state global old-style-forcing and deleted the definitions of recover-assumptions, recover-assumptions-from-goal, remove-assumptions1, remove-assumptions, and split-on-assumptions, and we renamed split-on-assumptions1 to split-on-assumptions. The special value 'none in the proof-checker commands claim and = has been replaced by :none. A bug in the handling of hints by subgoals has been fixed. For example, formerly a :do-not hint could be "erased" by a :use hint on a subgoal. Thanks go to Art Flatau for noticing the bug. The functions weak-termp and weak-term-listp have been deleted, and their calls have been replaced by corresponding calls of pseudo-termp and pseudo-term-listp. The notion of pseudo-termp has been slightly strenthened by requiring that terms of the form (quote ...) have length 2. Performance has been improved in various ways. At the prover level, backchaining through the recognizer alist has been eliminated in order to significantly speed up ACL2's rewriter. Among the other prover changes (of which there are several, all technical): we no longer clausify the input term when a proof is interrupted in favor of inducting on the input term. At the IO level, we have improved performance somewhat by suitable declarations and proclamations. These include technical modifications to the macros mv and mv-let, and introduction of a macro the-mv analogous to the macro the but for forms returning multiple values. The function spaces now takes an extra argument, the current column. A bug in the proof-checker equiv command was fixed. The function intersectp has been deleted, because it was essentially duplicated by the function intersectp-equal. We now proclaim functions in AKCL and GCL before compiling books. This should result in somewhat increased speed. The function repeat has been eliminated; use make-list instead. The proof-checker command expand has been fixed so that it eliminates let (lambda) expressions when one would expect it to. A new primitive function, mv-nth, has been introduced. Mv-nth is equivalent to nth and is used in place of nth in the translation of mv-let expressions. This allows the user to control the simplification of mv-let expressions without affecting how nth is treated. In that spirit, the rewriter has been modified so that certain mv-nth expressions, namely those produced in the translation of (mv-let (a b c)(mv x y z) p), are given special treatment. A minor bug in untranslate has been fixed, which for example will fix the printing of conjunctions. Translate now takes a logicp argument, which indicates whether it enforces the restriction that :program mode functions do not occur in the result. The modified version of trace provided by ACL2, for use in raw Lisp, has been modified so that the lisp special variable *trace-alist* has a slightly different functionality. This alist associates, using eq, symbols with the print representations of their values. For example, initially *trace-alist* is a one-element list containing the pair (cons 'state '|*the-live-state*|). Thus, one may cons the pair (cons '*foo* "It's a FOO!") on to *trace-alist*; then until *foo* is defined, this change will have no effect, but after for example (defconst *foo* 17) then trace will print 17 as "It's a FOO!". Trace also traces the corresponding logic function. Proof-tree display has been improved slightly in the case of successful proofs and certain event failures. The function positive-integer-log2 has been deleted. The macro skip-proofs now prints a warning message when it is encountered in the context of an encapsulate event or a book. *Note SKIP-PROOFS::. Some functions related to the-fn and wormhole1 now have defun-mode :program, but this change is almost certain to be inconsequential to all users.  File: acl2-doc-lemacs.info, Node: NOTE8-UPDATE, Prev: NOTE8, Up: RELEASE-NOTES NOTE8-UPDATE ACL2 Version 1.8 (Summer, 1995) Notes ACL2 can now use Ordered Binary Decision Diagram technology. *Note BDD::. There is also a proof-checker bdd command. ACL2 is now more respectful of the intention of the function hide. In particular, it is more careful not to dive inside any call of hide during equality substitution and case splitting. The ld special (*Note LD::) ld-pre-eval-print may now be used to turn off printing of input forms during processing of encapsulate and certify-book forms, by setting it to the value :never, i.e., (set-ld-pre-eval-print :never state). *Note LD-PRE-EVAL-PRINT::. The TUTORIAL documentation section has, with much help from Bill Young, been substantially improved to a bona fide introduction, and has been renamed acl2-tutorial. The term pretty-printer has been modified to introduce (<= X Y) as an abbreviation for (not (< Y X)). Forward chaining and linear arithmetic now both benefit from the evaluation of ground subterms. A new macro set-inhibit-output-lst has been defined. This should be used when setting the state global inhibit-output-lst; *Note SET-INHIBIT-OUTPUT-LST:: and *Note PROOF-TREE::. The test for redundancy in definitions includes the guard and type declarations. *Note REDUNDANT-EVENTS::. *Note GENERALIZED-BOOLEANS:: for a discussion of a potential soundness problem for ACL2 related to the question: Which Common Lisp functions are known to return Boolean values? Here we will put some less important changes, additions, and so on. A bug has been fixed so that now, execution of :comp t (*Note COMP::) correctly handles non-standard characters. A bug in digit-char-p has been fixed, so that the "default" is nil rather than 0. True-listp now tests the final cdr against nil using eq instead of equal, for improved efficiency. The logical meaning is, however, unchanged. Put-assoc-equal has been added to the logic (it used to have :defun-mode :program, and has been documented.  File: acl2-doc-lemacs.info, Node: RULE-CLASSES, Next: THEORIES, Prev: RELEASE-NOTES, Up: Top RULE-CLASSES adding rules to the data base General Form: a true list of rule class objects as defined below Special Cases: a symbol abbreviating a single rule class object ACL2 provides users with the ability to create a number of different kinds of rules, including (conditional) rewrite rules but also including others. Don't be put off by the long description to follow; usually, you'll probably want to use rewrite rules. More on this below. A rule class object is either one of the :class keywords or else is a list of the form shown below. Those fields marked with "(!)" are required when the :class is as indicated. (:class :COROLLARY term :TRIGGER-FNS (fn1 ... fnk) ; provided :class = :META (!) :TRIGGER-TERMS (t1 ... tk) ; provided :class = :FORWARD-CHAINING ; or :class = :LINEAR :TYPE-SET n ; provided :class = :TYPE-SET-INVERTER :TYPED-TERM term ; provided :class = :TYPE-PRESCRIPTION :CLIQUE (fn1 ... fnk) ; provided :class = :DEFINITION (!) :CONTROLLER-ALIST alist ; provided :class = :DEFINITION (!) :LOOP-STOPPER alist ; provided :class = :REWRITE :PATTERN term ; provided :class = :INDUCTION (!) :CONDITION term ; provided :class = :INDUCTION :SCHEME term ; provided :class = :INDUCTION (!) :HINTS hints ; provided instrs = nil :INSTRUCTIONS instrs ; provided hints = nil :OTF-FLG flg) When rule class objects are provided by the user, most of the fields are optional and their values are computed in a context sensitive way. When a :class keyword is used as a rule class object, all relevant fields are determined contextually. Each rule class object in :rule-classes causes one or more rules to be added to the data base. The :class keywords are documented individually under the following names. Note that when one of these names is used as a :class, it is expected to be in the keyword package (i.e., the names below should be preceded by a colon but the ACL2 documentation facilities do not permit us to use keywords below). * Menu: * BUILT-IN-CLAUSES:: to build in a clause for measure and guard processing * COMPOUND-RECOGNIZER:: make a rule used by the typing mechanism * CONGRUENCE:: the relations to maintain while simplifying arguments * DEFINITION:: make a rule that acts like a function definition * ELIM:: make a destructor elimination rule * EQUIVALENCE:: mark a relation as an equivalence relation * FORWARD-CHAINING:: make a rule to forward chain when a certain trigger arises * GENERALIZE:: make a rule to restrict generalizations * INDUCTION:: make a rule that suggests a certain induction * LINEAR:: make some arithmetic inequality rules * LINEAR-ALIAS:: make a rule to extend the applicability of linear arithmetic * META:: make a :meta rule (a hand-written simplifier) * REFINEMENT:: record that one equivalence relation refines another * REWRITE:: make some :rewrite rules (possibly conditional ones) * TYPE-PRESCRIPTION:: make a rule that specifies the type of a term * TYPE-SET-INVERTER:: exhibit a new decoding for an ACL2 type-set * WELL-FOUNDED-RELATION:: show that a relation is well-founded on a set Before we get into the discussion of rule classes, let us return to an important point. In spite of the large variety of rule classes available, at present we recommend that new ACL2 users rely almost exclusively on (conditional) rewrite rules. A reasonable but slightly bolder approach is to use :type-prescription and :forward-chaining rules for "type-theoretic" rules, especially ones whose top-level function symbol is a common one like true-listp or consp; *Note TYPE-PRESCRIPTION:: and *Note FORWARD-CHAINING::. However, the rest of the rule classes are really not intended for widespread use, but rather are mainly for experts. We expect that we will write more about the question of which kind of rule to use. For now: when in doubt, use a :rewrite rule. :Rule-classes is an optional keyword argument of the defthm (and defaxiom) event. In the following, let name be the name of the event and let thm be the formula to be proved or added as an axiom. If :rule-classes is not specified in a defthm (or defaxiom) event, it is as though :rule-classes ((:rewrite)) had been used. Use :rule-classes nil to specify that no rules are to be generated. If :rule-classes class is specified, where class is a non-nil symbol, it is as though :rule-classes ((class)) had been used. Thus, :rule-classes :forward-chaining is equivalent to :rule-classes ((:forward-chaining)). We therefore now consider :rule-classes as a true list. If any element of that list is a keyword, replace it by the singleton list containing that keyword. Thus, :rule-classes (:rewrite :elim) is the same as :rule-classes ((:rewrite) (:elim)). Each element of the expanded value of :rule-classes must be a true list whose car is one of the rule class keyword tokens listed above, e.g., :rewrite, :elim, etc., and whose cdr is a "keyword alist" alternately listing keywords and values. The keywords in this alist must be taken from those shown below. They may be listed in any order and most may be omitted, as specified below. :Corollary -- its value, term, must be a term. If omitted, this field defaults to thm. The :corollary of a rule class object is the formula actually used to justify the rule created and thus determines the form of the rule. Nqthm provided no similar capability: each rule was determined by thm, the theorem or axiom added. ACL2 permits thm to be stated "elegantly" and then allows the :corollary of a rule class object to specify how that elegant statement is to be interpreted as a rule. For the rule class object to be well-formed, its (defaulted) :corollary, term, must follow from thm. Unless term is trivially implied by thm, using little more than propositional logic, the formula (implies thm term) is submitted to the theorem prover and the proof attempt must be successful. During that proof attempt the values of :hints, :instructions, and :otf-flg, as provided in the rule class object, are provided as arguments to the prover. Such auxiliary proofs give the sort of output that one expects from the prover. However, as noted above, corollaries that follow trivially are not submitted to the prover; thus, such corollaries cause no prover output. Note that before term is stored, all calls of macros in it are expanded away. *Note TRANS::. :Hints, :instructions, :otf-flg -- the values of these fields must satisfy the same restrictions placed on the fields of the same names in defthm. These values are passed to the recursive call of the prover used to establish that the :corollary of the rule class object follows from the theorem or axiom thm. :Type-set -- this field may be supplied only if the :class is :type-set-inverter. When provided, the value must be a type-set, an integer in a certain range. If not provided, an attempt is made to compute it from the corollary. *Note TYPE-SET-INVERTER::. :Typed-term -- this field may be supplied only if the :class is :type-prescription. When provided, the value is the term for which the :corollary is a type-prescription lemma. If no :typed-term is provided in a :type-prescription rule class object, we try to compute heuristically an acceptable term. *Note TYPE-PRESCRIPTION::. :Trigger-terms -- this field may be supplied only if the :class is :forward-chaining or :linear. When provided, the value is a list of terms, each of which is to trigger the attempted application of the rule. If no :trigger-terms is provided, we attempt to compute heuristically an appropriate set of triggers. *Note FORWARD-CHAINING:: or *Note LINEAR::. :Trigger-fns -- this field must (and may only) be supplied if the :class is :meta. Its value must be a list of function symbols. Terms with these symbols trigger the application of the rule. *Note META::. :Clique and :controller-alist -- these two fields must (and may only) be supplied if the :class is :definition. Suppose the :corollary of the rule is (implies hyp (equiv (fn a1 ... an) body)). The value of the :clique field should be a true list of function symbols, and if non-nil must include fn. These symbols are all the members of the mutually recursive clique containing this definition of fn. That is, a call of any function in :clique is considered a "recursive call" for purposes of the expansion heuristics. The value of the :controller-alist field should be an alist that maps each function symbol in the :clique to a list of t's and nil's of length equal to the arity of the function. For example, if :clique consists of just two symbols, fn1 and fn2, of arities 2 and 3 respectively, then ((fn1 t nil) (fn2 nil t t)) is a legal value of :controller-alist. The value associated with a function symbol in this alist is a "mask" specifying which argument slots of the function "control" the recursion for heuristic purposes. Sloppy choice of :clique or :controller-alist can result in infinite expansion and stack overflow. :loop-stopper -- this field may only be supplied if the class is :rewrite. Its value must be a list of entries each consisting of two variables followed by a (possibly empty) list of functions, for example ((x y binary-+) (u v foo bar)). It will be used to restrict application of rewrite rules by requiring that the list of instances of the second variables must be "smaller" than the list of instances of the first variables in a sense related to the corresponding functions listed; *Note LOOP-STOPPER::. The list as a whole is allowed to be nil, indicating that no such restriction shall be made. Note that any such entry that contains a variable not being instantiated, i.e., not occurring on the left side of the rewrite rule, will be ignored. However, for simplicity we merely require that every variable mentioned should appear somewhere in the corresponding :corollary formula. :pattern, :condition, :scheme -- the first and last of these fields must (and may only) be supplied if the class is :induction. :Condition is optional but may only be supplied if the class is :induction. The values must all be terms and indicate, respectively, the pattern to which a new induction scheme is to be attached, the condition under which the suggestion is to be made, and a term which suggests the new scheme. *Note INDUCTION::. Once thm has been proved (in the case of defthm) and each rule class object has been checked for well-formedness (which might require additional proofs), we consider each rule class object in turn to generate and add rules. Let :class be the class keyword token of the ith class object (counting from left to right). Generate the rune (:class name . x), where x is nil if there is only one class and otherwise x is i. Then, from the :corollary of that object, generate one or more rules, each of which has the name (:class name . x). See the :doc entry for each rule class to see how formulas determine rules. Note that it is in principle possible for several rules to share the same name; it happens whenever a :corollary determines more than one rule. This in fact only occurs for :rewrite, :linear, and :forward-chaining class rules and only then if the :corollary is essentially a conjunction. (See the documentation for rewrite, linear, or forward-chaining for details.)  File: acl2-doc-lemacs.info, Node: BUILT-IN-CLAUSES, Next: COMPOUND-RECOGNIZER, Prev: RULE-CLASSES, Up: RULE-CLASSES BUILT-IN-CLAUSES to build in a clause for measure and guard processing *Note RULE-CLASSES:: for a general discussion of rule classes and how they are used to build rules from formulas. A :built-in-clause rule can be built from any formula other than propositional tautologies. Roughly speaking, the system uses the list of built-in clauses as the first method of proof when attacking a new goal. Any goal that is subsumed by a built in clause is proved "silently." ACL2 maintains a set of "built-in" clauses that are used to short-circuit certain theorem proving tasks. We discuss this at length below. When a theorem is given the rule class :built-in-clause ACL2 flattens the implies and and structure of the :corollary formula so as to obtain a set of formulas whose conjunction is equivalent to the given corollary. It then converts each of these to clausal form and adds each clause to the set of built-in clauses. For example, the following :corollary (regardless of the definition of abl) (and (implies (and (true-listp x) (not (equal x nil))) (< (acl2-count (abl x)) (acl2-count x))) (implies (and (true-listp x) (not (equal nil x))) (< (acl2-count (abl x)) (acl2-count x)))) will build in two clauses, {(not (true-listp x)) (equal x nil) (< (acl2-count (abl x)) (acl2-count x))} and {(not (true-listp x)) (equal nil x) (< (acl2-count (abl x)) (acl2-count x))}. We now give more background. Recall that a clause is a set of terms, implicitly representing the disjunction of the terms. Clause c1 is "subsumed" by clause c2 if some instance of c2 is a subset c1. For example, let c1 be {(not (consp l)) (equal a (car l)) (< (acl2-count (cdr l)) (acl2-count l))}. Then c1 is subsumed by c2, shown below, {(not (consp x)) ; second term omitted here (< (acl2-count (cdr x)) (acl2-count x))} because we can instantiate x in c2 with l to obtain a subset of c1. Observe that c1 is the clausal form of (implies (and (consp l) (not (equal a (car l)))) (< (acl2-count (cdr l)) (acl2-count l))), c2 is the clausal form of (implies (consp l) (< (acl2-count (cdr l)) (acl2-count l))) and the subsumption property just means that c1 follows trivially from c2 by instantiation. The set of built-in clauses is just a set of known theorems in clausal form. Any formula that is subsumed by a built-in clause is thus a theorem. If the set of built-in theorems is reasonably small, this little theorem prover is fast. ACL2 uses the "built-in clause check" in three places: at the entrance to the general-purpose theorem prover, as a filter on the clauses generated to prove the termination of recursively defun'd functions and as a filter on the clauses generated to verify the guards of a function. The latter two uses are the ones that most often motivate an extension to the set of built-in clauses. Frequently a given formalization problem requires the definition of many functions which require virtually identical termination and/or guard proofs. These proofs can be short-circuited by extending the set of built-in clauses to contain the most general forms of the clauses generated by the definitional schemes in use. The attentive user might have noticed that there are some recursive schemes, e.g., recursion by cdr after testing consp, that ACL2 just seems to "know" are ok, while for others it generates measure clauses to prove. Actually, it always generates measure clauses but then filters out any that pass the built-in clause check. When ACL2 is initialized, the clause justifying cdr recursion after a consp test is added to the set of built-in clauses. (That clause is c2 above.) Note that only a subsumptin check is made; no rewriting or simplification is done. Thus, if we want the system to "know" that cdr recursion is ok after a negative atom test (which, by the definition of atom, is the same as a consp test), we have to build in a second clause. The subsumption algorithm does not "know" about commutative functions. Thus, for predictability, we have built in commuted versions of each clause involving commutative functions. For example, we build in both {(not (integerp x)) (< 0 x) (= x 0) (< (acl2-count (+ -1 x)) (acl2-count x))} and the commuted version {(not (integerp x)) (< 0 x) (= 0 x) (< (acl2-count (+ -1 x)) (acl2-count x))} so that the user need not worry whether to write (= x 0) or (= 0 x) in definitions. :built-in-clause rules added by the user can be enabled and disabled.  File: acl2-doc-lemacs.info, Node: COMPOUND-RECOGNIZER, Next: CONGRUENCE, Prev: BUILT-IN-CLAUSES, Up: RULE-CLASSES COMPOUND-RECOGNIZER make a rule used by the typing mechanism *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 :compound-recognizer rule might be built is: Example: (implies (alistp x) When (alistp x) is assumed true, (true-listp x)) add the additional hypothesis that x is of primitive type true-listp. General Forms: (implies (fn x) concl) (implies (not (fn x)) concl) (and (implies (fn x) concl1) (implies (not (fn x)) concl2)) (iff (fn x) concl) (equal (fn x) concl) where fn is a Boolean valued function of one argument, x is a variable symbol, and the system can deduce some restriction on the primitive type of x from the assumption that concl holds. The third restriction is vague but one way to understand it is to weaken it a little to "and concl is a non-tautological conjunction or disjunction of the primitive type recognizers listed below." The primitive ACL2 types and a suitable primitive recognizing expression for each are listed below. type suitable primitive recognizer zero (equal x 0) negative integers (and (integerp x) (< x 0)) positive integers (and (integerp x) (> x 0)) negative ratio (and (rationalp x) (not (integerp x)) (< x 0)) positive ratio (and (rationalp x) (not (integerp x)) (> x 0)) complex rational (complex-rationalp x) nil (equal x nil) t (equal x t) other symbols (and (symbolp x) (not (equal x nil)) (not (equal x t))) proper conses (and (consp x) (true-listp x)) improper conses (and (consp x) (not (true-listp x))) strings (stringp x) characters (characterp x) Thus, a suitable concl to recognize the naturals would be (or (equal x 0) (and (integerp x) (> x 0))) but it turns out that we also permit (and (integerp x) (>= x 0)). Similarly, the true-lists could be specified by (or (equal x nil) (and (consp x) (true-listp x))) but we in fact allow (true-listp x). When time permits we will document more fully what is allowed or implement a macro that permits direct specification of the desired type in terms of the primitives. There are essentially four forms of :compound-recognizer rules, the last two general forms above being equivalent. We explain how such rules are used by considering the individual forms. Consider a rule of the first form, (implies (fn x) concl). The effect of such a rule is that when the rewriter assumes (fn x) true, as it would while diving through (if (fn x) xxx ...) to rewrite xxx, it restricts the type of x as specified by concl. However, when assuming (fn x) false, as necessary in (if (fn x) ... xxx), the rule permits no additional assumptions about the type of x. For example, if fn is primep, i.e., the predicate that recognizes prime numbers, then (implies (primep x) (and (integerp x) (>= x 0))) is a compound recognizer rule of the first form. When (primep x) is assumed true, the rewriter gains the additional information that x is a natural number. When (primep x) is assumed false, no additional information is gained -- since x may be a non-prime natural or may not even be a natural. The second general form addresses itself to the symmetric case, when assuming (fn x) false permits type restrictions on x but assuming (fn x) true permits no such restrictions. For example, if we defined exprp to be the recognizer for well-formed expressions for some language in which all symbols, numbers, character objects and strings were well-formed -- e.g., the well-formedness rules only put restrictions on expressions represented by consps -- then the theorem (implies (not (exprp x)) (consp x)) is a rule of the second form. Assuming (exprp x) true tells us nothing about the type of x; assuming it false tells us x is a consp. The third general form addresses itself to the case where one type may be deduced from (fn x) and a generally unrelated type may be deduced from its negation. If we modified the expression recognizer above so that character objects are illegal, then a rule of the third form is (and (implies (exprp x) (not (characterp x))) (implies (not (exprp x)) (or (consp x) (characterp x)))). Finally, rules of the fourth class address the case where fn recognizes all and only the objects whose type is described. In this case, fn is really just a new name for some "compound recognizers." The classic example is (booleanp x), which is just a handy combination of two primitive types: (iff (booleanp x) (or (equal x t) (equal x nil))). Often it is best to disable fn after proving that it is a compound recognizer, since (fn x) will not be recognized as a compound recognizer once it has been expanded. Every time you prove a new compound recognizer rule about fn it overrides all previously proved compound recognizer rules about fn. Thus, if you want to establish the type implied by (fn x) and you want to establish the type implied by (not (fn x)), you must prove a compound recognizer rule of the third or fourth forms. Proving a rule of the first form followed by one of the second only leaves the second fact in the data base. Compound recognizer rules can be disabled with the effect that older rules about fn, if any, are exposed. If you prove multiple compound recognizer rules for a function, you may see a *warning* message to the effect that the new rule is not as "restrictive" as the old. That is, the new rules do not give the rewriter strictly more type information than it already had. The new rule is stored anyway, overriding the old, if enabled. You may be playing subtle games with enabling or rewriting. But two other interpretions are more likely, we think. One is that you have forgotten about an earlier rule and should merely print it out to make sure it says what you know and then forget your new rule. The other is that you meant to give the system more information and the system has simply been unable to extract the intended type information from the term you placed in the conclusion of the new rule. Given our lack of specificity in saying how type information is extracted from rules, you can hardly blame yourself for this problem. Sorry. If you suspect you've been burned this way, you should rephrase the new rule in terms of the primitive recognizing expressions above and see if the warning is still given. It would also be helpful to let us see your example so we can consider it as we redesign this stuff. Compound recognizer rules are similar to :forward-chaining rules in that the system deduces new information from the act of assuming something true or false. If a compound recognizer rule were stored as a forward chaining rule it would have essentially the same effect as described, when it has any effect at all. The important point is that :forward-chaining rules, because of their more general and expensive form, are used "at the top level" of the simplification process: we forward chain from assumptions in the goal being proved. But compound recognizer rules are built in at the bottom-most level of the simplifier, where type reasoning is done. All that said, compound recognizer rules are a rather fancy, specialized mechanism. It may be more appropriate to create :forward-chaining rules instead of :compound-recognizer rules.  File: acl2-doc-lemacs.info, Node: CONGRUENCE, Next: DEFINITION, Prev: COMPOUND-RECOGNIZER, Up: RULE-CLASSES CONGRUENCE the relations to maintain while simplifying arguments *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 :congruence rule might be built is: Example: (implies (set-equal x y) (iff (memb e x) (memb e y))). Also *Note DEFCONG:: and *Note EQUIVALENCE::. General Form: (implies (equiv1 xk xk-equiv) (equiv2 (fn x1... xk ...xn) (fn x1... xk-equiv ...xn))) where equiv1 and equiv2 are known equivalence relations, fn is an n-ary function symbol and the xi and xk-equiv are all distinct variables. The effect of such a rule is to record that the equiv2-equivalence of fn-expressions can be maintained if, while rewriting the kth argument position, equiv1-equivalence is maintained. *Note EQUIVALENCE:: for a general discussion of the issues. We say that equiv2, above, is the "outside equivalence" in the rule and equiv1 is the "inside equivalence for the kth argument" The macro form (defcong equiv1 equiv2 (fn x1 ... x1) k) is an abbreviation for a defthm of rule-class :congruence that attempts to establish that equiv2 is maintained by maintaining equiv1 in fn's kth argument. The defcong macro automatically generates the general formula shown above. *Note DEFCONG::. The memb example above tells us that (memb e x) is propositionally equivalent to (memb e y), provided x and y are set-equal. The outside equivalence is iff and the inside equivalence for the second argument is set-equal. If we see a memb expression in a propositional context, e.g., as a literal of a clause or test of an if (but not, for example, as an argument to cons), we can rewrite its second argument maintaining set-equality. For example, a rule stating the commutativity of append (modulo set-equality) could be applied in this context. Since equality is a refinement of all equivalence relations, all equality rules are always available. *Note REFINEMENT::. All known :congruence rules about a given outside equivalence and fn can be used independently. That is, consider two :congruence rules with the same outside equivalence, equiv, and about the same function fn. Suppose one says that equiv1 is the inside equivalence for the first argument and the other says equiv2 is the inside equivalence for the second argument. Then (fn a b) is equiv (fn a' b') provided a is equiv1 to a' and b is equiv2 to b'. This is an easy consequence of the transitivity of equiv. It permits you to think independently about the inside equivalences. Furthermore, it is possible that more than one inside equivalence for a given argument slot will maintain a given outside equivalence. For example, (length a) is equal to (length a') if a and a' are related either by list-equal or by string-equal. You may prove two (or more) :congruence rules for the same slot of a function. The result is that the system uses a new, "generated" equivalence relation for that slot with the result that rules of both (or all) kinds are available while rewriting. :congruence rules can be disabled. For example, if you have two different inside equivalences for a given argument position and you find that the :rewrite rules for one are unexpectedly preventing the application of the desired rule, you can disable the rule that introduced the unwanted inside equivalence. More will be written about this as we develop the techniques.