summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/basics.tex

changeset 8743 | 3253c6046d57 |

child 8771 | 026f37a86ea7 |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/basics.tex Wed Apr 19 11:54:39 2000 +0200 @@ -0,0 +1,302 @@ +\chapter{Basic Concepts} + +\section{Introduction} + +This is a tutorial on how to use 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 assume that the reader is familiar with the basic concepts of both fields. +For excellent introductions to functional programming consult the textbooks +by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. 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. + +This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref}, +which is an extension of Isabelle~\cite{paulson-isa-book} with structured +proofs.\footnote{Thus the full name of the system should be + Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable +difference to classical Isabelle (which is the basis of another version of +this tutorial) is the replacement of the ML level by a dedicated language for +definitions and proofs. + +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 you need to consult the Isabelle/Isar Reference +Manual~\cite{isabelle-isar-ref}. 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} + +Working with Isabelle means creating theories. Roughly speaking, a +\bfindex{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 = B\(@1\) + \(\cdots\) + B\(@n\): +\(\textit{declarations, definitions, and proofs}\) +end +\end{ttbox} +where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing +theories that \texttt{T} is based on and \texttt{\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 theory} of \texttt{T}. +Everything defined in the parent theories (and their parents \dots) is +automatically visible. To avoid name clashes, identifiers can be +\textbf{qualified} by theory names as in \texttt{T.f} and +\texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must +reside in a \indexbold{theory file} named \texttt{T.thy}. + +This tutorial is concerned with introducing you to the different linguistic +constructs that can fill \textit{\texttt{declarations, definitions, and + proofs}} in the above theory template. A complete grammar of the basic +constructs is found in the Isabelle/Isar Reference Manual. + +HOL's theory library is available online at +\begin{center}\small + \url{http://isabelle.in.tum.de/library/} +\end{center} +and is recommended browsing. +\begin{warn} + HOL contains a theory \ttindexbold{Main}, the union of all the basic + predefined theories like arithmetic, lists, sets, etc.\ (see the online + library). Unless you know what you are doing, always include \texttt{Main} + as a direct or indirect parent theory of all your theories. +\end{warn} + + +\section{Interaction and interfaces} + +Interaction with Isabelle can either occur at the shell level or through more +advanced interfaces. To keep the tutorial independent of the interface we +have phrased the description of the intraction in a neutral language. For +example, the phrase ``to cancel a proof'' means to type \texttt{oops} at the +shell level, which is explained the first time the phrase is used. Other +interfaces perform the same act by cursor movements and/or mouse clicks. +Although shell-based interaction is quite feasible for the kind of proof +scripts currently presented in this tutorial, the recommended interface for +Isabelle/Isar is the Emacs-based \bfindex{Proof + General}~\cite{Aspinall:TACAS:2000,proofgeneral}. + +To improve readability some of the interfaces (including the shell level) +offer special fonts with mathematical symbols. Therefore the usual +mathematical symbols are used throughout the tutorial. Their +ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix. + +Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces, +for example Proof General, require each command to be terminated by a +semicolon, whereas others, for example the shell level, do not. But even at +the shell level it is advisable to use semicolons to enforce that a command +is executed immediately; otherwise Isabelle may wait for the next keyword +before it knows that the command is complete. Note that for readibility +reasons we often drop the final semicolon in the text. + + +\section{Types, terms and formulae} +\label{sec:TypesTermsForms} +\indexbold{type} + +Embedded in the declarations of 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 +\begin{description} +\item[base types,] in particular \ttindex{bool}, the type of truth values, +and \ttindex{nat}, the type of natural numbers. +\item[type constructors,] in particular \texttt{list}, the type of +lists, and \texttt{set}, the type of sets. Type constructors are written +postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are +natural numbers. Parentheses around single arguments can be dropped (as in +\texttt{nat list}), multiple arguments are separated by commas (as in +\texttt{(bool,nat)foo}). +\item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}. + In HOL \isasymFun\ represents {\em total} functions only. As is customary, + \texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means + \texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also + supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$} + which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$ + \isasymFun~$\tau$}. +\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in +ML. They give rise to polymorphic types like \texttt{'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 to set the \rmindex{flag} + \ttindexbold{show_types} that tells Isabelle to display type information + that is usually suppressed: simply type +\begin{ttbox} +ML "set show_types" +\end{ttbox} + +\noindent +This can be reversed by \texttt{ML "reset show_types"}. Various other flags +can be set and reset in the same manner.\bfindex{flag!(re)setting} +\end{warn} + + +\textbf{Terms}\indexbold{term} are formed as in functional programming by +applying functions to arguments. If \texttt{f} is a function of type +\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type +$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports +infix functions like \texttt{+} and some basic constructs from functional +programming: +\begin{description} +\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if} +means what you think it means and requires that +$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type. +\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let} +is equivalent to $u$ where all occurrences of $x$ have been replaced by +$t$. For example, +\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated +by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}. +\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}] +\indexbold{*case} +evaluates to $e@i$ if $e$ is of the form +$c@i$. See~\S\ref{sec:case-expressions} for details. +\end{description} + +Terms may also contain +\isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example, +\texttt{\isasymlambda{}x.~x+1} is the function that takes an argument +\texttt{x} and returns \texttt{x+1}. Instead of +\texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$ we can write +\texttt{\isasymlambda{}x~y~z.}~$t$. + +\textbf{Formulae}\indexbold{formula} +are terms of type \texttt{bool}. There are the basic +constants \ttindexbold{True} and \ttindexbold{False} and the usual logical +connectives (in decreasing order of priority): +\indexboldpos{\isasymnot}{$HOL0not}, +\indexboldpos{\isasymand}{$HOL0and}, +\indexboldpos{\isasymor}{$HOL0or}, and +\indexboldpos{\isasymimp}{$HOL0imp}, +all of which (except the unary \isasymnot) associate to the right. In +particular \texttt{A \isasymimp~B \isasymimp~C} means +\texttt{A \isasymimp~(B \isasymimp~C)} and is thus +logically equivalent with \texttt{A \isasymand~B \isasymimp~C} +(which is \texttt{(A \isasymand~B) \isasymimp~C}). + +Equality is available in the form of the infix function +\texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a + \isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$ +and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type +\texttt{bool}, \texttt{=} acts as if-and-only-if. The formula +$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for +\texttt{\isasymnot($t@1$ = $t@2$)}. + +The syntax for quantifiers is +\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and +\texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}. There is +even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which +means that there exists exactly one \texttt{x} that satisfies $P$. +Nested quantifications can be abbreviated: +\texttt{\isasymforall{}x~y~z.}~$P$ means +\texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$. + +Despite type inference, it is sometimes necessary to attach explicit +\bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as +in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly +and should therefore be enclosed in parentheses: \texttt{x < y::nat} is +ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason +for type constraints are overloaded functions like \texttt{+}, \texttt{*} and +\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of +overloading.) + +\begin{warn} +In general, HOL's concrete syntax tries to follow the conventions of +functional programming and mathematics. Below we list the main rules that you +should be familiar with to avoid certain syntactic traps. A particular +problem for novices can be the priority of operators. If you are unsure, use +more rather than fewer 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 (and possibly reset) the \rmindex{flag} +\ttindexbold{show_brackets}: +\begin{ttbox} +ML "set show_brackets"; \(\dots\); ML "reset show_brackets"; +\end{ttbox} +\end{warn} + +\begin{itemize} +\item +Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}! +\item +Isabelle allows infix functions like \texttt{+}. The prefix form of function +application binds more strongly than anything else and hence \texttt{f~x + y} +means \texttt{(f~x)~+~y} and not \texttt{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, \texttt{\isasymnot~\isasymnot~P = + P} means \texttt{\isasymnot\isasymnot(P = P)} and not + \texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean + logical equivalence, enclose both operands in parentheses, as in \texttt{(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 \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if}, +\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers. +\item +Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x} +because \texttt{x.x} is always read as a single qualified identifier that +refers to an item \texttt{x} in theory \texttt{x}. Write +\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead. +\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}. +\end{itemize} + +Remember that ASCII-equivalents of all mathematical symbols are +given in figure~\ref{fig:ascii} in the appendix. + +\section{Variables} +\label{sec:variables} +\indexbold{variable} + +Isabelle distinguishes free and bound variables just 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 \bfindex{schematic + variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts +with a \texttt{?}. 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 \texttt{?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 merely +indicates that Isabelle will automatically instantiate those unknowns +suitably when the theorem is used in some other proof. +\begin{warn} + If you use \texttt{?}\index{$HOL0Ex@\texttt{?}} as an existential + quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is + interpreted as a schematic variable. +\end{warn} + +\section{Getting started} + +Assuming you have installed Isabelle, you start it by typing \texttt{isabelle + -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I} + starts the default logic, which usually is already \texttt{HOL}. This is + controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle + System Manual} for more details.} This presents you with Isabelle's most +basic ASCII interface. In addition you need to open an editor window to +create theory files. While you are developing a theory, we recommend to +type each command into the file first and then enter it into Isabelle by +copy-and-paste, thus ensuring that you have a complete record of your theory. +As mentioned earlier, Proof General offers a much superior interface.