doc-src/TutorialI/basics.tex
author wenzelm
Wed Jul 25 12:38:54 2012 +0200 (2012-07-25)
changeset 48497 ba61aceaa18a
parent 38432 439f50a241c1
permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
     1 \chapter{The Basics}
     2 
     3 \section{Introduction}
     4 
     5 This book is a tutorial on how to use the theorem prover Isabelle/HOL as a
     6 specification and verification system. Isabelle is a generic system for
     7 implementing logical formalisms, and Isabelle/HOL is the specialization
     8 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
     9 HOL step by step following the equation
    10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
    11 We do not assume that you are familiar with mathematical logic. 
    12 However, we do assume that
    13 you are used to logical and set theoretic notation, as covered
    14 in a good discrete mathematics course~\cite{Rosen-DMA}, and
    15 that you are familiar with the basic concepts of functional
    16 programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
    17 Although this tutorial initially concentrates on functional programming, do
    18 not be misled: HOL can express most mathematical concepts, and functional
    19 programming is just one particularly simple and ubiquitous instance.
    20 
    21 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.  This has
    22 influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant
    23 for us: this tutorial is based on
    24 Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides
    25 the implementation language almost completely.  Thus the full name of the
    26 system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.
    27 
    28 There are other implementations of HOL, in particular the one by Mike Gordon
    29 \index{Gordon, Mike}%
    30 \emph{et al.}, which is usually referred to as ``the HOL system''
    31 \cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes
    32 its incarnation Isabelle/HOL\@.
    33 
    34 A tutorial is by definition incomplete.  Currently the tutorial only
    35 introduces the rudiments of Isar's proof language. To fully exploit the power
    36 of Isar, in particular the ability to write readable and structured proofs,
    37 you should start with Nipkow's overview~\cite{Nipkow-TYPES02} and consult
    38 the Isabelle/Isar Reference Manual~\cite{isabelle-isar-ref} and Wenzel's
    39 PhD thesis~\cite{Wenzel-PhD} (which discusses many proof patterns)
    40 for further details. If you want to use Isabelle's ML level
    41 directly (for example for writing your own proof procedures) see the Isabelle
    42 Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
    43 Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
    44 index.
    45 
    46 \section{Theories}
    47 \label{sec:Basic:Theories}
    48 
    49 \index{theories|(}%
    50 Working with Isabelle means creating theories. Roughly speaking, a
    51 \textbf{theory} is a named collection of types, functions, and theorems,
    52 much like a module in a programming language or a specification in a
    53 specification language. In fact, theories in HOL can be either. The general
    54 format of a theory \texttt{T} is
    55 \begin{ttbox}
    56 theory T
    57 imports B\(@1\) \(\ldots\) B\(@n\)
    58 begin
    59 {\rmfamily\textit{declarations, definitions, and proofs}}
    60 end
    61 \end{ttbox}\cmmdx{theory}\cmmdx{imports}
    62 where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing
    63 theories that \texttt{T} is based on and \textit{declarations,
    64     definitions, and proofs} represents the newly introduced concepts
    65 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
    66 direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@.
    67 Everything defined in the parent theories (and their parents, recursively) is
    68 automatically visible. To avoid name clashes, identifiers can be
    69 \textbf{qualified}\indexbold{identifiers!qualified}
    70 by theory names as in \texttt{T.f} and~\texttt{B.f}. 
    71 Each theory \texttt{T} must
    72 reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}.
    73 
    74 This tutorial is concerned with introducing you to the different linguistic
    75 constructs that can fill the \textit{declarations, definitions, and
    76     proofs} above.  A complete grammar of the basic
    77 constructs is found in the Isabelle/Isar Reference
    78 Manual~\cite{isabelle-isar-ref}.
    79 
    80 \begin{warn}
    81   HOL contains a theory \thydx{Main}, the union of all the basic
    82   predefined theories like arithmetic, lists, sets, etc.  
    83   Unless you know what you are doing, always include \isa{Main}
    84   as a direct or indirect parent of all your theories.
    85 \end{warn}
    86 HOL's theory collection is available online at
    87 \begin{center}\small
    88     \url{http://isabelle.in.tum.de/library/HOL/}
    89 \end{center}
    90 and is recommended browsing. In subdirectory \texttt{Library} you find
    91 a growing library of useful theories that are not part of \isa{Main}
    92 but can be included among the parents of a theory and will then be
    93 loaded automatically.
    94 
    95 For the more adventurous, there is the \emph{Archive of Formal Proofs},
    96 a journal-like collection of more advanced Isabelle theories:
    97 \begin{center}\small
    98     \url{http://afp.sourceforge.net/}
    99 \end{center}
   100 We hope that you will contribute to it yourself one day.%
   101 \index{theories|)}
   102 
   103 
   104 \section{Types, Terms and Formulae}
   105 \label{sec:TypesTermsForms}
   106 
   107 Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
   108 logic whose type system resembles that of functional programming languages
   109 like ML or Haskell. Thus there are
   110 \index{types|(}
   111 \begin{description}
   112 \item[base types,] 
   113 in particular \tydx{bool}, the type of truth values,
   114 and \tydx{nat}, the type of natural numbers.
   115 \item[type constructors,]\index{type constructors}
   116  in particular \tydx{list}, the type of
   117 lists, and \tydx{set}, the type of sets. Type constructors are written
   118 postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
   119 natural numbers. Parentheses around single arguments can be dropped (as in
   120 \isa{nat list}), multiple arguments are separated by commas (as in
   121 \isa{(bool,nat)ty}).
   122 \item[function types,]\index{function types}
   123 denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
   124   In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
   125   \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
   126   \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
   127   supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
   128   which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
   129     \isasymFun~$\tau$}.
   130 \item[type variables,]\index{type variables}\index{variables!type}
   131   denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
   132   to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
   133   function.
   134 \end{description}
   135 \begin{warn}
   136   Types are extremely important because they prevent us from writing
   137   nonsense.  Isabelle insists that all terms and formulae must be
   138   well-typed and will print an error message if a type mismatch is
   139   encountered. To reduce the amount of explicit type information that
   140   needs to be provided by the user, Isabelle infers the type of all
   141   variables automatically (this is called \bfindex{type inference})
   142   and keeps quiet about it. Occasionally this may lead to
   143   misunderstandings between you and the system. If anything strange
   144   happens, we recommend that you ask Isabelle to display all type
   145   information via the Proof General menu item \pgmenu{Isabelle} $>$
   146   \pgmenu{Settings} $>$ \pgmenu{Show Types} (see \S\ref{sec:interface}
   147   for details).
   148 \end{warn}%
   149 \index{types|)}
   150 
   151 
   152 \index{terms|(}
   153 \textbf{Terms} are formed as in functional programming by
   154 applying functions to arguments. If \isa{f} is a function of type
   155 \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
   156 $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
   157 infix functions like \isa{+} and some basic constructs from functional
   158 programming, such as conditional expressions:
   159 \begin{description}
   160 \item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}
   161 Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
   162 \item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}
   163 is equivalent to $u$ where all free occurrences of $x$ have been replaced by
   164 $t$. For example,
   165 \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
   166 by semicolons: \isa{let $x@1$ = $t@1$;\dots; $x@n$ = $t@n$ in $u$}.
   167 \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
   168 \index{*case expressions}
   169 evaluates to $e@i$ if $e$ is of the form $c@i$.
   170 \end{description}
   171 
   172 Terms may also contain
   173 \isasymlambda-abstractions.\index{lambda@$\lambda$ expressions}
   174 For example,
   175 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
   176 returns \isa{x+1}. Instead of
   177 \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
   178 \isa{\isasymlambda{}x~y~z.~$t$}.%
   179 \index{terms|)}
   180 
   181 \index{formulae|(}%
   182 \textbf{Formulae} are terms of type \tydx{bool}.
   183 There are the basic constants \cdx{True} and \cdx{False} and
   184 the usual logical connectives (in decreasing order of priority):
   185 \indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
   186 \indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
   187 all of which (except the unary \isasymnot) associate to the right. In
   188 particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
   189   \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
   190   \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
   191 
   192 Equality\index{equality} is available in the form of the infix function
   193 \isa{=} of type \isa{'a \isasymFun~'a
   194   \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
   195 and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type
   196 \isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}.
   197 The formula
   198 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
   199 \isa{\isasymnot($t@1$ = $t@2$)}.
   200 
   201 Quantifiers\index{quantifiers} are written as
   202 \isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}. 
   203 There is even
   204 \isa{\isasymuniqex{}x.~$P$}, which
   205 means that there exists exactly one \isa{x} that satisfies \isa{$P$}. 
   206 Nested quantifications can be abbreviated:
   207 \isa{\isasymforall{}x~y~z.~$P$} means
   208 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.%
   209 \index{formulae|)}
   210 
   211 Despite type inference, it is sometimes necessary to attach explicit
   212 \bfindex{type constraints} to a term.  The syntax is
   213 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
   214 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
   215 in parentheses.  For instance,
   216 \isa{x < y::nat} is ill-typed because it is interpreted as
   217 \isa{(x < y)::nat}.  Type constraints may be needed to disambiguate
   218 expressions
   219 involving overloaded functions such as~\isa{+}, 
   220 \isa{*} and~\isa{<}.  Section~\ref{sec:overloading} 
   221 discusses overloading, while Table~\ref{tab:overloading} presents the most
   222 important overloaded function symbols.
   223 
   224 In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of
   225 functional programming and mathematics.  Here are the main rules that you
   226 should be familiar with to avoid certain syntactic traps:
   227 \begin{itemize}
   228 \item
   229 Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
   230 \item
   231 Isabelle allows infix functions like \isa{+}. The prefix form of function
   232 application binds more strongly than anything else and hence \isa{f~x + y}
   233 means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
   234 \item Remember that in HOL if-and-only-if is expressed using equality.  But
   235   equality has a high priority, as befitting a relation, while if-and-only-if
   236   typically has the lowest priority.  Thus, \isa{\isasymnot~\isasymnot~P =
   237     P} means \isa{\isasymnot\isasymnot(P = P)} and not
   238   \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
   239   logical equivalence, enclose both operands in parentheses, as in \isa{(A
   240     \isasymand~B) = (B \isasymand~A)}.
   241 \item
   242 Constructs with an opening but without a closing delimiter bind very weakly
   243 and should therefore be enclosed in parentheses if they appear in subterms, as
   244 in \isa{(\isasymlambda{}x.~x) = f}.  This includes 
   245 \isa{if},\index{*if expressions}
   246 \isa{let},\index{*let expressions}
   247 \isa{case},\index{*case expressions}
   248 \isa{\isasymlambda}, and quantifiers.
   249 \item
   250 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
   251 because \isa{x.x} is always taken as a single qualified identifier. Write
   252 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
   253 \item Identifiers\indexbold{identifiers} may contain the characters \isa{_} 
   254 and~\isa{'}, except at the beginning.
   255 \end{itemize}
   256 
   257 For the sake of readability, we use the usual mathematical symbols throughout
   258 the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
   259 the appendix.
   260 
   261 \begin{warn}
   262 A particular problem for novices can be the priority of operators. If
   263 you are unsure, use additional parentheses. In those cases where
   264 Isabelle echoes your input, you can see which parentheses are dropped
   265 --- they were superfluous. If you are unsure how to interpret
   266 Isabelle's output because you don't know where the (dropped)
   267 parentheses go, set the Proof General flag \pgmenu{Isabelle} $>$
   268 \pgmenu{Settings} $>$ \pgmenu{Show Brackets} (see \S\ref{sec:interface}).
   269 \end{warn}
   270 
   271 
   272 \section{Variables}
   273 \label{sec:variables}
   274 \index{variables|(}
   275 
   276 Isabelle distinguishes free and bound variables, as is customary. Bound
   277 variables are automatically renamed to avoid clashes with free variables. In
   278 addition, Isabelle has a third kind of variable, called a \textbf{schematic
   279   variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns}, 
   280 which must have a~\isa{?} as its first character.  
   281 Logically, an unknown is a free variable. But it may be
   282 instantiated by another term during the proof process. For example, the
   283 mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
   284 which means that Isabelle can instantiate it arbitrarily. This is in contrast
   285 to ordinary variables, which remain fixed. The programming language Prolog
   286 calls unknowns {\em logical\/} variables.
   287 
   288 Most of the time you can and should ignore unknowns and work with ordinary
   289 variables. Just don't be surprised that after you have finished the proof of
   290 a theorem, Isabelle will turn your free variables into unknowns.  It
   291 indicates that Isabelle will automatically instantiate those unknowns
   292 suitably when the theorem is used in some other proof.
   293 Note that for readability we often drop the \isa{?}s when displaying a theorem.
   294 \begin{warn}
   295   For historical reasons, Isabelle accepts \isa{?} as an ASCII representation
   296   of the \(\exists\) symbol.  However, the \isa{?} character must then be followed
   297   by a space, as in \isa{?~x. f(x) = 0}.  Otherwise, \isa{?x} is
   298   interpreted as a schematic variable.  The preferred ASCII representation of
   299   the \(\exists\) symbol is \isa{EX}\@. 
   300 \end{warn}%
   301 \index{variables|)}
   302 
   303 \section{Interaction and Interfaces}
   304 \label{sec:interface}
   305 
   306 The recommended interface for Isabelle/Isar is the (X)Emacs-based
   307 \bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
   308 Interaction with Isabelle at the shell level, although possible,
   309 should be avoided. Most of the tutorial is independent of the
   310 interface and is phrased in a neutral language. For example, the
   311 phrase ``to abandon a proof'' corresponds to the obvious
   312 action of clicking on the \pgmenu{Undo} symbol in Proof General.
   313 Proof General specific information is often displayed in paragraphs
   314 identified by a miniature Proof General icon. Here are two examples:
   315 \begin{pgnote}
   316 Proof General supports a special font with mathematical symbols known
   317 as ``x-symbols''. All symbols have \textsc{ascii}-equivalents: for
   318 example, you can enter either \verb!&!  or \verb!\<and>! to obtain
   319 $\land$. For a list of the most frequent symbols see table~\ref{tab:ascii}
   320 in the appendix.
   321 
   322 Note that by default x-symbols are not enabled. You have to switch
   323 them on via the menu item \pgmenu{Proof-General} $>$ \pgmenu{Options} $>$
   324 \pgmenu{X-Symbols} (and save the option via the top-level
   325 \pgmenu{Options} menu).
   326 \end{pgnote}
   327 
   328 \begin{pgnote}
   329 Proof General offers the \pgmenu{Isabelle} menu for displaying
   330 information and setting flags. A particularly useful flag is
   331 \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgdx{Show Types} which
   332 causes Isabelle to output the type information that is usually
   333 suppressed. This is indispensible in case of errors of all kinds
   334 because often the types reveal the source of the problem. Once you
   335 have diagnosed the problem you may no longer want to see the types
   336 because they clutter all output. Simply reset the flag.
   337 \end{pgnote}
   338 
   339 \section{Getting Started}
   340 
   341 Assuming you have installed Isabelle and Proof General, you start it by typing
   342 \texttt{Isabelle} in a shell window. This launches a Proof General window.
   343 By default, you are in HOL\footnote{This is controlled by the
   344 \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual}
   345 for more details.}.
   346 
   347 \begin{pgnote}
   348 You can choose a different logic via the \pgmenu{Isabelle} $>$
   349 \pgmenu{Logics} menu.
   350 \end{pgnote}