doc-src/IsarRef/intro.tex
author wenzelm
Mon Apr 10 23:36:19 2000 +0200 (2000-04-10)
changeset 8684 dfe444b748aa
parent 8547 93b8685d004b
child 8843 5370a030dd47
permissions -rw-r--r--
improved document preparation;
wenzelm@7046
     1
wenzelm@7046
     2
\chapter{Introduction}
wenzelm@7046
     3
wenzelm@7167
     4
\section{Quick start}
wenzelm@7167
     5
wenzelm@8508
     6
\subsection{Terminal sessions}
wenzelm@8508
     7
wenzelm@7175
     8
Isar is already part of Isabelle (as of version Isabelle99, or later).  The
wenzelm@7175
     9
\texttt{isabelle} binary provides option \texttt{-I} to run the Isar
wenzelm@7175
    10
interaction loop at startup, rather than the plain ML top-level.  Thus the
wenzelm@8547
    11
quickest way to do \emph{anything} with Isabelle/Isar is as follows:
wenzelm@7175
    12
\begin{ttbox}
wenzelm@7175
    13
isabelle -I HOL\medskip
wenzelm@7175
    14
\out{> Welcome to Isabelle/HOL (Isabelle99)}\medskip
wenzelm@7175
    15
theory Foo = Main:
wenzelm@7297
    16
constdefs foo :: nat  "foo == 1";
wenzelm@7297
    17
lemma "0 < foo" by (simp add: foo_def);
wenzelm@7175
    18
end
wenzelm@7175
    19
\end{ttbox}
wenzelm@8547
    20
Note that any Isabelle/Isar command may be retracted by \texttt{undo}.  The
wenzelm@7981
    21
\texttt{help} command prints a list of available language elements.
wenzelm@7175
    22
wenzelm@8508
    23
wenzelm@8508
    24
\subsection{The Proof~General interface}
wenzelm@8508
    25
wenzelm@8508
    26
Plain TTY-based interaction as above used to be quite feasible with
wenzelm@8547
    27
traditional tactic based theorem proving, but developing Isar documents really
wenzelm@8508
    28
demands some better user-interface support.  David Aspinall's
wenzelm@8508
    29
\emph{Proof~General}\index{Proof General} environment
wenzelm@8547
    30
\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs interface for
wenzelm@8547
    31
interactive theorem provers that does all the cut-and-paste and
wenzelm@8508
    32
forward-backward walk through the text in a very neat way.  In Isabelle/Isar,
wenzelm@8508
    33
the current position within a partial proof document is equally important than
wenzelm@8508
    34
the actual proof state.  Thus Proof~General provides the canonical working
wenzelm@8508
    35
environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
wenzelm@8547
    36
existing Isar documents) and for production work.
wenzelm@7175
    37
wenzelm@7175
    38
\medskip
wenzelm@7167
    39
wenzelm@7315
    40
The easiest way to use Proof~General is to make it the default Isabelle user
wenzelm@8508
    41
interface (see also \cite{isabelle-sys}).  Just put something like this into
wenzelm@8508
    42
your Isabelle settings file:
wenzelm@7175
    43
\begin{ttbox}
wenzelm@7175
    44
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
wenzelm@8508
    45
PROOFGENERAL_OPTIONS=""
wenzelm@7175
    46
\end{ttbox}
wenzelm@7175
    47
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
wenzelm@7335
    48
actual installation directory of Proof~General.  From now on, the capital
wenzelm@7315
    49
\texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
wenzelm@7981
    50
interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for
wenzelm@8508
    51
  classic Isabelle tactic scripts.}
wenzelm@7175
    52
wenzelm@8547
    53
The interface script provides several options, just pass \verb,-?, to see its
wenzelm@8547
    54
usage.  Apart from the command line, the defaults for these options may be
wenzelm@8547
    55
overridden via the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For
wenzelm@8516
    56
example, plain FSF Emacs (instead of the default XEmacs) may be configured in
wenzelm@8516
    57
Isabelle's settings via \texttt{PROOFGENERAL_OPTIONS="-p emacs"}.
wenzelm@7460
    58
wenzelm@8516
    59
Occasionally, the user's \verb,~/.emacs, file contains material that is
wenzelm@8516
    60
incompatible with the version of Emacs that Proof~General prefers.  Then
wenzelm@8508
    61
proper startup may be still achieved by using the \texttt{-u false} option.
wenzelm@8547
    62
Also note that any Emacs lisp file called \texttt{proofgeneral-settings.el}
wenzelm@8547
    63
occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}
wenzelm@8547
    64
is automatically loaded by the Proof~General interface script as well.
wenzelm@7981
    65
wenzelm@7981
    66
\medskip
wenzelm@7981
    67
wenzelm@7175
    68
With the proper Isabelle interface setup, Isar documents may now be edited by
wenzelm@7175
    69
visiting appropriate theory files, e.g.\ 
wenzelm@7175
    70
\begin{ttbox}
wenzelm@7175
    71
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
wenzelm@7175
    72
\end{ttbox}
wenzelm@7315
    73
Users of XEmacs may note the tool bar for navigating forward and backward
wenzelm@8516
    74
through the text.  Consult the Proof~General documentation \cite{proofgeneral}
wenzelm@8547
    75
for further basic command sequences, such as ``\texttt{C-c C-return}'' or
wenzelm@8547
    76
``\texttt{C-c u}''.
wenzelm@8508
    77
wenzelm@8508
    78
\medskip
wenzelm@8508
    79
wenzelm@8508
    80
Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which
wenzelm@8508
    81
provides a nice way to get proper mathematical symbols displayed on screen.
wenzelm@8508
    82
Just pass option \texttt{-x true} to the Isabelle interface script, or check
wenzelm@8516
    83
the appropriate menu setting by hand.  In any case, the X-Symbol package must
wenzelm@8516
    84
have been properly installed already.
wenzelm@8516
    85
wenzelm@8516
    86
Note that using actual mathematical symbols in the text easily makes the ASCII
wenzelm@8516
    87
sources hard to read.  For example, $\forall$ will appear as \verb,\\<forall>,
wenzelm@8516
    88
according the default set of Isabelle symbols.  On the other hand, the
wenzelm@8516
    89
Isabelle document preparation system \cite{isabelle-sys} will be happy to
wenzelm@8516
    90
print non-ASCII symbols properly.  It is even possible to invent additional
wenzelm@8547
    91
notation beyond the display capabilities of XEmacs and X-Symbol.
wenzelm@7175
    92
wenzelm@7981
    93
wenzelm@7981
    94
\section{Isabelle/Isar theories}
wenzelm@7981
    95
wenzelm@8547
    96
Isabelle/Isar offers the following main improvements over classic Isabelle.
wenzelm@7981
    97
\begin{enumerate}
wenzelm@7981
    98
\item A new \emph{theory format}, occasionally referred to as ``new-style
wenzelm@7981
    99
  theories'', supporting interactive development and unlimited undo operation.
wenzelm@7981
   100
\item A \emph{formal proof document language} designed to support intelligible
wenzelm@7981
   101
  semi-automated reasoning.  Instead of putting together unreadable tactic
wenzelm@7981
   102
  scripts, the author is enabled to express the reasoning in way that is close
wenzelm@8508
   103
  to usual mathematical practice.
wenzelm@8547
   104
\item A simple document preparation system, for typesetting formal
wenzelm@8547
   105
  developments together with informal text.  The resulting hyper-linked PDF
wenzelm@8547
   106
  documents are equally well suited for WWW presentation and as printed
wenzelm@8547
   107
  copies.
wenzelm@7981
   108
\end{enumerate}
wenzelm@7981
   109
wenzelm@7981
   110
The Isar proof language is embedded into the new theory format as a proper
wenzelm@7981
   111
sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
wenzelm@7981
   112
$\LEMMANAME$ at the theory level, and left again with the final conclusion
wenzelm@7981
   113
(e.g.\ via $\QEDNAME$).  A few theory extension mechanisms require proof as
wenzelm@8547
   114
well, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness of the
wenzelm@8547
   115
representing sets.
wenzelm@7460
   116
wenzelm@7981
   117
New-style theory files may still be associated with separate ML files
wenzelm@7981
   118
consisting of plain old tactic scripts.  There is no longer any ML binding
wenzelm@7981
   119
generated for the theory and theorems, though.  ML functions \texttt{theory},
wenzelm@7981
   120
\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
wenzelm@7981
   121
Nevertheless, migration between classic Isabelle and Isabelle/Isar is
wenzelm@7981
   122
relatively easy.  Thus users may start to benefit from interactive theory
wenzelm@8547
   123
development and document preparation, even before they have any idea of the
wenzelm@8547
   124
Isar proof language at all.
wenzelm@7981
   125
wenzelm@7981
   126
\begin{warn}
wenzelm@8547
   127
  Currently, Proof~General does \emph{not} support mixed interactive
wenzelm@7981
   128
  development of classic Isabelle theory files or tactic scripts, together
wenzelm@7981
   129
  with Isar documents.  The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
wenzelm@7981
   130
  Proof~General are handled as two different theorem proving systems, only one
wenzelm@7981
   131
  of these may be active at the same time.
wenzelm@7981
   132
\end{warn}
wenzelm@7981
   133
wenzelm@7981
   134
Porting of existing tactic scripts is best done by running two separate
wenzelm@7981
   135
Proof~General sessions, one for replaying the old script and the other for the
wenzelm@7981
   136
emerging Isabelle/Isar document.
wenzelm@7981
   137
wenzelm@7167
   138
wenzelm@8684
   139
\subsection{Document preparation}
wenzelm@8684
   140
wenzelm@8684
   141
Isabelle/Isar provides a simple document preparation system based on current
wenzelm@8684
   142
(PDF) {\LaTeX} technology, with full support of hyper-links (both local
wenzelm@8684
   143
references and URLs), bookmarks, thumbnails etc.  Thus the results are equally
wenzelm@8684
   144
well suited for WWW browsing and as printed copies.
wenzelm@8684
   145
wenzelm@8684
   146
\medskip
wenzelm@8684
   147
wenzelm@8684
   148
Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
wenzelm@8684
   149
  session} (see also \cite{isabelle-sys}).  Getting started with a working
wenzelm@8684
   150
configuration for common situations is quite easy by using the Isabelle
wenzelm@8684
   151
\texttt{mkdir} and \texttt{make} tools.  Just invoke
wenzelm@8684
   152
\begin{ttbox}
wenzelm@8684
   153
  isatool mkdir -d Foo
wenzelm@8684
   154
\end{ttbox}
wenzelm@8684
   155
to setup a separate directory for session \texttt{Foo}.\footnote{It is safe to
wenzelm@8684
   156
  experiment, since \texttt{isatool mkdir} never overwrites existing files.}
wenzelm@8684
   157
Ensure that \texttt{Foo/ROOT.ML} loads all theories required for this session.
wenzelm@8684
   158
Furthermore \texttt{Foo/document/root.tex} should include any special {\LaTeX}
wenzelm@8684
   159
macro packages required for your document (the default is usually sufficient
wenzelm@8684
   160
as a start).
wenzelm@8684
   161
wenzelm@8684
   162
The session is controlled by a separate \texttt{IsaMakefile} (with very crude
wenzelm@8684
   163
source dependencies only by default).  This file is located one level up from
wenzelm@8684
   164
the \texttt{Foo} directory location.  At that point just invoke
wenzelm@8684
   165
\begin{ttbox}
wenzelm@8684
   166
  isatool make Foo
wenzelm@8684
   167
\end{ttbox}
wenzelm@8684
   168
to run the \texttt{Foo} session, with browser information and document
wenzelm@8684
   169
preparation enabled.  Unless any errors are reported by Isabelle or {\LaTeX},
wenzelm@8684
   170
the output will appear inside the directory indicated by \texttt{isatool
wenzelm@8684
   171
  getenv ISABELLE_BROWSER_INFO}, with the logical session prefix added (e.g.\ 
wenzelm@8684
   172
\texttt{HOL/Foo}).  Note that the \texttt{index.html} located there provides a
wenzelm@8684
   173
link to the finished {\LaTeX} document, too.
wenzelm@8684
   174
wenzelm@8684
   175
Note that this really is batch processing --- better let Isabelle check your
wenzelm@8684
   176
theory and proof developments beforehand in interactive mode.
wenzelm@8684
   177
wenzelm@8684
   178
\medskip
wenzelm@8684
   179
wenzelm@8684
   180
You may also consider to tune the \texttt{usedir} options in
wenzelm@8684
   181
\texttt{IsaMakefile}, for example to change the output format from
wenzelm@8684
   182
\texttt{dvi} to \texttt{pdf}, or activate the \texttt{-D document} option in
wenzelm@8684
   183
order to preserve a copy of the generated {\LaTeX} sources.  The latter
wenzelm@8684
   184
feature is very useful for debugging {\LaTeX} errors, while avoiding repeated
wenzelm@8684
   185
runs of Isabelle.
wenzelm@8684
   186
wenzelm@8684
   187
\medskip
wenzelm@8684
   188
wenzelm@8684
   189
See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
wenzelm@8684
   190
on Isabelle logic sessions and theory presentation.
wenzelm@8684
   191
wenzelm@8684
   192
wenzelm@8684
   193
\subsection{How to write Isar proofs anyway?}
wenzelm@7167
   194
wenzelm@7297
   195
This is one of the key questions, of course.  Isar offers a rather different
wenzelm@7297
   196
approach to formal proof documents than plain old tactic scripts.  Experienced
wenzelm@7297
   197
users of existing interactive theorem proving systems may have to learn
wenzelm@7895
   198
thinking differently in order to make effective use of Isabelle/Isar.  On the
wenzelm@7297
   199
other hand, Isabelle/Isar comes much closer to existing mathematical practice
wenzelm@7297
   200
of formal proof, so users with less experience in old-style tactical proving,
wenzelm@7895
   201
but a good understanding of mathematical proof, might cope with Isar even
wenzelm@7981
   202
better.  See also \cite{Wenzel:1999:TPHOL} for further background information
wenzelm@7981
   203
on Isar.
wenzelm@8547
   204
%FIXME cite [HahnBanach-in-Isar]
wenzelm@7297
   205
wenzelm@7981
   206
\medskip This really is a \emph{reference manual}.  Nevertheless, we will also
wenzelm@7981
   207
give some clues of how the concepts introduced here may be put into practice.
wenzelm@7981
   208
Appendix~\ref{ap:refcard} provides a quick reference card of the most common
wenzelm@7981
   209
Isabelle/Isar language elements.  There are several examples distributed with
wenzelm@8516
   210
Isabelle, and available via the Isabelle WWW library as well as the
wenzelm@8516
   211
Isabelle/Isar page:
wenzelm@7836
   212
\begin{center}\small
wenzelm@7836
   213
  \begin{tabular}{l}
wenzelm@7836
   214
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
wenzelm@8516
   215
    \url{http://isabelle.in.tum.de/library/} \\[1ex]
wenzelm@8508
   216
    \url{http://isabelle.in.tum.de/Isar/} \\
wenzelm@7836
   217
  \end{tabular}
wenzelm@7836
   218
\end{center}
wenzelm@7836
   219
wenzelm@7987
   220
See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
wenzelm@8547
   221
\texttt{HOL/HOL-Real/HahnBanach} for a big mathematics application.  Apart
wenzelm@8547
   222
from plain HTML sources, these sessions also provide actual documents (in
wenzelm@8547
   223
PDF).
wenzelm@8547
   224
wenzelm@7167
   225
wenzelm@7046
   226
%%% Local Variables: 
wenzelm@7046
   227
%%% mode: latex
wenzelm@7046
   228
%%% TeX-master: "isar-ref"
wenzelm@7046
   229
%%% End: