|
1 \chapter{Basic Concepts} |
|
2 |
|
3 \section{Introduction} |
|
4 |
|
5 This is a tutorial on how to use Isabelle/HOL as a specification and |
|
6 verification system. Isabelle is a generic system for implementing logical |
|
7 formalisms, and Isabelle/HOL is the specialization of Isabelle for |
|
8 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step |
|
9 following the equation |
|
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] |
|
11 We assume that the reader is familiar with the basic concepts of both fields. |
|
12 For excellent introductions to functional programming consult the textbooks |
|
13 by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{Paulson-ML}. Although |
|
14 this tutorial initially concentrates on functional programming, do not be |
|
15 misled: HOL can express most mathematical concepts, and functional |
|
16 programming is just one particularly simple and ubiquitous instance. |
|
17 |
|
18 A tutorial is by definition incomplete. To fully exploit the power of the |
|
19 system you need to consult the Isabelle Reference Manual~\cite{Isa-Ref-Man} |
|
20 for details about Isabelle and the HOL chapter of the Logics |
|
21 manual~\cite{Isa-Logics-Man} for details relating to HOL. Both manuals have a |
|
22 comprehensive index. |
|
23 |
|
24 \section{Theories, proofs and interaction} |
|
25 \label{sec:Basic:Theories} |
|
26 |
|
27 Working with Isabelle means creating two different kinds of documents: |
|
28 theories and proof scripts. Roughly speaking, a \bfindex{theory} is a named |
|
29 collection of types and functions, much like a module in a programming |
|
30 language or a specification in a specification language. In fact, theories in |
|
31 HOL can be either. Theories must reside in files with the suffix |
|
32 \texttt{.thy}. The general format of a theory file \texttt{T.thy} is |
|
33 \begin{ttbox} |
|
34 T = B\(@1\) + \(\cdots\) + B\(@n\) + |
|
35 \({<}declarations{>}\) |
|
36 end |
|
37 \end{ttbox} |
|
38 where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing |
|
39 theories that \texttt{T} is based on and ${<}declarations{>}$ stands for the |
|
40 newly introduced concepts (types, functions etc). The \texttt{B}$@i$ are the |
|
41 direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}. |
|
42 Everything defined in the parent theories (and their parents \dots) is |
|
43 automatically visible. To avoid name clashes, identifiers can be qualified by |
|
44 theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is |
|
45 available online at \verb$http://www.in.tum.de/~isabelle/library/HOL/$ and is |
|
46 recommended browsing. |
|
47 \begin{warn} |
|
48 HOL contains a theory \ttindexbold{Main}, the union of all the basic |
|
49 predefined theories like arithmetic, lists, sets, etc.\ (see the online |
|
50 library). Unless you know what you are doing, always include \texttt{Main} |
|
51 as a direct or indirect parent theory of all your theories. |
|
52 \end{warn} |
|
53 |
|
54 This tutorial is concerned with introducing you to the different linguistic |
|
55 constructs that can fill ${<}declarations{>}$ in the above theory template. |
|
56 A complete grammar of the basic constructs is found in Appendix~A |
|
57 of~\cite{Isa-Ref-Man}, for reference in times of doubt. |
|
58 |
|
59 The tutorial is also concerned with showing you how to prove theorems about |
|
60 the concepts in a theory. This involves invoking predefined theorem proving |
|
61 commands. Because Isabelle is written in the programming language |
|
62 ML,\footnote{Many concepts in HOL and ML are similar. Make sure you do not |
|
63 confuse the two levels.} interacting with Isabelle means calling ML |
|
64 functions. Hence \bfindex{proof scripts} are sequences of calls to ML |
|
65 functions that perform specific theorem proving tasks. Nevertheless, |
|
66 familiarity with ML is absolutely not required. All proof scripts for theory |
|
67 \texttt{T} (defined in file \texttt{T.thy}) should be contained in file |
|
68 \texttt{T.ML}. Theory and proof scripts are loaded (and checked!) by calling |
|
69 the ML function \ttindexbold{use_thy}: |
|
70 \begin{ttbox} |
|
71 use_thy "T"; |
|
72 \end{ttbox} |
|
73 |
|
74 There are more advanced interfaces for Isabelle that hide the ML level from |
|
75 you and replace function calls by menu selection. There is even a special |
|
76 font with mathematical symbols. For details see the Isabelle home page. This |
|
77 tutorial concentrates on the bare essentials and ignores such niceties. |
|
78 |
|
79 \section{Types, terms and formulae} |
|
80 \label{sec:TypesTermsForms} |
|
81 |
|
82 Embedded in the declarations of a theory are the types, terms and formulae of |
|
83 HOL. HOL is a typed logic whose type system resembles that of functional |
|
84 programming languages like ML or Haskell. Thus there are |
|
85 \begin{description} |
|
86 \item[base types,] in particular \ttindex{bool}, the type of truth values, |
|
87 and \ttindex{nat}, the type of natural numbers. |
|
88 \item[type constructors,] in particular \ttindex{list}, the type of |
|
89 lists, and \ttindex{set}, the type of sets. Type constructors are written |
|
90 postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are |
|
91 natural numbers. Parentheses around single arguments can be dropped (as in |
|
92 \texttt{nat list}), multiple arguments are separated by commas (as in |
|
93 \texttt{(bool,nat)foo}). |
|
94 \item[function types,] denoted by \ttindexbold{=>}. In HOL |
|
95 \texttt{=>} represents {\em total} functions only. As is customary, |
|
96 \texttt{$\tau@1$ => $\tau@2$ => $\tau@3$} means |
|
97 \texttt{$\tau@1$ => ($\tau@2$ => $\tau@3$)}. Isabelle also supports the |
|
98 notation \texttt{[$\tau@1,\dots,\tau@n$] => $\tau$} which abbreviates |
|
99 \texttt{$\tau@1$ => $\cdots$ => $\tau@n$ => $\tau$}. |
|
100 \item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in |
|
101 ML. They give rise to polymorphic types like \texttt{'a => 'a}, the type of the |
|
102 identity function. |
|
103 \end{description} |
|
104 \begin{warn} |
|
105 Types are extremely important because they prevent us from writing |
|
106 nonsense. Isabelle insists that all terms and formulae must be well-typed |
|
107 and will print an error message if a type mismatch is encountered. To |
|
108 reduce the amount of explicit type information that needs to be provided by |
|
109 the user, Isabelle infers the type of all variables automatically (this is |
|
110 called \bfindex{type inference}) and keeps quiet about it. Occasionally |
|
111 this may lead to misunderstandings between you and the system. If anything |
|
112 strange happens, we recommend to set the flag \ttindexbold{show_types} that |
|
113 tells Isabelle to display type information that is usually suppressed: |
|
114 simply type |
|
115 \begin{ttbox} |
|
116 set show_types; |
|
117 \end{ttbox} |
|
118 |
|
119 \noindent |
|
120 at the ML-level. This can be reversed by \texttt{reset show_types;}. |
|
121 \end{warn} |
|
122 |
|
123 |
|
124 \textbf{Terms}\indexbold{term} |
|
125 are formed as in functional programming by applying functions to |
|
126 arguments. If \texttt{f} is a function of type \texttt{$\tau@1$ => $\tau@2$} |
|
127 and \texttt{t} is a term of type $\tau@1$ then \texttt{f~t} is a term of type |
|
128 $\tau@2$. HOL also supports infix functions like \texttt{+} and some basic |
|
129 constructs from functional programming: |
|
130 \begin{description} |
|
131 \item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if} |
|
132 means what you think it means and requires that |
|
133 $b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type. |
|
134 \item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let} |
|
135 is equivalent to $u$ where all occurrences of $x$ have been replaced by |
|
136 $t$. For example, |
|
137 \texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated |
|
138 by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}. |
|
139 \item[\texttt{case $e$ of $c@1$ => $e@1$ | \dots | $c@n$ => $e@n$}] |
|
140 \indexbold{*case} |
|
141 evaluates to $e@i$ if $e$ is of the form |
|
142 $c@i$. See~\S\ref{sec:case-expressions} for details. |
|
143 \end{description} |
|
144 |
|
145 Terms may also contain $\lambda$-abstractions. For example, $\lambda |
|
146 x. x+1$ is the function that takes an argument $x$ and returns $x+1$. In |
|
147 Isabelle we write \texttt{\%x.~x+1}.\index{==>@{\tt\%}|bold} |
|
148 Instead of \texttt{\%x.~\%y.~\%z.~t} we can write \texttt{\%x~y~z.~t}. |
|
149 |
|
150 \textbf{Formulae}\indexbold{formula} |
|
151 are terms of type \texttt{bool}. There are the basic |
|
152 constants \ttindexbold{True} and \ttindexbold{False} and the usual logical |
|
153 connectives (in decreasing order of priority): |
|
154 \verb$~$\index{$HOL1@{\ttnot}|bold} (`not'), |
|
155 \texttt{\&}\index{$HOL2@{\tt\&}|bold} (`and'), |
|
156 \texttt{|}\index{$HOL2@{\ttor}|bold} (`or') and |
|
157 \texttt{-->}\index{$HOL2@{\tt-->}|bold} (`implies'), |
|
158 all of which (except the unary \verb$~$) associate to the right. In |
|
159 particular \texttt{A --> B --> C} means \texttt{A --> (B --> C)} and is thus |
|
160 logically equivalent with \texttt{A \& B --> C} |
|
161 (which is \texttt{(A \& B) --> C}). |
|
162 |
|
163 Equality is available in the form of the infix function |
|
164 \texttt{=} of type \texttt{'a => 'a => bool}. Thus \texttt{$t@1$ = $t@2$} is |
|
165 a formula provided $t@1$ and $t@2$ are terms of the same type. In case $t@1$ |
|
166 and $t@2$ are of type \texttt{bool}, \texttt{=} acts as if-and-only-if. |
|
167 |
|
168 The syntax for quantifiers is |
|
169 \texttt{!~$x$.$\,P$}\index{$HOLQ@{\ttall}|bold} (`for all $x$') and |
|
170 \texttt{?~$x$.$\,P$}\index{$HOLQ@{\tt?}|bold} (`exists $x$'). |
|
171 There is even \texttt{?!~$x$.$\,P$}\index{$HOLQ@{\ttuniquex}|bold}, which |
|
172 means that there exists exactly one $x$ that satisfies $P$. Instead of |
|
173 \texttt{!} and \texttt{?} you may also write \texttt{ALL} and \texttt{EX}. |
|
174 Nested quantifications can be abbreviated: |
|
175 \texttt{!$x~y~z$.$\,P$} means \texttt{!$x$.~!$y$.~!$z$.$\,P$}. |
|
176 |
|
177 Despite type inference, it is sometimes necessary to attach explicit |
|
178 \bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as |
|
179 in \texttt{x < (y::nat)}. Note that \texttt{::} binds weakly and should |
|
180 therefore be enclosed in parentheses: \texttt{x < y::nat} is ill-typed |
|
181 because it is interpreted as \texttt{(x < y)::nat}. The main reason for type |
|
182 constraints are overloaded functions like \texttt{+}, \texttt{*} and |
|
183 \texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of |
|
184 overloading.) |
|
185 |
|
186 \begin{warn} |
|
187 In general, HOL's concrete syntax tries to follow the conventions of |
|
188 functional programming and mathematics. Below we list the main rules that you |
|
189 should be familiar with to avoid certain syntactic traps. A particular |
|
190 problem for novices can be the priority of operators. If you are unsure, use |
|
191 more rather than fewer parentheses. In those cases where Isabelle echoes your |
|
192 input, you can see which parentheses are dropped---they were superfluous. If |
|
193 you are unsure how to interpret Isabelle's output because you don't know |
|
194 where the (dropped) parentheses go, set (and possibly reset) the flag |
|
195 \ttindexbold{show_brackets}: |
|
196 \begin{ttbox} |
|
197 set show_brackets; \(\dots\); reset show_brackets; |
|
198 \end{ttbox} |
|
199 \end{warn} |
|
200 |
|
201 \begin{itemize} |
|
202 \item |
|
203 Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}! |
|
204 \item |
|
205 Isabelle allows infix functions like \texttt{+}. The prefix form of function |
|
206 application binds more strongly than anything else and hence \texttt{f~x + y} |
|
207 means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}. |
|
208 \item |
|
209 Remember that in HOL if-and-only-if is expressed using equality. But equality |
|
210 has a high priority, as befitting a relation, while if-and-only-if typically |
|
211 has the lowest priority. Thus, \verb$~ ~ P = P$ means \verb$~ ~(P = P)$ and |
|
212 not \verb$(~ ~P) = P$. When using \texttt{=} to mean logical equivalence, |
|
213 enclose both operands in parentheses, as in \texttt{(A \& B) = (B \& A)}. |
|
214 \item |
|
215 Constructs with an opening but without a closing delimiter bind very weakly |
|
216 and should therefore be enclosed in parentheses if they appear in subterms, as |
|
217 in \texttt{f = (\%x.~x)}. This includes |
|
218 \ttindex{if}, \ttindex{let}, \ttindex{case}, \verb$%$ and quantifiers. |
|
219 \item |
|
220 Never write \texttt{\%x.x} or \texttt{!x.x=x} because \texttt{x.x} is always |
|
221 read as a single qualified identifier that refers to an item \texttt{x} in |
|
222 theory \texttt{x}. Write \texttt{\%x.~x} and \texttt{!x.~x=x} instead. |
|
223 \end{itemize} |
|
224 |
|
225 \section{Variables} |
|
226 \label{sec:variables} |
|
227 |
|
228 Isabelle distinguishes free and bound variables just as is customary. Bound |
|
229 variables are automatically renamed to avoid clashes with free variables. In |
|
230 addition, Isabelle has a third kind of variable, called a \bfindex{schematic |
|
231 variable} or \bfindex{unknown}, which starts with a \texttt{?}. Logically, |
|
232 an unknown is a free variable. But it may be instantiated by another term |
|
233 during the proof process. For example, the mathematical theorem $x = x$ is |
|
234 represented in Isabelle as \texttt{?x = ?x}, which means that Isabelle can |
|
235 instantiate it arbitrarily. This is in contrast to ordinary variables, which |
|
236 remain fixed. The programming language Prolog calls unknowns {\em logical\/} |
|
237 variables. |
|
238 |
|
239 Most of the time you can and should ignore unknowns and work with ordinary |
|
240 variables. Just don't be surprised that after you have finished the |
|
241 proof of a theorem, Isabelle will turn your free variables into unknowns: it |
|
242 merely indicates that Isabelle will automatically instantiate those unknowns |
|
243 suitably when the theorem is used in some other proof. |
|
244 \begin{warn} |
|
245 The existential quantifier \texttt{?}\index{$HOLQ@{\tt?}} needs to be |
|
246 followed by a space. Otherwise \texttt{?x} is interpreted as a schematic |
|
247 variable. |
|
248 \end{warn} |
|
249 |
|
250 \section{Getting started} |
|
251 |
|
252 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle |
|
253 HOL} in a shell window.\footnote{Since you will always want to use HOL when |
|
254 studying this tutorial, you can set the shell variable |
|
255 \texttt{ISABELLE_LOGIC} to \texttt{HOL} once and for all and simply execute |
|
256 \texttt{isabelle}.} This presents you with Isabelle's most basic ASCII |
|
257 interface. In addition you need to open an editor window to create theories |
|
258 (\texttt{.thy} files) and proof scripts (\texttt{.ML} files). While you are |
|
259 developing a proof, we recommend to type each proof command into the ML-file |
|
260 first and then enter it into Isabelle by copy-and-paste, thus ensuring that |
|
261 you have a complete record of your proof. |