wenzelm@7046

1 

wenzelm@7046

2 
\chapter{Introduction}

wenzelm@7046

3 

wenzelm@12618

4 
\section{Overview}

wenzelm@12618

5 

wenzelm@12618

6 
The \emph{Isabelle} system essentially provides a generic infrastructure for

wenzelm@12618

7 
building deductive systems (programmed in Standard ML), with a special focus

wenzelm@12618

8 
on interactive theorem proving in higherorder logics. In the olden days even

wenzelm@12618

9 
endusers would refer to certain ML functions (goal commands, tactics,

wenzelm@12879

10 
tacticals etc.) to pursue their everyday theorem proving tasks

wenzelm@12618

11 
\cite{isabelleintro,isabelleref}.

wenzelm@12618

12 

wenzelm@12618

13 
In contrast \emph{Isar} provides an interpreted language environment of its

wenzelm@12618

14 
own, which has been specifically tailored for the needs of theory and proof

wenzelm@12618

15 
development. Compared to raw ML, the Isabelle/Isar toplevel provides a more

wenzelm@12618

16 
robust and comfortable development platform, with proper support for theory

wenzelm@13039

17 
development graphs, singlestep transactions with unlimited undo, etc. The

wenzelm@12618

18 
Isabelle/Isar version of the \emph{Proof~General} user interface

wenzelm@12618

19 
\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate frontend for

wenzelm@13039

20 
interactive theory and proof development in this advanced theorem proving

wenzelm@13039

21 
environment.

wenzelm@12618

22 

wenzelm@13039

23 
\medskip Apart from the technical advances over barebones ML programming, the

wenzelm@13039

24 
main purpose of the Isar language is to provide a conceptually different view

wenzelm@13039

25 
on machinechecked proofs \cite{Wenzel:1999:TPHOL,WenzelPhD}. ``Isar''

wenzelm@13039

26 
stands for ``Intelligible semiautomated reasoning''. Drawing from both the

wenzelm@12618

27 
traditions of informal mathematical proof texts and highlevel programming

wenzelm@13039

28 
languages, Isar offers a versatile environment for structured formal proof

wenzelm@13039

29 
documents. Thus properly written Isar proofs become accessible to a broader

wenzelm@13039

30 
audience than unstructured tactic scripts (which typically only provide

wenzelm@13039

31 
operational information for the machine). Writing humanreadable proof texts

wenzelm@13039

32 
certainly requires some additional efforts by the writer to achieve a good

wenzelm@13039

33 
presentation, both of formal and informal parts of the text. On the other

wenzelm@13039

34 
hand, humanreadable formal texts gain some value in their own right,

wenzelm@13039

35 
independently of the mechanic proofchecking process.

wenzelm@12618

36 

wenzelm@12618

37 
Despite its grand design of structured proof texts, Isar is able to assimilate

wenzelm@12879

38 
the old tactical style as an ``improper'' sublanguage. This provides an easy

wenzelm@12618

39 
upgrade path for existing tactic scripts, as well as additional means for

wenzelm@12879

40 
interactive experimentation and debugging of structured proofs. Isabelle/Isar

wenzelm@12879

41 
supports a broad range of proof styles, both readable and unreadable ones.

wenzelm@12618

42 

wenzelm@12879

43 
\medskip The Isabelle/Isar framework is generic and should work reasonably

wenzelm@12879

44 
well for any Isabelle objectlogic that conforms to the natural deduction view

wenzelm@12879

45 
of the Isabelle/Pure framework. Major Isabelle logics like HOL

wenzelm@12879

46 
\cite{isabelleHOL}, HOLCF \cite{MuellerNvOS99}, FOL \cite{isabellelogics},

wenzelm@12879

47 
and ZF \cite{isabelleZF} have already been set up for endusers.

wenzelm@12879

48 
Nonetheless, much of the existing body of theories still consist of oldstyle

wenzelm@12879

49 
theory files with accompanied ML code for proof scripts; this legacy will be

wenzelm@12879

50 
gradually converted in due time.

wenzelm@12618

51 

wenzelm@12618

52 

wenzelm@7167

53 
\section{Quick start}

wenzelm@7167

54 

wenzelm@8508

55 
\subsection{Terminal sessions}

wenzelm@8508

56 

wenzelm@12879

57 
Isar is already part of Isabelle. The lowlevel \texttt{isabelle} binary

wenzelm@12879

58 
provides option \texttt{I} to run the Isabelle/Isar interaction loop at

wenzelm@12879

59 
startup, rather than the raw ML toplevel. So the most basic way to do

wenzelm@12879

60 
anything with Isabelle/Isar is as follows:

wenzelm@7175

61 
\begin{ttbox}

wenzelm@7175

62 
isabelle I HOL\medskip

wenzelm@17567

63 
\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip

wenzelm@17567

64 
theory Foo imports Main begin;

wenzelm@7297

65 
constdefs foo :: nat "foo == 1";

wenzelm@7297

66 
lemma "0 < foo" by (simp add: foo_def);

wenzelm@17567

67 
end;

wenzelm@7175

68 
\end{ttbox}

wenzelm@9233

69 
Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See

wenzelm@10160

70 
the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a

wenzelm@10110

71 
comprehensive overview of available commands and other language elements.

wenzelm@7175

72 

wenzelm@8508

73 

wenzelm@8843

74 
\subsection{Proof~General}

wenzelm@8508

75 

wenzelm@8508

76 
Plain TTYbased interaction as above used to be quite feasible with

wenzelm@8547

77 
traditional tactic based theorem proving, but developing Isar documents really

wenzelm@12879

78 
demands some better userinterface support. The Proof~General environment by

wenzelm@12879

79 
David Aspinall \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs

wenzelm@12879

80 
interface for interactive theorem provers that organizes all the cutandpaste

wenzelm@12879

81 
and forwardbackward walk through the text in a very neat way. In

wenzelm@12879

82 
Isabelle/Isar, the current position within a partial proof document is equally

wenzelm@12879

83 
important than the actual proof state. Thus Proof~General provides the

wenzelm@12879

84 
canonical working environment for Isabelle/Isar, both for getting acquainted

wenzelm@12879

85 
(e.g.\ by replaying existing Isar documents) and for production work.

wenzelm@7175

86 

wenzelm@8843

87 

wenzelm@8843

88 
\subsubsection{Proof~General as default Isabelle interface}

wenzelm@7167

89 

wenzelm@12879

90 
The Isabelle interface wrapper script provides an easy way to invoke

wenzelm@21703

91 
Proof~General (including XEmacs or GNU Emacs). The default

wenzelm@21703

92 
configuration of Isabelle is smart enough to detect the Proof~General

wenzelm@21703

93 
distribution in several canonical places (e.g.\

wenzelm@21703

94 
\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital

wenzelm@21703

95 
\texttt{Isabelle} executable would already refer to the

wenzelm@21703

96 
\texttt{ProofGeneral/isar} interface without further ado. The

wenzelm@21703

97 
Isabelle interface script provides several options; pass \verb,?, to

wenzelm@21703

98 
see its usage.

wenzelm@7981

99 

wenzelm@7175

100 
With the proper Isabelle interface setup, Isar documents may now be edited by

wenzelm@7175

101 
visiting appropriate theory files, e.g.\

wenzelm@7175

102 
\begin{ttbox}

wenzelm@12879

103 
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy

wenzelm@7175

104 
\end{ttbox}

wenzelm@13039

105 
Beginners may note the tool bar for navigating forward and backward through

wenzelm@13039

106 
the text (this depends on the local Emacs installation). Consult the

wenzelm@12879

107 
Proof~General documentation \cite{proofgeneral} for further basic command

wenzelm@12879

108 
sequences, in particular ``\texttt{Cc Creturn}'' and ``\texttt{Cc u}''.

wenzelm@8508

109 

wenzelm@9849

110 
\medskip

wenzelm@9849

111 

wenzelm@9849

112 
Proof~General may be also configured manually by giving Isabelle settings like

wenzelm@9849

113 
this (see also \cite{isabellesys}):

wenzelm@9849

114 
\begin{ttbox}

wenzelm@9849

115 
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface

wenzelm@9849

116 
PROOFGENERAL_OPTIONS=""

wenzelm@9849

117 
\end{ttbox}

wenzelm@9849

118 
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the

wenzelm@9849

119 
actual installation directory of Proof~General.

wenzelm@9849

120 

wenzelm@9849

121 
\medskip

wenzelm@9849

122 

wenzelm@9849

123 
Apart from the Isabelle command line, defaults for interface options may be

wenzelm@12879

124 
given by the \texttt{PROOFGENERAL_OPTIONS} setting. For example, the Emacs

wenzelm@12879

125 
executable to be used may be configured in Isabelle's settings like this:

wenzelm@9849

126 
\begin{ttbox}

wenzelm@16016

127 
PROOFGENERAL_OPTIONS="p xemacsmule"

wenzelm@9849

128 
\end{ttbox}

wenzelm@9849

129 

wenzelm@12879

130 
Occasionally, a user's \verb,~/.emacs, file contains code that is incompatible

wenzelm@12879

131 
with the (X)Emacs version used by Proof~General, causing the interface startup

wenzelm@12879

132 
to fail prematurely. Here the \texttt{u false} option helps to get the

wenzelm@12879

133 
interface process up and running. Note that additional Lisp customization

wenzelm@12879

134 
code may reside in \texttt{proofgeneralsettings.el} of

wenzelm@12879

135 
\texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}.

wenzelm@9849

136 

wenzelm@8843

137 

wenzelm@8843

138 
\subsubsection{The XSymbol package}

wenzelm@8508

139 

wenzelm@12879

140 
Proof~General provides native support for the Emacs XSymbol package

wenzelm@12879

141 
\cite{xsymbol}, which handles proper mathematical symbols displayed on

wenzelm@12879

142 
screen. Pass option \texttt{x true} to the Isabelle interface script, or

wenzelm@12879

143 
check the appropriate Proof~General menu setting by hand. In any case, the

wenzelm@12879

144 
XSymbol package must have been properly installed already.

wenzelm@8516

145 

wenzelm@8843

146 
Contrary to what you may expect from the documentation of XSymbol, the

wenzelm@9849

147 
package is very easy to install and configures itself automatically. The

wenzelm@9849

148 
default configuration of Isabelle is smart enough to detect the XSymbol

wenzelm@9849

149 
package in several canonical places (e.g.\

wenzelm@9849

150 
\texttt{\$ISABELLE_HOME/contrib/xsymbol}).

wenzelm@8843

151 

wenzelm@8843

152 
\medskip

wenzelm@8843

153 

wenzelm@8843

154 
Using proper mathematical symbols in Isabelle theories can be very convenient

wenzelm@8843

155 
for readability of large formulas. On the other hand, the plain ASCII sources

wenzelm@10160

156 
easily become somewhat unintelligible. For example, $\Longrightarrow$ would

wenzelm@9849

157 
appear as \verb,\<Longrightarrow>, according the default set of Isabelle

wenzelm@9849

158 
symbols. Nevertheless, the Isabelle document preparation system (see

wenzelm@9849

159 
\S\ref{sec:documentprep}) will be happy to print nonASCII symbols properly.

wenzelm@9849

160 
It is even possible to invent additional notation beyond the display

wenzelm@12879

161 
capabilities of Emacs and XSymbol.

wenzelm@7175

162 

wenzelm@7981

163 

wenzelm@7981

164 
\section{Isabelle/Isar theories}

wenzelm@7981

165 

wenzelm@8547

166 
Isabelle/Isar offers the following main improvements over classic Isabelle.

wenzelm@7981

167 
\begin{enumerate}

wenzelm@13039

168 

wenzelm@7981

169 
\item A new \emph{theory format}, occasionally referred to as ``newstyle

wenzelm@7981

170 
theories'', supporting interactive development and unlimited undo operation.

wenzelm@13039

171 

wenzelm@7981

172 
\item A \emph{formal proof document language} designed to support intelligible

wenzelm@7981

173 
semiautomated reasoning. Instead of putting together unreadable tactic

wenzelm@7981

174 
scripts, the author is enabled to express the reasoning in way that is close

wenzelm@13039

175 
to usual mathematical practice. The old tactical style has been assimilated

wenzelm@13039

176 
as ``improper'' language elements.

wenzelm@13039

177 

wenzelm@8547

178 
\item A simple document preparation system, for typesetting formal

wenzelm@8547

179 
developments together with informal text. The resulting hyperlinked PDF

wenzelm@8547

180 
documents are equally well suited for WWW presentation and as printed

wenzelm@8547

181 
copies.

wenzelm@13039

182 

wenzelm@7981

183 
\end{enumerate}

wenzelm@7981

184 

wenzelm@7981

185 
The Isar proof language is embedded into the new theory format as a proper

wenzelm@7981

186 
sublanguage. Proof mode is entered by stating some $\THEOREMNAME$ or

wenzelm@7981

187 
$\LEMMANAME$ at the theory level, and left again with the final conclusion

wenzelm@12879

188 
(e.g.\ via $\QEDNAME$). A few theory specification mechanisms also require

wenzelm@12879

189 
some proof, such as HOL's $\isarkeyword{typedef}$ which demands nonemptiness

wenzelm@12879

190 
of the representing sets.

wenzelm@7460

191 

wenzelm@7981

192 
Newstyle theory files may still be associated with separate ML files

wenzelm@7981

193 
consisting of plain old tactic scripts. There is no longer any ML binding

wenzelm@7981

194 
generated for the theory and theorems, though. ML functions \texttt{theory},

wenzelm@13039

195 
\texttt{thm}, and \texttt{thms} retrieve this information from the context

wenzelm@13039

196 
\cite{isabelleref}. Nevertheless, migration between classic Isabelle and

wenzelm@13039

197 
Isabelle/Isar is relatively easy. Thus users may start to benefit from

wenzelm@13039

198 
interactive theory development and document preparation, even before they have

wenzelm@13039

199 
any idea of the Isar proof language at all.

wenzelm@7981

200 

wenzelm@7981

201 
\begin{warn}

wenzelm@12879

202 
Proof~General does \emph{not} support mixed interactive development of

wenzelm@12879

203 
classic Isabelle theory files or tactic scripts, together with Isar

wenzelm@12879

204 
documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of

wenzelm@7981

205 
Proof~General are handled as two different theorem proving systems, only one

wenzelm@7981

206 
of these may be active at the same time.

wenzelm@7981

207 
\end{warn}

wenzelm@7981

208 

wenzelm@12879

209 
Manual conversion of existing tactic scripts may be done by running two

wenzelm@12879

210 
separate Proof~General sessions, one for replaying the old script and the

wenzelm@12879

211 
other for the emerging Isabelle/Isar document. Also note that Isar supports

wenzelm@12879

212 
emulation commands and methods that support traditional tactic scripts within

wenzelm@12879

213 
newstyle theories, see appendix~\ref{ap:conv} for more information.

wenzelm@7981

214 

wenzelm@7167

215 

wenzelm@8843

216 
\subsection{Document preparation}\label{sec:documentprep}

wenzelm@8684

217 

wenzelm@12879

218 
Isabelle/Isar provides a simple document preparation system based on existing

wenzelm@13039

219 
{PDF\LaTeX} technology, with full support of hyperlinks (both local

wenzelm@13039

220 
references and URLs), bookmarks, and thumbnails. Thus the results are equally

wenzelm@13039

221 
well suited for WWW browsing and as printed copies.

wenzelm@8684

222 

wenzelm@8684

223 
\medskip

wenzelm@8684

224 

wenzelm@8684

225 
Isabelle generates {\LaTeX} output as part of the run of a \emph{logic

wenzelm@8684

226 
session} (see also \cite{isabellesys}). Getting started with a working

wenzelm@8684

227 
configuration for common situations is quite easy by using the Isabelle

wenzelm@12879

228 
\texttt{mkdir} and \texttt{make} tools. First invoke

wenzelm@8684

229 
\begin{ttbox}

wenzelm@12879

230 
isatool mkdir Foo

wenzelm@8684

231 
\end{ttbox}

wenzelm@12879

232 
to initialize a separate directory for session \texttt{Foo}  it is safe to

wenzelm@12879

233 
experiment, since \texttt{isatool mkdir} never overwrites existing files.

wenzelm@12879

234 
Ensure that \texttt{Foo/ROOT.ML} holds ML commands to load all theories

wenzelm@12879

235 
required for this session; furthermore \texttt{Foo/document/root.tex} should

wenzelm@12879

236 
include any special {\LaTeX} macro packages required for your document (the

wenzelm@12879

237 
default is usually sufficient as a start).

wenzelm@8684

238 

wenzelm@12879

239 
The session is controlled by a separate \texttt{IsaMakefile} (with crude

wenzelm@12879

240 
source dependencies by default). This file is located one level up from the

wenzelm@12879

241 
\texttt{Foo} directory location. Now invoke

wenzelm@8684

242 
\begin{ttbox}

wenzelm@8684

243 
isatool make Foo

wenzelm@8684

244 
\end{ttbox}

wenzelm@8684

245 
to run the \texttt{Foo} session, with browser information and document

wenzelm@8684

246 
preparation enabled. Unless any errors are reported by Isabelle or {\LaTeX},

wenzelm@12879

247 
the output will appear inside the directory \texttt{ISABELLE_BROWSER_INFO}, as

wenzelm@12879

248 
reported by the batch job in verbose mode.

wenzelm@8684

249 

wenzelm@8684

250 
\medskip

wenzelm@8684

251 

wenzelm@8684

252 
You may also consider to tune the \texttt{usedir} options in

wenzelm@8684

253 
\texttt{IsaMakefile}, for example to change the output format from

wenzelm@13039

254 
\texttt{pdf} to \texttt{dvi}, or activate the \texttt{D} option to retain a

wenzelm@13039

255 
second copy of the generated {\LaTeX} sources.

wenzelm@8684

256 

wenzelm@8684

257 
\medskip

wenzelm@8684

258 

wenzelm@8684

259 
See \emph{The Isabelle System Manual} \cite{isabellesys} for further details

wenzelm@12879

260 
on Isabelle logic sessions and theory presentation. The Isabelle/HOL tutorial

wenzelm@12879

261 
\cite{isabelleholbook} also covers theory presentation issues.

wenzelm@8684

262 

wenzelm@8684

263 

wenzelm@10160

264 
\subsection{How to write Isar proofs anyway?}\label{sec:isarhowto}

wenzelm@7167

265 

wenzelm@12879

266 
This is one of the key questions, of course. First of all, the tactic script

wenzelm@12879

267 
emulation of Isabelle/Isar essentially provides a clarified version of the

wenzelm@12879

268 
very same unstructured proof style of classic Isabelle. Oldtime users should

wenzelm@13039

269 
quickly become acquainted with that (slightly degenerative) view of Isar.

wenzelm@12621

270 

wenzelm@12879

271 
Writing \emph{proper} Isar proof texts targeted at human readers is quite

wenzelm@12879

272 
different, though. Experienced users of the unstructured style may even have

wenzelm@12879

273 
to unlearn some of their habits to master proof composition in Isar. In

wenzelm@12879

274 
contrast, new users with less experience in oldstyle tactical proving, but a

wenzelm@13039

275 
good understanding of mathematical proof in general, often get started easier.

wenzelm@7297

276 

wenzelm@12879

277 
\medskip The present text really is only a reference manual on Isabelle/Isar,

wenzelm@12879

278 
not a tutorial. Nevertheless, we will attempt to give some clues of how the

wenzelm@12879

279 
concepts introduced here may be put into practice. Appendix~\ref{ap:refcard}

wenzelm@12879

280 
provides a quick reference card of the most common Isabelle/Isar language

wenzelm@12879

281 
elements. Appendix~\ref{ap:conv} offers some practical hints on converting

wenzelm@12879

282 
existing Isabelle theories and proof scripts to the new format (without

wenzelm@12879

283 
restructuring proofs).

wenzelm@10160

284 

wenzelm@12879

285 
Further issues concerning the Isar concepts are covered in the literature

wenzelm@12879

286 
\cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,BauerWenzel:2000:HB,BauerWenzel:2001}.

wenzelm@12879

287 
The author's PhD thesis \cite{WenzelPhD} presently provides the most complete

wenzelm@12879

288 
exposition of Isar foundations, techniques, and applications. A number of

wenzelm@12879

289 
example applications are distributed with Isabelle, and available via the

wenzelm@12879

290 
Isabelle WWW library (e.g.\ \url{http://isabelle.in.tum.de/library/}). As a

wenzelm@12879

291 
general rule of thumb, more recent Isabelle applications that also include a

wenzelm@12879

292 
separate ``document'' (in PDF) are more likely to consist of proper

wenzelm@12879

293 
Isabelle/Isar theories and proofs.

wenzelm@7836

294 

wenzelm@12879

295 
%FIXME

wenzelm@12879

296 
% The following examples may be of particular interest. Apart from the plain

wenzelm@12879

297 
% sources represented in HTML, these Isabelle sessions also provide actual

wenzelm@12879

298 
% documents (in PDF).

wenzelm@12879

299 
% \begin{itemize}

wenzelm@12879

300 
% \item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a

wenzelm@12879

301 
% collection of introductory examples.

wenzelm@12879

302 
% \item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of

wenzelm@12879

303 
% typical mathematicsstyle reasoning in ``axiomatic'' structures.

wenzelm@12879

304 
% \item \url{http://isabelle.in.tum.de/library/HOL/HOLReal/HahnBanach/} is a

wenzelm@12879

305 
% big mathematics application on infinitary vector spaces and functional

wenzelm@12879

306 
% analysis.

wenzelm@12879

307 
% \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental

wenzelm@12879

308 
% properties of $\lambda$calculus (ChurchRosser and termination).

wenzelm@10993

309 

wenzelm@12879

310 
% This may serve as a realistic example of porting of legacy proof scripts

wenzelm@12879

311 
% into Isar tactic emulation scripts.

wenzelm@12879

312 
% \item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical

wenzelm@12879

313 
% model of the main aspects of the Unix filesystem including its security

wenzelm@12879

314 
% model, but ignoring processes. A few odd effects caused by the general

wenzelm@12879

315 
% ``worseisbetter'' approach followed in Unix are discussed within the

wenzelm@12879

316 
% formal model.

wenzelm@10993

317 

wenzelm@12879

318 
% This example represents a nontrivial verification task, with all proofs

wenzelm@12879

319 
% carefully worked out using the proper part of the Isar proof language;

wenzelm@12879

320 
% unstructured scripts are only used for symbolic evaluation.

wenzelm@12879

321 
% \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a

wenzelm@12879

322 
% formalization of a fragment of Java, together with a corresponding virtual

wenzelm@12879

323 
% machine and a specification of its bytecode verifier and a lightweight

wenzelm@12879

324 
% bytecode verifier, including proofs of typesafety.

wenzelm@10993

325 

wenzelm@12879

326 
% This represents a very ``realistic'' example of large formalizations

wenzelm@12879

327 
% performed in form of tactic emulation scripts and proper Isar proof texts.

wenzelm@12879

328 
% \end{itemize}

wenzelm@8547

329 

wenzelm@7167

330 

wenzelm@7046

331 
%%% Local Variables:

wenzelm@7046

332 
%%% mode: latex

wenzelm@7046

333 
%%% TeXmaster: "isarref"

wenzelm@7046

334 
%%% End:
