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: ZP, Prev: ZIP, Up: PROGRAMMING ZP testing a "natural" against 0 (Zp n) is logically equivalent to (equal (nfix n) 0) and is the preferred termination test for recursion down the natural numbers. (Zp n) returns t if n is 0 or not a natural number; it returns nil otherwise. Thus, in the ACL2 logic (ignoring the issue of guards): n (zp n) 3 nil 0 t -1 t 5/2 t #c(1 3) t 'abc t (Zp n) has a guard requiring n to be a natural number. For a discussion of the various idioms for testing against 0, *Note ZERO-TEST-IDIOMS::. Zp is typically used as the termination test in recursions down the natural numbers. It has the advantage of "coercing" its argument to a natural and hence allows the definition to be admitted without an explicit type check in the body. Guard verification allows zp to be compiled as a direct =-comparision with 0.  File: acl2-doc-lemacs.info, Node: PROOF-CHECKER, Next: PROOF-TREE, Prev: PROGRAMMING, Up: Top PROOF-CHECKER support for low-level interaction Call this up with (verify ...). * Menu: * ACL2-PC||=:: (atomic macro) attempt an equality (or equivalence) substitution * ACL2-PC||ACL2-WRAP:: (macro) same as (lisp x) * ACL2-PC||ADD-ABBREVIATION:: (primitive) add an abbreviation * ACL2-PC||BASH:: (atomic macro) call the ACL2 theorem prover's simplifier * ACL2-PC||BDD:: (atomic macro) prove the current goal using bdds * ACL2-PC||BK:: (atomic macro) move backward one argument in the enclosing term * ACL2-PC||BOOKMARK:: (macro) insert matching "bookends" comments * ACL2-PC||CASESPLIT:: (primitive) split into two cases * ACL2-PC||CG:: (macro) change to another goal. * ACL2-PC||CHANGE-GOAL:: (primitive) change to another goal. * ACL2-PC||CLAIM:: (atomic macro) add a new hypothesis * ACL2-PC||COMM:: (macro) display instructions from the current interactive session * ACL2-PC||COMMANDS:: (macro) display instructions from the current interactive session * ACL2-PC||COMMENT:: (primitive) insert a comment * ACL2-PC||CONTRADICT:: (macro) same as contrapose * ACL2-PC||CONTRAPOSE:: (primitive) switch a hypothesis with the conclusion, negating both * ACL2-PC||DEMOTE:: (primitive) move top-level hypotheses to the conclusion * ACL2-PC||DIVE:: (primitive) move to the indicated subterm * ACL2-PC||DO-ALL:: (macro) run the given instructions * ACL2-PC||DO-ALL-NO-PROMPT:: (macro) run the given instructions, halting once there is a "failure" * ACL2-PC||DO-STRICT:: (macro) run the given instructions, halting once there is a "failure" * ACL2-PC||DROP:: (primitive) drop top-level hypotheses * ACL2-PC||DV:: (atomic macro) move to the indicated subterm * ACL2-PC||ELIM:: (atomic macro) call the ACL2 theorem prover's elimination process * ACL2-PC||EQUIV:: (primitive) attempt an equality (or congruence-based) substitution * ACL2-PC||EX:: (macro) exit after possibly saving the state * ACL2-PC||EXIT:: (meta) exit the interactive proof-checker * ACL2-PC||EXPAND:: (primitive) expand the current function call without simplification * ACL2-PC||FAIL:: (macro) cause a failure * ACL2-PC||FORWARDCHAIN:: (atomic macro) forward chain from an implication in the hyps * ACL2-PC||FREE:: (atomic macro) create a "free variable" * ACL2-PC||GENERALIZE:: (primitive) perform a generalization * ACL2-PC||GOALS:: (macro) list the names of goals on the stack * ACL2-PC||HELP:: (macro) proof-checker help facility * ACL2-PC||HELP!:: (macro) proof-checker help facility * ACL2-PC||HELP-LONG:: (macro) same as help! * ACL2-PC||HYPS:: (macro) print the hypotheses * ACL2-PC||ILLEGAL:: (macro) illegal instruction * ACL2-PC||IN-THEORY:: (primitive) set the current proof-checker theory * ACL2-PC||INDUCT:: (atomic macro) generate subgoals using induction * ACL2-PC||LISP:: (meta) evaluate the given form in Lisp * ACL2-PC||MORE:: (macro) proof-checker help facility * ACL2-PC||MORE!:: (macro) proof-checker help facility * ACL2-PC||NEGATE:: (macro) run the given instructions, and "succeed" if and only if they "fail" * ACL2-PC||NIL:: (macro) used for interpreting control-d * ACL2-PC||NOISE:: (meta) run instructions with output * ACL2-PC||NX:: (atomic macro) move forward one argument in the enclosing term * ACL2-PC||ORELSE:: (macro) run the first instruction; if (and only if) it "fails", run the second * ACL2-PC||P:: (macro) prettyprint the current term * ACL2-PC||P-TOP:: (macro) prettyprint the conclusion, highlighting the current term * ACL2-PC||PP:: (macro) prettyprint the current term * ACL2-PC||PRINT:: (macro) print the result of evaluating the given form * ACL2-PC||PRINT-ALL-GOALS:: (macro) print all the (as yet unproved) goals * ACL2-PC||PRINT-MAIN:: (macro) print the original goal * ACL2-PC||PRO:: (atomic macro) repeatedly apply promote * ACL2-PC||PROMOTE:: (primitive) move antecedents of conclusion's implies term to top-level hypotheses * ACL2-PC||PROTECT:: (macro) run the given instructions, reverting to existing state upon failure * ACL2-PC||PROVE:: (primitive) call the ACL2 theorem prover to prove the current goal * ACL2-PC||PUT:: (macro) substitute for a "free variable" * ACL2-PC||QUIET:: (meta) run instructions without output * ACL2-PC||R:: (macro) same as rewrite * ACL2-PC||REDUCE:: (atomic macro) call the ACL2 theorem prover's simplifier * ACL2-PC||REDUCE-BY-INDUCTION:: (macro) call the ACL2 prover without induction, after going into induction * ACL2-PC||REMOVE-ABBREVIATIONS:: (primitive) remove one or more abbreviations * ACL2-PC||REPEAT:: (macro) repeat the given instruction until it "fails" * ACL2-PC||REPEAT-REC:: (macro) auxiliary to repeat * ACL2-PC||REPLAY:: (macro) replay one or more instructions * ACL2-PC||RESTORE:: (meta) remove the effect of an UNDO command * ACL2-PC||RETAIN:: (atomic macro) drop all *but* the indicated top-level hypotheses * ACL2-PC||RETRIEVE:: (macro) re-enter the proof-checker * ACL2-PC||REWRITE:: (primitive) apply a rewrite rule * ACL2-PC||RUN-INSTR-ON-GOAL:: (macro) auxiliary toxae THEN * ACL2-PC||RUN-INSTR-ON-NEW-GOALS:: (macro) auxiliary to then * ACL2-PC||S:: (primitive) simplify the current subterm * ACL2-PC||S-PROP:: (atomic macro) simplify propositionally * ACL2-PC||SAVE:: (macro) save the proof-checker state (state-stack) * ACL2-PC||SEQUENCE:: (meta) run the given list of instructions according to a multitude of options * ACL2-PC||SHOW-ABBREVIATIONS:: (macro) display the current abbreviations * ACL2-PC||SHOW-REWRITES:: (macro) display the applicable rewrite rules * ACL2-PC||SKIP:: (macro) "succeed" without doing anything * ACL2-PC||SL:: (atomic macro) simplify with lemmas * ACL2-PC||SPLIT:: (atomic macro) split the current goal into cases * ACL2-PC||SR:: (macro) same as SHOW-REWRITES * ACL2-PC||SUCCEED:: (macro) run the given instructions, and "succeed" * ACL2-PC||TH:: (macro) print the top-level hypotheses and the current subterm * ACL2-PC||THEN:: (macro) apply one instruction to current goal and another to new subgoals * ACL2-PC||TOP:: (atomic macro) move to the top of the goal * ACL2-PC||TYPE-ALIST:: (macro) display the type-alist from the current context * ACL2-PC||UNDO:: (meta) undo some instructions * ACL2-PC||UNSAVE:: (macro) remove a proof-checker state * ACL2-PC||UP:: (primitive) move to the parent (or some ancestor) of the current subterm * ACL2-PC||USE:: (atomic macro) use a lemma instance * ACL2-PC||X:: (atomic macro) expand and (maybe) simplify function call at the current subterm * ACL2-PC||X-DUMB:: (atomic macro) expand function call at the current subterm, without simplifying * DEFINE-PC-HELP:: define a macro command whose purpose is to print something * INSTRUCTIONS:: instructions to the proof checker * MACRO-COMMAND:: compound command for the proof-checker * RETRIEVE:: re-enter a (specified) proof-checker state * TOGGLE-PC-MACRO:: change an ordinary macro command to an atomic macro, or vice-versa * UNSAVE:: remove a proof-checker state * VERIFY:: enter the interactive proof checker This is an interactive system for checking theorems in ACL2. One enters it using VERIFY; *Note VERIFY::. The result of an interactive session is a defthm event with an :instructions parameter supplied. Such an event can be replayed later in a new ACL2 session with the "proof-checker" loaded. Individual proof-checker commands have already been listed above. Among them are proof-checker commands help, help-long, more, and more!, which behave respectively like the ACL2 functions :doc, :doc!, :more, and :more!.  File: acl2-doc-lemacs.info, Node: ACL2-PC||=, Next: ACL2-PC||ACL2-WRAP, Prev: PROOF-CHECKER, Up: PROOF-CHECKER ACL2-PC||= (atomic macro) attempt an equality (or equivalence) substitution Examples: = -- replace the current subterm by a term equated to it in one of the hypotheses (if such a term exists) (= x) -- replace the current subterm by x, assuming that the prover can show that they are equal (= (+ x y) z) -- replace the term (+ x y) by the term z inside the current subterm, assuming that the prover can prove (equal (+ x y) z) from the current top-level hypotheses or that this term or (equal z (+ x y)) is among the current top-level hypotheses or the current governors (= & z) -- exactly the same as above, if (+ x y) is the current subterm (= (+ x y) z :hints :none) -- same as (= (+ x y) z), except that a new subgoal is created with the current goal's hypotheses and governors as its top-level hypotheses and (equal (+ x y) z) as its conclusion (= (+ x y) z 0) -- exactly the same as immediately above (= (p x) (p y) :equiv iff :otf-flg t :hints (("Subgoal 2" :BY FOO) ("Subgoal 1" :use bar))) -- same as (= (+ x y) z), except that the prover uses the indicated values for otf-flg and hints, and only propositional (iff) equivalence is used (however, it must be that only propositional equivalence matters at the current subterm) General Form: (= &optional x y &rest keyword-args) If terms x and y are supplied, then replace x by y inside the current subterm if they are "known" to be "equal". Here "known" means the following: the prover is called as in the prove command (using keyword-args) to prove (equal x y), except that a keyword argument :equiv is allowed, in which case (equiv x y) is proved instead, where equiv is that argument. (See below for how governors are handled.) Actually, keyword-args is either a single non-keyword or is a list of the form ((kw-1 x-1) ... (kw-n x-n)), where each kw-i is one of the keywords :equiv, :otf-flg, :hints. Here :equiv defaults to equal if the argument is not supplied or is nil, and otherwise should be the name of an ACL2 equivalence relation. :Otf-flg and :hints give directives to the prover, as explained above and in the documentation for the prove command; however, no prover call is made if :hints is a non-nil atom or if keyword-args is a single non-keyword (more on this below). *Remarks on defaults* (1) If there is only one argument, say a, then x defaults to the current subterm, in the sense that x is taken to be the current subterm and y is taken to be a. (2) If there are at least two arguments, then x may be the symbol &, which then represents the current subterm. Thus, (= a) is equivalent to (= & a). (Obscure point: actually, & can be in any package, except the keyword package.) (3) If there are no arguments, then we look for a top-level hypothesis or a governor of the form (equal c u) or (equal u c), where c is the current subterm. In that case we replace the current subterm by u. As with the prove command, we allow goals to be given "bye"s in the proof, which may be generated by a :hints keyword argument in keyword-args. These result in the creation of new subgoals. A proof is attempted unless the :hints argument is a non-nil atom other than :none, or unless there is one element of keyword-args and it is not a keyword. In that case, if there are any hypotheses in the current goal, then what is attempted is a proof of the implication whose antecedent is the conjunction of the current hypotheses and governors and whose conclusion is the appropriate equal term. *Notes:* (1) It is allowed to use abbreviations in the hints. (2) The keyword :none has the special role as a value of :hints that is shown clearly in an example above. (3) If there are governors, then the new subgoal has as additional hypotheses the current governors.  File: acl2-doc-lemacs.info, Node: ACL2-PC||ACL2-WRAP, Next: ACL2-PC||ADD-ABBREVIATION, Prev: ACL2-PC||=, Up: PROOF-CHECKER ACL2-PC||ACL2-WRAP (macro) same as (lisp x) Example: (acl2-wrap (pe :here)) General Form: (acl2-wrap form) Same as (lisp form). This is provided for interface tools that want to be able to execute the same form in raw Lisp, in the proof-checker, or in the ACL2 top-level loop (lp).  File: acl2-doc-lemacs.info, Node: ACL2-PC||ADD-ABBREVIATION, Next: ACL2-PC||BASH, Prev: ACL2-PC||ACL2-WRAP, Up: PROOF-CHECKER ACL2-PC||ADD-ABBREVIATION (primitive) add an abbreviation Example: (add-abbreviation v (* x y)) causes future occurrences of (* x y) to be printed as (? v), until (unless) a corresponding invocation of remove-abbreviations occurs. In this case we say that v "abbreviates" (* x y). General Form: (add-abbreviation var &optional raw-term) Let var be an abbreviation for raw-term, if raw-term is supplied, else for the current subterm. Note that var must be a variable that does not already abbreviate some term. A way to think of abbreviations is as follows. Imagine that whenever an abbreviation is added, say v abbreviates expr, an entry associating v to expr is made in an association list, which we will call "*abbreviations-alist*". Then simply imagine that ? is a function defined by something like: (defun ? (v) (let ((pair (assoc v *abbreviations-alist*))) (if pair (cdr pair) (error ...)))) Of course the implementation isn't exactly like that, since the "constant" *abbreviations-alist* actually changes each time an add-abbreviation instruction is successfully invoked. Nevertheless, if one imagines an appropriate redefinition of the "constant" *abbreviations-alist* each time an add-abbreviation is invoked, then one will have a clear model of the meaning of such an instruction. The effect of abbreviations on output is that before printing a term, each subterm that is abbreviated by a variable v is first replaced by (? v). The effect of abbreviations on input is that every built-in proof-checker command accepts abbreviations wherever a term is expected as an argument, i.e., accepts the syntax (? v) whenever v abbreviates a term. For example, the second argument of add-abbreviation may itself use abbreviations that have been defined by previous add-abbreviation instructions. See also remove-abbreviations and show-abbreviations.  File: acl2-doc-lemacs.info, Node: ACL2-PC||BASH, Next: ACL2-PC||BDD, Prev: ACL2-PC||ADD-ABBREVIATION, Up: PROOF-CHECKER ACL2-PC||BASH (atomic macro) call the ACL2 theorem prover's simplifier Examples: bash -- attempt to prove the current goal by simplification alone (bash ("Subgoal 2" :by foo) ("Subgoal 1" :use bar)) -- attempt to prove the current goal by simplification alone, with the indicated hints General Form: (bash &rest hints) Call the theorem prover's simplifier, creating a subgoal for each resulting goal. Notice that unlike prove, the arguments to bash are spread out, and are all hints. *Note:* All forcing rounds will be skipped (unless there are more than 15 subgoals generated in the first forcing round, an injustice that should be rectified by the next release).  File: acl2-doc-lemacs.info, Node: ACL2-PC||BDD, Next: ACL2-PC||BK, Prev: ACL2-PC||BASH, Up: PROOF-CHECKER ACL2-PC||BDD (atomic macro) prove the current goal using bdds Examples: bdd (bdd :vars nil :bdd-constructors (cons) :prove t :literal :all) The general form is as shown in the latter example above, but with any keyword-value pairs omitted and with values as described for the :bdd hint; *Note HINTS::. This command simply calls the theorem prover with the indicated bdd hint for the top-level goal. Note that if :prove is t (the default), then the proof will succeed entirely using bdds or else it will fail immediately. *Note BDD::.  File: acl2-doc-lemacs.info, Node: ACL2-PC||BK, Next: ACL2-PC||BOOKMARK, Prev: ACL2-PC||BDD, Up: PROOF-CHECKER ACL2-PC||BK (atomic macro) move backward one argument in the enclosing term Example and General Form: bk For example, if the conclusion is (= x (* (- y) z)) and the current subterm is (* (- y) z), then after executing bk, the current subterm will be x. Move to the previous argument of the enclosing term. 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||BOOKMARK, Next: ACL2-PC||CASESPLIT, Prev: ACL2-PC||BK, Up: PROOF-CHECKER ACL2-PC||BOOKMARK (macro) insert matching "bookends" comments Example: (bookmark final-goal) General Form: (bookmark name &rest instruction-list) Run the instructions in instruction-list (as though this were a call of do-all; see the documentation for do-all), but first insert a begin bookend with the given name and then, when the instructions have been completed, insert an end bookend with that same name. See the documentation of comm for an explanation of bookends and how they can affect the display of instructions.  File: acl2-doc-lemacs.info, Node: ACL2-PC||CASESPLIT, Next: ACL2-PC||CG, Prev: ACL2-PC||BOOKMARK, Up: PROOF-CHECKER ACL2-PC||CASESPLIT (primitive) split into two cases Example: (casesplit (< x y)) -- assuming that we are at the top of the conclusion, add (< x y) as a new top-level hypothesis in the current goal, and create a subgoal identical to the current goal except that it has (not (< x y)) as a new top-level hypothesis General Form: (casesplit expr &optional use-hyps-flag do-not-flatten-flag) When the current subterm is the entire conclusion, this instruction adds expr as a new top-level hypothesis, and create a subgoal identical to the existing current goal except that it has the negation of expr as a new top-level hypothesis. See also claim. The optional arguments control the use of governors and the "flattening" of new hypotheses, as we now explain. The argument use-hyps-flag is only of interest when there are governors. (To read about governors, see the documentation for the command hyps). In that case, if use-hyps-flag is not supplied or is nil, then the description above is correct; but otherwise, it is not expr but rather it is (implies govs expr) that is added as a new top-level hypothesis (and whose negation is added as a top-level hypothesis for the new goal), where govs is the conjunction of the governors. If do-not-flatten-flag is supplied and not nil, then that is all there is to this command. Otherwise (thus this is the default), when the claimed term (first argument) is a conjunction (and) of terms and the claim instruction succeeds, then each (nested) conjunct of the claimed term is added as a separate new top-level hypothesis. Consider the following example, assuming there are no governors. (casesplit (and (and (< x y) (integerp a)) (equal r s)) t) Three new top-level hypotheses are added to the current goal, namely (< x y), (integerp a), and (equal r s). In that case, only one hypothesis is added to create the new goal, namely the negation of (and (< x y) (integerp a) (equal r s)). If the negation of this term had been claimed, then it would be the other way around: the current goal would get a single new hypothesis while the new goal would be created by adding three hypotheses. *Note:* It is allowed to use abbreviations in the hints.  File: acl2-doc-lemacs.info, Node: ACL2-PC||CG, Next: ACL2-PC||CHANGE-GOAL, Prev: ACL2-PC||CASESPLIT, Up: PROOF-CHECKER ACL2-PC||CG (macro) change to another goal. Examples: (cg (main . 1)) -- change to the goal (main . 1) cg -- change to the next-to-top goal General Form: (CG &OPTIONAL goal-name) Same as (change-goal goal-name t), i.e. change to the indicated and move the current goal to the end of the goal stack.  File: acl2-doc-lemacs.info, Node: ACL2-PC||CHANGE-GOAL, Next: ACL2-PC||CLAIM, Prev: ACL2-PC||CG, Up: PROOF-CHECKER ACL2-PC||CHANGE-GOAL (primitive) change to another goal. Examples: (change-goal (main . 1)) -- change to the goal (main . 1) change-goal -- change to the next-to-top goal General Form: (change-goal &optional goal-name end-flg) Change to the goal with the name goal-name, i.e. make it the current goal. However, if goal-name is nil or is not supplied, then it defaults to the next-to-top goal, i.e., the second goal in the stack of goals. If end-flg is supplied and not nil, then move the current goal to the end of the goal stack; else merely swap it with the next-to-top goal. Also see documentation for cg.  File: acl2-doc-lemacs.info, Node: ACL2-PC||CLAIM, Next: ACL2-PC||COMM, Prev: ACL2-PC||CHANGE-GOAL, Up: PROOF-CHECKER ACL2-PC||CLAIM (atomic macro) add a new hypothesis Examples: (claim (< x y)) -- attempt to prove (< x y) from the current top-level hypotheses and if successful, then add (< x y) as a new top-level hypothesis in the current goal (claim (< x y) :otf-flg t :hints (("Goal" :induct t))) -- as above, but call the prover using the indicated values for the otf-flg and hints (claim (< x y) 0) -- as above, except instead of attempting to prove (< x y), create a new subgoal with the same top-level hypotheses as the current goal that has (< x y) as its conclusion (claim (< x y) :hints :none) -- same as immediately above General Form: (claim expr &rest rest-args) This command creates a new subgoal with the same top-level hypotheses as the current goal but with a conclusion of expr. If rest-args is a non-empty list headed by a non-keyword, then there will be no proof attempted for the new subgoal. With that possible exception, rest-args should consist of keyword arguments. The keyword argument :do-not-flatten controls the "flattening" of new hypotheses, just as with the casesplit command (as described in its documentation). The remaining rest-args are used with a call the prove command on the new subgoal, except that if :hints is a non-nil atom, then the prover is not called -- rather, this is the same as the situation described above, where rest-args is a non-empty list headed by a non-keyword. *Notes:* (1) Unlike the casesplit command, the claim command is completely insensitive to governors. (2) It is allowed to use abbreviations in the hints. (3) The keyword :none has the special role as a value of :hints that is shown clearly in an example above.  File: acl2-doc-lemacs.info, Node: ACL2-PC||COMM, Next: ACL2-PC||COMMANDS, Prev: ACL2-PC||CLAIM, Up: PROOF-CHECKER ACL2-PC||COMM (macro) display instructions from the current interactive session Examples: comm (comm 10) General Form: (comm &optional n) Prints out instructions in reverse order. This is actually the same as (commands n t) -- or, (commands nil t) if n is not supplied. As explained in the documentation for commands, the final argument of t causes suppression of instructions occurring between so-called "matching bookends," which we now explain. A "begin bookend" is an instruction of the form (COMMENT :BEGIN x . y). Similarly, an "end bookend" is an instruction of the form (COMMENT :END x' . y'). The "name" of the first bookend is x and the "name" of the second bookend is x'. When such a pair of instructions occurs in the current state-stack, we call them "matching bookends" provided that they have the same name (i.e. x equals x') and if no other begin or end bookend with name x occurs between them. The idea now is that comm hides matching bookends together with the instructions they enclose. Here is a more precise explanation of this "hiding"; probably there is no value in reading on! A comm instruction hides bookends in the following manner. (So does a comment instruction when its second optional argument is supplied and non-nil.) First, if the first argument n is supplied and not nil, then we consider only the last n instructions from the state-stack; otherwise, we consider them all. Now the resulting list of instructions is replaced by the result of applying the following process to each pair of matching bookends: the pair is removed, together with everything in between the begin and end bookend of the pair, and all this is replaced by the "instruction" ("***HIDING***" :COMMENT :BEGIN name ...) where (comment begin name ...) is the begin bookend of the pair. Finally, after applying this process to each pair of matching bookends, each begin bookend of the form (comment begin name ...) that remains is replaced by ("***UNFINISHED***" :COMMENT :BEGIN name ...) .  File: acl2-doc-lemacs.info, Node: ACL2-PC||COMMANDS, Next: ACL2-PC||COMMENT, Prev: ACL2-PC||COMM, Up: PROOF-CHECKER ACL2-PC||COMMANDS (macro) display instructions from the current interactive session Examples: commands (commands 10 t) General Forms: commands or (commands nil) Print out all the instructions (in the current state-stack) in reverse order, i.e. from the most recent instruction to the starting instruction. (commands n) [n a positive integer] Print out the most recent n instructions (in the current state-stack), in reverse order. (commands x abbreviate-flag) Same as above, but if abbreviate-flag is non-NIL, then do not display commands between "matching bookends". See documentation for comm for an explanation of matching bookends. *Note*: If there are more than n instructions in the state-stack, then (commands n) is the same as commands (and also, (commands n abb) is the same as (commands nil abb)).  File: acl2-doc-lemacs.info, Node: ACL2-PC||COMMENT, Next: ACL2-PC||CONTRADICT, Prev: ACL2-PC||COMMANDS, Up: PROOF-CHECKER ACL2-PC||COMMENT (primitive) insert a comment Example: (comment now begin difficult final goal) General Form: (comment &rest x) This instruction makes no change in the state except to insert the comment instruction. Some comments can be used to improve the display of commands; see documentation for comm.  File: acl2-doc-lemacs.info, Node: ACL2-PC||CONTRADICT, Next: ACL2-PC||CONTRAPOSE, Prev: ACL2-PC||COMMENT, Up: PROOF-CHECKER ACL2-PC||CONTRADICT (macro) same as contrapose see documentation for contrapose  File: acl2-doc-lemacs.info, Node: ACL2-PC||CONTRAPOSE, Next: ACL2-PC||DEMOTE, Prev: ACL2-PC||CONTRADICT, Up: PROOF-CHECKER ACL2-PC||CONTRAPOSE (primitive) switch a hypothesis with the conclusion, negating both Example: (contrapose 3) General Form: (contrapose &optional n) The (optional) argument n should be a positive integer that does not exceed the number of hypotheses. Negate the current conclusion and make it the nth hypothesis, while negating the current nth hypothesis and making it the current conclusion. If no argument is supplied then the effect is the same as for (contrapose 1). *Note:* By "negate" we mean an operation that replaces nil by t, x by nil for any other explicit value x, (not x) by x, and any other x by (not x).  File: acl2-doc-lemacs.info, Node: ACL2-PC||DEMOTE, Next: ACL2-PC||DIVE, Prev: ACL2-PC||CONTRAPOSE, Up: PROOF-CHECKER ACL2-PC||DEMOTE (primitive) move top-level hypotheses to the conclusion Examples: demote -- demote all top-level hypotheses (demote 3 5) -- demote hypotheses 3 and 5 For example, if the top-level hypotheses are x and y and the conclusion is z, then after execution of demote, the conclusion will be (implies (and x y) z) and there will be no (top-level) hypotheses. General Form: (demote &rest hyps-indices) Eliminate the indicated (top-level) hypotheses, but replace the conclusion conc with (implies hyps conc) where hyps is the conjunction of the hypotheses that were eliminated. If no arguments are supplied, then all hypotheses are demoted, i.e. demote is the same as (demote 1 2 ... n) where n is the number of top-level hypotheses. *Note*: You must be at the top of the conclusion in order to use this command. Otherwise, first invoke top. Also, demote fails if there are no top-level hypotheses or if indices are supplied that are out of range.  File: acl2-doc-lemacs.info, Node: ACL2-PC||DIVE, Next: ACL2-PC||DO-ALL, Prev: ACL2-PC||DEMOTE, Up: PROOF-CHECKER ACL2-PC||DIVE (primitive) move to the indicated subterm Examples: (DIVE 1) -- assign the new current subterm to be the first argument of the existing current subterm (DIVE 1 2) -- assign the new current subterm to be the result of first taking the 1st argument of the existing current subterm, and then the 2nd argument of that For example, if the current subterm is (* (+ a b) c), then after (dive 1) it is (+ a b). If after that, then (dive 2) is invoked, the new current subterm will be b. Instead of (dive 1) followed by (dive 2), the same current subterm could be obtained by instead submitting the single instruction (dive 1 2). General Form: (dive &rest naturals-list) If naturals-list is a non-empty list (n_1 ... n_k) of natural numbers, let the new current subterm be the result of selecting the n_1-st argument of the current subterm, and then the n_2-th subterm of that, ..., finally the n_k-th subterm. *Note:* Dive is related to the command pp, in that the diving is done according to raw (translated, internal form) syntax. Use the command dv if you want to dive according to the syntax displayed by the command p. Note that (dv n) can be abbreviated by simply n.  File: acl2-doc-lemacs.info, Node: ACL2-PC||DO-ALL, Next: ACL2-PC||DO-ALL-NO-PROMPT, Prev: ACL2-PC||DIVE, Up: PROOF-CHECKER ACL2-PC||DO-ALL (macro) run the given instructions Example: (do-all induct p prove) General Form: (do-all &rest instruction-list) Run the indicated instructions until there is a hard "failure". The instruction "succeeds" if and only if each instruction in instruction-list does. (See the documentation for sequence for an explanation of "success" and "failure.") As each instruction is executed, the system will print the usual prompt followed by that instruction, unless the global state variable print-prompt-and-instr-flg is nil. *Note:* If do-all "fails", then the failure is hard if and only if the last instruction it runs has a hard "failure". Obscure point: For the record, (do-all ins_1 ins_2 ... ins_k) is the same as (sequence (ins_1 ins_2 ... ins_k)).  File: acl2-doc-lemacs.info, Node: ACL2-PC||DO-ALL-NO-PROMPT, Next: ACL2-PC||DO-STRICT, Prev: ACL2-PC||DO-ALL, Up: PROOF-CHECKER ACL2-PC||DO-ALL-NO-PROMPT (macro) run the given instructions, halting once there is a "failure" Example: (do-all-no-prompt induct p prove) General Form: (do-all-no-prompt &rest instruction-list) Do-all-no-prompt is the same as do-all, except that the prompt and instruction are not printed each time, regardless of the value of print-prompt-and-instr-flg. Also, restoring is disabled. See the documentation for do-all.  File: acl2-doc-lemacs.info, Node: ACL2-PC||DO-STRICT, Next: ACL2-PC||DROP, Prev: ACL2-PC||DO-ALL-NO-PROMPT, Up: PROOF-CHECKER ACL2-PC||DO-STRICT (macro) run the given instructions, halting once there is a "failure" Example: (do-strict induct p prove) General Form: (do-strict &rest instruction-list) Run the indicated instructions until there is a (hard or soft) "failure". In fact do-strict is identical in effect to do-all, except that do-all only halts once there is a hard "failure". See the documentation for do-all.  File: acl2-doc-lemacs.info, Node: ACL2-PC||DROP, Next: ACL2-PC||DV, Prev: ACL2-PC||DO-STRICT, Up: PROOF-CHECKER ACL2-PC||DROP (primitive) drop top-level hypotheses Examples: (drop 2 3) -- drop the second and third hypotheses drop -- drop all top-level hypotheses General Forms: (drop n1 n2 ...) -- Drop the hypotheses with the indicated indices. drop -- Drop all the top-level hypotheses. *Note:* If there are no top-level hypotheses, then the instruction drop will fail. If any of the indices is out of range, i.e. is not an integer between one and the number of top-level hypotheses (inclusive), then (drop n1 n2 ...) will fail.  File: acl2-doc-lemacs.info, Node: ACL2-PC||DV, Next: ACL2-PC||ELIM, Prev: ACL2-PC||DROP, Up: PROOF-CHECKER ACL2-PC||DV (atomic macro) move to the indicated subterm Examples: (dv 1) -- assign the new current subterm to be the first argument of the existing current subterm (dv 1 2) -- assign the new current subterm to be the result of first taking the 1st argument of the existing current subterm, and then the 2nd argument of that For example, if the current subterm is (* (+ a b) c), then after (dv 1) it is (+ a b). If after that, then (dv 2) is invoked, the new current subterm will be b. Instead of (dv 1) followed by (dv 2), the same current subterm could be obtained by instead submitting the single instruction (dv 1 2). General Form: (dv &rest naturals-list) If naturals-list is a non-empty list (n_1 ... n_k) of natural numbers, let the new current subterm be the result of selecting the n_1-st argument of the current subterm, and then the n_2-th subterm of that, ..., finally the n_k-th subterm. *Note:* (dv n) may be abbreviated by simply n, so we could have typed 1 instead of (dv 1) in the first example above. *Note:* See also dive, which is related to the command pp, in that the diving is done according to raw (translated, internal form) syntax. Use the command dv if you want to dive according to the syntax displayed by the command p.  File: acl2-doc-lemacs.info, Node: ACL2-PC||ELIM, Next: ACL2-PC||EQUIV, Prev: ACL2-PC||DV, Up: PROOF-CHECKER ACL2-PC||ELIM (atomic macro) call the ACL2 theorem prover's elimination process Example and General Form: elim Upon running the elim command, the system will create a subgoal will be created for each goal that would have been pushed for proof by induction in an ordinary proof, where *only* elimination is used; not even simplification is used!  File: acl2-doc-lemacs.info, Node: ACL2-PC||EQUIV, Next: ACL2-PC||EX, Prev: ACL2-PC||ELIM, Up: PROOF-CHECKER ACL2-PC||EQUIV (primitive) attempt an equality (or congruence-based) substitution Examples: (equiv (* x y) 3) -- replace (* x y) by 3 everywhere inside the current subterm, if their equality is among the top-level hypotheses or the governors (equiv x t iff) -- replace x by t everywhere inside the current subterm, where only propositional equivalence needs to be maintained at each occurrence of x General form: (equiv old new &optional relation) Substitute new for old everywhere inside the current subterm, provided that either (relation old new) or (relation new old) is among the top-level hypotheses or the governors (possibly by way of backchaining and/or refinement; see below). If relation is nil or is not supplied, then it defaults to equal. See also the command =, which is much more flexible. Note that this command fails if no substitution is actually made. *Note:* No substitution takes place inside explicit values. So for example, the instruction (equiv 3 x) will cause 3 to be replaced by x if the current subterm is, say, (* 3 y), but not if the current subterm is (* 4 y) even though 4 = (1+ 3). The following remarks are quite technical and mostly describe a certain weak form of "backchaining" that has been implemented for equiv in order to support the = command. In fact neither the term (relation old new) nor the term (relation new old) needs to be *explicitly* among the current "assumptions", i.e., the top-level hypothesis or the governors. Rather, there need only be such an assumption that "tells us" (r old new) or (r new old), for *some* equivalence relation r that *refines* relation. Here, "tells us" means that either one of the indicated terms is among those assumptions, or else there is an assumption that is an implication whose conclusion is one of the indicated terms and whose hypotheses (gathered up by appropriately flattening the first argument of the implies term) are all among the current assumptions.  File: acl2-doc-lemacs.info, Node: ACL2-PC||EX, Next: ACL2-PC||EXIT, Prev: ACL2-PC||EQUIV, Up: PROOF-CHECKER ACL2-PC||EX (macro) exit after possibly saving the state Example and General Form: ex Same as exit, except that first the instruction save is executed. If save queries the user and is answered negatively, then the exit is aborted.  File: acl2-doc-lemacs.info, Node: ACL2-PC||EXIT, Next: ACL2-PC||EXPAND, Prev: ACL2-PC||EX, Up: PROOF-CHECKER ACL2-PC||EXIT (meta) exit the interactive proof-checker Examples: exit -- exit the interactive proof-checker (exit append-associativity) -- exit and create a defthm event named append-associativity General Forms: exit -- Exit without storing an event. (exit event-name &optional rule-classes do-it-flg) Exit, and store an event. The command exit returns you to the ACL2 loop. At a later time, (verify) may be executed to get back into the same proof-checker state, as long as there hasn't been an intervening use of the proof-checker (otherwise see save). When given one or more arguments as shown above, exit still returns you to the ACL2 loop, but first, if the interactive proof is complete, then it attempts create a defthm event with the specified event-name and rule-classes (which defaults to (:rewrite) if not supplied). The event will be printed to the terminal, and then normally the user will be queried whether an event should really be created. However, if the final optional argument do-it-flg is supplied and not nil, then an event will be made without a query. For example, the form (exit top-pop-elim (:elim :rewrite) t) causes a defthm event named top-pop-elim to be created with rule-classes (:elim :rewrite), without a query to the user (because of the argument t). *Note:* it is permitted for event-name to be nil. In that case, the name of the event will be the name supplied during the original call of verify. (See the documentation for verify and commands.) Also in that case, if rule-classes is not supplied then it defaults to the rule-classes supplied in the original call of verify. Comments on "success" and "failure". An exit instruction will always "fail", so for example, if it appears as an argument of a do-strict instruction then none of the later (instruction) arguments will be executed. Moreover, the "failure" will be "hard" if an event is successfully created or if the instruction is simply exit; otherwise it will be "soft". See the documentation for sequence for an explanation of hard and soft "failures". An obscure but potentially important fact is that if the "failure" is hard, then the error signal is a special signal that the top-level interactive loop can interpret as a request to exit. Thus for example, a sequencing command that turns an error triple (mv erp val state) into (mv t val state) would never cause an exit from the interactive loop. If the proof is not complete, then (exit event-name ...) will not cause an exit from the interactive loop. However, in that case it will print out the original user-supplied goal (the one that was supplied with the call to verify) and the current list of instructions.  File: acl2-doc-lemacs.info, Node: ACL2-PC||EXPAND, Next: ACL2-PC||FAIL, Prev: ACL2-PC||EXIT, Up: PROOF-CHECKER ACL2-PC||EXPAND (primitive) expand the current function call without simplification Examples: expand -- expand and do not simplify. For example, if the current subterm is (append a b), then after (expand t) the current subterm will be the term: (if (true-listp x) (if x (cons (car x) (append (cdr x) y)) y) (apply 'binary-append (list x y))) regardless of the top-level hypotheses and the governors. General Form: (expand &optional do-not-expand-lambda-flg new-goals-flg keep-all-guards-flg) Expand the function call at the current subterm, and do not simplify. The options have the following meanings: do-not-expand-lambda-flg: default is nil; otherwise, the result should be a lambda expression new-goals-flg: default of nil means to introduce APPLY for guards keep-all-guards-flg: default of nil means that the system should make a weak attempt to prove the guards from the current context See also x, which allows simplification.  File: acl2-doc-lemacs.info, Node: ACL2-PC||FAIL, Next: ACL2-PC||FORWARDCHAIN, Prev: ACL2-PC||EXPAND, Up: PROOF-CHECKER ACL2-PC||FAIL (macro) cause a failure Examples: fail (fail t) General Form: (fail &optional hard) This is probably only of interest to writers of macro commands. The only function of fail is to fail to "succeed". The full story is that fail and (fail nil) simply return (mv nil nil state), while (fail hard) returns (mv hard nil state) if hard-flag is not nil. See also do-strict, do-all, and sequence.  File: acl2-doc-lemacs.info, Node: ACL2-PC||FORWARDCHAIN, Next: ACL2-PC||FREE, Prev: ACL2-PC||FAIL, Up: PROOF-CHECKER ACL2-PC||FORWARDCHAIN (atomic macro) forward chain from an implication in the hyps Example: (forwardchain 2) ; Second hypothesis should be of the form ; (IMPLIES hyp concl), and the result is to replace ; that hypothesis with concl. General Forms: (forwardchain hypothesis-number) (forwardchain hypothesis-number hints) (forwardchain hypothesis-number hints quiet-flg) This command replaces the hypothesis corresponding to given index, which should be of the form (IMPLIES hyp concl), with its consequent concl. In fact, the given hypothesis is dropped, and the replacement hypothesis will appear as the final hypothesis after this command is executed. The prover must be able to prove the indicated hypothesis from the other hypotheses, or else the command will fail. The :hints argument is used in this prover call, and should have the usual syntax of hints to the prover. Output is suppressed if quiet-flg is supplied and not nil.  File: acl2-doc-lemacs.info, Node: ACL2-PC||FREE, Next: ACL2-PC||GENERALIZE, Prev: ACL2-PC||FORWARDCHAIN, Up: PROOF-CHECKER ACL2-PC||FREE (atomic macro) create a "free variable" Example: (free x) General Form: (free var) Mark var as a "free variable". Free variables are only of interest for the put command; see its documentation for an explanation.  File: acl2-doc-lemacs.info, Node: ACL2-PC||GENERALIZE, Next: ACL2-PC||GOALS, Prev: ACL2-PC||FREE, Up: PROOF-CHECKER ACL2-PC||GENERALIZE (primitive) perform a generalization Example: (generalize ((and (true-listp x) (true-listp y)) 0) ((append x y) w)) General Form: (generalize &rest substitution) Generalize using the indicated substitution, which should be a non-empty list. Each element of that list should be a two-element list of the form (term variable), where term may use abbreviations. The effect of the instruction is to replace each such term in the current goal by the corresponding variable. This replacement is carried out by a parallel substitution, outside-in in each hypothesis and in the conclusion. More generally, actually, the "variable" (second) component of each pair may be nil or a number, which causes the system to generate a new name of the form _ or _n, with n a natural number; more on this below. However, when a variable is supplied, it must not occur in any goal of the current proof-checker state. When the "variable" above is nil, the system will treat it as the variable |_| if that variable does not occur in any goal of the current proof-checker state. Otherwise it treats it as |_0|, or |_1|, or |_2|, and so on, until one of these is not among the variables of the current proof-checker state. If the "variable" is a non-negative integer n, then the system treats it as |_n| unless that variable already occurs among the current goals, in which case it increments n just as above until it obtains a new variable. *Note:* The same variable may not occur as the variable component of two different arguments (though nil may occur arbitrarily many times, as may a positive integer).  File: acl2-doc-lemacs.info, Node: ACL2-PC||GOALS, Next: ACL2-PC||HELP, Prev: ACL2-PC||GENERALIZE, Up: PROOF-CHECKER ACL2-PC||GOALS (macro) list the names of goals on the stack Example and General Form: goals Goals lists the names of all goals that remain to be proved. They are listed in the order in which they appear on the stack of remaining goals, which is relevant for example to the effect of a change-goal instruction.  File: acl2-doc-lemacs.info, Node: ACL2-PC||HELP, Next: ACL2-PC||HELP!, Prev: ACL2-PC||GOALS, Up: PROOF-CHECKER ACL2-PC||HELP (macro) proof-checker help facility Examples: (help rewrite) -- partial documentation on the rewrite command; the rest is available using more or more! (help! rewrite) -- full documentation on the rewrite command help, help! -- this documentation (in part, or in totality, respectively) General Forms: (help &optional command) (help! &optional command) more more! The proof checker supports the same kind of documentation as does ACL2 proper. The main difference is that you need to type (help command) in a list rather than :doc command. So, to get all the documentation on command, type (help! command) inside the interactive loop, but to get only a one-line description of the command together with some examples, type (help command). In the latter case, you can get the rest of the help by typing more!; or type more if you don't necessarily want all the rest of the help at once. (Then keep typing more if you want to keep getting more of the help for that command.) To summarize: as with ACL2, you can type either of the following: more, more! -- to obtain more (or, all the rest of) the documentation last requested by help (or, outside the proof-checker's loop, :doc) It has been arranged that the use of (help command) will tell you just about everything you could want to know about command, almost always by way of examples. For more details about a command, use help!, more, or more!. We use the word "command" to refer to the name itself, e.g. rewrite. We use the word "instruction" to refer to an input to the interactive system, e.g. (rewrite foo) or (help split). Of course, we allow commands with no arguments as instructions in many cases, e.g. rewrite. In such cases, command is treated identically to (command).  File: acl2-doc-lemacs.info, Node: ACL2-PC||HELP!, Next: ACL2-PC||HELP-LONG, Prev: ACL2-PC||HELP, Up: PROOF-CHECKER ACL2-PC||HELP! (macro) proof-checker help facility Same as help, except that the entire help message is printed without any need to invoke more! or more. Invoke help for documentation about the proof-checker help facility.  File: acl2-doc-lemacs.info, Node: ACL2-PC||HELP-LONG, Next: ACL2-PC||HYPS, Prev: ACL2-PC||HELP!, Up: PROOF-CHECKER ACL2-PC||HELP-LONG (macro) same as help! See the documentation for help!. Help-long has been included in addition to help! for historical reasons. (Such a command is included in Pc-Nqthm).  File: acl2-doc-lemacs.info, Node: ACL2-PC||HYPS, Next: ACL2-PC||ILLEGAL, Prev: ACL2-PC||HELP-LONG, Up: PROOF-CHECKER ACL2-PC||HYPS (macro) print the hypotheses Examples: hyps -- print all (top-level) hypotheses (hyps (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4 (hyps (1 3) t) -- print hypotheses 1 and 3 and all governors General Form: (hyps &optional hyps-indices govs-indices) Print the indicated top-level hypotheses and governors. (The notion of "governors" is defined below.) Here, hyps-indices and govs-indices should be lists of indices of hypotheses and governors (respectively), except that the atom t may be used to indicate that one wants all hypotheses or governors (respectively). The list of "governors" is defined as follows. Actually, we define here the notion of the governors for a pair of the form ]; we're interested in the special case where the term is the conclusion and the address is the current address. If the address is nil, then there are no governors, i.e., the list of governors is nil. If the term is of the form (if x y z) and the address is of the form (2 . rest) or (3 . rest), then the list of governors is the result of consing x or its negation (respectively) onto the list of governors for the pair or the pair (respectively). If the term is of the form (implies x y) and the address is of the form (2 . rest), then the list of governors is the result of consing x onto the list of governors for the pair . Otherwise, the list of governors for the pair is exactly the list of governors for the pair where argn is the nth argument of term. If all goals have been proved, a message saying so will be printed. (as there will be no current hypotheses or governors!). The hyps command never causes an error. It "succeeds" (in fact its value is t) if the arguments (when supplied) are appropriate, i.e. either t or lists of indices of hypotheses or governors, respectively. Otherwise it "fails" (its value is nil).