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