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

author | paulson |

Tue, 23 Jan 1996 11:27:29 +0100 | |

changeset 1449 | 25a7ddf9c080 |

parent 1448 | 77379ae9ff0d |

child 1450 | 19a256c8086d |

Added discussion of "let" and pattern-matching

--- 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