author paulson Tue Jan 23 11:27:29 1996 +0100 (1996-01-23) changeset 1449 25a7ddf9c080 parent 1448 77379ae9ff0d child 1450 19a256c8086d
Added discussion of "let" and pattern-matching
 doc-src/Logics/ZF.tex file | annotate | diff | revisions
     1.1 --- a/doc-src/Logics/ZF.tex	Tue Jan 23 11:10:39 1996 +0100
1.2 +++ b/doc-src/Logics/ZF.tex	Tue Jan 23 11:27:29 1996 +0100
1.3 @@ -67,6 +67,7 @@
1.4  \begin{center}
1.5  \begin{tabular}{rrr}
1.6    \it name      &\it meta-type  & \it description \\
1.7 +  \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\
1.8    \cdx{0}       & $i$           & empty set\\
1.9    \cdx{cons}    & $[i,i]\To i$  & finite set constructor\\
1.10    \cdx{Upair}   & $[i,i]\To i$  & unordered pairing\\
1.11 @@ -134,8 +135,13 @@
1.12  Figure~\ref{zf-syntax} presents the full grammar for set theory, including
1.13  the constructs of \FOL.
1.14
1.15 -Set theory does not use polymorphism.  All terms in {\ZF} have
1.16 -type~\tydx{i}, which is the type of individuals and has class~{\tt
1.17 +Local abbreviations can be introduced by a {\tt let} construct whose
1.18 +syntax appears in Fig.\ts\ref{zf-syntax}.  Internally it is translated into
1.19 +the constant~\cdx{Let}.  It can be expanded by rewriting with its
1.20 +definition, \tdx{Let_def}.
1.21 +
1.22 +Apart from {\tt let}, set theory does not use polymorphism.  All terms in
1.23 +{\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt
1.24    term}.  The type of first-order formulae, remember, is~{\tt o}.
1.25
1.26  Infix operators include binary union and intersection ($A\union B$ and
1.27 @@ -219,9 +225,12 @@
1.28
1.29
1.30  \begin{figure}
1.31 +\index{*let symbol}
1.32 +\index{*in symbol}
1.33  \dquotes
1.34  \[\begin{array}{rcl}
1.35      term & = & \hbox{expression of type~$i$} \\
1.36 +         & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\
1.37           & | & "\{ " term\; ("," term)^* " \}" \\
1.38           & | & "< "  term\; ("," term)^* " >"  \\
1.39           & | & "\{ " id ":" term " . " formula " \}" \\
1.40 @@ -344,6 +353,8 @@
1.41
1.42  \begin{figure}
1.43  \begin{ttbox}
1.44 +\tdx{Let_def}            Let(s, f) == f(s)
1.45 +
1.46  \tdx{Ball_def}           Ball(A,P) == ALL x. x:A --> P(x)
1.47  \tdx{Bex_def}            Bex(A,P)  == EX x. x:A & P(x)
1.48
1.49 @@ -784,6 +795,31 @@
1.50  merely states that $\pair{a,b}\in {\tt Sigma}(A,B)$ implies $a\in A$ and
1.51  $b\in B(a)$.
1.52
1.53 +In addition, it is possible to use tuples as patterns in abstractions:
1.54 +\begin{center}
1.55 +{\tt\%<$x$,$y$>.$t$} \quad stands for\quad {\tt split(\%$x$ $y$.$t$)}
1.56 +\end{center}
1.57 +Nested patterns are translated recursively:
1.58 +{\tt\%<$x$,$y$,$z$>.$t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>.$t$} $\leadsto$
1.59 +{\tt split(\%$x$.\%<$y$,$z$>.$t$)} $\leadsto$ {\tt split(\%$x$.split(\%$y$
1.60 +  $z$.$t$))}. The reverse translation is performed upon printing.
1.61 +\begin{warn}
1.62 +  The translation between patterns and {\tt split} is performed automatically
1.63 +  by the parser and printer.  Thus the internal and external form of a term
1.64 +  may differ, whichs affects proofs.  For example the term {\tt
1.65 +    (\%<x,y>.<y,x>)<a,b>} requires the theorem {\tt split} to rewrite to
1.66 +  {\tt<b,a>}.
1.67 +\end{warn}
1.68 +In addition to explicit $\lambda$-abstractions, patterns can be used in any
1.69 +variable binding construct which is internally described by a
1.70 +$\lambda$-abstraction. Some important examples are
1.71 +\begin{description}
1.72 +\item[Let:] {\tt let {\it pattern} = $t$ in $u$}
1.73 +\item[Choice:] {\tt THE~{\it pattern}~.~$P$}
1.74 +\item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$}
1.75 +\item[Comprehension:] {\tt \{~{\it pattern}:$A$~.~$P$~\}}
1.76 +\end{description}
1.77 +
1.78
1.79  %%% domrange.ML
1.80