doc-src/Logics/ZF.tex
author lcp
Wed, 10 Nov 1993 05:00:57 +0100
changeset 104 d8205bb279a7
child 111 1b3cddf41b2d
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
%%%See grant/bra/Lib/ZF.tex for lfp figure
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\chapter{Zermelo-Fraenkel set theory}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
The directory~\ttindexbold{ZF} implements Zermelo-Fraenkel set
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
theory~\cite{halmos60,suppes72} as an extension of~\ttindex{FOL}, classical
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
first-order logic.  The theory includes a collection of derived natural
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
deduction rules, for use with Isabelle's classical reasoning module.  Much
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
of it is based on the work of No\"el~\cite{noel}.  The theory has the {\ML}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
identifier \ttindexbold{ZF.thy}.  However, many further theories
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
are defined, introducing the natural numbers, etc.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
A tremendous amount of set theory has been formally developed, including
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
the basic properties of relations, functions and ordinals.  Significant
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
results have been proved, such as the Schr\"oder-Bernstein Theorem and the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
Recursion Theorem.  General methods have been developed for solving
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
recursion equations over monotonic functors; these have been applied to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
yield constructions of lists and trees.  Thus, we may even regard set
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
theory as a computational logic.  It admits recursive definitions of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
functions and types.  It has similarities with Martin-L\"of type theory,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
although of course it is classical.
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,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
namely \ttindex{hyp_subst_tac}, the simplifier, and the classical reasoning
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
module.  The main simplification set is called \ttindexbold{ZF_ss}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
Several classical rule sets are defined, including \ttindexbold{lemmas_cs},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
\ttindexbold{upair_cs} and~\ttindexbold{ZF_cs}.  See the files on directory
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
{\tt ZF} for details.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
\section{Which version of axiomatic set theory?}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
Resolution theorem provers can work in set theory, using the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
Bernays-G\"odel axiom system~(BG) because it is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
finite~\cite{boyer86,quaife92}.  {\ZF} does not have a finite axiom system
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
(because of its Axiom Scheme of Replacement) and is therefore unsuitable
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
for classical resolution.  Since Isabelle has no difficulty with axiom
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
schemes, we may adopt either axiom system.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
These two theories differ in their treatment of {\bf classes}, which are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
collections that are ``too big'' to be sets.  The class of all sets,~$V$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
cannot be a set without admitting Russell's Paradox.  In BG, both classes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
and sets are individuals; $x\in V$ expresses that $x$ is a set.  In {\ZF}, all
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
variables denote sets; classes are identified with unary predicates.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
two systems define essentially the same sets and classes, with similar
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
properties.  In particular, a class cannot belong to another class (let
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
alone a set).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
Modern set theorists tend to prefer {\ZF} because they are mainly concerned
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
with sets, rather than classes.  BG requires tiresome proofs that various
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
collections are sets; for instance, showing $x\in\{x\}$ requires showing that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
$x$ is a set.  {\ZF} does not have this problem.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
\begin{tabular}{rrr} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
  \it name    	&\it meta-type 	& \it description \\ 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
  \idx{0}	& $i$		& empty set\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
  \idx{cons}	& $[i,i]\To i$	& finite set constructor\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
  \idx{Upair}	& $[i,i]\To i$	& unordered pairing\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
  \idx{Pair}	& $[i,i]\To i$	& ordered pairing\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
  \idx{Inf}	& $i$	& infinite set\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
  \idx{Pow}	& $i\To i$	& powerset\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
  \idx{Union} \idx{Inter} & $i\To i$	& set union/intersection \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
  \idx{split}	& $[i, [i,i]\To i] \To i$ & generalized projection\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
  \idx{fst} \idx{snd}	& $i\To i$	& projections\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
  \idx{converse}& $i\To i$	& converse of a relation\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
  \idx{succ}	& $i\To i$	& successor\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
  \idx{Collect}	& $[i,i\To o]\To i$	& separation\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
  \idx{Replace}	& $[i, [i,i]\To o] \To i$	& replacement\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
  \idx{PrimReplace} & $[i, [i,i]\To o] \To i$	& primitive replacement\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
  \idx{RepFun}	& $[i, i\To i] \To i$	& functional replacement\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
  \idx{Pi} \idx{Sigma}	& $[i,i\To i]\To i$	& general product/sum\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
  \idx{domain}	& $i\To i$	& domain of a relation\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
  \idx{range}	& $i\To i$	& range of a relation\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
  \idx{field}	& $i\To i$	& field of a relation\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
  \idx{Lambda}	& $[i, i\To i]\To i$	& $\lambda$-abstraction\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
  \idx{restrict}& $[i, i] \To i$	& restriction of a function\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
  \idx{The}	& $[i\To o]\To i$	& definite description\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
  \idx{if}	& $[o,i,i]\To i$	& conditional\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
  \idx{Ball} \idx{Bex}	& $[i, i\To o]\To o$	& bounded quantifiers
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
\subcaption{Constants}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
\indexbold{*"`"`}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
\indexbold{*"-"`"`}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
\indexbold{*"`}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
\indexbold{*"-}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
\indexbold{*":}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
\indexbold{*"<"=}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
\begin{tabular}{rrrr} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
  \it symbol  & \it meta-type & \it precedence & \it description \\ 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
  \tt ``	& $[i,i]\To i$	&  Left 90	& image \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
  \tt -``	& $[i,i]\To i$	&  Left 90	& inverse image \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
  \tt `		& $[i,i]\To i$	&  Left 90	& application \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
  \idx{Int}	& $[i,i]\To i$	&  Left 70	& intersection ($\inter$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
  \idx{Un}	& $[i,i]\To i$	&  Left 65	& union ($\union$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
  \tt -		& $[i,i]\To i$	&  Left 65	& set difference ($-$) \\[1ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
  \tt:		& $[i,i]\To o$	&  Left 50	& membership ($\in$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
  \tt <=	& $[i,i]\To o$	&  Left 50	& subset ($\subseteq$) 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
\subcaption{Infixes}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
\caption{Constants of {\ZF}} \label{ZF-constants}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\end{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
\section{The syntax of set theory}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
The language of set theory, as studied by logicians, has no constants.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
traditional axioms merely assert the existence of empty sets, unions,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
powersets, etc.; this would be intolerable for practical reasoning.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
Isabelle theory declares constants for primitive sets.  It also extends
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
{\tt FOL} with additional syntax for finite sets, ordered pairs,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
comprehension, general union/intersection, general sums/products, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
bounded quantifiers.  In most other respects, Isabelle implements precisely
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
Zermelo-Fraenkel set theory.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
Figure~\ref{ZF-constants} lists the constants and infixes of~\ZF, while
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
Figure~\ref{ZF-trans} presents the syntax translations.  Finally,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
Figure~\ref{ZF-syntax} presents the full grammar for set theory, including
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
the constructs of \FOL.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
Set theory does not use polymorphism.  All terms in {\ZF} have type~{\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
i}, which is the type of individuals and lies in class {\it logic}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
The type of first-order formulae,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
remember, is~{\it o}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
Infix operators include union and intersection ($A\union B$ and $A\inter
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
B$), and the subset and membership relations.  Note that $a$\verb|~:|$b$ is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
translated to \verb|~(|$a$:$b$\verb|)|.  The union and intersection
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
operators ($\bigcup A$ and $\bigcap A$) form the union or intersection of a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
set of sets; $\bigcup A$ means the same as $\bigcup@{x\in A}x$.  Of these
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
operators, only $\bigcup A$ is primitive.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
The constant \ttindexbold{Upair} constructs unordered pairs; thus {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
Upair($A$,$B$)} denotes the set~$\{A,B\}$ and {\tt Upair($A$,$A$)} denotes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
the singleton~$\{A\}$.  As usual in {\ZF}, general union is used to define
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
binary union.  The Isabelle version goes on to define the constant
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
\ttindexbold{cons}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
\begin{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
   A\cup B  		& \equiv &	 \bigcup({\tt Upair}(A,B)) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
   {\tt cons}(a,B) 	& \equiv &	  {\tt Upair}(a,a) \union B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
\end{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
obvious manner using~{\tt cons} and~$\emptyset$ (the empty set):
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
\begin{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
 \{a,b,c\} & \equiv & {\tt cons}(a,{\tt cons}(b,{\tt cons}(c,\emptyset)))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
\end{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
The constant \ttindexbold{Pair} constructs ordered pairs, as in {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
Pair($a$,$b$)}.  Ordered pairs may also be written within angle brackets,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
as {\tt<$a$,$b$>}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
In {\ZF}, a function is a set of pairs.  A {\ZF} function~$f$ is simply an
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
individual as far as Isabelle is concerned: its Isabelle type is~$i$, not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
say $i\To i$.  The infix operator~{\tt`} denotes the application of a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
\indexbold{*"-">}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
\indexbold{*"*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
\begin{center} \tt\frenchspacing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
\begin{tabular}{rrr} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
  \it external		& \it internal	& \it description \\ 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
  $a$ \ttilde: $b$      & \ttilde($a$ : $b$)    & \rm negated membership\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
  \{$a@1$, $\ldots$, $a@n$\}  &  cons($a@1$,$\cdots$,cons($a@n$,0)) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
        \rm finite set \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
  <$a$, $b$>  		&  Pair($a$,$b$) 	& \rm ordered pair \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
  <$a$, $b$, $c$>	&  <$a$, <$b$, $c$>>  & \rm nested pairs (any depth) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
  \{$x$:$A . P[x]$\}	&  Collect($A$,$\lambda x.P[x]$) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
        \rm separation \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
  \{$y . x$:$A$, $Q[x,y]$\}  &  Replace($A$,$\lambda x\,y.Q[x,y]$) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
        \rm replacement \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
  \{$b[x] . x$:$A$\}  &  RepFun($A$,$\lambda x.b[x]$) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
        \rm functional replacement \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
  \idx{INT} $x$:$A . B[x]$	& Inter(\{$B[x] . x$:$A$\}) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
	\rm general intersection \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
  \idx{UN}  $x$:$A . B[x]$	& Union(\{$B[x] . x$:$A$\}) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
	\rm general union \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
  \idx{PROD} $x$:$A . B[x]$	& Pi($A$,$\lambda x.B[x]$) & 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
	\rm general product \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
  \idx{SUM}  $x$:$A . B[x]$	& Sigma($A$,$\lambda x.B[x]$) & 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
	\rm general sum \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
  $A$ -> $B$		& Pi($A$,$\lambda x.B$) & 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
	\rm function space \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
  $A$ * $B$		& Sigma($A$,$\lambda x.B$) & 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
	\rm binary product \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
  \idx{THE}  $x . P[x]$	& The($\lambda x.P[x]$) & 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
	\rm definite description \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
  \idx{lam}  $x$:$A . b[x]$	& Lambda($A$,$\lambda x.b[x]$) & 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
	\rm $\lambda$-abstraction\\[1ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
  \idx{ALL} $x$:$A . P[x]$	& Ball($A$,$\lambda x.P[x]$) & 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
	\rm bounded $\forall$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
  \idx{EX}  $x$:$A . P[x]$	& Bex($A$,$\lambda x.P[x]$) & 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
	\rm bounded $\exists$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
\caption{Translations for {\ZF}} \label{ZF-trans}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
\end{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
\dquotes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
\[\begin{array}{rcl}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
    term & = & \hbox{expression of type~$i$} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
	 & | & "\{ " term\; ("," term)^* " \}" \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
	 & | & "< " term ", " term " >" \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
	 & | & "\{ " id ":" term " . " formula " \}" \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
	 & | & "\{ " id " . " id ":" term "," formula " \}" \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
	 & | & "\{ " term " . " id ":" term " \}" \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
	 & | & term " `` " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
	 & | & term " -`` " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
	 & | & term " ` " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
	 & | & term " * " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
	 & | & term " Int " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
	 & | & term " Un " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
	 & | & term " - " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
	 & | & term " -> " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
	 & | & "THE~~"  id  " . " formula\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
	 & | & "lam~~"  id ":" term " . " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
	 & | & "INT~~"  id ":" term " . " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
	 & | & "UN~~~"  id ":" term " . " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
	 & | & "PROD~"  id ":" term " . " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
	 & | & "SUM~~"  id ":" term " . " term \\[2ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
 formula & = & \hbox{expression of type~$o$} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
	 & | & term " : " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
	 & | & term " <= " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
	 & | & term " = " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
	 & | & "\ttilde\ " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
	 & | & formula " \& " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
	 & | & formula " | " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
	 & | & formula " --> " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
	 & | & formula " <-> " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
	 & | & "ALL " id ":" term " . " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
	 & | & "EX~~" id ":" term " . " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
	 & | & "ALL~" id~id^* " . " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
	 & | & "EX~~" id~id^* " . " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
	 & | & "EX!~" id~id^* " . " formula
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
  \end{array}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
\caption{Full grammar for {\ZF}} \label{ZF-syntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
\end{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
\section{Binding operators}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
The constant \ttindexbold{Collect} constructs sets by the principle of {\bf
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
  separation}.  The syntax for separation is \hbox{\tt\{$x$:$A$.$P[x]$\}},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
where $P[x]$ is a formula that may contain free occurrences of~$x$.  It
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
abbreviates the set {\tt Collect($A$,$\lambda x.P$[x])}, which consists of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
all $x\in A$ that satisfy~$P[x]$.  Note that {\tt Collect} is an
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
unfortunate choice of name: some set theories adopt a set-formation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
principle, related to replacement, called collection.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
The constant \ttindexbold{Replace} constructs sets by the principle of {\bf
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
  replacement}.  The syntax for replacement is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
\hbox{\tt\{$y$.$x$:$A$,$Q[x,y]$\}}.  It denotes the set {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
  Replace($A$,$\lambda x\,y.Q$[x,y])} consisting of all $y$ such that there
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
exists $x\in A$ satisfying~$Q[x,y]$.  The Replacement Axiom has the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
condition that $Q$ must be single-valued over~$A$: for all~$x\in A$ there
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
exists at most one $y$ satisfying~$Q[x,y]$.  A single-valued binary
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
predicate is also called a {\bf class function}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
The constant \ttindexbold{RepFun} expresses a special case of replacement,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
where $Q[x,y]$ has the form $y=b[x]$.  Such a $Q$ is trivially
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
single-valued, since it is just the graph of the meta-level
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
function~$\lambda x.b[x]$.  The syntax is \hbox{\tt\{$b[x]$.$x$:$A$\}},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
denoting set {\tt RepFun($A$,$\lambda x.b[x]$)} of all $b[x]$ for~$x\in A$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
This is analogous to the \ML{} functional {\tt map}, since it applies a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
function to every element of a set.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
\indexbold{*INT}\indexbold{*UN}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
General unions and intersections of families, namely $\bigcup@{x\in A}B[x]$ and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
$\bigcap@{x\in A}B[x]$, are written \hbox{\tt UN $x$:$A$.$B[x]$} and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
\hbox{\tt INT $x$:$A$.$B[x]$}.  Their meaning is expressed using {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
RepFun} as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
\[ \bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
   \bigcap(\{B[x]. x\in A\}). 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
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
   283
constructed in set theory, where $B[x]$ is a family of sets over~$A$.  They
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
This is similar to the situation in Constructive Type Theory (set theory
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
has ``dependent sets'') and calls for similar syntactic conventions.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
constants~\ttindexbold{Sigma} and~\ttindexbold{Pi} construct general sums and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
products.  Instead of {\tt Sigma($A$,$B$)} and {\tt Pi($A$,$B$)} we may write
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
\hbox{\tt SUM $x$:$A$.$B[x]$} and \hbox{\tt PROD $x$:$A$.$B[x]$}.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
\indexbold{*SUM}\indexbold{*PROD}%
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$->$B$} abbreviate
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
general sums and products over a constant family.\footnote{Unlike normal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
infix operators, {\tt*} and {\tt->} merely define abbreviations; there are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
no constants~{\tt op~*} and~\hbox{\tt op~->}.} Isabelle accepts these
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
abbreviations in parsing and uses them whenever possible for printing.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
\indexbold{*THE} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
As mentioned above, whenever the axioms assert the existence and uniqueness
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
of a set, Isabelle's set theory declares a constant for that set.  These
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
constants can express the {\bf definite description} operator~$\iota
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
x.P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
Since all terms in {\ZF} denote something, a description is always
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
meaningful, but we do not know its value unless $P[x]$ defines it uniquely.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
Using the constant~\ttindexbold{The}, we may write descriptions as {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
  The($\lambda x.P[x]$)} or use the syntax \hbox{\tt THE $x$.$P[x]$}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
\indexbold{*lam}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
Function sets may be written in $\lambda$-notation; $\lambda x\in A.b[x]$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
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
   310
this to be a set, the function's domain~$A$ must be given.  Using the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
constant~\ttindexbold{Lambda}, we may express function sets as {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
Lambda($A$,$\lambda x.b[x]$)} or use the syntax \hbox{\tt lam $x$:$A$.$b[x]$}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
Isabelle's set theory defines two {\bf bounded quantifiers}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
\begin{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
   \forall x\in A.P[x] &\hbox{which abbreviates}& \forall x. x\in A\imp P[x] \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
   \exists x\in A.P[x] &\hbox{which abbreviates}& \exists x. x\in A\conj P[x]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
\end{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
The constants~\ttindexbold{Ball} and~\ttindexbold{Bex} are defined
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
accordingly.  Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
write
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
\hbox{\tt ALL $x$:$A$.$P[x]$} and \hbox{\tt EX $x$:$A$.$P[x]$}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
%%%% zf.thy
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
\idx{Ball_def}           Ball(A,P) == ALL x. x:A --> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
\idx{Bex_def}            Bex(A,P)  == EX x. x:A & P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
\idx{subset_def}         A <= B  == ALL x:A. x:B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
\idx{extension}          A = B  <->  A <= B & B <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
\idx{union_iff}          A : Union(C) <-> (EX B:C. A:B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
\idx{power_set}          A : Pow(B) <-> A <= B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
\idx{foundation}         A=0 | (EX x:A. ALL y:x. ~ y:A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
\idx{replacement}        (ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
                   b : PrimReplace(A,P) <-> (EX x:A. P(x,b))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
\subcaption{The Zermelo-Fraenkel Axioms}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
\idx{Replace_def}  Replace(A,P) == 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
                   PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
\idx{RepFun_def}   RepFun(A,f)  == \{y . x:A, y=f(x)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
\idx{the_def}      The(P)       == Union(\{y . x:\{0\}, P(y)\})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
\idx{if_def}       if(P,a,b)    == THE z. P & z=a | ~P & z=b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
\idx{Collect_def}  Collect(A,P) == \{y . x:A, x=y & P(x)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
\idx{Upair_def}    Upair(a,b)   == 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
                 \{y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
\subcaption{Consequences of replacement}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
\idx{Inter_def}    Inter(A) == \{ x:Union(A) . ALL y:A. x:y\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
\idx{Un_def}       A Un  B  == Union(Upair(A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
\idx{Int_def}      A Int B  == Inter(Upair(A,B))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
\idx{Diff_def}     A - B    == \{ x:A . ~(x:B) \}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
\subcaption{Union, intersection, difference}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
\idx{cons_def}     cons(a,A) == Upair(a,a) Un A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
\idx{succ_def}     succ(i) == cons(i,i)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
\idx{infinity}     0:Inf & (ALL y:Inf. succ(y): Inf)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
\subcaption{Finite and infinite sets}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
\caption{Rules and axioms of {\ZF}} \label{ZF-rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
\idx{Pair_def}       <a,b>      == \{\{a,a\}, \{a,b\}\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
\idx{split_def}      split(p,c) == THE y. EX a b. p=<a,b> & y=c(a,b)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
\idx{fst_def}        fst(A)     == split(p, %x y.x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
\idx{snd_def}        snd(A)     == split(p, %x y.y)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
\idx{Sigma_def}      Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
\subcaption{Ordered pairs and Cartesian products}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
\idx{converse_def}   converse(r) == \{z. w:r, EX x y. w=<x,y> & z=<y,x>\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
\idx{domain_def}     domain(r)   == \{x. w:r, EX y. w=<x,y>\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
\idx{range_def}      range(r)    == domain(converse(r))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
\idx{field_def}      field(r)    == domain(r) Un range(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
\idx{image_def}      r `` A      == \{y : range(r) . EX x:A. <x,y> : r\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
\idx{vimage_def}     r -`` A     == converse(r)``A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
\subcaption{Operations on relations}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
\idx{lam_def}    Lambda(A,b) == \{<x,b(x)> . x:A\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
\idx{apply_def}  f`a         == THE y. <a,y> : f
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
\idx{Pi_def}     Pi(A,B) == \{f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
\idx{restrict_def}   restrict(f,A) == lam x:A.f`x
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
\subcaption{Functions and general product}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   390
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
\caption{Further definitions of {\ZF}} \label{ZF-defs}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
%%%% zf.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
\idx{ballI}       [| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
\idx{bspec}       [| ALL x:A. P(x);  x: A |] ==> P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
\idx{ballE}       [| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
\idx{ball_cong}   [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
            (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
\idx{bexI}        [| P(x);  x: A |] ==> EX x:A. P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
\idx{bexCI}       [| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A.P(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
\idx{bexE}        [| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q |] ==> Q
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
\idx{bex_cong}    [| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
            (EX x:A. P(x)) <-> (EX x:A'. P'(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
\subcaption{Bounded quantifiers}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
\idx{subsetI}       (!!x.x:A ==> x:B) ==> A <= B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
\idx{subsetD}       [| A <= B;  c:A |] ==> c:B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
\idx{subsetCE}      [| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
\idx{subset_refl}   A <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
\idx{subset_trans}  [| A<=B;  B<=C |] ==> A<=C
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
\idx{equalityI}     [| A <= B;  B <= A |] ==> A = B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
\idx{equalityD1}    A = B ==> A<=B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
\idx{equalityD2}    A = B ==> B<=A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
\idx{equalityE}     [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
\subcaption{Subsets and extensionality}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
\idx{emptyE}          a:0 ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
\idx{empty_subsetI}   0 <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
\idx{equals0I}        [| !!y. y:A ==> False |] ==> A=0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
\idx{equals0D}        [| A=0;  a:A |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
\idx{PowI}            A <= B ==> A : Pow(B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
\idx{PowD}            A : Pow(B)  ==>  A<=B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
\subcaption{The empty set; power sets}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
\caption{Basic derived rules for {\ZF}} \label{ZF-lemmas1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
\idx{ReplaceI}      [| x: A;  P(x,b);  !!y. P(x,y) ==> y=b |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
              b : \{y. x:A, P(x,y)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
\idx{ReplaceE}      [| b : \{y. x:A, P(x,y)\};  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
                 !!x. [| x: A;  P(x,b);  ALL y. P(x,y)-->y=b |] ==> R 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   447
              |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
\idx{RepFunI}       [| a : A |] ==> f(a) : \{f(x). x:A\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
\idx{RepFunE}       [| b : \{f(x). x:A\};  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
                 !!x.[| x:A;  b=f(x) |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
\idx{separation}     a : \{x:A. P(x)\} <-> a:A & P(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
\idx{CollectI}       [| a:A;  P(a) |] ==> a : \{x:A. P(x)\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
\idx{CollectE}       [| a : \{x:A. P(x)\};  [| a:A; P(a) |] ==> R |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
\idx{CollectD1}      a : \{x:A. P(x)\} ==> a:A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
\idx{CollectD2}      a : \{x:A. P(x)\} ==> P(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
\caption{Replacement and separation} \label{ZF-lemmas2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
\idx{UnionI}    [| B: C;  A: B |] ==> A: Union(C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   466
\idx{UnionE}    [| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
\idx{InterI}    [| !!x. x: C ==> A: x;  c:C |] ==> A : Inter(C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
\idx{InterD}    [| A : Inter(C);  B : C |] ==> A : B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
\idx{InterE}    [| A : Inter(C);  A:B ==> R;  ~ B:C ==> R |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
\idx{UN_I}      [| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
\idx{UN_E}      [| b : (UN x:A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
          |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
\idx{INT_I}     [| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
\idx{INT_E}     [| b : (INT x:A. B(x));  a: A |] ==> b : B(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   479
\caption{General Union and Intersection} \label{ZF-lemmas3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   480
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
\section{The Zermelo-Fraenkel axioms}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
The axioms appear in Figure~\ref{ZF-rules}.  They resemble those
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   485
presented by Suppes~\cite{suppes72}.  Most of the theory consists of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
definitions.  In particular, bounded quantifiers and the subset relation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
appear in other axioms.  Object-level quantifiers and implications have
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
been replaced by meta-level ones wherever possible, to simplify use of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
axioms.  See the file \ttindexbold{ZF/zf.thy} for details.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
The traditional replacement axiom asserts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
\[ y \in {\tt PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
subject to the condition that $P(x,y)$ is single-valued for all~$x\in A$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
The Isabelle theory defines \ttindex{Replace} to apply
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
\ttindexbold{PrimReplace} to the single-valued part of~$P$, namely
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
\[ (\exists!z.P(x,z)) \conj P(x,y). \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
Thus $y\in {\tt Replace}(A,P)$ if and only if there is some~$x$ such that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
$P(x,-)$ holds uniquely for~$y$.  Because the equivalence is unconditional,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
{\tt Replace} is much easier to use than {\tt PrimReplace}; it defines the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
same set, if $P(x,y)$ is single-valued.  The nice syntax for replacement
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
expands to {\tt Replace}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
Other consequences of replacement include functional replacement
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
(\ttindexbold{RepFun}) and definite descriptions (\ttindexbold{The}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   505
Axioms for separation (\ttindexbold{Collect}) and unordered pairs
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   506
(\ttindexbold{Upair}) are traditionally assumed, but they actually follow
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
from replacement~\cite[pages 237--8]{suppes72}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
The definitions of general intersection, etc., are straightforward.  Note
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
the definition of \ttindex{cons}, which underlies the finite set notation.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
The axiom of infinity gives us a set that contains~0 and is closed under
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
successor (\ttindexbold{succ}).  Although this set is not uniquely defined,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
the theory names it (\ttindexbold{Inf}) in order to simplify the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
construction of the natural numbers.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
					     
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
Further definitions appear in Figure~\ref{ZF-defs}.  Ordered pairs are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$.  Recall
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
that \ttindexbold{Sigma}$(A,B)$ generalizes the Cartesian product of two
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
sets.  It is defined to be the union of all singleton sets
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
$\{\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
   521
general union.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
The projections involve definite descriptions.  The \ttindex{split}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
operation is like the similar operation in Martin-L\"of Type Theory, and is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
often easier to use than \ttindex{fst} and~\ttindex{snd}.  It is defined
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
using a description for convenience, but could equivalently be defined by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   527
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
split(p,c) == c(fst(p),snd(p))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
\end{ttbox}  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
Operations on relations include converse, domain, range, and image.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
set ${\tt Pi}(A,B)$ generalizes the space of functions between two sets.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
Note the simple definitions of $\lambda$-abstraction (using
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
\ttindex{RepFun}) and application (using a definite description).  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
function \ttindex{restrict}$(f,A)$ has the same values as~$f$, but only
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
over the domain~$A$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
No axiom of choice is provided.  It is traditional to include this axiom
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   538
only where it is needed --- mainly in the theory of cardinal numbers, which
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   539
Isabelle does not formalize at present.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   540
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   542
\section{From basic lemmas to function spaces}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
Faced with so many definitions, it is essential to prove lemmas.  Even
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   544
trivial theorems like $A\inter B=B\inter A$ would be difficult to prove
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   545
from the definitions alone.  Isabelle's set theory derives many rules using
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   546
a natural deduction style.  Ideally, a natural deduction rule should
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   547
introduce or eliminate just one operator, but this is not always practical.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   548
For most operators, we may forget its definition and use its derived rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
instead.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
\subsection{Fundamental lemmas}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   552
Figure~\ref{ZF-lemmas1} presents the derived rules for the most basic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
operators.  The rules for the bounded quantifiers resemble those for the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   554
ordinary quantifiers, but note that \ttindex{BallE} uses a negated
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   555
assumption in the style of Isabelle's classical module.  The congruence rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   556
\ttindex{ball_cong} and \ttindex{bex_cong} are required by Isabelle's
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   557
simplifier, but have few other uses.  Congruence rules must be specially
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
derived for all binding operators, and henceforth will not be shown.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   560
Figure~\ref{ZF-lemmas1} also shows rules for the subset and equality
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   561
relations (proof by extensionality), and rules about the empty set and the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   562
power set operator.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   564
Figure~\ref{ZF-lemmas2} presents rules for replacement and separation.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   565
The rules for \ttindex{Replace} and \ttindex{RepFun} are much simpler than
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
comparable rules for {\tt PrimReplace} would be.  The principle of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   567
separation is proved explicitly, although most proofs should use the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   568
natural deduction rules for \ttindex{Collect}.  The elimination rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
\ttindex{CollectE} is equivalent to the two destruction rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
\ttindex{CollectD1} and \ttindex{CollectD2}, but each rule is suited to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
particular circumstances.  Although too many rules can be confusing, there
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   572
is no reason to aim for a minimal set of rules.  See the file
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   573
\ttindexbold{ZF/zf.ML} for a complete listing.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   574
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   575
Figure~\ref{ZF-lemmas3} presents rules for general union and intersection.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   576
The empty intersection should be undefined.  We cannot have
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   577
$\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set.  All
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   578
expressions denote something in {\ZF} set theory; the definition of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   579
intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   580
arbitrary.  The rule \ttindexbold{InterI} must have a premise to exclude
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   581
the empty intersection.  Some of the laws governing intersections require
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
similar premises.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   583
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   584
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   585
%%% upair.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   586
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   587
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   588
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   589
\idx{pairing}      a:Upair(b,c) <-> (a=b | a=c)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   590
\idx{UpairI1}      a : Upair(a,b)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   591
\idx{UpairI2}      b : Upair(a,b)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   592
\idx{UpairE}       [| a : Upair(b,c);  a = b ==> P;  a = c ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   593
\subcaption{Unordered pairs}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   595
\idx{UnI1}         c : A ==> c : A Un B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   596
\idx{UnI2}         c : B ==> c : A Un B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   597
\idx{UnCI}         (~c : B ==> c : A) ==> c : A Un B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   598
\idx{UnE}          [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   599
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   600
\idx{IntI}         [| c : A;  c : B |] ==> c : A Int B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   601
\idx{IntD1}        c : A Int B ==> c : A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   602
\idx{IntD2}        c : A Int B ==> c : B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   603
\idx{IntE}         [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   604
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   605
\idx{DiffI}        [| c : A;  ~ c : B |] ==> c : A - B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   606
\idx{DiffD1}       c : A - B ==> c : A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   607
\idx{DiffD2}       [| c : A - B;  c : B |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   608
\idx{DiffE}        [| c : A - B;  [| c:A; ~ c:B |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   609
\subcaption{Union, intersection, difference}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   610
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
\caption{Unordered pairs and their consequences} \label{ZF-upair1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   612
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   613
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   614
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   615
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   616
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   617
\idx{consI1}       a : cons(a,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   618
\idx{consI2}       a : B ==> a : cons(b,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   619
\idx{consCI}       (~ a:B ==> a=b) ==> a: cons(b,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   620
\idx{consE}        [| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   621
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   622
\idx{singletonI}   a : \{a\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   623
\idx{singletonE}   [| a : \{b\}; a=b ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   624
\subcaption{Finite and singleton sets}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   625
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   626
\idx{succI1}       i : succ(i)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   627
\idx{succI2}       i : j ==> i : succ(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   628
\idx{succCI}       (~ i:j ==> i=j) ==> i: succ(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   629
\idx{succE}        [| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   630
\idx{succ_neq_0}   [| succ(n)=0 |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   631
\idx{succ_inject}  succ(m) = succ(n) ==> m=n
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   632
\subcaption{The successor function}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   633
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   634
\idx{the_equality}     [| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   635
\idx{theI}             EX! x. P(x) ==> P(THE x. P(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   636
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   637
\idx{if_P}             P ==> if(P,a,b) = a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   638
\idx{if_not_P}        ~P ==> if(P,a,b) = b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   639
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   640
\idx{mem_anti_sym}     [| a:b;  b:a |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   641
\idx{mem_anti_refl}    a:a ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   642
\subcaption{Descriptions; non-circularity}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   643
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   644
\caption{Finite sets and their consequences} \label{ZF-upair2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   645
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   646
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   647
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   648
\subsection{Unordered pairs and finite sets}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   649
Figure~\ref{ZF-upair1} presents the principle of unordered pairing, along
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   650
with its derived rules.  Binary union and intersection are defined in terms
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   651
of ordered pairs, and set difference is included for completeness.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   652
rule \ttindexbold{UnCI} is useful for classical reasoning about unions,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   653
like {\tt disjCI}\@; it supersedes \ttindexbold{UnI1} and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   654
\ttindexbold{UnI2}, but these rules are often easier to work with.  For
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   655
intersection and difference we have both elimination and destruction rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   656
Again, there is no reason to provide a minimal rule set.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   657
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   658
Figure~\ref{ZF-upair2} is concerned with finite sets.  It presents rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   659
for~\ttindex{cons}, the finite set constructor, and rules for singleton
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   660
sets.  Because the successor function is defined in terms of~{\tt cons},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   661
its derived rules appear here.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   662
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
Definite descriptions (\ttindex{THE}) are defined in terms of the singleton
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   664
set $\{0\}$, but their derived rules fortunately hide this.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   665
rule~\ttindex{theI} can be difficult to apply, because $\Var{P}$ must be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   666
instantiated correctly.  However, \ttindex{the_equality} does not have this
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   667
problem and the files contain many examples of its use.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   668
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   669
Finally, the impossibility of having both $a\in b$ and $b\in a$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   670
(\ttindex{mem_anti_sym}) is proved by applying the axiom of foundation to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   671
the set $\{a,b\}$.  The impossibility of $a\in a$ is a trivial consequence.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   672
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   673
See the file \ttindexbold{ZF/upair.ML} for full details.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   674
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   675
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   676
%%% subset.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   677
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   678
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   679
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   680
\idx{Union_upper}       B:A ==> B <= Union(A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
\idx{Union_least}       [| !!x. x:A ==> x<=C |] ==> Union(A) <= C
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   683
\idx{Inter_lower}       B:A ==> Inter(A) <= B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   684
\idx{Inter_greatest}    [| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   685
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   686
\idx{Un_upper1}         A <= A Un B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   687
\idx{Un_upper2}         B <= A Un B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   688
\idx{Un_least}          [| A<=C;  B<=C |] ==> A Un B <= C
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   689
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   690
\idx{Int_lower1}        A Int B <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   691
\idx{Int_lower2}        A Int B <= B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   692
\idx{Int_greatest}      [| C<=A;  C<=B |] ==> C <= A Int B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   693
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   694
\idx{Diff_subset}       A-B <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   695
\idx{Diff_contains}     [| C<=A;  C Int B = 0 |] ==> C <= A-B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   696
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   697
\idx{Collect_subset}    Collect(A,P) <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   698
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   699
\caption{Subset and lattice properties} \label{ZF-subset}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   700
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   701
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   702
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   703
\subsection{Subset and lattice properties}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   704
Figure~\ref{ZF-subset} shows that the subset relation is a complete
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   705
lattice.  Unions form least upper bounds; non-empty intersections form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   706
greatest lower bounds.  A few other laws involving subsets are included.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   707
See the file \ttindexbold{ZF/subset.ML}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   708
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   709
%%% pair.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   710
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   711
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   712
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   713
\idx{Pair_inject1}    <a,b> = <c,d> ==> a=c
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   714
\idx{Pair_inject2}    <a,b> = <c,d> ==> b=d
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   715
\idx{Pair_inject}     [| <a,b> = <c,d>;  [| a=c; b=d |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   716
\idx{Pair_neq_0}      <a,b>=0 ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   717
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   718
\idx{fst}       fst(<a,b>) = a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   719
\idx{snd}       snd(<a,b>) = b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   720
\idx{split}     split(<a,b>, %x y.c(x,y)) = c(a,b)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   721
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   722
\idx{SigmaI}    [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   723
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   724
\idx{SigmaE}    [| c: Sigma(A,B);  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   725
             !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   726
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   727
\idx{SigmaE2}   [| <a,b> : Sigma(A,B);    
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   728
             [| a:A;  b:B(a) |] ==> P   |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   729
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   730
\caption{Ordered pairs; projections; general sums} \label{ZF-pair}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   731
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   732
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   733
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   734
\subsection{Ordered pairs}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   735
Figure~\ref{ZF-pair} presents the rules governing ordered pairs,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   736
projections and general sums.  File \ttindexbold{ZF/pair.ML} contains the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   737
full (and tedious) proof that $\{\{a\},\{a,b\}\}$ functions as an ordered
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   738
pair.  This property is expressed as two destruction rules,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   739
\ttindexbold{Pair_inject1} and \ttindexbold{Pair_inject2}, and equivalently
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   740
as the elimination rule \ttindexbold{Pair_inject}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   741
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   742
Note the rule \ttindexbold{Pair_neq_0}, which asserts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   743
$\pair{a,b}\neq\emptyset$.  This is no arbitrary property of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   744
$\{\{a\},\{a,b\}\}$, but one that we can reasonably expect to hold for any
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   745
encoding of ordered pairs.  It turns out to be useful for constructing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   746
Lisp-style S-expressions in set theory.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   747
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   748
The natural deduction rules \ttindexbold{SigmaI} and \ttindexbold{SigmaE}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   749
assert that \ttindex{Sigma}$(A,B)$ consists of all pairs of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   750
$\pair{x,y}$, for $x\in A$ and $y\in B(x)$.  The rule \ttindexbold{SigmaE2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   751
merely states that $\pair{a,b}\in {\tt Sigma}(A,B)$ implies $a\in A$ and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   752
$b\in B(a)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   753
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   754
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   755
%%% domrange.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   756
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   757
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   758
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   759
\idx{domainI}        <a,b>: r ==> a : domain(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   760
\idx{domainE}        [| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   761
\idx{domain_subset}  domain(Sigma(A,B)) <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   762
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   763
\idx{rangeI}         <a,b>: r ==> b : range(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   764
\idx{rangeE}         [| b : range(r);  !!x. <x,b>: r ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   765
\idx{range_subset}   range(A*B) <= B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   766
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   767
\idx{fieldI1}        <a,b>: r ==> a : field(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   768
\idx{fieldI2}        <a,b>: r ==> b : field(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   769
\idx{fieldCI}        (~ <c,a>:r ==> <a,b>: r) ==> a : field(r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   770
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   771
\idx{fieldE}         [| a : field(r);  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   772
                  !!x. <a,x>: r ==> P;  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   773
                  !!x. <x,a>: r ==> P      
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   774
               |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   775
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   776
\idx{field_subset}   field(A*A) <= A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   777
\subcaption{Domain, range and field of a Relation}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   778
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   779
\idx{imageI}         [| <a,b>: r;  a:A |] ==> b : r``A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   780
\idx{imageE}         [| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   781
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   782
\idx{vimageI}        [| <a,b>: r;  b:B |] ==> a : r-``B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   783
\idx{vimageE}        [| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   784
\subcaption{Image and inverse image}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   785
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   786
\caption{Relations} \label{ZF-domrange}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   787
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   788
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   789
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   790
\subsection{Relations}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   791
Figure~\ref{ZF-domrange} presents rules involving relations, which are sets
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   792
of ordered pairs.  The converse of a relation~$r$ is the set of all pairs
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   793
$\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   794
{\ttindex{converse}$(r)$} is its inverse.  The rules for the domain
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   795
operation, \ttindex{domainI} and~\ttindex{domainE}, assert that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   796
\ttindex{domain}$(r)$ consists of every element~$a$ such that $r$ contains
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   797
some pair of the form~$\pair{x,y}$.  The range operation is similar, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   798
the field of a relation is merely the union of its domain and range.  Note
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   799
that image and inverse image are generalizations of range and domain,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   800
respectively.  See the file
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   801
\ttindexbold{ZF/domrange.ML} for derivations of the rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   802
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   803
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   804
%%% func.ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   805
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   806
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   807
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   808
\idx{fun_is_rel}      f: Pi(A,B) ==> f <= Sigma(A,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   809
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   810
\idx{apply_equality}  [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   811
\idx{apply_equality2} [| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   812
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   813
\idx{apply_type}      [| f: Pi(A,B);  a:A |] ==> f`a : B(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   814
\idx{apply_Pair}      [| f: Pi(A,B);  a:A |] ==> <a,f`a>: f
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   815
\idx{apply_iff}       f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   816
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   817
\idx{fun_extension}   [| f : Pi(A,B);  g: Pi(A,D);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   818
                   !!x. x:A ==> f`x = g`x     |] ==> f=g
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   819
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   820
\idx{domain_type}     [| <a,b> : f;  f: Pi(A,B) |] ==> a : A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   821
\idx{range_type}      [| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   822
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   823
\idx{Pi_type}         [| f: A->C;  !!x. x:A ==> f`x: B(x) |] ==> f: Pi(A,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   824
\idx{domain_of_fun}   f: Pi(A,B) ==> domain(f)=A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   825
\idx{range_of_fun}    f: Pi(A,B) ==> f: A->range(f)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   826
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   827
\idx{restrict}   a : A ==> restrict(f,A) ` a = f`a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   828
\idx{restrict_type}   [| !!x. x:A ==> f`x: B(x) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   829
                restrict(f,A) : Pi(A,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   830
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   831
\idx{lamI}       a:A ==> <a,b(a)> : (lam x:A. b(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   832
\idx{lamE}       [| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   833
           |] ==>  P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   834
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   835
\idx{lam_type}   [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   836
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   837
\idx{beta}       a : A ==> (lam x:A.b(x)) ` a = b(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   838
\idx{eta}        f : Pi(A,B) ==> (lam x:A. f`x) = f
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   839
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   840
\idx{lam_theI}   (!!x. x:A ==> EX! y. Q(x,y)) ==> EX h. ALL x:A. Q(x, h`x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   841
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   842
\caption{Functions and $\lambda$-abstraction} \label{ZF-func1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   843
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   844
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   845
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   846
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   847
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   848
\idx{fun_empty}            0: 0->0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   849
\idx{fun_single}           \{<a,b>\} : \{a\} -> \{b\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   850
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   851
\idx{fun_disjoint_Un}      [| f: A->B;  g: C->D;  A Int C = 0  |] ==>  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   852
                     (f Un g) : (A Un C) -> (B Un D)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   853
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   854
\idx{fun_disjoint_apply1}  [| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   855
                     (f Un g)`a = f`a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   856
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   857
\idx{fun_disjoint_apply2}  [| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   858
                     (f Un g)`c = g`c
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   859
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   860
\caption{Constructing functions from smaller sets} \label{ZF-func2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   861
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   862
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   863
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   864
\subsection{Functions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   865
Functions, represented by graphs, are notoriously difficult to reason
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   866
about.  The file \ttindexbold{ZF/func.ML} derives many rules, which overlap
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   867
more than they ought.  One day these rules will be tidied up; this section
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   868
presents only the more important ones.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   869
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   870
Figure~\ref{ZF-func1} presents the basic properties of \ttindex{Pi}$(A,B)$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   871
the generalized function space.  For example, if $f$ is a function and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   872
$\pair{a,b}\in f$, then $f`a=b$ (\ttindex{apply_equality}).  Two functions
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   873
are equal provided they have equal domains and deliver equals results
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   874
(\ttindex{fun_extension}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   875
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   876
By \ttindex{Pi_type}, a function typing of the form $f\in A\to C$ can be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   877
refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   878
family of sets $\{B(x)\}@{x\in A}$.  Conversely, by \ttindex{range_of_fun},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   879
any dependent typing can be flattened to yield a function type of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   880
$A\to C$; here, $C={\tt range}(f)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   881
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   882
Among the laws for $\lambda$-abstraction, \ttindex{lamI} and \ttindex{lamE}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   883
describe the graph of the generated function, while \ttindex{beta} and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   884
\ttindex{eta} are the standard conversions.  We essentially have a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   885
dependently-typed $\lambda$-calculus.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   886
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   887
Figure~\ref{ZF-func2} presents some rules that can be used to construct
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   888
functions explicitly.  We start with functions consisting of at most one
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   889
pair, and may form the union of two functions provided their domains are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   890
disjoint.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   891
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   892
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   893
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   894
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   895
\begin{tabular}{rrr} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   896
  \it name    	&\it meta-type 	& \it description \\ 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   897
  \idx{id}	& $i$		& identity function \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   898
  \idx{inj}	& $[i,i]\To i$	& injective function space\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   899
  \idx{surj}	& $[i,i]\To i$	& surjective function space\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   900
  \idx{bij}	& $[i,i]\To i$	& bijective function space
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   901
	\\[1ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   902
  \idx{1}	& $i$     	& $\{\emptyset\}$	\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   903
  \idx{bool}	& $i$		& the set $\{\emptyset,1\}$	\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   904
  \idx{cond}	& $[i,i,i]\To i$	& conditional for {\tt bool}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   905
	\\[1ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   906
  \idx{Inl}~~\idx{Inr}	& $i\To i$	& injections\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   907
  \idx{case}	& $[i,i\To i,i\To i]\To i$	& conditional for $+$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   908
	\\[1ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   909
  \idx{nat}	& $i$		& set of natural numbers \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   910
  \idx{nat_case}& $[i,i,i\To i]\To i$	& conditional for $nat$\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   911
  \idx{rec}	& $[i,i,[i,i]\To i]\To i$ & recursor for $nat$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   912
	\\[1ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   913
  \idx{list}	& $i\To i$ 	& lists over some set\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   914
  \idx{list_case} & $[i, i, [i,i]\To i] \To i$	& conditional for $list(A)$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   915
  \idx{list_rec} & $[i, i, [i,i,i]\To i] \To i$	& recursor for $list(A)$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   916
  \idx{map}	& $[i\To i, i] \To i$ 	& mapping functional\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   917
  \idx{length}	& $i\To i$ 		& length of a list\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   918
  \idx{rev}	& $i\To i$ 		& reverse of a list\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   919
  \idx{flat}	& $i\To i$ 		& flatting a list of lists\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   920
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   921
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   922
\subcaption{Constants}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   923
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   924
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   925
\indexbold{*"+}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   926
\index{#*@{\tt\#*}|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   927
\index{*div|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   928
\index{*mod|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   929
\index{#+@{\tt\#+}|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   930
\index{#-@{\tt\#-}|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   931
\begin{tabular}{rrrr} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   932
  \idx{O}	& $[i,i]\To i$	&  Right 60	& composition ($\circ$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   933
  \tt +		& $[i,i]\To i$	&  Right 65	& disjoint union \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   934
  \tt \#*	& $[i,i]\To i$	&  Left 70	& multiplication \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   935
  \tt div	& $[i,i]\To i$	&  Left 70	& division\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   936
  \tt mod	& $[i,i]\To i$	&  Left 70	& modulus\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   937
  \tt \#+	& $[i,i]\To i$	&  Left 65	& addition\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   938
  \tt \#-	& $[i,i]\To i$ 	&  Left 65	& subtraction\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   939
  \tt \@	& $[i,i]\To i$	&  Right 60	& append for lists
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   940
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   941
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   942
\subcaption{Infixes}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   943
\caption{Further constants for {\ZF}} \label{ZF-further-constants}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   944
\end{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   945
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   946
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   947
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   948
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   949
\idx{Int_absorb}         A Int A = A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   950
\idx{Int_commute}        A Int B = B Int A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   951
\idx{Int_assoc}          (A Int B) Int C  =  A Int (B Int C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   952
\idx{Int_Un_distrib}     (A Un B) Int C  =  (A Int C) Un (B Int C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   953
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   954
\idx{Un_absorb}          A Un A = A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   955
\idx{Un_commute}         A Un B = B Un A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   956
\idx{Un_assoc}           (A Un B) Un C  =  A Un (B Un C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   957
\idx{Un_Int_distrib}     (A Int B) Un C  =  (A Un C) Int (B Un C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   958
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   959
\idx{Diff_cancel}        A-A = 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   960
\idx{Diff_disjoint}      A Int (B-A) = 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   961
\idx{Diff_partition}     A<=B ==> A Un (B-A) = B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   962
\idx{double_complement}  [| A<=B; B<= C |] ==> (B - (C-A)) = A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   963
\idx{Diff_Un}            A - (B Un C) = (A-B) Int (A-C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   964
\idx{Diff_Int}           A - (B Int C) = (A-B) Un (A-C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   965
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   966
\idx{Union_Un_distrib}   Union(A Un B) = Union(A) Un Union(B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   967
\idx{Inter_Un_distrib}   [| a:A;  b:B |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   968
                   Inter(A Un B) = Inter(A) Int Inter(B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   969
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   970
\idx{Int_Union_RepFun}   A Int Union(B) = (UN C:B. A Int C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   971
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   972
\idx{Un_Inter_RepFun}    b:B ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   973
                   A Un Inter(B) = (INT C:B. A Un C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   974
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   975
\idx{SUM_Un_distrib1}    (SUM x:A Un B. C(x)) = 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   976
                   (SUM x:A. C(x)) Un (SUM x:B. C(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   977
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   978
\idx{SUM_Un_distrib2}    (SUM x:C. A(x) Un B(x)) =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   979
                   (SUM x:C. A(x))  Un  (SUM x:C. B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   980
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   981
\idx{SUM_Int_distrib1}   (SUM x:A Int B. C(x)) =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   982
                   (SUM x:A. C(x)) Int (SUM x:B. C(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   983
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   984
\idx{SUM_Int_distrib2}   (SUM x:C. A(x) Int B(x)) =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   985
                   (SUM x:C. A(x)) Int (SUM x:C. B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   986
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   987
\caption{Equalities} \label{zf-equalities}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   988
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   989
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   990
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   991
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   992
\idx{comp_def}  r O s     == \{xz : domain(s)*range(r) . 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   993
                        EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   994
\idx{id_def}    id(A)     == (lam x:A. x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   995
\idx{inj_def}   inj(A,B)  == \{ f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   996
\idx{surj_def}  surj(A,B) == \{ f: A->B . ALL y:B. EX x:A. f`x=y\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   997
\idx{bij_def}   bij(A,B)  == inj(A,B) Int surj(A,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   998
\subcaption{Definitions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   999
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1000
\idx{left_inverse}     [| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1001
\idx{right_inverse}    [| f: inj(A,B);  b: range(f) |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1002
                 f`(converse(f)`b) = b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1003
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1004
\idx{inj_converse_inj} f: inj(A,B) ==> converse(f): inj(range(f), A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1005
\idx{bij_converse_bij} f: bij(A,B) ==> converse(f): bij(B,A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1006
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1007
\idx{comp_type}        [| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1008
\idx{comp_assoc}       (r O s) O t = r O (s O t)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1009
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1010
\idx{left_comp_id}     r<=A*B ==> id(B) O r = r
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1011
\idx{right_comp_id}    r<=A*B ==> r O id(A) = r
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1012
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1013
\idx{comp_func}        [| g:A->B; f:B->C |] ==> (f O g):A->C
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1014
\idx{comp_func_apply}  [| g:A->B; f:B->C; a:A |] ==> (f O g)`a = f`(g`a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1015
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1016
\idx{comp_inj}         [| g:inj(A,B);  f:inj(B,C)  |] ==> (f O g):inj(A,C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1017
\idx{comp_surj}        [| g:surj(A,B); f:surj(B,C) |] ==> (f O g):surj(A,C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1018
\idx{comp_bij}         [| g:bij(A,B); f:bij(B,C) |] ==> (f O g):bij(A,C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1019
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1020
\idx{left_comp_inverse}     f: inj(A,B) ==> converse(f) O f = id(A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1021
\idx{right_comp_inverse}    f: surj(A,B) ==> f O converse(f) = id(B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1022
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1023
\idx{bij_disjoint_Un}   
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1024
    [| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1025
    (f Un g) : bij(A Un C, B Un D)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1026
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1027
\idx{restrict_bij}  [| f:inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1028
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1029
\caption{Permutations} \label{zf-perm}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1030
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1031
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1032
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1033
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1034
\idx{one_def}        1    == succ(0)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1035
\idx{bool_def}       bool == {0,1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1036
\idx{cond_def}       cond(b,c,d) == if(b=1,c,d)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1037
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1038
\idx{sum_def}        A+B == \{0\}*A Un \{1\}*B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1039
\idx{Inl_def}        Inl(a) == <0,a>
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1040
\idx{Inr_def}        Inr(b) == <1,b>
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1041
\idx{case_def}       case(u,c,d) == split(u, %y z. cond(y, d(z), c(z)))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1042
\subcaption{Definitions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1043
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1044
\idx{bool_1I}        1 : bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1045
\idx{bool_0I}        0 : bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1046
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1047
\idx{boolE}          [| c: bool;  P(1);  P(0) |] ==> P(c)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1048
\idx{cond_1}         cond(1,c,d) = c
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1049
\idx{cond_0}         cond(0,c,d) = d
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1050
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1051
\idx{sum_InlI}       a : A ==> Inl(a) : A+B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1052
\idx{sum_InrI}       b : B ==> Inr(b) : A+B
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1053
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1054
\idx{Inl_inject}     Inl(a)=Inl(b) ==> a=b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1055
\idx{Inr_inject}     Inr(a)=Inr(b) ==> a=b
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1056
\idx{Inl_neq_Inr}    Inl(a)=Inr(b) ==> P
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1057
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1058
\idx{sumE2}   u: A+B ==> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1059
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1060
\idx{case_Inl}       case(Inl(a),c,d) = c(a)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1061
\idx{case_Inr}       case(Inr(b),c,d) = d(b)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1062
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1063
\caption{Booleans and disjoint unions} \label{zf-sum}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1064
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1065
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1066
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1067
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1068
\idx{nat_def}       nat == lfp(lam r: Pow(Inf). \{0\} Un \{succ(x). x:r\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1069
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1070
\idx{nat_case_def}  nat_case(n,a,b) == 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1071
              THE y. n=0 & y=a | (EX x. n=succ(x) & y=b(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1072
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1073
\idx{rec_def}       rec(k,a,b) ==  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1074
              transrec(k, %n f. nat_case(n, a, %m. b(m, f`m)))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1075
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1076
\idx{add_def}       m#+n == rec(m, n, %u v.succ(v))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1077
\idx{diff_def}      m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1078
\idx{mult_def}      m#*n == rec(m, 0, %u v. n #+ v)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1079
\idx{mod_def}       m mod n == transrec(m, %j f. if(j:n, j, f`(j#-n)))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1080
\idx{quo_def}       m div n == transrec(m, %j f. if(j:n, 0, succ(f`(j#-n))))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1081
\subcaption{Definitions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1082
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1083
\idx{nat_0I}        0 : nat
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1084
\idx{nat_succI}     n : nat ==> succ(n) : nat
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1085
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1086
\idx{nat_induct}        
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1087
    [| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1088
    |] ==> P(n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1089
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1090
\idx{nat_case_0}    nat_case(0,a,b) = a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1091
\idx{nat_case_succ} nat_case(succ(m),a,b) = b(m)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1092
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1093
\idx{rec_0}         rec(0,a,b) = a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1094
\idx{rec_succ}      rec(succ(m),a,b) = b(m, rec(m,a,b))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1095
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1096
\idx{mult_type}     [| m:nat;  n:nat |] ==> m #* n : nat
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1097
\idx{mult_0}        0 #* n = 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1098
\idx{mult_succ}     succ(m) #* n = n #+ (m #* n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1099
\idx{mult_commute}  [| m:nat;  n:nat |] ==> m #* n = n #* m
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1100
\idx{add_mult_dist}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1101
    [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1102
\idx{mult_assoc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1103
    [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1105
\idx{mod_quo_equality}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1106
    [| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1107
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1108
\caption{The natural numbers} \label{zf-nat}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1109
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1110
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1111
\begin{figure}\underscoreon %%because @ is used here
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1112
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1113
\idx{list_def}        list(A) == lfp(univ(A), %X. {0} Un A*X)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1114
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1115
\idx{list_case_def}   list_case(l,c,h) ==
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1116
                THE z. l=0 & z=c | (EX x y. l = <x,y> & z=h(x,y))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1117
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1118
\idx{list_rec_def}    list_rec(l,c,h) == 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1119
                Vrec(l, %l g.list_case(l, c, %x xs. h(x, xs, g`xs)))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1120
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1121
\idx{map_def}         map(f,l)  == list_rec(l,  0,  %x xs r. <f(x), r>)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1122
\idx{length_def}      length(l) == list_rec(l,  0,  %x xs r. succ(r))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1123
\idx{app_def}         xs@ys     == list_rec(xs, ys, %x xs r. <x,r>)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1124
\idx{rev_def}         rev(l)    == list_rec(l,  0,  %x xs r. r @ <x,0>)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1125
\idx{flat_def}        flat(ls)  == list_rec(ls, 0,  %l ls r. l @ r)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1126
\subcaption{Definitions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1127
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1128
\idx{list_0I}         0 : list(A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1129
\idx{list_PairI}      [| a: A;  l: list(A) |] ==> <a,l> : list(A)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1130
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1131
\idx{list_induct}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1132
    [| l: list(A);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1133
       P(0);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1134
       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(<x,y>)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1135
    |] ==> P(l)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1136
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1137
\idx{list_case_0}     list_case(0,c,h) = c
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1138
\idx{list_case_Pair}  list_case(<a,l>, c, h) = h(a,l)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1139
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1140
\idx{list_rec_0}      list_rec(0,c,h) = c
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1141
\idx{list_rec_Pair}   list_rec(<a,l>, c, h) = h(a, l, list_rec(l,c,h))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1142
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1143
\idx{map_ident}       l: list(A) ==> map(%u.u, l) = l
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1144
\idx{map_compose}     l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1145
\idx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1146
\idx{map_type}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1147
    [| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1148
\idx{map_flat}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1149
    ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1150
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1151
\caption{Lists} \label{zf-list}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1152
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1153
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1154
\section{Further developments}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1155
The next group of developments is complex and extensive, and only
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1156
highlights can be covered here.  Figure~\ref{ZF-further-constants} lists
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1157
some of the further constants and infixes that are declared in the various
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1158
theory extensions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1159
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1160
Figure~\ref{zf-sum} defines $\{0,1\}$ as a set of booleans, with a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1161
conditional operator.  It also defines the disjoint union of two sets, with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1162
injections and a case analysis operator.  See files
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1163
\ttindexbold{ZF/bool.ML} and \ttindexbold{ZF/sum.ML}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1164
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1165
Monotonicity properties of most of the set-forming operations are proved.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1166
These are useful for applying the Knaster-Tarski Fixedpoint Theorem.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1167
See file \ttindexbold{ZF/mono.ML}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1168
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1169
Figure~\ref{zf-equalities} presents commutative, associative, distributive,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1170
and idempotency laws of union and intersection, along with other equations.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1171
See file \ttindexbold{ZF/equalities.ML}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1172
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1173
Figure~\ref{zf-perm} defines composition and injective, surjective and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1174
bijective function spaces, with proofs of many of their properties.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1175
See file \ttindexbold{ZF/perm.ML}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1176
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1177
Figure~\ref{zf-nat} presents the natural numbers, with induction and a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1178
primitive recursion operator.  See file \ttindexbold{ZF/nat.ML}.  File
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1179
\ttindexbold{ZF/arith.ML} develops arithmetic on the natural numbers.  It
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1180
defines addition, multiplication, subtraction, division, and remainder,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1181
proving the theorem $a \bmod b + (a/b)\times b = a$.  Division and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1182
remainder are defined by repeated subtraction, which requires well-founded
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1183
rather than primitive recursion.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1184
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1185
Figure~\ref{zf-list} presents defines the set of lists over~$A$, ${\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1186
list}(A)$ as the least solution of the equation ${\tt list}(A)\equiv \{0\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1187
\union (A\times{\tt list}(A))$.  Structural induction and recursion are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1188
derived, with some of the usual list functions.  See file
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1189
\ttindexbold{ZF/list.ML}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1190
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1191
The constructions of the natural numbers and lists make use of a suite of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1192
operators for handling recursive definitions.  The developments are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1193
summarized below:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1194
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1195
\item[\ttindexbold{ZF/lfp.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1196
proves the Knaster-Tarski Fixedpoint Theorem in the lattice of subsets of a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1197
set.  The file defines a least fixedpoint operator with corresponding
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1198
induction rules.  These are used repeatedly in the sequel to define sets
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1199
inductively.  As a simple application, the file contains a short proof of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1200
the Schr\"oder-Bernstein Theorem.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1201
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1202
\item[\ttindexbold{ZF/trancl.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1203
defines the transitive closure of a relation (as a least fixedpoint).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1204
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1205
\item[\ttindexbold{ZF/wf.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1206
proves the Well-Founded Recursion Theorem, using an elegant
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1207
approach of Tobias Nipkow.  This theorem permits general recursive
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1208
definitions within set theory.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1209
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1210
\item[\ttindexbold{ZF/ordinal.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1211
defines the notions of transitive set and ordinal number.  It derives
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1212
transfinite induction.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1213
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1214
\item[\ttindexbold{ZF/epsilon.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1215
derives $\epsilon$-induction and $\epsilon$-recursion, which are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1216
generalizations of transfinite induction.  It also defines
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1217
\ttindexbold{rank}$(x)$, which is the least ordinal $\alpha$ such that $x$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1218
is constructed at stage $\alpha$ of the cumulative hierarchy (thus $x\in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1219
V@{\alpha+1}$).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1220
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1221
\item[\ttindexbold{ZF/univ.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1222
defines a ``universe'' ${\tt univ}(A)$, for constructing sets inductively.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1223
This set contains $A$ and the natural numbers.  Vitally, it is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1224
closed under finite products: 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1225
${\tt univ}(A)\times{\tt univ}(A)\subseteq{\tt univ}(A)$.  This file also
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1226
defines set theory's cumulative hierarchy, traditionally written $V@\alpha$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1227
where $\alpha$ is any ordinal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1228
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1229
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1230
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1231
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1232
\begin{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1233
  a\in a 		& \bimp &  \bot\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1234
  a\in \emptyset 	& \bimp &  \bot\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1235
  a \in A \union B 	& \bimp &  a\in A \disj a\in B\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1236
  a \in A \inter B 	& \bimp &  a\in A \conj a\in B\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1237
  a \in A-B 		& \bimp &  a\in A \conj \neg (a\in B)\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1238
  a \in {\tt cons}(b,B) & \bimp &  a=b \disj a\in B\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1239
  i \in {\tt succ}(j) 	& \bimp &  i=j \disj i\in j\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1240
  \pair{a,b}\in {\tt Sigma}(A,B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1241
		  	& \bimp &  a\in A \conj b\in B(a)\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1242
  a \in {\tt Collect}(A,P) 	& \bimp &  a\in A \conj P(a)\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1243
  (\forall x \in A. \top) 	& \bimp &  \top
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1244
\end{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1245
\caption{Rewrite rules for set theory} \label{ZF-simpdata}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1246
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1247
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1248
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1249
\section{Simplification rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1250
{\ZF} does not merely inherit simplification from \FOL, but instantiates
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1251
the rewriting package new.  File \ttindexbold{ZF/simpdata.ML} contains the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1252
details; here is a summary of the key differences:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1253
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1254
\item 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1255
\ttindexbold{mk_rew_rules} is given as a function that can
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1256
strip bounded universal quantifiers from a formula.  For example, $\forall
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1257
x\in A.f(x)=g(x)$ yields the conditional rewrite rule $x\in A \Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1258
f(x)=g(x)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1259
\item
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1260
\ttindexbold{ZF_ss} contains congruence rules for all the operators of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1261
{\ZF}, including the binding operators.  It contains all the conversion
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1262
rules, such as \ttindex{fst} and \ttindex{snd}, as well as the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1263
rewrites shown in Figure~\ref{ZF-simpdata}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1264
\item
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1265
\ttindexbold{FOL_ss} is redeclared with the same {\FOL} rules as the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1266
previous version, so that it may still be used.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1267
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1268
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1269
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1270
\section{The examples directory}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1271
This directory contains further developments in {\ZF} set theory.  Here is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1272
an overview; see the files themselves for more details.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1273
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1274
\item[\ttindexbold{ZF/ex/misc.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1275
contains miscellaneous examples such as Cantor's Theorem and the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1276
``Composition of homomorphisms'' challenge.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1277
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1278
\item[\ttindexbold{ZF/ex/ramsey.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1279
proves the finite exponent 2 version of Ramsey's Theorem.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1280
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1281
\item[\ttindexbold{ZF/ex/bt.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1282
defines the recursive data structure ${\tt bt}(A)$, labelled binary trees.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1283
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1284
\item[\ttindexbold{ZF/ex/sexp.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1285
defines the set of Lisp $S$-expressions over~$A$, ${\tt sexp}(A)$.  These
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1286
are unlabelled binary trees whose leaves contain elements of $(A)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1287
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1288
\item[\ttindexbold{ZF/ex/term.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1289
defines a recursive data structure for terms and term lists.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1290
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1291
\item[\ttindexbold{ZF/ex/simult.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1292
defines primitives for solving mutually recursive equations over sets.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1293
It constructs sets of trees and forests as an example, including induction
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1294
and recursion rules that handle the mutual recursion.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1295
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1296
\item[\ttindexbold{ZF/ex/finite.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1297
inductively defines a finite powerset operator.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1298
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1299
\item[\ttindexbold{ZF/ex/prop-log.ML}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1300
proves soundness and completeness of propositional logic.  This illustrates
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1301
the main forms of induction.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1302
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1303
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1304
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1305
\section{A proof about powersets}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1306
To demonstrate high-level reasoning about subsets, let us prove the equation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1307
${Pow(A)\cap Pow(B)}= Pow(A\cap B)$.  Compared with first-order logic, set
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1308
theory involves a maze of rules, and theorems have many different proofs.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1309
Attempting other proofs of the theorem might be instructive.  This proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1310
exploits the lattice properties of intersection.  It also uses the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1311
monotonicity of the powerset operation, from {\tt ZF/mono.ML}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1312
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1313
\idx{Pow_mono}      A<=B ==> Pow(A) <= Pow(B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1314
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1315
We enter the goal and make the first step, which breaks the equation into
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1316
two inclusions by extensionality:\index{equalityI}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1317
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1318
goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1319
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1320
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1321
{\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1322
by (resolve_tac [equalityI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1323
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1324
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1325
{\out  1. Pow(A Int B) <= Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1326
{\out  2. Pow(A) Int Pow(B) <= Pow(A Int B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1327
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1328
Both inclusions could be tackled straightforwardly using {\tt subsetI}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1329
A shorter proof results from noting that intersection forms the greatest
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1330
lower bound:\index{*Int_greatest}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1331
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1332
by (resolve_tac [Int_greatest] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1333
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1334
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1335
{\out  1. Pow(A Int B) <= Pow(A)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1336
{\out  2. Pow(A Int B) <= Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1337
{\out  3. Pow(A) Int Pow(B) <= Pow(A Int B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1338
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1339
Subgoal~1 follows by applying the monotonicity of {\tt Pow} to $A\inter
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1340
B\subseteq A$; subgoal~2 follows similarly:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1341
\index{*Int_lower1}\index{*Int_lower2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1342
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1343
by (resolve_tac [Int_lower1 RS Pow_mono] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1344
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1345
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1346
{\out  1. Pow(A Int B) <= Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1347
{\out  2. Pow(A) Int Pow(B) <= Pow(A Int B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1348
by (resolve_tac [Int_lower2 RS Pow_mono] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1349
{\out Level 4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1350
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1351
{\out  1. Pow(A) Int Pow(B) <= Pow(A Int B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1352
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1353
We are left with the opposite inclusion, which we tackle in the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1354
straightforward way:\index{*subsetI}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1355
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1356
by (resolve_tac [subsetI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1357
{\out Level 5}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1358
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1359
{\out  1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1360
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1361
The subgoal is to show $x\in {\tt Pow}(A\cap B)$ assuming $x\in{\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1362
Pow}(A)\cap {\tt Pow}(B)$.  Eliminating this assumption produces two
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1363
subgoals, since intersection is like conjunction.\index{*IntE}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1364
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1365
by (eresolve_tac [IntE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1366
{\out Level 6}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1367
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1368
{\out  1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1369
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1370
The next step replaces the {\tt Pow} by the subset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1371
relation~($\subseteq$).\index{*PowI}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1372
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1373
by (resolve_tac [PowI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1374
{\out Level 7}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1375
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1376
{\out  1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1377
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1378
We perform the same replacement in the assumptions:\index{*PowD}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1379
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1380
by (REPEAT (dresolve_tac [PowD] 1));
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1381
{\out Level 8}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1382
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1383
{\out  1. !!x. [| x <= A; x <= B |] ==> x <= A Int B}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1384
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1385
Here, $x$ is a lower bound of $A$ and~$B$, but $A\inter B$ is the greatest
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1386
lower bound:\index{*Int_greatest}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1387
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1388
by (resolve_tac [Int_greatest] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1389
{\out Level 9}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1390
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1391
{\out  1. !!x. [| x <= A; x <= B |] ==> x <= A}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1392
{\out  2. !!x. [| x <= A; x <= B |] ==> x <= B}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1393
by (REPEAT (assume_tac 1));
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1394
{\out Level 10}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1395
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1396
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1397
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1398
We could have performed this proof in one step by applying
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1399
\ttindex{fast_tac} with the classical rule set \ttindex{ZF_cs}.  But we
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1400
must add \ttindex{equalityI} as an introduction rule, since extensionality
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1401
is not used by default:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1402
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1403
choplev 0;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1404
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1405
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1406
{\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1407
by (fast_tac (ZF_cs addIs [equalityI]) 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1408
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1409
{\out Pow(A Int B) = Pow(A) Int Pow(B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1410
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1411
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1412
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1413
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1414
\section{Monotonicity of the union operator}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1415
For another example, we prove that general union is monotonic:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1416
${C\subseteq D}$ implies $\bigcup(C)\subseteq \bigcup(D)$.  To begin, we
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1417
tackle the inclusion using \ttindex{subsetI}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1418
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1419
val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1420
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1421
{\out Union(C) <= Union(D)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1422
{\out  1. Union(C) <= Union(D)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1423
by (resolve_tac [subsetI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1424
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1425
{\out Union(C) <= Union(D)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1426
{\out  1. !!x. x : Union(C) ==> x : Union(D)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1427
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1428
Big union is like an existential quantifier --- the occurrence in the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1429
assumptions must be eliminated early, since it creates parameters.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1430
\index{*UnionE}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1431
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1432
by (eresolve_tac [UnionE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1433
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1434
{\out Union(C) <= Union(D)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1435
{\out  1. !!x B. [| x : B; B : C |] ==> x : Union(D)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1436
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1437
Now we may apply \ttindex{UnionI}, which creates an unknown involving the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1438
parameters.  To show $x\in \bigcup(D)$ it suffices to show that $x$ belongs
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1439
to some element, say~$\Var{B2}(x,B)$, of~$D$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1440
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1441
by (resolve_tac [UnionI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1442
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1443
{\out Union(C) <= Union(D)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1444
{\out  1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1445
{\out  2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1446
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1447
Combining \ttindex{subsetD} with the premise $C\subseteq D$ yields 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1448
$\Var{a}\in C \Imp \Var{a}\in D$, which reduces subgoal~1:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1449
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1450
by (resolve_tac [prem RS subsetD] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1451
{\out Level 4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1452
{\out Union(C) <= Union(D)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1453
{\out  1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1454
{\out  2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1455
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1456
The rest is routine.  Note how~$\Var{B2}(x,B)$ is instantiated.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1457
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1458
by (assume_tac 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1459
{\out Level 5}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1460
{\out Union(C) <= Union(D)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1461
{\out  1. !!x B. [| x : B; B : C |] ==> x : B}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1462
by (assume_tac 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1463
{\out Level 6}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1464
{\out Union(C) <= Union(D)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1465
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1466
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1467
Again, \ttindex{fast_tac} with \ttindex{ZF_cs} can do this proof in one
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1468
step, provided we somehow supply it with~{\tt prem}.  We can either add
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1469
this premise to the assumptions using \ttindex{cut_facts_tac}, or add
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1470
\hbox{\tt prem RS subsetD} to \ttindex{ZF_cs} as an introduction rule.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1471
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1472
The file \ttindex{ZF/equalities.ML} has many similar proofs.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1473
Reasoning about general intersection can be difficult because of its anomalous
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1474
behavior on the empty set.  However, \ttindex{fast_tac} copes well with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1475
these.  Here is a typical example:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1476
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1477
a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C.A(x)) Int (INT x:C.B(x))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1478
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1479
In traditional notation this is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1480
\[ a\in C \,\Imp\, \bigcap@{x\in C} \Bigl(A(x) \inter B(x)\Bigr) =        
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1481
       \Bigl(\bigcap@{x\in C} A(x)\Bigr)  \inter  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1482
       \Bigl(\bigcap@{x\in C} B(x)\Bigr)  \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1483
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1484
\section{Low-level reasoning about functions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1485
The derived rules {\tt lamI}, {\tt lamE}, {\tt lam_type}, {\tt beta}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1486
and {\tt eta} support reasoning about functions in a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1487
$\lambda$-calculus style.  This is generally easier than regarding
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1488
functions as sets of ordered pairs.  But sometimes we must look at the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1489
underlying representation, as in the following proof
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1490
of~\ttindex{fun_disjoint_apply1}.  This states that if $f$ and~$g$ are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1491
functions with disjoint domains~$A$ and~$C$, and if $a\in A$, then
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1492
$(f\union g)`a = f`a$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1493
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1494
val prems = goal ZF.thy
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1495
    "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \ttback
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1496
\ttback    (f Un g)`a = f`a";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1497
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1498
{\out (f Un g) ` a = f ` a}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1499
{\out  1. (f Un g) ` a = f ` a}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1500
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1501
Using \ttindex{apply_equality}, we reduce the equality to reasoning about
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1502
ordered pairs.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1503
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1504
by (resolve_tac [apply_equality] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1505
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1506
{\out (f Un g) ` a = f ` a}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1507
{\out  1. <a,f ` a> : f Un g}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1508
{\out  2. f Un g : (PROD x:?A. ?B(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1509
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1510
We must show that the pair belongs to~$f$ or~$g$; by~\ttindex{UnI1} we
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1511
choose~$f$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1512
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1513
by (resolve_tac [UnI1] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1514
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1515
{\out (f Un g) ` a = f ` a}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1516
{\out  1. <a,f ` a> : f}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1517
{\out  2. f Un g : (PROD x:?A. ?B(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1518
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1519
To show $\pair{a,f`a}\in f$ we use \ttindex{apply_Pair}, which is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1520
essentially the converse of \ttindex{apply_equality}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1521
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1522
by (resolve_tac [apply_Pair] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1523
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1524
{\out (f Un g) ` a = f ` a}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1525
{\out  1. f : (PROD x:?A2. ?B2(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1526
{\out  2. a : ?A2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1527
{\out  3. f Un g : (PROD x:?A. ?B(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1528
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1529
Using the premises $f\in A\to B$ and $a\in A$, we solve the two subgoals
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1530
from \ttindex{apply_Pair}.  Recall that a $\Pi$-set is merely a generalized
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1531
function space, and observe that~{\tt?A2} is instantiated to~{\tt A}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1532
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1533
by (resolve_tac prems 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1534
{\out Level 4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1535
{\out (f Un g) ` a = f ` a}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1536
{\out  1. a : A}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1537
{\out  2. f Un g : (PROD x:?A. ?B(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1538
by (resolve_tac prems 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1539
{\out Level 5}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1540
{\out (f Un g) ` a = f ` a}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1541
{\out  1. f Un g : (PROD x:?A. ?B(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1542
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1543
To construct functions of the form $f\union g$, we apply
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1544
\ttindex{fun_disjoint_Un}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1545
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1546
by (resolve_tac [fun_disjoint_Un] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1547
{\out Level 6}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1548
{\out (f Un g) ` a = f ` a}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1549
{\out  1. f : ?A3 -> ?B3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1550
{\out  2. g : ?C3 -> ?D3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1551
{\out  3. ?A3 Int ?C3 = 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1552
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1553
The remaining subgoals are instances of the premises.  Again, observe how
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1554
unknowns are instantiated:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1555
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1556
by (resolve_tac prems 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1557
{\out Level 7}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1558
{\out (f Un g) ` a = f ` a}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1559
{\out  1. g : ?C3 -> ?D3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1560
{\out  2. A Int ?C3 = 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1561
by (resolve_tac prems 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1562
{\out Level 8}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1563
{\out (f Un g) ` a = f ` a}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1564
{\out  1. A Int C = 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1565
by (resolve_tac prems 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1566
{\out Level 9}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1567
{\out (f Un g) ` a = f ` a}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1568
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1569
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1570
See the files \ttindex{ZF/func.ML} and \ttindex{ZF/wf.ML} for more
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1571
examples of reasoning about functions.