doc-src/Logics/ZF.tex
 author paulson Fri Feb 16 18:00:47 1996 +0100 (1996-02-16) changeset 1512 ce37c64244c0 parent 1449 25a7ddf9c080 child 2495 82ec47e0a8d3 permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 %% $Id$

     2 \chapter{Zermelo-Fraenkel Set Theory}

     3 \index{set theory|(}

     4

     5 The theory~\thydx{ZF} implements Zermelo-Fraenkel set

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

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

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

     9 of it is based on the work of No\"el~\cite{noel}.

    10

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

    12 the basic properties of relations, functions, ordinals and cardinals.

    13 Significant results have been proved, such as the Schr\"oder-Bernstein

    14 Theorem, the Wellordering Theorem and a version of Ramsey's Theorem.

    15 General methods have been developed for solving recursion equations over

    16 monotonic functors; these have been applied to yield constructions of

    17 lists, trees, infinite lists, etc.  The Recursion Theorem has been proved,

    18 admitting recursive definitions of functions over well-founded relations.

    19 Thus, we may even regard set theory as a computational logic, loosely

    20 inspired by Martin-L\"of's Type Theory.

    21

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

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

    27

    28 {\tt ZF} has a flexible package for handling inductive definitions,

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

    30 trees.  Moreover it handles coinductive definitions, such as

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

    32 recent paper describes the package~\cite{paulson-CADE}, but its examples

    33 use an obsolete declaration syntax.  Please consult the version of the

    34 paper distributed with Isabelle.

    35

    36 Recent reports~\cite{paulson-set-I,paulson-set-II} describe {\tt ZF} less

    37 formally than this chapter.  Isabelle employs a novel treatment of

    38 non-well-founded data structures within the standard {\sc zf} axioms including

    39 the Axiom of Foundation~\cite{paulson-final}.

    40

    41

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

    43 The two main axiom systems for set theory are Bernays-G\"odel~({\sc bg})

    44 and Zermelo-Fraenkel~({\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.

    50

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

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

    59

    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

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

    63 $x$ is a set.

    64

    65

    66 \begin{figure}

    67 \begin{center}

    68 \begin{tabular}{rrr}

    69   \it name      &\it meta-type  & \it description \\

    70   \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\

    71   \cdx{0}       & $i$           & empty set\\

    72   \cdx{cons}    & $[i,i]\To i$  & finite set constructor\\

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    95 \end{tabular}

    96 \end{center}

    97 \subcaption{Constants}

    98

    99 \begin{center}

   100 \index{*"" symbol}

   101 \index{*"-"" symbol}

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

   103 \index{*"- symbol}

   104 \index{*": symbol}

   105 \index{*"<"= symbol}

   106 \begin{tabular}{rrrr}

   107   \it symbol  & \it meta-type & \it priority & \it description \\

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

   109   \tt -       & $[i,i]\To i$  &  Left 90      & inverse image \\

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

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

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

   113   \tt -         & $[i,i]\To i$  &  Left 65      & set difference ($-$) \$1ex]   114 \tt: & [i,i]\To o & Left 50 & membership (\in) \\   115 \tt <= & [i,i]\To o & Left 50 & subset (\subseteq)   116 \end{tabular}   117 \end{center}   118 \subcaption{Infixes}   119 \caption{Constants of {\ZF}} \label{zf-constants}   120 \end{figure}   121   122   123 \section{The syntax of set theory}   124 The language of set theory, as studied by logicians, has no constants. The   125 traditional axioms merely assert the existence of empty sets, unions,   126 powersets, etc.; this would be intolerable for practical reasoning. The   127 Isabelle theory declares constants for primitive sets. It also extends   128 {\tt FOL} with additional syntax for finite sets, ordered pairs,   129 comprehension, general union/intersection, general sums/products, and   130 bounded quantifiers. In most other respects, Isabelle implements precisely   131 Zermelo-Fraenkel set theory.   132   133 Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while   134 Figure~\ref{zf-trans} presents the syntax translations. Finally,   135 Figure~\ref{zf-syntax} presents the full grammar for set theory, including   136 the constructs of \FOL.   137   138 Local abbreviations can be introduced by a {\tt let} construct whose   139 syntax appears in Fig.\ts\ref{zf-syntax}. Internally it is translated into   140 the constant~\cdx{Let}. It can be expanded by rewriting with its   141 definition, \tdx{Let_def}.   142   143 Apart from {\tt let}, set theory does not use polymorphism. All terms in   144 {\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt   145 term}. The type of first-order formulae, remember, is~{\tt o}.   146   147 Infix operators include binary union and intersection (A\union B and   148 A\inter B), set difference (A-B), and the subset and membership   149 relations. Note that a\verb|~:|b is translated to \neg(a\in b). The   150 union and intersection operators (\bigcup A and \bigcap A) form the   151 union or intersection of a set of sets; \bigcup A means the same as   152 \bigcup@{x\in A}x. Of these operators, only \bigcup A is primitive.   153   154 The constant \cdx{Upair} constructs unordered pairs; thus {\tt   155 Upair(A,B)} denotes the set~\{A,B\} and {\tt Upair(A,A)}   156 denotes the singleton~\{A\}. General union is used to define binary   157 union. The Isabelle version goes on to define the constant   158 \cdx{cons}:   159 \begin{eqnarray*}   160 A\cup B & \equiv & \bigcup({\tt Upair}(A,B)) \\   161 {\tt cons}(a,B) & \equiv & {\tt Upair}(a,a) \union B   162 \end{eqnarray*}   163 The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the   164 obvious manner using~{\tt cons} and~\emptyset (the empty set):   165 \begin{eqnarray*}   166 \{a,b,c\} & \equiv & {\tt cons}(a,{\tt cons}(b,{\tt cons}(c,\emptyset)))   167 \end{eqnarray*}   168   169 The constant \cdx{Pair} constructs ordered pairs, as in {\tt   170 Pair(a,b)}. Ordered pairs may also be written within angle brackets,   171 as {\tt<a,b>}. The n-tuple {\tt<a@1,\ldots,a@{n-1},a@n>}   172 abbreviates the nest of pairs\par\nobreak   173 \centerline{\tt Pair(a@1,\ldots,Pair(a@{n-1},a@n)\ldots).}   174   175 In {\ZF}, a function is a set of pairs. A {\ZF} function~f is simply an   176 individual as far as Isabelle is concerned: its Isabelle type is~i, not   177 say i\To i. The infix operator~{\tt} denotes the application of a   178 function set to its argument; we must write~f{\tt}x, not~f(x). The   179 syntax for image is~f{\tt}A and that for inverse image is~f{\tt-}A.   180   181   182 \begin{figure}   183 \index{lambda abs@\lambda-abstractions!in \ZF}   184 \index{*"-"> symbol}   185 \index{*"* symbol}   186 \begin{center} \footnotesize\tt\frenchspacing   187 \begin{tabular}{rrr}   188 \it external & \it internal & \it description \\   189 a \ttilde: b & \ttilde(a : b) & \rm negated membership\\   190 \{a@1, \ldots, a@n\} & cons(a@1,\cdots,cons(a@n,0)) &   191 \rm finite set \\   192 <a@1, \ldots, a@{n-1}, a@n> &   193 Pair(a@1,\ldots,Pair(a@{n-1},a@n)\ldots) &   194 \rm ordered n-tuple \\   195 \{x:A . P[x]\} & Collect(A,\lambda x.P[x]) &   196 \rm separation \\   197 \{y . x:A, Q[x,y]\} & Replace(A,\lambda x\,y.Q[x,y]) &   198 \rm replacement \\   199 \{b[x] . x:A\} & RepFun(A,\lambda x.b[x]) &   200 \rm functional replacement \\   201 \sdx{INT} x:A . B[x] & Inter(\{B[x] . x:A\}) &   202 \rm general intersection \\   203 \sdx{UN} x:A . B[x] & Union(\{B[x] . x:A\}) &   204 \rm general union \\   205 \sdx{PROD} x:A . B[x] & Pi(A,\lambda x.B[x]) &   206 \rm general product \\   207 \sdx{SUM} x:A . B[x] & Sigma(A,\lambda x.B[x]) &   208 \rm general sum \\   209 A -> B & Pi(A,\lambda x.B) &   210 \rm function space \\   211 A * B & Sigma(A,\lambda x.B) &   212 \rm binary product \\   213 \sdx{THE} x . P[x] & The(\lambda x.P[x]) &   214 \rm definite description \\   215 \sdx{lam} x:A . b[x] & Lambda(A,\lambda x.b[x]) &   216 \rm \lambda-abstraction\\[1ex]   217 \sdx{ALL} x:A . P[x] & Ball(A,\lambda x.P[x]) &   218 \rm bounded \forall \\   219 \sdx{EX} x:A . P[x] & Bex(A,\lambda x.P[x]) &   220 \rm bounded \exists   221 \end{tabular}   222 \end{center}   223 \caption{Translations for {\ZF}} \label{zf-trans}   224 \end{figure}   225   226   227 \begin{figure}   228 \index{*let symbol}   229 \index{*in symbol}   230 \dquotes   231 \[\begin{array}{rcl}   232 term & = & \hbox{expression of type~i} \\   233 & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\   234 & | & "\{ " term\; ("," term)^* " \}" \\   235 & | & "< " term\; ("," term)^* " >" \\   236 & | & "\{ " id ":" term " . " formula " \}" \\   237 & | & "\{ " id " . " id ":" term ", " formula " \}" \\   238 & | & "\{ " term " . " id ":" term " \}" \\   239 & | & term "  " term \\   240 & | & term " - " term \\   241 & | & term "  " term \\   242 & | & term " * " term \\   243 & | & term " Int " term \\   244 & | & term " Un " term \\   245 & | & term " - " term \\   246 & | & term " -> " term \\   247 & | & "THE~~" id " . " formula\\   248 & | & "lam~~" id ":" term " . " term \\   249 & | & "INT~~" id ":" term " . " term \\   250 & | & "UN~~~" id ":" term " . " term \\   251 & | & "PROD~" id ":" term " . " term \\   252 & | & "SUM~~" id ":" term " . " term \\[2ex]   253 formula & = & \hbox{expression of type~o} \\   254 & | & term " : " term \\   255 & | & term " \ttilde: " term \\   256 & | & term " <= " term \\   257 & | & term " = " term \\   258 & | & term " \ttilde= " term \\   259 & | & "\ttilde\ " formula \\   260 & | & formula " \& " formula \\   261 & | & formula " | " formula \\   262 & | & formula " --> " formula \\   263 & | & formula " <-> " formula \\   264 & | & "ALL " id ":" term " . " formula \\   265 & | & "EX~~" id ":" term " . " formula \\   266 & | & "ALL~" id~id^* " . " formula \\   267 & | & "EX~~" id~id^* " . " formula \\   268 & | & "EX!~" id~id^* " . " formula   269 \end{array}   270$

   271 \caption{Full grammar for {\ZF}} \label{zf-syntax}

   272 \end{figure}

   273

   274

   275 \section{Binding operators}

   276 The constant \cdx{Collect} constructs sets by the principle of {\bf

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

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

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

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

   281 unfortunate choice of name: some set theories adopt a set-formation

   282 principle, related to replacement, called collection.

   283

   284 The constant \cdx{Replace} constructs sets by the principle of {\bf

   285   replacement}.  The syntax \hbox{\tt\{$y$.$x$:$A$,$Q[x,y]$\}} denotes the

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

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

   288 the condition that $Q$ must be single-valued over~$A$: for all~$x\in A$

   289 there exists at most one $y$ satisfying~$Q[x,y]$.  A single-valued binary

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

   291

   292 The constant \cdx{RepFun} expresses a special case of replacement,

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

   294 single-valued, since it is just the graph of the meta-level

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

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

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

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

   300

   301 \index{*INT symbol}\index{*UN symbol}

   302 General unions and intersections of indexed

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

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

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

   306 $\bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad   307 \bigcap(\{B[x]. x\in A\}).   308$

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

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

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

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

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

   314 constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and

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

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

   317 \index{*SUM symbol}\index{*PROD symbol}%

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

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

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

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

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

   323

   324 \index{*THE symbol}

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

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

   327 constants can express the {\bf definite description} operator~$\iota   328 x.P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists.

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

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

   331 Using the constant~\cdx{The}, we may write descriptions as {\tt

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

   333

   334 \index{*lam symbol}

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

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

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

   338 constant~\cdx{Lambda}, we may express function sets as {\tt

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

   340

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

   342 \begin{eqnarray*}

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

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

   345 \end{eqnarray*}

   346 The constants~\cdx{Ball} and~\cdx{Bex} are defined

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

   348 write

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

   350

   351

   352 %%%% ZF.thy

   353

   354 \begin{figure}

   355 \begin{ttbox}

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

   357

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

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

   360

   361 \tdx{subset_def}         A <= B  == ALL x:A. x:B

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

   363

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

   365 \tdx{Pow_iff}            A : Pow(B) <-> A <= B

   366 \tdx{foundation}         A=0 | (EX x:A. ALL y:x. ~ y:A)

   367

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

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

   370 \subcaption{The Zermelo-Fraenkel Axioms}

   371

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

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

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

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

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

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

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

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

   380 \subcaption{Consequences of replacement}

   381

   382 \tdx{Inter_def}    Inter(A) == \{ x:Union(A) . ALL y:A. x:y\}

   383 \tdx{Un_def}       A Un  B  == Union(Upair(A,B))

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

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

   386 \subcaption{Union, intersection, difference}

   387 \end{ttbox}

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

   389 \end{figure}

   390

   391

   392 \begin{figure}

   393 \begin{ttbox}

   394 \tdx{cons_def}     cons(a,A) == Upair(a,a) Un A

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

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

   397 \subcaption{Finite and infinite sets}

   398

   399 \tdx{Pair_def}       <a,b>      == \{\{a,a\}, \{a,b\}\}

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

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

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

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

   404 \subcaption{Ordered pairs and Cartesian products}

   405

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

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

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

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

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

   411 \tdx{vimage_def}     r - A     == converse(r)A

   412 \subcaption{Operations on relations}

   413

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

   415 \tdx{apply_def}  fa         == THE y. <a,y> : f

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

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

   418 \subcaption{Functions and general product}

   419 \end{ttbox}

   420 \caption{Further definitions of {\ZF}} \label{zf-defs}

   421 \end{figure}

   422

   423

   424

   425 \section{The Zermelo-Fraenkel axioms}

   426 The axioms appear in Fig.\ts \ref{zf-rules}.  They resemble those

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

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

   429 appear in other axioms.  Object-level quantifiers and implications have

   430 been replaced by meta-level ones wherever possible, to simplify use of the

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

   432

   433 The traditional replacement axiom asserts

   434 $y \in {\tt PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y))$

   435 subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$.

   436 The Isabelle theory defines \cdx{Replace} to apply

   437 \cdx{PrimReplace} to the single-valued part of~$P$, namely

   438 $(\exists!z.P(x,z)) \conj P(x,y).$

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

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

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

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

   443 expands to {\tt Replace}.

   444

   445 Other consequences of replacement include functional replacement

   446 (\cdx{RepFun}) and definite descriptions (\cdx{The}).

   447 Axioms for separation (\cdx{Collect}) and unordered pairs

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

   449 from replacement~\cite[pages 237--8]{suppes72}.

   450

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

   452 the definition of {\tt cons}, which underlies the finite set notation.

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

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

   455 the theory names it (\cdx{Inf}) in order to simplify the

   456 construction of the natural numbers.

   457

   458 Further definitions appear in Fig.\ts\ref{zf-defs}.  Ordered pairs are

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

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

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

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

   463 general union.

   464

   465 The projections \cdx{fst} and~\cdx{snd} are defined in terms of the

   466 generalized projection \cdx{split}.  The latter has been borrowed from

   467 Martin-L\"of's Type Theory, and is often easier to use than \cdx{fst}

   468 and~\cdx{snd}.

   469

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

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

   472 Note the simple definitions of $\lambda$-abstraction (using

   473 \cdx{RepFun}) and application (using a definite description).  The

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

   475 over the domain~$A$.

   476

   477

   478 %%%% zf.ML

   479

   480 \begin{figure}

   481 \begin{ttbox}

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

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

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

   485

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

   487             (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))

   488

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

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

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

   492

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

   494             (EX x:A. P(x)) <-> (EX x:A'. P'(x))

   495 \subcaption{Bounded quantifiers}

   496

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

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

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

   500 \tdx{subset_refl}   A <= A

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

   502

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

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

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

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

   507 \subcaption{Subsets and extensionality}

   508

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

   510 \tdx{empty_subsetI}   0 <= A

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

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

   513

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

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

   516 \subcaption{The empty set; power sets}

   517 \end{ttbox}

   518 \caption{Basic derived rules for {\ZF}} \label{zf-lemmas1}

   519 \end{figure}

   520

   521

   522 \section{From basic lemmas to function spaces}

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

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

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

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

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

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

   529 instead.

   530

   531 \subsection{Fundamental lemmas}

   532 Figure~\ref{zf-lemmas1} presents the derived rules for the most basic

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

   534 ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption

   535 in the style of Isabelle's classical reasoner.  The \rmindex{congruence

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

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

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

   539

   540 Figure~\ref{zf-lemmas1} also shows rules for the subset and equality

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

   542 power set operator.

   543

   544 Figure~\ref{zf-lemmas2} presents rules for replacement and separation.

   545 The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than

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

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

   548 natural deduction rules for {\tt Collect}.  The elimination rule

   549 \tdx{CollectE} is equivalent to the two destruction rules

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

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

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

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

   554

   555 Figure~\ref{zf-lemmas3} presents rules for general union and intersection.

   556 The empty intersection should be undefined.  We cannot have

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

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

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

   560 arbitrary.  The rule \tdx{InterI} must have a premise to exclude

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

   562 similar premises.

   563

   564

   565 %the [p] gives better page breaking for the book

   566 \begin{figure}[p]

   567 \begin{ttbox}

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

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

   570

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

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

   573               |] ==> R

   574

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

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

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

   578

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

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

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

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

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

   584 \end{ttbox}

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

   586 \end{figure}

   587

   588

   589 \begin{figure}

   590 \begin{ttbox}

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

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

   593

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

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

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

   597

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

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

   600           |] ==> R

   601

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

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

   604 \end{ttbox}

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

   606 \end{figure}

   607

   608

   609 %%% upair.ML

   610

   611 \begin{figure}

   612 \begin{ttbox}

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

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

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

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

   617 \end{ttbox}

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

   619 \end{figure}

   620

   621

   622 \begin{figure}

   623 \begin{ttbox}

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

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

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

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

   628

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

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

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

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

   633

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

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

   636 \tdx{DiffD2}       c : A - B ==> c ~: B

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

   638 \end{ttbox}

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

   640 \end{figure}

   641

   642

   643 \begin{figure}

   644 \begin{ttbox}

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

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

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

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

   649

   650 \tdx{singletonI}   a : \{a\}

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

   652 \end{ttbox}

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

   654 \end{figure}

   655

   656

   657 \begin{figure}

   658 \begin{ttbox}

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

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

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

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

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

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

   665 \end{ttbox}

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

   667 \end{figure}

   668

   669

   670 \begin{figure}

   671 \begin{ttbox}

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

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

   674

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

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

   677

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

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

   680 \end{ttbox}

   681 \caption{Descriptions; non-circularity} \label{zf-the}

   682 \end{figure}

   683

   684

   685 \subsection{Unordered pairs and finite sets}

   686 Figure~\ref{zf-upair1} presents the principle of unordered pairing, along

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

   688 of ordered pairs (Fig.\ts\ref{zf-Un}).  Set difference is also included.  The

   689 rule \tdx{UnCI} is useful for classical reasoning about unions,

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

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

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

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

   694

   695 Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules

   696 for~{\tt cons}, the finite set constructor, and rules for singleton

   697 sets.  Figure~\ref{zf-succ} presents derived rules for the successor

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

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

   700

   701 Definite descriptions (\sdx{THE}) are defined in terms of the singleton

   702 set~$\{0\}$, but their derived rules fortunately hide this

   703 (Fig.\ts\ref{zf-the}).  The rule~\tdx{theI} is difficult to apply

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

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

   706 many examples of its use.

   707

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

   709 (\tdx{mem_asym}) is proved by applying the Axiom of Foundation to

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

   711

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

   713 this section.

   714

   715

   716 %%% subset.ML

   717

   718 \begin{figure}

   719 \begin{ttbox}

   720 \tdx{Union_upper}       B:A ==> B <= Union(A)

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

   722

   723 \tdx{Inter_lower}       B:A ==> Inter(A) <= B

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

   725

   726 \tdx{Un_upper1}         A <= A Un B

   727 \tdx{Un_upper2}         B <= A Un B

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

   729

   730 \tdx{Int_lower1}        A Int B <= A

   731 \tdx{Int_lower2}        A Int B <= B

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

   733

   734 \tdx{Diff_subset}       A-B <= A

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

   736

   737 \tdx{Collect_subset}    Collect(A,P) <= A

   738 \end{ttbox}

   739 \caption{Subset and lattice properties} \label{zf-subset}

   740 \end{figure}

   741

   742

   743 \subsection{Subset and lattice properties}

   744 The subset relation is a complete lattice.  Unions form least upper bounds;

   745 non-empty intersections form greatest lower bounds.  Figure~\ref{zf-subset}

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

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

   748

   749 Reasoning directly about subsets often yields clearer proofs than

   750 reasoning about the membership relation.  Section~\ref{sec:ZF-pow-example}

   751 below presents an example of this, proving the equation ${{\tt Pow}(A)\cap   752 {\tt Pow}(B)}= {\tt Pow}(A\cap B)$.

   753

   754 %%% pair.ML

   755

   756 \begin{figure}

   757 \begin{ttbox}

   758 \tdx{Pair_inject1}    <a,b> = <c,d> ==> a=c

   759 \tdx{Pair_inject2}    <a,b> = <c,d> ==> b=d

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

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

   762

   763 \tdx{fst_conv}        fst(<a,b>) = a

   764 \tdx{snd_conv}        snd(<a,b>) = b

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

   766

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

   768

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

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

   771

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

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

   774 \end{ttbox}

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

   776 \end{figure}

   777

   778

   779 \subsection{Ordered pairs}

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

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

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

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

   784 \tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently

   785 as the elimination rule \tdx{Pair_inject}.

   786

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

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

   789 encodings of ordered pairs.  The non-standard ordered pairs mentioned below

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

   791

   792 The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE}

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

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

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

   796 $b\in B(a)$.

   797

   798 In addition, it is possible to use tuples as patterns in abstractions:

   799 \begin{center}

   800 {\tt\%<$x$,$y$>.$t$} \quad stands for\quad {\tt split(\%$x$ $y$.$t$)}

   801 \end{center}

   802 Nested patterns are translated recursively:

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

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

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

   806 \begin{warn}

   807   The translation between patterns and {\tt split} is performed automatically

   808   by the parser and printer.  Thus the internal and external form of a term

   809   may differ, whichs affects proofs.  For example the term {\tt

   810     (\%<x,y>.<y,x>)<a,b>} requires the theorem {\tt split} to rewrite to

   811   {\tt<b,a>}.

   812 \end{warn}

   813 In addition to explicit $\lambda$-abstractions, patterns can be used in any

   814 variable binding construct which is internally described by a

   815 $\lambda$-abstraction. Some important examples are

   816 \begin{description}

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

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

   819 \item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$}

   820 \item[Comprehension:] {\tt \{~{\it pattern}:$A$~.~$P$~\}}

   821 \end{description}

   822

   823

   824 %%% domrange.ML

   825

   826 \begin{figure}

   827 \begin{ttbox}

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

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

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

   831

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

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

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

   835

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

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

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

   839

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

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

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

   843                |] ==> P

   844

   845 \tdx{field_subset}   field(A*A) <= A

   846 \end{ttbox}

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

   848 \end{figure}

   849

   850 \begin{figure}

   851 \begin{ttbox}

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

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

   854

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

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

   857 \end{ttbox}

   858 \caption{Image and inverse image} \label{zf-domrange2}

   859 \end{figure}

   860

   861

   862 \subsection{Relations}

   863 Figure~\ref{zf-domrange} presents rules involving relations, which are sets

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

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

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

   867 operation, namely \tdx{domainI} and~\tdx{domainE}, assert that

   868 \cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains

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

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

   871

   872 Figure~\ref{zf-domrange2} presents rules for images and inverse images.

   873 Note that these operations are generalisations of range and domain,

   874 respectively.  See the file {\tt ZF/domrange.ML} for derivations of the

   875 rules.

   876

   877

   878 %%% func.ML

   879

   880 \begin{figure}

   881 \begin{ttbox}

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

   883

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

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

   886

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

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

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

   890

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

   892                    !!x. x:A ==> fx = gx     |] ==> f=g

   893

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

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

   896

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

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

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

   900

   901 \tdx{restrict}        a : A ==> restrict(f,A)  a = fa

   902 \tdx{restrict_type}   [| !!x. x:A ==> fx: B(x) |] ==>

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

   904 \end{ttbox}

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

   906 \end{figure}

   907

   908

   909 \begin{figure}

   910 \begin{ttbox}

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

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

   913              |] ==>  P

   914

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

   916

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

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

   919 \end{ttbox}

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

   921 \end{figure}

   922

   923

   924 \begin{figure}

   925 \begin{ttbox}

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

   927 \tdx{fun_single}           \{<a,b>\} : \{a\} -> \{b\}

   928

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

   930                      (f Un g) : (A Un C) -> (B Un D)

   931

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

   933                      (f Un g)a = fa

   934

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

   936                      (f Un g)c = gc

   937 \end{ttbox}

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

   939 \end{figure}

   940

   941

   942 \subsection{Functions}

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

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

   945 than they ought.  This section presents the more important rules.

   946

   947 Figure~\ref{zf-func1} presents the basic properties of \cdx{Pi}$(A,B)$,

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

   949 $\pair{a,b}\in f$, then $fa=b$ (\tdx{apply_equality}).  Two functions

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

   951 (\tdx{fun_extension}).

   952

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

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

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

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

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

   958

   959 Among the laws for $\lambda$-abstraction, \tdx{lamI} and \tdx{lamE}

   960 describe the graph of the generated function, while \tdx{beta} and

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

   962 dependently-typed $\lambda$-calculus (Fig.\ts\ref{zf-lam}).

   963

   964 Figure~\ref{zf-func2} presents some rules that can be used to construct

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

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

   967 disjoint.

   968

   969

   970 \begin{figure}

   971 \begin{ttbox}

   972 \tdx{Int_absorb}         A Int A = A

   973 \tdx{Int_commute}        A Int B = B Int A

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

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

   976

   977 \tdx{Un_absorb}          A Un A = A

   978 \tdx{Un_commute}         A Un B = B Un A

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

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

   981

   982 \tdx{Diff_cancel}        A-A = 0

   983 \tdx{Diff_disjoint}      A Int (B-A) = 0

   984 \tdx{Diff_partition}     A<=B ==> A Un (B-A) = B

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

   986 \tdx{Diff_Un}            A - (B Un C) = (A-B) Int (A-C)

   987 \tdx{Diff_Int}           A - (B Int C) = (A-B) Un (A-C)

   988

   989 \tdx{Union_Un_distrib}   Union(A Un B) = Union(A) Un Union(B)

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

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

   992

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

   994

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

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

   997

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

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

  1000

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

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

  1003

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

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

  1006

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

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

  1009 \end{ttbox}

  1010 \caption{Equalities} \label{zf-equalities}

  1011 \end{figure}

  1012

  1013

  1014 \begin{figure}

  1015 %\begin{constants}

  1016 %  \cdx{1}       & $i$           &       & $\{\emptyset\}$       \\

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

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

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

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

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

  1022 %  \sdx{xor}    & $[i,i]\To i$   & Left 65 & exclusive-or for {\tt bool}

  1023 %\end{constants}

  1024 %

  1025 \begin{ttbox}

  1026 \tdx{bool_def}       bool == \{0,1\}

  1027 \tdx{cond_def}       cond(b,c,d) == if(b=1,c,d)

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

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

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

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

  1032

  1033 \tdx{bool_1I}        1 : bool

  1034 \tdx{bool_0I}        0 : bool

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

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

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

  1038 \end{ttbox}

  1039 \caption{The booleans} \label{zf-bool}

  1040 \end{figure}

  1041

  1042

  1043 \section{Further developments}

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

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

  1046 proofs.

  1047

  1048 Figure~\ref{zf-equalities} presents commutative, associative, distributive,

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

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

  1051

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

  1053 usual operators including a conditional (Fig.\ts\ref{zf-bool}).  Although

  1054 {\ZF} is a first-order theory, you can obtain the effect of higher-order

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

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

  1057

  1058 \begin{figure}

  1059 \index{*"+ symbol}

  1060 \begin{constants}

  1061   \it symbol    & \it meta-type & \it priority & \it description \\

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

  1063   \cdx{Inl}~~\cdx{Inr}  & $i\To i$      &       & injections\\

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

  1065 \end{constants}

  1066 \begin{ttbox}

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

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

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

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

  1071

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

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

  1074

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

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

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

  1078

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

  1080

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

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

  1083 \end{ttbox}

  1084 \caption{Disjoint unions} \label{zf-sum}

  1085 \end{figure}

  1086

  1087

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

  1089 injections and a case analysis operator (Fig.\ts\ref{zf-sum}).  Disjoint

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

  1091 mutual recursion~\cite{paulson-set-II}.

  1092

  1093 \begin{figure}

  1094 \begin{ttbox}

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

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

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

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

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

  1100

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

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

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

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

  1105 \end{ttbox}

  1106 \caption{Non-standard pairs, products and sums} \label{zf-qpair}

  1107 \end{figure}

  1108

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

  1110 non-well-founded tupling (Fig.\ts\ref{zf-qpair}).  Such pairs are written

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

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

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

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

  1115 non-standard notion of disjoint sum using non-standard pairs.  All of these

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

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

  1118 definitions, for example of infinite lists~\cite{paulson-final}.

  1119

  1120 \begin{figure}

  1121 \begin{ttbox}

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

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

  1124

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

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

  1127

  1128

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

  1130

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

  1132

  1133 \tdx{lfp_greatest}   [| bnd_mono(D,h);

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

  1135                |] ==> A <= lfp(D,h)

  1136

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

  1138

  1139 \tdx{induct}         [| a : lfp(D,h);  bnd_mono(D,h);

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

  1141                |] ==> P(a)

  1142

  1143 \tdx{lfp_mono}       [| bnd_mono(D,h);  bnd_mono(E,i);

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

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

  1146

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

  1148

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

  1150

  1151 \tdx{gfp_least}      [| bnd_mono(D,h);

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

  1153                |] ==> gfp(D,h) <= A

  1154

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

  1156

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

  1158                |] ==> a : gfp(D,h)

  1159

  1160 \tdx{gfp_mono}       [| bnd_mono(D,h);  D <= E;

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

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

  1163 \end{ttbox}

  1164 \caption{Least and greatest fixedpoints} \label{zf-fixedpt}

  1165 \end{figure}

  1166

  1167 The Knaster-Tarski Theorem states that every monotone function over a

  1168 complete lattice has a fixedpoint.  Theory \thydx{Fixedpt} proves the

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

  1170 set (Fig.\ts\ref{zf-fixedpt}).  The theory defines least and greatest

  1171 fixedpoint operators with corresponding induction and coinduction rules.

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

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

  1174 package also uses the fixedpoint operators~\cite{paulson-CADE}.  See

  1175 Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski

  1176 Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle

  1177 proofs.

  1178

  1179 Monotonicity properties are proved for most of the set-forming operations:

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

  1181 are useful for applying the Knaster-Tarski Fixedpoint Theorem.  The proofs

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

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

  1184

  1185

  1186 \begin{figure}

  1187 \begin{constants}

  1188   \it symbol  & \it meta-type & \it priority & \it description \\

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

  1190   \cdx{id}      & $i\To i$      &       & identity function \\

  1191   \cdx{inj}     & $[i,i]\To i$  &       & injective function space\\

  1192   \cdx{surj}    & $[i,i]\To i$  &       & surjective function space\\

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

  1194 \end{constants}

  1195

  1196 \begin{ttbox}

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

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

  1199 \tdx{id_def}    id(A)     == (lam x:A. x)

  1200 \tdx{inj_def}   inj(A,B)  == \{ f: A->B. ALL w:A. ALL x:A. fw=fx --> w=x\}

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

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

  1203

  1204

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

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

  1207                  f(converse(f)b) = b

  1208

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

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

  1211

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

  1213 \tdx{comp_assoc}       (r O s) O t = r O (s O t)

  1214

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

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

  1217

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

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

  1220

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

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

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

  1224

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

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

  1227

  1228 \tdx{bij_disjoint_Un}

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

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

  1231

  1232 \tdx{restrict_bij}  [| f:inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, fC)

  1233 \end{ttbox}

  1234 \caption{Permutations} \label{zf-perm}

  1235 \end{figure}

  1236

  1237 The theory \thydx{Perm} is concerned with permutations (bijections) and

  1238 related concepts.  These include composition of relations, the identity

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

  1240 bijective.  Figure~\ref{zf-perm} displays many of their properties that

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

  1242 equipollence and cardinality.

  1243

  1244 \begin{figure}

  1245 \index{#*@{\tt\#*} symbol}

  1246 \index{*div symbol}

  1247 \index{*mod symbol}

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

  1249 \index{#-@{\tt\#-} symbol}

  1250 \begin{constants}

  1251   \it symbol  & \it meta-type & \it priority & \it description \\

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

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

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

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

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

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

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

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

  1260 \end{constants}

  1261

  1262 \begin{ttbox}

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

  1264

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

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

  1267

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

  1269               transrec(k, \%n f. nat_case(a, \%m. b(m, fm), n))

  1270

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

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

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

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

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

  1276

  1277

  1278 \tdx{nat_0I}        0 : nat

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

  1280

  1281 \tdx{nat_induct}

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

  1283     |] ==> P(n)

  1284

  1285 \tdx{nat_case_0}    nat_case(a,b,0) = a

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

  1287

  1288 \tdx{rec_0}         rec(0,a,b) = a

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

  1290

  1291 \tdx{mult_type}     [| m:nat;  n:nat |] ==> m #* n : nat

  1292 \tdx{mult_0}        0 #* n = 0

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

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

  1295 \tdx{add_mult_dist}

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

  1297 \tdx{mult_assoc}

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

  1299 \tdx{mod_quo_equality}

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

  1301 \end{ttbox}

  1302 \caption{The natural numbers} \label{zf-nat}

  1303 \end{figure}

  1304

  1305 Theory \thydx{Nat} defines the natural numbers and mathematical

  1306 induction, along with a case analysis operator.  The set of natural

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

  1308

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

  1310 arithmetic on the natural numbers (Fig.\ts\ref{zf-nat}).  It defines

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

  1312 their properties are proved: commutative, associative and distributive

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

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

  1315 remainder are defined by repeated subtraction, which requires well-founded

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

  1317 divisor's being non-zero.

  1318

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

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

  1321 natural numbers.  Vitally, it is closed under finite products: ${\tt   1322 univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$.  This theory also

  1323 defines the cumulative hierarchy of axiomatic set theory, which

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

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

  1326

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

  1328 constructing codatatypes such as streams.  It is analogous to ${\tt   1329 univ}(A)$ (and is defined in terms of it) but is closed under the

  1330 non-standard product and sum.

  1331

  1332 Theory {\tt Finite} (Figure~\ref{zf-fin}) defines the finite set operator;

  1333 ${\tt Fin}(A)$ is the set of all finite sets over~$A$.  The theory employs

  1334 Isabelle's inductive definition package, which proves various rules

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

  1336 the package.  The theory also defines the set of all finite functions

  1337 between two given sets.

  1338

  1339 \begin{figure}

  1340 \begin{ttbox}

  1341 \tdx{Fin.emptyI}      0 : Fin(A)

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

  1343

  1344 \tdx{Fin_induct}

  1345     [| b: Fin(A);

  1346        P(0);

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

  1348     |] ==> P(b)

  1349

  1350 \tdx{Fin_mono}        A<=B ==> Fin(A) <= Fin(B)

  1351 \tdx{Fin_UnI}         [| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)

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

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

  1354 \end{ttbox}

  1355 \caption{The finite set operator} \label{zf-fin}

  1356 \end{figure}

  1357

  1358 \begin{figure}

  1359 \begin{constants}

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

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

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

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

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

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

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

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

  1368 \end{constants}

  1369

  1370 \underscoreon %%because @ is used here

  1371 \begin{ttbox}

  1372 \tdx{list_rec_def}    list_rec(l,c,h) ==

  1373                 Vrec(l, \%l g.list_case(c, \%x xs. h(x, xs, gxs), l))

  1374

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

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

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

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

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

  1380

  1381

  1382 \tdx{NilI}            Nil : list(A)

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

  1384

  1385 \tdx{List.induct}

  1386     [| l: list(A);

  1387        P(Nil);

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

  1389     |] ==> P(l)

  1390

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

  1392 \tdx{Nil_Cons_iff}    ~ Nil=Cons(a,l)

  1393

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

  1395

  1396 \tdx{list_rec_Nil}    list_rec(Nil,c,h) = c

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

  1398

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

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

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

  1402 \tdx{map_type}

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

  1404 \tdx{map_flat}

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

  1406 \end{ttbox}

  1407 \caption{Lists} \label{zf-list}

  1408 \end{figure}

  1409

  1410

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

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

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

  1414 and case operator (\verb|list_case|).  See file {\tt ZF/List.ML}.

  1415 The file {\tt ZF/ListFn.thy} proceeds to define structural

  1416 recursion and the usual list functions.

  1417

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

  1419 operators for handling recursive function definitions.  I have described

  1420 the developments in detail elsewhere~\cite{paulson-set-II}.  Here is a brief

  1421 summary:

  1422 \begin{itemize}

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

  1424     (as a least fixedpoint).

  1425

  1426   \item Theory {\tt WF} proves the Well-Founded Recursion Theorem, using an

  1427     elegant approach of Tobias Nipkow.  This theorem permits general

  1428     recursive definitions within set theory.

  1429

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

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

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

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

  1434     numbers.

  1435

  1436   \item Theory {\tt Epsilon} derives $\epsilon$-induction and

  1437     $\epsilon$-recursion, which are generalisations of transfinite

  1438     induction and recursion.  It also defines \cdx{rank}$(x)$, which is the

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

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

  1441 \end{itemize}

  1442

  1443 Other important theories lead to a theory of cardinal numbers.  They have

  1444 not yet been written up anywhere.  Here is a summary:

  1445 \begin{itemize}

  1446 \item Theory {\tt Rel} defines the basic properties of relations, such as

  1447   (ir)reflexivity, (a)symmetry, and transitivity.

  1448

  1449 \item Theory {\tt EquivClass} develops a theory of equivalence

  1450   classes, not using the Axiom of Choice.

  1451

  1452 \item Theory {\tt Order} defines partial orderings, total orderings and

  1453   wellorderings.

  1454

  1455 \item Theory {\tt OrderArith} defines orderings on sum and product sets.

  1456   These can be used to define ordinal arithmetic and have applications to

  1457   cardinal arithmetic.

  1458

  1459 \item Theory {\tt OrderType} defines order types.  Every wellordering is

  1460   equivalent to a unique ordinal, which is its order type.

  1461

  1462 \item Theory {\tt Cardinal} defines equipollence and cardinal numbers.

  1463

  1464 \item Theory {\tt CardinalArith} defines cardinal addition and

  1465   multiplication, and proves their elementary laws.  It proves that there

  1466   is no greatest cardinal.  It also proves a deep result, namely

  1467   $\kappa\otimes\kappa=\kappa$ for every infinite cardinal~$\kappa$; see

  1468   Kunen~\cite[page 29]{kunen80}.  None of these results assume the Axiom of

  1469   Choice, which complicates their proofs considerably.

  1470 \end{itemize}

  1471

  1472 The following developments involve the Axiom of Choice (AC):

  1473 \begin{itemize}

  1474 \item Theory {\tt AC} asserts the Axiom of Choice and proves some simple

  1475   equivalent forms.

  1476

  1477 \item Theory {\tt Zorn} proves Hausdorff's Maximal Principle, Zorn's Lemma

  1478   and the Wellordering Theorem, following Abrial and

  1479   Laffitte~\cite{abrial93}.

  1480

  1481 \item Theory \verb|Cardinal_AC| uses AC to prove simplified theorems about

  1482   the cardinals.  It also proves a theorem needed to justify

  1483   infinitely branching datatype declarations: if $\kappa$ is an infinite

  1484   cardinal and $|X(\alpha)| \le \kappa$ for all $\alpha<\kappa$ then

  1485   $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.

  1486

  1487 \item Theory {\tt InfDatatype} proves theorems to justify infinitely

  1488   branching datatypes.  Arbitrary index sets are allowed, provided their

  1489   cardinalities have an upper bound.  The theory also justifies some

  1490   unusual cases of finite branching, involving the finite powerset operator

  1491   and the finite function space operator.

  1492 \end{itemize}

  1493

  1494

  1495

  1496 \section{Simplification rules}

  1497 {\ZF} does not merely inherit simplification from \FOL, but modifies it

  1498 extensively.  File {\tt ZF/simpdata.ML} contains the details.

  1499

  1500 The extraction of rewrite rules takes set theory primitives into account.

  1501 It can strip bounded universal quantifiers from a formula; for example,

  1502 ${\forall x\in A.f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp   1503 f(x)=g(x)$.  Given $a\in\{x\in A.P(x)\}$ it extracts rewrite rules from

  1504 $a\in A$ and~$P(a)$.  It can also break down $a\in A\int B$ and $a\in A-B$.

  1505

  1506 The simplification set \ttindexbold{ZF_ss} contains congruence rules for

  1507 all the binding operators of {\ZF}\@.  It contains all the conversion

  1508 rules, such as {\tt fst} and {\tt snd}, as well as the rewrites

  1509 shown in Fig.\ts\ref{zf-simpdata}.

  1510

  1511

  1512 \begin{figure}

  1513 \begin{eqnarray*}

  1514   a\in \emptyset        & \bimp &  \bot\\

  1515   a \in A \union B      & \bimp &  a\in A \disj a\in B\\

  1516   a \in A \inter B      & \bimp &  a\in A \conj a\in B\\

  1517   a \in A-B             & \bimp &  a\in A \conj \neg (a\in B)\\

  1518   \pair{a,b}\in {\tt Sigma}(A,B)

  1519                         & \bimp &  a\in A \conj b\in B(a)\\

  1520   a \in {\tt Collect}(A,P)      & \bimp &  a\in A \conj P(a)\\

  1521   (\forall x \in \emptyset. P(x)) & \bimp &  \top\\

  1522   (\forall x \in A. \top)       & \bimp &  \top

  1523 \end{eqnarray*}

  1524 \caption{Rewrite rules for set theory} \label{zf-simpdata}

  1525 \end{figure}

  1526

  1527

  1528 \section{The examples directories}

  1529 Directory {\tt HOL/IMP} contains a mechanised version of a semantic

  1530 equivalence proof taken from Winskel~\cite{winskel93}.  It formalises the

  1531 denotational and operational semantics of a simple while-language, then

  1532 proves the two equivalent.  It contains several datatype and inductive

  1533 definitions, and demonstrates their use.

  1534

  1535 The directory {\tt ZF/ex} contains further developments in {\ZF} set

  1536 theory.  Here is an overview; see the files themselves for more details.  I

  1537 describe much of this material in other

  1538 publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}.

  1539 \begin{itemize}

  1540 \item File {\tt misc.ML} contains miscellaneous examples such as

  1541   Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the Composition

  1542   of homomorphisms' challenge~\cite{boyer86}.

  1543

  1544 \item Theory {\tt Ramsey} proves the finite exponent 2 version of

  1545   Ramsey's Theorem, following Basin and Kaufmann's

  1546   presentation~\cite{basin91}.

  1547

  1548 \item Theory {\tt Integ} develops a theory of the integers as

  1549   equivalence classes of pairs of natural numbers.

  1550

  1551 \item Theory {\tt Bin} defines a datatype for two's complement binary

  1552   integers, then proves rewrite rules to perform binary arithmetic.  For

  1553   instance, $1359\times {-}2468 = {-}3354012$ takes under 14 seconds.

  1554

  1555 \item Theory {\tt BT} defines the recursive data structure ${\tt   1556 bt}(A)$, labelled binary trees.

  1557

  1558 \item Theory {\tt Term} defines a recursive data structure for terms

  1559   and term lists.  These are simply finite branching trees.

  1560

  1561 \item Theory {\tt TF} defines primitives for solving mutually

  1562   recursive equations over sets.  It constructs sets of trees and forests

  1563   as an example, including induction and recursion rules that handle the

  1564   mutual recursion.

  1565

  1566 \item Theory {\tt Prop} proves soundness and completeness of

  1567   propositional logic~\cite{paulson-set-II}.  This illustrates datatype

  1568   definitions, inductive definitions, structural induction and rule

  1569   induction.

  1570

  1571 \item Theory {\tt ListN} inductively defines the lists of $n$

  1572   elements~\cite{paulin92}.

  1573

  1574 \item Theory {\tt Acc} inductively defines the accessible part of a

  1575   relation~\cite{paulin92}.

  1576

  1577 \item Theory {\tt Comb} defines the datatype of combinators and

  1578   inductively defines contraction and parallel contraction.  It goes on to

  1579   prove the Church-Rosser Theorem.  This case study follows Camilleri and

  1580   Melham~\cite{camilleri92}.

  1581

  1582 \item Theory {\tt LList} defines lazy lists and a coinduction

  1583   principle for proving equations between them.

  1584 \end{itemize}

  1585

  1586

  1587 \section{A proof about powersets}\label{sec:ZF-pow-example}

  1588 To demonstrate high-level reasoning about subsets, let us prove the

  1589 equation ${{\tt Pow}(A)\cap {\tt Pow}(B)}= {\tt Pow}(A\cap B)$.  Compared

  1590 with first-order logic, set theory involves a maze of rules, and theorems

  1591 have many different proofs.  Attempting other proofs of the theorem might

  1592 be instructive.  This proof exploits the lattice properties of

  1593 intersection.  It also uses the monotonicity of the powerset operation,

  1594 from {\tt ZF/mono.ML}:

  1595 \begin{ttbox}

  1596 \tdx{Pow_mono}      A<=B ==> Pow(A) <= Pow(B)

  1597 \end{ttbox}

  1598 We enter the goal and make the first step, which breaks the equation into

  1599 two inclusions by extensionality:\index{*equalityI theorem}

  1600 \begin{ttbox}

  1601 goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";

  1602 {\out Level 0}

  1603 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1604 {\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}

  1605 \ttbreak

  1606 by (resolve_tac [equalityI] 1);

  1607 {\out Level 1}

  1608 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1609 {\out  1. Pow(A Int B) <= Pow(A) Int Pow(B)}

  1610 {\out  2. Pow(A) Int Pow(B) <= Pow(A Int B)}

  1611 \end{ttbox}

  1612 Both inclusions could be tackled straightforwardly using {\tt subsetI}.

  1613 A shorter proof results from noting that intersection forms the greatest

  1614 lower bound:\index{*Int_greatest theorem}

  1615 \begin{ttbox}

  1616 by (resolve_tac [Int_greatest] 1);

  1617 {\out Level 2}

  1618 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1619 {\out  1. Pow(A Int B) <= Pow(A)}

  1620 {\out  2. Pow(A Int B) <= Pow(B)}

  1621 {\out  3. Pow(A) Int Pow(B) <= Pow(A Int B)}

  1622 \end{ttbox}

  1623 Subgoal~1 follows by applying the monotonicity of {\tt Pow} to $A\inter   1624 B\subseteq A$; subgoal~2 follows similarly:

  1625 \index{*Int_lower1 theorem}\index{*Int_lower2 theorem}

  1626 \begin{ttbox}

  1627 by (resolve_tac [Int_lower1 RS Pow_mono] 1);

  1628 {\out Level 3}

  1629 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1630 {\out  1. Pow(A Int B) <= Pow(B)}

  1631 {\out  2. Pow(A) Int Pow(B) <= Pow(A Int B)}

  1632 \ttbreak

  1633 by (resolve_tac [Int_lower2 RS Pow_mono] 1);

  1634 {\out Level 4}

  1635 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1636 {\out  1. Pow(A) Int Pow(B) <= Pow(A Int B)}

  1637 \end{ttbox}

  1638 We are left with the opposite inclusion, which we tackle in the

  1639 straightforward way:\index{*subsetI theorem}

  1640 \begin{ttbox}

  1641 by (resolve_tac [subsetI] 1);

  1642 {\out Level 5}

  1643 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1644 {\out  1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)}

  1645 \end{ttbox}

  1646 The subgoal is to show $x\in {\tt Pow}(A\cap B)$ assuming $x\in{\tt   1647 Pow}(A)\cap {\tt Pow}(B)$; eliminating this assumption produces two

  1648 subgoals.  The rule \tdx{IntE} treats the intersection like a conjunction

  1649 instead of unfolding its definition.

  1650 \begin{ttbox}

  1651 by (eresolve_tac [IntE] 1);

  1652 {\out Level 6}

  1653 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1654 {\out  1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)}

  1655 \end{ttbox}

  1656 The next step replaces the {\tt Pow} by the subset

  1657 relation~($\subseteq$).\index{*PowI theorem}

  1658 \begin{ttbox}

  1659 by (resolve_tac [PowI] 1);

  1660 {\out Level 7}

  1661 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1662 {\out  1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B}

  1663 \end{ttbox}

  1664 We perform the same replacement in the assumptions.  This is a good

  1665 demonstration of the tactic \ttindex{dresolve_tac}:\index{*PowD theorem}

  1666 \begin{ttbox}

  1667 by (REPEAT (dresolve_tac [PowD] 1));

  1668 {\out Level 8}

  1669 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1670 {\out  1. !!x. [| x <= A; x <= B |] ==> x <= A Int B}

  1671 \end{ttbox}

  1672 The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but

  1673 $A\inter B$ is the greatest lower bound:\index{*Int_greatest theorem}

  1674 \begin{ttbox}

  1675 by (resolve_tac [Int_greatest] 1);

  1676 {\out Level 9}

  1677 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1678 {\out  1. !!x. [| x <= A; x <= B |] ==> x <= A}

  1679 {\out  2. !!x. [| x <= A; x <= B |] ==> x <= B}

  1680 \end{ttbox}

  1681 To conclude the proof, we clear up the trivial subgoals:

  1682 \begin{ttbox}

  1683 by (REPEAT (assume_tac 1));

  1684 {\out Level 10}

  1685 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1686 {\out No subgoals!}

  1687 \end{ttbox}

  1688 \medskip

  1689 We could have performed this proof in one step by applying

  1690 \ttindex{fast_tac} with the classical rule set \ttindex{ZF_cs}.  Let us

  1691 go back to the start:

  1692 \begin{ttbox}

  1693 choplev 0;

  1694 {\out Level 0}

  1695 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1696 {\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}

  1697 \end{ttbox}

  1698 We must add \tdx{equalityI} to {\tt ZF_cs} as an introduction rule.

  1699 Extensionality is not used by default because many equalities can be proved

  1700 by rewriting.

  1701 \begin{ttbox}

  1702 by (fast_tac (ZF_cs addIs [equalityI]) 1);

  1703 {\out Level 1}

  1704 {\out Pow(A Int B) = Pow(A) Int Pow(B)}

  1705 {\out No subgoals!}

  1706 \end{ttbox}

  1707 In the past this was regarded as a difficult proof, as indeed it is if all

  1708 the symbols are replaced by their definitions.

  1709 \goodbreak

  1710

  1711 \section{Monotonicity of the union operator}

  1712 For another example, we prove that general union is monotonic:

  1713 ${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$.  To begin, we

  1714 tackle the inclusion using \tdx{subsetI}:

  1715 \begin{ttbox}

  1716 val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";

  1717 {\out Level 0}

  1718 {\out Union(C) <= Union(D)}

  1719 {\out  1. Union(C) <= Union(D)}

  1720 {\out val prem = "C <= D  [C <= D]" : thm}

  1721 \ttbreak

  1722 by (resolve_tac [subsetI] 1);

  1723 {\out Level 1}

  1724 {\out Union(C) <= Union(D)}

  1725 {\out  1. !!x. x : Union(C) ==> x : Union(D)}

  1726 \end{ttbox}

  1727 Big union is like an existential quantifier --- the occurrence in the

  1728 assumptions must be eliminated early, since it creates parameters.

  1729 \index{*UnionE theorem}

  1730 \begin{ttbox}

  1731 by (eresolve_tac [UnionE] 1);

  1732 {\out Level 2}

  1733 {\out Union(C) <= Union(D)}

  1734 {\out  1. !!x B. [| x : B; B : C |] ==> x : Union(D)}

  1735 \end{ttbox}

  1736 Now we may apply \tdx{UnionI}, which creates an unknown involving the

  1737 parameters.  To show $x\in \bigcup(D)$ it suffices to show that $x$ belongs

  1738 to some element, say~$\Var{B2}(x,B)$, of~$D$.

  1739 \begin{ttbox}

  1740 by (resolve_tac [UnionI] 1);

  1741 {\out Level 3}

  1742 {\out Union(C) <= Union(D)}

  1743 {\out  1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D}

  1744 {\out  2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)}

  1745 \end{ttbox}

  1746 Combining \tdx{subsetD} with the premise $C\subseteq D$ yields

  1747 $\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1:

  1748 \begin{ttbox}

  1749 by (resolve_tac [prem RS subsetD] 1);

  1750 {\out Level 4}

  1751 {\out Union(C) <= Union(D)}

  1752 {\out  1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C}

  1753 {\out  2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)}

  1754 \end{ttbox}

  1755 The rest is routine.  Note how~$\Var{B2}(x,B)$ is instantiated.

  1756 \begin{ttbox}

  1757 by (assume_tac 1);

  1758 {\out Level 5}

  1759 {\out Union(C) <= Union(D)}

  1760 {\out  1. !!x B. [| x : B; B : C |] ==> x : B}

  1761 by (assume_tac 1);

  1762 {\out Level 6}

  1763 {\out Union(C) <= Union(D)}

  1764 {\out No subgoals!}

  1765 \end{ttbox}

  1766 Again, \ttindex{fast_tac} with \ttindex{ZF_cs} can do this proof in one

  1767 step, provided we somehow supply it with~{\tt prem}.  We can either add

  1768 this premise to the assumptions using \ttindex{cut_facts_tac}, or add

  1769 \hbox{\tt prem RS subsetD} to \ttindex{ZF_cs} as an introduction rule.

  1770

  1771 The file {\tt ZF/equalities.ML} has many similar proofs.  Reasoning about

  1772 general intersection can be difficult because of its anomalous behaviour on

  1773 the empty set.  However, \ttindex{fast_tac} copes well with these.  Here is

  1774 a typical example, borrowed from Devlin~\cite[page 12]{devlin79}:

  1775 \begin{ttbox}

  1776 a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C.A(x)) Int (INT x:C.B(x))

  1777 \end{ttbox}

  1778 In traditional notation this is

  1779 $a\in C \,\Imp\, \inter@{x\in C} \Bigl(A(x) \int B(x)\Bigr) =   1780 \Bigl(\inter@{x\in C} A(x)\Bigr) \int   1781 \Bigl(\inter@{x\in C} B(x)\Bigr)$

  1782

  1783 \section{Low-level reasoning about functions}

  1784 The derived rules {\tt lamI}, {\tt lamE}, {\tt lam_type}, {\tt beta}

  1785 and {\tt eta} support reasoning about functions in a

  1786 $\lambda$-calculus style.  This is generally easier than regarding

  1787 functions as sets of ordered pairs.  But sometimes we must look at the

  1788 underlying representation, as in the following proof

  1789 of~\tdx{fun_disjoint_apply1}.  This states that if $f$ and~$g$ are

  1790 functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then

  1791 $(f\un g)a = fa$:

  1792 \begin{ttbox}

  1793 val prems = goal ZF.thy

  1794     "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \ttback

  1795 \ttback    (f Un g)a = fa";

  1796 {\out Level 0}

  1797 {\out (f Un g)  a = f  a}

  1798 {\out  1. (f Un g)  a = f  a}

  1799 \end{ttbox}

  1800 Isabelle has produced the output above; the \ML{} top-level now echoes the

  1801 binding of {\tt prems}.

  1802 \begin{ttbox}

  1803 {\out val prems = ["a : A  [a : A]",}

  1804 {\out              "f : A -> B  [f : A -> B]",}

  1805 {\out              "g : C -> D  [g : C -> D]",}

  1806 {\out              "A Int C = 0  [A Int C = 0]"] : thm list}

  1807 \end{ttbox}

  1808 Using \tdx{apply_equality}, we reduce the equality to reasoning about

  1809 ordered pairs.  The second subgoal is to verify that $f\un g$ is a function.

  1810 \begin{ttbox}

  1811 by (resolve_tac [apply_equality] 1);

  1812 {\out Level 1}

  1813 {\out (f Un g)  a = f  a}

  1814 {\out  1. <a,f  a> : f Un g}

  1815 {\out  2. f Un g : (PROD x:?A. ?B(x))}

  1816 \end{ttbox}

  1817 We must show that the pair belongs to~$f$ or~$g$; by~\tdx{UnI1} we

  1818 choose~$f$:

  1819 \begin{ttbox}

  1820 by (resolve_tac [UnI1] 1);

  1821 {\out Level 2}

  1822 {\out (f Un g)  a = f  a}

  1823 {\out  1. <a,f  a> : f}

  1824 {\out  2. f Un g : (PROD x:?A. ?B(x))}

  1825 \end{ttbox}

  1826 To show $\pair{a,fa}\in f$ we use \tdx{apply_Pair}, which is

  1827 essentially the converse of \tdx{apply_equality}:

  1828 \begin{ttbox}

  1829 by (resolve_tac [apply_Pair] 1);

  1830 {\out Level 3}

  1831 {\out (f Un g)  a = f  a}

  1832 {\out  1. f : (PROD x:?A2. ?B2(x))}

  1833 {\out  2. a : ?A2}

  1834 {\out  3. f Un g : (PROD x:?A. ?B(x))}

  1835 \end{ttbox}

  1836 Using the premises $f\in A\to B$ and $a\in A$, we solve the two subgoals

  1837 from \tdx{apply_Pair}.  Recall that a $\Pi$-set is merely a generalized

  1838 function space, and observe that~{\tt?A2} is instantiated to~{\tt A}.

  1839 \begin{ttbox}

  1840 by (resolve_tac prems 1);

  1841 {\out Level 4}

  1842 {\out (f Un g)  a = f  a}

  1843 {\out  1. a : A}

  1844 {\out  2. f Un g : (PROD x:?A. ?B(x))}

  1845 by (resolve_tac prems 1);

  1846 {\out Level 5}

  1847 {\out (f Un g)  a = f  a}

  1848 {\out  1. f Un g : (PROD x:?A. ?B(x))}

  1849 \end{ttbox}

  1850 To construct functions of the form $f\union g$, we apply

  1851 \tdx{fun_disjoint_Un}:

  1852 \begin{ttbox}

  1853 by (resolve_tac [fun_disjoint_Un] 1);

  1854 {\out Level 6}

  1855 {\out (f Un g)  a = f  a}

  1856 {\out  1. f : ?A3 -> ?B3}

  1857 {\out  2. g : ?C3 -> ?D3}

  1858 {\out  3. ?A3 Int ?C3 = 0}

  1859 \end{ttbox}

  1860 The remaining subgoals are instances of the premises.  Again, observe how

  1861 unknowns are instantiated:

  1862 \begin{ttbox}

  1863 by (resolve_tac prems 1);

  1864 {\out Level 7}

  1865 {\out (f Un g)  a = f  a}

  1866 {\out  1. g : ?C3 -> ?D3}

  1867 {\out  2. A Int ?C3 = 0}

  1868 by (resolve_tac prems 1);

  1869 {\out Level 8}

  1870 {\out (f Un g)  a = f  a}

  1871 {\out  1. A Int C = 0}

  1872 by (resolve_tac prems 1);

  1873 {\out Level 9}

  1874 {\out (f Un g)  a = f  a}

  1875 {\out No subgoals!}

  1876 \end{ttbox}

  1877 See the files {\tt ZF/func.ML} and {\tt ZF/WF.ML} for more

  1878 examples of reasoning about functions.

  1879

  1880 \index{set theory|)}
`