doc-src/TutorialI/basics.tex
author nipkow
Wed Jun 22 09:26:18 2005 +0200 (2005-06-22)
changeset 16523 f8a734dc0fbc
parent 16359 af7239e3054d
child 38432 439f50a241c1
permissions -rw-r--r--
*** empty log message ***
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 Higher-Order 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{Rosen-DMA}, and
paulson@11450
    15
that you are familiar with the basic concepts of functional
nipkow@11209
    16
programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
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{paulson-isa-book} 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{isabelle-isar-ref}, 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{mgordon-hol}. 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{Nipkow-TYPES02} and consult
nipkow@15429
    38
the Isabelle/Isar Reference Manual~\cite{isabelle-isar-ref} and Wenzel's
nipkow@15429
    39
PhD thesis~\cite{Wenzel-PhD} (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{isabelle-ref}; for details relating to HOL see the
nipkow@8743
    43
Isabelle/HOL manual~\cite{isabelle-HOL}. 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{isabelle-isar-ref}.
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 journal-like 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
  well-typed 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@16523
   145
  information via the Proof General menu item \pgmenu{Isabelle} $>$
nipkow@16523
   146
  \pgmenu{Settings} $>$ \pgmenu{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
\isasymlambda-abstractions.\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{if-and-only-if}.
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 ill-typed 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 if-and-only-if is expressed using equality.  But
nipkow@8743
   235
  equality has a high priority, as befitting a relation, while if-and-only-if
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@16523
   267
parentheses go, set the Proof General flag \pgmenu{Isabelle} $>$
nipkow@16523
   268
\pgmenu{Settings} $>$ \pgmenu{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)Emacs-based
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@16523
   312
action of clicking on the \pgmenu{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 ``x-symbols''. 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 x-symbols are not enabled. You have to switch
nipkow@16523
   323
them on via the menu item \pgmenu{Proof-General} $>$ \pgmenu{Options} $>$
nipkow@16523
   324
\pgmenu{X-Symbols} (and save the option via the top-level
nipkow@16523
   325
\pgmenu{Options} menu).
nipkow@16306
   326
\end{pgnote}
nipkow@8771
   327
nipkow@16306
   328
\begin{pgnote}
nipkow@16523
   329
Proof General offers the \pgmenu{Isabelle} menu for displaying
nipkow@16359
   330
information and setting flags. A particularly useful flag is
nipkow@16523
   331
\pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgdx{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@16523
   348
You can choose a different logic via the \pgmenu{Isabelle} $>$
nipkow@16523
   349
\pgmenu{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
\end{pgnote}