theory intro
imports CPure
begin
chapter {* Introduction *}
section {* Overview *}
text {*
The \emph{Isabelle} system essentially provides a generic
infrastructure for building deductive systems (programmed in
Standard ML), with a special focus on interactive theorem proving in
higher-order logics. In the olden days even end-users would refer
to certain ML functions (goal commands, tactics, tacticals etc.) to
pursue their everyday theorem proving tasks
\cite{isabelle-intro,isabelle-ref}.
In contrast \emph{Isar} provides an interpreted language environment
of its own, which has been specifically tailored for the needs of
theory and proof development. Compared to raw ML, the Isabelle/Isar
top-level provides a more robust and comfortable development
platform, with proper support for theory development graphs,
single-step transactions with unlimited undo, etc. The
Isabelle/Isar version of the \emph{Proof~General} user interface
\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
front-end for interactive theory and proof development in this
advanced theorem proving environment.
\medskip Apart from the technical advances over bare-bones ML
programming, the main purpose of the Isar language is to provide a
conceptually different view on machine-checked proofs
\cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
``Intelligible semi-automated reasoning''. Drawing from both the
traditions of informal mathematical proof texts and high-level
programming languages, Isar offers a versatile environment for
structured formal proof documents. Thus properly written Isar
proofs become accessible to a broader audience than unstructured
tactic scripts (which typically only provide operational information
for the machine). Writing human-readable proof texts certainly
requires some additional efforts by the writer to achieve a good
presentation, both of formal and informal parts of the text. On the
other hand, human-readable formal texts gain some value in their own
right, independently of the mechanic proof-checking process.
Despite its grand design of structured proof texts, Isar is able to
assimilate the old tactical style as an ``improper'' sub-language.
This provides an easy upgrade path for existing tactic scripts, as
well as additional means for interactive experimentation and
debugging of structured proofs. Isabelle/Isar supports a broad
range of proof styles, both readable and unreadable ones.
\medskip The Isabelle/Isar framework is generic and should work
reasonably well for any Isabelle object-logic that conforms to the
natural deduction view of the Isabelle/Pure framework. Major
Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF
\cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF
\cite{isabelle-ZF} have already been set up for end-users.
*}
section {* Quick start *}
subsection {* Terminal sessions *}
text {*
Isar is already part of Isabelle. The low-level \texttt{isabelle} binary
provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
startup, rather than the raw ML top-level. So the most basic way to do
anything with Isabelle/Isar is as follows:
\begin{ttbox}
isabelle -I HOL\medskip
\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
theory Foo imports Main begin;
definition foo :: nat where "foo == 1";
lemma "0 < foo" by (simp add: foo_def);
end;
\end{ttbox}
Note that any Isabelle/Isar command may be retracted by
\texttt{undo}. See the Isabelle/Isar Quick Reference
(appendix~\ref{ap:refcard}) for a comprehensive overview of
available commands and other language elements.
*}
subsection {* Proof General *}
text {*
Plain TTY-based interaction as above used to be quite feasible with
traditional tactic based theorem proving, but developing Isar
documents really demands some better user-interface support. The
Proof~General environment by David Aspinall
\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
interface for interactive theorem provers that organizes all the
cut-and-paste and forward-backward walk through the text in a very
neat way. In Isabelle/Isar, the current position within a partial
proof document is equally important than the actual proof state.
Thus Proof~General provides the canonical working environment for
Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
existing Isar documents) and for production work.
*}
subsubsection{* Proof~General as default Isabelle interface *}
text {*
The Isabelle interface wrapper script provides an easy way to invoke
Proof~General (including XEmacs or GNU Emacs). The default
configuration of Isabelle is smart enough to detect the
Proof~General distribution in several canonical places (e.g.\
\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
\texttt{Isabelle} executable would already refer to the
\texttt{ProofGeneral/isar} interface without further ado. The
Isabelle interface script provides several options; pass \verb,-?,
to see its usage.
With the proper Isabelle interface setup, Isar documents may now be edited by
visiting appropriate theory files, e.g.\
\begin{ttbox}
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
\end{ttbox}
Beginners may note the tool bar for navigating forward and backward
through the text (this depends on the local Emacs installation).
Consult the Proof~General documentation \cite{proofgeneral} for
further basic command sequences, in particular ``\texttt{C-c
C-return}'' and ``\texttt{C-c u}''.
\medskip Proof~General may be also configured manually by giving
Isabelle settings like this (see also \cite{isabelle-sys}):
\begin{ttbox}
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
PROOFGENERAL_OPTIONS=""
\end{ttbox}
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}
to the actual installation directory of Proof~General.
\medskip Apart from the Isabelle command line, defaults for
interface options may be given by the \texttt{PROOFGENERAL_OPTIONS}
setting. For example, the Emacs executable to be used may be
configured in Isabelle's settings like this:
\begin{ttbox}
PROOFGENERAL_OPTIONS="-p xemacs-mule"
\end{ttbox}
Occasionally, a user's \verb,~/.emacs, file contains code that is
incompatible with the (X)Emacs version used by Proof~General,
causing the interface startup to fail prematurely. Here the
\texttt{-u false} option helps to get the interface process up and
running. Note that additional Lisp customization code may reside in
\texttt{proofgeneral-settings.el} of \texttt{\$ISABELLE_HOME/etc} or
\texttt{\$ISABELLE_HOME_USER/etc}.
*}
subsubsection {* The X-Symbol package *}
text {*
Proof~General incorporates a version of the Emacs X-Symbol package
\cite{x-symbol}, which handles proper mathematical symbols displayed
on screen. Pass option \texttt{-x true} to the Isabelle interface
script, or check the appropriate Proof~General menu setting by hand.
The main challenge of getting X-Symbol to work properly is the
underlying (semi-automated) X11 font setup.
\medskip Using proper mathematical symbols in Isabelle theories can
be very convenient for readability of large formulas. On the other
hand, the plain ASCII sources easily become somewhat unintelligible.
For example, $\Longrightarrow$ would appear as \verb,\<Longrightarrow>, according
the default set of Isabelle symbols. Nevertheless, the Isabelle
document preparation system (see \S\ref{sec:document-prep}) will be
happy to print non-ASCII symbols properly. It is even possible to
invent additional notation beyond the display capabilities of Emacs
and X-Symbol.
*}
section {* Isabelle/Isar theories *}
text {*
Isabelle/Isar offers the following main improvements over classic
Isabelle.
\begin{enumerate}
\item A \emph{theory format} that integrates specifications and
proofs, supporting interactive development and unlimited undo
operation.
\item A \emph{formal proof document language} designed to support
intelligible semi-automated reasoning. Instead of putting together
unreadable tactic scripts, the author is enabled to express the
reasoning in way that is close to usual mathematical practice. The
old tactical style has been assimilated as ``improper'' language
elements.
\item A simple document preparation system, for typesetting formal
developments together with informal text. The resulting
hyper-linked PDF documents are equally well suited for WWW
presentation and as printed copies.
\end{enumerate}
The Isar proof language is embedded into the new theory format as a
proper sub-language. Proof mode is entered by stating some
$\THEOREMNAME$ or $\LEMMANAME$ at the theory level, and left again
with the final conclusion (e.g.\ via $\QEDNAME$). A few theory
specification mechanisms also require some proof, such as HOL's
$\isarkeyword{typedef}$ which demands non-emptiness of the
representing sets.
New-style theory files may still be associated with separate ML
files consisting of plain old tactic scripts. There is no longer
any ML binding generated for the theory and theorems, though. ML
functions \texttt{theory}, \texttt{thm}, and \texttt{thms} retrieve
this information from the context \cite{isabelle-ref}.
Nevertheless, migration between classic Isabelle and Isabelle/Isar
is relatively easy. Thus users may start to benefit from
interactive theory development and document preparation, even before
they have any idea of the Isar proof language at all.
Manual conversion of existing tactic scripts may be done by running
two separate Proof~General sessions, one for replaying the old
script and the other for the emerging Isabelle/Isar document. Also
note that Isar supports emulation commands and methods that support
traditional tactic scripts within new-style theories, see
appendix~\ref{ap:conv} for more information.
*}
subsection {* Document preparation \label{sec:document-prep} *}
text {*
Isabelle/Isar provides a simple document preparation system based on
existing {PDF-\LaTeX} technology, with full support of hyper-links
(both local references and URLs), bookmarks, and thumbnails. Thus
the results are equally well suited for WWW browsing and as printed
copies.
\medskip
Isabelle generates {\LaTeX} output as part of the run of a
\emph{logic session} (see also \cite{isabelle-sys}). Getting
started with a working configuration for common situations is quite
easy by using the Isabelle \texttt{mkdir} and \texttt{make} tools.
First invoke
\begin{ttbox}
isatool mkdir Foo
\end{ttbox}
to initialize a separate directory for session \texttt{Foo} --- it
is safe to experiment, since \texttt{isatool mkdir} never overwrites
existing files. Ensure that \texttt{Foo/ROOT.ML} holds ML commands
to load all theories required for this session; furthermore
\texttt{Foo/document/root.tex} should include any special {\LaTeX}
macro packages required for your document (the default is usually
sufficient as a start).
The session is controlled by a separate \texttt{IsaMakefile} (with
crude source dependencies by default). This file is located one
level up from the \texttt{Foo} directory location. Now invoke
\begin{ttbox}
isatool make Foo
\end{ttbox}
to run the \texttt{Foo} session, with browser information and
document preparation enabled. Unless any errors are reported by
Isabelle or {\LaTeX}, the output will appear inside the directory
\texttt{ISABELLE_BROWSER_INFO}, as reported by the batch job in
verbose mode.
\medskip You may also consider to tune the \texttt{usedir} options
in \texttt{IsaMakefile}, for example to change the output format
from \texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D}
option to retain a second copy of the generated {\LaTeX} sources.
\medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
for further details on Isabelle logic sessions and theory
presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
also covers theory presentation issues.
*}
subsection {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
text {*
This is one of the key questions, of course. First of all, the
tactic script emulation of Isabelle/Isar essentially provides a
clarified version of the very same unstructured proof style of
classic Isabelle. Old-time users should quickly become acquainted
with that (slightly degenerative) view of Isar.
Writing \emph{proper} Isar proof texts targeted at human readers is
quite different, though. Experienced users of the unstructured
style may even have to unlearn some of their habits to master proof
composition in Isar. In contrast, new users with less experience in
old-style tactical proving, but a good understanding of mathematical
proof in general, often get started easier.
\medskip The present text really is only a reference manual on
Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
give some clues of how the concepts introduced here may be put into
practice. Appendix~\ref{ap:refcard} provides a quick reference card
of the most common Isabelle/Isar language elements.
Appendix~\ref{ap:conv} offers some practical hints on converting
existing Isabelle theories and proof scripts to the new format
(without restructuring proofs).
Further issues concerning the Isar concepts are covered in the
literature
\cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
The author's PhD thesis \cite{Wenzel-PhD} presently provides the
most complete exposition of Isar foundations, techniques, and
applications. A number of example applications are distributed with
Isabelle, and available via the Isabelle WWW library (e.g.\
\url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
examples, both in proper Isar proof style and unstructured tactic
scripts.
*}
end