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@9604

9 
\texttt{isabelle} binary provides option \texttt{I} to run the Isabelle/Isar

wenzelm@9604

10 
interaction loop at startup, rather than the raw ML toplevel. So the

wenzelm@9604

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@9272

14 
\out{> Welcome to Isabelle/HOL (Isabelle991)}\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@10160

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

wenzelm@10110

22 
comprehensive 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 TTYbased 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 userinterface 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 cutandpaste and

wenzelm@8508

33 
forwardbackward 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@9849

42 
The easiest way to invoke Proof~General is via the Isabelle interface wrapper

wenzelm@9849

43 
script. The default configuration of Isabelle is smart enough to detect the

wenzelm@9849

44 
Proof~General distribution in several canonical places (e.g.\

wenzelm@9849

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

wenzelm@9849

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

wenzelm@9849

47 
\texttt{ProofGeneral/isar} interface without further ado.\footnote{There is

wenzelm@9849

48 
also a \texttt{ProofGeneral/isa} interface for old tactic scripts written in

wenzelm@9849

49 
ML.} The Isabelle interface script provides several options, just pass

wenzelm@9849

50 
\verb,?, to see its usage.

wenzelm@7981

51 

wenzelm@7175

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

wenzelm@7175

53 
visiting appropriate theory files, e.g.\

wenzelm@7175

54 
\begin{ttbox}

wenzelm@7175

55 
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy

wenzelm@7175

56 
\end{ttbox}

wenzelm@7315

57 
Users of XEmacs may note the tool bar for navigating forward and backward

wenzelm@8516

58 
through the text. Consult the Proof~General documentation \cite{proofgeneral}

wenzelm@8547

59 
for further basic command sequences, such as ``\texttt{Cc Creturn}'' or

wenzelm@8547

60 
``\texttt{Cc u}''.

wenzelm@8508

61 

wenzelm@9849

62 
\medskip

wenzelm@9849

63 

wenzelm@9849

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

wenzelm@9849

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

wenzelm@9849

66 
\begin{ttbox}

wenzelm@9849

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

wenzelm@9849

68 
PROOFGENERAL_OPTIONS=""

wenzelm@9849

69 
\end{ttbox}

wenzelm@9849

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

wenzelm@9849

71 
actual installation directory of Proof~General.

wenzelm@9849

72 

wenzelm@9849

73 
\medskip

wenzelm@9849

74 

wenzelm@9849

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

wenzelm@9849

76 
given by the \texttt{PROOFGENERAL_OPTIONS} setting as well. For example, the

wenzelm@9849

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

wenzelm@9849

78 
\begin{ttbox}

wenzelm@9849

79 
PROOFGENERAL_OPTIONS="p xemacsnomule"

wenzelm@9849

80 
\end{ttbox}

wenzelm@9849

81 

wenzelm@9849

82 
Occasionally, the user's \verb,~/.emacs, file contains material that is

wenzelm@9849

83 
incompatible with the version of Emacs that Proof~General prefers. Then

wenzelm@9849

84 
proper startup may be still achieved by using the \texttt{u false} option.

wenzelm@9849

85 
Also note that any Emacs lisp file called \texttt{proofgeneralsettings.el}

wenzelm@9849

86 
occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}

wenzelm@9849

87 
is automatically loaded by the Proof~General interface script as well.

wenzelm@9849

88 

wenzelm@8843

89 

wenzelm@8843

90 
\subsubsection{The XSymbol package}

wenzelm@8508

91 

wenzelm@8508

92 
Proof~General also supports the Emacs XSymbol package \cite{xsymbol}, which

wenzelm@8508

93 
provides a nice way to get proper mathematical symbols displayed on screen.

wenzelm@8508

94 
Just pass option \texttt{x true} to the Isabelle interface script, or check

wenzelm@8516

95 
the appropriate menu setting by hand. In any case, the XSymbol package must

wenzelm@8516

96 
have been properly installed already.

wenzelm@8516

97 

wenzelm@8843

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

wenzelm@9849

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

wenzelm@9849

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

wenzelm@9849

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

wenzelm@9849

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

wenzelm@8843

103 

wenzelm@8843

104 
\medskip

wenzelm@8843

105 

wenzelm@8843

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

wenzelm@8843

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

wenzelm@10160

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

wenzelm@9849

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

wenzelm@9849

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

wenzelm@9849

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

wenzelm@9849

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

wenzelm@9849

113 
capabilities of XEmacs and XSymbol.

wenzelm@7175

114 

wenzelm@7981

115 

wenzelm@7981

116 
\section{Isabelle/Isar theories}

wenzelm@7981

117 

wenzelm@8547

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

wenzelm@7981

119 
\begin{enumerate}

wenzelm@7981

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

wenzelm@7981

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

wenzelm@7981

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

wenzelm@7981

123 
semiautomated reasoning. Instead of putting together unreadable tactic

wenzelm@7981

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

wenzelm@8508

125 
to usual mathematical practice.

wenzelm@8547

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

wenzelm@8547

127 
developments together with informal text. The resulting hyperlinked PDF

wenzelm@8547

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

wenzelm@8547

129 
copies.

wenzelm@7981

130 
\end{enumerate}

wenzelm@7981

131 

wenzelm@7981

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

wenzelm@7981

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

wenzelm@7981

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

wenzelm@7981

135 
(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as

wenzelm@8547

136 
well, such as HOL's $\isarkeyword{typedef}$ which demands nonemptiness of the

wenzelm@8547

137 
representing sets.

wenzelm@7460

138 

wenzelm@7981

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

wenzelm@7981

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

wenzelm@7981

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

wenzelm@7981

142 
\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelleref}.

wenzelm@7981

143 
Nevertheless, migration between classic Isabelle and Isabelle/Isar is

wenzelm@7981

144 
relatively easy. Thus users may start to benefit from interactive theory

wenzelm@8547

145 
development and document preparation, even before they have any idea of the

wenzelm@8547

146 
Isar proof language at all.

wenzelm@7981

147 

wenzelm@7981

148 
\begin{warn}

wenzelm@8547

149 
Currently, Proof~General does \emph{not} support mixed interactive

wenzelm@7981

150 
development of classic Isabelle theory files or tactic scripts, together

wenzelm@7981

151 
with Isar documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of

wenzelm@7981

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

wenzelm@7981

153 
of these may be active at the same time.

wenzelm@7981

154 
\end{warn}

wenzelm@7981

155 

wenzelm@10160

156 
Conversion of existing tactic scripts is best done by running two separate

wenzelm@7981

157 
Proof~General sessions, one for replaying the old script and the other for the

wenzelm@10160

158 
emerging Isabelle/Isar document. Also note that Isar supports emulation

wenzelm@10160

159 
commands and methods that support traditional tactic scripts within newstyle

wenzelm@10160

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

wenzelm@7981

161 

wenzelm@7167

162 

wenzelm@8843

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

wenzelm@8684

164 

wenzelm@8684

165 
Isabelle/Isar provides a simple document preparation system based on current

wenzelm@8684

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

wenzelm@8684

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

wenzelm@8684

168 
well suited for WWW browsing and as printed copies.

wenzelm@8684

169 

wenzelm@8684

170 
\medskip

wenzelm@8684

171 

wenzelm@8684

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

wenzelm@8684

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

wenzelm@8684

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

wenzelm@8684

175 
\texttt{mkdir} and \texttt{make} tools. Just invoke

wenzelm@8684

176 
\begin{ttbox}

wenzelm@8684

177 
isatool mkdir d Foo

wenzelm@8684

178 
\end{ttbox}

wenzelm@8684

179 
to setup a separate directory for session \texttt{Foo}.\footnote{It is safe to

wenzelm@8684

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

wenzelm@8684

181 
Ensure that \texttt{Foo/ROOT.ML} loads all theories required for this session.

wenzelm@8684

182 
Furthermore \texttt{Foo/document/root.tex} should include any special {\LaTeX}

wenzelm@8684

183 
macro packages required for your document (the default is usually sufficient

wenzelm@8684

184 
as a start).

wenzelm@8684

185 

wenzelm@8684

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

wenzelm@8684

187 
source dependencies only by default). This file is located one level up from

wenzelm@8684

188 
the \texttt{Foo} directory location. At that point just invoke

wenzelm@8684

189 
\begin{ttbox}

wenzelm@8684

190 
isatool make Foo

wenzelm@8684

191 
\end{ttbox}

wenzelm@8684

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

wenzelm@8684

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

wenzelm@8684

194 
the output will appear inside the directory indicated by \texttt{isatool

wenzelm@8684

195 
getenv ISABELLE_BROWSER_INFO}, with the logical session prefix added (e.g.\

wenzelm@8684

196 
\texttt{HOL/Foo}). Note that the \texttt{index.html} located there provides a

wenzelm@8684

197 
link to the finished {\LaTeX} document, too.

wenzelm@8684

198 

wenzelm@8684

199 
Note that this really is batch processing  better let Isabelle check your

wenzelm@8684

200 
theory and proof developments beforehand in interactive mode.

wenzelm@8684

201 

wenzelm@8684

202 
\medskip

wenzelm@8684

203 

wenzelm@8684

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

wenzelm@8684

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

wenzelm@8684

206 
\texttt{dvi} to \texttt{pdf}, or activate the \texttt{D document} option in

wenzelm@8684

207 
order to preserve a copy of the generated {\LaTeX} sources. The latter

wenzelm@8684

208 
feature is very useful for debugging {\LaTeX} errors, while avoiding repeated

wenzelm@8684

209 
runs of Isabelle.

wenzelm@8684

210 

wenzelm@8684

211 
\medskip

wenzelm@8684

212 

wenzelm@8684

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

wenzelm@8684

214 
on Isabelle logic sessions and theory presentation.

wenzelm@8684

215 

wenzelm@8684

216 

wenzelm@10160

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

wenzelm@7167

218 

wenzelm@7297

219 
This is one of the key questions, of course. Isar offers a rather different

wenzelm@7297

220 
approach to formal proof documents than plain old tactic scripts. Experienced

wenzelm@7297

221 
users of existing interactive theorem proving systems may have to learn

wenzelm@7895

222 
thinking differently in order to make effective use of Isabelle/Isar. On the

wenzelm@7297

223 
other hand, Isabelle/Isar comes much closer to existing mathematical practice

wenzelm@7297

224 
of formal proof, so users with less experience in oldstyle tactical proving,

wenzelm@7895

225 
but a good understanding of mathematical proof, might cope with Isar even

wenzelm@10160

226 
better. See also \cite{Wenzel:1999:TPHOL,BauerWenzel:2000:HB} for further

wenzelm@10160

227 
background information on Isar.

wenzelm@7297

228 

wenzelm@10160

229 
\medskip This really is a reference manual on Isabelle/Isar, not a tutorial.

wenzelm@10160

230 
Nevertheless, we will also give some clues of how the concepts introduced here

wenzelm@10160

231 
may be put into practice. Appendix~\ref{ap:refcard} provides a quick

wenzelm@10160

232 
reference card of the most common Isabelle/Isar language elements.

wenzelm@10160

233 
Appendix~\ref{ap:conv} offers some practical hints on converting existing

wenzelm@10160

234 
Isabelle theories and proof scripts to the new format.

wenzelm@10160

235 

wenzelm@10160

236 
Several example applications are distributed with Isabelle, and available via

wenzelm@10160

237 
the Isabelle WWW library as well as the Isabelle/Isar page:

wenzelm@7836

238 
\begin{center}\small

wenzelm@7836

239 
\begin{tabular}{l}

wenzelm@7836

240 
\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\

wenzelm@8516

241 
\url{http://isabelle.in.tum.de/library/} \\[1ex]

wenzelm@8508

242 
\url{http://isabelle.in.tum.de/Isar/} \\

wenzelm@7836

243 
\end{tabular}

wenzelm@7836

244 
\end{center}

wenzelm@7836

245 

wenzelm@10160

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

wenzelm@10160

247 
sources represented in HTML, these Isabelle sessions also provide actual

wenzelm@10160

248 
documents (in PDF).

wenzelm@10160

249 
\begin{itemize}

wenzelm@10160

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

wenzelm@10160

251 
collection of introductory examples.

wenzelm@10160

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

wenzelm@10160

253 
typical mathematicsstyle reasoning in ``axiomatic'' structures.

wenzelm@10160

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

wenzelm@10160

255 
big mathematics application on infinitary vector spaces and functional

wenzelm@10160

256 
analysis.

wenzelm@10160

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

wenzelm@10160

258 
properties of $\lambda$calculus (ChurchRosser and termination). This may

wenzelm@10160

259 
serve as a realistic example of porting of legacy proof scripts into Isar

wenzelm@10160

260 
tactic emulation scripts.

wenzelm@10160

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

wenzelm@10160

262 
formalization of a fragment of Java, together with a corresponding virtual

wenzelm@10160

263 
machine and a specification of its bytecode verifier and a lightweight

wenzelm@10160

264 
bytecode verifier, including proofs of typesafety. This represents a very

wenzelm@10160

265 
``realistic'' example of large formalizations performed in either form of

wenzelm@10160

266 
legacy scripts, tactic emulation scripts, and proper Isar proof texts.

wenzelm@10160

267 
\end{itemize}

wenzelm@8547

268 

wenzelm@7167

269 

wenzelm@7046

270 
%%% Local Variables:

wenzelm@7046

271 
%%% mode: latex

wenzelm@7046

272 
%%% TeXmaster: "isarref"

wenzelm@7046

273 
%%% End:
