author nipkow Thu, 04 Apr 1996 18:01:26 +0200 changeset 1649 c4901f7161c5 parent 1648 60ded8c1748c child 1650 a4ed2655b08c
Added 'constdefs' and extended the section on 'defs'
--- a/doc-src/Intro/advanced.tex	Thu Apr 04 17:31:37 1996 +0200
+++ b/doc-src/Intro/advanced.tex	Thu Apr 04 18:01:26 1996 +0200
@@ -420,12 +420,17 @@

\indexbold{definitions} The {\bf definition part} is similar, but with the
keyword {\tt defs} instead of {\tt rules}.  {\bf Definitions} are rules of the
-form $t\equiv u$, and should serve only as abbreviations.  Isabelle checks for
-common errors in definitions, such as extra variables on the right-hand side.
-Determined users can write non-conservative definitions' by using mutual
-recursion, for example; the consequences of such actions are their
-responsibility.
-
+form $s \equiv t$, and should serve only as abbreviations. The simplest form
+of a definition is $f \equiv t$, where $f$ is a constant. Isabelle also
+allows a derived form where the parameters of $f$ appear on the left:
+\begin{itemize}
+\item In uncurried syntax: $f(x@1,\dots,x@n) \equiv u$ (\FOL, \ZF, \dots)
+\item In curried syntax: $f~x@1~\dots~x@n \equiv u$ (\HOL, \HOLCF)
+\end{itemize}
+Isabelle checks for common errors in definitions, such as extra variables on
+the right-hand side.  Determined users can write non-conservative
+definitions' by using mutual recursion, for example; the consequences of
+such actions are their responsibility.

\index{examples!of theories}
This theory extends first-order logic by declaring and defining two constants,
@@ -438,6 +443,27 @@
end
\end{ttbox}

+Declaring and defining constants can be combined:
+\begin{ttbox}
+Gate = FOL +
+constdefs  nand :: [o,o] => o
+           "nand(P,Q) == ~(P & Q)"
+           xor  :: [o,o] => o
+           "xor(P,Q)  == P & ~Q | ~P & Q"
+end
+\end{ttbox}
+{\tt constdefs} generates the names {\tt nand_def} and {\tt xor_def}
+automatically, which is why it is restricted to alphanumeric identifiers. In
+general it has the form
+\begin{ttbox}
+constdefs  $$id@1$$ :: $$\tau@1$$
+           "$$id@1 \equiv \dots$$"
+           \vdots
+           $$id@n$$ :: $$\tau@n$$
+           "$$id@n \equiv \dots$$"
+\end{ttbox}
+
+
\begin{warn}
A common mistake when writing definitions is to introduce extra free variables
on the right-hand side as in the following fictitious definition: