The Fundamental Theorem of Calculus
Matt Kaufmann
matt.kaufmann@amd.com

SUMMARY

These books can be certified using Ruben Gamboa's modification ACL2(r) of ACL2,
which supports non-standard analysis.  This directory should be placed
immediately underneath directory books/case-studies/ of the ACL2(r)
installation.

The top-level theorem in these books is the final event in file
fundamental-theorem-of-calculus.lisp, which is a formalization of the
Fundamental Theorem of Calculus.  The easiest way to certify all these
books in a Unix environment is to stand in this directory and execute
"make".

THE METHODOLOGY

These books were developed with a particular top-down methodology.
Conceptually, there are two types of books.  So-called "lemma books"
are those whose name is the same as the name of the last theorem in
the file.  Other books are called "library books".  Some details
follow.

As a book was developed, certain main lemmas were typically "stubbed
out" as defaxioms in order to make the book certifiable.  These
stubbed-out axioms were then replaced by encapsulated defthms using
the following keyboard macro in emacs (where the cursor is within the
defaxiom event):

(fset 'localize
   "\C-e\C-[\C-a\C-e\C-[\C-b\C-@\C-[\C-f\C-[w\C-a\C-o\C-o(encapsulate\C-j()\C-j(local (include-book \"\C-y\"))\C-[f\C-[\C-?defthm\C-a\C-[\C-f)\C-[\C-b\C-[\C-q")

For example,

(defaxiom foo
  (equal (fn1 x) (fn2 x)))

is transformed into the following event.

(encapsulate
 ()
 (local (include-book "foo"))

 (defthm foo
   (equal (fn1 x) (fn2 x))))

It then becomes necessary to create a book with the same book name as
the lemma name.  In this case, the book named "foo" (in file foo.lisp)
is what we call a "lemma book": it is a book that is primarily
intended to be included locally for the purpose of obtaining the
theorem that is the last event in the book.  (Technically, the last
event may be an encapsulate event, in which case we take the last
event of the encapsulate, and so on.)  Formally, a lemma book is one
whose book name is the same as the lemma name of the event that is
last (in the above sense) in the book, which should be a defthm or
defthm-std event.

From time to time during a proof effort, one may collect
general-purpose lemmas into so-called "library books," which are books
that are not lemma books.

Typing "make proof-outline" will create a proof outline, displayed to
various depths in files outline.*, based on this methodology.  See
file outline/outline.12 for the full outline or, at the other extreme,
files outline.1, outline.2, or outline.3 for an abbreviated outline.

USING THE PROOF OUTLINE TOOL

To use the proof outline tool on your own project, copy
Makefile-essence from this directory to your own directory, together
with file proof-outline.lisp.  Include Makefile-essence in a Makefile
in your own directory (or, let Makefile-essence be your Makefile).
Edit your copy of Makefile-essence by deleting everything under the
following line.

# Dependencies:

Or, replace these with your own dependencies, though this is not
necessary for the outline tool.  Then, replace
fundamental-theorem-of-calculus with your top-level lemma book name.
Finally, create an outline/ subdirectory and execute:

make proof-outline

Please feel free to send email to matt.kaufmann@amd.com if you have
any questions (for example, if you want ideas for using the outline
tool on non-Unix platforms).