7046

1 


2 
\chapter{Introduction}


3 

7167

4 
\section{Quick start}


5 

8508

6 
\subsection{Terminal sessions}


7 

7175

8 
Isar is already part of Isabelle (as of version Isabelle99, or later). The

9604

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


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


11 
quickest way to do anything with Isabelle/Isar is as follows:

7175

12 
\begin{ttbox}


13 
isabelle I HOL\medskip

9272

14 
\out{> Welcome to Isabelle/HOL (Isabelle991)}\medskip

7175

15 
theory Foo = Main:

7297

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


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

7175

18 
end


19 
\end{ttbox}

9233

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

10160

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

10110

22 
comprehensive overview of available commands and other language elements.

7175

23 

8508

24 

8843

25 
\subsection{Proof~General}

8508

26 


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

8547

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

8508

29 
demands some better userinterface support. David Aspinall's


30 
\emph{Proof~General}\index{Proof General} environment

8547

31 
\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs interface for


32 
interactive theorem provers that does all the cutandpaste and

8508

33 
forwardbackward walk through the text in a very neat way. In Isabelle/Isar,


34 
the current position within a partial proof document is equally important than


35 
the actual proof state. Thus Proof~General provides the canonical working


36 
environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying

8547

37 
existing Isar documents) and for production work.

7175

38 

8843

39 


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

7167

41 

9849

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


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


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


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


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


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


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


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


50 
\verb,?, to see its usage.

7981

51 

7175

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


53 
visiting appropriate theory files, e.g.\


54 
\begin{ttbox}


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


56 
\end{ttbox}

7315

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

8516

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

8547

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


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

8508

61 

9849

62 
\medskip


63 


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


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


66 
\begin{ttbox}


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


68 
PROOFGENERAL_OPTIONS=""


69 
\end{ttbox}


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


71 
actual installation directory of Proof~General.


72 


73 
\medskip


74 


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


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


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


78 
\begin{ttbox}


79 
PROOFGENERAL_OPTIONS="p xemacsnomule"


80 
\end{ttbox}


81 


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


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


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


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


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


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


88 

8843

89 


90 
\subsubsection{The XSymbol package}

8508

91 


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


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


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

8516

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


96 
have been properly installed already.


97 

8843

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

9849

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


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


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


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

8843

103 


104 
\medskip


105 


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


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

10160

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

9849

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


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


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


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


113 
capabilities of XEmacs and XSymbol.

7175

114 

7981

115 


116 
\section{Isabelle/Isar theories}


117 

8547

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

7981

119 
\begin{enumerate}


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


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


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


123 
semiautomated reasoning. Instead of putting together unreadable tactic


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

8508

125 
to usual mathematical practice.

8547

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


127 
developments together with informal text. The resulting hyperlinked PDF


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


129 
copies.

7981

130 
\end{enumerate}


131 


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


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


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


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

8547

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


137 
representing sets.

7460

138 

7981

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


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


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


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


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


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

8547

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


146 
Isar proof language at all.

7981

147 


148 
\begin{warn}

8547

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

7981

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


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


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


153 
of these may be active at the same time.


154 
\end{warn}


155 

10160

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

7981

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

10160

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


159 
commands and methods that support traditional tactic scripts within newstyle


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

7981

161 

7167

162 

8843

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

8684

164 


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


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


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


168 
well suited for WWW browsing and as printed copies.


169 


170 
\medskip


171 


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


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


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


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


176 
\begin{ttbox}


177 
isatool mkdir d Foo


178 
\end{ttbox}


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


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


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


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


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


184 
as a start).


185 


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


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


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


189 
\begin{ttbox}


190 
isatool make Foo


191 
\end{ttbox}


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


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


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


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


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


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


198 


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


200 
theory and proof developments beforehand in interactive mode.


201 


202 
\medskip


203 


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


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


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


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


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


209 
runs of Isabelle.


210 


211 
\medskip


212 


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


214 
on Isabelle logic sessions and theory presentation.


215 


216 

10160

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

7167

218 

7297

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


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


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

7895

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

7297

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


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

7895

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

10160

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


227 
background information on Isar.

7297

228 

10160

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


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


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


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


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


234 
Isabelle theories and proof scripts to the new format.


235 


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


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

7836

238 
\begin{center}\small


239 
\begin{tabular}{l}


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

8516

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

8508

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

7836

243 
\end{tabular}


244 
\end{center}


245 

10160

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


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


248 
documents (in PDF).


249 
\begin{itemize}


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


251 
collection of introductory examples.


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


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


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


255 
big mathematics application on infinitary vector spaces and functional


256 
analysis.


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


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


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


260 
tactic emulation scripts.


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


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


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


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


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


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


267 
\end{itemize}

8547

268 

7167

269 

7046

270 
%%% Local Variables:


271 
%%% mode: latex


272 
%%% TeXmaster: "isarref"


273 
%%% End:
