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