--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/basics.tex Tue Aug 28 14:37:57 2012 +0200
@@ -0,0 +1,350 @@
+\chapter{The Basics}
+
+\section{Introduction}
+
+This book is a tutorial on how to use the theorem prover 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 do not assume that you are familiar with mathematical logic.
+However, we do assume that
+you are used to logical and set theoretic notation, as covered
+in a good discrete mathematics course~\cite{Rosen-DMA}, and
+that you are familiar with the basic concepts of functional
+programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
+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.
+
+Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has
+influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant
+for us: this tutorial is based on
+Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides
+the implementation language almost completely. Thus the full name of the
+system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.
+
+There are other implementations of HOL, in particular the one by Mike Gordon
+\index{Gordon, Mike}%
+\emph{et al.}, which is usually referred to as ``the HOL system''
+\cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes
+its incarnation Isabelle/HOL\@.
+
+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, in particular the ability to write readable and structured proofs,
+you should start with Nipkow's overview~\cite{Nipkow-TYPES02} and consult
+the Isabelle/Isar Reference Manual~\cite{isabelle-isar-ref} and Wenzel's
+PhD thesis~\cite{Wenzel-PhD} (which discusses many proof patterns)
+for further details. 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}
+
+\index{theories|(}%
+Working with Isabelle means creating theories. Roughly speaking, a
+\textbf{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
+imports B\(@1\) \(\ldots\) B\(@n\)
+begin
+{\rmfamily\textit{declarations, definitions, and proofs}}
+end
+\end{ttbox}\cmmdx{theory}\cmmdx{imports}
+where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing
+theories that \texttt{T} is based on and \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 theories} of~\texttt{T}\@.
+Everything defined in the parent theories (and their parents, recursively) is
+automatically visible. To avoid name clashes, identifiers can be
+\textbf{qualified}\indexbold{identifiers!qualified}
+by theory names as in \texttt{T.f} and~\texttt{B.f}.
+Each theory \texttt{T} must
+reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}.
+
+This tutorial is concerned with introducing you to the different linguistic
+constructs that can fill the \textit{declarations, definitions, and
+ proofs} above. A complete grammar of the basic
+constructs is found in the Isabelle/Isar Reference
+Manual~\cite{isabelle-isar-ref}.
+
+\begin{warn}
+ HOL contains a theory \thydx{Main}, the union of all the basic
+ predefined theories like arithmetic, lists, sets, etc.
+ Unless you know what you are doing, always include \isa{Main}
+ as a direct or indirect parent of all your theories.
+\end{warn}
+HOL's theory collection is available online at
+\begin{center}\small
+ \url{http://isabelle.in.tum.de/library/HOL/}
+\end{center}
+and is recommended browsing. In subdirectory \texttt{Library} you find
+a growing library of useful theories that are not part of \isa{Main}
+but can be included among the parents of a theory and will then be
+loaded automatically.
+
+For the more adventurous, there is the \emph{Archive of Formal Proofs},
+a journal-like collection of more advanced Isabelle theories:
+\begin{center}\small
+ \url{http://afp.sourceforge.net/}
+\end{center}
+We hope that you will contribute to it yourself one day.%
+\index{theories|)}
+
+
+\section{Types, Terms and Formulae}
+\label{sec:TypesTermsForms}
+
+Embedded in 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
+\index{types|(}
+\begin{description}
+\item[base types,]
+in particular \tydx{bool}, the type of truth values,
+and \tydx{nat}, the type of natural numbers.
+\item[type constructors,]\index{type constructors}
+ in particular \tydx{list}, the type of
+lists, and \tydx{set}, the type of sets. Type constructors are written
+postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
+natural numbers. Parentheses around single arguments can be dropped (as in
+\isa{nat list}), multiple arguments are separated by commas (as in
+\isa{(bool,nat)ty}).
+\item[function types,]\index{function types}
+denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
+ In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
+ \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
+ \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
+ supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
+ which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
+ \isasymFun~$\tau$}.
+\item[type variables,]\index{type variables}\index{variables!type}
+ denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
+ to polymorphic types like \isa{'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 that you ask Isabelle to display all type
+ information via the Proof General menu item \pgmenu{Isabelle} $>$
+ \pgmenu{Settings} $>$ \pgmenu{Show Types} (see \S\ref{sec:interface}
+ for details).
+\end{warn}%
+\index{types|)}
+
+
+\index{terms|(}
+\textbf{Terms} are formed as in functional programming by
+applying functions to arguments. If \isa{f} is a function of type
+\isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
+$\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
+infix functions like \isa{+} and some basic constructs from functional
+programming, such as conditional expressions:
+\begin{description}
+\item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}
+Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
+\item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}
+is equivalent to $u$ where all free occurrences of $x$ have been replaced by
+$t$. For example,
+\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
+by semicolons: \isa{let $x@1$ = $t@1$;\dots; $x@n$ = $t@n$ in $u$}.
+\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
+\index{*case expressions}
+evaluates to $e@i$ if $e$ is of the form $c@i$.
+\end{description}
+
+Terms may also contain
+\isasymlambda-abstractions.\index{lambda@$\lambda$ expressions}
+For example,
+\isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
+returns \isa{x+1}. Instead of
+\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
+\isa{\isasymlambda{}x~y~z.~$t$}.%
+\index{terms|)}
+
+\index{formulae|(}%
+\textbf{Formulae} are terms of type \tydx{bool}.
+There are the basic constants \cdx{True} and \cdx{False} and
+the usual logical connectives (in decreasing order of priority):
+\indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
+\indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
+all of which (except the unary \isasymnot) associate to the right. In
+particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
+ \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
+ \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
+
+Equality\index{equality} is available in the form of the infix function
+\isa{=} of type \isa{'a \isasymFun~'a
+ \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
+and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type
+\isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}.
+The formula
+\isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
+\isa{\isasymnot($t@1$ = $t@2$)}.
+
+Quantifiers\index{quantifiers} are written as
+\isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}.
+There is even
+\isa{\isasymuniqex{}x.~$P$}, which
+means that there exists exactly one \isa{x} that satisfies \isa{$P$}.
+Nested quantifications can be abbreviated:
+\isa{\isasymforall{}x~y~z.~$P$} means
+\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.%
+\index{formulae|)}
+
+Despite type inference, it is sometimes necessary to attach explicit
+\bfindex{type constraints} to a term. The syntax is
+\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
+\ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
+in parentheses. For instance,
+\isa{x < y::nat} is ill-typed because it is interpreted as
+\isa{(x < y)::nat}. Type constraints may be needed to disambiguate
+expressions
+involving overloaded functions such as~\isa{+},
+\isa{*} and~\isa{<}. Section~\ref{sec:overloading}
+discusses overloading, while Table~\ref{tab:overloading} presents the most
+important overloaded function symbols.
+
+In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of
+functional programming and mathematics. Here are the main rules that you
+should be familiar with to avoid certain syntactic traps:
+\begin{itemize}
+\item
+Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
+\item
+Isabelle allows infix functions like \isa{+}. The prefix form of function
+application binds more strongly than anything else and hence \isa{f~x + y}
+means \isa{(f~x)~+~y} and not \isa{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, \isa{\isasymnot~\isasymnot~P =
+ P} means \isa{\isasymnot\isasymnot(P = P)} and not
+ \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
+ logical equivalence, enclose both operands in parentheses, as in \isa{(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 \isa{(\isasymlambda{}x.~x) = f}. This includes
+\isa{if},\index{*if expressions}
+\isa{let},\index{*let expressions}
+\isa{case},\index{*case expressions}
+\isa{\isasymlambda}, and quantifiers.
+\item
+Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
+because \isa{x.x} is always taken as a single qualified identifier. Write
+\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
+\item Identifiers\indexbold{identifiers} may contain the characters \isa{_}
+and~\isa{'}, except at the beginning.
+\end{itemize}
+
+For the sake of readability, we use the usual mathematical symbols throughout
+the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
+the appendix.
+
+\begin{warn}
+A particular problem for novices can be the priority of operators. If
+you are unsure, use additional 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 the Proof General flag \pgmenu{Isabelle} $>$
+\pgmenu{Settings} $>$ \pgmenu{Show Brackets} (see \S\ref{sec:interface}).
+\end{warn}
+
+
+\section{Variables}
+\label{sec:variables}
+\index{variables|(}
+
+Isabelle distinguishes free and bound variables, 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 \textbf{schematic
+ variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns},
+which must have a~\isa{?} as its first character.
+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 \isa{?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
+indicates that Isabelle will automatically instantiate those unknowns
+suitably when the theorem is used in some other proof.
+Note that for readability we often drop the \isa{?}s when displaying a theorem.
+\begin{warn}
+ For historical reasons, Isabelle accepts \isa{?} as an ASCII representation
+ of the \(\exists\) symbol. However, the \isa{?} character must then be followed
+ by a space, as in \isa{?~x. f(x) = 0}. Otherwise, \isa{?x} is
+ interpreted as a schematic variable. The preferred ASCII representation of
+ the \(\exists\) symbol is \isa{EX}\@.
+\end{warn}%
+\index{variables|)}
+
+\section{Interaction and Interfaces}
+\label{sec:interface}
+
+The recommended interface for Isabelle/Isar is the (X)Emacs-based
+\bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
+Interaction with Isabelle at the shell level, although possible,
+should be avoided. Most of the tutorial is independent of the
+interface and is phrased in a neutral language. For example, the
+phrase ``to abandon a proof'' corresponds to the obvious
+action of clicking on the \pgmenu{Undo} symbol in Proof General.
+Proof General specific information is often displayed in paragraphs
+identified by a miniature Proof General icon. Here are two examples:
+\begin{pgnote}
+Proof General supports a special font with mathematical symbols known
+as ``x-symbols''. All symbols have \textsc{ascii}-equivalents: for
+example, you can enter either \verb!&! or \verb!\<and>! to obtain
+$\land$. For a list of the most frequent symbols see table~\ref{tab:ascii}
+in the appendix.
+
+Note that by default x-symbols are not enabled. You have to switch
+them on via the menu item \pgmenu{Proof-General} $>$ \pgmenu{Options} $>$
+\pgmenu{X-Symbols} (and save the option via the top-level
+\pgmenu{Options} menu).
+\end{pgnote}
+
+\begin{pgnote}
+Proof General offers the \pgmenu{Isabelle} menu for displaying
+information and setting flags. A particularly useful flag is
+\pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgdx{Show Types} which
+causes Isabelle to output the type information that is usually
+suppressed. This is indispensible in case of errors of all kinds
+because often the types reveal the source of the problem. Once you
+have diagnosed the problem you may no longer want to see the types
+because they clutter all output. Simply reset the flag.
+\end{pgnote}
+
+\section{Getting Started}
+
+Assuming you have installed Isabelle and Proof General, you start it by typing
+\texttt{Isabelle} in a shell window. This launches a Proof General window.
+By default, you are in HOL\footnote{This is controlled by the
+\texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual}
+for more details.}.
+
+\begin{pgnote}
+You can choose a different logic via the \pgmenu{Isabelle} $>$
+\pgmenu{Logics} menu.
+\end{pgnote}