Info file: acl2-doc-lemacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-lemacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.9 Copyright (C) 1997 Computational Logic, Inc. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. Written by: Matt Kaufmann and J Strother Moore Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, TX 78703-4776 U.S.A.  File: acl2-doc-lemacs.info, Node: ACL2-PC||ILLEGAL, Next: ACL2-PC||IN-THEORY, Prev: ACL2-PC||HYPS, Up: PROOF-CHECKER ACL2-PC||ILLEGAL (macro) illegal instruction Example: (illegal -3) General Form: (illegal instruction) Probably not of interest to most users; always "fails" since it expands to the fail command. The illegal command is used mainly in the implementation. For example, the instruction 0 is "read" as (illegal 0), since dive expects positive integers.  File: acl2-doc-lemacs.info, Node: ACL2-PC||IN-THEORY, Next: ACL2-PC||INDUCT, Prev: ACL2-PC||ILLEGAL, Up: PROOF-CHECKER ACL2-PC||IN-THEORY (primitive) set the current proof-checker theory Example: (in-theory (union-theories *s-prop-theory* '(true-listp binary-append))) General Form: (in-theory &optional atom-or-theory-expression) If the argument is not supplied, then this command sets the current proof-checker theory (see below for explanation) to agree with the current ACL2 theory. Otherwise, the argument should be a theory expression, and in that case the proof-checker theory is set to the value of that theory expression. The current proof-checker theory is used in all calls to the ACL2 theorem prover and rewriter from inside the proof-checker. Thus, the most recent in-theory instruction in the current state-stack has an effect in the proof-checker totally analogous to the effect caused by an in-theory hint or event in ACL2. However, in-theory instructions in the proof-checker have no effect outside the proof-checker's interactive loop. If the most recent in-theory instruction in the current state of the proof-checker has no arguments, or if there is no in-theory instruction in the current state of the proof-checker, then the proof-checker will use the current ACL2 theory. This is true even if the user has interrupted the interactive loop by exiting and changing the global ACL2 theory. However, if the most recent in-theory instruction in the current state of the proof-checker had an argument, then global changes to the current theory will have no effect on the proof-checker state.  File: acl2-doc-lemacs.info, Node: ACL2-PC||INDUCT, Next: ACL2-PC||LISP, Prev: ACL2-PC||IN-THEORY, Up: PROOF-CHECKER ACL2-PC||INDUCT (atomic macro) generate subgoals using induction Examples: induct, (induct t) -- induct according to a heuristically-chosen scheme, creating a new subgoal for each base and induction step (induct (append (reverse x) y)) -- as above, but choose an induction scheme based on the term (append (reverse x) y) rather than on the current goal General Form: (induct &optional term) Induct as in the corresponding :induct hint given to the theorem prover, creating new subgoals for the base and induction steps. If term is t or is not supplied, then use the current goal to determine the induction scheme; otherwise, use that term. *Note:* As usual, abbreviations are allowed in the term. *Note:* Induct actually calls the prove command with all processes turned off. Thus, you must be at top of the goal for an induct instruction.  File: acl2-doc-lemacs.info, Node: ACL2-PC||LISP, Next: ACL2-PC||MORE, Prev: ACL2-PC||INDUCT, Up: PROOF-CHECKER ACL2-PC||LISP (meta) evaluate the given form in Lisp Example: (lisp (assign xxx 3)) General Form: (lisp form) Evaluate form. The lisp command is mainly of interest for side effects. See also print, skip, and fail. The rest of the documentation for lisp is of interest only to those who use it in macro commands. If the Lisp evaluation (by trans-eval) of form returns an "error triple" of the form (mv erp (cons 3 val) &), then val is of the form (erp-1 val-1 &), and the lisp command returns the appropriate error triple (mv (or erp erp-1) val-1 state) . Otherwise, the trans-eval of form must return an "error triple" of the form (mv erp (list* state-out mult val) &), and the lisp command returns the appropriate error triple (mv erp val state) .  File: acl2-doc-lemacs.info, Node: ACL2-PC||MORE, Next: ACL2-PC||MORE!, Prev: ACL2-PC||LISP, Up: PROOF-CHECKER ACL2-PC||MORE (macro) proof-checker help facility Continues documentation of last proof-checker command visited with help. Invoke help for documentation about the proof-checker help facility.  File: acl2-doc-lemacs.info, Node: ACL2-PC||MORE!, Next: ACL2-PC||NEGATE, Prev: ACL2-PC||MORE, Up: PROOF-CHECKER ACL2-PC||MORE! (macro) proof-checker help facility Continues documentation of last proof-checker command visited with help, until all documentation on that command is printed out. Invoke help for documentation about the proof-checker help facility.  File: acl2-doc-lemacs.info, Node: ACL2-PC||NEGATE, Next: ACL2-PC||NIL, Prev: ACL2-PC||MORE!, Up: PROOF-CHECKER ACL2-PC||NEGATE (macro) run the given instructions, and "succeed" if and only if they "fail" Example: (negate prove) General form: (negate &rest instruction-list) Run the indicated instructions exactly in the sense of do-all, and "succeed" if and only if they "fail". *Note:* Negate instructions will never produce hard "failures".  File: acl2-doc-lemacs.info, Node: ACL2-PC||NIL, Next: ACL2-PC||NOISE, Prev: ACL2-PC||NEGATE, Up: PROOF-CHECKER ACL2-PC||NIL (macro) used for interpreting control-d Example and General form: nil (or, control-d). The whole point of this command is that in some Lisps (including akcl), if you type control-d then it seems, on occasion, to get interpreted as nil. Without this command, one seems to get into an infinite loop.  File: acl2-doc-lemacs.info, Node: ACL2-PC||NOISE, Next: ACL2-PC||NX, Prev: ACL2-PC||NIL, Up: PROOF-CHECKER ACL2-PC||NOISE (meta) run instructions with output Example: (noise induct prove) General Form: (noise &rest instruction-list) Run the instruction-list through the top-level loop with output. In fact, having output is the default. Noise is useful inside a surrounding call of quiet, when one temporarily wants output. For example, if one wants to see output for a prove command immediately following an induct command but before an s command, one may want to submit an instruction like (quiet induct (noise prove) s). See also quiet.  File: acl2-doc-lemacs.info, Node: ACL2-PC||NX, Next: ACL2-PC||ORELSE, Prev: ACL2-PC||NOISE, Up: PROOF-CHECKER ACL2-PC||NX (atomic macro) move forward one argument in the enclosing term Example and General Form: nx For example, if the conclusion is (= x (* (- y) z)) and the current subterm is x, then after executing nx, the current subterm will be (* (- y) z). This is the same as up followed by (dive n+1), where n is the position of the current subterm in its parent term in the conclusion. Thus in particular, the nx command fails if one is already at the top of the conclusion. See also up, dive, top, and bk.  File: acl2-doc-lemacs.info, Node: ACL2-PC||ORELSE, Next: ACL2-PC||P, Prev: ACL2-PC||NX, Up: PROOF-CHECKER ACL2-PC||ORELSE (macro) run the first instruction; if (and only if) it "fails", run the second Example: (orelse top (print "Couldn't move to the top")) General form: (orelse instr1 instr2) Run the first instruction. Then if it "fails", run the second instruction also; otherwise, stop after the first. This instruction "succeeds" if and only if either instr1 "succeeds", or else instr2 "succeeds". If it "fails", then the failure is soft.  File: acl2-doc-lemacs.info, Node: ACL2-PC||P, Next: ACL2-PC||P-TOP, Prev: ACL2-PC||ORELSE, Up: PROOF-CHECKER ACL2-PC||P (macro) prettyprint the current term Example and General Form: p Prettyprint the current term. The usual user syntax is used, so that for example one would see (and x y) rather than (if x y 'nil). (See also pp.) Also, abbreviations are inserted where appropriate; see add-abbreviation. The "current term" is the entire conclusion unless dive commands have been given, in which case it may be a subterm of the conclusion. If all goals have been proved, a message saying so will be printed (as there will be no current term!).  File: acl2-doc-lemacs.info, Node: ACL2-PC||P-TOP, Next: ACL2-PC||PP, Prev: ACL2-PC||P, Up: PROOF-CHECKER ACL2-PC||P-TOP (macro) prettyprint the conclusion, highlighting the current term Example and General Form: p-top For example, if the conclusion is (equal (and x (p y)) (foo z)) and the current subterm is (p y), then p-top will print (equal (and x (*** (p y) ***)) (foo z)). Prettyprint the the conclusion, highlighting the current term. The usual user syntax is used, as with the command p (as opposed to pp). This is illustrated in the example above, where one would *not* see (equal (if x (*** (p y) ***) 'nil) (foo z)). *Note* (obscure): In some situations, a term of the form (if x t y) occurring inside the current subterm will not print as (or x y), when x isn't a call of a boolean primitive. There's nothing incorrect about this, however.  File: acl2-doc-lemacs.info, Node: ACL2-PC||PP, Next: ACL2-PC||PRINT, Prev: ACL2-PC||P-TOP, Up: PROOF-CHECKER ACL2-PC||PP (macro) prettyprint the current term Example and General Form: pp This is the same as p (see its documentation), except that raw syntax (internal form) is used. So for example, one would see (if x y 'nil) rather than (and x y). Abbreviations are however still inserted, as with p.  File: acl2-doc-lemacs.info, Node: ACL2-PC||PRINT, Next: ACL2-PC||PRINT-ALL-GOALS, Prev: ACL2-PC||PP, Up: PROOF-CHECKER ACL2-PC||PRINT (macro) print the result of evaluating the given form Example: (print (append '(a b) '(c d))) Print the list (a b c d) to the terminal General Form: (print form) Prettyprints the result of evaluating form. The evaluation of form should return a single value that is not state. If the form you want to evaluate does not satisfy the criterion above, you should create an appropriate call of the lisp command instead. Notice that this command always returns (mv nil state state).  File: acl2-doc-lemacs.info, Node: ACL2-PC||PRINT-ALL-GOALS, Next: ACL2-PC||PRINT-MAIN, Prev: ACL2-PC||PRINT, Up: PROOF-CHECKER ACL2-PC||PRINT-ALL-GOALS (macro) print all the (as yet unproved) goals Example and General Form: print-all-goals Prints all the goals that remain to be proved, in a pleasant format.  File: acl2-doc-lemacs.info, Node: ACL2-PC||PRINT-MAIN, Next: ACL2-PC||PRO, Prev: ACL2-PC||PRINT-ALL-GOALS, Up: PROOF-CHECKER ACL2-PC||PRINT-MAIN (macro) print the original goal Example and General Form: print-main Prints the goal as originally entered.  File: acl2-doc-lemacs.info, Node: ACL2-PC||PRO, Next: ACL2-PC||PROMOTE, Prev: ACL2-PC||PRINT-MAIN, Up: PROOF-CHECKER ACL2-PC||PRO (atomic macro) repeatedly apply promote Example and General Form: pro Apply the promote command until there is no change. This command "succeeds" exactly when at least one call of promote "succeeds". In that case, only a single new proof-checker state will be created.  File: acl2-doc-lemacs.info, Node: ACL2-PC||PROMOTE, Next: ACL2-PC||PROTECT, Prev: ACL2-PC||PRO, Up: PROOF-CHECKER ACL2-PC||PROMOTE (primitive) move antecedents of conclusion's implies term to top-level hypotheses Examples: promote (promote t) For example, if the conclusion is (implies (and x y) z), then after execution of promote, the conclusion will be z and the terms x and y will be new top-level hypotheses. General Form: (promote &optional do-not-flatten-flag) Replace conclusion of (implies hyps exp) or (if hyps exp t) with simply exp, adding hyps to the list of top-level hypotheses. Moreover, if hyps is viewed as a conjunction then each conjunct will be added as a separate top-level hypothesis. An exception is that if do-not-flatten-flag is supplied and not nil, then only one top-level hypothesis will be added, namely hyps. *Note*: You must be at the top of the conclusion in order to use this command. Otherwise, first invoke top.  File: acl2-doc-lemacs.info, Node: ACL2-PC||PROTECT, Next: ACL2-PC||PROVE, Prev: ACL2-PC||PROMOTE, Up: PROOF-CHECKER ACL2-PC||PROTECT (macro) run the given instructions, reverting to existing state upon failure Example: (protect induct p prove) General Form: (protect &rest instruction-list) Protect is the same as do-strict, except that as soon as an instruction "fails", the state-stack reverts to what it was before the protect instruction began, and restore is given the same meaning that it had before the protect instruction began. See the documentation for do-strict.  File: acl2-doc-lemacs.info, Node: ACL2-PC||PROVE, Next: ACL2-PC||PUT, Prev: ACL2-PC||PROTECT, Up: PROOF-CHECKER ACL2-PC||PROVE (primitive) call the ACL2 theorem prover to prove the current goal Examples: prove -- attempt to prove the current goal (prove :otf-flg t :hints (("Subgoal 2" :by foo) ("Subgoal 1" :use bar))) -- attempt to prove the current goal, with the indicated hints and with OTF-FLG set General Form: (prove &rest rest-args) Attempt to prove the current goal, where rest-args is as in the keyword arguments to defthm except that only :hints and :otf-flg are allowed. The command succeeds exactly when the corresponding defthm would succeed, except that it is all right for some goals to be given "bye"s. Each goal given a "bye" will be turned into a new subgoal. (*Note HINTS:: for an explanation of :by hints.) *Note:* Use (= t) instead if you are not at the top of the conclusion. Also note that if there are any hypotheses in the current goal, then what is actually attempted is a proof of (implies hyps conc), where hyps is the conjunction of the top-level hypotheses and conc is the goal's conclusion. *Note:* It is allowed to use abbreviations in the hints.  File: acl2-doc-lemacs.info, Node: ACL2-PC||PUT, Next: ACL2-PC||QUIET, Prev: ACL2-PC||PROVE, Up: PROOF-CHECKER ACL2-PC||PUT (macro) substitute for a "free variable" Example: (put x 17) General Form: (put var expr) Substitute expr for the "free variable" var, as explained below. A "free variable" is, for our purposes, a variable var such that the instruction (free var) has been executed earlier in the state-stack. What (free var) really does is to let var be an abbreviation for the term (hide var) (see documentation for add-abbreviation). What (put var expr) really does is to unwind the state-stack, replacing that free instruction with the instruction (add-abbreviation var expr), so that future references to (? var) become reference to expr rather than to (hide var), and then to replay all the other instructions that were unwound. Because hide was used, the expectation is that in most cases, the instructions will replay successfully and put will "succeed". However, if any replayed instruction "fails", then the entire replay will abort and "fail", and the state-stack will revert to its value before the put instruction was executed. If (put var expr) "succeeds", then (remove-abbreviation var) will be executed at the end. *Note*: The restore command will revert the state-stack to its value present before the put instruction was executed.  File: acl2-doc-lemacs.info, Node: ACL2-PC||QUIET, Next: ACL2-PC||R, Prev: ACL2-PC||PUT, Up: PROOF-CHECKER ACL2-PC||QUIET (meta) run instructions without output Example: (quiet induct prove) General Form: (quiet &rest instruction-list) Run the instruction-list through the top-level loop with no output. See also noise.  File: acl2-doc-lemacs.info, Node: ACL2-PC||R, Next: ACL2-PC||REDUCE, Prev: ACL2-PC||QUIET, Up: PROOF-CHECKER ACL2-PC||R (macro) same as rewrite Example: (r 3) General Form: (rewrite &optional rule-id substitution ;; below are rare arguments, used for disambiguation: target-lhs target-rhs target-hyps target-equiv) See the documentation for rewrite, as r and rewrite are identical.  File: acl2-doc-lemacs.info, Node: ACL2-PC||REDUCE, Next: ACL2-PC||REDUCE-BY-INDUCTION, Prev: ACL2-PC||R, Up: PROOF-CHECKER ACL2-PC||REDUCE (atomic macro) call the ACL2 theorem prover's simplifier Examples: reduce -- attempt to prove the current goal without using induction (reduce ("Subgoal 2" :by foo) ("Subgoal 1" :use bar)) -- attempt to prove the current goal by without using induction, with the indicated hints General Form: (reduce &rest hints) Attempt to prove the current goal without using induction, using the indicated hints (if any). A subgoal will be created for each goal that would have been pushed for proof by induction in an ordinary proof. Notice that unlike prove, the arguments to reduce are spread out, and are all hints. *Note:* Induction will be used to the extent that it is ordered explicitly in the hints.  File: acl2-doc-lemacs.info, Node: ACL2-PC||REDUCE-BY-INDUCTION, Next: ACL2-PC||REMOVE-ABBREVIATIONS, Prev: ACL2-PC||REDUCE, Up: PROOF-CHECKER ACL2-PC||REDUCE-BY-INDUCTION (macro) call the ACL2 prover without induction, after going into induction Examples: reduce-by-induction -- attempt to prove the current goal after going into induction, with no further inductions (reduce-by-induction ("Subgoal 2" :by foo) ("Subgoal 1" :use bar)) -- attempt to prove the current goal after going into induction, with no further inductions, using the indicated hints General Form: (reduce-by-induction &rest hints) A subgoal will be created for each goal that would have been pushed for proof by induction in an ordinary proof, except that the proof begins with a top-level induction. Notice that unlike prove, the arguments to reduce-by-induction are spread out, and are all hints. See also prove, reduce, and bash. *Note*: Induction and the various processes will be used to the extent that they are ordered explicitly in the :induct and :do-not hints.  File: acl2-doc-lemacs.info, Node: ACL2-PC||REMOVE-ABBREVIATIONS, Next: ACL2-PC||REPEAT, Prev: ACL2-PC||REDUCE-BY-INDUCTION, Up: PROOF-CHECKER ACL2-PC||REMOVE-ABBREVIATIONS (primitive) remove one or more abbreviations Examples: remove-abbreviations -- remove all abbreviations (remove-abbreviations v w) -- assuming that V and W currently abbreviate terms, then they are "removed" in the sense that they are no longer considered to abbreviate those terms General Forms: (remove-abbreviations &rest vars) If vars is not empty (i.e., not nil), remove the variables in vars from the current list of abbreviations, in the sense that each variable in vars will no longer abbreviate a term. *Note:* The instruction fails if at least one of the arguments fails to be a variable that abbreviates a term. See also the documentation for add-abbreviation, which contains a discussion of abbreviations in general, and show-abbreviations.  File: acl2-doc-lemacs.info, Node: ACL2-PC||REPEAT, Next: ACL2-PC||REPEAT-REC, Prev: ACL2-PC||REMOVE-ABBREVIATIONS, Up: PROOF-CHECKER ACL2-PC||REPEAT (macro) repeat the given instruction until it "fails" Example: (repeat promote) General Form: (repeat instruction) The given instruction is run repeatedly until it "fails". *Note:* There is nothing here in general to prevent the instruction from being run after all goals have been proved, though this is indeed the case for primitive instructions.  File: acl2-doc-lemacs.info, Node: ACL2-PC||REPEAT-REC, Next: ACL2-PC||REPLAY, Prev: ACL2-PC||REPEAT, Up: PROOF-CHECKER ACL2-PC||REPEAT-REC (macro) auxiliary to repeat See documentation for repeat.  File: acl2-doc-lemacs.info, Node: ACL2-PC||REPLAY, Next: ACL2-PC||RESTORE, Prev: ACL2-PC||REPEAT-REC, Up: PROOF-CHECKER ACL2-PC||REPLAY (macro) replay one or more instructions Examples: REPLAY -- replay all instructions in the current session (i.e., state-stack) (REPLAY 5) -- replay the most recent 5 instructions (REPLAY 5 (COMMENT deleted dive command here)) -- replace the 5th most recent instruction with the indicated comment instruction, and then replay it followed by the remaining 4 instructions General Form: (REPLAY &OPTIONAL n replacement-instruction) Replay the last n instructions if n is a positive integer; else n should be nil or not supplied, and replay all instructions. However, if replacement-instruction is supplied and not nil, then before the replay, replace the nth instruction (from the most recent, as shown by commands) with replacement-instruction. If this command "fails", then the restore command will revert the state-stack to its value present before the replay instruction was executed.  File: acl2-doc-lemacs.info, Node: ACL2-PC||RESTORE, Next: ACL2-PC||RETAIN, Prev: ACL2-PC||REPLAY, Up: PROOF-CHECKER ACL2-PC||RESTORE (meta) remove the effect of an UNDO command Example and General Form: restore Restore removes the effect of an undo command. This always works as expected if restore is invoked immediately after undo, without intervening instructions. However, other commands may also interact with restore, notably "sequencing" commands such as do-all, do-strict, protect, and more generally, sequence. *Note:* Another way to control the saving of proof-checker state is with the save command; see the documentation for save. The restore command always "succeeds"; it returns (mv nil t state).  File: acl2-doc-lemacs.info, Node: ACL2-PC||RETAIN, Next: ACL2-PC||RETRIEVE, Prev: ACL2-PC||RESTORE, Up: PROOF-CHECKER ACL2-PC||RETAIN (atomic macro) drop all *but* the indicated top-level hypotheses Example: (RETAIN 2 3) -- keep the second and third hypotheses, and drop the rest General Form: (retain &rest args) Drop all top-level hypotheses *except* those with the indicated indices. There must be at least one argument, and all must be in range (i.e. integers between one and the number of top-level hypotheses, inclusive).  File: acl2-doc-lemacs.info, Node: ACL2-PC||RETRIEVE, Next: ACL2-PC||REWRITE, Prev: ACL2-PC||RETAIN, Up: PROOF-CHECKER ACL2-PC||RETRIEVE (macro) re-enter the proof-checker Examples: (retrieve associativity-of-permutationp) retrieve General Form: (retrieve &optional name) Must be used from outside the interactive proof-checker loop. If name is supplied and not nil, this causes re-entry to the interactive proof-checker loop in the state at which save was last executed for the indicated name. (See documentation for save.) If name is nil or is not supplied, then the user is queried regarding which proof-checker state to re-enter. The query is omitted, however, if there only one proof-checker state is present that was saved with save, in which case that is the one that is used. See also unsave.  File: acl2-doc-lemacs.info, Node: ACL2-PC||REWRITE, Next: ACL2-PC||RUN-INSTR-ON-GOAL, Prev: ACL2-PC||RETRIEVE, Up: PROOF-CHECKER ACL2-PC||REWRITE (primitive) apply a rewrite rule Examples: (rewrite reverse-reverse) -- apply the rewrite rule `reverse-reverse' (rewrite (:rewrite reverse-reverse)) -- same as above (rewrite 2) -- apply the second rewrite rule, as displayed by show-rewrites rewrite -- apply the first rewrite rule, as displayed by show-rewrites (rewrite transitivity-of-< ((y 7))) -- apply the rewrite rule transitivity-of-< with the substitution that associates 7 to the "free variable" y General Form: (rewrite &optional rule-id substitution) Replace the current subterm with a new term by applying a rewrite rule. If rule-id is a positive integer n, then the nth rewrite rule as displayed by show-rewrites is the one that is applied. If rule-id is nil or is not supplied, then it is treated as the number 1. Otherwise, rule-id should be either a rune of or name of a rewrite rule. If a name is supplied, then any rule of that name may be used. More explanation of all of these points follows below. Consider first the following example. Suppose that the current subterm is (reverse (reverse y)) and that there is a rewrite rule called reverse-reverse of the form (implies (true-listp x) (equal (reverse (reverse x)) x)) . Then the instruction (rewrite reverse-reverse) would cause the current subterm to be replaced by y and would create a new goal with conclusion (true-listp y). An exception is that if the top-level hypotheses imply (true-listp y) using only "trivial reasoning" (more on this below), then no new goal is created. A rather important point is that if the rule-id argument is a number or is not supplied, then the system will store an instruction of the form (rewrite name ...), where name is the name of a rewrite rule; this is in order to make it easier to replay instructions when there have been changes to the history. Actually, instead of the name (whether the name is supplied or calculated), the system stores the rune if there is any chance of ambiguity. (Formally, "ambiguity" here means that the rune being applied is of the form (:rewrite name . index), where index is not nil.) Speaking in general, then, a rewrite instruction works as follows: First, a rewrite rule is selected according to the arguments of the rewrite instruction. The selection is made as explained above under "General Form" above. The "disambiguating rare arguments" will rarely be of interest to the user; as explained just above, the stored instruction always contains the name of the rewrite rule, so if there is more than one rule of that name then the system creates and stores these extra arguments in order to make the resulting instruction unambiguous, i.e., so that only one rewrite rule applies. For what it's worth, they correspond respectively to the fields of a rewrite rule record named lhs, rhs, hyps, and equiv. Next, the left-hand side of the rule is matched with the current subterm, i.e., a substitution unify-subst is found such that if one instantiates the left-hand side of the rule with unify-subst, then one obtains the current subterm. If this matching fails, then the instruction fails. Now an attempt is made to relieve the hypotheses, in much the same sense as the theorem prover relieves hypotheses except that there is no call to the rewriter. Essentially, this means that the substitution unify-subst is applied to the hypotheses and the system then checks whether all hypotheses are "clearly" true in the current context. If there are variables in the hypotheses of the rewrite rule that do not occur in the left-hand side of the conclusion even after the user-supplied substitution (default: nil) is applied, then a weak attempt is made to extend that substitution so that even those hypotheses can be relieved. However, if even one hypothesis remains unrelieved, then no automatic extension of the substitution is made, and in fact hypotheses that contain even one uninstantiated variable will remain unrelieved. Finally, the instruction is applied as follows. The current subterm is replaced by applying the final substitution, i.e., the extension of unify-subst by the user-supplied substitution which may in turn be extended by the system (as explained above) in order to relieve all hypotheses, to the right-hand side of the selected rewrite rule. And, one new subgoal is created for each unrelieved hypothesis of the rule, whose top-level hypotheses are the governors and top-level hypotheses of the current goal and whose conclusion and current subterm are the instance, by that same final substitution, of that unrelieved hypothesis. *Note:* The substitution argument should be a list whose elements have the form (variable term), where term may contain abbreviations.  File: acl2-doc-lemacs.info, Node: ACL2-PC||RUN-INSTR-ON-GOAL, Next: ACL2-PC||RUN-INSTR-ON-NEW-GOALS, Prev: ACL2-PC||REWRITE, Up: PROOF-CHECKER ACL2-PC||RUN-INSTR-ON-GOAL (macro) auxiliary toxae THEN See documentation for then.  File: acl2-doc-lemacs.info, Node: ACL2-PC||RUN-INSTR-ON-NEW-GOALS, Next: ACL2-PC||S, Prev: ACL2-PC||RUN-INSTR-ON-GOAL, Up: PROOF-CHECKER ACL2-PC||RUN-INSTR-ON-NEW-GOALS (macro) auxiliary to then See documentation for then.  File: acl2-doc-lemacs.info, Node: ACL2-PC||S, Next: ACL2-PC||S-PROP, Prev: ACL2-PC||RUN-INSTR-ON-NEW-GOALS, Up: PROOF-CHECKER ACL2-PC||S (primitive) simplify the current subterm Examples: S -- simplify the current subterm (S :backchain-limit 2 :normalize t :expand (append x z)) -- simplify the current subterm, but during the rewriting process first "normalize" it by pushing IFs to the top-level, and also force the term (append x z) to be expanded during the rewriting process General Form: (s &key rewrite normalize backchain-limit repeat in-theory hands-off expand) Simplify the current subterm according to the keyword parameters supplied. First if-normalization is applied (unless the normalize argument is nil), i.e., each subterm of the form (f ... (if test x y) ...) is replaced by the term (if test (f ... x ...) (f ... y ...)) except, of course, when f is if and the indicated if subterm is in the second or third argument position. Then rewriting is applied (unless the rewrite argument is nil). Finally this pair of actions is repeated -- until the rewriting step causes no change in the term. A description of each parameter follows. :rewrite -- default t When non-nil, instructs the system to use ACL2's rewriter (or, something close to it) during simplification. :normalize -- default t When non-nil, instructs the system to use if-normalization (as described above) during simplification. :backchain-limit -- default 0 Sets the number of recursive calls to the rewriter that are allowed for backchaining. Even with the default of 0, some reasoning is allowed (technically speaking, type-set reasoning is allowed) in the relieving of hypotheses. :repeat -- default 0 Sets the number of times the current term is to be rewritten. If this value is t, then the default is used (as specified by the constant *default-s-repeat-limit*). :in-theory, :hands-off, :expand These have their usual meaning; *Note HINTS::. *Note:* if conditional rewrite rules are used that cause case splits because of the use of force, then appropriate new subgoals will be created, i.e., with the same current subterm (and address) but with each new (forced) hypothesis being negated and then used to create a corresponding new subgoal. In that case, the current goal will have all such new hypotheses added to the list of top-level hypotheses.  File: acl2-doc-lemacs.info, Node: ACL2-PC||S-PROP, Next: ACL2-PC||SAVE, Prev: ACL2-PC||S, Up: PROOF-CHECKER ACL2-PC||S-PROP (atomic macro) simplify propositionally Example: s-prop General Form: (s-prop &rest names) Simplify, using the default settings for s (which include if-normalization and rewriting without real backchaining), but with respect to a theory in which only basic functions and rules (the ones in *s-prop-theory*), together with the names (or parenthesized names) in the &rest argument names, are enabled. See also the documentation for s.  File: acl2-doc-lemacs.info, Node: ACL2-PC||SAVE, Next: ACL2-PC||SEQUENCE, Prev: ACL2-PC||S-PROP, Up: PROOF-CHECKER ACL2-PC||SAVE (macro) save the proof-checker state (state-stack) Example: (save lemma3-attempt General Form: (save &optional name do-it-flg) Saves the current proof-checker state by "associating" it with the given name. Submit (retrieve name) to Lisp to get back to this proof-checker state. If verify was originally supplied with an event name, then the argument can be omitted in favor of that name as the default. *Note* that if a save has already been done with the indicated name (or the default event name), then the user will be queried regarding whether to go ahead with the save -- except, if do-it-flg is supplied and not nil, then there will be no query and the save will be effected. See also the documentation for retrieve and unsave.  File: acl2-doc-lemacs.info, Node: ACL2-PC||SEQUENCE, Next: ACL2-PC||SHOW-ABBREVIATIONS, Prev: ACL2-PC||SAVE, Up: PROOF-CHECKER ACL2-PC||SEQUENCE (meta) run the given list of instructions according to a multitude of options Example: (sequence (induct p prove) t) See also the definitions of commands do-all, do-strict, protect, and succeed. General Form: (sequence instruction-list &optional strict-flg protect-flg success-expr no-prompt-flg) Each instruction in the list instruction-list is run, and the instruction "succeeds" if every instruction in instruction-list "succeeds". However, it might "succeed" even if some instructions in the list "fail"; more generally, the various arguments control a number of aspects of the running of the instructions. All this is explained in the paragraphs below. First we embark on a general discussion of the instruction interpreter, including the notions of "succeed" and "fail". *Note:* The arguments are *not* evaluated, except (in a sense) for success-expr, as described below. Each primitive and meta instruction can be thought of as returning an error triple (in the standard ACL2 sense), say (erp val state). An instruction (primitive or meta) "succeeds" if erp is nil and val is not nil; otherwise it "fails". (When we use the words "succeed" or "fail" in this technical sense, we'll always include them in double quotes.) If an instruction "fails," we say that that the failure is "soft" if erp is nil; otherwise the failure is "hard". The sequence command gives the user control over how to treat "success" and "failure" when sequencing instructions, though we have created a number of handy macro commands for this purpose, notably do-all, do-strict and protect. Here is precisely what happens when a sequence instruction is run. The instruction interpreter is run on the instructions supplied in the argument instruction-list (in order). The interpreter halts the first time there is a hard "failure." except that if strict-flg is supplied and not nil, then the interpreter halts the first time there is any "failure." The error triple (erp val state) returned by the sequence instruction is the triple returned by the last instruction executed (or, the triple (nil t state) if instruction-list is nil), except for the following provision. If success-expr is supplied and not nil, then it is evaluated with the state global variables erp and val (in ACL2 package) bound to the corresponding components of the error triple returned (as described above). At least two values should be returned, and the first two of these will be substituted for erp and val in the triple finally returned by sequence. For example, if success-expr is (mv erp val), then no change will be made to the error triple, and if instead it is (mv nil t), then the sequence instruction will "succeed". That concludes the description of the error triple returned by a sequence instruction, but it remains to explain the effects of the arguments protect-flg and no-prompt-flg. If protect-flg is supplied and not nil and if also the instruction "fails" (i.e., the error component of the triple is not nil or the value component is nil), then the state is reverted so that the proof-checker's state (including the behavior of restore) is set back to what it was before the sequence instruction was executed. Otherwise, unless no-restore-flg is set, the state is changed so that the restore command will now undo the effect of this sequence instruction (even if there were nested calls to sequence). Finally, as each instruction in instruction-list is executed, the prompt and that instruction will be printed, unless the global state variable print-prompt-and-instr-flg is unbound or nil and the parameter no-prompt-flg is supplied and not nil.  File: acl2-doc-lemacs.info, Node: ACL2-PC||SHOW-ABBREVIATIONS, Next: ACL2-PC||SHOW-REWRITES, Prev: ACL2-PC||SEQUENCE, Up: PROOF-CHECKER ACL2-PC||SHOW-ABBREVIATIONS (macro) display the current abbreviations Examples: (show-abbreviations v w) -- assuming that v and w currently abbreviate terms, then this instruction displays them together with the terms they abbreviate show-abbreviations -- display all abbreviations See also add-abbreviation and remove-abbreviations. In particular, the documentation for add-abbreviation contains a general discussion of abbreviations. General Form: (show-abbreviations &rest vars) Display each argument in vars together with the term it abbreviates (if any). If there are no arguments, i.e. the instruction is simply show-abbreviations, then display all abbreviations together with the terms they abbreviate. If the term abbreviated by a variable, say v, contains a proper subterm that is also abbreviate by (another) variable, then both the unabbreviated term and the abbreviated term (but not using (? v) to abbreviate the term) are displayed with together with v.  File: acl2-doc-lemacs.info, Node: ACL2-PC||SHOW-REWRITES, Next: ACL2-PC||SKIP, Prev: ACL2-PC||SHOW-ABBREVIATIONS, Up: PROOF-CHECKER ACL2-PC||SHOW-REWRITES (macro) display the applicable rewrite rules Example: show-rewrites General Form: (show-rewrites &optional rule-id enabled-only-flg) Display rewrite rules whose left-hand side matches the current subterm. This command is useful in conjunction with rewrite. If rule-id is supplied and is a name (non-nil symbol) or a rune, then only the corresponding rewrite rule(s) will be displayed, while if rule-id is a positive integer n, then only the nth rule that would be in the list is displayed. In each case, the display will point out when a rule is currently disabled (in the interactive environment), except that if enabled-only-flg is supplied and not nil, then disabled rules will not be displayed at all. Finally, the free variables of any rule (those occurring in the rule that do not occur in the left-hand side of its conclusion) will be displayed. See also the documentation for rewrite.  File: acl2-doc-lemacs.info, Node: ACL2-PC||SKIP, Next: ACL2-PC||SL, Prev: ACL2-PC||SHOW-REWRITES, Up: PROOF-CHECKER ACL2-PC||SKIP (macro) "succeed" without doing anything Example and General Form: skip Make no change in the state-stack, but "succeed". Same as (sequence nil).  File: acl2-doc-lemacs.info, Node: ACL2-PC||SL, Next: ACL2-PC||SPLIT, Prev: ACL2-PC||SKIP, Up: PROOF-CHECKER ACL2-PC||SL (atomic macro) simplify with lemmas Examples: sl (sl 3) General Form: (sl &optional backchain-limit) Simplify, but with all function definitions disabled (*Note FUNCTION-THEORY:: in the top-level ACL2 loop), except for a few basic functions (the ones in *s-prop-theory*). If backchain-limit is supplied and not nil, then it should be a nonnegative integer; see (help s).  File: acl2-doc-lemacs.info, Node: ACL2-PC||SPLIT, Next: ACL2-PC||SR, Prev: ACL2-PC||SL, Up: PROOF-CHECKER ACL2-PC||SPLIT (atomic macro) split the current goal into cases Example: split For example, if the current goal has one hypothesis (or x y) and a conclusion of (and a b), then split will create four new goals: one with hypothesis X and conclusion A one with hypothesis X and conclusion B one with hypothesis Y and conclusion A one with hypothesis Y and conclusion B. General Form: SPLIT Replace the current goal by subgoals whose conjunction is equivalent (primarily by propositional reasoning) to the original goal, where each such goal cannot be similarly split. *Note:* The new goals will all have their hypotheses promoted; in particular, no conclusion will have a top function symbol of implies. Also note that split will fail if there is exactly one new goal created and it is the same as the existing current goal. The way split really works is to call the ACL2 theorem prover with only simplification (and preprocessing) turned on, and with only a few built-in functions (especially, propositional ones) enabled, namely, the ones in the list *s-prop-theory*. However, because the prover is called, type-set reasoning can be used to eliminate some cases. For example, if (true-listp x) is in the hypotheses, then probably (true-listp (cdr x)) will be reduced to t.  File: acl2-doc-lemacs.info, Node: ACL2-PC||SR, Next: ACL2-PC||SUCCEED, Prev: ACL2-PC||SPLIT, Up: PROOF-CHECKER ACL2-PC||SR (macro) same as SHOW-REWRITES Example: sr General Form: (sr &optional rule-id) See the documentation for show-rewrites, as sr and show-rewrites are identical.  File: acl2-doc-lemacs.info, Node: ACL2-PC||SUCCEED, Next: ACL2-PC||TH, Prev: ACL2-PC||SR, Up: PROOF-CHECKER ACL2-PC||SUCCEED (macro) run the given instructions, and "succeed" Example: (succeed induct p prove) General Form: (succeed &rest instruction-list) Run the indicated instructions until there is a hard "failure", and "succeed". (See the documentation for sequence for an explanation of "success" and "failure".)  File: acl2-doc-lemacs.info, Node: ACL2-PC||TH, Next: ACL2-PC||THEN, Prev: ACL2-PC||SUCCEED, Up: PROOF-CHECKER ACL2-PC||TH (macro) print the top-level hypotheses and the current subterm Examples: th -- print all (top-level) hypotheses and the current subterm (th (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4, and the current subterm (th (1 3) t) -- print hypotheses 1 and 3 and all governors, and the current subterm General Form: (th &optional hyps-indices govs-indices) Print hypotheses and the current subterm. The printing of hypotheses (and perhaps governors) are controlled as in the hyps command; see its documentation. Historical note: The name th is adapted from the Gypsy Verification Environment, where th abbreviates the command theorem, which says to print information on the current goal.  File: acl2-doc-lemacs.info, Node: ACL2-PC||THEN, Next: ACL2-PC||TOP, Prev: ACL2-PC||TH, Up: PROOF-CHECKER ACL2-PC||THEN (macro) apply one instruction to current goal and another to new subgoals Example: (then induct prove) General Form: (then first-instruction &optional completion must-succeed-flg) Run first-instruction, and then run completion (another instruction) on each subgoal created by first-instruction. If must-succeed-flg is supplied and not nil, then immediately remove the effects of each invocation of completion that "fails".  File: acl2-doc-lemacs.info, Node: ACL2-PC||TOP, Next: ACL2-PC||TYPE-ALIST, Prev: ACL2-PC||THEN, Up: PROOF-CHECKER ACL2-PC||TOP (atomic macro) move to the top of the goal Example and General Form: top For example, if the conclusion is (= x (* (- y) z)) and the current subterm is y, then after executing top, the current subterm will be the same as the conclusion, i.e., (= x (* (- y) z)). Top is the same as (up n), where n is the number of times one needs to execute up in order to get to the top of the conclusion. The top command fails if one is already at the top of the conclusion. See also up, dive, nx, and bk.  File: acl2-doc-lemacs.info, Node: ACL2-PC||TYPE-ALIST, Next: ACL2-PC||UNDO, Prev: ACL2-PC||TOP, Up: PROOF-CHECKER ACL2-PC||TYPE-ALIST (macro) display the type-alist from the current context Example and General Form: type-alist Display the current assumptions as a type-alist. Note that this display includes the result of forward chaining.  File: acl2-doc-lemacs.info, Node: ACL2-PC||UNDO, Next: ACL2-PC||UNSAVE, Prev: ACL2-PC||TYPE-ALIST, Up: PROOF-CHECKER ACL2-PC||UNDO (meta) undo some instructions Examples: (undo 7) undo General Forms: (undo n) -- Undo the last n instructions. The argument n should be a positive integer. undo -- Same as (undo 1). *Note:* To remove the effect of an undo command, use restore. See the documentation for details. *Note:* If the argument n is greater than the total number of interactive instructions in the current session, then (undo n) will simply take you back to the start of the session. The undo meta command always "succeeds"; it returns (mv nil t state) unless its optional argument is supplied and of the wrong type (i.e. not a positive integer) or there are no instructions to undo.  File: acl2-doc-lemacs.info, Node: ACL2-PC||UNSAVE, Next: ACL2-PC||UP, Prev: ACL2-PC||UNDO, Up: PROOF-CHECKER ACL2-PC||UNSAVE (macro) remove a proof-checker state Example: (unsave assoc-of-append) General Form: (unsave &optional name) Eliminates the association of a proof-checker state with name, if name is supplied and not nil. The name may be nil or not supplied, in which case it defaults to the event name supplied with the original call to verify (if there is one -- otherwise, the instruction "fails" and there is no change). The ACL2 function unsave may also be executed outside the interactive loop, with the same syntax. See also documentation for save and retrieve.  File: acl2-doc-lemacs.info, Node: ACL2-PC||UP, Next: ACL2-PC||USE, Prev: ACL2-PC||UNSAVE, Up: PROOF-CHECKER ACL2-PC||UP (primitive) move to the parent (or some ancestor) of the current subterm Examples: if the conclusion is (= x (* (- y) z)) and the current subterm is y, then we have: up or (up 1) -- the current subterm becomes (- y) (up 2) -- the current subterm becomes (* (- y) z) (up 3) -- the current subterm becomes the entire conclusion (up 4) -- no change; can't go up that many levels General Form: (up &optional n) Move up n levels in the conclusion from the current subterm, where n is a positive integer. If n is not supplied or is nil, then move up 1 level, i.e., treat the instruction as (up 1). See also dive, top, nx, and bk.  File: acl2-doc-lemacs.info, Node: ACL2-PC||USE, Next: ACL2-PC||X, Prev: ACL2-PC||UP, Up: PROOF-CHECKER ACL2-PC||USE (atomic macro) use a lemma instance Example: (USE true-listp-append (:instance assoc-of-append (x a) (y b) (z c))) -- Add two top-level hypotheses, one the lemma called true-listp-append, and the other an instance of the lemma called assoc-of-append by the substitution in which x is assigned a, y is assigned b, and z is assigned c. General Form: (use &rest args) Add the given lemma instances to the list of top-level hypotheses. *Note HINTS:: for the syntax of :use hints in defthm, which is essentially the same as the syntax here (see the example above). This command calls the prove command, and hence should only be used at the top of the conclusion.  File: acl2-doc-lemacs.info, Node: ACL2-PC||X, Next: ACL2-PC||X-DUMB, Prev: ACL2-PC||USE, Up: PROOF-CHECKER ACL2-PC||X (atomic macro) expand and (maybe) simplify function call at the current subterm Examples: x -- expand and simplify. For example, if the current subterm is (append a b), then after x the current subterm will probably be (cons (car a) (append (cdr a) b)) if (consp a) and (true-listp a) are among the top-level hypotheses and governors. If there are no top-level hypotheses and governors, then after x the current subterm will probably be: (if (true-listp x) (if x (cons (car x) (append (cdr x) y)) y) (apply 'binary-append (list x y))). General Form: (X &key rewrite normalize backchain-limit in-theory hands-off expand) Expand the function call at the current subterm, and simplify using the same conventions as with the s command (see documentation for s). Unlike s, it is permitted to set both :rewrite and :normalize to nil, which will result in no simplification; see x-dumb. *Note* (obscure): On rare occasions the current address may be affected by the use of x. For example, suppose we have the definition (defun g (x) (if (consp x) x 3)) and then we enter the proof-checker with (verify (if (integerp x) (equal (g x) 3) t)) . Then after invoking the instruction (dive 2 1), so that the current subterm is (g x), followed by the instruction x, we would expect the conclusion to be (if (integerp x) (equal 3 3) t). However, the system actually replaces (equal 3 3) with t (because we use the ACL2 term-forming primitives), and hence the conclusion is actually (if (integerp x) (equal 3 3) t). Therefore, the current address is put at (2) rather than (2 1). In such cases, a warning "NOTE" will be printed to the terminal. The other primitive commands to which the above "truncation" note applies are equiv, rewrite, and s.  File: acl2-doc-lemacs.info, Node: ACL2-PC||X-DUMB, Next: DEFINE-PC-HELP, Prev: ACL2-PC||X, Up: PROOF-CHECKER ACL2-PC||X-DUMB (atomic macro) expand function call at the current subterm, without simplifying Example: x-dumb: expand without simplification. General Form: (x-dumb &optional new-goals-flg keep-all-guards-flg) Same as (expand t new-goals-flg keep-all-guards-flg). See documentation for expand. See also x, which allows simplification.