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