This is documentation for ACL2 Version 3.0
Copyright (C) 2006  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.

Conversion    Conversion to Uppercase

When symbols are read by Common Lisp they are converted to upper case.
Note carefully that this remark applies to the characters in *symbols*.
The characters in strings are not converted upper case.

To type a symbol containing lower case characters you can enclose the
symbol in vertical bars, as in |AbC| or you can put a "backslash" before
each lower case character you wish to preserve, as in A\bC.  |AbC| and
A\bC are two different ways of writing the same symbol (just like 2/4
and 1/2 are two different ways of writing the same rational).  The
symbol has three characters in its name, the middle one of which is a
lower case b.

Corroborating Models    Corroborating Models

After producing a model, it must be corroborated against reality.  The
Falling Body Model has been corroborated by a vast number of experiments
in which the time and distance were measured and compared according to
the formula.  In general all models must be corroborated by experiment.

The Falling Body Model can be derived from deeper models, namely
Newton's laws of motion and the assertion that, over the limited
distances concerned, graviation exerts a constant acceleration on the
object.  When the model in question can be derived from other models, it
is the other models that are being corroborated by our experiments.

Because nature is not formal, we cannot prove that our models of it are
correct.  All we can do is test our models against nature's behavior.

Such testing often exposes restrictions on the applicability of our
models.  For example, the Falling Body Model is inaccurate if air
resistance is significant.  Thus, we learn not to use that model to
predict how long it takes a feather to fall from a 200 foot tower in the
earth's atmosphere.

In addition, attempts at corroboration might reveal that the model is
actually incorrect.  Careful measurements might expose the fact that the
gravitational force increases as the body falls closer to earth.  Very
careful measurements might reveal relativistic effects.  Technically,
the familiar Falling Body Model is just wrong, even under excessive
restrictions such as "in a perfect vacuum" and "over small distances."
But it is an incredibly useful model nonetheless.

There are several morals here.

Models need not be complete to be useful.

Models need not be perfectly accurate to be useful.

The user of a model must understand its limitations.

Flying Tour: Models of Computer Hardware and Software

Evaluating App on Sample Input    Evaluating App on Sample Input

     ACL2 !>(app nil '(x y z))
     (X Y Z)

     ACL2 !>(app '(1 2 3) '(4 5 6 7))
     (1 2 3 4 5 6 7)

     ACL2 !>(app '(a b c d e f g) '(x y z))   ; see Conversion for an explanation
     (A B C D E F G X Y Z)

     ACL2 !>(app (app '(1 2) '(3 4)) '(5 6))
     (1 2 3 4 5 6)

     ACL2 !>(app '(1 2) (app '(3 4) '(5 6)))
     (1 2 3 4 5 6)

     ACL2!>(let ((a '(1 2))
                 (b '(3 4))
                 (c '(5 6)))
             (equal (app (app a b) c)
                    (app a (app b c))))
     T

As we can see from these examples, ACL2 functions can be executed more
or less as Common Lisp.

The last three examples suggest an interesting property of app.

Walking Tour: The Associativity of App

Flawed Induction Candidates in App Example    Flawed Induction Candidates in App Example

Induction on a is unflawed: every occurrence of a in the conjecture

     (equal (app (app a b) c)
            (app a (app b c)))

is in a position being recursively decomposed!

Now look at the occurrences of b.  The first (shown in bold below) is in
a position that is held constant in the recursion of (app a b).  It
would be "bad" to induct on b here.

     (equal (app (app a b) c)
            (app a (app b c)))

Free Variables in Top-Level Input    Free Variables in Top-Level Input

     ACL2 !>(equal (app (app a b) c)
                   (app a (app b c))))

     ACL2 Error in TOP-LEVEL:  Global variables, such as C, B, and A, are
     not allowed. See :DOC ASSIGN and :DOC @.

ACL2 does not allow "global variables" in top-level input.  There is no
"top-level binding environment" to give meaning to these variables.

Thus, expressions involving no variables can generally be evaluated,

     ACL2 !>(equal (app (app '(1 2) '(3 4)) '(5 6))
                   (app '(1 2) (app '(3 4) '(5 6))))
     (1 2 3 4 5 6)

but expressions containing variables cannot.

There is an exception to rule.  References to "single-threaded objects"
may appear in top-level forms.  See STOBJ <>.  A single-threaded
object is an ACL2 object, usually containing many fields, whose use is
syntactically restricted so that it may be given as input only to
certain functions and must be returned as output by certain functions.
These restrictions allow single- threaded objects to be efficiently
manipulated.  For example, only a single copy of the object actually
exists, even though from a logical perspective one might expect the
object to be "copied on write."

The most commonly used single-threaded object in ACL2 is the ACL2 system
state, whose current value is always held in the variable state <>.

ACL2 provides a way for you to use state to save values of computations
at the top-level and refer to them later.  See assign <> and @ <>.

Functions for Manipulating these Objects    Functions for Manipulating these Objects

Consider a typical "stack" of control frames.

Suppose the model required that we express the idea of "the most recent
frame whose return program counter points into MAIN."

The natural expression of this notion involves

function application -- "fetch the return-pc of this frame"

case analysis -- "if the pc is MAIN, then ..."

iteration or recursion -- "pop this frame off and repeat."

The designers of ACL2 have taken the position that a programming
language is the natural language in which to define such notions,
provided the language has a mathematical foundation so that models can
be analyzed and properties derived logically.

is the language supported by ACL2.  See Common Lisp for an
optional and very brief introduction to Common Lisp.

Flying Tour: Modeling in ACL2

Guards    Guards

Common Lisp functions are partial; they are not defined for all possible
inputs.  But ACL2 functions are total.  Roughly speaking, the logical
function of a given name in ACL2 is a completion of the Common Lisp
function of the same name obtained by adding some arbitrary but
"natural" values on arguments outside the "intended domain" of the
Common Lisp function.

ACL2 requires that every ACL2 function symbol have a "guard," which may
be thought of as a predicate on the formals of the function describing
the intended domain.  The guard on the primitive function car <>, for
example, is (or (consp x) (equal x nil)), which requires the argument to
be either an ordered pair or nil.  We will discuss later how to specify
a guard for a defined function; when one is not specified, the guard is
t which is just to say all arguments are allowed.

But guards are entirely extra-logical: they are not involved in the
axioms defining functions.  If you put a guard on a defined function,
the defining axiom added to the logic defines the function on all
arguments, not just on the guarded domain.

So what is the purpose of guards?

The key to the utility of guards is that we provide a mechanism, called
"guard verification," for checking that all the guards in a formula are
true.  See VERIFY-GUARDS.  This mechanism will attempt to prove
that all the guards encountered in the evaluation of a guarded function
are true every time they are encountered.

For a thorough discussion of guards, see the paper [km97] in the ACL2
bibliography.

Guessing the Type of a Newly Admitted Function    Guessing the Type of a Newly Admitted Function

When a function is admitted to the logic, ACL2 tries to "guess" what
type of object it returns.  This guess is codified as a term that
expresses a property of the value of the function.  For app the term is

     (OR (CONSP (APP X Y))
         (EQUAL (APP X Y) Y))

which says that app returns either a cons or its second argument.  This
formula is added to ACL2's rule base as a type-prescription <> rule.
Later we will discuss how rules are used by the ACL2 theorem prover.
The point here is just that when you add a definition, the data base of
rules is updated, not just by the addition of the definitional axiom,
but by several new rules.

You should now return to the Walking Tour.

Guiding the ACL2 Theorem Prover    Guiding the ACL2 Theorem Prover

Now that you have seen the theorem prover in action you might be curious
as to how you guide it.

The idea is that the user submits conjectures and advice and reads the
proof attempts as they are produced.

Most of the time, the conjectures submitted are lemmas to be used in the
proofs of other theorems.

Walking Tour: ACL2 as an Interactive Theorem Prover (cont)

Hey Wait!  Is ACL2 Typed or Untyped(Q)    Hey Wait!  Is ACL2 Typed or Untyped?

The example

     ACL2 !>(app 7 27)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol ENDP, which
     is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
     call (ENDP 7).

illustrates the fact that while ACL2 is an untyped language the ACL2
evaluator can be configured so as to check "types" at runtime.  We
should not say "types" here but "guards."  See Undocumented Topic
for a discussion of guards.

The guard on endp <> requires its argument to be a true list.  Since 7
is not a true list, and since ACL2 is checking guards in this example,
an error is signaled by ACL2.  How do you know ACL2 is checking guards?
Because the prompt tells us (see About the Prompt) with its "!".

How Long Does It Take to Become an Effective User(Q)    How Long Does It Take to Become an Effective User?

The training time depends primarily on the background of the user.

We expect that a user who

       * has a bachelor's degree in computer science or mathematics,

       * has some experience with formal methods,

       * has had some exposure to Lisp programming and is comfortable
         with the Lisp notation,

       * is familiar with and has unlimited access to a Common Lisp
         host processor, operating system, and text editor (we
         use Sun workstations running Unix and GNU Emacs),

       * is willing to read and study the ACL2 documentation, and

       * is given the opportunity to start with "toy" projects before
         being expected to tackle the company's Grand Challenge,

will probably take several months to become an effective ACL2 user.

Flying Tour: Other Requirements

How To Find Out about ACL2 Functions    How To Find Out about ACL2 Functions

Most ACL2 primitives are documented.  Here is the definition of app
again, with the documented topics highlighted.  <> All of the links
below lead into the ACL2 online documentation, 1.5 megabytes of
hyperlinked text.  So follow these links around, but remember to come
back here!

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

By following the link on endp <> we see that it is a Common Lisp
function and is defined to be the same as atom <>, which recognizes
non-conses.  But endp has a guard.  Since we are ignorning guards for
now, we'll ignore the guard issue on endp.

So this definition reads "to app x and y: if x is an atom, return y;
otherwise, app (cdr x) and y and then cons (car x) onto that."

Walking Tour: How To Find Out about ACL2 Functions (cont)

How To Find Out about ACL2 Functions (cont)    How To Find Out about ACL2 Functions (cont)

You can always use the Index <> to find the documentation of functions.
Try it.  Click on the Index icon below.  Then use the Find command of
your browser to find "endp" in that document and follow the link.  But
remember to come back here.

The ACL2 documentation is also available via Emacs' TexInfo, allowing
you to explore the hyperlinked documentation in the comfort of a text
editor that can also interact with ACL2.

In addition, runtime images of ACL2 have the hyperlinked text as a large
ACL2 data structure that can be explored with ACL2's :doc command.  If
you have ACL2 running, try the command :doc endp.

Another way to find out about ACL2 functions, if you have an ACL2 image
available, is to use the command :args <> which prints the formals,
type, and guard of a function symbol.

Of course, the ACL2 documentation can also be printed out as 700 page
book.  See the ACL2 Home Page to download the Postscript.

Now let's continue with app.

Walking Tour: The Admission of App

Modeling in ACL2    Modeling in ACL2

Below we define mc(s,n) to be the function that single-steps n times
from a given starting state, s.  In Common Lisp, "mc(s,n)" is written
(mc s n).

     (defun mc (s n)                     ; To step s n times:
      (if (zp n)                         ; If n is 0
          s                              ;    then return s
          (mc (single-step s) (- n 1)))) ;    else step single-step(s)
                                                           n-1 times.

This is an example of a formal model in ACL2.

Flying Tour: Running Models

Models in Engineering    Models in Engineering

Frequently, engineers use mathematical models.  Use of such models
frequently lead to

better designs,

faster completion of acceptable products, and

reduced overall cost,

because models allow the trained user to study the design before it is
built and analyze its properties.  Usually, testing and analyzing a
model is cheaper and faster than fabricating and refabricating the
product.

See The Falling Body Model to continue.

Models of Computer Hardware and Software    Models of Computer Hardware and Software

Computing machines, whether hardware or software or some combintation,
are frequently modeled as "state machines."

To so model a computing machine we must represent its states as objects
in our mathematical framework.

Transitions are functions or relations on state objects.

In what language shall we define these objects, functions, and
relations?

The mathematical languages we were taught in high school

algebra,

geometry,

trignometry, and

calculus

are inappropriate for modeling digital systems.  They primarily let us
talk about numbers and continuous functions.

To see what kind of expressive power we need, take a closer look at what
a typical state contains.

Flying Tour: A Typical State

Name the Formula Above    Name the Formula Above

When the theorem prover explicitly assigns a name, like *1, to a
formula, it has decided to prove the formula by induction.

Nontautological Subgoals    Prover output omits some details

The theorem prover's proof output is intended to suggest an outline of
the reasoning process employed by its proof engine, which is virtually
always more than is necessary for the ACL2 user.  In particular, the
output often omits subgoals that are sufficiently trivial, including
tautologies.

Numbers in ACL2    Numbers in ACL2

The numbers in ACL2 can be partitioned into the following subtypes:

      Rationals
       Integers
        Positive integers                3
        Zero                             0
        Negative Integers                -3
       Non-Integral Rationals
        Positive Non-Integral Rationals  19/3
        Negative Non-Integral Rationals  -22/7
      Complex Rational Numbers           #c(3 5/2) ; = 3+(5/2)i

 Signed integer constants are usually written (as illustrated above)
 as sequences of decimal digits, possibly preceded by + or -.
 Decimal points are not allowed.  Integers may be written in binary,
 as in #b1011 (= 23) and #b-111 (= -7).  Octal may also be
 used, #o-777 = -511.  Non-integral rationals are written as a
 signed decimal integer and an unsigned decimal integer, separated by
 a slash.  Complex rationals are written as #c(rpart ipart) where
 rpart and ipart are rationals.

 Of course, 4/2 = 2/1 = 2 (i.e., not every rational written with a slash
 is a non-integer).  Similarly, #c(4/2 0) = #c(2 0) = 2.

 The common arithmetic functions and relations are denoted by +,
 -, *, /, =, <, <=, > and >=.  However there
 are many others, e.g., floor, ceiling, and lognot.  We
 suggest you see PROGRAMMING <> where we list all of the primitive
 ACL2 functions.  Alternatively, see any Common Lisp language
 documentation.

 The primitive predicates for recognizing numbers are illustrated
 below.  The following ACL2 function will classify an object, x,
 according to its numeric subtype, or else return 'NaN (not a
 number).  We show it this way just to illustrate programming in
 ACL2.

      (defun classify-number (x)
        (cond ((rationalp x)
               (cond ((integerp x)
                      (cond ((< 0 x) 'positive-integer)
                            ((= 0 x) 'zero)
                            (t 'negative-integer)))
                     ((< 0 x) 'positive-non-integral-rational)
                     (t 'negative-non-integral-rational)))
              ((complex-rationalp x) 'complex-rational)
              (t 'NaN)))

On the Naming of Subgoals    On the Naming of Subgoals

Subgoal *1/2 is the induction step from the scheme, obtained by
instantiating the scheme with our conjecture.

We number the cases "backward", so this is case "2" of the
proof of "*1".  We number them backward so you can look at a subgoal
number and get an estimate for how close you are to the end.

Other Requirements    Other Requirements

ACL2 is distributed on the Web without fee.

There is a License agreement, which is available via the ACL2 Home
Page link below.

ACL2 currently runs on Unix, Linux, Windows, and
Macintosh operating systems.

It can be built in any of the following Common Lisps:

       * Allegro,
       * GCL (Gnu Common Lisp),
       * Lispworks,
       * CLISP,
       * CMU Common Lisp,
       * SBCL,
       * OpenMCL, and
       * MCL (Macintosh Common Lisp).

Flying Tour: The End of the Flying Tour

Overview of the Expansion of ENDP in the Base Case    Overview of the Expansion of ENDP in the Base Case

Subgoal *1/1 is the Base Case of our induction.  It simplifies to
Subgoal *1/1' by expanding the ENDP term in the hypothesis, just as we
saw in the earlier proof of Subgoal *1/2.

Overview of the Expansion of ENDP in the Induction Step    Overview of the Expansion of ENDP in the Induction Step

In this message the system is saying that Subgoal *1/2 has been
rewritten to the Subgoal *1/2', by expanding the definition of endp.
This is an example of simplification, one of the main proof techniques
used by the theorem prover.

See The Expansion of ENDP in the Induction Step (Step 0) if you
would like to step through the simplification of Subgoal *1/2.

Overview of the Final Simplification in the Base Case    Overview of the Final Simplification in the Base Case

The But is our signal that the goal is proved.

See The Final Simplification in the Base Case (Step 0) to step
through the proof.  It is very simple.

Overview of the Proof of a Trivial Consequence    Overview of the Proof of a Trivial Consequence

     ACL2 !>(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))))))

     ACL2 Warning [Subsume] in ( DEFTHM TRIVIAL-CONSEQUENCE ...):  The previously
     added rule ASSOCIATIVITY-OF-APP subsumes the newly proposed :REWRITE
     rule TRIVIAL-CONSEQUENCE, in the sense that the old rule rewrites a
     more general target.  Because the new rule will be tried first, it
     may nonetheless find application.

     By the simple :rewrite rule ASSOCIATIVITY-OF-APP we reduce the conjecture
     to

     Goal'
     (EQUAL (APP X1
                 (APP X2
                      (APP X3 (APP X4 (APP X5 (APP X6 X7))))))
            (APP X1
                 (APP X2
                      (APP X3 (APP X4 (APP X5 (APP X6 X7))))))).

     But we reduce the conjecture to T, by primitive type reasoning.

     Q.E.D.

     Summary
     Form:  ( DEFTHM TRIVIAL-CONSEQUENCE ...)
     Rules: ((:REWRITE ASSOCIATIVITY-OF-APP)
             (:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  Subsume
     Time:  0.20 seconds (prove: 0.02, print: 0.00, other: 0.18)
      TRIVIAL-CONSEQUENCE

You might explore the links before moving on.

Walking Tour: The End of the Walking Tour

Overview of the Simplification of the Base Case to T    Overview of the Simplification of the Base Case to T

     Subgoal *1/1
     (IMPLIES (ENDP A)
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

     By the simple :definition ENDP we reduce the conjecture to

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP A))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

     But simplification reduces this to T, using the :definition APP and
     primitive type reasoning.

Walking Tour: The End of the Proof of the Associativity of App

Overview of the Simplification of the Induction Conclusion    Overview of the Simplification of the Induction Conclusion

In this message the system is saying that Subgoal *1/2' has been
rewritten T using the rules noted.  The word "But" at the beginning of
the sentence is a signal that the goal has been proved.

See The Simplification of the Induction Conclusion (Step 0) to
step through the proof of Subgoal *1/2'.

Overview of the Simplification of the Induction Step to T    Overview of the Simplification of the Induction Step to T

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

     By the simple :definition ENDP we reduce the conjecture to

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

     But simplification reduces this to T, using the :definition APP, the
     :rewrite rules CDR-CONS and CAR-CONS and primitive type reasoning.

Walking Tour: Overview of the Simplification of the Base Case to T

Perhaps    Perhaps

The theorem prover's proof is printed in real time.  At the time it
prints "Perhaps" it does not know the proof will succeed.

Popping out of an Inductive Proof    Popping out of an Inductive Proof

Recall that our induction scheme (see The Proof of the Associativity of App
to revisit it) had two cases, the induction step
(Subgoal *1/2) and the base case (Subgoal *1/1).  Both have been proved!

Proving Theorems about Models    Proving Theorems about Models

But ACL2 is a logic.  We can prove theorems about the model.

     Theorem.  MC 'mult is a multiplier
     (implies (and (natp x)
                   (natp y))
              (equal (lookup 'z (mc (s 'mult x y) (mclk x)))
                     (* x y))).

This theorem says that a certain program running on the mc machine will
correctly multiply any two natural numbers.

It is a statement about an infinite number of test cases!

We know it is true about the model because we proved it.

Flying Tour: What is Required of the User(Q)

Revisiting the Admission of App    Revisiting the Admission of App

Here is the definition of app again with certain parts highlighted.  If
you are taking the Walking Tour, please read the text carefully and
click on each of the links below, except those marked <>.  Then come
back here.

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

     The admission of APP is trivial, using the
     relation O< <> (which is known to be well-founded on
     the domain recognized by O-P <>) and the measure
     (ACL2-COUNT <> X).  We observe that the
     type of APP is described by the theorem (OR
     (CONSP (APP X Y)) (EQUAL (APP X Y) Y)).  We used primitive type
     reasoning.

     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

Walking Tour: Evaluating App on Sample Input

Rewrite Rules are Generated from DEFTHM Events    Rewrite Rules are Generated from DEFTHM Events

By reading the documentation of defthm <> (and especially of its
:rule-classes <> argument) you would learn that when we submitted the
command

     (defthm associativity-of-app
       (equal (app (app a b) c)
              (app a (app b c))))

we not only command the system to prove that app is an associative
function but

       * we commanded it to use that fact as a rewrite rule.

That means that every time the system encounters a term of the form

     (app (app x y) z)

it will replace it with

     (app x (app y z))!

Walking Tour: You Must Think about the Use of a Formula as a Rule

Running Models    Running Models

Suppose the machine being modeled is some kind of arithmetic unit.
Suppose the model can be initialized so as to multiply x times y and
leave the answer in z.  Then if we initialize s to multiply with x=5 and
y=7 and run the machine long enough, we can read the answer 35 in the
final state.

Because ACL2 is a programming language, our model can be run or
executed.

If you defined the model in ACL2 and then typed

     > (lookup 'z (mc (s 'mult 5 7) 29))

then ACL2 would compute 35.  You can emulate or test the model of your
machine.

This is obvious because ACL2 is Common Lisp; and Common Lisp is a
programming language.

Flying Tour: Symbolic Execution of Models

Subsumption of Induction Candidates in App Example    Subsumption of Induction Candidates in App Example

After collecting induction suggestions from these three terms

     (app a b)

     (app b c)

     (app a (app b c))

the system notices that the first and last suggest the same
decomposition of a.  So we are left with two ideas about how to induct:

Decompose a as we would to unwind (app a b).

Decompose b as we would to unwind (app b c).

Suggested Inductions in the Associativity of App Example    Suggested Inductions in the Associativity of App Example

To find a plausible induction argument, the system studies the
recursions exhibited by the terms in the conjecture.

Roughly speaking, a call of a recursive function "suggests" an induction
if the argument position decomposed in recursion is occupied by a
variable.

In this conjecture, three terms suggest inductions:

     (app a b)

     (app b c)

     (app a (app b c))

The variable recursively decomposed is indicated in bold.

Symbolic Execution of Models    Symbolic Execution of Models

But ACL2 is more than a programming language.

Initialize x to 5 and let y be any legal value.

Because ACL2 is a mathematical language, we can simplify the expression

     (lookup 'z (mc (s 'mult 5 y) 29))

and get (+ y y y y y).  This is symbolic execution because not all of
the parameters are known.

Flying Tour: Proving Theorems about Models

The Admission of App    The Admission of App

Here is what it looks like to submit the definition of app to ACL2:

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

     The admission of APP is trivial, using the relation O< (which
     is known to be well-founded on the domain recognized by O-P)
     and the measure (ACL2-COUNT X).  We observe that the type of APP is
     described by the theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)).
     We used primitive type reasoning.

     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 text between the lines above is one interaction with the ACL2
command loop.

Above you see the user's input and how the system responds.  This little
example shows you what the syntax looks like and is a very typical
successful interaction with the definitional principle.

Let's look at it a little more closely.

Walking Tour: Revisiting the Admission of App

The Associativity of App    The Associativity of App

     ACL2!>(let ((a '(1 2))
                 (b '(3 4))
                 (c '(5 6)))
             (equal (app (app a b) c)
                    (app a (app b c))))
     T

Observe that, for the particular a, b, and c above, (app (app a b) c)
returns the same thing as (app a (app b c)).  Perhaps app is
associative.  Of course, to be associative means that the above property
must hold for all values of a, b, and c, not just the ones tested above.

Wouldn't it be cool if you could type

     ACL2!>(equal (app (app a b) c)
                  (app a (app b c))))

and have ACL2 compute the value T?  Well, you can't!  If you try it,
you'll get an error message!  The message says we can't evaluate that
form because it contains free variables, i.e., variables not given
values.  See Free Variables in Top-Level Input to see the
message.

We cannot evaluate a form on an infinite number of cases.  But we can
prove that a form is a theorem and hence know that it will always
evaluate to true.

Walking Tour: The Theorem that App is Associative

The Base Case in the App Example    The Base Case in the App Example

This formula is the Base Case.  It consists of two parts, a test
identifying the non-inductive case and the conjecture to prove.

     (IMPLIES (ENDP A)                 ; Test
              (:P A B C))              ; Conjecture

When we prove this we can assume

       * A is empty

and we have to prove the conjecture for A.

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: A Walking Tour of ACL2

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: Guiding the ACL2 Theorem Prover

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

The Event Summary    The Event Summary

At the conclusion of most events (see About the Prompt for a
brief discussion of events or see 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 RUNE) <>)
which are list-structured 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
LD-POST-EVAL-PRINT<> for some details.  If you really want to follow
that link, however, you might see LD <> first.

You should now return to the Walking Tour.

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.

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

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 Overview of the Simplification of the Induction Step to T
to return to the main proof.

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 Corroborating Models to continue

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.

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.

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

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 Overview of the Simplification of the Base Case to T
to return to the main proof.

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

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.

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.