doc-src/TutorialI/basics.tex
author nipkow
Mon Jun 06 21:20:54 2005 +0200 (2005-06-06)
changeset 16306 8117e2037d3b
parent 15429 b08a5eaf22e3
child 16359 af7239e3054d
permissions -rw-r--r--
updating...
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@16306
    90
and is recommended browsing.
nipkow@12473
    91
There is also a growing Library~\cite{HOL-Library}\index{Library}
nipkow@13814
    92
of useful theories that are not part of \isa{Main} but can be included
nipkow@16306
    93
among the parents of a theory and will then be 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@8743
   137
  nonsense.  Isabelle insists that all terms and formulae must be well-typed
nipkow@8743
   138
  and will print an error message if a type mismatch is encountered. To
nipkow@8743
   139
  reduce the amount of explicit type information that needs to be provided by
nipkow@8743
   140
  the user, Isabelle infers the type of all variables automatically (this is
nipkow@8743
   141
  called \bfindex{type inference}) and keeps quiet about it. Occasionally
nipkow@8743
   142
  this may lead to misunderstandings between you and the system. If anything
nipkow@16306
   143
  strange happens, we recommend that you ask Isabelle to display all type
nipkow@16306
   144
  information. This is best done through the Proof General interface; see
nipkow@16306
   145
  \S\ref{sec:interface} for details.
paulson@11450
   146
\end{warn}%
paulson@11450
   147
\index{types|)}
nipkow@8743
   148
nipkow@8743
   149
paulson@11450
   150
\index{terms|(}
paulson@11450
   151
\textbf{Terms} are formed as in functional programming by
nipkow@8771
   152
applying functions to arguments. If \isa{f} is a function of type
nipkow@8771
   153
\isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
nipkow@8771
   154
$\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
nipkow@8771
   155
infix functions like \isa{+} and some basic constructs from functional
paulson@11428
   156
programming, such as conditional expressions:
nipkow@8743
   157
\begin{description}
paulson@11450
   158
\item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}
paulson@11428
   159
Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
paulson@11450
   160
\item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}
nipkow@13814
   161
is equivalent to $u$ where all free occurrences of $x$ have been replaced by
nipkow@8743
   162
$t$. For example,
nipkow@8771
   163
\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
nipkow@13814
   164
by semicolons: \isa{let $x@1$ = $t@1$;\dots; $x@n$ = $t@n$ in $u$}.
nipkow@8771
   165
\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
paulson@11450
   166
\index{*case expressions}
nipkow@8771
   167
evaluates to $e@i$ if $e$ is of the form $c@i$.
nipkow@8743
   168
\end{description}
nipkow@8743
   169
nipkow@8743
   170
Terms may also contain
paulson@11450
   171
\isasymlambda-abstractions.\index{lambda@$\lambda$ expressions}
paulson@11450
   172
For example,
nipkow@8771
   173
\isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
nipkow@8771
   174
returns \isa{x+1}. Instead of
nipkow@8771
   175
\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
paulson@11450
   176
\isa{\isasymlambda{}x~y~z.~$t$}.%
paulson@11450
   177
\index{terms|)}
nipkow@8743
   178
paulson@11450
   179
\index{formulae|(}%
paulson@11450
   180
\textbf{Formulae} are terms of type \tydx{bool}.
paulson@11428
   181
There are the basic constants \cdx{True} and \cdx{False} and
nipkow@8771
   182
the usual logical connectives (in decreasing order of priority):
paulson@11420
   183
\indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
paulson@11420
   184
\indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
nipkow@8743
   185
all of which (except the unary \isasymnot) associate to the right. In
nipkow@8771
   186
particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
nipkow@8771
   187
  \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
nipkow@8771
   188
  \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
nipkow@8743
   189
paulson@11450
   190
Equality\index{equality} is available in the form of the infix function
paulson@11450
   191
\isa{=} of type \isa{'a \isasymFun~'a
nipkow@8771
   192
  \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
paulson@11450
   193
and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type
paulson@11450
   194
\isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}.
paulson@11450
   195
The formula
nipkow@8771
   196
\isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
nipkow@8771
   197
\isa{\isasymnot($t@1$ = $t@2$)}.
nipkow@8743
   198
paulson@11450
   199
Quantifiers\index{quantifiers} are written as
paulson@11450
   200
\isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}. 
paulson@11420
   201
There is even
paulson@11450
   202
\isa{\isasymuniqex{}x.~$P$}, which
paulson@11420
   203
means that there exists exactly one \isa{x} that satisfies \isa{$P$}. 
paulson@11420
   204
Nested quantifications can be abbreviated:
paulson@11420
   205
\isa{\isasymforall{}x~y~z.~$P$} means
paulson@11450
   206
\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.%
paulson@11450
   207
\index{formulae|)}
nipkow@8743
   208
nipkow@8743
   209
Despite type inference, it is sometimes necessary to attach explicit
paulson@11428
   210
\bfindex{type constraints} to a term.  The syntax is
nipkow@8771
   211
\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
nipkow@10538
   212
\ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
paulson@11450
   213
in parentheses.  For instance,
paulson@11450
   214
\isa{x < y::nat} is ill-typed because it is interpreted as
paulson@11450
   215
\isa{(x < y)::nat}.  Type constraints may be needed to disambiguate
paulson@11450
   216
expressions
paulson@11450
   217
involving overloaded functions such as~\isa{+}, 
paulson@11450
   218
\isa{*} and~\isa{<}.  Section~\ref{sec:overloading} 
paulson@11450
   219
discusses overloading, while Table~\ref{tab:overloading} presents the most
nipkow@10695
   220
important overloaded function symbols.
nipkow@8743
   221
paulson@11450
   222
In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of
paulson@11450
   223
functional programming and mathematics.  Here are the main rules that you
paulson@11450
   224
should be familiar with to avoid certain syntactic traps:
nipkow@8743
   225
\begin{itemize}
nipkow@8743
   226
\item
nipkow@8771
   227
Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
nipkow@8743
   228
\item
nipkow@8771
   229
Isabelle allows infix functions like \isa{+}. The prefix form of function
nipkow@8771
   230
application binds more strongly than anything else and hence \isa{f~x + y}
nipkow@8771
   231
means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
nipkow@8743
   232
\item Remember that in HOL if-and-only-if is expressed using equality.  But
nipkow@8743
   233
  equality has a high priority, as befitting a relation, while if-and-only-if
nipkow@8771
   234
  typically has the lowest priority.  Thus, \isa{\isasymnot~\isasymnot~P =
nipkow@8771
   235
    P} means \isa{\isasymnot\isasymnot(P = P)} and not
nipkow@8771
   236
  \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
nipkow@8771
   237
  logical equivalence, enclose both operands in parentheses, as in \isa{(A
nipkow@8743
   238
    \isasymand~B) = (B \isasymand~A)}.
nipkow@8743
   239
\item
nipkow@8743
   240
Constructs with an opening but without a closing delimiter bind very weakly
nipkow@8743
   241
and should therefore be enclosed in parentheses if they appear in subterms, as
paulson@11450
   242
in \isa{(\isasymlambda{}x.~x) = f}.  This includes 
paulson@11450
   243
\isa{if},\index{*if expressions}
paulson@11450
   244
\isa{let},\index{*let expressions}
paulson@11450
   245
\isa{case},\index{*case expressions}
paulson@11450
   246
\isa{\isasymlambda}, and quantifiers.
nipkow@8743
   247
\item
nipkow@8771
   248
Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
nipkow@12327
   249
because \isa{x.x} is always taken as a single qualified identifier. Write
nipkow@8771
   250
\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
paulson@11450
   251
\item Identifiers\indexbold{identifiers} may contain the characters \isa{_} 
nipkow@12327
   252
and~\isa{'}, except at the beginning.
nipkow@8743
   253
\end{itemize}
nipkow@8743
   254
paulson@11450
   255
For the sake of readability, we use the usual mathematical symbols throughout
nipkow@10983
   256
the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
nipkow@8771
   257
the appendix.
nipkow@8771
   258
paulson@11450
   259
\begin{warn}
paulson@11450
   260
A particular
paulson@11450
   261
problem for novices can be the priority of operators. If you are unsure, use
paulson@11450
   262
additional parentheses. In those cases where Isabelle echoes your
paulson@11450
   263
input, you can see which parentheses are dropped --- they were superfluous. If
paulson@11450
   264
you are unsure how to interpret Isabelle's output because you don't know
paulson@11450
   265
where the (dropped) parentheses go, set the flag\index{flags}
paulson@11450
   266
\isa{show_brackets}\index{*show_brackets (flag)}:
paulson@11450
   267
\begin{ttbox}
paulson@11450
   268
ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
paulson@11450
   269
\end{ttbox}
paulson@11450
   270
\end{warn}
paulson@11450
   271
nipkow@8743
   272
nipkow@8743
   273
\section{Variables}
nipkow@8743
   274
\label{sec:variables}
paulson@11450
   275
\index{variables|(}
nipkow@8743
   276
paulson@11450
   277
Isabelle distinguishes free and bound variables, as is customary. Bound
nipkow@8743
   278
variables are automatically renamed to avoid clashes with free variables. In
paulson@11428
   279
addition, Isabelle has a third kind of variable, called a \textbf{schematic
paulson@11428
   280
  variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns}, 
nipkow@13439
   281
which must have a~\isa{?} as its first character.  
paulson@11428
   282
Logically, an unknown is a free variable. But it may be
nipkow@8743
   283
instantiated by another term during the proof process. For example, the
nipkow@8771
   284
mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
nipkow@8743
   285
which means that Isabelle can instantiate it arbitrarily. This is in contrast
nipkow@8743
   286
to ordinary variables, which remain fixed. The programming language Prolog
nipkow@8743
   287
calls unknowns {\em logical\/} variables.
nipkow@8743
   288
nipkow@8743
   289
Most of the time you can and should ignore unknowns and work with ordinary
nipkow@8743
   290
variables. Just don't be surprised that after you have finished the proof of
paulson@11450
   291
a theorem, Isabelle will turn your free variables into unknowns.  It
nipkow@8743
   292
indicates that Isabelle will automatically instantiate those unknowns
nipkow@8743
   293
suitably when the theorem is used in some other proof.
nipkow@9689
   294
Note that for readability we often drop the \isa{?}s when displaying a theorem.
nipkow@8743
   295
\begin{warn}
paulson@11450
   296
  For historical reasons, Isabelle accepts \isa{?} as an ASCII representation
paulson@11450
   297
  of the \(\exists\) symbol.  However, the \isa{?} character must then be followed
paulson@11450
   298
  by a space, as in \isa{?~x. f(x) = 0}.  Otherwise, \isa{?x} is
paulson@11450
   299
  interpreted as a schematic variable.  The preferred ASCII representation of
paulson@11450
   300
  the \(\exists\) symbol is \isa{EX}\@. 
paulson@11450
   301
\end{warn}%
paulson@11450
   302
\index{variables|)}
nipkow@8743
   303
paulson@10885
   304
\section{Interaction and Interfaces}
nipkow@16306
   305
\label{sec:interface}
nipkow@8771
   306
nipkow@8771
   307
Interaction with Isabelle can either occur at the shell level or through more
paulson@11301
   308
advanced interfaces. To keep the tutorial independent of the interface, we
paulson@11301
   309
have phrased the description of the interaction in a neutral language. For
nipkow@8771
   310
example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
nipkow@8771
   311
shell level, which is explained the first time the phrase is used. Other
nipkow@8771
   312
interfaces perform the same act by cursor movements and/or mouse clicks.
nipkow@8771
   313
Although shell-based interaction is quite feasible for the kind of proof
nipkow@8771
   314
scripts currently presented in this tutorial, the recommended interface for
nipkow@8771
   315
Isabelle/Isar is the Emacs-based \bfindex{Proof
paulson@11450
   316
  General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
nipkow@8771
   317
nipkow@16306
   318
\begin{pgnote}
nipkow@16306
   319
Proof General specific information is always displayed in paragraphs
nipkow@16306
   320
identified by this miniature Proof General icon.
nipkow@8771
   321
nipkow@16306
   322
On particularly nice feature of Proof General is its support for a special
nipkow@16306
   323
fonts with mathematical symbols. Most symbols have
nipkow@16306
   324
\textsc{ascii}-equivalents: for example, you can enter either \verb!&!
nipkow@16306
   325
or \verb!\<and>! to obtain $\land$. For a list of the most frequent symbols
nipkow@16306
   326
see table~\ref{tab:ascii} in the appendix.
nipkow@16306
   327
\end{pgnote}
nipkow@8771
   328
nipkow@16306
   329
\begin{pgnote}
nipkow@16306
   330
Proof General offers an \texttt{Isabelle} menu for displaying information
nipkow@16306
   331
and setting flags. A particularly useful flag is \texttt{Show Types}
nipkow@16306
   332
which 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@16306
   334
because often the types reveal the source of the problem. Once you have
nipkow@16306
   335
diagnosed the problem you may no longer want to see the types because they
nipkow@16306
   336
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@8743
   341
Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
nipkow@8743
   342
  -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
nipkow@8743
   343
  starts the default logic, which usually is already \texttt{HOL}.  This is
nipkow@8743
   344
  controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
nipkow@8743
   345
    System Manual} for more details.} This presents you with Isabelle's most
nipkow@10983
   346
basic \textsc{ascii} interface.  In addition you need to open an editor window to
paulson@11450
   347
create theory files.  While you are developing a theory, we recommend that you
nipkow@8743
   348
type each command into the file first and then enter it into Isabelle by
nipkow@8743
   349
copy-and-paste, thus ensuring that you have a complete record of your theory.
nipkow@8771
   350
As mentioned above, Proof General offers a much superior interface.
paulson@10795
   351
If you have installed Proof General, you can start it by typing \texttt{Isabelle}.