doc-src/IsarRef/intro.tex
author wenzelm
Thu Sep 28 19:06:46 2000 +0200 (2000-09-28)
changeset 10110 7d6e03a1f11e
parent 9849 71ad08ad2cf0
child 10160 bb8f9412fec6
permissions -rw-r--r--
fixed ref;
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@10110
    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@9849
   108
easily become somewhat unintelligible.  For example, $\Longrightarrow$ will
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@7981
   156
Porting 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@7981
   158
emerging Isabelle/Isar document.
wenzelm@7981
   159
wenzelm@7167
   160
wenzelm@8843
   161
\subsection{Document preparation}\label{sec:document-prep}
wenzelm@8684
   162
wenzelm@8684
   163
Isabelle/Isar provides a simple document preparation system based on current
wenzelm@8684
   164
(PDF) {\LaTeX} technology, with full support of hyper-links (both local
wenzelm@8684
   165
references and URLs), bookmarks, thumbnails etc.  Thus the results are equally
wenzelm@8684
   166
well suited for WWW browsing and as printed copies.
wenzelm@8684
   167
wenzelm@8684
   168
\medskip
wenzelm@8684
   169
wenzelm@8684
   170
Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
wenzelm@8684
   171
  session} (see also \cite{isabelle-sys}).  Getting started with a working
wenzelm@8684
   172
configuration for common situations is quite easy by using the Isabelle
wenzelm@8684
   173
\texttt{mkdir} and \texttt{make} tools.  Just invoke
wenzelm@8684
   174
\begin{ttbox}
wenzelm@8684
   175
  isatool mkdir -d Foo
wenzelm@8684
   176
\end{ttbox}
wenzelm@8684
   177
to setup a separate directory for session \texttt{Foo}.\footnote{It is safe to
wenzelm@8684
   178
  experiment, since \texttt{isatool mkdir} never overwrites existing files.}
wenzelm@8684
   179
Ensure that \texttt{Foo/ROOT.ML} loads all theories required for this session.
wenzelm@8684
   180
Furthermore \texttt{Foo/document/root.tex} should include any special {\LaTeX}
wenzelm@8684
   181
macro packages required for your document (the default is usually sufficient
wenzelm@8684
   182
as a start).
wenzelm@8684
   183
wenzelm@8684
   184
The session is controlled by a separate \texttt{IsaMakefile} (with very crude
wenzelm@8684
   185
source dependencies only by default).  This file is located one level up from
wenzelm@8684
   186
the \texttt{Foo} directory location.  At that point just invoke
wenzelm@8684
   187
\begin{ttbox}
wenzelm@8684
   188
  isatool make Foo
wenzelm@8684
   189
\end{ttbox}
wenzelm@8684
   190
to run the \texttt{Foo} session, with browser information and document
wenzelm@8684
   191
preparation enabled.  Unless any errors are reported by Isabelle or {\LaTeX},
wenzelm@8684
   192
the output will appear inside the directory indicated by \texttt{isatool
wenzelm@8684
   193
  getenv ISABELLE_BROWSER_INFO}, with the logical session prefix added (e.g.\ 
wenzelm@8684
   194
\texttt{HOL/Foo}).  Note that the \texttt{index.html} located there provides a
wenzelm@8684
   195
link to the finished {\LaTeX} document, too.
wenzelm@8684
   196
wenzelm@8684
   197
Note that this really is batch processing --- better let Isabelle check your
wenzelm@8684
   198
theory and proof developments beforehand in interactive mode.
wenzelm@8684
   199
wenzelm@8684
   200
\medskip
wenzelm@8684
   201
wenzelm@8684
   202
You may also consider to tune the \texttt{usedir} options in
wenzelm@8684
   203
\texttt{IsaMakefile}, for example to change the output format from
wenzelm@8684
   204
\texttt{dvi} to \texttt{pdf}, or activate the \texttt{-D document} option in
wenzelm@8684
   205
order to preserve a copy of the generated {\LaTeX} sources.  The latter
wenzelm@8684
   206
feature is very useful for debugging {\LaTeX} errors, while avoiding repeated
wenzelm@8684
   207
runs of Isabelle.
wenzelm@8684
   208
wenzelm@8684
   209
\medskip
wenzelm@8684
   210
wenzelm@8684
   211
See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
wenzelm@8684
   212
on Isabelle logic sessions and theory presentation.
wenzelm@8684
   213
wenzelm@8684
   214
wenzelm@8684
   215
\subsection{How to write Isar proofs anyway?}
wenzelm@7167
   216
wenzelm@7297
   217
This is one of the key questions, of course.  Isar offers a rather different
wenzelm@7297
   218
approach to formal proof documents than plain old tactic scripts.  Experienced
wenzelm@7297
   219
users of existing interactive theorem proving systems may have to learn
wenzelm@7895
   220
thinking differently in order to make effective use of Isabelle/Isar.  On the
wenzelm@7297
   221
other hand, Isabelle/Isar comes much closer to existing mathematical practice
wenzelm@7297
   222
of formal proof, so users with less experience in old-style tactical proving,
wenzelm@7895
   223
but a good understanding of mathematical proof, might cope with Isar even
wenzelm@7981
   224
better.  See also \cite{Wenzel:1999:TPHOL} for further background information
wenzelm@7981
   225
on Isar.
wenzelm@8547
   226
%FIXME cite [HahnBanach-in-Isar]
wenzelm@7297
   227
wenzelm@7981
   228
\medskip This really is a \emph{reference manual}.  Nevertheless, we will also
wenzelm@7981
   229
give some clues of how the concepts introduced here may be put into practice.
wenzelm@7981
   230
Appendix~\ref{ap:refcard} provides a quick reference card of the most common
wenzelm@7981
   231
Isabelle/Isar language elements.  There are several examples distributed with
wenzelm@8516
   232
Isabelle, and available via the Isabelle WWW library as well as the
wenzelm@8516
   233
Isabelle/Isar page:
wenzelm@7836
   234
\begin{center}\small
wenzelm@7836
   235
  \begin{tabular}{l}
wenzelm@7836
   236
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
wenzelm@8516
   237
    \url{http://isabelle.in.tum.de/library/} \\[1ex]
wenzelm@8508
   238
    \url{http://isabelle.in.tum.de/Isar/} \\
wenzelm@7836
   239
  \end{tabular}
wenzelm@7836
   240
\end{center}
wenzelm@7836
   241
wenzelm@7987
   242
See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
wenzelm@8547
   243
\texttt{HOL/HOL-Real/HahnBanach} for a big mathematics application.  Apart
wenzelm@8547
   244
from plain HTML sources, these sessions also provide actual documents (in
wenzelm@8547
   245
PDF).
wenzelm@8547
   246
wenzelm@7167
   247
wenzelm@7046
   248
%%% Local Variables: 
wenzelm@7046
   249
%%% mode: latex
wenzelm@7046
   250
%%% TeX-master: "isar-ref"
wenzelm@7046
   251
%%% End: