doc-src/TutorialI/basics.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/basics.tex	Wed Apr 19 11:54:39 2000 +0200
@@ -0,0 +1,302 @@
+\chapter{Basic Concepts}
+
+\section{Introduction}
+
+This is a tutorial on how to use Isabelle/HOL as a specification and
+verification system. Isabelle is a generic system for implementing logical
+formalisms, and Isabelle/HOL is the specialization of Isabelle for
+HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
+following the equation
+\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
+We assume that the reader is familiar with the basic concepts of both fields.
+For excellent introductions to functional programming consult the textbooks
+by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although
+this tutorial initially concentrates on functional programming, do not be
+misled: HOL can express most mathematical concepts, and functional
+programming is just one particularly simple and ubiquitous instance.
+
+This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref},
+which is an extension of Isabelle~\cite{paulson-isa-book} with structured
+proofs.\footnote{Thus the full name of the system should be
+  Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable
+difference to classical Isabelle (which is the basis of another version of
+this tutorial) is the replacement of the ML level by a dedicated language for
+definitions and proofs.
+
+A tutorial is by definition incomplete.  Currently the tutorial only
+introduces the rudiments of Isar's proof language. To fully exploit the power
+of Isar you need to consult the Isabelle/Isar Reference
+Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
+directly (for example for writing your own proof procedures) see the Isabelle
+Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
+Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
+index.
+
+\section{Theories}
+\label{sec:Basic:Theories}
+
+Working with Isabelle means creating theories. Roughly speaking, a
+\bfindex{theory} is a named collection of types, functions, and theorems,
+much like a module in a programming language or a specification in a
+specification language. In fact, theories in HOL can be either. The general
+format of a theory \texttt{T} is
+\begin{ttbox}
+theory T = B\(@1\) + \(\cdots\) + B\(@n\):
+\(\textit{declarations, definitions, and proofs}\)
+end
+\end{ttbox}
+where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
+theories that \texttt{T} is based on and \texttt{\textit{declarations,
+    definitions, and proofs}} represents the newly introduced concepts
+(types, functions etc) and proofs about them. The \texttt{B}$@i$ are the
+direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
+Everything defined in the parent theories (and their parents \dots) is
+automatically visible. To avoid name clashes, identifiers can be
+\textbf{qualified} by theory names as in \texttt{T.f} and
+\texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
+reside in a \indexbold{theory file} named \texttt{T.thy}.
+
+This tutorial is concerned with introducing you to the different linguistic
+constructs that can fill \textit{\texttt{declarations, definitions, and
+    proofs}} in the above theory template.  A complete grammar of the basic
+constructs is found in the Isabelle/Isar Reference Manual.
+
+HOL's theory library is available online at
+\begin{center}\small
+    \url{http://isabelle.in.tum.de/library/}
+\end{center}
+and is recommended browsing.
+\begin{warn}
+  HOL contains a theory \ttindexbold{Main}, the union of all the basic
+  predefined theories like arithmetic, lists, sets, etc.\ (see the online
+  library).  Unless you know what you are doing, always include \texttt{Main}
+  as a direct or indirect parent theory of all your theories.
+\end{warn}
+
+
+\section{Interaction and interfaces}
+
+Interaction with Isabelle can either occur at the shell level or through more
+advanced interfaces. To keep the tutorial independent of the interface we
+have phrased the description of the intraction in a neutral language. For
+example, the phrase ``to cancel a proof'' means to type \texttt{oops} at the
+shell level, which is explained the first time the phrase is used. Other
+interfaces perform the same act by cursor movements and/or mouse clicks.
+Although shell-based interaction is quite feasible for the kind of proof
+scripts currently presented in this tutorial, the recommended interface for
+Isabelle/Isar is the Emacs-based \bfindex{Proof
+  General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
+
+To improve readability some of the interfaces (including the shell level)
+offer special fonts with mathematical symbols. Therefore the usual
+mathematical symbols are used throughout the tutorial. Their
+ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix.
+
+Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
+for example Proof General, require each command to be terminated by a
+semicolon, whereas others, for example the shell level, do not. But even at
+the shell level it is advisable to use semicolons to enforce that a command
+is executed immediately; otherwise Isabelle may wait for the next keyword
+before it knows that the command is complete. Note that for readibility
+reasons we often drop the final semicolon in the text.
+
+
+\section{Types, terms and formulae}
+\label{sec:TypesTermsForms}
+\indexbold{type}
+
+Embedded in the declarations of a theory are the types, terms and formulae of
+HOL. HOL is a typed logic whose type system resembles that of functional
+programming languages like ML or Haskell. Thus there are
+\begin{description}
+\item[base types,] in particular \ttindex{bool}, the type of truth values,
+and \ttindex{nat}, the type of natural numbers.
+\item[type constructors,] in particular \texttt{list}, the type of
+lists, and \texttt{set}, the type of sets. Type constructors are written
+postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are
+natural numbers. Parentheses around single arguments can be dropped (as in
+\texttt{nat list}), multiple arguments are separated by commas (as in
+\texttt{(bool,nat)foo}).
+\item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
+  In HOL \isasymFun\ represents {\em total} functions only. As is customary,
+  \texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
+  \texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
+  supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
+  which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
+    \isasymFun~$\tau$}.
+\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in
+ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the
+type of the identity function.
+\end{description}
+\begin{warn}
+  Types are extremely important because they prevent us from writing
+  nonsense.  Isabelle insists that all terms and formulae must be well-typed
+  and will print an error message if a type mismatch is encountered. To
+  reduce the amount of explicit type information that needs to be provided by
+  the user, Isabelle infers the type of all variables automatically (this is
+  called \bfindex{type inference}) and keeps quiet about it. Occasionally
+  this may lead to misunderstandings between you and the system. If anything
+  strange happens, we recommend to set the \rmindex{flag}
+  \ttindexbold{show_types} that tells Isabelle to display type information
+  that is usually suppressed: simply type
+\begin{ttbox}
+ML "set show_types"
+\end{ttbox}
+
+\noindent
+This can be reversed by \texttt{ML "reset show_types"}. Various other flags
+can be set and reset in the same manner.\bfindex{flag!(re)setting}
+\end{warn}
+
+
+\textbf{Terms}\indexbold{term} are formed as in functional programming by
+applying functions to arguments. If \texttt{f} is a function of type
+\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type
+$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports
+infix functions like \texttt{+} and some basic constructs from functional
+programming:
+\begin{description}
+\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
+means what you think it means and requires that
+$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.
+\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}
+is equivalent to $u$ where all occurrences of $x$ have been replaced by
+$t$. For example,
+\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated
+by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
+\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
+\indexbold{*case}
+evaluates to $e@i$ if $e$ is of the form
+$c@i$. See~\S\ref{sec:case-expressions} for details.
+\end{description}
+
+Terms may also contain
+\isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,
+\texttt{\isasymlambda{}x.~x+1} is the function that takes an argument
+\texttt{x} and returns \texttt{x+1}. Instead of
+\texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$ we can write
+\texttt{\isasymlambda{}x~y~z.}~$t$.
+
+\textbf{Formulae}\indexbold{formula}
+are terms of type \texttt{bool}. There are the basic
+constants \ttindexbold{True} and \ttindexbold{False} and the usual logical
+connectives (in decreasing order of priority):
+\indexboldpos{\isasymnot}{$HOL0not},
+\indexboldpos{\isasymand}{$HOL0and},
+\indexboldpos{\isasymor}{$HOL0or}, and
+\indexboldpos{\isasymimp}{$HOL0imp},
+all of which (except the unary \isasymnot) associate to the right. In
+particular \texttt{A \isasymimp~B \isasymimp~C} means
+\texttt{A \isasymimp~(B \isasymimp~C)} and is thus
+logically equivalent with \texttt{A \isasymand~B \isasymimp~C}
+(which is \texttt{(A \isasymand~B) \isasymimp~C}).
+
+Equality is available in the form of the infix function
+\texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a
+  \isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$
+and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
+\texttt{bool}, \texttt{=} acts as if-and-only-if. The formula
+$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for
+\texttt{\isasymnot($t@1$ = $t@2$)}.
+
+The syntax for quantifiers is
+\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and
+\texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}.  There is
+even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which
+means that there exists exactly one \texttt{x} that satisfies $P$.
+Nested quantifications can be abbreviated:
+\texttt{\isasymforall{}x~y~z.}~$P$ means
+\texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$.
+
+Despite type inference, it is sometimes necessary to attach explicit
+\bfindex{type constraints} to a term.  The syntax is \texttt{$t$::$\tau$} as
+in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly
+and should therefore be enclosed in parentheses: \texttt{x < y::nat} is
+ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason
+for type constraints are overloaded functions like \texttt{+}, \texttt{*} and
+\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of
+overloading.)
+
+\begin{warn}
+In general, HOL's concrete syntax tries to follow the conventions of
+functional programming and mathematics. Below we list the main rules that you
+should be familiar with to avoid certain syntactic traps. A particular
+problem for novices can be the priority of operators. If you are unsure, use
+more rather than fewer parentheses. In those cases where Isabelle echoes your
+input, you can see which parentheses are dropped---they were superfluous. If
+you are unsure how to interpret Isabelle's output because you don't know
+where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag}
+\ttindexbold{show_brackets}:
+\begin{ttbox}
+ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
+\end{ttbox}
+\end{warn}
+
+\begin{itemize}
+\item
+Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!
+\item
+Isabelle allows infix functions like \texttt{+}. The prefix form of function
+application binds more strongly than anything else and hence \texttt{f~x + y}
+means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.
+\item Remember that in HOL if-and-only-if is expressed using equality.  But
+  equality has a high priority, as befitting a relation, while if-and-only-if
+  typically has the lowest priority.  Thus, \texttt{\isasymnot~\isasymnot~P =
+    P} means \texttt{\isasymnot\isasymnot(P = P)} and not
+  \texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean
+  logical equivalence, enclose both operands in parentheses, as in \texttt{(A
+    \isasymand~B) = (B \isasymand~A)}.
+\item
+Constructs with an opening but without a closing delimiter bind very weakly
+and should therefore be enclosed in parentheses if they appear in subterms, as
+in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if},
+\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers.
+\item
+Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x}
+because \texttt{x.x} is always read as a single qualified identifier that
+refers to an item \texttt{x} in theory \texttt{x}. Write
+\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead.
+\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}.
+\end{itemize}
+
+Remember that ASCII-equivalents of all mathematical symbols are
+given in figure~\ref{fig:ascii} in the appendix.
+
+\section{Variables}
+\label{sec:variables}
+\indexbold{variable}
+
+Isabelle distinguishes free and bound variables just as is customary. Bound
+variables are automatically renamed to avoid clashes with free variables. In
+addition, Isabelle has a third kind of variable, called a \bfindex{schematic
+  variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
+with a \texttt{?}.  Logically, an unknown is a free variable. But it may be
+instantiated by another term during the proof process. For example, the
+mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x},
+which means that Isabelle can instantiate it arbitrarily. This is in contrast
+to ordinary variables, which remain fixed. The programming language Prolog
+calls unknowns {\em logical\/} variables.
+
+Most of the time you can and should ignore unknowns and work with ordinary
+variables. Just don't be surprised that after you have finished the proof of
+a theorem, Isabelle will turn your free variables into unknowns: it merely
+indicates that Isabelle will automatically instantiate those unknowns
+suitably when the theorem is used in some other proof.
+\begin{warn}
+  If you use \texttt{?}\index{$HOL0Ex@\texttt{?}} as an existential
+  quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is
+  interpreted as a schematic variable.
+\end{warn}
+
+\section{Getting started}
+
+Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
+  -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
+  starts the default logic, which usually is already \texttt{HOL}.  This is
+  controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
+    System Manual} for more details.} This presents you with Isabelle's most
+basic ASCII interface.  In addition you need to open an editor window to
+create theory files.  While you are developing a theory, we recommend to
+type each command into the file first and then enter it into Isabelle by
+copy-and-paste, thus ensuring that you have a complete record of your theory.
+As mentioned earlier, Proof General offers a much superior interface.