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: The End of the Flying Tour, Next: The End of the Proof of the Associativity of App, Prev: The Base Case in the App Example, Up: Pages Written Especially for the Tours The End of the Flying Tour The End of the Flying Tour This completes the Flying Tour. You may wish now to go back and revisit selected nodes of the Flying Tour so that you can explore some of the branches not on the Tour. You can do so via The Flight Plan. These branches mainly provide some background and motivational material, rather than details of ACL2. If you would like to learn more about ACL2 itself, we recommend that you now take the walking Tour. You may do so by clicking on the Walking Tour icon below. Thanks. Matt Kaufmann and J Moore Walking Tour: *Note A Walking Tour of ACL2::  File: acl2-doc-emacs.info, Node: The End of the Proof of the Associativity of App, Next: The End of the Walking Tour, Prev: The End of the Flying Tour, Up: Pages Written Especially for the Tours The End of the Proof of the Associativity of App The End of the Proof of the Associativity of App That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM ASSOCIATIVITY-OF-APP ...) Rules: ((:REWRITE CDR-CONS) (:REWRITE CAR-CONS) (:DEFINITION NOT) (:DEFINITION ENDP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:DEFINITION APP)) Warnings: None Time: 0.27 seconds (prove: 0.10, print: 0.05, other: 0.12) ASSOCIATIVITY-OF-APP Walking Tour: *Note Guiding the ACL2 Theorem Prover::  File: acl2-doc-emacs.info, Node: The End of the Walking Tour, Next: The Event Summary, Prev: The End of the Proof of the Associativity of App, Up: Pages Written Especially for the Tours The End of the Walking Tour The End of the Walking Tour This completes the Walking Tour. We intend to document many other parts of the system this way, but we just haven't gotten around to it. If you feel like reading more, see *Note TUTORIAL-EXAMPLES:: in the documentation. There you will find several challenging but simple applications. At the conclusion of the examples is a simple challenge to try. We hope you enjoy ACL2. We do. Matt Kaufmann and J Strother Moore  File: acl2-doc-emacs.info, Node: The Event Summary, Next: The Expansion of ENDP in the Induction Step (Step 0), Prev: The End of the Walking Tour, Up: Pages Written Especially for the Tours The Event Summary The Event Summary At the conclusion of most events (see *Note About the Prompt:: for a brief discussion of events or see *Note EVENTS:: <>), ACL2 prints a summary. The summary for app is: Summary Form: ( DEFUN APP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) APP The "rules" listed are those used in function admission or proof summarized. What is actually listed are "runes" (see *Note RUNE::) <>) which are list-structured unique names for rules in the ACL2 data base or "world" <>. Using theories <> you can "enable" and "disable" rules so as to make them available (or not) to the ACL2 theorem prover. The "warnings" mentioned (none are listed for app) remind the reader whether the event provoked any warnings. The warnings themselves would have been printed earlier in the processing and this part of the summary just names the earlier warnings printed. The "time" indicates how much processing time was used and is divided into three parts: the time devoted to proof, to printing, and to syntactic checks, pre-processing and data base updates. Despite the fact that ACL2 is an applicative language it is possible to measure time with ACL2 programs. The state <> contains a clock. The times are printed in decimal notation but are actually counted in integral units. The final APP is the value of the defun command and was printed by the read-eval-print loop. The fact that it is indented one space is a subtle reminder that the command actually returned an "error triple", consisting of a flag indicating (in this case) that no error occurred, a value (in this case the symbol APP), and the final state <>). See *Note LD-POST-EVAL-PRINT::<> for some details. If you really want to follow that link, however, you might see *Note LD:: <> first. You should now return to the Walking Tour.  File: acl2-doc-emacs.info, Node: The Expansion of ENDP in the Induction Step (Step 0), Next: The Expansion of ENDP in the Induction Step (Step 1), Prev: The Event Summary, Up: Pages Written Especially for the Tours The Expansion of ENDP in the Induction Step (Step 0) The Expansion of ENDP in the Induction Step (Step 0) Subgoal *1/2 (IMPLIES (AND (NOT (ENDP A)) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). Click on the link above (the open parenthesis before ENDP) to replace (ENDP A) by its definition.  File: acl2-doc-emacs.info, Node: The Expansion of ENDP in the Induction Step (Step 1), Next: The Expansion of ENDP in the Induction Step (Step 2), Prev: The Expansion of ENDP in the Induction Step (Step 0), Up: Pages Written Especially for the Tours The Expansion of ENDP in the Induction Step (Step 1) The Expansion of ENDP in the Induction Step (Step 1) Subgoal *1/2 (IMPLIES (AND (NOT (NOT (CONSP A))) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). The bold text is the instantiated definition of ENDP. Now click on the link above to simplify (NOT (NOT (CONSP A)))  File: acl2-doc-emacs.info, Node: The Expansion of ENDP in the Induction Step (Step 2), Next: The Falling Body Model, Prev: The Expansion of ENDP in the Induction Step (Step 1), Up: Pages Written Especially for the Tours The Expansion of ENDP in the Induction Step (Step 2) The Expansion of ENDP in the Induction Step (Step 2) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). Note that this is Subgoal *1/2'. You may see *Note Overview of the Simplification of the Induction Step to T:: to return to the main proof.  File: acl2-doc-emacs.info, Node: The Falling Body Model, Next: The Final Simplification in the Base Case (Step 0), Prev: The Expansion of ENDP in the Induction Step (Step 2), Up: Pages Written Especially for the Tours The Falling Body Model The Falling Body Model One particularly famous and very simple model is the equation of a falling body: the distance d an object falls is proportional to the square of the time t. If the time is measured in seconds and the distance in feet, the equation relating these two is 2 d = 16t This equation is a model of falling objects. It can be used to predict how long it takes a cannonball to fall from the top of a 200 foot tower (3.5 seconds). This might be important if your product is designed to drop cannonballs on moving targets. See *Note Corroborating Models:: to continue  File: acl2-doc-emacs.info, Node: The Final Simplification in the Base Case (Step 0), Next: The Final Simplification in the Base Case (Step 1), Prev: The Falling Body Model, Up: Pages Written Especially for the Tours The Final Simplification in the Base Case (Step 0) the Final Simplification in the Base Case (Step 0) Subgoal *1/1' (IMPLIES (NOT (CONSP A)) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). Click on the link above to replace (APP A B) by its definition. Note that the hypothesis (NOT (CONSP A)) allows us to simplify the IF in APP to its false branch this time.  File: acl2-doc-emacs.info, Node: The Final Simplification in the Base Case (Step 1), Next: The Final Simplification in the Base Case (Step 2), Prev: The Final Simplification in the Base Case (Step 0), Up: Pages Written Especially for the Tours The Final Simplification in the Base Case (Step 1) the Final Simplification in the Base Case (Step 1) Subgoal *1/1' (IMPLIES (NOT (CONSP A)) (EQUAL (APP B C) (APP A (APP B C)))). Click on the link above to expand the definition of APP. Again, we come out through the false branch because of the hypothesis.  File: acl2-doc-emacs.info, Node: The Final Simplification in the Base Case (Step 2), Next: The Final Simplification in the Base Case (Step 3), Prev: The Final Simplification in the Base Case (Step 1), Up: Pages Written Especially for the Tours The Final Simplification in the Base Case (Step 2) the Final Simplification in the Base Case (Step 2) Subgoal *1/1' (IMPLIES (NOT (CONSP A)) (EQUAL (APP B C) (APP B C))). Click on the link above to use the Axiom (EQUAL x x) = t  File: acl2-doc-emacs.info, Node: The Final Simplification in the Base Case (Step 3), Next: The First Application of the Associativity Rule, Prev: The Final Simplification in the Base Case (Step 2), Up: Pages Written Especially for the Tours The Final Simplification in the Base Case (Step 3) the Final Simplification in the Base Case (Step 3) Subgoal *1/1' (IMPLIES (NOT (CONSP A)) T) Now that its conclusion is identically T the IMPLIES will simplify to T (not shown) and we are done with Subgoal *1/1'. You may see *Note Overview of the Simplification of the Base Case to T:: to return to the main proof.  File: acl2-doc-emacs.info, Node: The First Application of the Associativity Rule, Next: The Induction Scheme Selected for the App Example, Prev: The Final Simplification in the Base Case (Step 3), Up: Pages Written Especially for the Tours The First Application of the Associativity Rule The First Application of the Associativity Rule So here we see our associativity rule being used! The rewriter sweeps the conjecture in a leftmost innermost fashion, applying rewrite rules as it goes. The associativity rule is used many times in this sweep. The first "target" is highlighted below. Click on it to see what happens: Current Conjecture: (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7) (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7)))))  File: acl2-doc-emacs.info, Node: The Induction Scheme Selected for the App Example, Next: The Induction Step in the App Example, Prev: The First Application of the Associativity Rule, Up: Pages Written Especially for the Tours The Induction Scheme Selected for the App Example The Induction Scheme Selected for the App Example (AND (IMPLIES (AND (NOT (ENDP A)) ; Induction Step: test (:P (CDR A) B C)) ; and induction hypothesis (:P A B C)) ; implies induction conclusion. (IMPLIES (ENDP A) (:P A B C))) ; Base Case The formula beginning with this parenthesis is the induction scheme suggested by (APP A B) applied to (P A B C). It is a conjunction (AND <>) of two formulas. The first is the induction step and the second is the base case.  File: acl2-doc-emacs.info, Node: The Induction Step in the App Example, Next: The Instantiation of the Induction Scheme, Prev: The Induction Scheme Selected for the App Example, Up: Pages Written Especially for the Tours The Induction Step in the App Example The Induction Step in the App Example This formula is the Induction Step. It basically consists of three parts, a test identifying the inductive case, an induction hypothesis and an induction conclusion. (IMPLIES (AND (NOT (ENDP A)) ; Test (:P (CDR A) B C)) ; Induction Hypothesis (:P A B C)) ; Induction Conclusion When we prove this we can assume * A is not empty, and that * the associativity conjecture holds for a "smaller" version of A, namely, (CDR A). Under those hypotheses we have to prove the associativity conjecture for A itself.  File: acl2-doc-emacs.info, Node: The Instantiation of the Induction Scheme, Next: The Justification of the Induction Scheme, Prev: The Induction Step in the App Example, Up: Pages Written Especially for the Tours The Instantiation of the Induction Scheme The Instantiation of the Induction Scheme The induction scheme just shown is just an abbreviation for our real goal. To obtain our actual goals we have to replace the schema :P by the associativity conjecture (instantiated as shown in the scheme). This produces two actual goals, the induction step and the base case.  File: acl2-doc-emacs.info, Node: The Justification of the Induction Scheme, Next: The Proof of the Associativity of App, Prev: The Instantiation of the Induction Scheme, Up: Pages Written Especially for the Tours The Justification of the Induction Scheme The Justification of the Induction Scheme This paragraph explains why the induction selected is legal. The explanation is basically the same as the explanation for why the recursion in (APP A B) terminates.  File: acl2-doc-emacs.info, Node: The Proof of the Associativity of App, Next: The Q.E.D. Message, Prev: The Justification of the Induction Scheme, Up: Pages Written Especially for the Tours The Proof of the Associativity of App The Proof of the Associativity of App Here is the theorem prover's output when it processes the defthm command for the associativity of app. We have highlighted text for which we offer some explanation, and broken the presentation into several pages. Just follow the Walking Tour after exploring the explanations. ACL2!>(defthm associativity-of-app (equal (app (app a b) c) (app a (app b c)))) Name the formula above *1. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (APP A B). If we let (:P A B C) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP A)) (:P (CDR A) B C)) (:P A B C)) (IMPLIES (ENDP A) (:P A B C))). This induction is justified by the same argument used to admit APP, namely, the measure (ACL2-COUNT A) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Walking Tour: *Note Overview of the Simplification of the Induction Step to T::  File: acl2-doc-emacs.info, Node: The Q.E.D. Message, Next: The Rules used in the Associativity of App Proof, Prev: The Proof of the Associativity of App, Up: Pages Written Especially for the Tours The Q.E.D. Message The Q.E.D. Message Q.E.D. stands for "quod erat demonstrandum" which is Latin for "which was to be demonstrated" and is the signal that a proof is completely done.  File: acl2-doc-emacs.info, Node: The Rules used in the Associativity of App Proof, Next: The Simplification of the Induction Conclusion (Step 0), Prev: The Q.E.D. Message, Up: Pages Written Especially for the Tours The Rules used in the Associativity of App Proof The Rules used in the Associativity of App Proof Note that under Rules we list the runes <> of all the rules used in the proof. This list says that we used the rewrite rules CAR-CONS and CDR-CONS, the definitions of the functions NOT, ENDP and APP, and primitive type reasoning (which is how we simplified the IF and EQUAL terms). For what it is worth, IMPLIES and AND are actually macros <> that are expanded into IF expressions before the proof ever begins. The use of macros is not reported among the rules.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 0), Next: The Simplification of the Induction Conclusion (Step 1), Prev: The Rules used in the Associativity of App Proof, Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 0) the Simplification of the Induction Conclusion (Step 0) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))). Click on the link above to replace (APP A B) by its definition.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 1), Next: The Simplification of the Induction Conclusion (Step 10), Prev: The Simplification of the Induction Conclusion (Step 0), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 1) the Simplification of the Induction Conclusion (Step 1) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (IF (CONSP A) (CONS (CAR A) (APPEND (CDR A) B)) B) C) (APP A (APP B C)))). Note that the IF expression above is the simplified body of APP. But we know the test (CONSP A) is true, by the first hypothesis. Click on the link above to replace the test by T. Actually this step and several subsequent ones are done during the simplification of the body of APP but we want to illustrate the basic principles of simplification without bothering with every detail.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 10), Next: The Simplification of the Induction Conclusion (Step 11), Prev: The Simplification of the Induction Conclusion (Step 1), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 10) the Simplification of the Induction Conclusion (Step 10) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APPEND (CDR A) B) C) (APP (CDR A) (APP B C)))). Click on the link above to use the Induction Hypothesis (which is the second of the two hypotheses above and which is identical to the rewritten conclusion).  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 11), Next: The Simplification of the Induction Conclusion (Step 12), Prev: The Simplification of the Induction Conclusion (Step 10), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 11) the Simplification of the Induction Conclusion (Step 11) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) T) Click on the link above to use the definition of IMPLIES. Since the conclusion of the implication is now identically T, the implication simplifies to T.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 12), Next: The Simplification of the Induction Conclusion (Step 2), Prev: The Simplification of the Induction Conclusion (Step 11), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 12) the Simplification of the Induction Conclusion (Step 12) Subgoal *1/2' T So, indeed, Subgoal *1/2' does simplify to T! You can see that even in an example as simple as this one, quite a lot happens in simplification. You may see *Note Overview of the Simplification of the Induction Step to T:: to return to the main proof.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 2), Next: The Simplification of the Induction Conclusion (Step 3), Prev: The Simplification of the Induction Conclusion (Step 12), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 2) the Simplification of the Induction Conclusion (Step 2) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (IF T (CONS (CAR A) (APPEND (CDR A) B)) B) C) (APP A (APP B C)))). Click on the link above to apply the Axiom (IF T x y) = x.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 3), Next: The Simplification of the Induction Conclusion (Step 4), Prev: The Simplification of the Induction Conclusion (Step 2), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 3) the Simplification of the Induction Conclusion (Step 3) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (CONS (CAR A) (APPEND (CDR A) B)) C) (APP A (APP B C)))). Click on the link above to apply the expand the definition of APP here.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 4), Next: The Simplification of the Induction Conclusion (Step 5), Prev: The Simplification of the Induction Conclusion (Step 3), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 4) the Simplification of the Induction Conclusion (Step 4) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (IF (CONSP (CONS (CAR A) (APPEND (CDR A) B))) (CONS (CAR (CONS (CAR A) (APPEND (CDR A) B))) (APP (CDR (CONS (CAR A) (APPEND (CDR A) B))) C)) C) (APP A (APP B C)))). Click on the link above to apply the Axiom (CONSP (CONS x y)) = T.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 5), Next: The Simplification of the Induction Conclusion (Step 6), Prev: The Simplification of the Induction Conclusion (Step 4), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 5) the Simplification of the Induction Conclusion (Step 5) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (IF T (CONS (CAR (CONS (CAR A) (APPEND (CDR A) B))) (APP (CDR (CONS (CAR A) (APPEND (CDR A) B))) C)) C) (APP A (APP B C)))). Click on the link above to apply the Axiom (CAR (CONS x y)) = x.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 6), Next: The Simplification of the Induction Conclusion (Step 7), Prev: The Simplification of the Induction Conclusion (Step 5), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 6) the Simplification of the Induction Conclusion (Step 6) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (IF T (CONS (CAR A) (APP (CDR (CONS (CAR A) (APPEND (CDR A) B))) C)) C) (APP A (APP B C)))). Click on the link above to apply the Axiom (CDR (CONS x y)) = y.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 7), Next: The Simplification of the Induction Conclusion (Step 8), Prev: The Simplification of the Induction Conclusion (Step 6), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 7) the Simplification of the Induction Conclusion (Step 7) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (IF T (CONS (CAR A) (APP (APPEND (CDR A) B) C)) C) (APP A (APP B C)))). Click on the link above to apply the Axiom (IF T x y) = x.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 8), Next: The Simplification of the Induction Conclusion (Step 9), Prev: The Simplification of the Induction Conclusion (Step 7), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 8) the Simplification of the Induction Conclusion (Step 8) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (CONS (CAR A) (APP (APPEND (CDR A) B) C)) (APP A (APP B C)))). Click on the link above to expand the definition of APP here. This time, we'll do the whole expansion at once, including the simplification of the resulting IF. This is how ACL2 actually does it.  File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 9), Next: The Summary of the Proof of the Trivial Consequence, Prev: The Simplification of the Induction Conclusion (Step 8), Up: Pages Written Especially for the Tours The Simplification of the Induction Conclusion (Step 9) the Simplification of the Induction Conclusion (Step 9) Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (CONS (CAR A) (APP (APPEND (CDR A) B) C)) (CONS (CAR A) (APP (CDR A) (APP B C))))). Click on the link above to apply the Axiom that (EQUAL (CONS x y) (CONS u v)) is equal to the conjunction of (EQUAL x u) and (EQUAL y v). In this case, (EQUAL x u) is trivial, (EQUAL (CAR A) (CAR A)).  File: acl2-doc-emacs.info, Node: The Summary of the Proof of the Trivial Consequence, Next: The Theorem that App is Associative, Prev: The Simplification of the Induction Conclusion (Step 9), Up: Pages Written Especially for the Tours The Summary of the Proof of the Trivial Consequence The Summary of the Proof of the Trivial Consequence Note that at the conclusion of the proof, the system reminds you of the earlier Warning. It is a good idea, when the Q.E.D. flys by, to see if there were any Warnings.  File: acl2-doc-emacs.info, Node: The Theorem that App is Associative, Next: The Time Taken to do the Associativity of App Proof, Prev: The Summary of the Proof of the Trivial Consequence, Up: Pages Written Especially for the Tours The Theorem that App is Associative The Theorem that App is Associative ACL2!>(defthm associativity-of-app (equal (app (app a b) c) (app a (app b c)))) The formula above says app is associative. The defthm <> command instructs ACL2 to prove the formula and to name it associativity-of-app. Actually, the defthm command also builds the formula into the data base as a rewrite <> rule, but we won't go into that just yet. What we will consider is how the ACL2 theorem prover proves this formula. If you proceed you will find the actual output of ACL2 in response to the command above. Some of the text is highlighted for the purposes of the tour. ACL2 does not highlight its output. You will note that we sometimes highlight a single open parenthesis. This is our way of drawing your attention to the subformula that begins with that parenthesis. By clicking on the parenthesis you will get an explanation of the subformula or its processing. Walking Tour: *Note The Proof of the Associativity of App::  File: acl2-doc-emacs.info, Node: The Time Taken to do the Associativity of App Proof, Next: The Tours, Prev: The Theorem that App is Associative, Up: Pages Written Especially for the Tours The Time Taken to do the Associativity of App Proof The Time Taken to do the Associativity of App Proof The time it took us to explain this proof may leave the impression that the proof is complicated. In a way, it is. But it happens quickly. The time taken to do this proof is about 1/10 second. The rest of the time (about 2/10 seconds) is spent in pre- and post-processing. Basically, this proof flashes across your screen before you can read it; you see the Q.E.D. and don't bother to scroll back to read it. You have more important things to do than read successful proofs.  File: acl2-doc-emacs.info, Node: The Tours, Next: The WARNING about the Trivial Consequence, Prev: The Time Taken to do the Associativity of App Proof, Up: Pages Written Especially for the Tours The Tours The Tours ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semi-automatic theorem prover, just to name its most common uses. This home page includes all of ACL2's online documentation, which is quite extensive. To help ease your introduction to ACL2, we have built two tours through this documentation. Newcomers to ACL2 should first take the "Flying Tour." Then, if you want to know more, take the "Walking Tour." To start a tour, click on the appropriate icon below. Flying Tour: *Note A Flying Tour of ACL2:: Walking Tour: *Note A Walking Tour of ACL2:: For readers using Web browsers: This "page" actually contains many other pages of our documentation, organized alphabetically and separated by many blank lines. Be careful when using the scroll bar! For readers using our :DOC or our TexInfo format in Emacs: The tours will probably be unsatisfying because we use gif files and assume you can navigate "back."  File: acl2-doc-emacs.info, Node: The WARNING about the Trivial Consequence, Next: Undocumented Topic, Prev: The Tours, Up: Pages Written Especially for the Tours The WARNING about the Trivial Consequence The WARNING about the Trivial Consequence This Warning alerts us to the fact that when treated as a rewrite rule, the new rule TRIVIAL-CONSEQUENCE, rewrites terms of the same form as a rule we have already proved, namely ASSOCIATIVITY-OF-APP. When you see this warning you should think about your rules! In the current case, it would be a good idea not to make TRIVIAL-CONSEQUENCE a rule at all. We could do this with :rule-classes <> nil. ACL2 proceeds to try to prove the theorem, even though it printed some warnings. The basic assumption in ACL2 is that the user understands what he or she is doing but may need a little reminding just to manage a complicated set of facts.  File: acl2-doc-emacs.info, Node: Undocumented Topic, Next: Using the Associativity of App to Prove a Trivial Consequence, Prev: The WARNING about the Trivial Consequence, Up: Pages Written Especially for the Tours Undocumented Topic Undocumented Topic This topic has not yet been documented. Sorry  File: acl2-doc-emacs.info, Node: Using the Associativity of App to Prove a Trivial Consequence, Next: What Is ACL2(Q), Prev: Undocumented Topic, Up: Pages Written Especially for the Tours Using the Associativity of App to Prove a Trivial Consequence Using the Associativity of App to Prove a Trivial Consequence If we have proved the associativity-of-app rule, then the following theorem is trivial: (defthm trivial-consequence (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7) (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7)))))) Below we show the proof Walking Tour: *Note Overview of the Proof of a Trivial Consequence::  File: acl2-doc-emacs.info, Node: What Is ACL2(Q), Next: What is Required of the User(Q), Prev: Using the Associativity of App to Prove a Trivial Consequence, Up: Pages Written Especially for the Tours What Is ACL2(Q) What Is ACL2? ACL2 is a mathematical logic together with a mechanical theorem prover to help you reason in the logic. The logic is just a subset of applicative Common Lisp. The theorem prover is an "industrial strength" version of the Boyer-Moore theorem prover, Nqthm. Models of all kinds of computing systems can be built in ACL2, just as in Nqthm, even though the formal logic is Lisp. Once you've built an ACL2 model of a system, you can run it. You can also use ACL2 to prove theorems about the model. Flying Tour: *Note What is a Mathematical Logic(Q)::  File: acl2-doc-emacs.info, Node: What is Required of the User(Q), Next: What is a Mathematical Logic(Q), Prev: What Is ACL2(Q), Up: Pages Written Especially for the Tours What is Required of the User(Q) What is Required of the User? It is not easy to build ACL2 models of complex systems. To do so, the user must understand * the system being modeled, and * ACL2, at least as a programming language. It is not easy to get ACL2 to prove hard theorems. To do so, the user must understand * the model, * ACL2 as a mathematical logic, and * be able to construct a proof (in interaction with ACL2). ACL2 will help construct the proof but its primary role is to prevent logical mistakes. The creative burden -- the mathematical insight into why the model has the desired property -- is the user's responsibility. Flying Tour: *Note How Long Does It Take to Become an Effective User(Q)::  File: acl2-doc-emacs.info, Node: What is a Mathematical Logic(Q), Next: What is a Mechanical Theorem Prover(Q), Prev: What is Required of the User(Q), Up: Pages Written Especially for the Tours What is a Mathematical Logic(Q) What is a Mathematical Logic? A mathematical logic is a formal system of formulas (axioms) and rules for deriving other formulas, called theorems. A proof is a derivation of a theorem. To see a concrete proof tree, see *Note A Trivial Proof::. Why should you care? The neat thing about Theorems is that they are "true." More precisely, if all the axioms are valid and the rules are validity preserving, then anything derived from the axioms via the rules is valid. So, if you want to determine if some formula is true, prove it. Flying Tour: *Note What is a Mechanical Theorem Prover(Q)::  File: acl2-doc-emacs.info, Node: What is a Mechanical Theorem Prover(Q), Next: What is a Mechanical Theorem Prover(Q) (continued), Prev: What is a Mathematical Logic(Q), Up: Pages Written Especially for the Tours What is a Mechanical Theorem Prover(Q) What is a Mechanical Theorem Prover? A mechanical theorem prover is a computer program that finds proofs of theorems. The ideal mechanical theorem prover is automatic: you give it a formula and it gives you a proof of that formula or tells you there is no proof. Unfortunately, automatic theorem provers can be built only for very simple logics (e.g., propositional calculus) and even then practical considerations (e.g., how many centuries you are willing to wait) limit the problems they can solve. Flying Tour: *Note What is a Mechanical Theorem Prover(Q) (continued)::  File: acl2-doc-emacs.info, Node: What is a Mechanical Theorem Prover(Q) (continued), Next: You Must Think about the Use of a Formula as a Rule, Prev: What is a Mechanical Theorem Prover(Q), Up: Pages Written Especially for the Tours What is a Mechanical Theorem Prover(Q) (continued) What is a Mechanical Theorem Prover? (continued) To get around this, mechanical theorem provers often require help from the user. See *Note ACL2 as an Interactive Theorem Prover:: to continue downward. Flying Tour: *Note About Models::  File: acl2-doc-emacs.info, Node: You Must Think about the Use of a Formula as a Rule, Prev: What is a Mechanical Theorem Prover(Q) (continued), Up: Pages Written Especially for the Tours You Must Think about the Use of a Formula as a Rule You Must Think about the Use of a Formula as a Rule This is good and bad. The good news is that you can program ACL2's simplifier. The bad news is that when you command ACL2 to prove a theorem you must give some thought to how that theorem is to be used as a rule! For example, if you engaged in the mathematically trivial act of proving the associativity rule again, but with the equality reversed, you would have programmed ACL2's rewriter to loop forever. You can avoid adding any rule by using the command: (defthm associativity-of-app (equal (app (app a b) c) (app a (app b c))) :rule-classes nil) Walking Tour: *Note Using the Associativity of App to Prove a Trivial Consequence::  File: acl2-doc-emacs.info, Node: RELEASE-NOTES, Next: RULE-CLASSES, Prev: Pages Written Especially for the Tours, Up: Top RELEASE-NOTES pointers to what has changed * Menu: * NOTE1:: Acl2 Version 1.1 Notes * NOTE2:: Acl2 Version 1.2 Notes * NOTE3:: Acl2 Version 1.3 Notes * NOTE4:: Acl2 Version 1.4 Notes * NOTE5:: Acl2 Version 1.5 Notes * NOTE6:: Acl2 Version 1.6 Notes * NOTE7:: ACL2 Version 1.7 (released October 1994) Notes * NOTE8:: ACL2 Version 1.8 (May, 1995) Notes * NOTE8-UPDATE:: ACL2 Version 1.8 (Summer, 1995) Notes * NOTE9:: ACL2 Version 1.9 (Fall, 1996) Notes This section of the online documentation contains notes on the changes that distinguish successive released versions of ACL2. The current version of ACL2 is the value of the constant *acl2-version*.  File: acl2-doc-emacs.info, Node: NOTE1, Next: NOTE2, Prev: RELEASE-NOTES, Up: RELEASE-NOTES NOTE1 Acl2 Version 1.1 Notes The new features are extensively documented. The relevant topics are: * Menu: Related topics other than immediate subtopics: * BOOKS:: files of ACL2 event forms * GUARD:: restricting the domain of a function * MORE:: your response to :doc or :more-doc's "(cont'd)" * REDUNDANT-EVENTS:: allowing a name to be introduced "twice" It is especially important to read all of of the documentation for books before trying to use books. However, the new :more keyword command is so handy for reading long documentation strings that we recommend you start with :doc more if reading at the terminal. Some documentation has been written for guards which you might find interesting.  File: acl2-doc-emacs.info, Node: NOTE2, Next: NOTE3, Prev: NOTE1, Up: RELEASE-NOTES NOTE2 Acl2 Version 1.2 Notes Hacker mode has been eliminated and programming mode has been added. Programming mode is unsound but does syntax checking and permits redefinitions of names. See :doc load-mode and :doc g-mode. The arguments to ld have changed. Ld is now much more sophisticated. See *Note LD::. For those occasions on which you wish to look at a large list structure that you are afraid to print, try (walkabout x state), where x is an Acl2 expression that evaluates to the structure in question. I am afraid there is no documentation yet, but it is similar in spirit to the Interlisp structure editor. You are standing on an object and commands move you around in it. E.g., 1 moves you to its first element, 2 to its second, etc.; 0 moves you up to its parent; nx and bk move you to its next sibling and previous sibling; pp prettyprints it; q exits returning nil; = exits returning the thing you're standing on; (= symb) assigns the thing you're standing on to the state global variable symb. Several new hints have been implemented, including :by and :do-not. The old :do-not-generalize has been scrapped in favor of such new hints as :do-not (generalize elim). :By lets you say "this goal is subsumed by" a given lemma instance. The :by hint also lets you say "this goal can't be proved yet but skip it and see how the rest of the proof goes." See *Note HINTS::.  File: acl2-doc-emacs.info, Node: NOTE3, Next: NOTE4, Prev: NOTE2, Up: RELEASE-NOTES NOTE3 Acl2 Version 1.3 Notes Programming mode has been eliminated. Instead, all functions have a "color" which indicates what can be done with the function. For example, :red functions can be executed but have no axioms describing them. Thus, :red functions can be introduced after passing a simple syntactic check and they can be redefined without undoing. But nothing of consequence can be proved about them. At the other extreme are :gold functions which can be executed and which also have passed both the termination and the guard verification proofs. The color of a function can be specified with the new xargs keyword, :color, which, if omitted defaults to the global setting of ld-color. Ld-color replaces load-mode. Setting ld-color to :red causes behavior similar to the old :g-mode. Setting ld-color to :gold causes behavior similar to the old :v-mode. It is possible to prototype your system in :red and then convert :red functions to :blue individually by calling verify-termination on them. They can then be converted to :gold with verify-guards. This allows us to undertake to verify the termination and guards of system functions. See :doc color for an introduction to the use of colors. Type prescription rules have been added. Recall that in Nqthm, some rewrite rules were actually stored as "type-prescriptions." Such rules allow the user to inform Nqthm's primitive type mechanism as to the kinds of shells returned by a function. Earlier versions of Acl2 did not have an analogous kind of rule because Acl2's type mechanism is complicated by guards. Version 1.3 supports type-prescription rules. See *Note TYPE-PRESCRIPTION::. Three more new rule-classes implement congruence-based rewriting. It is possible to identify a binary relation as an equivalence relation (see *Note EQUIVALENCE::), to show that one equivalence relation refines another (see *Note REFINEMENT::) and to show that a given equivalence relation is maintained when rewriting a given function call, e.g., (fn ...xk...), by maintaining another equivalence relation while rewriting the kth argument (see *Note CONGRUENCE::). If r has been shown to be an equivalence relation and then (implies hyps (r (foo x) (bar x))) is proved as a :rewrite rule, then instances of (foo x) will be replaced by corresponding instances of (bar x) provided the instance occurs in a slot where the maintainence of r-equivalence is known to be sufficient and hyps can be established as usual. In Version 1.2, rule-classes were simple keywords, e.g., :rewrite or :elim. In Version 1.3, rule-classes have been elaborated to allow you to specify how the theorem ought to be used as a rule. That is, the new rule-classes allows you to separate the mathematical statement of the formula from its interpretation as a rule. See *Note RULE-CLASSES::. Rules used to be named by symbols, e.g., car and car-cons were the names of rules. Unfortunately, this was ambiguous because there are three rules associated with function symbols: the symbolic definition, the executable counterpart, and the type-prescription; many different rules might be associated with theorems, depending on the rule classes. In Version 1.3 rules are named by "runes" (which is just short hand for "rule names"). Example runes are (:definition car), (:executable-counterpart car), and (:type-prescription car . 1). Every rule added by an event has a different name and you can enable and disable them independently. See *Note RUNE:: and see *Note THEORIES::. The identity function force, of one argument, has been added and given a special interpretation by the functions responsible for establishing hypotheses in backchaining: When the system fails to establish some hypothesis of the form (force term), it simply assumes it is true and goes on, delaying until later the establishment of term. In particular, pushes a new subgoal to prove term in the current context. When that subgoal is attacked, all of the resources of the theorem prover, not just rewriting, are brought to bear. Thus, for example, if you wish to prove the rule (implies (good-statep s) (equal (exec s n) s')) and it is your expectation that every time exec appears its first argument is a good-statep then you might write the rule as (implies (force (good-statep s)) (equal (exec s n) s')). This rule is essentially an unconditional rewrite of (exec s n) to s' that spawns the new goal (good-statep s). See *Note FORCE::. Because you can now specify independently how a theorem is used as a rule, you need not write the force in the actual theorem proved. See *Note RULE-CLASSES::. Version 1.3 supports a facility similar to Nqthm's break-lemma. See *Note BREAK-REWRITE::. You can install "monitors" on runes that will cause interactive breaks under certain conditions. Acl2 also provides "wormholes" which allow you to write functions that cause interaction with the user but which do not require that you have access to state. See *Note WORMHOLE::. The rewriter now automatically backchains to stronger recognizers. There is no user hook to this feature but it may simplify some proofs with which older versions of Acl2 had trouble. For example, if the rewriter is trying to prove (rationalp (foo a b c)) it is now smart enough to try lemmas that match with (integerp (foo a b c)).  File: acl2-doc-emacs.info, Node: NOTE4, Next: NOTE5, Prev: NOTE3, Up: RELEASE-NOTES NOTE4 Acl2 Version 1.4 Notes Once again ld only takes one required argument, as the bind-flg has been deleted. Three commands have been added in the spirit of :pe. :Pe! is similar to :pe but it prints all events with the given name, rather than just the most recent. The command :pf prints the corollary formula corresponding to a name or rune. The command :pl (print lemmas) prints rules whose top function symbol is the given name. See *Note PE!::, see *Note PF::, and see *Note PL::. Book naming conventions have been changed somewhat. The once-required .lisp extension is now prohibited! Directories are supported, including a notion of "connected book directory". See *Note BOOK-NAME::. Also, the second argument of certify-book is now optional, defaulting to 0. Compilation is now supported inside the Acl2 loop. See *Note COMP::and see *Note SET-COMPILE-FNS::. The default color is now part of the Acl2 world; see :doc default-color. Ld-color is no longer an ld special. Instead, colors are events; see the documentation for red, pink, blue, and gold. A table exists for controlling whether Acl2 prints comments when it forces hypotheses of rules; see :doc force-table. Also, it is now possible to turn off the forcing of assumptions by disabling the definition of force; see *Note FORCE::. The event defconstant is no longer supported, but a very similar event, defconst, has been provided in its place. See *Note DEFCONST::. The event for defining congruence relations is now defcong (formerly, defcon). Patterns are now allowed in :expand hints. See the documentation for :expand inside the documentation for hints. We have improved the way we report rules used by the simplifier. All runes of the same type are reported together in the running commentary associated with each goal, so that for example, executable counterparts are listed separately from definitions, and rewrite rules are listed separately from linear rules. The preprocessor now mentions "simple" rules; see *Note SIMPLE::. The mechanism for printing warning messages for new rewrite rules, related to subsumption, now avoids worrying about nonrecursive function symbols when those symbols are disabled. These messages have also been eliminated for the case where the old rule is a :definition rule. Backquote has been modified so that it can usually provide predictable results when used on the left side of a rewrite rule. Time statistics are now printed even when an event fails. The Acl2 trace package has been modified so that it prints using the values of the Lisp globals *print-level* and *print-length* (respectively). Table has been modified so that the :clear option lets you replace the entire table with one that satisfies the val and key guards (if any); see *Note TABLE::. We have relaxed the translation rules for :measure hints to defun, so that the the same rules apply to these terms that apply to terms in defthm events. In particular, in :measure hints mv is treated just like list, and state receives no special handling. The loop-stopper test has been relaxed. The old test required that every new argument be strictly less than the corresponding old argument in a certain term-order. The new test uses a lexicographic order on term lists instead. For example, consider the following rewrite rule. (equal (variable-update var1 val1 (variable-update var2 val2 vs)) (variable-update var2 val2 (variable-update var1 val1 vs))) This rule is permutative. Now imagine that we want to apply this rule to the term (variable-update u y (variable-update u x vs)). Since the actual corresponding to both var1 and var2 is u, which is not strictly less than itself in the term-order, this rule would fail to be applied in this situation when using the old test. However, since the pair (u x) is lexicographically less than the pair (u y) with respect to our term-order, the rule is in fact applied using our new test. Messages about events now contain a space after certain left parentheses, in order to assist emacs users. For example, the event (defthm abc (equal (+ (len x) 0) (len x))) leads to a summary containing the line Form: ( DEFTHM ABC ...) and hence, if you search backwards for "(defthm abc", you won't stop at this message. More tautology checking is done during a proof; in fact, no goal printed to the screen, except for the results of applying :use and :by hints or the top-level goals from an induction proof, are known to Acl2 to be tautologies. The ld-query-control-alist may now be used to suppress printing of queries; see *Note LD-QUERY-CONTROL-ALIST::. Warning messages are printed with short summary strings, for example the string "Use" in the following message. Acl2 Warning [Use] in DEFTHM: It is unusual to :USE an enabled :REWRITE or :DEFINITION rule, so you may want to consider disabling FOO. At the end of the event, just before the time is printed, all such summary strings are printed out. The keyword command :u has been introduced as an abbreviation for :ubt :max. Printing of query messages is suppressed by :u. The keyword :cheat is no longer supported by any event form. Some irrelevant formals are detected; see *Note IRRELEVANT-FORMALS::. A bug in the application of metafunctions was fixed: now if the output of a metafunction is equal to its input, the application of the metafunction is deemed unsuccessful and the next metafunction is tried. An example has been added to the documentation for equivalence to suggest how to make use of equivalence relations in rewriting. The following Common Lisp functions have been added to Acl2: alpha-char-p, upper-case-p, lower-case-p, char-upcase, char-downcase, string-downcase, string-upcase, and digit-charp-p. A documentation section called proof-checker has been added for the interactive facility, whose documentation has been slightly improved. See in particular the documentation for proof-checker, verify, and macro-command. A number of events that had been inadvertently disallowed in books are now permitted in books. These are: defcong, defcor, defequiv, defrefinement, defstub, and verify-termination.