1.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy Mon Jul 23 19:06:11 2001 +0200
1.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Tue Jul 24 11:25:54 2001 +0200
1.3 @@ -19,16 +19,16 @@
1.4 empty~list and the operator that adds an element to the front of a list. For
1.5 example, the term \isa{Cons True (Cons False Nil)} is a value of
1.6 type @{typ"bool list"}, namely the list with the elements @{term"True"} and
1.7 -@{term"False"}. Because this notation becomes unwieldy very quickly, the
1.8 +@{term"False"}. Because this notation quickly becomes unwieldy, the
1.9 datatype declaration is annotated with an alternative syntax: instead of
1.10 @{term[source]Nil} and \isa{Cons x xs} we can write
1.11 @{term"[]"}\index{$HOL2list@\texttt{[]}|bold} and
1.12 @{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
1.13 -alternative syntax is the standard syntax. Thus the list \isa{Cons True
1.14 +alternative syntax is the familiar one. Thus the list \isa{Cons True
1.15 (Cons False Nil)} becomes @{term"True # False # []"}. The annotation
1.16 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)}
1.17 means that @{text"#"} associates to
1.18 -the right, i.e.\ the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
1.19 +the right: the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
1.20 and not as @{text"(x # y) # z"}.
1.21 The @{text 65} is the priority of the infix @{text"#"}.
1.22
2.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Jul 23 19:06:11 2001 +0200
2.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Jul 24 11:25:54 2001 +0200
2.3 @@ -21,16 +21,16 @@
2.4 empty~list and the operator that adds an element to the front of a list. For
2.5 example, the term \isa{Cons True (Cons False Nil)} is a value of
2.6 type \isa{bool\ list}, namely the list with the elements \isa{True} and
2.7 -\isa{False}. Because this notation becomes unwieldy very quickly, the
2.8 +\isa{False}. Because this notation quickly becomes unwieldy, the
2.9 datatype declaration is annotated with an alternative syntax: instead of
2.10 \isa{Nil} and \isa{Cons x xs} we can write
2.11 \isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and
2.12 \isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
2.13 -alternative syntax is the standard syntax. Thus the list \isa{Cons True
2.14 +alternative syntax is the familiar one. Thus the list \isa{Cons True
2.15 (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
2.16 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)}
2.17 means that \isa{{\isacharhash}} associates to
2.18 -the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
2.19 +the right: the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
2.20 and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
2.21 The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
2.22
3.1 --- a/doc-src/TutorialI/appendix.tex Mon Jul 23 19:06:11 2001 +0200
3.2 +++ b/doc-src/TutorialI/appendix.tex Tue Jul 24 11:25:54 2001 +0200
3.3 @@ -107,7 +107,7 @@
3.4 \hline
3.5 \end{tabular}
3.6 \end{center}
3.7 -\caption{Mathematical symbols, their \textsc{ascii}-equivalents and internal names}
3.8 +\caption{Mathematical Symbols, Their \textsc{ascii}-Equivalents and Internal Names}
3.9 \label{tab:ascii}
3.10 \end{table}\indexbold{ASCII@\textsc{ascii} symbols}
3.11
3.12 @@ -153,7 +153,7 @@
3.13 \hline
3.14 \end{tabular}
3.15 \end{center}
3.16 -\caption{Reserved words in HOL terms}
3.17 +\caption{Reserved Words in HOL Terms}
3.18 \label{tab:ReservedWords}
3.19 \end{table}
3.20
3.21 @@ -185,6 +185,6 @@
3.22 %\hline
3.23 %\end{tabular}
3.24 %\end{center}
3.25 -%\caption{Minor keywords in HOL theories}
3.26 +%\caption{Minor Keywords in HOL Theories}
3.27 %\label{tab:keywords}
3.28 %\end{table}
4.1 --- a/doc-src/TutorialI/basics.tex Mon Jul 23 19:06:11 2001 +0200
4.2 +++ b/doc-src/TutorialI/basics.tex Tue Jul 24 11:25:54 2001 +0200
4.3 @@ -8,10 +8,11 @@
4.4 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
4.5 HOL step by step following the equation
4.6 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
4.7 -We do not assume that the reader is familiar with mathematical logic but that
4.8 -(s)he is used to logical and set theoretic notation, such as covered
4.9 -in a good discrete math course~\cite{Rosen-DMA}. In contrast, we do assume
4.10 -that the reader is familiar with the basic concepts of functional
4.11 +We do not assume that you are familiar with mathematical logic but that
4.12 +you are used to logical and set theoretic notation, such as covered
4.13 +in a good discrete mathematics course~\cite{Rosen-DMA}.
4.14 +In contrast, we do assume
4.15 +that you are familiar with the basic concepts of functional
4.16 programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
4.17 Although this tutorial initially concentrates on functional programming, do
4.18 not be misled: HOL can express most mathematical concepts, and functional
4.19 @@ -19,15 +20,16 @@
4.20
4.21 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has
4.22 influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant
4.23 -for us because this tutorial is based on
4.24 +for us: this tutorial is based on
4.25 Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides
4.26 the implementation language almost completely. Thus the full name of the
4.27 system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.
4.28
4.29 There are other implementations of HOL, in particular the one by Mike Gordon
4.30 +\index{Gordon, Mike}%
4.31 \emph{et al.}, which is usually referred to as ``the HOL system''
4.32 \cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes
4.33 -its incarnation Isabelle/HOL.
4.34 +its incarnation Isabelle/HOL\@.
4.35
4.36 A tutorial is by definition incomplete. Currently the tutorial only
4.37 introduces the rudiments of Isar's proof language. To fully exploit the power
4.38 @@ -50,23 +52,24 @@
4.39 format of a theory \texttt{T} is
4.40 \begin{ttbox}
4.41 theory T = B\(@1\) + \(\cdots\) + B\(@n\):
4.42 -\(\textit{declarations, definitions, and proofs}\)
4.43 +{\rmfamily\textit{declarations, definitions, and proofs}}
4.44 end
4.45 \end{ttbox}
4.46 where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
4.47 -theories that \texttt{T} is based on and \texttt{\textit{declarations,
4.48 - definitions, and proofs}} represents the newly introduced concepts
4.49 +theories that \texttt{T} is based on and \textit{declarations,
4.50 + definitions, and proofs} represents the newly introduced concepts
4.51 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
4.52 -direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
4.53 -Everything defined in the parent theories (and their parents \dots) is
4.54 +direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@.
4.55 +Everything defined in the parent theories (and their parents, recursively) is
4.56 automatically visible. To avoid name clashes, identifiers can be
4.57 -\textbf{qualified} by theory names as in \texttt{T.f} and
4.58 -\texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
4.59 +\textbf{qualified}\indexbold{identifiers!qualified}
4.60 +by theory names as in \texttt{T.f} and~\texttt{B.f}.
4.61 +Each theory \texttt{T} must
4.62 reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}.
4.63
4.64 This tutorial is concerned with introducing you to the different linguistic
4.65 -constructs that can fill \textit{\texttt{declarations, definitions, and
4.66 - proofs}} in the above theory template. A complete grammar of the basic
4.67 +constructs that can fill the \textit{declarations, definitions, and
4.68 + proofs} above. A complete grammar of the basic
4.69 constructs is found in the Isabelle/Isar Reference Manual.
4.70
4.71 HOL's theory collection is available online at
4.72 @@ -92,24 +95,28 @@
4.73
4.74 Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
4.75 logic whose type system resembles that of functional programming languages
4.76 -like ML or Haskell. Thus there are\index{types}
4.77 +like ML or Haskell. Thus there are
4.78 +\index{types|(}
4.79 \begin{description}
4.80 -\item[base types,] in particular \tydx{bool}, the type of truth values,
4.81 +\item[base types,]
4.82 +in particular \tydx{bool}, the type of truth values,
4.83 and \tydx{nat}, the type of natural numbers.
4.84 -\item[type constructors,] in particular \tydx{list}, the type of
4.85 +\item[type constructors,]\index{type constructors}
4.86 + in particular \tydx{list}, the type of
4.87 lists, and \tydx{set}, the type of sets. Type constructors are written
4.88 postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
4.89 natural numbers. Parentheses around single arguments can be dropped (as in
4.90 \isa{nat list}), multiple arguments are separated by commas (as in
4.91 \isa{(bool,nat)ty}).
4.92 -\item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
4.93 +\item[function types,]\index{function types}
4.94 +denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
4.95 In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
4.96 \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
4.97 \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
4.98 supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
4.99 which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
4.100 \isasymFun~$\tau$}.
4.101 -\item[type variables,]\indexbold{type variables}\indexbold{variables!type}
4.102 +\item[type variables,]\index{type variables}\index{variables!type}
4.103 denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
4.104 to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
4.105 function.
4.106 @@ -125,7 +132,7 @@
4.107 strange happens, we recommend that you set the flag\index{flags}
4.108 \isa{show_types}\index{*show_types (flag)}.
4.109 Isabelle will then display type information
4.110 - that is usually suppressed. simply type
4.111 + that is usually suppressed. Simply type
4.112 \begin{ttbox}
4.113 ML "set show_types"
4.114 \end{ttbox}
4.115 @@ -134,36 +141,41 @@
4.116 This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
4.117 which we introduce as we go along, can be set and reset in the same manner.%
4.118 \index{flags!setting and resetting}
4.119 -\end{warn}
4.120 +\end{warn}%
4.121 +\index{types|)}
4.122
4.123
4.124 -\textbf{Terms}\index{terms} are formed as in functional programming by
4.125 +\index{terms|(}
4.126 +\textbf{Terms} are formed as in functional programming by
4.127 applying functions to arguments. If \isa{f} is a function of type
4.128 \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
4.129 $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
4.130 infix functions like \isa{+} and some basic constructs from functional
4.131 programming, such as conditional expressions:
4.132 \begin{description}
4.133 -\item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if (symbol)}
4.134 +\item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}
4.135 Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
4.136 -\item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let (symbol)}
4.137 +\item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}
4.138 is equivalent to $u$ where all occurrences of $x$ have been replaced by
4.139 $t$. For example,
4.140 \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
4.141 by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
4.142 \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
4.143 -\indexbold{*case (symbol)}
4.144 +\index{*case expressions}
4.145 evaluates to $e@i$ if $e$ is of the form $c@i$.
4.146 \end{description}
4.147
4.148 Terms may also contain
4.149 -\isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,
4.150 +\isasymlambda-abstractions.\index{lambda@$\lambda$ expressions}
4.151 +For example,
4.152 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
4.153 returns \isa{x+1}. Instead of
4.154 \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
4.155 -\isa{\isasymlambda{}x~y~z.~$t$}.
4.156 +\isa{\isasymlambda{}x~y~z.~$t$}.%
4.157 +\index{terms|)}
4.158
4.159 -\textbf{Formulae}\indexbold{formulae} are terms of type \tydx{bool}.
4.160 +\index{formulae|(}%
4.161 +\textbf{Formulae} are terms of type \tydx{bool}.
4.162 There are the basic constants \cdx{True} and \cdx{False} and
4.163 the usual logical connectives (in decreasing order of priority):
4.164 \indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
4.165 @@ -173,49 +185,41 @@
4.166 \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
4.167 \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
4.168
4.169 -Equality is available in the form of the infix function
4.170 -\isa{=}\indexbold{$HOL0eq@\texttt{=}} of type \isa{'a \isasymFun~'a
4.171 +Equality\index{equality} is available in the form of the infix function
4.172 +\isa{=} of type \isa{'a \isasymFun~'a
4.173 \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
4.174 -and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
4.175 -\isa{bool}, \isa{=} acts as if-and-only-if. The formula
4.176 +and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type
4.177 +\isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}.
4.178 +The formula
4.179 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
4.180 \isa{\isasymnot($t@1$ = $t@2$)}.
4.181
4.182 -Quantifiers are written as
4.183 -\isa{\isasymforall{}x.~$P$}\index{$HOL0All@\isasymforall|bold} and
4.184 -\isa{\isasymexists{}x.~$P$}\index{$HOL0Ex@\isasymexists|bold}.
4.185 +Quantifiers\index{quantifiers} are written as
4.186 +\isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}.
4.187 There is even
4.188 -\isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which
4.189 +\isa{\isasymuniqex{}x.~$P$}, which
4.190 means that there exists exactly one \isa{x} that satisfies \isa{$P$}.
4.191 Nested quantifications can be abbreviated:
4.192 \isa{\isasymforall{}x~y~z.~$P$} means
4.193 -\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.
4.194 +\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.%
4.195 +\index{formulae|)}
4.196
4.197 Despite type inference, it is sometimes necessary to attach explicit
4.198 \bfindex{type constraints} to a term. The syntax is
4.199 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
4.200 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
4.201 -in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
4.202 -\isa{(x < y)::nat}. The main reason for type constraints is overloading of
4.203 -functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for
4.204 -a full discussion of overloading and Table~\ref{tab:overloading} for the most
4.205 +in parentheses. For instance,
4.206 +\isa{x < y::nat} is ill-typed because it is interpreted as
4.207 +\isa{(x < y)::nat}. Type constraints may be needed to disambiguate
4.208 +expressions
4.209 +involving overloaded functions such as~\isa{+},
4.210 +\isa{*} and~\isa{<}. Section~\ref{sec:overloading}
4.211 +discusses overloading, while Table~\ref{tab:overloading} presents the most
4.212 important overloaded function symbols.
4.213
4.214 -\begin{warn}
4.215 -In general, HOL's concrete syntax tries to follow the conventions of
4.216 -functional programming and mathematics. Below we list the main rules that you
4.217 -should be familiar with to avoid certain syntactic traps. A particular
4.218 -problem for novices can be the priority of operators. If you are unsure, use
4.219 -additional parentheses. In those cases where Isabelle echoes your
4.220 -input, you can see which parentheses are dropped --- they were superfluous. If
4.221 -you are unsure how to interpret Isabelle's output because you don't know
4.222 -where the (dropped) parentheses go, set the flag\index{flags}
4.223 -\isa{show_brackets}\index{*show_brackets (flag)}:
4.224 -\begin{ttbox}
4.225 -ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
4.226 -\end{ttbox}
4.227 -\end{warn}
4.228 -
4.229 +In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of
4.230 +functional programming and mathematics. Here are the main rules that you
4.231 +should be familiar with to avoid certain syntactic traps:
4.232 \begin{itemize}
4.233 \item
4.234 Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
4.235 @@ -233,26 +237,43 @@
4.236 \item
4.237 Constructs with an opening but without a closing delimiter bind very weakly
4.238 and should therefore be enclosed in parentheses if they appear in subterms, as
4.239 -in \isa{(\isasymlambda{}x.~x) = f}. This includes \sdx{if},
4.240 -\sdx{let}, \sdx{case}, \isa{\isasymlambda}, and quantifiers.
4.241 +in \isa{(\isasymlambda{}x.~x) = f}. This includes
4.242 +\isa{if},\index{*if expressions}
4.243 +\isa{let},\index{*let expressions}
4.244 +\isa{case},\index{*case expressions}
4.245 +\isa{\isasymlambda}, and quantifiers.
4.246 \item
4.247 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
4.248 -because \isa{x.x} is always read as a single qualified identifier that
4.249 +because \isa{x.x} is always taken as a single qualified identifier that
4.250 refers to an item \isa{x} in theory \isa{x}. Write
4.251 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
4.252 -\item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}.
4.253 +\item Identifiers\indexbold{identifiers} may contain the characters \isa{_}
4.254 +and~\isa{'}.
4.255 \end{itemize}
4.256
4.257 -For the sake of readability the usual mathematical symbols are used throughout
4.258 +For the sake of readability, we use the usual mathematical symbols throughout
4.259 the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
4.260 the appendix.
4.261
4.262 +\begin{warn}
4.263 +A particular
4.264 +problem for novices can be the priority of operators. If you are unsure, use
4.265 +additional parentheses. In those cases where Isabelle echoes your
4.266 +input, you can see which parentheses are dropped --- they were superfluous. If
4.267 +you are unsure how to interpret Isabelle's output because you don't know
4.268 +where the (dropped) parentheses go, set the flag\index{flags}
4.269 +\isa{show_brackets}\index{*show_brackets (flag)}:
4.270 +\begin{ttbox}
4.271 +ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
4.272 +\end{ttbox}
4.273 +\end{warn}
4.274 +
4.275
4.276 \section{Variables}
4.277 \label{sec:variables}
4.278 -\indexbold{variable}
4.279 +\index{variables|(}
4.280
4.281 -Isabelle distinguishes free and bound variables just as is customary. Bound
4.282 +Isabelle distinguishes free and bound variables, as is customary. Bound
4.283 variables are automatically renamed to avoid clashes with free variables. In
4.284 addition, Isabelle has a third kind of variable, called a \textbf{schematic
4.285 variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns},
4.286 @@ -266,15 +287,18 @@
4.287
4.288 Most of the time you can and should ignore unknowns and work with ordinary
4.289 variables. Just don't be surprised that after you have finished the proof of
4.290 -a theorem, Isabelle will turn your free variables into unknowns: it merely
4.291 +a theorem, Isabelle will turn your free variables into unknowns. It
4.292 indicates that Isabelle will automatically instantiate those unknowns
4.293 suitably when the theorem is used in some other proof.
4.294 Note that for readability we often drop the \isa{?}s when displaying a theorem.
4.295 \begin{warn}
4.296 - If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential
4.297 - quantifier, it needs to be followed by a space. Otherwise \isa{?x} is
4.298 - interpreted as a schematic variable.
4.299 -\end{warn}
4.300 + For historical reasons, Isabelle accepts \isa{?} as an ASCII representation
4.301 + of the \(\exists\) symbol. However, the \isa{?} character must then be followed
4.302 + by a space, as in \isa{?~x. f(x) = 0}. Otherwise, \isa{?x} is
4.303 + interpreted as a schematic variable. The preferred ASCII representation of
4.304 + the \(\exists\) symbol is \isa{EX}\@.
4.305 +\end{warn}%
4.306 +\index{variables|)}
4.307
4.308 \section{Interaction and Interfaces}
4.309
4.310 @@ -287,7 +311,7 @@
4.311 Although shell-based interaction is quite feasible for the kind of proof
4.312 scripts currently presented in this tutorial, the recommended interface for
4.313 Isabelle/Isar is the Emacs-based \bfindex{Proof
4.314 - General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
4.315 + General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
4.316
4.317 Some interfaces (including the shell level) offer special fonts with
4.318 mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
4.319 @@ -308,7 +332,7 @@
4.320 controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
4.321 System Manual} for more details.} This presents you with Isabelle's most
4.322 basic \textsc{ascii} interface. In addition you need to open an editor window to
4.323 -create theory files. While you are developing a theory, we recommend to
4.324 +create theory files. While you are developing a theory, we recommend that you
4.325 type each command into the file first and then enter it into Isabelle by
4.326 copy-and-paste, thus ensuring that you have a complete record of your theory.
4.327 As mentioned above, Proof General offers a much superior interface.
5.1 --- a/doc-src/TutorialI/fp.tex Mon Jul 23 19:06:11 2001 +0200
5.2 +++ b/doc-src/TutorialI/fp.tex Tue Jul 24 11:25:54 2001 +0200
5.3 @@ -1,17 +1,19 @@
5.4 \chapter{Functional Programming in HOL}
5.5
5.6 -Although on the surface this chapter is mainly concerned with how to write
5.7 -functional programs in HOL and how to verify them, most of the constructs and
5.8 -proof procedures introduced are general purpose and recur in any specification
5.9 -or verification task. In fact, we really should speak of functional
5.10 -\emph{modelling} rather than \emph{programming}: our primary aim is not
5.11 +This chapter describes how to write
5.12 +functional programs in HOL and how to verify them. However,
5.13 +most of the constructs and
5.14 +proof procedures introduced are general and recur in any specification
5.15 +or verification task. We really should speak of functional
5.16 +\emph{modelling} rather than functional \emph{programming}:
5.17 +our primary aim is not
5.18 to write programs but to design abstract models of systems. HOL is
5.19 a specification language that goes well beyond what can be expressed as a
5.20 program. However, for the time being we concentrate on the computable.
5.21
5.22 -The dedicated functional programmer should be warned: HOL offers only
5.23 -\emph{total functional programming} --- all functions in HOL must be total,
5.24 -i.e.\ they must terminate for all inputs; lazy data structures are not
5.25 +If you are a purist functional programmer, please note that all functions
5.26 +in HOL must be total:
5.27 +they must terminate for all inputs. Lazy data structures are not
5.28 directly available.
5.29
5.30 \section{An Introductory Theory}
5.31 @@ -25,22 +27,24 @@
5.32 \begin{figure}[htbp]
5.33 \begin{ttbox}\makeatother
5.34 \input{ToyList2/ToyList1}\end{ttbox}
5.35 -\caption{A theory of lists}
5.36 +\caption{A Theory of Lists}
5.37 \label{fig:ToyList}
5.38 \end{figure}
5.39
5.40 +\index{*ToyList (example)|(}
5.41 {\makeatother\input{ToyList/document/ToyList.tex}}
5.42
5.43 The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
5.44 concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
5.45 constitutes the complete theory \texttt{ToyList} and should reside in file
5.46 \texttt{ToyList.thy}. It is good practice to present all declarations and
5.47 -definitions at the beginning of a theory to facilitate browsing.
5.48 +definitions at the beginning of a theory to facilitate browsing.%
5.49 +\index{*ToyList (example)|)}
5.50
5.51 \begin{figure}[htbp]
5.52 \begin{ttbox}\makeatother
5.53 \input{ToyList2/ToyList2}\end{ttbox}
5.54 -\caption{Proofs about lists}
5.55 +\caption{Proofs about Lists}
5.56 \label{fig:ToyList-proofs}
5.57 \end{figure}
5.58
5.59 @@ -465,7 +469,7 @@
5.60 \put(30,30){\line(3,-2){13}}
5.61 \end{picture}
5.62 \end{center}
5.63 -\caption{A sample trie}
5.64 +\caption{A Sample Trie}
5.65 \label{fig:trie}
5.66 \end{figure}
5.67
6.1 --- a/doc-src/TutorialI/preface.tex Mon Jul 23 19:06:11 2001 +0200
6.2 +++ b/doc-src/TutorialI/preface.tex Tue Jul 24 11:25:54 2001 +0200
6.3 @@ -8,8 +8,9 @@
6.4 discussion of meta-theory. It is written for potential users rather
6.5 than for our colleagues in the research world.
6.6
6.7 -Another departure from previous documentation is the use of Markus
6.8 -Wenzel's proof script notation instead of ML tactic files. The latter
6.9 +\index{Wenzel, Markus}%
6.10 +Another departure from previous documentation is that we describe Markus
6.11 +Wenzel's proof script notation instead of ML tactic scripts. The latter
6.12 make it easier to introduce new tactics on the fly, but hardly anybody
6.13 does that. Wenzel's dedicated syntax is elegant, replacing for example
6.14 eight simplification tactics with a single method, namely \isa{simp},
7.1 --- a/doc-src/TutorialI/tutorial.ind Mon Jul 23 19:06:11 2001 +0200
7.2 +++ b/doc-src/TutorialI/tutorial.ind Tue Jul 24 11:25:54 2001 +0200
7.3 @@ -1,20 +1,16 @@
7.4 \begin{theindex}
7.5
7.6 \item \emph {$\forall \tmspace +\thinmuskip {.1667em}$}, \bold{189}
7.7 - \item \isasymforall, \bold{3}
7.8 \item \ttall, \bold{189}
7.9 \item \emph {$\exists \tmspace +\thinmuskip {.1667em}$}, \bold{189}
7.10 - \item \isasymexists, \bold{3}
7.11 \item \texttt{?}, 5, \bold{189}
7.12 \item \emph {$\varepsilon $}, \bold{189}
7.13 - \item \isasymuniqex, \bold{3}, \bold{189}
7.14 + \item \isasymuniqex, \bold{189}
7.15 \item \ttuniquex, \bold{189}
7.16 \item \emph {$\wedge $}, \bold{189}
7.17 \item \isasymand, \bold{3}
7.18 \item {\texttt {\&}}, \bold{189}
7.19 - \item \texttt {=}, \bold{3}
7.20 - \item \emph {$\DOTSB \mathrel {\smash -}\mathrel {\mkern -3mu}\rightarrow $},
7.21 - \bold{189}
7.22 + \item \emph {$\DOTSB \relbar \joinrel \rightarrow $}, \bold{189}
7.23 \item \isasymimp, \bold{3}
7.24 \item \texttt {-->}, \bold{189}
7.25 \item \emph {$\neg $}, \bold{189}
7.26 @@ -60,14 +56,13 @@
7.27 \item \emph {$\Rightarrow $}, \bold{3}, \bold{189}
7.28 \item \texttt {=>}, \bold{189}
7.29 \item \texttt {<=}, \bold{189}
7.30 - \item \emph {$\DOTSB \mathrel =\mathrel {\mkern -3mu}\Rightarrow $},
7.31 - \bold{189}
7.32 + \item \emph {$\DOTSB \Relbar \joinrel \Rightarrow $}, \bold{189}
7.33 \item \texttt {==>}, \bold{189}
7.34 \item \emph {$\mathopen {[\mkern -3mu[}$}, \bold{10}, \bold{189}
7.35 \item \ttlbr, \bold{189}
7.36 \item \emph {$\mathclose {]\mkern -3mu]}$}, \bold{10}, \bold{189}
7.37 \item \ttrbr, \bold{189}
7.38 - \item \emph {$\lambda $}, \bold{3}, \bold{189}
7.39 + \item \emph {$\lambda $}, \bold{189}
7.40 \item \texttt {\%}, \bold{189}
7.41 \item \texttt {,}, \bold{29}
7.42 \item \texttt {;}, \bold{5}
7.43 @@ -138,7 +133,8 @@
7.44 \item \isa {card_Pow} (theorem), \bold{93}
7.45 \item \isa {card_Un_Int} (theorem), \bold{93}
7.46 \item cardinality, 93
7.47 - \item \isa {case} (symbol), \bold{3}, 4, 16, 30, 31
7.48 + \item \isa {case} (symbol), 16, 30, 31
7.49 + \item \isa {case} expressions, 3, 4
7.50 \item case distinction, \bold{17}
7.51 \item case splits, \bold{29}
7.52 \item \isa {case_tac} (method), 17, 85
7.53 @@ -154,6 +150,7 @@
7.54 \item composition
7.55 \subitem of functions, \bold{94}
7.56 \subitem of relations, \bold{96}
7.57 + \item conditional expressions, \see{\isa{if} expressions}{1}
7.58 \item congruence rules, \bold{157}
7.59 \item \isa {conjE} (theorem), \bold{55}
7.60 \item \isa {conjI} (theorem), \bold{52}
7.61 @@ -202,7 +199,7 @@
7.62 \item \isa {elim!} (attribute), 115
7.63 \item elimination rules, 53--54
7.64 \item \isa {Eps} (constant), 93
7.65 - \item equality
7.66 + \item equality, 3
7.67 \subitem of functions, \bold{93}
7.68 \subitem of records, 143
7.69 \subitem of sets, \bold{90}
7.70 @@ -234,11 +231,12 @@
7.71 \item flags, 3, 4, 31
7.72 \subitem setting and resetting, 3
7.73 \item \isa {force} (method), 75, 76
7.74 - \item formulae, \bold{3}
7.75 + \item formulae, 3
7.76 \item forward proof, 76--82
7.77 \item \isa {frule} (method), 67
7.78 \item \isa {frule_tac} (method), 60
7.79 \item \isa {fst} (constant), 21
7.80 + \item function types, 3
7.81 \item functions, 93--95
7.82 \subitem total, 9, 45--50
7.83 \subitem underdefined, 165
7.84 @@ -248,6 +246,7 @@
7.85 \item \isa {gcd} (constant), 76--78, 85--87
7.86 \item generalizing for induction, 113
7.87 \item Girard, Jean-Yves, \fnote{55}
7.88 + \item Gordon, Mike, 1
7.89 \item ground terms example, 119--124
7.90
7.91 \indexspace
7.92 @@ -262,10 +261,12 @@
7.93 \item \isa {Id_def} (theorem), \bold{96}
7.94 \item \isa {id_def} (theorem), \bold{94}
7.95 \item identifier, \bold{4}
7.96 + \item identifiers
7.97 \subitem qualified, \bold{2}
7.98 \item identity function, \bold{94}
7.99 \item identity relation, \bold{96}
7.100 - \item \isa {if} (symbol), \bold{3}, 4
7.101 + \item \isa {if} expressions, 3, 4
7.102 + \item if-and-only-if, 3
7.103 \item \isa {iff} (attribute), 73, 74, 86, 114
7.104 \item \isa {iffD1} (theorem), \bold{78}
7.105 \item \isa {iffD2} (theorem), \bold{78}
7.106 @@ -324,6 +325,7 @@
7.107
7.108 \indexspace
7.109
7.110 + \item $\lambda$ expressions, 3
7.111 \item \isa {LEAST} (symbol), 21, 69
7.112 \item least number operator, \see{\protect\isa{LEAST}}{69}
7.113 \item \isacommand {lemma} (command), 11
7.114 @@ -332,7 +334,8 @@
7.115 \item \isa {length_induct}, \bold{172}
7.116 \item \isa {less_than} (constant), 98
7.117 \item \isa {less_than_iff} (theorem), \bold{98}
7.118 - \item \isa {let} (symbol), \bold{3}, 4, 29
7.119 + \item \isa {let} (symbol), 29
7.120 + \item \isa {let} expressions, 3, 4
7.121 \item \isa {lex_prod_def} (theorem), \bold{99}
7.122 \item lexicographic product, \bold{99}, 160
7.123 \item {\texttt{lfp}}
7.124 @@ -400,7 +403,7 @@
7.125 \indexspace
7.126
7.127 \item pairs and tuples, 21, 137--140
7.128 - \item parent theory, \bold{2}
7.129 + \item parent theories, \bold{2}
7.130 \item partial function, 164
7.131 \item pattern, higher-order, \bold{159}
7.132 \item PDL, 102--105
7.133 @@ -419,7 +422,7 @@
7.134
7.135 \indexspace
7.136
7.137 - \item quantifiers
7.138 + \item quantifiers, 3
7.139 \subitem and inductive definitions, 119--121
7.140 \subitem existential, 66
7.141 \subitem for sets, 92
7.142 @@ -543,11 +546,12 @@
7.143 \item tuples, \see{pairs and tuples}{1}
7.144 \item \isacommand {typ} (command), 14
7.145 \item type constraints, \bold{4}
7.146 + \item type constructors, 2
7.147 \item type inference, \bold{3}
7.148 - \item type variables, \bold{3}
7.149 + \item type variables, 3
7.150 \item \isacommand {typedecl} (command), 150
7.151 \item \isacommand {typedef} (command), 151--155
7.152 - \item types, 2
7.153 + \item types, 2--3
7.154 \subitem declaring, 150--151
7.155 \subitem defining, 151--155
7.156 \item \isacommand {types} (command), 22
7.157 @@ -577,11 +581,12 @@
7.158 \item variable, \bold{4}
7.159 \item variables
7.160 \subitem schematic, 4
7.161 - \subitem type, \bold{3}
7.162 + \subitem type, 3
7.163 \item \isa {vimage_def} (theorem), \bold{95}
7.164
7.165 \indexspace
7.166
7.167 + \item Wenzel, Markus, v
7.168 \item \isa {wf_induct} (theorem), \bold{99}
7.169 \item \isa {while} (constant), 167
7.170 \item \isa {While_Combinator} (theory), 167
8.1 --- a/doc-src/TutorialI/tutorial.tex Mon Jul 23 19:06:11 2001 +0200
8.2 +++ b/doc-src/TutorialI/tutorial.tex Tue Jul 24 11:25:54 2001 +0200
8.3 @@ -10,6 +10,7 @@
8.4
8.5 \makeindex
8.6
8.7 +\index{conditional expressions|see{\isa{if} expressions}}
8.8 \index{primitive recursion|see{\isacommand{primrec}}}
8.9 \index{product type|see{pairs and tuples}}
8.10 \index{termination|see{functions, total}}
8.11 @@ -42,7 +43,7 @@
8.12
8.13 \tableofcontents
8.14
8.15 -\newpage\pagenumbering{arabic}
8.16 +\cleardoublepage\pagenumbering{arabic}
8.17
8.18 \input{basics}
8.19 \input{fp}