7046
|
1 |
|
|
2 |
\chapter{Introduction}
|
|
3 |
|
7167
|
4 |
\section{Quick start}
|
|
5 |
|
7175
|
6 |
Isar is already part of Isabelle (as of version Isabelle99, or later). The
|
|
7 |
\texttt{isabelle} binary provides option \texttt{-I} to run the Isar
|
|
8 |
interaction loop at startup, rather than the plain ML top-level. Thus the
|
|
9 |
quickest way to do anything with Isabelle/Isar is as follows:
|
|
10 |
\begin{ttbox}
|
|
11 |
isabelle -I HOL\medskip
|
|
12 |
\out{> Welcome to Isabelle/HOL (Isabelle99)}\medskip
|
|
13 |
theory Foo = Main:
|
7297
|
14 |
constdefs foo :: nat "foo == 1";
|
|
15 |
lemma "0 < foo" by (simp add: foo_def);
|
7175
|
16 |
end
|
|
17 |
\end{ttbox}
|
7315
|
18 |
Note that any Isabelle/Isar command may be retracted by \texttt{undo}.
|
7175
|
19 |
|
|
20 |
Plain TTY-based interaction like this used to be quite feasible with
|
|
21 |
traditional tactic based theorem proving, but developing Isar documents
|
7297
|
22 |
demands some better user-interface support. \emph{Proof~General}\index{Proof
|
|
23 |
General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based
|
|
24 |
environment for interactive theorem provers that does all the cut-and-paste
|
|
25 |
and forward-backward walk through the document in a very neat way. Note that
|
|
26 |
in Isabelle/Isar, the current position within a partial proof document is more
|
|
27 |
informative than the actual proof state. Thus Proof~General provides the
|
|
28 |
canonical working environment for Isabelle/Isar, both for getting acquainted
|
|
29 |
(e.g.\ by replaying existing Isar documents) and serious production work.
|
7175
|
30 |
|
|
31 |
\medskip
|
7167
|
32 |
|
7315
|
33 |
The easiest way to use Proof~General is to make it the default Isabelle user
|
7297
|
34 |
interface. Just say something like this in your Isabelle settings file (cf.\
|
|
35 |
\cite{isabelle-sys}):
|
7175
|
36 |
\begin{ttbox}
|
|
37 |
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
|
|
38 |
PROOFGENERAL_OPTIONS=""
|
|
39 |
\end{ttbox}
|
|
40 |
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
|
7335
|
41 |
actual installation directory of Proof~General. From now on, the capital
|
7315
|
42 |
\texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
|
7335
|
43 |
interface. Its usage is as follows:
|
7175
|
44 |
\begin{ttbox}
|
|
45 |
Usage: interface [OPTIONS] [FILES ...]
|
|
46 |
|
|
47 |
Options are:
|
|
48 |
-l NAME logic image name (default $ISABELLE_LOGIC=HOL)
|
|
49 |
-p NAME Emacs program name (default xemacs)
|
|
50 |
-u BOOL use .emacs file (default false)
|
|
51 |
-w BOOL use window system (default true)
|
|
52 |
|
7297
|
53 |
Starts Proof General for Isabelle/Isar with proof documents FILES
|
7175
|
54 |
(default Scratch.thy).
|
|
55 |
\end{ttbox}
|
7335
|
56 |
Apart from the command line, the defaults for these options may be overridden
|
|
57 |
via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For example, plain GNU
|
|
58 |
Emacs with loading of the startup file enabled\footnote{The interface disables
|
7315
|
59 |
\texttt{.emacs} by default to ensure successful startup despite any strange
|
7335
|
60 |
commands that tend to occur there.} may be configured as follows:
|
7175
|
61 |
\begin{ttbox}
|
|
62 |
PROOFGENERAL_OPTIONS="-p emacs -u true"
|
|
63 |
\end{ttbox}
|
|
64 |
|
|
65 |
With the proper Isabelle interface setup, Isar documents may now be edited by
|
|
66 |
visiting appropriate theory files, e.g.\
|
|
67 |
\begin{ttbox}
|
|
68 |
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
|
|
69 |
\end{ttbox}
|
7315
|
70 |
Users of XEmacs may note the tool bar for navigating forward and backward
|
7297
|
71 |
through the text. Consult the Proof~General documentation \cite{proofgeneral}
|
|
72 |
for further basic commands, such as \texttt{c-c return} or \texttt{c-c u}.
|
7175
|
73 |
|
7167
|
74 |
|
|
75 |
\section{How to write Isar proofs anyway?}
|
|
76 |
|
7297
|
77 |
This is one of the key questions, of course. Isar offers a rather different
|
|
78 |
approach to formal proof documents than plain old tactic scripts. Experienced
|
|
79 |
users of existing interactive theorem proving systems may have to learn
|
|
80 |
thinking different in order to make effective use of Isabelle/Isar. On the
|
|
81 |
other hand, Isabelle/Isar comes much closer to existing mathematical practice
|
|
82 |
of formal proof, so users with less experience in old-style tactical proving,
|
|
83 |
but a good understanding of mathematical proof might cope with Isar even
|
|
84 |
better.
|
|
85 |
|
|
86 |
Unfortunately, there is no tutorial on Isabelle/Isar available yet. This
|
|
87 |
document really is a \emph{reference manual}. Nevertheless, we will give some
|
|
88 |
discussions of the general principles underlying Isar in
|
|
89 |
chapter~\ref{ch:basics}, and provide some clues of how these may be put into
|
|
90 |
practice. Some more background information on Isar is given in
|
|
91 |
\cite{Wenzel:1999:TPHOL}. Furthermore, there are several examples distributed
|
|
92 |
with Isabelle (see directory \texttt{HOL/Isar_examples}).
|
7175
|
93 |
|
7167
|
94 |
|
7046
|
95 |
%%% Local Variables:
|
|
96 |
%%% mode: latex
|
|
97 |
%%% TeX-master: "isar-ref"
|
|
98 |
%%% End:
|