doc-src/Logics/ZF.tex

Documented the new distinct_subgoals_tac

%% $Id$
\chapter{Zermelo-Fraenkel Set Theory}
\index{set theory|(}

The theory~\thydx{ZF} implements Zermelo-Fraenkel set
theory~\cite{halmos60,suppes72} as an extension of~{\tt FOL}, classical
first-order logic.  The theory includes a collection of derived natural
deduction rules, for use with Isabelle's classical reasoner.  Much
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, 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.  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 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
trees.  Moreover it handles coinductive definitions, such as
bisimulation relations, and codatatype definitions, such as streams.
There is a paper \cite{paulson-CADE} describing the package, 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
non-well-founded data structures within the standard {\sc zf} axioms including
the Axiom of Foundation~\cite{paulson-final}.


\section{Which version of axiomatic set theory?}
The two main axiom systems for set theory are Bernays-G\"odel~({\sc bg})
and Zermelo-Fraenkel~({\sc zf}).  Resolution theorem provers can use {\sc
  bg} because it is finite~\cite{boyer86,quaife92}.  {\sc zf} does not
have a finite axiom system because of its Axiom Scheme of Replacement.
This makes it awkward to use with many theorem provers, since instances
of the axiom scheme have to be invoked explicitly.  Since Isabelle has no
difficulty with axiom schemes, we may adopt either axiom system.

These two theories differ in their treatment of {\bf classes}, which are
collections that are `too big' to be sets.  The class of all sets,~$V$,
cannot be a set without admitting Russell's Paradox.  In {\sc bg}, both
classes and sets are individuals; $x\in V$ expresses that $x$ is a set.  In
{\sc zf}, all variables denote sets; classes are identified with unary
predicates.  The two systems define essentially the same sets and classes,
with similar properties.  In particular, a class cannot belong to another
class (let alone a set).

Modern set theorists tend to prefer {\sc zf} because they are mainly concerned
with sets, rather than classes.  {\sc bg} requires tiresome proofs that various
collections are sets; for instance, showing $x\in\{x\}$ requires showing that
$x$ is a set.


\begin{figure} \small
\begin{center}
\begin{tabular}{rrr} 
  \it name      &\it meta-type  & \it description \\ 
  \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\
  \cdx{0}       & $i$           & empty set\\
  \cdx{cons}    & $[i,i]\To i$  & finite set constructor\\
  \cdx{Upair}   & $[i,i]\To i$  & unordered pairing\\
  \cdx{Pair}    & $[i,i]\To i$  & ordered pairing\\
  \cdx{Inf}     & $i$   & infinite set\\
  \cdx{Pow}     & $i\To i$      & powerset\\
  \cdx{Union} \cdx{Inter} & $i\To i$    & set union/intersection \\
  \cdx{split}   & $[[i,i]\To i, i] \To i$ & generalized projection\\
  \cdx{fst} \cdx{snd}   & $i\To i$      & projections\\
  \cdx{converse}& $i\To i$      & converse of a relation\\
  \cdx{succ}    & $i\To i$      & successor\\
  \cdx{Collect} & $[i,i\To o]\To i$     & separation\\
  \cdx{Replace} & $[i, [i,i]\To o] \To i$       & replacement\\
  \cdx{PrimReplace} & $[i, [i,i]\To o] \To i$   & primitive replacement\\
  \cdx{RepFun}  & $[i, i\To i] \To i$   & functional replacement\\
  \cdx{Pi} \cdx{Sigma}  & $[i,i\To i]\To i$     & general product/sum\\
  \cdx{domain}  & $i\To i$      & domain of a relation\\
  \cdx{range}   & $i\To i$      & range of a relation\\
  \cdx{field}   & $i\To i$      & field of a relation\\
  \cdx{Lambda}  & $[i, i\To i]\To i$    & $\lambda$-abstraction\\
  \cdx{restrict}& $[i, i] \To i$        & restriction of a function\\
  \cdx{The}     & $[i\To o]\To i$       & definite description\\
  \cdx{if}      & $[o,i,i]\To i$        & conditional\\
  \cdx{Ball} \cdx{Bex}  & $[i, i\To o]\To o$    & bounded quantifiers
\end{tabular}
\end{center}
\subcaption{Constants}

\begin{center}
\index{*"`"` symbol}
\index{*"-"`"` symbol}
\index{*"` symbol}\index{function applications!in \ZF}
\index{*"- symbol}
\index{*": symbol}
\index{*"<"= symbol}
\begin{tabular}{rrrr} 
  \it symbol  & \it meta-type & \it priority & \it description \\ 
  \tt ``        & $[i,i]\To i$  &  Left 90      & image \\
  \tt -``       & $[i,i]\To i$  &  Left 90      & inverse image \\
  \tt `         & $[i,i]\To i$  &  Left 90      & application \\
  \sdx{Int}     & $[i,i]\To i$  &  Left 70      & intersection ($\int$) \\
  \sdx{Un}      & $[i,i]\To i$  &  Left 65      & union ($\un$) \\
  \tt -         & $[i,i]\To i$  &  Left 65      & set difference ($-$) \\[1ex]
  \tt:          & $[i,i]\To o$  &  Left 50      & membership ($\in$) \\
  \tt <=        & $[i,i]\To o$  &  Left 50      & subset ($\subseteq$) 
\end{tabular}
\end{center}
\subcaption{Infixes}
\caption{Constants of {\ZF}} \label{zf-constants}
\end{figure} 


\section{The syntax of set theory}
The language of set theory, as studied by logicians, has no constants.  The
traditional axioms merely assert the existence of empty sets, unions,
powersets, etc.; this would be intolerable for practical reasoning.  The
Isabelle theory declares constants for primitive sets.  It also extends
{\tt FOL} with additional syntax for finite sets, ordered pairs,
comprehension, general union/intersection, general sums/products, and
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-trans} presents the syntax translations.  Finally,
Figure~\ref{zf-syntax} presents the full grammar for set theory, including
the constructs of \FOL.

Local abbreviations can be introduced by a {\tt let} construct whose
syntax appears in Fig.\ts\ref{zf-syntax}.  Internally it is translated into
the constant~\cdx{Let}.  It can be expanded by rewriting with its
definition, \tdx{Let_def}.

Apart from {\tt 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
  term}.  The type of first-order formulae, remember, is~{\tt o}.

Infix operators include binary union and intersection ($A\un B$ and
$A\int B$), set difference ($A-B$), and the subset and membership
relations.  Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$.  The
union and intersection operators ($\bigcup A$ and $\bigcap A$) form the
union or intersection of a set of sets; $\bigcup A$ means the same as
$\bigcup@{x\in A}x$.  Of these operators, only $\bigcup A$ is primitive.

The constant \cdx{Upair} constructs unordered pairs; thus {\tt
  Upair($A$,$B$)} denotes the set~$\{A,B\}$ and {\tt Upair($A$,$A$)}
denotes the singleton~$\{A\}$.  General union is used to define binary
union.  The Isabelle version goes on to define the constant
\cdx{cons}:
\begin{eqnarray*}
   A\cup B              & \equiv &       \bigcup({\tt Upair}(A,B)) \\
   {\tt cons}(a,B)      & \equiv &        {\tt Upair}(a,a) \un B
\end{eqnarray*}
The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the
obvious manner using~{\tt cons} and~$\emptyset$ (the empty set):
\begin{eqnarray*}
 \{a,b,c\} & \equiv & {\tt cons}(a,{\tt cons}(b,{\tt cons}(c,\emptyset)))
\end{eqnarray*}

The constant \cdx{Pair} constructs ordered pairs, as in {\tt
Pair($a$,$b$)}.  Ordered pairs may also be written within angle brackets,
as {\tt<$a$,$b$>}.  The $n$-tuple {\tt<$a@1$,\ldots,$a@{n-1}$,$a@n$>}
abbreviates the nest of pairs\par\nobreak
\centerline{\tt 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$.


\begin{figure} 
\index{lambda abs@$\lambda$-abstractions!in \ZF}
\index{*"-"> symbol}
\index{*"* symbol}
\begin{center} \footnotesize\tt\frenchspacing
\begin{tabular}{rrr} 
  \it external          & \it internal  & \it description \\ 
  $a$ \ttilde: $b$      & \ttilde($a$ : $b$)    & \rm negated membership\\
  \ttlbrace$a@1$, $\ldots$, $a@n$\ttrbrace  &  cons($a@1$,$\ldots$,cons($a@n$,0)) &
        \rm finite set \\
  <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & 
        Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) &
        \rm ordered $n$-tuple \\
  \ttlbrace$x$:$A . P[x]$\ttrbrace    &  Collect($A$,$\lambda x.P[x]$) &
        \rm separation \\
  \ttlbrace$y . x$:$A$, $Q[x,y]$\ttrbrace  &  Replace($A$,$\lambda x\,y.Q[x,y]$) &
        \rm replacement \\
  \ttlbrace$b[x] . x$:$A$\ttrbrace  &  RepFun($A$,$\lambda x.b[x]$) &
        \rm functional replacement \\
  \sdx{INT} $x$:$A . B[x]$      & Inter(\ttlbrace$B[x] . x$:$A$\ttrbrace) &
        \rm general intersection \\
  \sdx{UN}  $x$:$A . B[x]$      & Union(\ttlbrace$B[x] . x$:$A$\ttrbrace) &
        \rm general union \\
  \sdx{PROD} $x$:$A . B[x]$     & Pi($A$,$\lambda x.B[x]$) & 
        \rm general product \\
  \sdx{SUM}  $x$:$A . B[x]$     & Sigma($A$,$\lambda x.B[x]$) & 
        \rm general sum \\
  $A$ -> $B$            & Pi($A$,$\lambda x.B$) & 
        \rm function space \\
  $A$ * $B$             & Sigma($A$,$\lambda x.B$) & 
        \rm binary product \\
  \sdx{THE}  $x . P[x]$ & The($\lambda x.P[x]$) & 
        \rm definite description \\
  \sdx{lam}  $x$:$A . b[x]$     & Lambda($A$,$\lambda x.b[x]$) & 
        \rm $\lambda$-abstraction\\[1ex]
  \sdx{ALL} $x$:$A . P[x]$      & Ball($A$,$\lambda x.P[x]$) & 
        \rm bounded $\forall$ \\
  \sdx{EX}  $x$:$A . P[x]$      & Bex($A$,$\lambda x.P[x]$) & 
        \rm bounded $\exists$
\end{tabular}
\end{center}
\caption{Translations for {\ZF}} \label{zf-trans}
\end{figure} 


\begin{figure} 
\index{*let symbol}
\index{*in symbol}
\dquotes
\[\begin{array}{rcl}
    term & = & \hbox{expression of type~$i$} \\
         & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\
         & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
         & | & "< "  term\; ("," term)^* " >"  \\
         & | & "{\ttlbrace} " id ":" term " . " formula " {\ttrbrace}" \\
         & | & "{\ttlbrace} " id " . " id ":" term ", " formula " {\ttrbrace}" \\
         & | & "{\ttlbrace} " term " . " id ":" term " {\ttrbrace}" \\
         & | & term " `` " term \\
         & | & term " -`` " term \\
         & | & term " ` " term \\
         & | & term " * " term \\
         & | & term " Int " term \\
         & | & term " Un " term \\
         & | & term " - " term \\
         & | & term " -> " term \\
         & | & "THE~~"  id  " . " formula\\
         & | & "lam~~"  id ":" term " . " term \\
         & | & "INT~~"  id ":" term " . " term \\
         & | & "UN~~~"  id ":" term " . " term \\
         & | & "PROD~"  id ":" term " . " term \\
         & | & "SUM~~"  id ":" term " . " term \\[2ex]
 formula & = & \hbox{expression of type~$o$} \\
         & | & term " : " term \\
         & | & term " \ttilde: " term \\
         & | & term " <= " term \\
         & | & term " = " term \\
         & | & term " \ttilde= " term \\
         & | & "\ttilde\ " formula \\
         & | & formula " \& " formula \\
         & | & formula " | " formula \\
         & | & formula " --> " formula \\
         & | & formula " <-> " formula \\
         & | & "ALL " id ":" term " . " formula \\
         & | & "EX~~" id ":" term " . " formula \\
         & | & "ALL~" id~id^* " . " formula \\
         & | & "EX~~" id~id^* " . " formula \\
         & | & "EX!~" id~id^* " . " formula
  \end{array}
\]
\caption{Full grammar for {\ZF}} \label{zf-syntax}
\end{figure} 


\section{Binding operators}
The constant \cdx{Collect} constructs sets by the principle of {\bf
  separation}.  The syntax for separation is
\hbox{\tt\ttlbrace$x$:$A$.$P[x]$\ttrbrace}, where $P[x]$ is a formula
that may contain free occurrences of~$x$.  It abbreviates the set {\tt
  Collect($A$,$\lambda x.P[x]$)}, which consists of all $x\in A$ that
satisfy~$P[x]$.  Note that {\tt Collect} is an unfortunate choice of
name: some set theories adopt a set-formation principle, related to
replacement, called collection.

The constant \cdx{Replace} constructs sets by the principle of {\bf
  replacement}.  The syntax
\hbox{\tt\ttlbrace$y$.$x$:$A$,$Q[x,y]$\ttrbrace} denotes the set {\tt
  Replace($A$,$\lambda x\,y.Q[x,y]$)}, which consists of all~$y$ such
that there exists $x\in A$ satisfying~$Q[x,y]$.  The Replacement Axiom
has the condition that $Q$ must be single-valued over~$A$: for
all~$x\in A$ there exists at most one $y$ satisfying~$Q[x,y]$.  A
single-valued binary predicate is also called a {\bf class function}.

The constant \cdx{RepFun} expresses a special case of replacement,
where $Q[x,y]$ has the form $y=b[x]$.  Such a $Q$ is trivially
single-valued, since it is just the graph of the meta-level
function~$\lambda x.b[x]$.  The resulting set consists of all $b[x]$
for~$x\in A$.  This is analogous to the \ML{} functional {\tt map},
since it applies a function to every element of a set.  The syntax is
\hbox{\tt\ttlbrace$b[x]$.$x$:$A$\ttrbrace}, which expands to {\tt
  RepFun($A$,$\lambda x.b[x]$)}.

\index{*INT symbol}\index{*UN symbol} 
General unions and intersections of indexed
families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$,
are written \hbox{\tt UN $x$:$A$.$B[x]$} and \hbox{\tt INT $x$:$A$.$B[x]$}.
Their meaning is expressed using {\tt RepFun} as
\[
\bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad 
\bigcap(\{B[x]. x\in A\}). 
\]
General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be
constructed in set theory, where $B[x]$ is a family of sets over~$A$.  They
have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set.
This is similar to the situation in Constructive Type Theory (set theory
has `dependent sets') and calls for similar syntactic conventions.  The
constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and
products.  Instead of {\tt Sigma($A$,$B$)} and {\tt Pi($A$,$B$)} we may write
\hbox{\tt SUM $x$:$A$.$B[x]$} and \hbox{\tt PROD $x$:$A$.$B[x]$}.  
\index{*SUM symbol}\index{*PROD symbol}%
The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate
general sums and products over a constant family.\footnote{Unlike normal
infix operators, {\tt*} and {\tt->} merely define abbreviations; there are
no constants~{\tt 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
  The($\lambda x.P[x]$)} or use the syntax \hbox{\tt THE $x$.$P[x]$}.

\index{*lam symbol}
Function sets may be written in $\lambda$-notation; $\lambda x\in A.b[x]$
stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$.  In order for
this to be a set, the function's domain~$A$ must be given.  Using the
constant~\cdx{Lambda}, we may express function sets as {\tt
Lambda($A$,$\lambda x.b[x]$)} or use the syntax \hbox{\tt lam $x$:$A$.$b[x]$}.

Isabelle's set theory defines two {\bf bounded quantifiers}:
\begin{eqnarray*}
   \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
   \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
\end{eqnarray*}
The constants~\cdx{Ball} and~\cdx{Bex} are defined
accordingly.  Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
write
\hbox{\tt ALL $x$:$A$.$P[x]$} and \hbox{\tt EX $x$:$A$.$P[x]$}.


%%%% ZF.thy

\begin{figure}
\begin{ttbox}
\tdx{Let_def}            Let(s, f) == f(s)

\tdx{Ball_def}           Ball(A,P) == ALL x. x:A --> P(x)
\tdx{Bex_def}            Bex(A,P)  == EX x. x:A & P(x)

\tdx{subset_def}         A <= B  == ALL x:A. x:B
\tdx{extension}          A = B  <->  A <= B & B <= A

\tdx{Union_iff}          A : Union(C) <-> (EX B:C. A:B)
\tdx{Pow_iff}            A : Pow(B) <-> A <= B
\tdx{foundation}         A=0 | (EX x:A. ALL y:x. ~ y:A)

\tdx{replacement}        (ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
                   b : PrimReplace(A,P) <-> (EX x:A. P(x,b))
\subcaption{The Zermelo-Fraenkel Axioms}

\tdx{Replace_def}  Replace(A,P) == 
                   PrimReplace(A, \%x y. (EX!z.P(x,z)) & P(x,y))
\tdx{RepFun_def}   RepFun(A,f)  == {\ttlbrace}y . x:A, y=f(x)\ttrbrace
\tdx{the_def}      The(P)       == Union({\ttlbrace}y . x:{\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace})
\tdx{if_def}       if(P,a,b)    == THE z. P & z=a | ~P & z=b
\tdx{Collect_def}  Collect(A,P) == {\ttlbrace}y . x:A, x=y & P(x){\ttrbrace}
\tdx{Upair_def}    Upair(a,b)   == 
                 {\ttlbrace}y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b){\ttrbrace}
\subcaption{Consequences of replacement}

\tdx{Inter_def}    Inter(A) == {\ttlbrace}x:Union(A) . ALL y:A. x:y{\ttrbrace}
\tdx{Un_def}       A Un  B  == Union(Upair(A,B))
\tdx{Int_def}      A Int B  == Inter(Upair(A,B))
\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}
\end{figure}


\begin{figure}
\begin{ttbox}
\tdx{cons_def}     cons(a,A) == Upair(a,a) Un A
\tdx{succ_def}     succ(i) == cons(i,i)
\tdx{infinity}     0:Inf & (ALL y:Inf. succ(y): Inf)
\subcaption{Finite and infinite sets}

\tdx{Pair_def}       <a,b>      == {\ttlbrace}{\ttlbrace}a,a{\ttrbrace}, {\ttlbrace}a,b{\ttrbrace}{\ttrbrace}
\tdx{split_def}      split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b)
\tdx{fst_def}        fst(A)     == split(\%x y.x, p)
\tdx{snd_def}        snd(A)     == split(\%x y.y, p)
\tdx{Sigma_def}      Sigma(A,B) == UN x:A. UN y:B(x). {\ttlbrace}<x,y>{\ttrbrace}
\subcaption{Ordered pairs and Cartesian products}

\tdx{converse_def}   converse(r) == {\ttlbrace}z. w:r, EX x y. w=<x,y> & z=<y,x>{\ttrbrace}
\tdx{domain_def}     domain(r)   == {\ttlbrace}x. w:r, EX y. w=<x,y>{\ttrbrace}
\tdx{range_def}      range(r)    == domain(converse(r))
\tdx{field_def}      field(r)    == domain(r) Un range(r)
\tdx{image_def}      r `` A      == {\ttlbrace}y : range(r) . EX x:A. <x,y> : r{\ttrbrace}
\tdx{vimage_def}     r -`` A     == converse(r)``A
\subcaption{Operations on relations}

\tdx{lam_def}    Lambda(A,b) == {\ttlbrace}<x,b(x)> . x:A{\ttrbrace}
\tdx{apply_def}  f`a         == THE y. <a,y> : f
\tdx{Pi_def}     Pi(A,B) == {\ttlbrace}f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f{\ttrbrace}
\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}
\end{figure}



\section{The Zermelo-Fraenkel axioms}
The axioms appear in Fig.\ts \ref{zf-rules}.  They resemble those
presented by Suppes~\cite{suppes72}.  Most of the theory consists of
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.

The traditional replacement axiom asserts
\[ y \in {\tt PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \]
subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$.
The Isabelle theory defines \cdx{Replace} to apply
\cdx{PrimReplace} to the single-valued part of~$P$, namely
\[ (\exists!z.P(x,z)) \conj P(x,y). \]
Thus $y\in {\tt Replace}(A,P)$ if and only if there is some~$x$ such that
$P(x,-)$ holds uniquely for~$y$.  Because the equivalence is unconditional,
{\tt Replace} is much easier to use than {\tt PrimReplace}; it defines the
same set, if $P(x,y)$ is single-valued.  The nice syntax for replacement
expands to {\tt Replace}.

Other consequences of replacement include functional replacement
(\cdx{RepFun}) and definite descriptions (\cdx{The}).
Axioms for separation (\cdx{Collect}) and unordered pairs
(\cdx{Upair}) are traditionally assumed, but they actually follow
from replacement~\cite[pages 237--8]{suppes72}.

The definitions of general intersection, etc., are straightforward.  Note
the definition of {\tt cons}, which underlies the finite set notation.
The axiom of infinity gives us a set that contains~0 and is closed under
successor (\cdx{succ}).  Although this set is not uniquely defined,
the theory names it (\cdx{Inf}) in order to simplify the
construction of the natural numbers.
                                             
Further definitions appear in Fig.\ts\ref{zf-defs}.  Ordered pairs are
defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$.  Recall
that \cdx{Sigma}$(A,B)$ generalizes the Cartesian product of two
sets.  It is defined to be the union of all singleton sets
$\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$.  This is a typical usage of
general union.

The projections \cdx{fst} and~\cdx{snd} are defined in terms of the
generalized projection \cdx{split}.  The latter has been borrowed from
Martin-L\"of's Type Theory, and is often easier to use than \cdx{fst}
and~\cdx{snd}.

Operations on relations include converse, domain, range, and image.  The
set ${\tt Pi}(A,B)$ generalizes the space of functions between two sets.
Note the simple definitions of $\lambda$-abstraction (using
\cdx{RepFun}) and application (using a definite description).  The
function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only
over the domain~$A$.


%%%% zf.ML

\begin{figure}
\begin{ttbox}
\tdx{ballI}       [| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)
\tdx{bspec}       [| ALL x:A. P(x);  x: A |] ==> P(x)
\tdx{ballE}       [| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q

\tdx{ball_cong}   [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
            (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))

\tdx{bexI}        [| P(x);  x: A |] ==> EX x:A. P(x)
\tdx{bexCI}       [| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A.P(x)
\tdx{bexE}        [| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q |] ==> Q

\tdx{bex_cong}    [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
            (EX x:A. P(x)) <-> (EX x:A'. P'(x))
\subcaption{Bounded quantifiers}

\tdx{subsetI}       (!!x.x:A ==> x:B) ==> A <= B
\tdx{subsetD}       [| A <= B;  c:A |] ==> c:B
\tdx{subsetCE}      [| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P
\tdx{subset_refl}   A <= A
\tdx{subset_trans}  [| A<=B;  B<=C |] ==> A<=C

\tdx{equalityI}     [| A <= B;  B <= A |] ==> A = B
\tdx{equalityD1}    A = B ==> A<=B
\tdx{equalityD2}    A = B ==> B<=A
\tdx{equalityE}     [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
\subcaption{Subsets and extensionality}

\tdx{emptyE}          a:0 ==> P
\tdx{empty_subsetI}   0 <= A
\tdx{equals0I}        [| !!y. y:A ==> False |] ==> A=0
\tdx{equals0D}        [| A=0;  a:A |] ==> P

\tdx{PowI}            A <= B ==> A : Pow(B)
\tdx{PowD}            A : Pow(B)  ==>  A<=B
\subcaption{The empty set; power sets}
\end{ttbox}
\caption{Basic derived rules for {\ZF}} \label{zf-lemmas1}
\end{figure}


\section{From basic lemmas to function spaces}
Faced with so many definitions, it is essential to prove lemmas.  Even
trivial theorems like $A \int B = B \int A$ would be difficult to
prove from the definitions alone.  Isabelle's set theory derives many
rules using a natural deduction style.  Ideally, a natural deduction
rule should introduce or eliminate just one operator, but this is not
always practical.  For most operators, we may forget its definition
and use its derived rules instead.

\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 \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.

Figure~\ref{zf-lemmas1} also shows rules for the subset and equality
relations (proof by extensionality), and rules about the empty set and the
power set operator.

Figure~\ref{zf-lemmas2} presents rules for replacement and separation.
The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than
comparable rules for {\tt PrimReplace} would be.  The principle of
separation is proved explicitly, although most proofs should use the
natural deduction rules for {\tt Collect}.  The elimination rule
\tdx{CollectE} is equivalent to the two destruction rules
\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.

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
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
similar premises.


%the [p] gives better page breaking for the book
\begin{figure}[p]
\begin{ttbox}
\tdx{ReplaceI}      [| x: A;  P(x,b);  !!y. P(x,y) ==> y=b |] ==> 
              b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace}

\tdx{ReplaceE}      [| b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace};  
                 !!x. [| x: A;  P(x,b);  ALL y. P(x,y)-->y=b |] ==> R 
              |] ==> R

\tdx{RepFunI}       [| a : A |] ==> f(a) : {\ttlbrace}f(x). x:A{\ttrbrace}
\tdx{RepFunE}       [| b : {\ttlbrace}f(x). x:A{\ttrbrace};  
                 !!x.[| x:A;  b=f(x) |] ==> P |] ==> P

\tdx{separation}     a : {\ttlbrace}x:A. P(x){\ttrbrace} <-> a:A & P(a)
\tdx{CollectI}       [| a:A;  P(a) |] ==> a : {\ttlbrace}x:A. P(x){\ttrbrace}
\tdx{CollectE}       [| a : {\ttlbrace}x:A. P(x){\ttrbrace};  [| a:A; P(a) |] ==> R |] ==> R
\tdx{CollectD1}      a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> a:A
\tdx{CollectD2}      a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> P(a)
\end{ttbox}
\caption{Replacement and separation} \label{zf-lemmas2}
\end{figure}


\begin{figure}
\begin{ttbox}
\tdx{UnionI}    [| B: C;  A: B |] ==> A: Union(C)
\tdx{UnionE}    [| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R

\tdx{InterI}    [| !!x. x: C ==> A: x;  c:C |] ==> A : Inter(C)
\tdx{InterD}    [| A : Inter(C);  B : C |] ==> A : B
\tdx{InterE}    [| A : Inter(C);  A:B ==> R;  ~ B:C ==> R |] ==> R

\tdx{UN_I}      [| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))
\tdx{UN_E}      [| b : (UN x:A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R 
          |] ==> R

\tdx{INT_I}     [| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))
\tdx{INT_E}     [| b : (INT x:A. B(x));  a: A |] ==> b : B(a)
\end{ttbox}
\caption{General union and intersection} \label{zf-lemmas3}
\end{figure}


%%% upair.ML

\begin{figure}
\begin{ttbox}
\tdx{pairing}      a:Upair(b,c) <-> (a=b | a=c)
\tdx{UpairI1}      a : Upair(a,b)
\tdx{UpairI2}      b : Upair(a,b)
\tdx{UpairE}       [| a : Upair(b,c);  a = b ==> P;  a = c ==> P |] ==> P
\end{ttbox}
\caption{Unordered pairs} \label{zf-upair1}
\end{figure}


\begin{figure}
\begin{ttbox}
\tdx{UnI1}         c : A ==> c : A Un B
\tdx{UnI2}         c : B ==> c : A Un B
\tdx{UnCI}         (~c : B ==> c : A) ==> c : A Un B
\tdx{UnE}          [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P

\tdx{IntI}         [| c : A;  c : B |] ==> c : A Int B
\tdx{IntD1}        c : A Int B ==> c : A
\tdx{IntD2}        c : A Int B ==> c : B
\tdx{IntE}         [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P

\tdx{DiffI}        [| c : A;  ~ c : B |] ==> c : A - B
\tdx{DiffD1}       c : A - B ==> c : A
\tdx{DiffD2}       c : A - B ==> c ~: B
\tdx{DiffE}        [| c : A - B;  [| c:A; ~ c:B |] ==> P |] ==> P
\end{ttbox}
\caption{Union, intersection, difference} \label{zf-Un}
\end{figure}


\begin{figure}
\begin{ttbox}
\tdx{consI1}       a : cons(a,B)
\tdx{consI2}       a : B ==> a : cons(b,B)
\tdx{consCI}       (~ a:B ==> a=b) ==> a: cons(b,B)
\tdx{consE}        [| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P

\tdx{singletonI}   a : {\ttlbrace}a{\ttrbrace}
\tdx{singletonE}   [| a : {\ttlbrace}b{\ttrbrace}; a=b ==> P |] ==> P
\end{ttbox}
\caption{Finite and singleton sets} \label{zf-upair2}
\end{figure}


\begin{figure}
\begin{ttbox}
\tdx{succI1}       i : succ(i)
\tdx{succI2}       i : j ==> i : succ(j)
\tdx{succCI}       (~ i:j ==> i=j) ==> i: succ(j)
\tdx{succE}        [| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P
\tdx{succ_neq_0}   [| succ(n)=0 |] ==> P
\tdx{succ_inject}  succ(m) = succ(n) ==> m=n
\end{ttbox}
\caption{The successor function} \label{zf-succ}
\end{figure}


\begin{figure}
\begin{ttbox}
\tdx{the_equality}     [| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a
\tdx{theI}             EX! x. P(x) ==> P(THE x. P(x))

\tdx{if_P}              P ==> if(P,a,b) = a
\tdx{if_not_P}         ~P ==> if(P,a,b) = b

\tdx{mem_asym}         [| a:b;  b:a |] ==> P
\tdx{mem_irrefl}       a:a ==> P
\end{ttbox}
\caption{Descriptions; non-circularity} \label{zf-the}
\end{figure}


\subsection{Unordered pairs and finite sets}
Figure~\ref{zf-upair1} presents the principle of unordered pairing, along
with its derived rules.  Binary union and intersection are defined in terms
of ordered pairs (Fig.\ts\ref{zf-Un}).  Set difference is also included.  The
rule \tdx{UnCI} is useful for classical reasoning about unions,
like {\tt disjCI}\@; it supersedes \tdx{UnI1} and
\tdx{UnI2}, but these rules are often easier to work with.  For
intersection and difference we have both elimination and destruction rules.
Again, there is no reason to provide a minimal rule set.

Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules
for~{\tt cons}, the finite set constructor, and rules for singleton
sets.  Figure~\ref{zf-succ} presents derived rules for the successor
function, which is defined in terms of~{\tt cons}.  The proof that {\tt
  succ} is injective appears to require the Axiom of Foundation.

Definite descriptions (\sdx{THE}) are defined in terms of the singleton
set~$\{0\}$, but their derived rules fortunately hide this
(Fig.\ts\ref{zf-the}).  The rule~\tdx{theI} is difficult to apply
because of the two occurrences of~$\Var{P}$.  However,
\tdx{the_equality} does not have this problem and the files contain
many examples of its use.

Finally, the impossibility of having both $a\in b$ and $b\in a$
(\tdx{mem_asym}) is proved by applying the Axiom of Foundation to
the set $\{a,b\}$.  The impossibility of $a\in a$ is a trivial consequence.

See the file {\tt ZF/upair.ML} for full proofs of the rules discussed in
this section.


%%% subset.ML

\begin{figure}
\begin{ttbox}
\tdx{Union_upper}       B:A ==> B <= Union(A)
\tdx{Union_least}       [| !!x. x:A ==> x<=C |] ==> Union(A) <= C

\tdx{Inter_lower}       B:A ==> Inter(A) <= B
\tdx{Inter_greatest}    [| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)

\tdx{Un_upper1}         A <= A Un B
\tdx{Un_upper2}         B <= A Un B
\tdx{Un_least}          [| A<=C;  B<=C |] ==> A Un B <= C

\tdx{Int_lower1}        A Int B <= A
\tdx{Int_lower2}        A Int B <= B
\tdx{Int_greatest}      [| C<=A;  C<=B |] ==> C <= A Int B

\tdx{Diff_subset}       A-B <= A
\tdx{Diff_contains}     [| C<=A;  C Int B = 0 |] ==> C <= A-B

\tdx{Collect_subset}    Collect(A,P) <= A
\end{ttbox}
\caption{Subset and lattice properties} \label{zf-subset}
\end{figure}


\subsection{Subset and lattice properties}
The subset relation is a complete lattice.  Unions form least upper bounds;
non-empty intersections form greatest lower bounds.  Figure~\ref{zf-subset}
shows the corresponding rules.  A few other laws involving subsets are
included.  Proofs are in the file {\tt ZF/subset.ML}.

Reasoning directly about subsets often yields clearer proofs than
reasoning about the membership relation.  Section~\ref{sec:ZF-pow-example}
below presents an example of this, proving the equation ${{\tt Pow}(A)\cap
  {\tt Pow}(B)}= {\tt Pow}(A\cap B)$.

%%% pair.ML

\begin{figure}
\begin{ttbox}
\tdx{Pair_inject1}    <a,b> = <c,d> ==> a=c
\tdx{Pair_inject2}    <a,b> = <c,d> ==> b=d
\tdx{Pair_inject}     [| <a,b> = <c,d>;  [| a=c; b=d |] ==> P |] ==> P
\tdx{Pair_neq_0}      <a,b>=0 ==> P

\tdx{fst_conv}        fst(<a,b>) = a
\tdx{snd_conv}        snd(<a,b>) = b
\tdx{split}           split(\%x y.c(x,y), <a,b>) = c(a,b)

\tdx{SigmaI}          [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)

\tdx{SigmaE}          [| c: Sigma(A,B);  
                   !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P

\tdx{SigmaE2}         [| <a,b> : Sigma(A,B);    
                   [| a:A;  b:B(a) |] ==> P   |] ==> P
\end{ttbox}
\caption{Ordered pairs; projections; general sums} \label{zf-pair}
\end{figure}


\subsection{Ordered pairs}
Figure~\ref{zf-pair} presents the rules governing ordered pairs,
projections and general sums.  File {\tt ZF/pair.ML} contains the
full (and tedious) proof that $\{\{a\},\{a,b\}\}$ functions as an ordered
pair.  This property is expressed as two destruction rules,
\tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently
as the elimination rule \tdx{Pair_inject}.

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 
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}
assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form
$\pair{x,y}$, for $x\in A$ and $y\in B(x)$.  The rule \tdx{SigmaE2}
merely states that $\pair{a,b}\in {\tt Sigma}(A,B)$ implies $a\in A$ and
$b\in B(a)$.

In addition, it is possible to use tuples as patterns in abstractions:
\begin{center}
{\tt\%<$x$,$y$>.$t$} \quad stands for\quad {\tt split(\%$x$ $y$.$t$)}
\end{center}
Nested patterns are translated recursively:
{\tt\%<$x$,$y$,$z$>.$t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>.$t$} $\leadsto$
{\tt split(\%$x$.\%<$y$,$z$>.$t$)} $\leadsto$ {\tt split(\%$x$.split(\%$y$
  $z$.$t$))}. The reverse translation is performed upon printing.
\begin{warn}
  The translation between patterns and {\tt split} is performed automatically
  by the parser and printer.  Thus the internal and external form of a term
  may differ, which affects proofs.  For example the term {\tt
    (\%<x,y>.<y,x>)<a,b>} requires the theorem {\tt split} to rewrite to
  {\tt<b,a>}.
\end{warn}
In addition to explicit $\lambda$-abstractions, patterns can be used in any
variable binding construct which is internally described by a
$\lambda$-abstraction. Some important examples are
\begin{description}
\item[Let:] {\tt let {\it pattern} = $t$ in $u$}
\item[Choice:] {\tt THE~{\it pattern}~.~$P$}
\item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$}
\item[Comprehension:] {\tt {\ttlbrace}~{\it pattern}:$A$~.~$P$~{\ttrbrace}}
\end{description}


%%% domrange.ML

\begin{figure}
\begin{ttbox}
\tdx{domainI}        <a,b>: r ==> a : domain(r)
\tdx{domainE}        [| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P
\tdx{domain_subset}  domain(Sigma(A,B)) <= A

\tdx{rangeI}         <a,b>: r ==> b : range(r)
\tdx{rangeE}         [| b : range(r);  !!x. <x,b>: r ==> P |] ==> P
\tdx{range_subset}   range(A*B) <= B

\tdx{fieldI1}        <a,b>: r ==> a : field(r)
\tdx{fieldI2}        <a,b>: r ==> b : field(r)
\tdx{fieldCI}        (~ <c,a>:r ==> <a,b>: r) ==> a : field(r)

\tdx{fieldE}         [| a : field(r);  
                  !!x. <a,x>: r ==> P;  
                  !!x. <x,a>: r ==> P      
               |] ==> P

\tdx{field_subset}   field(A*A) <= A
\end{ttbox}
\caption{Domain, range and field of a relation} \label{zf-domrange}
\end{figure}

\begin{figure}
\begin{ttbox}
\tdx{imageI}         [| <a,b>: r;  a:A |] ==> b : r``A
\tdx{imageE}         [| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P

\tdx{vimageI}        [| <a,b>: r;  b:B |] ==> a : r-``B
\tdx{vimageE}        [| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P
\end{ttbox}
\caption{Image and inverse image} \label{zf-domrange2}
\end{figure}


\subsection{Relations}
Figure~\ref{zf-domrange} presents rules involving relations, which are sets
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, 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 generalisations of range and domain,
respectively.  See the file {\tt ZF/domrange.ML} for derivations of the
rules.


%%% func.ML

\begin{figure}
\begin{ttbox}
\tdx{fun_is_rel}      f: Pi(A,B) ==> f <= Sigma(A,B)

\tdx{apply_equality}  [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b
\tdx{apply_equality2} [| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c

\tdx{apply_type}      [| f: Pi(A,B);  a:A |] ==> f`a : B(a)
\tdx{apply_Pair}      [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f
\tdx{apply_iff}       f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b

\tdx{fun_extension}   [| f : Pi(A,B);  g: Pi(A,D);
                   !!x. x:A ==> f`x = g`x     |] ==> f=g

\tdx{domain_type}     [| <a,b> : f;  f: Pi(A,B) |] ==> a : A
\tdx{range_type}      [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)

\tdx{Pi_type}         [| f: A->C;  !!x. x:A ==> f`x: B(x) |] ==> f: Pi(A,B)
\tdx{domain_of_fun}   f: Pi(A,B) ==> domain(f)=A
\tdx{range_of_fun}    f: Pi(A,B) ==> f: A->range(f)

\tdx{restrict}        a : A ==> restrict(f,A) ` a = f`a
\tdx{restrict_type}   [| !!x. x:A ==> f`x: B(x) |] ==> 
                restrict(f,A) : Pi(A,B)
\end{ttbox}
\caption{Functions} \label{zf-func1}
\end{figure}


\begin{figure}
\begin{ttbox}
\tdx{lamI}         a:A ==> <a,b(a)> : (lam x:A. b(x))
\tdx{lamE}         [| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P 
             |] ==>  P

\tdx{lam_type}     [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)

\tdx{beta}         a : A ==> (lam x:A.b(x)) ` a = b(a)
\tdx{eta}          f : Pi(A,B) ==> (lam x:A. f`x) = f
\end{ttbox}
\caption{$\lambda$-abstraction} \label{zf-lam}
\end{figure}


\begin{figure}
\begin{ttbox}
\tdx{fun_empty}            0: 0->0
\tdx{fun_single}           {\ttlbrace}<a,b>{\ttrbrace} : {\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace}

\tdx{fun_disjoint_Un}      [| f: A->B;  g: C->D;  A Int C = 0  |] ==>  
                     (f Un g) : (A Un C) -> (B Un D)

\tdx{fun_disjoint_apply1}  [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
                     (f Un g)`a = f`a

\tdx{fun_disjoint_apply2}  [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
                     (f Un g)`c = g`c
\end{ttbox}
\caption{Constructing functions from smaller sets} \label{zf-func2}
\end{figure}


\subsection{Functions}
Functions, represented by graphs, are notoriously difficult to reason
about.  The file {\tt ZF/func.ML} derives many rules, which overlap more
than they ought.  This section presents the more important rules.

Figure~\ref{zf-func1} presents the basic properties of \cdx{Pi}$(A,B)$,
the generalized function space.  For example, if $f$ is a function and
$\pair{a,b}\in f$, then $f`a=b$ (\tdx{apply_equality}).  Two functions
are equal provided they have equal domains and deliver equals results
(\tdx{fun_extension}).

By \tdx{Pi_type}, a function typing of the form $f\in A\to C$ can be
refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable
family of sets $\{B(x)\}@{x\in A}$.  Conversely, by \tdx{range_of_fun},
any dependent typing can be flattened to yield a function type of the form
$A\to C$; here, $C={\tt range}(f)$.

Among the laws for $\lambda$-abstraction, \tdx{lamI} and \tdx{lamE}
describe the graph of the generated function, while \tdx{beta} and
\tdx{eta} are the standard conversions.  We essentially have a
dependently-typed $\lambda$-calculus (Fig.\ts\ref{zf-lam}).

Figure~\ref{zf-func2} presents some rules that can be used to construct
functions explicitly.  We start with functions consisting of at most one
pair, and may form the union of two functions provided their domains are
disjoint.  


\begin{figure}
\begin{ttbox}
\tdx{Int_absorb}         A Int A = A
\tdx{Int_commute}        A Int B = B Int A
\tdx{Int_assoc}          (A Int B) Int C  =  A Int (B Int C)
\tdx{Int_Un_distrib}     (A Un B) Int C  =  (A Int C) Un (B Int C)

\tdx{Un_absorb}          A Un A = A
\tdx{Un_commute}         A Un B = B Un A
\tdx{Un_assoc}           (A Un B) Un C  =  A Un (B Un C)
\tdx{Un_Int_distrib}     (A Int B) Un C  =  (A Un C) Int (B Un C)

\tdx{Diff_cancel}        A-A = 0
\tdx{Diff_disjoint}      A Int (B-A) = 0
\tdx{Diff_partition}     A<=B ==> A Un (B-A) = B
\tdx{double_complement}  [| A<=B; B<= C |] ==> (B - (C-A)) = A
\tdx{Diff_Un}            A - (B Un C) = (A-B) Int (A-C)
\tdx{Diff_Int}           A - (B Int C) = (A-B) Un (A-C)

\tdx{Union_Un_distrib}   Union(A Un B) = Union(A) Un Union(B)
\tdx{Inter_Un_distrib}   [| a:A;  b:B |] ==> 
                   Inter(A Un B) = Inter(A) Int Inter(B)

\tdx{Int_Union_RepFun}   A Int Union(B) = (UN C:B. A Int C)

\tdx{Un_Inter_RepFun}    b:B ==> 
                   A Un Inter(B) = (INT C:B. A Un C)

\tdx{SUM_Un_distrib1}    (SUM x:A Un B. C(x)) = 
                   (SUM x:A. C(x)) Un (SUM x:B. C(x))

\tdx{SUM_Un_distrib2}    (SUM x:C. A(x) Un B(x)) =
                   (SUM x:C. A(x))  Un  (SUM x:C. B(x))

\tdx{SUM_Int_distrib1}   (SUM x:A Int B. C(x)) =
                   (SUM x:A. C(x)) Int (SUM x:B. C(x))

\tdx{SUM_Int_distrib2}   (SUM x:C. A(x) Int B(x)) =
                   (SUM x:C. A(x)) Int (SUM x:C. B(x))
\end{ttbox}
\caption{Equalities} \label{zf-equalities}
\end{figure}


\begin{figure}
%\begin{constants} 
%  \cdx{1}       & $i$           &       & $\{\emptyset\}$       \\
%  \cdx{bool}    & $i$           &       & the set $\{\emptyset,1\}$     \\
%  \cdx{cond}   & $[i,i,i]\To i$ &       & conditional for {\tt bool}    \\
%  \cdx{not}    & $i\To i$       &       & negation for {\tt bool}       \\
%  \sdx{and}    & $[i,i]\To i$   & Left 70 & conjunction for {\tt bool}  \\
%  \sdx{or}     & $[i,i]\To i$   & Left 65 & disjunction for {\tt bool}  \\
%  \sdx{xor}    & $[i,i]\To i$   & Left 65 & exclusive-or for {\tt bool}
%\end{constants}
%
\begin{ttbox}
\tdx{bool_def}       bool == {\ttlbrace}0,1{\ttrbrace}
\tdx{cond_def}       cond(b,c,d) == if(b=1,c,d)
\tdx{not_def}        not(b)  == cond(b,0,1)
\tdx{and_def}        a and b == cond(a,b,0)
\tdx{or_def}         a or b  == cond(a,1,b)
\tdx{xor_def}        a xor b == cond(a,not(b),b)

\tdx{bool_1I}        1 : bool
\tdx{bool_0I}        0 : bool
\tdx{boolE}          [| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P
\tdx{cond_1}         cond(1,c,d) = c
\tdx{cond_0}         cond(0,c,d) = d
\end{ttbox}
\caption{The booleans} \label{zf-bool}
\end{figure}


\section{Further developments}
The next group of developments is complex and extensive, and only
highlights can be covered here.  It involves many theories and ML files of
proofs. 

Figure~\ref{zf-equalities} presents commutative, associative, distributive,
and idempotency laws of union and intersection, along with other equations.
See file {\tt 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 first-order theory, you can obtain the effect of higher-order
logic using {\tt bool}-valued functions, for example.  The constant~{\tt1}
is translated to {\tt succ(0)}.

\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$
\end{constants}
\begin{ttbox}
\tdx{sum_def}        A+B == {\ttlbrace}0{\ttrbrace}*A Un {\ttlbrace}1{\ttrbrace}*B
\tdx{Inl_def}        Inl(a) == <0,a>
\tdx{Inr_def}        Inr(b) == <1,b>
\tdx{case_def}       case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u)

\tdx{sum_InlI}       a : A ==> Inl(a) : A+B
\tdx{sum_InrI}       b : B ==> Inr(b) : A+B

\tdx{Inl_inject}     Inl(a)=Inl(b) ==> a=b
\tdx{Inr_inject}     Inr(a)=Inr(b) ==> a=b
\tdx{Inl_neq_Inr}    Inl(a)=Inr(b) ==> P

\tdx{sumE2}   u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))

\tdx{case_Inl}       case(c,d,Inl(a)) = c(a)
\tdx{case_Inr}       case(c,d,Inr(b)) = d(b)
\end{ttbox}
\caption{Disjoint unions} \label{zf-sum}
\end{figure}


Theory \thydx{Sum} defines the disjoint union of two sets, with
injections and a case analysis operator (Fig.\ts\ref{zf-sum}).  Disjoint
unions play a role in datatype definitions, particularly when there is
mutual recursion~\cite{paulson-set-II}.

\begin{figure}
\begin{ttbox}
\tdx{QPair_def}       <a;b> == a+b
\tdx{qsplit_def}      qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)
\tdx{qfsplit_def}     qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)
\tdx{qconverse_def}   qconverse(r) == {\ttlbrace}z. w:r, EX x y. w=<x;y> & z=<y;x>{\ttrbrace}
\tdx{QSigma_def}      QSigma(A,B)  == UN x:A. UN y:B(x). {\ttlbrace}<x;y>{\ttrbrace}

\tdx{qsum_def}        A <+> B      == ({\ttlbrace}0{\ttrbrace} <*> A) Un ({\ttlbrace}1{\ttrbrace} <*> B)
\tdx{QInl_def}        QInl(a)      == <0;a>
\tdx{QInr_def}        QInr(b)      == <1;b>
\tdx{qcase_def}       qcase(c,d)   == qsplit(\%y z. cond(y, d(z), c(z)))
\end{ttbox}
\caption{Non-standard pairs, products and sums} \label{zf-qpair}
\end{figure}

Theory \thydx{QPair} defines a notion of ordered pair that admits
non-well-founded tupling (Fig.\ts\ref{zf-qpair}).  Such pairs are written
{\tt<$a$;$b$>}.  It also defines the eliminator \cdx{qsplit}, the
converse operator \cdx{qconverse}, and the summation operator
\cdx{QSigma}.  These are completely analogous to the corresponding
versions for standard ordered pairs.  The theory goes on to define a
non-standard notion of disjoint sum using non-standard pairs.  All of these
concepts satisfy the same properties as their standard counterparts; in
addition, {\tt<$a$;$b$>} is continuous.  The theory supports coinductive
definitions, for example of infinite lists~\cite{paulson-final}.

\begin{figure}
\begin{ttbox}
\tdx{bnd_mono_def}   bnd_mono(D,h) == 
                 h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))

\tdx{lfp_def}        lfp(D,h) == Inter({\ttlbrace}X: Pow(D). h(X) <= X{\ttrbrace})
\tdx{gfp_def}        gfp(D,h) == Union({\ttlbrace}X: Pow(D). X <= h(X){\ttrbrace})


\tdx{lfp_lowerbound} [| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A

\tdx{lfp_subset}     lfp(D,h) <= D

\tdx{lfp_greatest}   [| bnd_mono(D,h);  
                  !!X. [| h(X) <= X;  X<=D |] ==> A<=X 
               |] ==> A <= lfp(D,h)

\tdx{lfp_Tarski}     bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))

\tdx{induct}         [| a : lfp(D,h);  bnd_mono(D,h);
                  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x)
               |] ==> P(a)

\tdx{lfp_mono}       [| bnd_mono(D,h);  bnd_mono(E,i);
                  !!X. X<=D ==> h(X) <= i(X)  
               |] ==> lfp(D,h) <= lfp(E,i)

\tdx{gfp_upperbound} [| A <= h(A);  A<=D |] ==> A <= gfp(D,h)

\tdx{gfp_subset}     gfp(D,h) <= D

\tdx{gfp_least}      [| bnd_mono(D,h);  
                  !!X. [| X <= h(X);  X<=D |] ==> X<=A
               |] ==> gfp(D,h) <= A

\tdx{gfp_Tarski}     bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))

\tdx{coinduct}       [| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D 
               |] ==> a : gfp(D,h)

\tdx{gfp_mono}       [| bnd_mono(D,h);  D <= E;
                  !!X. X<=D ==> h(X) <= i(X)  
               |] ==> gfp(D,h) <= gfp(E,i)
\end{ttbox}
\caption{Least and greatest fixedpoints} \label{zf-fixedpt}
\end{figure}

The Knaster-Tarski Theorem states that every monotone function over a
complete lattice has a fixedpoint.  Theory \thydx{Fixedpt} proves the
Theorem only for a particular lattice, namely the lattice of subsets of a
set (Fig.\ts\ref{zf-fixedpt}).  The theory defines least and greatest
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-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.

Monotonicity properties are proved for most of the set-forming operations:
union, intersection, Cartesian product, image, domain, range, etc.  These
are useful for applying the Knaster-Tarski Fixedpoint Theorem.  The proofs
themselves are trivial applications of Isabelle's classical reasoner.  See
file {\tt ZF/mono.ML}.


\begin{figure}
\begin{constants} 
  \it symbol  & \it meta-type & \it priority & \it description \\ 
  \sdx{O}       & $[i,i]\To i$  &  Right 60     & composition ($\circ$) \\
  \cdx{id}      & $i\To i$      &       & identity function \\
  \cdx{inj}     & $[i,i]\To i$  &       & injective function space\\
  \cdx{surj}    & $[i,i]\To i$  &       & surjective function space\\
  \cdx{bij}     & $[i,i]\To i$  &       & bijective function space
\end{constants}

\begin{ttbox}
\tdx{comp_def}  r O s     == {\ttlbrace}xz : domain(s)*range(r) . 
                        EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r{\ttrbrace}
\tdx{id_def}    id(A)     == (lam x:A. x)
\tdx{inj_def}   inj(A,B)  == {\ttlbrace} f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x {\ttrbrace}
\tdx{surj_def}  surj(A,B) == {\ttlbrace} f: A->B . ALL y:B. EX x:A. f`x=y {\ttrbrace}
\tdx{bij_def}   bij(A,B)  == inj(A,B) Int surj(A,B)


\tdx{left_inverse}     [| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a
\tdx{right_inverse}    [| f: inj(A,B);  b: range(f) |] ==> 
                 f`(converse(f)`b) = b

\tdx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A)
\tdx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A)

\tdx{comp_type}        [| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C
\tdx{comp_assoc}       (r O s) O t = r O (s O t)

\tdx{left_comp_id}     r<=A*B ==> id(B) O r = r
\tdx{right_comp_id}    r<=A*B ==> r O id(A) = r

\tdx{comp_func}        [| g:A->B; f:B->C |] ==> (f O g):A->C
\tdx{comp_func_apply}  [| g:A->B; f:B->C; a:A |] ==> (f O g)`a = f`(g`a)

\tdx{comp_inj}         [| g:inj(A,B);  f:inj(B,C)  |] ==> (f O g):inj(A,C)
\tdx{comp_surj}        [| g:surj(A,B); f:surj(B,C) |] ==> (f O g):surj(A,C)
\tdx{comp_bij}         [| g:bij(A,B); f:bij(B,C) |] ==> (f O g):bij(A,C)

\tdx{left_comp_inverse}     f: inj(A,B) ==> converse(f) O f = id(A)
\tdx{right_comp_inverse}    f: surj(A,B) ==> f O converse(f) = id(B)

\tdx{bij_disjoint_Un}   
    [| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> 
    (f Un g) : bij(A Un C, B Un D)

\tdx{restrict_bij}  [| f:inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)
\end{ttbox}
\caption{Permutations} \label{zf-perm}
\end{figure}

The theory \thydx{Perm} is concerned with permutations (bijections) and
related concepts.  These include composition of relations, the identity
relation, and three specialized function spaces: injective, surjective and
bijective.  Figure~\ref{zf-perm} displays many of their properties that
have been proved.  These results are fundamental to a treatment of
equipollence and cardinality.

\begin{figure}\small
\index{#*@{\tt\#*} symbol}
\index{*div symbol}
\index{*mod symbol}
\index{#+@{\tt\#+} symbol}
\index{#-@{\tt\#-} symbol}
\begin{constants}
  \it symbol  & \it meta-type & \it priority & \it description \\ 
  \cdx{nat}     & $i$                   &       & set of natural numbers \\
  \cdx{nat_case}& $[i,i\To i,i]\To i$     &     & conditional for $nat$\\
  \cdx{rec}     & $[i,i,[i,i]\To i]\To i$ &     & recursor for $nat$\\
  \tt \#*       & $[i,i]\To i$  &  Left 70      & multiplication \\
  \tt div       & $[i,i]\To i$  &  Left 70      & division\\
  \tt mod       & $[i,i]\To i$  &  Left 70      & modulus\\
  \tt \#+       & $[i,i]\To i$  &  Left 65      & addition\\
  \tt \#-       & $[i,i]\To i$  &  Left 65      & subtraction
\end{constants}

\begin{ttbox}
\tdx{nat_def}       nat == lfp(lam r: Pow(Inf). {\ttlbrace}0{\ttrbrace} Un {\ttlbrace}succ(x). x:r{\ttrbrace}

\tdx{nat_case_def}  nat_case(a,b,k) == 
              THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))

\tdx{rec_def}       rec(k,a,b) ==  
              transrec(k, \%n f. nat_case(a, \%m. b(m, f`m), n))

\tdx{add_def}       m#+n    == rec(m, n, \%u v.succ(v))
\tdx{diff_def}      m#-n    == rec(n, m, \%u v. rec(v, 0, \%x y.x))
\tdx{mult_def}      m#*n    == rec(m, 0, \%u v. n #+ v)
\tdx{mod_def}       m mod n == transrec(m, \%j f. if(j:n, j, f`(j#-n)))
\tdx{div_def}       m div n == transrec(m, \%j f. if(j:n, 0, succ(f`(j#-n))))


\tdx{nat_0I}        0 : nat
\tdx{nat_succI}     n : nat ==> succ(n) : nat

\tdx{nat_induct}        
    [| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) 
    |] ==> P(n)

\tdx{nat_case_0}    nat_case(a,b,0) = a
\tdx{nat_case_succ} nat_case(a,b,succ(m)) = b(m)

\tdx{rec_0}         rec(0,a,b) = a
\tdx{rec_succ}      rec(succ(m),a,b) = b(m, rec(m,a,b))

\tdx{mult_type}     [| m:nat;  n:nat |] ==> m #* n : nat
\tdx{mult_0}        0 #* n = 0
\tdx{mult_succ}     succ(m) #* n = n #+ (m #* n)
\tdx{mult_commute}  [| m:nat; n:nat |] ==> m #* n = n #* m
\tdx{add_mult_dist} [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k){\thinspace}#+{\thinspace}(n #* k)
\tdx{mult_assoc}
    [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)
\tdx{mod_quo_equality}
    [| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m
\end{ttbox}
\caption{The natural numbers} \label{zf-nat}
\end{figure}

Theory \thydx{Nat} defines the natural numbers and mathematical
induction, along with a case analysis operator.  The set of natural
numbers, here called {\tt nat}, is known in set theory as the ordinal~$\omega$.

Theory \thydx{Arith} defines primitive recursion and goes on to develop
arithmetic on the natural numbers (Fig.\ts\ref{zf-nat}).  It defines
addition, multiplication, subtraction, division, and remainder.  Many of
their properties are proved: commutative, associative and distributive
laws, identity and cancellation laws, etc.  The most interesting result is
perhaps the theorem $a \bmod b + (a/b)\times b = a$.  Division and
remainder are defined by repeated subtraction, which requires well-founded
rather than primitive recursion; the termination argument relies on the
divisor's being non-zero.

Theory \thydx{Univ} defines a `universe' ${\tt univ}(A)$, for
constructing datatypes such as trees.  This set contains $A$ and the
natural numbers.  Vitally, it is closed under finite products: ${\tt
  univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$.  This theory also
defines the cumulative hierarchy of axiomatic set theory, which
traditionally is written $V@\alpha$ for an ordinal~$\alpha$.  The
`universe' is a simple generalization of~$V@\omega$.

Theory \thydx{QUniv} defines a `universe' ${\tt quniv}(A)$, for
constructing codatatypes such as streams.  It is analogous to ${\tt
  univ}(A)$ (and is defined in terms of it) but is closed under the
non-standard product and sum.

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.emptyI}      0 : Fin(A)
\tdx{Fin.consI}       [| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)

\tdx{Fin_induct}
    [| b: Fin(A);
       P(0);
       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y))
    |] ==> P(b)

\tdx{Fin_mono}        A<=B ==> Fin(A) <= Fin(B)
\tdx{Fin_UnI}         [| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)
\tdx{Fin_UnionI}      C : Fin(Fin(A)) ==> Union(C) : Fin(A)
\tdx{Fin_subset}      [| c<=b;  b: Fin(A) |] ==> c: Fin(A)
\end{ttbox}
\caption{The finite set operator} \label{zf-fin}
\end{figure}

\begin{figure}
\begin{constants}
  \cdx{list}    & $i\To i$      && lists over some set\\
  \cdx{list_case} & $[i, [i,i]\To i, i] \To i$  && conditional for $list(A)$ \\
  \cdx{list_rec} & $[i, i, [i,i,i]\To i] \To i$ && recursor for $list(A)$ \\
  \cdx{map}     & $[i\To i, i] \To i$   &       & mapping functional\\
  \cdx{length}  & $i\To i$              &       & length of a list\\
  \cdx{rev}     & $i\To i$              &       & reverse of a list\\
  \tt \at       & $[i,i]\To i$  &  Right 60     & append for lists\\
  \cdx{flat}    & $i\To i$   &                  & append of list of lists
\end{constants}

\underscoreon %%because @ is used here
\begin{ttbox}
\tdx{list_rec_def}    list_rec(l,c,h) == 
                Vrec(l, \%l g.list_case(c, \%x xs. h(x, xs, g`xs), l))

\tdx{map_def}         map(f,l)  == list_rec(l,  0,  \%x xs r. <f(x), r>)
\tdx{length_def}      length(l) == list_rec(l,  0,  \%x xs r. succ(r))
\tdx{app_def}         xs@ys     == list_rec(xs, ys, \%x xs r. <x,r>)
\tdx{rev_def}         rev(l)    == list_rec(l,  0,  \%x xs r. r @ <x,0>)
\tdx{flat_def}        flat(ls)  == list_rec(ls, 0,  \%l ls r. l @ r)


\tdx{NilI}            Nil : list(A)
\tdx{ConsI}           [| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)

\tdx{List.induct}
    [| l: list(A);
       P(Nil);
       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(Cons(x,y))
    |] ==> P(l)

\tdx{Cons_iff}        Cons(a,l)=Cons(a',l') <-> a=a' & l=l'
\tdx{Nil_Cons_iff}    ~ Nil=Cons(a,l)

\tdx{list_mono}       A<=B ==> list(A) <= list(B)

\tdx{list_rec_Nil}    list_rec(Nil,c,h) = c
\tdx{list_rec_Cons}   list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))

\tdx{map_ident}       l: list(A) ==> map(\%u.u, l) = l
\tdx{map_compose}     l: list(A) ==> map(h, map(j,l)) = map(\%u.h(j(u)), l)
\tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)
\tdx{map_type}
    [| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)
\tdx{map_flat}
    ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))
\end{ttbox}
\caption{Lists} \label{zf-list}
\end{figure}


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
recursion and the usual list functions.

The constructions of the natural numbers and lists make use of a suite of
operators for handling recursive function definitions.  I have described
the developments in detail elsewhere~\cite{paulson-set-II}.  Here is a brief
summary:
\begin{itemize}
  \item Theory {\tt Trancl} defines the transitive closure of a relation
    (as a least fixedpoint).

  \item Theory {\tt WF} proves the Well-Founded Recursion Theorem, using an
    elegant approach of Tobias Nipkow.  This theorem permits general
    recursive definitions within set theory.

  \item Theory {\tt Ord} defines the notions of transitive set and ordinal
    number.  It derives transfinite induction.  A key definition is {\bf
      less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and
    $i\in j$.  As a special case, it includes less than on the natural
    numbers.
    
  \item Theory {\tt Epsilon} derives $\varepsilon$-induction and
    $\varepsilon$-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}

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
extensively.  File {\tt ZF/simpdata.ML} contains the details.

The extraction of rewrite rules takes set theory 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 A$ and~$P(a)$.  It can also break down $a\in A\int B$ and $a\in A-B$.

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}.  See the file 
{\tt ZF/simpdata.ML} for a fuller list.

\begin{figure}
\begin{eqnarray*}
  a\in \emptyset        & \bimp &  \bot\\
  a \in A \un B      & \bimp &  a\in A \disj a\in B\\
  a \in A \int B      & \bimp &  a\in A \conj a\in B\\
  a \in A-B             & \bimp &  a\in A \conj \neg (a\in B)\\
  \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{Some rewrite rules for set theory} \label{zf-simpdata}
\end{figure}


\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-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 Theory {\tt Ramsey} proves the finite exponent 2 version of
  Ramsey's Theorem, following Basin and Kaufmann's
  presentation~\cite{basin91}.

\item Theory {\tt Integ} develops a theory of the integers as
  equivalence classes of pairs of natural numbers.

\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 Theory {\tt BT} defines the recursive data structure ${\tt
    bt}(A)$, labelled binary trees.

\item Theory {\tt Term} defines a recursive data structure for terms
  and term lists.  These are simply finite branching trees.

\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 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.

\item Theory {\tt ListN} inductively defines the lists of $n$
  elements~\cite{paulin92}.

\item Theory {\tt Acc} inductively defines the accessible part of a
  relation~\cite{paulin92}.

\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}
To demonstrate high-level reasoning about subsets, let us prove the
equation ${{\tt Pow}(A)\cap {\tt Pow}(B)}= {\tt Pow}(A\cap B)$.  Compared
with first-order logic, set theory involves a maze of rules, and theorems
have many different proofs.  Attempting other proofs of the theorem might
be instructive.  This proof exploits the lattice properties of
intersection.  It also uses the monotonicity of the powerset operation,
from {\tt ZF/mono.ML}:
\begin{ttbox}
\tdx{Pow_mono}      A<=B ==> Pow(A) <= Pow(B)
\end{ttbox}
We enter the goal and make the first step, which breaks the equation into
two inclusions by extensionality:\index{*equalityI theorem}
\begin{ttbox}
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)}
\ttbreak
by (resolve_tac [equalityI] 1);
{\out Level 1}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out  1. Pow(A Int B) <= Pow(A) Int Pow(B)}
{\out  2. Pow(A) Int Pow(B) <= Pow(A Int B)}
\end{ttbox}
Both inclusions could be tackled straightforwardly using {\tt subsetI}.
A shorter proof results from noting that intersection forms the greatest
lower bound:\index{*Int_greatest theorem}
\begin{ttbox}
by (resolve_tac [Int_greatest] 1);
{\out Level 2}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out  1. Pow(A Int B) <= Pow(A)}
{\out  2. Pow(A Int B) <= Pow(B)}
{\out  3. Pow(A) Int Pow(B) <= Pow(A Int B)}
\end{ttbox}
Subgoal~1 follows by applying the monotonicity of {\tt Pow} to $A\int
B\subseteq A$; subgoal~2 follows similarly:
\index{*Int_lower1 theorem}\index{*Int_lower2 theorem}
\begin{ttbox}
by (resolve_tac [Int_lower1 RS Pow_mono] 1);
{\out Level 3}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out  1. Pow(A Int B) <= Pow(B)}
{\out  2. Pow(A) Int Pow(B) <= Pow(A Int B)}
\ttbreak
by (resolve_tac [Int_lower2 RS Pow_mono] 1);
{\out Level 4}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out  1. Pow(A) Int Pow(B) <= Pow(A Int B)}
\end{ttbox}
We are left with the opposite inclusion, which we tackle in the
straightforward way:\index{*subsetI theorem}
\begin{ttbox}
by (resolve_tac [subsetI] 1);
{\out Level 5}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out  1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)}
\end{ttbox}
The subgoal is to show $x\in {\tt Pow}(A\cap B)$ assuming $x\in{\tt
Pow}(A)\cap {\tt Pow}(B)$; eliminating this assumption produces two
subgoals.  The rule \tdx{IntE} treats the intersection like a conjunction
instead of unfolding its definition.
\begin{ttbox}
by (eresolve_tac [IntE] 1);
{\out Level 6}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out  1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)}
\end{ttbox}
The next step replaces the {\tt Pow} by the subset
relation~($\subseteq$).\index{*PowI theorem}
\begin{ttbox}
by (resolve_tac [PowI] 1);
{\out Level 7}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out  1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B}
\end{ttbox}
We perform the same replacement in the assumptions.  This is a good
demonstration of the tactic \ttindex{dresolve_tac}:\index{*PowD theorem}
\begin{ttbox}
by (REPEAT (dresolve_tac [PowD] 1));
{\out Level 8}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out  1. !!x. [| x <= A; x <= B |] ==> x <= A Int B}
\end{ttbox}
The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but
$A\int B$ is the greatest lower bound:\index{*Int_greatest theorem}
\begin{ttbox}
by (resolve_tac [Int_greatest] 1);
{\out Level 9}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out  1. !!x. [| x <= A; x <= B |] ==> x <= A}
{\out  2. !!x. [| x <= A; x <= B |] ==> x <= B}
\end{ttbox}
To conclude the proof, we clear up the trivial subgoals:
\begin{ttbox}
by (REPEAT (assume_tac 1));
{\out Level 10}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out No subgoals!}
\end{ttbox}
\medskip
We could have performed this proof in one step by applying
\ttindex{Blast_tac}.  Let us
go back to the start:
\begin{ttbox}
choplev 0;
{\out Level 0}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}
by (Blast_tac 1);
{\out Depth = 0}
{\out Depth = 1}
{\out Depth = 2}
{\out Depth = 3}
{\out Level 1}
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
{\out No subgoals!}
\end{ttbox}
Past researchers regarded this as a difficult proof, as indeed it is if all
the symbols are replaced by their definitions.
\goodbreak

\section{Monotonicity of the union operator}
For another example, we prove that general union is monotonic:
${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$.  To begin, we
tackle the inclusion using \tdx{subsetI}:
\begin{ttbox}
val [prem] = goal thy "C<=D ==> Union(C) <= Union(D)";
{\out Level 0}
{\out Union(C) <= Union(D)}
{\out  1. Union(C) <= Union(D)}
{\out val prem = "C <= D  [C <= D]" : thm}
\ttbreak
by (resolve_tac [subsetI] 1);
{\out Level 1}
{\out Union(C) <= Union(D)}
{\out  1. !!x. x : Union(C) ==> x : Union(D)}
\end{ttbox}
Big union is like an existential quantifier --- the occurrence in the
assumptions must be eliminated early, since it creates parameters.
\index{*UnionE theorem}
\begin{ttbox}
by (eresolve_tac [UnionE] 1);
{\out Level 2}
{\out Union(C) <= Union(D)}
{\out  1. !!x B. [| x : B; B : C |] ==> x : Union(D)}
\end{ttbox}
Now we may apply \tdx{UnionI}, which creates an unknown involving the
parameters.  To show $x\in \bigcup(D)$ it suffices to show that $x$ belongs
to some element, say~$\Var{B2}(x,B)$, of~$D$.
\begin{ttbox}
by (resolve_tac [UnionI] 1);
{\out Level 3}
{\out Union(C) <= Union(D)}
{\out  1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D}
{\out  2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)}
\end{ttbox}
Combining \tdx{subsetD} with the premise $C\subseteq D$ yields 
$\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1:
\begin{ttbox}
by (resolve_tac [prem RS subsetD] 1);
{\out Level 4}
{\out Union(C) <= Union(D)}
{\out  1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C}
{\out  2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)}
\end{ttbox}
The rest is routine.  Note how~$\Var{B2}(x,B)$ is instantiated.
\begin{ttbox}
by (assume_tac 1);
{\out Level 5}
{\out Union(C) <= Union(D)}
{\out  1. !!x B. [| x : B; B : C |] ==> x : B}
by (assume_tac 1);
{\out Level 6}
{\out Union(C) <= Union(D)}
{\out No subgoals!}
\end{ttbox}
Again, \ttindex{Blast_tac} can prove the theorem in one
step, provided we somehow supply it with~{\tt prem}.  We can add
\hbox{\tt prem RS subsetD} to the claset as an introduction rule:
\begin{ttbox}
by (blast_tac (!claset addIs [prem RS subsetD]) 1);
{\out Depth = 0}
{\out Depth = 1}
{\out Depth = 2}
{\out Level 1}
{\out Union(C) <= Union(D)}
{\out No subgoals!}
\end{ttbox}
As an alternative, we could add premise to the assumptions, either using
\ttindex{cut_facts_tac} or by stating the original goal using~\texttt{!!}:
\begin{ttbox}
goal thy "!!C D. C<=D ==> Union(C) <= Union(D)";
{\out Level 0}
{\out Union(C) <= Union(D)}
{\out  1. !!C D. C <= D ==> Union(C) <= Union(D)}
by (Blast_tac 1);
\end{ttbox}

The file {\tt ZF/equalities.ML} has many similar proofs.  Reasoning about
general intersection can be difficult because of its anomalous behaviour on
the empty set.  However, \ttindex{Blast_tac} copes well with these.  Here is
a typical example, borrowed from Devlin~\cite[page 12]{devlin79}:
\begin{ttbox}
a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C.A(x)) Int (INT x:C.B(x))
\end{ttbox}
In traditional notation this is
\[ a\in C \,\Imp\, \inter@{x\in C} \Bigl(A(x) \int B(x)\Bigr) =        
       \Bigl(\inter@{x\in C} A(x)\Bigr)  \int  
       \Bigl(\inter@{x\in C} B(x)\Bigr)  \]

\section{Low-level reasoning about functions}
The derived rules {\tt lamI}, {\tt lamE}, {\tt lam_type}, {\tt beta}
and {\tt eta} support reasoning about functions in a
$\lambda$-calculus style.  This is generally easier than regarding
functions as sets of ordered pairs.  But sometimes we must look at the
underlying representation, as in the following proof
of~\tdx{fun_disjoint_apply1}.  This states that if $f$ and~$g$ are
functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then
$(f\un g)`a = f`a$:
\begin{ttbox}
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}
{\out (f Un g) ` a = f ` a}
{\out  1. (f Un g) ` a = f ` a}
\end{ttbox}
Isabelle has produced the output above; the \ML{} top-level now echoes the
binding of {\tt prems}.
\begin{ttbox}
{\out val prems = ["a : A  [a : A]",}
{\out              "f : A -> B  [f : A -> B]",}
{\out              "g : C -> D  [g : C -> D]",}
{\out              "A Int C = 0  [A Int C = 0]"] : thm list}
\end{ttbox}
Using \tdx{apply_equality}, we reduce the equality to reasoning about
ordered pairs.  The second subgoal is to verify that $f\un g$ is a function.
\begin{ttbox}
by (resolve_tac [apply_equality] 1);
{\out Level 1}
{\out (f Un g) ` a = f ` a}
{\out  1. <a,f ` a> : f Un g}
{\out  2. f Un g : (PROD x:?A. ?B(x))}
\end{ttbox}
We must show that the pair belongs to~$f$ or~$g$; by~\tdx{UnI1} we
choose~$f$:
\begin{ttbox}
by (resolve_tac [UnI1] 1);
{\out Level 2}
{\out (f Un g) ` a = f ` a}
{\out  1. <a,f ` a> : f}
{\out  2. f Un g : (PROD x:?A. ?B(x))}
\end{ttbox}
To show $\pair{a,f`a}\in f$ we use \tdx{apply_Pair}, which is
essentially the converse of \tdx{apply_equality}:
\begin{ttbox}
by (resolve_tac [apply_Pair] 1);
{\out Level 3}
{\out (f Un g) ` a = f ` a}
{\out  1. f : (PROD x:?A2. ?B2(x))}
{\out  2. a : ?A2}
{\out  3. f Un g : (PROD x:?A. ?B(x))}
\end{ttbox}
Using the premises $f\in A\to B$ and $a\in A$, we solve the two subgoals
from \tdx{apply_Pair}.  Recall that a $\Pi$-set is merely a generalized
function space, and observe that~{\tt?A2} is instantiated to~{\tt A}.
\begin{ttbox}
by (resolve_tac prems 1);
{\out Level 4}
{\out (f Un g) ` a = f ` a}
{\out  1. a : A}
{\out  2. f Un g : (PROD x:?A. ?B(x))}
by (resolve_tac prems 1);
{\out Level 5}
{\out (f Un g) ` a = f ` a}
{\out  1. f Un g : (PROD x:?A. ?B(x))}
\end{ttbox}
To construct functions of the form $f\un g$, we apply
\tdx{fun_disjoint_Un}:
\begin{ttbox}
by (resolve_tac [fun_disjoint_Un] 1);
{\out Level 6}
{\out (f Un g) ` a = f ` a}
{\out  1. f : ?A3 -> ?B3}
{\out  2. g : ?C3 -> ?D3}
{\out  3. ?A3 Int ?C3 = 0}
\end{ttbox}
The remaining subgoals are instances of the premises.  Again, observe how
unknowns are instantiated:
\begin{ttbox}
by (resolve_tac prems 1);
{\out Level 7}
{\out (f Un g) ` a = f ` a}
{\out  1. g : ?C3 -> ?D3}
{\out  2. A Int ?C3 = 0}
by (resolve_tac prems 1);
{\out Level 8}
{\out (f Un g) ` a = f ` a}
{\out  1. A Int C = 0}
by (resolve_tac prems 1);
{\out Level 9}
{\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
examples of reasoning about functions.

\index{set theory|)}