Added discussion of "let" and pattern-matching
authorpaulson
Tue Jan 23 11:27:29 1996 +0100 (1996-01-23)
changeset 144925a7ddf9c080
parent 1448 77379ae9ff0d
child 1450 19a256c8086d
Added discussion of "let" and pattern-matching
doc-src/Logics/ZF.tex
     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