\chapter{Basic Concepts}

 \section{Introduction}

 This 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 the reader is familiar with mathematical logic but that

 (s)he is used to logical and set theoretic notation.  In contrast, we do assume

 that the reader is familiar with the basic concepts of functional programming.

 For excellent introductions 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.

 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 because this tutorial is based on

 Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle with

 structured proofs. 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 \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 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 \bfindex{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 collection is available online at

 \begin{center}\small

     \url{http://isabelle.in.tum.de/library/HOL/}

 \end{center}

 and is recommended browsing. Note that most of the theories 

 are based on classical Isabelle without the Isar extension. This means that

 they look slightly different than the theories in this tutorial, and that all

 proofs are in separate ML files.

 \begin{warn}

   HOL contains a theory \isaindexbold{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}

 \section{Types, Terms and Formulae}

 \label{sec:TypesTermsForms}

 \indexbold{type}

 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

 \begin{description}

 \item[base types,] in particular \isaindex{bool}, the type of truth values,

 and \isaindex{nat}, the type of natural numbers.

 \item[type constructors,] in particular \isaindex{list}, the type of

 lists, and \isaindex{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,] 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,]\indexbold{type variable}\indexbold{variable!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 to set the \rmindex{flag}

   \isaindexbold{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,

 which we introduce as we go along,

 can be set and reset in the same manner.\indexbold{flag!(re)setting}

 \end{warn}

 \textbf{Terms}\indexbold{term} 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:

 \begin{description}

 \item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}

 means what you think it means and requires that

 $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.

 \item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let}

 is equivalent to $u$ where all 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$}]

 \indexbold{*case}

 evaluates to $e@i$ if $e$ is of the form $c@i$.

 \end{description}

 Terms may also contain

 \isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. 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$}.

 \textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}.

 There are the basic constants \isaindexbold{True} and \isaindexbold{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 \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 is available in the form of the infix function

 \isa{=}\indexbold{$HOL0eq@\texttt{=}} 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. In case $t@1$ and $t@2$ are of type

 \isa{bool}, \isa{=} acts as if-and-only-if. The formula

 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for

 \isa{\isasymnot($t@1$ = $t@2$)}.

 Quantifiers are written as

 \isa{\isasymforall{}x.~$P$}\indexbold{$HOL0All@\isasymforall} and

 \isa{\isasymexists{}x.~$P$}\indexbold{$HOL0Ex@\isasymexists}.  There is

 even \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, 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$}.

 Despite type inference, it is sometimes necessary to attach explicit

 \textbf{type constraints}\indexbold{type constraint} 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: \isa{x < y::nat} is ill-typed because it is interpreted as

 \isa{(x < y)::nat}. The main reason for type constraints is overloading of

 functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for

 a full discussion of overloading and Table~\ref{tab:overloading} for the most

 important overloaded function symbols.

 \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

 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 \rmindex{flag}

 \isaindexbold{show_brackets}:

 \begin{ttbox}

 ML "set show_brackets"; \(\dots\); ML "reset show_brackets";

 \end{ttbox}

 \end{warn}

 \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 \isaindex{if},

 \isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.

 \item

 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}

 because \isa{x.x} is always read as a single qualified identifier that

 refers to an item \isa{x} in theory \isa{x}. Write

 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.

 \item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}.

 \end{itemize}

 For the sake of readability the usual mathematical symbols are used throughout

 the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab: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 \isa{?}.  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 merely

 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}

   If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential

   quantifier, it needs to be followed by a space. Otherwise \isa{?x} is

   interpreted as a schematic variable.

 \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 abandon a proof'' means to type \isacommand{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}.

 Some interfaces (including the shell level) offer special fonts with

 mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents

 are shown in table~\ref{tab:ascii} in the appendix.

 Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 

 Commands may but need not be terminated by semicolons.

 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.

 \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 \textsc{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 above, Proof General offers a much superior interface.

 If you have installed Proof General, you can start it by typing \texttt{Isabelle}.