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