doc-src/Logics/ZF.tex
author lcp
Thu, 17 Nov 1994 22:01:08 +0100
changeset 713 b470cc6326aa
parent 595 96c87d5bb015
child 1449 25a7ddf9c080
permissions -rw-r--r--
In ZF, type i has class term, not (just) logic
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
     2
\chapter{Zermelo-Fraenkel Set Theory}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
     3
\index{set theory|(}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
     4
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
     5
The theory~\thydx{ZF} implements Zermelo-Fraenkel set
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
     6
theory~\cite{halmos60,suppes72} as an extension of~{\tt FOL}, classical
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
first-order logic.  The theory includes a collection of derived natural
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
     8
deduction rules, for use with Isabelle's classical reasoner.  Much
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
     9
of it is based on the work of No\"el~\cite{noel}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
A tremendous amount of set theory has been formally developed, including
595
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    12
the basic properties of relations, functions, ordinals and cardinals.
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    13
Significant results have been proved, such as the Schr\"oder-Bernstein
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    14
Theorem, the Wellordering Theorem and a version of Ramsey's Theorem.
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    15
General methods have been developed for solving recursion equations over
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    16
monotonic functors; these have been applied to yield constructions of
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    17
lists, trees, infinite lists, etc.  The Recursion Theorem has been proved,
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    18
admitting recursive definitions of functions over well-founded relations.
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    19
Thus, we may even regard set theory as a computational logic, loosely
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    20
inspired by Martin-L\"of's Type Theory.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
Because {\ZF} is an extension of {\FOL}, it provides the same packages,
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    23
namely {\tt hyp_subst_tac}, the simplifier, and the classical reasoner.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    24
The main simplification set is called {\tt ZF_ss}.  Several
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    25
classical rule sets are defined, including {\tt lemmas_cs},
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    26
{\tt upair_cs} and~{\tt ZF_cs}.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
595
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    28
{\tt ZF} has a flexible package for handling inductive definitions,
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    29
such as inference systems, and datatype definitions, such as lists and
595
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    30
trees.  Moreover it handles coinductive definitions, such as
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    31
bisimulation relations, and codatatype definitions, such as streams.  A
595
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    32
recent paper describes the package~\cite{paulson-CADE}, but its examples
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    33
use an obsolete declaration syntax.  Please consult the version of the
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
    34
paper distributed with Isabelle.
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    35
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    36
Recent reports~\cite{paulson-set-I,paulson-set-II} describe {\tt ZF} less
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    37
formally than this chapter.  Isabelle employs a novel treatment of
343
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
    38
non-well-founded data structures within the standard {\sc zf} axioms including
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    39
the Axiom of Foundation~\cite{paulson-final}.
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    40
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
\section{Which version of axiomatic set theory?}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    43
The two main axiom systems for set theory are Bernays-G\"odel~({\sc bg})
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    44
and Zermelo-Fraenkel~({\sc zf}).  Resolution theorem provers can use {\sc
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    45
  bg} because it is finite~\cite{boyer86,quaife92}.  {\sc zf} does not
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    46
have a finite axiom system because of its Axiom Scheme of Replacement.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    47
This makes it awkward to use with many theorem provers, since instances
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    48
of the axiom scheme have to be invoked explicitly.  Since Isabelle has no
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    49
difficulty with axiom schemes, we may adopt either axiom system.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
These two theories differ in their treatment of {\bf classes}, which are
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    52
collections that are `too big' to be sets.  The class of all sets,~$V$,
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    53
cannot be a set without admitting Russell's Paradox.  In {\sc bg}, both
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    54
classes and sets are individuals; $x\in V$ expresses that $x$ is a set.  In
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    55
{\sc zf}, all variables denote sets; classes are identified with unary
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    56
predicates.  The two systems define essentially the same sets and classes,
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    57
with similar properties.  In particular, a class cannot belong to another
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    58
class (let alone a set).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    60
Modern set theorists tend to prefer {\sc zf} because they are mainly concerned
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    61
with sets, rather than classes.  {\sc bg} requires tiresome proofs that various
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
collections are sets; for instance, showing $x\in\{x\}$ requires showing that
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    63
$x$ is a set.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
\begin{tabular}{rrr} 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    69
  \it name      &\it meta-type  & \it description \\ 
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    70
  \cdx{0}       & $i$           & empty set\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    71
  \cdx{cons}    & $[i,i]\To i$  & finite set constructor\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    72
  \cdx{Upair}   & $[i,i]\To i$  & unordered pairing\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    73
  \cdx{Pair}    & $[i,i]\To i$  & ordered pairing\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    74
  \cdx{Inf}     & $i$   & infinite set\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    75
  \cdx{Pow}     & $i\To i$      & powerset\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    76
  \cdx{Union} \cdx{Inter} & $i\To i$    & set union/intersection \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    77
  \cdx{split}   & $[[i,i]\To i, i] \To i$ & generalized projection\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    78
  \cdx{fst} \cdx{snd}   & $i\To i$      & projections\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    79
  \cdx{converse}& $i\To i$      & converse of a relation\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    80
  \cdx{succ}    & $i\To i$      & successor\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    81
  \cdx{Collect} & $[i,i\To o]\To i$     & separation\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    82
  \cdx{Replace} & $[i, [i,i]\To o] \To i$       & replacement\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    83
  \cdx{PrimReplace} & $[i, [i,i]\To o] \To i$   & primitive replacement\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    84
  \cdx{RepFun}  & $[i, i\To i] \To i$   & functional replacement\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    85
  \cdx{Pi} \cdx{Sigma}  & $[i,i\To i]\To i$     & general product/sum\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    86
  \cdx{domain}  & $i\To i$      & domain of a relation\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    87
  \cdx{range}   & $i\To i$      & range of a relation\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    88
  \cdx{field}   & $i\To i$      & field of a relation\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    89
  \cdx{Lambda}  & $[i, i\To i]\To i$    & $\lambda$-abstraction\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    90
  \cdx{restrict}& $[i, i] \To i$        & restriction of a function\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    91
  \cdx{The}     & $[i\To o]\To i$       & definite description\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    92
  \cdx{if}      & $[o,i,i]\To i$        & conditional\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    93
  \cdx{Ball} \cdx{Bex}  & $[i, i\To o]\To o$    & bounded quantifiers
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
\subcaption{Constants}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
\begin{center}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
    99
\index{*"`"` symbol}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   100
\index{*"-"`"` symbol}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   101
\index{*"` symbol}\index{function applications!in \ZF}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   102
\index{*"- symbol}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   103
\index{*": symbol}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   104
\index{*"<"= symbol}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
\begin{tabular}{rrrr} 
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   106
  \it symbol  & \it meta-type & \it priority & \it description \\ 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   107
  \tt ``        & $[i,i]\To i$  &  Left 90      & image \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   108
  \tt -``       & $[i,i]\To i$  &  Left 90      & inverse image \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   109
  \tt `         & $[i,i]\To i$  &  Left 90      & application \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   110
  \sdx{Int}     & $[i,i]\To i$  &  Left 70      & intersection ($\inter$) \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   111
  \sdx{Un}      & $[i,i]\To i$  &  Left 65      & union ($\union$) \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   112
  \tt -         & $[i,i]\To i$  &  Left 65      & set difference ($-$) \\[1ex]
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   113
  \tt:          & $[i,i]\To o$  &  Left 50      & membership ($\in$) \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   114
  \tt <=        & $[i,i]\To o$  &  Left 50      & subset ($\subseteq$) 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
\subcaption{Infixes}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   118
\caption{Constants of {\ZF}} \label{zf-constants}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
\end{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
\section{The syntax of set theory}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
The language of set theory, as studied by logicians, has no constants.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
traditional axioms merely assert the existence of empty sets, unions,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
powersets, etc.; this would be intolerable for practical reasoning.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
Isabelle theory declares constants for primitive sets.  It also extends
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
{\tt FOL} with additional syntax for finite sets, ordered pairs,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
comprehension, general union/intersection, general sums/products, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
bounded quantifiers.  In most other respects, Isabelle implements precisely
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
Zermelo-Fraenkel set theory.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
498
689e2bd78c19 renamed union_iff to Union_iff
lcp
parents: 461
diff changeset
   132
Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   133
Figure~\ref{zf-trans} presents the syntax translations.  Finally,
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   134
Figure~\ref{zf-syntax} presents the full grammar for set theory, including
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
the constructs of \FOL.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   137
Set theory does not use polymorphism.  All terms in {\ZF} have
713
b470cc6326aa In ZF, type i has class term, not (just) logic
lcp
parents: 595
diff changeset
   138
type~\tydx{i}, which is the type of individuals and has class~{\tt
b470cc6326aa In ZF, type i has class term, not (just) logic
lcp
parents: 595
diff changeset
   139
  term}.  The type of first-order formulae, remember, is~{\tt o}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   141
Infix operators include binary union and intersection ($A\union B$ and
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   142
$A\inter B$), set difference ($A-B$), and the subset and membership
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   143
relations.  Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$.  The
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   144
union and intersection operators ($\bigcup A$ and $\bigcap A$) form the
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   145
union or intersection of a set of sets; $\bigcup A$ means the same as
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   146
$\bigcup@{x\in A}x$.  Of these operators, only $\bigcup A$ is primitive.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   148
The constant \cdx{Upair} constructs unordered pairs; thus {\tt
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   149
  Upair($A$,$B$)} denotes the set~$\{A,B\}$ and {\tt Upair($A$,$A$)}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   150
denotes the singleton~$\{A\}$.  General union is used to define binary
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   151
union.  The Isabelle version goes on to define the constant
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   152
\cdx{cons}:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
\begin{eqnarray*}
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   154
   A\cup B              & \equiv &       \bigcup({\tt Upair}(A,B)) \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   155
   {\tt cons}(a,B)      & \equiv &        {\tt Upair}(a,a) \union B
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
\end{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
obvious manner using~{\tt cons} and~$\emptyset$ (the empty set):
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
\begin{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
 \{a,b,c\} & \equiv & {\tt cons}(a,{\tt cons}(b,{\tt cons}(c,\emptyset)))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
\end{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   163
The constant \cdx{Pair} constructs ordered pairs, as in {\tt
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
Pair($a$,$b$)}.  Ordered pairs may also be written within angle brackets,
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   165
as {\tt<$a$,$b$>}.  The $n$-tuple {\tt<$a@1$,\ldots,$a@{n-1}$,$a@n$>}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   166
abbreviates the nest of pairs\par\nobreak
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   167
\centerline{\tt Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
In {\ZF}, a function is a set of pairs.  A {\ZF} function~$f$ is simply an
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
individual as far as Isabelle is concerned: its Isabelle type is~$i$, not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
say $i\To i$.  The infix operator~{\tt`} denotes the application of a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
\begin{figure} 
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   177
\index{lambda abs@$\lambda$-abstractions!in \ZF}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   178
\index{*"-"> symbol}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   179
\index{*"* symbol}
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   180
\begin{center} \footnotesize\tt\frenchspacing
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
\begin{tabular}{rrr} 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   182
  \it external          & \it internal  & \it description \\ 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
  $a$ \ttilde: $b$      & \ttilde($a$ : $b$)    & \rm negated membership\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
  \{$a@1$, $\ldots$, $a@n$\}  &  cons($a@1$,$\cdots$,cons($a@n$,0)) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
        \rm finite set \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   186
  <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & 
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   187
        Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) &
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   188
        \rm ordered $n$-tuple \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   189
  \{$x$:$A . P[x]$\}    &  Collect($A$,$\lambda x.P[x]$) &
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
        \rm separation \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
  \{$y . x$:$A$, $Q[x,y]$\}  &  Replace($A$,$\lambda x\,y.Q[x,y]$) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
        \rm replacement \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
  \{$b[x] . x$:$A$\}  &  RepFun($A$,$\lambda x.b[x]$) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
        \rm functional replacement \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   195
  \sdx{INT} $x$:$A . B[x]$      & Inter(\{$B[x] . x$:$A$\}) &
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   196
        \rm general intersection \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   197
  \sdx{UN}  $x$:$A . B[x]$      & Union(\{$B[x] . x$:$A$\}) &
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   198
        \rm general union \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   199
  \sdx{PROD} $x$:$A . B[x]$     & Pi($A$,$\lambda x.B[x]$) & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   200
        \rm general product \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   201
  \sdx{SUM}  $x$:$A . B[x]$     & Sigma($A$,$\lambda x.B[x]$) & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   202
        \rm general sum \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   203
  $A$ -> $B$            & Pi($A$,$\lambda x.B$) & 
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   204
        \rm function space \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   205
  $A$ * $B$             & Sigma($A$,$\lambda x.B$) & 
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   206
        \rm binary product \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   207
  \sdx{THE}  $x . P[x]$ & The($\lambda x.P[x]$) & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   208
        \rm definite description \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   209
  \sdx{lam}  $x$:$A . b[x]$     & Lambda($A$,$\lambda x.b[x]$) & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   210
        \rm $\lambda$-abstraction\\[1ex]
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   211
  \sdx{ALL} $x$:$A . P[x]$      & Ball($A$,$\lambda x.P[x]$) & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   212
        \rm bounded $\forall$ \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   213
  \sdx{EX}  $x$:$A . P[x]$      & Bex($A$,$\lambda x.P[x]$) & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   214
        \rm bounded $\exists$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
\end{center}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   217
\caption{Translations for {\ZF}} \label{zf-trans}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
\end{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
\dquotes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
\[\begin{array}{rcl}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
    term & = & \hbox{expression of type~$i$} \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   225
         & | & "\{ " term\; ("," term)^* " \}" \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   226
         & | & "< "  term\; ("," term)^* " >"  \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   227
         & | & "\{ " id ":" term " . " formula " \}" \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   228
         & | & "\{ " id " . " id ":" term ", " formula " \}" \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   229
         & | & "\{ " term " . " id ":" term " \}" \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   230
         & | & term " `` " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   231
         & | & term " -`` " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   232
         & | & term " ` " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   233
         & | & term " * " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   234
         & | & term " Int " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   235
         & | & term " Un " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   236
         & | & term " - " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   237
         & | & term " -> " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   238
         & | & "THE~~"  id  " . " formula\\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   239
         & | & "lam~~"  id ":" term " . " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   240
         & | & "INT~~"  id ":" term " . " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   241
         & | & "UN~~~"  id ":" term " . " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   242
         & | & "PROD~"  id ":" term " . " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   243
         & | & "SUM~~"  id ":" term " . " term \\[2ex]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
 formula & = & \hbox{expression of type~$o$} \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   245
         & | & term " : " term \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   246
         & | & term " \ttilde: " term \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   247
         & | & term " <= " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   248
         & | & term " = " term \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   249
         & | & term " \ttilde= " term \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   250
         & | & "\ttilde\ " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   251
         & | & formula " \& " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   252
         & | & formula " | " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   253
         & | & formula " --> " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   254
         & | & formula " <-> " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   255
         & | & "ALL " id ":" term " . " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   256
         & | & "EX~~" id ":" term " . " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   257
         & | & "ALL~" id~id^* " . " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   258
         & | & "EX~~" id~id^* " . " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   259
         & | & "EX!~" id~id^* " . " formula
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
  \end{array}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
\]
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   262
\caption{Full grammar for {\ZF}} \label{zf-syntax}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
\end{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
\section{Binding operators}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   267
The constant \cdx{Collect} constructs sets by the principle of {\bf
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
  separation}.  The syntax for separation is \hbox{\tt\{$x$:$A$.$P[x]$\}},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
where $P[x]$ is a formula that may contain free occurrences of~$x$.  It
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   270
abbreviates the set {\tt Collect($A$,$\lambda x.P[x]$)}, which consists of
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
all $x\in A$ that satisfy~$P[x]$.  Note that {\tt Collect} is an
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
unfortunate choice of name: some set theories adopt a set-formation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
principle, related to replacement, called collection.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   275
The constant \cdx{Replace} constructs sets by the principle of {\bf
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   276
  replacement}.  The syntax \hbox{\tt\{$y$.$x$:$A$,$Q[x,y]$\}} denotes the
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   277
set {\tt Replace($A$,$\lambda x\,y.Q[x,y]$)}, which consists of all~$y$ such
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   278
that there exists $x\in A$ satisfying~$Q[x,y]$.  The Replacement Axiom has
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   279
the condition that $Q$ must be single-valued over~$A$: for all~$x\in A$
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   280
there exists at most one $y$ satisfying~$Q[x,y]$.  A single-valued binary
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
predicate is also called a {\bf class function}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   283
The constant \cdx{RepFun} expresses a special case of replacement,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
where $Q[x,y]$ has the form $y=b[x]$.  Such a $Q$ is trivially
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
single-valued, since it is just the graph of the meta-level
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   286
function~$\lambda x.b[x]$.  The resulting set consists of all $b[x]$
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   287
for~$x\in A$.  This is analogous to the \ML{} functional {\tt map}, since
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   288
it applies a function to every element of a set.  The syntax is
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   289
\hbox{\tt\{$b[x]$.$x$:$A$\}}, which expands to {\tt RepFun($A$,$\lambda
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   290
  x.b[x]$)}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   292
\index{*INT symbol}\index{*UN symbol} 
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   293
General unions and intersections of indexed
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   294
families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$,
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   295
are written \hbox{\tt UN $x$:$A$.$B[x]$} and \hbox{\tt INT $x$:$A$.$B[x]$}.
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   296
Their meaning is expressed using {\tt RepFun} as
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
\[ \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
   \bigcap(\{B[x]. x\in A\}). 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
constructed in set theory, where $B[x]$ is a family of sets over~$A$.  They
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
This is similar to the situation in Constructive Type Theory (set theory
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   304
has `dependent sets') and calls for similar syntactic conventions.  The
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   305
constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
products.  Instead of {\tt Sigma($A$,$B$)} and {\tt Pi($A$,$B$)} we may write
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
\hbox{\tt SUM $x$:$A$.$B[x]$} and \hbox{\tt PROD $x$:$A$.$B[x]$}.  
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   308
\index{*SUM symbol}\index{*PROD symbol}%
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
general sums and products over a constant family.\footnote{Unlike normal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
infix operators, {\tt*} and {\tt->} merely define abbreviations; there are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
no constants~{\tt op~*} and~\hbox{\tt op~->}.} Isabelle accepts these
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
abbreviations in parsing and uses them whenever possible for printing.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   315
\index{*THE symbol} 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
As mentioned above, whenever the axioms assert the existence and uniqueness
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
of a set, Isabelle's set theory declares a constant for that set.  These
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
constants can express the {\bf definite description} operator~$\iota
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
x.P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
Since all terms in {\ZF} denote something, a description is always
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
meaningful, but we do not know its value unless $P[x]$ defines it uniquely.
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   322
Using the constant~\cdx{The}, we may write descriptions as {\tt
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
  The($\lambda x.P[x]$)} or use the syntax \hbox{\tt THE $x$.$P[x]$}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   325
\index{*lam symbol}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
Function sets may be written in $\lambda$-notation; $\lambda x\in A.b[x]$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$.  In order for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
this to be a set, the function's domain~$A$ must be given.  Using the
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   329
constant~\cdx{Lambda}, we may express function sets as {\tt
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
Lambda($A$,$\lambda x.b[x]$)} or use the syntax \hbox{\tt lam $x$:$A$.$b[x]$}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
Isabelle's set theory defines two {\bf bounded quantifiers}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
\begin{eqnarray*}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   334
   \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   335
   \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
\end{eqnarray*}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   337
The constants~\cdx{Ball} and~\cdx{Bex} are defined
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
accordingly.  Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
write
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
\hbox{\tt ALL $x$:$A$.$P[x]$} and \hbox{\tt EX $x$:$A$.$P[x]$}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
343
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
   343
%%%% ZF.thy
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   347
\tdx{Ball_def}           Ball(A,P) == ALL x. x:A --> P(x)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   348
\tdx{Bex_def}            Bex(A,P)  == EX x. x:A & P(x)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   350
\tdx{subset_def}         A <= B  == ALL x:A. x:B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   351
\tdx{extension}          A = B  <->  A <= B & B <= A
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
498
689e2bd78c19 renamed union_iff to Union_iff
lcp
parents: 461
diff changeset
   353
\tdx{Union_iff}          A : Union(C) <-> (EX B:C. A:B)
689e2bd78c19 renamed union_iff to Union_iff
lcp
parents: 461
diff changeset
   354
\tdx{Pow_iff}            A : Pow(B) <-> A <= B
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   355
\tdx{foundation}         A=0 | (EX x:A. ALL y:x. ~ y:A)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   357
\tdx{replacement}        (ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
                   b : PrimReplace(A,P) <-> (EX x:A. P(x,b))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
\subcaption{The Zermelo-Fraenkel Axioms}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   361
\tdx{Replace_def}  Replace(A,P) == 
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   362
                   PrimReplace(A, \%x y. (EX!z.P(x,z)) & P(x,y))
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   363
\tdx{RepFun_def}   RepFun(A,f)  == \{y . x:A, y=f(x)\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   364
\tdx{the_def}      The(P)       == Union(\{y . x:\{0\}, P(y)\})
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   365
\tdx{if_def}       if(P,a,b)    == THE z. P & z=a | ~P & z=b
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   366
\tdx{Collect_def}  Collect(A,P) == \{y . x:A, x=y & P(x)\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   367
\tdx{Upair_def}    Upair(a,b)   == 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
                 \{y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
\subcaption{Consequences of replacement}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   371
\tdx{Inter_def}    Inter(A) == \{ x:Union(A) . ALL y:A. x:y\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   372
\tdx{Un_def}       A Un  B  == Union(Upair(A,B))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   373
\tdx{Int_def}      A Int B  == Inter(Upair(A,B))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   374
\tdx{Diff_def}     A - B    == \{ x:A . ~(x:B) \}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
\subcaption{Union, intersection, difference}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
\end{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   377
\caption{Rules and axioms of {\ZF}} \label{zf-rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   383
\tdx{cons_def}     cons(a,A) == Upair(a,a) Un A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   384
\tdx{succ_def}     succ(i) == cons(i,i)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   385
\tdx{infinity}     0:Inf & (ALL y:Inf. succ(y): Inf)
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   386
\subcaption{Finite and infinite sets}
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   387
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   388
\tdx{Pair_def}       <a,b>      == \{\{a,a\}, \{a,b\}\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   389
\tdx{split_def}      split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   390
\tdx{fst_def}        fst(A)     == split(\%x y.x, p)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   391
\tdx{snd_def}        snd(A)     == split(\%x y.y, p)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   392
\tdx{Sigma_def}      Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
\subcaption{Ordered pairs and Cartesian products}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   395
\tdx{converse_def}   converse(r) == \{z. w:r, EX x y. w=<x,y> & z=<y,x>\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   396
\tdx{domain_def}     domain(r)   == \{x. w:r, EX y. w=<x,y>\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   397
\tdx{range_def}      range(r)    == domain(converse(r))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   398
\tdx{field_def}      field(r)    == domain(r) Un range(r)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   399
\tdx{image_def}      r `` A      == \{y : range(r) . EX x:A. <x,y> : r\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   400
\tdx{vimage_def}     r -`` A     == converse(r)``A
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
\subcaption{Operations on relations}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   403
\tdx{lam_def}    Lambda(A,b) == \{<x,b(x)> . x:A\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   404
\tdx{apply_def}  f`a         == THE y. <a,y> : f
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   405
\tdx{Pi_def}     Pi(A,B) == \{f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   406
\tdx{restrict_def}   restrict(f,A) == lam x:A.f`x
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
\subcaption{Functions and general product}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
\end{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   409
\caption{Further definitions of {\ZF}} \label{zf-defs}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
\section{The Zermelo-Fraenkel axioms}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   415
The axioms appear in Fig.\ts \ref{zf-rules}.  They resemble those
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
presented by Suppes~\cite{suppes72}.  Most of the theory consists of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
definitions.  In particular, bounded quantifiers and the subset relation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
appear in other axioms.  Object-level quantifiers and implications have
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
been replaced by meta-level ones wherever possible, to simplify use of the
343
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
   420
axioms.  See the file {\tt ZF/ZF.thy} for details.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
The traditional replacement axiom asserts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
\[ y \in {\tt PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$.
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   425
The Isabelle theory defines \cdx{Replace} to apply
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   426
\cdx{PrimReplace} to the single-valued part of~$P$, namely
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
\[ (\exists!z.P(x,z)) \conj P(x,y). \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
Thus $y\in {\tt Replace}(A,P)$ if and only if there is some~$x$ such that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
$P(x,-)$ holds uniquely for~$y$.  Because the equivalence is unconditional,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
{\tt Replace} is much easier to use than {\tt PrimReplace}; it defines the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
same set, if $P(x,y)$ is single-valued.  The nice syntax for replacement
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
expands to {\tt Replace}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
Other consequences of replacement include functional replacement
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   435
(\cdx{RepFun}) and definite descriptions (\cdx{The}).
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   436
Axioms for separation (\cdx{Collect}) and unordered pairs
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   437
(\cdx{Upair}) are traditionally assumed, but they actually follow
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
from replacement~\cite[pages 237--8]{suppes72}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
The definitions of general intersection, etc., are straightforward.  Note
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   441
the definition of {\tt cons}, which underlies the finite set notation.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
The axiom of infinity gives us a set that contains~0 and is closed under
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   443
successor (\cdx{succ}).  Although this set is not uniquely defined,
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   444
the theory names it (\cdx{Inf}) in order to simplify the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
construction of the natural numbers.
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   446
                                             
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   447
Further definitions appear in Fig.\ts\ref{zf-defs}.  Ordered pairs are
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$.  Recall
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   449
that \cdx{Sigma}$(A,B)$ generalizes the Cartesian product of two
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
sets.  It is defined to be the union of all singleton sets
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
$\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$.  This is a typical usage of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
general union.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   454
The projections \cdx{fst} and~\cdx{snd} are defined in terms of the
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   455
generalized projection \cdx{split}.  The latter has been borrowed from
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   456
Martin-L\"of's Type Theory, and is often easier to use than \cdx{fst}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   457
and~\cdx{snd}.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   458
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
Operations on relations include converse, domain, range, and image.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
set ${\tt Pi}(A,B)$ generalizes the space of functions between two sets.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
Note the simple definitions of $\lambda$-abstraction (using
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   462
\cdx{RepFun}) and application (using a definite description).  The
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   463
function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
over the domain~$A$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   466
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   467
%%%% zf.ML
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   468
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   469
\begin{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   470
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   471
\tdx{ballI}       [| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   472
\tdx{bspec}       [| ALL x:A. P(x);  x: A |] ==> P(x)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   473
\tdx{ballE}       [| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   474
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   475
\tdx{ball_cong}   [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   476
            (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   477
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   478
\tdx{bexI}        [| P(x);  x: A |] ==> EX x:A. P(x)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   479
\tdx{bexCI}       [| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A.P(x)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   480
\tdx{bexE}        [| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q |] ==> Q
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   481
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   482
\tdx{bex_cong}    [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   483
            (EX x:A. P(x)) <-> (EX x:A'. P'(x))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   484
\subcaption{Bounded quantifiers}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   485
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   486
\tdx{subsetI}       (!!x.x:A ==> x:B) ==> A <= B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   487
\tdx{subsetD}       [| A <= B;  c:A |] ==> c:B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   488
\tdx{subsetCE}      [| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   489
\tdx{subset_refl}   A <= A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   490
\tdx{subset_trans}  [| A<=B;  B<=C |] ==> A<=C
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   491
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   492
\tdx{equalityI}     [| A <= B;  B <= A |] ==> A = B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   493
\tdx{equalityD1}    A = B ==> A<=B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   494
\tdx{equalityD2}    A = B ==> B<=A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   495
\tdx{equalityE}     [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   496
\subcaption{Subsets and extensionality}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   497
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   498
\tdx{emptyE}          a:0 ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   499
\tdx{empty_subsetI}   0 <= A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   500
\tdx{equals0I}        [| !!y. y:A ==> False |] ==> A=0
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   501
\tdx{equals0D}        [| A=0;  a:A |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   502
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   503
\tdx{PowI}            A <= B ==> A : Pow(B)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   504
\tdx{PowD}            A : Pow(B)  ==>  A<=B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   505
\subcaption{The empty set; power sets}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   506
\end{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   507
\caption{Basic derived rules for {\ZF}} \label{zf-lemmas1}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   508
\end{figure}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
\section{From basic lemmas to function spaces}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
Faced with so many definitions, it is essential to prove lemmas.  Even
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
trivial theorems like $A\inter B=B\inter A$ would be difficult to prove
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
from the definitions alone.  Isabelle's set theory derives many rules using
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
a natural deduction style.  Ideally, a natural deduction rule should
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
introduce or eliminate just one operator, but this is not always practical.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
For most operators, we may forget its definition and use its derived rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
instead.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
\subsection{Fundamental lemmas}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   521
Figure~\ref{zf-lemmas1} presents the derived rules for the most basic
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
operators.  The rules for the bounded quantifiers resemble those for the
343
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
   523
ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
   524
in the style of Isabelle's classical reasoner.  The \rmindex{congruence
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
   525
  rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
simplifier, but have few other uses.  Congruence rules must be specially
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   527
derived for all binding operators, and henceforth will not be shown.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   529
Figure~\ref{zf-lemmas1} also shows rules for the subset and equality
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
relations (proof by extensionality), and rules about the empty set and the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
power set operator.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   533
Figure~\ref{zf-lemmas2} presents rules for replacement and separation.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   534
The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
comparable rules for {\tt PrimReplace} would be.  The principle of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
separation is proved explicitly, although most proofs should use the
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   537
natural deduction rules for {\tt Collect}.  The elimination rule
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   538
\tdx{CollectE} is equivalent to the two destruction rules
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   539
\tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   540
particular circumstances.  Although too many rules can be confusing, there
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
is no reason to aim for a minimal set of rules.  See the file
343
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
   542
{\tt ZF/ZF.ML} for a complete listing.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   544
Figure~\ref{zf-lemmas3} presents rules for general union and intersection.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   545
The empty intersection should be undefined.  We cannot have
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   546
$\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set.  All
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   547
expressions denote something in {\ZF} set theory; the definition of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   548
intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   549
arbitrary.  The rule \tdx{InterI} must have a premise to exclude
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
the empty intersection.  Some of the laws governing intersections require
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
similar premises.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   552
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   554
%the [p] gives better page breaking for the book
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   555
\begin{figure}[p]
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   556
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   557
\tdx{ReplaceI}      [| x: A;  P(x,b);  !!y. P(x,y) ==> y=b |] ==> 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   558
              b : \{y. x:A, P(x,y)\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   559
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   560
\tdx{ReplaceE}      [| b : \{y. x:A, P(x,y)\};  
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   561
                 !!x. [| x: A;  P(x,b);  ALL y. P(x,y)-->y=b |] ==> R 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   562
              |] ==> R
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   563
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   564
\tdx{RepFunI}       [| a : A |] ==> f(a) : \{f(x). x:A\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   565
\tdx{RepFunE}       [| b : \{f(x). x:A\};  
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   566
                 !!x.[| x:A;  b=f(x) |] ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   567
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   568
\tdx{separation}     a : \{x:A. P(x)\} <-> a:A & P(a)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   569
\tdx{CollectI}       [| a:A;  P(a) |] ==> a : \{x:A. P(x)\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   570
\tdx{CollectE}       [| a : \{x:A. P(x)\};  [| a:A; P(a) |] ==> R |] ==> R
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   571
\tdx{CollectD1}      a : \{x:A. P(x)\} ==> a:A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   572
\tdx{CollectD2}      a : \{x:A. P(x)\} ==> P(a)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   573
\end{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   574
\caption{Replacement and separation} \label{zf-lemmas2}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   575
\end{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   576
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   577
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   578
\begin{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   579
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   580
\tdx{UnionI}    [| B: C;  A: B |] ==> A: Union(C)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   581
\tdx{UnionE}    [| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   582
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   583
\tdx{InterI}    [| !!x. x: C ==> A: x;  c:C |] ==> A : Inter(C)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   584
\tdx{InterD}    [| A : Inter(C);  B : C |] ==> A : B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   585
\tdx{InterE}    [| A : Inter(C);  A:B ==> R;  ~ B:C ==> R |] ==> R
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   586
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   587
\tdx{UN_I}      [| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   588
\tdx{UN_E}      [| b : (UN x:A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   589
          |] ==> R
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   590
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   591
\tdx{INT_I}     [| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   592
\tdx{INT_E}     [| b : (INT x:A. B(x));  a: A |] ==> b : B(a)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   593
\end{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   594
\caption{General union and intersection} \label{zf-lemmas3}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   595
\end{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   596
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   597
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   598
%%% upair.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   599
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   600
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   601
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   602
\tdx{pairing}      a:Upair(b,c) <-> (a=b | a=c)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   603
\tdx{UpairI1}      a : Upair(a,b)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   604
\tdx{UpairI2}      b : Upair(a,b)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   605
\tdx{UpairE}       [| a : Upair(b,c);  a = b ==> P;  a = c ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   606
\end{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   607
\caption{Unordered pairs} \label{zf-upair1}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   608
\end{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   609
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   610
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   611
\begin{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   612
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   613
\tdx{UnI1}         c : A ==> c : A Un B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   614
\tdx{UnI2}         c : B ==> c : A Un B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   615
\tdx{UnCI}         (~c : B ==> c : A) ==> c : A Un B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   616
\tdx{UnE}          [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   617
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   618
\tdx{IntI}         [| c : A;  c : B |] ==> c : A Int B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   619
\tdx{IntD1}        c : A Int B ==> c : A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   620
\tdx{IntD2}        c : A Int B ==> c : B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   621
\tdx{IntE}         [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   622
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   623
\tdx{DiffI}        [| c : A;  ~ c : B |] ==> c : A - B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   624
\tdx{DiffD1}       c : A - B ==> c : A
498
689e2bd78c19 renamed union_iff to Union_iff
lcp
parents: 461
diff changeset
   625
\tdx{DiffD2}       c : A - B ==> c ~: B
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   626
\tdx{DiffE}        [| c : A - B;  [| c:A; ~ c:B |] ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   627
\end{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   628
\caption{Union, intersection, difference} \label{zf-Un}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   629
\end{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   630
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   631
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   632
\begin{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   633
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   634
\tdx{consI1}       a : cons(a,B)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   635
\tdx{consI2}       a : B ==> a : cons(b,B)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   636
\tdx{consCI}       (~ a:B ==> a=b) ==> a: cons(b,B)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   637
\tdx{consE}        [| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   638
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   639
\tdx{singletonI}   a : \{a\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   640
\tdx{singletonE}   [| a : \{b\}; a=b ==> P |] ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   641
\end{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   642
\caption{Finite and singleton sets} \label{zf-upair2}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   643
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   644
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   645
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   646
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   647
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   648
\tdx{succI1}       i : succ(i)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   649
\tdx{succI2}       i : j ==> i : succ(j)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   650
\tdx{succCI}       (~ i:j ==> i=j) ==> i: succ(j)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   651
\tdx{succE}        [| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   652
\tdx{succ_neq_0}   [| succ(n)=0 |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   653
\tdx{succ_inject}  succ(m) = succ(n) ==> m=n
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   654
\end{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   655
\caption{The successor function} \label{zf-succ}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   656
\end{figure}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   657
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   658
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   659
\begin{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   660
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   661
\tdx{the_equality}     [| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   662
\tdx{theI}             EX! x. P(x) ==> P(THE x. P(x))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
461
170de0c52a9b minor edits
lcp
parents: 349
diff changeset
   664
\tdx{if_P}              P ==> if(P,a,b) = a
170de0c52a9b minor edits
lcp
parents: 349
diff changeset
   665
\tdx{if_not_P}         ~P ==> if(P,a,b) = b
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   666
461
170de0c52a9b minor edits
lcp
parents: 349
diff changeset
   667
\tdx{mem_asym}         [| a:b;  b:a |] ==> P
170de0c52a9b minor edits
lcp
parents: 349
diff changeset
   668
\tdx{mem_irrefl}       a:a ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   669
\end{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   670
\caption{Descriptions; non-circularity} \label{zf-the}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   671
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   672
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   673
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   674
\subsection{Unordered pairs and finite sets}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   675
Figure~\ref{zf-upair1} presents the principle of unordered pairing, along
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   676
with its derived rules.  Binary union and intersection are defined in terms
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   677
of ordered pairs (Fig.\ts\ref{zf-Un}).  Set difference is also included.  The
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   678
rule \tdx{UnCI} is useful for classical reasoning about unions,
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   679
like {\tt disjCI}\@; it supersedes \tdx{UnI1} and
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   680
\tdx{UnI2}, but these rules are often easier to work with.  For
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
intersection and difference we have both elimination and destruction rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
Again, there is no reason to provide a minimal rule set.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   683
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   684
Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   685
for~{\tt cons}, the finite set constructor, and rules for singleton
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   686
sets.  Figure~\ref{zf-succ} presents derived rules for the successor
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   687
function, which is defined in terms of~{\tt cons}.  The proof that {\tt
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   688
  succ} is injective appears to require the Axiom of Foundation.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   689
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   690
Definite descriptions (\sdx{THE}) are defined in terms of the singleton
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   691
set~$\{0\}$, but their derived rules fortunately hide this
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   692
(Fig.\ts\ref{zf-the}).  The rule~\tdx{theI} is difficult to apply
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   693
because of the two occurrences of~$\Var{P}$.  However,
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   694
\tdx{the_equality} does not have this problem and the files contain
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   695
many examples of its use.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   696
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   697
Finally, the impossibility of having both $a\in b$ and $b\in a$
461
170de0c52a9b minor edits
lcp
parents: 349
diff changeset
   698
(\tdx{mem_asym}) is proved by applying the Axiom of Foundation to
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   699
the set $\{a,b\}$.  The impossibility of $a\in a$ is a trivial consequence.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   700
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   701
See the file {\tt ZF/upair.ML} for full proofs of the rules discussed in
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   702
this section.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   703
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   704
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   705
%%% subset.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   706
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   707
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   708
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   709
\tdx{Union_upper}       B:A ==> B <= Union(A)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   710
\tdx{Union_least}       [| !!x. x:A ==> x<=C |] ==> Union(A) <= C
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   711
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   712
\tdx{Inter_lower}       B:A ==> Inter(A) <= B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   713
\tdx{Inter_greatest}    [| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   714
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   715
\tdx{Un_upper1}         A <= A Un B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   716
\tdx{Un_upper2}         B <= A Un B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   717
\tdx{Un_least}          [| A<=C;  B<=C |] ==> A Un B <= C
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   718
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   719
\tdx{Int_lower1}        A Int B <= A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   720
\tdx{Int_lower2}        A Int B <= B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   721
\tdx{Int_greatest}      [| C<=A;  C<=B |] ==> C <= A Int B
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   722
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   723
\tdx{Diff_subset}       A-B <= A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   724
\tdx{Diff_contains}     [| C<=A;  C Int B = 0 |] ==> C <= A-B
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   725
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   726
\tdx{Collect_subset}    Collect(A,P) <= A
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   727
\end{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   728
\caption{Subset and lattice properties} \label{zf-subset}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   729
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   730
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   731
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   732
\subsection{Subset and lattice properties}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   733
The subset relation is a complete lattice.  Unions form least upper bounds;
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   734
non-empty intersections form greatest lower bounds.  Figure~\ref{zf-subset}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   735
shows the corresponding rules.  A few other laws involving subsets are
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   736
included.  Proofs are in the file {\tt ZF/subset.ML}.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   737
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   738
Reasoning directly about subsets often yields clearer proofs than
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   739
reasoning about the membership relation.  Section~\ref{sec:ZF-pow-example}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   740
below presents an example of this, proving the equation ${{\tt Pow}(A)\cap
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   741
  {\tt Pow}(B)}= {\tt Pow}(A\cap B)$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   742
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   743
%%% pair.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   744
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   745
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   746
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   747
\tdx{Pair_inject1}    <a,b> = <c,d> ==> a=c
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   748
\tdx{Pair_inject2}    <a,b> = <c,d> ==> b=d
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   749
\tdx{Pair_inject}     [| <a,b> = <c,d>;  [| a=c; b=d |] ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   750
\tdx{Pair_neq_0}      <a,b>=0 ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   751
349
0ddc495e8b83 post-CRC corrections
lcp
parents: 343
diff changeset
   752
\tdx{fst_conv}        fst(<a,b>) = a
0ddc495e8b83 post-CRC corrections
lcp
parents: 343
diff changeset
   753
\tdx{snd_conv}        snd(<a,b>) = b
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   754
\tdx{split}           split(\%x y.c(x,y), <a,b>) = c(a,b)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   755
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   756
\tdx{SigmaI}          [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   757
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   758
\tdx{SigmaE}          [| c: Sigma(A,B);  
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   759
                   !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   760
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   761
\tdx{SigmaE2}         [| <a,b> : Sigma(A,B);    
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   762
                   [| a:A;  b:B(a) |] ==> P   |] ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   763
\end{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   764
\caption{Ordered pairs; projections; general sums} \label{zf-pair}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   765
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   766
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   767
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   768
\subsection{Ordered pairs}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   769
Figure~\ref{zf-pair} presents the rules governing ordered pairs,
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
   770
projections and general sums.  File {\tt ZF/pair.ML} contains the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   771
full (and tedious) proof that $\{\{a\},\{a,b\}\}$ functions as an ordered
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   772
pair.  This property is expressed as two destruction rules,
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   773
\tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   774
as the elimination rule \tdx{Pair_inject}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   775
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   776
The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$.  This
114
96c627d2815e Misc updates
lcp
parents: 111
diff changeset
   777
is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other 
343
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
   778
encodings of ordered pairs.  The non-standard ordered pairs mentioned below
114
96c627d2815e Misc updates
lcp
parents: 111
diff changeset
   779
satisfy $\pair{\emptyset;\emptyset}=\emptyset$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   780
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   781
The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   782
assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   783
$\pair{x,y}$, for $x\in A$ and $y\in B(x)$.  The rule \tdx{SigmaE2}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   784
merely states that $\pair{a,b}\in {\tt Sigma}(A,B)$ implies $a\in A$ and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   785
$b\in B(a)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   786
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   787
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   788
%%% domrange.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   789
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   790
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   791
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   792
\tdx{domainI}        <a,b>: r ==> a : domain(r)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   793
\tdx{domainE}        [| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   794
\tdx{domain_subset}  domain(Sigma(A,B)) <= A
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   795
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   796
\tdx{rangeI}         <a,b>: r ==> b : range(r)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   797
\tdx{rangeE}         [| b : range(r);  !!x. <x,b>: r ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   798
\tdx{range_subset}   range(A*B) <= B
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   799
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   800
\tdx{fieldI1}        <a,b>: r ==> a : field(r)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   801
\tdx{fieldI2}        <a,b>: r ==> b : field(r)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   802
\tdx{fieldCI}        (~ <c,a>:r ==> <a,b>: r) ==> a : field(r)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   803
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   804
\tdx{fieldE}         [| a : field(r);  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   805
                  !!x. <a,x>: r ==> P;  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   806
                  !!x. <x,a>: r ==> P      
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   807
               |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   808
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   809
\tdx{field_subset}   field(A*A) <= A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   810
\end{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   811
\caption{Domain, range and field of a relation} \label{zf-domrange}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   812
\end{figure}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   813
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   814
\begin{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   815
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   816
\tdx{imageI}         [| <a,b>: r;  a:A |] ==> b : r``A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   817
\tdx{imageE}         [| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   818
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   819
\tdx{vimageI}        [| <a,b>: r;  b:B |] ==> a : r-``B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   820
\tdx{vimageE}        [| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   821
\end{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   822
\caption{Image and inverse image} \label{zf-domrange2}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   823
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   824
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   825
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   826
\subsection{Relations}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   827
Figure~\ref{zf-domrange} presents rules involving relations, which are sets
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   828
of ordered pairs.  The converse of a relation~$r$ is the set of all pairs
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   829
$\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   830
{\cdx{converse}$(r)$} is its inverse.  The rules for the domain
343
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
   831
operation, namely \tdx{domainI} and~\tdx{domainE}, assert that
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
   832
\cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   833
some pair of the form~$\pair{x,y}$.  The range operation is similar, and
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   834
the field of a relation is merely the union of its domain and range.  
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   835
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   836
Figure~\ref{zf-domrange2} presents rules for images and inverse images.
343
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
   837
Note that these operations are generalisations of range and domain,
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   838
respectively.  See the file {\tt ZF/domrange.ML} for derivations of the
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   839
rules.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   840
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   841
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   842
%%% func.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   843
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   844
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   845
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   846
\tdx{fun_is_rel}      f: Pi(A,B) ==> f <= Sigma(A,B)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   847
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   848
\tdx{apply_equality}  [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   849
\tdx{apply_equality2} [| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   850
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   851
\tdx{apply_type}      [| f: Pi(A,B);  a:A |] ==> f`a : B(a)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   852
\tdx{apply_Pair}      [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   853
\tdx{apply_iff}       f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   854
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   855
\tdx{fun_extension}   [| f : Pi(A,B);  g: Pi(A,D);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   856
                   !!x. x:A ==> f`x = g`x     |] ==> f=g
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   857
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   858
\tdx{domain_type}     [| <a,b> : f;  f: Pi(A,B) |] ==> a : A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   859
\tdx{range_type}      [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   860
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   861
\tdx{Pi_type}         [| f: A->C;  !!x. x:A ==> f`x: B(x) |] ==> f: Pi(A,B)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   862
\tdx{domain_of_fun}   f: Pi(A,B) ==> domain(f)=A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   863
\tdx{range_of_fun}    f: Pi(A,B) ==> f: A->range(f)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   864
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   865
\tdx{restrict}        a : A ==> restrict(f,A) ` a = f`a
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   866
\tdx{restrict_type}   [| !!x. x:A ==> f`x: B(x) |] ==> 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   867
                restrict(f,A) : Pi(A,B)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   868
\end{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   869
\caption{Functions} \label{zf-func1}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   870
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   871
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   872
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   873
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   874
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   875
\tdx{lamI}         a:A ==> <a,b(a)> : (lam x:A. b(x))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   876
\tdx{lamE}         [| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   877
             |] ==>  P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   878
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   879
\tdx{lam_type}     [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   880
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   881
\tdx{beta}         a : A ==> (lam x:A.b(x)) ` a = b(a)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   882
\tdx{eta}          f : Pi(A,B) ==> (lam x:A. f`x) = f
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   883
\end{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   884
\caption{$\lambda$-abstraction} \label{zf-lam}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   885
\end{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   886
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   887
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   888
\begin{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   889
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   890
\tdx{fun_empty}            0: 0->0
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   891
\tdx{fun_single}           \{<a,b>\} : \{a\} -> \{b\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   892
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   893
\tdx{fun_disjoint_Un}      [| f: A->B;  g: C->D;  A Int C = 0  |] ==>  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   894
                     (f Un g) : (A Un C) -> (B Un D)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   895
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   896
\tdx{fun_disjoint_apply1}  [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   897
                     (f Un g)`a = f`a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   898
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   899
\tdx{fun_disjoint_apply2}  [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   900
                     (f Un g)`c = g`c
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   901
\end{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   902
\caption{Constructing functions from smaller sets} \label{zf-func2}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   903
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   904
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   905
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   906
\subsection{Functions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   907
Functions, represented by graphs, are notoriously difficult to reason
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   908
about.  The file {\tt ZF/func.ML} derives many rules, which overlap more
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   909
than they ought.  This section presents the more important rules.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   910
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   911
Figure~\ref{zf-func1} presents the basic properties of \cdx{Pi}$(A,B)$,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   912
the generalized function space.  For example, if $f$ is a function and
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   913
$\pair{a,b}\in f$, then $f`a=b$ (\tdx{apply_equality}).  Two functions
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   914
are equal provided they have equal domains and deliver equals results
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   915
(\tdx{fun_extension}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   916
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   917
By \tdx{Pi_type}, a function typing of the form $f\in A\to C$ can be
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   918
refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   919
family of sets $\{B(x)\}@{x\in A}$.  Conversely, by \tdx{range_of_fun},
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   920
any dependent typing can be flattened to yield a function type of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   921
$A\to C$; here, $C={\tt range}(f)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   922
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   923
Among the laws for $\lambda$-abstraction, \tdx{lamI} and \tdx{lamE}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   924
describe the graph of the generated function, while \tdx{beta} and
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   925
\tdx{eta} are the standard conversions.  We essentially have a
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   926
dependently-typed $\lambda$-calculus (Fig.\ts\ref{zf-lam}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   927
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   928
Figure~\ref{zf-func2} presents some rules that can be used to construct
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   929
functions explicitly.  We start with functions consisting of at most one
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   930
pair, and may form the union of two functions provided their domains are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   931
disjoint.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   932
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   933
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   934
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   935
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   936
\tdx{Int_absorb}         A Int A = A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   937
\tdx{Int_commute}        A Int B = B Int A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   938
\tdx{Int_assoc}          (A Int B) Int C  =  A Int (B Int C)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   939
\tdx{Int_Un_distrib}     (A Un B) Int C  =  (A Int C) Un (B Int C)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   940
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   941
\tdx{Un_absorb}          A Un A = A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   942
\tdx{Un_commute}         A Un B = B Un A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   943
\tdx{Un_assoc}           (A Un B) Un C  =  A Un (B Un C)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   944
\tdx{Un_Int_distrib}     (A Int B) Un C  =  (A Un C) Int (B Un C)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   945
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   946
\tdx{Diff_cancel}        A-A = 0
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   947
\tdx{Diff_disjoint}      A Int (B-A) = 0
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   948
\tdx{Diff_partition}     A<=B ==> A Un (B-A) = B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   949
\tdx{double_complement}  [| A<=B; B<= C |] ==> (B - (C-A)) = A
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   950
\tdx{Diff_Un}            A - (B Un C) = (A-B) Int (A-C)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   951
\tdx{Diff_Int}           A - (B Int C) = (A-B) Un (A-C)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   952
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   953
\tdx{Union_Un_distrib}   Union(A Un B) = Union(A) Un Union(B)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   954
\tdx{Inter_Un_distrib}   [| a:A;  b:B |] ==> 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   955
                   Inter(A Un B) = Inter(A) Int Inter(B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   956
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   957
\tdx{Int_Union_RepFun}   A Int Union(B) = (UN C:B. A Int C)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   958
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   959
\tdx{Un_Inter_RepFun}    b:B ==> 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   960
                   A Un Inter(B) = (INT C:B. A Un C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   961
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   962
\tdx{SUM_Un_distrib1}    (SUM x:A Un B. C(x)) = 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   963
                   (SUM x:A. C(x)) Un (SUM x:B. C(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   964
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   965
\tdx{SUM_Un_distrib2}    (SUM x:C. A(x) Un B(x)) =
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   966
                   (SUM x:C. A(x))  Un  (SUM x:C. B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   967
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   968
\tdx{SUM_Int_distrib1}   (SUM x:A Int B. C(x)) =
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   969
                   (SUM x:A. C(x)) Int (SUM x:B. C(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   970
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   971
\tdx{SUM_Int_distrib2}   (SUM x:C. A(x) Int B(x)) =
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   972
                   (SUM x:C. A(x)) Int (SUM x:C. B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   973
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   974
\caption{Equalities} \label{zf-equalities}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   975
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   976
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   977
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   978
\begin{figure}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   979
%\begin{constants} 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   980
%  \cdx{1}       & $i$           &       & $\{\emptyset\}$       \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   981
%  \cdx{bool}    & $i$           &       & the set $\{\emptyset,1\}$     \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   982
%  \cdx{cond}   & $[i,i,i]\To i$ &       & conditional for {\tt bool}    \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   983
%  \cdx{not}    & $i\To i$       &       & negation for {\tt bool}       \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   984
%  \sdx{and}    & $[i,i]\To i$   & Left 70 & conjunction for {\tt bool}  \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   985
%  \sdx{or}     & $[i,i]\To i$   & Left 65 & disjunction for {\tt bool}  \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   986
%  \sdx{xor}    & $[i,i]\To i$   & Left 65 & exclusive-or for {\tt bool}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   987
%\end{constants}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   988
%
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   989
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   990
\tdx{bool_def}       bool == \{0,1\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   991
\tdx{cond_def}       cond(b,c,d) == if(b=1,c,d)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   992
\tdx{not_def}        not(b)  == cond(b,0,1)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   993
\tdx{and_def}        a and b == cond(a,b,0)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   994
\tdx{or_def}         a or b  == cond(a,1,b)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   995
\tdx{xor_def}        a xor b == cond(a,not(b),b)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   996
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   997
\tdx{bool_1I}        1 : bool
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   998
\tdx{bool_0I}        0 : bool
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
   999
\tdx{boolE}          [| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1000
\tdx{cond_1}         cond(1,c,d) = c
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1001
\tdx{cond_0}         cond(0,c,d) = d
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1002
\end{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1003
\caption{The booleans} \label{zf-bool}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1004
\end{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1005
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1006
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1007
\section{Further developments}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1008
The next group of developments is complex and extensive, and only
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1009
highlights can be covered here.  It involves many theories and ML files of
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1010
proofs. 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1011
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1012
Figure~\ref{zf-equalities} presents commutative, associative, distributive,
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1013
and idempotency laws of union and intersection, along with other equations.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1014
See file {\tt ZF/equalities.ML}.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1015
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1016
Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1017
usual operators including a conditional (Fig.\ts\ref{zf-bool}).  Although
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1018
{\ZF} is a first-order theory, you can obtain the effect of higher-order
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1019
logic using {\tt bool}-valued functions, for example.  The constant~{\tt1}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1020
is translated to {\tt succ(0)}.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1021
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1022
\begin{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1023
\index{*"+ symbol}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1024
\begin{constants}
343
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
  1025
  \it symbol    & \it meta-type & \it priority & \it description \\ 
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1026
  \tt +         & $[i,i]\To i$  &  Right 65     & disjoint union operator\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1027
  \cdx{Inl}~~\cdx{Inr}  & $i\To i$      &       & injections\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1028
  \cdx{case}    & $[i\To i,i\To i, i]\To i$ &   & conditional for $A+B$
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1029
\end{constants}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1030
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1031
\tdx{sum_def}        A+B == \{0\}*A Un \{1\}*B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1032
\tdx{Inl_def}        Inl(a) == <0,a>
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1033
\tdx{Inr_def}        Inr(b) == <1,b>
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1034
\tdx{case_def}       case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1035
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1036
\tdx{sum_InlI}       a : A ==> Inl(a) : A+B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1037
\tdx{sum_InrI}       b : B ==> Inr(b) : A+B
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1038
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1039
\tdx{Inl_inject}     Inl(a)=Inl(b) ==> a=b
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1040
\tdx{Inr_inject}     Inr(a)=Inr(b) ==> a=b
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1041
\tdx{Inl_neq_Inr}    Inl(a)=Inr(b) ==> P
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1042
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1043
\tdx{sumE2}   u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1044
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1045
\tdx{case_Inl}       case(c,d,Inl(a)) = c(a)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1046
\tdx{case_Inr}       case(c,d,Inr(b)) = d(b)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1047
\end{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1048
\caption{Disjoint unions} \label{zf-sum}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1049
\end{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1050
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1051
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1052
Theory \thydx{Sum} defines the disjoint union of two sets, with
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1053
injections and a case analysis operator (Fig.\ts\ref{zf-sum}).  Disjoint
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1054
unions play a role in datatype definitions, particularly when there is
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1055
mutual recursion~\cite{paulson-set-II}.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1056
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1057
\begin{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1058
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1059
\tdx{QPair_def}       <a;b> == a+b
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1060
\tdx{qsplit_def}      qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1061
\tdx{qfsplit_def}     qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)
461
170de0c52a9b minor edits
lcp
parents: 349
diff changeset
  1062
\tdx{qconverse_def}   qconverse(r) == \{z. w:r, EX x y. w=<x;y> & z=<y;x>\}
170de0c52a9b minor edits
lcp
parents: 349
diff changeset
  1063
\tdx{QSigma_def}      QSigma(A,B)  == UN x:A. UN y:B(x). \{<x;y>\}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1064
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1065
\tdx{qsum_def}        A <+> B      == (\{0\} <*> A) Un (\{1\} <*> B)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1066
\tdx{QInl_def}        QInl(a)      == <0;a>
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1067
\tdx{QInr_def}        QInr(b)      == <1;b>
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1068
\tdx{qcase_def}       qcase(c,d)   == qsplit(\%y z. cond(y, d(z), c(z)))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1069
\end{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1070
\caption{Non-standard pairs, products and sums} \label{zf-qpair}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1071
\end{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1072
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1073
Theory \thydx{QPair} defines a notion of ordered pair that admits
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1074
non-well-founded tupling (Fig.\ts\ref{zf-qpair}).  Such pairs are written
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1075
{\tt<$a$;$b$>}.  It also defines the eliminator \cdx{qsplit}, the
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1076
converse operator \cdx{qconverse}, and the summation operator
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1077
\cdx{QSigma}.  These are completely analogous to the corresponding
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1078
versions for standard ordered pairs.  The theory goes on to define a
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1079
non-standard notion of disjoint sum using non-standard pairs.  All of these
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1080
concepts satisfy the same properties as their standard counterparts; in
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1081
addition, {\tt<$a$;$b$>} is continuous.  The theory supports coinductive
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1082
definitions, for example of infinite lists~\cite{paulson-final}.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1083
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1084
\begin{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1085
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1086
\tdx{bnd_mono_def}   bnd_mono(D,h) == 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1087
                 h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1088
461
170de0c52a9b minor edits
lcp
parents: 349
diff changeset
  1089
\tdx{lfp_def}        lfp(D,h) == Inter(\{X: Pow(D). h(X) <= X\})
170de0c52a9b minor edits
lcp
parents: 349
diff changeset
  1090
\tdx{gfp_def}        gfp(D,h) == Union(\{X: Pow(D). X <= h(X)\})
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1091
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1092
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1093
\tdx{lfp_lowerbound} [| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1094
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1095
\tdx{lfp_subset}     lfp(D,h) <= D
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1096
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1097
\tdx{lfp_greatest}   [| bnd_mono(D,h);  
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1098
                  !!X. [| h(X) <= X;  X<=D |] ==> A<=X 
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1099
               |] ==> A <= lfp(D,h)
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1100
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1101
\tdx{lfp_Tarski}     bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1102
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1103
\tdx{induct}         [| a : lfp(D,h);  bnd_mono(D,h);
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1104
                  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x)
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1105
               |] ==> P(a)
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1106
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1107
\tdx{lfp_mono}       [| bnd_mono(D,h);  bnd_mono(E,i);
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1108
                  !!X. X<=D ==> h(X) <= i(X)  
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1109
               |] ==> lfp(D,h) <= lfp(E,i)
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1110
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1111
\tdx{gfp_upperbound} [| A <= h(A);  A<=D |] ==> A <= gfp(D,h)
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1112
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1113
\tdx{gfp_subset}     gfp(D,h) <= D
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1114
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1115
\tdx{gfp_least}      [| bnd_mono(D,h);  
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1116
                  !!X. [| X <= h(X);  X<=D |] ==> X<=A
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1117
               |] ==> gfp(D,h) <= A
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1118
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1119
\tdx{gfp_Tarski}     bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1120
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1121
\tdx{coinduct}       [| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1122
               |] ==> a : gfp(D,h)
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1123
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1124
\tdx{gfp_mono}       [| bnd_mono(D,h);  D <= E;
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1125
                  !!X. X<=D ==> h(X) <= i(X)  
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1126
               |] ==> gfp(D,h) <= gfp(E,i)
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1127
\end{ttbox}
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1128
\caption{Least and greatest fixedpoints} \label{zf-fixedpt}
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1129
\end{figure}
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1130
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1131
The Knaster-Tarski Theorem states that every monotone function over a
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1132
complete lattice has a fixedpoint.  Theory \thydx{Fixedpt} proves the
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1133
Theorem only for a particular lattice, namely the lattice of subsets of a
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1134
set (Fig.\ts\ref{zf-fixedpt}).  The theory defines least and greatest
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1135
fixedpoint operators with corresponding induction and coinduction rules.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1136
These are essential to many definitions that follow, including the natural
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1137
numbers and the transitive closure operator.  The (co)inductive definition
595
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1138
package also uses the fixedpoint operators~\cite{paulson-CADE}.  See
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1139
Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1140
Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1141
proofs.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1142
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1143
Monotonicity properties are proved for most of the set-forming operations:
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1144
union, intersection, Cartesian product, image, domain, range, etc.  These
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1145
are useful for applying the Knaster-Tarski Fixedpoint Theorem.  The proofs
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1146
themselves are trivial applications of Isabelle's classical reasoner.  See
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1147
file {\tt ZF/mono.ML}.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1148
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1149
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1150
\begin{figure}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1151
\begin{constants} 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1152
  \it symbol  & \it meta-type & \it priority & \it description \\ 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1153
  \sdx{O}       & $[i,i]\To i$  &  Right 60     & composition ($\circ$) \\
349
0ddc495e8b83 post-CRC corrections
lcp
parents: 343
diff changeset
  1154
  \cdx{id}      & $i\To i$      &       & identity function \\
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1155
  \cdx{inj}     & $[i,i]\To i$  &       & injective function space\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1156
  \cdx{surj}    & $[i,i]\To i$  &       & surjective function space\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1157
  \cdx{bij}     & $[i,i]\To i$  &       & bijective function space
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1158
\end{constants}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1159
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1160
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1161
\tdx{comp_def}  r O s     == \{xz : domain(s)*range(r) . 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1162
                        EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r\}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1163
\tdx{id_def}    id(A)     == (lam x:A. x)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1164
\tdx{inj_def}   inj(A,B)  == \{ f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1165
\tdx{surj_def}  surj(A,B) == \{ f: A->B . ALL y:B. EX x:A. f`x=y\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1166
\tdx{bij_def}   bij(A,B)  == inj(A,B) Int surj(A,B)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1167
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1168
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1169
\tdx{left_inverse}     [| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1170
\tdx{right_inverse}    [| f: inj(A,B);  b: range(f) |] ==> 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1171
                 f`(converse(f)`b) = b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1172
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1173
\tdx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1174
\tdx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1175
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1176
\tdx{comp_type}        [| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1177
\tdx{comp_assoc}       (r O s) O t = r O (s O t)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1178
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1179
\tdx{left_comp_id}     r<=A*B ==> id(B) O r = r
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1180
\tdx{right_comp_id}    r<=A*B ==> r O id(A) = r
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1181
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1182
\tdx{comp_func}        [| g:A->B; f:B->C |] ==> (f O g):A->C
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1183
\tdx{comp_func_apply}  [| g:A->B; f:B->C; a:A |] ==> (f O g)`a = f`(g`a)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1184
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1185
\tdx{comp_inj}         [| g:inj(A,B);  f:inj(B,C)  |] ==> (f O g):inj(A,C)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1186
\tdx{comp_surj}        [| g:surj(A,B); f:surj(B,C) |] ==> (f O g):surj(A,C)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1187
\tdx{comp_bij}         [| g:bij(A,B); f:bij(B,C) |] ==> (f O g):bij(A,C)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1188
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1189
\tdx{left_comp_inverse}     f: inj(A,B) ==> converse(f) O f = id(A)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1190
\tdx{right_comp_inverse}    f: surj(A,B) ==> f O converse(f) = id(B)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1191
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1192
\tdx{bij_disjoint_Un}   
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1193
    [| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1194
    (f Un g) : bij(A Un C, B Un D)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1195
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1196
\tdx{restrict_bij}  [| f:inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1197
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1198
\caption{Permutations} \label{zf-perm}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1199
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1200
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1201
The theory \thydx{Perm} is concerned with permutations (bijections) and
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1202
related concepts.  These include composition of relations, the identity
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1203
relation, and three specialized function spaces: injective, surjective and
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1204
bijective.  Figure~\ref{zf-perm} displays many of their properties that
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1205
have been proved.  These results are fundamental to a treatment of
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1206
equipollence and cardinality.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1207
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1208
\begin{figure}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1209
\index{#*@{\tt\#*} symbol}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1210
\index{*div symbol}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1211
\index{*mod symbol}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1212
\index{#+@{\tt\#+} symbol}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1213
\index{#-@{\tt\#-} symbol}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1214
\begin{constants}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1215
  \it symbol  & \it meta-type & \it priority & \it description \\ 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1216
  \cdx{nat}     & $i$                   &       & set of natural numbers \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1217
  \cdx{nat_case}& $[i,i\To i,i]\To i$     &     & conditional for $nat$\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1218
  \cdx{rec}     & $[i,i,[i,i]\To i]\To i$ &     & recursor for $nat$\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1219
  \tt \#*       & $[i,i]\To i$  &  Left 70      & multiplication \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1220
  \tt div       & $[i,i]\To i$  &  Left 70      & division\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1221
  \tt mod       & $[i,i]\To i$  &  Left 70      & modulus\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1222
  \tt \#+       & $[i,i]\To i$  &  Left 65      & addition\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1223
  \tt \#-       & $[i,i]\To i$  &  Left 65      & subtraction
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1224
\end{constants}
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1225
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1226
\begin{ttbox}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1227
\tdx{nat_def}       nat == lfp(lam r: Pow(Inf). \{0\} Un \{succ(x). x:r\}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1228
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1229
\tdx{nat_case_def}  nat_case(a,b,k) == 
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1230
              THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1231
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1232
\tdx{rec_def}       rec(k,a,b) ==  
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1233
              transrec(k, \%n f. nat_case(a, \%m. b(m, f`m), n))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1234
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1235
\tdx{add_def}       m#+n    == rec(m, n, \%u v.succ(v))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1236
\tdx{diff_def}      m#-n    == rec(n, m, \%u v. rec(v, 0, \%x y.x))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1237
\tdx{mult_def}      m#*n    == rec(m, 0, \%u v. n #+ v)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1238
\tdx{mod_def}       m mod n == transrec(m, \%j f. if(j:n, j, f`(j#-n)))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1239
\tdx{div_def}       m div n == transrec(m, \%j f. if(j:n, 0, succ(f`(j#-n))))
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1240
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1241
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1242
\tdx{nat_0I}        0 : nat
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1243
\tdx{nat_succI}     n : nat ==> succ(n) : nat
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1244
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1245
\tdx{nat_induct}        
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1246
    [| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1247
    |] ==> P(n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1248
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1249
\tdx{nat_case_0}    nat_case(a,b,0) = a
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1250
\tdx{nat_case_succ} nat_case(a,b,succ(m)) = b(m)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1251
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1252
\tdx{rec_0}         rec(0,a,b) = a
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1253
\tdx{rec_succ}      rec(succ(m),a,b) = b(m, rec(m,a,b))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1254
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1255
\tdx{mult_type}     [| m:nat;  n:nat |] ==> m #* n : nat
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1256
\tdx{mult_0}        0 #* n = 0
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1257
\tdx{mult_succ}     succ(m) #* n = n #+ (m #* n)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1258
\tdx{mult_commute}  [| m:nat;  n:nat |] ==> m #* n = n #* m
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1259
\tdx{add_mult_dist}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1260
    [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1261
\tdx{mult_assoc}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1262
    [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1263
\tdx{mod_quo_equality}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1264
    [| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1265
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1266
\caption{The natural numbers} \label{zf-nat}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1267
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1268
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1269
Theory \thydx{Nat} defines the natural numbers and mathematical
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1270
induction, along with a case analysis operator.  The set of natural
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1271
numbers, here called {\tt nat}, is known in set theory as the ordinal~$\omega$.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1272
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1273
Theory \thydx{Arith} defines primitive recursion and goes on to develop
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1274
arithmetic on the natural numbers (Fig.\ts\ref{zf-nat}).  It defines
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1275
addition, multiplication, subtraction, division, and remainder.  Many of
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1276
their properties are proved: commutative, associative and distributive
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1277
laws, identity and cancellation laws, etc.  The most interesting result is
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1278
perhaps the theorem $a \bmod b + (a/b)\times b = a$.  Division and
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1279
remainder are defined by repeated subtraction, which requires well-founded
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1280
rather than primitive recursion; the termination argument relies on the
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1281
divisor's being non-zero.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1282
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1283
Theory \thydx{Univ} defines a `universe' ${\tt univ}(A)$, for
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1284
constructing datatypes such as trees.  This set contains $A$ and the
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1285
natural numbers.  Vitally, it is closed under finite products: ${\tt
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1286
  univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$.  This theory also
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1287
defines the cumulative hierarchy of axiomatic set theory, which
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1288
traditionally is written $V@\alpha$ for an ordinal~$\alpha$.  The
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1289
`universe' is a simple generalization of~$V@\omega$.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1290
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1291
Theory \thydx{QUniv} defines a `universe' ${\tt quniv}(A)$, for
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1292
constructing codatatypes such as streams.  It is analogous to ${\tt
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1293
  univ}(A)$ (and is defined in terms of it) but is closed under the
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1294
non-standard product and sum.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1295
595
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1296
Theory {\tt Finite} (Figure~\ref{zf-fin}) defines the finite set operator;
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1297
${\tt Fin}(A)$ is the set of all finite sets over~$A$.  The theory employs
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1298
Isabelle's inductive definition package, which proves various rules
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1299
automatically.  The induction rule shown is stronger than the one proved by
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1300
the package.  The theory also defines the set of all finite functions
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1301
between two given sets.
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1302
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1303
\begin{figure}
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1304
\begin{ttbox}
595
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1305
\tdx{Fin.emptyI}      0 : Fin(A)
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1306
\tdx{Fin.consI}       [| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1307
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1308
\tdx{Fin_induct}
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1309
    [| b: Fin(A);
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1310
       P(0);
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1311
       !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y))
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1312
    |] ==> P(b)
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1313
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1314
\tdx{Fin_mono}        A<=B ==> Fin(A) <= Fin(B)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1315
\tdx{Fin_UnI}         [| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1316
\tdx{Fin_UnionI}      C : Fin(Fin(A)) ==> Union(C) : Fin(A)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1317
\tdx{Fin_subset}      [| c<=b;  b: Fin(A) |] ==> c: Fin(A)
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1318
\end{ttbox}
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1319
\caption{The finite set operator} \label{zf-fin}
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1320
\end{figure}
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1321
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1322
\begin{figure}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1323
\begin{constants}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1324
  \cdx{list}    & $i\To i$      && lists over some set\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1325
  \cdx{list_case} & $[i, [i,i]\To i, i] \To i$  && conditional for $list(A)$ \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1326
  \cdx{list_rec} & $[i, i, [i,i,i]\To i] \To i$ && recursor for $list(A)$ \\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1327
  \cdx{map}     & $[i\To i, i] \To i$   &       & mapping functional\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1328
  \cdx{length}  & $i\To i$              &       & length of a list\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1329
  \cdx{rev}     & $i\To i$              &       & reverse of a list\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1330
  \tt \at       & $[i,i]\To i$  &  Right 60     & append for lists\\
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1331
  \cdx{flat}    & $i\To i$   &                  & append of list of lists
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1332
\end{constants}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1333
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1334
\underscoreon %%because @ is used here
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1335
\begin{ttbox}
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1336
\tdx{list_rec_def}    list_rec(l,c,h) == 
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 131
diff changeset
  1337
                Vrec(l, \%l g.list_case(c, \%x xs. h(x, xs, g`xs), l))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1338
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1339
\tdx{map_def}         map(f,l)  == list_rec(l,  0,  \%x xs r. <f(x), r>)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1340
\tdx{length_def}      length(l) == list_rec(l,  0,  \%x xs r. succ(r))
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1341
\tdx{app_def}         xs@ys     == list_rec(xs, ys, \%x xs r. <x,r>)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1342
\tdx{rev_def}         rev(l)    == list_rec(l,  0,  \%x xs r. r @ <x,0>)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1343
\tdx{flat_def}        flat(ls)  == list_rec(ls, 0,  \%l ls r. l @ r)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1344
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1345
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1346
\tdx{NilI}            Nil : list(A)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1347
\tdx{ConsI}           [| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1348
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1349
\tdx{List.induct}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1350
    [| l: list(A);
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1351
       P(Nil);
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1352
       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(Cons(x,y))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1353
    |] ==> P(l)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1354
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1355
\tdx{Cons_iff}        Cons(a,l)=Cons(a',l') <-> a=a' & l=l'
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1356
\tdx{Nil_Cons_iff}    ~ Nil=Cons(a,l)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1357
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1358
\tdx{list_mono}       A<=B ==> list(A) <= list(B)
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1359
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1360
\tdx{list_rec_Nil}    list_rec(Nil,c,h) = c
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1361
\tdx{list_rec_Cons}   list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1362
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1363
\tdx{map_ident}       l: list(A) ==> map(\%u.u, l) = l
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1364
\tdx{map_compose}     l: list(A) ==> map(h, map(j,l)) = map(\%u.h(j(u)), l)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1365
\tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1366
\tdx{map_type}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1367
    [| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1368
\tdx{map_flat}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1369
    ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1370
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1371
\caption{Lists} \label{zf-list}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1372
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1373
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1374
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1375
Figure~\ref{zf-list} presents the set of lists over~$A$, ${\tt list}(A)$.
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1376
The definition employs Isabelle's datatype package, which defines the
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1377
introduction and induction rules automatically, as well as the constructors
343
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
  1378
and case operator (\verb|list_case|).  See file {\tt ZF/List.ML}.
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
  1379
The file {\tt ZF/ListFn.thy} proceeds to define structural
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1380
recursion and the usual list functions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1381
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1382
The constructions of the natural numbers and lists make use of a suite of
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1383
operators for handling recursive function definitions.  I have described
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1384
the developments in detail elsewhere~\cite{paulson-set-II}.  Here is a brief
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1385
summary:
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1386
\begin{itemize}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1387
  \item Theory {\tt Trancl} defines the transitive closure of a relation
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1388
    (as a least fixedpoint).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1389
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1390
  \item Theory {\tt WF} proves the Well-Founded Recursion Theorem, using an
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1391
    elegant approach of Tobias Nipkow.  This theorem permits general
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1392
    recursive definitions within set theory.
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1393
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1394
  \item Theory {\tt Ord} defines the notions of transitive set and ordinal
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1395
    number.  It derives transfinite induction.  A key definition is {\bf
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1396
      less than}: $i<j$ if and only if $i$ and $j$ are both ordinals and
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1397
    $i\in j$.  As a special case, it includes less than on the natural
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1398
    numbers.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1399
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1400
  \item Theory {\tt Epsilon} derives $\epsilon$-induction and
343
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
  1401
    $\epsilon$-recursion, which are generalisations of transfinite
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
  1402
    induction and recursion.  It also defines \cdx{rank}$(x)$, which is the
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
  1403
    least ordinal $\alpha$ such that $x$ is constructed at stage $\alpha$
8d77f767bd26 final Springer copy
lcp
parents: 317
diff changeset
  1404
    of the cumulative hierarchy (thus $x\in V@{\alpha+1}$).
317
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1405
\end{itemize}
8a96a64e0b35 penultimate Springer draft
lcp
parents: 287
diff changeset
  1406
595
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1407
Other important theories lead to a theory of cardinal numbers.  They have
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1408
not yet been written up anywhere.  Here is a summary:
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1409
\begin{itemize}
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1410
\item Theory {\tt Rel} defines the basic properties of relations, such as
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1411
  (ir)reflexivity, (a)symmetry, and transitivity.
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1412
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1413
\item Theory {\tt EquivClass} develops a theory of equivalence
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1414
  classes, not using the Axiom of Choice.
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1415
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498
diff changeset
  1416
\item Theory {\tt Order} defines partial orderings, total orderings and
96c87d5bb015 Added mention of directory IMP; tidied the section on examples.
lcp
parents: 498