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