wenzelm@12668: \chapter{The Basics}
nipkow@8743: 
nipkow@8743: \section{Introduction}
nipkow@8743: 
paulson@11405: This book is a tutorial on how to use the theorem prover Isabelle/HOL as a
paulson@11405: specification and verification system. Isabelle is a generic system for
paulson@11405: implementing logical formalisms, and Isabelle/HOL is the specialization
paulson@11405: of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
paulson@11405: HOL step by step following the equation
nipkow@8743: \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
paulson@11456: We do not assume that you are familiar with mathematical logic. 
paulson@11456: However, we do assume that
paulson@11456: you are used to logical and set theoretic notation, as covered
paulson@11456: in a good discrete mathematics course~\cite{Rosen-DMA}, and
paulson@11450: that you are familiar with the basic concepts of functional
nipkow@11209: programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
nipkow@11209: Although this tutorial initially concentrates on functional programming, do
nipkow@11209: not be misled: HOL can express most mathematical concepts, and functional
nipkow@11209: programming is just one particularly simple and ubiquitous instance.
nipkow@8743: 
nipkow@11205: Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.  This has
nipkow@11205: influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant
paulson@11450: for us: this tutorial is based on
nipkow@11213: Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides
nipkow@11213: the implementation language almost completely.  Thus the full name of the
nipkow@11213: system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.
nipkow@11213: 
nipkow@11213: There are other implementations of HOL, in particular the one by Mike Gordon
paulson@11450: \index{Gordon, Mike}%
nipkow@11213: \emph{et al.}, which is usually referred to as ``the HOL system''
nipkow@11213: \cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes
paulson@11450: its incarnation Isabelle/HOL\@.
nipkow@8743: 
nipkow@8743: A tutorial is by definition incomplete.  Currently the tutorial only
nipkow@8743: introduces the rudiments of Isar's proof language. To fully exploit the power
nipkow@11213: of Isar, in particular the ability to write readable and structured proofs,
nipkow@15429: you should start with Nipkow's overview~\cite{Nipkow-TYPES02} and consult
nipkow@15429: the Isabelle/Isar Reference Manual~\cite{isabelle-isar-ref} and Wenzel's
nipkow@15429: PhD thesis~\cite{Wenzel-PhD} (which discusses many proof patterns)
nipkow@15429: for further details. If you want to use Isabelle's ML level
nipkow@8743: directly (for example for writing your own proof procedures) see the Isabelle
nipkow@8743: Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
nipkow@8743: Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
nipkow@8743: index.
nipkow@8743: 
nipkow@8743: \section{Theories}
nipkow@8743: \label{sec:Basic:Theories}
nipkow@8743: 
paulson@11428: \index{theories|(}%
nipkow@8743: Working with Isabelle means creating theories. Roughly speaking, a
paulson@11428: \textbf{theory} is a named collection of types, functions, and theorems,
nipkow@8743: much like a module in a programming language or a specification in a
nipkow@8743: specification language. In fact, theories in HOL can be either. The general
nipkow@8743: format of a theory \texttt{T} is
nipkow@8743: \begin{ttbox}
nipkow@15136: theory T
nipkow@15141: imports B\(@1\) \(\ldots\) B\(@n\)
nipkow@15136: begin
paulson@11450: {\rmfamily\textit{declarations, definitions, and proofs}}
nipkow@8743: end
nipkow@15358: \end{ttbox}\cmmdx{theory}\cmmdx{imports}
nipkow@15136: where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing
paulson@11450: theories that \texttt{T} is based on and \textit{declarations,
paulson@11450:     definitions, and proofs} represents the newly introduced concepts
nipkow@8771: (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
paulson@11450: direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@.
paulson@11450: Everything defined in the parent theories (and their parents, recursively) is
nipkow@8743: automatically visible. To avoid name clashes, identifiers can be
paulson@11450: \textbf{qualified}\indexbold{identifiers!qualified}
paulson@11450: by theory names as in \texttt{T.f} and~\texttt{B.f}. 
paulson@11450: Each theory \texttt{T} must
paulson@11428: reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}.
nipkow@8743: 
nipkow@8743: This tutorial is concerned with introducing you to the different linguistic
paulson@11450: constructs that can fill the \textit{declarations, definitions, and
paulson@11450:     proofs} above.  A complete grammar of the basic
nipkow@12327: constructs is found in the Isabelle/Isar Reference
nipkow@12327: Manual~\cite{isabelle-isar-ref}.
nipkow@8743: 
nipkow@8743: \begin{warn}
paulson@11428:   HOL contains a theory \thydx{Main}, the union of all the basic
paulson@10885:   predefined theories like arithmetic, lists, sets, etc.  
paulson@10885:   Unless you know what you are doing, always include \isa{Main}
nipkow@10971:   as a direct or indirect parent of all your theories.
nipkow@12332: \end{warn}
nipkow@16306: HOL's theory collection is available online at
nipkow@16306: \begin{center}\small
nipkow@16306:     \url{http://isabelle.in.tum.de/library/HOL/}
nipkow@16306: \end{center}
nipkow@16359: and is recommended browsing. In subdirectory \texttt{Library} you find
nipkow@16359: a growing library of useful theories that are not part of \isa{Main}
nipkow@16359: but can be included among the parents of a theory and will then be
nipkow@16359: loaded automatically.
nipkow@16306: 
nipkow@16306: For the more adventurous, there is the \emph{Archive of Formal Proofs},
nipkow@16306: a journal-like collection of more advanced Isabelle theories:
nipkow@16306: \begin{center}\small
nipkow@16306:     \url{http://afp.sourceforge.net/}
nipkow@16306: \end{center}
nipkow@16306: We hope that you will contribute to it yourself one day.%
paulson@11428: \index{theories|)}
nipkow@8743: 
nipkow@8743: 
paulson@10885: \section{Types, Terms and Formulae}
nipkow@8743: \label{sec:TypesTermsForms}
nipkow@8743: 
paulson@10795: Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
nipkow@8771: logic whose type system resembles that of functional programming languages
paulson@11450: like ML or Haskell. Thus there are
paulson@11450: \index{types|(}
nipkow@8743: \begin{description}
paulson@11450: \item[base types,] 
paulson@11450: in particular \tydx{bool}, the type of truth values,
paulson@11428: and \tydx{nat}, the type of natural numbers.
paulson@11450: \item[type constructors,]\index{type constructors}
paulson@11450:  in particular \tydx{list}, the type of
paulson@11428: lists, and \tydx{set}, the type of sets. Type constructors are written
nipkow@8771: postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
nipkow@8743: natural numbers. Parentheses around single arguments can be dropped (as in
nipkow@8771: \isa{nat list}), multiple arguments are separated by commas (as in
nipkow@8771: \isa{(bool,nat)ty}).
paulson@11450: \item[function types,]\index{function types}
paulson@11450: denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
nipkow@8771:   In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
nipkow@8771:   \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
nipkow@8771:   \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
nipkow@8771:   supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
nipkow@8771:   which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
nipkow@8743:     \isasymFun~$\tau$}.
paulson@11450: \item[type variables,]\index{type variables}\index{variables!type}
paulson@10795:   denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
nipkow@8771:   to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
nipkow@8771:   function.
nipkow@8743: \end{description}
nipkow@8743: \begin{warn}
nipkow@8743:   Types are extremely important because they prevent us from writing
nipkow@16359:   nonsense.  Isabelle insists that all terms and formulae must be
nipkow@16359:   well-typed and will print an error message if a type mismatch is
nipkow@16359:   encountered. To reduce the amount of explicit type information that
nipkow@16359:   needs to be provided by the user, Isabelle infers the type of all
nipkow@16359:   variables automatically (this is called \bfindex{type inference})
nipkow@16359:   and keeps quiet about it. Occasionally this may lead to
nipkow@16359:   misunderstandings between you and the system. If anything strange
nipkow@16359:   happens, we recommend that you ask Isabelle to display all type
nipkow@16359:   information via the Proof General menu item \textsf{Isabelle} $>$
nipkow@16359:   \textsf{Settings} $>$ \textsf{Show Types} (see \S\ref{sec:interface}
nipkow@16359:   for details).
paulson@11450: \end{warn}%
paulson@11450: \index{types|)}
nipkow@8743: 
nipkow@8743: 
paulson@11450: \index{terms|(}
paulson@11450: \textbf{Terms} are formed as in functional programming by
nipkow@8771: applying functions to arguments. If \isa{f} is a function of type
nipkow@8771: \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
nipkow@8771: $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
nipkow@8771: infix functions like \isa{+} and some basic constructs from functional
paulson@11428: programming, such as conditional expressions:
nipkow@8743: \begin{description}
paulson@11450: \item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}
paulson@11428: Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
paulson@11450: \item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}
nipkow@13814: is equivalent to $u$ where all free occurrences of $x$ have been replaced by
nipkow@8743: $t$. For example,
nipkow@8771: \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
nipkow@13814: by semicolons: \isa{let $x@1$ = $t@1$;\dots; $x@n$ = $t@n$ in $u$}.
nipkow@8771: \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
paulson@11450: \index{*case expressions}
nipkow@8771: evaluates to $e@i$ if $e$ is of the form $c@i$.
nipkow@8743: \end{description}
nipkow@8743: 
nipkow@8743: Terms may also contain
paulson@11450: \isasymlambda-abstractions.\index{lambda@$\lambda$ expressions}
paulson@11450: For example,
nipkow@8771: \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
nipkow@8771: returns \isa{x+1}. Instead of
nipkow@8771: \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
paulson@11450: \isa{\isasymlambda{}x~y~z.~$t$}.%
paulson@11450: \index{terms|)}
nipkow@8743: 
paulson@11450: \index{formulae|(}%
paulson@11450: \textbf{Formulae} are terms of type \tydx{bool}.
paulson@11428: There are the basic constants \cdx{True} and \cdx{False} and
nipkow@8771: the usual logical connectives (in decreasing order of priority):
paulson@11420: \indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
paulson@11420: \indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
nipkow@8743: all of which (except the unary \isasymnot) associate to the right. In
nipkow@8771: particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
nipkow@8771:   \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
nipkow@8771:   \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
nipkow@8743: 
paulson@11450: Equality\index{equality} is available in the form of the infix function
paulson@11450: \isa{=} of type \isa{'a \isasymFun~'a
nipkow@8771:   \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
paulson@11450: and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type
paulson@11450: \isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}.
paulson@11450: The formula
nipkow@8771: \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
nipkow@8771: \isa{\isasymnot($t@1$ = $t@2$)}.
nipkow@8743: 
paulson@11450: Quantifiers\index{quantifiers} are written as
paulson@11450: \isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}. 
paulson@11420: There is even
paulson@11450: \isa{\isasymuniqex{}x.~$P$}, which
paulson@11420: means that there exists exactly one \isa{x} that satisfies \isa{$P$}. 
paulson@11420: Nested quantifications can be abbreviated:
paulson@11420: \isa{\isasymforall{}x~y~z.~$P$} means
paulson@11450: \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.%
paulson@11450: \index{formulae|)}
nipkow@8743: 
nipkow@8743: Despite type inference, it is sometimes necessary to attach explicit
paulson@11428: \bfindex{type constraints} to a term.  The syntax is
nipkow@8771: \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
nipkow@10538: \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
paulson@11450: in parentheses.  For instance,
paulson@11450: \isa{x < y::nat} is ill-typed because it is interpreted as
paulson@11450: \isa{(x < y)::nat}.  Type constraints may be needed to disambiguate
paulson@11450: expressions
paulson@11450: involving overloaded functions such as~\isa{+}, 
paulson@11450: \isa{*} and~\isa{<}.  Section~\ref{sec:overloading} 
paulson@11450: discusses overloading, while Table~\ref{tab:overloading} presents the most
nipkow@10695: important overloaded function symbols.
nipkow@8743: 
paulson@11450: In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of
paulson@11450: functional programming and mathematics.  Here are the main rules that you
paulson@11450: should be familiar with to avoid certain syntactic traps:
nipkow@8743: \begin{itemize}
nipkow@8743: \item
nipkow@8771: Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
nipkow@8743: \item
nipkow@8771: Isabelle allows infix functions like \isa{+}. The prefix form of function
nipkow@8771: application binds more strongly than anything else and hence \isa{f~x + y}
nipkow@8771: means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
nipkow@8743: \item Remember that in HOL if-and-only-if is expressed using equality.  But
nipkow@8743:   equality has a high priority, as befitting a relation, while if-and-only-if
nipkow@8771:   typically has the lowest priority.  Thus, \isa{\isasymnot~\isasymnot~P =
nipkow@8771:     P} means \isa{\isasymnot\isasymnot(P = P)} and not
nipkow@8771:   \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
nipkow@8771:   logical equivalence, enclose both operands in parentheses, as in \isa{(A
nipkow@8743:     \isasymand~B) = (B \isasymand~A)}.
nipkow@8743: \item
nipkow@8743: Constructs with an opening but without a closing delimiter bind very weakly
nipkow@8743: and should therefore be enclosed in parentheses if they appear in subterms, as
paulson@11450: in \isa{(\isasymlambda{}x.~x) = f}.  This includes 
paulson@11450: \isa{if},\index{*if expressions}
paulson@11450: \isa{let},\index{*let expressions}
paulson@11450: \isa{case},\index{*case expressions}
paulson@11450: \isa{\isasymlambda}, and quantifiers.
nipkow@8743: \item
nipkow@8771: Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
nipkow@12327: because \isa{x.x} is always taken as a single qualified identifier. Write
nipkow@8771: \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
paulson@11450: \item Identifiers\indexbold{identifiers} may contain the characters \isa{_} 
nipkow@12327: and~\isa{'}, except at the beginning.
nipkow@8743: \end{itemize}
nipkow@8743: 
paulson@11450: For the sake of readability, we use the usual mathematical symbols throughout
nipkow@10983: the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
nipkow@8771: the appendix.
nipkow@8771: 
paulson@11450: \begin{warn}
nipkow@16359: A particular problem for novices can be the priority of operators. If
nipkow@16359: you are unsure, use additional parentheses. In those cases where
nipkow@16359: Isabelle echoes your input, you can see which parentheses are dropped
nipkow@16359: --- they were superfluous. If you are unsure how to interpret
nipkow@16359: Isabelle's output because you don't know where the (dropped)
nipkow@16359: parentheses go, set the Proof General flag \textsf{Isabelle} $>$
nipkow@16359: \textsf{Settings} $>$ \textsf{Show Brackets} (see \S\ref{sec:interface}).
paulson@11450: \end{warn}
paulson@11450: 
nipkow@8743: 
nipkow@8743: \section{Variables}
nipkow@8743: \label{sec:variables}
paulson@11450: \index{variables|(}
nipkow@8743: 
paulson@11450: Isabelle distinguishes free and bound variables, as is customary. Bound
nipkow@8743: variables are automatically renamed to avoid clashes with free variables. In
paulson@11428: addition, Isabelle has a third kind of variable, called a \textbf{schematic
paulson@11428:   variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns}, 
nipkow@13439: which must have a~\isa{?} as its first character.  
paulson@11428: Logically, an unknown is a free variable. But it may be
nipkow@8743: instantiated by another term during the proof process. For example, the
nipkow@8771: mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
nipkow@8743: which means that Isabelle can instantiate it arbitrarily. This is in contrast
nipkow@8743: to ordinary variables, which remain fixed. The programming language Prolog
nipkow@8743: calls unknowns {\em logical\/} variables.
nipkow@8743: 
nipkow@8743: Most of the time you can and should ignore unknowns and work with ordinary
nipkow@8743: variables. Just don't be surprised that after you have finished the proof of
paulson@11450: a theorem, Isabelle will turn your free variables into unknowns.  It
nipkow@8743: indicates that Isabelle will automatically instantiate those unknowns
nipkow@8743: suitably when the theorem is used in some other proof.
nipkow@9689: Note that for readability we often drop the \isa{?}s when displaying a theorem.
nipkow@8743: \begin{warn}
paulson@11450:   For historical reasons, Isabelle accepts \isa{?} as an ASCII representation
paulson@11450:   of the \(\exists\) symbol.  However, the \isa{?} character must then be followed
paulson@11450:   by a space, as in \isa{?~x. f(x) = 0}.  Otherwise, \isa{?x} is
paulson@11450:   interpreted as a schematic variable.  The preferred ASCII representation of
paulson@11450:   the \(\exists\) symbol is \isa{EX}\@. 
paulson@11450: \end{warn}%
paulson@11450: \index{variables|)}
nipkow@8743: 
paulson@10885: \section{Interaction and Interfaces}
nipkow@16306: \label{sec:interface}
nipkow@8771: 
nipkow@16359: The recommended interface for Isabelle/Isar is the (X)Emacs-based
nipkow@16359: \bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
nipkow@16359: Interaction with Isabelle at the shell level, although possible,
nipkow@16359: should be avoided. Most of the tutorial is independent of the
nipkow@16359: interface and is phrased in a neutral language. For example, the
nipkow@16359: phrase ``to abandon a proof'' corresponds to the obvious
nipkow@16359: action of clicking on the \textsf{Undo} symbol in Proof General.
nipkow@16359: Proof General specific information is often displayed in paragraphs
nipkow@16359: identified by a miniature Proof General icon. Here are two examples:
nipkow@16359: \begin{pgnote}
nipkow@16359: Proof General supports a special font with mathematical symbols known
nipkow@16359: as ``x-symbols''. All symbols have \textsc{ascii}-equivalents: for
nipkow@16359: example, you can enter either \verb!&!  or \verb!\<and>! to obtain
nipkow@16359: $\land$. For a list of the most frequent symbols see table~\ref{tab:ascii}
nipkow@16359: in the appendix.
nipkow@8771: 
nipkow@16359: Note that by default x-symbols are not enabled. You have to switch
nipkow@16359: them on via the menu item \textsf{Proof-General} $>$ \textsf{Options} $>$
nipkow@16359: \textsf{X-Symbols} (and save the option via the top-level
nipkow@16359: \textsf{Options} menu).
nipkow@16306: \end{pgnote}
nipkow@8771: 
nipkow@16306: \begin{pgnote}
nipkow@16359: Proof General offers the \textsf{Isabelle} menu for displaying
nipkow@16359: information and setting flags. A particularly useful flag is
nipkow@16359: \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Show Types} which
nipkow@16359: causes Isabelle to output the type information that is usually
nipkow@16306: suppressed. This is indispensible in case of errors of all kinds
nipkow@16359: because often the types reveal the source of the problem. Once you
nipkow@16359: have diagnosed the problem you may no longer want to see the types
nipkow@16359: because they clutter all output. Simply reset the flag.
nipkow@16306: \end{pgnote}
nipkow@8771: 
paulson@10885: \section{Getting Started}
nipkow@8743: 
nipkow@16359: Assuming you have installed Isabelle and Proof General, you start it by typing
nipkow@16359: \texttt{Isabelle} in a shell window. This launches a Proof General window.
nipkow@16359: By default, you are in HOL\footnote{This is controlled by the
nipkow@16359: \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual}
nipkow@16359: for more details.}.
nipkow@16359: 
nipkow@16359: \begin{pgnote}
nipkow@16359: You can choose a different logic via the \textsf{Isabelle} $>$
nipkow@16359: \textsf{Logics} menu. For example, you may want to work in the real
nipkow@16359: numbers, an extension of HOL (see \S\ref{sec:real}).
nipkow@16359: % This is just excess baggage:
nipkow@16359: %(You have to restart Proof General if you only compile the new logic
nipkow@16359: %after having launching Proof General already).
nipkow@16359: \end{pgnote}