wenzelm@12668

1 
\chapter{The Basics}

nipkow@8743

2 

nipkow@8743

3 
\section{Introduction}

nipkow@8743

4 

paulson@11405

5 
This book is a tutorial on how to use the theorem prover Isabelle/HOL as a

paulson@11405

6 
specification and verification system. Isabelle is a generic system for

paulson@11405

7 
implementing logical formalisms, and Isabelle/HOL is the specialization

paulson@11405

8 
of Isabelle for HOL, which abbreviates HigherOrder Logic. We introduce

paulson@11405

9 
HOL step by step following the equation

nipkow@8743

10 
\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]

paulson@11456

11 
We do not assume that you are familiar with mathematical logic.

paulson@11456

12 
However, we do assume that

paulson@11456

13 
you are used to logical and set theoretic notation, as covered

paulson@11456

14 
in a good discrete mathematics course~\cite{RosenDMA}, and

paulson@11450

15 
that you are familiar with the basic concepts of functional

nipkow@11209

16 
programming~\cite{BirdHaskell,HudakHaskell,paulsonml2,ThompsonHaskell}.

nipkow@11209

17 
Although this tutorial initially concentrates on functional programming, do

nipkow@11209

18 
not be misled: HOL can express most mathematical concepts, and functional

nipkow@11209

19 
programming is just one particularly simple and ubiquitous instance.

nipkow@8743

20 

nipkow@11205

21 
Isabelle~\cite{paulsonisabook} is implemented in ML~\cite{SML}. This has

nipkow@11205

22 
influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant

paulson@11450

23 
for us: this tutorial is based on

nipkow@11213

24 
Isabelle/Isar~\cite{isabelleisarref}, an extension of Isabelle which hides

nipkow@11213

25 
the implementation language almost completely. Thus the full name of the

nipkow@11213

26 
system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.

nipkow@11213

27 

nipkow@11213

28 
There are other implementations of HOL, in particular the one by Mike Gordon

paulson@11450

29 
\index{Gordon, Mike}%

nipkow@11213

30 
\emph{et al.}, which is usually referred to as ``the HOL system''

nipkow@11213

31 
\cite{mgordonhol}. For us, HOL refers to the logical system, and sometimes

paulson@11450

32 
its incarnation Isabelle/HOL\@.

nipkow@8743

33 

nipkow@8743

34 
A tutorial is by definition incomplete. Currently the tutorial only

nipkow@8743

35 
introduces the rudiments of Isar's proof language. To fully exploit the power

nipkow@11213

36 
of Isar, in particular the ability to write readable and structured proofs,

nipkow@15429

37 
you should start with Nipkow's overview~\cite{NipkowTYPES02} and consult

nipkow@15429

38 
the Isabelle/Isar Reference Manual~\cite{isabelleisarref} and Wenzel's

nipkow@15429

39 
PhD thesis~\cite{WenzelPhD} (which discusses many proof patterns)

nipkow@15429

40 
for further details. If you want to use Isabelle's ML level

nipkow@8743

41 
directly (for example for writing your own proof procedures) see the Isabelle

nipkow@8743

42 
Reference Manual~\cite{isabelleref}; for details relating to HOL see the

nipkow@8743

43 
Isabelle/HOL manual~\cite{isabelleHOL}. All manuals have a comprehensive

nipkow@8743

44 
index.

nipkow@8743

45 

nipkow@8743

46 
\section{Theories}

nipkow@8743

47 
\label{sec:Basic:Theories}

nipkow@8743

48 

paulson@11428

49 
\index{theories(}%

nipkow@8743

50 
Working with Isabelle means creating theories. Roughly speaking, a

paulson@11428

51 
\textbf{theory} is a named collection of types, functions, and theorems,

nipkow@8743

52 
much like a module in a programming language or a specification in a

nipkow@8743

53 
specification language. In fact, theories in HOL can be either. The general

nipkow@8743

54 
format of a theory \texttt{T} is

nipkow@8743

55 
\begin{ttbox}

nipkow@15136

56 
theory T

nipkow@15141

57 
imports B\(@1\) \(\ldots\) B\(@n\)

nipkow@15136

58 
begin

paulson@11450

59 
{\rmfamily\textit{declarations, definitions, and proofs}}

nipkow@8743

60 
end

nipkow@15358

61 
\end{ttbox}\cmmdx{theory}\cmmdx{imports}

nipkow@15136

62 
where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing

paulson@11450

63 
theories that \texttt{T} is based on and \textit{declarations,

paulson@11450

64 
definitions, and proofs} represents the newly introduced concepts

nipkow@8771

65 
(types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the

paulson@11450

66 
direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@.

paulson@11450

67 
Everything defined in the parent theories (and their parents, recursively) is

nipkow@8743

68 
automatically visible. To avoid name clashes, identifiers can be

paulson@11450

69 
\textbf{qualified}\indexbold{identifiers!qualified}

paulson@11450

70 
by theory names as in \texttt{T.f} and~\texttt{B.f}.

paulson@11450

71 
Each theory \texttt{T} must

paulson@11428

72 
reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}.

nipkow@8743

73 

nipkow@8743

74 
This tutorial is concerned with introducing you to the different linguistic

paulson@11450

75 
constructs that can fill the \textit{declarations, definitions, and

paulson@11450

76 
proofs} above. A complete grammar of the basic

nipkow@12327

77 
constructs is found in the Isabelle/Isar Reference

nipkow@12327

78 
Manual~\cite{isabelleisarref}.

nipkow@8743

79 

nipkow@8743

80 
\begin{warn}

paulson@11428

81 
HOL contains a theory \thydx{Main}, the union of all the basic

paulson@10885

82 
predefined theories like arithmetic, lists, sets, etc.

paulson@10885

83 
Unless you know what you are doing, always include \isa{Main}

nipkow@10971

84 
as a direct or indirect parent of all your theories.

nipkow@12332

85 
\end{warn}

nipkow@16306

86 
HOL's theory collection is available online at

nipkow@16306

87 
\begin{center}\small

nipkow@16306

88 
\url{http://isabelle.in.tum.de/library/HOL/}

nipkow@16306

89 
\end{center}

nipkow@16359

90 
and is recommended browsing. In subdirectory \texttt{Library} you find

nipkow@16359

91 
a growing library of useful theories that are not part of \isa{Main}

nipkow@16359

92 
but can be included among the parents of a theory and will then be

nipkow@16359

93 
loaded automatically.

nipkow@16306

94 

nipkow@16306

95 
For the more adventurous, there is the \emph{Archive of Formal Proofs},

nipkow@16306

96 
a journallike collection of more advanced Isabelle theories:

nipkow@16306

97 
\begin{center}\small

nipkow@16306

98 
\url{http://afp.sourceforge.net/}

nipkow@16306

99 
\end{center}

nipkow@16306

100 
We hope that you will contribute to it yourself one day.%

paulson@11428

101 
\index{theories)}

nipkow@8743

102 

nipkow@8743

103 

paulson@10885

104 
\section{Types, Terms and Formulae}

nipkow@8743

105 
\label{sec:TypesTermsForms}

nipkow@8743

106 

paulson@10795

107 
Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed

nipkow@8771

108 
logic whose type system resembles that of functional programming languages

paulson@11450

109 
like ML or Haskell. Thus there are

paulson@11450

110 
\index{types(}

nipkow@8743

111 
\begin{description}

paulson@11450

112 
\item[base types,]

paulson@11450

113 
in particular \tydx{bool}, the type of truth values,

paulson@11428

114 
and \tydx{nat}, the type of natural numbers.

paulson@11450

115 
\item[type constructors,]\index{type constructors}

paulson@11450

116 
in particular \tydx{list}, the type of

paulson@11428

117 
lists, and \tydx{set}, the type of sets. Type constructors are written

nipkow@8771

118 
postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are

nipkow@8743

119 
natural numbers. Parentheses around single arguments can be dropped (as in

nipkow@8771

120 
\isa{nat list}), multiple arguments are separated by commas (as in

nipkow@8771

121 
\isa{(bool,nat)ty}).

paulson@11450

122 
\item[function types,]\index{function types}

paulson@11450

123 
denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.

nipkow@8771

124 
In HOL \isasymFun\ represents \emph{total} functions only. As is customary,

nipkow@8771

125 
\isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means

nipkow@8771

126 
\isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also

nipkow@8771

127 
supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}

nipkow@8771

128 
which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$

nipkow@8743

129 
\isasymFun~$\tau$}.

paulson@11450

130 
\item[type variables,]\index{type variables}\index{variables!type}

paulson@10795

131 
denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise

nipkow@8771

132 
to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity

nipkow@8771

133 
function.

nipkow@8743

134 
\end{description}

nipkow@8743

135 
\begin{warn}

nipkow@8743

136 
Types are extremely important because they prevent us from writing

nipkow@16359

137 
nonsense. Isabelle insists that all terms and formulae must be

nipkow@16359

138 
welltyped and will print an error message if a type mismatch is

nipkow@16359

139 
encountered. To reduce the amount of explicit type information that

nipkow@16359

140 
needs to be provided by the user, Isabelle infers the type of all

nipkow@16359

141 
variables automatically (this is called \bfindex{type inference})

nipkow@16359

142 
and keeps quiet about it. Occasionally this may lead to

nipkow@16359

143 
misunderstandings between you and the system. If anything strange

nipkow@16359

144 
happens, we recommend that you ask Isabelle to display all type

nipkow@16359

145 
information via the Proof General menu item \textsf{Isabelle} $>$

nipkow@16359

146 
\textsf{Settings} $>$ \textsf{Show Types} (see \S\ref{sec:interface}

nipkow@16359

147 
for details).

paulson@11450

148 
\end{warn}%

paulson@11450

149 
\index{types)}

nipkow@8743

150 

nipkow@8743

151 

paulson@11450

152 
\index{terms(}

paulson@11450

153 
\textbf{Terms} are formed as in functional programming by

nipkow@8771

154 
applying functions to arguments. If \isa{f} is a function of type

nipkow@8771

155 
\isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type

nipkow@8771

156 
$\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports

nipkow@8771

157 
infix functions like \isa{+} and some basic constructs from functional

paulson@11428

158 
programming, such as conditional expressions:

nipkow@8743

159 
\begin{description}

paulson@11450

160 
\item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}

paulson@11428

161 
Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.

paulson@11450

162 
\item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}

nipkow@13814

163 
is equivalent to $u$ where all free occurrences of $x$ have been replaced by

nipkow@8743

164 
$t$. For example,

nipkow@8771

165 
\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated

nipkow@13814

166 
by semicolons: \isa{let $x@1$ = $t@1$;\dots; $x@n$ = $t@n$ in $u$}.

nipkow@8771

167 
\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ ~\dots~ $c@n$ \isasymFun~$e@n$}]

paulson@11450

168 
\index{*case expressions}

nipkow@8771

169 
evaluates to $e@i$ if $e$ is of the form $c@i$.

nipkow@8743

170 
\end{description}

nipkow@8743

171 

nipkow@8743

172 
Terms may also contain

paulson@11450

173 
\isasymlambdaabstractions.\index{lambda@$\lambda$ expressions}

paulson@11450

174 
For example,

nipkow@8771

175 
\isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and

nipkow@8771

176 
returns \isa{x+1}. Instead of

nipkow@8771

177 
\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write

paulson@11450

178 
\isa{\isasymlambda{}x~y~z.~$t$}.%

paulson@11450

179 
\index{terms)}

nipkow@8743

180 

paulson@11450

181 
\index{formulae(}%

paulson@11450

182 
\textbf{Formulae} are terms of type \tydx{bool}.

paulson@11428

183 
There are the basic constants \cdx{True} and \cdx{False} and

nipkow@8771

184 
the usual logical connectives (in decreasing order of priority):

paulson@11420

185 
\indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},

paulson@11420

186 
\indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},

nipkow@8743

187 
all of which (except the unary \isasymnot) associate to the right. In

nipkow@8771

188 
particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B

nipkow@8771

189 
\isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B

nipkow@8771

190 
\isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).

nipkow@8743

191 

paulson@11450

192 
Equality\index{equality} is available in the form of the infix function

paulson@11450

193 
\isa{=} of type \isa{'a \isasymFun~'a

nipkow@8771

194 
\isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$

paulson@11450

195 
and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type

paulson@11450

196 
\isa{bool} then \isa{=} acts as \rmindex{ifandonlyif}.

paulson@11450

197 
The formula

nipkow@8771

198 
\isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for

nipkow@8771

199 
\isa{\isasymnot($t@1$ = $t@2$)}.

nipkow@8743

200 

paulson@11450

201 
Quantifiers\index{quantifiers} are written as

paulson@11450

202 
\isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}.

paulson@11420

203 
There is even

paulson@11450

204 
\isa{\isasymuniqex{}x.~$P$}, which

paulson@11420

205 
means that there exists exactly one \isa{x} that satisfies \isa{$P$}.

paulson@11420

206 
Nested quantifications can be abbreviated:

paulson@11420

207 
\isa{\isasymforall{}x~y~z.~$P$} means

paulson@11450

208 
\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.%

paulson@11450

209 
\index{formulae)}

nipkow@8743

210 

nipkow@8743

211 
Despite type inference, it is sometimes necessary to attach explicit

paulson@11428

212 
\bfindex{type constraints} to a term. The syntax is

nipkow@8771

213 
\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that

nipkow@10538

214 
\ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed

paulson@11450

215 
in parentheses. For instance,

paulson@11450

216 
\isa{x < y::nat} is illtyped because it is interpreted as

paulson@11450

217 
\isa{(x < y)::nat}. Type constraints may be needed to disambiguate

paulson@11450

218 
expressions

paulson@11450

219 
involving overloaded functions such as~\isa{+},

paulson@11450

220 
\isa{*} and~\isa{<}. Section~\ref{sec:overloading}

paulson@11450

221 
discusses overloading, while Table~\ref{tab:overloading} presents the most

nipkow@10695

222 
important overloaded function symbols.

nipkow@8743

223 

paulson@11450

224 
In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of

paulson@11450

225 
functional programming and mathematics. Here are the main rules that you

paulson@11450

226 
should be familiar with to avoid certain syntactic traps:

nipkow@8743

227 
\begin{itemize}

nipkow@8743

228 
\item

nipkow@8771

229 
Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!

nipkow@8743

230 
\item

nipkow@8771

231 
Isabelle allows infix functions like \isa{+}. The prefix form of function

nipkow@8771

232 
application binds more strongly than anything else and hence \isa{f~x + y}

nipkow@8771

233 
means \isa{(f~x)~+~y} and not \isa{f(x+y)}.

nipkow@8743

234 
\item Remember that in HOL ifandonlyif is expressed using equality. But

nipkow@8743

235 
equality has a high priority, as befitting a relation, while ifandonlyif

nipkow@8771

236 
typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P =

nipkow@8771

237 
P} means \isa{\isasymnot\isasymnot(P = P)} and not

nipkow@8771

238 
\isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean

nipkow@8771

239 
logical equivalence, enclose both operands in parentheses, as in \isa{(A

nipkow@8743

240 
\isasymand~B) = (B \isasymand~A)}.

nipkow@8743

241 
\item

nipkow@8743

242 
Constructs with an opening but without a closing delimiter bind very weakly

nipkow@8743

243 
and should therefore be enclosed in parentheses if they appear in subterms, as

paulson@11450

244 
in \isa{(\isasymlambda{}x.~x) = f}. This includes

paulson@11450

245 
\isa{if},\index{*if expressions}

paulson@11450

246 
\isa{let},\index{*let expressions}

paulson@11450

247 
\isa{case},\index{*case expressions}

paulson@11450

248 
\isa{\isasymlambda}, and quantifiers.

nipkow@8743

249 
\item

nipkow@8771

250 
Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}

nipkow@12327

251 
because \isa{x.x} is always taken as a single qualified identifier. Write

nipkow@8771

252 
\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.

paulson@11450

253 
\item Identifiers\indexbold{identifiers} may contain the characters \isa{_}

nipkow@12327

254 
and~\isa{'}, except at the beginning.

nipkow@8743

255 
\end{itemize}

nipkow@8743

256 

paulson@11450

257 
For the sake of readability, we use the usual mathematical symbols throughout

nipkow@10983

258 
the tutorial. Their \textsc{ascii}equivalents are shown in table~\ref{tab:ascii} in

nipkow@8771

259 
the appendix.

nipkow@8771

260 

paulson@11450

261 
\begin{warn}

nipkow@16359

262 
A particular problem for novices can be the priority of operators. If

nipkow@16359

263 
you are unsure, use additional parentheses. In those cases where

nipkow@16359

264 
Isabelle echoes your input, you can see which parentheses are dropped

nipkow@16359

265 
 they were superfluous. If you are unsure how to interpret

nipkow@16359

266 
Isabelle's output because you don't know where the (dropped)

nipkow@16359

267 
parentheses go, set the Proof General flag \textsf{Isabelle} $>$

nipkow@16359

268 
\textsf{Settings} $>$ \textsf{Show Brackets} (see \S\ref{sec:interface}).

paulson@11450

269 
\end{warn}

paulson@11450

270 

nipkow@8743

271 

nipkow@8743

272 
\section{Variables}

nipkow@8743

273 
\label{sec:variables}

paulson@11450

274 
\index{variables(}

nipkow@8743

275 

paulson@11450

276 
Isabelle distinguishes free and bound variables, as is customary. Bound

nipkow@8743

277 
variables are automatically renamed to avoid clashes with free variables. In

paulson@11428

278 
addition, Isabelle has a third kind of variable, called a \textbf{schematic

paulson@11428

279 
variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns},

nipkow@13439

280 
which must have a~\isa{?} as its first character.

paulson@11428

281 
Logically, an unknown is a free variable. But it may be

nipkow@8743

282 
instantiated by another term during the proof process. For example, the

nipkow@8771

283 
mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},

nipkow@8743

284 
which means that Isabelle can instantiate it arbitrarily. This is in contrast

nipkow@8743

285 
to ordinary variables, which remain fixed. The programming language Prolog

nipkow@8743

286 
calls unknowns {\em logical\/} variables.

nipkow@8743

287 

nipkow@8743

288 
Most of the time you can and should ignore unknowns and work with ordinary

nipkow@8743

289 
variables. Just don't be surprised that after you have finished the proof of

paulson@11450

290 
a theorem, Isabelle will turn your free variables into unknowns. It

nipkow@8743

291 
indicates that Isabelle will automatically instantiate those unknowns

nipkow@8743

292 
suitably when the theorem is used in some other proof.

nipkow@9689

293 
Note that for readability we often drop the \isa{?}s when displaying a theorem.

nipkow@8743

294 
\begin{warn}

paulson@11450

295 
For historical reasons, Isabelle accepts \isa{?} as an ASCII representation

paulson@11450

296 
of the \(\exists\) symbol. However, the \isa{?} character must then be followed

paulson@11450

297 
by a space, as in \isa{?~x. f(x) = 0}. Otherwise, \isa{?x} is

paulson@11450

298 
interpreted as a schematic variable. The preferred ASCII representation of

paulson@11450

299 
the \(\exists\) symbol is \isa{EX}\@.

paulson@11450

300 
\end{warn}%

paulson@11450

301 
\index{variables)}

nipkow@8743

302 

paulson@10885

303 
\section{Interaction and Interfaces}

nipkow@16306

304 
\label{sec:interface}

nipkow@8771

305 

nipkow@16359

306 
The recommended interface for Isabelle/Isar is the (X)Emacsbased

nipkow@16359

307 
\bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}.

nipkow@16359

308 
Interaction with Isabelle at the shell level, although possible,

nipkow@16359

309 
should be avoided. Most of the tutorial is independent of the

nipkow@16359

310 
interface and is phrased in a neutral language. For example, the

nipkow@16359

311 
phrase ``to abandon a proof'' corresponds to the obvious

nipkow@16359

312 
action of clicking on the \textsf{Undo} symbol in Proof General.

nipkow@16359

313 
Proof General specific information is often displayed in paragraphs

nipkow@16359

314 
identified by a miniature Proof General icon. Here are two examples:

nipkow@16359

315 
\begin{pgnote}

nipkow@16359

316 
Proof General supports a special font with mathematical symbols known

nipkow@16359

317 
as ``xsymbols''. All symbols have \textsc{ascii}equivalents: for

nipkow@16359

318 
example, you can enter either \verb!&! or \verb!\<and>! to obtain

nipkow@16359

319 
$\land$. For a list of the most frequent symbols see table~\ref{tab:ascii}

nipkow@16359

320 
in the appendix.

nipkow@8771

321 

nipkow@16359

322 
Note that by default xsymbols are not enabled. You have to switch

nipkow@16359

323 
them on via the menu item \textsf{ProofGeneral} $>$ \textsf{Options} $>$

nipkow@16359

324 
\textsf{XSymbols} (and save the option via the toplevel

nipkow@16359

325 
\textsf{Options} menu).

nipkow@16306

326 
\end{pgnote}

nipkow@8771

327 

nipkow@16306

328 
\begin{pgnote}

nipkow@16359

329 
Proof General offers the \textsf{Isabelle} menu for displaying

nipkow@16359

330 
information and setting flags. A particularly useful flag is

nipkow@16359

331 
\textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Show Types} which

nipkow@16359

332 
causes Isabelle to output the type information that is usually

nipkow@16306

333 
suppressed. This is indispensible in case of errors of all kinds

nipkow@16359

334 
because often the types reveal the source of the problem. Once you

nipkow@16359

335 
have diagnosed the problem you may no longer want to see the types

nipkow@16359

336 
because they clutter all output. Simply reset the flag.

nipkow@16306

337 
\end{pgnote}

nipkow@8771

338 

paulson@10885

339 
\section{Getting Started}

nipkow@8743

340 

nipkow@16359

341 
Assuming you have installed Isabelle and Proof General, you start it by typing

nipkow@16359

342 
\texttt{Isabelle} in a shell window. This launches a Proof General window.

nipkow@16359

343 
By default, you are in HOL\footnote{This is controlled by the

nipkow@16359

344 
\texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual}

nipkow@16359

345 
for more details.}.

nipkow@16359

346 

nipkow@16359

347 
\begin{pgnote}

nipkow@16359

348 
You can choose a different logic via the \textsf{Isabelle} $>$

nipkow@16359

349 
\textsf{Logics} menu. For example, you may want to work in the real

nipkow@16359

350 
numbers, an extension of HOL (see \S\ref{sec:real}).

nipkow@16359

351 
% This is just excess baggage:

nipkow@16359

352 
%(You have to restart Proof General if you only compile the new logic

nipkow@16359

353 
%after having launching Proof General already).

nipkow@16359

354 
\end{pgnote}
