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