1.1 --- a/doc-src/TutorialI/basics.tex Sun Apr 23 11:41:45 2000 +0200
1.2 +++ b/doc-src/TutorialI/basics.tex Tue Apr 25 08:09:10 2000 +0200
1.3 @@ -48,13 +48,13 @@
1.4 where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
1.5 theories that \texttt{T} is based on and \texttt{\textit{declarations,
1.6 definitions, and proofs}} represents the newly introduced concepts
1.7 -(types, functions etc) and proofs about them. The \texttt{B}$@i$ are the
1.8 +(types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
1.9 direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
1.10 Everything defined in the parent theories (and their parents \dots) is
1.11 automatically visible. To avoid name clashes, identifiers can be
1.12 \textbf{qualified} by theory names as in \texttt{T.f} and
1.13 \texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
1.14 -reside in a \indexbold{theory file} named \texttt{T.thy}.
1.15 +reside in a \bfindex{theory file} named \texttt{T.thy}.
1.16
1.17 This tutorial is concerned with introducing you to the different linguistic
1.18 constructs that can fill \textit{\texttt{declarations, definitions, and
1.19 @@ -74,59 +74,33 @@
1.20 \end{warn}
1.21
1.22
1.23 -\section{Interaction and interfaces}
1.24 -
1.25 -Interaction with Isabelle can either occur at the shell level or through more
1.26 -advanced interfaces. To keep the tutorial independent of the interface we
1.27 -have phrased the description of the intraction in a neutral language. For
1.28 -example, the phrase ``to cancel a proof'' means to type \texttt{oops} at the
1.29 -shell level, which is explained the first time the phrase is used. Other
1.30 -interfaces perform the same act by cursor movements and/or mouse clicks.
1.31 -Although shell-based interaction is quite feasible for the kind of proof
1.32 -scripts currently presented in this tutorial, the recommended interface for
1.33 -Isabelle/Isar is the Emacs-based \bfindex{Proof
1.34 - General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
1.35 -
1.36 -To improve readability some of the interfaces (including the shell level)
1.37 -offer special fonts with mathematical symbols. Therefore the usual
1.38 -mathematical symbols are used throughout the tutorial. Their
1.39 -ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix.
1.40 -
1.41 -Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
1.42 -for example Proof General, require each command to be terminated by a
1.43 -semicolon, whereas others, for example the shell level, do not. But even at
1.44 -the shell level it is advisable to use semicolons to enforce that a command
1.45 -is executed immediately; otherwise Isabelle may wait for the next keyword
1.46 -before it knows that the command is complete. Note that for readibility
1.47 -reasons we often drop the final semicolon in the text.
1.48 -
1.49 -
1.50 \section{Types, terms and formulae}
1.51 \label{sec:TypesTermsForms}
1.52 \indexbold{type}
1.53
1.54 -Embedded in the declarations of a theory are the types, terms and formulae of
1.55 -HOL. HOL is a typed logic whose type system resembles that of functional
1.56 -programming languages like ML or Haskell. Thus there are
1.57 +Embedded in a theory are the types, terms and formulae of HOL. HOL is a typed
1.58 +logic whose type system resembles that of functional programming languages
1.59 +like ML or Haskell. Thus there are
1.60 \begin{description}
1.61 -\item[base types,] in particular \ttindex{bool}, the type of truth values,
1.62 -and \ttindex{nat}, the type of natural numbers.
1.63 -\item[type constructors,] in particular \texttt{list}, the type of
1.64 -lists, and \texttt{set}, the type of sets. Type constructors are written
1.65 -postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are
1.66 +\item[base types,] in particular \isaindex{bool}, the type of truth values,
1.67 +and \isaindex{nat}, the type of natural numbers.
1.68 +\item[type constructors,] in particular \isaindex{list}, the type of
1.69 +lists, and \isaindex{set}, the type of sets. Type constructors are written
1.70 +postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
1.71 natural numbers. Parentheses around single arguments can be dropped (as in
1.72 -\texttt{nat list}), multiple arguments are separated by commas (as in
1.73 -\texttt{(bool,nat)foo}).
1.74 +\isa{nat list}), multiple arguments are separated by commas (as in
1.75 +\isa{(bool,nat)ty}).
1.76 \item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
1.77 - In HOL \isasymFun\ represents {\em total} functions only. As is customary,
1.78 - \texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
1.79 - \texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
1.80 - supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
1.81 - which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
1.82 + In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
1.83 + \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
1.84 + \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
1.85 + supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
1.86 + which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
1.87 \isasymFun~$\tau$}.
1.88 -\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in
1.89 -ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the
1.90 -type of the identity function.
1.91 +\item[type variables,]\indexbold{type variable}\indexbold{variable!type}
1.92 + denoted by \isaindexbold{'a}, \isa{'b} etc., just like in ML. They give rise
1.93 + to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
1.94 + function.
1.95 \end{description}
1.96 \begin{warn}
1.97 Types are extremely important because they prevent us from writing
1.98 @@ -145,77 +119,71 @@
1.99
1.100 \noindent
1.101 This can be reversed by \texttt{ML "reset show_types"}. Various other flags
1.102 -can be set and reset in the same manner.\bfindex{flag!(re)setting}
1.103 +can be set and reset in the same manner.\indexbold{flag!(re)setting}
1.104 \end{warn}
1.105
1.106
1.107 \textbf{Terms}\indexbold{term} are formed as in functional programming by
1.108 -applying functions to arguments. If \texttt{f} is a function of type
1.109 -\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type
1.110 -$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports
1.111 -infix functions like \texttt{+} and some basic constructs from functional
1.112 +applying functions to arguments. If \isa{f} is a function of type
1.113 +\isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
1.114 +$\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
1.115 +infix functions like \isa{+} and some basic constructs from functional
1.116 programming:
1.117 \begin{description}
1.118 -\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
1.119 +\item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
1.120 means what you think it means and requires that
1.121 -$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.
1.122 -\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}
1.123 +$b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
1.124 +\item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let}
1.125 is equivalent to $u$ where all occurrences of $x$ have been replaced by
1.126 $t$. For example,
1.127 -\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated
1.128 -by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
1.129 -\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
1.130 +\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
1.131 +by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
1.132 +\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
1.133 \indexbold{*case}
1.134 -evaluates to $e@i$ if $e$ is of the form
1.135 -$c@i$. See~\S\ref{sec:case-expressions} for details.
1.136 +evaluates to $e@i$ if $e$ is of the form $c@i$.
1.137 \end{description}
1.138
1.139 Terms may also contain
1.140 \isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,
1.141 -\texttt{\isasymlambda{}x.~x+1} is the function that takes an argument
1.142 -\texttt{x} and returns \texttt{x+1}. Instead of
1.143 -\texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$ we can write
1.144 -\texttt{\isasymlambda{}x~y~z.}~$t$.
1.145 +\isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
1.146 +returns \isa{x+1}. Instead of
1.147 +\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
1.148 +\isa{\isasymlambda{}x~y~z.~$t$}.
1.149
1.150 -\textbf{Formulae}\indexbold{formula}
1.151 -are terms of type \texttt{bool}. There are the basic
1.152 -constants \ttindexbold{True} and \ttindexbold{False} and the usual logical
1.153 -connectives (in decreasing order of priority):
1.154 -\indexboldpos{\isasymnot}{$HOL0not},
1.155 -\indexboldpos{\isasymand}{$HOL0and},
1.156 -\indexboldpos{\isasymor}{$HOL0or}, and
1.157 -\indexboldpos{\isasymimp}{$HOL0imp},
1.158 +\textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}.
1.159 +There are the basic constants \isaindexbold{True} and \isaindexbold{False} and
1.160 +the usual logical connectives (in decreasing order of priority):
1.161 +\indexboldpos{\isasymnot}{$HOL0not}, \indexboldpos{\isasymand}{$HOL0and},
1.162 +\indexboldpos{\isasymor}{$HOL0or}, and \indexboldpos{\isasymimp}{$HOL0imp},
1.163 all of which (except the unary \isasymnot) associate to the right. In
1.164 -particular \texttt{A \isasymimp~B \isasymimp~C} means
1.165 -\texttt{A \isasymimp~(B \isasymimp~C)} and is thus
1.166 -logically equivalent with \texttt{A \isasymand~B \isasymimp~C}
1.167 -(which is \texttt{(A \isasymand~B) \isasymimp~C}).
1.168 +particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
1.169 + \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
1.170 + \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
1.171
1.172 Equality is available in the form of the infix function
1.173 -\texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a
1.174 - \isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$
1.175 +\isa{=}\indexbold{$HOL0eq@\texttt{=}} of type \isa{'a \isasymFun~'a
1.176 + \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
1.177 and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
1.178 -\texttt{bool}, \texttt{=} acts as if-and-only-if. The formula
1.179 -$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for
1.180 -\texttt{\isasymnot($t@1$ = $t@2$)}.
1.181 +\isa{bool}, \isa{=} acts as if-and-only-if. The formula
1.182 +\isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
1.183 +\isa{\isasymnot($t@1$ = $t@2$)}.
1.184
1.185 The syntax for quantifiers is
1.186 -\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and
1.187 -\texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}. There is
1.188 -even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which
1.189 -means that there exists exactly one \texttt{x} that satisfies $P$.
1.190 -Nested quantifications can be abbreviated:
1.191 -\texttt{\isasymforall{}x~y~z.}~$P$ means
1.192 -\texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$.
1.193 +\isa{\isasymforall{}x.~$P$}\indexbold{$HOL0All@\isasymforall} and
1.194 +\isa{\isasymexists{}x.~$P$}\indexbold{$HOL0Ex@\isasymexists}. There is
1.195 +even \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which
1.196 +means that there exists exactly one \isa{x} that satisfies \isa{$P$}. Nested
1.197 +quantifications can be abbreviated: \isa{\isasymforall{}x~y~z.~$P$} means
1.198 +\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.
1.199
1.200 Despite type inference, it is sometimes necessary to attach explicit
1.201 -\bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as
1.202 -in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly
1.203 -and should therefore be enclosed in parentheses: \texttt{x < y::nat} is
1.204 -ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason
1.205 -for type constraints are overloaded functions like \texttt{+}, \texttt{*} and
1.206 -\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of
1.207 -overloading.)
1.208 +\textbf{type constraints}\indexbold{type constraint} to a term. The syntax is
1.209 +\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
1.210 +\ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed
1.211 +in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
1.212 +\isa{(x < y)::nat}. The main reason for type constraints are overloaded
1.213 +functions like \isa{+}, \isa{*} and \isa{<}. (See \S\ref{sec:TypeClasses} for
1.214 +a full discussion of overloading.)
1.215
1.216 \begin{warn}
1.217 In general, HOL's concrete syntax tries to follow the conventions of
1.218 @@ -234,33 +202,35 @@
1.219
1.220 \begin{itemize}
1.221 \item
1.222 -Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!
1.223 +Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
1.224 \item
1.225 -Isabelle allows infix functions like \texttt{+}. The prefix form of function
1.226 -application binds more strongly than anything else and hence \texttt{f~x + y}
1.227 -means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.
1.228 +Isabelle allows infix functions like \isa{+}. The prefix form of function
1.229 +application binds more strongly than anything else and hence \isa{f~x + y}
1.230 +means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
1.231 \item Remember that in HOL if-and-only-if is expressed using equality. But
1.232 equality has a high priority, as befitting a relation, while if-and-only-if
1.233 - typically has the lowest priority. Thus, \texttt{\isasymnot~\isasymnot~P =
1.234 - P} means \texttt{\isasymnot\isasymnot(P = P)} and not
1.235 - \texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean
1.236 - logical equivalence, enclose both operands in parentheses, as in \texttt{(A
1.237 + typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P =
1.238 + P} means \isa{\isasymnot\isasymnot(P = P)} and not
1.239 + \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
1.240 + logical equivalence, enclose both operands in parentheses, as in \isa{(A
1.241 \isasymand~B) = (B \isasymand~A)}.
1.242 \item
1.243 Constructs with an opening but without a closing delimiter bind very weakly
1.244 and should therefore be enclosed in parentheses if they appear in subterms, as
1.245 -in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if},
1.246 -\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers.
1.247 +in \isa{f = (\isasymlambda{}x.~x)}. This includes \isaindex{if},
1.248 +\isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
1.249 \item
1.250 -Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x}
1.251 -because \texttt{x.x} is always read as a single qualified identifier that
1.252 -refers to an item \texttt{x} in theory \texttt{x}. Write
1.253 -\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead.
1.254 -\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}.
1.255 +Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
1.256 +because \isa{x.x} is always read as a single qualified identifier that
1.257 +refers to an item \isa{x} in theory \isa{x}. Write
1.258 +\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
1.259 +\item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}.
1.260 \end{itemize}
1.261
1.262 -Remember that ASCII-equivalents of all mathematical symbols are
1.263 -given in figure~\ref{fig:ascii} in the appendix.
1.264 +For the sake of readability the usual mathematical symbols are used throughout
1.265 +the tutorial. Their ASCII-equivalents are shown in figure~\ref{fig:ascii} in
1.266 +the appendix.
1.267 +
1.268
1.269 \section{Variables}
1.270 \label{sec:variables}
1.271 @@ -270,9 +240,9 @@
1.272 variables are automatically renamed to avoid clashes with free variables. In
1.273 addition, Isabelle has a third kind of variable, called a \bfindex{schematic
1.274 variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
1.275 -with a \texttt{?}. Logically, an unknown is a free variable. But it may be
1.276 +with a \isa{?}. Logically, an unknown is a free variable. But it may be
1.277 instantiated by another term during the proof process. For example, the
1.278 -mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x},
1.279 +mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
1.280 which means that Isabelle can instantiate it arbitrarily. This is in contrast
1.281 to ordinary variables, which remain fixed. The programming language Prolog
1.282 calls unknowns {\em logical\/} variables.
1.283 @@ -283,11 +253,37 @@
1.284 indicates that Isabelle will automatically instantiate those unknowns
1.285 suitably when the theorem is used in some other proof.
1.286 \begin{warn}
1.287 - If you use \texttt{?}\index{$HOL0Ex@\texttt{?}} as an existential
1.288 - quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is
1.289 + If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential
1.290 + quantifier, it needs to be followed by a space. Otherwise \isa{?x} is
1.291 interpreted as a schematic variable.
1.292 \end{warn}
1.293
1.294 +\section{Interaction and interfaces}
1.295 +
1.296 +Interaction with Isabelle can either occur at the shell level or through more
1.297 +advanced interfaces. To keep the tutorial independent of the interface we
1.298 +have phrased the description of the intraction in a neutral language. For
1.299 +example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
1.300 +shell level, which is explained the first time the phrase is used. Other
1.301 +interfaces perform the same act by cursor movements and/or mouse clicks.
1.302 +Although shell-based interaction is quite feasible for the kind of proof
1.303 +scripts currently presented in this tutorial, the recommended interface for
1.304 +Isabelle/Isar is the Emacs-based \bfindex{Proof
1.305 + General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
1.306 +
1.307 +Some interfaces (including the shell level) offer special fonts with
1.308 +mathematical symbols. For those that do not, remember that ASCII-equivalents
1.309 +are shown in figure~\ref{fig:ascii} in the appendix.
1.310 +
1.311 +Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
1.312 +for example Proof General, require each command to be terminated by a
1.313 +semicolon, whereas others, for example the shell level, do not. But even at
1.314 +the shell level it is advisable to use semicolons to enforce that a command
1.315 +is executed immediately; otherwise Isabelle may wait for the next keyword
1.316 +before it knows that the command is complete. Note that for readibility
1.317 +reasons we often drop the final semicolon in the text.
1.318 +
1.319 +
1.320 \section{Getting started}
1.321
1.322 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
1.323 @@ -299,4 +295,4 @@
1.324 create theory files. While you are developing a theory, we recommend to
1.325 type each command into the file first and then enter it into Isabelle by
1.326 copy-and-paste, thus ensuring that you have a complete record of your theory.
1.327 -As mentioned earlier, Proof General offers a much superior interface.
1.328 +As mentioned above, Proof General offers a much superior interface.