author lcp Mon, 25 Apr 1994 11:05:58 +0200 changeset 343 8d77f767bd26 parent 342 82104a03565a child 344 753b50b07c46
final Springer copy
 doc-src/Logics/ZF.tex file | annotate | diff | comparison | revisions doc-src/Logics/intro.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Logics/ZF.tex	Sun Apr 24 11:30:00 1994 +0200
+++ b/doc-src/Logics/ZF.tex	Mon Apr 25 11:05:58 1994 +0200
@@ -32,7 +32,7 @@

Recent reports~\cite{paulson-set-I,paulson-set-II} describe {\tt ZF} less
formally than this chapter.  Isabelle employs a novel treatment of
-non-well-founded data structures within the standard ZF axioms including
+non-well-founded data structures within the standard {\sc zf} axioms including
the Axiom of Foundation~\cite{paulson-final}.

@@ -337,7 +337,7 @@
\hbox{\tt ALL $x$:$A$.$P[x]$} and \hbox{\tt EX $x$:$A$.$P[x]$}.

-%%%% zf.thy
+%%%% ZF.thy

\begin{figure}
\begin{ttbox}
@@ -414,7 +414,7 @@
definitions.  In particular, bounded quantifiers and the subset relation
appear in other axioms.  Object-level quantifiers and implications have
been replaced by meta-level ones wherever possible, to simplify use of the
-axioms.  See the file {\tt ZF/zf.thy} for details.
+axioms.  See the file {\tt ZF/ZF.thy} for details.

$y \in {\tt PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y))$
@@ -517,9 +517,9 @@
\subsection{Fundamental lemmas}
Figure~\ref{zf-lemmas1} presents the derived rules for the most basic
operators.  The rules for the bounded quantifiers resemble those for the
-ordinary quantifiers, but note that \tdx{ballE} uses a negated
-assumption in the style of Isabelle's classical reasoner.  The congruence rules
-\tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's
+ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption
+in the style of Isabelle's classical reasoner.  The \rmindex{congruence
+  rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's
simplifier, but have few other uses.  Congruence rules must be specially
derived for all binding operators, and henceforth will not be shown.

@@ -536,7 +536,7 @@
\tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to
particular circumstances.  Although too many rules can be confusing, there
is no reason to aim for a minimal set of rules.  See the file
-{\tt ZF/zf.ML} for a complete listing.
+{\tt ZF/ZF.ML} for a complete listing.

Figure~\ref{zf-lemmas3} presents rules for general union and intersection.
The empty intersection should be undefined.  We cannot have
@@ -772,7 +772,7 @@

The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$.  This
is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other
-encoding of ordered pairs.  The non-standard ordered pairs mentioned below
+encodings of ordered pairs.  The non-standard ordered pairs mentioned below
satisfy $\pair{\emptyset;\emptyset}=\emptyset$.

The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE}
@@ -825,13 +825,13 @@
of ordered pairs.  The converse of a relation~$r$ is the set of all pairs
$\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then
{\cdx{converse}$(r)$} is its inverse.  The rules for the domain
-operation, \tdx{domainI} and~\tdx{domainE}, assert that
-\cdx{domain}$(r)$ consists of every element~$a$ such that $r$ contains
+operation, namely \tdx{domainI} and~\tdx{domainE}, assert that
+\cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains
some pair of the form~$\pair{x,y}$.  The range operation is similar, and
the field of a relation is merely the union of its domain and range.

Figure~\ref{zf-domrange2} presents rules for images and inverse images.
-Note that these operations are generalizations of range and domain,
+Note that these operations are generalisations of range and domain,
respectively.  See the file {\tt ZF/domrange.ML} for derivations of the
rules.

@@ -1019,6 +1019,7 @@
\begin{figure}
\index{*"+ symbol}
\begin{constants}
+  \it symbol    & \it meta-type & \it priority & \it description \\
\tt +         & $[i,i]\To i$  &  Right 65     & disjoint union operator\\
\cdx{Inl}~~\cdx{Inr}  & $i\To i$      &       & injections\\
\cdx{case}    & $[i\To i,i\To i, i]\To i$ &   & conditional for $A+B$
@@ -1293,7 +1294,7 @@
set of all finite sets over~$A$.  The definition employs Isabelle's
inductive definition package~\cite{paulson-fixedpt}, which proves various
rules automatically.  The induction rule shown is stronger than the one
-proved by the package.  See file {\tt ZF/fin.ML}.
+proved by the package.  See file {\tt ZF/Fin.ML}.

\begin{figure}
\begin{ttbox}
@@ -1370,8 +1371,8 @@
Figure~\ref{zf-list} presents the set of lists over~$A$, ${\tt list}(A)$.
The definition employs Isabelle's datatype package, which defines the
introduction and induction rules automatically, as well as the constructors
-and case operator (\verb|list_case|).  See file {\tt ZF/list.ML}.
-The file {\tt ZF/listfn.thy} proceeds to define structural
+and case operator (\verb|list_case|).  See file {\tt ZF/List.ML}.
+The file {\tt ZF/ListFn.thy} proceeds to define structural
recursion and the usual list functions.

The constructions of the natural numbers and lists make use of a suite of
@@ -1393,10 +1394,10 @@
numbers.

\item Theory {\tt Epsilon} derives $\epsilon$-induction and
-    $\epsilon$-recursion, which are generalizations of transfinite
-    induction.  It also defines \cdx{rank}$(x)$, which is the least
-    ordinal $\alpha$ such that $x$ is constructed at stage $\alpha$ of the
-    cumulative hierarchy (thus $x\in V@{\alpha+1}$).
+    $\epsilon$-recursion, which are generalisations of transfinite
+    induction and recursion.  It also defines \cdx{rank}$(x)$, which is the
+    least ordinal $\alpha$ such that $x$ is constructed at stage $\alpha$
+    of the cumulative hierarchy (thus $x\in V@{\alpha+1}$).
\end{itemize}

@@ -1422,11 +1423,10 @@
a \in A \union B      & \bimp &  a\in A \disj a\in B\\
a \in A \inter B      & \bimp &  a\in A \conj a\in B\\
a \in A-B             & \bimp &  a\in A \conj \neg (a\in B)\\
-  a \in {\tt cons}(b,B) & \bimp &  a=b \disj a\in B\\
-  i \in {\tt succ}(j)   & \bimp &  i=j \disj i\in j\\
\pair{a,b}\in {\tt Sigma}(A,B)
& \bimp &  a\in A \conj b\in B(a)\\
a \in {\tt Collect}(A,P)      & \bimp &  a\in A \conj P(a)\\
+  (\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}
@@ -1443,57 +1443,57 @@
Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the
Composition of homomorphisms' challenge~\cite{boyer86}.

-\item[ZF/ex/ramsey.ML]
+\item[ZF/ex/Ramsey.ML]
proves the finite exponent 2 version of Ramsey's Theorem, following Basin
and Kaufmann's presentation~\cite{basin91}.

-\item[ZF/ex/equiv.ML]
-develops a ZF theory of equivalence classes, not using the Axiom of Choice.
+\item[ZF/ex/Equiv.ML]
+develops a theory of equivalence classes, not using the Axiom of Choice.

-\item[ZF/ex/integ.ML]
+\item[ZF/ex/Integ.ML]
develops a theory of the integers as equivalence classes of pairs of
natural numbers.

-\item[ZF/ex/bin.ML]
+\item[ZF/ex/Bin.ML]
defines a datatype for two's complement binary integers.  File
-{\tt binfn.ML} then develops rewrite rules for binary
+{\tt BinFn.ML} then develops rewrite rules for binary
arithmetic.  For instance, $1359\times {-}2468 = {-}3354012$ takes under
14 seconds.

-\item[ZF/ex/bt.ML]
+\item[ZF/ex/BT.ML]
defines the recursive data structure ${\tt bt}(A)$, labelled binary trees.

-\item[ZF/ex/term.ML]
-  and {\tt termfn.ML} define a recursive data structure for
+\item[ZF/ex/Term.ML]
+  and {\tt TermFn.ML} define a recursive data structure for
terms and term lists.  These are simply finite branching trees.

-\item[ZF/ex/tf.ML]
-  and {\tt tf_fn.ML} define primitives for solving mutually
+\item[ZF/ex/TF.ML]
+  and {\tt TF_Fn.ML} define primitives for solving mutually
recursive equations over sets.  It constructs sets of trees and forests
as an example, including induction and recursion rules that handle the
mutual recursion.

-\item[ZF/ex/prop.ML]
-  and {\tt proplog.ML} proves soundness and completeness of
-  propositional logic.  This illustrates datatype definitions, inductive
-  definitions, structural induction and rule induction.
+\item[ZF/ex/Prop.ML]
+  and {\tt PropLog.ML} proves soundness and completeness of
+  propositional logic~\cite{paulson-set-II}.  This illustrates datatype
+  definitions, inductive definitions, structural induction and rule induction.

-\item[ZF/ex/listn.ML]
+\item[ZF/ex/ListN.ML]
presents the inductive definition of the lists of $n$ elements~\cite{paulin92}.

-\item[ZF/ex/acc.ML]
+\item[ZF/ex/Acc.ML]
presents the inductive definition of the accessible part of a
relation~\cite{paulin92}.

-\item[ZF/ex/comb.ML]
+\item[ZF/ex/Comb.ML]
presents the datatype definition of combinators.  The file
-  {\tt contract0.ML} defines contraction, while file
-  {\tt parcontract.ML} defines parallel contraction and
+  {\tt Contract0.ML} defines contraction, while file
+  {\tt ParContract.ML} defines parallel contraction and
proves the Church-Rosser Theorem.  This case study follows Camilleri and
Melham~\cite{camilleri92}.

-\item[ZF/ex/llist.ML]
-  and {\tt llist_eq.ML} develop lazy lists in ZF and a notion
+\item[ZF/ex/LList.ML]
+  and {\tt LList_Eq.ML} develop lazy lists and a notion
of coinduction for proving equations between them.
\end{ttdescription}

@@ -1683,7 +1683,7 @@
\hbox{\tt prem RS subsetD} to \ttindex{ZF_cs} 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 behavior on
+general intersection can be difficult because of its anomalous behaviour on
the empty set.  However, \ttindex{fast_tac} copes well with these.  Here is
a typical example, borrowed from Devlin~\cite[page 12]{devlin79}:
\begin{ttbox}
@@ -1788,7 +1788,7 @@
{\out (f Un g)  a = f  a}
{\out No subgoals!}
\end{ttbox}
-See the files {\tt ZF/func.ML} and {\tt ZF/wf.ML} for more
+See the files {\tt ZF/func.ML} and {\tt ZF/WF.ML} for more

\index{set theory|)}
--- a/doc-src/Logics/intro.tex	Sun Apr 24 11:30:00 1994 +0200
+++ b/doc-src/Logics/intro.tex	Mon Apr 25 11:05:58 1994 +0200
@@ -21,8 +21,8 @@
system~\cite{paulson87}.  It is built upon classical~\FOL{}.

\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40},
-which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon88a}.  This
-object-logic should not be confused with Isabelle's meta-logic, which is
+which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}.
+This object-logic should not be confused with Isabelle's meta-logic, which is
also a form of higher-order logic.

\item[\thydx{HOLCF}] is an alternative version of {\sc lcf}, defined
@@ -99,7 +99,7 @@
actual syntax definitions in the {\tt.thy} files.

Each nonterminal symbol is associated with some Isabelle type.  For
-example, the {\bf formulae} of first-order logic have type~$o$.  Every
+example, the formulae of first-order logic have type~$o$.  Every
Isabelle expression of type~$o$ is therefore a formula.  These include
atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more
generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have
@@ -134,7 +134,7 @@

Many of the proof procedures use backtracking.  Typically they attempt to
solve subgoal~$i$ by repeatedly applying a certain tactic to it.  This
-tactic, which is known as a {\it step tactic}, resolves a selection of
+tactic, which is known as a {\bf step tactic}, resolves a selection of
rules with subgoal~$i$. This may replace one subgoal by many;  the
search persists until there are fewer subgoals in total than at the start.
Backtracking happens when the search reaches a dead end: when the step`