7046

1 


2 
\chapter{Introduction}


3 

12618

4 
\section{Overview}


5 


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


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


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


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

12879

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

12618

11 
\cite{isabelleintro,isabelleref}.


12 


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


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


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


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

13039

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

12618

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


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

13039

20 
interactive theory and proof development in this advanced theorem proving


21 
environment.

12618

22 

13039

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


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


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


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

12618

27 
traditions of informal mathematical proof texts and highlevel programming

13039

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


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


30 
audience than unstructured tactic scripts (which typically only provide


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


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


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


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


35 
independently of the mechanic proofchecking process.

12618

36 


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

12879

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

12618

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

12879

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


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

12618

42 

12879

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


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


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


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


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


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


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


50 
gradually converted in due time.

12618

51 


52 

7167

53 
\section{Quick start}


54 

8508

55 
\subsection{Terminal sessions}


56 

12879

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


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


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


60 
anything with Isabelle/Isar is as follows:

7175

61 
\begin{ttbox}


62 
isabelle I HOL\medskip

12879

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

7175

64 
theory Foo = Main:

7297

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


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

7175

67 
end


68 
\end{ttbox}

9233

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

10160

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

10110

71 
comprehensive overview of available commands and other language elements.

7175

72 

8508

73 

8843

74 
\subsection{Proof~General}

8508

75 


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

8547

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

12879

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


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


80 
interface for interactive theorem provers that organizes all the cutandpaste


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


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


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


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


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

7175

86 

8843

87 


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

7167

89 

12879

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

13039

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

12879

92 
Isabelle is smart enough to detect the Proof~General distribution in several


93 
canonical places (e.g.\ \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus


94 
the capital \texttt{Isabelle} executable would already refer to the

9849

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


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

12879

97 
ML.} The Isabelle interface script provides several options; pass \verb,?,


98 
to see its usage.

7981

99 

7175

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


101 
visiting appropriate theory files, e.g.\


102 
\begin{ttbox}

12879

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

7175

104 
\end{ttbox}

13039

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


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

12879

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


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

8508

109 

9849

110 
\medskip


111 


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


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


114 
\begin{ttbox}


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


116 
PROOFGENERAL_OPTIONS=""


117 
\end{ttbox}


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


119 
actual installation directory of Proof~General.


120 


121 
\medskip


122 


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

12879

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


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

9849

126 
\begin{ttbox}


127 
PROOFGENERAL_OPTIONS="p xemacsnomule"


128 
\end{ttbox}


129 

12879

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


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


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


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


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


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

9849

136 

8843

137 


138 
\subsubsection{The XSymbol package}

8508

139 

12879

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


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


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


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


144 
XSymbol package must have been properly installed already.

8516

145 

8843

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

9849

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


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


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


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

8843

151 


152 
\medskip


153 


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


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

10160

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

9849

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


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


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


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

12879

161 
capabilities of Emacs and XSymbol.

7175

162 

7981

163 


164 
\section{Isabelle/Isar theories}


165 

8547

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

7981

167 
\begin{enumerate}

13039

168 

7981

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


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

13039

171 

7981

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


173 
semiautomated reasoning. Instead of putting together unreadable tactic


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

13039

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


176 
as ``improper'' language elements.


177 

8547

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


179 
developments together with informal text. The resulting hyperlinked PDF


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


181 
copies.

13039

182 

7981

183 
\end{enumerate}


184 


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


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


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

12879

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


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


190 
of the representing sets.

7460

191 

7981

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


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


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

13039

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


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


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


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


199 
any idea of the Isar proof language at all.

7981

200 


201 
\begin{warn}

12879

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


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


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

7981

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


206 
of these may be active at the same time.


207 
\end{warn}


208 

12879

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


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


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


212 
emulation commands and methods that support traditional tactic scripts within


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

7981

214 

7167

215 

8843

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

8684

217 

12879

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

13039

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


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


221 
well suited for WWW browsing and as printed copies.

8684

222 


223 
\medskip


224 


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


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


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

12879

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

8684

229 
\begin{ttbox}

12879

230 
isatool mkdir Foo

8684

231 
\end{ttbox}

12879

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


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


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


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


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


237 
default is usually sufficient as a start).

8684

238 

12879

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


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


241 
\texttt{Foo} directory location. Now invoke

8684

242 
\begin{ttbox}


243 
isatool make Foo


244 
\end{ttbox}


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


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

12879

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


248 
reported by the batch job in verbose mode.

8684

249 


250 
\medskip


251 


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


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

13039

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


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

8684

256 


257 
\medskip


258 


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

12879

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


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

8684

262 


263 

10160

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

7167

265 

12879

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


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


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

13039

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

12621

270 

12879

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


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


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


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

13039

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

7297

276 

12879

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


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


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


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


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


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


283 
restructuring proofs).

10160

284 

12879

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


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


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


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


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


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


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


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


293 
Isabelle/Isar theories and proofs.

7836

294 

12879

295 
%FIXME


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


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


298 
% documents (in PDF).


299 
% \begin{itemize}


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


301 
% collection of introductory examples.


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


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


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


305 
% big mathematics application on infinitary vector spaces and functional


306 
% analysis.


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


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

10993

309 

12879

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


311 
% into Isar tactic emulation scripts.


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


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


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


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


316 
% formal model.

10993

317 

12879

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


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


320 
% unstructured scripts are only used for symbolic evaluation.


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


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


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


324 
% bytecode verifier, including proofs of typesafety.

10993

325 

12879

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


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


328 
% \end{itemize}

8547

329 

7167

330 

7046

331 
%%% Local Variables:


332 
%%% mode: latex


333 
%%% TeXmaster: "isarref"


334 
%%% End:
