1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/TutorialI/basics.tex Wed Apr 19 11:54:39 2000 +0200
1.3 @@ -0,0 +1,302 @@
1.4 +\chapter{Basic Concepts}
1.5 +
1.6 +\section{Introduction}
1.7 +
1.8 +This is a tutorial on how to use Isabelle/HOL as a specification and
1.9 +verification system. Isabelle is a generic system for implementing logical
1.10 +formalisms, and Isabelle/HOL is the specialization of Isabelle for
1.11 +HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
1.12 +following the equation
1.13 +\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
1.14 +We assume that the reader is familiar with the basic concepts of both fields.
1.15 +For excellent introductions to functional programming consult the textbooks
1.16 +by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although
1.17 +this tutorial initially concentrates on functional programming, do not be
1.18 +misled: HOL can express most mathematical concepts, and functional
1.19 +programming is just one particularly simple and ubiquitous instance.
1.20 +
1.21 +This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref},
1.22 +which is an extension of Isabelle~\cite{paulson-isa-book} with structured
1.23 +proofs.\footnote{Thus the full name of the system should be
1.24 + Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable
1.25 +difference to classical Isabelle (which is the basis of another version of
1.26 +this tutorial) is the replacement of the ML level by a dedicated language for
1.27 +definitions and proofs.
1.28 +
1.29 +A tutorial is by definition incomplete. Currently the tutorial only
1.30 +introduces the rudiments of Isar's proof language. To fully exploit the power
1.31 +of Isar you need to consult the Isabelle/Isar Reference
1.32 +Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
1.33 +directly (for example for writing your own proof procedures) see the Isabelle
1.34 +Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
1.35 +Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
1.36 +index.
1.37 +
1.38 +\section{Theories}
1.39 +\label{sec:Basic:Theories}
1.40 +
1.41 +Working with Isabelle means creating theories. Roughly speaking, a
1.42 +\bfindex{theory} is a named collection of types, functions, and theorems,
1.43 +much like a module in a programming language or a specification in a
1.44 +specification language. In fact, theories in HOL can be either. The general
1.45 +format of a theory \texttt{T} is
1.46 +\begin{ttbox}
1.47 +theory T = B\(@1\) + \(\cdots\) + B\(@n\):
1.48 +\(\textit{declarations, definitions, and proofs}\)
1.49 +end
1.50 +\end{ttbox}
1.51 +where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
1.52 +theories that \texttt{T} is based on and \texttt{\textit{declarations,
1.53 + definitions, and proofs}} represents the newly introduced concepts
1.54 +(types, functions etc) and proofs about them. The \texttt{B}$@i$ are the
1.55 +direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
1.56 +Everything defined in the parent theories (and their parents \dots) is
1.57 +automatically visible. To avoid name clashes, identifiers can be
1.58 +\textbf{qualified} by theory names as in \texttt{T.f} and
1.59 +\texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
1.60 +reside in a \indexbold{theory file} named \texttt{T.thy}.
1.61 +
1.62 +This tutorial is concerned with introducing you to the different linguistic
1.63 +constructs that can fill \textit{\texttt{declarations, definitions, and
1.64 + proofs}} in the above theory template. A complete grammar of the basic
1.65 +constructs is found in the Isabelle/Isar Reference Manual.
1.66 +
1.67 +HOL's theory library is available online at
1.68 +\begin{center}\small
1.69 + \url{http://isabelle.in.tum.de/library/}
1.70 +\end{center}
1.71 +and is recommended browsing.
1.72 +\begin{warn}
1.73 + HOL contains a theory \ttindexbold{Main}, the union of all the basic
1.74 + predefined theories like arithmetic, lists, sets, etc.\ (see the online
1.75 + library). Unless you know what you are doing, always include \texttt{Main}
1.76 + as a direct or indirect parent theory of all your theories.
1.77 +\end{warn}
1.78 +
1.79 +
1.80 +\section{Interaction and interfaces}
1.81 +
1.82 +Interaction with Isabelle can either occur at the shell level or through more
1.83 +advanced interfaces. To keep the tutorial independent of the interface we
1.84 +have phrased the description of the intraction in a neutral language. For
1.85 +example, the phrase ``to cancel a proof'' means to type \texttt{oops} at the
1.86 +shell level, which is explained the first time the phrase is used. Other
1.87 +interfaces perform the same act by cursor movements and/or mouse clicks.
1.88 +Although shell-based interaction is quite feasible for the kind of proof
1.89 +scripts currently presented in this tutorial, the recommended interface for
1.90 +Isabelle/Isar is the Emacs-based \bfindex{Proof
1.91 + General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
1.92 +
1.93 +To improve readability some of the interfaces (including the shell level)
1.94 +offer special fonts with mathematical symbols. Therefore the usual
1.95 +mathematical symbols are used throughout the tutorial. Their
1.96 +ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix.
1.97 +
1.98 +Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
1.99 +for example Proof General, require each command to be terminated by a
1.100 +semicolon, whereas others, for example the shell level, do not. But even at
1.101 +the shell level it is advisable to use semicolons to enforce that a command
1.102 +is executed immediately; otherwise Isabelle may wait for the next keyword
1.103 +before it knows that the command is complete. Note that for readibility
1.104 +reasons we often drop the final semicolon in the text.
1.105 +
1.106 +
1.107 +\section{Types, terms and formulae}
1.108 +\label{sec:TypesTermsForms}
1.109 +\indexbold{type}
1.110 +
1.111 +Embedded in the declarations of a theory are the types, terms and formulae of
1.112 +HOL. HOL is a typed logic whose type system resembles that of functional
1.113 +programming languages like ML or Haskell. Thus there are
1.114 +\begin{description}
1.115 +\item[base types,] in particular \ttindex{bool}, the type of truth values,
1.116 +and \ttindex{nat}, the type of natural numbers.
1.117 +\item[type constructors,] in particular \texttt{list}, the type of
1.118 +lists, and \texttt{set}, the type of sets. Type constructors are written
1.119 +postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are
1.120 +natural numbers. Parentheses around single arguments can be dropped (as in
1.121 +\texttt{nat list}), multiple arguments are separated by commas (as in
1.122 +\texttt{(bool,nat)foo}).
1.123 +\item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
1.124 + In HOL \isasymFun\ represents {\em total} functions only. As is customary,
1.125 + \texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
1.126 + \texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
1.127 + supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
1.128 + which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
1.129 + \isasymFun~$\tau$}.
1.130 +\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in
1.131 +ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the
1.132 +type of the identity function.
1.133 +\end{description}
1.134 +\begin{warn}
1.135 + Types are extremely important because they prevent us from writing
1.136 + nonsense. Isabelle insists that all terms and formulae must be well-typed
1.137 + and will print an error message if a type mismatch is encountered. To
1.138 + reduce the amount of explicit type information that needs to be provided by
1.139 + the user, Isabelle infers the type of all variables automatically (this is
1.140 + called \bfindex{type inference}) and keeps quiet about it. Occasionally
1.141 + this may lead to misunderstandings between you and the system. If anything
1.142 + strange happens, we recommend to set the \rmindex{flag}
1.143 + \ttindexbold{show_types} that tells Isabelle to display type information
1.144 + that is usually suppressed: simply type
1.145 +\begin{ttbox}
1.146 +ML "set show_types"
1.147 +\end{ttbox}
1.148 +
1.149 +\noindent
1.150 +This can be reversed by \texttt{ML "reset show_types"}. Various other flags
1.151 +can be set and reset in the same manner.\bfindex{flag!(re)setting}
1.152 +\end{warn}
1.153 +
1.154 +
1.155 +\textbf{Terms}\indexbold{term} are formed as in functional programming by
1.156 +applying functions to arguments. If \texttt{f} is a function of type
1.157 +\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type
1.158 +$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports
1.159 +infix functions like \texttt{+} and some basic constructs from functional
1.160 +programming:
1.161 +\begin{description}
1.162 +\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
1.163 +means what you think it means and requires that
1.164 +$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.
1.165 +\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}
1.166 +is equivalent to $u$ where all occurrences of $x$ have been replaced by
1.167 +$t$. For example,
1.168 +\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated
1.169 +by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
1.170 +\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
1.171 +\indexbold{*case}
1.172 +evaluates to $e@i$ if $e$ is of the form
1.173 +$c@i$. See~\S\ref{sec:case-expressions} for details.
1.174 +\end{description}
1.175 +
1.176 +Terms may also contain
1.177 +\isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,
1.178 +\texttt{\isasymlambda{}x.~x+1} is the function that takes an argument
1.179 +\texttt{x} and returns \texttt{x+1}. Instead of
1.180 +\texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$ we can write
1.181 +\texttt{\isasymlambda{}x~y~z.}~$t$.
1.182 +
1.183 +\textbf{Formulae}\indexbold{formula}
1.184 +are terms of type \texttt{bool}. There are the basic
1.185 +constants \ttindexbold{True} and \ttindexbold{False} and the usual logical
1.186 +connectives (in decreasing order of priority):
1.187 +\indexboldpos{\isasymnot}{$HOL0not},
1.188 +\indexboldpos{\isasymand}{$HOL0and},
1.189 +\indexboldpos{\isasymor}{$HOL0or}, and
1.190 +\indexboldpos{\isasymimp}{$HOL0imp},
1.191 +all of which (except the unary \isasymnot) associate to the right. In
1.192 +particular \texttt{A \isasymimp~B \isasymimp~C} means
1.193 +\texttt{A \isasymimp~(B \isasymimp~C)} and is thus
1.194 +logically equivalent with \texttt{A \isasymand~B \isasymimp~C}
1.195 +(which is \texttt{(A \isasymand~B) \isasymimp~C}).
1.196 +
1.197 +Equality is available in the form of the infix function
1.198 +\texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a
1.199 + \isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$
1.200 +and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
1.201 +\texttt{bool}, \texttt{=} acts as if-and-only-if. The formula
1.202 +$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for
1.203 +\texttt{\isasymnot($t@1$ = $t@2$)}.
1.204 +
1.205 +The syntax for quantifiers is
1.206 +\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and
1.207 +\texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}. There is
1.208 +even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which
1.209 +means that there exists exactly one \texttt{x} that satisfies $P$.
1.210 +Nested quantifications can be abbreviated:
1.211 +\texttt{\isasymforall{}x~y~z.}~$P$ means
1.212 +\texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$.
1.213 +
1.214 +Despite type inference, it is sometimes necessary to attach explicit
1.215 +\bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as
1.216 +in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly
1.217 +and should therefore be enclosed in parentheses: \texttt{x < y::nat} is
1.218 +ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason
1.219 +for type constraints are overloaded functions like \texttt{+}, \texttt{*} and
1.220 +\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of
1.221 +overloading.)
1.222 +
1.223 +\begin{warn}
1.224 +In general, HOL's concrete syntax tries to follow the conventions of
1.225 +functional programming and mathematics. Below we list the main rules that you
1.226 +should be familiar with to avoid certain syntactic traps. A particular
1.227 +problem for novices can be the priority of operators. If you are unsure, use
1.228 +more rather than fewer parentheses. In those cases where Isabelle echoes your
1.229 +input, you can see which parentheses are dropped---they were superfluous. If
1.230 +you are unsure how to interpret Isabelle's output because you don't know
1.231 +where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag}
1.232 +\ttindexbold{show_brackets}:
1.233 +\begin{ttbox}
1.234 +ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
1.235 +\end{ttbox}
1.236 +\end{warn}
1.237 +
1.238 +\begin{itemize}
1.239 +\item
1.240 +Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!
1.241 +\item
1.242 +Isabelle allows infix functions like \texttt{+}. The prefix form of function
1.243 +application binds more strongly than anything else and hence \texttt{f~x + y}
1.244 +means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.
1.245 +\item Remember that in HOL if-and-only-if is expressed using equality. But
1.246 + equality has a high priority, as befitting a relation, while if-and-only-if
1.247 + typically has the lowest priority. Thus, \texttt{\isasymnot~\isasymnot~P =
1.248 + P} means \texttt{\isasymnot\isasymnot(P = P)} and not
1.249 + \texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean
1.250 + logical equivalence, enclose both operands in parentheses, as in \texttt{(A
1.251 + \isasymand~B) = (B \isasymand~A)}.
1.252 +\item
1.253 +Constructs with an opening but without a closing delimiter bind very weakly
1.254 +and should therefore be enclosed in parentheses if they appear in subterms, as
1.255 +in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if},
1.256 +\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers.
1.257 +\item
1.258 +Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x}
1.259 +because \texttt{x.x} is always read as a single qualified identifier that
1.260 +refers to an item \texttt{x} in theory \texttt{x}. Write
1.261 +\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead.
1.262 +\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}.
1.263 +\end{itemize}
1.264 +
1.265 +Remember that ASCII-equivalents of all mathematical symbols are
1.266 +given in figure~\ref{fig:ascii} in the appendix.
1.267 +
1.268 +\section{Variables}
1.269 +\label{sec:variables}
1.270 +\indexbold{variable}
1.271 +
1.272 +Isabelle distinguishes free and bound variables just as is customary. Bound
1.273 +variables are automatically renamed to avoid clashes with free variables. In
1.274 +addition, Isabelle has a third kind of variable, called a \bfindex{schematic
1.275 + variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
1.276 +with a \texttt{?}. Logically, an unknown is a free variable. But it may be
1.277 +instantiated by another term during the proof process. For example, the
1.278 +mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x},
1.279 +which means that Isabelle can instantiate it arbitrarily. This is in contrast
1.280 +to ordinary variables, which remain fixed. The programming language Prolog
1.281 +calls unknowns {\em logical\/} variables.
1.282 +
1.283 +Most of the time you can and should ignore unknowns and work with ordinary
1.284 +variables. Just don't be surprised that after you have finished the proof of
1.285 +a theorem, Isabelle will turn your free variables into unknowns: it merely
1.286 +indicates that Isabelle will automatically instantiate those unknowns
1.287 +suitably when the theorem is used in some other proof.
1.288 +\begin{warn}
1.289 + If you use \texttt{?}\index{$HOL0Ex@\texttt{?}} as an existential
1.290 + quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is
1.291 + interpreted as a schematic variable.
1.292 +\end{warn}
1.293 +
1.294 +\section{Getting started}
1.295 +
1.296 +Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
1.297 + -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
1.298 + starts the default logic, which usually is already \texttt{HOL}. This is
1.299 + controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
1.300 + System Manual} for more details.} This presents you with Isabelle's most
1.301 +basic ASCII interface. In addition you need to open an editor window to
1.302 +create theory files. While you are developing a theory, we recommend to
1.303 +type each command into the file first and then enter it into Isabelle by
1.304 +copy-and-paste, thus ensuring that you have a complete record of your theory.
1.305 +As mentioned earlier, Proof General offers a much superior interface.