Info file: acl2-doc-emacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-emacs.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-emacs.info, Node: AREF1, Next: AREF2, Prev: ARRAYS, Up: ARRAYS AREF1 access the elements of a 1-dimensional array Example Form: (aref1 'delta1 a (+ i k)) General Form: (aref1 name alist index) where name is a symbol, alist is a 1-dimensional array and index is a legal index into alist. This function returns the value associated with index in alist, or else the default value of the array. See *Note ARRAYS:: for details. This function executes in virtually constant time if alist is in fact the "semantic value" associated with name (see *Note ARRAYS::). When it is not, aref1 must do a linear search through alist. In that case the correct answer is returned but a *slow array* comment is printed to the comment window. See *Note SLOW-ARRAY-WARNING::.  File: acl2-doc-emacs.info, Node: AREF2, Next: ARRAY1P, Prev: AREF1, Up: ARRAYS AREF2 access the elements of a 2-dimensional array Example Form: (aref2 'delta1 a i j) General Form: (aref2 name alist i j) where name is a symbol, alist is a 2-dimensional array and i and j are legal indices into alist. This function returns the value associated with (i . j) in alist, or else the default value of the array. See *Note ARRAYS:: for details. This function executes in virtually constant time if alist is in fact the "semantic value" associated with name (see *Note ARRAYS::). When it is not, aref2 must do a linear search through alist. In that case the correct answer is returned but a *slow array* comment is printed to the comment window. See *Note SLOW-ARRAY-WARNING::.  File: acl2-doc-emacs.info, Node: ARRAY1P, Next: ARRAY2P, Prev: AREF2, Up: ARRAYS ARRAY1P recognize a 1-dimensional array Example Form: (array1p 'delta1 a) General Form: (array1p name alist) where name and alist are arbitrary objects. This function returns t if alist is a 1-dimensional ACL2 array. Otherwise it returns nil. The function operates in constant time if alist is the semantic value of name. See *Note ARRAYS::.  File: acl2-doc-emacs.info, Node: ARRAY2P, Next: ASET1, Prev: ARRAY1P, Up: ARRAYS ARRAY2P recognize a 2-dimensional array Example Form: (array2p 'delta1 a) General Form: (array2p name alist) where name and alist are arbitrary objects. This function returns t if alist is a 2-dimensional ACL2 array. Otherwise it returns nil. The function operates in constant time if alist is the semantic value of name. See *Note ARRAYS::.  File: acl2-doc-emacs.info, Node: ASET1, Next: ASET2, Prev: ARRAY2P, Up: ARRAYS ASET1 set the elements of a 1-dimensional array Example Form: (aset1 'delta1 a (+ i k) 27) General Form: (aset1 name alist index val) where name is a symbol, alist is a 1-dimensional array named name, index is a legal index into alist, and val is an arbitrary object. See *Note ARRAYS:: for details. Roughly speaking this function "modifies" alist so that the value associated with index is val. More precisely, it returns a new array, alist', of the same name and dimension as alist that, under aref1, is everywhere equal to alist except at index where the result is val. That is, (aref1 name alist' i) is (aref1 name alist i) for all legal indices i except index, where (aref1 name alist' i) is val. In order to "modify" alist, aset1 conses a new pair onto the front. If the length of the resulting alist exceeds the :maximum-length entry in the array header, aset1 compresses the array as with compress1. It is generally expected that the "semantic value" of name will be alist (see *Note ARRAYS::). This function operates in virtually constant time whether this condition is true or not (unless the compress1 operation is required). But the value returned by this function cannot be used efficiently by subsequent aset1 operations unless alist is the semantic value of name when aset1 is executed. Thus, if the condition is not true, aset1 prints a *slow array* warning to the comment window. See *Note SLOW-ARRAY-WARNING::.  File: acl2-doc-emacs.info, Node: ASET2, Next: COMPRESS1, Prev: ASET1, Up: ARRAYS ASET2 set the elements of a 2-dimensional array Example Form: (aset2 'delta1 a i j 27) General Form: (aset2 name alist i j val) where name is a symbol, alist is a 2-dimensional array named name, i and j are legal indices into alist, and val is an arbitrary object. See *Note ARRAYS:: for details. Roughly speaking this function "modifies" alist so that the value associated with (i . j) is val. More precisely, it returns a new array, alist', of the same name and dimension as alist that, under aref2, is everywhere equal to alist except at (i . j) where the result is val. That is, (aref2 name alist' x y) is (aref2 name alist x y) for all legal indices x y except i and j where (aref2 name alist' i j) is val. In order to "modify" alist, aset2 conses a new pair onto the front. If the length of the resulting alist exceeds the :maximum-length entry in the array header, aset2 compresses the array as with compress2. It is generally expected that the "semantic value" of name will be alist (see *Note ARRAYS::). This function operates in virtually constant time whether this condition is true or not (unless the compress2 operation is required). But the value returned by this function cannot be used efficiently by subsequent aset2 operations unless alist is the semantic value of name when aset2 is executed. Thus, if the condition is not true, aset2 prints a *slow array* warning to the comment window. See *Note SLOW-ARRAY-WARNING::.  File: acl2-doc-emacs.info, Node: COMPRESS1, Next: COMPRESS2, Prev: ASET2, Up: ARRAYS COMPRESS1 remove irrelevant pairs from a 1-dimensional array Example Form: (compress1 'delta1 a) General Form: (compress1 name alist) where name is a symbol and alist is a 1-dimensional array named name. See *Note ARRAYS:: for details. Logically speaking, this function removes irrelevant pairs from alist, possibly shortening it. The function returns a new array, alist', of the same name and dimension as alist, that, under aref1, is everywhere equal to alist. That is, (aref1 name alist' i) is (aref1 name alist i), for all legal indices i. Alist' may be shorter than alist and the non-irrelevant pairs may occur in a different order than in alist. Practically speaking, this function plays an important role in the efficient implementation of aref1. In addition to creating the new array, alist', compress1 makes that array the "semantic value" of name and allocates a raw lisp array to name. For each legal index, i, that raw lisp array contains (aref1 name alist' i) in slot i. Thus, subsequent aref1 operations can be executed in virtually constant time provided they are given name and the alist' returned by the most recently executed compress1 or aset1 on name. See *Note ARRAYS::.  File: acl2-doc-emacs.info, Node: COMPRESS2, Next: DEFAULT, Prev: COMPRESS1, Up: ARRAYS COMPRESS2 remove irrelevant pairs from a 2-dimensional array Example Form: (compress2 'delta1 a) General Form: (compress2 name alist) where name is a symbol and alist is a 2-dimensional array named name. See *Note ARRAYS:: for details. Logically speaking, this function removes irrelevant pairs from alist, possibly shortening it. The function returns a new array, alist', of the same name and dimension as alist, that, under aref2, is everywhere equal to alist. That is, (aref2 name alist' i j) is (aref2 name alist i j), for all legal indices i and j. Alist' may be shorter than alist and the non-irrelevant pairs may occur in a different order in alist' than in alist. Practically speaking, this function plays an important role in the efficient implementation of aref2. In addition to creating the new array, alist', compress2 makes that array the "semantic value" of name and allocates a raw lisp array to name. For all legal indices, i and j, that raw lisp array contains (aref2 name alist' i j) in slot i,j. Thus, subsequent aref2 operations can be executed in virtually constant time provided they are given name and the alist' returned by the most recently executed compress2 or aset2 on name. See *Note ARRAYS::.  File: acl2-doc-emacs.info, Node: DEFAULT, Next: DIMENSIONS, Prev: COMPRESS2, Up: ARRAYS DEFAULT return the :default from the header of a 1- or 2-dimensional array Example Form: (default 'delta1 a) General Form: (default name alist) where name is an arbitrary object and alist is a 1- or 2-dimensional array. This function returns the contents of the :default field of the header of alist. When aref1 or aref2 is used to obtain a value for an index (or index pair) not bound in alist, the default value is returned instead. Thus, the array alist may be thought of as having been initialized with the default value. default operates in virtually constant time if alist is the semantic value of name. See *Note ARRAYS::.  File: acl2-doc-emacs.info, Node: DIMENSIONS, Next: HEADER, Prev: DEFAULT, Up: ARRAYS DIMENSIONS return the :dimensions from the header of a 1- or 2-dimensional array Example Form: (dimensions 'delta1 a) General Form: (dimensions name alist) where name is arbitrary and alist is a 1- or 2-dimensional array. This function returns the dimensions list of the array alist. That list will either be of the form (dim1) or (dim1 dim2), depending on whether alist is a 1- or 2-dimensional array. Dim1 and dim2 will be integers and each exceed by 1 the maximum legal corresponding index. Thus, if dimensions returns, say, '(100) for an array a named 'delta1, then (aref1 'delta1 a 99) is legal but (aref1 'delta1 a 100) violates the guards on aref1. Dimensions operates in virtually constant time if alist is the semantic value of name. See *Note ARRAYS::.  File: acl2-doc-emacs.info, Node: HEADER, Next: MAXIMUM-LENGTH, Prev: DIMENSIONS, Up: ARRAYS HEADER return the header of a 1- or 2-dimensional array Example Form: (header 'delta1 a) General Form: (header name alist) where name is arbitrary and alist is a 1- or 2-dimensional array. This function returns the header of the array alist. The function operates in virtually constant time if alist is the semantic value of name. See *Note ARRAYS::.  File: acl2-doc-emacs.info, Node: MAXIMUM-LENGTH, Next: SLOW-ARRAY-WARNING, Prev: HEADER, Up: ARRAYS MAXIMUM-LENGTH return the :maximum-length from the header of an array Example Form: (maximum-length 'delta1 a) General Form: (maximum-length name alist) where name is an arbitrary object and alist is a 1- or 2-dimensional array. This function returns the contents of the :maximum-length field of the header of alist. Whenever an aset1 or aset2 would cause the length of the alist to exceed its maximum length, a compress1 or compress2 is done automatically to remove irrelevant pairs from the array. Maximum-length operates in virtually constant time if alist is the semantic value of name. See *Note ARRAYS::.  File: acl2-doc-emacs.info, Node: SLOW-ARRAY-WARNING, Prev: MAXIMUM-LENGTH, Up: ARRAYS SLOW-ARRAY-WARNING a warning issued when arrays are used inefficiently If you use ACL2 arrays you may sometimes see a *slow array* warning. We here explain what that warning means and some likely "mistakes" it may signify. The discussion in the documentation for arrays defines what we mean by the semantic value of a name. As noted there, behind the scenes ACL2 maintains the invariant that with some names there is associated a pair consisting of an ACL2 array alist, called the semantic value of the name, and an equivalent raw lisp array. Access to ACL2 array elements, as in (aref1 name alist i), is executed in constant time when the array alist is the semantic value of the name, because we can just use the corresponding raw lisp array to obtain the answer. Aset1 and compress1 modify the raw lisp array appropriately to maintain the invariant. If aref1 is called on a name and alist, and the alist is not the then-current semantic value of the name, the correct result is computed but it requires linear time because the alist must be searched. When this happens, aref1 prints a *slow array* warning message to the comment window. Aset1 behaves similarly because the array it returns will cause the *slow array* warning every time it is used. From the purely logical perspective there is nothing "wrong" about such use of arrays and it may be spurious to print a warning message. But because arrays are generally used to achieve efficiency, the *slow array* warning often means the user's intentions are not being realized. Sometimes merely performance expectations are not met; but the message may mean that the functional behavior of the program is different than intended. Here are some "mistakes" that might cause this behavior. In the following we suppose the message was printed by aset1 about an array named name. Suppose the alist supplied aset1 is alist. (1) Compress1 was never called on name and alist. That is, perhaps you created an alist that is an array1p and then proceeded to access it with aref1 but never gave ACL2 the chance to create a raw lisp array for it. After creating an alist that is intended for use as an array, you must do (compress1 name alist) and pass the resulting alist' as the array. (2) Name is misspelled. Perhaps the array was compressed under the name 'delta-1 but accessed under 'delta1? (3) An aset1 was done to modify alist, producing a new array, alist', but you subsequently used alist as an array. Inspect all (aset1 name ...) occurrences and make sure that the alist modified is never used subsequently (either in that function or any other). It is good practice to adopt the following syntactic style. Suppose the alist you are manipulating is the value of the local variable alist. Suppose at some point in a function definition you wish to modify alist with aset1. Then write (let ((alist (aset1 name alist i val))) ...) and make sure that the subsequent function body is entirely within the scope of the let. Any uses of alist subsequently will refer to the new alist and it is impossible to refer to the old alist. Note that if you write (foo (let ((alist (aset1 name alist i val))) ...) ; arg 1 (bar alist)) ; arg 2 you have broken the rules, because in arg 1 you have modified alist but in arg 2 you refer to the old value. An appropriate rewriting is to lift the let out: (let ((alist (aset1 name alist alist i val))) (foo ... ; arg 1 (bar alist))) ; arg 2 Of course, this may not mean the same thing. (4) A function which takes alist as an argument and modifies it with aset1 fails to return the modified version. This is really the same as (3) above, but focuses on function interfaces. If a function takes an array alist as an argument and the function uses aset1 (or a subfunction uses aset1, etc.), then the function probably "ought" to return the result produced by aset1. The reasoning is as follows. If the array is passed into the function, then the caller is holding the array. After the function modifies it, the caller's version of the array is obsolete. If the caller is going to make further use of the array, it must obtain the latest version, i.e., that produced by the function.  File: acl2-doc-emacs.info, Node: BIBLIOGRAPHY, Next: BREAKS, Prev: ARRAYS, Up: MISCELLANEOUS BIBLIOGRAPHY reports about ACL2 Below is a list of notes and reports pertaining to ACL2. [km94] M. Kaufmann and J S. Moore. Design Goals for ACL2, CLI Technical Report 101, August 1994. See reports/km94.ps. (Written about a year before ACL2 was first released, this document is now somewhat dated but does provide some perspective on the system, especially with respect to Nqthm.) [bkm96] B. Brock, M. Kaufmann, and J S. Moore. ACL2 Theorems about Commercial Microprocessors. CLI Technical Report 117. August, 1996. See reports/bkm96.ps. (An overview of ACL2 and its use in two commercial projects, the Motorola CAP chip and the AMD5K86 floating-point division.) [km97] M. Kaufmann and J S. Moore. An Industrial Strength Theorem Prover for a Logic Based on Common Lisp, IEEE TSE (to appear, 1997) (An early version appeared as "ACL2: An Industrial Strength Version of Nqthm," in the Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS-96), IEEE Computer Society Press, June, 1996, pp 23-34. See reports/km97.ps. (An explanation of our treatment of guards, why we choose to make logical functions total and how guards allow us to compute them via Common Lisp's partial functions.) [km97a] M. Kaufmann and J S. Moore. A Precise Description of the ACL2 Logic. See reports/km97a.ps. (The most complete description of the ACL2 logic available. This is a dry mathematical document describing the base logic -- not the theorem prover or the system -- from first principles. It is a working draft. At the moment it does not include multiple values, property lists, arrays, or STATE.) [y96a] W. D. Young. Interactive Consistency in ACL2. CLI Technical Report 116. January, 1996 (essentially the same as Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS-96), IEEE Computer Society Press, June, 1996, pp 35-45). See reports/y96a.ps. An ACL2 formalization of Rushby's improvement to Bevier and Young's Nqthm formalization of Pease, Shostak and Lamport's Oral Messages ("Byzantine Generals) algorithm. [y96b] W. D. Young. The Specification of a Simple Autopilot in ACL2. CLI Internal Note 327. July, 1996. See reports/y96b.ps. An ACL2 treatment of Butler's autopilot example. [bm96] R. S. Boyer and J S. Moore. Mechanized Formal Reasoning about Programs and Computing Machines. CLI Technical Report 119. August, 1996. See reports/bm96.ps. An explanation of how programming languages and computing machines are formalized in ACL2 in a way that enables mechanized reasoning and which has been shown to "scale up." M. Kaufmann. High-level Correctness of ACL2: A Story. See reports/story.txt. An explanation of the logical meaning of ACL2's "worlds" with particular attention paid to the semantics of encapsulation and local events.  File: acl2-doc-emacs.info, Node: BREAKS, Next: CHECK-SUM, Prev: BIBLIOGRAPHY, Up: MISCELLANEOUS BREAKS Common Lisp breaks Example: Broken at PROVE. Type :H for Help. >>:Q ACL2 !> If a break occurs, e.g. because of a bug in ACL2 or a user interrupt, the break will run a Common Lisp read-eval-print loop, not an ACL2 read-eval-print loop. This may not be obvious if the prompts in the two loops are similar. Because you are typing to a Common Lisp evaluator, you must be careful. It is possible to damage your ACL2 state in irreparable ways by executing non-ACL2 Common Lisp. It is even possible to disrupt and render inaccurate the interrupted evaluation of a simple ACL2 expression. Quitting from the break (as with :q in AKCL) will return to the innermost ACL2 read-eval-print loop. Before the loop is continued, any pending cleanup forms from acl2-unwind-protects are evaluated (unless acl2::*acl2-panic-exit-flg* is non-nil, in which case no cleanup is done). If at any time you type the token #. to either a raw lisp break or to the ACL2 read-eval-print loop, an abort is executed. Control is passed to the outermost ACL2 read-eval-print loop (lp). Again, unwind-protection cleanup forms are executed first.  File: acl2-doc-emacs.info, Node: CHECK-SUM, Next: CLAUSE-IDENTIFIER, Prev: BREAKS, Up: MISCELLANEOUS CHECK-SUM assigning "often unique" integers to files and objects A "check sum" is an integer in some fixed range computed from the printed representation of an object, e.g., the sum, modulo 2**32, of the ascii codes of all the characters in the printed representation. Ideally, you would like the check sum of an object to be uniquely associated with that object, like a fingerprint. It could then be used as a convenient way to recognize the object in the future: you could remember the check sum (which is relatively small) and when an object is presented to you and alleged to be the special one you could compute its check sum and see if indeed it was. Alas, there are many more objects than check sums (after all, each check sum is an object, and then there's t). So you try to design a check sum algorithm that maps similar looking objects far apart, in the hopes that corruptions and counterfeits -- which appear to be similar to the object -- have different check sums. Nevertheless, the best you can do is a many-to-one map. If an object with a different check sum is presented, you can be positive it is not the special object. But if an object with the same check sum is presented, you have no grounds for positive identification. The basic check sum algorithm in ACL2 is called check-sum-obj, which computes the check sum of an ACL2 object. Roughly speaking, we scan the print representation of the object and, for each character encountered, we multiply the ascii code of the character times its position in the stream (modulo a certain prime) and then add (modulo a certain prime) that into the running sum. This is inaccurate in many senses (for example, we don't always use the ascii code and we see numbers as though they were printed in base 127) but indicates the basic idea. ACL2 uses check sums to increase security in the books mechanism; see *Note CERTIFICATE::.  File: acl2-doc-emacs.info, Node: CLAUSE-IDENTIFIER, Next: COMMAND, Prev: CHECK-SUM, Up: MISCELLANEOUS CLAUSE-IDENTIFIER the internal form of a goal-spec To each goal-spec, str, there corresponds a clause-identifier produced by (parse-clause-id str). For example, (parse-clause-id "[2]Subgoal *4.5.6/7.8.9"'") returns ((2 4 5 6) (7 8 9) . 3). The function string-for-tilde-@-clause-id-phrase inverts parse-clause-id in the sense that given a clause identifier it returns the corresponding goal-spec. As noted in the documentation for goal-spec, each clause printed in the theorem prover's proof attempt is identified by a name. When these names are represented as strings they are called "goal specs." Such strings are used to specify where in the proof attempt a given hint is to be applied. The function parse-clause-id converts goal-specs into clause identifiers, which are cons-trees containing natural numbers. Examples of goal-specs and their corresponding clause identifiers are shown below. parse-clause-id --> "Goal" ((0) NIL . 0) "Subgoal 3.2.1'" ((0) (3 2 1) . 1) "[2]Subgoal *4.5.6/7.8.9"'" ((2 4 5 6) (7 8 9) . 3) <-- string-for-tilde-@-clause-id-phrase The caar of a clause id specifies the forcing round, the cdar specifies the goal being proved by induction, the cadr specifies the particular subgoal, and the cddr is the number of primes in that subgoal. Internally, the system maintains clause ids, not goal-specs. The system prints clause ids in the form shown by goal-specs. When a goal-spec is used in a hint, it is parsed (before the proof attempt begins) into a clause id. During the proof attempt, the system watches for the clause id and uses the corresponding hint when the id arises. (Because of the expense of creating and garbage collecting a lot of strings, this design is more efficient than the alternative.)  File: acl2-doc-emacs.info, Node: COMMAND, Next: COMMAND-DESCRIPTOR, Prev: CLAUSE-IDENTIFIER, Up: MISCELLANEOUS COMMAND forms you type at the top-level, but... ...the word "command" usually refers to a top-level form whose evaluation produces a new logical world. Typical commands are: (defun foo (x) (cons x x)) (defthm consp-foo (consp (foo x))) (defrec pair (hd . tl) nil) The first two forms are examples of commands that are in fact primitive events. See *Note EVENTS::. defrec, on the other hand, is a macro that expands into a progn of several primitive events. In general, a world extending command generates one or more events. Both events and commands leave landmarks on the world that enable us to determine how the given world was created from the previous one. Most of your interactions will occur at the command level, i.e., you type commands, you print previous commands, and you undo back through commands. Commands are denoted by command descriptors. See *Note COMMAND-DESCRIPTOR::.  File: acl2-doc-emacs.info, Node: COMMAND-DESCRIPTOR, Next: COMPUTED-HINTS, Prev: COMMAND, Up: MISCELLANEOUS COMMAND-DESCRIPTOR an object describing a particular command typed by the user Examples: :max ; the command most recently typed by the user :x ; synonymous with :max (:x -1) ; the command before the most recent one (:x -2) ; the command before that :x-2 ; synonymous with (:x -2) 5 ; the fifth command typed by the user 1 ; the first command typed by the user 0 ; the last command of the system initialization -1 ; the next-to-last initialization command :min ; the first command of the initialization fn ; the command that introduced the logical name fn (:search (defmacro foo-bar)) ; the first command encountered in a search from :max to ; 0 that either contains defmacro and foo-bar in the ; command form or contains defmacro and foo-bar in some ; event within its block. The recorded history of your interactions with the top-level ACL2 command loop is marked by the commands you typed that changed the logical world. Each such command generated one or more events, since the only way for you to change the logical world is to execute an event function. See *Note COMMAND:: and see *Note EVENTS::. We divide history into "command blocks," grouping together each world changing command and its events. A "command descriptor" is an object that can be used to describe a particular command in the history of the ongoing session. Each command is assigned a unique integer called its "command number" which indicates the command's position in the chronological ordering of all of the commands ever executed in this session (including those executed to initialize the system). We assign the number 1 to the first command you type to ACL2. We assign 2 to the second and so on. The non-positive integers are assigned to "prehistoric" commands, i.e., the commands used to initialize the ACL2 system: 0 is the last command of the initialization, -1 is the one before that, etc. The legal command descriptors are described below. We use n to denote any integer, sym to denote any logical name (see *Note LOGICAL-NAME::), and cd to denote, recursively, any command descriptor. command command descriptor described :max -- the most recently executed command (i.e., the one with the largest command number) :x -- synonymous with :max :x-k -- synonymous with (:x -k), if k is an integer and k>0 :min -- the earliest command (i.e., the one with the smallest command number and hence the first command of the system initialization) n -- command number n (If n is not in the range :min<=n<=:max, n is replaced by the nearest of :min and :max.) sym -- the command that introduced the logical name sym (cd n) -- the command whose number is n plus the command number of the command described by cd (:search pat cd1 cd2) In this command descriptor, pat must be either an atom or a true list of atoms and cd1 and cd2 must be command descriptors. We search the interval from cd1 through cd2 for the first command that matches pat. Note that if cd1 occurs chronologically after cd2, the search is "backwards" through history while if cd1 occurs chronologically before cd2, the search is "forwards". A backwards search will find the most recent match; a forward search will find the chronologically earliest match. A command matches pat if either the command form itself or one of the events in the block contains pat (or all of the atoms in pat if pat is a list). (:search pat) the command found by (:search pat :max 0), i.e., the most recent command matching pat that was part of the user's session, not part of the system initialization.  File: acl2-doc-emacs.info, Node: COMPUTED-HINTS, Next: CONSTRAINT, Prev: COMMAND-DESCRIPTOR, Up: MISCELLANEOUS COMPUTED-HINTS computing advice to the theorem proving process General Form of :hints: (hint1 hint2 ... hintk) Each element, hinti, must be either a common hint or a computed hint. A common hint is of the form (goal-spec :key1 val1 ... :keyn valn) where goal-spec is as specified in goal-spec and each :keyi and vali is as specified in hints. A computed hint is either a function symbol, fn, of three arguments or is a term involving, at most, the three free variables ID, CLAUSE and WORLD. The function symbol case is treated as an abbreviation of the term (fn ID CLAUSE WORLD). (Note that this tells you which argument is which.) In the discussion below we assume all computed hints are of the term form. The evaluation of the term (in a context in which its variables are bound as described below) should be either nil, indicating that the hint is not applicable to the clause in question, or else the value is an alternating list of :keyi vali "pairs" as specified in hints. The first applicable hint, if any, is used and deleted from the list of hints available to the descendants of the clause (see below). The evaluation of a hint term is done with guard checking turned off (see *Note SET-GUARD-CHECKING::); e.g., the form (car 23) in a computed hint returns nil as per the axioms. When a non-nil value is returned it is treated just as though it had been typed as part of the original input. That is, your job as the programmer of computed hints is to generate the form you would have typed had you supplied a common hint at that point. (In particular, any theory expressions in it are evaluated with respect to the global current-theory, not whatever theory is active on the subgoal in question.) If the generated list of keywords and values is illegal, an error will be signaled and the proof attempt will be aborted. It remains only to describe the bindings of the three variables. Suppose the theorem prover is working on some clause, clause, named by some goal-spec, e.g., "Subgoal *1/2"'" in some logical world, world. Corresponding to the printed goal-spec is an internal data structure called a "clause identifier" id. See *Note CLAUSE-IDENTIFIER::. In the case of a common hint, the hint applies if the goal-spec of the hint is the same as the goal-spec of the clause in question. In the case of a computed hint, the variable ID is bound to the clause id, the variable CLAUSE is bound to the (translated form of the) clause, and the variable WORLD is bound to the current ACL2 world. When a computed hint applies, it is removed from the list of hints available to the children of the clause to which it applied. This prevents it from being reapplied (often infinitely). The goals produced by induction and the top-level goals of forcing rounds are not considered children; all original hints are available to them. Insert n copies of a computed hint into the :hints to allow the hint to be used "repeatedly" at n different levels. For some instruction about how to use computed hints, see *Note USING-COMPUTED-HINTS::.  File: acl2-doc-emacs.info, Node: CONSTRAINT, Next: COPYRIGHT, Prev: COMPUTED-HINTS, Up: MISCELLANEOUS CONSTRAINT restrictions on certain functions introduced in encapsulate events Suppose that a given theorem, thm, is to be functionally instantiated using a given functional substitution, alist, as described in :DOC lemma-instance. What is the set of proof obligations generated? It is the set of all terms, tm, such that (a) tm mentions some function symbol in the domain of alist, and (b) either tm arises from the "constraint" on a function symbol ancestral in thm or some defaxiom or (ii) tm is the body of a defaxiom. Here, a function symbol is "ancestral" in thm if either it occurs in thm, or it occurs in the definition of some function symbol that occurs in thm, and so on. The remainder of this note explains what we mean by "constraint" in the words above. In a certain sense, function symbols are introduced in essentially two ways. The most common way is to use defun (or when there is mutual recursion, mutual-recursion or defuns). There is also a mechanism for introducing "witness functions"; see *Note DEFCHOOSE::. The documentation for these events describes the axioms they introduce, which we will call here their "definitional axioms." These definitional axioms are generally the constraints on the function symbols that these axioms introduce. However, when a function symbol is introduced in the scope of an encapsulate event, its constraints may differ from the definitional axioms introduced for it. For example, suppose that a function's definition is local to the encapsulate; that is, suppose the function is introduced in the signature of the encapsulate. Then its constraints include, at the least, those non-local theorems and definitions in the encapsulate that mention the function symbol. Actually, it will follow from the discussion below that if the signature is empty for an encapsulate, then the constraint on each of its new function symbols is exactly the definitional axiom introduced for it. Intuitively, we view such encapsulates just as we view include-book events. But the general case, where the signature is not empty, is more complicated. In the discussion that follows we describe in detail exactly which constraints are associated with which function symbols that are introduced in the scope of an encapsulate event. In order to simplify the exposition we make two cuts at it. In the first cut we present an over-simplified explanation that nevertheless captures the main ideas. In the second cut we complete our explanation by explaining how we view certain events as being "lifted" out of the encapsulate, resulting in a possibly smaller encapsulate, which becomes the target of the algorithm described in the first cut. At the end of this note we present an example showing why a more naive approach is unsound. Finally, before we start our "first cut," we note that constrained functions always have guards of T. This makes sense when one considers that a constrained function's "guard" only appears in the context of a local defun, which is skipped. Note also that any information you want "exported" outside an encapsulate event must be there as an explicit definition or theorem. For example, even if a function foo has output type (mv t t) in its signature, the system will not know (true-listp (foo x)) merely on account of this information. Thus, if you are using functions like foo (constrained mv functions) in a context where you are verifying guards, then you should probably provide a :type-prescription rule for the constrained function, for example, the :type-prescription rule (true-listp (foo x)). *First cut at constraint-assigning algorithm.* Quite simply, the formulas introduced in the scope of an encapsulate are conjoined, and each function symbol introduced by the encapsulate is assigned that conjunction as its constraint. Clearly this is a rather severe algorithm. Let us consider two possible optimizations in an informal manner before presenting our second cut. Consider the (rather artificial) event below. The function before1 does not refer at all, even indirectly, to the locally-introduced function sig-fn, so it is unfortunate to saddle it with constraints about sig-fn. (encapsulate ((sig-fn (x) t)) (defun before1 (x) (if (consp x) (before1 (cdr x)) x)) (local (defun sig-fn (x) (cons x x))) (defthm sig-fn-prop (consp (sig-fn x))) ) We would like to imagine moving the definition of before1 to just in front of this encapsulate, as follows. (defun before1 (x) (if (consp x) (before1 (cdr x)) x)) (encapsulate ((sig-fn (x) t)) (local (defun sig-fn (x) (cons x x))) (defthm sig-fn-prop (consp (sig-fn x))) ) Thus, we will only assign the constraint (consp (sig-fn x)), from the theorem sig-fn-prop, to the function sig-fn, not to the function before1. More generally, suppose an event in an encapsulate event does not mention any function symbol in the signature of the encapsulate, nor any function symbol that mentions any such function symbol, and so on. (We might say that no function symbol from the signature is an "ancestor" of any function symbol occurring in the event.) Then we imagine moving the event, so that it appears in front of the encapsulate. We don't actually move it, but we pretend we do when it comes time to assign constraints. Thus, such definitions only introduce definitional axioms as the constraints on the function symbols being defined, and such theorems introduce no constraints. Once this first optimization is performed, we have in mind a set of "constrained functions." These are the functions introduced in the encapsulate that would remain after moving some of them out, as indicated above. Consider the collection of all formulas introduced by the encapsulate, except the definitional axioms, that mention these constrained functions. So for example, in the event below, no such formula mentions the function symbol after1. (encapsulate ((sig-fn (x) t)) (local (defun sig-fn (x) (cons x x))) (defthm sig-fn-prop (consp (sig-fn x))) (defun after1 (x) (sig-fn x)) ) We can see that there is really no harm in imagining that we move the definition of after1 out of the encapsulate, to just after the encapsulate. We may summarize the observations above as follows, after which we conclude with a more elaborate example. *Second cut at constraint-assigning algorithm.* Given an encapsulate event, first move, to just in front of it and in the same order, all definitions and theorems for which none of the functions declared in the signature is ancestral. (In fact perform this process recursively, handling nested encapsulates.) Now collect up all formulas introduced in the encapsulate other than the definitional axioms, and restrict the set of constrained functions to those that are ancestral in at least one such formula. Finally, assign all formulas introduced in the resulting encapsulate as the common constraint on all function symbols that are introduced in the resulting encapsulate. (Thus, we imagine that the definitions of functions that are omitted from this list of function symbols, together with all non-definitional formulas omitted from this list of formulas, are moved outside the encapsulate, to just after it.) Implementation note. In the implementation we do not actually move events, but we create constraints that pretend that we did. Here is an example illustrating our constraint-assigning algorithm. It builds on the preceding examples. (encapsulate ((sig-fn (x) t)) (defun before1 (x) (if (consp x) (before1 (cdr x)) x)) (local (defun sig-fn (x) (cons x x))) (defthm sig-fn-prop (consp (sig-fn x))) (defun during (x) (if (consp x) x (cons (car (sig-fn x)) 17))) (defun before2 (x) (before1 x)) (defthm before2-prop (atom (before2 x))) (defthm during-prop (implies (and (atom x) (before2 x)) (equal (car (during x)) (car (sig-fn x))))) (defun after1 (x) (sig-fn x)) (defchoose after2 (x) (u) (and (< u x) (during x))) ) Only the functions sig-fn and during receive extra constraints. The functions before1 and before2 are viewed as moving in front of the encapsulate, as is the theorem before2-prop. The functions after1 and after2 are viewed as being moved past the encapsulate. Notice that the formula (consp (during x)) is a conjunct of the constraint. It comes from the :type-prescription rule deduced during the definition of the function during. The implementation reports the following. (SIG-FN X) is axiomatized to return one result. In addition, we export AFTER2, AFTER1, DURING-PROP, BEFORE2-PROP, BEFORE2, DURING, SIG-FN-PROP and BEFORE1. The following constraint is associated with both of the functions DURING and SIG-FN: (AND (EQUAL (DURING X) (IF (CONSP X) X (CONS (CAR (SIG-FN X)) 17))) (CONSP (DURING X)) (CONSP (SIG-FN X)) (IMPLIES (AND (ATOM X) (BEFORE2 X)) (EQUAL (CAR (DURING X)) (CAR (SIG-FN X))))) We conclude by asking (and to a certain extent, answering) the following question: Isn't there an approach to assigning constraints that avoids over-constraining more simply than our "second cut" above? Perhaps it seems that given an encapsulate, we should simply assign to each locally defined function the theorems exported about that function. If we adopted that simple approach the events below would be admissible. (encapsulate ((foo (x) t)) (local (defun foo (x) x)) (defun bar (x) (foo x)) (defthm bar-prop (equal (bar x) x) :rule-classes nil)) (defthm foo-id (equal (foo x) x) :hints (("Goal" :use bar-prop))) ; The following event is not admissible in ACL2. (defthm ouch! nil :rule-classes nil :hints (("Goal" :use ((:functional-instance foo-id (foo (lambda (x) (cons x x)))))))) Under the simple approach we have in mind, bar is constrained to satisfy both its definition and bar-prop because bar mentions a function declared in the signatures of the encapsulation. In fact, bar is so-constrained in the ACL2 semantics of encapsulation and the first two events above (the encapsulate and the consequence that foo must be the identity function) are actually admissible. But under the simple approach to assigning constraints, foo is unconstrained because no theorem about it is exported. Under that approach, ouch! is proveable because foo can be instantiated in foo-id to a function other than the identity function. It's tempting to think we can fix this by including definitions, not just theorems, in constraints. But consider the following slightly more elaborate example. The problem is that we need to include as a constraint on foo not only the definition of bar, which mentions foo explicitly, but also abc, which has foo as an ancestor. (encapsulate ((foo (x) t)) (local (defun foo (x) x)) (local (defthm foo-prop (equal (foo x) x))) (defun bar (x) (foo x)) (defun abc (x) (bar x)) (defthm abc-prop (equal (abc x) x) :rule-classes nil)) (defthm foo-id (equal (foo x) x) :hints (("Goal" :use abc-prop))) ; The following event is not admissible in ACL2. (defthm ouch! nil :rule-classes nil :hints (("Goal" :use ((:functional-instance foo-id (foo (lambda (x) (cons x x))) (bar (lambda (x) (cons x x))))))))  File: acl2-doc-emacs.info, Node: COPYRIGHT, Next: COROLLARY, Prev: CONSTRAINT, Up: MISCELLANEOUS COPYRIGHT ACL2 copyright, license, sponsorship ACL2 Version 1.9 -- A Computational Logic for Applicative Common Lisp 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. See the file LICENSE. If not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. Written by: Matt Kaufmann and J Strother Moore email: Matt_Kaufmann@email.mot.com and Moore@cs.utexas.edu Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, TX 78703-4776 U.S.A. Please also see *Note ACKNOWLEDGEMENTS::.  File: acl2-doc-emacs.info, Node: COROLLARY, Next: CURRENT-PACKAGE, Prev: COPYRIGHT, Up: MISCELLANEOUS COROLLARY the corollary formula of a rune This is a low-level system function at the present time. See *Note PR:: and see *Note PR!:: instead. Also see *Note RULE-CLASSES::for the use of the symbol :corollary in specifying a rule class.  File: acl2-doc-emacs.info, Node: CURRENT-PACKAGE, Next: DEFAULT-DEFUN-MODE, Prev: COROLLARY, Up: MISCELLANEOUS CURRENT-PACKAGE the package used for reading and printing Current-package is an ld special (see *Note LD::). The accessor is (current-package state) and the updater is (set-current-package val state), or more conventionally, (in-package val). The value of current-package is actually the string that names the package. (Common Lisp's "package" objects do not exist in ACL2.) The current package must be known to ACL2, i.e., it must be one of the initial packages or a package defined with defpkg by the user. When printing symbols, the package prefix is displayed if it is not the current-package and may be optionally displayed otherwise. Thus, if current-package is "ACL2" then the symbol 'ACL2::SYMB may be printed as SYMB or ACL2::SYMB, while 'MY-PKG::SYMB must be printed as MY-PKG::SYMB. But if current-package is "MY-PKG" then the former symbol must be printed as ACL2::SYMB while the latter may be printed as SYMB. In Common Lisp, current-package also affects how objects are read from character streams. Roughly speaking, read and print are inverses if the current-package is fixed, so reading from a stream produced by printing an object must produce an equal object. In ACL2, the situation is more complicated because we never read objects from character streams, we only read them from object "streams" (channels). Logically speaking, the objects in such a channel are fixed regardless of the setting of current-package. However, our host file systems do not support the idea of Lisp object files and instead only support character files. So when you open an object input channel to a given (character file) we must somehow convert it to a list of ACL2 objects. This is done by a deus ex machina ("a person or thing that appears or is introduced suddenly and unexpectedly and provides a contrived solution to an apparently insoluble difficulty," Webster's Ninth New Collegiate Dictionary). Roughly speaking, the deus ex machina determines what sequence of calls to read-object will occur in the future and what the current-package will be during each of those calls, and then produces a channel containing the sequence of objects produced by an analogous sequence of Common Lisp reads with *current-package* bound appropriately for each. A simple rule suffices to make sane file io possible: before you read an object from an object channel to a file created by printing to a character channel, make sure the current-package at read-time is the same as it was at print-time.  File: acl2-doc-emacs.info, Node: DEFAULT-DEFUN-MODE, Next: DEFAULT-PRINT-PROMPT, Prev: CURRENT-PACKAGE, Up: MISCELLANEOUS DEFAULT-DEFUN-MODE the default defun-mode of defun'd functions When a defun is processed and no :mode xarg is supplied, the function default-defun-mode is used. To find the default defun-mode of the current ACL2 world, type (default-defun-mode (w state)). See *Note DEFUN-MODE:: for a discussion of defun-modes. To change the default defun-mode of the ACL2 world, type one of the keywords :program or :logic. The default ACL2 prompt displays the current default defun-mode by showing the character p for :program mode, and omitting it for :logic mode; see *Note DEFAULT-PRINT-PROMPT::. The default defun-mode may be changed using the keyword commands :program and :logic, which are equivalent to the commands (program) and (logic). Each of these names is documented separately: see *Note PROGRAM:: and see *Note LOGIC::. The default defun-mode is stored in the table acl2-defaults-table and hence may also be changed by a table command. See *Note TABLE:: and also see *Note ACL2-DEFAULTS-TABLE::. Both mode-changing commands are events. While events that change the default defun-mode are permitted within an encapsulate or the text of a book, their effects are local in scope to the duration of the encapsulation or inclusion. For example, if the default defun-mode is :logic and a book is included that contains the event (program), then subsequent events within the book are processed with the default defun-mode :program; but when the include-book event completes, the default defun-mode will still be :logic. Commands that change the default defun-mode are not permitted inside local forms.