doc-src/Logics/ZF.tex
 changeset 1449 25a7ddf9c080 parent 713 b470cc6326aa child 2495 82ec47e0a8d3
equal inserted replaced
1448:77379ae9ff0d 1449:25a7ddf9c080
    65
    65
    66 \begin{figure}
    66 \begin{figure}
    67 \begin{center}
    67 \begin{center}
    68 \begin{tabular}{rrr}
    68 \begin{tabular}{rrr}
    69   \it name      &\it meta-type  & \it description \\
    69   \it name      &\it meta-type  & \it description \\

    70   \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\
    70   \cdx{0}       & $i$           & empty set\\
    71   \cdx{0}       & $i$           & empty set\\
    71   \cdx{cons}    & $[i,i]\To i$  & finite set constructor\\
    72   \cdx{cons}    & $[i,i]\To i$  & finite set constructor\\
    72   \cdx{Upair}   & $[i,i]\To i$  & unordered pairing\\
    73   \cdx{Upair}   & $[i,i]\To i$  & unordered pairing\\
    73   \cdx{Pair}    & $[i,i]\To i$  & ordered pairing\\
    74   \cdx{Pair}    & $[i,i]\To i$  & ordered pairing\\
    74   \cdx{Inf}     & $i$   & infinite set\\
    75   \cdx{Inf}     & $i$   & infinite set\\
   132 Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while
   133 Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while
   133 Figure~\ref{zf-trans} presents the syntax translations.  Finally,
   134 Figure~\ref{zf-trans} presents the syntax translations.  Finally,
   134 Figure~\ref{zf-syntax} presents the full grammar for set theory, including
   135 Figure~\ref{zf-syntax} presents the full grammar for set theory, including
   135 the constructs of \FOL.
   136 the constructs of \FOL.
   136
   137
   137 Set theory does not use polymorphism.  All terms in {\ZF} have
   138 Local abbreviations can be introduced by a {\tt let} construct whose
   138 type~\tydx{i}, which is the type of individuals and has class~{\tt
   139 syntax appears in Fig.\ts\ref{zf-syntax}.  Internally it is translated into

   140 the constant~\cdx{Let}.  It can be expanded by rewriting with its

   141 definition, \tdx{Let_def}.

   142

   143 Apart from {\tt let}, set theory does not use polymorphism.  All terms in

   144 {\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt
   139   term}.  The type of first-order formulae, remember, is~{\tt o}.
   145   term}.  The type of first-order formulae, remember, is~{\tt o}.
   140
   146
   141 Infix operators include binary union and intersection ($A\union B$ and
   147 Infix operators include binary union and intersection ($A\union B$ and
   142 $A\inter B$), set difference ($A-B$), and the subset and membership
   148 $A\inter B$), set difference ($A-B$), and the subset and membership
   143 relations.  Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$.  The
   149 relations.  Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$.  The
   217 \caption{Translations for {\ZF}} \label{zf-trans}
   223 \caption{Translations for {\ZF}} \label{zf-trans}
   218 \end{figure}
   224 \end{figure}
   219
   225
   220
   226
   221 \begin{figure}
   227 \begin{figure}

   228 \index{*let symbol}

   229 \index{*in symbol}
   222 \dquotes
   230 \dquotes
   223 \[\begin{array}{rcl}
   231 \[\begin{array}{rcl}
   224     term & = & \hbox{expression of type~$i$} \\
   232     term & = & \hbox{expression of type~$i$} \\

   233          & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\
   225          & | & "\{ " term\; ("," term)^* " \}" \\
   234          & | & "\{ " term\; ("," term)^* " \}" \\
   226          & | & "< "  term\; ("," term)^* " >"  \\
   235          & | & "< "  term\; ("," term)^* " >"  \\
   227          & | & "\{ " id ":" term " . " formula " \}" \\
   236          & | & "\{ " id ":" term " . " formula " \}" \\
   228          & | & "\{ " id " . " id ":" term ", " formula " \}" \\
   237          & | & "\{ " id " . " id ":" term ", " formula " \}" \\
   229          & | & "\{ " term " . " id ":" term " \}" \\
   238          & | & "\{ " term " . " id ":" term " \}" \\
   342
   351
   343 %%%% ZF.thy
   352 %%%% ZF.thy
   344
   353
   345 \begin{figure}
   354 \begin{figure}
   346 \begin{ttbox}
   355 \begin{ttbox}

   356 \tdx{Let_def}            Let(s, f) == f(s)

   357
   347 \tdx{Ball_def}           Ball(A,P) == ALL x. x:A --> P(x)
   358 \tdx{Ball_def}           Ball(A,P) == ALL x. x:A --> P(x)
   348 \tdx{Bex_def}            Bex(A,P)  == EX x. x:A & P(x)
   359 \tdx{Bex_def}            Bex(A,P)  == EX x. x:A & P(x)
   349
   360
   350 \tdx{subset_def}         A <= B  == ALL x:A. x:B
   361 \tdx{subset_def}         A <= B  == ALL x:A. x:B
   351 \tdx{extension}          A = B  <->  A <= B & B <= A
   362 \tdx{extension}          A = B  <->  A <= B & B <= A
   781 The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE}
   792 The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE}
   782 assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form
   793 assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form
   783 $\pair{x,y}$, for $x\in A$ and $y\in B(x)$.  The rule \tdx{SigmaE2}
   794 $\pair{x,y}$, for $x\in A$ and $y\in B(x)$.  The rule \tdx{SigmaE2}
   784 merely states that $\pair{a,b}\in {\tt Sigma}(A,B)$ implies $a\in A$ and
   795 merely states that $\pair{a,b}\in {\tt Sigma}(A,B)$ implies $a\in A$ and
   785 $b\in B(a)$.
   796 $b\in B(a)$.

   797

   798 In addition, it is possible to use tuples as patterns in abstractions:

   799 \begin{center}

   800 {\tt\%<$x$,$y$>.$t$} \quad stands for\quad {\tt split(\%$x$ $y$.$t$)}

   801 \end{center}

   802 Nested patterns are translated recursively:

   803 {\tt\%<$x$,$y$,$z$>.$t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>.$t$} $\leadsto$

   804 {\tt split(\%$x$.\%<$y$,$z$>.$t$)} $\leadsto$ {\tt split(\%$x$.split(\%$y$

   805   $z$.$t$))}. The reverse translation is performed upon printing.

   806 \begin{warn}

   807   The translation between patterns and {\tt split} is performed automatically

   808   by the parser and printer.  Thus the internal and external form of a term

   809   may differ, whichs affects proofs.  For example the term {\tt

   810     (\%<x,y>.<y,x>)<a,b>} requires the theorem {\tt split} to rewrite to

   811   {\tt<b,a>}.

   812 \end{warn}

   813 In addition to explicit $\lambda$-abstractions, patterns can be used in any

   814 variable binding construct which is internally described by a

   815 $\lambda$-abstraction. Some important examples are

   816 \begin{description}

   817 \item[Let:] {\tt let {\it pattern} = $t$ in $u$}

   818 \item[Choice:] {\tt THE~{\it pattern}~.~$P$}

   819 \item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$}

   820 \item[Comprehension:] {\tt \{~{\it pattern}:$A$~.~$P$~\}}

   821 \end{description}
   786
   822
   787
   823
   788 %%% domrange.ML
   824 %%% domrange.ML
   789
   825
   790 \begin{figure}
   826 \begin{figure}