This is documentation for ACL2 Version 3.4
Copyright (C) 2008  University of Texas at Austin

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
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

PROOF-TREE-BINDINGS    using emacs with proof trees

The key bindings set up when you start proof trees are shown below.
See PROOF-TREE-EMACS for how to get started with proof trees.

        C-z h               help
        C-z ?               help

Provides information about proof-tree/checkpoint tool.  Use `C-h d' to
get more detailed information for specific functions.

        C-z c               Go to checkpoint

Go to a checkpoint, as displayed in the "prooftree" buffer with the
character c in the first column.  With non-zero prefix argument: move
the point in the ACL2 buffer (emacs variable *mfm-buffer*) to the first
checkpoint displayed in the "prooftree" buffer, suspend the proof tree
(see suspend-proof-tree), and move the cursor below that checkpoint in
the "prooftree" buffer.  Without a prefix argument, go to the first
checkpoint named below the point in the "prooftree" buffer (or if there
is none, to the first checkpoint).  Note however that unless the proof
tree is suspended or the ACL2 proof is complete or interrupted, the
cursor will be generally be at the bottom of the "prooftree" buffer
each time it is modified, which causes the first checkpoint to be the
one that is found.

If the prefix argument is 0, move to the first checkpoint but do not
keep suspended.

        C-z g               Goto subgoal

Go to the specified subgoal in the ACL2 buffer (emacs variable
*mfm-buffer*) that lies closest to the end of that buffer - except if
the current buffer is "prooftree" when this command is invoked, the
subgoal is the one from the proof whose tree is displayed in that
buffer.  A default is obtained, when possible, from the current line of
the current buffer.

        C-z r               Resume proof tree

Resume original proof tree display, re-creating buffer "prooftree" if
necessary.  See also suspend-proof-tree.  With prefix argument: push the
mark, do not modify the windows, and move point to end of *mfm-buffer*.

        C-z s               Suspend proof tree

Freeze the contents of the "prooftree" buffer, until resume-proof-tree
is invoked.  Unlike stop-proof-tree, the only effect of
suspend-proof-tree is to stop putting characters into the "prooftree"
buffer; in particular, strings destined for that buffer continue NOT to
be put into the primary buffer, which is the value of the emacs variable
*mfm-buffer*.

       C-z o                Select other frame
       C-z b                Switch to "prooftree" buffer
       C-z B                Switch to frame called "prooftree-frame"

These commands move between buffers and frames, as indicated.  The
first of these has nothing specifically to do with proof trees, but is
handy if you have at least two emacs frames displayed.  The second
takes you to the "prooftree" buffer (in the current frame), while the
third takes you to the frame called "prooftree-frame", creating it if
it does not already exist.

PROOF-TREE-EXAMPLES    proof tree example

See 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 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 ...)
     <<PROOF TREE IS EMPTY>>

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 ...)
     <<PROOF TREE IS EMPTY>>

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.

START-PROOF-TREE    start displaying proof trees during proofs

Also see PROOF-TREE and see STOP-PROOF-TREE.  Note that
:start-proof-tree works by removing 'proof-tree from the
inhibit-output-lst; see SET-INHIBIT-OUTPUT-LST.

Explanations of proof tree displays, including emacs support, may be
found elsewhere; see PROOF-TREE and see
PROOF-TREE-EMACS.  In a nutshell: :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.

STOP-PROOF-TREE    stop displaying proof trees during proofs

Also see PROOF-TREE and see START-PROOF-TREE.  Note that
:stop-proof-tree works by adding 'proof-tree to the inhibit-output-lst;
see 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.

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.

Generally, the topics listed above will not be of use to the ACL2 user.

A Flying Tour of ACL2    A Flying Tour of ACL2

Next on the Flying Tour:  About the ACL2 Home Page

On this tour you will learn a little about what ACL2 is for rather than
how ACL2 works.  At the top and bottom bottom of the "page" (which may
extend beyond the end of your screen) there is a small "flying tour"
icon.  Click on either icon 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.

Next on the Flying Tour:  About the ACL2 Home Page

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.

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.

A Trivial Proof    A Trivial Proof

A Typical State    A Typical State

Next on the Flying Tour:  Functions for Manipulating these Objects

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 pieces.

The functions we need to manipulate these objects do things like
concatenate, reverse, sort, search, count, etc.

Next on the Flying Tour:  Functions for Manipulating these Objects

A Walking Tour of ACL2    A Walking Tour of ACL2

Next on the Walking Tour:  Common Lisp

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 follow the Walking Tour icon at the top
or 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.

Next on the Walking Tour:  Common Lisp

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 CHARACTERS <>.

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
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 TRUE-LISTP <>) is either nil or a
proper cons.  (A b c . 7) is an improper cons and hence not a true list.

ACL2 Strings    ACL2 Strings

Strings of ACL2 characters are written as sequences of characters
delimited by "double quotation marks" (").  To put a double quotation
mark in a string (or, any other character such as backslash or newline
that seems to cause problems), 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 PROGRAMMING <> where we
list all of the primitive ACL2 functions.  Alternatively, see any
Common Lisp language documentation.

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 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 SYMBOL-PACKAGE-NAME <> and see 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 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.

ACL2 System Architecture    ACL2 System Architecture

Next on the Walking Tour:  Rewrite Rules are Generated from DEFTHM Events

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.

Next on the Walking Tour:  Rewrite Rules are Generated from DEFTHM Events

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 ACL2 as an Interactive Theorem Prover (cont) to continue.

ACL2 as an Interactive Theorem Prover (cont)    ACL2 as an Interactive Theorem Prover (cont)

Next on the Walking Tour:  ACL2 System Architecture

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 ACL2 System Architecture to continue.

Next on the Walking Tour:  ACL2 System Architecture

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 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.

About Models    About Models

Next on the Flying Tour:  Models of Computer Hardware and Software

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 Models in Engineering for more discussion of these
assertions in an engineering context.

Next on the Flying Tour:  Models of Computer Hardware and Software

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.

About the ACL2 Home Page    About the ACL2 Home Page

Next on the Flying Tour:  What Is ACL2(Q)

The ACL2 Home Page is integrated into the ACL2 online documentation.
Over 1.5 megabytes of text is available here.

The vast majority of the text is user-level documentation.  For
example, to find out about rewrite <> rules you could click on the word
"rewrite <>."  But before you do that remember that you must then use
your browser's back commands to come back here.

The tiny warning signs <> mark pointers that lead out of the
introductory-level material and into the user documentation.  If you are
taking the Flying Tour, we advise you to avoid following such pointers
the first time; it is easy to get lost in the full documentation unless
you are pursuing the answer to a specific question.  If you do wander
down these other paths, remember you can back out to a page containing
the Flying Tour icon to resume the tour.

At the end of the tour you will have a chance to return to The Flight
Plan where you can revisit the main stops of the Flying Tour and
explore the alternative paths more fully.

Finally, every page contains two icons at the bottom.  The ACL2 icon
leads you back to the ACL2 Home Page.  The Index icon allows you to
browse an alphabetical listing of all the topics in ACL2's online
documentation.

Next on the Flying Tour:  What Is ACL2(Q)

About the Admission of Recursive Definitions    About the Admission of Recursive Definitions

You can't just add any formula as an axiom or definition and expect the
logic to stay sound!  The purported "definition" of APP must have
several properties to be admitted to the logic as a new axiom

The key property a recursive definition must have is that the recursion
terminate.  This, along with some syntactic criteria, ensures us that
there exists a function satisfying the definition.

Termination must be proved before the definition is admitted.  This is
done in general by finding a measure of the arguments of the function
and a well-founded relation such that the arguments "get smaller" every
time a recursive branch is taken.

For app the measure is the "size" of the first argument, x, as
determined by the primitive function acl2-count <>.  The well-founded
relation used in this example is o-p <>, which is the standard ordering
on the ordinals less than "epsilon naught."  These particular choices
for app were made "automatically" by ACL2.  But they are in fact
determined by various "default" settings.  The user of ACL2 can change
the defaults or specify a "hint" to the defun <> command to specify the
measure and relation.

You should now return to the Walking Tour.

About the Prompt    About the Prompt

The string "ACL2 !>" is the ACL2 prompt.

The prompt tells the user that an ACL2 command <>is expected.  In
addition, the prompt tells us a little about the current state of the
ACL2 command interpreter.  We explain the prompt briefly below.  But
first we talk about the command interpreter.

An ACL2 command is generally a Lisp expression to be evaluated.  There
are some unusual commands (such as :q <> for quitting ACL2) which cause
other behavior.  But most commands are read, evaluated, and then have
their results printed.  Thus, we call the command interpreter a
"read-eval-print loop."  The ACL2 command interpreter is named LD <>
(after Lisp's "load").

A command like (defun app (x y) ...) causes ACL2 to evaluate the defun
<> function on app, (x y) and ....  When that command is evaluated it
prints some information to the terminal explaining the processing of
the proposed definition.  It returns the symbol APP as its value, which
is printed by the command interpreter.  (Actually, defun is not a
function but a macro which expands to a form that involves state <>, a
necessary precondition to printing output to the terminal and to
"changing" the set of axioms.  But we do not discuss this further here.)

The defun command is an example of a special kind of command called an
"event."  Events <> are those commands that change the "logical world"
by adding such things as axioms or theorems to ACL2's data base.  See
WORLD <>.  But not every command is an event command.

A command like (app '(1 2 3) '(4 5 6 7)) is an example of a non-event.
It is processed the same general way:  the function app is applied to
the indicated arguments and the result is printed.  The function app
does not print anything and does not change the "world."

A third kind of command are those that display information about the
current logical world or that "backup" to previous versions of the
world.  Such commands are called "history" <> commands.

What does the ACL2 prompt tell us about the read-eval-print loop?  The
prompt "ACL2 !>" tells us that the command will be read with
current-package <> set to "ACL2", that guard checking (see
SET-GUARD-CHECKING <>) is on ("!"), and that we are at the top-level
(there is only one ">").  For more about the prompt, see
DEFAULT-PRINT-PROMPT <>.

You should now return to the Walking Tour.

An Example Common Lisp Function Definition    An Example Common Lisp Function Definition

Next on the Walking Tour:  An Example of ACL2 in Use

Consider the binary trees x and y below.

In Lisp, x is written as the list '(A B) or, equivalently, as '(A B .
NIL).  Similarly, y may be written '(C D E).  Suppose we wish to
replace the right-most tip of x by the entire tree y.   This is denoted
(app x y), where app stands for "append".

We can define app with:

     (defun app (x y)                           ; Concatenate x and y.
       (declare (type (satisfies true-listp) x)); We expect x to end in NIL.
       (cond ((endp x) y)                       ; If x is empty, return y.
             (t (cons (car x)                   ; Else, copy first node
                      (app (cdr x) y)))))       ;  and recur into next.

If you defined this function in some Common Lisp, then to run app on
the x and y above you could then type

     (app '(A B) '(C D E))

and Common Lisp will print the result (A B C D E).

Next on the Walking Tour:  An Example of ACL2 in Use

An Example of ACL2 in Use    An Example of ACL2 in Use

Next on the Walking Tour:  How To Find Out about ACL2 Functions

To introduce you to ACL2 we will consider the app function discussed in
the Common Lisp page, except we will omit for the moment the declare
form, which in ACL2 is called a guard.    We will deal with guards
later.

Here is the definition again

     (defun app (x y)
       (cond ((endp x) y)
             (t (cons (car x)
                      (app (cdr x) y)))))

The next few stops along the Walking Tour will show you

       * how to use the ACL2 documentation,
       * what happens when the above definition is submitted to ACL2,
       * what happens when you evaluate calls of app,
       * what one simple theorem about app looks like,
       * how ACL2 proves the theorem, and
       * how that theorem can be used in another proof.

Along the way we will talk about the definitional principle, types, the
ACL2 read-eval-print loop, and how the theorem prover works.

When we complete this part of the tour we will introduce the notion of
guards and revisit several of the topics above in that context.

Next on the Walking Tour:  How To Find Out about ACL2 Functions