%% $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~\texttt{FOL}, classical

first-order logic.  The theory includes a collection of derived natural

deduction rules, for use with Isabelle's classical reasoner.  Some

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.  \texttt{ZF} provides

both the integers and the natural numbers.  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.

\texttt{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.  It

provides a streamlined syntax for defining primitive recursive functions over

datatypes. 

Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{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-mscs}.

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

\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

\texttt{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 \isa{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 \isa{let}, set theory does not use polymorphism.  All terms in

ZF have type~\tydx{i}, which is the type of individuals and has

class~\cldx{term}.  The type of first-order formulae, remember, 

is~\tydx{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 $\lnot(a\in b)$,

which is equivalent to  $a\notin 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 \isa{Upair($A$,$B$)} denotes the set~$\{A,B\}$ and

\isa{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(\isa{Upair}(A,B)) \\

   \isa{cons}(a,B)      & \equiv &        \isa{Upair}(a,a) \un B

\end{eqnarray*}

The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the

obvious manner using~\isa{cons} and~$\emptyset$ (the empty set) \isasymin \begin{eqnarray*}

 \{a,b,c\} & \equiv & \isa{cons}(a,\isa{cons}(b,\isa{cons}(c,\emptyset)))

\end{eqnarray*}

The constant \cdx{Pair} constructs ordered pairs, as in \isa{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{\isa{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}

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

         & | & "if"~term~"then"~term~"else"~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 " \isasyminter " term \\

         & | & term " \isasymunion " 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 \isa{Collect($A$,$\lambda x. P[x]$)}, which consists of all $x\in A$ that

satisfy~$P[x]$.  Note that \isa{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 

\isa{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 \isa{map},

since it applies a function to every element of a set.  The syntax is

\isa{\ttlbrace$b[x]$.\ $x$:$A$\ttrbrace}, which expands to 

\isa{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 \isa{UN $x$:$A$.\ $B[x]$} and \isa{INT $x$:$A$.\ $B[x]$}.

Their meaning is expressed using \isa{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 \isa{Sigma($A$,$B$)} and \isa{Pi($A$,$B$)} we may

write 

\isa{SUM $x$:$A$.\ $B[x]$} and \isa{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~\isa{op~*} and~\isa{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 

\isa{The($\lambda x. P[x]$)} or use the syntax \isa{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 \isa{Lambda($A$,$\lambda x. b[x]$)} or use the syntax \isa{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 \isa{Ball($A$,$P$)} and \isa{Bex($A$,$P$)} we may

write

\isa{ALL $x$:$A$.\ $P[x]$} and \isa{EX $x$:$A$.\ $P[x]$}.

%%%% ZF.thy

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{Let_def}:           Let(s, f) == f(s)

\tdx{Ball_def}:          Ball(A,P) == {\isasymforall}x. x \isasymin A --> P(x)

\tdx{Bex_def}:           Bex(A,P)  == {\isasymexists}x. x \isasymin A & P(x)

\tdx{subset_def}:        A \isasymsubseteq B  == {\isasymforall}x \isasymin A. x \isasymin B

\tdx{extension}:         A = B  <->  A \isasymsubseteq B & B \isasymsubseteq A

\tdx{Union_iff}:         A \isasymin Union(C) <-> ({\isasymexists}B \isasymin C. A \isasymin B)

\tdx{Pow_iff}:           A \isasymin Pow(B) <-> A \isasymsubseteq B

\tdx{foundation}:        A=0 | ({\isasymexists}x \isasymin A. {\isasymforall}y \isasymin x. y \isasymnotin A)

\tdx{replacement}:       ({\isasymforall}x \isasymin A. {\isasymforall}y z. P(x,y) & P(x,z) --> y=z) ==>

                   b \isasymin PrimReplace(A,P) <-> ({\isasymexists}x{\isasymin}A. P(x,b))

\subcaption{The Zermelo-Fraenkel Axioms}

\tdx{Replace_def}: Replace(A,P) == 

                   PrimReplace(A, \%x y. (\isasymexists!z. P(x,z)) & P(x,y))

\tdx{RepFun_def}:  RepFun(A,f)  == {\ttlbrace}y . x \isasymin A, y=f(x)\ttrbrace

\tdx{the_def}:     The(P)       == Union({\ttlbrace}y . x \isasymin {\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 \isasymin A, x=y & P(x){\ttrbrace}

\tdx{Upair_def}:   Upair(a,b)   == 

               {\ttlbrace}y. x\isasymin{}Pow(Pow(0)), x=0 & y=a | x=Pow(0) & y=b{\ttrbrace}

\subcaption{Consequences of replacement}

\tdx{Inter_def}:   Inter(A) == {\ttlbrace}x \isasymin Union(A) . {\isasymforall}y \isasymin A. x \isasymin y{\ttrbrace}

\tdx{Un_def}:      A \isasymunion B  == Union(Upair(A,B))

\tdx{Int_def}:     A \isasyminter B  == Inter(Upair(A,B))

\tdx{Diff_def}:    A - B    == {\ttlbrace}x \isasymin A . x \isasymnotin B{\ttrbrace}

\subcaption{Union, intersection, difference}

\end{alltt*}

\caption{Rules and axioms of ZF} \label{zf-rules}

\end{figure}

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{cons_def}:    cons(a,A) == Upair(a,a) \isasymunion A

\tdx{succ_def}:    succ(i) == cons(i,i)

\tdx{infinity}:    0 \isasymin Inf & ({\isasymforall}y \isasymin Inf. succ(y) \isasymin 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. {\isasymexists}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) == {\isasymUnion}x \isasymin A. {\isasymUnion}y \isasymin B(x). {\ttlbrace}<x,y>{\ttrbrace}

\subcaption{Ordered pairs and Cartesian products}

\tdx{converse_def}: converse(r) == {\ttlbrace}z. w\isasymin{}r, {\isasymexists}x y. w=<x,y> & z=<y,x>{\ttrbrace}

\tdx{domain_def}:   domain(r)   == {\ttlbrace}x. w \isasymin r, {\isasymexists}y. w=<x,y>{\ttrbrace}

\tdx{range_def}:    range(r)    == domain(converse(r))

\tdx{field_def}:    field(r)    == domain(r) \isasymunion range(r)

\tdx{image_def}:    r `` A      == {\ttlbrace}y\isasymin{}range(r) . {\isasymexists}x \isasymin A. <x,y> \isasymin 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 \isasymin A{\ttrbrace}

\tdx{apply_def}: f`a         == THE y. <a,y> \isasymin f

\tdx{Pi_def}: Pi(A,B) == {\ttlbrace}f\isasymin{}Pow(Sigma(A,B)). {\isasymforall}x\isasymin{}A. \isasymexists!y. <x,y>\isasymin{}f{\ttrbrace}

\tdx{restrict_def}:  restrict(f,A) == lam x \isasymin A. f`x

\subcaption{Functions and general product}

\end{alltt*}

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

The traditional replacement axiom asserts

\[ y \in \isa{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 \isa{Replace}(A,P)$ if and only if there is some~$x$ such that

$P(x,-)$ holds uniquely for~$y$.  Because the equivalence is unconditional,

\isa{Replace} is much easier to use than \isa{PrimReplace}; it defines the

same set, if $P(x,y)$ is single-valued.  The nice syntax for replacement

expands to \isa{Replace}.

Other consequences of replacement include replacement for 

meta-level functions

(\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 \isa{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 $\isa{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.thy

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{ballI}:     [| !!x. x\isasymin{}A ==> P(x) |] ==> {\isasymforall}x\isasymin{}A. P(x)

\tdx{bspec}:     [| {\isasymforall}x\isasymin{}A. P(x);  x\isasymin{}A |] ==> P(x)

\tdx{ballE}:     [| {\isasymforall}x\isasymin{}A. P(x);  P(x) ==> Q;  x \isasymnotin A ==> Q |] ==> Q

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

             ({\isasymforall}x\isasymin{}A. P(x)) <-> ({\isasymforall}x\isasymin{}A'. P'(x))

\tdx{bexI}:      [| P(x);  x\isasymin{}A |] ==> {\isasymexists}x\isasymin{}A. P(x)

\tdx{bexCI}:     [| {\isasymforall}x\isasymin{}A. ~P(x) ==> P(a);  a\isasymin{}A |] ==> {\isasymexists}x\isasymin{}A. P(x)

\tdx{bexE}:      [| {\isasymexists}x\isasymin{}A. P(x);  !!x. [| x\isasymin{}A; P(x) |] ==> Q |] ==> Q

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

             ({\isasymexists}x\isasymin{}A. P(x)) <-> ({\isasymexists}x\isasymin{}A'. P'(x))

\subcaption{Bounded quantifiers}

\tdx{subsetI}:     (!!x. x \isasymin A ==> x \isasymin B) ==> A \isasymsubseteq B

\tdx{subsetD}:     [| A \isasymsubseteq B;  c \isasymin A |] ==> c \isasymin B

\tdx{subsetCE}:    [| A \isasymsubseteq B;  c \isasymnotin A ==> P;  c \isasymin B ==> P |] ==> P

\tdx{subset_refl}:  A \isasymsubseteq A

\tdx{subset_trans}: [| A \isasymsubseteq B;  B \isasymsubseteq C |] ==> A \isasymsubseteq C

\tdx{equalityI}:   [| A \isasymsubseteq B;  B \isasymsubseteq A |] ==> A = B

\tdx{equalityD1}:  A = B ==> A \isasymsubseteq B

\tdx{equalityD2}:  A = B ==> B \isasymsubseteq A

\tdx{equalityE}:   [| A = B;  [| A \isasymsubseteq B; B \isasymsubseteq A |] ==> P |]  ==>  P

\subcaption{Subsets and extensionality}

\tdx{emptyE}:        a \isasymin 0 ==> P

\tdx{empty_subsetI}:  0 \isasymsubseteq A

\tdx{equals0I}:      [| !!y. y \isasymin A ==> False |] ==> A=0

\tdx{equals0D}:      [| A=0;  a \isasymin A |] ==> P

\tdx{PowI}:          A \isasymsubseteq B ==> A \isasymin Pow(B)

\tdx{PowD}:          A \isasymin Pow(B)  ==>  A \isasymsubseteq B

\subcaption{The empty set; power sets}

\end{alltt*}

\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 \isa{PrimReplace} would be.  The principle of

separation is proved explicitly, although most proofs should use the

natural deduction rules for \isa{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.  

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{alltt*}\isastyleminor

\tdx{ReplaceI}:   [| x\isasymin{}A;  P(x,b);  !!y. P(x,y) ==> y=b |] ==> 

            b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace}

\tdx{ReplaceE}:   [| b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace};  

               !!x. [| x\isasymin{}A; P(x,b); {\isasymforall}y. P(x,y)-->y=b |] ==> R 

            |] ==> R

\tdx{RepFunI}:    [| a\isasymin{}A |] ==> f(a)\isasymin{}{\ttlbrace}f(x). x\isasymin{}A{\ttrbrace}

\tdx{RepFunE}:    [| b\isasymin{}{\ttlbrace}f(x). x\isasymin{}A{\ttrbrace};  

                !!x.[| x\isasymin{}A;  b=f(x) |] ==> P |] ==> P

\tdx{separation}:  a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} <-> a\isasymin{}A & P(a)

\tdx{CollectI}:    [| a\isasymin{}A;  P(a) |] ==> a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace}

\tdx{CollectE}:    [| a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace};  [| a\isasymin{}A; P(a) |] ==> R |] ==> R

\tdx{CollectD1}:   a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} ==> a\isasymin{}A

\tdx{CollectD2}:   a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} ==> P(a)

\end{alltt*}

\caption{Replacement and separation} \label{zf-lemmas2}

\end{figure}

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{UnionI}: [| B\isasymin{}C;  A\isasymin{}B |] ==> A\isasymin{}Union(C)

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

\tdx{InterI}: [| !!x. x\isasymin{}C ==> A\isasymin{}x;  c\isasymin{}C |] ==> A\isasymin{}Inter(C)

\tdx{InterD}: [| A\isasymin{}Inter(C);  B\isasymin{}C |] ==> A\isasymin{}B

\tdx{InterE}: [| A\isasymin{}Inter(C);  A\isasymin{}B ==> R;  B \isasymnotin C ==> R |] ==> R

\tdx{UN_I}:   [| a\isasymin{}A;  b\isasymin{}B(a) |] ==> b\isasymin{}({\isasymUnion}x\isasymin{}A. B(x))

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

           |] ==> R

\tdx{INT_I}:  [| !!x. x\isasymin{}A ==> b\isasymin{}B(x);  a\isasymin{}A |] ==> b\isasymin{}({\isasymInter}x\isasymin{}A. B(x))

\tdx{INT_E}:  [| b\isasymin{}({\isasymInter}x\isasymin{}A. B(x));  a\isasymin{}A |] ==> b\isasymin{}B(a)

\end{alltt*}

\caption{General union and intersection} \label{zf-lemmas3}

\end{figure}

%%% upair.thy

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{pairing}:   a\isasymin{}Upair(b,c) <-> (a=b | a=c)

\tdx{UpairI1}:   a\isasymin{}Upair(a,b)

\tdx{UpairI2}:   b\isasymin{}Upair(a,b)

\tdx{UpairE}:    [| a\isasymin{}Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P

\end{alltt*}

\caption{Unordered pairs} \label{zf-upair1}

\end{figure}

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{UnI1}:      c\isasymin{}A ==> c\isasymin{}A \isasymunion B

\tdx{UnI2}:      c\isasymin{}B ==> c\isasymin{}A \isasymunion B

\tdx{UnCI}:      (c \isasymnotin B ==> c\isasymin{}A) ==> c\isasymin{}A \isasymunion B

\tdx{UnE}:       [| c\isasymin{}A \isasymunion B;  c\isasymin{}A ==> P;  c\isasymin{}B ==> P |] ==> P

\tdx{IntI}:      [| c\isasymin{}A;  c\isasymin{}B |] ==> c\isasymin{}A \isasyminter B

\tdx{IntD1}:     c\isasymin{}A \isasyminter B ==> c\isasymin{}A

\tdx{IntD2}:     c\isasymin{}A \isasyminter B ==> c\isasymin{}B

\tdx{IntE}:      [| c\isasymin{}A \isasyminter B;  [| c\isasymin{}A; c\isasymin{}B |] ==> P |] ==> P

\tdx{DiffI}:     [| c\isasymin{}A;  c \isasymnotin B |] ==> c\isasymin{}A - B

\tdx{DiffD1}:    c\isasymin{}A - B ==> c\isasymin{}A

\tdx{DiffD2}:    c\isasymin{}A - B ==> c  \isasymnotin  B

\tdx{DiffE}:     [| c\isasymin{}A - B;  [| c\isasymin{}A; c \isasymnotin B |] ==> P |] ==> P

\end{alltt*}

\caption{Union, intersection, difference} \label{zf-Un}

\end{figure}

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{consI1}:    a\isasymin{}cons(a,B)

\tdx{consI2}:    a\isasymin{}B ==> a\isasymin{}cons(b,B)

\tdx{consCI}:    (a \isasymnotin B ==> a=b) ==> a\isasymin{}cons(b,B)

\tdx{consE}:     [| a\isasymin{}cons(b,A);  a=b ==> P;  a\isasymin{}A ==> P |] ==> P

\tdx{singletonI}:  a\isasymin{}{\ttlbrace}a{\ttrbrace}

\tdx{singletonE}:  [| a\isasymin{}{\ttlbrace}b{\ttrbrace}; a=b ==> P |] ==> P

\end{alltt*}

\caption{Finite and singleton sets} \label{zf-upair2}

\end{figure}

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{succI1}:    i\isasymin{}succ(i)

\tdx{succI2}:    i\isasymin{}j ==> i\isasymin{}succ(j)

\tdx{succCI}:    (i \isasymnotin j ==> i=j) ==> i\isasymin{}succ(j)

\tdx{succE}:     [| i\isasymin{}succ(j);  i=j ==> P;  i\isasymin{}j ==> P |] ==> P

\tdx{succ_neq_0}:  [| succ(n)=0 |] ==> P

\tdx{succ_inject}: succ(m) = succ(n) ==> m=n

\end{alltt*}

\caption{The successor function} \label{zf-succ}

\end{figure}

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{the_equality}: [| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x))=a

\tdx{theI}:         \isasymexists! x. P(x) ==> P(THE x. P(x))

\tdx{if_P}:          P ==> (if P then a else b) = a

\tdx{if_not_P}:     ~P ==> (if P then a else b) = b

\tdx{mem_asym}:     [| a\isasymin{}b;  b\isasymin{}a |] ==> P

\tdx{mem_irrefl}:   a\isasymin{}a ==> P

\end{alltt*}

\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 \isa{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~\isa{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~\isa{cons}.  The proof that 

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

%%% subset.thy?

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{Union_upper}:    B\isasymin{}A ==> B \isasymsubseteq Union(A)

\tdx{Union_least}:    [| !!x. x\isasymin{}A ==> x \isasymsubseteq C |] ==> Union(A) \isasymsubseteq C

\tdx{Inter_lower}:    B\isasymin{}A ==> Inter(A) \isasymsubseteq B

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

\tdx{Un_upper1}:      A \isasymsubseteq A \isasymunion B

\tdx{Un_upper2}:      B \isasymsubseteq A \isasymunion B

\tdx{Un_least}:       [| A \isasymsubseteq C;  B \isasymsubseteq C |] ==> A \isasymunion B \isasymsubseteq C

\tdx{Int_lower1}:     A \isasyminter B \isasymsubseteq A

\tdx{Int_lower2}:     A \isasyminter B \isasymsubseteq B

\tdx{Int_greatest}:   [| C \isasymsubseteq A;  C \isasymsubseteq B |] ==> C \isasymsubseteq A \isasyminter B

\tdx{Diff_subset}:    A-B \isasymsubseteq A

\tdx{Diff_contains}:  [| C \isasymsubseteq A;  C \isasyminter B = 0 |] ==> C \isasymsubseteq A-B

\tdx{Collect_subset}: Collect(A,P) \isasymsubseteq A

\end{alltt*}

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

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 

${\isa{Pow}(A)\cap \isa{Pow}(B)}= \isa{Pow}(A\cap B)$.

%%% pair.thy

\begin{figure}

\begin{alltt*}\isastyleminor

\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\isasymin{}A;  b\isasymin{}B(a) |] ==> <a,b>\isasymin{}Sigma(A,B)

\tdx{SigmaE}:     [| c\isasymin{}Sigma(A,B);  

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

\tdx{SigmaE2}:    [| <a,b>\isasymin{}Sigma(A,B);    

                [| a\isasymin{}A;  b\isasymin{}B(a) |] ==> P   |] ==> P

\end{alltt*}

\caption{Ordered pairs; projections; general sums} \label{zf-pair}

\end{figure}

\subsection{Ordered pairs} \label{sec:pairs}

Figure~\ref{zf-pair} presents the rules governing ordered pairs,

projections and general sums --- in particular, 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 \isa{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 \isa{split(\%$x$ $y$.\ $t$)}

\end{center}

Nested patterns are translated recursively:

{\tt\%<$x$,$y$,$z$>. $t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>. $t$} $\leadsto$

\isa{split(\%$x$.\%<$y$,$z$>. $t$)} $\leadsto$ \isa{split(\%$x$. split(\%$y$

  $z$.\ $t$))}.  The reverse translation is performed upon printing.

\begin{warn}

  The translation between patterns and \isa{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 \isa{(\%<x,y>.<y,x>)<a,b>} requires the theorem \isa{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.  Here are some important examples:

\begin{description}

\item[Let:] \isa{let {\it pattern} = $t$ in $u$}

\item[Choice:] \isa{THE~{\it pattern}~.~$P$}

\item[Set operations:] \isa{\isasymUnion~{\it pattern}:$A$.~$B$}

\item[Comprehension:] \isa{{\ttlbrace}~{\it pattern}:$A$~.~$P$~{\ttrbrace}}

\end{description}

%%% domrange.thy?

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{domainI}:     <a,b>\isasymin{}r ==> a\isasymin{}domain(r)

\tdx{domainE}:     [| a\isasymin{}domain(r); !!y. <a,y>\isasymin{}r ==> P |] ==> P

\tdx{domain_subset}: domain(Sigma(A,B)) \isasymsubseteq A

\tdx{rangeI}:      <a,b>\isasymin{}r ==> b\isasymin{}range(r)

\tdx{rangeE}:      [| b\isasymin{}range(r); !!x. <x,b>\isasymin{}r ==> P |] ==> P

\tdx{range_subset}: range(A*B) \isasymsubseteq B

\tdx{fieldI1}:     <a,b>\isasymin{}r ==> a\isasymin{}field(r)

\tdx{fieldI2}:     <a,b>\isasymin{}r ==> b\isasymin{}field(r)

\tdx{fieldCI}:     (<c,a> \isasymnotin r ==> <a,b>\isasymin{}r) ==> a\isasymin{}field(r)

\tdx{fieldE}:      [| a\isasymin{}field(r); 

                !!x. <a,x>\isasymin{}r ==> P; 

                !!x. <x,a>\isasymin{}r ==> P      

             |] ==> P

\tdx{field_subset}:  field(A*A) \isasymsubseteq A

\end{alltt*}

\caption{Domain, range and field of a relation} \label{zf-domrange}

\end{figure}

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{imageI}:      [| <a,b>\isasymin{}r; a\isasymin{}A |] ==> b\isasymin{}r``A

\tdx{imageE}:      [| b\isasymin{}r``A; !!x.[| <x,b>\isasymin{}r; x\isasymin{}A |] ==> P |] ==> P

\tdx{vimageI}:     [| <a,b>\isasymin{}r; b\isasymin{}B |] ==> a\isasymin{}r-``B

\tdx{vimageE}:     [| a\isasymin{}r-``B; !!x.[| <a,x>\isasymin{}r;  x\isasymin{}B |] ==> P |] ==> P

\end{alltt*}

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

%%% func.thy

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{fun_is_rel}:     f\isasymin{}Pi(A,B) ==> f \isasymsubseteq Sigma(A,B)

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

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

\tdx{apply_type}:     [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> f`a\isasymin{}B(a)

\tdx{apply_Pair}:     [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> <a,f`a>\isasymin{}f

\tdx{apply_iff}:      f\isasymin{}Pi(A,B) ==> <a,b>\isasymin{}f <-> a\isasymin{}A & f`a = b

\tdx{fun_extension}:  [| f\isasymin{}Pi(A,B); g\isasymin{}Pi(A,D);

                   !!x. x\isasymin{}A ==> f`x = g`x     |] ==> f=g

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

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

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

\tdx{domain_of_fun}:  f\isasymin{}Pi(A,B) ==> domain(f)=A

\tdx{range_of_fun}:   f\isasymin{}Pi(A,B) ==> f\isasymin{}A->range(f)

\tdx{restrict}:       a\isasymin{}A ==> restrict(f,A) ` a = f`a

\tdx{restrict_type}:  [| !!x. x\isasymin{}A ==> f`x\isasymin{}B(x) |] ==> 

                restrict(f,A)\isasymin{}Pi(A,B)

\end{alltt*}

\caption{Functions} \label{zf-func1}

\end{figure}

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{lamI}:     a\isasymin{}A ==> <a,b(a)>\isasymin{}(lam x\isasymin{}A. b(x))

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

          |] ==>  P

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

\tdx{beta}:     a\isasymin{}A ==> (lam x\isasymin{}A. b(x)) ` a = b(a)

\tdx{eta}:      f\isasymin{}Pi(A,B) ==> (lam x\isasymin{}A. f`x) = f

\end{alltt*}

\caption{$\lambda$-abstraction} \label{zf-lam}

\end{figure}

\begin{figure}

\begin{alltt*}\isastyleminor

\tdx{fun_empty}:           0\isasymin{}0->0

\tdx{fun_single}:          {\ttlbrace}<a,b>{\ttrbrace}\isasymin{}{\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace}

\tdx{fun_disjoint_Un}:     [| f\isasymin{}A->B; g\isasymin{}C->D; A \isasyminter C = 0  |] ==>  

                     (f \isasymunion g)\isasymin{}(A \isasymunion C) -> (B \isasymunion D)

\tdx{fun_disjoint_apply1}: [| a\isasymin{}A; f\isasymin{}A->B; g\isasymin{}C->D;  A\isasyminter{}C = 0 |] ==>  

                     (f \isasymunion g)`a = f`a

\tdx{fun_disjoint_apply2}: [| c\isasymin{}C; f\isasymin{}A->B; g\isasymin{}C->D;  A\isasyminter{}C = 0 |] ==>  

                     (f \isasymunion g)`c = g`c

\end{alltt*}

\caption{Constructing functions from smaller sets} \label{zf-func2}

\end{figure}

\subsection{Functions}

Functions, represented by graphs, are notoriously difficult to reason

about.  The ZF theory provides many derived 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=\isa{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{alltt*}\isastyleminor

\tdx{Int_absorb}:        A \isasyminter A = A

\tdx{Int_commute}:       A \isasyminter B = B \isasyminter A

\tdx{Int_assoc}:         (A \isasyminter B) \isasyminter C  =  A \isasyminter (B \isasyminter C)

\tdx{Int_Un_distrib}:    (A \isasymunion B) \isasyminter C  =  (A \isasyminter C) \isasymunion (B \isasyminter C)

\tdx{Un_absorb}:         A \isasymunion A = A

\tdx{Un_commute}:        A \isasymunion B = B \isasymunion A

\tdx{Un_assoc}:          (A \isasymunion B) \isasymunion C  =  A \isasymunion (B \isasymunion C)

\tdx{Un_Int_distrib}:    (A \isasyminter B) \isasymunion C  =  (A \isasymunion C) \isasyminter (B \isasymunion C)

\tdx{Diff_cancel}:       A-A = 0

\tdx{Diff_disjoint}:     A \isasyminter (B-A) = 0

\tdx{Diff_partition}:    A \isasymsubseteq B ==> A \isasymunion (B-A) = B

\tdx{double_complement}: [| A \isasymsubseteq B; B \isasymsubseteq C |] ==> (B - (C-A)) = A

\tdx{Diff_Un}:           A - (B \isasymunion C) = (A-B) \isasyminter (A-C)

\tdx{Diff_Int}:          A - (B \isasyminter C) = (A-B) \isasymunion (A-C)

\tdx{Union_Un_distrib}:  Union(A \isasymunion B) = Union(A) \isasymunion Union(B)

\tdx{Inter_Un_distrib}:  [| a \isasymin A;  b \isasymin B |] ==> 

                   Inter(A \isasymunion B) = Inter(A) \isasyminter Inter(B)

\tdx{Int_Union_RepFun}:  A \isasyminter Union(B) = ({\isasymUnion}C \isasymin B. A \isasyminter C)

\tdx{Un_Inter_RepFun}:   b \isasymin B ==> 

                   A \isasymunion Inter(B) = ({\isasymInter}C \isasymin B. A \isasymunion C)

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

                   (SUM x \isasymin A. C(x)) \isasymunion (SUM x \isasymin B. C(x))

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

                   (SUM x \isasymin C. A(x)) \isasymunion (SUM x \isasymin C. B(x))

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

                   (SUM x \isasymin A. C(x)) \isasyminter (SUM x \isasymin B. C(x))