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