--- a/doc-src/Logics/ZF.tex Tue Jan 23 11:10:39 1996 +0100
+++ b/doc-src/Logics/ZF.tex Tue Jan 23 11:27:29 1996 +0100
@@ -67,6 +67,7 @@
\begin{center}
\begin{tabular}{rrr}
\it name &\it meta-type & \it description \\
+ \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\
\cdx{0} & $i$ & empty set\\
\cdx{cons} & $[i,i]\To i$ & finite set constructor\\
\cdx{Upair} & $[i,i]\To i$ & unordered pairing\\
@@ -134,8 +135,13 @@
Figure~\ref{zf-syntax} presents the full grammar for set theory, including
the constructs of \FOL.
-Set theory does not use polymorphism. All terms in {\ZF} have
-type~\tydx{i}, which is the type of individuals and has class~{\tt
+Local abbreviations can be introduced by a {\tt let} construct whose
+syntax appears in Fig.\ts\ref{zf-syntax}. Internally it is translated into
+the constant~\cdx{Let}. It can be expanded by rewriting with its
+definition, \tdx{Let_def}.
+
+Apart from {\tt let}, set theory does not use polymorphism. All terms in
+{\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt
term}. The type of first-order formulae, remember, is~{\tt o}.
Infix operators include binary union and intersection ($A\union B$ and
@@ -219,9 +225,12 @@
\begin{figure}
+\index{*let symbol}
+\index{*in symbol}
\dquotes
\[\begin{array}{rcl}
term & = & \hbox{expression of type~$i$} \\
+ & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\
& | & "\{ " term\; ("," term)^* " \}" \\
& | & "< " term\; ("," term)^* " >" \\
& | & "\{ " id ":" term " . " formula " \}" \\
@@ -344,6 +353,8 @@
\begin{figure}
\begin{ttbox}
+\tdx{Let_def} Let(s, f) == f(s)
+
\tdx{Ball_def} Ball(A,P) == ALL x. x:A --> P(x)
\tdx{Bex_def} Bex(A,P) == EX x. x:A & P(x)
@@ -784,6 +795,31 @@
merely states that $\pair{a,b}\in {\tt Sigma}(A,B)$ implies $a\in A$ and
$b\in B(a)$.
+In addition, it is possible to use tuples as patterns in abstractions:
+\begin{center}
+{\tt\%<$x$,$y$>.$t$} \quad stands for\quad {\tt split(\%$x$ $y$.$t$)}
+\end{center}
+Nested patterns are translated recursively:
+{\tt\%<$x$,$y$,$z$>.$t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>.$t$} $\leadsto$
+{\tt split(\%$x$.\%<$y$,$z$>.$t$)} $\leadsto$ {\tt split(\%$x$.split(\%$y$
+ $z$.$t$))}. The reverse translation is performed upon printing.
+\begin{warn}
+ The translation between patterns and {\tt split} is performed automatically
+ by the parser and printer. Thus the internal and external form of a term
+ may differ, whichs affects proofs. For example the term {\tt
+ (\%<x,y>.<y,x>)<a,b>} requires the theorem {\tt split} to rewrite to
+ {\tt<b,a>}.
+\end{warn}
+In addition to explicit $\lambda$-abstractions, patterns can be used in any
+variable binding construct which is internally described by a
+$\lambda$-abstraction. Some important examples are
+\begin{description}
+\item[Let:] {\tt let {\it pattern} = $t$ in $u$}
+\item[Choice:] {\tt THE~{\it pattern}~.~$P$}
+\item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$}
+\item[Comprehension:] {\tt \{~{\it pattern}:$A$~.~$P$~\}}
+\end{description}
+
%%% domrange.ML