104

1 
%% $Id$


2 
%%%See grant/bra/Lib/ZF.tex for lfp figure

287

3 
\chapter{ZermeloFraenkel Set Theory}

104

4 
The directory~\ttindexbold{ZF} implements ZermeloFraenkel set


5 
theory~\cite{halmos60,suppes72} as an extension of~\ttindex{FOL}, classical


6 
firstorder logic. The theory includes a collection of derived natural


7 
deduction rules, for use with Isabelle's classical reasoning module. Much


8 
of it is based on the work of No\"el~\cite{noel}. The theory has the {\ML}


9 
identifier \ttindexbold{ZF.thy}. However, many further theories


10 
are defined, introducing the natural numbers, etc.


11 


12 
A tremendous amount of set theory has been formally developed, including


13 
the basic properties of relations, functions and ordinals. Significant


14 
results have been proved, such as the Schr\"oderBernstein Theorem and the


15 
Recursion Theorem. General methods have been developed for solving


16 
recursion equations over monotonic functors; these have been applied to


17 
yield constructions of lists and trees. Thus, we may even regard set


18 
theory as a computational logic. It admits recursive definitions of

111

19 
functions and types. It has much in common with MartinL\"of type theory,

104

20 
although of course it is classical.


21 


22 
Because {\ZF} is an extension of {\FOL}, it provides the same packages,


23 
namely \ttindex{hyp_subst_tac}, the simplifier, and the classical reasoning


24 
module. The main simplification set is called \ttindexbold{ZF_ss}.


25 
Several classical rule sets are defined, including \ttindexbold{lemmas_cs},


26 
\ttindexbold{upair_cs} and~\ttindexbold{ZF_cs}. See the files on directory


27 
{\tt ZF} for details.


28 

111

29 
Isabelle/ZF now has a flexible package for handling inductive definitions,


30 
such as inference systems, and datatype definitions, such as lists and


31 
trees. Moreover it also handles coinductive definitions, such as


32 
bisimulation relations, and codatatype definitions, such as streams. A


33 
recent paper describes the package~\cite{paulsonfixedpt}.


34 


35 
Recent reports describe Isabelle/ZF less formally than this


36 
chapter~\cite{paulsonsetI,paulsonsetII}. Isabelle/ZF employs a novel


37 
treatment of nonwellfounded data structures within the standard ZF axioms


38 
including the Axiom of Foundation, but no report describes this treatment.


39 

104

40 


41 
\section{Which version of axiomatic set theory?}


42 
Resolution theorem provers can work in set theory, using the


43 
BernaysG\"odel axiom system~(BG) because it is


44 
finite~\cite{boyer86,quaife92}. {\ZF} does not have a finite axiom system


45 
(because of its Axiom Scheme of Replacement) and is therefore unsuitable


46 
for classical resolution. Since Isabelle has no difficulty with axiom


47 
schemes, we may adopt either axiom system.


48 


49 
These two theories differ in their treatment of {\bf classes}, which are


50 
collections that are ``too big'' to be sets. The class of all sets,~$V$,


51 
cannot be a set without admitting Russell's Paradox. In BG, both classes


52 
and sets are individuals; $x\in V$ expresses that $x$ is a set. In {\ZF}, all


53 
variables denote sets; classes are identified with unary predicates. The


54 
two systems define essentially the same sets and classes, with similar


55 
properties. In particular, a class cannot belong to another class (let


56 
alone a set).


57 


58 
Modern set theorists tend to prefer {\ZF} because they are mainly concerned


59 
with sets, rather than classes. BG requires tiresome proofs that various


60 
collections are sets; for instance, showing $x\in\{x\}$ requires showing that


61 
$x$ is a set. {\ZF} does not have this problem.


62 


63 


64 
\begin{figure}


65 
\begin{center}


66 
\begin{tabular}{rrr}

111

67 
\it name &\it metatype & \it description \\


68 
\idx{0} & $i$ & empty set\\


69 
\idx{cons} & $[i,i]\To i$ & finite set constructor\\


70 
\idx{Upair} & $[i,i]\To i$ & unordered pairing\\


71 
\idx{Pair} & $[i,i]\To i$ & ordered pairing\\


72 
\idx{Inf} & $i$ & infinite set\\


73 
\idx{Pow} & $i\To i$ & powerset\\


74 
\idx{Union} \idx{Inter} & $i\To i$ & set union/intersection \\


75 
\idx{split} & $[[i,i]\To i, i] \To i$ & generalized projection\\


76 
\idx{fst} \idx{snd} & $i\To i$ & projections\\


77 
\idx{converse}& $i\To i$ & converse of a relation\\


78 
\idx{succ} & $i\To i$ & successor\\


79 
\idx{Collect} & $[i,i\To o]\To i$ & separation\\


80 
\idx{Replace} & $[i, [i,i]\To o] \To i$ & replacement\\


81 
\idx{PrimReplace} & $[i, [i,i]\To o] \To i$ & primitive replacement\\


82 
\idx{RepFun} & $[i, i\To i] \To i$ & functional replacement\\


83 
\idx{Pi} \idx{Sigma} & $[i,i\To i]\To i$ & general product/sum\\


84 
\idx{domain} & $i\To i$ & domain of a relation\\


85 
\idx{range} & $i\To i$ & range of a relation\\


86 
\idx{field} & $i\To i$ & field of a relation\\


87 
\idx{Lambda} & $[i, i\To i]\To i$ & $\lambda$abstraction\\


88 
\idx{restrict}& $[i, i] \To i$ & restriction of a function\\


89 
\idx{The} & $[i\To o]\To i$ & definite description\\


90 
\idx{if} & $[o,i,i]\To i$ & conditional\\


91 
\idx{Ball} \idx{Bex} & $[i, i\To o]\To o$ & bounded quantifiers

104

92 
\end{tabular}


93 
\end{center}


94 
\subcaption{Constants}


95 


96 
\begin{center}


97 
\indexbold{*"`"`}


98 
\indexbold{*""`"`}


99 
\indexbold{*"`}


100 
\indexbold{*"}


101 
\indexbold{*":}


102 
\indexbold{*"<"=}


103 
\begin{tabular}{rrrr}


104 
\it symbol & \it metatype & \it precedence & \it description \\

111

105 
\tt `` & $[i,i]\To i$ & Left 90 & image \\


106 
\tt `` & $[i,i]\To i$ & Left 90 & inverse image \\


107 
\tt ` & $[i,i]\To i$ & Left 90 & application \\


108 
\idx{Int} & $[i,i]\To i$ & Left 70 & intersection ($\inter$) \\


109 
\idx{Un} & $[i,i]\To i$ & Left 65 & union ($\union$) \\


110 
\tt  & $[i,i]\To i$ & Left 65 & set difference ($$) \\[1ex]


111 
\tt: & $[i,i]\To o$ & Left 50 & membership ($\in$) \\


112 
\tt <= & $[i,i]\To o$ & Left 50 & subset ($\subseteq$)

104

113 
\end{tabular}


114 
\end{center}


115 
\subcaption{Infixes}


116 
\caption{Constants of {\ZF}} \label{ZFconstants}


117 
\end{figure}


118 


119 


120 
\section{The syntax of set theory}


121 
The language of set theory, as studied by logicians, has no constants. The


122 
traditional axioms merely assert the existence of empty sets, unions,


123 
powersets, etc.; this would be intolerable for practical reasoning. The


124 
Isabelle theory declares constants for primitive sets. It also extends


125 
{\tt FOL} with additional syntax for finite sets, ordered pairs,


126 
comprehension, general union/intersection, general sums/products, and


127 
bounded quantifiers. In most other respects, Isabelle implements precisely


128 
ZermeloFraenkel set theory.


129 


130 
Figure~\ref{ZFconstants} lists the constants and infixes of~\ZF, while


131 
Figure~\ref{ZFtrans} presents the syntax translations. Finally,


132 
Figure~\ref{ZFsyntax} presents the full grammar for set theory, including


133 
the constructs of \FOL.


134 


135 
Set theory does not use polymorphism. All terms in {\ZF} have type~{\it


136 
i}, which is the type of individuals and lies in class {\it logic}.


137 
The type of firstorder formulae,


138 
remember, is~{\it o}.


139 


140 
Infix operators include union and intersection ($A\union B$ and $A\inter


141 
B$), and the subset and membership relations. Note that $a$\verb~:$b$ is


142 
translated to \verb~($a$:$b$\verb). The union and intersection


143 
operators ($\bigcup A$ and $\bigcap A$) form the union or intersection of a


144 
set of sets; $\bigcup A$ means the same as $\bigcup@{x\in A}x$. Of these


145 
operators, only $\bigcup A$ is primitive.


146 


147 
The constant \ttindexbold{Upair} constructs unordered pairs; thus {\tt


148 
Upair($A$,$B$)} denotes the set~$\{A,B\}$ and {\tt Upair($A$,$A$)} denotes


149 
the singleton~$\{A\}$. As usual in {\ZF}, general union is used to define


150 
binary union. The Isabelle version goes on to define the constant


151 
\ttindexbold{cons}:


152 
\begin{eqnarray*}

111

153 
A\cup B & \equiv & \bigcup({\tt Upair}(A,B)) \\


154 
{\tt cons}(a,B) & \equiv & {\tt Upair}(a,a) \union B

104

155 
\end{eqnarray*}


156 
The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the


157 
obvious manner using~{\tt cons} and~$\emptyset$ (the empty set):


158 
\begin{eqnarray*}


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


160 
\end{eqnarray*}


161 


162 
The constant \ttindexbold{Pair} constructs ordered pairs, as in {\tt


163 
Pair($a$,$b$)}. Ordered pairs may also be written within angle brackets,

111

164 
as {\tt<$a$,$b$>}. The $n$tuple {\tt<$a@1$,\ldots,$a@{n1}$,$a@n$>}

287

165 
abbreviates the nest of pairs


166 
\begin{quote}


167 
\tt Pair($a@1$,\ldots,Pair($a@{n1}$,$a@n$)\ldots).


168 
\end{quote}

104

169 


170 
In {\ZF}, a function is a set of pairs. A {\ZF} function~$f$ is simply an


171 
individual as far as Isabelle is concerned: its Isabelle type is~$i$, not


172 
say $i\To i$. The infix operator~{\tt`} denotes the application of a


173 
function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$. The


174 
syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt``}A$.


175 


176 


177 
\begin{figure}


178 
\indexbold{*"">}


179 
\indexbold{*"*}

287

180 
\begin{center} \footnotesize\tt\frenchspacing

104

181 
\begin{tabular}{rrr}

111

182 
\it external & \it internal & \it description \\

104

183 
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\


184 
\{$a@1$, $\ldots$, $a@n$\} & cons($a@1$,$\cdots$,cons($a@n$,0)) &


185 
\rm finite set \\

111

186 
<$a@1$, $\ldots$, $a@{n1}$, $a@n$> &


187 
Pair($a@1$,\ldots,Pair($a@{n1}$,$a@n$)\ldots) &


188 
\rm ordered $n$tuple \\


189 
\{$x$:$A . P[x]$\} & Collect($A$,$\lambda x.P[x]$) &

104

190 
\rm separation \\


191 
\{$y . x$:$A$, $Q[x,y]$\} & Replace($A$,$\lambda x\,y.Q[x,y]$) &


192 
\rm replacement \\


193 
\{$b[x] . x$:$A$\} & RepFun($A$,$\lambda x.b[x]$) &


194 
\rm functional replacement \\

111

195 
\idx{INT} $x$:$A . B[x]$ & Inter(\{$B[x] . x$:$A$\}) &


196 
\rm general intersection \\


197 
\idx{UN} $x$:$A . B[x]$ & Union(\{$B[x] . x$:$A$\}) &


198 
\rm general union \\


199 
\idx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x.B[x]$) &


200 
\rm general product \\


201 
\idx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x.B[x]$) &


202 
\rm general sum \\


203 
$A$ > $B$ & Pi($A$,$\lambda x.B$) &


204 
\rm function space \\


205 
$A$ * $B$ & Sigma($A$,$\lambda x.B$) &


206 
\rm binary product \\


207 
\idx{THE} $x . P[x]$ & The($\lambda x.P[x]$) &


208 
\rm definite description \\


209 
\idx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x.b[x]$) &


210 
\rm $\lambda$abstraction\\[1ex]


211 
\idx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x.P[x]$) &


212 
\rm bounded $\forall$ \\


213 
\idx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x.P[x]$) &


214 
\rm bounded $\exists$

104

215 
\end{tabular}


216 
\end{center}


217 
\caption{Translations for {\ZF}} \label{ZFtrans}


218 
\end{figure}


219 


220 


221 
\begin{figure}


222 
\dquotes


223 
\[\begin{array}{rcl}


224 
term & = & \hbox{expression of type~$i$} \\

111

225 
&  & "\{ " term\; ("," term)^* " \}" \\


226 
&  & "< " term ", " term " >" \\


227 
&  & "\{ " id ":" term " . " formula " \}" \\


228 
&  & "\{ " id " . " id ":" term "," formula " \}" \\


229 
&  & "\{ " term " . " id ":" term " \}" \\


230 
&  & term " `` " term \\


231 
&  & term " `` " term \\


232 
&  & term " ` " term \\


233 
&  & term " * " term \\


234 
&  & term " Int " term \\


235 
&  & term " Un " term \\


236 
&  & term "  " term \\


237 
&  & term " > " term \\


238 
&  & "THE~~" id " . " formula\\


239 
&  & "lam~~" id ":" term " . " term \\


240 
&  & "INT~~" id ":" term " . " term \\


241 
&  & "UN~~~" id ":" term " . " term \\


242 
&  & "PROD~" id ":" term " . " term \\


243 
&  & "SUM~~" id ":" term " . " term \\[2ex]

104

244 
formula & = & \hbox{expression of type~$o$} \\

111

245 
&  & term " : " term \\


246 
&  & term " <= " term \\


247 
&  & term " = " term \\


248 
&  & "\ttilde\ " formula \\


249 
&  & formula " \& " formula \\


250 
&  & formula "  " formula \\


251 
&  & formula " > " formula \\


252 
&  & formula " <> " formula \\


253 
&  & "ALL " id ":" term " . " formula \\


254 
&  & "EX~~" id ":" term " . " formula \\


255 
&  & "ALL~" id~id^* " . " formula \\


256 
&  & "EX~~" id~id^* " . " formula \\


257 
&  & "EX!~" id~id^* " . " formula

104

258 
\end{array}


259 
\]


260 
\caption{Full grammar for {\ZF}} \label{ZFsyntax}


261 
\end{figure}


262 


263 


264 
\section{Binding operators}


265 
The constant \ttindexbold{Collect} constructs sets by the principle of {\bf


266 
separation}. The syntax for separation is \hbox{\tt\{$x$:$A$.$P[x]$\}},


267 
where $P[x]$ is a formula that may contain free occurrences of~$x$. It


268 
abbreviates the set {\tt Collect($A$,$\lambda x.P$[x])}, which consists of


269 
all $x\in A$ that satisfy~$P[x]$. Note that {\tt Collect} is an


270 
unfortunate choice of name: some set theories adopt a setformation


271 
principle, related to replacement, called collection.


272 


273 
The constant \ttindexbold{Replace} constructs sets by the principle of {\bf


274 
replacement}. The syntax for replacement is


275 
\hbox{\tt\{$y$.$x$:$A$,$Q[x,y]$\}}. It denotes the set {\tt


276 
Replace($A$,$\lambda x\,y.Q$[x,y])} consisting of all $y$ such that there


277 
exists $x\in A$ satisfying~$Q[x,y]$. The Replacement Axiom has the


278 
condition that $Q$ must be singlevalued over~$A$: for all~$x\in A$ there


279 
exists at most one $y$ satisfying~$Q[x,y]$. A singlevalued binary


280 
predicate is also called a {\bf class function}.


281 


282 
The constant \ttindexbold{RepFun} expresses a special case of replacement,


283 
where $Q[x,y]$ has the form $y=b[x]$. Such a $Q$ is trivially


284 
singlevalued, since it is just the graph of the metalevel

287

285 
function~$\lambda x.b[x]$. The resulting set consists of all $b[x]$


286 
for~$x\in A$. This is analogous to the \ML{} functional {\tt map}, since


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


288 
\hbox{\tt\{$b[x]$.$x$:$A$\}}, which expands to {\tt RepFun($A$,$\lambda


289 
x.b[x]$)}.

104

290 

287

291 


292 
\indexbold{*INT}\indexbold{*UN}


293 
General unions and intersections of indexed


294 
families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$,


295 
are written \hbox{\tt UN $x$:$A$.$B[x]$} and \hbox{\tt INT $x$:$A$.$B[x]$}.


296 
Their meaning is expressed using {\tt RepFun} as

104

297 
\[ \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad


298 
\bigcap(\{B[x]. x\in A\}).


299 
\]


300 
General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be


301 
constructed in set theory, where $B[x]$ is a family of sets over~$A$. They


302 
have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set.


303 
This is similar to the situation in Constructive Type Theory (set theory


304 
has ``dependent sets'') and calls for similar syntactic conventions. The


305 
constants~\ttindexbold{Sigma} and~\ttindexbold{Pi} construct general sums and


306 
products. Instead of {\tt Sigma($A$,$B$)} and {\tt Pi($A$,$B$)} we may write


307 
\hbox{\tt SUM $x$:$A$.$B[x]$} and \hbox{\tt PROD $x$:$A$.$B[x]$}.


308 
\indexbold{*SUM}\indexbold{*PROD}%


309 
The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$>$B$} abbreviate


310 
general sums and products over a constant family.\footnote{Unlike normal


311 
infix operators, {\tt*} and {\tt>} merely define abbreviations; there are


312 
no constants~{\tt op~*} and~\hbox{\tt op~>}.} Isabelle accepts these


313 
abbreviations in parsing and uses them whenever possible for printing.


314 


315 
\indexbold{*THE}


316 
As mentioned above, whenever the axioms assert the existence and uniqueness


317 
of a set, Isabelle's set theory declares a constant for that set. These


318 
constants can express the {\bf definite description} operator~$\iota


319 
x.P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists.


320 
Since all terms in {\ZF} denote something, a description is always


321 
meaningful, but we do not know its value unless $P[x]$ defines it uniquely.


322 
Using the constant~\ttindexbold{The}, we may write descriptions as {\tt


323 
The($\lambda x.P[x]$)} or use the syntax \hbox{\tt THE $x$.$P[x]$}.


324 


325 
\indexbold{*lam}


326 
Function sets may be written in $\lambda$notation; $\lambda x\in A.b[x]$


327 
stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$. In order for


328 
this to be a set, the function's domain~$A$ must be given. Using the


329 
constant~\ttindexbold{Lambda}, we may express function sets as {\tt


330 
Lambda($A$,$\lambda x.b[x]$)} or use the syntax \hbox{\tt lam $x$:$A$.$b[x]$}.


331 


332 
Isabelle's set theory defines two {\bf bounded quantifiers}:


333 
\begin{eqnarray*}


334 
\forall x\in A.P[x] &\hbox{which abbreviates}& \forall x. x\in A\imp P[x] \\


335 
\exists x\in A.P[x] &\hbox{which abbreviates}& \exists x. x\in A\conj P[x]


336 
\end{eqnarray*}


337 
The constants~\ttindexbold{Ball} and~\ttindexbold{Bex} are defined


338 
accordingly. Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may


339 
write


340 
\hbox{\tt ALL $x$:$A$.$P[x]$} and \hbox{\tt EX $x$:$A$.$P[x]$}.


341 


342 


343 
%%%% zf.thy


344 


345 
\begin{figure}


346 
\begin{ttbox}


347 
\idx{Ball_def} Ball(A,P) == ALL x. x:A > P(x)


348 
\idx{Bex_def} Bex(A,P) == EX x. x:A & P(x)


349 


350 
\idx{subset_def} A <= B == ALL x:A. x:B


351 
\idx{extension} A = B <> A <= B & B <= A


352 


353 
\idx{union_iff} A : Union(C) <> (EX B:C. A:B)


354 
\idx{power_set} A : Pow(B) <> A <= B


355 
\idx{foundation} A=0  (EX x:A. ALL y:x. ~ y:A)


356 


357 
\idx{replacement} (ALL x:A. ALL y z. P(x,y) & P(x,z) > y=z) ==>


358 
b : PrimReplace(A,P) <> (EX x:A. P(x,b))


359 
\subcaption{The ZermeloFraenkel Axioms}


360 


361 
\idx{Replace_def} Replace(A,P) ==

287

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

104

363 
\idx{RepFun_def} RepFun(A,f) == \{y . x:A, y=f(x)\}


364 
\idx{the_def} The(P) == Union(\{y . x:\{0\}, P(y)\})


365 
\idx{if_def} if(P,a,b) == THE z. P & z=a  ~P & z=b


366 
\idx{Collect_def} Collect(A,P) == \{y . x:A, x=y & P(x)\}


367 
\idx{Upair_def} Upair(a,b) ==


368 
\{y. x:Pow(Pow(0)), (x=0 & y=a)  (x=Pow(0) & y=b)\}


369 
\subcaption{Consequences of replacement}


370 


371 
\idx{Inter_def} Inter(A) == \{ x:Union(A) . ALL y:A. x:y\}


372 
\idx{Un_def} A Un B == Union(Upair(A,B))


373 
\idx{Int_def} A Int B == Inter(Upair(A,B))


374 
\idx{Diff_def} A  B == \{ x:A . ~(x:B) \}


375 
\subcaption{Union, intersection, difference}


376 
\end{ttbox}


377 
\caption{Rules and axioms of {\ZF}} \label{ZFrules}


378 
\end{figure}


379 


380 


381 
\begin{figure}


382 
\begin{ttbox}

111

383 
\idx{cons_def} cons(a,A) == Upair(a,a) Un A


384 
\idx{succ_def} succ(i) == cons(i,i)


385 
\idx{infinity} 0:Inf & (ALL y:Inf. succ(y): Inf)


386 
\subcaption{Finite and infinite sets}


387 

104

388 
\idx{Pair_def} <a,b> == \{\{a,a\}, \{a,b\}\}

111

389 
\idx{split_def} split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b)

287

390 
\idx{fst_def} fst(A) == split(\%x y.x, p)


391 
\idx{snd_def} snd(A) == split(\%x y.y, p)

104

392 
\idx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}


393 
\subcaption{Ordered pairs and Cartesian products}


394 


395 
\idx{converse_def} converse(r) == \{z. w:r, EX x y. w=<x,y> & z=<y,x>\}


396 
\idx{domain_def} domain(r) == \{x. w:r, EX y. w=<x,y>\}


397 
\idx{range_def} range(r) == domain(converse(r))


398 
\idx{field_def} field(r) == domain(r) Un range(r)


399 
\idx{image_def} r `` A == \{y : range(r) . EX x:A. <x,y> : r\}


400 
\idx{vimage_def} r `` A == converse(r)``A


401 
\subcaption{Operations on relations}


402 


403 
\idx{lam_def} Lambda(A,b) == \{<x,b(x)> . x:A\}


404 
\idx{apply_def} f`a == THE y. <a,y> : f


405 
\idx{Pi_def} Pi(A,B) == \{f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f\}


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


407 
\subcaption{Functions and general product}


408 
\end{ttbox}


409 
\caption{Further definitions of {\ZF}} \label{ZFdefs}


410 
\end{figure}


411 


412 


413 
%%%% zf.ML


414 


415 
\begin{figure}


416 
\begin{ttbox}


417 
\idx{ballI} [ !!x. x:A ==> P(x) ] ==> ALL x:A. P(x)


418 
\idx{bspec} [ ALL x:A. P(x); x: A ] ==> P(x)


419 
\idx{ballE} [ ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q ] ==> Q


420 


421 
\idx{ball_cong} [ A=A'; !!x. x:A' ==> P(x) <> P'(x) ] ==>


422 
(ALL x:A. P(x)) <> (ALL x:A'. P'(x))


423 


424 
\idx{bexI} [ P(x); x: A ] ==> EX x:A. P(x)


425 
\idx{bexCI} [ ALL x:A. ~P(x) ==> P(a); a: A ] ==> EX x:A.P(x)


426 
\idx{bexE} [ EX x:A. P(x); !!x. [ x:A; P(x) ] ==> Q ] ==> Q


427 


428 
\idx{bex_cong} [ A=A'; !!x. x:A' ==> P(x) <> P'(x) ] ==>


429 
(EX x:A. P(x)) <> (EX x:A'. P'(x))


430 
\subcaption{Bounded quantifiers}


431 


432 
\idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B


433 
\idx{subsetD} [ A <= B; c:A ] ==> c:B


434 
\idx{subsetCE} [ A <= B; ~(c:A) ==> P; c:B ==> P ] ==> P


435 
\idx{subset_refl} A <= A


436 
\idx{subset_trans} [ A<=B; B<=C ] ==> A<=C


437 


438 
\idx{equalityI} [ A <= B; B <= A ] ==> A = B


439 
\idx{equalityD1} A = B ==> A<=B


440 
\idx{equalityD2} A = B ==> B<=A


441 
\idx{equalityE} [ A = B; [ A<=B; B<=A ] ==> P ] ==> P


442 
\subcaption{Subsets and extensionality}


443 


444 
\idx{emptyE} a:0 ==> P


445 
\idx{empty_subsetI} 0 <= A


446 
\idx{equals0I} [ !!y. y:A ==> False ] ==> A=0


447 
\idx{equals0D} [ A=0; a:A ] ==> P


448 


449 
\idx{PowI} A <= B ==> A : Pow(B)


450 
\idx{PowD} A : Pow(B) ==> A<=B


451 
\subcaption{The empty set; power sets}


452 
\end{ttbox}


453 
\caption{Basic derived rules for {\ZF}} \label{ZFlemmas1}


454 
\end{figure}


455 


456 


457 


458 
\begin{figure}


459 
\begin{ttbox}


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


461 
b : \{y. x:A, P(x,y)\}


462 


463 
\idx{ReplaceE} [ b : \{y. x:A, P(x,y)\};


464 
!!x. [ x: A; P(x,b); ALL y. P(x,y)>y=b ] ==> R


465 
] ==> R


466 


467 
\idx{RepFunI} [ a : A ] ==> f(a) : \{f(x). x:A\}


468 
\idx{RepFunE} [ b : \{f(x). x:A\};


469 
!!x.[ x:A; b=f(x) ] ==> P ] ==> P


470 


471 
\idx{separation} a : \{x:A. P(x)\} <> a:A & P(a)


472 
\idx{CollectI} [ a:A; P(a) ] ==> a : \{x:A. P(x)\}


473 
\idx{CollectE} [ a : \{x:A. P(x)\}; [ a:A; P(a) ] ==> R ] ==> R


474 
\idx{CollectD1} a : \{x:A. P(x)\} ==> a:A


475 
\idx{CollectD2} a : \{x:A. P(x)\} ==> P(a)


476 
\end{ttbox}


477 
\caption{Replacement and separation} \label{ZFlemmas2}


478 
\end{figure}


479 


480 


481 
\begin{figure}


482 
\begin{ttbox}


483 
\idx{UnionI} [ B: C; A: B ] ==> A: Union(C)


484 
\idx{UnionE} [ A : Union(C); !!B.[ A: B; B: C ] ==> R ] ==> R


485 


486 
\idx{InterI} [ !!x. x: C ==> A: x; c:C ] ==> A : Inter(C)


487 
\idx{InterD} [ A : Inter(C); B : C ] ==> A : B


488 
\idx{InterE} [ A : Inter(C); A:B ==> R; ~ B:C ==> R ] ==> R


489 


490 
\idx{UN_I} [ a: A; b: B(a) ] ==> b: (UN x:A. B(x))


491 
\idx{UN_E} [ b : (UN x:A. B(x)); !!x.[ x: A; b: B(x) ] ==> R


492 
] ==> R


493 


494 
\idx{INT_I} [ !!x. x: A ==> b: B(x); a: A ] ==> b: (INT x:A. B(x))


495 
\idx{INT_E} [ b : (INT x:A. B(x)); a: A ] ==> b : B(a)


496 
\end{ttbox}


497 
\caption{General Union and Intersection} \label{ZFlemmas3}


498 
\end{figure}


499 


500 


501 
\section{The ZermeloFraenkel axioms}

287

502 
The axioms appear in Fig.\ts \ref{ZFrules}. They resemble those

104

503 
presented by Suppes~\cite{suppes72}. Most of the theory consists of


504 
definitions. In particular, bounded quantifiers and the subset relation


505 
appear in other axioms. Objectlevel quantifiers and implications have


506 
been replaced by metalevel ones wherever possible, to simplify use of the

287

507 
axioms. See the file {\tt ZF/zf.thy} for details.

104

508 


509 
The traditional replacement axiom asserts


510 
\[ y \in {\tt PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \]


511 
subject to the condition that $P(x,y)$ is singlevalued for all~$x\in A$.


512 
The Isabelle theory defines \ttindex{Replace} to apply


513 
\ttindexbold{PrimReplace} to the singlevalued part of~$P$, namely


514 
\[ (\exists!z.P(x,z)) \conj P(x,y). \]


515 
Thus $y\in {\tt Replace}(A,P)$ if and only if there is some~$x$ such that


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


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


518 
same set, if $P(x,y)$ is singlevalued. The nice syntax for replacement


519 
expands to {\tt Replace}.


520 


521 
Other consequences of replacement include functional replacement


522 
(\ttindexbold{RepFun}) and definite descriptions (\ttindexbold{The}).


523 
Axioms for separation (\ttindexbold{Collect}) and unordered pairs


524 
(\ttindexbold{Upair}) are traditionally assumed, but they actually follow


525 
from replacement~\cite[pages 2378]{suppes72}.


526 


527 
The definitions of general intersection, etc., are straightforward. Note


528 
the definition of \ttindex{cons}, which underlies the finite set notation.


529 
The axiom of infinity gives us a set that contains~0 and is closed under


530 
successor (\ttindexbold{succ}). Although this set is not uniquely defined,


531 
the theory names it (\ttindexbold{Inf}) in order to simplify the


532 
construction of the natural numbers.

111

533 

287

534 
Further definitions appear in Fig.\ts\ref{ZFdefs}. Ordered pairs are

104

535 
defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$. Recall


536 
that \ttindexbold{Sigma}$(A,B)$ generalizes the Cartesian product of two


537 
sets. It is defined to be the union of all singleton sets


538 
$\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$. This is a typical usage of


539 
general union.


540 


541 
The projections involve definite descriptions. The \ttindex{split}


542 
operation is like the similar operation in MartinL\"of Type Theory, and is


543 
often easier to use than \ttindex{fst} and~\ttindex{snd}. It is defined


544 
using a description for convenience, but could equivalently be defined by


545 
\begin{ttbox}

111

546 
split(c,p) == c(fst(p),snd(p))

104

547 
\end{ttbox}


548 
Operations on relations include converse, domain, range, and image. The


549 
set ${\tt Pi}(A,B)$ generalizes the space of functions between two sets.


550 
Note the simple definitions of $\lambda$abstraction (using


551 
\ttindex{RepFun}) and application (using a definite description). The


552 
function \ttindex{restrict}$(f,A)$ has the same values as~$f$, but only


553 
over the domain~$A$.


554 


555 
No axiom of choice is provided. It is traditional to include this axiom


556 
only where it is needed  mainly in the theory of cardinal numbers, which


557 
Isabelle does not formalize at present.


558 


559 


560 
\section{From basic lemmas to function spaces}


561 
Faced with so many definitions, it is essential to prove lemmas. Even


562 
trivial theorems like $A\inter B=B\inter A$ would be difficult to prove


563 
from the definitions alone. Isabelle's set theory derives many rules using


564 
a natural deduction style. Ideally, a natural deduction rule should


565 
introduce or eliminate just one operator, but this is not always practical.


566 
For most operators, we may forget its definition and use its derived rules


567 
instead.


568 


569 
\subsection{Fundamental lemmas}


570 
Figure~\ref{ZFlemmas1} presents the derived rules for the most basic


571 
operators. The rules for the bounded quantifiers resemble those for the


572 
ordinary quantifiers, but note that \ttindex{BallE} uses a negated


573 
assumption in the style of Isabelle's classical module. The congruence rules


574 
\ttindex{ball_cong} and \ttindex{bex_cong} are required by Isabelle's


575 
simplifier, but have few other uses. Congruence rules must be specially


576 
derived for all binding operators, and henceforth will not be shown.


577 


578 
Figure~\ref{ZFlemmas1} also shows rules for the subset and equality


579 
relations (proof by extensionality), and rules about the empty set and the


580 
power set operator.


581 


582 
Figure~\ref{ZFlemmas2} presents rules for replacement and separation.


583 
The rules for \ttindex{Replace} and \ttindex{RepFun} are much simpler than


584 
comparable rules for {\tt PrimReplace} would be. The principle of


585 
separation is proved explicitly, although most proofs should use the


586 
natural deduction rules for \ttindex{Collect}. The elimination rule


587 
\ttindex{CollectE} is equivalent to the two destruction rules


588 
\ttindex{CollectD1} and \ttindex{CollectD2}, but each rule is suited to


589 
particular circumstances. Although too many rules can be confusing, there


590 
is no reason to aim for a minimal set of rules. See the file

287

591 
{\tt ZF/zf.ML} for a complete listing.

104

592 


593 
Figure~\ref{ZFlemmas3} presents rules for general union and intersection.


594 
The empty intersection should be undefined. We cannot have


595 
$\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set. All


596 
expressions denote something in {\ZF} set theory; the definition of


597 
intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is


598 
arbitrary. The rule \ttindexbold{InterI} must have a premise to exclude


599 
the empty intersection. Some of the laws governing intersections require


600 
similar premises.


601 


602 


603 
%%% upair.ML


604 


605 
\begin{figure}


606 
\begin{ttbox}


607 
\idx{pairing} a:Upair(b,c) <> (a=b  a=c)


608 
\idx{UpairI1} a : Upair(a,b)


609 
\idx{UpairI2} b : Upair(a,b)


610 
\idx{UpairE} [ a : Upair(b,c); a = b ==> P; a = c ==> P ] ==> P


611 
\subcaption{Unordered pairs}


612 


613 
\idx{UnI1} c : A ==> c : A Un B


614 
\idx{UnI2} c : B ==> c : A Un B


615 
\idx{UnCI} (~c : B ==> c : A) ==> c : A Un B


616 
\idx{UnE} [ c : A Un B; c:A ==> P; c:B ==> P ] ==> P


617 


618 
\idx{IntI} [ c : A; c : B ] ==> c : A Int B


619 
\idx{IntD1} c : A Int B ==> c : A


620 
\idx{IntD2} c : A Int B ==> c : B


621 
\idx{IntE} [ c : A Int B; [ c:A; c:B ] ==> P ] ==> P


622 


623 
\idx{DiffI} [ c : A; ~ c : B ] ==> c : A  B


624 
\idx{DiffD1} c : A  B ==> c : A


625 
\idx{DiffD2} [ c : A  B; c : B ] ==> P


626 
\idx{DiffE} [ c : A  B; [ c:A; ~ c:B ] ==> P ] ==> P


627 
\subcaption{Union, intersection, difference}


628 
\end{ttbox}


629 
\caption{Unordered pairs and their consequences} \label{ZFupair1}


630 
\end{figure}


631 


632 


633 
\begin{figure}


634 
\begin{ttbox}


635 
\idx{consI1} a : cons(a,B)


636 
\idx{consI2} a : B ==> a : cons(b,B)


637 
\idx{consCI} (~ a:B ==> a=b) ==> a: cons(b,B)


638 
\idx{consE} [ a : cons(b,A); a=b ==> P; a:A ==> P ] ==> P


639 


640 
\idx{singletonI} a : \{a\}


641 
\idx{singletonE} [ a : \{b\}; a=b ==> P ] ==> P


642 
\subcaption{Finite and singleton sets}


643 


644 
\idx{succI1} i : succ(i)


645 
\idx{succI2} i : j ==> i : succ(j)


646 
\idx{succCI} (~ i:j ==> i=j) ==> i: succ(j)


647 
\idx{succE} [ i : succ(j); i=j ==> P; i:j ==> P ] ==> P


648 
\idx{succ_neq_0} [ succ(n)=0 ] ==> P


649 
\idx{succ_inject} succ(m) = succ(n) ==> m=n


650 
\subcaption{The successor function}


651 


652 
\idx{the_equality} [ P(a); !!x. P(x) ==> x=a ] ==> (THE x. P(x)) = a


653 
\idx{theI} EX! x. P(x) ==> P(THE x. P(x))


654 


655 
\idx{if_P} P ==> if(P,a,b) = a


656 
\idx{if_not_P} ~P ==> if(P,a,b) = b


657 


658 
\idx{mem_anti_sym} [ a:b; b:a ] ==> P


659 
\idx{mem_anti_refl} a:a ==> P


660 
\subcaption{Descriptions; noncircularity}


661 
\end{ttbox}


662 
\caption{Finite sets and their consequences} \label{ZFupair2}


663 
\end{figure}


664 


665 


666 
\subsection{Unordered pairs and finite sets}


667 
Figure~\ref{ZFupair1} presents the principle of unordered pairing, along


668 
with its derived rules. Binary union and intersection are defined in terms


669 
of ordered pairs, and set difference is included for completeness. The


670 
rule \ttindexbold{UnCI} is useful for classical reasoning about unions,


671 
like {\tt disjCI}\@; it supersedes \ttindexbold{UnI1} and


672 
\ttindexbold{UnI2}, but these rules are often easier to work with. For


673 
intersection and difference we have both elimination and destruction rules.


674 
Again, there is no reason to provide a minimal rule set.


675 


676 
Figure~\ref{ZFupair2} is concerned with finite sets. It presents rules


677 
for~\ttindex{cons}, the finite set constructor, and rules for singleton


678 
sets. Because the successor function is defined in terms of~{\tt cons},


679 
its derived rules appear here.


680 


681 
Definite descriptions (\ttindex{THE}) are defined in terms of the singleton


682 
set $\{0\}$, but their derived rules fortunately hide this. The


683 
rule~\ttindex{theI} can be difficult to apply, because $\Var{P}$ must be


684 
instantiated correctly. However, \ttindex{the_equality} does not have this


685 
problem and the files contain many examples of its use.


686 


687 
Finally, the impossibility of having both $a\in b$ and $b\in a$


688 
(\ttindex{mem_anti_sym}) is proved by applying the axiom of foundation to


689 
the set $\{a,b\}$. The impossibility of $a\in a$ is a trivial consequence.


690 

287

691 
See the file {\tt ZF/upair.ML} for full details.

104

692 


693 


694 
%%% subset.ML


695 


696 
\begin{figure}


697 
\begin{ttbox}


698 
\idx{Union_upper} B:A ==> B <= Union(A)


699 
\idx{Union_least} [ !!x. x:A ==> x<=C ] ==> Union(A) <= C


700 


701 
\idx{Inter_lower} B:A ==> Inter(A) <= B


702 
\idx{Inter_greatest} [ a:A; !!x. x:A ==> C<=x ] ==> C <= Inter(A)


703 


704 
\idx{Un_upper1} A <= A Un B


705 
\idx{Un_upper2} B <= A Un B


706 
\idx{Un_least} [ A<=C; B<=C ] ==> A Un B <= C


707 


708 
\idx{Int_lower1} A Int B <= A


709 
\idx{Int_lower2} A Int B <= B


710 
\idx{Int_greatest} [ C<=A; C<=B ] ==> C <= A Int B


711 


712 
\idx{Diff_subset} AB <= A


713 
\idx{Diff_contains} [ C<=A; C Int B = 0 ] ==> C <= AB


714 


715 
\idx{Collect_subset} Collect(A,P) <= A


716 
\end{ttbox}


717 
\caption{Subset and lattice properties} \label{ZFsubset}


718 
\end{figure}


719 


720 


721 
\subsection{Subset and lattice properties}


722 
Figure~\ref{ZFsubset} shows that the subset relation is a complete


723 
lattice. Unions form least upper bounds; nonempty intersections form


724 
greatest lower bounds. A few other laws involving subsets are included.

287

725 
See the file {\tt ZF/subset.ML}.

104

726 


727 
%%% pair.ML


728 


729 
\begin{figure}


730 
\begin{ttbox}


731 
\idx{Pair_inject1} <a,b> = <c,d> ==> a=c


732 
\idx{Pair_inject2} <a,b> = <c,d> ==> b=d


733 
\idx{Pair_inject} [ <a,b> = <c,d>; [ a=c; b=d ] ==> P ] ==> P


734 
\idx{Pair_neq_0} <a,b>=0 ==> P


735 


736 
\idx{fst} fst(<a,b>) = a


737 
\idx{snd} snd(<a,b>) = b

287

738 
\idx{split} split(\%x y.c(x,y), <a,b>) = c(a,b)

104

739 


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


741 


742 
\idx{SigmaE} [ c: Sigma(A,B);


743 
!!x y.[ x:A; y:B(x); c=<x,y> ] ==> P ] ==> P


744 


745 
\idx{SigmaE2} [ <a,b> : Sigma(A,B);


746 
[ a:A; b:B(a) ] ==> P ] ==> P


747 
\end{ttbox}


748 
\caption{Ordered pairs; projections; general sums} \label{ZFpair}


749 
\end{figure}


750 


751 


752 
\subsection{Ordered pairs}


753 
Figure~\ref{ZFpair} presents the rules governing ordered pairs,

287

754 
projections and general sums. File {\tt ZF/pair.ML} contains the

104

755 
full (and tedious) proof that $\{\{a\},\{a,b\}\}$ functions as an ordered


756 
pair. This property is expressed as two destruction rules,


757 
\ttindexbold{Pair_inject1} and \ttindexbold{Pair_inject2}, and equivalently


758 
as the elimination rule \ttindexbold{Pair_inject}.


759 

114

760 
The rule \ttindexbold{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$. This


761 
is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other


762 
encoding of ordered pairs. The nonstandard ordered pairs mentioned below


763 
satisfy $\pair{\emptyset;\emptyset}=\emptyset$.

104

764 


765 
The natural deduction rules \ttindexbold{SigmaI} and \ttindexbold{SigmaE}


766 
assert that \ttindex{Sigma}$(A,B)$ consists of all pairs of the form


767 
$\pair{x,y}$, for $x\in A$ and $y\in B(x)$. The rule \ttindexbold{SigmaE2}


768 
merely states that $\pair{a,b}\in {\tt Sigma}(A,B)$ implies $a\in A$ and


769 
$b\in B(a)$.


770 


771 


772 
%%% domrange.ML


773 


774 
\begin{figure}


775 
\begin{ttbox}


776 
\idx{domainI} <a,b>: r ==> a : domain(r)


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


778 
\idx{domain_subset} domain(Sigma(A,B)) <= A


779 


780 
\idx{rangeI} <a,b>: r ==> b : range(r)


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


782 
\idx{range_subset} range(A*B) <= B


783 


784 
\idx{fieldI1} <a,b>: r ==> a : field(r)


785 
\idx{fieldI2} <a,b>: r ==> b : field(r)


786 
\idx{fieldCI} (~ <c,a>:r ==> <a,b>: r) ==> a : field(r)


787 


788 
\idx{fieldE} [ a : field(r);


789 
!!x. <a,x>: r ==> P;


790 
!!x. <x,a>: r ==> P


791 
] ==> P


792 


793 
\idx{field_subset} field(A*A) <= A


794 
\subcaption{Domain, range and field of a Relation}


795 


796 
\idx{imageI} [ <a,b>: r; a:A ] ==> b : r``A


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


798 


799 
\idx{vimageI} [ <a,b>: r; b:B ] ==> a : r``B


800 
\idx{vimageE} [ a: r``B; !!x.[ <a,x>: r; x:B ] ==> P ] ==> P


801 
\subcaption{Image and inverse image}


802 
\end{ttbox}


803 
\caption{Relations} \label{ZFdomrange}


804 
\end{figure}


805 


806 


807 
\subsection{Relations}


808 
Figure~\ref{ZFdomrange} presents rules involving relations, which are sets


809 
of ordered pairs. The converse of a relation~$r$ is the set of all pairs


810 
$\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then


811 
{\ttindex{converse}$(r)$} is its inverse. The rules for the domain


812 
operation, \ttindex{domainI} and~\ttindex{domainE}, assert that


813 
\ttindex{domain}$(r)$ consists of every element~$a$ such that $r$ contains


814 
some pair of the form~$\pair{x,y}$. The range operation is similar, and


815 
the field of a relation is merely the union of its domain and range. Note


816 
that image and inverse image are generalizations of range and domain,


817 
respectively. See the file

287

818 
{\tt ZF/domrange.ML} for derivations of the rules.

104

819 


820 


821 
%%% func.ML


822 


823 
\begin{figure}


824 
\begin{ttbox}


825 
\idx{fun_is_rel} f: Pi(A,B) ==> f <= Sigma(A,B)


826 


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


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


829 


830 
\idx{apply_type} [ f: Pi(A,B); a:A ] ==> f`a : B(a)


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


832 
\idx{apply_iff} f: Pi(A,B) ==> <a,b>: f <> a:A & f`a = b


833 


834 
\idx{fun_extension} [ f : Pi(A,B); g: Pi(A,D);


835 
!!x. x:A ==> f`x = g`x ] ==> f=g


836 


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


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


839 


840 
\idx{Pi_type} [ f: A>C; !!x. x:A ==> f`x: B(x) ] ==> f: Pi(A,B)


841 
\idx{domain_of_fun} f: Pi(A,B) ==> domain(f)=A


842 
\idx{range_of_fun} f: Pi(A,B) ==> f: A>range(f)


843 


844 
\idx{restrict} a : A ==> restrict(f,A) ` a = f`a


845 
\idx{restrict_type} [ !!x. x:A ==> f`x: B(x) ] ==>


846 
restrict(f,A) : Pi(A,B)


847 


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


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


850 
] ==> P


851 


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


853 


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


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


856 


857 
\idx{lam_theI} (!!x. x:A ==> EX! y. Q(x,y)) ==> EX h. ALL x:A. Q(x, h`x)


858 
\end{ttbox}


859 
\caption{Functions and $\lambda$abstraction} \label{ZFfunc1}


860 
\end{figure}


861 


862 


863 
\begin{figure}


864 
\begin{ttbox}


865 
\idx{fun_empty} 0: 0>0


866 
\idx{fun_single} \{<a,b>\} : \{a\} > \{b\}


867 


868 
\idx{fun_disjoint_Un} [ f: A>B; g: C>D; A Int C = 0 ] ==>


869 
(f Un g) : (A Un C) > (B Un D)


870 


871 
\idx{fun_disjoint_apply1} [ a:A; f: A>B; g: C>D; A Int C = 0 ] ==>


872 
(f Un g)`a = f`a


873 


874 
\idx{fun_disjoint_apply2} [ c:C; f: A>B; g: C>D; A Int C = 0 ] ==>


875 
(f Un g)`c = g`c


876 
\end{ttbox}


877 
\caption{Constructing functions from smaller sets} \label{ZFfunc2}


878 
\end{figure}


879 


880 


881 
\subsection{Functions}


882 
Functions, represented by graphs, are notoriously difficult to reason

287

883 
about. The file {\tt ZF/func.ML} derives many rules, which overlap

104

884 
more than they ought. One day these rules will be tidied up; this section


885 
presents only the more important ones.


886 


887 
Figure~\ref{ZFfunc1} presents the basic properties of \ttindex{Pi}$(A,B)$,


888 
the generalized function space. For example, if $f$ is a function and


889 
$\pair{a,b}\in f$, then $f`a=b$ (\ttindex{apply_equality}). Two functions


890 
are equal provided they have equal domains and deliver equals results


891 
(\ttindex{fun_extension}).


892 


893 
By \ttindex{Pi_type}, a function typing of the form $f\in A\to C$ can be


894 
refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable


895 
family of sets $\{B(x)\}@{x\in A}$. Conversely, by \ttindex{range_of_fun},


896 
any dependent typing can be flattened to yield a function type of the form


897 
$A\to C$; here, $C={\tt range}(f)$.


898 


899 
Among the laws for $\lambda$abstraction, \ttindex{lamI} and \ttindex{lamE}


900 
describe the graph of the generated function, while \ttindex{beta} and


901 
\ttindex{eta} are the standard conversions. We essentially have a


902 
dependentlytyped $\lambda$calculus.


903 


904 
Figure~\ref{ZFfunc2} presents some rules that can be used to construct


905 
functions explicitly. We start with functions consisting of at most one


906 
pair, and may form the union of two functions provided their domains are


907 
disjoint.


908 


909 


910 
\begin{figure}


911 
\begin{center}


912 
\begin{tabular}{rrr}

111

913 
\it name &\it metatype & \it description \\

287

914 
\idx{id} & $\To i$ & identity function \\

111

915 
\idx{inj} & $[i,i]\To i$ & injective function space\\


916 
\idx{surj} & $[i,i]\To i$ & surjective function space\\


917 
\idx{bij} & $[i,i]\To i$ & bijective function space


918 
\\[1ex]


919 
\idx{1} & $i$ & $\{\emptyset\}$ \\


920 
\idx{bool} & $i$ & the set $\{\emptyset,1\}$ \\


921 
\idx{cond} & $[i,i,i]\To i$ & conditional for {\tt bool}


922 
\\[1ex]


923 
\idx{Inl}~~\idx{Inr} & $i\To i$ & injections\\


924 
\idx{case} & $[i\To i,i\To i, i]\To i$ & conditional for $+$


925 
\\[1ex]


926 
\idx{nat} & $i$ & set of natural numbers \\


927 
\idx{nat_case}& $[i,i\To i,i]\To i$ & conditional for $nat$\\


928 
\idx{rec} & $[i,i,[i,i]\To i]\To i$ & recursor for $nat$


929 
\\[1ex]


930 
\idx{list} & $i\To i$ & lists over some set\\


931 
\idx{list_case} & $[i, [i,i]\To i, i] \To i$ & conditional for $list(A)$ \\


932 
\idx{list_rec} & $[i, i, [i,i,i]\To i] \To i$ & recursor for $list(A)$ \\


933 
\idx{map} & $[i\To i, i] \To i$ & mapping functional\\


934 
\idx{length} & $i\To i$ & length of a list\\


935 
\idx{rev} & $i\To i$ & reverse of a list\\


936 
\idx{flat} & $i\To i$ & flatting a list of lists\\

104

937 
\end{tabular}


938 
\end{center}


939 
\subcaption{Constants}


940 


941 
\begin{center}


942 
\indexbold{*"+}


943 
\index{#*@{\tt\#*}bold}


944 
\index{*divbold}


945 
\index{*modbold}


946 
\index{#+@{\tt\#+}bold}


947 
\index{#@{\tt\#}bold}


948 
\begin{tabular}{rrrr}

111

949 
\idx{O} & $[i,i]\To i$ & Right 60 & composition ($\circ$) \\


950 
\tt + & $[i,i]\To i$ & Right 65 & disjoint union \\


951 
\tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\


952 
\tt div & $[i,i]\To i$ & Left 70 & division\\


953 
\tt mod & $[i,i]\To i$ & Left 70 & modulus\\


954 
\tt \#+ & $[i,i]\To i$ & Left 65 & addition\\


955 
\tt \# & $[i,i]\To i$ & Left 65 & subtraction\\


956 
\tt \@ & $[i,i]\To i$ & Right 60 & append for lists

104

957 
\end{tabular}


958 
\end{center}


959 
\subcaption{Infixes}


960 
\caption{Further constants for {\ZF}} \label{ZFfurtherconstants}


961 
\end{figure}


962 


963 


964 
\begin{figure}


965 
\begin{ttbox}


966 
\idx{Int_absorb} A Int A = A


967 
\idx{Int_commute} A Int B = B Int A


968 
\idx{Int_assoc} (A Int B) Int C = A Int (B Int C)


969 
\idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)


970 


971 
\idx{Un_absorb} A Un A = A


972 
\idx{Un_commute} A Un B = B Un A


973 
\idx{Un_assoc} (A Un B) Un C = A Un (B Un C)


974 
\idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)


975 


976 
\idx{Diff_cancel} AA = 0


977 
\idx{Diff_disjoint} A Int (BA) = 0


978 
\idx{Diff_partition} A<=B ==> A Un (BA) = B


979 
\idx{double_complement} [ A<=B; B<= C ] ==> (B  (CA)) = A


980 
\idx{Diff_Un} A  (B Un C) = (AB) Int (AC)


981 
\idx{Diff_Int} A  (B Int C) = (AB) Un (AC)


982 


983 
\idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)


984 
\idx{Inter_Un_distrib} [ a:A; b:B ] ==>


985 
Inter(A Un B) = Inter(A) Int Inter(B)


986 


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


988 


989 
\idx{Un_Inter_RepFun} b:B ==>


990 
A Un Inter(B) = (INT C:B. A Un C)


991 


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


993 
(SUM x:A. C(x)) Un (SUM x:B. C(x))


994 


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


996 
(SUM x:C. A(x)) Un (SUM x:C. B(x))


997 


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


999 
(SUM x:A. C(x)) Int (SUM x:B. C(x))


1000 


1001 
\idx{SUM_Int_distrib2} (SUM x:C. A(x) Int B(x)) =


1002 
(SUM x:C. A(x)) Int (SUM x:C. B(x))


1003 
\end{ttbox}


1004 
\caption{Equalities} \label{zfequalities}


1005 
\end{figure}


1006 

111

1007 


1008 
\begin{figure}


1009 
\begin{ttbox}


1010 
\idx{bnd_mono_def} bnd_mono(D,h) ==


1011 
h(D)<=D & (ALL W X. W<=X > X<=D > h(W) <= h(X))


1012 


1013 
\idx{lfp_def} lfp(D,h) == Inter({X: Pow(D). h(X) <= X})


1014 
\idx{gfp_def} gfp(D,h) == Union({X: Pow(D). X <= h(X)})


1015 
\subcaption{Definitions}


1016 


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


1018 


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


1020 


1021 
\idx{lfp_greatest} [ bnd_mono(D,h);


1022 
!!X. [ h(X) <= X; X<=D ] ==> A<=X


1023 
] ==> A <= lfp(D,h)


1024 


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


1026 


1027 
\idx{induct} [ a : lfp(D,h); bnd_mono(D,h);


1028 
!!x. x : h(Collect(lfp(D,h),P)) ==> P(x)


1029 
] ==> P(a)


1030 


1031 
\idx{lfp_mono} [ bnd_mono(D,h); bnd_mono(E,i);


1032 
!!X. X<=D ==> h(X) <= i(X)


1033 
] ==> lfp(D,h) <= lfp(E,i)


1034 


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


1036 


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


1038 


1039 
\idx{gfp_least} [ bnd_mono(D,h);


1040 
!!X. [ X <= h(X); X<=D ] ==> X<=A


1041 
] ==> gfp(D,h) <= A


1042 


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


1044 


1045 
\idx{coinduct} [ bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D


1046 
] ==> a : gfp(D,h)


1047 


1048 
\idx{gfp_mono} [ bnd_mono(D,h); D <= E;


1049 
!!X. X<=D ==> h(X) <= i(X)


1050 
] ==> gfp(D,h) <= gfp(E,i)


1051 
\end{ttbox}


1052 
\caption{Least and greatest fixedpoints} \label{zffixedpt}


1053 
\end{figure}


1054 


1055 

104

1056 
\begin{figure}


1057 
\begin{ttbox}


1058 
\idx{comp_def} r O s == \{xz : domain(s)*range(r) .


1059 
EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r\}


1060 
\idx{id_def} id(A) == (lam x:A. x)


1061 
\idx{inj_def} inj(A,B) == \{ f: A>B. ALL w:A. ALL x:A. f`w=f`x > w=x\}


1062 
\idx{surj_def} surj(A,B) == \{ f: A>B . ALL y:B. EX x:A. f`x=y\}


1063 
\idx{bij_def} bij(A,B) == inj(A,B) Int surj(A,B)


1064 
\subcaption{Definitions}


1065 


1066 
\idx{left_inverse} [ f: inj(A,B); a: A ] ==> converse(f)`(f`a) = a


1067 
\idx{right_inverse} [ f: inj(A,B); b: range(f) ] ==>


1068 
f`(converse(f)`b) = b


1069 


1070 
\idx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A)


1071 
\idx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A)


1072 


1073 
\idx{comp_type} [ s<=A*B; r<=B*C ] ==> (r O s) <= A*C


1074 
\idx{comp_assoc} (r O s) O t = r O (s O t)


1075 


1076 
\idx{left_comp_id} r<=A*B ==> id(B) O r = r


1077 
\idx{right_comp_id} r<=A*B ==> r O id(A) = r


1078 


1079 
\idx{comp_func} [ g:A>B; f:B>C ] ==> (f O g):A>C


1080 
\idx{comp_func_apply} [ g:A>B; f:B>C; a:A ] ==> (f O g)`a = f`(g`a)


1081 


1082 
\idx{comp_inj} [ g:inj(A,B); f:inj(B,C) ] ==> (f O g):inj(A,C)


1083 
\idx{comp_surj} [ g:surj(A,B); f:surj(B,C) ] ==> (f O g):surj(A,C)


1084 
\idx{comp_bij} [ g:bij(A,B); f:bij(B,C) ] ==> (f O g):bij(A,C)


1085 


1086 
\idx{left_comp_inverse} f: inj(A,B) ==> converse(f) O f = id(A)


1087 
\idx{right_comp_inverse} f: surj(A,B) ==> f O converse(f) = id(B)


1088 


1089 
\idx{bij_disjoint_Un}


1090 
[ f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 ] ==>


1091 
(f Un g) : bij(A Un C, B Un D)


1092 


1093 
\idx{restrict_bij} [ f:inj(A,B); C<=A ] ==> restrict(f,C): bij(C, f``C)


1094 
\end{ttbox}


1095 
\caption{Permutations} \label{zfperm}


1096 
\end{figure}


1097 


1098 
\begin{figure}


1099 
\begin{ttbox}


1100 
\idx{one_def} 1 == succ(0)


1101 
\idx{bool_def} bool == {0,1}


1102 
\idx{cond_def} cond(b,c,d) == if(b=1,c,d)

131

1103 
\idx{not_def} not(b) == cond(b,0,1)


1104 
\idx{and_def} a and b == cond(a,b,0)


1105 
\idx{or_def} a or b == cond(a,1,b)


1106 
\idx{xor_def} a xor b == cond(a,not(b),b)

104

1107 


1108 
\idx{sum_def} A+B == \{0\}*A Un \{1\}*B


1109 
\idx{Inl_def} Inl(a) == <0,a>


1110 
\idx{Inr_def} Inr(b) == <1,b>

287

1111 
\idx{case_def} case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u)

104

1112 
\subcaption{Definitions}


1113 


1114 
\idx{bool_1I} 1 : bool


1115 
\idx{bool_0I} 0 : bool


1116 

131

1117 
\idx{boolE} [ c: bool; c=1 ==> P; c=0 ==> P ] ==> P

104

1118 
\idx{cond_1} cond(1,c,d) = c


1119 
\idx{cond_0} cond(0,c,d) = d


1120 


1121 
\idx{sum_InlI} a : A ==> Inl(a) : A+B


1122 
\idx{sum_InrI} b : B ==> Inr(b) : A+B


1123 


1124 
\idx{Inl_inject} Inl(a)=Inl(b) ==> a=b


1125 
\idx{Inr_inject} Inr(a)=Inr(b) ==> a=b


1126 
\idx{Inl_neq_Inr} Inl(a)=Inr(b) ==> P


1127 


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


1129 

111

1130 
\idx{case_Inl} case(c,d,Inl(a)) = c(a)


1131 
\idx{case_Inr} case(c,d,Inr(b)) = d(b)

104

1132 
\end{ttbox}


1133 
\caption{Booleans and disjoint unions} \label{zfsum}


1134 
\end{figure}


1135 


1136 
\begin{figure}


1137 
\begin{ttbox}

111

1138 
\idx{QPair_def} <a;b> == a+b


1139 
\idx{qsplit_def} qsplit(c,p) == THE y. EX a b. p=<a;b> & y=c(a,b)


1140 
\idx{qfsplit_def} qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)


1141 
\idx{qconverse_def} qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}


1142 
\idx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>}


1143 


1144 
\idx{qsum_def} A <+> B == (\{0\} <*> A) Un (\{1\} <*> B)


1145 
\idx{QInl_def} QInl(a) == <0;a>


1146 
\idx{QInr_def} QInr(b) == <1;b>

287

1147 
\idx{qcase_def} qcase(c,d) == qsplit(\%y z. cond(y, d(z), c(z)))

111

1148 
\end{ttbox}


1149 
\caption{Nonstandard pairs, products and sums} \label{zfqpair}


1150 
\end{figure}


1151 


1152 


1153 
\begin{figure}


1154 
\begin{ttbox}

104

1155 
\idx{nat_def} nat == lfp(lam r: Pow(Inf). \{0\} Un \{succ(x). x:r\}


1156 

111

1157 
\idx{nat_case_def} nat_case(a,b,k) ==


1158 
THE y. k=0 & y=a  (EX x. k=succ(x) & y=b(x))

104

1159 


1160 
\idx{rec_def} rec(k,a,b) ==

287

1161 
transrec(k, \%n f. nat_case(a, \%m. b(m, f`m), n))

104

1162 

287

1163 
\idx{add_def} m#+n == rec(m, n, \%u v.succ(v))


1164 
\idx{diff_def} m#n == rec(n, m, \%u v. rec(v, 0, \%x y.x))


1165 
\idx{mult_def} m#*n == rec(m, 0, \%u v. n #+ v)


1166 
\idx{mod_def} m mod n == transrec(m, \%j f. if(j:n, j, f`(j#n)))


1167 
\idx{div_def} m div n == transrec(m, \%j f. if(j:n, 0, succ(f`(j#n))))

104

1168 
\subcaption{Definitions}


1169 


1170 
\idx{nat_0I} 0 : nat


1171 
\idx{nat_succI} n : nat ==> succ(n) : nat


1172 


1173 
\idx{nat_induct}


1174 
[ n: nat; P(0); !!x. [ x: nat; P(x) ] ==> P(succ(x))


1175 
] ==> P(n)


1176 

111

1177 
\idx{nat_case_0} nat_case(a,b,0) = a


1178 
\idx{nat_case_succ} nat_case(a,b,succ(m)) = b(m)

104

1179 


1180 
\idx{rec_0} rec(0,a,b) = a


1181 
\idx{rec_succ} rec(succ(m),a,b) = b(m, rec(m,a,b))


1182 


1183 
\idx{mult_type} [ m:nat; n:nat ] ==> m #* n : nat


1184 
\idx{mult_0} 0 #* n = 0


1185 
\idx{mult_succ} succ(m) #* n = n #+ (m #* n)


1186 
\idx{mult_commute} [ m:nat; n:nat ] ==> m #* n = n #* m


1187 
\idx{add_mult_dist}


1188 
[ m:nat; k:nat ] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)


1189 
\idx{mult_assoc}


1190 
[ m:nat; n:nat; k:nat ] ==> (m #* n) #* k = m #* (n #* k)


1191 


1192 
\idx{mod_quo_equality}


1193 
[ 0:n; m:nat; n:nat ] ==> (m div n)#*n #+ m mod n = m


1194 
\end{ttbox}


1195 
\caption{The natural numbers} \label{zfnat}


1196 
\end{figure}


1197 

111

1198 
\begin{figure}


1199 
\begin{ttbox}


1200 
\idx{Fin_0I} 0 : Fin(A)


1201 
\idx{Fin_consI} [ a: A; b: Fin(A) ] ==> cons(a,b) : Fin(A)


1202 


1203 
\idx{Fin_induct}


1204 
[ b: Fin(A);


1205 
P(0);


1206 
!!x y. [ x: A; y: Fin(A); x~:y; P(y) ] ==> P(cons(x,y))


1207 
] ==> P(b)


1208 

114

1209 
\idx{Fin_mono} A<=B ==> Fin(A) <= Fin(B)

111

1210 
\idx{Fin_UnI} [ b: Fin(A); c: Fin(A) ] ==> b Un c : Fin(A)


1211 
\idx{Fin_UnionI} C : Fin(Fin(A)) ==> Union(C) : Fin(A)


1212 
\idx{Fin_subset} [ c<=b; b: Fin(A) ] ==> c: Fin(A)


1213 
\end{ttbox}


1214 
\caption{The finite set operator} \label{zffin}


1215 
\end{figure}


1216 

104

1217 
\begin{figure}\underscoreon %%because @ is used here


1218 
\begin{ttbox}


1219 
\idx{list_rec_def} list_rec(l,c,h) ==

287

1220 
Vrec(l, \%l g.list_case(c, \%x xs. h(x, xs, g`xs), l))

104

1221 

287

1222 
\idx{map_def} map(f,l) == list_rec(l, 0, \%x xs r. <f(x), r>)


1223 
\idx{length_def} length(l) == list_rec(l, 0, \%x xs r. succ(r))


1224 
\idx{app_def} xs@ys == list_rec(xs, ys, \%x xs r. <x,r>)


1225 
\idx{rev_def} rev(l) == list_rec(l, 0, \%x xs r. r @ <x,0>)


1226 
\idx{flat_def} flat(ls) == list_rec(ls, 0, \%l ls r. l @ r)

104

1227 
\subcaption{Definitions}


1228 

111

1229 
\idx{NilI} Nil : list(A)


1230 
\idx{ConsI} [ a: A; l: list(A) ] ==> Cons(a,l) : list(A)

104

1231 

111

1232 
\idx{List.induct}

104

1233 
[ l: list(A);

111

1234 
P(Nil);


1235 
!!x y. [ x: A; y: list(A); P(y) ] ==> P(Cons(x,y))

104

1236 
] ==> P(l)


1237 

111

1238 
\idx{Cons_iff} Cons(a,l)=Cons(a',l') <> a=a' & l=l'


1239 
\idx{Nil_Cons_iff} ~ Nil=Cons(a,l)

104

1240 

111

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


1242 


1243 
\idx{list_rec_Nil} list_rec(Nil,c,h) = c


1244 
\idx{list_rec_Cons} list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))

104

1245 

287

1246 
\idx{map_ident} l: list(A) ==> map(\%u.u, l) = l


1247 
\idx{map_compose} l: list(A) ==> map(h, map(j,l)) = map(\%u.h(j(u)), l)

104

1248 
\idx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)


1249 
\idx{map_type}


1250 
[ l: list(A); !!x. x: A ==> h(x): B ] ==> map(h,l) : list(B)


1251 
\idx{map_flat}


1252 
ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))


1253 
\end{ttbox}


1254 
\caption{Lists} \label{zflist}


1255 
\end{figure}


1256 


1257 
\section{Further developments}


1258 
The next group of developments is complex and extensive, and only


1259 
highlights can be covered here. Figure~\ref{ZFfurtherconstants} lists


1260 
some of the further constants and infixes that are declared in the various


1261 
theory extensions.


1262 

114

1263 
Figure~\ref{zfequalities} presents commutative, associative, distributive,


1264 
and idempotency laws of union and intersection, along with other equations.

287

1265 
See file {\tt ZF/equalities.ML}.

114

1266 

131

1267 
Figure~\ref{zfsum} defines $\{0,1\}$ as a set of booleans, with the usual


1268 
operators including a conditional. It also defines the disjoint union of


1269 
two sets, with injections and a case analysis operator. See files

287

1270 
{\tt ZF/bool.ML} and {\tt ZF/sum.ML}.

104

1271 

111

1272 
Figure~\ref{zfqpair} defines a notion of ordered pair that admits


1273 
nonwellfounded tupling. Such pairs are written {\tt<$a$;$b$>}. It also


1274 
defines the eliminator \ttindexbold{qsplit}, the converse operator


1275 
\ttindexbold{qconverse}, and the summation operator \ttindexbold{QSigma}.


1276 
These are completely analogous to the corresponding versions for standard


1277 
ordered pairs. The theory goes on to define a nonstandard notion of

114

1278 
disjoint sum using nonstandard pairs. This will support coinductive


1279 
definitions, for example of infinite lists. See file \ttindexbold{qpair.thy}.

111

1280 

104

1281 
Monotonicity properties of most of the setforming operations are proved.


1282 
These are useful for applying the KnasterTarski Fixedpoint Theorem.

287

1283 
See file {\tt ZF/mono.ML}.

104

1284 

111

1285 
Figure~\ref{zffixedpt} presents the KnasterTarski Fixedpoint Theorem, proved


1286 
for the lattice of subsets of a set. The theory defines least and greatest


1287 
fixedpoint operators with corresponding induction and coinduction rules.


1288 
Later definitions use these, such as the natural numbers and


1289 
the transitive closure operator. The (co)inductive definition

287

1290 
package also uses them. See file {\tt ZF/fixedpt.ML}.

111

1291 

104

1292 
Figure~\ref{zfperm} defines composition and injective, surjective and


1293 
bijective function spaces, with proofs of many of their properties.

287

1294 
See file {\tt ZF/perm.ML}.

104

1295 


1296 
Figure~\ref{zfnat} presents the natural numbers, with induction and a

287

1297 
primitive recursion operator. See file {\tt ZF/nat.ML}. File


1298 
{\tt ZF/arith.ML} develops arithmetic on the natural numbers. It

104

1299 
defines addition, multiplication, subtraction, division, and remainder,


1300 
proving the theorem $a \bmod b + (a/b)\times b = a$. Division and


1301 
remainder are defined by repeated subtraction, which requires wellfounded


1302 
rather than primitive recursion.


1303 

287

1304 
The file {\tt ZF/univ.ML} defines a ``universe'' ${\tt univ}(A)$,

111

1305 
for constructing datatypes such as trees. This set contains $A$ and the


1306 
natural numbers. Vitally, it is closed under finite products: ${\tt


1307 
univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$. This file also


1308 
defines set theory's cumulative hierarchy, traditionally written $V@\alpha$


1309 
where $\alpha$ is any ordinal.


1310 

287

1311 
The file {\tt ZF/quniv.ML} defines a ``universe'' ${\tt quniv}(A)$,

114

1312 
for constructing codatatypes such as streams. It is analogous to ${\tt

111

1313 
univ}(A)$ but is closed under the nonstandard product and sum.


1314 


1315 
Figure~\ref{zffin} presents the finite set operator; ${\tt Fin}(A)$ is the


1316 
set of all finite sets over~$A$. The definition employs Isabelle's


1317 
inductive definition package, which proves the introduction rules


1318 
automatically. The induction rule shown is stronger than the one proved by

287

1319 
the package. See file {\tt ZF/fin.ML}.

111

1320 


1321 
Figure~\ref{zflist} presents the set of lists over~$A$, ${\tt list}(A)$.


1322 
The definition employs Isabelle's datatype package, which defines the


1323 
introduction and induction rules automatically, as well as the constructors

287

1324 
and case operator (\verblist_case). See file {\tt ZF/list.ML}.


1325 
The file {\tt ZF/listfn.thy} proceeds to define structural

111

1326 
recursion and the usual list functions.

104

1327 


1328 
The constructions of the natural numbers and lists make use of a suite of

111

1329 
operators for handling recursive function definitions. The developments are

104

1330 
summarized below:


1331 
\begin{description}

287

1332 
\item[{\tt ZF/trancl.ML}]

104

1333 
defines the transitive closure of a relation (as a least fixedpoint).


1334 

287

1335 
\item[{\tt ZF/wf.ML}]

104

1336 
proves the WellFounded Recursion Theorem, using an elegant


1337 
approach of Tobias Nipkow. This theorem permits general recursive


1338 
definitions within set theory.


1339 

287

1340 
\item[{\tt ZF/ord.ML}] defines the notions of transitive set and

111

1341 
ordinal number. It derives transfinite induction. A key definition is


1342 
{\bf less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and


1343 
$i\in j$. As a special case, it includes less than on the natural


1344 
numbers.

104

1345 

287

1346 
\item[{\tt ZF/epsilon.ML}]

104

1347 
derives $\epsilon$induction and $\epsilon$recursion, which are


1348 
generalizations of transfinite induction. It also defines


1349 
\ttindexbold{rank}$(x)$, which is the least ordinal $\alpha$ such that $x$


1350 
is constructed at stage $\alpha$ of the cumulative hierarchy (thus $x\in


1351 
V@{\alpha+1}$).


1352 
\end{description}


1353 


1354 


1355 
\begin{figure}


1356 
\begin{eqnarray*}

111

1357 
a\in \emptyset & \bimp & \bot\\


1358 
a \in A \union B & \bimp & a\in A \disj a\in B\\


1359 
a \in A \inter B & \bimp & a\in A \conj a\in B\\


1360 
a \in AB & \bimp & a\in A \conj \neg (a\in B)\\

104

1361 
a \in {\tt cons}(b,B) & \bimp & a=b \disj a\in B\\

111

1362 
i \in {\tt succ}(j) & \bimp & i=j \disj i\in j\\

104

1363 
\pair{a,b}\in {\tt Sigma}(A,B)

111

1364 
& \bimp & a\in A \conj b\in B(a)\\


1365 
a \in {\tt Collect}(A,P) & \bimp & a\in A \conj P(a)\\


1366 
(\forall x \in A. \top) & \bimp & \top

104

1367 
\end{eqnarray*}


1368 
\caption{Rewrite rules for set theory} \label{ZFsimpdata}


1369 
\end{figure}


1370 


1371 


1372 
\section{Simplification rules}


1373 
{\ZF} does not merely inherit simplification from \FOL, but instantiates

287

1374 
the rewriting package new. File {\tt ZF/simpdata.ML} contains the

104

1375 
details; here is a summary of the key differences:


1376 
\begin{itemize}


1377 
\item


1378 
\ttindexbold{mk_rew_rules} is given as a function that can


1379 
strip bounded universal quantifiers from a formula. For example, $\forall


1380 
x\in A.f(x)=g(x)$ yields the conditional rewrite rule $x\in A \Imp


1381 
f(x)=g(x)$.


1382 
\item


1383 
\ttindexbold{ZF_ss} contains congruence rules for all the operators of


1384 
{\ZF}, including the binding operators. It contains all the conversion


1385 
rules, such as \ttindex{fst} and \ttindex{snd}, as well as the

287

1386 
rewrites shown in Fig.\ts\ref{ZFsimpdata}.

104

1387 
\item


1388 
\ttindexbold{FOL_ss} is redeclared with the same {\FOL} rules as the


1389 
previous version, so that it may still be used.


1390 
\end{itemize}


1391 


1392 


1393 
\section{The examples directory}


1394 
This directory contains further developments in {\ZF} set theory. Here is


1395 
an overview; see the files themselves for more details.


1396 
\begin{description}

287

1397 
\item[{\tt ZF/ex/misc.ML}] contains miscellaneous examples such as

111

1398 
Cantor's Theorem, the Schr\"oderBernstein Theorem. and the


1399 
``Composition of homomorphisms'' challenge~\cite{boyer86}.

104

1400 

287

1401 
\item[{\tt ZF/ex/ramsey.ML}]

114

1402 
proves the finite exponent 2 version of Ramsey's Theorem, following Basin


1403 
and Kaufmann's presentation~\cite{basin91}.


1404 

287

1405 
\item[{\tt ZF/ex/equiv.ML}]

114

1406 
develops a ZF theory of equivalence classes, not using the Axiom of Choice.


1407 

287

1408 
\item[{\tt ZF/ex/integ.ML}]

114

1409 
develops a theory of the integers as equivalence classes of pairs of


1410 
natural numbers.


1411 

287

1412 
\item[{\tt ZF/ex/bin.ML}]

114

1413 
defines a datatype for two's complement binary integers. File

287

1414 
{\tt binfn.ML} then develops rewrite rules for binary

114

1415 
arithmetic. For instance, $1359\times {}2468 = {}3354012$ takes under


1416 
14 seconds.

104

1417 

287

1418 
\item[{\tt ZF/ex/bt.ML}]

104

1419 
defines the recursive data structure ${\tt bt}(A)$, labelled binary trees.


1420 

287

1421 
\item[{\tt ZF/ex/term.ML}]


1422 
and {\tt termfn.ML} define a recursive data structure for

114

1423 
terms and term lists. These are simply finite branching trees.

104

1424 

287

1425 
\item[{\tt ZF/ex/tf.ML}]


1426 
and {\tt tf_fn.ML} define primitives for solving mutually

114

1427 
recursive equations over sets. It constructs sets of trees and forests


1428 
as an example, including induction and recursion rules that handle the


1429 
mutual recursion.


1430 

287

1431 
\item[{\tt ZF/ex/prop.ML}]


1432 
and {\tt proplog.ML} proves soundness and completeness of

114

1433 
propositional logic. This illustrates datatype definitions, inductive


1434 
definitions, structural induction and rule induction.


1435 

287

1436 
\item[{\tt ZF/ex/listn.ML}]

114

1437 
presents the inductive definition of the lists of $n$ elements~\cite{paulin92}.

104

1438 

287

1439 
\item[{\tt ZF/ex/acc.ML}]

114

1440 
presents the inductive definition of the accessible part of a


1441 
relation~\cite{paulin92}.

104

1442 

287

1443 
\item[{\tt ZF/ex/comb.ML}]


1444 
presents the datatype definition of combinators. The file


1445 
{\tt contract0.ML} defines contraction, while file


1446 
{\tt parcontract.ML} defines parallel contraction and

114

1447 
proves the ChurchRosser Theorem. This case study follows Camilleri and


1448 
Melham~\cite{camilleri92}.


1449 

287

1450 
\item[{\tt ZF/ex/llist.ML}]


1451 
and {\tt llist_eq.ML} develop lazy lists in ZF and a notion

114

1452 
of coinduction for proving equations between them.

104

1453 
\end{description}


1454 


1455 


1456 
\section{A proof about powersets}

114

1457 
To demonstrate highlevel reasoning about subsets, let us prove the


1458 
equation ${{\tt Pow}(A)\cap {\tt Pow}(B)}= {\tt Pow}(A\cap B)$. Compared


1459 
with firstorder logic, set theory involves a maze of rules, and theorems


1460 
have many different proofs. Attempting other proofs of the theorem might


1461 
be instructive. This proof exploits the lattice properties of


1462 
intersection. It also uses the monotonicity of the powerset operation,


1463 
from {\tt ZF/mono.ML}:

104

1464 
\begin{ttbox}


1465 
\idx{Pow_mono} A<=B ==> Pow(A) <= Pow(B)


1466 
\end{ttbox}


1467 
We enter the goal and make the first step, which breaks the equation into


1468 
two inclusions by extensionality:\index{equalityI}


1469 
\begin{ttbox}


1470 
goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";


1471 
{\out Level 0}


1472 
{\out Pow(A Int B) = Pow(A) Int Pow(B)}


1473 
{\out 1. Pow(A Int B) = Pow(A) Int Pow(B)}

287

1474 
\ttbreak

104

1475 
by (resolve_tac [equalityI] 1);


1476 
{\out Level 1}


1477 
{\out Pow(A Int B) = Pow(A) Int Pow(B)}


1478 
{\out 1. Pow(A Int B) <= Pow(A) Int Pow(B)}


1479 
{\out 2. Pow(A) Int Pow(B) <= Pow(A Int B)}


1480 
\end{ttbox}


1481 
Both inclusions could be tackled straightforwardly using {\tt subsetI}.


1482 
A shorter proof results from noting that intersection forms the greatest


1483 
lower bound:\index{*Int_greatest}


1484 
\begin{ttbox}


1485 
by (resolve_tac [Int_greatest] 1);


1486 
{\out Level 2}


1487 
{\out Pow(A Int B) = Pow(A) Int Pow(B)}


1488 
{\out 1. Pow(A Int B) <= Pow(A)}


1489 
{\out 2. Pow(A Int B) <= Pow(B)}


1490 
{\out 3. Pow(A) Int Pow(B) <= Pow(A Int B)}


1491 
\end{ttbox}


1492 
Subgoal~1 follows by applying the monotonicity of {\tt Pow} to $A\inter


1493 
B\subseteq A$; subgoal~2 follows similarly:


1494 
\index{*Int_lower1}\index{*Int_lower2}


1495 
\begin{ttbox}


1496 
by (resolve_tac [Int_lower1 RS Pow_mono] 1);


1497 
{\out Level 3}


1498 
{\out Pow(A Int B) = Pow(A) Int Pow(B)}


1499 
{\out 1. Pow(A Int B) <= Pow(B)}


1500 
{\out 2. Pow(A) Int Pow(B) <= Pow(A Int B)}

287

1501 
\ttbreak

104

1502 
by (resolve_tac [Int_lower2 RS Pow_mono] 1);


1503 
{\out Level 4}


1504 
{\out Pow(A Int B) = Pow(A) Int Pow(B)}


1505 
{\out 1. Pow(A) Int Pow(B) <= Pow(A Int B)}


1506 
\end{ttbox}


1507 
We are left with the opposite inclusion, which we tackle in the


1508 
straightforward way:\index{*subsetI}


1509 
\begin{ttbox}


1510 
by (resolve_tac [subsetI] 1);


1511 
{\out Level 5}


1512 
{\out Pow(A Int B) = Pow(A) Int Pow(B)}


1513 
{\out 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)}


1514 
\end{ttbox}


1515 
The subgoal is to show $x\in {\tt Pow}(A\cap B)$ assuming $x\in{\tt

287

1516 
Pow}(A)\cap {\tt Pow}(B)$; eliminating this assumption produces two


1517 
subgoals. The rule \ttindex{IntE} treats the intersection like a conjunction


1518 
instead of unfolding its definition.

104

1519 
\begin{ttbox}


1520 
by (eresolve_tac [IntE] 1);


1521 
{\out Level 6}


1522 
{\out Pow(A Int B) = Pow(A) Int Pow(B)}


1523 
{\out 1. !!x. [ x : Pow(A); x : Pow(B) ] ==> x : Pow(A Int B)}


1524 
\end{ttbox}


1525 
The next step replaces the {\tt Pow} by the subset


1526 
relation~($\subseteq$).\index{*PowI}


1527 
\begin{ttbox}


1528 
by (resolve_tac [PowI] 1);


1529 
{\out Level 7}
