--- a/doc-src/Logics/ZF.tex Fri Sep 09 11:45:44 1994 +0200
+++ b/doc-src/Logics/ZF.tex Fri Sep 09 11:52:38 1994 +0200
@@ -9,14 +9,15 @@
of it is based on the work of No\"el~\cite{noel}.
A tremendous amount of set theory has been formally developed, including
-the basic properties of relations, functions and ordinals. Significant
-results have been proved, such as the Schr\"oder-Bernstein Theorem and a
-version of Ramsey's Theorem. General methods have been developed for
-solving recursion equations over monotonic functors; these have been
-applied to yield constructions of lists, trees, infinite lists, etc. The
-Recursion Theorem has been proved, admitting recursive definitions of
-functions over well-founded relations. Thus, we may even regard set theory
-as a computational logic, loosely inspired by Martin-L\"of's Type Theory.
+the basic properties of relations, functions, ordinals and cardinals.
+Significant results have been proved, such as the Schr\"oder-Bernstein
+Theorem, the Wellordering Theorem and a version of Ramsey's Theorem.
+General methods have been developed for solving recursion equations over
+monotonic functors; these have been applied to yield constructions of
+lists, trees, infinite lists, etc. The Recursion Theorem has been proved,
+admitting recursive definitions of functions over well-founded relations.
+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.
@@ -24,11 +25,13 @@
classical rule sets are defined, including {\tt lemmas_cs},
{\tt upair_cs} and~{\tt ZF_cs}.
-{\tt ZF} now has a flexible package for handling inductive definitions,
+{\tt ZF} has a flexible package for handling inductive definitions,
such as inference systems, and datatype definitions, such as lists and
-trees. Moreover it also handles coinductive definitions, such as
+trees. Moreover it handles coinductive definitions, such as
bisimulation relations, and codatatype definitions, such as streams. A
-recent paper describes the package~\cite{paulson-fixedpt}.
+recent paper describes the package~\cite{paulson-CADE}, but its examples
+use an obsolete declaration syntax. Please consult the version of the
+paper distributed with Isabelle.
Recent reports~\cite{paulson-set-I,paulson-set-II} describe {\tt ZF} less
formally than this chapter. Isabelle employs a novel treatment of
@@ -1132,7 +1135,7 @@
fixedpoint operators with corresponding induction and coinduction rules.
These are essential to many definitions that follow, including the natural
numbers and the transitive closure operator. The (co)inductive definition
-package also uses the fixedpoint operators~\cite{paulson-fixedpt}. See
+package also uses the fixedpoint operators~\cite{paulson-CADE}. See
Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski
Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle
proofs.
@@ -1290,16 +1293,17 @@
univ}(A)$ (and is defined in terms of it) but is closed under the
non-standard product and sum.
-Figure~\ref{zf-fin} presents the finite set operator; ${\tt Fin}(A)$ is the
-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}.
+Theory {\tt Finite} (Figure~\ref{zf-fin}) defines the finite set operator;
+${\tt Fin}(A)$ is the set of all finite sets over~$A$. The theory employs
+Isabelle's inductive definition package, which proves various rules
+automatically. The induction rule shown is stronger than the one proved by
+the package. The theory also defines the set of all finite functions
+between two given sets.
\begin{figure}
\begin{ttbox}
-\tdx{Fin_0I} 0 : Fin(A)
-\tdx{Fin_consI} [| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)
+\tdx{Fin.emptyI} 0 : Fin(A)
+\tdx{Fin.consI} [| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)
\tdx{Fin_induct}
[| b: Fin(A);
@@ -1400,6 +1404,58 @@
of the cumulative hierarchy (thus $x\in V@{\alpha+1}$).
\end{itemize}
+Other important theories lead to a theory of cardinal numbers. They have
+not yet been written up anywhere. Here is a summary:
+\begin{itemize}
+\item Theory {\tt Rel} defines the basic properties of relations, such as
+ (ir)reflexivity, (a)symmetry, and transitivity.
+
+\item Theory {\tt EquivClass} develops a theory of equivalence
+ classes, not using the Axiom of Choice.
+
+\item Theory {\tt Order} defines partial orderings, total orderings and
+ wellorderings.
+
+\item Theory {\tt OrderArith} defines orderings on sum and product sets.
+ These can be used to define ordinal arithmetic and have applications to
+ cardinal arithmetic.
+
+\item Theory {\tt OrderType} defines order types. Every wellordering is
+ equivalent to a unique ordinal, which is its order type.
+
+\item Theory {\tt Cardinal} defines equipollence and cardinal numbers.
+
+\item Theory {\tt CardinalArith} defines cardinal addition and
+ multiplication, and proves their elementary laws. It proves that there
+ is no greatest cardinal. It also proves a deep result, namely
+ $\kappa\otimes\kappa=\kappa$ for every infinite cardinal~$\kappa$; see
+ Kunen~\cite[page 29]{kunen80}. None of these results assume the Axiom of
+ Choice, which complicates their proofs considerably.
+\end{itemize}
+
+The following developments involve the Axiom of Choice (AC):
+\begin{itemize}
+\item Theory {\tt AC} asserts the Axiom of Choice and proves some simple
+ equivalent forms.
+
+\item Theory {\tt Zorn} proves Hausdorff's Maximal Principle, Zorn's Lemma
+ and the Wellordering Theorem, following Abrial and
+ Laffitte~\cite{abrial93}.
+
+\item Theory \verb|Cardinal_AC| uses AC to prove simplified theorems about
+ the cardinals. It also proves a theorem needed to justify
+ infinitely branching datatype declarations: if $\kappa$ is an infinite
+ cardinal and $|X(\alpha)| \le \kappa$ for all $\alpha<\kappa$ then
+ $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.
+
+\item Theory {\tt InfDatatype} proves theorems to justify infinitely
+ branching datatypes. Arbitrary index sets are allowed, provided their
+ cardinalities have an upper bound. The theory also justifies some
+ unusual cases of finite branching, involving the finite powerset operator
+ and the finite function space operator.
+\end{itemize}
+
+
\section{Simplification rules}
{\ZF} does not merely inherit simplification from \FOL, but modifies it
@@ -1433,69 +1489,63 @@
\end{figure}
-\section{The examples directory}
+\section{The examples directories}
+Directory {\tt HOL/IMP} contains a mechanised version of a semantic
+equivalence proof taken from Winskel~\cite{winskel93}. It formalises the
+denotational and operational semantics of a simple while-language, then
+proves the two equivalent. It contains several datatype and inductive
+definitions, and demonstrates their use.
+
The directory {\tt 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-fixedpt,paulson-set-I,paulson-set-II}.
-\begin{ttdescription}
-\item[ZF/ex/misc.ML] contains miscellaneous examples such as
- Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the
- `Composition of homomorphisms' challenge~\cite{boyer86}.
+publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}.
+\begin{itemize}
+\item File {\tt misc.ML} contains miscellaneous examples such as
+ Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition
+ of homomorphisms' challenge~\cite{boyer86}.
-\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 theory of equivalence classes, not using the Axiom of Choice.
+\item Theory {\tt Ramsey} proves the finite exponent 2 version of
+ Ramsey's Theorem, following Basin and Kaufmann's
+ presentation~\cite{basin91}.
-\item[ZF/ex/Integ.ML]
-develops a theory of the integers as equivalence classes of pairs of
-natural numbers.
+\item Theory {\tt Integ} develops a theory of the integers as
+ equivalence classes of pairs of natural numbers.
-\item[ZF/ex/Bin.ML]
-defines a datatype for two's complement binary integers. File
-{\tt BinFn.ML} then develops rewrite rules for binary
-arithmetic. For instance, $1359\times {-}2468 = {-}3354012$ takes under
-14 seconds.
+\item Theory {\tt Bin} defines a datatype for two's complement binary
+ integers, then proves rewrite rules to perform binary arithmetic. For
+ instance, $1359\times {-}2468 = {-}3354012$ takes under 14 seconds.
-\item[ZF/ex/BT.ML]
-defines the recursive data structure ${\tt bt}(A)$, labelled binary trees.
+\item Theory {\tt BT} 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
- terms and term lists. These are simply finite branching trees.
+\item Theory {\tt Term} defines 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 Theory {\tt TF} defines 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
+\item Theory {\tt Prop} proves soundness and completeness of
propositional logic~\cite{paulson-set-II}. This illustrates datatype
- definitions, inductive definitions, structural induction and rule induction.
+ definitions, inductive definitions, structural induction and rule
+ induction.
-\item[ZF/ex/ListN.ML]
-presents the inductive definition of the lists of $n$ elements~\cite{paulin92}.
-
-\item[ZF/ex/Acc.ML]
-presents the inductive definition of the accessible part of a
-relation~\cite{paulin92}.
+\item Theory {\tt ListN} inductively defines the lists of $n$
+ elements~\cite{paulin92}.
-\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
- proves the Church-Rosser Theorem. This case study follows Camilleri and
- Melham~\cite{camilleri92}.
+\item Theory {\tt Acc} inductively defines the accessible part of a
+ relation~\cite{paulin92}.
-\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}
+\item Theory {\tt Comb} defines the datatype of combinators and
+ inductively defines contraction and parallel contraction. It goes on to
+ prove the Church-Rosser Theorem. This case study follows Camilleri and
+ Melham~\cite{camilleri92}.
+
+\item Theory {\tt LList} defines lazy lists and a coinduction
+ principle for proving equations between them.
+\end{itemize}
\section{A proof about powersets}\label{sec:ZF-pow-example}