doc-src/ZF/ZF.tex
changeset 9695 ec7d7f877712
parent 9584 af21f4364c05
child 9836 56b632fd1dcd
--- a/doc-src/ZF/ZF.tex	Mon Aug 28 13:50:24 2000 +0200
+++ b/doc-src/ZF/ZF.tex	Mon Aug 28 13:52:38 2000 +0200
@@ -23,10 +23,9 @@
 provides a streamlined syntax for defining primitive recursive functions over
 datatypes. 
 
-Because {\ZF} is an extension of {\FOL}, it provides the same
-packages, namely \texttt{hyp_subst_tac}, the simplifier, and the
-classical reasoner.  The default simpset and claset are usually
-satisfactory.
+Because ZF is an extension of FOL, it provides the same packages, namely
+\texttt{hyp_subst_tac}, the simplifier, and the classical reasoner.  The
+default simpset and claset are usually satisfactory.
 
 Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF}
 less formally than this chapter.  Isabelle employs a novel treatment of
@@ -94,7 +93,7 @@
 \begin{center}
 \index{*"`"` symbol}
 \index{*"-"`"` symbol}
-\index{*"` symbol}\index{function applications!in \ZF}
+\index{*"` symbol}\index{function applications!in ZF}
 \index{*"- symbol}
 \index{*": symbol}
 \index{*"<"= symbol}
@@ -111,7 +110,7 @@
 \end{tabular}
 \end{center}
 \subcaption{Infixes}
-\caption{Constants of {\ZF}} \label{zf-constants}
+\caption{Constants of ZF} \label{zf-constants}
 \end{figure} 
 
 
@@ -125,10 +124,10 @@
 bounded quantifiers.  In most other respects, Isabelle implements precisely
 Zermelo-Fraenkel set theory.
 
-Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while
+Figure~\ref{zf-constants} lists the constants and infixes of~ZF, while
 Figure~\ref{zf-trans} presents the syntax translations.  Finally,
-Figure~\ref{zf-syntax} presents the full grammar for set theory, including
-the constructs of \FOL.
+Figure~\ref{zf-syntax} presents the full grammar for set theory, including the
+constructs of FOL.
 
 Local abbreviations can be introduced by a \texttt{let} construct whose
 syntax appears in Fig.\ts\ref{zf-syntax}.  Internally it is translated into
@@ -136,7 +135,7 @@
 definition, \tdx{Let_def}.
 
 Apart from \texttt{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
+ZF have type~\tydx{i}, which is the type of individuals and has class~{\tt
   term}.  The type of first-order formulae, remember, is~\textit{o}.
 
 Infix operators include binary union and intersection ($A\un B$ and
@@ -167,15 +166,15 @@
 abbreviates the nest of pairs\par\nobreak
 \centerline{\texttt{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}}
 
-In {\ZF}, a function is a set of pairs.  A {\ZF} function~$f$ is simply an
-individual as far as Isabelle is concerned: its Isabelle type is~$i$, not
-say $i\To i$.  The infix operator~{\tt`} denotes the application of a
-function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$.  The
-syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
+In ZF, a function is a set of pairs.  A ZF function~$f$ is simply an
+individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
+$i\To i$.  The infix operator~{\tt`} denotes the application of a function set
+to its argument; we must write~$f{\tt`}x$, not~$f(x)$.  The syntax for image
+is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
 
 
 \begin{figure} 
-\index{lambda abs@$\lambda$-abstractions!in \ZF}
+\index{lambda abs@$\lambda$-abstractions!in ZF}
 \index{*"-"> symbol}
 \index{*"* symbol}
 \begin{center} \footnotesize\tt\frenchspacing
@@ -215,7 +214,7 @@
         \rm bounded $\exists$
 \end{tabular}
 \end{center}
-\caption{Translations for {\ZF}} \label{zf-trans}
+\caption{Translations for ZF} \label{zf-trans}
 \end{figure} 
 
 
@@ -264,7 +263,7 @@
          & | & "EX!~" id~id^* " . " formula
   \end{array}
 \]
-\caption{Full grammar for {\ZF}} \label{zf-syntax}
+\caption{Full grammar for ZF} \label{zf-syntax}
 \end{figure} 
 
 
@@ -321,14 +320,13 @@
 no constants~\texttt{op~*} and~\hbox{\tt op~->}.} Isabelle accepts these
 abbreviations in parsing and uses them whenever possible for printing.
 
-\index{*THE symbol} 
-As mentioned above, whenever the axioms assert the existence and uniqueness
-of a set, Isabelle's set theory declares a constant for that set.  These
-constants can express the {\bf definite description} operator~$\iota
-x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists.
-Since all terms in {\ZF} denote something, a description is always
-meaningful, but we do not know its value unless $P[x]$ defines it uniquely.
-Using the constant~\cdx{The}, we may write descriptions as {\tt
+\index{*THE symbol} As mentioned above, whenever the axioms assert the
+existence and uniqueness of a set, Isabelle's set theory declares a constant
+for that set.  These constants can express the {\bf definite description}
+operator~$\iota x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$,
+if such exists.  Since all terms in ZF denote something, a description is
+always meaningful, but we do not know its value unless $P[x]$ defines it
+uniquely.  Using the constant~\cdx{The}, we may write descriptions as {\tt
   The($\lambda x. P[x]$)} or use the syntax \hbox{\tt THE $x$.\ $P[x]$}.
 
 \index{*lam symbol}
@@ -385,7 +383,7 @@
 \tdx{Diff_def}     A - B    == {\ttlbrace}x:A . x~:B{\ttrbrace}
 \subcaption{Union, intersection, difference}
 \end{ttbox}
-\caption{Rules and axioms of {\ZF}} \label{zf-rules}
+\caption{Rules and axioms of ZF} \label{zf-rules}
 \end{figure}
 
 
@@ -417,7 +415,7 @@
 \tdx{restrict_def}   restrict(f,A) == lam x:A. f`x
 \subcaption{Functions and general product}
 \end{ttbox}
-\caption{Further definitions of {\ZF}} \label{zf-defs}
+\caption{Further definitions of ZF} \label{zf-defs}
 \end{figure}
 
 
@@ -515,7 +513,7 @@
 \tdx{PowD}            A : Pow(B)  ==>  A<=B
 \subcaption{The empty set; power sets}
 \end{ttbox}
-\caption{Basic derived rules for {\ZF}} \label{zf-lemmas1}
+\caption{Basic derived rules for ZF} \label{zf-lemmas1}
 \end{figure}
 
 
@@ -555,7 +553,7 @@
 Figure~\ref{zf-lemmas3} presents rules for general union and intersection.
 The empty intersection should be undefined.  We cannot have
 $\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set.  All
-expressions denote something in {\ZF} set theory; the definition of
+expressions denote something in ZF set theory; the definition of
 intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is
 arbitrary.  The rule \tdx{InterI} must have a premise to exclude
 the empty intersection.  Some of the laws governing intersections require
@@ -1051,7 +1049,7 @@
 See file \texttt{ZF/equalities.ML}.
 
 Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual
-operators including a conditional (Fig.\ts\ref{zf-bool}).  Although {\ZF} is a
+operators including a conditional (Fig.\ts\ref{zf-bool}).  Although ZF is a
 first-order theory, you can obtain the effect of higher-order logic using
 \texttt{bool}-valued functions, for example.  The constant~\texttt{1} is
 translated to \texttt{succ(0)}.
@@ -1343,13 +1341,13 @@
 
 \section{Automatic Tools}
 
-{\ZF} provides the simplifier and the classical reasoner.   Moreover it
-supplies a specialized tool to infer `types' of terms.
+ZF provides the simplifier and the classical reasoner.  Moreover it supplies a
+specialized tool to infer `types' of terms.
 
 \subsection{Simplification}
 
-{\ZF} inherits simplification from {\FOL} but adopts it for set theory.  The
-extraction of rewrite rules takes the {\ZF} primitives into account.  It can
+ZF inherits simplification from FOL but adopts it for set theory.  The
+extraction of rewrite rules takes the ZF primitives into account.  It can
 strip bounded universal quantifiers from a formula; for example, ${\forall
   x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp
 f(x)=g(x)$.  Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in
@@ -1360,10 +1358,9 @@
 works for most purposes.  A small simplification set for set theory is
 called~\ttindexbold{ZF_ss}, and you can even use \ttindex{FOL_ss} as a minimal
 starting point.  \texttt{ZF_ss} contains congruence rules for all the binding
-operators of {\ZF}\@.  It contains all the conversion rules, such as
-\texttt{fst} and \texttt{snd}, as well as the rewrites shown in
-Fig.\ts\ref{zf-simpdata}.  See the file \texttt{ZF/simpdata.ML} for a fuller
-list.
+operators of ZF.  It contains all the conversion rules, such as \texttt{fst}
+and \texttt{snd}, as well as the rewrites shown in Fig.\ts\ref{zf-simpdata}.
+See the file \texttt{ZF/simpdata.ML} for a fuller list.
 
 
 \subsection{Classical Reasoning}
@@ -1396,7 +1393,7 @@
 \subsection{Type-Checking Tactics}
 \index{type-checking tactics}
 
-Isabelle/{\ZF} provides simple tactics to help automate those proofs that are
+Isabelle/ZF provides simple tactics to help automate those proofs that are
 essentially type-checking.  Such proofs are built by applying rules such as
 these:
 \begin{ttbox}
@@ -1614,13 +1611,13 @@
 \label{sec:ZF:datatype}
 \index{*datatype|(}
 
-The \ttindex{datatype} definition package of \ZF\ constructs inductive
-datatypes similar to those of \ML.  It can also construct coinductive
-datatypes (codatatypes), which are non-well-founded structures such as
-streams.  It defines the set using a fixed-point construction and proves
-induction rules, as well as theorems for recursion and case combinators.  It
-supplies mechanisms for reasoning about freeness.  The datatype package can
-handle both mutual and indirect recursion.
+The \ttindex{datatype} definition package of ZF constructs inductive datatypes
+similar to those of \ML.  It can also construct coinductive datatypes
+(codatatypes), which are non-well-founded structures such as streams.  It
+defines the set using a fixed-point construction and proves induction rules,
+as well as theorems for recursion and case combinators.  It supplies
+mechanisms for reasoning about freeness.  The datatype package can handle both
+mutual and indirect recursion.
 
 
 \subsection{Basics}
@@ -2440,10 +2437,10 @@
 proves the two equivalent.  It contains several datatype and inductive
 definitions, and demonstrates their use.
 
-The directory \texttt{ZF/ex} contains further developments in {\ZF} set
-theory.  Here is an overview; see the files themselves for more details.  I
-describe much of this material in other
-publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}. 
+The directory \texttt{ZF/ex} contains further developments in ZF set theory.
+Here is an overview; see the files themselves for more details.  I describe
+much of this material in other
+publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}.
 \begin{itemize}
 \item File \texttt{misc.ML} contains miscellaneous examples such as
   Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition