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}
|
7895
|
18 |
Note that any Isabelle/Isar command may be retracted by \texttt{undo}; the
|
7981
|
19 |
\texttt{help} command prints a list of available language elements.
|
7175
|
20 |
|
|
21 |
Plain TTY-based interaction like this used to be quite feasible with
|
|
22 |
traditional tactic based theorem proving, but developing Isar documents
|
7297
|
23 |
demands some better user-interface support. \emph{Proof~General}\index{Proof
|
|
24 |
General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based
|
|
25 |
environment for interactive theorem provers that does all the cut-and-paste
|
7981
|
26 |
and forward-backward walk through the text in a very neat way. Note that in
|
|
27 |
Isabelle/Isar, the current position within a partial proof document is equally
|
|
28 |
important than the actual proof state. Thus Proof~General provides the
|
|
29 |
canonical working environment for Isabelle/Isar, both for getting acquainted
|
|
30 |
(e.g.\ by replaying existing Isar documents) and real production work.
|
7175
|
31 |
|
|
32 |
\medskip
|
7167
|
33 |
|
7315
|
34 |
The easiest way to use Proof~General is to make it the default Isabelle user
|
7895
|
35 |
interface. Just put something like this into your Isabelle settings file (see
|
|
36 |
also \cite{isabelle-sys}):
|
7175
|
37 |
\begin{ttbox}
|
|
38 |
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
|
7875
|
39 |
PROOFGENERAL_OPTIONS="-u false"
|
7175
|
40 |
\end{ttbox}
|
|
41 |
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
|
7335
|
42 |
actual installation directory of Proof~General. From now on, the capital
|
7315
|
43 |
\texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
|
7981
|
44 |
interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for
|
|
45 |
classic Isabelle tactic scripts.} Its usage is as follows:
|
7175
|
46 |
\begin{ttbox}
|
|
47 |
Usage: interface [OPTIONS] [FILES ...]
|
|
48 |
|
7460
|
49 |
Options are:
|
|
50 |
-l NAME logic image name (default $ISABELLE_LOGIC=HOL)
|
|
51 |
-p NAME Emacs program name (default xemacs)
|
|
52 |
-u BOOL use .emacs file (default true)
|
|
53 |
-w BOOL use window system (default true)
|
7175
|
54 |
|
7460
|
55 |
Starts Proof General for Isabelle/Isar with proof documents FILES
|
|
56 |
(default Scratch.thy).
|
|
57 |
|
|
58 |
PROOFGENERAL_OPTIONS=
|
7508
|
59 |
\end{ttbox} %$
|
7335
|
60 |
Apart from the command line, the defaults for these options may be overridden
|
|
61 |
via the \texttt{PROOFGENERAL_OPTIONS} setting as well. For example, plain GNU
|
7460
|
62 |
Emacs may be configured as follows:
|
7175
|
63 |
\begin{ttbox}
|
7981
|
64 |
PROOFGENERAL_OPTIONS="-u false -p emacs"
|
7175
|
65 |
\end{ttbox}
|
|
66 |
|
7981
|
67 |
Occasionally, a user's \texttt{.emacs} file contains material that is
|
|
68 |
incompatible with the version of (X)Emacs that Proof~General prefers. Then
|
|
69 |
proper startup may be still achieved by using the \texttt{-u false}
|
|
70 |
option.\footnote{Any Emacs lisp file \texttt{proofgeneral-settings.el}
|
|
71 |
occurring in \texttt{\$ISABELLE_HOME/etc} or
|
|
72 |
\texttt{\$ISABELLE_HOME_USER/etc} is automatically loaded by the
|
|
73 |
Proof~General interface script as well.}
|
|
74 |
|
|
75 |
\medskip
|
|
76 |
|
7175
|
77 |
With the proper Isabelle interface setup, Isar documents may now be edited by
|
|
78 |
visiting appropriate theory files, e.g.\
|
|
79 |
\begin{ttbox}
|
|
80 |
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
|
|
81 |
\end{ttbox}
|
7315
|
82 |
Users of XEmacs may note the tool bar for navigating forward and backward
|
7297
|
83 |
through the text. Consult the Proof~General documentation \cite{proofgeneral}
|
7981
|
84 |
for further basic command sequences, such as ``\texttt{c-c return}'' or
|
7895
|
85 |
``\texttt{c-c u}''.
|
7175
|
86 |
|
7981
|
87 |
|
|
88 |
\section{Isabelle/Isar theories}
|
|
89 |
|
|
90 |
Isabelle/Isar offers two main improvements over classic Isabelle:
|
|
91 |
\begin{enumerate}
|
|
92 |
\item A new \emph{theory format}, occasionally referred to as ``new-style
|
|
93 |
theories'', supporting interactive development and unlimited undo operation.
|
|
94 |
\item A \emph{formal proof document language} designed to support intelligible
|
|
95 |
semi-automated reasoning. Instead of putting together unreadable tactic
|
|
96 |
scripts, the author is enabled to express the reasoning in way that is close
|
|
97 |
to mathematical practice.
|
|
98 |
\end{enumerate}
|
|
99 |
|
|
100 |
The Isar proof language is embedded into the new theory format as a proper
|
|
101 |
sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or
|
|
102 |
$\LEMMANAME$ at the theory level, and left again with the final conclusion
|
|
103 |
(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as
|
|
104 |
well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of
|
|
105 |
the representing sets.
|
7460
|
106 |
|
7981
|
107 |
New-style theory files may still be associated with separate ML files
|
|
108 |
consisting of plain old tactic scripts. There is no longer any ML binding
|
|
109 |
generated for the theory and theorems, though. ML functions \texttt{theory},
|
|
110 |
\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
|
|
111 |
Nevertheless, migration between classic Isabelle and Isabelle/Isar is
|
|
112 |
relatively easy. Thus users may start to benefit from interactive theory
|
|
113 |
development even before they have any idea of the Isar proof language at all.
|
|
114 |
|
|
115 |
\begin{warn}
|
|
116 |
Currently Proof~General does \emph{not} support mixed interactive
|
|
117 |
development of classic Isabelle theory files or tactic scripts, together
|
|
118 |
with Isar documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
|
|
119 |
Proof~General are handled as two different theorem proving systems, only one
|
|
120 |
of these may be active at the same time.
|
|
121 |
\end{warn}
|
|
122 |
|
|
123 |
Porting of existing tactic scripts is best done by running two separate
|
|
124 |
Proof~General sessions, one for replaying the old script and the other for the
|
|
125 |
emerging Isabelle/Isar document.
|
|
126 |
|
7167
|
127 |
|
|
128 |
\section{How to write Isar proofs anyway?}
|
|
129 |
|
7297
|
130 |
This is one of the key questions, of course. Isar offers a rather different
|
|
131 |
approach to formal proof documents than plain old tactic scripts. Experienced
|
|
132 |
users of existing interactive theorem proving systems may have to learn
|
7895
|
133 |
thinking differently in order to make effective use of Isabelle/Isar. On the
|
7297
|
134 |
other hand, Isabelle/Isar comes much closer to existing mathematical practice
|
|
135 |
of formal proof, so users with less experience in old-style tactical proving,
|
7895
|
136 |
but a good understanding of mathematical proof, might cope with Isar even
|
7981
|
137 |
better. See also \cite{Wenzel:1999:TPHOL} for further background information
|
|
138 |
on Isar.
|
7297
|
139 |
|
7981
|
140 |
\medskip This really is a \emph{reference manual}. Nevertheless, we will also
|
|
141 |
give some clues of how the concepts introduced here may be put into practice.
|
|
142 |
Appendix~\ref{ap:refcard} provides a quick reference card of the most common
|
|
143 |
Isabelle/Isar language elements. There are several examples distributed with
|
|
144 |
Isabelle, and available via the Isabelle WWW library:
|
7836
|
145 |
\begin{center}\small
|
|
146 |
\begin{tabular}{l}
|
|
147 |
\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
|
|
148 |
\url{http://isabelle.in.tum.de/library/} \\
|
|
149 |
\end{tabular}
|
|
150 |
\end{center}
|
|
151 |
|
7987
|
152 |
See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
|
7981
|
153 |
\texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application. Apart from
|
|
154 |
browsable HTML sources, both sessions provide actual documents (in PDF).
|
7167
|
155 |
|
7046
|
156 |
%%% Local Variables:
|
|
157 |
%%% mode: latex
|
|
158 |
%%% TeX-master: "isar-ref"
|
|
159 |
%%% End:
|