doc-src/IsarRef/intro.tex
author wenzelm
Sat Mar 18 19:10:02 2000 +0100 (2000-03-18)
changeset 8516 f5f6a97ee43f
parent 8508 76d8d8aab881
child 8547 93b8685d004b
permissions -rw-r--r--
simplified setup;
tuned;
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@7175
    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@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@7895
    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@7175
    27
traditional tactic based theorem proving, but developing Isar documents
wenzelm@8508
    28
demands some better user-interface support.  David Aspinall's
wenzelm@8508
    29
\emph{Proof~General}\index{Proof General} environment
wenzelm@8508
    30
\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs-based interface
wenzelm@8508
    31
for 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@8508
    36
existing Isar documents) and real 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@8516
    53
The interface script provides several options, just pass ``\texttt{-?}'' to
wenzelm@8516
    54
see its usage.  Apart from the command line, the defaults for these options
wenzelm@8516
    55
may be 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@8508
    62
Also note that any Emacs lisp file \texttt{proofgeneral-settings.el} occurring
wenzelm@8508
    63
in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc} is
wenzelm@8508
    64
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@8516
    75
for further basic command sequences, such as ``\texttt{c-c c-return}'' or
wenzelm@8516
    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@8516
    91
notation beyond the display capabilities of XEmacs~/X-Symbol.
wenzelm@7175
    92
wenzelm@7981
    93
wenzelm@7981
    94
\section{Isabelle/Isar theories}
wenzelm@7981
    95
wenzelm@8516
    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@8516
   104
\item A simple document preparation system for Isabelle/Isar theories, for
wenzelm@8516
   105
  typesetting formal developments together with informal text.  The resulting
wenzelm@8516
   106
  resulting hyper-linked PDF documents are equally well suited for WWW
wenzelm@8516
   107
  presentation and printed 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@7981
   114
well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
wenzelm@7981
   115
the 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@7981
   123
development even before they have any idea of the Isar proof language at all.
wenzelm@7981
   124
wenzelm@7981
   125
\begin{warn}
wenzelm@7981
   126
  Currently Proof~General does \emph{not} support mixed interactive
wenzelm@7981
   127
  development of classic Isabelle theory files or tactic scripts, together
wenzelm@7981
   128
  with Isar documents.  The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
wenzelm@7981
   129
  Proof~General are handled as two different theorem proving systems, only one
wenzelm@7981
   130
  of these may be active at the same time.
wenzelm@7981
   131
\end{warn}
wenzelm@7981
   132
wenzelm@7981
   133
Porting of existing tactic scripts is best done by running two separate
wenzelm@7981
   134
Proof~General sessions, one for replaying the old script and the other for the
wenzelm@7981
   135
emerging Isabelle/Isar document.
wenzelm@7981
   136
wenzelm@7167
   137
wenzelm@7167
   138
\section{How to write Isar proofs anyway?}
wenzelm@7167
   139
wenzelm@7297
   140
This is one of the key questions, of course.  Isar offers a rather different
wenzelm@7297
   141
approach to formal proof documents than plain old tactic scripts.  Experienced
wenzelm@7297
   142
users of existing interactive theorem proving systems may have to learn
wenzelm@7895
   143
thinking differently in order to make effective use of Isabelle/Isar.  On the
wenzelm@7297
   144
other hand, Isabelle/Isar comes much closer to existing mathematical practice
wenzelm@7297
   145
of formal proof, so users with less experience in old-style tactical proving,
wenzelm@7895
   146
but a good understanding of mathematical proof, might cope with Isar even
wenzelm@7981
   147
better.  See also \cite{Wenzel:1999:TPHOL} for further background information
wenzelm@7981
   148
on Isar.
wenzelm@7297
   149
wenzelm@7981
   150
\medskip This really is a \emph{reference manual}.  Nevertheless, we will also
wenzelm@7981
   151
give some clues of how the concepts introduced here may be put into practice.
wenzelm@7981
   152
Appendix~\ref{ap:refcard} provides a quick reference card of the most common
wenzelm@7981
   153
Isabelle/Isar language elements.  There are several examples distributed with
wenzelm@8516
   154
Isabelle, and available via the Isabelle WWW library as well as the
wenzelm@8516
   155
Isabelle/Isar page:
wenzelm@7836
   156
\begin{center}\small
wenzelm@7836
   157
  \begin{tabular}{l}
wenzelm@7836
   158
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
wenzelm@8516
   159
    \url{http://isabelle.in.tum.de/library/} \\[1ex]
wenzelm@8508
   160
    \url{http://isabelle.in.tum.de/Isar/} \\
wenzelm@7836
   161
  \end{tabular}
wenzelm@7836
   162
\end{center}
wenzelm@7836
   163
wenzelm@7987
   164
See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
wenzelm@7981
   165
\texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application.  Apart from
wenzelm@8508
   166
plain HTML sources, these sessions also provide actual documents (in PDF).
wenzelm@7167
   167
wenzelm@7046
   168
%%% Local Variables: 
wenzelm@7046
   169
%%% mode: latex
wenzelm@7046
   170
%%% TeX-master: "isar-ref"
wenzelm@7046
   171
%%% End: