doc-src/TutorialI/basics.tex
 author nipkow Wed Apr 19 11:54:39 2000 +0200 (2000-04-19) changeset 8743 3253c6046d57 child 8771 026f37a86ea7 permissions -rw-r--r--
I wonder if that's all?
 nipkow@8743  1 \chapter{Basic Concepts}  nipkow@8743  2 nipkow@8743  3 \section{Introduction}  nipkow@8743  4 nipkow@8743  5 This is a tutorial on how to use Isabelle/HOL as a specification and  nipkow@8743  6 verification system. Isabelle is a generic system for implementing logical  nipkow@8743  7 formalisms, and Isabelle/HOL is the specialization of Isabelle for  nipkow@8743  8 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step  nipkow@8743  9 following the equation  nipkow@8743  10 $\mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}.$  nipkow@8743  11 We assume that the reader is familiar with the basic concepts of both fields.  nipkow@8743  12 For excellent introductions to functional programming consult the textbooks  nipkow@8743  13 by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although  nipkow@8743  14 this tutorial initially concentrates on functional programming, do not be  nipkow@8743  15 misled: HOL can express most mathematical concepts, and functional  nipkow@8743  16 programming is just one particularly simple and ubiquitous instance.  nipkow@8743  17 nipkow@8743  18 This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref},  nipkow@8743  19 which is an extension of Isabelle~\cite{paulson-isa-book} with structured  nipkow@8743  20 proofs.\footnote{Thus the full name of the system should be  nipkow@8743  21  Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable  nipkow@8743  22 difference to classical Isabelle (which is the basis of another version of  nipkow@8743  23 this tutorial) is the replacement of the ML level by a dedicated language for  nipkow@8743  24 definitions and proofs.  nipkow@8743  25 nipkow@8743  26 A tutorial is by definition incomplete. Currently the tutorial only  nipkow@8743  27 introduces the rudiments of Isar's proof language. To fully exploit the power  nipkow@8743  28 of Isar you need to consult the Isabelle/Isar Reference  nipkow@8743  29 Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level  nipkow@8743  30 directly (for example for writing your own proof procedures) see the Isabelle  nipkow@8743  31 Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the  nipkow@8743  32 Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive  nipkow@8743  33 index.  nipkow@8743  34 nipkow@8743  35 \section{Theories}  nipkow@8743  36 \label{sec:Basic:Theories}  nipkow@8743  37 nipkow@8743  38 Working with Isabelle means creating theories. Roughly speaking, a  nipkow@8743  39 \bfindex{theory} is a named collection of types, functions, and theorems,  nipkow@8743  40 much like a module in a programming language or a specification in a  nipkow@8743  41 specification language. In fact, theories in HOL can be either. The general  nipkow@8743  42 format of a theory \texttt{T} is  nipkow@8743  43 \begin{ttbox}  nipkow@8743  44 theory T = B$$@1$$ + $$\cdots$$ + B$$@n$$:  nipkow@8743  45 $$\textit{declarations, definitions, and proofs}$$  nipkow@8743  46 end  nipkow@8743  47 \end{ttbox}  nipkow@8743  48 where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing  nipkow@8743  49 theories that \texttt{T} is based on and \texttt{\textit{declarations,  nipkow@8743  50  definitions, and proofs}} represents the newly introduced concepts  nipkow@8743  51 (types, functions etc) and proofs about them. The \texttt{B}$@i$ are the  nipkow@8743  52 direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.  nipkow@8743  53 Everything defined in the parent theories (and their parents \dots) is  nipkow@8743  54 automatically visible. To avoid name clashes, identifiers can be  nipkow@8743  55 \textbf{qualified} by theory names as in \texttt{T.f} and  nipkow@8743  56 \texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must  nipkow@8743  57 reside in a \indexbold{theory file} named \texttt{T.thy}.  nipkow@8743  58 nipkow@8743  59 This tutorial is concerned with introducing you to the different linguistic  nipkow@8743  60 constructs that can fill \textit{\texttt{declarations, definitions, and  nipkow@8743  61  proofs}} in the above theory template. A complete grammar of the basic  nipkow@8743  62 constructs is found in the Isabelle/Isar Reference Manual.  nipkow@8743  63 nipkow@8743  64 HOL's theory library is available online at  nipkow@8743  65 \begin{center}\small  nipkow@8743  66  \url{http://isabelle.in.tum.de/library/}  nipkow@8743  67 \end{center}  nipkow@8743  68 and is recommended browsing.  nipkow@8743  69 \begin{warn}  nipkow@8743  70  HOL contains a theory \ttindexbold{Main}, the union of all the basic  nipkow@8743  71  predefined theories like arithmetic, lists, sets, etc.\ (see the online  nipkow@8743  72  library). Unless you know what you are doing, always include \texttt{Main}  nipkow@8743  73  as a direct or indirect parent theory of all your theories.  nipkow@8743  74 \end{warn}  nipkow@8743  75 nipkow@8743  76 nipkow@8743  77 \section{Interaction and interfaces}  nipkow@8743  78 nipkow@8743  79 Interaction with Isabelle can either occur at the shell level or through more  nipkow@8743  80 advanced interfaces. To keep the tutorial independent of the interface we  nipkow@8743  81 have phrased the description of the intraction in a neutral language. For  nipkow@8743  82 example, the phrase to cancel a proof'' means to type \texttt{oops} at the  nipkow@8743  83 shell level, which is explained the first time the phrase is used. Other  nipkow@8743  84 interfaces perform the same act by cursor movements and/or mouse clicks.  nipkow@8743  85 Although shell-based interaction is quite feasible for the kind of proof  nipkow@8743  86 scripts currently presented in this tutorial, the recommended interface for  nipkow@8743  87 Isabelle/Isar is the Emacs-based \bfindex{Proof  nipkow@8743  88  General}~\cite{Aspinall:TACAS:2000,proofgeneral}.  nipkow@8743  89 nipkow@8743  90 To improve readability some of the interfaces (including the shell level)  nipkow@8743  91 offer special fonts with mathematical symbols. Therefore the usual  nipkow@8743  92 mathematical symbols are used throughout the tutorial. Their  nipkow@8743  93 ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix.  nipkow@8743  94 nipkow@8743  95 Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,  nipkow@8743  96 for example Proof General, require each command to be terminated by a  nipkow@8743  97 semicolon, whereas others, for example the shell level, do not. But even at  nipkow@8743  98 the shell level it is advisable to use semicolons to enforce that a command  nipkow@8743  99 is executed immediately; otherwise Isabelle may wait for the next keyword  nipkow@8743  100 before it knows that the command is complete. Note that for readibility  nipkow@8743  101 reasons we often drop the final semicolon in the text.  nipkow@8743  102 nipkow@8743  103 nipkow@8743  104 \section{Types, terms and formulae}  nipkow@8743  105 \label{sec:TypesTermsForms}  nipkow@8743  106 \indexbold{type}  nipkow@8743  107 nipkow@8743  108 Embedded in the declarations of a theory are the types, terms and formulae of  nipkow@8743  109 HOL. HOL is a typed logic whose type system resembles that of functional  nipkow@8743  110 programming languages like ML or Haskell. Thus there are  nipkow@8743  111 \begin{description}  nipkow@8743  112 \item[base types,] in particular \ttindex{bool}, the type of truth values,  nipkow@8743  113 and \ttindex{nat}, the type of natural numbers.  nipkow@8743  114 \item[type constructors,] in particular \texttt{list}, the type of  nipkow@8743  115 lists, and \texttt{set}, the type of sets. Type constructors are written  nipkow@8743  116 postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are  nipkow@8743  117 natural numbers. Parentheses around single arguments can be dropped (as in  nipkow@8743  118 \texttt{nat list}), multiple arguments are separated by commas (as in  nipkow@8743  119 \texttt{(bool,nat)foo}).  nipkow@8743  120 \item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.  nipkow@8743  121  In HOL \isasymFun\ represents {\em total} functions only. As is customary,  nipkow@8743  122  \texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means  nipkow@8743  123  \texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also  nipkow@8743  124  supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}  nipkow@8743  125  which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$  nipkow@8743  126  \isasymFun~$\tau$}.  nipkow@8743  127 \item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in  nipkow@8743  128 ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the  nipkow@8743  129 type of the identity function.  nipkow@8743  130 \end{description}  nipkow@8743  131 \begin{warn}  nipkow@8743  132  Types are extremely important because they prevent us from writing  nipkow@8743  133  nonsense. Isabelle insists that all terms and formulae must be well-typed  nipkow@8743  134  and will print an error message if a type mismatch is encountered. To  nipkow@8743  135  reduce the amount of explicit type information that needs to be provided by  nipkow@8743  136  the user, Isabelle infers the type of all variables automatically (this is  nipkow@8743  137  called \bfindex{type inference}) and keeps quiet about it. Occasionally  nipkow@8743  138  this may lead to misunderstandings between you and the system. If anything  nipkow@8743  139  strange happens, we recommend to set the \rmindex{flag}  nipkow@8743  140  \ttindexbold{show_types} that tells Isabelle to display type information  nipkow@8743  141  that is usually suppressed: simply type  nipkow@8743  142 \begin{ttbox}  nipkow@8743  143 ML "set show_types"  nipkow@8743  144 \end{ttbox}  nipkow@8743  145 nipkow@8743  146 \noindent  nipkow@8743  147 This can be reversed by \texttt{ML "reset show_types"}. Various other flags  nipkow@8743  148 can be set and reset in the same manner.\bfindex{flag!(re)setting}  nipkow@8743  149 \end{warn}  nipkow@8743  150 nipkow@8743  151 nipkow@8743  152 \textbf{Terms}\indexbold{term} are formed as in functional programming by  nipkow@8743  153 applying functions to arguments. If \texttt{f} is a function of type  nipkow@8743  154 \texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type  nipkow@8743  155 $\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports  nipkow@8743  156 infix functions like \texttt{+} and some basic constructs from functional  nipkow@8743  157 programming:  nipkow@8743  158 \begin{description}  nipkow@8743  159 \item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}  nipkow@8743  160 means what you think it means and requires that  nipkow@8743  161 $b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.  nipkow@8743  162 \item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}  nipkow@8743  163 is equivalent to $u$ where all occurrences of $x$ have been replaced by  nipkow@8743  164 $t$. For example,  nipkow@8743  165 \texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated  nipkow@8743  166 by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.  nipkow@8743  167 \item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]  nipkow@8743  168 \indexbold{*case}  nipkow@8743  169 evaluates to $e@i$ if $e$ is of the form  nipkow@8743  170 $c@i$. See~\S\ref{sec:case-expressions} for details.  nipkow@8743  171 \end{description}  nipkow@8743  172 nipkow@8743  173 Terms may also contain  nipkow@8743  174 \isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,  nipkow@8743  175 \texttt{\isasymlambda{}x.~x+1} is the function that takes an argument  nipkow@8743  176 \texttt{x} and returns \texttt{x+1}. Instead of  nipkow@8743  177 \texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$we can write  nipkow@8743  178 \texttt{\isasymlambda{}x~y~z.}~$t$.  nipkow@8743  179 nipkow@8743  180 \textbf{Formulae}\indexbold{formula}  nipkow@8743  181 are terms of type \texttt{bool}. There are the basic  nipkow@8743  182 constants \ttindexbold{True} and \ttindexbold{False} and the usual logical  nipkow@8743  183 connectives (in decreasing order of priority):  nipkow@8743  184 \indexboldpos{\isasymnot}{$HOL0not},  nipkow@8743  185 \indexboldpos{\isasymand}{$HOL0and},  nipkow@8743  186 \indexboldpos{\isasymor}{$HOL0or}, and  nipkow@8743  187 \indexboldpos{\isasymimp}{$HOL0imp},  nipkow@8743  188 all of which (except the unary \isasymnot) associate to the right. In  nipkow@8743  189 particular \texttt{A \isasymimp~B \isasymimp~C} means  nipkow@8743  190 \texttt{A \isasymimp~(B \isasymimp~C)} and is thus  nipkow@8743  191 logically equivalent with \texttt{A \isasymand~B \isasymimp~C}  nipkow@8743  192 (which is \texttt{(A \isasymand~B) \isasymimp~C}).  nipkow@8743  193 nipkow@8743  194 Equality is available in the form of the infix function  nipkow@8743  195 \texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a  nipkow@8743  196  \isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$  nipkow@8743  197 and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type  nipkow@8743  198 \texttt{bool}, \texttt{=} acts as if-and-only-if. The formula  nipkow@8743  199 $t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for  nipkow@8743  200 \texttt{\isasymnot($t@1$ = $t@2$)}.  nipkow@8743  201 nipkow@8743  202 The syntax for quantifiers is  nipkow@8743  203 \texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and  nipkow@8743  204 \texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}. There is  nipkow@8743  205 even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which  nipkow@8743  206 means that there exists exactly one \texttt{x} that satisfies$P$.  nipkow@8743  207 Nested quantifications can be abbreviated:  nipkow@8743  208 \texttt{\isasymforall{}x~y~z.}~$P$means  nipkow@8743  209 \texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$.  nipkow@8743  210 nipkow@8743  211 Despite type inference, it is sometimes necessary to attach explicit  nipkow@8743  212 \bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as  nipkow@8743  213 in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly  nipkow@8743  214 and should therefore be enclosed in parentheses: \texttt{x < y::nat} is  nipkow@8743  215 ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason  nipkow@8743  216 for type constraints are overloaded functions like \texttt{+}, \texttt{*} and  nipkow@8743  217 \texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of  nipkow@8743  218 overloading.)  nipkow@8743  219 nipkow@8743  220 \begin{warn}  nipkow@8743  221 In general, HOL's concrete syntax tries to follow the conventions of  nipkow@8743  222 functional programming and mathematics. Below we list the main rules that you  nipkow@8743  223 should be familiar with to avoid certain syntactic traps. A particular  nipkow@8743  224 problem for novices can be the priority of operators. If you are unsure, use  nipkow@8743  225 more rather than fewer parentheses. In those cases where Isabelle echoes your  nipkow@8743  226 input, you can see which parentheses are dropped---they were superfluous. If  nipkow@8743  227 you are unsure how to interpret Isabelle's output because you don't know  nipkow@8743  228 where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag}  nipkow@8743  229 \ttindexbold{show_brackets}:  nipkow@8743  230 \begin{ttbox}  nipkow@8743  231 ML "set show_brackets"; $$\dots$$; ML "reset show_brackets";  nipkow@8743  232 \end{ttbox}  nipkow@8743  233 \end{warn}  nipkow@8743  234 nipkow@8743  235 \begin{itemize}  nipkow@8743  236 \item  nipkow@8743  237 Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!  nipkow@8743  238 \item  nipkow@8743  239 Isabelle allows infix functions like \texttt{+}. The prefix form of function  nipkow@8743  240 application binds more strongly than anything else and hence \texttt{f~x + y}  nipkow@8743  241 means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.  nipkow@8743  242 \item Remember that in HOL if-and-only-if is expressed using equality. But  nipkow@8743  243  equality has a high priority, as befitting a relation, while if-and-only-if  nipkow@8743  244  typically has the lowest priority. Thus, \texttt{\isasymnot~\isasymnot~P =  nipkow@8743  245  P} means \texttt{\isasymnot\isasymnot(P = P)} and not  nipkow@8743  246  \texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean  nipkow@8743  247  logical equivalence, enclose both operands in parentheses, as in \texttt{(A  nipkow@8743  248  \isasymand~B) = (B \isasymand~A)}.  nipkow@8743  249 \item  nipkow@8743  250 Constructs with an opening but without a closing delimiter bind very weakly  nipkow@8743  251 and should therefore be enclosed in parentheses if they appear in subterms, as  nipkow@8743  252 in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if},  nipkow@8743  253 \ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers.  nipkow@8743  254 \item  nipkow@8743  255 Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x}  nipkow@8743  256 because \texttt{x.x} is always read as a single qualified identifier that  nipkow@8743  257 refers to an item \texttt{x} in theory \texttt{x}. Write  nipkow@8743  258 \texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead.  nipkow@8743  259 \item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}.  nipkow@8743  260 \end{itemize}  nipkow@8743  261 nipkow@8743  262 Remember that ASCII-equivalents of all mathematical symbols are  nipkow@8743  263 given in figure~\ref{fig:ascii} in the appendix.  nipkow@8743  264 nipkow@8743  265 \section{Variables}  nipkow@8743  266 \label{sec:variables}  nipkow@8743  267 \indexbold{variable}  nipkow@8743  268 nipkow@8743  269 Isabelle distinguishes free and bound variables just as is customary. Bound  nipkow@8743  270 variables are automatically renamed to avoid clashes with free variables. In  nipkow@8743  271 addition, Isabelle has a third kind of variable, called a \bfindex{schematic  nipkow@8743  272  variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts  nipkow@8743  273 with a \texttt{?}. Logically, an unknown is a free variable. But it may be  nipkow@8743  274 instantiated by another term during the proof process. For example, the  nipkow@8743  275 mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x},  nipkow@8743  276 which means that Isabelle can instantiate it arbitrarily. This is in contrast  nipkow@8743  277 to ordinary variables, which remain fixed. The programming language Prolog  nipkow@8743  278 calls unknowns {\em logical\/} variables.  nipkow@8743  279 nipkow@8743  280 Most of the time you can and should ignore unknowns and work with ordinary  nipkow@8743  281 variables. Just don't be surprised that after you have finished the proof of  nipkow@8743  282 a theorem, Isabelle will turn your free variables into unknowns: it merely  nipkow@8743  283 indicates that Isabelle will automatically instantiate those unknowns  nipkow@8743  284 suitably when the theorem is used in some other proof.  nipkow@8743  285 \begin{warn}  nipkow@8743  286  If you use \texttt{?}\index{\$HOL0Ex@\texttt{?}} as an existential  nipkow@8743  287  quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is  nipkow@8743  288  interpreted as a schematic variable.  nipkow@8743  289 \end{warn}  nipkow@8743  290 nipkow@8743  291 \section{Getting started}  nipkow@8743  292 nipkow@8743  293 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle  nipkow@8743  294  -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}  nipkow@8743  295  starts the default logic, which usually is already \texttt{HOL}. This is  nipkow@8743  296  controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle  nipkow@8743  297  System Manual} for more details.} This presents you with Isabelle's most  nipkow@8743  298 basic ASCII interface. In addition you need to open an editor window to  nipkow@8743  299 create theory files. While you are developing a theory, we recommend to  nipkow@8743  300 type each command into the file first and then enter it into Isabelle by  nipkow@8743  301 copy-and-paste, thus ensuring that you have a complete record of your theory.  nipkow@8743  302 As mentioned earlier, Proof General offers a much superior interface.