\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. For example, you may want to work in the real

numbers, an extension of HOL (see \S\ref{sec:real}).

\end{pgnote}