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.