doc-src/ZF/ZF.tex
changeset 9695 ec7d7f877712
parent 9584 af21f4364c05
child 9836 56b632fd1dcd
     1.1 --- a/doc-src/ZF/ZF.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/ZF/ZF.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -23,10 +23,9 @@
     1.4  provides a streamlined syntax for defining primitive recursive functions over
     1.5  datatypes. 
     1.6  
     1.7 -Because {\ZF} is an extension of {\FOL}, it provides the same
     1.8 -packages, namely \texttt{hyp_subst_tac}, the simplifier, and the
     1.9 -classical reasoner.  The default simpset and claset are usually
    1.10 -satisfactory.
    1.11 +Because ZF is an extension of FOL, it provides the same packages, namely
    1.12 +\texttt{hyp_subst_tac}, the simplifier, and the classical reasoner.  The
    1.13 +default simpset and claset are usually satisfactory.
    1.14  
    1.15  Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF}
    1.16  less formally than this chapter.  Isabelle employs a novel treatment of
    1.17 @@ -94,7 +93,7 @@
    1.18  \begin{center}
    1.19  \index{*"`"` symbol}
    1.20  \index{*"-"`"` symbol}
    1.21 -\index{*"` symbol}\index{function applications!in \ZF}
    1.22 +\index{*"` symbol}\index{function applications!in ZF}
    1.23  \index{*"- symbol}
    1.24  \index{*": symbol}
    1.25  \index{*"<"= symbol}
    1.26 @@ -111,7 +110,7 @@
    1.27  \end{tabular}
    1.28  \end{center}
    1.29  \subcaption{Infixes}
    1.30 -\caption{Constants of {\ZF}} \label{zf-constants}
    1.31 +\caption{Constants of ZF} \label{zf-constants}
    1.32  \end{figure} 
    1.33  
    1.34  
    1.35 @@ -125,10 +124,10 @@
    1.36  bounded quantifiers.  In most other respects, Isabelle implements precisely
    1.37  Zermelo-Fraenkel set theory.
    1.38  
    1.39 -Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while
    1.40 +Figure~\ref{zf-constants} lists the constants and infixes of~ZF, while
    1.41  Figure~\ref{zf-trans} presents the syntax translations.  Finally,
    1.42 -Figure~\ref{zf-syntax} presents the full grammar for set theory, including
    1.43 -the constructs of \FOL.
    1.44 +Figure~\ref{zf-syntax} presents the full grammar for set theory, including the
    1.45 +constructs of FOL.
    1.46  
    1.47  Local abbreviations can be introduced by a \texttt{let} construct whose
    1.48  syntax appears in Fig.\ts\ref{zf-syntax}.  Internally it is translated into
    1.49 @@ -136,7 +135,7 @@
    1.50  definition, \tdx{Let_def}.
    1.51  
    1.52  Apart from \texttt{let}, set theory does not use polymorphism.  All terms in
    1.53 -{\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt
    1.54 +ZF have type~\tydx{i}, which is the type of individuals and has class~{\tt
    1.55    term}.  The type of first-order formulae, remember, is~\textit{o}.
    1.56  
    1.57  Infix operators include binary union and intersection ($A\un B$ and
    1.58 @@ -167,15 +166,15 @@
    1.59  abbreviates the nest of pairs\par\nobreak
    1.60  \centerline{\texttt{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}}
    1.61  
    1.62 -In {\ZF}, a function is a set of pairs.  A {\ZF} function~$f$ is simply an
    1.63 -individual as far as Isabelle is concerned: its Isabelle type is~$i$, not
    1.64 -say $i\To i$.  The infix operator~{\tt`} denotes the application of a
    1.65 -function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$.  The
    1.66 -syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
    1.67 +In ZF, a function is a set of pairs.  A ZF function~$f$ is simply an
    1.68 +individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
    1.69 +$i\To i$.  The infix operator~{\tt`} denotes the application of a function set
    1.70 +to its argument; we must write~$f{\tt`}x$, not~$f(x)$.  The syntax for image
    1.71 +is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
    1.72  
    1.73  
    1.74  \begin{figure} 
    1.75 -\index{lambda abs@$\lambda$-abstractions!in \ZF}
    1.76 +\index{lambda abs@$\lambda$-abstractions!in ZF}
    1.77  \index{*"-"> symbol}
    1.78  \index{*"* symbol}
    1.79  \begin{center} \footnotesize\tt\frenchspacing
    1.80 @@ -215,7 +214,7 @@
    1.81          \rm bounded $\exists$
    1.82  \end{tabular}
    1.83  \end{center}
    1.84 -\caption{Translations for {\ZF}} \label{zf-trans}
    1.85 +\caption{Translations for ZF} \label{zf-trans}
    1.86  \end{figure} 
    1.87  
    1.88  
    1.89 @@ -264,7 +263,7 @@
    1.90           & | & "EX!~" id~id^* " . " formula
    1.91    \end{array}
    1.92  \]
    1.93 -\caption{Full grammar for {\ZF}} \label{zf-syntax}
    1.94 +\caption{Full grammar for ZF} \label{zf-syntax}
    1.95  \end{figure} 
    1.96  
    1.97  
    1.98 @@ -321,14 +320,13 @@
    1.99  no constants~\texttt{op~*} and~\hbox{\tt op~->}.} Isabelle accepts these
   1.100  abbreviations in parsing and uses them whenever possible for printing.
   1.101  
   1.102 -\index{*THE symbol} 
   1.103 -As mentioned above, whenever the axioms assert the existence and uniqueness
   1.104 -of a set, Isabelle's set theory declares a constant for that set.  These
   1.105 -constants can express the {\bf definite description} operator~$\iota
   1.106 -x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists.
   1.107 -Since all terms in {\ZF} denote something, a description is always
   1.108 -meaningful, but we do not know its value unless $P[x]$ defines it uniquely.
   1.109 -Using the constant~\cdx{The}, we may write descriptions as {\tt
   1.110 +\index{*THE symbol} As mentioned above, whenever the axioms assert the
   1.111 +existence and uniqueness of a set, Isabelle's set theory declares a constant
   1.112 +for that set.  These constants can express the {\bf definite description}
   1.113 +operator~$\iota x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$,
   1.114 +if such exists.  Since all terms in ZF denote something, a description is
   1.115 +always meaningful, but we do not know its value unless $P[x]$ defines it
   1.116 +uniquely.  Using the constant~\cdx{The}, we may write descriptions as {\tt
   1.117    The($\lambda x. P[x]$)} or use the syntax \hbox{\tt THE $x$.\ $P[x]$}.
   1.118  
   1.119  \index{*lam symbol}
   1.120 @@ -385,7 +383,7 @@
   1.121  \tdx{Diff_def}     A - B    == {\ttlbrace}x:A . x~:B{\ttrbrace}
   1.122  \subcaption{Union, intersection, difference}
   1.123  \end{ttbox}
   1.124 -\caption{Rules and axioms of {\ZF}} \label{zf-rules}
   1.125 +\caption{Rules and axioms of ZF} \label{zf-rules}
   1.126  \end{figure}
   1.127  
   1.128  
   1.129 @@ -417,7 +415,7 @@
   1.130  \tdx{restrict_def}   restrict(f,A) == lam x:A. f`x
   1.131  \subcaption{Functions and general product}
   1.132  \end{ttbox}
   1.133 -\caption{Further definitions of {\ZF}} \label{zf-defs}
   1.134 +\caption{Further definitions of ZF} \label{zf-defs}
   1.135  \end{figure}
   1.136  
   1.137  
   1.138 @@ -515,7 +513,7 @@
   1.139  \tdx{PowD}            A : Pow(B)  ==>  A<=B
   1.140  \subcaption{The empty set; power sets}
   1.141  \end{ttbox}
   1.142 -\caption{Basic derived rules for {\ZF}} \label{zf-lemmas1}
   1.143 +\caption{Basic derived rules for ZF} \label{zf-lemmas1}
   1.144  \end{figure}
   1.145  
   1.146  
   1.147 @@ -555,7 +553,7 @@
   1.148  Figure~\ref{zf-lemmas3} presents rules for general union and intersection.
   1.149  The empty intersection should be undefined.  We cannot have
   1.150  $\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set.  All
   1.151 -expressions denote something in {\ZF} set theory; the definition of
   1.152 +expressions denote something in ZF set theory; the definition of
   1.153  intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is
   1.154  arbitrary.  The rule \tdx{InterI} must have a premise to exclude
   1.155  the empty intersection.  Some of the laws governing intersections require
   1.156 @@ -1051,7 +1049,7 @@
   1.157  See file \texttt{ZF/equalities.ML}.
   1.158  
   1.159  Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual
   1.160 -operators including a conditional (Fig.\ts\ref{zf-bool}).  Although {\ZF} is a
   1.161 +operators including a conditional (Fig.\ts\ref{zf-bool}).  Although ZF is a
   1.162  first-order theory, you can obtain the effect of higher-order logic using
   1.163  \texttt{bool}-valued functions, for example.  The constant~\texttt{1} is
   1.164  translated to \texttt{succ(0)}.
   1.165 @@ -1343,13 +1341,13 @@
   1.166  
   1.167  \section{Automatic Tools}
   1.168  
   1.169 -{\ZF} provides the simplifier and the classical reasoner.   Moreover it
   1.170 -supplies a specialized tool to infer `types' of terms.
   1.171 +ZF provides the simplifier and the classical reasoner.  Moreover it supplies a
   1.172 +specialized tool to infer `types' of terms.
   1.173  
   1.174  \subsection{Simplification}
   1.175  
   1.176 -{\ZF} inherits simplification from {\FOL} but adopts it for set theory.  The
   1.177 -extraction of rewrite rules takes the {\ZF} primitives into account.  It can
   1.178 +ZF inherits simplification from FOL but adopts it for set theory.  The
   1.179 +extraction of rewrite rules takes the ZF primitives into account.  It can
   1.180  strip bounded universal quantifiers from a formula; for example, ${\forall
   1.181    x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp
   1.182  f(x)=g(x)$.  Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in
   1.183 @@ -1360,10 +1358,9 @@
   1.184  works for most purposes.  A small simplification set for set theory is
   1.185  called~\ttindexbold{ZF_ss}, and you can even use \ttindex{FOL_ss} as a minimal
   1.186  starting point.  \texttt{ZF_ss} contains congruence rules for all the binding
   1.187 -operators of {\ZF}\@.  It contains all the conversion rules, such as
   1.188 -\texttt{fst} and \texttt{snd}, as well as the rewrites shown in
   1.189 -Fig.\ts\ref{zf-simpdata}.  See the file \texttt{ZF/simpdata.ML} for a fuller
   1.190 -list.
   1.191 +operators of ZF.  It contains all the conversion rules, such as \texttt{fst}
   1.192 +and \texttt{snd}, as well as the rewrites shown in Fig.\ts\ref{zf-simpdata}.
   1.193 +See the file \texttt{ZF/simpdata.ML} for a fuller list.
   1.194  
   1.195  
   1.196  \subsection{Classical Reasoning}
   1.197 @@ -1396,7 +1393,7 @@
   1.198  \subsection{Type-Checking Tactics}
   1.199  \index{type-checking tactics}
   1.200  
   1.201 -Isabelle/{\ZF} provides simple tactics to help automate those proofs that are
   1.202 +Isabelle/ZF provides simple tactics to help automate those proofs that are
   1.203  essentially type-checking.  Such proofs are built by applying rules such as
   1.204  these:
   1.205  \begin{ttbox}
   1.206 @@ -1614,13 +1611,13 @@
   1.207  \label{sec:ZF:datatype}
   1.208  \index{*datatype|(}
   1.209  
   1.210 -The \ttindex{datatype} definition package of \ZF\ constructs inductive
   1.211 -datatypes similar to those of \ML.  It can also construct coinductive
   1.212 -datatypes (codatatypes), which are non-well-founded structures such as
   1.213 -streams.  It defines the set using a fixed-point construction and proves
   1.214 -induction rules, as well as theorems for recursion and case combinators.  It
   1.215 -supplies mechanisms for reasoning about freeness.  The datatype package can
   1.216 -handle both mutual and indirect recursion.
   1.217 +The \ttindex{datatype} definition package of ZF constructs inductive datatypes
   1.218 +similar to those of \ML.  It can also construct coinductive datatypes
   1.219 +(codatatypes), which are non-well-founded structures such as streams.  It
   1.220 +defines the set using a fixed-point construction and proves induction rules,
   1.221 +as well as theorems for recursion and case combinators.  It supplies
   1.222 +mechanisms for reasoning about freeness.  The datatype package can handle both
   1.223 +mutual and indirect recursion.
   1.224  
   1.225  
   1.226  \subsection{Basics}
   1.227 @@ -2440,10 +2437,10 @@
   1.228  proves the two equivalent.  It contains several datatype and inductive
   1.229  definitions, and demonstrates their use.
   1.230  
   1.231 -The directory \texttt{ZF/ex} contains further developments in {\ZF} set
   1.232 -theory.  Here is an overview; see the files themselves for more details.  I
   1.233 -describe much of this material in other
   1.234 -publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}. 
   1.235 +The directory \texttt{ZF/ex} contains further developments in ZF set theory.
   1.236 +Here is an overview; see the files themselves for more details.  I describe
   1.237 +much of this material in other
   1.238 +publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}.
   1.239  \begin{itemize}
   1.240  \item File \texttt{misc.ML} contains miscellaneous examples such as
   1.241    Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition