doc-src/IsarRef/intro.tex
author wenzelm
Sat Feb 03 00:11:07 2001 +0100 (2001-02-03)
changeset 11041 e07b601e2b5a
parent 10993 883248dcf3f8
child 12618 43a97a2155d0
permissions -rw-r--r--
updated;
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@9604
     9
\texttt{isabelle} binary provides option \texttt{-I} to run the Isabelle/Isar
wenzelm@9604
    10
interaction loop at startup, rather than the raw ML top-level.  So the
wenzelm@9604
    11
quickest way to do anything with Isabelle/Isar is as follows:
wenzelm@7175
    12
\begin{ttbox}
wenzelm@7175
    13
isabelle -I HOL\medskip
wenzelm@9272
    14
\out{> Welcome to Isabelle/HOL (Isabelle99-1)}\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@9233
    20
Note that any Isabelle/Isar command may be retracted by \texttt{undo}.  See
wenzelm@10160
    21
the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
wenzelm@10110
    22
comprehensive overview of available commands and other language elements.
wenzelm@7175
    23
wenzelm@8508
    24
wenzelm@8843
    25
\subsection{Proof~General}
wenzelm@8508
    26
wenzelm@8508
    27
Plain TTY-based interaction as above used to be quite feasible with
wenzelm@8547
    28
traditional tactic based theorem proving, but developing Isar documents really
wenzelm@8508
    29
demands some better user-interface support.  David Aspinall's
wenzelm@8508
    30
\emph{Proof~General}\index{Proof General} environment
wenzelm@8547
    31
\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs interface for
wenzelm@8547
    32
interactive theorem provers that does all the cut-and-paste and
wenzelm@8508
    33
forward-backward walk through the text in a very neat way.  In Isabelle/Isar,
wenzelm@8508
    34
the current position within a partial proof document is equally important than
wenzelm@8508
    35
the actual proof state.  Thus Proof~General provides the canonical working
wenzelm@8508
    36
environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
wenzelm@8547
    37
existing Isar documents) and for production work.
wenzelm@7175
    38
wenzelm@8843
    39
wenzelm@8843
    40
\subsubsection{Proof~General as default Isabelle interface}
wenzelm@7167
    41
wenzelm@9849
    42
The easiest way to invoke Proof~General is via the Isabelle interface wrapper
wenzelm@9849
    43
script.  The default configuration of Isabelle is smart enough to detect the
wenzelm@9849
    44
Proof~General distribution in several canonical places (e.g.\ 
wenzelm@9849
    45
\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}).  Thus the capital
wenzelm@9849
    46
\texttt{Isabelle} executable would already refer to the
wenzelm@9849
    47
\texttt{ProofGeneral/isar} interface without further ado.\footnote{There is
wenzelm@9849
    48
  also a \texttt{ProofGeneral/isa} interface for old tactic scripts written in
wenzelm@9849
    49
  ML.} The Isabelle interface script provides several options, just pass
wenzelm@9849
    50
\verb,-?, to see its usage.
wenzelm@7981
    51
wenzelm@7175
    52
With the proper Isabelle interface setup, Isar documents may now be edited by
wenzelm@7175
    53
visiting appropriate theory files, e.g.\ 
wenzelm@7175
    54
\begin{ttbox}
wenzelm@7175
    55
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
wenzelm@7175
    56
\end{ttbox}
wenzelm@7315
    57
Users of XEmacs may note the tool bar for navigating forward and backward
wenzelm@8516
    58
through the text.  Consult the Proof~General documentation \cite{proofgeneral}
wenzelm@8547
    59
for further basic command sequences, such as ``\texttt{C-c C-return}'' or
wenzelm@8547
    60
``\texttt{C-c u}''.
wenzelm@8508
    61
wenzelm@9849
    62
\medskip
wenzelm@9849
    63
wenzelm@9849
    64
Proof~General may be also configured manually by giving Isabelle settings like
wenzelm@9849
    65
this (see also \cite{isabelle-sys}):
wenzelm@9849
    66
\begin{ttbox}
wenzelm@9849
    67
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
wenzelm@9849
    68
PROOFGENERAL_OPTIONS=""
wenzelm@9849
    69
\end{ttbox}
wenzelm@9849
    70
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
wenzelm@9849
    71
actual installation directory of Proof~General.
wenzelm@9849
    72
wenzelm@9849
    73
\medskip
wenzelm@9849
    74
wenzelm@9849
    75
Apart from the Isabelle command line, defaults for interface options may be
wenzelm@9849
    76
given by the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For example, the
wenzelm@9849
    77
Emacs executable to be used may be configured in Isabelle's settings like this:
wenzelm@9849
    78
\begin{ttbox}
wenzelm@9849
    79
PROOFGENERAL_OPTIONS="-p xemacs-nomule"  
wenzelm@9849
    80
\end{ttbox}
wenzelm@9849
    81
wenzelm@9849
    82
Occasionally, the user's \verb,~/.emacs, file contains material that is
wenzelm@9849
    83
incompatible with the version of Emacs that Proof~General prefers.  Then
wenzelm@9849
    84
proper startup may be still achieved by using the \texttt{-u false} option.
wenzelm@9849
    85
Also note that any Emacs lisp file called \texttt{proofgeneral-settings.el}
wenzelm@9849
    86
occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}
wenzelm@9849
    87
is automatically loaded by the Proof~General interface script as well.
wenzelm@9849
    88
wenzelm@8843
    89
wenzelm@8843
    90
\subsubsection{The X-Symbol package}
wenzelm@8508
    91
wenzelm@8508
    92
Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which
wenzelm@8508
    93
provides a nice way to get proper mathematical symbols displayed on screen.
wenzelm@8508
    94
Just pass option \texttt{-x true} to the Isabelle interface script, or check
wenzelm@8516
    95
the appropriate menu setting by hand.  In any case, the X-Symbol package must
wenzelm@8516
    96
have been properly installed already.
wenzelm@8516
    97
wenzelm@8843
    98
Contrary to what you may expect from the documentation of X-Symbol, the
wenzelm@9849
    99
package is very easy to install and configures itself automatically.  The
wenzelm@9849
   100
default configuration of Isabelle is smart enough to detect the X-Symbol
wenzelm@9849
   101
package in several canonical places (e.g.\ 
wenzelm@9849
   102
\texttt{\$ISABELLE_HOME/contrib/x-symbol}).
wenzelm@8843
   103
wenzelm@8843
   104
\medskip
wenzelm@8843
   105
wenzelm@8843
   106
Using proper mathematical symbols in Isabelle theories can be very convenient
wenzelm@8843
   107
for readability of large formulas.  On the other hand, the plain ASCII sources
wenzelm@10160
   108
easily become somewhat unintelligible.  For example, $\Longrightarrow$ would
wenzelm@9849
   109
appear as \verb,\<Longrightarrow>, according the default set of Isabelle
wenzelm@9849
   110
symbols.  Nevertheless, the Isabelle document preparation system (see
wenzelm@9849
   111
\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
wenzelm@9849
   112
It is even possible to invent additional notation beyond the display
wenzelm@9849
   113
capabilities of XEmacs and X-Symbol.
wenzelm@7175
   114
wenzelm@7981
   115
wenzelm@7981
   116
\section{Isabelle/Isar theories}
wenzelm@7981
   117
wenzelm@8547
   118
Isabelle/Isar offers the following main improvements over classic Isabelle.
wenzelm@7981
   119
\begin{enumerate}
wenzelm@7981
   120
\item A new \emph{theory format}, occasionally referred to as ``new-style
wenzelm@7981
   121
  theories'', supporting interactive development and unlimited undo operation.
wenzelm@7981
   122
\item A \emph{formal proof document language} designed to support intelligible
wenzelm@7981
   123
  semi-automated reasoning.  Instead of putting together unreadable tactic
wenzelm@7981
   124
  scripts, the author is enabled to express the reasoning in way that is close
wenzelm@8508
   125
  to usual mathematical practice.
wenzelm@8547
   126
\item A simple document preparation system, for typesetting formal
wenzelm@8547
   127
  developments together with informal text.  The resulting hyper-linked PDF
wenzelm@8547
   128
  documents are equally well suited for WWW presentation and as printed
wenzelm@8547
   129
  copies.
wenzelm@7981
   130
\end{enumerate}
wenzelm@7981
   131
wenzelm@7981
   132
The Isar proof language is embedded into the new theory format as a proper
wenzelm@7981
   133
sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
wenzelm@7981
   134
$\LEMMANAME$ at the theory level, and left again with the final conclusion
wenzelm@7981
   135
(e.g.\ via $\QEDNAME$).  A few theory extension mechanisms require proof as
wenzelm@8547
   136
well, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness of the
wenzelm@8547
   137
representing sets.
wenzelm@7460
   138
wenzelm@7981
   139
New-style theory files may still be associated with separate ML files
wenzelm@7981
   140
consisting of plain old tactic scripts.  There is no longer any ML binding
wenzelm@7981
   141
generated for the theory and theorems, though.  ML functions \texttt{theory},
wenzelm@7981
   142
\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
wenzelm@7981
   143
Nevertheless, migration between classic Isabelle and Isabelle/Isar is
wenzelm@7981
   144
relatively easy.  Thus users may start to benefit from interactive theory
wenzelm@8547
   145
development and document preparation, even before they have any idea of the
wenzelm@8547
   146
Isar proof language at all.
wenzelm@7981
   147
wenzelm@7981
   148
\begin{warn}
wenzelm@8547
   149
  Currently, Proof~General does \emph{not} support mixed interactive
wenzelm@7981
   150
  development of classic Isabelle theory files or tactic scripts, together
wenzelm@7981
   151
  with Isar documents.  The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
wenzelm@7981
   152
  Proof~General are handled as two different theorem proving systems, only one
wenzelm@7981
   153
  of these may be active at the same time.
wenzelm@7981
   154
\end{warn}
wenzelm@7981
   155
wenzelm@10160
   156
Conversion of existing tactic scripts is best done by running two separate
wenzelm@7981
   157
Proof~General sessions, one for replaying the old script and the other for the
wenzelm@10160
   158
emerging Isabelle/Isar document.  Also note that Isar supports emulation
wenzelm@10160
   159
commands and methods that support traditional tactic scripts within new-style
wenzelm@10160
   160
theories, see appendix~\ref{ap:conv} for more information.
wenzelm@7981
   161
wenzelm@7167
   162
wenzelm@8843
   163
\subsection{Document preparation}\label{sec:document-prep}
wenzelm@8684
   164
wenzelm@8684
   165
Isabelle/Isar provides a simple document preparation system based on current
wenzelm@8684
   166
(PDF) {\LaTeX} technology, with full support of hyper-links (both local
wenzelm@8684
   167
references and URLs), bookmarks, thumbnails etc.  Thus the results are equally
wenzelm@8684
   168
well suited for WWW browsing and as printed copies.
wenzelm@8684
   169
wenzelm@8684
   170
\medskip
wenzelm@8684
   171
wenzelm@8684
   172
Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
wenzelm@8684
   173
  session} (see also \cite{isabelle-sys}).  Getting started with a working
wenzelm@8684
   174
configuration for common situations is quite easy by using the Isabelle
wenzelm@8684
   175
\texttt{mkdir} and \texttt{make} tools.  Just invoke
wenzelm@8684
   176
\begin{ttbox}
wenzelm@8684
   177
  isatool mkdir -d Foo
wenzelm@8684
   178
\end{ttbox}
wenzelm@8684
   179
to setup a separate directory for session \texttt{Foo}.\footnote{It is safe to
wenzelm@8684
   180
  experiment, since \texttt{isatool mkdir} never overwrites existing files.}
wenzelm@8684
   181
Ensure that \texttt{Foo/ROOT.ML} loads all theories required for this session.
wenzelm@8684
   182
Furthermore \texttt{Foo/document/root.tex} should include any special {\LaTeX}
wenzelm@8684
   183
macro packages required for your document (the default is usually sufficient
wenzelm@8684
   184
as a start).
wenzelm@8684
   185
wenzelm@8684
   186
The session is controlled by a separate \texttt{IsaMakefile} (with very crude
wenzelm@8684
   187
source dependencies only by default).  This file is located one level up from
wenzelm@8684
   188
the \texttt{Foo} directory location.  At that point just invoke
wenzelm@8684
   189
\begin{ttbox}
wenzelm@8684
   190
  isatool make Foo
wenzelm@8684
   191
\end{ttbox}
wenzelm@8684
   192
to run the \texttt{Foo} session, with browser information and document
wenzelm@8684
   193
preparation enabled.  Unless any errors are reported by Isabelle or {\LaTeX},
wenzelm@8684
   194
the output will appear inside the directory indicated by \texttt{isatool
wenzelm@8684
   195
  getenv ISABELLE_BROWSER_INFO}, with the logical session prefix added (e.g.\ 
wenzelm@8684
   196
\texttt{HOL/Foo}).  Note that the \texttt{index.html} located there provides a
wenzelm@8684
   197
link to the finished {\LaTeX} document, too.
wenzelm@8684
   198
wenzelm@8684
   199
Note that this really is batch processing --- better let Isabelle check your
wenzelm@8684
   200
theory and proof developments beforehand in interactive mode.
wenzelm@8684
   201
wenzelm@8684
   202
\medskip
wenzelm@8684
   203
wenzelm@8684
   204
You may also consider to tune the \texttt{usedir} options in
wenzelm@8684
   205
\texttt{IsaMakefile}, for example to change the output format from
wenzelm@8684
   206
\texttt{dvi} to \texttt{pdf}, or activate the \texttt{-D document} option in
wenzelm@8684
   207
order to preserve a copy of the generated {\LaTeX} sources.  The latter
wenzelm@8684
   208
feature is very useful for debugging {\LaTeX} errors, while avoiding repeated
wenzelm@8684
   209
runs of Isabelle.
wenzelm@8684
   210
wenzelm@8684
   211
\medskip
wenzelm@8684
   212
wenzelm@8684
   213
See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
wenzelm@8684
   214
on Isabelle logic sessions and theory presentation.
wenzelm@8684
   215
wenzelm@8684
   216
wenzelm@10160
   217
\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
wenzelm@7167
   218
wenzelm@7297
   219
This is one of the key questions, of course.  Isar offers a rather different
wenzelm@7297
   220
approach to formal proof documents than plain old tactic scripts.  Experienced
wenzelm@7297
   221
users of existing interactive theorem proving systems may have to learn
wenzelm@7895
   222
thinking differently in order to make effective use of Isabelle/Isar.  On the
wenzelm@7297
   223
other hand, Isabelle/Isar comes much closer to existing mathematical practice
wenzelm@7297
   224
of formal proof, so users with less experience in old-style tactical proving,
wenzelm@7895
   225
but a good understanding of mathematical proof, might cope with Isar even
wenzelm@10160
   226
better.  See also \cite{Wenzel:1999:TPHOL,Bauer-Wenzel:2000:HB} for further
wenzelm@10160
   227
background information on Isar.
wenzelm@7297
   228
wenzelm@10160
   229
\medskip This really is a reference manual on Isabelle/Isar, not a tutorial.
wenzelm@10160
   230
Nevertheless, we will also give some clues of how the concepts introduced here
wenzelm@10160
   231
may be put into practice.  Appendix~\ref{ap:refcard} provides a quick
wenzelm@10160
   232
reference card of the most common Isabelle/Isar language elements.
wenzelm@10160
   233
Appendix~\ref{ap:conv} offers some practical hints on converting existing
wenzelm@10160
   234
Isabelle theories and proof scripts to the new format.
wenzelm@10160
   235
wenzelm@10160
   236
Several example applications are distributed with Isabelle, and available via
wenzelm@10160
   237
the Isabelle WWW library as well as the Isabelle/Isar page:
wenzelm@7836
   238
\begin{center}\small
wenzelm@7836
   239
  \begin{tabular}{l}
wenzelm@7836
   240
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
wenzelm@8516
   241
    \url{http://isabelle.in.tum.de/library/} \\[1ex]
wenzelm@8508
   242
    \url{http://isabelle.in.tum.de/Isar/} \\
wenzelm@7836
   243
  \end{tabular}
wenzelm@7836
   244
\end{center}
wenzelm@7836
   245
wenzelm@10160
   246
The following examples may be of particular interest.  Apart from the plain
wenzelm@10160
   247
sources represented in HTML, these Isabelle sessions also provide actual
wenzelm@10160
   248
documents (in PDF).
wenzelm@10160
   249
\begin{itemize}
wenzelm@10160
   250
\item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
wenzelm@10160
   251
  collection of introductory examples.
wenzelm@10160
   252
\item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
wenzelm@10160
   253
  typical mathematics-style reasoning in ``axiomatic'' structures.
wenzelm@10160
   254
\item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
wenzelm@10160
   255
  big mathematics application on infinitary vector spaces and functional
wenzelm@10160
   256
  analysis.
wenzelm@10160
   257
\item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
wenzelm@10993
   258
  properties of $\lambda$-calculus (Church-Rosser and termination).
wenzelm@10993
   259
  
wenzelm@10993
   260
  This may serve as a realistic example of porting of legacy proof scripts
wenzelm@10993
   261
  into Isar tactic emulation scripts.
wenzelm@10993
   262
\item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
wenzelm@10993
   263
  model of the main aspects of the Unix file-system including its security
wenzelm@10993
   264
  model, but ignoring processes.  A few odd effects caused by the general
wenzelm@10993
   265
  ``worse-is-better'' approach followed in Unix are discussed within the
wenzelm@10993
   266
  formal model.
wenzelm@10993
   267
  
wenzelm@10993
   268
  This example represents a non-trivial verification task, with all proofs
wenzelm@10993
   269
  carefully worked out using the proper part of the Isar proof language;
wenzelm@10993
   270
  unstructured scripts are only used for symbolic evaluation.
wenzelm@10160
   271
\item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
wenzelm@10160
   272
  formalization of a fragment of Java, together with a corresponding virtual
wenzelm@10160
   273
  machine and a specification of its bytecode verifier and a lightweight
wenzelm@10993
   274
  bytecode verifier, including proofs of type-safety.
wenzelm@10993
   275
  
wenzelm@10993
   276
  This represents a very ``realistic'' example of large formalizations
wenzelm@11041
   277
  performed in form of tactic emulation scripts and proper Isar proof texts.
wenzelm@10160
   278
\end{itemize}
wenzelm@8547
   279
wenzelm@7167
   280
wenzelm@7046
   281
%%% Local Variables: 
wenzelm@7046
   282
%%% mode: latex
wenzelm@7046
   283
%%% TeX-master: "isar-ref"
wenzelm@7046
   284
%%% End: