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}  f`a         == 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.f`x
   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 : r``A
   853 \tdx{imageE}         [| b: r``A;  !!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) |] ==> f`a = 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 |] ==> f`a : B(a)
   888 \tdx{apply_Pair}      [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f
   889 \tdx{apply_iff}       f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b
   890 
   891 \tdx{fun_extension}   [| f : Pi(A,B);  g: Pi(A,D);
   892                    !!x. x:A ==> f`x = g`x     |] ==> 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 ==> f`x: 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 = f`a
   902 \tdx{restrict_type}   [| !!x. x:A ==> f`x: 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. f`x) = 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 = f`a
   934 
   935 \tdx{fun_disjoint_apply2}  [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
   936                      (f Un g)`c = g`c
   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 $f`a=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. f`w=f`x --> w=x\}
  1201 \tdx{surj_def}  surj(A,B) == \{ f: A->B . ALL y:B. EX x:A. f`x=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)`(f`a) = 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`(g`a)
  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, f``C)
  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, f`m), 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, g`xs), 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 = f`a$:
  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 = f`a";
  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,f`a}\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|)}