doc-src/TutorialI/basics.tex
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10538 d1bf9ca9008d
child 10695 ffb153ef6366
permissions -rw-r--r--
*** empty log message ***
     1 \chapter{Basic Concepts}
     2 
     3 \section{Introduction}
     4 
     5 This is a tutorial on how to use Isabelle/HOL as a specification and
     6 verification system. Isabelle is a generic system for implementing logical
     7 formalisms, and Isabelle/HOL is the specialization of Isabelle for
     8 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
     9 following the equation
    10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
    11 We assume that the reader is familiar with the basic concepts of both fields.
    12 For excellent introductions to functional programming consult the textbooks
    13 by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although
    14 this tutorial initially concentrates on functional programming, do not be
    15 misled: HOL can express most mathematical concepts, and functional
    16 programming is just one particularly simple and ubiquitous instance.
    17 
    18 This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref},
    19 which is an extension of Isabelle~\cite{paulson-isa-book} with structured
    20 proofs.\footnote{Thus the full name of the system should be
    21   Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable
    22 difference to classical Isabelle (which is the basis of another version of
    23 this tutorial) is the replacement of the ML level by a dedicated language for
    24 definitions and proofs.
    25 
    26 A tutorial is by definition incomplete.  Currently the tutorial only
    27 introduces the rudiments of Isar's proof language. To fully exploit the power
    28 of Isar you need to consult the Isabelle/Isar Reference
    29 Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
    30 directly (for example for writing your own proof procedures) see the Isabelle
    31 Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
    32 Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
    33 index.
    34 
    35 \section{Theories}
    36 \label{sec:Basic:Theories}
    37 
    38 Working with Isabelle means creating theories. Roughly speaking, a
    39 \bfindex{theory} is a named collection of types, functions, and theorems,
    40 much like a module in a programming language or a specification in a
    41 specification language. In fact, theories in HOL can be either. The general
    42 format of a theory \texttt{T} is
    43 \begin{ttbox}
    44 theory T = B\(@1\) + \(\cdots\) + B\(@n\):
    45 \(\textit{declarations, definitions, and proofs}\)
    46 end
    47 \end{ttbox}
    48 where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
    49 theories that \texttt{T} is based on and \texttt{\textit{declarations,
    50     definitions, and proofs}} represents the newly introduced concepts
    51 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
    52 direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
    53 Everything defined in the parent theories (and their parents \dots) is
    54 automatically visible. To avoid name clashes, identifiers can be
    55 \textbf{qualified} by theory names as in \texttt{T.f} and
    56 \texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
    57 reside in a \bfindex{theory file} named \texttt{T.thy}.
    58 
    59 This tutorial is concerned with introducing you to the different linguistic
    60 constructs that can fill \textit{\texttt{declarations, definitions, and
    61     proofs}} in the above theory template.  A complete grammar of the basic
    62 constructs is found in the Isabelle/Isar Reference Manual.
    63 
    64 HOL's theory library is available online at
    65 \begin{center}\small
    66     \url{http://isabelle.in.tum.de/library/}
    67 \end{center}
    68 and is recommended browsing. Note that most of the theories in the library
    69 are based on classical Isabelle without the Isar extension. This means that
    70 they look slightly different than the theories in this tutorial, and that all
    71 proofs are in separate ML files.
    72 
    73 \begin{warn}
    74   HOL contains a theory \isaindexbold{Main}, the union of all the basic
    75   predefined theories like arithmetic, lists, sets, etc.\ (see the online
    76   library).  Unless you know what you are doing, always include \isa{Main}
    77   as a direct or indirect parent theory of all your theories.
    78 \end{warn}
    79 
    80 
    81 \section{Types, terms and formulae}
    82 \label{sec:TypesTermsForms}
    83 \indexbold{type}
    84 
    85 Embedded in a theory are the types, terms and formulae of HOL. HOL is a typed
    86 logic whose type system resembles that of functional programming languages
    87 like ML or Haskell. Thus there are
    88 \begin{description}
    89 \item[base types,] in particular \isaindex{bool}, the type of truth values,
    90 and \isaindex{nat}, the type of natural numbers.
    91 \item[type constructors,] in particular \isaindex{list}, the type of
    92 lists, and \isaindex{set}, the type of sets. Type constructors are written
    93 postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
    94 natural numbers. Parentheses around single arguments can be dropped (as in
    95 \isa{nat list}), multiple arguments are separated by commas (as in
    96 \isa{(bool,nat)ty}).
    97 \item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
    98   In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
    99   \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
   100   \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
   101   supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
   102   which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
   103     \isasymFun~$\tau$}.
   104 \item[type variables,]\indexbold{type variable}\indexbold{variable!type}
   105   denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML. They give rise
   106   to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
   107   function.
   108 \end{description}
   109 \begin{warn}
   110   Types are extremely important because they prevent us from writing
   111   nonsense.  Isabelle insists that all terms and formulae must be well-typed
   112   and will print an error message if a type mismatch is encountered. To
   113   reduce the amount of explicit type information that needs to be provided by
   114   the user, Isabelle infers the type of all variables automatically (this is
   115   called \bfindex{type inference}) and keeps quiet about it. Occasionally
   116   this may lead to misunderstandings between you and the system. If anything
   117   strange happens, we recommend to set the \rmindex{flag}
   118   \isaindexbold{show_types} that tells Isabelle to display type information
   119   that is usually suppressed: simply type
   120 \begin{ttbox}
   121 ML "set show_types"
   122 \end{ttbox}
   123 
   124 \noindent
   125 This can be reversed by \texttt{ML "reset show_types"}. Various other flags
   126 can be set and reset in the same manner.\indexbold{flag!(re)setting}
   127 \end{warn}
   128 
   129 
   130 \textbf{Terms}\indexbold{term} are formed as in functional programming by
   131 applying functions to arguments. If \isa{f} is a function of type
   132 \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
   133 $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
   134 infix functions like \isa{+} and some basic constructs from functional
   135 programming:
   136 \begin{description}
   137 \item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
   138 means what you think it means and requires that
   139 $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
   140 \item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let}
   141 is equivalent to $u$ where all occurrences of $x$ have been replaced by
   142 $t$. For example,
   143 \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
   144 by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
   145 \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
   146 \indexbold{*case}
   147 evaluates to $e@i$ if $e$ is of the form $c@i$.
   148 \end{description}
   149 
   150 Terms may also contain
   151 \isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,
   152 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
   153 returns \isa{x+1}. Instead of
   154 \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
   155 \isa{\isasymlambda{}x~y~z.~$t$}.
   156 
   157 \textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}.
   158 There are the basic constants \isaindexbold{True} and \isaindexbold{False} and
   159 the usual logical connectives (in decreasing order of priority):
   160 \indexboldpos{\isasymnot}{$HOL0not}, \indexboldpos{\isasymand}{$HOL0and},
   161 \indexboldpos{\isasymor}{$HOL0or}, and \indexboldpos{\isasymimp}{$HOL0imp},
   162 all of which (except the unary \isasymnot) associate to the right. In
   163 particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
   164   \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
   165   \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
   166 
   167 Equality is available in the form of the infix function
   168 \isa{=}\indexbold{$HOL0eq@\texttt{=}} of type \isa{'a \isasymFun~'a
   169   \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
   170 and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
   171 \isa{bool}, \isa{=} acts as if-and-only-if. The formula
   172 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
   173 \isa{\isasymnot($t@1$ = $t@2$)}.
   174 
   175 The syntax for quantifiers is
   176 \isa{\isasymforall{}x.~$P$}\indexbold{$HOL0All@\isasymforall} and
   177 \isa{\isasymexists{}x.~$P$}\indexbold{$HOL0Ex@\isasymexists}.  There is
   178 even \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which
   179 means that there exists exactly one \isa{x} that satisfies \isa{$P$}.  Nested
   180 quantifications can be abbreviated: \isa{\isasymforall{}x~y~z.~$P$} means
   181 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.
   182 
   183 Despite type inference, it is sometimes necessary to attach explicit
   184 \textbf{type constraints}\indexbold{type constraint} to a term.  The syntax is
   185 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
   186 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
   187 in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
   188 \isa{(x < y)::nat}. The main reason for type constraints are overloaded
   189 functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for
   190 a full discussion of overloading.
   191 
   192 \begin{warn}
   193 In general, HOL's concrete syntax tries to follow the conventions of
   194 functional programming and mathematics. Below we list the main rules that you
   195 should be familiar with to avoid certain syntactic traps. A particular
   196 problem for novices can be the priority of operators. If you are unsure, use
   197 more rather than fewer parentheses. In those cases where Isabelle echoes your
   198 input, you can see which parentheses are dropped---they were superfluous. If
   199 you are unsure how to interpret Isabelle's output because you don't know
   200 where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag}
   201 \isaindexbold{show_brackets}:
   202 \begin{ttbox}
   203 ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
   204 \end{ttbox}
   205 \end{warn}
   206 
   207 \begin{itemize}
   208 \item
   209 Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
   210 \item
   211 Isabelle allows infix functions like \isa{+}. The prefix form of function
   212 application binds more strongly than anything else and hence \isa{f~x + y}
   213 means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
   214 \item Remember that in HOL if-and-only-if is expressed using equality.  But
   215   equality has a high priority, as befitting a relation, while if-and-only-if
   216   typically has the lowest priority.  Thus, \isa{\isasymnot~\isasymnot~P =
   217     P} means \isa{\isasymnot\isasymnot(P = P)} and not
   218   \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
   219   logical equivalence, enclose both operands in parentheses, as in \isa{(A
   220     \isasymand~B) = (B \isasymand~A)}.
   221 \item
   222 Constructs with an opening but without a closing delimiter bind very weakly
   223 and should therefore be enclosed in parentheses if they appear in subterms, as
   224 in \isa{f = (\isasymlambda{}x.~x)}. This includes \isaindex{if},
   225 \isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
   226 \item
   227 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
   228 because \isa{x.x} is always read as a single qualified identifier that
   229 refers to an item \isa{x} in theory \isa{x}. Write
   230 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
   231 \item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}.
   232 \end{itemize}
   233 
   234 For the sake of readability the usual mathematical symbols are used throughout
   235 the tutorial. Their ASCII-equivalents are shown in figure~\ref{fig:ascii} in
   236 the appendix.
   237 
   238 
   239 \section{Variables}
   240 \label{sec:variables}
   241 \indexbold{variable}
   242 
   243 Isabelle distinguishes free and bound variables just as is customary. Bound
   244 variables are automatically renamed to avoid clashes with free variables. In
   245 addition, Isabelle has a third kind of variable, called a \bfindex{schematic
   246   variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
   247 with a \isa{?}.  Logically, an unknown is a free variable. But it may be
   248 instantiated by another term during the proof process. For example, the
   249 mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
   250 which means that Isabelle can instantiate it arbitrarily. This is in contrast
   251 to ordinary variables, which remain fixed. The programming language Prolog
   252 calls unknowns {\em logical\/} variables.
   253 
   254 Most of the time you can and should ignore unknowns and work with ordinary
   255 variables. Just don't be surprised that after you have finished the proof of
   256 a theorem, Isabelle will turn your free variables into unknowns: it merely
   257 indicates that Isabelle will automatically instantiate those unknowns
   258 suitably when the theorem is used in some other proof.
   259 Note that for readability we often drop the \isa{?}s when displaying a theorem.
   260 \begin{warn}
   261   If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential
   262   quantifier, it needs to be followed by a space. Otherwise \isa{?x} is
   263   interpreted as a schematic variable.
   264 \end{warn}
   265 
   266 \section{Interaction and interfaces}
   267 
   268 Interaction with Isabelle can either occur at the shell level or through more
   269 advanced interfaces. To keep the tutorial independent of the interface we
   270 have phrased the description of the intraction in a neutral language. For
   271 example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
   272 shell level, which is explained the first time the phrase is used. Other
   273 interfaces perform the same act by cursor movements and/or mouse clicks.
   274 Although shell-based interaction is quite feasible for the kind of proof
   275 scripts currently presented in this tutorial, the recommended interface for
   276 Isabelle/Isar is the Emacs-based \bfindex{Proof
   277   General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
   278 
   279 Some interfaces (including the shell level) offer special fonts with
   280 mathematical symbols. For those that do not, remember that ASCII-equivalents
   281 are shown in figure~\ref{fig:ascii} in the appendix.
   282 
   283 Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
   284 Commands may but need not be terminated by semicolons.
   285 At the shell level it is advisable to use semicolons to enforce that a command
   286 is executed immediately; otherwise Isabelle may wait for the next keyword
   287 before it knows that the command is complete.
   288 
   289 
   290 \section{Getting started}
   291 
   292 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
   293   -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
   294   starts the default logic, which usually is already \texttt{HOL}.  This is
   295   controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
   296     System Manual} for more details.} This presents you with Isabelle's most
   297 basic ASCII interface.  In addition you need to open an editor window to
   298 create theory files.  While you are developing a theory, we recommend to
   299 type each command into the file first and then enter it into Isabelle by
   300 copy-and-paste, thus ensuring that you have a complete record of your theory.
   301 As mentioned above, Proof General offers a much superior interface.
   302 If you have installed Proof General, you can start it with \texttt{Isabelle}.