1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Tutorial/basics.tex Wed Aug 26 16:57:49 1998 +0200
1.3 @@ -0,0 +1,261 @@
1.4 +\chapter{Basic Concepts}
1.5 +
1.6 +\section{Introduction}
1.7 +
1.8 +This is a tutorial on how to use Isabelle/HOL as a specification and
1.9 +verification system. Isabelle is a generic system for implementing logical
1.10 +formalisms, and Isabelle/HOL is the specialization of Isabelle for
1.11 +HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
1.12 +following the equation
1.13 +\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
1.14 +We assume that the reader is familiar with the basic concepts of both fields.
1.15 +For excellent introductions to functional programming consult the textbooks
1.16 +by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{Paulson-ML}. Although
1.17 +this tutorial initially concentrates on functional programming, do not be
1.18 +misled: HOL can express most mathematical concepts, and functional
1.19 +programming is just one particularly simple and ubiquitous instance.
1.20 +
1.21 +A tutorial is by definition incomplete. To fully exploit the power of the
1.22 +system you need to consult the Isabelle Reference Manual~\cite{Isa-Ref-Man}
1.23 +for details about Isabelle and the HOL chapter of the Logics
1.24 +manual~\cite{Isa-Logics-Man} for details relating to HOL. Both manuals have a
1.25 +comprehensive index.
1.26 +
1.27 +\section{Theories, proofs and interaction}
1.28 +\label{sec:Basic:Theories}
1.29 +
1.30 +Working with Isabelle means creating two different kinds of documents:
1.31 +theories and proof scripts. Roughly speaking, a \bfindex{theory} is a named
1.32 +collection of types and functions, much like a module in a programming
1.33 +language or a specification in a specification language. In fact, theories in
1.34 +HOL can be either. Theories must reside in files with the suffix
1.35 +\texttt{.thy}. The general format of a theory file \texttt{T.thy} is
1.36 +\begin{ttbox}
1.37 +T = B\(@1\) + \(\cdots\) + B\(@n\) +
1.38 +\({<}declarations{>}\)
1.39 +end
1.40 +\end{ttbox}
1.41 +where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
1.42 +theories that \texttt{T} is based on and ${<}declarations{>}$ stands for the
1.43 +newly introduced concepts (types, functions etc). The \texttt{B}$@i$ are the
1.44 +direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
1.45 +Everything defined in the parent theories (and their parents \dots) is
1.46 +automatically visible. To avoid name clashes, identifiers can be qualified by
1.47 +theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is
1.48 +available online at \verb$http://www.in.tum.de/~isabelle/library/HOL/$ and is
1.49 +recommended browsing.
1.50 +\begin{warn}
1.51 + HOL contains a theory \ttindexbold{Main}, the union of all the basic
1.52 + predefined theories like arithmetic, lists, sets, etc.\ (see the online
1.53 + library). Unless you know what you are doing, always include \texttt{Main}
1.54 + as a direct or indirect parent theory of all your theories.
1.55 +\end{warn}
1.56 +
1.57 +This tutorial is concerned with introducing you to the different linguistic
1.58 +constructs that can fill ${<}declarations{>}$ in the above theory template.
1.59 +A complete grammar of the basic constructs is found in Appendix~A
1.60 +of~\cite{Isa-Ref-Man}, for reference in times of doubt.
1.61 +
1.62 +The tutorial is also concerned with showing you how to prove theorems about
1.63 +the concepts in a theory. This involves invoking predefined theorem proving
1.64 +commands. Because Isabelle is written in the programming language
1.65 +ML,\footnote{Many concepts in HOL and ML are similar. Make sure you do not
1.66 + confuse the two levels.} interacting with Isabelle means calling ML
1.67 +functions. Hence \bfindex{proof scripts} are sequences of calls to ML
1.68 +functions that perform specific theorem proving tasks. Nevertheless,
1.69 +familiarity with ML is absolutely not required. All proof scripts for theory
1.70 +\texttt{T} (defined in file \texttt{T.thy}) should be contained in file
1.71 +\texttt{T.ML}. Theory and proof scripts are loaded (and checked!) by calling
1.72 +the ML function \ttindexbold{use_thy}:
1.73 +\begin{ttbox}
1.74 +use_thy "T";
1.75 +\end{ttbox}
1.76 +
1.77 +There are more advanced interfaces for Isabelle that hide the ML level from
1.78 +you and replace function calls by menu selection. There is even a special
1.79 +font with mathematical symbols. For details see the Isabelle home page. This
1.80 +tutorial concentrates on the bare essentials and ignores such niceties.
1.81 +
1.82 +\section{Types, terms and formulae}
1.83 +\label{sec:TypesTermsForms}
1.84 +
1.85 +Embedded in the declarations of a theory are the types, terms and formulae of
1.86 +HOL. HOL is a typed logic whose type system resembles that of functional
1.87 +programming languages like ML or Haskell. Thus there are
1.88 +\begin{description}
1.89 +\item[base types,] in particular \ttindex{bool}, the type of truth values,
1.90 +and \ttindex{nat}, the type of natural numbers.
1.91 +\item[type constructors,] in particular \ttindex{list}, the type of
1.92 +lists, and \ttindex{set}, the type of sets. Type constructors are written
1.93 +postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are
1.94 +natural numbers. Parentheses around single arguments can be dropped (as in
1.95 +\texttt{nat list}), multiple arguments are separated by commas (as in
1.96 +\texttt{(bool,nat)foo}).
1.97 +\item[function types,] denoted by \ttindexbold{=>}. In HOL
1.98 +\texttt{=>} represents {\em total} functions only. As is customary,
1.99 +\texttt{$\tau@1$ => $\tau@2$ => $\tau@3$} means
1.100 +\texttt{$\tau@1$ => ($\tau@2$ => $\tau@3$)}. Isabelle also supports the
1.101 +notation \texttt{[$\tau@1,\dots,\tau@n$] => $\tau$} which abbreviates
1.102 +\texttt{$\tau@1$ => $\cdots$ => $\tau@n$ => $\tau$}.
1.103 +\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in
1.104 +ML. They give rise to polymorphic types like \texttt{'a => 'a}, the type of the
1.105 +identity function.
1.106 +\end{description}
1.107 +\begin{warn}
1.108 + Types are extremely important because they prevent us from writing
1.109 + nonsense. Isabelle insists that all terms and formulae must be well-typed
1.110 + and will print an error message if a type mismatch is encountered. To
1.111 + reduce the amount of explicit type information that needs to be provided by
1.112 + the user, Isabelle infers the type of all variables automatically (this is
1.113 + called \bfindex{type inference}) and keeps quiet about it. Occasionally
1.114 + this may lead to misunderstandings between you and the system. If anything
1.115 + strange happens, we recommend to set the flag \ttindexbold{show_types} that
1.116 + tells Isabelle to display type information that is usually suppressed:
1.117 + simply type
1.118 +\begin{ttbox}
1.119 +set show_types;
1.120 +\end{ttbox}
1.121 +
1.122 +\noindent
1.123 +at the ML-level. This can be reversed by \texttt{reset show_types;}.
1.124 +\end{warn}
1.125 +
1.126 +
1.127 +\textbf{Terms}\indexbold{term}
1.128 +are formed as in functional programming by applying functions to
1.129 +arguments. If \texttt{f} is a function of type \texttt{$\tau@1$ => $\tau@2$}
1.130 +and \texttt{t} is a term of type $\tau@1$ then \texttt{f~t} is a term of type
1.131 +$\tau@2$. HOL also supports infix functions like \texttt{+} and some basic
1.132 +constructs from functional programming:
1.133 +\begin{description}
1.134 +\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
1.135 +means what you think it means and requires that
1.136 +$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.
1.137 +\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}
1.138 +is equivalent to $u$ where all occurrences of $x$ have been replaced by
1.139 +$t$. For example,
1.140 +\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated
1.141 +by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
1.142 +\item[\texttt{case $e$ of $c@1$ => $e@1$ | \dots | $c@n$ => $e@n$}]
1.143 +\indexbold{*case}
1.144 +evaluates to $e@i$ if $e$ is of the form
1.145 +$c@i$. See~\S\ref{sec:case-expressions} for details.
1.146 +\end{description}
1.147 +
1.148 +Terms may also contain $\lambda$-abstractions. For example, $\lambda
1.149 +x. x+1$ is the function that takes an argument $x$ and returns $x+1$. In
1.150 +Isabelle we write \texttt{\%x.~x+1}.\index{==>@{\tt\%}|bold}
1.151 +Instead of \texttt{\%x.~\%y.~\%z.~t} we can write \texttt{\%x~y~z.~t}.
1.152 +
1.153 +\textbf{Formulae}\indexbold{formula}
1.154 +are terms of type \texttt{bool}. There are the basic
1.155 +constants \ttindexbold{True} and \ttindexbold{False} and the usual logical
1.156 +connectives (in decreasing order of priority):
1.157 +\verb$~$\index{$HOL1@{\ttnot}|bold} (`not'),
1.158 +\texttt{\&}\index{$HOL2@{\tt\&}|bold} (`and'),
1.159 +\texttt{|}\index{$HOL2@{\ttor}|bold} (`or') and
1.160 +\texttt{-->}\index{$HOL2@{\tt-->}|bold} (`implies'),
1.161 +all of which (except the unary \verb$~$) associate to the right. In
1.162 +particular \texttt{A --> B --> C} means \texttt{A --> (B --> C)} and is thus
1.163 +logically equivalent with \texttt{A \& B --> C}
1.164 +(which is \texttt{(A \& B) --> C}).
1.165 +
1.166 +Equality is available in the form of the infix function
1.167 +\texttt{=} of type \texttt{'a => 'a => bool}. Thus \texttt{$t@1$ = $t@2$} is
1.168 +a formula provided $t@1$ and $t@2$ are terms of the same type. In case $t@1$
1.169 +and $t@2$ are of type \texttt{bool}, \texttt{=} acts as if-and-only-if.
1.170 +
1.171 +The syntax for quantifiers is
1.172 +\texttt{!~$x$.$\,P$}\index{$HOLQ@{\ttall}|bold} (`for all $x$') and
1.173 +\texttt{?~$x$.$\,P$}\index{$HOLQ@{\tt?}|bold} (`exists $x$').
1.174 +There is even \texttt{?!~$x$.$\,P$}\index{$HOLQ@{\ttuniquex}|bold}, which
1.175 +means that there exists exactly one $x$ that satisfies $P$. Instead of
1.176 +\texttt{!} and \texttt{?} you may also write \texttt{ALL} and \texttt{EX}.
1.177 +Nested quantifications can be abbreviated:
1.178 +\texttt{!$x~y~z$.$\,P$} means \texttt{!$x$.~!$y$.~!$z$.$\,P$}.
1.179 +
1.180 +Despite type inference, it is sometimes necessary to attach explicit
1.181 +\bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as
1.182 +in \texttt{x < (y::nat)}. Note that \texttt{::} binds weakly and should
1.183 +therefore be enclosed in parentheses: \texttt{x < y::nat} is ill-typed
1.184 +because it is interpreted as \texttt{(x < y)::nat}. The main reason for type
1.185 +constraints are overloaded functions like \texttt{+}, \texttt{*} and
1.186 +\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of
1.187 +overloading.)
1.188 +
1.189 +\begin{warn}
1.190 +In general, HOL's concrete syntax tries to follow the conventions of
1.191 +functional programming and mathematics. Below we list the main rules that you
1.192 +should be familiar with to avoid certain syntactic traps. A particular
1.193 +problem for novices can be the priority of operators. If you are unsure, use
1.194 +more rather than fewer parentheses. In those cases where Isabelle echoes your
1.195 +input, you can see which parentheses are dropped---they were superfluous. If
1.196 +you are unsure how to interpret Isabelle's output because you don't know
1.197 +where the (dropped) parentheses go, set (and possibly reset) the flag
1.198 +\ttindexbold{show_brackets}:
1.199 +\begin{ttbox}
1.200 +set show_brackets; \(\dots\); reset show_brackets;
1.201 +\end{ttbox}
1.202 +\end{warn}
1.203 +
1.204 +\begin{itemize}
1.205 +\item
1.206 +Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!
1.207 +\item
1.208 +Isabelle allows infix functions like \texttt{+}. The prefix form of function
1.209 +application binds more strongly than anything else and hence \texttt{f~x + y}
1.210 +means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.
1.211 +\item
1.212 +Remember that in HOL if-and-only-if is expressed using equality. But equality
1.213 +has a high priority, as befitting a relation, while if-and-only-if typically
1.214 +has the lowest priority. Thus, \verb$~ ~ P = P$ means \verb$~ ~(P = P)$ and
1.215 +not \verb$(~ ~P) = P$. When using \texttt{=} to mean logical equivalence,
1.216 +enclose both operands in parentheses, as in \texttt{(A \& B) = (B \& A)}.
1.217 +\item
1.218 +Constructs with an opening but without a closing delimiter bind very weakly
1.219 +and should therefore be enclosed in parentheses if they appear in subterms, as
1.220 +in \texttt{f = (\%x.~x)}. This includes
1.221 +\ttindex{if}, \ttindex{let}, \ttindex{case}, \verb$%$ and quantifiers.
1.222 +\item
1.223 +Never write \texttt{\%x.x} or \texttt{!x.x=x} because \texttt{x.x} is always
1.224 +read as a single qualified identifier that refers to an item \texttt{x} in
1.225 +theory \texttt{x}. Write \texttt{\%x.~x} and \texttt{!x.~x=x} instead.
1.226 +\end{itemize}
1.227 +
1.228 +\section{Variables}
1.229 +\label{sec:variables}
1.230 +
1.231 +Isabelle distinguishes free and bound variables just as is customary. Bound
1.232 +variables are automatically renamed to avoid clashes with free variables. In
1.233 +addition, Isabelle has a third kind of variable, called a \bfindex{schematic
1.234 + variable} or \bfindex{unknown}, which starts with a \texttt{?}. Logically,
1.235 +an unknown is a free variable. But it may be instantiated by another term
1.236 +during the proof process. For example, the mathematical theorem $x = x$ is
1.237 +represented in Isabelle as \texttt{?x = ?x}, which means that Isabelle can
1.238 +instantiate it arbitrarily. This is in contrast to ordinary variables, which
1.239 +remain fixed. The programming language Prolog calls unknowns {\em logical\/}
1.240 +variables.
1.241 +
1.242 +Most of the time you can and should ignore unknowns and work with ordinary
1.243 +variables. Just don't be surprised that after you have finished the
1.244 +proof of a theorem, Isabelle will turn your free variables into unknowns: it
1.245 +merely indicates that Isabelle will automatically instantiate those unknowns
1.246 +suitably when the theorem is used in some other proof.
1.247 +\begin{warn}
1.248 + The existential quantifier \texttt{?}\index{$HOLQ@{\tt?}} needs to be
1.249 + followed by a space. Otherwise \texttt{?x} is interpreted as a schematic
1.250 + variable.
1.251 +\end{warn}
1.252 +
1.253 +\section{Getting started}
1.254 +
1.255 +Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
1.256 + HOL} in a shell window.\footnote{Since you will always want to use HOL when
1.257 + studying this tutorial, you can set the shell variable
1.258 + \texttt{ISABELLE_LOGIC} to \texttt{HOL} once and for all and simply execute
1.259 + \texttt{isabelle}.} This presents you with Isabelle's most basic ASCII
1.260 +interface. In addition you need to open an editor window to create theories
1.261 +(\texttt{.thy} files) and proof scripts (\texttt{.ML} files). While you are
1.262 +developing a proof, we recommend to type each proof command into the ML-file
1.263 +first and then enter it into Isabelle by copy-and-paste, thus ensuring that
1.264 +you have a complete record of your proof.