doc-src/TutorialI/basics.tex
author wenzelm
Tue Jan 08 17:31:43 2002 +0100 (2002-01-08)
changeset 12668 b839bd6e06c6
parent 12473 f41e477576b9
child 13439 2f98365f57a8
permissions -rw-r--r--
\chapter{The Basics};
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@11213
    37
you need to consult the Isabelle/Isar Reference
nipkow@12327
    38
Manual~\cite{isabelle-isar-ref} and Wenzel's PhD thesis~\cite{Wenzel-PhD}
nipkow@12327
    39
which discusses many proof patterns. If you want to use Isabelle's ML level
nipkow@8743
    40
directly (for example for writing your own proof procedures) see the Isabelle
nipkow@8743
    41
Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
nipkow@8743
    42
Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
nipkow@8743
    43
index.
nipkow@8743
    44
nipkow@8743
    45
\section{Theories}
nipkow@8743
    46
\label{sec:Basic:Theories}
nipkow@8743
    47
paulson@11428
    48
\index{theories|(}%
nipkow@8743
    49
Working with Isabelle means creating theories. Roughly speaking, a
paulson@11428
    50
\textbf{theory} is a named collection of types, functions, and theorems,
nipkow@8743
    51
much like a module in a programming language or a specification in a
nipkow@8743
    52
specification language. In fact, theories in HOL can be either. The general
nipkow@8743
    53
format of a theory \texttt{T} is
nipkow@8743
    54
\begin{ttbox}
nipkow@8743
    55
theory T = B\(@1\) + \(\cdots\) + B\(@n\):
paulson@11450
    56
{\rmfamily\textit{declarations, definitions, and proofs}}
nipkow@8743
    57
end
nipkow@8743
    58
\end{ttbox}
nipkow@8743
    59
where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
paulson@11450
    60
theories that \texttt{T} is based on and \textit{declarations,
paulson@11450
    61
    definitions, and proofs} represents the newly introduced concepts
nipkow@8771
    62
(types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
paulson@11450
    63
direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@.
paulson@11450
    64
Everything defined in the parent theories (and their parents, recursively) is
nipkow@8743
    65
automatically visible. To avoid name clashes, identifiers can be
paulson@11450
    66
\textbf{qualified}\indexbold{identifiers!qualified}
paulson@11450
    67
by theory names as in \texttt{T.f} and~\texttt{B.f}. 
paulson@11450
    68
Each theory \texttt{T} must
paulson@11428
    69
reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}.
nipkow@8743
    70
nipkow@8743
    71
This tutorial is concerned with introducing you to the different linguistic
paulson@11450
    72
constructs that can fill the \textit{declarations, definitions, and
paulson@11450
    73
    proofs} above.  A complete grammar of the basic
nipkow@12327
    74
constructs is found in the Isabelle/Isar Reference
nipkow@12327
    75
Manual~\cite{isabelle-isar-ref}.
nipkow@8743
    76
paulson@10885
    77
HOL's theory collection is available online at
nipkow@8743
    78
\begin{center}\small
nipkow@10978
    79
    \url{http://isabelle.in.tum.de/library/HOL/}
nipkow@8743
    80
\end{center}
paulson@10885
    81
and is recommended browsing. Note that most of the theories 
nipkow@9541
    82
are based on classical Isabelle without the Isar extension. This means that
nipkow@9541
    83
they look slightly different than the theories in this tutorial, and that all
nipkow@9541
    84
proofs are in separate ML files.
nipkow@9541
    85
nipkow@8743
    86
\begin{warn}
paulson@11428
    87
  HOL contains a theory \thydx{Main}, the union of all the basic
paulson@10885
    88
  predefined theories like arithmetic, lists, sets, etc.  
paulson@10885
    89
  Unless you know what you are doing, always include \isa{Main}
nipkow@10971
    90
  as a direct or indirect parent of all your theories.
nipkow@12332
    91
\end{warn}
nipkow@12473
    92
There is also a growing Library~\cite{HOL-Library}\index{Library}
nipkow@12332
    93
of useful theories that are not part of \isa{Main} but can to be included
nipkow@12473
    94
among the parents of a theory and will then be loaded automatically.%
paulson@11428
    95
\index{theories|)}
nipkow@8743
    96
nipkow@8743
    97
paulson@10885
    98
\section{Types, Terms and Formulae}
nipkow@8743
    99
\label{sec:TypesTermsForms}
nipkow@8743
   100
paulson@10795
   101
Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
nipkow@8771
   102
logic whose type system resembles that of functional programming languages
paulson@11450
   103
like ML or Haskell. Thus there are
paulson@11450
   104
\index{types|(}
nipkow@8743
   105
\begin{description}
paulson@11450
   106
\item[base types,] 
paulson@11450
   107
in particular \tydx{bool}, the type of truth values,
paulson@11428
   108
and \tydx{nat}, the type of natural numbers.
paulson@11450
   109
\item[type constructors,]\index{type constructors}
paulson@11450
   110
 in particular \tydx{list}, the type of
paulson@11428
   111
lists, and \tydx{set}, the type of sets. Type constructors are written
nipkow@8771
   112
postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
nipkow@8743
   113
natural numbers. Parentheses around single arguments can be dropped (as in
nipkow@8771
   114
\isa{nat list}), multiple arguments are separated by commas (as in
nipkow@8771
   115
\isa{(bool,nat)ty}).
paulson@11450
   116
\item[function types,]\index{function types}
paulson@11450
   117
denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
nipkow@8771
   118
  In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
nipkow@8771
   119
  \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
nipkow@8771
   120
  \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
nipkow@8771
   121
  supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
nipkow@8771
   122
  which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
nipkow@8743
   123
    \isasymFun~$\tau$}.
paulson@11450
   124
\item[type variables,]\index{type variables}\index{variables!type}
paulson@10795
   125
  denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
nipkow@8771
   126
  to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
nipkow@8771
   127
  function.
nipkow@8743
   128
\end{description}
nipkow@8743
   129
\begin{warn}
nipkow@8743
   130
  Types are extremely important because they prevent us from writing
nipkow@8743
   131
  nonsense.  Isabelle insists that all terms and formulae must be well-typed
nipkow@8743
   132
  and will print an error message if a type mismatch is encountered. To
nipkow@8743
   133
  reduce the amount of explicit type information that needs to be provided by
nipkow@8743
   134
  the user, Isabelle infers the type of all variables automatically (this is
nipkow@8743
   135
  called \bfindex{type inference}) and keeps quiet about it. Occasionally
nipkow@8743
   136
  this may lead to misunderstandings between you and the system. If anything
paulson@11428
   137
  strange happens, we recommend that you set the flag\index{flags}
paulson@11428
   138
  \isa{show_types}\index{*show_types (flag)}.  
paulson@11428
   139
  Isabelle will then display type information
paulson@11450
   140
  that is usually suppressed.  Simply type
nipkow@8743
   141
\begin{ttbox}
nipkow@8743
   142
ML "set show_types"
nipkow@8743
   143
\end{ttbox}
nipkow@8743
   144
nipkow@8743
   145
\noindent
nipkow@10971
   146
This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
paulson@11428
   147
which we introduce as we go along, can be set and reset in the same manner.%
paulson@11428
   148
\index{flags!setting and resetting}
paulson@11450
   149
\end{warn}%
paulson@11450
   150
\index{types|)}
nipkow@8743
   151
nipkow@8743
   152
paulson@11450
   153
\index{terms|(}
paulson@11450
   154
\textbf{Terms} are formed as in functional programming by
nipkow@8771
   155
applying functions to arguments. If \isa{f} is a function of type
nipkow@8771
   156
\isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
nipkow@8771
   157
$\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
nipkow@8771
   158
infix functions like \isa{+} and some basic constructs from functional
paulson@11428
   159
programming, such as conditional expressions:
nipkow@8743
   160
\begin{description}
paulson@11450
   161
\item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}
paulson@11428
   162
Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
paulson@11450
   163
\item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}
nipkow@8743
   164
is equivalent to $u$ where all occurrences of $x$ have been replaced by
nipkow@8743
   165
$t$. For example,
nipkow@8771
   166
\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
nipkow@8771
   167
by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
nipkow@8771
   168
\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
paulson@11450
   169
\index{*case expressions}
nipkow@8771
   170
evaluates to $e@i$ if $e$ is of the form $c@i$.
nipkow@8743
   171
\end{description}
nipkow@8743
   172
nipkow@8743
   173
Terms may also contain
paulson@11450
   174
\isasymlambda-abstractions.\index{lambda@$\lambda$ expressions}
paulson@11450
   175
For example,
nipkow@8771
   176
\isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
nipkow@8771
   177
returns \isa{x+1}. Instead of
nipkow@8771
   178
\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
paulson@11450
   179
\isa{\isasymlambda{}x~y~z.~$t$}.%
paulson@11450
   180
\index{terms|)}
nipkow@8743
   181
paulson@11450
   182
\index{formulae|(}%
paulson@11450
   183
\textbf{Formulae} are terms of type \tydx{bool}.
paulson@11428
   184
There are the basic constants \cdx{True} and \cdx{False} and
nipkow@8771
   185
the usual logical connectives (in decreasing order of priority):
paulson@11420
   186
\indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
paulson@11420
   187
\indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
nipkow@8743
   188
all of which (except the unary \isasymnot) associate to the right. In
nipkow@8771
   189
particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
nipkow@8771
   190
  \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
nipkow@8771
   191
  \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
nipkow@8743
   192
paulson@11450
   193
Equality\index{equality} is available in the form of the infix function
paulson@11450
   194
\isa{=} of type \isa{'a \isasymFun~'a
nipkow@8771
   195
  \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
paulson@11450
   196
and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type
paulson@11450
   197
\isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}.
paulson@11450
   198
The formula
nipkow@8771
   199
\isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
nipkow@8771
   200
\isa{\isasymnot($t@1$ = $t@2$)}.
nipkow@8743
   201
paulson@11450
   202
Quantifiers\index{quantifiers} are written as
paulson@11450
   203
\isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}. 
paulson@11420
   204
There is even
paulson@11450
   205
\isa{\isasymuniqex{}x.~$P$}, which
paulson@11420
   206
means that there exists exactly one \isa{x} that satisfies \isa{$P$}. 
paulson@11420
   207
Nested quantifications can be abbreviated:
paulson@11420
   208
\isa{\isasymforall{}x~y~z.~$P$} means
paulson@11450
   209
\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.%
paulson@11450
   210
\index{formulae|)}
nipkow@8743
   211
nipkow@8743
   212
Despite type inference, it is sometimes necessary to attach explicit
paulson@11428
   213
\bfindex{type constraints} to a term.  The syntax is
nipkow@8771
   214
\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
nipkow@10538
   215
\ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
paulson@11450
   216
in parentheses.  For instance,
paulson@11450
   217
\isa{x < y::nat} is ill-typed because it is interpreted as
paulson@11450
   218
\isa{(x < y)::nat}.  Type constraints may be needed to disambiguate
paulson@11450
   219
expressions
paulson@11450
   220
involving overloaded functions such as~\isa{+}, 
paulson@11450
   221
\isa{*} and~\isa{<}.  Section~\ref{sec:overloading} 
paulson@11450
   222
discusses overloading, while Table~\ref{tab:overloading} presents the most
nipkow@10695
   223
important overloaded function symbols.
nipkow@8743
   224
paulson@11450
   225
In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of
paulson@11450
   226
functional programming and mathematics.  Here are the main rules that you
paulson@11450
   227
should be familiar with to avoid certain syntactic traps:
nipkow@8743
   228
\begin{itemize}
nipkow@8743
   229
\item
nipkow@8771
   230
Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
nipkow@8743
   231
\item
nipkow@8771
   232
Isabelle allows infix functions like \isa{+}. The prefix form of function
nipkow@8771
   233
application binds more strongly than anything else and hence \isa{f~x + y}
nipkow@8771
   234
means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
nipkow@8743
   235
\item Remember that in HOL if-and-only-if is expressed using equality.  But
nipkow@8743
   236
  equality has a high priority, as befitting a relation, while if-and-only-if
nipkow@8771
   237
  typically has the lowest priority.  Thus, \isa{\isasymnot~\isasymnot~P =
nipkow@8771
   238
    P} means \isa{\isasymnot\isasymnot(P = P)} and not
nipkow@8771
   239
  \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
nipkow@8771
   240
  logical equivalence, enclose both operands in parentheses, as in \isa{(A
nipkow@8743
   241
    \isasymand~B) = (B \isasymand~A)}.
nipkow@8743
   242
\item
nipkow@8743
   243
Constructs with an opening but without a closing delimiter bind very weakly
nipkow@8743
   244
and should therefore be enclosed in parentheses if they appear in subterms, as
paulson@11450
   245
in \isa{(\isasymlambda{}x.~x) = f}.  This includes 
paulson@11450
   246
\isa{if},\index{*if expressions}
paulson@11450
   247
\isa{let},\index{*let expressions}
paulson@11450
   248
\isa{case},\index{*case expressions}
paulson@11450
   249
\isa{\isasymlambda}, and quantifiers.
nipkow@8743
   250
\item
nipkow@8771
   251
Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
nipkow@12327
   252
because \isa{x.x} is always taken as a single qualified identifier. Write
nipkow@8771
   253
\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
paulson@11450
   254
\item Identifiers\indexbold{identifiers} may contain the characters \isa{_} 
nipkow@12327
   255
and~\isa{'}, except at the beginning.
nipkow@8743
   256
\end{itemize}
nipkow@8743
   257
paulson@11450
   258
For the sake of readability, we use the usual mathematical symbols throughout
nipkow@10983
   259
the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
nipkow@8771
   260
the appendix.
nipkow@8771
   261
paulson@11450
   262
\begin{warn}
paulson@11450
   263
A particular
paulson@11450
   264
problem for novices can be the priority of operators. If you are unsure, use
paulson@11450
   265
additional parentheses. In those cases where Isabelle echoes your
paulson@11450
   266
input, you can see which parentheses are dropped --- they were superfluous. If
paulson@11450
   267
you are unsure how to interpret Isabelle's output because you don't know
paulson@11450
   268
where the (dropped) parentheses go, set the flag\index{flags}
paulson@11450
   269
\isa{show_brackets}\index{*show_brackets (flag)}:
paulson@11450
   270
\begin{ttbox}
paulson@11450
   271
ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
paulson@11450
   272
\end{ttbox}
paulson@11450
   273
\end{warn}
paulson@11450
   274
nipkow@8743
   275
nipkow@8743
   276
\section{Variables}
nipkow@8743
   277
\label{sec:variables}
paulson@11450
   278
\index{variables|(}
nipkow@8743
   279
paulson@11450
   280
Isabelle distinguishes free and bound variables, as is customary. Bound
nipkow@8743
   281
variables are automatically renamed to avoid clashes with free variables. In
paulson@11428
   282
addition, Isabelle has a third kind of variable, called a \textbf{schematic
paulson@11428
   283
  variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns}, 
paulson@11428
   284
which must a~\isa{?} as its first character.  
paulson@11428
   285
Logically, an unknown is a free variable. But it may be
nipkow@8743
   286
instantiated by another term during the proof process. For example, the
nipkow@8771
   287
mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
nipkow@8743
   288
which means that Isabelle can instantiate it arbitrarily. This is in contrast
nipkow@8743
   289
to ordinary variables, which remain fixed. The programming language Prolog
nipkow@8743
   290
calls unknowns {\em logical\/} variables.
nipkow@8743
   291
nipkow@8743
   292
Most of the time you can and should ignore unknowns and work with ordinary
nipkow@8743
   293
variables. Just don't be surprised that after you have finished the proof of
paulson@11450
   294
a theorem, Isabelle will turn your free variables into unknowns.  It
nipkow@8743
   295
indicates that Isabelle will automatically instantiate those unknowns
nipkow@8743
   296
suitably when the theorem is used in some other proof.
nipkow@9689
   297
Note that for readability we often drop the \isa{?}s when displaying a theorem.
nipkow@8743
   298
\begin{warn}
paulson@11450
   299
  For historical reasons, Isabelle accepts \isa{?} as an ASCII representation
paulson@11450
   300
  of the \(\exists\) symbol.  However, the \isa{?} character must then be followed
paulson@11450
   301
  by a space, as in \isa{?~x. f(x) = 0}.  Otherwise, \isa{?x} is
paulson@11450
   302
  interpreted as a schematic variable.  The preferred ASCII representation of
paulson@11450
   303
  the \(\exists\) symbol is \isa{EX}\@. 
paulson@11450
   304
\end{warn}%
paulson@11450
   305
\index{variables|)}
nipkow@8743
   306
paulson@10885
   307
\section{Interaction and Interfaces}
nipkow@8771
   308
nipkow@8771
   309
Interaction with Isabelle can either occur at the shell level or through more
paulson@11301
   310
advanced interfaces. To keep the tutorial independent of the interface, we
paulson@11301
   311
have phrased the description of the interaction in a neutral language. For
nipkow@8771
   312
example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
nipkow@8771
   313
shell level, which is explained the first time the phrase is used. Other
nipkow@8771
   314
interfaces perform the same act by cursor movements and/or mouse clicks.
nipkow@8771
   315
Although shell-based interaction is quite feasible for the kind of proof
nipkow@8771
   316
scripts currently presented in this tutorial, the recommended interface for
nipkow@8771
   317
Isabelle/Isar is the Emacs-based \bfindex{Proof
paulson@11450
   318
  General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
nipkow@8771
   319
nipkow@8771
   320
Some interfaces (including the shell level) offer special fonts with
nipkow@10983
   321
mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
nipkow@10978
   322
are shown in table~\ref{tab:ascii} in the appendix.
nipkow@8771
   323
nipkow@9541
   324
Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
nipkow@9541
   325
Commands may but need not be terminated by semicolons.
nipkow@9541
   326
At the shell level it is advisable to use semicolons to enforce that a command
nipkow@8771
   327
is executed immediately; otherwise Isabelle may wait for the next keyword
nipkow@9541
   328
before it knows that the command is complete.
nipkow@8771
   329
nipkow@8771
   330
paulson@10885
   331
\section{Getting Started}
nipkow@8743
   332
nipkow@8743
   333
Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
nipkow@8743
   334
  -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
nipkow@8743
   335
  starts the default logic, which usually is already \texttt{HOL}.  This is
nipkow@8743
   336
  controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
nipkow@8743
   337
    System Manual} for more details.} This presents you with Isabelle's most
nipkow@10983
   338
basic \textsc{ascii} interface.  In addition you need to open an editor window to
paulson@11450
   339
create theory files.  While you are developing a theory, we recommend that you
nipkow@8743
   340
type each command into the file first and then enter it into Isabelle by
nipkow@8743
   341
copy-and-paste, thus ensuring that you have a complete record of your theory.
nipkow@8771
   342
As mentioned above, Proof General offers a much superior interface.
paulson@10795
   343
If you have installed Proof General, you can start it by typing \texttt{Isabelle}.