Info file: acl2-doc-emacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-emacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.9 Copyright (C) 1997 Computational Logic, Inc. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. Written by: Matt Kaufmann and J Strother Moore Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, TX 78703-4776 U.S.A.  File: acl2-doc-emacs.info, Node: DEFINE-PC-HELP, Next: INSTRUCTIONS, Prev: ACL2-PC||X-DUMB, Up: PROOF-CHECKER DEFINE-PC-HELP define a macro command whose purpose is to print something Example: (define-pc-help pp () (if (goals t) (io? proof-checker nil state (fms0 "~|~y0~|" (list (cons #0 (fetch-term (conc t) (current-addr t)))))) (print-all-goals-proved-message state))) General Form: (define-pc-help name args &rest body) This defines a macro command named name, as explained further below. The body should (after removing optional declarations) have multiplicity 1 and state-out t, i.e. it should return a single value of state. Typically, it will just print something. What (define-pc-help name args &rest body) really does is to create a call of define-pc-macro that defines name to take arguments args, to have the declarations indicated by all but the last form in body, and to have a body that (via pprogn) first executes the form in the last element of body and then returns a call to the command skip (which will return (mv nil t state)).  File: acl2-doc-emacs.info, Node: INSTRUCTIONS, Next: MACRO-COMMAND, Prev: DEFINE-PC-HELP, Up: PROOF-CHECKER INSTRUCTIONS instructions to the proof checker Example: :instructions (induct prove promote (dive 1) x (dive 2) = top (drop 2) prove) See *Note DEFTHM:: for the role of :instructions in place of :hints. As illustrated by the example above, the value associated with :instructions is a list of proof-checker commands. At the moment the best way to understand the idea of the interactive proof-checker (see *Note PROOF-CHECKER:: and see *Note VERIFY::) is probably to read the first 11 pages of CLI Technical Report 19, which describes the corresponding facility for Nqthm. When inside the interactive loop (i.e., after executing verify), use help to get a list of legal instructions and (help instr) to get help for the instruction instr.  File: acl2-doc-emacs.info, Node: MACRO-COMMAND, Next: RETRIEVE, Prev: INSTRUCTIONS, Up: PROOF-CHECKER MACRO-COMMAND compound command for the proof-checker The proof-checker (see *Note PROOF-CHECKER::) allows the user to supply interactive commands. Compound commands, called macro commands, may be defined; these expand into zero or more other commands. Some of these are "atomic" macro commands; these are viewed as a single command step when completed successfully. More documentation will be written on the proof-checker. For now, we simply point out that there are lots of examples of the use of define-pc-macro and define-pc-atomic-macro in the ACL2 source file "proof-checker-b.lisp". The former is used to create macro commands, which can be submitted to the interactive loop (see *Note VERIFY::) and will "expand" into zero or more commands. The latter is similar, except that the undoing mechanism (see *Note ACL2-PC::UNDO::) understands atomic macro commands to represent single interactive commands. Also see *Note ACL2-PC::COMM::and see *Note ACL2-PC::COMMANDS:: for a discussion of the display of interactive commands. Also see *Note TOGGLE-PC-MACRO:: for how to change a macro command to an atomic macro command, and vice versa.  File: acl2-doc-emacs.info, Node: RETRIEVE, Next: TOGGLE-PC-MACRO, Prev: MACRO-COMMAND, Up: PROOF-CHECKER RETRIEVE re-enter a (specified) proof-checker state Examples: (retrieve associativity-of-permutationp) retrieve General Form: (retrieve &optional name) See *Note ACL2-PC::RETRIEVE::, or use (help retrieve) inside the interactive proof-checker loop. Also see *Note UNSAVE::.  File: acl2-doc-emacs.info, Node: TOGGLE-PC-MACRO, Next: UNSAVE, Prev: RETRIEVE, Up: PROOF-CHECKER TOGGLE-PC-MACRO change an ordinary macro command to an atomic macro, or vice-versa Example: (toggle-pc-macro pro) Change pro from an atomic macro command to an ordinary one (or vice-versa, if pro happens to be an ordinary macro command) General Form: (toggle-pc-macro name &optional new-tp) If name is an atomic macro command then this turns it into an ordinary one, and vice-versa. However, if new-tp is supplied and not nil, then it should be the new type, or else there is no change.  File: acl2-doc-emacs.info, Node: UNSAVE, Next: VERIFY, Prev: TOGGLE-PC-MACRO, Up: PROOF-CHECKER UNSAVE remove a proof-checker state Example: (unsave assoc-of-append) General Form: (unsave name) Eliminates the association of a proof-checker state with name. See *Note UNSAVE:: or see *Note ACL2-PC::UNSAVE::. Also see *Note ACL2-PC::SAVE:: and see *Note RETRIEVE::.  File: acl2-doc-emacs.info, Node: VERIFY, Prev: UNSAVE, Up: PROOF-CHECKER VERIFY enter the interactive proof checker For proof-checker command summaries, see *Note PROOF-CHECKER::. Examples: (VERIFY (implies (and (true-listp x) (true-listp y)) (equal (append (append x y) z) (append x (append y z))))) -- Attempt to prove the given term interactively. (VERIFY (p x) :event-name p-always-holds :rule-classes (:rewrite :generalize) :instructions ((rewrite p-always-holds-lemma) change-goal)) -- Attempt to prove (p x), where the intention is to call the resulting DEFTHM event by the name p-always-holds, with rule-classes as indicated. The two indicated instructions will be run immediately to start the proof. (VERIFY) -- Re-enter the proof-checker in the state at which is was last left. General Form: (VERIFY &OPTIONAL raw-term &KEY event-name rule-classes instructions) Verify is the function used for entering the proof-checker's interactive loop.  File: acl2-doc-emacs.info, Node: PROOF-TREE, Next: Pages Written Especially for the Tours, Prev: PROOF-CHECKER, Up: Top PROOF-TREE proof tree displays A view of ACL2 proofs may be obtained by way of "proof tree displays." Environments such as emacs may be customized to provide window-based versions of proof tree displays. (See for example documentation of the emacs function start-proof-tree, co-written with Michael K. Smith, that the implementors are happy to make available.) Proof tree displays may be turned on with the command :start-proof-tree and may be turned off with the command :start-proof-tree; see *Note START-PROOF-TREE:: and see *Note STOP-PROOF-TREE::. * Menu: * CHECKPOINT-FORCED-GOALS:: Cause forcing goals to be checkpointed in proof trees * PROOF-TREE-DETAILS:: proof tree details not covered elsewhere * PROOF-TREE-EXAMPLES:: proof tree example * START-PROOF-TREE:: start displaying proof trees during proofs * STOP-PROOF-TREE:: stop displaying proof trees during proofs Here is an example of a proof tree display, with comments. Lines marked with "c" are considered "checkpoints," i.e., goals whose scrutiny may be of particular value. ( DEFTHM PLUS-TREE-DEL ...) ;currently proving PLUS-TREE-DEL 1 Goal preprocess ;"Goal" creates 1 subgoal by preprocessing 2 | Goal' simp ;"Goal'" creates 2 subgoals by simplification c 0 | | Subgoal 2 PUSH *1 ;"Subgoal 2" pushes "*1" for INDUCT ++++++++++++++++++++++++++++++ ;first pass thru waterfall completed c 6 *1 INDUCT ;Proof by induction of "*1" has | <5 more subgoals> ; created 6 top-level subgoals. At ; this point, one of those 6 has been ; proved, and 5 remain to be proved. ; We are currently working on the ; first of those 5 remaining goals. See *Note PROOF-TREE-EXAMPLES:: for many examples that contain proof tree displays. But first, we summarize the kinds of lines that may appear in a proof tree display. The simplest form of a proof tree display is a header showing the current event, followed by list of lines, each having one of the following forms. n ... Says that the indicated goal created n subgoals using the indicated process. Here "..." refers to possible additional information. c n ... As above, but calls attention to the fact that this goal is a "checkpoint" in the sense that it may be of particular interest. Some displays may overwrite "c" with ">" to indicate the current checkpoint being shown in the proof transcript. | ... | | Indicates that the goal just above this line, which is pointed to by the rightmost vertical bar ("|"), has k subgoals, none of which have yet been processed. | ... | | As above, except that some subgoals have already been processed. ++++++++++++++++++++++++++++++ Separates successive passes through the "waterfall". Thus, this "fencepost" mark indicates the start of a new proof by induction or of a new forcing round. See *Note PROOF-TREE-EXAMPLES:: for detailed examples. To learn how to turn off proof tree displays or to turn them back on again, see *Note STOP-PROOF-TREE:: and see *Note START-PROOF-TREE::, respectively. See *Note CHECKPOINT-FORCED-GOALS:: to learn how to mark goals as checkpoints that force the creation of goals in forcing rounds. Finally, see *Note PROOF-TREE-DETAILS:: for some points not covered elsewhere.  File: acl2-doc-emacs.info, Node: CHECKPOINT-FORCED-GOALS, Next: PROOF-TREE-DETAILS, Prev: PROOF-TREE, Up: PROOF-TREE CHECKPOINT-FORCED-GOALS Cause forcing goals to be checkpointed in proof trees Example forms: (checkpoint-forced-goals t) (checkpoint-forced-goals nil) Also see *Note PROOF-TREE::. By default, goals are not marked as checkpoints by a proof tree display (as described in the documentation for proof-tree) merely because they force some hypotheses, thus possibly contributing to a forcing round. However, some users may want such behavior, which will occur once the command (checkpoint-forced-goals) t) has been executed. To return to the default behavior, use the command (checkpoint-forced-goals nil).  File: acl2-doc-emacs.info, Node: PROOF-TREE-DETAILS, Next: PROOF-TREE-EXAMPLES, Prev: CHECKPOINT-FORCED-GOALS, Up: PROOF-TREE PROOF-TREE-DETAILS proof tree details not covered elsewhere See *Note PROOF-TREE:: for an introduction to proof trees, and for a list of related topics. Here we present some details not covered elsewhere. 1. When proof tree display is enabled (because the command :stop-proof-tree has not been executed, or has been superseded by a later :start-proof-tree command), then time summaries will include the time for proof tree display. This time includes the time spent computing with proof trees, such as the pruning process described briefly above. Even when proof trees are not displayed, such as when their display is turned off in the middle of a proof, this time will be printed if it is not 0. 2. When a goal is given a :bye in a proof (see *Note HINTS::), it is treated for the purpose of proof tree display just as though it had been proved. 3. Several state global variables affect proof tree display. (@ proof-tree-indent) is initially the string "| ": it is the string that is laid down the appropriate number of times to effect indentation. (@ proof-tree-buffer-width) is initially the value of (fmt-soft-right-margin state), and is used to prevent printing of the annotation "(forced ...)" in any greater column than this value. However, (assign proof-tree-buffer-width nil) to avoid any such suppression. Finally, (@ checkpoint-processors) is a list of processors from the constant list *preprocess-clause-ledge*, together with :induct. You may remove elements of (@ checkpoint-processors) to limit which processes are considered checkpoints. 4. When :otf-flg is not set to t in a proof, and the prover then decides to revert to the original goal and prove it by induction, the proof tree display will reflect this fact as shown here: c 0 | | Subgoal 2 PUSH (reverting) 5. Proof-tree display is turned off during calls of certify-book. 6. The usual failure message is printed as part of the prooftree display when a proof has failed.  File: acl2-doc-emacs.info, Node: PROOF-TREE-EXAMPLES, Next: START-PROOF-TREE, Prev: PROOF-TREE-DETAILS, Up: PROOF-TREE PROOF-TREE-EXAMPLES proof tree example See *Note PROOF-TREE:: for an introduction to proof trees, and for a list of related topics. Here we present a detailed example followed by a shorter example that illustrates proof by induction. Consider the guard proof for the definition of a function cancel_equal_plus; the body of this definition is of no importance here. The first proof tree display is: ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess | <18 subgoals> This is to be read as follows. At this stage of the proof we have encountered the top-level goal, named "Goal", which generated 18 subgoals using the "preprocess" process. We have not yet begun to work on those subgoals. The corresponding message from the ordinary prover output is: By case analysis we reduce the conjecture to the following 18 conjectures. Note that the field just before the name of the goal ("Goal"), which here contains the number 18, indicates the number of cases (children) created by the goal using the indicated process. This number will remain unchanged as long as this goal is displayed. The next proof tree display is: ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 1 | Subgoal 18 simp | | <1 subgoal> | <17 more subgoals> which indicates that at this point, the prover has used the simplification ("simp") process on Subgoal 18 to create one subgoal ("<1 subgoal>"). The vertical bar ("|") below "Subgoal 18", accompanied by the line below it, signifies that there are 17 siblings of Subgoal 18 that remain to be processed. The next proof tree displayed is: ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 1 | Subgoal 18 simp c 2 | | Subgoal 18' ELIM | | | <2 subgoals> | <17 more subgoals> Let us focus on the fourth line of this display: c 2 | | Subgoal 18' ELIM The "c" field marks this goal as a "checkpoint", i.e., a goal worthy of careful scrutiny. In fact, any goal that creates children by a process other than "preprocess" or "simp" is marked as a checkpoint. In this case, the destructor-elimination ("ELIM") process has been used to create subgoals of this goal. The indentation shows that this goal, Subgoal 18', is a child of Subgoal 18. The number "2" indicates that 2 subgoals have been created (by ELIM). Note that this information is consistent with the line just below it, which says "<2 subgoals>". Finally, the last line of this proof tree display, | <17 more subgoals> is connected by vertical bars ("|") up to the string "Subgoal 18", which suggests that there are 17 immediate subgoals of Goal remaining to process after Subgoal 18. Note that this line is indented one level from the second line, which is the line for the goal named "Goal". The display is intended to suggest that the subgoals of Goal that remain to be proved consist of Subgoal 18 together with 17 more subgoals. The next proof tree display differs from the previous one only in that now, Subgoal 18' has only one more subgoal to be processed. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 1 | Subgoal 18 simp c 2 | | Subgoal 18' ELIM | | | <1 more subgoal> | <17 more subgoals> Note that the word "more" in "<1 more subgoal>" tells us that there was originally more than one subgoal of Subgoal 18. In fact that information already follows from the line above, which (as previously explained) says that Subgoal 18' originally created 2 subgoals. The next proof tree display occurs when the prover completes the proof of that "1 more subgoal" referred to above. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess | <17 more subgoals> Then, Subgoal 17 is processed and creates one subgoal, by simplification: ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 1 | Subgoal 17 simp | | <1 subgoal> | <16 more subgoals> ... and so on. Later in the proof one might find the following successive proof tree displays. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess | <9 more subgoals> ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 0 | Subgoal 9 simp (FORCED) | <8 more subgoals> These displays tell us that Subgoal 9 simplified to t (note that the "0" shows clearly that no subgoals were created), but that some rule's hypotheses were forced. Although this goal is not checkpointed (i.e., no "c" appears on the left margin), one can cause such goals to be checkpointed; see *Note CHECKPOINT-FORCED-GOALS::. In fact, the proof tree displayed at the end of the "main proof" (the 0-th forcing round) is as follows. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 0 | Subgoal 9 simp (FORCED) 0 | Subgoal 8 simp (FORCED) 0 | Subgoal 7 simp (FORCED) 0 | Subgoal 6 simp (FORCED) 0 | Subgoal 4 simp (FORCED) 0 | Subgoal 3 simp (FORCED) This is followed by the following proof tree display at the start of the forcing round. 18 Goal preprocess 0 | Subgoal 9 simp (FORCED [1]Subgoal 4) 0 | Subgoal 8 simp (FORCED [1]Subgoal 6) 0 | Subgoal 7 simp (FORCED [1]Subgoal 1) 0 | Subgoal 6 simp (FORCED [1]Subgoal 3) 0 | Subgoal 4 simp (FORCED [1]Subgoal 5) 0 | Subgoal 3 simp (FORCED [1]Subgoal 2) ++++++++++++++++++++++++++++++ 6 [1]Goal FORCING-ROUND 2 | [1]Subgoal 6 preprocess | | <2 subgoals> | <5 more subgoals> This display shows which goals to "blame" for the existence of each goal in the forcing round. For example, Subgoal 9 is to blame for the creation of [1]Subgoal 4. Actually, there is no real goal named "[1]Goal". However, the line 6 [1]Goal FORCING-ROUND appears in the proof tree display to suggest a "parent" of the six top-level goals in that forcing round. As usual, the numeric field before the goal name contains the original number of children of that (virtual, in this case) goal -- in this case, 6. In our example proof, Subgoal 6 eventually gets proved, without doing any further forcing. At that point, the proof tree display looks as follows. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 0 | Subgoal 9 simp (FORCED [1]Subgoal 4) 0 | Subgoal 7 simp (FORCED [1]Subgoal 1) 0 | Subgoal 6 simp (FORCED [1]Subgoal 3) 0 | Subgoal 4 simp (FORCED [1]Subgoal 5) 0 | Subgoal 3 simp (FORCED [1]Subgoal 2) ++++++++++++++++++++++++++++++ 6 [1]Goal FORCING-ROUND | <5 more subgoals> Notice that the line for Subgoal 8, 0 | Subgoal 8 simp (FORCED [1]Subgoal 6) no longer appears. That is because the goal [1]Subgoal 6 has been proved, along with all its children; and hence, the proof of Subgoal 8 no longer depends on any further reasoning. The final two proof tree displays in our example are as follows. ( DEFUN CANCEL_EQUAL_PLUS ...) 18 Goal preprocess 0 | Subgoal 7 simp (FORCED [1]Subgoal 1) ++++++++++++++++++++++++++++++ 6 [1]Goal FORCING-ROUND 2 | [1]Subgoal 1 preprocess 1 | | [1]Subgoal 1.1 preprocess 1 | | | [1]Subgoal 1.1' simp c 3 | | | | [1]Subgoal 1.1" ELIM | | | | | <1 more subgoal> ( DEFUN CANCEL_EQUAL_PLUS ...) <> The explanation for the empty proof tree is simple: once [1]Subgoal 1.1.1 was proved, nothing further remained to be proved. In fact, the much sought-after "Q.E.D." appeared shortly after the final proof tree was displayed. Let us conclude with a final, brief example that illustrates proof by induction. Partway through the proof one might come across the following proof tree display. ( DEFTHM PLUS-TREE-DEL ...) 1 Goal preprocess 2 | Goal' simp c 0 | | Subgoal 2 PUSH *1 | | <1 more subgoal> This display says that in the attempt to prove a theorem called plus-tree-del, preprocessing created the only child Goal' from Goal, and Goal' simplified to two subgoals. Subgoal 2 is immediately pushed for proof by induction, under the name "*1". In fact if Subgoal 1 simplifies to t, then we see the following successive proof tree displays after the one shown above. ( DEFTHM PLUS-TREE-DEL ...) 1 Goal preprocess 2 | Goal' simp c 0 | | Subgoal 2 PUSH *1 ( DEFTHM PLUS-TREE-DEL ...) 1 Goal preprocess 2 | Goal' simp c 0 | | Subgoal 2 PUSH *1 ++++++++++++++++++++++++++++++ c 6 *1 INDUCT | <5 more subgoals> The separator "+++++..." says that we are beginning another trip through the waterfall. In fact this trip is for a proof by induction (as opposed to a forcing round), as indicated by the word "INDUCT". Apparently *1.6 was proved immediately, because it was not even displayed; a goal is only displayed when there is some work left to do either on it or on some goal that it brought (perhaps indirectly) into existence. Once a proof by induction is completed, the "PUSH" line that refers to that proof is eliminated ("pruned"). So for example, when the present proof by induction is completed, the line c 0 | | Subgoal 2 PUSH *1 is eliminated, which in fact causes the lines above it to be eliminated (since they no longer refer to unproved children). Hence, at that point one might expect to see: ( DEFTHM PLUS-TREE-DEL ...) <> However, if the proof by induction of *1 necessitates further proofs by induction or a forcing round, then this "pruning" will not yet be done.  File: acl2-doc-emacs.info, Node: START-PROOF-TREE, Next: STOP-PROOF-TREE, Prev: PROOF-TREE-EXAMPLES, Up: PROOF-TREE START-PROOF-TREE start displaying proof trees during proofs Also see *Note PROOF-TREE:: and see *Note STOP-PROOF-TREE::. Note that :start-proof-tree works by removing 'proof-tree from the inhibit-output-lst; see *Note SET-INHIBIT-OUTPUT-LST::. Proof tree displays are explained in the documentation for proof-tree. :start-proof-tree causes proof tree display to be turned on, once it has been turned off by :stop-proof-tree. Do not attempt to invoke start-proof-tree during an interrupt in the middle of a proof.  File: acl2-doc-emacs.info, Node: STOP-PROOF-TREE, Prev: START-PROOF-TREE, Up: PROOF-TREE STOP-PROOF-TREE stop displaying proof trees during proofs Also see *Note PROOF-TREE:: and see *Note START-PROOF-TREE::. Note that :stop-proof-tree works by adding 'proof-tree to the inhibit-output-lst; see *Note SET-INHIBIT-OUTPUT-LST::. Proof tree displays are explained in the documentation for proof-tree. :Stop-proof-tree causes proof tree display to be turned off. It is permissible to submit the form (stop-proof-tree) during a break. Thus, you can actually turn off proof tree display in the middle of a proof by interrupting ACL2 and submitting the form (stop-proof-tree) in raw Lisp.  File: acl2-doc-emacs.info, Node: Pages Written Especially for the Tours, Next: RELEASE-NOTES, Prev: PROOF-TREE, Up: Top Pages Written Especially for the Tours Pages Written Especially for the Tours The ACL2 Home Page is generated from ACL2's online documentation strings. (How else could we achieve the total integration of ACL2's online documentation with the home page?) This page is just an artifact of the structure of our documentation strings: each string must belong to a "major section" of the documentation database. This page is not structured to be used by a person browsing via the Web. It contains, in an arbitrary order, the pages written specificially for the Web user. Furthermore, browsing the pages below via the ACL2 :DOC command or via TexInfo is often unsatisfying because those browsers do not support gif files and the notion of going "back" to a node just visited. If you wish to look at the pages below, we strongly recommend that you do so via a HTML-based Web browser. Indeed, you should simply visit ACL2's Home Page and take one of the Tours. * Menu: * A Flying Tour of ACL2:: A Flying Tour of ACL2 * A Sketch of How the Rewriter Works:: A Sketch of How the Rewriter Works * A Tiny Warning Sign:: A Tiny Warning Sign * A Trivial Proof:: A Trivial Proof * A Typical State:: A Typical State * A Walking Tour of ACL2:: A Walking Tour of ACL2 * ACL2 Characters:: ACL2 Characters * ACL2 Conses or Ordered Pairs:: ACL2 Conses or Ordered Pairs * ACL2 Strings:: ACL2 Strings * ACL2 Symbols:: ACL2 Symbols * ACL2 System Architecture:: ACL2 System Architecture * ACL2 as an Interactive Theorem Prover:: ACL2 as an Interactive Theorem Prover * ACL2 as an Interactive Theorem Prover (continued):: ACL2 as an Interactive Theorem Prover (continued) * ACL2 is an Untyped Language:: ACL2 is an Untyped Language * About Models:: About Models * About Types:: About Types * About the ACL2 Home Page:: About the ACL2 Home Page * About the Admission of Recursive Definitions:: About the Admission of Recursive Definitions * About the Prompt:: About the Prompt * An Example Common Lisp Function Definition:: An Example Common Lisp Function Definition * An Example of ACL2 in Use:: An Example of ACL2 in Use * Analyzing Common Lisp Models:: Analyzing Common Lisp Models * Common Lisp:: Common Lisp * Common Lisp as a Modeling Language:: Common Lisp as a Modeling Language * Conversion:: Conversion to Uppercase * Corroborating Models:: Corroborating Models * Evaluating App on Sample Input:: Evaluating App on Sample Input * Flawed Induction Candidates in App Example:: Flawed Induction Candidates in App Example * Functions for Manipulating these Objects:: Functions for Manipulating these Objects * Guards:: Guards * Guessing the Type of a Newly Admitted Function:: Guessing the Type of a Newly Admitted Function * Guiding the ACL2 Theorem Prover:: Guiding the ACL2 Theorem Prover * Hey Wait! Is ACL2 Typed or Untyped(Q):: Hey Wait! Is ACL2 Typed or Untyped? * How Long Does It Take to Become an Effective User(Q):: How Long Does It Take to Become an Effective User? * How To Find Out about ACL2 Functions:: How To Find Out about ACL2 Functions * How To Find Out about ACL2 Functions (continued):: How To Find Out about ACL2 Functions (continued) * Modeling in ACL2:: Modeling in ACL2 * Models in Engineering:: Models in Engineering * Models of Computer Hardware and Software:: Models of Computer Hardware and Software * Name the Formula Above:: Name the Formula Above * Numbers in ACL2:: Numbers in ACL2 * On the Naming of Subgoals:: On the Naming of Subgoals * Other Requirements:: Other Requirements * Overview of the Expansion of ENDP in the Base Case:: Overview of the Expansion of ENDP in the Base Case * Overview of the Expansion of ENDP in the Induction Step:: Overview of the Expansion of ENDP in the Induction Step * Overview of the Final Simplification in the Base Case:: Overview of the Final Simplification in the Base Case * Overview of the Proof of a Trivial Consequence:: Overview of the Proof of a Trivial Consequence * Overview of the Simplification of the Base Case to T:: Overview of the Simplification of the Base Case to T * Overview of the Simplification of the Induction Conclusion:: Overview of the Simplification of the Induction Conclusion * Overview of the Simplification of the Induction Step to T:: Overview of the Simplification of the Induction Step to T * Perhaps:: Perhaps * Popping out of an Inductive Proof:: Popping out of an Inductive Proof * Proving Theorems about Models:: Proving Theorems about Models * Revisiting the Admission of App:: Revisiting the Admission of App * Rewrite Rules are Generated from DEFTHM Events:: Rewrite Rules are Generated from DEFTHM Events * Running Models:: Running Models * STATE is the Only Variable in Top-Level Forms:: STATE is the Only Variable in Top-Level Forms * Subsumption of Induction Candidates in App Example:: Subsumption of Induction Candidates in App Example * Suggested Inductions in the Associativity of App Example:: Suggested Inductions in the Associativity of App Example * Symbolic Execution of Models:: Symbolic Execution of Models * The Admission of App:: The Admission of App * The Associativity of App:: The Associativity of App * The Base Case in the App Example:: The Base Case in the App Example * The End of the Flying Tour:: The End of the Flying Tour * The End of the Proof of the Associativity of App:: The End of the Proof of the Associativity of App * The End of the Walking Tour:: The End of the Walking Tour * The Event Summary:: The Event Summary * The Expansion of ENDP in the Induction Step (Step 0):: The Expansion of ENDP in the Induction Step (Step 0) * The Expansion of ENDP in the Induction Step (Step 1):: The Expansion of ENDP in the Induction Step (Step 1) * The Expansion of ENDP in the Induction Step (Step 2):: The Expansion of ENDP in the Induction Step (Step 2) * The Falling Body Model:: The Falling Body Model * The Final Simplification in the Base Case (Step 0):: the Final Simplification in the Base Case (Step 0) * The Final Simplification in the Base Case (Step 1):: the Final Simplification in the Base Case (Step 1) * The Final Simplification in the Base Case (Step 2):: the Final Simplification in the Base Case (Step 2) * The Final Simplification in the Base Case (Step 3):: the Final Simplification in the Base Case (Step 3) * The First Application of the Associativity Rule:: The First Application of the Associativity Rule * The Induction Scheme Selected for the App Example:: The Induction Scheme Selected for the App Example * The Induction Step in the App Example:: The Induction Step in the App Example * The Instantiation of the Induction Scheme:: The Instantiation of the Induction Scheme * The Justification of the Induction Scheme:: The Justification of the Induction Scheme * The Proof of the Associativity of App:: The Proof of the Associativity of App * The Q.E.D. Message:: The Q.E.D. Message * The Rules used in the Associativity of App Proof:: The Rules used in the Associativity of App Proof * The Simplification of the Induction Conclusion (Step 0):: the Simplification of the Induction Conclusion (Step 0) * The Simplification of the Induction Conclusion (Step 1):: the Simplification of the Induction Conclusion (Step 1) * The Simplification of the Induction Conclusion (Step 10):: the Simplification of the Induction Conclusion (Step 10) * The Simplification of the Induction Conclusion (Step 11):: the Simplification of the Induction Conclusion (Step 11) * The Simplification of the Induction Conclusion (Step 12):: the Simplification of the Induction Conclusion (Step 12) * The Simplification of the Induction Conclusion (Step 2):: the Simplification of the Induction Conclusion (Step 2) * The Simplification of the Induction Conclusion (Step 3):: the Simplification of the Induction Conclusion (Step 3) * The Simplification of the Induction Conclusion (Step 4):: the Simplification of the Induction Conclusion (Step 4) * The Simplification of the Induction Conclusion (Step 5):: the Simplification of the Induction Conclusion (Step 5) * The Simplification of the Induction Conclusion (Step 6):: the Simplification of the Induction Conclusion (Step 6) * The Simplification of the Induction Conclusion (Step 7):: the Simplification of the Induction Conclusion (Step 7) * The Simplification of the Induction Conclusion (Step 8):: the Simplification of the Induction Conclusion (Step 8) * The Simplification of the Induction Conclusion (Step 9):: the Simplification of the Induction Conclusion (Step 9) * The Summary of the Proof of the Trivial Consequence:: The Summary of the Proof of the Trivial Consequence * The Theorem that App is Associative:: The Theorem that App is Associative * The Time Taken to do the Associativity of App Proof:: The Time Taken to do the Associativity of App Proof * The Tours:: The Tours * The WARNING about the Trivial Consequence:: The WARNING about the Trivial Consequence * Undocumented Topic:: Undocumented Topic * Using the Associativity of App to Prove a Trivial Consequence:: Using the Associativity of App to Prove a Trivial Consequence * What Is ACL2(Q):: What Is ACL2? * What is Required of the User(Q):: What is Required of the User? * What is a Mathematical Logic(Q):: What is a Mathematical Logic? * What is a Mechanical Theorem Prover(Q):: What is a Mechanical Theorem Prover? * What is a Mechanical Theorem Prover(Q) (continued):: What is a Mechanical Theorem Prover? (continued) * You Must Think about the Use of a Formula as a Rule:: You Must Think about the Use of a Formula as a Rule Generally, the topics listed above will not be of use to the ACL2 user.  File: acl2-doc-emacs.info, Node: A Flying Tour of ACL2, Next: A Sketch of How the Rewriter Works, Prev: Pages Written Especially for the Tours, Up: Pages Written Especially for the Tours A Flying Tour of ACL2 A Flying Tour of ACL2 On this tour you will learn a little about what ACL2 is for rather than how ACL2 works. At the bottom of the "page" (which may extend beyond the end of your screen) there is a small "flying tour" icon. Click on it to go to the next page of the tour. The tour visits the following topics sequentially. The Flight Plan * This Documentation * What is ACL2? * Mathematical Logic * Mechanical Theorem Proving * Mathematical Models in General * Mathematical Models of Computing Machines Formalizing Models Running Models Symbolic Execution of Models Proving Theorems about Models * Requirements of ACL2 The User's Skills Training Host System We intend the tour to take about 10 minutes of your time. Some pages on the tour contain pointers to other documents. You need not follow these pointers to stay on the tour. Flying Tour: *Note About the ACL2 Home Page::  File: acl2-doc-emacs.info, Node: A Sketch of How the Rewriter Works, Next: A Tiny Warning Sign, Prev: A Flying Tour of ACL2, Up: Pages Written Especially for the Tours A Sketch of How the Rewriter Works A Sketch of How the Rewriter Works Below we show the first target term, extracted from the current conjecture. Below it we show the associativity rule. The variables of the rewrite rule are instantiated so that the left-hand side of the rule matches the target: variable term from target a x1 b x2 c (app x3 x4) Then the target is replaced by the instantiated right-hand side of the rule. Sometimes rules have hypotheses. To make a long story short, if the rule has hypotheses, then after matching the left-hand side, the rewriter instantiates the hypotheses and rewrites them recursively. This is called backchaining. If they all rewrite to true, then the target is replaced as above. For more details on how the ACL2 rewriter works, see Boyer and Moore's book A Computational Logic, Academic Press, 1979.  File: acl2-doc-emacs.info, Node: A Tiny Warning Sign, Next: A Trivial Proof, Prev: A Sketch of How the Rewriter Works, Up: Pages Written Especially for the Tours A Tiny Warning Sign A Tiny Warning Sign This warning sign, which usually appears as "", indicates that the link it marks takes you into ACL2's online documentation. The documentation is a vast graph of documented topics intended to help the *user* of ACL2 rather than the *potential user*. If you are exploring ACL2's home page to learn about the system, perhaps you should go back rather than follow the link marked with this sign. But you are welcome to explore the online documentation as well. Good luck.  File: acl2-doc-emacs.info, Node: A Trivial Proof, Next: A Typical State, Prev: A Tiny Warning Sign, Up: Pages Written Especially for the Tours A Trivial Proof A Trivial Proof  File: acl2-doc-emacs.info, Node: A Typical State, Next: A Walking Tour of ACL2, Prev: A Trivial Proof, Up: Pages Written Especially for the Tours A Typical State A Typical State Observe that the states in typical models talk about booleans integers vectors records caches bits symbols arrays stacks files characters strings sequences tables directories These objects are discrete rather than continuous; furthermore they are built incrementally or inductively by repeatedly using primitive operations to put together smaller peices. The functions we need to manipulate these objects do things like concatenate, reverse, sort, search, count, etc. Flying Tour: *Note Functions for Manipulating these Objects::  File: acl2-doc-emacs.info, Node: A Walking Tour of ACL2, Next: ACL2 Characters, Prev: A Typical State, Up: Pages Written Especially for the Tours A Walking Tour of ACL2 A Walking Tour of ACL2 On this tour you will learn a little more about the ACL2 logic, the theorem prover, and the user interface. This time we will stick with really simple things, such as the associativity of list concatenation. We assume you have taken the Flying Tour but that you did not necessarily follow all the "off-tour" links. So this tour may revisit some pages you've seen. Just click on the Walking Tour icon at the bottom of each page. On this tour you will see many more links marked <>. We would like to discourage you from following these links right now. However we encourage you to note them. Basically, the <> sign here illustrates the documentation and introduces you to its main entry points. Once you have started to use ACL2 you can take the Walking Tour again but pursue more of the indicated links. Walking Tour: *Note Common Lisp::  File: acl2-doc-emacs.info, Node: ACL2 Characters, Next: ACL2 Conses or Ordered Pairs, Prev: A Walking Tour of ACL2, Up: Pages Written Especially for the Tours ACL2 Characters ACL2 Characters ACL2 accepts 256 distinct characters, which are the characters obtained by applying the function code-char <> to each integer from 0 to 255. Among these, Common Lisp designates certain ones as *standard-characters*, namely those of the form (code-char n) where n is from 33 to 126, together with #\Newline and #\Space. The actual standard characters may be viewed by evaluating the constant expression *standard-chars*. The standard character constants are written by writing a hash mark followed by a backslash (#\) followed by the character. The function characterp <> recognizes characters. For more details, See *Note CHARACTERS:: <>.  File: acl2-doc-emacs.info, Node: ACL2 Conses or Ordered Pairs, Next: ACL2 Strings, Prev: ACL2 Characters, Up: Pages Written Especially for the Tours ACL2 Conses or Ordered Pairs ACL2 Conses or Ordered Pairs The function cons <> creates an ordered pair. Car <> and cdr <> return the first and second components, respectively, of an ordered pair. The function consp <> recognizes ordered pairs. Ordered pairs are used to represent lists and trees. See any Common Lisp documentation for a discussion of how list constants are written and for the many list processing functions available. Also, see *Note PROGRAMMING:: <> where we list all the ACL2 primitive functions. Here are some examples of list constants to suggest their syntax. '(a . b) ; a pair whose car is 'a and cdr is 'b '(a . nil) ; a pair whose car is 'a and cdr is nil '(a) ; another way to write the same thing '(a b) ; a pair whose car is 'a and cdr is '(b) '(a b c) ; a pair whose car is 'a and cdr is '(b c) ; i.e., a list of three symbols, a, b, and c. '((a . 1) (b . 2)) ; a list of two pairs It is useful to distinguish "proper" conses from "improper" ones, the former being those cons trees whose right-most branch terminates with nil. A "true list" (see *Note TRUE-LISTP:: <>) is either nil or a proper cons. (A b c . 7) is an improper cons and hence not a true list.  File: acl2-doc-emacs.info, Node: ACL2 Strings, Next: ACL2 Symbols, Prev: ACL2 Conses or Ordered Pairs, Up: Pages Written Especially for the Tours ACL2 Strings ACL2 Strings Strings of ACL2 characters are written as sequences of characters delimited by "double quotation marks" ("). To put such a character in a string, escape it by preceding it with a backslash. The function stringp <> recognizes strings and char <> will fetch the nth character of a string. There are many other primitives for handling strings, such as string< <> for comparing two strings lexicographically. We suggest you See *Note PROGRAMMING:: <> where we list all of the primitive ACL2 functions. Alternatively, see any Common Lisp language documentation.  File: acl2-doc-emacs.info, Node: ACL2 Symbols, Next: ACL2 System Architecture, Prev: ACL2 Strings, Up: Pages Written Especially for the Tours ACL2 Symbols ACL2 Symbols Common Lisp's symbols are a data type representing words. They are frequently regarded as atomic objects in the sense that they are not frequently broken down into their constituents. Often the only important properties of symbols is that they are not numbers, characters, strings, or lists and that two symbols are not equal if they look different (!). Examples of symbols include PLUS and SMITH::ABC. All function and variable names in ACL2 are symbols. When symbols are used as constants they must be quoted, as in 'PLUS. The symbol T is commonly used as the Boolean "true." The symbol NIL is commonly used both as the Boolean "false" and as the "empty list." Despite sometimes being called the "empty list" NIL is a symbol not an "empty cons." Unlike other symbols, T and NIL may be used as constants without quoting them. Usually, symbols are written as sequences of alphanumeric characters other than those denoting numbers. Thus, A12, +1A and 1+ are symbols but +12 is a number. Roughly speaking, when symbols are read lower case characters are converted to upper case, so we frequently do not distinguish ABC from Abc or abc. See *Note Conversion:: for information about case conversion when symbols are read. However, any character can be used in a symbol, but some characters must be "escaped" to allow the Lisp reader to parse the sequence as a symbol. For example, |Abc| is a symbol whose first character is capitalized and whose remaining characters are in lower case. |An odd duck| is a symbol containing two #\Space characters. See any Common Lisp documentation for the syntactic rules for symbols. Technically, a symbol is a special kind of pair consisting of a package name (which is a string) and a symbol name (which is also a string). (See *Note SYMBOL-PACKAGE-NAME:: <> and see *Note SYMBOL-NAME::<>.) The symbol SMITH::ABC is said to be in package "SMITH" and to have the symbol name "ABC". The symbol ABC in package "SMITH" is generally not equal to the symbol ABC in package "JONES". However, it is possible to "import" symbols from one package into another one, but in ACL2 this can only be done when the package is created. (See *Note DEFPKG:: <>.) If the current-package <> is "SMITH" then SMITH::ABC may be more briefly written as just ABC. Intern <> "creates" a symbol of a given name in a given package.  File: acl2-doc-emacs.info, Node: ACL2 System Architecture, Next: ACL2 as an Interactive Theorem Prover, Prev: ACL2 Symbols, Up: Pages Written Especially for the Tours ACL2 System Architecture ACL2 System Architecture The user interacts with the theorem prover by giving it definitions, theorems and advice (e.g., "use this lemma."), often in the form of books books <>. The theorem prover uses the rules in the library of books the user has selected. The theorem prover prints its proof attempts to the user. When a theorem is proved it is converted to a rule under the control of the user's rule-classes <>. The informed user can make ACL2 do amazing things. Walking Tour: *Note Rewrite Rules are Generated from DEFTHM Events::  File: acl2-doc-emacs.info, Node: ACL2 as an Interactive Theorem Prover, Next: ACL2 as an Interactive Theorem Prover (continued), Prev: ACL2 System Architecture, Up: Pages Written Especially for the Tours ACL2 as an Interactive Theorem Prover ACL2 as an Interactive Theorem Prover The ACL2 theorem prover finds proofs in the ACL2 logic. It can be automatic. But most often the user must help it. The user usually guides ACL2 by suggesting that it first prove key lemmas. Lemmas are just theorems used in the proofs of other theorems. See *Note ACL2 as an Interactive Theorem Prover (continued):: to continue.  File: acl2-doc-emacs.info, Node: ACL2 as an Interactive Theorem Prover (continued), Next: ACL2 is an Untyped Language, Prev: ACL2 as an Interactive Theorem Prover, Up: Pages Written Especially for the Tours ACL2 as an Interactive Theorem Prover (continued) ACL2 as an Interactive Theorem Prover (continued) Theorems, lemmas, definitions, and advice of various sorts can be stored in books <>. When a theorem or definition is stored in a book, the user can specify how it should be used in the future. When viewed this way, theorems and definitions are thought of as rules. The ACL2 theorem prover is rule driven. The rules are obtained from books. See *Note ACL2 System Architecture:: to continue. Walking Tour: *Note ACL2 System Architecture::  File: acl2-doc-emacs.info, Node: ACL2 is an Untyped Language, Next: About Models, Prev: ACL2 as an Interactive Theorem Prover (continued), Up: Pages Written Especially for the Tours ACL2 is an Untyped Language ACL2 is an Untyped Language The example ACL2 !>(app '(a b c) 27) (A B C . 27) illustrates the fact that ACL2's logic is untyped (see *Note About Types::for a brief discussion of the typed versus untyped nature of the logic). The definition of app makes no restriction of the arguments to lists. The definition says that if the first argument satisfies endp <> then return the second argument. In this example, when app has recursed three times down the cdr of its first argument, '(a b c), it reaches the final nil, which satisfies endp, and so 27 is returned. It is naturally consed into the emerging list as the function returns from successive recursive calls (since cons does not require its arguments to be lists, either). The result is an "improper" list, (a b c . 27). You can think of (app x y) as building a binary tree by replacing the right-most tip of the tree x with the tree y.  File: acl2-doc-emacs.info, Node: About Models, Next: About Types, Prev: ACL2 is an Untyped Language, Up: Pages Written Especially for the Tours About Models About Models ACL2 is used to construct mathematical models of computer hardware and software (i.e., "digital systems"). A mathematical model is a set of mathematical formulas used to predict the behavior of some artifact. The use of mathematical models allows faster and cheaper delivery of better systems. Models need not be complete or perfectly accurate to be useful to the trained engineer. See *Note Models in Engineering:: for more discussion of these assertions in an engineering context. Flying Tour: *Note Models of Computer Hardware and Software::  File: acl2-doc-emacs.info, Node: About Types, Next: About the ACL2 Home Page, Prev: About Models, Up: Pages Written Especially for the Tours About Types About Types The universe of ACL2 objects includes objects of many different types. For example, t is a "symbol" and 3 is an "integer." Roughly speaking the objects of ACL2 can be partitioned into the following types: Numbers 3, -22/7, #c(3 5/2) Characters #\A, #\a, #\Space Strings "This is a string." Symbols 'abc, 'smith::abc Conses (or Ordered Pairs) '((a . 1) (b . 2)) When proving theorems it is important to know the types of object returned by a term. ACL2 uses a complicated heuristic algorithm, called type-set <>, to determine what types of objects a term may produce. The user can more or less program the type-set algorithm by proving type-prescription <> rules. ACL2 is an "untyped" logic in the sense that the syntax is not typed: It is legal to apply a function symbol of n arguments to any n terms, regardless of the types of the argument terms. Thus, it is permitted to write such odd expressions as (+ t 3) which sums the symbol t and the integer 3. Common Lisp does not prohibit such expressions. We like untyped languages because they are simple to describe, though proving theorems about them can be awkward because, unless one is careful in the way one defines or states things, unusual cases (like (+ t 3)) can arise. To make theorem proving easier in ACL2, the axioms actually define a value for such terms. The value of (+ t 3) is 3; under the ACL2 axioms, non-numeric arguments to + are treated as though they were 0. You might immediately wonder about our claim that ACL2 is Common Lisp, since (+ t 3) is "an error" (and will sometimes even "signal an error") in Common Lisp. It is to handle this problem that ACL2 has guards. We will discuss guards later in the Walking Tour. However, many new users simply ignore the issue of guards entirely. You should now return to the Walking Tour.