doc-src/Logics/ZF.tex
changeset 1449 25a7ddf9c080
parent 713 b470cc6326aa
child 2495 82ec47e0a8d3
equal deleted 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}