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