doc-src/ZF/ZF.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 9584 af21f4364c05
child 9836 56b632fd1dcd
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
     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~\texttt{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 the
    12 basic properties of relations, functions, ordinals and cardinals.  Significant
    13 results have been proved, such as the Schr\"oder-Bernstein Theorem, the
    14 Wellordering Theorem and a version of Ramsey's Theorem.  \texttt{ZF} provides
    15 both the integers and the natural numbers.  General methods have been
    16 developed for solving recursion equations over monotonic functors; these have
    17 been applied to yield constructions of lists, trees, infinite lists, etc.
    18 
    19 \texttt{ZF} has a flexible package for handling inductive definitions,
    20 such as inference systems, and datatype definitions, such as lists and
    21 trees.  Moreover it handles coinductive definitions, such as
    22 bisimulation relations, and codatatype definitions, such as streams.  It
    23 provides a streamlined syntax for defining primitive recursive functions over
    24 datatypes. 
    25 
    26 Because ZF is an extension of FOL, it provides the same packages, namely
    27 \texttt{hyp_subst_tac}, the simplifier, and the classical reasoner.  The
    28 default simpset and claset are usually satisfactory.
    29 
    30 Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF}
    31 less formally than this chapter.  Isabelle employs a novel treatment of
    32 non-well-founded data structures within the standard {\sc zf} axioms including
    33 the Axiom of Foundation~\cite{paulson-mscs}.
    34 
    35 
    36 \section{Which version of axiomatic set theory?}
    37 The two main axiom systems for set theory are Bernays-G\"odel~({\sc bg})
    38 and Zermelo-Fraenkel~({\sc zf}).  Resolution theorem provers can use {\sc
    39   bg} because it is finite~\cite{boyer86,quaife92}.  {\sc zf} does not
    40 have a finite axiom system because of its Axiom Scheme of Replacement.
    41 This makes it awkward to use with many theorem provers, since instances
    42 of the axiom scheme have to be invoked explicitly.  Since Isabelle has no
    43 difficulty with axiom schemes, we may adopt either axiom system.
    44 
    45 These two theories differ in their treatment of {\bf classes}, which are
    46 collections that are `too big' to be sets.  The class of all sets,~$V$,
    47 cannot be a set without admitting Russell's Paradox.  In {\sc bg}, both
    48 classes and sets are individuals; $x\in V$ expresses that $x$ is a set.  In
    49 {\sc zf}, all variables denote sets; classes are identified with unary
    50 predicates.  The two systems define essentially the same sets and classes,
    51 with similar properties.  In particular, a class cannot belong to another
    52 class (let alone a set).
    53 
    54 Modern set theorists tend to prefer {\sc zf} because they are mainly concerned
    55 with sets, rather than classes.  {\sc bg} requires tiresome proofs that various
    56 collections are sets; for instance, showing $x\in\{x\}$ requires showing that
    57 $x$ is a set.
    58 
    59 
    60 \begin{figure} \small
    61 \begin{center}
    62 \begin{tabular}{rrr} 
    63   \it name      &\it meta-type  & \it description \\ 
    64   \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\
    65   \cdx{0}       & $i$           & empty set\\
    66   \cdx{cons}    & $[i,i]\To i$  & finite set constructor\\
    67   \cdx{Upair}   & $[i,i]\To i$  & unordered pairing\\
    68   \cdx{Pair}    & $[i,i]\To i$  & ordered pairing\\
    69   \cdx{Inf}     & $i$   & infinite set\\
    70   \cdx{Pow}     & $i\To i$      & powerset\\
    71   \cdx{Union} \cdx{Inter} & $i\To i$    & set union/intersection \\
    72   \cdx{split}   & $[[i,i]\To i, i] \To i$ & generalized projection\\
    73   \cdx{fst} \cdx{snd}   & $i\To i$      & projections\\
    74   \cdx{converse}& $i\To i$      & converse of a relation\\
    75   \cdx{succ}    & $i\To i$      & successor\\
    76   \cdx{Collect} & $[i,i\To o]\To i$     & separation\\
    77   \cdx{Replace} & $[i, [i,i]\To o] \To i$       & replacement\\
    78   \cdx{PrimReplace} & $[i, [i,i]\To o] \To i$   & primitive replacement\\
    79   \cdx{RepFun}  & $[i, i\To i] \To i$   & functional replacement\\
    80   \cdx{Pi} \cdx{Sigma}  & $[i,i\To i]\To i$     & general product/sum\\
    81   \cdx{domain}  & $i\To i$      & domain of a relation\\
    82   \cdx{range}   & $i\To i$      & range of a relation\\
    83   \cdx{field}   & $i\To i$      & field of a relation\\
    84   \cdx{Lambda}  & $[i, i\To i]\To i$    & $\lambda$-abstraction\\
    85   \cdx{restrict}& $[i, i] \To i$        & restriction of a function\\
    86   \cdx{The}     & $[i\To o]\To i$       & definite description\\
    87   \cdx{if}      & $[o,i,i]\To i$        & conditional\\
    88   \cdx{Ball} \cdx{Bex}  & $[i, i\To o]\To o$    & bounded quantifiers
    89 \end{tabular}
    90 \end{center}
    91 \subcaption{Constants}
    92 
    93 \begin{center}
    94 \index{*"`"` symbol}
    95 \index{*"-"`"` symbol}
    96 \index{*"` symbol}\index{function applications!in ZF}
    97 \index{*"- symbol}
    98 \index{*": symbol}
    99 \index{*"<"= symbol}
   100 \begin{tabular}{rrrr} 
   101   \it symbol  & \it meta-type & \it priority & \it description \\ 
   102   \tt ``        & $[i,i]\To i$  &  Left 90      & image \\
   103   \tt -``       & $[i,i]\To i$  &  Left 90      & inverse image \\
   104   \tt `         & $[i,i]\To i$  &  Left 90      & application \\
   105   \sdx{Int}     & $[i,i]\To i$  &  Left 70      & intersection ($\int$) \\
   106   \sdx{Un}      & $[i,i]\To i$  &  Left 65      & union ($\un$) \\
   107   \tt -         & $[i,i]\To i$  &  Left 65      & set difference ($-$) \\[1ex]
   108   \tt:          & $[i,i]\To o$  &  Left 50      & membership ($\in$) \\
   109   \tt <=        & $[i,i]\To o$  &  Left 50      & subset ($\subseteq$) 
   110 \end{tabular}
   111 \end{center}
   112 \subcaption{Infixes}
   113 \caption{Constants of ZF} \label{zf-constants}
   114 \end{figure} 
   115 
   116 
   117 \section{The syntax of set theory}
   118 The language of set theory, as studied by logicians, has no constants.  The
   119 traditional axioms merely assert the existence of empty sets, unions,
   120 powersets, etc.; this would be intolerable for practical reasoning.  The
   121 Isabelle theory declares constants for primitive sets.  It also extends
   122 \texttt{FOL} with additional syntax for finite sets, ordered pairs,
   123 comprehension, general union/intersection, general sums/products, and
   124 bounded quantifiers.  In most other respects, Isabelle implements precisely
   125 Zermelo-Fraenkel set theory.
   126 
   127 Figure~\ref{zf-constants} lists the constants and infixes of~ZF, while
   128 Figure~\ref{zf-trans} presents the syntax translations.  Finally,
   129 Figure~\ref{zf-syntax} presents the full grammar for set theory, including the
   130 constructs of FOL.
   131 
   132 Local abbreviations can be introduced by a \texttt{let} construct whose
   133 syntax appears in Fig.\ts\ref{zf-syntax}.  Internally it is translated into
   134 the constant~\cdx{Let}.  It can be expanded by rewriting with its
   135 definition, \tdx{Let_def}.
   136 
   137 Apart from \texttt{let}, set theory does not use polymorphism.  All terms in
   138 ZF have type~\tydx{i}, which is the type of individuals and has class~{\tt
   139   term}.  The type of first-order formulae, remember, is~\textit{o}.
   140 
   141 Infix operators include binary union and intersection ($A\un B$ and
   142 $A\int B$), set difference ($A-B$), and the subset and membership
   143 relations.  Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$.  The
   144 union and intersection operators ($\bigcup A$ and $\bigcap A$) form the
   145 union or intersection of a set of sets; $\bigcup A$ means the same as
   146 $\bigcup@{x\in A}x$.  Of these operators, only $\bigcup A$ is primitive.
   147 
   148 The constant \cdx{Upair} constructs unordered pairs; thus {\tt
   149   Upair($A$,$B$)} denotes the set~$\{A,B\}$ and \texttt{Upair($A$,$A$)}
   150 denotes the singleton~$\{A\}$.  General union is used to define binary
   151 union.  The Isabelle version goes on to define the constant
   152 \cdx{cons}:
   153 \begin{eqnarray*}
   154    A\cup B              & \equiv &       \bigcup(\texttt{Upair}(A,B)) \\
   155    \texttt{cons}(a,B)      & \equiv &        \texttt{Upair}(a,a) \un B
   156 \end{eqnarray*}
   157 The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the
   158 obvious manner using~\texttt{cons} and~$\emptyset$ (the empty set):
   159 \begin{eqnarray*}
   160  \{a,b,c\} & \equiv & \texttt{cons}(a,\texttt{cons}(b,\texttt{cons}(c,\emptyset)))
   161 \end{eqnarray*}
   162 
   163 The constant \cdx{Pair} constructs ordered pairs, as in {\tt
   164 Pair($a$,$b$)}.  Ordered pairs may also be written within angle brackets,
   165 as {\tt<$a$,$b$>}.  The $n$-tuple {\tt<$a@1$,\ldots,$a@{n-1}$,$a@n$>}
   166 abbreviates the nest of pairs\par\nobreak
   167 \centerline{\texttt{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}}
   168 
   169 In ZF, a function is a set of pairs.  A ZF function~$f$ is simply an
   170 individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
   171 $i\To i$.  The infix operator~{\tt`} denotes the application of a function set
   172 to its argument; we must write~$f{\tt`}x$, not~$f(x)$.  The syntax for image
   173 is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
   174 
   175 
   176 \begin{figure} 
   177 \index{lambda abs@$\lambda$-abstractions!in ZF}
   178 \index{*"-"> symbol}
   179 \index{*"* symbol}
   180 \begin{center} \footnotesize\tt\frenchspacing
   181 \begin{tabular}{rrr} 
   182   \it external          & \it internal  & \it description \\ 
   183   $a$ \ttilde: $b$      & \ttilde($a$ : $b$)    & \rm negated membership\\
   184   \ttlbrace$a@1$, $\ldots$, $a@n$\ttrbrace  &  cons($a@1$,$\ldots$,cons($a@n$,0)) &
   185         \rm finite set \\
   186   <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & 
   187         Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) &
   188         \rm ordered $n$-tuple \\
   189   \ttlbrace$x$:$A . P[x]$\ttrbrace    &  Collect($A$,$\lambda x. P[x]$) &
   190         \rm separation \\
   191   \ttlbrace$y . x$:$A$, $Q[x,y]$\ttrbrace  &  Replace($A$,$\lambda x\,y. Q[x,y]$) &
   192         \rm replacement \\
   193   \ttlbrace$b[x] . x$:$A$\ttrbrace  &  RepFun($A$,$\lambda x. b[x]$) &
   194         \rm functional replacement \\
   195   \sdx{INT} $x$:$A . B[x]$      & Inter(\ttlbrace$B[x] . x$:$A$\ttrbrace) &
   196         \rm general intersection \\
   197   \sdx{UN}  $x$:$A . B[x]$      & Union(\ttlbrace$B[x] . x$:$A$\ttrbrace) &
   198         \rm general union \\
   199   \sdx{PROD} $x$:$A . B[x]$     & Pi($A$,$\lambda x. B[x]$) & 
   200         \rm general product \\
   201   \sdx{SUM}  $x$:$A . B[x]$     & Sigma($A$,$\lambda x. B[x]$) & 
   202         \rm general sum \\
   203   $A$ -> $B$            & Pi($A$,$\lambda x. B$) & 
   204         \rm function space \\
   205   $A$ * $B$             & Sigma($A$,$\lambda x. B$) & 
   206         \rm binary product \\
   207   \sdx{THE}  $x . P[x]$ & The($\lambda x. P[x]$) & 
   208         \rm definite description \\
   209   \sdx{lam}  $x$:$A . b[x]$     & Lambda($A$,$\lambda x. b[x]$) & 
   210         \rm $\lambda$-abstraction\\[1ex]
   211   \sdx{ALL} $x$:$A . P[x]$      & Ball($A$,$\lambda x. P[x]$) & 
   212         \rm bounded $\forall$ \\
   213   \sdx{EX}  $x$:$A . P[x]$      & Bex($A$,$\lambda x. P[x]$) & 
   214         \rm bounded $\exists$
   215 \end{tabular}
   216 \end{center}
   217 \caption{Translations for ZF} \label{zf-trans}
   218 \end{figure} 
   219 
   220 
   221 \begin{figure} 
   222 \index{*let symbol}
   223 \index{*in symbol}
   224 \dquotes
   225 \[\begin{array}{rcl}
   226     term & = & \hbox{expression of type~$i$} \\
   227          & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\
   228          & | & "if"~term~"then"~term~"else"~term \\
   229          & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
   230          & | & "< "  term\; ("," term)^* " >"  \\
   231          & | & "{\ttlbrace} " id ":" term " . " formula " {\ttrbrace}" \\
   232          & | & "{\ttlbrace} " id " . " id ":" term ", " formula " {\ttrbrace}" \\
   233          & | & "{\ttlbrace} " term " . " id ":" term " {\ttrbrace}" \\
   234          & | & term " `` " term \\
   235          & | & term " -`` " term \\
   236          & | & term " ` " term \\
   237          & | & term " * " term \\
   238          & | & term " Int " term \\
   239          & | & term " Un " term \\
   240          & | & term " - " term \\
   241          & | & term " -> " term \\
   242          & | & "THE~~"  id  " . " formula\\
   243          & | & "lam~~"  id ":" term " . " term \\
   244          & | & "INT~~"  id ":" term " . " term \\
   245          & | & "UN~~~"  id ":" term " . " term \\
   246          & | & "PROD~"  id ":" term " . " term \\
   247          & | & "SUM~~"  id ":" term " . " term \\[2ex]
   248  formula & = & \hbox{expression of type~$o$} \\
   249          & | & term " : " term \\
   250          & | & term " \ttilde: " term \\
   251          & | & term " <= " term \\
   252          & | & term " = " term \\
   253          & | & term " \ttilde= " term \\
   254          & | & "\ttilde\ " formula \\
   255          & | & formula " \& " formula \\
   256          & | & formula " | " formula \\
   257          & | & formula " --> " formula \\
   258          & | & formula " <-> " formula \\
   259          & | & "ALL " id ":" term " . " formula \\
   260          & | & "EX~~" id ":" term " . " formula \\
   261          & | & "ALL~" id~id^* " . " formula \\
   262          & | & "EX~~" id~id^* " . " formula \\
   263          & | & "EX!~" id~id^* " . " formula
   264   \end{array}
   265 \]
   266 \caption{Full grammar for ZF} \label{zf-syntax}
   267 \end{figure} 
   268 
   269 
   270 \section{Binding operators}
   271 The constant \cdx{Collect} constructs sets by the principle of {\bf
   272   separation}.  The syntax for separation is
   273 \hbox{\tt\ttlbrace$x$:$A$.\ $P[x]$\ttrbrace}, where $P[x]$ is a formula
   274 that may contain free occurrences of~$x$.  It abbreviates the set {\tt
   275   Collect($A$,$\lambda x. P[x]$)}, which consists of all $x\in A$ that
   276 satisfy~$P[x]$.  Note that \texttt{Collect} is an unfortunate choice of
   277 name: some set theories adopt a set-formation principle, related to
   278 replacement, called collection.
   279 
   280 The constant \cdx{Replace} constructs sets by the principle of {\bf
   281   replacement}.  The syntax
   282 \hbox{\tt\ttlbrace$y$.\ $x$:$A$,$Q[x,y]$\ttrbrace} denotes the set {\tt
   283   Replace($A$,$\lambda x\,y. Q[x,y]$)}, which consists of all~$y$ such
   284 that there exists $x\in A$ satisfying~$Q[x,y]$.  The Replacement Axiom
   285 has the condition that $Q$ must be single-valued over~$A$: for
   286 all~$x\in A$ there exists at most one $y$ satisfying~$Q[x,y]$.  A
   287 single-valued binary predicate is also called a {\bf class function}.
   288 
   289 The constant \cdx{RepFun} expresses a special case of replacement,
   290 where $Q[x,y]$ has the form $y=b[x]$.  Such a $Q$ is trivially
   291 single-valued, since it is just the graph of the meta-level
   292 function~$\lambda x. b[x]$.  The resulting set consists of all $b[x]$
   293 for~$x\in A$.  This is analogous to the \ML{} functional \texttt{map},
   294 since it applies a function to every element of a set.  The syntax is
   295 \hbox{\tt\ttlbrace$b[x]$.\ $x$:$A$\ttrbrace}, which expands to {\tt
   296   RepFun($A$,$\lambda x. b[x]$)}.
   297 
   298 \index{*INT symbol}\index{*UN symbol} 
   299 General unions and intersections of indexed
   300 families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$,
   301 are written \hbox{\tt UN $x$:$A$.\ $B[x]$} and \hbox{\tt INT $x$:$A$.\ $B[x]$}.
   302 Their meaning is expressed using \texttt{RepFun} as
   303 \[
   304 \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad 
   305 \bigcap(\{B[x]. x\in A\}). 
   306 \]
   307 General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be
   308 constructed in set theory, where $B[x]$ is a family of sets over~$A$.  They
   309 have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set.
   310 This is similar to the situation in Constructive Type Theory (set theory
   311 has `dependent sets') and calls for similar syntactic conventions.  The
   312 constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and
   313 products.  Instead of \texttt{Sigma($A$,$B$)} and \texttt{Pi($A$,$B$)} we may
   314 write 
   315 \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt PROD $x$:$A$.\ $B[x]$}.  
   316 \index{*SUM symbol}\index{*PROD symbol}%
   317 The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate
   318 general sums and products over a constant family.\footnote{Unlike normal
   319 infix operators, {\tt*} and {\tt->} merely define abbreviations; there are
   320 no constants~\texttt{op~*} and~\hbox{\tt op~->}.} Isabelle accepts these
   321 abbreviations in parsing and uses them whenever possible for printing.
   322 
   323 \index{*THE symbol} As mentioned above, whenever the axioms assert the
   324 existence and uniqueness of a set, Isabelle's set theory declares a constant
   325 for that set.  These constants can express the {\bf definite description}
   326 operator~$\iota x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$,
   327 if such exists.  Since all terms in ZF denote something, a description is
   328 always meaningful, but we do not know its value unless $P[x]$ defines it
   329 uniquely.  Using the constant~\cdx{The}, we may write descriptions as {\tt
   330   The($\lambda x. P[x]$)} or use the syntax \hbox{\tt THE $x$.\ $P[x]$}.
   331 
   332 \index{*lam symbol}
   333 Function sets may be written in $\lambda$-notation; $\lambda x\in A. b[x]$
   334 stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$.  In order for
   335 this to be a set, the function's domain~$A$ must be given.  Using the
   336 constant~\cdx{Lambda}, we may express function sets as {\tt
   337 Lambda($A$,$\lambda x. b[x]$)} or use the syntax \hbox{\tt lam $x$:$A$.\ $b[x]$}.
   338 
   339 Isabelle's set theory defines two {\bf bounded quantifiers}:
   340 \begin{eqnarray*}
   341    \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
   342    \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
   343 \end{eqnarray*}
   344 The constants~\cdx{Ball} and~\cdx{Bex} are defined
   345 accordingly.  Instead of \texttt{Ball($A$,$P$)} and \texttt{Bex($A$,$P$)} we may
   346 write
   347 \hbox{\tt ALL $x$:$A$.\ $P[x]$} and \hbox{\tt EX $x$:$A$.\ $P[x]$}.
   348 
   349 
   350 %%%% ZF.thy
   351 
   352 \begin{figure}
   353 \begin{ttbox}
   354 \tdx{Let_def}            Let(s, f) == f(s)
   355 
   356 \tdx{Ball_def}           Ball(A,P) == ALL x. x:A --> P(x)
   357 \tdx{Bex_def}            Bex(A,P)  == EX x. x:A & P(x)
   358 
   359 \tdx{subset_def}         A <= B  == ALL x:A. x:B
   360 \tdx{extension}          A = B  <->  A <= B & B <= A
   361 
   362 \tdx{Union_iff}          A : Union(C) <-> (EX B:C. A:B)
   363 \tdx{Pow_iff}            A : Pow(B) <-> A <= B
   364 \tdx{foundation}         A=0 | (EX x:A. ALL y:x. ~ y:A)
   365 
   366 \tdx{replacement}        (ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
   367                    b : PrimReplace(A,P) <-> (EX x:A. P(x,b))
   368 \subcaption{The Zermelo-Fraenkel Axioms}
   369 
   370 \tdx{Replace_def}  Replace(A,P) == 
   371                    PrimReplace(A, \%x y. (EX!z. P(x,z)) & P(x,y))
   372 \tdx{RepFun_def}   RepFun(A,f)  == {\ttlbrace}y . x:A, y=f(x)\ttrbrace
   373 \tdx{the_def}      The(P)       == Union({\ttlbrace}y . x:{\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace})
   374 \tdx{if_def}       if(P,a,b)    == THE z. P & z=a | ~P & z=b
   375 \tdx{Collect_def}  Collect(A,P) == {\ttlbrace}y . x:A, x=y & P(x){\ttrbrace}
   376 \tdx{Upair_def}    Upair(a,b)   == 
   377                  {\ttlbrace}y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b){\ttrbrace}
   378 \subcaption{Consequences of replacement}
   379 
   380 \tdx{Inter_def}    Inter(A) == {\ttlbrace}x:Union(A) . ALL y:A. x:y{\ttrbrace}
   381 \tdx{Un_def}       A Un  B  == Union(Upair(A,B))
   382 \tdx{Int_def}      A Int B  == Inter(Upair(A,B))
   383 \tdx{Diff_def}     A - B    == {\ttlbrace}x:A . x~:B{\ttrbrace}
   384 \subcaption{Union, intersection, difference}
   385 \end{ttbox}
   386 \caption{Rules and axioms of ZF} \label{zf-rules}
   387 \end{figure}
   388 
   389 
   390 \begin{figure}
   391 \begin{ttbox}
   392 \tdx{cons_def}     cons(a,A) == Upair(a,a) Un A
   393 \tdx{succ_def}     succ(i) == cons(i,i)
   394 \tdx{infinity}     0:Inf & (ALL y:Inf. succ(y): Inf)
   395 \subcaption{Finite and infinite sets}
   396 
   397 \tdx{Pair_def}       <a,b>      == {\ttlbrace}{\ttlbrace}a,a{\ttrbrace}, {\ttlbrace}a,b{\ttrbrace}{\ttrbrace}
   398 \tdx{split_def}      split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b)
   399 \tdx{fst_def}        fst(A)     == split(\%x y. x, p)
   400 \tdx{snd_def}        snd(A)     == split(\%x y. y, p)
   401 \tdx{Sigma_def}      Sigma(A,B) == UN x:A. UN y:B(x). {\ttlbrace}<x,y>{\ttrbrace}
   402 \subcaption{Ordered pairs and Cartesian products}
   403 
   404 \tdx{converse_def}   converse(r) == {\ttlbrace}z. w:r, EX x y. w=<x,y> & z=<y,x>{\ttrbrace}
   405 \tdx{domain_def}     domain(r)   == {\ttlbrace}x. w:r, EX y. w=<x,y>{\ttrbrace}
   406 \tdx{range_def}      range(r)    == domain(converse(r))
   407 \tdx{field_def}      field(r)    == domain(r) Un range(r)
   408 \tdx{image_def}      r `` A      == {\ttlbrace}y : range(r) . EX x:A. <x,y> : r{\ttrbrace}
   409 \tdx{vimage_def}     r -`` A     == converse(r)``A
   410 \subcaption{Operations on relations}
   411 
   412 \tdx{lam_def}    Lambda(A,b) == {\ttlbrace}<x,b(x)> . x:A{\ttrbrace}
   413 \tdx{apply_def}  f`a         == THE y. <a,y> : f
   414 \tdx{Pi_def}     Pi(A,B) == {\ttlbrace}f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f{\ttrbrace}
   415 \tdx{restrict_def}   restrict(f,A) == lam x:A. f`x
   416 \subcaption{Functions and general product}
   417 \end{ttbox}
   418 \caption{Further definitions of ZF} \label{zf-defs}
   419 \end{figure}
   420 
   421 
   422 
   423 \section{The Zermelo-Fraenkel axioms}
   424 The axioms appear in Fig.\ts \ref{zf-rules}.  They resemble those
   425 presented by Suppes~\cite{suppes72}.  Most of the theory consists of
   426 definitions.  In particular, bounded quantifiers and the subset relation
   427 appear in other axioms.  Object-level quantifiers and implications have
   428 been replaced by meta-level ones wherever possible, to simplify use of the
   429 axioms.  See the file \texttt{ZF/ZF.thy} for details.
   430 
   431 The traditional replacement axiom asserts
   432 \[ y \in \texttt{PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \]
   433 subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$.
   434 The Isabelle theory defines \cdx{Replace} to apply
   435 \cdx{PrimReplace} to the single-valued part of~$P$, namely
   436 \[ (\exists!z. P(x,z)) \conj P(x,y). \]
   437 Thus $y\in \texttt{Replace}(A,P)$ if and only if there is some~$x$ such that
   438 $P(x,-)$ holds uniquely for~$y$.  Because the equivalence is unconditional,
   439 \texttt{Replace} is much easier to use than \texttt{PrimReplace}; it defines the
   440 same set, if $P(x,y)$ is single-valued.  The nice syntax for replacement
   441 expands to \texttt{Replace}.
   442 
   443 Other consequences of replacement include functional replacement
   444 (\cdx{RepFun}) and definite descriptions (\cdx{The}).
   445 Axioms for separation (\cdx{Collect}) and unordered pairs
   446 (\cdx{Upair}) are traditionally assumed, but they actually follow
   447 from replacement~\cite[pages 237--8]{suppes72}.
   448 
   449 The definitions of general intersection, etc., are straightforward.  Note
   450 the definition of \texttt{cons}, which underlies the finite set notation.
   451 The axiom of infinity gives us a set that contains~0 and is closed under
   452 successor (\cdx{succ}).  Although this set is not uniquely defined,
   453 the theory names it (\cdx{Inf}) in order to simplify the
   454 construction of the natural numbers.
   455                                              
   456 Further definitions appear in Fig.\ts\ref{zf-defs}.  Ordered pairs are
   457 defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$.  Recall
   458 that \cdx{Sigma}$(A,B)$ generalizes the Cartesian product of two
   459 sets.  It is defined to be the union of all singleton sets
   460 $\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$.  This is a typical usage of
   461 general union.
   462 
   463 The projections \cdx{fst} and~\cdx{snd} are defined in terms of the
   464 generalized projection \cdx{split}.  The latter has been borrowed from
   465 Martin-L\"of's Type Theory, and is often easier to use than \cdx{fst}
   466 and~\cdx{snd}.
   467 
   468 Operations on relations include converse, domain, range, and image.  The
   469 set ${\tt Pi}(A,B)$ generalizes the space of functions between two sets.
   470 Note the simple definitions of $\lambda$-abstraction (using
   471 \cdx{RepFun}) and application (using a definite description).  The
   472 function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only
   473 over the domain~$A$.
   474 
   475 
   476 %%%% zf.ML
   477 
   478 \begin{figure}
   479 \begin{ttbox}
   480 \tdx{ballI}       [| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)
   481 \tdx{bspec}       [| ALL x:A. P(x);  x: A |] ==> P(x)
   482 \tdx{ballE}       [| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q
   483 
   484 \tdx{ball_cong}   [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
   485             (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))
   486 
   487 \tdx{bexI}        [| P(x);  x: A |] ==> EX x:A. P(x)
   488 \tdx{bexCI}       [| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A. P(x)
   489 \tdx{bexE}        [| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q |] ==> Q
   490 
   491 \tdx{bex_cong}    [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
   492             (EX x:A. P(x)) <-> (EX x:A'. P'(x))
   493 \subcaption{Bounded quantifiers}
   494 
   495 \tdx{subsetI}       (!!x. x:A ==> x:B) ==> A <= B
   496 \tdx{subsetD}       [| A <= B;  c:A |] ==> c:B
   497 \tdx{subsetCE}      [| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P
   498 \tdx{subset_refl}   A <= A
   499 \tdx{subset_trans}  [| A<=B;  B<=C |] ==> A<=C
   500 
   501 \tdx{equalityI}     [| A <= B;  B <= A |] ==> A = B
   502 \tdx{equalityD1}    A = B ==> A<=B
   503 \tdx{equalityD2}    A = B ==> B<=A
   504 \tdx{equalityE}     [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
   505 \subcaption{Subsets and extensionality}
   506 
   507 \tdx{emptyE}          a:0 ==> P
   508 \tdx{empty_subsetI}   0 <= A
   509 \tdx{equals0I}        [| !!y. y:A ==> False |] ==> A=0
   510 \tdx{equals0D}        [| A=0;  a:A |] ==> P
   511 
   512 \tdx{PowI}            A <= B ==> A : Pow(B)
   513 \tdx{PowD}            A : Pow(B)  ==>  A<=B
   514 \subcaption{The empty set; power sets}
   515 \end{ttbox}
   516 \caption{Basic derived rules for ZF} \label{zf-lemmas1}
   517 \end{figure}
   518 
   519 
   520 \section{From basic lemmas to function spaces}
   521 Faced with so many definitions, it is essential to prove lemmas.  Even
   522 trivial theorems like $A \int B = B \int A$ would be difficult to
   523 prove from the definitions alone.  Isabelle's set theory derives many
   524 rules using a natural deduction style.  Ideally, a natural deduction
   525 rule should introduce or eliminate just one operator, but this is not
   526 always practical.  For most operators, we may forget its definition
   527 and use its derived rules instead.
   528 
   529 \subsection{Fundamental lemmas}
   530 Figure~\ref{zf-lemmas1} presents the derived rules for the most basic
   531 operators.  The rules for the bounded quantifiers resemble those for the
   532 ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption
   533 in the style of Isabelle's classical reasoner.  The \rmindex{congruence
   534   rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's
   535 simplifier, but have few other uses.  Congruence rules must be specially
   536 derived for all binding operators, and henceforth will not be shown.
   537 
   538 Figure~\ref{zf-lemmas1} also shows rules for the subset and equality
   539 relations (proof by extensionality), and rules about the empty set and the
   540 power set operator.
   541 
   542 Figure~\ref{zf-lemmas2} presents rules for replacement and separation.
   543 The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than
   544 comparable rules for \texttt{PrimReplace} would be.  The principle of
   545 separation is proved explicitly, although most proofs should use the
   546 natural deduction rules for \texttt{Collect}.  The elimination rule
   547 \tdx{CollectE} is equivalent to the two destruction rules
   548 \tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to
   549 particular circumstances.  Although too many rules can be confusing, there
   550 is no reason to aim for a minimal set of rules.  See the file
   551 \texttt{ZF/ZF.ML} for a complete listing.
   552 
   553 Figure~\ref{zf-lemmas3} presents rules for general union and intersection.
   554 The empty intersection should be undefined.  We cannot have
   555 $\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set.  All
   556 expressions denote something in ZF set theory; the definition of
   557 intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is
   558 arbitrary.  The rule \tdx{InterI} must have a premise to exclude
   559 the empty intersection.  Some of the laws governing intersections require
   560 similar premises.
   561 
   562 
   563 %the [p] gives better page breaking for the book
   564 \begin{figure}[p]
   565 \begin{ttbox}
   566 \tdx{ReplaceI}      [| x: A;  P(x,b);  !!y. P(x,y) ==> y=b |] ==> 
   567               b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace}
   568 
   569 \tdx{ReplaceE}      [| b : {\ttlbrace}y. x:A, P(x,y){\ttrbrace};  
   570                  !!x. [| x: A;  P(x,b);  ALL y. P(x,y)-->y=b |] ==> R 
   571               |] ==> R
   572 
   573 \tdx{RepFunI}       [| a : A |] ==> f(a) : {\ttlbrace}f(x). x:A{\ttrbrace}
   574 \tdx{RepFunE}       [| b : {\ttlbrace}f(x). x:A{\ttrbrace};  
   575                  !!x.[| x:A;  b=f(x) |] ==> P |] ==> P
   576 
   577 \tdx{separation}     a : {\ttlbrace}x:A. P(x){\ttrbrace} <-> a:A & P(a)
   578 \tdx{CollectI}       [| a:A;  P(a) |] ==> a : {\ttlbrace}x:A. P(x){\ttrbrace}
   579 \tdx{CollectE}       [| a : {\ttlbrace}x:A. P(x){\ttrbrace};  [| a:A; P(a) |] ==> R |] ==> R
   580 \tdx{CollectD1}      a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> a:A
   581 \tdx{CollectD2}      a : {\ttlbrace}x:A. P(x){\ttrbrace} ==> P(a)
   582 \end{ttbox}
   583 \caption{Replacement and separation} \label{zf-lemmas2}
   584 \end{figure}
   585 
   586 
   587 \begin{figure}
   588 \begin{ttbox}
   589 \tdx{UnionI}    [| B: C;  A: B |] ==> A: Union(C)
   590 \tdx{UnionE}    [| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R
   591 
   592 \tdx{InterI}    [| !!x. x: C ==> A: x;  c:C |] ==> A : Inter(C)
   593 \tdx{InterD}    [| A : Inter(C);  B : C |] ==> A : B
   594 \tdx{InterE}    [| A : Inter(C);  A:B ==> R;  ~ B:C ==> R |] ==> R
   595 
   596 \tdx{UN_I}      [| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))
   597 \tdx{UN_E}      [| b : (UN x:A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R 
   598           |] ==> R
   599 
   600 \tdx{INT_I}     [| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))
   601 \tdx{INT_E}     [| b : (INT x:A. B(x));  a: A |] ==> b : B(a)
   602 \end{ttbox}
   603 \caption{General union and intersection} \label{zf-lemmas3}
   604 \end{figure}
   605 
   606 
   607 %%% upair.ML
   608 
   609 \begin{figure}
   610 \begin{ttbox}
   611 \tdx{pairing}      a:Upair(b,c) <-> (a=b | a=c)
   612 \tdx{UpairI1}      a : Upair(a,b)
   613 \tdx{UpairI2}      b : Upair(a,b)
   614 \tdx{UpairE}       [| a : Upair(b,c);  a = b ==> P;  a = c ==> P |] ==> P
   615 \end{ttbox}
   616 \caption{Unordered pairs} \label{zf-upair1}
   617 \end{figure}
   618 
   619 
   620 \begin{figure}
   621 \begin{ttbox}
   622 \tdx{UnI1}         c : A ==> c : A Un B
   623 \tdx{UnI2}         c : B ==> c : A Un B
   624 \tdx{UnCI}         (~c : B ==> c : A) ==> c : A Un B
   625 \tdx{UnE}          [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P
   626 
   627 \tdx{IntI}         [| c : A;  c : B |] ==> c : A Int B
   628 \tdx{IntD1}        c : A Int B ==> c : A
   629 \tdx{IntD2}        c : A Int B ==> c : B
   630 \tdx{IntE}         [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
   631 
   632 \tdx{DiffI}        [| c : A;  ~ c : B |] ==> c : A - B
   633 \tdx{DiffD1}       c : A - B ==> c : A
   634 \tdx{DiffD2}       c : A - B ==> c ~: B
   635 \tdx{DiffE}        [| c : A - B;  [| c:A; ~ c:B |] ==> P |] ==> P
   636 \end{ttbox}
   637 \caption{Union, intersection, difference} \label{zf-Un}
   638 \end{figure}
   639 
   640 
   641 \begin{figure}
   642 \begin{ttbox}
   643 \tdx{consI1}       a : cons(a,B)
   644 \tdx{consI2}       a : B ==> a : cons(b,B)
   645 \tdx{consCI}       (~ a:B ==> a=b) ==> a: cons(b,B)
   646 \tdx{consE}        [| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P
   647 
   648 \tdx{singletonI}   a : {\ttlbrace}a{\ttrbrace}
   649 \tdx{singletonE}   [| a : {\ttlbrace}b{\ttrbrace}; a=b ==> P |] ==> P
   650 \end{ttbox}
   651 \caption{Finite and singleton sets} \label{zf-upair2}
   652 \end{figure}
   653 
   654 
   655 \begin{figure}
   656 \begin{ttbox}
   657 \tdx{succI1}       i : succ(i)
   658 \tdx{succI2}       i : j ==> i : succ(j)
   659 \tdx{succCI}       (~ i:j ==> i=j) ==> i: succ(j)
   660 \tdx{succE}        [| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P
   661 \tdx{succ_neq_0}   [| succ(n)=0 |] ==> P
   662 \tdx{succ_inject}  succ(m) = succ(n) ==> m=n
   663 \end{ttbox}
   664 \caption{The successor function} \label{zf-succ}
   665 \end{figure}
   666 
   667 
   668 \begin{figure}
   669 \begin{ttbox}
   670 \tdx{the_equality}     [| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a
   671 \tdx{theI}             EX! x. P(x) ==> P(THE x. P(x))
   672 
   673 \tdx{if_P}              P ==> (if P then a else b) = a
   674 \tdx{if_not_P}         ~P ==> (if P then a else b) = b
   675 
   676 \tdx{mem_asym}         [| a:b;  b:a |] ==> P
   677 \tdx{mem_irrefl}       a:a ==> P
   678 \end{ttbox}
   679 \caption{Descriptions; non-circularity} \label{zf-the}
   680 \end{figure}
   681 
   682 
   683 \subsection{Unordered pairs and finite sets}
   684 Figure~\ref{zf-upair1} presents the principle of unordered pairing, along
   685 with its derived rules.  Binary union and intersection are defined in terms
   686 of ordered pairs (Fig.\ts\ref{zf-Un}).  Set difference is also included.  The
   687 rule \tdx{UnCI} is useful for classical reasoning about unions,
   688 like \texttt{disjCI}\@; it supersedes \tdx{UnI1} and
   689 \tdx{UnI2}, but these rules are often easier to work with.  For
   690 intersection and difference we have both elimination and destruction rules.
   691 Again, there is no reason to provide a minimal rule set.
   692 
   693 Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules
   694 for~\texttt{cons}, the finite set constructor, and rules for singleton
   695 sets.  Figure~\ref{zf-succ} presents derived rules for the successor
   696 function, which is defined in terms of~\texttt{cons}.  The proof that {\tt
   697   succ} is injective appears to require the Axiom of Foundation.
   698 
   699 Definite descriptions (\sdx{THE}) are defined in terms of the singleton
   700 set~$\{0\}$, but their derived rules fortunately hide this
   701 (Fig.\ts\ref{zf-the}).  The rule~\tdx{theI} is difficult to apply
   702 because of the two occurrences of~$\Var{P}$.  However,
   703 \tdx{the_equality} does not have this problem and the files contain
   704 many examples of its use.
   705 
   706 Finally, the impossibility of having both $a\in b$ and $b\in a$
   707 (\tdx{mem_asym}) is proved by applying the Axiom of Foundation to
   708 the set $\{a,b\}$.  The impossibility of $a\in a$ is a trivial consequence.
   709 
   710 See the file \texttt{ZF/upair.ML} for full proofs of the rules discussed in
   711 this section.
   712 
   713 
   714 %%% subset.ML
   715 
   716 \begin{figure}
   717 \begin{ttbox}
   718 \tdx{Union_upper}       B:A ==> B <= Union(A)
   719 \tdx{Union_least}       [| !!x. x:A ==> x<=C |] ==> Union(A) <= C
   720 
   721 \tdx{Inter_lower}       B:A ==> Inter(A) <= B
   722 \tdx{Inter_greatest}    [| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)
   723 
   724 \tdx{Un_upper1}         A <= A Un B
   725 \tdx{Un_upper2}         B <= A Un B
   726 \tdx{Un_least}          [| A<=C;  B<=C |] ==> A Un B <= C
   727 
   728 \tdx{Int_lower1}        A Int B <= A
   729 \tdx{Int_lower2}        A Int B <= B
   730 \tdx{Int_greatest}      [| C<=A;  C<=B |] ==> C <= A Int B
   731 
   732 \tdx{Diff_subset}       A-B <= A
   733 \tdx{Diff_contains}     [| C<=A;  C Int B = 0 |] ==> C <= A-B
   734 
   735 \tdx{Collect_subset}    Collect(A,P) <= A
   736 \end{ttbox}
   737 \caption{Subset and lattice properties} \label{zf-subset}
   738 \end{figure}
   739 
   740 
   741 \subsection{Subset and lattice properties}
   742 The subset relation is a complete lattice.  Unions form least upper bounds;
   743 non-empty intersections form greatest lower bounds.  Figure~\ref{zf-subset}
   744 shows the corresponding rules.  A few other laws involving subsets are
   745 included.  Proofs are in the file \texttt{ZF/subset.ML}.
   746 
   747 Reasoning directly about subsets often yields clearer proofs than
   748 reasoning about the membership relation.  Section~\ref{sec:ZF-pow-example}
   749 below presents an example of this, proving the equation ${{\tt Pow}(A)\cap
   750   {\tt Pow}(B)}= {\tt Pow}(A\cap B)$.
   751 
   752 %%% pair.ML
   753 
   754 \begin{figure}
   755 \begin{ttbox}
   756 \tdx{Pair_inject1}    <a,b> = <c,d> ==> a=c
   757 \tdx{Pair_inject2}    <a,b> = <c,d> ==> b=d
   758 \tdx{Pair_inject}     [| <a,b> = <c,d>;  [| a=c; b=d |] ==> P |] ==> P
   759 \tdx{Pair_neq_0}      <a,b>=0 ==> P
   760 
   761 \tdx{fst_conv}        fst(<a,b>) = a
   762 \tdx{snd_conv}        snd(<a,b>) = b
   763 \tdx{split}           split(\%x y. c(x,y), <a,b>) = c(a,b)
   764 
   765 \tdx{SigmaI}          [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)
   766 
   767 \tdx{SigmaE}          [| c: Sigma(A,B);  
   768                    !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
   769 
   770 \tdx{SigmaE2}         [| <a,b> : Sigma(A,B);    
   771                    [| a:A;  b:B(a) |] ==> P   |] ==> P
   772 \end{ttbox}
   773 \caption{Ordered pairs; projections; general sums} \label{zf-pair}
   774 \end{figure}
   775 
   776 
   777 \subsection{Ordered pairs} \label{sec:pairs}
   778 
   779 Figure~\ref{zf-pair} presents the rules governing ordered pairs,
   780 projections and general sums.  File \texttt{ZF/pair.ML} contains the
   781 full (and tedious) proof that $\{\{a\},\{a,b\}\}$ functions as an ordered
   782 pair.  This property is expressed as two destruction rules,
   783 \tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently
   784 as the elimination rule \tdx{Pair_inject}.
   785 
   786 The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$.  This
   787 is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other 
   788 encodings of ordered pairs.  The non-standard ordered pairs mentioned below
   789 satisfy $\pair{\emptyset;\emptyset}=\emptyset$.
   790 
   791 The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE}
   792 assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form
   793 $\pair{x,y}$, for $x\in A$ and $y\in B(x)$.  The rule \tdx{SigmaE2}
   794 merely states that $\pair{a,b}\in \texttt{Sigma}(A,B)$ implies $a\in A$ and
   795 $b\in B(a)$.
   796 
   797 In addition, it is possible to use tuples as patterns in abstractions:
   798 \begin{center}
   799 {\tt\%<$x$,$y$>. $t$} \quad stands for\quad \texttt{split(\%$x$ $y$.\ $t$)}
   800 \end{center}
   801 Nested patterns are translated recursively:
   802 {\tt\%<$x$,$y$,$z$>. $t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>. $t$} $\leadsto$
   803 \texttt{split(\%$x$.\%<$y$,$z$>. $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$
   804   $z$.\ $t$))}.  The reverse translation is performed upon printing.
   805 \begin{warn}
   806   The translation between patterns and \texttt{split} is performed automatically
   807   by the parser and printer.  Thus the internal and external form of a term
   808   may differ, which affects proofs.  For example the term {\tt
   809     (\%<x,y>.<y,x>)<a,b>} requires the theorem \texttt{split} to rewrite to
   810   {\tt<b,a>}.
   811 \end{warn}
   812 In addition to explicit $\lambda$-abstractions, patterns can be used in any
   813 variable binding construct which is internally described by a
   814 $\lambda$-abstraction.  Here are some important examples:
   815 \begin{description}
   816 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$}
   817 \item[Choice:] \texttt{THE~{\it pattern}~.~$P$}
   818 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}
   819 \item[Comprehension:] \texttt{{\ttlbrace}~{\it pattern}:$A$~.~$P$~{\ttrbrace}}
   820 \end{description}
   821 
   822 
   823 %%% domrange.ML
   824 
   825 \begin{figure}
   826 \begin{ttbox}
   827 \tdx{domainI}        <a,b>: r ==> a : domain(r)
   828 \tdx{domainE}        [| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P
   829 \tdx{domain_subset}  domain(Sigma(A,B)) <= A
   830 
   831 \tdx{rangeI}         <a,b>: r ==> b : range(r)
   832 \tdx{rangeE}         [| b : range(r);  !!x. <x,b>: r ==> P |] ==> P
   833 \tdx{range_subset}   range(A*B) <= B
   834 
   835 \tdx{fieldI1}        <a,b>: r ==> a : field(r)
   836 \tdx{fieldI2}        <a,b>: r ==> b : field(r)
   837 \tdx{fieldCI}        (~ <c,a>:r ==> <a,b>: r) ==> a : field(r)
   838 
   839 \tdx{fieldE}         [| a : field(r);  
   840                   !!x. <a,x>: r ==> P;  
   841                   !!x. <x,a>: r ==> P      
   842                |] ==> P
   843 
   844 \tdx{field_subset}   field(A*A) <= A
   845 \end{ttbox}
   846 \caption{Domain, range and field of a relation} \label{zf-domrange}
   847 \end{figure}
   848 
   849 \begin{figure}
   850 \begin{ttbox}
   851 \tdx{imageI}         [| <a,b>: r;  a:A |] ==> b : r``A
   852 \tdx{imageE}         [| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P
   853 
   854 \tdx{vimageI}        [| <a,b>: r;  b:B |] ==> a : r-``B
   855 \tdx{vimageE}        [| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P
   856 \end{ttbox}
   857 \caption{Image and inverse image} \label{zf-domrange2}
   858 \end{figure}
   859 
   860 
   861 \subsection{Relations}
   862 Figure~\ref{zf-domrange} presents rules involving relations, which are sets
   863 of ordered pairs.  The converse of a relation~$r$ is the set of all pairs
   864 $\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then
   865 {\cdx{converse}$(r)$} is its inverse.  The rules for the domain
   866 operation, namely \tdx{domainI} and~\tdx{domainE}, assert that
   867 \cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains
   868 some pair of the form~$\pair{x,y}$.  The range operation is similar, and
   869 the field of a relation is merely the union of its domain and range.  
   870 
   871 Figure~\ref{zf-domrange2} presents rules for images and inverse images.
   872 Note that these operations are generalisations of range and domain,
   873 respectively.  See the file \texttt{ZF/domrange.ML} for derivations of the
   874 rules.
   875 
   876 
   877 %%% func.ML
   878 
   879 \begin{figure}
   880 \begin{ttbox}
   881 \tdx{fun_is_rel}      f: Pi(A,B) ==> f <= Sigma(A,B)
   882 
   883 \tdx{apply_equality}  [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b
   884 \tdx{apply_equality2} [| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c
   885 
   886 \tdx{apply_type}      [| f: Pi(A,B);  a:A |] ==> f`a : B(a)
   887 \tdx{apply_Pair}      [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f
   888 \tdx{apply_iff}       f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b
   889 
   890 \tdx{fun_extension}   [| f : Pi(A,B);  g: Pi(A,D);
   891                    !!x. x:A ==> f`x = g`x     |] ==> f=g
   892 
   893 \tdx{domain_type}     [| <a,b> : f;  f: Pi(A,B) |] ==> a : A
   894 \tdx{range_type}      [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)
   895 
   896 \tdx{Pi_type}         [| f: A->C;  !!x. x:A ==> f`x: B(x) |] ==> f: Pi(A,B)
   897 \tdx{domain_of_fun}   f: Pi(A,B) ==> domain(f)=A
   898 \tdx{range_of_fun}    f: Pi(A,B) ==> f: A->range(f)
   899 
   900 \tdx{restrict}        a : A ==> restrict(f,A) ` a = f`a
   901 \tdx{restrict_type}   [| !!x. x:A ==> f`x: B(x) |] ==> 
   902                 restrict(f,A) : Pi(A,B)
   903 \end{ttbox}
   904 \caption{Functions} \label{zf-func1}
   905 \end{figure}
   906 
   907 
   908 \begin{figure}
   909 \begin{ttbox}
   910 \tdx{lamI}      a:A ==> <a,b(a)> : (lam x:A. b(x))
   911 \tdx{lamE}      [| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P 
   912           |] ==>  P
   913 
   914 \tdx{lam_type}  [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)
   915 
   916 \tdx{beta}      a : A ==> (lam x:A. b(x)) ` a = b(a)
   917 \tdx{eta}       f : Pi(A,B) ==> (lam x:A. f`x) = f
   918 \end{ttbox}
   919 \caption{$\lambda$-abstraction} \label{zf-lam}
   920 \end{figure}
   921 
   922 
   923 \begin{figure}
   924 \begin{ttbox}
   925 \tdx{fun_empty}            0: 0->0
   926 \tdx{fun_single}           {\ttlbrace}<a,b>{\ttrbrace} : {\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace}
   927 
   928 \tdx{fun_disjoint_Un}      [| f: A->B;  g: C->D;  A Int C = 0  |] ==>  
   929                      (f Un g) : (A Un C) -> (B Un D)
   930 
   931 \tdx{fun_disjoint_apply1}  [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
   932                      (f Un g)`a = f`a
   933 
   934 \tdx{fun_disjoint_apply2}  [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
   935                      (f Un g)`c = g`c
   936 \end{ttbox}
   937 \caption{Constructing functions from smaller sets} \label{zf-func2}
   938 \end{figure}
   939 
   940 
   941 \subsection{Functions}
   942 Functions, represented by graphs, are notoriously difficult to reason
   943 about.  The file \texttt{ZF/func.ML} derives many rules, which overlap more
   944 than they ought.  This section presents the more important rules.
   945 
   946 Figure~\ref{zf-func1} presents the basic properties of \cdx{Pi}$(A,B)$,
   947 the generalized function space.  For example, if $f$ is a function and
   948 $\pair{a,b}\in f$, then $f`a=b$ (\tdx{apply_equality}).  Two functions
   949 are equal provided they have equal domains and deliver equals results
   950 (\tdx{fun_extension}).
   951 
   952 By \tdx{Pi_type}, a function typing of the form $f\in A\to C$ can be
   953 refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable
   954 family of sets $\{B(x)\}@{x\in A}$.  Conversely, by \tdx{range_of_fun},
   955 any dependent typing can be flattened to yield a function type of the form
   956 $A\to C$; here, $C={\tt range}(f)$.
   957 
   958 Among the laws for $\lambda$-abstraction, \tdx{lamI} and \tdx{lamE}
   959 describe the graph of the generated function, while \tdx{beta} and
   960 \tdx{eta} are the standard conversions.  We essentially have a
   961 dependently-typed $\lambda$-calculus (Fig.\ts\ref{zf-lam}).
   962 
   963 Figure~\ref{zf-func2} presents some rules that can be used to construct
   964 functions explicitly.  We start with functions consisting of at most one
   965 pair, and may form the union of two functions provided their domains are
   966 disjoint.  
   967 
   968 
   969 \begin{figure}
   970 \begin{ttbox}
   971 \tdx{Int_absorb}         A Int A = A
   972 \tdx{Int_commute}        A Int B = B Int A
   973 \tdx{Int_assoc}          (A Int B) Int C  =  A Int (B Int C)
   974 \tdx{Int_Un_distrib}     (A Un B) Int C  =  (A Int C) Un (B Int C)
   975 
   976 \tdx{Un_absorb}          A Un A = A
   977 \tdx{Un_commute}         A Un B = B Un A
   978 \tdx{Un_assoc}           (A Un B) Un C  =  A Un (B Un C)
   979 \tdx{Un_Int_distrib}     (A Int B) Un C  =  (A Un C) Int (B Un C)
   980 
   981 \tdx{Diff_cancel}        A-A = 0
   982 \tdx{Diff_disjoint}      A Int (B-A) = 0
   983 \tdx{Diff_partition}     A<=B ==> A Un (B-A) = B
   984 \tdx{double_complement}  [| A<=B; B<= C |] ==> (B - (C-A)) = A
   985 \tdx{Diff_Un}            A - (B Un C) = (A-B) Int (A-C)
   986 \tdx{Diff_Int}           A - (B Int C) = (A-B) Un (A-C)
   987 
   988 \tdx{Union_Un_distrib}   Union(A Un B) = Union(A) Un Union(B)
   989 \tdx{Inter_Un_distrib}   [| a:A;  b:B |] ==> 
   990                    Inter(A Un B) = Inter(A) Int Inter(B)
   991 
   992 \tdx{Int_Union_RepFun}   A Int Union(B) = (UN C:B. A Int C)
   993 
   994 \tdx{Un_Inter_RepFun}    b:B ==> 
   995                    A Un Inter(B) = (INT C:B. A Un C)
   996 
   997 \tdx{SUM_Un_distrib1}    (SUM x:A Un B. C(x)) = 
   998                    (SUM x:A. C(x)) Un (SUM x:B. C(x))
   999 
  1000 \tdx{SUM_Un_distrib2}    (SUM x:C. A(x) Un B(x)) =
  1001                    (SUM x:C. A(x))  Un  (SUM x:C. B(x))
  1002 
  1003 \tdx{SUM_Int_distrib1}   (SUM x:A Int B. C(x)) =
  1004                    (SUM x:A. C(x)) Int (SUM x:B. C(x))
  1005 
  1006 \tdx{SUM_Int_distrib2}   (SUM x:C. A(x) Int B(x)) =
  1007                    (SUM x:C. A(x)) Int (SUM x:C. B(x))
  1008 \end{ttbox}
  1009 \caption{Equalities} \label{zf-equalities}
  1010 \end{figure}
  1011 
  1012 
  1013 \begin{figure}
  1014 %\begin{constants} 
  1015 %  \cdx{1}       & $i$           &       & $\{\emptyset\}$       \\
  1016 %  \cdx{bool}    & $i$           &       & the set $\{\emptyset,1\}$     \\
  1017 %  \cdx{cond}   & $[i,i,i]\To i$ &       & conditional for \texttt{bool}    \\
  1018 %  \cdx{not}    & $i\To i$       &       & negation for \texttt{bool}       \\
  1019 %  \sdx{and}    & $[i,i]\To i$   & Left 70 & conjunction for \texttt{bool}  \\
  1020 %  \sdx{or}     & $[i,i]\To i$   & Left 65 & disjunction for \texttt{bool}  \\
  1021 %  \sdx{xor}    & $[i,i]\To i$   & Left 65 & exclusive-or for \texttt{bool}
  1022 %\end{constants}
  1023 %
  1024 \begin{ttbox}
  1025 \tdx{bool_def}       bool == {\ttlbrace}0,1{\ttrbrace}
  1026 \tdx{cond_def}       cond(b,c,d) == if b=1 then c else d
  1027 \tdx{not_def}        not(b)  == cond(b,0,1)
  1028 \tdx{and_def}        a and b == cond(a,b,0)
  1029 \tdx{or_def}         a or b  == cond(a,1,b)
  1030 \tdx{xor_def}        a xor b == cond(a,not(b),b)
  1031 
  1032 \tdx{bool_1I}        1 : bool
  1033 \tdx{bool_0I}        0 : bool
  1034 \tdx{boolE}          [| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P
  1035 \tdx{cond_1}         cond(1,c,d) = c
  1036 \tdx{cond_0}         cond(0,c,d) = d
  1037 \end{ttbox}
  1038 \caption{The booleans} \label{zf-bool}
  1039 \end{figure}
  1040 
  1041 
  1042 \section{Further developments}
  1043 The next group of developments is complex and extensive, and only
  1044 highlights can be covered here.  It involves many theories and ML files of
  1045 proofs. 
  1046 
  1047 Figure~\ref{zf-equalities} presents commutative, associative, distributive,
  1048 and idempotency laws of union and intersection, along with other equations.
  1049 See file \texttt{ZF/equalities.ML}.
  1050 
  1051 Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual
  1052 operators including a conditional (Fig.\ts\ref{zf-bool}).  Although ZF is a
  1053 first-order theory, you can obtain the effect of higher-order logic using
  1054 \texttt{bool}-valued functions, for example.  The constant~\texttt{1} is
  1055 translated to \texttt{succ(0)}.
  1056 
  1057 \begin{figure}
  1058 \index{*"+ symbol}
  1059 \begin{constants}
  1060   \it symbol    & \it meta-type & \it priority & \it description \\ 
  1061   \tt +         & $[i,i]\To i$  &  Right 65     & disjoint union operator\\
  1062   \cdx{Inl}~~\cdx{Inr}  & $i\To i$      &       & injections\\
  1063   \cdx{case}    & $[i\To i,i\To i, i]\To i$ &   & conditional for $A+B$
  1064 \end{constants}
  1065 \begin{ttbox}
  1066 \tdx{sum_def}        A+B == {\ttlbrace}0{\ttrbrace}*A Un {\ttlbrace}1{\ttrbrace}*B
  1067 \tdx{Inl_def}        Inl(a) == <0,a>
  1068 \tdx{Inr_def}        Inr(b) == <1,b>
  1069 \tdx{case_def}       case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u)
  1070 
  1071 \tdx{sum_InlI}       a : A ==> Inl(a) : A+B
  1072 \tdx{sum_InrI}       b : B ==> Inr(b) : A+B
  1073 
  1074 \tdx{Inl_inject}     Inl(a)=Inl(b) ==> a=b
  1075 \tdx{Inr_inject}     Inr(a)=Inr(b) ==> a=b
  1076 \tdx{Inl_neq_Inr}    Inl(a)=Inr(b) ==> P
  1077 
  1078 \tdx{sumE2}   u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))
  1079 
  1080 \tdx{case_Inl}       case(c,d,Inl(a)) = c(a)
  1081 \tdx{case_Inr}       case(c,d,Inr(b)) = d(b)
  1082 \end{ttbox}
  1083 \caption{Disjoint unions} \label{zf-sum}
  1084 \end{figure}
  1085 
  1086 
  1087 \subsection{Disjoint unions}
  1088 
  1089 Theory \thydx{Sum} defines the disjoint union of two sets, with
  1090 injections and a case analysis operator (Fig.\ts\ref{zf-sum}).  Disjoint
  1091 unions play a role in datatype definitions, particularly when there is
  1092 mutual recursion~\cite{paulson-set-II}.
  1093 
  1094 \begin{figure}
  1095 \begin{ttbox}
  1096 \tdx{QPair_def}       <a;b> == a+b
  1097 \tdx{qsplit_def}      qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)
  1098 \tdx{qfsplit_def}     qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)
  1099 \tdx{qconverse_def}   qconverse(r) == {\ttlbrace}z. w:r, EX x y. w=<x;y> & z=<y;x>{\ttrbrace}
  1100 \tdx{QSigma_def}      QSigma(A,B)  == UN x:A. UN y:B(x). {\ttlbrace}<x;y>{\ttrbrace}
  1101 
  1102 \tdx{qsum_def}        A <+> B      == ({\ttlbrace}0{\ttrbrace} <*> A) Un ({\ttlbrace}1{\ttrbrace} <*> B)
  1103 \tdx{QInl_def}        QInl(a)      == <0;a>
  1104 \tdx{QInr_def}        QInr(b)      == <1;b>
  1105 \tdx{qcase_def}       qcase(c,d)   == qsplit(\%y z. cond(y, d(z), c(z)))
  1106 \end{ttbox}
  1107 \caption{Non-standard pairs, products and sums} \label{zf-qpair}
  1108 \end{figure}
  1109 
  1110 
  1111 \subsection{Non-standard ordered pairs}
  1112 
  1113 Theory \thydx{QPair} defines a notion of ordered pair that admits
  1114 non-well-founded tupling (Fig.\ts\ref{zf-qpair}).  Such pairs are written
  1115 {\tt<$a$;$b$>}.  It also defines the eliminator \cdx{qsplit}, the
  1116 converse operator \cdx{qconverse}, and the summation operator
  1117 \cdx{QSigma}.  These are completely analogous to the corresponding
  1118 versions for standard ordered pairs.  The theory goes on to define a
  1119 non-standard notion of disjoint sum using non-standard pairs.  All of these
  1120 concepts satisfy the same properties as their standard counterparts; in
  1121 addition, {\tt<$a$;$b$>} is continuous.  The theory supports coinductive
  1122 definitions, for example of infinite lists~\cite{paulson-mscs}.
  1123 
  1124 \begin{figure}
  1125 \begin{ttbox}
  1126 \tdx{bnd_mono_def}   bnd_mono(D,h) == 
  1127                  h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))
  1128 
  1129 \tdx{lfp_def}        lfp(D,h) == Inter({\ttlbrace}X: Pow(D). h(X) <= X{\ttrbrace})
  1130 \tdx{gfp_def}        gfp(D,h) == Union({\ttlbrace}X: Pow(D). X <= h(X){\ttrbrace})
  1131 
  1132 
  1133 \tdx{lfp_lowerbound} [| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A
  1134 
  1135 \tdx{lfp_subset}     lfp(D,h) <= D
  1136 
  1137 \tdx{lfp_greatest}   [| bnd_mono(D,h);  
  1138                   !!X. [| h(X) <= X;  X<=D |] ==> A<=X 
  1139                |] ==> A <= lfp(D,h)
  1140 
  1141 \tdx{lfp_Tarski}     bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))
  1142 
  1143 \tdx{induct}         [| a : lfp(D,h);  bnd_mono(D,h);
  1144                   !!x. x : h(Collect(lfp(D,h),P)) ==> P(x)
  1145                |] ==> P(a)
  1146 
  1147 \tdx{lfp_mono}       [| bnd_mono(D,h);  bnd_mono(E,i);
  1148                   !!X. X<=D ==> h(X) <= i(X)  
  1149                |] ==> lfp(D,h) <= lfp(E,i)
  1150 
  1151 \tdx{gfp_upperbound} [| A <= h(A);  A<=D |] ==> A <= gfp(D,h)
  1152 
  1153 \tdx{gfp_subset}     gfp(D,h) <= D
  1154 
  1155 \tdx{gfp_least}      [| bnd_mono(D,h);  
  1156                   !!X. [| X <= h(X);  X<=D |] ==> X<=A
  1157                |] ==> gfp(D,h) <= A
  1158 
  1159 \tdx{gfp_Tarski}     bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))
  1160 
  1161 \tdx{coinduct}       [| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D 
  1162                |] ==> a : gfp(D,h)
  1163 
  1164 \tdx{gfp_mono}       [| bnd_mono(D,h);  D <= E;
  1165                   !!X. X<=D ==> h(X) <= i(X)  
  1166                |] ==> gfp(D,h) <= gfp(E,i)
  1167 \end{ttbox}
  1168 \caption{Least and greatest fixedpoints} \label{zf-fixedpt}
  1169 \end{figure}
  1170 
  1171 
  1172 \subsection{Least and greatest fixedpoints}
  1173 
  1174 The Knaster-Tarski Theorem states that every monotone function over a
  1175 complete lattice has a fixedpoint.  Theory \thydx{Fixedpt} proves the
  1176 Theorem only for a particular lattice, namely the lattice of subsets of a
  1177 set (Fig.\ts\ref{zf-fixedpt}).  The theory defines least and greatest
  1178 fixedpoint operators with corresponding induction and coinduction rules.
  1179 These are essential to many definitions that follow, including the natural
  1180 numbers and the transitive closure operator.  The (co)inductive definition
  1181 package also uses the fixedpoint operators~\cite{paulson-CADE}.  See
  1182 Davey and Priestley~\cite{davey-priestley} for more on the Knaster-Tarski
  1183 Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle
  1184 proofs.
  1185 
  1186 Monotonicity properties are proved for most of the set-forming operations:
  1187 union, intersection, Cartesian product, image, domain, range, etc.  These
  1188 are useful for applying the Knaster-Tarski Fixedpoint Theorem.  The proofs
  1189 themselves are trivial applications of Isabelle's classical reasoner.  See
  1190 file \texttt{ZF/mono.ML}.
  1191 
  1192 
  1193 \subsection{Finite sets and lists}
  1194 
  1195 Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines the finite set operator;
  1196 ${\tt Fin}(A)$ is the set of all finite sets over~$A$.  The theory employs
  1197 Isabelle's inductive definition package, which proves various rules
  1198 automatically.  The induction rule shown is stronger than the one proved by
  1199 the package.  The theory also defines the set of all finite functions
  1200 between two given sets.
  1201 
  1202 \begin{figure}
  1203 \begin{ttbox}
  1204 \tdx{Fin.emptyI}      0 : Fin(A)
  1205 \tdx{Fin.consI}       [| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)
  1206 
  1207 \tdx{Fin_induct}
  1208     [| b: Fin(A);
  1209        P(0);
  1210        !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y))
  1211     |] ==> P(b)
  1212 
  1213 \tdx{Fin_mono}        A<=B ==> Fin(A) <= Fin(B)
  1214 \tdx{Fin_UnI}         [| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)
  1215 \tdx{Fin_UnionI}      C : Fin(Fin(A)) ==> Union(C) : Fin(A)
  1216 \tdx{Fin_subset}      [| c<=b;  b: Fin(A) |] ==> c: Fin(A)
  1217 \end{ttbox}
  1218 \caption{The finite set operator} \label{zf-fin}
  1219 \end{figure}
  1220 
  1221 \begin{figure}
  1222 \begin{constants}
  1223   \it symbol  & \it meta-type & \it priority & \it description \\ 
  1224   \cdx{list}    & $i\To i$      && lists over some set\\
  1225   \cdx{list_case} & $[i, [i,i]\To i, i] \To i$  && conditional for $list(A)$ \\
  1226   \cdx{map}     & $[i\To i, i] \To i$   &       & mapping functional\\
  1227   \cdx{length}  & $i\To i$              &       & length of a list\\
  1228   \cdx{rev}     & $i\To i$              &       & reverse of a list\\
  1229   \tt \at       & $[i,i]\To i$  &  Right 60     & append for lists\\
  1230   \cdx{flat}    & $i\To i$   &                  & append of list of lists
  1231 \end{constants}
  1232 
  1233 \underscoreon %%because @ is used here
  1234 \begin{ttbox}
  1235 \tdx{NilI}            Nil : list(A)
  1236 \tdx{ConsI}           [| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)
  1237 
  1238 \tdx{List.induct}
  1239     [| l: list(A);
  1240        P(Nil);
  1241        !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(Cons(x,y))
  1242     |] ==> P(l)
  1243 
  1244 \tdx{Cons_iff}        Cons(a,l)=Cons(a',l') <-> a=a' & l=l'
  1245 \tdx{Nil_Cons_iff}    ~ Nil=Cons(a,l)
  1246 
  1247 \tdx{list_mono}       A<=B ==> list(A) <= list(B)
  1248 
  1249 \tdx{map_ident}       l: list(A) ==> map(\%u. u, l) = l
  1250 \tdx{map_compose}     l: list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l)
  1251 \tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)
  1252 \tdx{map_type}
  1253     [| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)
  1254 \tdx{map_flat}
  1255     ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))
  1256 \end{ttbox}
  1257 \caption{Lists} \label{zf-list}
  1258 \end{figure}
  1259 
  1260 
  1261 Figure~\ref{zf-list} presents the set of lists over~$A$, ${\tt list}(A)$.  The
  1262 definition employs Isabelle's datatype package, which defines the introduction
  1263 and induction rules automatically, as well as the constructors, case operator
  1264 (\verb|list_case|) and recursion operator.  The theory then defines the usual
  1265 list functions by primitive recursion.  See theory \texttt{List}.
  1266 
  1267 
  1268 \subsection{Miscellaneous}
  1269 
  1270 \begin{figure}
  1271 \begin{constants} 
  1272   \it symbol  & \it meta-type & \it priority & \it description \\ 
  1273   \sdx{O}       & $[i,i]\To i$  &  Right 60     & composition ($\circ$) \\
  1274   \cdx{id}      & $i\To i$      &       & identity function \\
  1275   \cdx{inj}     & $[i,i]\To i$  &       & injective function space\\
  1276   \cdx{surj}    & $[i,i]\To i$  &       & surjective function space\\
  1277   \cdx{bij}     & $[i,i]\To i$  &       & bijective function space
  1278 \end{constants}
  1279 
  1280 \begin{ttbox}
  1281 \tdx{comp_def}  r O s     == {\ttlbrace}xz : domain(s)*range(r) . 
  1282                         EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r{\ttrbrace}
  1283 \tdx{id_def}    id(A)     == (lam x:A. x)
  1284 \tdx{inj_def}   inj(A,B)  == {\ttlbrace} f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x {\ttrbrace}
  1285 \tdx{surj_def}  surj(A,B) == {\ttlbrace} f: A->B . ALL y:B. EX x:A. f`x=y {\ttrbrace}
  1286 \tdx{bij_def}   bij(A,B)  == inj(A,B) Int surj(A,B)
  1287 
  1288 
  1289 \tdx{left_inverse}     [| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a
  1290 \tdx{right_inverse}    [| f: inj(A,B);  b: range(f) |] ==> 
  1291                  f`(converse(f)`b) = b
  1292 
  1293 \tdx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A)
  1294 \tdx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A)
  1295 
  1296 \tdx{comp_type}        [| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C
  1297 \tdx{comp_assoc}       (r O s) O t = r O (s O t)
  1298 
  1299 \tdx{left_comp_id}     r<=A*B ==> id(B) O r = r
  1300 \tdx{right_comp_id}    r<=A*B ==> r O id(A) = r
  1301 
  1302 \tdx{comp_func}        [| g:A->B; f:B->C |] ==> (f O g):A->C
  1303 \tdx{comp_func_apply}  [| g:A->B; f:B->C; a:A |] ==> (f O g)`a = f`(g`a)
  1304 
  1305 \tdx{comp_inj}         [| g:inj(A,B);  f:inj(B,C)  |] ==> (f O g):inj(A,C)
  1306 \tdx{comp_surj}        [| g:surj(A,B); f:surj(B,C) |] ==> (f O g):surj(A,C)
  1307 \tdx{comp_bij}         [| g:bij(A,B); f:bij(B,C) |] ==> (f O g):bij(A,C)
  1308 
  1309 \tdx{left_comp_inverse}     f: inj(A,B) ==> converse(f) O f = id(A)
  1310 \tdx{right_comp_inverse}    f: surj(A,B) ==> f O converse(f) = id(B)
  1311 
  1312 \tdx{bij_disjoint_Un}   
  1313     [| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> 
  1314     (f Un g) : bij(A Un C, B Un D)
  1315 
  1316 \tdx{restrict_bij}  [| f:inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)
  1317 \end{ttbox}
  1318 \caption{Permutations} \label{zf-perm}
  1319 \end{figure}
  1320 
  1321 The theory \thydx{Perm} is concerned with permutations (bijections) and
  1322 related concepts.  These include composition of relations, the identity
  1323 relation, and three specialized function spaces: injective, surjective and
  1324 bijective.  Figure~\ref{zf-perm} displays many of their properties that
  1325 have been proved.  These results are fundamental to a treatment of
  1326 equipollence and cardinality.
  1327 
  1328 Theory \thydx{Univ} defines a `universe' $\texttt{univ}(A)$, which is used by
  1329 the datatype package.  This set contains $A$ and the
  1330 natural numbers.  Vitally, it is closed under finite products: ${\tt
  1331   univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$.  This theory also
  1332 defines the cumulative hierarchy of axiomatic set theory, which
  1333 traditionally is written $V@\alpha$ for an ordinal~$\alpha$.  The
  1334 `universe' is a simple generalization of~$V@\omega$.
  1335 
  1336 Theory \thydx{QUniv} defines a `universe' ${\tt quniv}(A)$, which is used by
  1337 the datatype package to construct codatatypes such as streams.  It is
  1338 analogous to ${\tt univ}(A)$ (and is defined in terms of it) but is closed
  1339 under the non-standard product and sum.
  1340 
  1341 
  1342 \section{Automatic Tools}
  1343 
  1344 ZF provides the simplifier and the classical reasoner.  Moreover it supplies a
  1345 specialized tool to infer `types' of terms.
  1346 
  1347 \subsection{Simplification}
  1348 
  1349 ZF inherits simplification from FOL but adopts it for set theory.  The
  1350 extraction of rewrite rules takes the ZF primitives into account.  It can
  1351 strip bounded universal quantifiers from a formula; for example, ${\forall
  1352   x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp
  1353 f(x)=g(x)$.  Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in
  1354 A$ and~$P(a)$.  It can also break down $a\in A\int B$ and $a\in A-B$.
  1355 
  1356 Simplification tactics tactics such as \texttt{Asm_simp_tac} and
  1357 \texttt{Full_simp_tac} use the default simpset (\texttt{simpset()}), which
  1358 works for most purposes.  A small simplification set for set theory is
  1359 called~\ttindexbold{ZF_ss}, and you can even use \ttindex{FOL_ss} as a minimal
  1360 starting point.  \texttt{ZF_ss} contains congruence rules for all the binding
  1361 operators of ZF.  It contains all the conversion rules, such as \texttt{fst}
  1362 and \texttt{snd}, as well as the rewrites shown in Fig.\ts\ref{zf-simpdata}.
  1363 See the file \texttt{ZF/simpdata.ML} for a fuller list.
  1364 
  1365 
  1366 \subsection{Classical Reasoning}
  1367 
  1368 As for the classical reasoner, tactics such as \texttt{Blast_tac} and {\tt
  1369   Best_tac} refer to the default claset (\texttt{claset()}).  This works for
  1370 most purposes.  Named clasets include \ttindexbold{ZF_cs} (basic set theory)
  1371 and \ttindexbold{le_cs} (useful for reasoning about the relations $<$ and
  1372 $\le$).  You can use \ttindex{FOL_cs} as a minimal basis for building your own
  1373 clasets.  See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
  1374 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
  1375 
  1376 
  1377 \begin{figure}
  1378 \begin{eqnarray*}
  1379   a\in \emptyset        & \bimp &  \bot\\
  1380   a \in A \un B      & \bimp &  a\in A \disj a\in B\\
  1381   a \in A \int B      & \bimp &  a\in A \conj a\in B\\
  1382   a \in A-B             & \bimp &  a\in A \conj \neg (a\in B)\\
  1383   \pair{a,b}\in {\tt Sigma}(A,B)
  1384                         & \bimp &  a\in A \conj b\in B(a)\\
  1385   a \in {\tt Collect}(A,P)      & \bimp &  a\in A \conj P(a)\\
  1386   (\forall x \in \emptyset. P(x)) & \bimp &  \top\\
  1387   (\forall x \in A. \top)       & \bimp &  \top
  1388 \end{eqnarray*}
  1389 \caption{Some rewrite rules for set theory} \label{zf-simpdata}
  1390 \end{figure}
  1391 
  1392 
  1393 \subsection{Type-Checking Tactics}
  1394 \index{type-checking tactics}
  1395 
  1396 Isabelle/ZF provides simple tactics to help automate those proofs that are
  1397 essentially type-checking.  Such proofs are built by applying rules such as
  1398 these:
  1399 \begin{ttbox}
  1400 [| ?P ==> ?a: ?A; ~?P ==> ?b: ?A |] ==> (if ?P then ?a else ?b): ?A
  1401 
  1402 [| ?m : nat; ?n : nat |] ==> ?m #+ ?n : nat
  1403 
  1404 ?a : ?A ==> Inl(?a) : ?A + ?B  
  1405 \end{ttbox}
  1406 In typical applications, the goal has the form $t\in\Var{A}$: in other words,
  1407 we have a specific term~$t$ and need to infer its `type' by instantiating the
  1408 set variable~$\Var{A}$.  Neither the simplifier nor the classical reasoner
  1409 does this job well.  The if-then-else rule, and many similar ones, can make
  1410 the classical reasoner loop.  The simplifier refuses (on principle) to
  1411 instantiate variables during rewriting, so goals such as \texttt{i\#+j :\ ?A}
  1412 are left unsolved.
  1413 
  1414 The simplifier calls the type-checker to solve rewritten subgoals: this stage
  1415 can indeed instantiate variables.  If you have defined new constants and
  1416 proved type-checking rules for them, then insert the rules using
  1417 \texttt{AddTCs} and the rest should be automatic.  In particular, the
  1418 simplifier will use type-checking to help satisfy conditional rewrite rules.
  1419 Call the tactic \ttindex{Typecheck_tac} to break down all subgoals using
  1420 type-checking rules.
  1421 
  1422 Though the easiest way to invoke the type-checker is via the simplifier,
  1423 specialized applications may require more detailed knowledge of
  1424 the type-checking primitives.  They are modelled on the simplifier's:
  1425 \begin{ttdescription}
  1426 \item[\ttindexbold{tcset}] is the type of tcsets: sets of type-checking rules.
  1427 
  1428 \item[\ttindexbold{addTCs}] is an infix operator to add type-checking rules to
  1429   a tcset.
  1430   
  1431 \item[\ttindexbold{delTCs}] is an infix operator to remove type-checking rules
  1432   from a tcset.
  1433 
  1434 \item[\ttindexbold{typecheck_tac}] is a tactic for attempting to prove all
  1435   subgoals using the rules given in its argument, a tcset.
  1436 \end{ttdescription}
  1437 
  1438 Tcsets, like simpsets, are associated with theories and are merged when
  1439 theories are merged.  There are further primitives that use the default tcset.
  1440 \begin{ttdescription}
  1441 \item[\ttindexbold{tcset}] is a function to return the default tcset; use the
  1442   expression \texttt{tcset()}.
  1443 
  1444 \item[\ttindexbold{AddTCs}] adds type-checking rules to the default tcset.
  1445   
  1446 \item[\ttindexbold{DelTCs}] removes type-checking rules from the default
  1447   tcset.
  1448 
  1449 \item[\ttindexbold{Typecheck_tac}] calls \texttt{typecheck_tac} using the
  1450   default tcset.
  1451 \end{ttdescription}
  1452 
  1453 To supply some type-checking rules temporarily, using \texttt{Addrules} and
  1454 later \texttt{Delrules} is the simplest way.  There is also a high-tech
  1455 approach.  Call the simplifier with a new solver expressed using
  1456 \ttindexbold{type_solver_tac} and your temporary type-checking rules.
  1457 \begin{ttbox}
  1458 by (asm_simp_tac 
  1459      (simpset() setSolver type_solver_tac (tcset() addTCs prems)) 2);
  1460 \end{ttbox}
  1461 
  1462 
  1463 \section{Natural number and integer arithmetic}
  1464 
  1465 \index{arithmetic|(}
  1466 
  1467 \begin{figure}\small
  1468 \index{#*@{\tt\#*} symbol}
  1469 \index{*div symbol}
  1470 \index{*mod symbol}
  1471 \index{#+@{\tt\#+} symbol}
  1472 \index{#-@{\tt\#-} symbol}
  1473 \begin{constants}
  1474   \it symbol  & \it meta-type & \it priority & \it description \\ 
  1475   \cdx{nat}     & $i$                   &       & set of natural numbers \\
  1476   \cdx{nat_case}& $[i,i\To i,i]\To i$     &     & conditional for $nat$\\
  1477   \tt \#*       & $[i,i]\To i$  &  Left 70      & multiplication \\
  1478   \tt div       & $[i,i]\To i$  &  Left 70      & division\\
  1479   \tt mod       & $[i,i]\To i$  &  Left 70      & modulus\\
  1480   \tt \#+       & $[i,i]\To i$  &  Left 65      & addition\\
  1481   \tt \#-       & $[i,i]\To i$  &  Left 65      & subtraction
  1482 \end{constants}
  1483 
  1484 \begin{ttbox}
  1485 \tdx{nat_def}  nat == lfp(lam r: Pow(Inf). {\ttlbrace}0{\ttrbrace} Un {\ttlbrace}succ(x). x:r{\ttrbrace}
  1486 
  1487 \tdx{nat_case_def}  nat_case(a,b,k) == 
  1488               THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))
  1489 
  1490 \tdx{nat_0I}           0 : nat
  1491 \tdx{nat_succI}        n : nat ==> succ(n) : nat
  1492 
  1493 \tdx{nat_induct}        
  1494     [| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) 
  1495     |] ==> P(n)
  1496 
  1497 \tdx{nat_case_0}      nat_case(a,b,0) = a
  1498 \tdx{nat_case_succ}   nat_case(a,b,succ(m)) = b(m)
  1499 
  1500 \tdx{add_0_natify}     0 #+ n = natify(n)
  1501 \tdx{add_succ}         succ(m) #+ n = succ(m #+ n)
  1502 
  1503 \tdx{mult_type}        m #* n : nat
  1504 \tdx{mult_0}           0 #* n = 0
  1505 \tdx{mult_succ}        succ(m) #* n = n #+ (m #* n)
  1506 \tdx{mult_commute}     m #* n = n #* m
  1507 \tdx{add_mult_dist}    (m #+ n) #* k = (m #* k) #+ (n #* k)
  1508 \tdx{mult_assoc}       (m #* n) #* k = m #* (n #* k)
  1509 \tdx{mod_div_equality} m: nat ==> (m div n)#*n #+ m mod n = m
  1510 \end{ttbox}
  1511 \caption{The natural numbers} \label{zf-nat}
  1512 \end{figure}
  1513 
  1514 \index{natural numbers}
  1515 
  1516 Theory \thydx{Nat} defines the natural numbers and mathematical
  1517 induction, along with a case analysis operator.  The set of natural
  1518 numbers, here called \texttt{nat}, is known in set theory as the ordinal~$\omega$.
  1519 
  1520 Theory \thydx{Arith} develops arithmetic on the natural numbers
  1521 (Fig.\ts\ref{zf-nat}).  Addition, multiplication and subtraction are defined
  1522 by primitive recursion.  Division and remainder are defined by repeated
  1523 subtraction, which requires well-founded recursion; the termination argument
  1524 relies on the divisor's being non-zero.  Many properties are proved:
  1525 commutative, associative and distributive laws, identity and cancellation
  1526 laws, etc.  The most interesting result is perhaps the theorem $a \bmod b +
  1527 (a/b)\times b = a$.
  1528 
  1529 To minimize the need for tedious proofs of $t\in\texttt{nat}$, the arithmetic
  1530 operators coerce their arguments to be natural numbers.  The function
  1531 \cdx{natify} is defined such that $\texttt{natify}(n) = n$ if $n$ is a natural
  1532 number, $\texttt{natify}(\texttt{succ}(x)) =
  1533 \texttt{succ}(\texttt{natify}(x))$ for all $x$, and finally
  1534 $\texttt{natify}(x)=0$ in all other cases.  The benefit is that the addition,
  1535 subtraction, multiplication, division and remainder operators always return
  1536 natural numbers, regardless of their arguments.  Algebraic laws (commutative,
  1537 associative, distributive) are unconditional.  Occurrences of \texttt{natify}
  1538 as operands of those operators are simplified away.  Any remaining occurrences
  1539 can either be tolerated or else eliminated by proving that the argument is a
  1540 natural number.
  1541 
  1542 The simplifier automatically cancels common terms on the opposite sides of
  1543 subtraction and of relations ($=$, $<$ and $\le$).  Here is an example:
  1544 \begin{ttbox}
  1545  1. i #+ j #+ k #- j < k #+ l
  1546 > by (Simp_tac 1);
  1547  1. natify(i) < natify(l)
  1548 \end{ttbox}
  1549 Given the assumptions \texttt{i:nat} and \texttt{l:nat}, both occurrences of
  1550 \cdx{natify} would be simplified away.
  1551 
  1552 
  1553 \begin{figure}\small
  1554 \index{$*@{\tt\$*} symbol}
  1555 \index{$+@{\tt\$+} symbol}
  1556 \index{$-@{\tt\$-} symbol}
  1557 \begin{constants}
  1558   \it symbol  & \it meta-type & \it priority & \it description \\ 
  1559   \cdx{int}     & $i$                   &       & set of integers \\
  1560   \tt \$*       & $[i,i]\To i$  &  Left 70      & multiplication \\
  1561   \tt \$+       & $[i,i]\To i$  &  Left 65      & addition\\
  1562   \tt \$-       & $[i,i]\To i$  &  Left 65      & subtraction\\
  1563   \tt \$<       & $[i,i]\To o$  &  Left 50      & $<$ on integers\\
  1564   \tt \$<=      & $[i,i]\To o$  &  Left 50      & $\le$ on integers
  1565 \end{constants}
  1566 
  1567 \begin{ttbox}
  1568 \tdx{zadd_0_intify}     0 $+ n = intify(n)
  1569 
  1570 \tdx{zmult_type}        m $* n : int
  1571 \tdx{zmult_0}           0 $* n = 0
  1572 \tdx{zmult_commute}     m $* n = n $* m
  1573 \tdx{zadd_zmult_dist}    (m $+ n) $* k = (m $* k) $+ (n $* k)
  1574 \tdx{zmult_assoc}       (m $* n) $* k = m $* (n $* k)
  1575 \end{ttbox}
  1576 \caption{The integers} \label{zf-int}
  1577 \end{figure}
  1578 
  1579 
  1580 \index{integers}
  1581 
  1582 Theory \thydx{Int} defines the integers, as equivalence classes of natural
  1583 numbers.   Figure~\ref{zf-int} presents a tidy collection of laws.  In
  1584 fact, a large library of facts is proved, including monotonicity laws for
  1585 addition and multiplication, covering both positive and negative operands.  
  1586 
  1587 As with the natural numbers, the need for typing proofs is minimized.  All the
  1588 operators defined in Fig.\ts\ref{zf-int} coerce their operands to integers by
  1589 applying the function \cdx{intify}.  This function is the identity on integers
  1590 and maps other operands to zero.
  1591 
  1592 Decimal notation is provided for the integers.  Numbers, written as
  1593 \texttt{\#$nnn$} or \texttt{\#-$nnn$}, are represented internally in
  1594 two's-complement binary.  Expressions involving addition, subtraction and
  1595 multiplication of numeral constants are evaluated (with acceptable efficiency)
  1596 by simplification.  The simplifier also collects similar terms, multiplying
  1597 them by a numerical coefficient.  It also cancels occurrences of the same
  1598 terms on the other side of the relational operators.  Example:
  1599 \begin{ttbox}
  1600  1. y $+ z $+ #-3 $* x $+ y $<= x $* #2 $+ z
  1601 > by (Simp_tac 1);
  1602  1. #2 $* y $<= #5 $* x
  1603 \end{ttbox}
  1604 For more information on the integers, please see the theories on directory
  1605 \texttt{ZF/Integ}. 
  1606 
  1607 \index{arithmetic|)}
  1608 
  1609 
  1610 \section{Datatype definitions}
  1611 \label{sec:ZF:datatype}
  1612 \index{*datatype|(}
  1613 
  1614 The \ttindex{datatype} definition package of ZF constructs inductive datatypes
  1615 similar to those of \ML.  It can also construct coinductive datatypes
  1616 (codatatypes), which are non-well-founded structures such as streams.  It
  1617 defines the set using a fixed-point construction and proves induction rules,
  1618 as well as theorems for recursion and case combinators.  It supplies
  1619 mechanisms for reasoning about freeness.  The datatype package can handle both
  1620 mutual and indirect recursion.
  1621 
  1622 
  1623 \subsection{Basics}
  1624 \label{subsec:datatype:basics}
  1625 
  1626 A \texttt{datatype} definition has the following form:
  1627 \[
  1628 \begin{array}{llcl}
  1629 \mathtt{datatype} & t@1(A@1,\ldots,A@h) & = &
  1630   constructor^1@1 ~\mid~ \ldots ~\mid~ constructor^1@{k@1} \\
  1631  & & \vdots \\
  1632 \mathtt{and} & t@n(A@1,\ldots,A@h) & = &
  1633   constructor^n@1~ ~\mid~ \ldots ~\mid~ constructor^n@{k@n}
  1634 \end{array}
  1635 \]
  1636 Here $t@1$, \ldots,~$t@n$ are identifiers and $A@1$, \ldots,~$A@h$ are
  1637 variables: the datatype's parameters.  Each constructor specification has the
  1638 form \dquotesoff
  1639 \[ C \hbox{\tt~( } \hbox{\tt"} x@1 \hbox{\tt:} T@1 \hbox{\tt"},\;
  1640                    \ldots,\;
  1641                    \hbox{\tt"} x@m \hbox{\tt:} T@m \hbox{\tt"}
  1642      \hbox{\tt~)}
  1643 \]
  1644 Here $C$ is the constructor name, and variables $x@1$, \ldots,~$x@m$ are the
  1645 constructor arguments, belonging to the sets $T@1$, \ldots, $T@m$,
  1646 respectively.  Typically each $T@j$ is either a constant set, a datatype
  1647 parameter (one of $A@1$, \ldots, $A@h$) or a recursive occurrence of one of
  1648 the datatypes, say $t@i(A@1,\ldots,A@h)$.  More complex possibilities exist,
  1649 but they are much harder to realize.  Often, additional information must be
  1650 supplied in the form of theorems.
  1651 
  1652 A datatype can occur recursively as the argument of some function~$F$.  This
  1653 is called a {\em nested} (or \emph{indirect}) occurrence.  It is only allowed
  1654 if the datatype package is given a theorem asserting that $F$ is monotonic.
  1655 If the datatype has indirect occurrences, then Isabelle/ZF does not support
  1656 recursive function definitions.
  1657 
  1658 A simple example of a datatype is \texttt{list}, which is built-in, and is
  1659 defined by
  1660 \begin{ttbox}
  1661 consts     list :: i=>i
  1662 datatype  "list(A)" = Nil | Cons ("a:A", "l: list(A)")
  1663 \end{ttbox}
  1664 Note that the datatype operator must be declared as a constant first.
  1665 However, the package declares the constructors.  Here, \texttt{Nil} gets type
  1666 $i$ and \texttt{Cons} gets type $[i,i]\To i$.
  1667 
  1668 Trees and forests can be modelled by the mutually recursive datatype
  1669 definition
  1670 \begin{ttbox}
  1671 consts     tree, forest, tree_forest :: i=>i
  1672 datatype  "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
  1673 and       "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
  1674 \end{ttbox}
  1675 Here $\texttt{tree}(A)$ is the set of trees over $A$, $\texttt{forest}(A)$ is
  1676 the set of forests over $A$, and  $\texttt{tree_forest}(A)$ is the union of
  1677 the previous two sets.  All three operators must be declared first.
  1678 
  1679 The datatype \texttt{term}, which is defined by
  1680 \begin{ttbox}
  1681 consts     term :: i=>i
  1682 datatype  "term(A)" = Apply ("a: A", "l: list(term(A))")
  1683   monos "[list_mono]"
  1684 \end{ttbox}
  1685 is an example of nested recursion.  (The theorem \texttt{list_mono} is proved
  1686 in file \texttt{List.ML}, and the \texttt{term} example is devaloped in theory
  1687 \thydx{ex/Term}.)
  1688 
  1689 \subsubsection{Freeness of the constructors}
  1690 
  1691 Constructors satisfy {\em freeness} properties.  Constructions are distinct,
  1692 for example $\texttt{Nil}\not=\texttt{Cons}(a,l)$, and they are injective, for
  1693 example $\texttt{Cons}(a,l)=\texttt{Cons}(a',l') \bimp a=a' \conj l=l'$.
  1694 Because the number of freeness is quadratic in the number of constructors, the
  1695 datatype package does not prove them.  Instead, it ensures that simplification
  1696 will prove them dynamically: when the simplifier encounters a formula
  1697 asserting the equality of two datatype constructors, it performs freeness
  1698 reasoning.  
  1699 
  1700 Freeness reasoning can also be done using the classical reasoner, but it is
  1701 more complicated.  You have to add some safe elimination rules rules to the
  1702 claset.  For the \texttt{list} datatype, they are called
  1703 \texttt{list.free_SEs}.  Occasionally this exposes the underlying
  1704 representation of some constructor, which can be rectified using the command
  1705 \hbox{\tt fold_tac list.con_defs}.
  1706 
  1707 
  1708 \subsubsection{Structural induction}
  1709 
  1710 The datatype package also provides structural induction rules.  For datatypes
  1711 without mutual or nested recursion, the rule has the form exemplified by
  1712 \texttt{list.induct} in Fig.\ts\ref{zf-list}.  For mutually recursive
  1713 datatypes, the induction rule is supplied in two forms.  Consider datatype
  1714 \texttt{TF}.  The rule \texttt{tree_forest.induct} performs induction over a
  1715 single predicate~\texttt{P}, which is presumed to be defined for both trees
  1716 and forests:
  1717 \begin{ttbox}
  1718 [| x : tree_forest(A);
  1719    !!a f. [| a : A; f : forest(A); P(f) |] ==> P(Tcons(a, f)); 
  1720    P(Fnil);
  1721    !!f t. [| t : tree(A); P(t); f : forest(A); P(f) |]
  1722           ==> P(Fcons(t, f)) 
  1723 |] ==> P(x)
  1724 \end{ttbox}
  1725 The rule \texttt{tree_forest.mutual_induct} performs induction over two
  1726 distinct predicates, \texttt{P_tree} and \texttt{P_forest}.
  1727 \begin{ttbox}
  1728 [| !!a f.
  1729       [| a : A; f : forest(A); P_forest(f) |] ==> P_tree(Tcons(a, f));
  1730    P_forest(Fnil);
  1731    !!f t. [| t : tree(A); P_tree(t); f : forest(A); P_forest(f) |]
  1732           ==> P_forest(Fcons(t, f)) 
  1733 |] ==> (ALL za. za : tree(A) --> P_tree(za)) &
  1734     (ALL za. za : forest(A) --> P_forest(za))
  1735 \end{ttbox}
  1736 
  1737 For datatypes with nested recursion, such as the \texttt{term} example from
  1738 above, things are a bit more complicated.  The rule \texttt{term.induct}
  1739 refers to the monotonic operator, \texttt{list}:
  1740 \begin{ttbox}
  1741 [| x : term(A);
  1742    !!a l. [| a: A; l: list(Collect(term(A), P)) |] ==> P(Apply(a, l)) 
  1743 |] ==> P(x)
  1744 \end{ttbox}
  1745 The file \texttt{ex/Term.ML} derives two higher-level induction rules, one of
  1746 which is particularly useful for proving equations:
  1747 \begin{ttbox}
  1748 [| t : term(A);
  1749    !!x zs. [| x : A; zs : list(term(A)); map(f, zs) = map(g, zs) |]
  1750            ==> f(Apply(x, zs)) = g(Apply(x, zs)) 
  1751 |] ==> f(t) = g(t)  
  1752 \end{ttbox}
  1753 How this can be generalized to other nested datatypes is a matter for future
  1754 research.
  1755 
  1756 
  1757 \subsubsection{The \texttt{case} operator}
  1758 
  1759 The package defines an operator for performing case analysis over the
  1760 datatype.  For \texttt{list}, it is called \texttt{list_case} and satisfies
  1761 the equations
  1762 \begin{ttbox}
  1763 list_case(f_Nil, f_Cons, []) = f_Nil
  1764 list_case(f_Nil, f_Cons, Cons(a, l)) = f_Cons(a, l)
  1765 \end{ttbox}
  1766 Here \texttt{f_Nil} is the value to return if the argument is \texttt{Nil} and
  1767 \texttt{f_Cons} is a function that computes the value to return if the
  1768 argument has the form $\texttt{Cons}(a,l)$.  The function can be expressed as
  1769 an abstraction, over patterns if desired (\S\ref{sec:pairs}).
  1770 
  1771 For mutually recursive datatypes, there is a single \texttt{case} operator.
  1772 In the tree/forest example, the constant \texttt{tree_forest_case} handles all
  1773 of the constructors of the two datatypes.
  1774 
  1775 
  1776 
  1777 
  1778 \subsection{Defining datatypes}
  1779 
  1780 The theory syntax for datatype definitions is shown in
  1781 Fig.~\ref{datatype-grammar}.  In order to be well-formed, a datatype
  1782 definition has to obey the rules stated in the previous section.  As a result
  1783 the theory is extended with the new types, the constructors, and the theorems
  1784 listed in the previous section.  The quotation marks are necessary because
  1785 they enclose general Isabelle formul\ae.
  1786 
  1787 \begin{figure}
  1788 \begin{rail}
  1789 datatype : ( 'datatype' | 'codatatype' ) datadecls;
  1790 
  1791 datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and'
  1792          ;
  1793 constructor : name ( () | consargs )  ( () | ( '(' mixfix ')' ) )
  1794          ;
  1795 consargs : '(' ('"' var ':' term '"' + ',') ')'
  1796          ;
  1797 \end{rail}
  1798 \caption{Syntax of datatype declarations}
  1799 \label{datatype-grammar}
  1800 \end{figure}
  1801 
  1802 Codatatypes are declared like datatypes and are identical to them in every
  1803 respect except that they have a coinduction rule instead of an induction rule.
  1804 Note that while an induction rule has the effect of limiting the values
  1805 contained in the set, a coinduction rule gives a way of constructing new
  1806 values of the set.
  1807 
  1808 Most of the theorems about datatypes become part of the default simpset.  You
  1809 never need to see them again because the simplifier applies them
  1810 automatically.  Induction or exhaustion are usually invoked by hand,
  1811 usually via these special-purpose tactics:
  1812 \begin{ttdescription}
  1813 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] applies structural
  1814   induction on variable $x$ to subgoal $i$, provided the type of $x$ is a
  1815   datatype.  The induction variable should not occur among other assumptions
  1816   of the subgoal.
  1817 \end{ttdescription}
  1818 In some cases, induction is overkill and a case distinction over all
  1819 constructors of the datatype suffices.
  1820 \begin{ttdescription}
  1821 \item[\ttindexbold{exhaust_tac} {\tt"}$x${\tt"} $i$]
  1822  performs an exhaustive case analysis for the variable~$x$.
  1823 \end{ttdescription}
  1824 
  1825 Both tactics can only be applied to a variable, whose typing must be given in
  1826 some assumption, for example the assumption \texttt{x:\ list(A)}.  The tactics
  1827 also work for the natural numbers (\texttt{nat}) and disjoint sums, although
  1828 these sets were not defined using the datatype package.  (Disjoint sums are
  1829 not recursive, so only \texttt{exhaust_tac} is available.)
  1830 
  1831 \bigskip
  1832 Here are some more details for the technically minded.  Processing the
  1833 theory file produces an \ML\ structure which, in addition to the usual
  1834 components, contains a structure named $t$ for each datatype $t$ defined in
  1835 the file.  Each structure $t$ contains the following elements:
  1836 \begin{ttbox}
  1837 val intrs         : thm list  \textrm{the introduction rules}
  1838 val elim          : thm       \textrm{the elimination (case analysis) rule}
  1839 val induct        : thm       \textrm{the standard induction rule}
  1840 val mutual_induct : thm       \textrm{the mutual induction rule, or \texttt{True}}
  1841 val case_eqns     : thm list  \textrm{equations for the case operator}
  1842 val recursor_eqns : thm list  \textrm{equations for the recursor}
  1843 val con_defs      : thm list  \textrm{definitions of the case operator and constructors}
  1844 val free_iffs     : thm list  \textrm{logical equivalences for proving freeness}
  1845 val free_SEs      : thm list  \textrm{elimination rules for proving freeness}
  1846 val mk_free       : string -> thm  \textrm{A function for proving freeness theorems}
  1847 val mk_cases      : string -> thm  \textrm{case analysis, see below}
  1848 val defs          : thm list  \textrm{definitions of operators}
  1849 val bnd_mono      : thm list  \textrm{monotonicity property}
  1850 val dom_subset    : thm list  \textrm{inclusion in `bounding set'}
  1851 \end{ttbox}
  1852 Furthermore there is the theorem $C$\texttt{_I} for every constructor~$C$; for
  1853 example, the \texttt{list} datatype's introduction rules are bound to the
  1854 identifiers \texttt{Nil_I} and \texttt{Cons_I}.
  1855 
  1856 For a codatatype, the component \texttt{coinduct} is the coinduction rule,
  1857 replacing the \texttt{induct} component.
  1858 
  1859 See the theories \texttt{ex/Ntree} and \texttt{ex/Brouwer} for examples of
  1860 infinitely branching datatypes.  See theory \texttt{ex/LList} for an example
  1861 of a codatatype.  Some of these theories illustrate the use of additional,
  1862 undocumented features of the datatype package.  Datatype definitions are
  1863 reduced to inductive definitions, and the advanced features should be
  1864 understood in that light.
  1865 
  1866 
  1867 \subsection{Examples}
  1868 
  1869 \subsubsection{The datatype of binary trees}
  1870 
  1871 Let us define the set $\texttt{bt}(A)$ of binary trees over~$A$.  The theory
  1872 must contain these lines:
  1873 \begin{ttbox}
  1874 consts   bt :: i=>i
  1875 datatype "bt(A)"  =  Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
  1876 \end{ttbox}
  1877 After loading the theory, we can prove, for example, that no tree equals its
  1878 left branch.  To ease the induction, we state the goal using quantifiers.
  1879 \begin{ttbox}
  1880 Goal "l : bt(A) ==> ALL x r. Br(x,l,r) ~= l";
  1881 {\out Level 0}
  1882 {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
  1883 {\out  1. l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
  1884 \end{ttbox}
  1885 This can be proved by the structural induction tactic:
  1886 \begin{ttbox}
  1887 by (induct_tac "l" 1);
  1888 {\out Level 1}
  1889 {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
  1890 {\out  1. ALL x r. Br(x, Lf, r) ~= Lf}
  1891 {\out  2. !!a t1 t2.}
  1892 {\out        [| a : A; t1 : bt(A);}
  1893 {\out           ALL x r. Br(x, t1, r) ~= t1; t2 : bt(A);}
  1894 {\out           ALL x r. Br(x, t2, r) ~= t2 |]}
  1895 {\out        ==> ALL x r. Br(x, Br(a, t1, t2), r) ~= Br(a, t1, t2)}
  1896 \end{ttbox}
  1897 Both subgoals are proved using \texttt{Auto_tac}, which performs the necessary
  1898 freeness reasoning. 
  1899 \begin{ttbox}
  1900 by Auto_tac;
  1901 {\out Level 2}
  1902 {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
  1903 {\out No subgoals!}
  1904 \end{ttbox}
  1905 To remove the quantifiers from the induction formula, we save the theorem using
  1906 \ttindex{qed_spec_mp}.
  1907 \begin{ttbox}
  1908 qed_spec_mp "Br_neq_left";
  1909 {\out val Br_neq_left = "?l : bt(?A) ==> Br(?x, ?l, ?r) ~= ?l" : thm}
  1910 \end{ttbox}
  1911 
  1912 When there are only a few constructors, we might prefer to prove the freenness
  1913 theorems for each constructor.  This is trivial, using the function given us
  1914 for that purpose:
  1915 \begin{ttbox}
  1916 val Br_iff = 
  1917     bt.mk_free "Br(a,l,r)=Br(a',l',r') <-> a=a' & l=l' & r=r'";
  1918 {\out val Br_iff =}
  1919 {\out   "Br(?a, ?l, ?r) = Br(?a', ?l', ?r') <->}
  1920 {\out                     ?a = ?a' & ?l = ?l' & ?r = ?r'" : thm}
  1921 \end{ttbox}
  1922 
  1923 The purpose of \ttindex{mk_cases} is to generate instances of the elimination
  1924 (case analysis) rule that have been simplified using freeness reasoning.  For
  1925 example, this instance of the elimination rule propagates type-checking
  1926 information from the premise $\texttt{Br}(a,l,r)\in\texttt{bt}(A)$:
  1927 \begin{ttbox}
  1928 val BrE = bt.mk_cases "Br(a,l,r) : bt(A)";
  1929 {\out val BrE =}
  1930 {\out   "[| Br(?a, ?l, ?r) : bt(?A);}
  1931 {\out       [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |]}
  1932 {\out    ==> ?Q" : thm}
  1933 \end{ttbox}
  1934 
  1935 
  1936 \subsubsection{Mixfix syntax in datatypes}
  1937 
  1938 Mixfix syntax is sometimes convenient.  The theory \texttt{ex/PropLog} makes a
  1939 deep embedding of propositional logic:
  1940 \begin{ttbox}
  1941 consts     prop :: i
  1942 datatype  "prop" = Fls
  1943                  | Var ("n: nat")                ("#_" [100] 100)
  1944                  | "=>" ("p: prop", "q: prop")   (infixr 90)
  1945 \end{ttbox}
  1946 The second constructor has a special $\#n$ syntax, while the third constructor
  1947 is an infixed arrow.
  1948 
  1949 
  1950 \subsubsection{A giant enumeration type}
  1951 
  1952 This example shows a datatype that consists of 60 constructors:
  1953 \begin{ttbox}
  1954 consts  enum :: i
  1955 datatype
  1956   "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
  1957          | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19
  1958          | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29
  1959          | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39
  1960          | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
  1961          | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
  1962 end
  1963 \end{ttbox}
  1964 The datatype package scales well.  Even though all properties are proved
  1965 rather than assumed, full processing of this definition takes under 15 seconds
  1966 (on a 300 MHz Pentium).  The constructors have a balanced representation,
  1967 essentially binary notation, so freeness properties can be proved fast.
  1968 \begin{ttbox}
  1969 Goal "C00 ~= C01";
  1970 by (Simp_tac 1);
  1971 \end{ttbox}
  1972 You need not derive such inequalities explicitly.  The simplifier will dispose
  1973 of them automatically.
  1974 
  1975 \index{*datatype|)}
  1976 
  1977 
  1978 \subsection{Recursive function definitions}\label{sec:ZF:recursive}
  1979 \index{recursive functions|see{recursion}}
  1980 \index{*primrec|(}
  1981 \index{recursion!primitive|(}
  1982 
  1983 Datatypes come with a uniform way of defining functions, {\bf primitive
  1984   recursion}.  Such definitions rely on the recursion operator defined by the
  1985 datatype package.  Isabelle proves the desired recursion equations as
  1986 theorems.
  1987 
  1988 In principle, one could introduce primitive recursive functions by asserting
  1989 their reduction rules as new axioms.  Here is a dangerous way of defining the
  1990 append function for lists:
  1991 \begin{ttbox}\slshape
  1992 consts  "\at" :: [i,i]=>i                        (infixr 60)
  1993 rules 
  1994    app_Nil   "[] \at ys = ys"
  1995    app_Cons  "(Cons(a,l)) \at ys = Cons(a, l \at ys)"
  1996 \end{ttbox}
  1997 Asserting axioms brings the danger of accidentally asserting nonsense.  It
  1998 should be avoided at all costs!
  1999 
  2000 The \ttindex{primrec} declaration is a safe means of defining primitive
  2001 recursive functions on datatypes:
  2002 \begin{ttbox}
  2003 consts  "\at" :: [i,i]=>i                        (infixr 60)
  2004 primrec 
  2005    "[] \at ys = ys"
  2006    "(Cons(a,l)) \at ys = Cons(a, l \at ys)"
  2007 \end{ttbox}
  2008 Isabelle will now check that the two rules do indeed form a primitive
  2009 recursive definition.  For example, the declaration
  2010 \begin{ttbox}
  2011 primrec
  2012    "[] \at ys = us"
  2013 \end{ttbox}
  2014 is rejected with an error message ``\texttt{Extra variables on rhs}''.
  2015 
  2016 
  2017 \subsubsection{Syntax of recursive definitions}
  2018 
  2019 The general form of a primitive recursive definition is
  2020 \begin{ttbox}
  2021 primrec
  2022     {\it reduction rules}
  2023 \end{ttbox}
  2024 where \textit{reduction rules} specify one or more equations of the form
  2025 \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
  2026 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
  2027 contains only the free variables on the left-hand side, and all recursive
  2028 calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$.  
  2029 There must be at most one reduction rule for each constructor.  The order is
  2030 immaterial.  For missing constructors, the function is defined to return zero.
  2031 
  2032 All reduction rules are added to the default simpset.
  2033 If you would like to refer to some rule by name, then you must prefix
  2034 the rule with an identifier.  These identifiers, like those in the
  2035 \texttt{rules} section of a theory, will be visible at the \ML\ level.
  2036 
  2037 The reduction rules for {\tt\at} become part of the default simpset, which
  2038 leads to short proof scripts:
  2039 \begin{ttbox}\underscoreon
  2040 Goal "xs: list(A) ==> (xs @ ys) @ zs = xs @ (ys @ zs)";
  2041 by (induct\_tac "xs" 1);
  2042 by (ALLGOALS Asm\_simp\_tac);
  2043 \end{ttbox}
  2044 
  2045 You can even use the \texttt{primrec} form with non-recursive datatypes and
  2046 with codatatypes.  Recursion is not allowed, but it provides a convenient
  2047 syntax for defining functions by cases.
  2048 
  2049 
  2050 \subsubsection{Example: varying arguments}
  2051 
  2052 All arguments, other than the recursive one, must be the same in each equation
  2053 and in each recursive call.  To get around this restriction, use explict
  2054 $\lambda$-abstraction and function application.  Here is an example, drawn
  2055 from the theory \texttt{Resid/Substitution}.  The type of redexes is declared
  2056 as follows:
  2057 \begin{ttbox}
  2058 consts  redexes :: i
  2059 datatype
  2060   "redexes" = Var ("n: nat")            
  2061             | Fun ("t: redexes")
  2062             | App ("b:bool" ,"f:redexes" , "a:redexes")
  2063 \end{ttbox}
  2064 
  2065 The function \texttt{lift} takes a second argument, $k$, which varies in
  2066 recursive calls.
  2067 \begin{ttbox}
  2068 primrec
  2069   "lift(Var(i)) = (lam k:nat. if i<k then Var(i) else Var(succ(i)))"
  2070   "lift(Fun(t)) = (lam k:nat. Fun(lift(t) ` succ(k)))"
  2071   "lift(App(b,f,a)) = (lam k:nat. App(b, lift(f)`k, lift(a)`k))"
  2072 \end{ttbox}
  2073 Now \texttt{lift(r)`k} satisfies the required recursion equations.
  2074 
  2075 \index{recursion!primitive|)}
  2076 \index{*primrec|)}
  2077 
  2078 
  2079 \section{Inductive and coinductive definitions}
  2080 \index{*inductive|(}
  2081 \index{*coinductive|(}
  2082 
  2083 An {\bf inductive definition} specifies the least set~$R$ closed under given
  2084 rules.  (Applying a rule to elements of~$R$ yields a result within~$R$.)  For
  2085 example, a structural operational semantics is an inductive definition of an
  2086 evaluation relation.  Dually, a {\bf coinductive definition} specifies the
  2087 greatest set~$R$ consistent with given rules.  (Every element of~$R$ can be
  2088 seen as arising by applying a rule to elements of~$R$.)  An important example
  2089 is using bisimulation relations to formalise equivalence of processes and
  2090 infinite data structures.
  2091 
  2092 A theory file may contain any number of inductive and coinductive
  2093 definitions.  They may be intermixed with other declarations; in
  2094 particular, the (co)inductive sets {\bf must} be declared separately as
  2095 constants, and may have mixfix syntax or be subject to syntax translations.
  2096 
  2097 Each (co)inductive definition adds definitions to the theory and also
  2098 proves some theorems.  Each definition creates an \ML\ structure, which is a
  2099 substructure of the main theory structure.
  2100 This package is described in detail in a separate paper,%
  2101 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
  2102   distributed with Isabelle as \emph{A Fixedpoint Approach to 
  2103  (Co)Inductive and (Co)Datatype Definitions}.}  %
  2104 which you might refer to for background information.
  2105 
  2106 
  2107 \subsection{The syntax of a (co)inductive definition}
  2108 An inductive definition has the form
  2109 \begin{ttbox}
  2110 inductive
  2111   domains    {\it domain declarations}
  2112   intrs      {\it introduction rules}
  2113   monos      {\it monotonicity theorems}
  2114   con_defs   {\it constructor definitions}
  2115   type_intrs {\it introduction rules for type-checking}
  2116   type_elims {\it elimination rules for type-checking}
  2117 \end{ttbox}
  2118 A coinductive definition is identical, but starts with the keyword
  2119 {\tt co\-inductive}.  
  2120 
  2121 The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
  2122 sections are optional.  If present, each is specified either as a list of
  2123 identifiers or as a string.  If the latter, then the string must be a valid
  2124 \textsc{ml} expression of type {\tt thm list}.  The string is simply inserted
  2125 into the {\tt _thy.ML} file; if it is ill-formed, it will trigger \textsc{ml}
  2126 error messages.  You can then inspect the file on the temporary directory.
  2127 
  2128 \begin{description}
  2129 \item[\it domain declarations] are items of the form
  2130   {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with
  2131   its domain.  (The domain is some existing set that is large enough to
  2132   hold the new set being defined.)
  2133 
  2134 \item[\it introduction rules] specify one or more introduction rules in
  2135   the form {\it ident\/}~{\it string}, where the identifier gives the name of
  2136   the rule in the result structure.
  2137 
  2138 \item[\it monotonicity theorems] are required for each operator applied to
  2139   a recursive set in the introduction rules.  There \textbf{must} be a theorem
  2140   of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each premise $t\in M(R_i)$
  2141   in an introduction rule!
  2142 
  2143 \item[\it constructor definitions] contain definitions of constants
  2144   appearing in the introduction rules.  The (co)datatype package supplies
  2145   the constructors' definitions here.  Most (co)inductive definitions omit
  2146   this section; one exception is the primitive recursive functions example;
  2147   see theory \texttt{ex/Primrec}.
  2148   
  2149 \item[\it type\_intrs] consists of introduction rules for type-checking the
  2150   definition: for demonstrating that the new set is included in its domain.
  2151   (The proof uses depth-first search.)
  2152 
  2153 \item[\it type\_elims] consists of elimination rules for type-checking the
  2154   definition.  They are presumed to be safe and are applied as often as
  2155   possible prior to the {\tt type\_intrs} search.
  2156 \end{description}
  2157 
  2158 The package has a few restrictions:
  2159 \begin{itemize}
  2160 \item The theory must separately declare the recursive sets as
  2161   constants.
  2162 
  2163 \item The names of the recursive sets must be identifiers, not infix
  2164 operators.  
  2165 
  2166 \item Side-conditions must not be conjunctions.  However, an introduction rule
  2167 may contain any number of side-conditions.
  2168 
  2169 \item Side-conditions of the form $x=t$, where the variable~$x$ does not
  2170   occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
  2171 \end{itemize}
  2172 
  2173 
  2174 \subsection{Example of an inductive definition}
  2175 
  2176 Two declarations, included in a theory file, define the finite powerset
  2177 operator.  First we declare the constant~\texttt{Fin}.  Then we declare it
  2178 inductively, with two introduction rules:
  2179 \begin{ttbox}
  2180 consts  Fin :: i=>i
  2181 
  2182 inductive
  2183   domains   "Fin(A)" <= "Pow(A)"
  2184   intrs
  2185     emptyI  "0 : Fin(A)"
  2186     consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
  2187   type_intrs empty_subsetI, cons_subsetI, PowI
  2188   type_elims "[make_elim PowD]"
  2189 \end{ttbox}
  2190 The resulting theory structure contains a substructure, called~\texttt{Fin}.
  2191 It contains the \texttt{Fin}$~A$ introduction rules as the list
  2192 \texttt{Fin.intrs}, and also individually as \texttt{Fin.emptyI} and
  2193 \texttt{Fin.consI}.  The induction rule is \texttt{Fin.induct}.
  2194 
  2195 The chief problem with making (co)inductive definitions involves type-checking
  2196 the rules.  Sometimes, additional theorems need to be supplied under
  2197 \texttt{type_intrs} or \texttt{type_elims}.  If the package fails when trying
  2198 to prove your introduction rules, then set the flag \ttindexbold{trace_induct}
  2199 to \texttt{true} and try again.  (See the manual \emph{A Fixedpoint Approach
  2200   \ldots} for more discussion of type-checking.)
  2201 
  2202 In the example above, $\texttt{Pow}(A)$ is given as the domain of
  2203 $\texttt{Fin}(A)$, for obviously every finite subset of~$A$ is a subset
  2204 of~$A$.  However, the inductive definition package can only prove that given a
  2205 few hints.
  2206 Here is the output that results (with the flag set) when the
  2207 \texttt{type_intrs} and \texttt{type_elims} are omitted from the inductive
  2208 definition above:
  2209 \begin{ttbox}
  2210 Inductive definition Finite.Fin
  2211 Fin(A) ==
  2212 lfp(Pow(A),
  2213     \%X. {z: Pow(A) . z = 0 | (EX a b. z = cons(a, b) & a : A & b : X)})
  2214   Proving monotonicity...
  2215 \ttbreak
  2216   Proving the introduction rules...
  2217 The type-checking subgoal:
  2218 0 : Fin(A)
  2219  1. 0 : Pow(A)
  2220 \ttbreak
  2221 The subgoal after monos, type_elims:
  2222 0 : Fin(A)
  2223  1. 0 : Pow(A)
  2224 *** prove_goal: tactic failed
  2225 \end{ttbox}
  2226 We see the need to supply theorems to let the package prove
  2227 $\emptyset\in\texttt{Pow}(A)$.  Restoring the \texttt{type_intrs} but not the
  2228 \texttt{type_elims}, we again get an error message:
  2229 \begin{ttbox}
  2230 The type-checking subgoal:
  2231 0 : Fin(A)
  2232  1. 0 : Pow(A)
  2233 \ttbreak
  2234 The subgoal after monos, type_elims:
  2235 0 : Fin(A)
  2236  1. 0 : Pow(A)
  2237 \ttbreak
  2238 The type-checking subgoal:
  2239 cons(a, b) : Fin(A)
  2240  1. [| a : A; b : Fin(A) |] ==> cons(a, b) : Pow(A)
  2241 \ttbreak
  2242 The subgoal after monos, type_elims:
  2243 cons(a, b) : Fin(A)
  2244  1. [| a : A; b : Pow(A) |] ==> cons(a, b) : Pow(A)
  2245 *** prove_goal: tactic failed
  2246 \end{ttbox}
  2247 The first rule has been type-checked, but the second one has failed.  The
  2248 simplest solution to such problems is to prove the failed subgoal separately
  2249 and to supply it under \texttt{type_intrs}.  The solution actually used is
  2250 to supply, under \texttt{type_elims}, a rule that changes
  2251 $b\in\texttt{Pow}(A)$ to $b\subseteq A$; together with \texttt{cons_subsetI}
  2252 and \texttt{PowI}, it is enough to complete the type-checking.
  2253 
  2254 
  2255 
  2256 \subsection{Further examples}
  2257 
  2258 An inductive definition may involve arbitrary monotonic operators.  Here is a
  2259 standard example: the accessible part of a relation.  Note the use
  2260 of~\texttt{Pow} in the introduction rule and the corresponding mention of the
  2261 rule \verb|Pow_mono| in the \texttt{monos} list.  If the desired rule has a
  2262 universally quantified premise, usually the effect can be obtained using
  2263 \texttt{Pow}.
  2264 \begin{ttbox}
  2265 consts  acc :: i=>i
  2266 inductive
  2267   domains "acc(r)" <= "field(r)"
  2268   intrs
  2269     vimage  "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
  2270   monos      Pow_mono
  2271 \end{ttbox}
  2272 
  2273 Finally, here is a coinductive definition.  It captures (as a bisimulation)
  2274 the notion of equality on lazy lists, which are first defined as a codatatype:
  2275 \begin{ttbox}
  2276 consts  llist :: i=>i
  2277 codatatype  "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
  2278 \ttbreak
  2279 
  2280 consts  lleq :: i=>i
  2281 coinductive
  2282   domains "lleq(A)" <= "llist(A) * llist(A)"
  2283   intrs
  2284     LNil  "<LNil, LNil> : lleq(A)"
  2285     LCons "[| a:A; <l,l'>: lleq(A) |] 
  2286            ==> <LCons(a,l), LCons(a,l')>: lleq(A)"
  2287   type_intrs  "llist.intrs"
  2288 \end{ttbox}
  2289 This use of \texttt{type_intrs} is typical: the relation concerns the
  2290 codatatype \texttt{llist}, so naturally the introduction rules for that
  2291 codatatype will be required for type-checking the rules.
  2292 
  2293 The Isabelle distribution contains many other inductive definitions.  Simple
  2294 examples are collected on subdirectory \texttt{ZF/ex}.  The directory
  2295 \texttt{Coind} and the theory \texttt{ZF/ex/LList} contain coinductive
  2296 definitions.  Larger examples may be found on other subdirectories of
  2297 \texttt{ZF}, such as \texttt{IMP}, and \texttt{Resid}.
  2298 
  2299 
  2300 \subsection{The result structure}
  2301 
  2302 Each (co)inductive set defined in a theory file generates an \ML\ substructure
  2303 having the same name.  The the substructure contains the following elements:
  2304 
  2305 \begin{ttbox}
  2306 val intrs         : thm list  \textrm{the introduction rules}
  2307 val elim          : thm       \textrm{the elimination (case analysis) rule}
  2308 val mk_cases      : string -> thm  \textrm{case analysis, see below}
  2309 val induct        : thm       \textrm{the standard induction rule}
  2310 val mutual_induct : thm       \textrm{the mutual induction rule, or \texttt{True}}
  2311 val defs          : thm list  \textrm{definitions of operators}
  2312 val bnd_mono      : thm list  \textrm{monotonicity property}
  2313 val dom_subset    : thm list  \textrm{inclusion in `bounding set'}
  2314 \end{ttbox}
  2315 Furthermore there is the theorem $C$\texttt{_I} for every constructor~$C$; for
  2316 example, the \texttt{list} datatype's introduction rules are bound to the
  2317 identifiers \texttt{Nil_I} and \texttt{Cons_I}.
  2318 
  2319 For a codatatype, the component \texttt{coinduct} is the coinduction rule,
  2320 replacing the \texttt{induct} component.
  2321 
  2322 Recall that \ttindex{mk_cases} generates simplified instances of the
  2323 elimination (case analysis) rule.  It is as useful for inductive definitions
  2324 as it is for datatypes.  There are many examples in the theory
  2325 \texttt{ex/Comb}, which is discussed at length
  2326 elsewhere~\cite{paulson-generic}.  The theory first defines the datatype
  2327 \texttt{comb} of combinators:
  2328 \begin{ttbox}
  2329 consts comb :: i
  2330 datatype  "comb" = K
  2331                  | S
  2332                  | "#" ("p: comb", "q: comb")   (infixl 90)
  2333 \end{ttbox}
  2334 The theory goes on to define contraction and parallel contraction
  2335 inductively.  Then the file \texttt{ex/Comb.ML} defines special cases of
  2336 contraction using \texttt{mk_cases}:
  2337 \begin{ttbox}
  2338 val K_contractE = contract.mk_cases "K -1-> r";
  2339 {\out val K_contractE = "K -1-> ?r ==> ?Q" : thm}
  2340 \end{ttbox}
  2341 We can read this as saying that the combinator \texttt{K} cannot reduce to
  2342 anything.  Similar elimination rules for \texttt{S} and application are also
  2343 generated and are supplied to the classical reasoner.  Note that
  2344 \texttt{comb.con_defs} is given to \texttt{mk_cases} to allow freeness
  2345 reasoning on datatype \texttt{comb}.
  2346 
  2347 \index{*coinductive|)} \index{*inductive|)}
  2348 
  2349 
  2350 
  2351 
  2352 \section{The outer reaches of set theory}
  2353 
  2354 The constructions of the natural numbers and lists use a suite of
  2355 operators for handling recursive function definitions.  I have described
  2356 the developments in detail elsewhere~\cite{paulson-set-II}.  Here is a brief
  2357 summary:
  2358 \begin{itemize}
  2359   \item Theory \texttt{Trancl} defines the transitive closure of a relation
  2360     (as a least fixedpoint).
  2361 
  2362   \item Theory \texttt{WF} proves the Well-Founded Recursion Theorem, using an
  2363     elegant approach of Tobias Nipkow.  This theorem permits general
  2364     recursive definitions within set theory.
  2365 
  2366   \item Theory \texttt{Ord} defines the notions of transitive set and ordinal
  2367     number.  It derives transfinite induction.  A key definition is {\bf
  2368       less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and
  2369     $i\in j$.  As a special case, it includes less than on the natural
  2370     numbers.
  2371     
  2372   \item Theory \texttt{Epsilon} derives $\varepsilon$-induction and
  2373     $\varepsilon$-recursion, which are generalisations of transfinite
  2374     induction and recursion.  It also defines \cdx{rank}$(x)$, which
  2375     is the least ordinal $\alpha$ such that $x$ is constructed at
  2376     stage $\alpha$ of the cumulative hierarchy (thus $x\in
  2377     V@{\alpha+1}$).
  2378 \end{itemize}
  2379 
  2380 Other important theories lead to a theory of cardinal numbers.  They have
  2381 not yet been written up anywhere.  Here is a summary:
  2382 \begin{itemize}
  2383 \item Theory \texttt{Rel} defines the basic properties of relations, such as
  2384   (ir)reflexivity, (a)symmetry, and transitivity.
  2385 
  2386 \item Theory \texttt{EquivClass} develops a theory of equivalence
  2387   classes, not using the Axiom of Choice.
  2388 
  2389 \item Theory \texttt{Order} defines partial orderings, total orderings and
  2390   wellorderings.
  2391 
  2392 \item Theory \texttt{OrderArith} defines orderings on sum and product sets.
  2393   These can be used to define ordinal arithmetic and have applications to
  2394   cardinal arithmetic.
  2395 
  2396 \item Theory \texttt{OrderType} defines order types.  Every wellordering is
  2397   equivalent to a unique ordinal, which is its order type.
  2398 
  2399 \item Theory \texttt{Cardinal} defines equipollence and cardinal numbers.
  2400  
  2401 \item Theory \texttt{CardinalArith} defines cardinal addition and
  2402   multiplication, and proves their elementary laws.  It proves that there
  2403   is no greatest cardinal.  It also proves a deep result, namely
  2404   $\kappa\otimes\kappa=\kappa$ for every infinite cardinal~$\kappa$; see
  2405   Kunen~\cite[page 29]{kunen80}.  None of these results assume the Axiom of
  2406   Choice, which complicates their proofs considerably.  
  2407 \end{itemize}
  2408 
  2409 The following developments involve the Axiom of Choice (AC):
  2410 \begin{itemize}
  2411 \item Theory \texttt{AC} asserts the Axiom of Choice and proves some simple
  2412   equivalent forms.
  2413 
  2414 \item Theory \texttt{Zorn} proves Hausdorff's Maximal Principle, Zorn's Lemma
  2415   and the Wellordering Theorem, following Abrial and
  2416   Laffitte~\cite{abrial93}.
  2417 
  2418 \item Theory \verb|Cardinal_AC| uses AC to prove simplified theorems about
  2419   the cardinals.  It also proves a theorem needed to justify
  2420   infinitely branching datatype declarations: if $\kappa$ is an infinite
  2421   cardinal and $|X(\alpha)| \le \kappa$ for all $\alpha<\kappa$ then
  2422   $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.
  2423 
  2424 \item Theory \texttt{InfDatatype} proves theorems to justify infinitely
  2425   branching datatypes.  Arbitrary index sets are allowed, provided their
  2426   cardinalities have an upper bound.  The theory also justifies some
  2427   unusual cases of finite branching, involving the finite powerset operator
  2428   and the finite function space operator.
  2429 \end{itemize}
  2430 
  2431 
  2432 
  2433 \section{The examples directories}
  2434 Directory \texttt{HOL/IMP} contains a mechanised version of a semantic
  2435 equivalence proof taken from Winskel~\cite{winskel93}.  It formalises the
  2436 denotational and operational semantics of a simple while-language, then
  2437 proves the two equivalent.  It contains several datatype and inductive
  2438 definitions, and demonstrates their use.
  2439 
  2440 The directory \texttt{ZF/ex} contains further developments in ZF set theory.
  2441 Here is an overview; see the files themselves for more details.  I describe
  2442 much of this material in other
  2443 publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}.
  2444 \begin{itemize}
  2445 \item File \texttt{misc.ML} contains miscellaneous examples such as
  2446   Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition
  2447   of homomorphisms' challenge~\cite{boyer86}.
  2448 
  2449 \item Theory \texttt{Ramsey} proves the finite exponent 2 version of
  2450   Ramsey's Theorem, following Basin and Kaufmann's
  2451   presentation~\cite{basin91}.
  2452 
  2453 \item Theory \texttt{Integ} develops a theory of the integers as
  2454   equivalence classes of pairs of natural numbers.
  2455 
  2456 \item Theory \texttt{Primrec} develops some computation theory.  It
  2457   inductively defines the set of primitive recursive functions and presents a
  2458   proof that Ackermann's function is not primitive recursive.
  2459 
  2460 \item Theory \texttt{Primes} defines the Greatest Common Divisor of two
  2461   natural numbers and and the ``divides'' relation.
  2462 
  2463 \item Theory \texttt{Bin} defines a datatype for two's complement binary
  2464   integers, then proves rewrite rules to perform binary arithmetic.  For
  2465   instance, $1359\times {-}2468 = {-}3354012$ takes under 14 seconds.
  2466 
  2467 \item Theory \texttt{BT} defines the recursive data structure ${\tt
  2468     bt}(A)$, labelled binary trees.
  2469 
  2470 \item Theory \texttt{Term} defines a recursive data structure for terms
  2471   and term lists.  These are simply finite branching trees.
  2472 
  2473 \item Theory \texttt{TF} defines primitives for solving mutually
  2474   recursive equations over sets.  It constructs sets of trees and forests
  2475   as an example, including induction and recursion rules that handle the
  2476   mutual recursion.
  2477 
  2478 \item Theory \texttt{Prop} proves soundness and completeness of
  2479   propositional logic~\cite{paulson-set-II}.  This illustrates datatype
  2480   definitions, inductive definitions, structural induction and rule
  2481   induction.
  2482 
  2483 \item Theory \texttt{ListN} inductively defines the lists of $n$
  2484   elements~\cite{paulin-tlca}.
  2485 
  2486 \item Theory \texttt{Acc} inductively defines the accessible part of a
  2487   relation~\cite{paulin-tlca}.
  2488 
  2489 \item Theory \texttt{Comb} defines the datatype of combinators and
  2490   inductively defines contraction and parallel contraction.  It goes on to
  2491   prove the Church-Rosser Theorem.  This case study follows Camilleri and
  2492   Melham~\cite{camilleri92}.
  2493 
  2494 \item Theory \texttt{LList} defines lazy lists and a coinduction
  2495   principle for proving equations between them.
  2496 \end{itemize}
  2497 
  2498 
  2499 \section{A proof about powersets}\label{sec:ZF-pow-example}
  2500 To demonstrate high-level reasoning about subsets, let us prove the
  2501 equation ${{\tt Pow}(A)\cap {\tt Pow}(B)}= {\tt Pow}(A\cap B)$.  Compared
  2502 with first-order logic, set theory involves a maze of rules, and theorems
  2503 have many different proofs.  Attempting other proofs of the theorem might
  2504 be instructive.  This proof exploits the lattice properties of
  2505 intersection.  It also uses the monotonicity of the powerset operation,
  2506 from \texttt{ZF/mono.ML}:
  2507 \begin{ttbox}
  2508 \tdx{Pow_mono}      A<=B ==> Pow(A) <= Pow(B)
  2509 \end{ttbox}
  2510 We enter the goal and make the first step, which breaks the equation into
  2511 two inclusions by extensionality:\index{*equalityI theorem}
  2512 \begin{ttbox}
  2513 Goal "Pow(A Int B) = Pow(A) Int Pow(B)";
  2514 {\out Level 0}
  2515 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2516 {\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}
  2517 \ttbreak
  2518 by (resolve_tac [equalityI] 1);
  2519 {\out Level 1}
  2520 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2521 {\out  1. Pow(A Int B) <= Pow(A) Int Pow(B)}
  2522 {\out  2. Pow(A) Int Pow(B) <= Pow(A Int B)}
  2523 \end{ttbox}
  2524 Both inclusions could be tackled straightforwardly using \texttt{subsetI}.
  2525 A shorter proof results from noting that intersection forms the greatest
  2526 lower bound:\index{*Int_greatest theorem}
  2527 \begin{ttbox}
  2528 by (resolve_tac [Int_greatest] 1);
  2529 {\out Level 2}
  2530 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2531 {\out  1. Pow(A Int B) <= Pow(A)}
  2532 {\out  2. Pow(A Int B) <= Pow(B)}
  2533 {\out  3. Pow(A) Int Pow(B) <= Pow(A Int B)}
  2534 \end{ttbox}
  2535 Subgoal~1 follows by applying the monotonicity of \texttt{Pow} to $A\int
  2536 B\subseteq A$; subgoal~2 follows similarly:
  2537 \index{*Int_lower1 theorem}\index{*Int_lower2 theorem}
  2538 \begin{ttbox}
  2539 by (resolve_tac [Int_lower1 RS Pow_mono] 1);
  2540 {\out Level 3}
  2541 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2542 {\out  1. Pow(A Int B) <= Pow(B)}
  2543 {\out  2. Pow(A) Int Pow(B) <= Pow(A Int B)}
  2544 \ttbreak
  2545 by (resolve_tac [Int_lower2 RS Pow_mono] 1);
  2546 {\out Level 4}
  2547 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2548 {\out  1. Pow(A) Int Pow(B) <= Pow(A Int B)}
  2549 \end{ttbox}
  2550 We are left with the opposite inclusion, which we tackle in the
  2551 straightforward way:\index{*subsetI theorem}
  2552 \begin{ttbox}
  2553 by (resolve_tac [subsetI] 1);
  2554 {\out Level 5}
  2555 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2556 {\out  1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)}
  2557 \end{ttbox}
  2558 The subgoal is to show $x\in {\tt Pow}(A\cap B)$ assuming $x\in{\tt
  2559 Pow}(A)\cap {\tt Pow}(B)$; eliminating this assumption produces two
  2560 subgoals.  The rule \tdx{IntE} treats the intersection like a conjunction
  2561 instead of unfolding its definition.
  2562 \begin{ttbox}
  2563 by (eresolve_tac [IntE] 1);
  2564 {\out Level 6}
  2565 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2566 {\out  1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)}
  2567 \end{ttbox}
  2568 The next step replaces the \texttt{Pow} by the subset
  2569 relation~($\subseteq$).\index{*PowI theorem}
  2570 \begin{ttbox}
  2571 by (resolve_tac [PowI] 1);
  2572 {\out Level 7}
  2573 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2574 {\out  1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B}
  2575 \end{ttbox}
  2576 We perform the same replacement in the assumptions.  This is a good
  2577 demonstration of the tactic \ttindex{dresolve_tac}:\index{*PowD theorem}
  2578 \begin{ttbox}
  2579 by (REPEAT (dresolve_tac [PowD] 1));
  2580 {\out Level 8}
  2581 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2582 {\out  1. !!x. [| x <= A; x <= B |] ==> x <= A Int B}
  2583 \end{ttbox}
  2584 The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but
  2585 $A\int B$ is the greatest lower bound:\index{*Int_greatest theorem}
  2586 \begin{ttbox}
  2587 by (resolve_tac [Int_greatest] 1);
  2588 {\out Level 9}
  2589 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2590 {\out  1. !!x. [| x <= A; x <= B |] ==> x <= A}
  2591 {\out  2. !!x. [| x <= A; x <= B |] ==> x <= B}
  2592 \end{ttbox}
  2593 To conclude the proof, we clear up the trivial subgoals:
  2594 \begin{ttbox}
  2595 by (REPEAT (assume_tac 1));
  2596 {\out Level 10}
  2597 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2598 {\out No subgoals!}
  2599 \end{ttbox}
  2600 \medskip
  2601 We could have performed this proof in one step by applying
  2602 \ttindex{Blast_tac}.  Let us
  2603 go back to the start:
  2604 \begin{ttbox}
  2605 choplev 0;
  2606 {\out Level 0}
  2607 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2608 {\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}
  2609 by (Blast_tac 1);
  2610 {\out Depth = 0}
  2611 {\out Depth = 1}
  2612 {\out Depth = 2}
  2613 {\out Depth = 3}
  2614 {\out Level 1}
  2615 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
  2616 {\out No subgoals!}
  2617 \end{ttbox}
  2618 Past researchers regarded this as a difficult proof, as indeed it is if all
  2619 the symbols are replaced by their definitions.
  2620 \goodbreak
  2621 
  2622 \section{Monotonicity of the union operator}
  2623 For another example, we prove that general union is monotonic:
  2624 ${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$.  To begin, we
  2625 tackle the inclusion using \tdx{subsetI}:
  2626 \begin{ttbox}
  2627 Goal "C<=D ==> Union(C) <= Union(D)";
  2628 {\out Level 0}
  2629 {\out C <= D ==> Union(C) <= Union(D)}
  2630 {\out  1. C <= D ==> Union(C) <= Union(D)}
  2631 \ttbreak
  2632 by (resolve_tac [subsetI] 1);
  2633 {\out Level 1}
  2634 {\out C <= D ==> Union(C) <= Union(D)}
  2635 {\out  1. !!x. [| C <= D; x : Union(C) |] ==> x : Union(D)}
  2636 \end{ttbox}
  2637 Big union is like an existential quantifier --- the occurrence in the
  2638 assumptions must be eliminated early, since it creates parameters.
  2639 \index{*UnionE theorem}
  2640 \begin{ttbox}
  2641 by (eresolve_tac [UnionE] 1);
  2642 {\out Level 2}
  2643 {\out C <= D ==> Union(C) <= Union(D)}
  2644 {\out  1. !!x B. [| C <= D; x : B; B : C |] ==> x : Union(D)}
  2645 \end{ttbox}
  2646 Now we may apply \tdx{UnionI}, which creates an unknown involving the
  2647 parameters.  To show $x\in \bigcup(D)$ it suffices to show that $x$ belongs
  2648 to some element, say~$\Var{B2}(x,B)$, of~$D$.
  2649 \begin{ttbox}
  2650 by (resolve_tac [UnionI] 1);
  2651 {\out Level 3}
  2652 {\out C <= D ==> Union(C) <= Union(D)}
  2653 {\out  1. !!x B. [| C <= D; x : B; B : C |] ==> ?B2(x,B) : D}
  2654 {\out  2. !!x B. [| C <= D; x : B; B : C |] ==> x : ?B2(x,B)}
  2655 \end{ttbox}
  2656 Combining \tdx{subsetD} with the assumption $C\subseteq D$ yields 
  2657 $\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1.  Note that
  2658 \texttt{eresolve_tac} has removed that assumption.
  2659 \begin{ttbox}
  2660 by (eresolve_tac [subsetD] 1);
  2661 {\out Level 4}
  2662 {\out C <= D ==> Union(C) <= Union(D)}
  2663 {\out  1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C}
  2664 {\out  2. !!x B. [| C <= D; x : B; B : C |] ==> x : ?B2(x,B)}
  2665 \end{ttbox}
  2666 The rest is routine.  Observe how~$\Var{B2}(x,B)$ is instantiated.
  2667 \begin{ttbox}
  2668 by (assume_tac 1);
  2669 {\out Level 5}
  2670 {\out C <= D ==> Union(C) <= Union(D)}
  2671 {\out  1. !!x B. [| C <= D; x : B; B : C |] ==> x : B}
  2672 by (assume_tac 1);
  2673 {\out Level 6}
  2674 {\out C <= D ==> Union(C) <= Union(D)}
  2675 {\out No subgoals!}
  2676 \end{ttbox}
  2677 Again, \ttindex{Blast_tac} can prove the theorem in one step.
  2678 \begin{ttbox}
  2679 by (Blast_tac 1);
  2680 {\out Depth = 0}
  2681 {\out Depth = 1}
  2682 {\out Depth = 2}
  2683 {\out Level 1}
  2684 {\out C <= D ==> Union(C) <= Union(D)}
  2685 {\out No subgoals!}
  2686 \end{ttbox}
  2687 
  2688 The file \texttt{ZF/equalities.ML} has many similar proofs.  Reasoning about
  2689 general intersection can be difficult because of its anomalous behaviour on
  2690 the empty set.  However, \ttindex{Blast_tac} copes well with these.  Here is
  2691 a typical example, borrowed from Devlin~\cite[page 12]{devlin79}:
  2692 \begin{ttbox}
  2693 a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C. A(x)) Int (INT x:C. B(x))
  2694 \end{ttbox}
  2695 In traditional notation this is
  2696 \[ a\in C \,\Imp\, \inter@{x\in C} \Bigl(A(x) \int B(x)\Bigr) =        
  2697        \Bigl(\inter@{x\in C} A(x)\Bigr)  \int  
  2698        \Bigl(\inter@{x\in C} B(x)\Bigr)  \]
  2699 
  2700 \section{Low-level reasoning about functions}
  2701 The derived rules \texttt{lamI}, \texttt{lamE}, \texttt{lam_type}, \texttt{beta}
  2702 and \texttt{eta} support reasoning about functions in a
  2703 $\lambda$-calculus style.  This is generally easier than regarding
  2704 functions as sets of ordered pairs.  But sometimes we must look at the
  2705 underlying representation, as in the following proof
  2706 of~\tdx{fun_disjoint_apply1}.  This states that if $f$ and~$g$ are
  2707 functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then
  2708 $(f\un g)`a = f`a$:
  2709 \begin{ttbox}
  2710 Goal "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \ttback
  2711 \ttback    (f Un g)`a = f`a";
  2712 {\out Level 0}
  2713 {\out [| a : A; f : A -> B; g : C -> D; A Int C = 0 |]}
  2714 {\out ==> (f Un g) ` a = f ` a}
  2715 {\out  1. [| a : A; f : A -> B; g : C -> D; A Int C = 0 |]}
  2716 {\out     ==> (f Un g) ` a = f ` a}
  2717 \end{ttbox}
  2718 Using \tdx{apply_equality}, we reduce the equality to reasoning about
  2719 ordered pairs.  The second subgoal is to verify that $f\un g$ is a function.
  2720 To save space, the assumptions will be abbreviated below.
  2721 \begin{ttbox}
  2722 by (resolve_tac [apply_equality] 1);
  2723 {\out Level 1}
  2724 {\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  2725 {\out  1. [| \ldots |] ==> <a,f ` a> : f Un g}
  2726 {\out  2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))}
  2727 \end{ttbox}
  2728 We must show that the pair belongs to~$f$ or~$g$; by~\tdx{UnI1} we
  2729 choose~$f$:
  2730 \begin{ttbox}
  2731 by (resolve_tac [UnI1] 1);
  2732 {\out Level 2}
  2733 {\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  2734 {\out  1. [| \ldots |] ==> <a,f ` a> : f}
  2735 {\out  2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))}
  2736 \end{ttbox}
  2737 To show $\pair{a,f`a}\in f$ we use \tdx{apply_Pair}, which is
  2738 essentially the converse of \tdx{apply_equality}:
  2739 \begin{ttbox}
  2740 by (resolve_tac [apply_Pair] 1);
  2741 {\out Level 3}
  2742 {\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  2743 {\out  1. [| \ldots |] ==> f : (PROD x:?A2. ?B2(x))}
  2744 {\out  2. [| \ldots |] ==> a : ?A2}
  2745 {\out  3. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))}
  2746 \end{ttbox}
  2747 Using the assumptions $f\in A\to B$ and $a\in A$, we solve the two subgoals
  2748 from \tdx{apply_Pair}.  Recall that a $\Pi$-set is merely a generalized
  2749 function space, and observe that~{\tt?A2} is instantiated to~\texttt{A}.
  2750 \begin{ttbox}
  2751 by (assume_tac 1);
  2752 {\out Level 4}
  2753 {\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  2754 {\out  1. [| \ldots |] ==> a : A}
  2755 {\out  2. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))}
  2756 by (assume_tac 1);
  2757 {\out Level 5}
  2758 {\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  2759 {\out  1. [| \ldots |] ==> f Un g : (PROD x:?A. ?B(x))}
  2760 \end{ttbox}
  2761 To construct functions of the form $f\un g$, we apply
  2762 \tdx{fun_disjoint_Un}:
  2763 \begin{ttbox}
  2764 by (resolve_tac [fun_disjoint_Un] 1);
  2765 {\out Level 6}
  2766 {\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  2767 {\out  1. [| \ldots |] ==> f : ?A3 -> ?B3}
  2768 {\out  2. [| \ldots |] ==> g : ?C3 -> ?D3}
  2769 {\out  3. [| \ldots |] ==> ?A3 Int ?C3 = 0}
  2770 \end{ttbox}
  2771 The remaining subgoals are instances of the assumptions.  Again, observe how
  2772 unknowns are instantiated:
  2773 \begin{ttbox}
  2774 by (assume_tac 1);
  2775 {\out Level 7}
  2776 {\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  2777 {\out  1. [| \ldots |] ==> g : ?C3 -> ?D3}
  2778 {\out  2. [| \ldots |] ==> A Int ?C3 = 0}
  2779 by (assume_tac 1);
  2780 {\out Level 8}
  2781 {\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  2782 {\out  1. [| \ldots |] ==> A Int C = 0}
  2783 by (assume_tac 1);
  2784 {\out Level 9}
  2785 {\out [| \ldots |] ==> (f Un g) ` a = f ` a}
  2786 {\out No subgoals!}
  2787 \end{ttbox}
  2788 See the files \texttt{ZF/func.ML} and \texttt{ZF/WF.ML} for more
  2789 examples of reasoning about functions.
  2790 
  2791 \index{set theory|)}