summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 06 May 1999 11:48:09 +0200 | |

changeset 6606 | 94b638b3827c |

parent 6605 | c2754409919b |

child 6607 | df9b0abf77e0 |

Refs.

doc-src/Tutorial/basics.tex | file | annotate | diff | comparison | revisions | |

doc-src/Tutorial/fp.tex | file | annotate | diff | comparison | revisions |

--- a/doc-src/Tutorial/basics.tex Thu May 06 11:13:01 1999 +0200 +++ b/doc-src/Tutorial/basics.tex Thu May 06 11:48:09 1999 +0200 @@ -10,16 +10,15 @@ \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] We assume that the reader is familiar with the basic concepts of both fields. For excellent introductions to functional programming consult the textbooks -by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{Paulson-ML}. Although +by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although this tutorial initially concentrates on functional programming, do not be misled: HOL can express most mathematical concepts, and functional programming is just one particularly simple and ubiquitous instance. A tutorial is by definition incomplete. To fully exploit the power of the -system you need to consult the Isabelle Reference Manual~\cite{Isa-Ref-Man} -for details about Isabelle and the HOL chapter of the Logics -manual~\cite{Isa-Logics-Man} for details relating to HOL. Both manuals have a -comprehensive index. +system you need to consult the Isabelle Reference Manual~\cite{isabelle-ref} +for details about Isabelle and the Isabelle/HOL manual~\cite{isabelle-HOL} +for details relating to HOL. Both manuals have a comprehensive index. \section{Theories, proofs and interaction} \label{sec:Basic:Theories} @@ -58,7 +57,7 @@ This tutorial is concerned with introducing you to the different linguistic constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template. A complete grammar of the basic constructs is found in Appendix~A -of~\cite{Isa-Ref-Man}, for reference in times of doubt. +of~\cite{isabelle-ref}, for reference in times of doubt. The tutorial is also concerned with showing you how to prove theorems about the concepts in a theory. This involves invoking predefined theorem proving

--- a/doc-src/Tutorial/fp.tex Thu May 06 11:13:01 1999 +0200 +++ b/doc-src/Tutorial/fp.tex Thu May 06 11:48:09 1999 +0200 @@ -382,7 +382,7 @@ constructor names and $\tau@{ij}$ are types; it is customary to capitalize the first letter in constructor names. There are a number of restrictions (such as the type should not be empty) detailed -elsewhere~\cite{Isa-Logics-Man}. Isabelle notifies you if you violate them. +elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them. Laws about datatypes, such as \verb$[] ~= x#xs$ and \texttt{(x\#xs = y\#ys) = (x=y \& xs=ys)}, are used automatically during proofs by simplification. @@ -1068,7 +1068,7 @@ is commutativity: $x+y = y+x$. Another example is $(x-y)-z = (x-z)-y$. Such rules are problematic because once they apply, they can be used forever. The simplifier is aware of this danger and treats permutative rules -separately. For details see~\cite{Isa-Ref-Man}. +separately. For details see~\cite{isabelle-ref}. \subsubsection{Tracing} \indexbold{tracing the simplifier} @@ -1486,13 +1486,13 @@ For a theoretical analysis of what kinds of datatypes are feasible in HOL see, for example,~\cite{Gunter-HOL92}. There are alternatives to pure HOL: -LCF~\cite{Paulson-LCF} is a logic where types like +LCF~\cite{paulson87} is a logic where types like \begin{ttbox} datatype t = C (t -> t) \end{ttbox} do indeed make sense (note the intentionally different arrow \texttt{->}!). There is even a version of LCF on top of HOL, called -HOLCF~\cite{MuellerNvOS98}. +HOLCF~\cite{MuellerNvOS99}. \index{*primrec|)} \index{*datatype|)} @@ -1737,7 +1737,7 @@ Ackermann's function requires the lexicographic product \texttt{**}: \begin{ttbox} \input{Recdef/ack}\end{ttbox} -For details see the manual~\cite{Isa-Logics-Man} and the examples in the +For details see the manual~\cite{isabelle-HOL} and the examples in the library.