doc-src/Logics/ZF.tex

--- a/doc-src/Logics/ZF.tex	Wed Jan 08 15:12:44 1997 +0100
+++ b/doc-src/Logics/ZF.tex	Wed Jan 08 15:17:25 1997 +0100
@@ -19,11 +19,13 @@
 Thus, we may even regard set theory as a computational logic, loosely
 inspired by Martin-L\"of's Type Theory.
 
-Because {\ZF} is an extension of {\FOL}, it provides the same packages,
-namely {\tt hyp_subst_tac}, the simplifier, and the classical reasoner.
-The main simplification set is called {\tt ZF_ss}.  Several
-classical rule sets are defined, including {\tt lemmas_cs},
-{\tt upair_cs} and~{\tt ZF_cs}.  
+Because {\ZF} is an extension of {\FOL}, it provides the same packages, namely
+{\tt hyp_subst_tac}, the simplifier, and the classical reasoner.  The default
+simpset and claset are usually satisfactory.  Named simpsets include
+\ttindexbold{ZF_ss} (basic set theory rules) and \ttindexbold{rank_ss} (for
+proving termination of well-founded recursion).  Named clasets sets include
+\ttindexbold{ZF_cs} (basic set theory) and \ttindexbold{le_cs} (useful for
+reasoning about the relations $<$ and $\le$).
 
 {\tt ZF} has a flexible package for handling inductive definitions,
 such as inference systems, and datatype definitions, such as lists and
@@ -1503,11 +1505,11 @@
 f(x)=g(x)$.  Given $a\in\{x\in A.P(x)\}$ it extracts rewrite rules from
 $a\in A$ and~$P(a)$.  It can also break down $a\in A\int B$ and $a\in A-B$.
 
-The simplification set \ttindexbold{ZF_ss} contains congruence rules for
+The default simplification set contains congruence rules for
 all the binding operators of {\ZF}\@.  It contains all the conversion
 rules, such as {\tt fst} and {\tt snd}, as well as the rewrites
-shown in Fig.\ts\ref{zf-simpdata}.
-
+shown in Fig.\ts\ref{zf-simpdata}.  See the file 
+{\tt ZF/simpdata.ML} for a fuller list.
 
 \begin{figure}
 \begin{eqnarray*}
@@ -1521,7 +1523,7 @@
   (\forall x \in \emptyset. P(x)) & \bimp &  \top\\
   (\forall x \in A. \top)       & \bimp &  \top
 \end{eqnarray*}
-\caption{Rewrite rules for set theory} \label{zf-simpdata}
+\caption{Some rewrite rules for set theory} \label{zf-simpdata}
 \end{figure}
 
 
@@ -1598,7 +1600,7 @@
 We enter the goal and make the first step, which breaks the equation into
 two inclusions by extensionality:\index{*equalityI theorem}
 \begin{ttbox}
-goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
+goal thy "Pow(A Int B) = Pow(A) Int Pow(B)";
 {\out Level 0}
 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
 {\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}
@@ -1687,7 +1689,7 @@
 \end{ttbox}
 \medskip
 We could have performed this proof in one step by applying
-\ttindex{fast_tac} with the classical rule set \ttindex{ZF_cs}.  Let us
+\ttindex{Fast_tac}.  Let us
 go back to the start:
 \begin{ttbox}
 choplev 0;
@@ -1695,11 +1697,11 @@
 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
 {\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}
 \end{ttbox}
-We must add \tdx{equalityI} to {\tt ZF_cs} as an introduction rule.
-Extensionality is not used by default because many equalities can be proved
+We must add \tdx{equalityI} as an introduction rule.
+Extensionality is not used by default: many equalities can be proved
 by rewriting.
 \begin{ttbox}
-by (fast_tac (ZF_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 {\out Level 1}
 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
 {\out No subgoals!}
@@ -1713,7 +1715,7 @@
 ${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$.  To begin, we
 tackle the inclusion using \tdx{subsetI}:
 \begin{ttbox}
-val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
+val [prem] = goal thy "C<=D ==> Union(C) <= Union(D)";
 {\out Level 0}
 {\out Union(C) <= Union(D)}
 {\out  1. Union(C) <= Union(D)}
@@ -1763,10 +1765,10 @@
 {\out Union(C) <= Union(D)}
 {\out No subgoals!}
 \end{ttbox}
-Again, \ttindex{fast_tac} with \ttindex{ZF_cs} can do this proof in one
+Again, \ttindex{fast_tac} can prove the theorem in one
 step, provided we somehow supply it with~{\tt prem}.  We can either add
 this premise to the assumptions using \ttindex{cut_facts_tac}, or add
-\hbox{\tt prem RS subsetD} to \ttindex{ZF_cs} as an introduction rule.
+\hbox{\tt prem RS subsetD} to the claset as an introduction rule.
 
 The file {\tt ZF/equalities.ML} has many similar proofs.  Reasoning about
 general intersection can be difficult because of its anomalous behaviour on
@@ -1790,7 +1792,7 @@
 functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then
 $(f\un g)`a = f`a$:
 \begin{ttbox}
-val prems = goal ZF.thy
+val prems = goal thy
     "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \ttback
 \ttback    (f Un g)`a = f`a";
 {\out Level 0}