author  lcp 
Fri, 09 Sep 1994 11:52:38 +0200  
changeset 595  96c87d5bb015 
parent 498  689e2bd78c19 
child 713  b470cc6326aa 
permissions  rwrr 
104  1 
%% $Id$ 
287  2 
\chapter{ZermeloFraenkel Set Theory} 
317  3 
\index{set theory(} 
4 

5 
The theory~\thydx{ZF} implements ZermeloFraenkel set 

6 
theory~\cite{halmos60,suppes72} as an extension of~{\tt FOL}, classical 

104  7 
firstorder logic. The theory includes a collection of derived natural 
317  8 
deduction rules, for use with Isabelle's classical reasoner. Much 
9 
of it is based on the work of No\"el~\cite{noel}. 

104  10 

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

595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

12 
the basic properties of relations, functions, ordinals and cardinals. 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

13 
Significant results have been proved, such as the Schr\"oderBernstein 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

14 
Theorem, the Wellordering Theorem and a version of Ramsey's Theorem. 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

15 
General methods have been developed for solving recursion equations over 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

16 
monotonic functors; these have been applied to yield constructions of 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

17 
lists, trees, infinite lists, etc. The Recursion Theorem has been proved, 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

18 
admitting recursive definitions of functions over wellfounded relations. 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

19 
Thus, we may even regard set theory as a computational logic, loosely 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

20 
inspired by MartinL\"of's Type Theory. 
104  21 

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

317  23 
namely {\tt hyp_subst_tac}, the simplifier, and the classical reasoner. 
24 
The main simplification set is called {\tt ZF_ss}. Several 

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

26 
{\tt upair_cs} and~{\tt ZF_cs}. 

104  27 

595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

28 
{\tt ZF} has a flexible package for handling inductive definitions, 
111  29 
such as inference systems, and datatype definitions, such as lists and 
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

30 
trees. Moreover it handles coinductive definitions, such as 
317  31 
bisimulation relations, and codatatype definitions, such as streams. A 
595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

32 
recent paper describes the package~\cite{paulsonCADE}, but its examples 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

33 
use an obsolete declaration syntax. Please consult the version of the 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

34 
paper distributed with Isabelle. 
111  35 

317  36 
Recent reports~\cite{paulsonsetI,paulsonsetII} describe {\tt ZF} less 
37 
formally than this chapter. Isabelle employs a novel treatment of 

343  38 
nonwellfounded data structures within the standard {\sc zf} axioms including 
317  39 
the Axiom of Foundation~\cite{paulsonfinal}. 
111  40 

104  41 

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

317  43 
The two main axiom systems for set theory are BernaysG\"odel~({\sc bg}) 
44 
and ZermeloFraenkel~({\sc zf}). Resolution theorem provers can use {\sc 

45 
bg} because it is finite~\cite{boyer86,quaife92}. {\sc zf} does not 

46 
have a finite axiom system because of its Axiom Scheme of Replacement. 

47 
This makes it awkward to use with many theorem provers, since instances 

48 
of the axiom scheme have to be invoked explicitly. Since Isabelle has no 

49 
difficulty with axiom schemes, we may adopt either axiom system. 

104  50 

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

317  52 
collections that are `too big' to be sets. The class of all sets,~$V$, 
53 
cannot be a set without admitting Russell's Paradox. In {\sc bg}, both 

54 
classes and sets are individuals; $x\in V$ expresses that $x$ is a set. In 

55 
{\sc zf}, all variables denote sets; classes are identified with unary 

56 
predicates. The two systems define essentially the same sets and classes, 

57 
with similar properties. In particular, a class cannot belong to another 

58 
class (let alone a set). 

104  59 

317  60 
Modern set theorists tend to prefer {\sc zf} because they are mainly concerned 
61 
with sets, rather than classes. {\sc bg} requires tiresome proofs that various 

104  62 
collections are sets; for instance, showing $x\in\{x\}$ requires showing that 
317  63 
$x$ is a set. 
104  64 

65 

66 
\begin{figure} 

67 
\begin{center} 

68 
\begin{tabular}{rrr} 

111  69 
\it name &\it metatype & \it description \\ 
317  70 
\cdx{0} & $i$ & empty set\\ 
71 
\cdx{cons} & $[i,i]\To i$ & finite set constructor\\ 

72 
\cdx{Upair} & $[i,i]\To i$ & unordered pairing\\ 

73 
\cdx{Pair} & $[i,i]\To i$ & ordered pairing\\ 

74 
\cdx{Inf} & $i$ & infinite set\\ 

75 
\cdx{Pow} & $i\To i$ & powerset\\ 

76 
\cdx{Union} \cdx{Inter} & $i\To i$ & set union/intersection \\ 

77 
\cdx{split} & $[[i,i]\To i, i] \To i$ & generalized projection\\ 

78 
\cdx{fst} \cdx{snd} & $i\To i$ & projections\\ 

79 
\cdx{converse}& $i\To i$ & converse of a relation\\ 

80 
\cdx{succ} & $i\To i$ & successor\\ 

81 
\cdx{Collect} & $[i,i\To o]\To i$ & separation\\ 

82 
\cdx{Replace} & $[i, [i,i]\To o] \To i$ & replacement\\ 

83 
\cdx{PrimReplace} & $[i, [i,i]\To o] \To i$ & primitive replacement\\ 

84 
\cdx{RepFun} & $[i, i\To i] \To i$ & functional replacement\\ 

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

86 
\cdx{domain} & $i\To i$ & domain of a relation\\ 

87 
\cdx{range} & $i\To i$ & range of a relation\\ 

88 
\cdx{field} & $i\To i$ & field of a relation\\ 

89 
\cdx{Lambda} & $[i, i\To i]\To i$ & $\lambda$abstraction\\ 

90 
\cdx{restrict}& $[i, i] \To i$ & restriction of a function\\ 

91 
\cdx{The} & $[i\To o]\To i$ & definite description\\ 

92 
\cdx{if} & $[o,i,i]\To i$ & conditional\\ 

93 
\cdx{Ball} \cdx{Bex} & $[i, i\To o]\To o$ & bounded quantifiers 

104  94 
\end{tabular} 
95 
\end{center} 

96 
\subcaption{Constants} 

97 

98 
\begin{center} 

317  99 
\index{*"`"` symbol} 
100 
\index{*""`"` symbol} 

101 
\index{*"` symbol}\index{function applications!in \ZF} 

102 
\index{*" symbol} 

103 
\index{*": symbol} 

104 
\index{*"<"= symbol} 

104  105 
\begin{tabular}{rrrr} 
317  106 
\it symbol & \it metatype & \it priority & \it description \\ 
111  107 
\tt `` & $[i,i]\To i$ & Left 90 & image \\ 
108 
\tt `` & $[i,i]\To i$ & Left 90 & inverse image \\ 

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

317  110 
\sdx{Int} & $[i,i]\To i$ & Left 70 & intersection ($\inter$) \\ 
111 
\sdx{Un} & $[i,i]\To i$ & Left 65 & union ($\union$) \\ 

111  112 
\tt  & $[i,i]\To i$ & Left 65 & set difference ($$) \\[1ex] 
113 
\tt: & $[i,i]\To o$ & Left 50 & membership ($\in$) \\ 

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

104  115 
\end{tabular} 
116 
\end{center} 

117 
\subcaption{Infixes} 

317  118 
\caption{Constants of {\ZF}} \label{zfconstants} 
104  119 
\end{figure} 
120 

121 

122 
\section{The syntax of set theory} 

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

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

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

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

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

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

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

130 
ZermeloFraenkel set theory. 

131 

498  132 
Figure~\ref{zfconstants} lists the constants and infixes of~\ZF, while 
317  133 
Figure~\ref{zftrans} presents the syntax translations. Finally, 
134 
Figure~\ref{zfsyntax} presents the full grammar for set theory, including 

104  135 
the constructs of \FOL. 
136 

317  137 
Set theory does not use polymorphism. All terms in {\ZF} have 
138 
type~\tydx{i}, which is the type of individuals and lies in class~{\tt 

139 
logic}. The type of firstorder formulae, remember, is~{\tt o}. 

104  140 

317  141 
Infix operators include binary union and intersection ($A\union B$ and 
142 
$A\inter B$), set difference ($AB$), and the subset and membership 

143 
relations. Note that $a$\verb~:$b$ is translated to $\neg(a\in b)$. The 

144 
union and intersection operators ($\bigcup A$ and $\bigcap A$) form the 

145 
union or intersection of a set of sets; $\bigcup A$ means the same as 

146 
$\bigcup@{x\in A}x$. Of these operators, only $\bigcup A$ is primitive. 

104  147 

317  148 
The constant \cdx{Upair} constructs unordered pairs; thus {\tt 
149 
Upair($A$,$B$)} denotes the set~$\{A,B\}$ and {\tt Upair($A$,$A$)} 

150 
denotes the singleton~$\{A\}$. General union is used to define binary 

151 
union. The Isabelle version goes on to define the constant 

152 
\cdx{cons}: 

104  153 
\begin{eqnarray*} 
111  154 
A\cup B & \equiv & \bigcup({\tt Upair}(A,B)) \\ 
155 
{\tt cons}(a,B) & \equiv & {\tt Upair}(a,a) \union B 

104  156 
\end{eqnarray*} 
157 
The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the 

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

159 
\begin{eqnarray*} 

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

161 
\end{eqnarray*} 

162 

317  163 
The constant \cdx{Pair} constructs ordered pairs, as in {\tt 
104  164 
Pair($a$,$b$)}. Ordered pairs may also be written within angle brackets, 
111  165 
as {\tt<$a$,$b$>}. The $n$tuple {\tt<$a@1$,\ldots,$a@{n1}$,$a@n$>} 
317  166 
abbreviates the nest of pairs\par\nobreak 
167 
\centerline{\tt Pair($a@1$,\ldots,Pair($a@{n1}$,$a@n$)\ldots).} 

104  168 

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

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

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

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

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

174 

175 

176 
\begin{figure} 

317  177 
\index{lambda abs@$\lambda$abstractions!in \ZF} 
178 
\index{*""> symbol} 

179 
\index{*"* symbol} 

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

317  195 
\sdx{INT} $x$:$A . B[x]$ & Inter(\{$B[x] . x$:$A$\}) & 
111  196 
\rm general intersection \\ 
317  197 
\sdx{UN} $x$:$A . B[x]$ & Union(\{$B[x] . x$:$A$\}) & 
111  198 
\rm general union \\ 
317  199 
\sdx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x.B[x]$) & 
111  200 
\rm general product \\ 
317  201 
\sdx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x.B[x]$) & 
111  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 \\ 

317  207 
\sdx{THE} $x . P[x]$ & The($\lambda x.P[x]$) & 
111  208 
\rm definite description \\ 
317  209 
\sdx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x.b[x]$) & 
111  210 
\rm $\lambda$abstraction\\[1ex] 
317  211 
\sdx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x.P[x]$) & 
111  212 
\rm bounded $\forall$ \\ 
317  213 
\sdx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x.P[x]$) & 
111  214 
\rm bounded $\exists$ 
104  215 
\end{tabular} 
216 
\end{center} 

317  217 
\caption{Translations for {\ZF}} \label{zftrans} 
104  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)^* " \}" \\ 
317  226 
&  & "< " term\; ("," term)^* " >" \\ 
111  227 
&  & "\{ " id ":" term " . " formula " \}" \\ 
317  228 
&  & "\{ " id " . " id ":" term ", " formula " \}" \\ 
111  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 \\ 
317  246 
&  & term " \ttilde: " term \\ 
111  247 
&  & term " <= " term \\ 
248 
&  & term " = " term \\ 

317  249 
&  & term " \ttilde= " term \\ 
111  250 
&  & "\ttilde\ " formula \\ 
251 
&  & formula " \& " formula \\ 

252 
&  & formula "  " formula \\ 

253 
&  & formula " > " formula \\ 

254 
&  & formula " <> " formula \\ 

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

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

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

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

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

104  260 
\end{array} 
261 
\] 

317  262 
\caption{Full grammar for {\ZF}} \label{zfsyntax} 
104  263 
\end{figure} 
264 

265 

266 
\section{Binding operators} 

317  267 
The constant \cdx{Collect} constructs sets by the principle of {\bf 
104  268 
separation}. The syntax for separation is \hbox{\tt\{$x$:$A$.$P[x]$\}}, 
269 
where $P[x]$ is a formula that may contain free occurrences of~$x$. It 

317  270 
abbreviates the set {\tt Collect($A$,$\lambda x.P[x]$)}, which consists of 
104  271 
all $x\in A$ that satisfy~$P[x]$. Note that {\tt Collect} is an 
272 
unfortunate choice of name: some set theories adopt a setformation 

273 
principle, related to replacement, called collection. 

274 

317  275 
The constant \cdx{Replace} constructs sets by the principle of {\bf 
276 
replacement}. The syntax \hbox{\tt\{$y$.$x$:$A$,$Q[x,y]$\}} denotes the 

277 
set {\tt Replace($A$,$\lambda x\,y.Q[x,y]$)}, which consists of all~$y$ such 

278 
that there exists $x\in A$ satisfying~$Q[x,y]$. The Replacement Axiom has 

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

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

104  281 
predicate is also called a {\bf class function}. 
282 

317  283 
The constant \cdx{RepFun} expresses a special case of replacement, 
104  284 
where $Q[x,y]$ has the form $y=b[x]$. Such a $Q$ is trivially 
285 
singlevalued, since it is just the graph of the metalevel 

287  286 
function~$\lambda x.b[x]$. The resulting set consists of all $b[x]$ 
287 
for~$x\in A$. This is analogous to the \ML{} functional {\tt map}, since 

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

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

290 
x.b[x]$)}. 

104  291 

317  292 
\index{*INT symbol}\index{*UN symbol} 
287  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 

317  304 
has `dependent sets') and calls for similar syntactic conventions. The 
305 
constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and 

104  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]$}. 

317  308 
\index{*SUM symbol}\index{*PROD symbol}% 
104  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 

317  315 
\index{*THE symbol} 
104  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. 

317  322 
Using the constant~\cdx{The}, we may write descriptions as {\tt 
104  323 
The($\lambda x.P[x]$)} or use the syntax \hbox{\tt THE $x$.$P[x]$}. 
324 

317  325 
\index{*lam symbol} 
104  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 

317  329 
constant~\cdx{Lambda}, we may express function sets as {\tt 
104  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*} 

317  334 
\forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ 
335 
\exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] 

104  336 
\end{eqnarray*} 
317  337 
The constants~\cdx{Ball} and~\cdx{Bex} are defined 
104  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  343 
%%%% ZF.thy 
104  344 

345 
\begin{figure} 

346 
\begin{ttbox} 

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

104  349 

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

104  352 

498  353 
\tdx{Union_iff} A : Union(C) <> (EX B:C. A:B) 
354 
\tdx{Pow_iff} A : Pow(B) <> A <= B 

317  355 
\tdx{foundation} A=0  (EX x:A. ALL y:x. ~ y:A) 
104  356 

317  357 
\tdx{replacement} (ALL x:A. ALL y z. P(x,y) & P(x,z) > y=z) ==> 
104  358 
b : PrimReplace(A,P) <> (EX x:A. P(x,b)) 
359 
\subcaption{The ZermeloFraenkel Axioms} 

360 

317  361 
\tdx{Replace_def} Replace(A,P) == 
287  362 
PrimReplace(A, \%x y. (EX!z.P(x,z)) & P(x,y)) 
317  363 
\tdx{RepFun_def} RepFun(A,f) == \{y . x:A, y=f(x)\} 
364 
\tdx{the_def} The(P) == Union(\{y . x:\{0\}, P(y)\}) 

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

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

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

104  368 
\{y. x:Pow(Pow(0)), (x=0 & y=a)  (x=Pow(0) & y=b)\} 
369 
\subcaption{Consequences of replacement} 

370 

317  371 
\tdx{Inter_def} Inter(A) == \{ x:Union(A) . ALL y:A. x:y\} 
372 
\tdx{Un_def} A Un B == Union(Upair(A,B)) 

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

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

104  375 
\subcaption{Union, intersection, difference} 
376 
\end{ttbox} 

317  377 
\caption{Rules and axioms of {\ZF}} \label{zfrules} 
104  378 
\end{figure} 
379 

380 

381 
\begin{figure} 

382 
\begin{ttbox} 

317  383 
\tdx{cons_def} cons(a,A) == Upair(a,a) Un A 
384 
\tdx{succ_def} succ(i) == cons(i,i) 

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

111  386 
\subcaption{Finite and infinite sets} 
387 

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

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

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

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

104  393 
\subcaption{Ordered pairs and Cartesian products} 
394 

317  395 
\tdx{converse_def} converse(r) == \{z. w:r, EX x y. w=<x,y> & z=<y,x>\} 
396 
\tdx{domain_def} domain(r) == \{x. w:r, EX y. w=<x,y>\} 

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

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

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

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

104  401 
\subcaption{Operations on relations} 
402 

317  403 
\tdx{lam_def} Lambda(A,b) == \{<x,b(x)> . x:A\} 
404 
\tdx{apply_def} f`a == THE y. <a,y> : f 

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

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

104  407 
\subcaption{Functions and general product} 
408 
\end{ttbox} 

317  409 
\caption{Further definitions of {\ZF}} \label{zfdefs} 
104  410 
\end{figure} 
411 

412 

413 

414 
\section{The ZermeloFraenkel axioms} 

317  415 
The axioms appear in Fig.\ts \ref{zfrules}. They resemble those 
104  416 
presented by Suppes~\cite{suppes72}. Most of the theory consists of 
417 
definitions. In particular, bounded quantifiers and the subset relation 

418 
appear in other axioms. Objectlevel quantifiers and implications have 

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

343  420 
axioms. See the file {\tt ZF/ZF.thy} for details. 
104  421 

422 
The traditional replacement axiom asserts 

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

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

317  425 
The Isabelle theory defines \cdx{Replace} to apply 
426 
\cdx{PrimReplace} to the singlevalued part of~$P$, namely 

104  427 
\[ (\exists!z.P(x,z)) \conj P(x,y). \] 
428 
Thus $y\in {\tt Replace}(A,P)$ if and only if there is some~$x$ such that 

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

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

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

432 
expands to {\tt Replace}. 

433 

434 
Other consequences of replacement include functional replacement 

317  435 
(\cdx{RepFun}) and definite descriptions (\cdx{The}). 
436 
Axioms for separation (\cdx{Collect}) and unordered pairs 

437 
(\cdx{Upair}) are traditionally assumed, but they actually follow 

104  438 
from replacement~\cite[pages 2378]{suppes72}. 
439 

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

317  441 
the definition of {\tt cons}, which underlies the finite set notation. 
104  442 
The axiom of infinity gives us a set that contains~0 and is closed under 
317  443 
successor (\cdx{succ}). Although this set is not uniquely defined, 
444 
the theory names it (\cdx{Inf}) in order to simplify the 

104  445 
construction of the natural numbers. 
111  446 

317  447 
Further definitions appear in Fig.\ts\ref{zfdefs}. Ordered pairs are 
104  448 
defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$. Recall 
317  449 
that \cdx{Sigma}$(A,B)$ generalizes the Cartesian product of two 
104  450 
sets. It is defined to be the union of all singleton sets 
451 
$\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$. This is a typical usage of 

452 
general union. 

453 

317  454 
The projections \cdx{fst} and~\cdx{snd} are defined in terms of the 
455 
generalized projection \cdx{split}. The latter has been borrowed from 

456 
MartinL\"of's Type Theory, and is often easier to use than \cdx{fst} 

457 
and~\cdx{snd}. 

458 

104  459 
Operations on relations include converse, domain, range, and image. The 
460 
set ${\tt Pi}(A,B)$ generalizes the space of functions between two sets. 

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

317  462 
\cdx{RepFun}) and application (using a definite description). The 
463 
function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only 

104  464 
over the domain~$A$. 
465 

317  466 

467 
%%%% zf.ML 

468 

469 
\begin{figure} 

470 
\begin{ttbox} 

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

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

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

474 

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

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

477 

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

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

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

481 

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

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

484 
\subcaption{Bounded quantifiers} 

485 

486 
\tdx{subsetI} (!!x.x:A ==> x:B) ==> A <= B 

487 
\tdx{subsetD} [ A <= B; c:A ] ==> c:B 

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

489 
\tdx{subset_refl} A <= A 

490 
\tdx{subset_trans} [ A<=B; B<=C ] ==> A<=C 

491 

492 
\tdx{equalityI} [ A <= B; B <= A ] ==> A = B 

493 
\tdx{equalityD1} A = B ==> A<=B 

494 
\tdx{equalityD2} A = B ==> B<=A 

495 
\tdx{equalityE} [ A = B; [ A<=B; B<=A ] ==> P ] ==> P 

496 
\subcaption{Subsets and extensionality} 

497 

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

499 
\tdx{empty_subsetI} 0 <= A 

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

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

502 

503 
\tdx{PowI} A <= B ==> A : Pow(B) 

504 
\tdx{PowD} A : Pow(B) ==> A<=B 

505 
\subcaption{The empty set; power sets} 

506 
\end{ttbox} 

507 
\caption{Basic derived rules for {\ZF}} \label{zflemmas1} 

508 
\end{figure} 

104  509 

510 

511 
\section{From basic lemmas to function spaces} 

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

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

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

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

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

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

518 
instead. 

519 

520 
\subsection{Fundamental lemmas} 

317  521 
Figure~\ref{zflemmas1} presents the derived rules for the most basic 
104  522 
operators. The rules for the bounded quantifiers resemble those for the 
343  523 
ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption 
524 
in the style of Isabelle's classical reasoner. The \rmindex{congruence 

525 
rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's 

104  526 
simplifier, but have few other uses. Congruence rules must be specially 
527 
derived for all binding operators, and henceforth will not be shown. 

528 

317  529 
Figure~\ref{zflemmas1} also shows rules for the subset and equality 
104  530 
relations (proof by extensionality), and rules about the empty set and the 
531 
power set operator. 

532 

317  533 
Figure~\ref{zflemmas2} presents rules for replacement and separation. 
534 
The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than 

104  535 
comparable rules for {\tt PrimReplace} would be. The principle of 
536 
separation is proved explicitly, although most proofs should use the 

317  537 
natural deduction rules for {\tt Collect}. The elimination rule 
538 
\tdx{CollectE} is equivalent to the two destruction rules 

539 
\tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to 

104  540 
particular circumstances. Although too many rules can be confusing, there 
541 
is no reason to aim for a minimal set of rules. See the file 

343  542 
{\tt ZF/ZF.ML} for a complete listing. 
104  543 

317  544 
Figure~\ref{zflemmas3} presents rules for general union and intersection. 
104  545 
The empty intersection should be undefined. We cannot have 
546 
$\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set. All 

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

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

317  549 
arbitrary. The rule \tdx{InterI} must have a premise to exclude 
104  550 
the empty intersection. Some of the laws governing intersections require 
551 
similar premises. 

552 

553 

317  554 
%the [p] gives better page breaking for the book 
555 
\begin{figure}[p] 

556 
\begin{ttbox} 

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

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

559 

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

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

562 
] ==> R 

563 

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

565 
\tdx{RepFunE} [ b : \{f(x). x:A\}; 

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

567 

568 
\tdx{separation} a : \{x:A. P(x)\} <> a:A & P(a) 

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

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

571 
\tdx{CollectD1} a : \{x:A. P(x)\} ==> a:A 

572 
\tdx{CollectD2} a : \{x:A. P(x)\} ==> P(a) 

573 
\end{ttbox} 

574 
\caption{Replacement and separation} \label{zflemmas2} 

575 
\end{figure} 

576 

577 

578 
\begin{figure} 

579 
\begin{ttbox} 

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

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

582 

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

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

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

586 

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

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

589 
] ==> R 

590 

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

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

593 
\end{ttbox} 

594 
\caption{General union and intersection} \label{zflemmas3} 

595 
\end{figure} 

596 

597 

104  598 
%%% upair.ML 
599 

600 
\begin{figure} 

601 
\begin{ttbox} 

317  602 
\tdx{pairing} a:Upair(b,c) <> (a=b  a=c) 
603 
\tdx{UpairI1} a : Upair(a,b) 

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

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

606 
\end{ttbox} 

607 
\caption{Unordered pairs} \label{zfupair1} 

608 
\end{figure} 

609 

104  610 

317  611 
\begin{figure} 
612 
\begin{ttbox} 

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

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

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

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

617 

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

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

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

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

104  622 

317  623 
\tdx{DiffI} [ c : A; ~ c : B ] ==> c : A  B 
624 
\tdx{DiffD1} c : A  B ==> c : A 

498  625 
\tdx{DiffD2} c : A  B ==> c ~: B 
317  626 
\tdx{DiffE} [ c : A  B; [ c:A; ~ c:B ] ==> P ] ==> P 
627 
\end{ttbox} 

628 
\caption{Union, intersection, difference} \label{zfUn} 

629 
\end{figure} 

630 

104  631 

317  632 
\begin{figure} 
633 
\begin{ttbox} 

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

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

636 
\tdx{consCI} (~ a:B ==> a=b) ==> a: cons(b,B) 

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

638 

639 
\tdx{singletonI} a : \{a\} 

640 
\tdx{singletonE} [ a : \{b\}; a=b ==> P ] ==> P 

104  641 
\end{ttbox} 
317  642 
\caption{Finite and singleton sets} \label{zfupair2} 
104  643 
\end{figure} 
644 

645 

646 
\begin{figure} 

647 
\begin{ttbox} 

317  648 
\tdx{succI1} i : succ(i) 
649 
\tdx{succI2} i : j ==> i : succ(j) 

650 
\tdx{succCI} (~ i:j ==> i=j) ==> i: succ(j) 

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

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

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

654 
\end{ttbox} 

655 
\caption{The successor function} \label{zfsucc} 

656 
\end{figure} 

104  657 

658 

317  659 
\begin{figure} 
660 
\begin{ttbox} 

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

662 
\tdx{theI} EX! x. P(x) ==> P(THE x. P(x)) 

104  663 

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

104  666 

461  667 
\tdx{mem_asym} [ a:b; b:a ] ==> P 
668 
\tdx{mem_irrefl} a:a ==> P 

104  669 
\end{ttbox} 
317  670 
\caption{Descriptions; noncircularity} \label{zfthe} 
104  671 
\end{figure} 
672 

673 

674 
\subsection{Unordered pairs and finite sets} 

317  675 
Figure~\ref{zfupair1} presents the principle of unordered pairing, along 
104  676 
with its derived rules. Binary union and intersection are defined in terms 
317  677 
of ordered pairs (Fig.\ts\ref{zfUn}). Set difference is also included. The 
678 
rule \tdx{UnCI} is useful for classical reasoning about unions, 

679 
like {\tt disjCI}\@; it supersedes \tdx{UnI1} and 

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

104  681 
intersection and difference we have both elimination and destruction rules. 
682 
Again, there is no reason to provide a minimal rule set. 

683 

317  684 
Figure~\ref{zfupair2} is concerned with finite sets: it presents rules 
685 
for~{\tt cons}, the finite set constructor, and rules for singleton 

686 
sets. Figure~\ref{zfsucc} presents derived rules for the successor 

687 
function, which is defined in terms of~{\tt cons}. The proof that {\tt 

688 
succ} is injective appears to require the Axiom of Foundation. 

104  689 

317  690 
Definite descriptions (\sdx{THE}) are defined in terms of the singleton 
691 
set~$\{0\}$, but their derived rules fortunately hide this 

692 
(Fig.\ts\ref{zfthe}). The rule~\tdx{theI} is difficult to apply 

693 
because of the two occurrences of~$\Var{P}$. However, 

694 
\tdx{the_equality} does not have this problem and the files contain 

695 
many examples of its use. 

104  696 

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

461  698 
(\tdx{mem_asym}) is proved by applying the Axiom of Foundation to 
104  699 
the set $\{a,b\}$. The impossibility of $a\in a$ is a trivial consequence. 
700 

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

104  703 

704 

705 
%%% subset.ML 

706 

707 
\begin{figure} 

708 
\begin{ttbox} 

317  709 
\tdx{Union_upper} B:A ==> B <= Union(A) 
710 
\tdx{Union_least} [ !!x. x:A ==> x<=C ] ==> Union(A) <= C 

104  711 

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

104  714 

317  715 
\tdx{Un_upper1} A <= A Un B 
716 
\tdx{Un_upper2} B <= A Un B 

717 
\tdx{Un_least} [ A<=C; B<=C ] ==> A Un B <= C 

104  718 

317  719 
\tdx{Int_lower1} A Int B <= A 
720 
\tdx{Int_lower2} A Int B <= B 

721 
\tdx{Int_greatest} [ C<=A; C<=B ] ==> C <= A Int B 

104  722 

317  723 
\tdx{Diff_subset} AB <= A 
724 
\tdx{Diff_contains} [ C<=A; C Int B = 0 ] ==> C <= AB 

104  725 

317  726 
\tdx{Collect_subset} Collect(A,P) <= A 
104  727 
\end{ttbox} 
317  728 
\caption{Subset and lattice properties} \label{zfsubset} 
104  729 
\end{figure} 
730 

731 

732 
\subsection{Subset and lattice properties} 

317  733 
The subset relation is a complete lattice. Unions form least upper bounds; 
734 
nonempty intersections form greatest lower bounds. Figure~\ref{zfsubset} 

735 
shows the corresponding rules. A few other laws involving subsets are 

736 
included. Proofs are in the file {\tt ZF/subset.ML}. 

737 

738 
Reasoning directly about subsets often yields clearer proofs than 

739 
reasoning about the membership relation. Section~\ref{sec:ZFpowexample} 

740 
below presents an example of this, proving the equation ${{\tt Pow}(A)\cap 

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

104  742 

743 
%%% pair.ML 

744 

745 
\begin{figure} 

746 
\begin{ttbox} 

317  747 
\tdx{Pair_inject1} <a,b> = <c,d> ==> a=c 
748 
\tdx{Pair_inject2} <a,b> = <c,d> ==> b=d 

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

750 
\tdx{Pair_neq_0} <a,b>=0 ==> P 

104  751 

349  752 
\tdx{fst_conv} fst(<a,b>) = a 
753 
\tdx{snd_conv} snd(<a,b>) = b 

317  754 
\tdx{split} split(\%x y.c(x,y), <a,b>) = c(a,b) 
104  755 

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

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

104  760 

317  761 
\tdx{SigmaE2} [ <a,b> : Sigma(A,B); 
762 
[ a:A; b:B(a) ] ==> P ] ==> P 

104  763 
\end{ttbox} 
317  764 
\caption{Ordered pairs; projections; general sums} \label{zfpair} 
104  765 
\end{figure} 
766 

767 

768 
\subsection{Ordered pairs} 

317  769 
Figure~\ref{zfpair} presents the rules governing ordered pairs, 
287  770 
projections and general sums. File {\tt ZF/pair.ML} contains the 
104  771 
full (and tedious) proof that $\{\{a\},\{a,b\}\}$ functions as an ordered 
772 
pair. This property is expressed as two destruction rules, 

317  773 
\tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently 
774 
as the elimination rule \tdx{Pair_inject}. 

104  775 

317  776 
The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$. This 
114  777 
is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other 
343  778 
encodings of ordered pairs. The nonstandard ordered pairs mentioned below 
114  779 
satisfy $\pair{\emptyset;\emptyset}=\emptyset$. 
104  780 

317  781 
The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE} 
782 
assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form 

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

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

786 

787 

788 
%%% domrange.ML 

789 

790 
\begin{figure} 

791 
\begin{ttbox} 

317  792 
\tdx{domainI} <a,b>: r ==> a : domain(r) 
793 
\tdx{domainE} [ a : domain(r); !!y. <a,y>: r ==> P ] ==> P 

794 
\tdx{domain_subset} domain(Sigma(A,B)) <= A 

104  795 

317  796 
\tdx{rangeI} <a,b>: r ==> b : range(r) 
797 
\tdx{rangeE} [ b : range(r); !!x. <x,b>: r ==> P ] ==> P 

798 
\tdx{range_subset} range(A*B) <= B 

104  799 

317  800 
\tdx{fieldI1} <a,b>: r ==> a : field(r) 
801 
\tdx{fieldI2} <a,b>: r ==> b : field(r) 

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

104  803 

317  804 
\tdx{fieldE} [ a : field(r); 
104  805 
!!x. <a,x>: r ==> P; 
806 
!!x. <x,a>: r ==> P 

807 
] ==> P 

808 

317  809 
\tdx{field_subset} field(A*A) <= A 
810 
\end{ttbox} 

811 
\caption{Domain, range and field of a relation} \label{zfdomrange} 

812 
\end{figure} 

104  813 

317  814 
\begin{figure} 
815 
\begin{ttbox} 

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

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

818 

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

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

104  821 
\end{ttbox} 
317  822 
\caption{Image and inverse image} \label{zfdomrange2} 
104  823 
\end{figure} 
824 

825 

826 
\subsection{Relations} 

317  827 
Figure~\ref{zfdomrange} presents rules involving relations, which are sets 
104  828 
of ordered pairs. The converse of a relation~$r$ is the set of all pairs 
829 
$\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then 

317  830 
{\cdx{converse}$(r)$} is its inverse. The rules for the domain 
343  831 
operation, namely \tdx{domainI} and~\tdx{domainE}, assert that 
832 
\cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains 

104  833 
some pair of the form~$\pair{x,y}$. The range operation is similar, and 
317  834 
the field of a relation is merely the union of its domain and range. 
835 

836 
Figure~\ref{zfdomrange2} presents rules for images and inverse images. 

343  837 
Note that these operations are generalisations of range and domain, 
317  838 
respectively. See the file {\tt ZF/domrange.ML} for derivations of the 
839 
rules. 

104  840 

841 

842 
%%% func.ML 

843 

844 
\begin{figure} 

845 
\begin{ttbox} 

317  846 
\tdx{fun_is_rel} f: Pi(A,B) ==> f <= Sigma(A,B) 
104  847 

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

104  850 

317  851 
\tdx{apply_type} [ f: Pi(A,B); a:A ] ==> f`a : B(a) 
852 
\tdx{apply_Pair} [ f: Pi(A,B); a:A ] ==> <a,f`a>: f 

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

104  854 

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

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

104  860 

317  861 
\tdx{Pi_type} [ f: A>C; !!x. x:A ==> f`x: B(x) ] ==> f: Pi(A,B) 
862 
\tdx{domain_of_fun} f: Pi(A,B) ==> domain(f)=A 

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

104  864 

317  865 
\tdx{restrict} a : A ==> restrict(f,A) ` a = f`a 
866 
\tdx{restrict_type} [ !!x. x:A ==> f`x: B(x) ] ==> 

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

104  868 
\end{ttbox} 
317  869 
\caption{Functions} \label{zffunc1} 
104  870 
\end{figure} 
871 

872 

873 
\begin{figure} 

874 
\begin{ttbox} 

317  875 
\tdx{lamI} a:A ==> <a,b(a)> : (lam x:A. b(x)) 
876 
\tdx{lamE} [ p: (lam x:A. b(x)); !!x.[ x:A; p=<x,b(x)> ] ==> P 

877 
] ==> P 

878 

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

104  880 

317  881 
\tdx{beta} a : A ==> (lam x:A.b(x)) ` a = b(a) 
882 
\tdx{eta} f : Pi(A,B) ==> (lam x:A. f`x) = f 

883 
\end{ttbox} 

884 
\caption{$\lambda$abstraction} \label{zflam} 

885 
\end{figure} 

886 

887 

888 
\begin{figure} 

889 
\begin{ttbox} 

890 
\tdx{fun_empty} 0: 0>0 

891 
\tdx{fun_single} \{<a,b>\} : \{a\} > \{b\} 

892 

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

104  894 
(f Un g) : (A Un C) > (B Un D) 
895 

317  896 
\tdx{fun_disjoint_apply1} [ a:A; f: A>B; g: C>D; A Int C = 0 ] ==> 
104  897 
(f Un g)`a = f`a 
898 

317  899 
\tdx{fun_disjoint_apply2} [ c:C; f: A>B; g: C>D; A Int C = 0 ] ==> 
104  900 
(f Un g)`c = g`c 
901 
\end{ttbox} 

317  902 
\caption{Constructing functions from smaller sets} \label{zffunc2} 
104  903 
\end{figure} 
904 

905 

906 
\subsection{Functions} 

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

317  908 
about. The file {\tt ZF/func.ML} derives many rules, which overlap more 
909 
than they ought. This section presents the more important rules. 

104  910 

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

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

922 

317  923 
Among the laws for $\lambda$abstraction, \tdx{lamI} and \tdx{lamE} 
924 
describe the graph of the generated function, while \tdx{beta} and 

925 
\tdx{eta} are the standard conversions. We essentially have a 

926 
dependentlytyped $\lambda$calculus (Fig.\ts\ref{zflam}). 

104  927 

317  928 
Figure~\ref{zffunc2} presents some rules that can be used to construct 
104  929 
functions explicitly. We start with functions consisting of at most one 
930 
pair, and may form the union of two functions provided their domains are 

931 
disjoint. 

932 

933 

934 
\begin{figure} 

935 
\begin{ttbox} 

317  936 
\tdx{Int_absorb} A Int A = A 
937 
\tdx{Int_commute} A Int B = B Int A 

938 
\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C) 

939 
\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) 

104  940 

317  941 
\tdx{Un_absorb} A Un A = A 
942 
\tdx{Un_commute} A Un B = B Un A 

943 
\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C) 

944 
\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) 

104  945 

317  946 
\tdx{Diff_cancel} AA = 0 
947 
\tdx{Diff_disjoint} A Int (BA) = 0 

948 
\tdx{Diff_partition} A<=B ==> A Un (BA) = B 

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

950 
\tdx{Diff_Un} A  (B Un C) = (AB) Int (AC) 

951 
\tdx{Diff_Int} A  (B Int C) = (AB) Un (AC) 

104  952 

317  953 
\tdx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B) 
954 
\tdx{Inter_Un_distrib} [ a:A; b:B ] ==> 

104  955 
Inter(A Un B) = Inter(A) Int Inter(B) 
956 

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

317  959 
\tdx{Un_Inter_RepFun} b:B ==> 
104  960 
A Un Inter(B) = (INT C:B. A Un C) 
961 

317  962 
\tdx{SUM_Un_distrib1} (SUM x:A Un B. C(x)) = 
104  963 
(SUM x:A. C(x)) Un (SUM x:B. C(x)) 
964 

317  965 
\tdx{SUM_Un_distrib2} (SUM x:C. A(x) Un B(x)) = 
104  966 
(SUM x:C. A(x)) Un (SUM x:C. B(x)) 
967 

317  968 
\tdx{SUM_Int_distrib1} (SUM x:A Int B. C(x)) = 
104  969 
(SUM x:A. C(x)) Int (SUM x:B. C(x)) 
970 

317  971 
\tdx{SUM_Int_distrib2} (SUM x:C. A(x) Int B(x)) = 
104  972 
(SUM x:C. A(x)) Int (SUM x:C. B(x)) 
973 
\end{ttbox} 

974 
\caption{Equalities} \label{zfequalities} 

975 
\end{figure} 

976 

111  977 

978 
\begin{figure} 

317  979 
%\begin{constants} 
980 
% \cdx{1} & $i$ & & $\{\emptyset\}$ \\ 

981 
% \cdx{bool} & $i$ & & the set $\{\emptyset,1\}$ \\ 

982 
% \cdx{cond} & $[i,i,i]\To i$ & & conditional for {\tt bool} \\ 

983 
% \cdx{not} & $i\To i$ & & negation for {\tt bool} \\ 

984 
% \sdx{and} & $[i,i]\To i$ & Left 70 & conjunction for {\tt bool} \\ 

985 
% \sdx{or} & $[i,i]\To i$ & Left 65 & disjunction for {\tt bool} \\ 

986 
% \sdx{xor} & $[i,i]\To i$ & Left 65 & exclusiveor for {\tt bool} 

987 
%\end{constants} 

988 
% 

111  989 
\begin{ttbox} 
317  990 
\tdx{bool_def} bool == \{0,1\} 
991 
\tdx{cond_def} cond(b,c,d) == if(b=1,c,d) 

992 
\tdx{not_def} not(b) == cond(b,0,1) 

993 
\tdx{and_def} a and b == cond(a,b,0) 

994 
\tdx{or_def} a or b == cond(a,1,b) 

995 
\tdx{xor_def} a xor b == cond(a,not(b),b) 

996 

997 
\tdx{bool_1I} 1 : bool 

998 
\tdx{bool_0I} 0 : bool 

999 
\tdx{boolE} [ c: bool; c=1 ==> P; c=0 ==> P ] ==> P 

1000 
\tdx{cond_1} cond(1,c,d) = c 

1001 
\tdx{cond_0} cond(0,c,d) = d 

1002 
\end{ttbox} 

1003 
\caption{The booleans} \label{zfbool} 

1004 
\end{figure} 

1005 

1006 

1007 
\section{Further developments} 

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

1009 
highlights can be covered here. It involves many theories and ML files of 

1010 
proofs. 

1011 

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

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

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

1015 

1016 
Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the 

1017 
usual operators including a conditional (Fig.\ts\ref{zfbool}). Although 

1018 
{\ZF} is a firstorder theory, you can obtain the effect of higherorder 

1019 
logic using {\tt bool}valued functions, for example. The constant~{\tt1} 

1020 
is translated to {\tt succ(0)}. 

1021 

1022 
\begin{figure} 

1023 
\index{*"+ symbol} 

1024 
\begin{constants} 

343  1025 
\it symbol & \it metatype & \it priority & \it description \\ 
317  1026 
\tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\ 
1027 
\cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\ 

1028 
\cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$ 

1029 
\end{constants} 

1030 
\begin{ttbox} 

1031 
\tdx{sum_def} A+B == \{0\}*A Un \{1\}*B 

1032 
\tdx{Inl_def} Inl(a) == <0,a> 

1033 
\tdx{Inr_def} Inr(b) == <1,b> 

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

1035 

1036 
\tdx{sum_InlI} a : A ==> Inl(a) : A+B 

1037 
\tdx{sum_InrI} b : B ==> Inr(b) : A+B 

1038 

1039 
\tdx{Inl_inject} Inl(a)=Inl(b) ==> a=b 

1040 
\tdx{Inr_inject} Inr(a)=Inr(b) ==> a=b 

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

1042 

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

1044 

1045 
\tdx{case_Inl} case(c,d,Inl(a)) = c(a) 

1046 
\tdx{case_Inr} case(c,d,Inr(b)) = d(b) 

1047 
\end{ttbox} 

1048 
\caption{Disjoint unions} \label{zfsum} 

1049 
\end{figure} 

1050 

1051 

1052 
Theory \thydx{Sum} defines the disjoint union of two sets, with 

1053 
injections and a case analysis operator (Fig.\ts\ref{zfsum}). Disjoint 

1054 
unions play a role in datatype definitions, particularly when there is 

1055 
mutual recursion~\cite{paulsonsetII}. 

1056 

1057 
\begin{figure} 

1058 
\begin{ttbox} 

1059 
\tdx{QPair_def} <a;b> == a+b 

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

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

461  1062 
\tdx{qconverse_def} qconverse(r) == \{z. w:r, EX x y. w=<x;y> & z=<y;x>\} 
1063 
\tdx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). \{<x;y>\} 

317  1064 

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

1066 
\tdx{QInl_def} QInl(a) == <0;a> 

1067 
\tdx{QInr_def} QInr(b) == <1;b> 

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

1069 
\end{ttbox} 

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

1071 
\end{figure} 

1072 

1073 
Theory \thydx{QPair} defines a notion of ordered pair that admits 

1074 
nonwellfounded tupling (Fig.\ts\ref{zfqpair}). Such pairs are written 

1075 
{\tt<$a$;$b$>}. It also defines the eliminator \cdx{qsplit}, the 

1076 
converse operator \cdx{qconverse}, and the summation operator 

1077 
\cdx{QSigma}. These are completely analogous to the corresponding 

1078 
versions for standard ordered pairs. The theory goes on to define a 

1079 
nonstandard notion of disjoint sum using nonstandard pairs. All of these 

1080 
concepts satisfy the same properties as their standard counterparts; in 

1081 
addition, {\tt<$a$;$b$>} is continuous. The theory supports coinductive 

1082 
definitions, for example of infinite lists~\cite{paulsonfinal}. 

1083 

1084 
\begin{figure} 

1085 
\begin{ttbox} 

1086 
\tdx{bnd_mono_def} bnd_mono(D,h) == 

111  1087 
h(D)<=D & (ALL W X. W<=X > X<=D > h(W) <= h(X)) 
1088 

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

317  1091 

111  1092 

317  1093 
\tdx{lfp_lowerbound} [ h(A) <= A; A<=D ] ==> lfp(D,h) <= A 
111  1094 

317  1095 
\tdx{lfp_subset} lfp(D,h) <= D 
111  1096 

317  1097 
\tdx{lfp_greatest} [ bnd_mono(D,h); 
111  1098 
!!X. [ h(X) <= X; X<=D ] ==> A<=X 
1099 
] ==> A <= lfp(D,h) 

1100 

317  1101 
\tdx{lfp_Tarski} bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h)) 
111  1102 

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

1106 

317  1107 
\tdx{lfp_mono} [ bnd_mono(D,h); bnd_mono(E,i); 
111  1108 
!!X. X<=D ==> h(X) <= i(X) 
1109 
] ==> lfp(D,h) <= lfp(E,i) 

1110 

317  1111 
\tdx{gfp_upperbound} [ A <= h(A); A<=D ] ==> A <= gfp(D,h) 
111  1112 

317  1113 
\tdx{gfp_subset} gfp(D,h) <= D 
111  1114 

317  1115 
\tdx{gfp_least} [ bnd_mono(D,h); 
111  1116 
!!X. [ X <= h(X); X<=D ] ==> X<=A 
1117 
] ==> gfp(D,h) <= A 

1118 

317  1119 
\tdx{gfp_Tarski} bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h)) 
111  1120 

317  1121 
\tdx{coinduct} [ bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D 
111  1122 
] ==> a : gfp(D,h) 
1123 

317  1124 
\tdx{gfp_mono} [ bnd_mono(D,h); D <= E; 
111  1125 
!!X. X<=D ==> h(X) <= i(X) 
1126 
] ==> gfp(D,h) <= gfp(E,i) 

1127 
\end{ttbox} 

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

1129 
\end{figure} 

1130 

317  1131 
The KnasterTarski Theorem states that every monotone function over a 
1132 
complete lattice has a fixedpoint. Theory \thydx{Fixedpt} proves the 

1133 
Theorem only for a particular lattice, namely the lattice of subsets of a 

1134 
set (Fig.\ts\ref{zffixedpt}). The theory defines least and greatest 

1135 
fixedpoint operators with corresponding induction and coinduction rules. 

1136 
These are essential to many definitions that follow, including the natural 

1137 
numbers and the transitive closure operator. The (co)inductive definition 

595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1138 
package also uses the fixedpoint operators~\cite{paulsonCADE}. See 
317  1139 
Davey and Priestley~\cite{davey&priestley} for more on the KnasterTarski 
1140 
Theorem and my paper~\cite{paulsonsetII} for discussion of the Isabelle 

1141 
proofs. 

1142 

1143 
Monotonicity properties are proved for most of the setforming operations: 

1144 
union, intersection, Cartesian product, image, domain, range, etc. These 

1145 
are useful for applying the KnasterTarski Fixedpoint Theorem. The proofs 

1146 
themselves are trivial applications of Isabelle's classical reasoner. See 

1147 
file {\tt ZF/mono.ML}. 

1148 

111  1149 

104  1150 
\begin{figure} 
317  1151 
\begin{constants} 
1152 
\it symbol & \it metatype & \it priority & \it description \\ 

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

349  1154 
\cdx{id} & $i\To i$ & & identity function \\ 
317  1155 
\cdx{inj} & $[i,i]\To i$ & & injective function space\\ 
1156 
\cdx{surj} & $[i,i]\To i$ & & surjective function space\\ 

1157 
\cdx{bij} & $[i,i]\To i$ & & bijective function space 

1158 
\end{constants} 

1159 

104  1160 
\begin{ttbox} 
317  1161 
\tdx{comp_def} r O s == \{xz : domain(s)*range(r) . 
104  1162 
EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r\} 
317  1163 
\tdx{id_def} id(A) == (lam x:A. x) 
1164 
\tdx{inj_def} inj(A,B) == \{ f: A>B. ALL w:A. ALL x:A. f`w=f`x > w=x\} 

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

1166 
\tdx{bij_def} bij(A,B) == inj(A,B) Int surj(A,B) 

104  1167 

317  1168 

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

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

104  1171 
f`(converse(f)`b) = b 
1172 

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

104  1175 

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

104  1178 

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

104  1181 

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

104  1184 

317  1185 
\tdx{comp_inj} [ g:inj(A,B); f:inj(B,C) ] ==> (f O g):inj(A,C) 
1186 
\tdx{comp_surj} [ g:surj(A,B); f:surj(B,C) ] ==> (f O g):surj(A,C) 

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

104  1188 

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

104  1191 

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

1195 

317  1196 
\tdx{restrict_bij} [ f:inj(A,B); C<=A ] ==> restrict(f,C): bij(C, f``C) 
104  1197 
\end{ttbox} 
1198 
\caption{Permutations} \label{zfperm} 

1199 
\end{figure} 

1200 

317  1201 
The theory \thydx{Perm} is concerned with permutations (bijections) and 
1202 
related concepts. These include composition of relations, the identity 

1203 
relation, and three specialized function spaces: injective, surjective and 

1204 
bijective. Figure~\ref{zfperm} displays many of their properties that 

1205 
have been proved. These results are fundamental to a treatment of 

1206 
equipollence and cardinality. 

104  1207 

1208 
\begin{figure} 

317  1209 
\index{#*@{\tt\#*} symbol} 
1210 
\index{*div symbol} 

1211 
\index{*mod symbol} 

1212 
\index{#+@{\tt\#+} symbol} 

1213 
\index{#@{\tt\#} symbol} 

1214 
\begin{constants} 

1215 
\it symbol & \it metatype & \it priority & \it description \\ 

1216 
\cdx{nat} & $i$ & & set of natural numbers \\ 

1217 
\cdx{nat_case}& $[i,i\To i,i]\To i$ & & conditional for $nat$\\ 

1218 
\cdx{rec} & $[i,i,[i,i]\To i]\To i$ & & recursor for $nat$\\ 

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

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

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

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

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

1224 
\end{constants} 

111  1225 

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

1228 

1229 
\tdx{nat_case_def} nat_case(a,b,k) == 

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

1231 

1232 
\tdx{rec_def} rec(k,a,b) == 

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

1234 

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

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

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

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

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

111  1240 

1241 

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

104  1244 

317  1245 
\tdx{nat_induct} 
104  1246 
[ n: nat; P(0); !!x. [ x: nat; P(x) ] ==> P(succ(x)) 
1247 
] ==> P(n) 

1248 

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

104  1251 

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

104  1254 

317  1255 
\tdx{mult_type} [ m:nat; n:nat ] ==> m #* n : nat 
1256 
\tdx{mult_0} 0 #* n = 0 

1257 
\tdx{mult_succ} succ(m) #* n = n #+ (m #* n) 

1258 
\tdx{mult_commute} [ m:nat; n:nat ] ==> m #* n = n #* m 

1259 
\tdx{add_mult_dist} 

104  1260 
[ m:nat; k:nat ] ==> (m #+ n) #* k = (m #* k) #+ (n #* k) 
317  1261 
\tdx{mult_assoc} 
104  1262 
[ m:nat; n:nat; k:nat ] ==> (m #* n) #* k = m #* (n #* k) 
317  1263 
\tdx{mod_quo_equality} 
104  1264 
[ 0:n; m:nat; n:nat ] ==> (m div n)#*n #+ m mod n = m 
1265 
\end{ttbox} 

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

1267 
\end{figure} 

1268 

317  1269 
Theory \thydx{Nat} defines the natural numbers and mathematical 
1270 
induction, along with a case analysis operator. The set of natural 

1271 
numbers, here called {\tt nat}, is known in set theory as the ordinal~$\omega$. 

1272 

1273 
Theory \thydx{Arith} defines primitive recursion and goes on to develop 

1274 
arithmetic on the natural numbers (Fig.\ts\ref{zfnat}). It defines 

1275 
addition, multiplication, subtraction, division, and remainder. Many of 

1276 
their properties are proved: commutative, associative and distributive 

1277 
laws, identity and cancellation laws, etc. The most interesting result is 

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

1279 
remainder are defined by repeated subtraction, which requires wellfounded 

1280 
rather than primitive recursion; the termination argument relies on the 

1281 
divisor's being nonzero. 

1282 

1283 
Theory \thydx{Univ} defines a `universe' ${\tt univ}(A)$, for 

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

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

1286 
univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$. This theory also 

1287 
defines the cumulative hierarchy of axiomatic set theory, which 

1288 
traditionally is written $V@\alpha$ for an ordinal~$\alpha$. The 

1289 
`universe' is a simple generalization of~$V@\omega$. 

1290 

1291 
Theory \thydx{QUniv} defines a `universe' ${\tt quniv}(A)$, for 

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

1293 
univ}(A)$ (and is defined in terms of it) but is closed under the 

1294 
nonstandard product and sum. 

1295 

595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1296 
Theory {\tt Finite} (Figure~\ref{zffin}) defines the finite set operator; 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1297 
${\tt Fin}(A)$ is the set of all finite sets over~$A$. The theory employs 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1298 
Isabelle's inductive definition package, which proves various rules 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1299 
automatically. The induction rule shown is stronger than the one proved by 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1300 
the package. The theory also defines the set of all finite functions 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1301 
between two given sets. 
317  1302 

111  1303 
\begin{figure} 
1304 
\begin{ttbox} 

595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1305 
\tdx{Fin.emptyI} 0 : Fin(A) 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1306 
\tdx{Fin.consI} [ a: A; b: Fin(A) ] ==> cons(a,b) : Fin(A) 
111  1307 

317  1308 
\tdx{Fin_induct} 
111  1309 
[ b: Fin(A); 
1310 
P(0); 

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

1312 
] ==> P(b) 

1313 

317  1314 
\tdx{Fin_mono} A<=B ==> Fin(A) <= Fin(B) 
1315 
\tdx{Fin_UnI} [ b: Fin(A); c: Fin(A) ] ==> b Un c : Fin(A) 

1316 
\tdx{Fin_UnionI} C : Fin(Fin(A)) ==> Union(C) : Fin(A) 

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

111  1318 
\end{ttbox} 
1319 
\caption{The finite set operator} \label{zffin} 

1320 
\end{figure} 

1321 

317  1322 
\begin{figure} 
1323 
\begin{constants} 

1324 
\cdx{list} & $i\To i$ && lists over some set\\ 

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

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

1327 
\cdx{map} & $[i\To i, i] \To i$ & & mapping functional\\ 

1328 
\cdx{length} & $i\To i$ & & length of a list\\ 

1329 
\cdx{rev} & $i\To i$ & & reverse of a list\\ 

1330 
\tt \at & $[i,i]\To i$ & Right 60 & append for lists\\ 

1331 
\cdx{flat} & $i\To i$ & & append of list of lists 

1332 
\end{constants} 

1333 

1334 
\underscoreon %%because @ is used here 

104  1335 
\begin{ttbox} 
317  1336 
\tdx{list_rec_def} list_rec(l,c,h) == 
287  1337 
Vrec(l, \%l g.list_case(c, \%x xs. h(x, xs, g`xs), l)) 
104  1338 

317  1339 
\tdx{map_def} map(f,l) == list_rec(l, 0, \%x xs r. <f(x), r>) 
1340 
\tdx{length_def} length(l) == list_rec(l, 0, \%x xs r. succ(r)) 

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

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

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

104  1344 

1345 

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

1348 

1349 
\tdx{List.induct} 

104  1350 
[ l: list(A); 
111  1351 
P(Nil); 
1352 
!!x y. [ x: A; y: list(A); P(y) ] ==> P(Cons(x,y)) 

104  1353 
] ==> P(l) 
1354 

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

104  1357 

317  1358 
\tdx{list_mono} A<=B ==> list(A) <= list(B) 
111  1359 

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

104  1362 

317  1363 
\tdx{map_ident} l: list(A) ==> map(\%u.u, l) = l 
1364 
\tdx{map_compose} l: list(A) ==> map(h, map(j,l)) = map(\%u.h(j(u)), l) 

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

1366 
\tdx{map_type} 

104  1367 
[ l: list(A); !!x. x: A ==> h(x): B ] ==> map(h,l) : list(B) 
317  1368 
\tdx{map_flat} 
104  1369 
ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls)) 
1370 
\end{ttbox} 

1371 
\caption{Lists} \label{zflist} 

1372 
\end{figure} 

1373 

111  1374 

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

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

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

343  1378 
and case operator (\verblist_case). See file {\tt ZF/List.ML}. 
1379 
The file {\tt ZF/ListFn.thy} proceeds to define structural 

111  1380 
recursion and the usual list functions. 
104  1381 

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

317  1383 
operators for handling recursive function definitions. I have described 
1384 
the developments in detail elsewhere~\cite{paulsonsetII}. Here is a brief 

1385 
summary: 

1386 
\begin{itemize} 

1387 
\item Theory {\tt Trancl} defines the transitive closure of a relation 

1388 
(as a least fixedpoint). 

104  1389 

317  1390 
\item Theory {\tt WF} proves the WellFounded Recursion Theorem, using an 
1391 
elegant approach of Tobias Nipkow. This theorem permits general 

1392 
recursive definitions within set theory. 

1393 

1394 
\item Theory {\tt Ord} defines the notions of transitive set and ordinal 

1395 
number. It derives transfinite induction. A key definition is {\bf 

1396 
less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and 

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

1398 
numbers. 

104  1399 

317  1400 
\item Theory {\tt Epsilon} derives $\epsilon$induction and 
343  1401 
$\epsilon$recursion, which are generalisations of transfinite 
1402 
induction and recursion. It also defines \cdx{rank}$(x)$, which is the 

1403 
least ordinal $\alpha$ such that $x$ is constructed at stage $\alpha$ 

1404 
of the cumulative hierarchy (thus $x\in V@{\alpha+1}$). 

317  1405 
\end{itemize} 
1406 

595
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1407 
Other important theories lead to a theory of cardinal numbers. They have 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1408 
not yet been written up anywhere. Here is a summary: 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1409 
\begin{itemize} 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1410 
\item Theory {\tt Rel} defines the basic properties of relations, such as 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1411 
(ir)reflexivity, (a)symmetry, and transitivity. 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1412 

96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1413 
\item Theory {\tt EquivClass} develops a theory of equivalence 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1414 
classes, not using the Axiom of Choice. 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1415 

96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp
parents:
498
diff
changeset

1416 
\item Theory {\tt Order} defines partial orderings, total orderings and 
96c87d5bb015
Added mention of directory IMP; tidied the section on examples.
lcp< 