diff -r f51d4a302962 -r 5386df44a037 src/Doc/Tutorial/document/basics.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Tutorial/document/basics.tex Tue Aug 28 18:57:32 2012 +0200 @@ -0,0 +1,350 @@ +\chapter{The Basics} + +\section{Introduction} + +This book is a tutorial on how to use the theorem prover Isabelle/HOL as a +specification and verification system. Isabelle is a generic system for +implementing logical formalisms, and Isabelle/HOL is the specialization +of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce +HOL step by step following the equation +\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] +We do not assume that you are familiar with mathematical logic. +However, we do assume that +you are used to logical and set theoretic notation, as covered +in a good discrete mathematics course~\cite{Rosen-DMA}, and +that you are familiar with the basic concepts of functional +programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}. +Although this tutorial initially concentrates on functional programming, do +not be misled: HOL can express most mathematical concepts, and functional +programming is just one particularly simple and ubiquitous instance. + +Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has +influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant +for us: this tutorial is based on +Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides +the implementation language almost completely. Thus the full name of the +system should be Isabelle/Isar/HOL, but that is a bit of a mouthful. + +There are other implementations of HOL, in particular the one by Mike Gordon +\index{Gordon, Mike}% +\emph{et al.}, which is usually referred to as ``the HOL system'' +\cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes +its incarnation Isabelle/HOL\@. + +A tutorial is by definition incomplete. Currently the tutorial only +introduces the rudiments of Isar's proof language. To fully exploit the power +of Isar, in particular the ability to write readable and structured proofs, +you should start with Nipkow's overview~\cite{Nipkow-TYPES02} and consult +the Isabelle/Isar Reference Manual~\cite{isabelle-isar-ref} and Wenzel's +PhD thesis~\cite{Wenzel-PhD} (which discusses many proof patterns) +for further details. If you want to use Isabelle's ML level +directly (for example for writing your own proof procedures) see the Isabelle +Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the +Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive +index. + +\section{Theories} +\label{sec:Basic:Theories} + +\index{theories|(}% +Working with Isabelle means creating theories. Roughly speaking, a +\textbf{theory} is a named collection of types, functions, and theorems, +much like a module in a programming language or a specification in a +specification language. In fact, theories in HOL can be either. The general +format of a theory \texttt{T} is +\begin{ttbox} +theory T +imports B\(@1\) \(\ldots\) B\(@n\) +begin +{\rmfamily\textit{declarations, definitions, and proofs}} +end +\end{ttbox}\cmmdx{theory}\cmmdx{imports} +where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing +theories that \texttt{T} is based on and \textit{declarations, + definitions, and proofs} represents the newly introduced concepts +(types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the +direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@. +Everything defined in the parent theories (and their parents, recursively) is +automatically visible. To avoid name clashes, identifiers can be +\textbf{qualified}\indexbold{identifiers!qualified} +by theory names as in \texttt{T.f} and~\texttt{B.f}. +Each theory \texttt{T} must +reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}. + +This tutorial is concerned with introducing you to the different linguistic +constructs that can fill the \textit{declarations, definitions, and + proofs} above. A complete grammar of the basic +constructs is found in the Isabelle/Isar Reference +Manual~\cite{isabelle-isar-ref}. + +\begin{warn} + HOL contains a theory \thydx{Main}, the union of all the basic + predefined theories like arithmetic, lists, sets, etc. + Unless you know what you are doing, always include \isa{Main} + as a direct or indirect parent of all your theories. +\end{warn} +HOL's theory collection is available online at +\begin{center}\small + \url{http://isabelle.in.tum.de/library/HOL/} +\end{center} +and is recommended browsing. In subdirectory \texttt{Library} you find +a growing library of useful theories that are not part of \isa{Main} +but can be included among the parents of a theory and will then be +loaded automatically. + +For the more adventurous, there is the \emph{Archive of Formal Proofs}, +a journal-like collection of more advanced Isabelle theories: +\begin{center}\small + \url{http://afp.sourceforge.net/} +\end{center} +We hope that you will contribute to it yourself one day.% +\index{theories|)} + + +\section{Types, Terms and Formulae} +\label{sec:TypesTermsForms} + +Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed +logic whose type system resembles that of functional programming languages +like ML or Haskell. Thus there are +\index{types|(} +\begin{description} +\item[base types,] +in particular \tydx{bool}, the type of truth values, +and \tydx{nat}, the type of natural numbers. +\item[type constructors,]\index{type constructors} + in particular \tydx{list}, the type of +lists, and \tydx{set}, the type of sets. Type constructors are written +postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are +natural numbers. Parentheses around single arguments can be dropped (as in +\isa{nat list}), multiple arguments are separated by commas (as in +\isa{(bool,nat)ty}). +\item[function types,]\index{function types} +denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}. + In HOL \isasymFun\ represents \emph{total} functions only. As is customary, + \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means + \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also + supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$} + which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$ + \isasymFun~$\tau$}. +\item[type variables,]\index{type variables}\index{variables!type} + denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise + to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity + function. +\end{description} +\begin{warn} + Types are extremely important because they prevent us from writing + nonsense. Isabelle insists that all terms and formulae must be + well-typed and will print an error message if a type mismatch is + encountered. To reduce the amount of explicit type information that + needs to be provided by the user, Isabelle infers the type of all + variables automatically (this is called \bfindex{type inference}) + and keeps quiet about it. Occasionally this may lead to + misunderstandings between you and the system. If anything strange + happens, we recommend that you ask Isabelle to display all type + information via the Proof General menu item \pgmenu{Isabelle} $>$ + \pgmenu{Settings} $>$ \pgmenu{Show Types} (see \S\ref{sec:interface} + for details). +\end{warn}% +\index{types|)} + + +\index{terms|(} +\textbf{Terms} are formed as in functional programming by +applying functions to arguments. If \isa{f} is a function of type +\isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type +$\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports +infix functions like \isa{+} and some basic constructs from functional +programming, such as conditional expressions: +\begin{description} +\item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions} +Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type. +\item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions} +is equivalent to $u$ where all free occurrences of $x$ have been replaced by +$t$. For example, +\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated +by semicolons: \isa{let $x@1$ = $t@1$;\dots; $x@n$ = $t@n$ in $u$}. +\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}] +\index{*case expressions} +evaluates to $e@i$ if $e$ is of the form $c@i$. +\end{description} + +Terms may also contain +\isasymlambda-abstractions.\index{lambda@$\lambda$ expressions} +For example, +\isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and +returns \isa{x+1}. Instead of +\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write +\isa{\isasymlambda{}x~y~z.~$t$}.% +\index{terms|)} + +\index{formulae|(}% +\textbf{Formulae} are terms of type \tydx{bool}. +There are the basic constants \cdx{True} and \cdx{False} and +the usual logical connectives (in decreasing order of priority): +\indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and}, +\indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp}, +all of which (except the unary \isasymnot) associate to the right. In +particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B + \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B + \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}). + +Equality\index{equality} is available in the form of the infix function +\isa{=} of type \isa{'a \isasymFun~'a + \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$ +and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type +\isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}. +The formula +\isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for +\isa{\isasymnot($t@1$ = $t@2$)}. + +Quantifiers\index{quantifiers} are written as +\isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}. +There is even +\isa{\isasymuniqex{}x.~$P$}, which +means that there exists exactly one \isa{x} that satisfies \isa{$P$}. +Nested quantifications can be abbreviated: +\isa{\isasymforall{}x~y~z.~$P$} means +\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.% +\index{formulae|)} + +Despite type inference, it is sometimes necessary to attach explicit +\bfindex{type constraints} to a term. The syntax is +\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that +\ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed +in parentheses. For instance, +\isa{x < y::nat} is ill-typed because it is interpreted as +\isa{(x < y)::nat}. Type constraints may be needed to disambiguate +expressions +involving overloaded functions such as~\isa{+}, +\isa{*} and~\isa{<}. Section~\ref{sec:overloading} +discusses overloading, while Table~\ref{tab:overloading} presents the most +important overloaded function symbols. + +In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of +functional programming and mathematics. Here are the main rules that you +should be familiar with to avoid certain syntactic traps: +\begin{itemize} +\item +Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}! +\item +Isabelle allows infix functions like \isa{+}. The prefix form of function +application binds more strongly than anything else and hence \isa{f~x + y} +means \isa{(f~x)~+~y} and not \isa{f(x+y)}. +\item Remember that in HOL if-and-only-if is expressed using equality. But + equality has a high priority, as befitting a relation, while if-and-only-if + typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P = + P} means \isa{\isasymnot\isasymnot(P = P)} and not + \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean + logical equivalence, enclose both operands in parentheses, as in \isa{(A + \isasymand~B) = (B \isasymand~A)}. +\item +Constructs with an opening but without a closing delimiter bind very weakly +and should therefore be enclosed in parentheses if they appear in subterms, as +in \isa{(\isasymlambda{}x.~x) = f}. This includes +\isa{if},\index{*if expressions} +\isa{let},\index{*let expressions} +\isa{case},\index{*case expressions} +\isa{\isasymlambda}, and quantifiers. +\item +Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x} +because \isa{x.x} is always taken as a single qualified identifier. Write +\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead. +\item Identifiers\indexbold{identifiers} may contain the characters \isa{_} +and~\isa{'}, except at the beginning. +\end{itemize} + +For the sake of readability, we use the usual mathematical symbols throughout +the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in +the appendix. + +\begin{warn} +A particular problem for novices can be the priority of operators. If +you are unsure, use additional parentheses. In those cases where +Isabelle echoes your input, you can see which parentheses are dropped +--- they were superfluous. If you are unsure how to interpret +Isabelle's output because you don't know where the (dropped) +parentheses go, set the Proof General flag \pgmenu{Isabelle} $>$ +\pgmenu{Settings} $>$ \pgmenu{Show Brackets} (see \S\ref{sec:interface}). +\end{warn} + + +\section{Variables} +\label{sec:variables} +\index{variables|(} + +Isabelle distinguishes free and bound variables, as is customary. Bound +variables are automatically renamed to avoid clashes with free variables. In +addition, Isabelle has a third kind of variable, called a \textbf{schematic + variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns}, +which must have a~\isa{?} as its first character. +Logically, an unknown is a free variable. But it may be +instantiated by another term during the proof process. For example, the +mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x}, +which means that Isabelle can instantiate it arbitrarily. This is in contrast +to ordinary variables, which remain fixed. The programming language Prolog +calls unknowns {\em logical\/} variables. + +Most of the time you can and should ignore unknowns and work with ordinary +variables. Just don't be surprised that after you have finished the proof of +a theorem, Isabelle will turn your free variables into unknowns. It +indicates that Isabelle will automatically instantiate those unknowns +suitably when the theorem is used in some other proof. +Note that for readability we often drop the \isa{?}s when displaying a theorem. +\begin{warn} + For historical reasons, Isabelle accepts \isa{?} as an ASCII representation + of the \(\exists\) symbol. However, the \isa{?} character must then be followed + by a space, as in \isa{?~x. f(x) = 0}. Otherwise, \isa{?x} is + interpreted as a schematic variable. The preferred ASCII representation of + the \(\exists\) symbol is \isa{EX}\@. +\end{warn}% +\index{variables|)} + +\section{Interaction and Interfaces} +\label{sec:interface} + +The recommended interface for Isabelle/Isar is the (X)Emacs-based +\bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}. +Interaction with Isabelle at the shell level, although possible, +should be avoided. Most of the tutorial is independent of the +interface and is phrased in a neutral language. For example, the +phrase ``to abandon a proof'' corresponds to the obvious +action of clicking on the \pgmenu{Undo} symbol in Proof General. +Proof General specific information is often displayed in paragraphs +identified by a miniature Proof General icon. Here are two examples: +\begin{pgnote} +Proof General supports a special font with mathematical symbols known +as ``x-symbols''. All symbols have \textsc{ascii}-equivalents: for +example, you can enter either \verb!&! or \verb!\! to obtain +$\land$. For a list of the most frequent symbols see table~\ref{tab:ascii} +in the appendix. + +Note that by default x-symbols are not enabled. You have to switch +them on via the menu item \pgmenu{Proof-General} $>$ \pgmenu{Options} $>$ +\pgmenu{X-Symbols} (and save the option via the top-level +\pgmenu{Options} menu). +\end{pgnote} + +\begin{pgnote} +Proof General offers the \pgmenu{Isabelle} menu for displaying +information and setting flags. A particularly useful flag is +\pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgdx{Show Types} which +causes Isabelle to output the type information that is usually +suppressed. This is indispensible in case of errors of all kinds +because often the types reveal the source of the problem. Once you +have diagnosed the problem you may no longer want to see the types +because they clutter all output. Simply reset the flag. +\end{pgnote} + +\section{Getting Started} + +Assuming you have installed Isabelle and Proof General, you start it by typing +\texttt{Isabelle} in a shell window. This launches a Proof General window. +By default, you are in HOL\footnote{This is controlled by the +\texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual} +for more details.}. + +\begin{pgnote} +You can choose a different logic via the \pgmenu{Isabelle} $>$ +\pgmenu{Logics} menu. +\end{pgnote}