doc-src/ZF/ZF.tex
author paulson
Tue, 19 Aug 2003 18:45:48 +0200
changeset 14154 3bc0128e2c74
parent 9836 56b632fd1dcd
child 14158 15bab630ae31
permissions -rw-r--r--
partial conversion to Isar format
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
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
     8
deduction rules, for use with Isabelle's classical reasoner.  Some
6121
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    26
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
    27
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
    28
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
    29
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
    30
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    31
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    32
\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
    33
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
    34
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
    35
  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
    36
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
    37
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
    38
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
    39
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
    40
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    41
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
    42
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
    43
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
    44
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
    45
{\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
    46
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
    47
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
    48
class (let alone a set).
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    49
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    50
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
    51
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
    52
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
    53
$x$ is a set.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    54
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    55
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    56
\begin{figure} \small
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    57
\begin{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    58
\begin{tabular}{rrr} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    59
  \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
    60
  \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
    61
  \cdx{0}       & $i$           & empty set\\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    62
  \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
    63
  \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
    64
  \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
    65
  \cdx{Inf}     & $i$   & infinite set\\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    66
  \cdx{Pow}     & $i\To i$      & powerset\\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    67
  \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
    68
  \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
    69
  \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
    70
  \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
    71
  \cdx{succ}    & $i\To i$      & successor\\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    72
  \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
    73
  \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
    74
  \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
    75
  \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
    76
  \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
    77
  \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
    78
  \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
    79
  \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
    80
  \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
    81
  \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
    82
  \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
    83
  \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
    84
  \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
    85
\end{tabular}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    86
\end{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    87
\subcaption{Constants}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    88
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    89
\begin{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    90
\index{*"`"` symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    91
\index{*"-"`"` symbol}
9836
56b632fd1dcd simplified two index entries, since now ZF is by itself
paulson
parents: 9695
diff changeset
    92
\index{*"` symbol}\index{function applications}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    93
\index{*"- symbol}
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}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    96
\begin{tabular}{rrrr} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    97
  \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
    98
  \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
    99
  \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
   100
  \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
   101
  \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
   102
  \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
   103
  \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
   104
  \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
   105
  \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
   106
\end{tabular}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   107
\end{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   108
\subcaption{Infixes}
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
   109
\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
   110
\end{figure} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   111
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   112
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   113
\section{The syntax of set theory}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   114
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
   115
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
   116
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
   117
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
   118
\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
   119
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
   120
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
   121
Zermelo-Fraenkel set theory.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   122
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
   123
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
   124
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
   125
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
   126
constructs of FOL.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   127
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   128
Local abbreviations can be introduced by a \isa{let} construct whose
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   129
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
   130
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
   131
definition, \tdx{Let_def}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   132
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   133
Apart from \isa{let}, set theory does not use polymorphism.  All terms in
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   134
ZF have type~\tydx{i}, which is the type of individuals and has
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   135
class~\cldx{term}.  The type of first-order formulae, remember, 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   136
is~\tydx{o}.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   137
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   138
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
   139
$A\int B$), set difference ($A-B$), and the subset and membership
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   140
relations.  Note that $a$\verb|~:|$b$ is translated to $\lnot(a\in b)$,
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   141
which is equivalent to  $a\notin b$.  The
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   142
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
   143
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
   144
$\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
   145
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   146
The constant \cdx{Upair} constructs unordered pairs; thus \isa{Upair($A$,$B$)} denotes the set~$\{A,B\}$ and
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   147
\isa{Upair($A$,$A$)} denotes the singleton~$\{A\}$.  General union is
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   148
used to define binary union.  The Isabelle version goes on to define
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   149
the constant
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   150
\cdx{cons}:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   151
\begin{eqnarray*}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   152
   A\cup B              & \equiv &       \bigcup(\isa{Upair}(A,B)) \\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   153
   \isa{cons}(a,B)      & \equiv &        \isa{Upair}(a,a) \un B
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   154
\end{eqnarray*}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   155
The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   156
obvious manner using~\isa{cons} and~$\emptyset$ (the empty set) \isasymin \begin{eqnarray*}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   157
 \{a,b,c\} & \equiv & \isa{cons}(a,\isa{cons}(b,\isa{cons}(c,\emptyset)))
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   158
\end{eqnarray*}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   159
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   160
The constant \cdx{Pair} constructs ordered pairs, as in \isa{Pair($a$,$b$)}.  Ordered pairs may also be written within angle brackets,
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   161
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
   162
abbreviates the nest of pairs\par\nobreak
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   163
\centerline{\isa{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   164
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
   165
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
   166
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
   167
$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
   168
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
   169
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
   170
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   171
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   172
\begin{figure} 
9836
56b632fd1dcd simplified two index entries, since now ZF is by itself
paulson
parents: 9695
diff changeset
   173
\index{lambda abs@$\lambda$-abstractions}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   174
\index{*"-"> symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   175
\index{*"* symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   176
\begin{center} \footnotesize\tt\frenchspacing
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   177
\begin{tabular}{rrr} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   178
  \it external          & \it internal  & \it description \\ 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   179
  $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
   180
  \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
   181
        \rm finite set \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   182
  <$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
   183
        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
   184
        \rm ordered $n$-tuple \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   185
  \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
   186
        \rm separation \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   187
  \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
   188
        \rm replacement \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   189
  \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
   190
        \rm functional replacement \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   191
  \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
   192
        \rm general intersection \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   193
  \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
   194
        \rm general union \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   195
  \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
   196
        \rm general product \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   197
  \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
   198
        \rm general sum \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   199
  $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
   200
        \rm function space \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   201
  $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
   202
        \rm binary product \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   203
  \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
   204
        \rm definite description \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   205
  \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
   206
        \rm $\lambda$-abstraction\\[1ex]
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   207
  \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
   208
        \rm bounded $\forall$ \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   209
  \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
   210
        \rm bounded $\exists$
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   211
\end{tabular}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   212
\end{center}
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
   213
\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
   214
\end{figure} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   215
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   216
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   217
\begin{figure} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   218
\index{*let symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   219
\index{*in symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   220
\dquotes
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   221
\[\begin{array}{rcl}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   222
    term & = & \hbox{expression of type~$i$} \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   223
         & | & "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
   224
         & | & "if"~term~"then"~term~"else"~term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   225
         & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   226
         & | & "< "  term\; ("," term)^* " >"  \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   227
         & | & "{\ttlbrace} " id ":" term " . " formula " {\ttrbrace}" \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   228
         & | & "{\ttlbrace} " id " . " id ":" term ", " formula " {\ttrbrace}" \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   229
         & | & "{\ttlbrace} " term " . " id ":" 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
         & | & term " -`` " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   232
         & | & term " ` " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   233
         & | & term " * " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   234
         & | & term " Int " term \\
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   235
         & | & term " \isasymunion " term \\
6121
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
         & | & "THE~~"  id  " . " formula\\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   239
         & | & "lam~~"  id ":" term " . " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   240
         & | & "INT~~"  id ":" term " . " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   241
         & | & "UN~~~"  id ":" term " . " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   242
         & | & "PROD~"  id ":" term " . " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   243
         & | & "SUM~~"  id ":" term " . " term \\[2ex]
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   244
 formula & = & \hbox{expression of type~$o$} \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   245
         & | & term " : " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   246
         & | & term " \ttilde: " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   247
         & | & term " <= " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   248
         & | & term " = " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   249
         & | & term " \ttilde= " term \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   250
         & | & "\ttilde\ " formula \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   251
         & | & formula " \& " formula \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   252
         & | & formula " | " formula \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   253
         & | & formula " --> " formula \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   254
         & | & formula " <-> " formula \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   255
         & | & "ALL " id ":" term " . " formula \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   256
         & | & "EX~~" id ":" term " . " formula \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   257
         & | & "ALL~" id~id^* " . " formula \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   258
         & | & "EX~~" id~id^* " . " formula \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   259
         & | & "EX!~" id~id^* " . " formula
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   260
  \end{array}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   261
\]
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
   262
\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
   263
\end{figure} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   264
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   265
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   266
\section{Binding operators}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   267
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
   268
  separation}.  The syntax for separation is
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   269
\hbox{\tt\ttlbrace$x$:$A$.\ $P[x]$\ttrbrace}, where $P[x]$ is a formula
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   270
that may contain free occurrences of~$x$.  It abbreviates the set \isa{Collect($A$,$\lambda x. P[x]$)}, which consists of all $x\in A$ that
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   271
satisfy~$P[x]$.  Note that \isa{Collect} is an unfortunate choice of
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   272
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
   273
replacement, called collection.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   274
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   275
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
   276
  replacement}.  The syntax
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   277
\hbox{\tt\ttlbrace$y$.\ $x$:$A$,$Q[x,y]$\ttrbrace} denotes the set 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   278
\isa{Replace($A$,$\lambda x\,y. Q[x,y]$)}, which consists of all~$y$ such
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   279
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
   280
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
   281
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
   282
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
   283
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   284
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
   285
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
   286
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
   287
function~$\lambda x. b[x]$.  The resulting set consists of all $b[x]$
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   288
for~$x\in A$.  This is analogous to the \ML{} functional \isa{map},
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   289
since it applies a function to every element of a set.  The syntax is
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   290
\isa{\ttlbrace$b[x]$.\ $x$:$A$\ttrbrace}, which expands to 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   291
\isa{RepFun($A$,$\lambda x. b[x]$)}.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   292
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   293
\index{*INT symbol}\index{*UN symbol} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   294
General unions and intersections of indexed
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   295
families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$,
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   296
are written \isa{UN $x$:$A$.\ $B[x]$} and \isa{INT $x$:$A$.\ $B[x]$}.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   297
Their meaning is expressed using \isa{RepFun} as
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   298
\[
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   299
\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
   300
\bigcap(\{B[x]. x\in A\}). 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   301
\]
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   302
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
   303
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
   304
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
   305
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
   306
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
   307
constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   308
products.  Instead of \isa{Sigma($A$,$B$)} and \isa{Pi($A$,$B$)} we may
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   309
write 
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   310
\isa{SUM $x$:$A$.\ $B[x]$} and \isa{PROD $x$:$A$.\ $B[x]$}.  
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   311
\index{*SUM symbol}\index{*PROD symbol}%
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   312
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
   313
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
   314
infix operators, {\tt*} and {\tt->} merely define abbreviations; there are
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   315
no constants~\isa{op~*} and~\isa{op~->}.} Isabelle accepts these
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   316
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
   317
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
   318
\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
   319
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
   320
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
   321
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
   322
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
   323
always meaningful, but we do not know its value unless $P[x]$ defines it
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   324
uniquely.  Using the constant~\cdx{The}, we may write descriptions as 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   325
\isa{The($\lambda x. P[x]$)} or use the syntax \isa{THE $x$.\ $P[x]$}.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   326
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   327
\index{*lam symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   328
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
   329
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
   330
this to be a set, the function's domain~$A$ must be given.  Using the
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   331
constant~\cdx{Lambda}, we may express function sets as \isa{Lambda($A$,$\lambda x. b[x]$)} or use the syntax \isa{lam $x$:$A$.\ $b[x]$}.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   332
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   333
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
   334
\begin{eqnarray*}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   335
   \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
   336
   \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
   337
\end{eqnarray*}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   338
The constants~\cdx{Ball} and~\cdx{Bex} are defined
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   339
accordingly.  Instead of \isa{Ball($A$,$P$)} and \isa{Bex($A$,$P$)} we may
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   340
write
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   341
\isa{ALL $x$:$A$.\ $P[x]$} and \isa{EX $x$:$A$.\ $P[x]$}.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   342
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   343
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   344
%%%% ZF.thy
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   345
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   346
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   347
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   348
\tdx{Let_def}:           Let(s, f) == f(s)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   349
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   350
\tdx{Ball_def}:          Ball(A,P) == {\isasymforall}x. x \isasymin A --> P(x)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   351
\tdx{Bex_def}:           Bex(A,P)  == {\isasymexists}x. x \isasymin A & P(x)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   352
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   353
\tdx{subset_def}:        A \isasymsubseteq B  == {\isasymforall}x \isasymin A. x \isasymin B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   354
\tdx{extension}:         A = B  <->  A \isasymsubseteq B & B \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   355
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   356
\tdx{Union_iff}:         A \isasymin Union(C) <-> ({\isasymexists}B \isasymin C. A \isasymin B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   357
\tdx{Pow_iff}:           A \isasymin Pow(B) <-> A \isasymsubseteq B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   358
\tdx{foundation}:        A=0 | ({\isasymexists}x \isasymin A. {\isasymforall}y \isasymin x. y \isasymnotin A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   359
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   360
\tdx{replacement}:       ({\isasymforall}x \isasymin A. {\isasymforall}y z. P(x,y) & P(x,z) --> y=z) ==>
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   361
                   b \isasymin PrimReplace(A,P) <-> ({\isasymexists}x{\isasymin}A. P(x,b))
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   362
\subcaption{The Zermelo-Fraenkel Axioms}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   363
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   364
\tdx{Replace_def}: Replace(A,P) == 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   365
                   PrimReplace(A, \%x y. (\isasymexists!z. P(x,z)) & P(x,y))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   366
\tdx{RepFun_def}:  RepFun(A,f)  == {\ttlbrace}y . x \isasymin A, y=f(x)\ttrbrace
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   367
\tdx{the_def}:     The(P)       == Union({\ttlbrace}y . x \isasymin {\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace})
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   368
\tdx{if_def}:      if(P,a,b)    == THE z. P & z=a | ~P & z=b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   369
\tdx{Collect_def}: Collect(A,P) == {\ttlbrace}y . x \isasymin A, x=y & P(x){\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   370
\tdx{Upair_def}:   Upair(a,b)   == 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   371
               {\ttlbrace}y. x\isasymin{}Pow(Pow(0)), x=0 & y=a | x=Pow(0) & y=b{\ttrbrace}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   372
\subcaption{Consequences of replacement}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   373
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   374
\tdx{Inter_def}:   Inter(A) == {\ttlbrace}x \isasymin Union(A) . {\isasymforall}y \isasymin A. x \isasymin y{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   375
\tdx{Un_def}:      A \isasymunion B  == Union(Upair(A,B))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   376
\tdx{Int_def}:     A Int B  == Inter(Upair(A,B))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   377
\tdx{Diff_def}:    A - B    == {\ttlbrace}x \isasymin A . x \isasymnotin B{\ttrbrace}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   378
\subcaption{Union, intersection, difference}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   379
\end{alltt*}
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
   380
\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
   381
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   382
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   383
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   384
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   385
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   386
\tdx{cons_def}:    cons(a,A) == Upair(a,a) \isasymunion A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   387
\tdx{succ_def}:    succ(i) == cons(i,i)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   388
\tdx{infinity}:    0 \isasymin Inf & ({\isasymforall}y \isasymin Inf. succ(y) \isasymin Inf)
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   389
\subcaption{Finite and infinite sets}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   390
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   391
\tdx{Pair_def}:      <a,b>      == {\ttlbrace}{\ttlbrace}a,a{\ttrbrace}, {\ttlbrace}a,b{\ttrbrace}{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   392
\tdx{split_def}:     split(c,p) == THE y. {\isasymexists}a b. p=<a,b> & y=c(a,b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   393
\tdx{fst_def}:       fst(A)     == split(\%x y. x, p)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   394
\tdx{snd_def}:       snd(A)     == split(\%x y. y, p)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   395
\tdx{Sigma_def}:     Sigma(A,B) == {\isasymUnion}x \isasymin A. {\isasymUnion}y \isasymin B(x). {\ttlbrace}<x,y>{\ttrbrace}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   396
\subcaption{Ordered pairs and Cartesian products}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   397
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   398
\tdx{converse_def}: converse(r) == {\ttlbrace}z. w\isasymin{}r, {\isasymexists}x y. w=<x,y> & z=<y,x>{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   399
\tdx{domain_def}:   domain(r)   == {\ttlbrace}x. w \isasymin r, {\isasymexists}y. w=<x,y>{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   400
\tdx{range_def}:    range(r)    == domain(converse(r))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   401
\tdx{field_def}:    field(r)    == domain(r) \isasymunion range(r)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   402
\tdx{image_def}:    r `` A      == {\ttlbrace}y\isasymin{}range(r) . {\isasymexists}x \isasymin A. <x,y> \isasymin r{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   403
\tdx{vimage_def}:   r -`` A     == converse(r)``A
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   404
\subcaption{Operations on relations}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   405
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   406
\tdx{lam_def}:   Lambda(A,b) == {\ttlbrace}<x,b(x)> . x \isasymin A{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   407
\tdx{apply_def}: f`a         == THE y. <a,y> \isasymin f
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   408
\tdx{Pi_def}: Pi(A,B) == {\ttlbrace}f\isasymin{}Pow(Sigma(A,B)). {\isasymforall}x\isasymin{}A. \isasymexists!y. <x,y>\isasymin{}f{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   409
\tdx{restrict_def}:  restrict(f,A) == lam x \isasymin A. f`x
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   410
\subcaption{Functions and general product}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   411
\end{alltt*}
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
   412
\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
   413
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   414
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   415
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   416
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   417
\section{The Zermelo-Fraenkel axioms}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   418
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
   419
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
   420
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
   421
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
   422
been replaced by meta-level ones wherever possible, to simplify use of the
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   423
axioms.  
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   424
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   425
The traditional replacement axiom asserts
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   426
\[ y \in \isa{PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \]
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   427
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
   428
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
   429
\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
   430
\[ (\exists!z. P(x,z)) \conj P(x,y). \]
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   431
Thus $y\in \isa{Replace}(A,P)$ if and only if there is some~$x$ such that
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   432
$P(x,-)$ holds uniquely for~$y$.  Because the equivalence is unconditional,
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   433
\isa{Replace} is much easier to use than \isa{PrimReplace}; it defines the
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   434
same set, if $P(x,y)$ is single-valued.  The nice syntax for replacement
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   435
expands to \isa{Replace}.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   436
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   437
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
   438
(\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
   439
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
   440
(\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
   441
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
   442
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   443
The definitions of general intersection, etc., are straightforward.  Note
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   444
the definition of \isa{cons}, which underlies the finite set notation.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   445
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
   446
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
   447
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
   448
construction of the natural numbers.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   449
                                             
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   450
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
   451
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
   452
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
   453
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
   454
$\{\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
   455
general union.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   456
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   457
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
   458
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
   459
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
   460
and~\cdx{snd}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   461
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   462
Operations on relations include converse, domain, range, and image.  The
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   463
set $\isa{Pi}(A,B)$ generalizes the space of functions between two sets.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   464
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
   465
\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
   466
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
   467
over the domain~$A$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   468
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   469
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   470
%%%% zf.thy
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   471
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   472
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   473
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   474
\tdx{ballI}:     [| !!x. x\isasymin{}A ==> P(x) |] ==> {\isasymforall}x\isasymin{}A. P(x)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   475
\tdx{bspec}:     [| {\isasymforall}x\isasymin{}A. P(x);  x\isasymin{}A |] ==> P(x)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   476
\tdx{ballE}:     [| {\isasymforall}x\isasymin{}A. P(x);  P(x) ==> Q;  x \isasymnotin A ==> Q |] ==> Q
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   477
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   478
\tdx{ball_cong}:  [| A=A';  !!x. x\isasymin{}A' ==> P(x) <-> P'(x) |] ==> 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   479
             ({\isasymforall}x\isasymin{}A. P(x)) <-> ({\isasymforall}x\isasymin{}A'. P'(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   480
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   481
\tdx{bexI}:      [| P(x);  x\isasymin{}A |] ==> {\isasymexists}x\isasymin{}A. P(x)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   482
\tdx{bexCI}:     [| {\isasymforall}x\isasymin{}A. ~P(x) ==> P(a);  a\isasymin{}A |] ==> {\isasymexists}x\isasymin{}A. P(x)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   483
\tdx{bexE}:      [| {\isasymexists}x\isasymin{}A. P(x);  !!x. [| x\isasymin{}A; P(x) |] ==> Q |] ==> Q
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   484
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   485
\tdx{bex_cong}:  [| A=A';  !!x. x\isasymin{}A' ==> P(x) <-> P'(x) |] ==> 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   486
             ({\isasymexists}x\isasymin{}A. P(x)) <-> ({\isasymexists}x\isasymin{}A'. P'(x))
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   487
\subcaption{Bounded quantifiers}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   488
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   489
\tdx{subsetI}:     (!!x. x \isasymin A ==> x \isasymin B) ==> A \isasymsubseteq B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   490
\tdx{subsetD}:     [| A \isasymsubseteq B;  c \isasymin A |] ==> c \isasymin B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   491
\tdx{subsetCE}:    [| A \isasymsubseteq B;  c \isasymnotin A ==> P;  c \isasymin B ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   492
\tdx{subset_refl}:  A \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   493
\tdx{subset_trans}: [| A \isasymsubseteq B;  B \isasymsubseteq C |] ==> A \isasymsubseteq C
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   494
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   495
\tdx{equalityI}:   [| A \isasymsubseteq B;  B \isasymsubseteq A |] ==> A = B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   496
\tdx{equalityD1}:  A = B ==> A \isasymsubseteq B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   497
\tdx{equalityD2}:  A = B ==> B \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   498
\tdx{equalityE}:   [| A = B;  [| A \isasymsubseteq B; B \isasymsubseteq A |] ==> P |]  ==>  P
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   499
\subcaption{Subsets and extensionality}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   500
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   501
\tdx{emptyE}:        a \isasymin 0 ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   502
\tdx{empty_subsetI}:  0 \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   503
\tdx{equals0I}:      [| !!y. y \isasymin A ==> False |] ==> A=0
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   504
\tdx{equals0D}:      [| A=0;  a \isasymin A |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   505
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   506
\tdx{PowI}:          A \isasymsubseteq B ==> A \isasymin Pow(B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   507
\tdx{PowD}:          A \isasymin Pow(B)  ==>  A \isasymsubseteq B
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   508
\subcaption{The empty set; power sets}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   509
\end{alltt*}
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
   510
\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
   511
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   512
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   513
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   514
\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
   515
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
   516
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
   517
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
   518
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
   519
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
   520
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
   521
and use its derived rules instead.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   522
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   523
\subsection{Fundamental lemmas}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   524
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
   525
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
   526
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
   527
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
   528
  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
   529
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
   530
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
   531
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   532
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
   533
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
   534
power set operator.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   535
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   536
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
   537
The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   538
comparable rules for \isa{PrimReplace} would be.  The principle of
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   539
separation is proved explicitly, although most proofs should use the
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   540
natural deduction rules for \isa{Collect}.  The elimination rule
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   541
\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
   542
\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
   543
particular circumstances.  Although too many rules can be confusing, there
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   544
is no reason to aim for a minimal set of rules.  
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   545
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   546
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
   547
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
   548
$\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
   549
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
   550
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
   551
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
   552
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
   553
similar premises.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   554
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   555
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   556
%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
   557
\begin{figure}[p]
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   558
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   559
\tdx{ReplaceI}:   [| x\isasymin{}A;  P(x,b);  !!y. P(x,y) ==> y=b |] ==> 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   560
            b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   561
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   562
\tdx{ReplaceE}:   [| b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace};  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   563
               !!x. [| x\isasymin{}A; P(x,b); {\isasymforall}y. P(x,y)-->y=b |] ==> R 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   564
            |] ==> R
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   565
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   566
\tdx{RepFunI}:    [| a\isasymin{}A |] ==> f(a)\isasymin{}{\ttlbrace}f(x). x\isasymin{}A{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   567
\tdx{RepFunE}:    [| b\isasymin{}{\ttlbrace}f(x). x\isasymin{}A{\ttrbrace};  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   568
                !!x.[| x\isasymin{}A;  b=f(x) |] ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   569
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   570
\tdx{separation}:  a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} <-> a\isasymin{}A & P(a)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   571
\tdx{CollectI}:    [| a\isasymin{}A;  P(a) |] ==> a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   572
\tdx{CollectE}:    [| a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace};  [| a\isasymin{}A; P(a) |] ==> R |] ==> R
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   573
\tdx{CollectD1}:   a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} ==> a\isasymin{}A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   574
\tdx{CollectD2}:   a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} ==> P(a)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   575
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   576
\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
   577
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   578
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   579
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   580
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   581
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   582
\tdx{UnionI}: [| B\isasymin{}C;  A\isasymin{}B |] ==> A\isasymin{}Union(C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   583
\tdx{UnionE}: [| A\isasymin{}Union(C);  !!B.[| A\isasymin{}B;  B\isasymin{}C |] ==> R |] ==> R
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   584
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   585
\tdx{InterI}: [| !!x. x\isasymin{}C ==> A\isasymin{}x;  c\isasymin{}C |] ==> A\isasymin{}Inter(C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   586
\tdx{InterD}: [| A\isasymin{}Inter(C);  B\isasymin{}C |] ==> A\isasymin{}B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   587
\tdx{InterE}: [| A\isasymin{}Inter(C);  A\isasymin{}B ==> R;  B \isasymnotin C ==> R |] ==> R
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   588
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   589
\tdx{UN_I}:   [| a\isasymin{}A;  b\isasymin{}B(a) |] ==> b\isasymin{}({\isasymUnion}x\isasymin{}A. B(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   590
\tdx{UN_E}:   [| b\isasymin{}({\isasymUnion}x\isasymin{}A. B(x));  !!x.[| x\isasymin{}A;  b\isasymin{}B(x) |] ==> R 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   591
           |] ==> R
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   592
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   593
\tdx{INT_I}:  [| !!x. x\isasymin{}A ==> b\isasymin{}B(x);  a\isasymin{}A |] ==> b\isasymin{}({\isasymInter}x\isasymin{}A. B(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   594
\tdx{INT_E}:  [| b\isasymin{}({\isasymInter}x\isasymin{}A. B(x));  a\isasymin{}A |] ==> b\isasymin{}B(a)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   595
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   596
\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
   597
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   598
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   599
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   600
%%% upair.thy
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   601
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   602
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   603
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   604
\tdx{pairing}:   a\isasymin{}Upair(b,c) <-> (a=b | a=c)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   605
\tdx{UpairI1}:   a\isasymin{}Upair(a,b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   606
\tdx{UpairI2}:   b\isasymin{}Upair(a,b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   607
\tdx{UpairE}:    [| a\isasymin{}Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   608
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   609
\caption{Unordered pairs} \label{zf-upair1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   610
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   611
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   612
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   613
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   614
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   615
\tdx{UnI1}:      c\isasymin{}A ==> c\isasymin{}A \isasymunion B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   616
\tdx{UnI2}:      c\isasymin{}B ==> c\isasymin{}A \isasymunion B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   617
\tdx{UnCI}:      (c \isasymnotin B ==> c\isasymin{}A) ==> c\isasymin{}A \isasymunion B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   618
\tdx{UnE}:       [| c\isasymin{}A \isasymunion B;  c\isasymin{}A ==> P;  c\isasymin{}B ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   619
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   620
\tdx{IntI}:      [| c\isasymin{}A;  c\isasymin{}B |] ==> c\isasymin{}A Int B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   621
\tdx{IntD1}:     c\isasymin{}A Int B ==> c\isasymin{}A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   622
\tdx{IntD2}:     c\isasymin{}A Int B ==> c\isasymin{}B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   623
\tdx{IntE}:      [| c\isasymin{}A Int B;  [| c\isasymin{}A; c\isasymin{}B |] ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   624
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   625
\tdx{DiffI}:     [| c\isasymin{}A;  c \isasymnotin B |] ==> c\isasymin{}A - B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   626
\tdx{DiffD1}:    c\isasymin{}A - B ==> c\isasymin{}A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   627
\tdx{DiffD2}:    c\isasymin{}A - B ==> c  \isasymnotin  B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   628
\tdx{DiffE}:     [| c\isasymin{}A - B;  [| c\isasymin{}A; c \isasymnotin B |] ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   629
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   630
\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
   631
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   632
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   633
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   634
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   635
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   636
\tdx{consI1}:    a\isasymin{}cons(a,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   637
\tdx{consI2}:    a\isasymin{}B ==> a\isasymin{}cons(b,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   638
\tdx{consCI}:    (a \isasymnotin B ==> a=b) ==> a\isasymin{}cons(b,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   639
\tdx{consE}:     [| a\isasymin{}cons(b,A);  a=b ==> P;  a\isasymin{}A ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   640
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   641
\tdx{singletonI}:  a\isasymin{}{\ttlbrace}a{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   642
\tdx{singletonE}:  [| a\isasymin{}{\ttlbrace}b{\ttrbrace}; a=b ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   643
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   644
\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
   645
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   646
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
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   649
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   650
\tdx{succI1}:    i\isasymin{}succ(i)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   651
\tdx{succI2}:    i\isasymin{}j ==> i\isasymin{}succ(j)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   652
\tdx{succCI}:    (i \isasymnotin j ==> i=j) ==> i\isasymin{}succ(j)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   653
\tdx{succE}:     [| i\isasymin{}succ(j);  i=j ==> P;  i\isasymin{}j ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   654
\tdx{succ_neq_0}:  [| succ(n)=0 |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   655
\tdx{succ_inject}: succ(m) = succ(n) ==> m=n
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   656
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   657
\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
   658
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   659
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   660
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   661
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   662
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   663
\tdx{the_equality}: [| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x))=a
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   664
\tdx{theI}:         \isasymexists! x. P(x) ==> P(THE x. P(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   665
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   666
\tdx{if_P}:          P ==> (if P then a else b) = a
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   667
\tdx{if_not_P}:     ~P ==> (if P then a else b) = b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   668
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   669
\tdx{mem_asym}:     [| a\isasymin{}b;  b\isasymin{}a |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   670
\tdx{mem_irrefl}:   a\isasymin{}a ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   671
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   672
\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
   673
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   674
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
\subsection{Unordered pairs and finite sets}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   677
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
   678
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
   679
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
   680
rule \tdx{UnCI} is useful for classical reasoning about unions,
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   681
like \isa{disjCI}\@; it supersedes \tdx{UnI1} and
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   682
\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
   683
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
   684
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
   685
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   686
Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   687
for~\isa{cons}, the finite set constructor, and rules for singleton
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   688
sets.  Figure~\ref{zf-succ} presents derived rules for the successor
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   689
function, which is defined in terms of~\isa{cons}.  The proof that 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   690
\isa{succ} is injective appears to require the Axiom of Foundation.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   691
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   692
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
   693
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
   694
(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
   695
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
   696
\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
   697
many examples of its use.
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
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
   700
(\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
   701
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
   702
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   703
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   704
%%% subset.thy?
6121
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
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   707
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   708
\tdx{Union_upper}:    B\isasymin{}A ==> B \isasymsubseteq Union(A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   709
\tdx{Union_least}:    [| !!x. x\isasymin{}A ==> x \isasymsubseteq C |] ==> Union(A) \isasymsubseteq C
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   710
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   711
\tdx{Inter_lower}:    B\isasymin{}A ==> Inter(A) \isasymsubseteq B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   712
\tdx{Inter_greatest}: [| a\isasymin{}A; !!x. x\isasymin{}A ==> C \isasymsubseteq x |] ==> C\isasymsubseteq{}Inter(A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   713
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   714
\tdx{Un_upper1}:      A \isasymsubseteq A \isasymunion B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   715
\tdx{Un_upper2}:      B \isasymsubseteq A \isasymunion B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   716
\tdx{Un_least}:       [| A \isasymsubseteq C;  B \isasymsubseteq C |] ==> A \isasymunion B \isasymsubseteq C
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   717
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   718
\tdx{Int_lower1}:     A Int B \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   719
\tdx{Int_lower2}:     A Int B \isasymsubseteq B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   720
\tdx{Int_greatest}:   [| C \isasymsubseteq A;  C \isasymsubseteq B |] ==> C \isasymsubseteq A Int B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   721
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   722
\tdx{Diff_subset}:    A-B \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   723
\tdx{Diff_contains}:  [| C \isasymsubseteq A;  C Int B = 0 |] ==> C \isasymsubseteq A-B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   724
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   725
\tdx{Collect_subset}: Collect(A,P) \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   726
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   727
\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
   728
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   729
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   730
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   731
\subsection{Subset and lattice properties}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   732
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
   733
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
   734
shows the corresponding rules.  A few other laws involving subsets are
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   735
included. 
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   736
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
   737
reasoning about the membership relation.  Section~\ref{sec:ZF-pow-example}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   738
below presents an example of this, proving the equation 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   739
${\isa{Pow}(A)\cap \isa{Pow}(B)}= \isa{Pow}(A\cap B)$.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   740
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   741
%%% pair.thy
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   742
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   743
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   744
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   745
\tdx{Pair_inject1}: <a,b> = <c,d> ==> a=c
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   746
\tdx{Pair_inject2}: <a,b> = <c,d> ==> b=d
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   747
\tdx{Pair_inject}:  [| <a,b> = <c,d>;  [| a=c; b=d |] ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   748
\tdx{Pair_neq_0}:   <a,b>=0 ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   749
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   750
\tdx{fst_conv}:     fst(<a,b>) = a
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   751
\tdx{snd_conv}:     snd(<a,b>) = b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   752
\tdx{split}:        split(\%x y. c(x,y), <a,b>) = c(a,b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   753
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   754
\tdx{SigmaI}:     [| a\isasymin{}A;  b\isasymin{}B(a) |] ==> <a,b>\isasymin{}Sigma(A,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   755
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   756
\tdx{SigmaE}:     [| c\isasymin{}Sigma(A,B);  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   757
                !!x y.[| x\isasymin{}A; y\isasymin{}B(x); c=<x,y> |] ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   758
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   759
\tdx{SigmaE2}:    [| <a,b>\isasymin{}Sigma(A,B);    
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   760
                [| a\isasymin{}A;  b\isasymin{}B(a) |] ==> P   |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   761
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   762
\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
   763
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   766
\subsection{Ordered pairs} \label{sec:pairs}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   767
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   768
Figure~\ref{zf-pair} presents the rules governing ordered pairs,
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   769
projections and general sums --- in particular, that
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   770
$\{\{a\},\{a,b\}\}$ functions as an ordered pair.  This property is
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   771
expressed as two destruction rules,
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   772
\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
   773
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
   774
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   775
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
   776
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
   777
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
   778
satisfy $\pair{\emptyset;\emptyset}=\emptyset$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   779
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   780
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
   781
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
   782
$\pair{x,y}$, for $x\in A$ and $y\in B(x)$.  The rule \tdx{SigmaE2}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   783
merely states that $\pair{a,b}\in \isa{Sigma}(A,B)$ implies $a\in A$ and
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   784
$b\in B(a)$.
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
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
   787
\begin{center}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   788
{\tt\%<$x$,$y$>. $t$} \quad stands for\quad \isa{split(\%$x$ $y$.\ $t$)}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   789
\end{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   790
Nested patterns are translated recursively:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   791
{\tt\%<$x$,$y$,$z$>. $t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>. $t$} $\leadsto$
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   792
\isa{split(\%$x$.\%<$y$,$z$>. $t$)} $\leadsto$ \isa{split(\%$x$. split(\%$y$
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   793
  $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
   794
\begin{warn}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   795
  The translation between patterns and \isa{split} is performed automatically
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   796
  by the parser and printer.  Thus the internal and external form of a term
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   797
  may differ, which affects proofs.  For example the term \isa{(\%<x,y>.<y,x>)<a,b>} requires the theorem \isa{split} to rewrite to
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   798
  {\tt<b,a>}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   799
\end{warn}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   800
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
   801
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
   802
$\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
   803
\begin{description}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   804
\item[Let:] \isa{let {\it pattern} = $t$ in $u$}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   805
\item[Choice:] \isa{THE~{\it pattern}~.~$P$}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   806
\item[Set operations:] \isa{\isasymUnion~{\it pattern}:$A$.~$B$}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   807
\item[Comprehension:] \isa{{\ttlbrace}~{\it pattern}:$A$~.~$P$~{\ttrbrace}}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   808
\end{description}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   809
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   810
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   811
%%% domrange.thy?
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   812
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   813
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   814
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   815
\tdx{domainI}:     <a,b>\isasymin{}r ==> a\isasymin{}domain(r)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   816
\tdx{domainE}:     [| a\isasymin{}domain(r); !!y. <a,y>\isasymin{}r ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   817
\tdx{domain_subset}: domain(Sigma(A,B)) \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   818
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   819
\tdx{rangeI}:      <a,b>\isasymin{}r ==> b\isasymin{}range(r)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   820
\tdx{rangeE}:      [| b\isasymin{}range(r); !!x. <x,b>\isasymin{}r ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   821
\tdx{range_subset}: range(A*B) \isasymsubseteq B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   822
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   823
\tdx{fieldI1}:     <a,b>\isasymin{}r ==> a\isasymin{}field(r)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   824
\tdx{fieldI2}:     <a,b>\isasymin{}r ==> b\isasymin{}field(r)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   825
\tdx{fieldCI}:     (<c,a> \isasymnotin r ==> <a,b>\isasymin{}r) ==> a\isasymin{}field(r)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   826
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   827
\tdx{fieldE}:      [| a\isasymin{}field(r); 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   828
                  !!x. <a,x>\isasymin{}r ==> P; 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   829
                  !!x. <x,a>\isasymin{}r ==> P      
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   830
               |] ==> P
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   831
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   832
\tdx{field_subset}:  field(A*A) \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   833
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   834
\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
   835
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   836
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   837
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   838
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   839
\tdx{imageI}:      [| <a,b>\isasymin{}r; a\isasymin{}A |] ==> b\isasymin{}r``A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   840
\tdx{imageE}:      [| b\isasymin{}r``A; !!x.[| <x,b>\isasymin{}r; x\isasymin{}A |] ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   841
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   842
\tdx{vimageI}:     [| <a,b>\isasymin{}r; b\isasymin{}B |] ==> a\isasymin{}r-``B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   843
\tdx{vimageE}:     [| a\isasymin{}r-``B; !!x.[| <a,x>\isasymin{}r;  x\isasymin{}B |] ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   844
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   845
\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
   846
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   847
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
\subsection{Relations}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   850
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
   851
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
   852
$\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
   853
{\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
   854
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
   855
\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
   856
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
   857
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
   858
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   859
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
   860
Note that these operations are generalisations of range and domain,
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   861
respectively. 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   862
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   863
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   864
%%% func.thy
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   865
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   866
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   867
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   868
\tdx{fun_is_rel}:     f\isasymin{}Pi(A,B) ==> f \isasymsubseteq Sigma(A,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   869
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   870
\tdx{apply_equality}: [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   871
\tdx{apply_equality2}: [| <a,b>\isasymin{}f; <a,c>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> b=c
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   872
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   873
\tdx{apply_type}:     [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> f`a\isasymin{}B(a)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   874
\tdx{apply_Pair}:     [| f\isasymin{}Pi(A,B); a\isasymin{}A |] ==> <a,f`a>\isasymin{}f
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   875
\tdx{apply_iff}:      f\isasymin{}Pi(A,B) ==> <a,b>\isasymin{}f <-> a\isasymin{}A & f`a = b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   876
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   877
\tdx{fun_extension}:  [| f\isasymin{}Pi(A,B); g\isasymin{}Pi(A,D);
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   878
                   !!x. x\isasymin{}A ==> f`x = g`x     |] ==> f=g
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   879
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   880
\tdx{domain_type}:    [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> a\isasymin{}A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   881
\tdx{range_type}:     [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> b\isasymin{}B(a)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   882
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   883
\tdx{Pi_type}:        [| f\isasymin{}A->C; !!x. x\isasymin{}A ==> f`x\isasymin{}B(x) |] ==> f\isasymin{}Pi(A,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   884
\tdx{domain_of_fun}:  f\isasymin{}Pi(A,B) ==> domain(f)=A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   885
\tdx{range_of_fun}:   f\isasymin{}Pi(A,B) ==> f\isasymin{}A->range(f)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   886
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   887
\tdx{restrict}:       a\isasymin{}A ==> restrict(f,A) ` a = f`a
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   888
\tdx{restrict_type}:  [| !!x. x\isasymin{}A ==> f`x\isasymin{}B(x) |] ==> 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   889
                restrict(f,A)\isasymin{}Pi(A,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   890
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   891
\caption{Functions} \label{zf-func1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   892
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   893
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   894
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   895
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   896
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   897
\tdx{lamI}:     a\isasymin{}A ==> <a,b(a)>\isasymin{}(lam x\isasymin{}A. b(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   898
\tdx{lamE}:     [| p\isasymin{}(lam x\isasymin{}A. b(x)); !!x.[| x\isasymin{}A; p=<x,b(x)> |] ==> P 
8249
3fc32155372c fixed some overfull lines
paulson
parents: 6745
diff changeset
   899
          |] ==>  P
3fc32155372c fixed some overfull lines
paulson
parents: 6745
diff changeset
   900
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   901
\tdx{lam_type}: [| !!x. x\isasymin{}A ==> b(x)\isasymin{}B(x) |] ==> (lam x\isasymin{}A. b(x))\isasymin{}Pi(A,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   902
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   903
\tdx{beta}:     a\isasymin{}A ==> (lam x\isasymin{}A. b(x)) ` a = b(a)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   904
\tdx{eta}:      f\isasymin{}Pi(A,B) ==> (lam x\isasymin{}A. f`x) = f
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   905
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   906
\caption{$\lambda$-abstraction} \label{zf-lam}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   907
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   908
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   909
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   910
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   911
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   912
\tdx{fun_empty}:           0\isasymin{}0->0
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   913
\tdx{fun_single}:          {\ttlbrace}<a,b>{\ttrbrace}\isasymin{}{\ttlbrace}a{\ttrbrace} -> {\ttlbrace}b{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   914
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   915
\tdx{fun_disjoint_Un}:     [| f\isasymin{}A->B; g\isasymin{}C->D; A Int C = 0  |] ==>  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   916
                     (f \isasymunion g)\isasymin{}(A \isasymunion C) -> (B \isasymunion D)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   917
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   918
\tdx{fun_disjoint_apply1}: [| a\isasymin{}A; f\isasymin{}A->B; g\isasymin{}C->D;  A\isasyminter{}C = 0 |] ==>  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   919
                     (f \isasymunion g)`a = f`a
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   920
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   921
\tdx{fun_disjoint_apply2}: [| c\isasymin{}C; f\isasymin{}A->B; g\isasymin{}C->D;  A\isasyminter{}C = 0 |] ==>  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   922
                     (f \isasymunion g)`c = g`c
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   923
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   924
\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
   925
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   926
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
\subsection{Functions}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   929
Functions, represented by graphs, are notoriously difficult to reason
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   930
about.  The ZF theory provides many derived rules, which overlap more
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   931
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
   932
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   933
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
   934
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
   935
$\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
   936
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
   937
(\tdx{fun_extension}).
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   938
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   939
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
   940
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
   941
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
   942
any dependent typing can be flattened to yield a function type of the form
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   943
$A\to C$; here, $C=\isa{range}(f)$.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   944
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   945
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
   946
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
   947
\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
   948
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
   949
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   950
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
   951
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
   952
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
   953
disjoint.  
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   954
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   955
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   956
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   957
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   958
\tdx{Int_absorb}:        A Int A = A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   959
\tdx{Int_commute}:       A Int B = B Int A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   960
\tdx{Int_assoc}:         (A Int B) Int C  =  A Int (B Int C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   961
\tdx{Int_Un_distrib}:    (A \isasymunion B) Int C  =  (A Int C) \isasymunion (B Int C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   962
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   963
\tdx{Un_absorb}:         A \isasymunion A = A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   964
\tdx{Un_commute}:        A \isasymunion B = B \isasymunion A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   965
\tdx{Un_assoc}:          (A \isasymunion B) \isasymunion C  =  A \isasymunion (B \isasymunion C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   966
\tdx{Un_Int_distrib}:    (A Int B) \isasymunion C  =  (A \isasymunion C) Int (B \isasymunion C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   967
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   968
\tdx{Diff_cancel}:       A-A = 0
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   969
\tdx{Diff_disjoint}:     A Int (B-A) = 0
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   970
\tdx{Diff_partition}:    A \isasymsubseteq B ==> A \isasymunion (B-A) = B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   971
\tdx{double_complement}: [| A \isasymsubseteq B; B \isasymsubseteq C |] ==> (B - (C-A)) = A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   972
\tdx{Diff_Un}:           A - (B \isasymunion C) = (A-B) Int (A-C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   973
\tdx{Diff_Int}:          A - (B Int C) = (A-B) \isasymunion (A-C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   974
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   975
\tdx{Union_Un_distrib}:  Union(A \isasymunion B) = Union(A) \isasymunion Union(B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   976
\tdx{Inter_Un_distrib}:  [| a \isasymin A;  b \isasymin B |] ==> 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   977
                   Inter(A \isasymunion B) = Inter(A) Int Inter(B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   978
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   979
\tdx{Int_Union_RepFun}:  A Int Union(B) = ({\isasymUnion}C \isasymin B. A Int C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   980
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   981
\tdx{Un_Inter_RepFun}:   b \isasymin B ==> 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   982
                   A \isasymunion Inter(B) = ({\isasymInter}C \isasymin B. A \isasymunion C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   983
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   984
\tdx{SUM_Un_distrib1}:   (SUM x \isasymin A \isasymunion B. C(x)) = 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   985
                   (SUM x \isasymin A. C(x)) \isasymunion (SUM x \isasymin B. C(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   986
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   987
\tdx{SUM_Un_distrib2}:   (SUM x \isasymin C. A(x) \isasymunion B(x)) =
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   988
                   (SUM x \isasymin C. A(x)) \isasymunion (SUM x \isasymin C. B(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   989
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   990
\tdx{SUM_Int_distrib1}:  (SUM x \isasymin A Int B. C(x)) =
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   991
                   (SUM x \isasymin A. C(x)) Int (SUM x \isasymin B. C(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   992
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   993
\tdx{SUM_Int_distrib2}:  (SUM x \isasymin C. A(x) Int B(x)) =
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   994
                   (SUM x \isasymin C. A(x)) Int (SUM x \isasymin C. B(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   995
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   996
\caption{Equalities} \label{zf-equalities}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   997
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   998
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
\begin{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1001
%\begin{constants} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1002
%  \cdx{1}       & $i$           &       & $\{\emptyset\}$       \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1003
%  \cdx{bool}    & $i$           &       & the set $\{\emptyset,1\}$     \\
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1004
%  \cdx{cond}   & $[i,i,i]\To i$ &       & conditional for \isa{bool}    \\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1005
%  \cdx{not}    & $i\To i$       &       & negation for \isa{bool}       \\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1006
%  \sdx{and}    & $[i,i]\To i$   & Left 70 & conjunction for \isa{bool}  \\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1007
%  \sdx{or}     & $[i,i]\To i$   & Left 65 & disjunction for \isa{bool}  \\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1008
%  \sdx{xor}    & $[i,i]\To i$   & Left 65 & exclusive-or for \isa{bool}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1009
%\end{constants}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1010
%
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1011
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1012
\tdx{bool_def}:      bool == {\ttlbrace}0,1{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1013
\tdx{cond_def}:      cond(b,c,d) == if b=1 then c else d
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1014
\tdx{not_def}:       not(b)  == cond(b,0,1)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1015
\tdx{and_def}:       a and b == cond(a,b,0)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1016
\tdx{or_def}:        a or b  == cond(a,1,b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1017
\tdx{xor_def}:       a xor b == cond(a,not(b),b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1018
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1019
\tdx{bool_1I}:       1 \isasymin bool
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1020
\tdx{bool_0I}:       0 \isasymin bool
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1021
\tdx{boolE}:         [| c \isasymin bool;  c=1 ==> P;  c=0 ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1022
\tdx{cond_1}:        cond(1,c,d) = c
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1023
\tdx{cond_0}:        cond(0,c,d) = d
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1024
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1025
\caption{The booleans} \label{zf-bool}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1026
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1027
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1028
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1029
\section{Further developments}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1030
The next group of developments is complex and extensive, and only
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1031
highlights can be covered here.  It involves many theories and proofs. 
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1032
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1033
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
  1034
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
  1035
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1036
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
  1037
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
  1038
first-order theory, you can obtain the effect of higher-order logic using
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1039
\isa{bool}-valued functions, for example.  The constant~\isa{1} is
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1040
translated to \isa{succ(0)}.
6121
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
\begin{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1043
\index{*"+ symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1044
\begin{constants}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1045
  \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
  1046
  \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
  1047
  \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
  1048
  \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
  1049
\end{constants}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1050
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1051
\tdx{sum_def}:   A+B == {\ttlbrace}0{\ttrbrace}*A \isasymunion {\ttlbrace}1{\ttrbrace}*B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1052
\tdx{Inl_def}:   Inl(a) == <0,a>
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1053
\tdx{Inr_def}:   Inr(b) == <1,b>
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1054
\tdx{case_def}:  case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1055
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1056
\tdx{InlI}:      a \isasymin A ==> Inl(a) \isasymin A+B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1057
\tdx{InrI}:      b \isasymin B ==> Inr(b) \isasymin A+B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1058
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1059
\tdx{Inl_inject}:  Inl(a)=Inl(b) ==> a=b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1060
\tdx{Inr_inject}:  Inr(a)=Inr(b) ==> a=b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1061
\tdx{Inl_neq_Inr}: Inl(a)=Inr(b) ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1062
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1063
\tdx{sum_iff}:  u \isasymin A+B <-> ({\isasymexists}x\isasymin{}A. u=Inl(x)) | ({\isasymexists}y\isasymin{}B. u=Inr(y))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1064
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1065
\tdx{case_Inl}:  case(c,d,Inl(a)) = c(a)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1066
\tdx{case_Inr}:  case(c,d,Inr(b)) = d(b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1067
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1068
\caption{Disjoint unions} \label{zf-sum}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1069
\end{figure}
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
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1072
\subsection{Disjoint unions}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1073
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1074
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
  1075
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
  1076
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
  1077
mutual recursion~\cite{paulson-set-II}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1078
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1079
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1080
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1081
\tdx{QPair_def}:      <a;b> == a+b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1082
\tdx{qsplit_def}:     qsplit(c,p)  == THE y. {\isasymexists}a b. p=<a;b> & y=c(a,b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1083
\tdx{qfsplit_def}:    qfsplit(R,z) == {\isasymexists}x y. z=<x;y> & R(x,y)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1084
\tdx{qconverse_def}:  qconverse(r) == {\ttlbrace}z. w \isasymin r, {\isasymexists}x y. w=<x;y> & z=<y;x>{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1085
\tdx{QSigma_def}:     QSigma(A,B)  == {\isasymUnion}x \isasymin A. {\isasymUnion}y \isasymin B(x). {\ttlbrace}<x;y>{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1086
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1087
\tdx{qsum_def}:       A <+> B      == ({\ttlbrace}0{\ttrbrace} <*> A) \isasymunion ({\ttlbrace}1{\ttrbrace} <*> B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1088
\tdx{QInl_def}:       QInl(a)      == <0;a>
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1089
\tdx{QInr_def}:       QInr(b)      == <1;b>
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1090
\tdx{qcase_def}:      qcase(c,d)   == qsplit(\%y z. cond(y, d(z), c(z)))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1091
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1092
\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
  1093
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1094
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1095
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1096
\subsection{Non-standard ordered pairs}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1097
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1098
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
  1099
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
  1100
{\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
  1101
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
  1102
\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
  1103
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
  1104
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
  1105
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
  1106
addition, {\tt<$a$;$b$>} is continuous.  The theory supports coinductive
6592
c120262044b6 Now uses manual.bib; some references updated
paulson
parents: 6173
diff changeset
  1107
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
  1108
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1109
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1110
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1111
\tdx{bnd_mono_def}:  bnd_mono(D,h) == 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1112
                 h(D) \isasymsubseteq D & ({\isasymforall}W X. W \isasymsubseteq X --> X \isasymsubseteq D --> h(W) \isasymsubseteq h(X))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1113
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1114
\tdx{lfp_def}:       lfp(D,h) == Inter({\ttlbrace}X \isasymin Pow(D). h(X) \isasymsubseteq X{\ttrbrace})
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1115
\tdx{gfp_def}:       gfp(D,h) == Union({\ttlbrace}X \isasymin Pow(D). X \isasymsubseteq h(X){\ttrbrace})
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1116
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1117
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1118
\tdx{lfp_lowerbound} [| h(A) \isasymsubseteq A;  A \isasymsubseteq D |] ==> lfp(D,h) \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1119
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1120
\tdx{lfp_subset}:    lfp(D,h) \isasymsubseteq D
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1121
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1122
\tdx{lfp_greatest}:  [| bnd_mono(D,h);  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1123
                  !!X. [| h(X) \isasymsubseteq X;  X \isasymsubseteq D |] ==> A \isasymsubseteq X 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1124
               |] ==> A \isasymsubseteq lfp(D,h)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1125
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1126
\tdx{lfp_Tarski}:    bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1127
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1128
\tdx{induct}:        [| a \isasymin lfp(D,h);  bnd_mono(D,h);
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1129
                  !!x. x \isasymin h(Collect(lfp(D,h),P)) ==> P(x)
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1130
               |] ==> P(a)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1131
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1132
\tdx{lfp_mono}:      [| bnd_mono(D,h);  bnd_mono(E,i);
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1133
                  !!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X)  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1134
               |] ==> lfp(D,h) \isasymsubseteq lfp(E,i)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1135
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1136
\tdx{gfp_upperbound} [| A \isasymsubseteq h(A);  A \isasymsubseteq D |] ==> A \isasymsubseteq gfp(D,h)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1137
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1138
\tdx{gfp_subset}:    gfp(D,h) \isasymsubseteq D
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1139
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1140
\tdx{gfp_least}:     [| bnd_mono(D,h);  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1141
                  !!X. [| X \isasymsubseteq h(X);  X \isasymsubseteq D |] ==> X \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1142
               |] ==> gfp(D,h) \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1143
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1144
\tdx{gfp_Tarski}:    bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1145
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1146
\tdx{coinduct}:      [| bnd_mono(D,h); a \isasymin X; X \isasymsubseteq h(X \isasymunion gfp(D,h)); X \isasymsubseteq D 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1147
               |] ==> a \isasymin gfp(D,h)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1148
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1149
\tdx{gfp_mono}:      [| bnd_mono(D,h);  D \isasymsubseteq E;
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1150
                  !!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X)  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1151
               |] ==> gfp(D,h) \isasymsubseteq gfp(E,i)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1152
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1153
\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
  1154
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1155
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1156
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1157
\subsection{Least and greatest fixedpoints}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1158
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1159
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
  1160
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
  1161
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
  1162
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
  1163
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
  1164
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
  1165
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
  1166
package also uses the fixedpoint operators~\cite{paulson-CADE}.  See
6745
74e8f703f5f2 tuned manual.bib;
wenzelm
parents: 6592
diff changeset
  1167
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
  1168
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
  1169
proofs.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1170
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1171
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
  1172
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
  1173
are useful for applying the Knaster-Tarski Fixedpoint Theorem.  The proofs
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1174
themselves are trivial applications of Isabelle's classical reasoner. 
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1175
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1176
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1177
\subsection{Finite sets and lists}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1178
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1179
Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines the finite set operator;
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1180
$\isa{Fin}(A)$ is the set of all finite sets over~$A$.  The theory employs
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1181
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
  1182
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
  1183
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
  1184
between two given sets.
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
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1187
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1188
\tdx{Fin.emptyI}      0 \isasymin Fin(A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1189
\tdx{Fin.consI}       [| a \isasymin A;  b \isasymin Fin(A) |] ==> cons(a,b) \isasymin Fin(A)
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1190
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1191
\tdx{Fin_induct}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1192
    [| b \isasymin Fin(A);
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1193
       P(0);
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1194
       !!x y. [| x \isasymin A;  y \isasymin Fin(A);  x \isasymnotin y;  P(y) |] ==> P(cons(x,y))
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1195
    |] ==> P(b)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1196
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1197
\tdx{Fin_mono}:       A \isasymsubseteq B ==> Fin(A) \isasymsubseteq Fin(B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1198
\tdx{Fin_UnI}:        [| b \isasymin Fin(A);  c \isasymin Fin(A) |] ==> b \isasymunion c \isasymin Fin(A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1199
\tdx{Fin_UnionI}:     C \isasymin Fin(Fin(A)) ==> Union(C) \isasymin Fin(A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1200
\tdx{Fin_subset}:     [| c \isasymsubseteq b;  b \isasymin Fin(A) |] ==> c \isasymin Fin(A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1201
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1202
\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
  1203
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1204
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1205
\begin{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1206
\begin{constants}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1207
  \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
  1208
  \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
  1209
  \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
  1210
  \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
  1211
  \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
  1212
  \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
  1213
  \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
  1214
  \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
  1215
\end{constants}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1216
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1217
\underscoreon %%because @ is used here
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1218
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1219
\tdx{NilI}:           Nil \isasymin list(A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1220
\tdx{ConsI}:          [| a \isasymin A;  l \isasymin list(A) |] ==> Cons(a,l) \isasymin list(A)
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1221
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1222
\tdx{List.induct}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1223
    [| l \isasymin list(A);
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1224
       P(Nil);
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1225
       !!x y. [| x \isasymin A;  y \isasymin list(A);  P(y) |] ==> P(Cons(x,y))
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1226
    |] ==> P(l)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1227
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1228
\tdx{Cons_iff}:       Cons(a,l)=Cons(a',l') <-> a=a' & l=l'
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1229
\tdx{Nil_Cons_iff}:    Nil \isasymnoteq Cons(a,l)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1230
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1231
\tdx{list_mono}:      A \isasymsubseteq B ==> list(A) \isasymsubseteq list(B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1232
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1233
\tdx{map_ident}:      l \isasymin list(A) ==> map(\%u. u, l) = l
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1234
\tdx{map_compose}:    l \isasymin list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l)
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1235
\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
  1236
\tdx{map_type}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1237
    [| l \isasymin list(A);  !!x. x \isasymin A ==> h(x) \isasymin B |] ==> map(h,l) \isasymin list(B)
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1238
\tdx{map_flat}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1239
    ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1240
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1241
\caption{Lists} \label{zf-list}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1242
\end{figure}
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
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1245
Figure~\ref{zf-list} presents the set of lists over~$A$, $\isa{list}(A)$.  The
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1246
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
  1247
and induction rules automatically, as well as the constructors, case operator
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1248
(\isa{list\_case}) and recursion operator.  The theory then defines the usual
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1249
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
  1250
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1251
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1252
\subsection{Miscellaneous}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1253
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1254
\begin{figure}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1255
\begin{constants} 
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1256
  \it symbol  & \it meta-type & \it priority & \it description \\ 
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1257
  \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
  1258
  \cdx{id}      & $i\To i$      &       & identity function \\
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1259
  \cdx{inj}     & $[i,i]\To i$  &       & injective function space\\
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1260
  \cdx{surj}    & $[i,i]\To i$  &       & surjective function space\\
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1261
  \cdx{bij}     & $[i,i]\To i$  &       & bijective function space
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1262
\end{constants}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1263
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1264
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1265
\tdx{comp_def}: r O s     == {\ttlbrace}xz \isasymin domain(s)*range(r) . 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1266
                        {\isasymexists}x y z. xz=<x,z> & <x,y> \isasymin s & <y,z> \isasymin r{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1267
\tdx{id_def}:   id(A)     == (lam x \isasymin A. x)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1268
\tdx{inj_def}:  inj(A,B)  == {\ttlbrace} f \isasymin A->B. {\isasymforall}w \isasymin A. {\isasymforall}x \isasymin A. f`w=f`x --> w=x {\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1269
\tdx{surj_def}: surj(A,B) == {\ttlbrace} f \isasymin A->B . {\isasymforall}y \isasymin B. {\isasymexists}x \isasymin A. f`x=y {\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1270
\tdx{bij_def}:  bij(A,B)  == inj(A,B) Int surj(A,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1271
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1272
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1273
\tdx{left_inverse}:    [| f \isasymin inj(A,B);  a \isasymin A |] ==> converse(f)`(f`a) = a
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1274
\tdx{right_inverse}:   [| f \isasymin inj(A,B);  b \isasymin range(f) |] ==> 
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1275
                 f`(converse(f)`b) = b
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1276
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1277
\tdx{inj_converse_inj} f \isasymin inj(A,B) ==> converse(f) \isasymin inj(range(f), A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1278
\tdx{bij_converse_bij} f \isasymin bij(A,B) ==> converse(f) \isasymin bij(B,A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1279
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1280
\tdx{comp_type}:       [| s \isasymsubseteq A*B;  r \isasymsubseteq B*C |] ==> (r O s) \isasymsubseteq A*C
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1281
\tdx{comp_assoc}:      (r O s) O t = r O (s O t)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1282
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1283
\tdx{left_comp_id}:    r \isasymsubseteq A*B ==> id(B) O r = r
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1284
\tdx{right_comp_id}:   r \isasymsubseteq A*B ==> r O id(A) = r
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1285
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1286
\tdx{comp_func}:       [| g \isasymin A->B; f \isasymin B->C |] ==> (f O g)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1287
\isasymin A ->C
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1288
\tdx{comp_func_apply}: [| g \isasymin A->B; f \isasymin B->C; a \isasymin A |] ==> (f O g)`a = f`(g`a)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1289
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1290
\tdx{comp_inj}:        [| g \isasymin inj(A,B);  f \isasymin inj(B,C)  |] ==> (f O g):inj(A,C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1291
\tdx{comp_surj}:       [| g \isasymin surj(A,B); f \isasymin surj(B,C) |] ==> (f O g):surj(A,C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1292
\tdx{comp_bij}:        [| g \isasymin bij(A,B); f \isasymin bij(B,C) |] ==> (f O g):bij(A,C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1293
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1294
\tdx{left_comp_inverse}:    f \isasymin inj(A,B) ==> converse(f) O f = id(A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1295
\tdx{right_comp_inverse}:   f \isasymin surj(A,B) ==> f O converse(f) = id(B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1296
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1297
\tdx{bij_disjoint_Un}:  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1298
    [| f \isasymin bij(A,B);  g \isasymin bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1299
    (f \isasymunion g) \isasymin bij(A \isasymunion C, B \isasymunion D)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1300
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1301
\tdx{restrict_bij}: [| f \isasymin inj(A,B);  C \isasymsubseteq A |] ==> restrict(f,C) \isasymin bij(C, f``C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1302
\end{alltt*}
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1303
\caption{Permutations} \label{zf-perm}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1304
\end{figure}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1305
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1306
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
  1307
related concepts.  These include composition of relations, the identity
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1308
relation, and three specialized function spaces: injective, surjective and
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1309
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
  1310
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
  1311
equipollence and cardinality.
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1312
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1313
Theory \thydx{Univ} defines a `universe' $\isa{univ}(A)$, which is used by
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1314
the datatype package.  This set contains $A$ and the
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1315
natural numbers.  Vitally, it is closed under finite products: 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1316
$\isa{univ}(A)\times\isa{univ}(A)\subseteq\isa{univ}(A)$.  This theory also
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1317
defines the cumulative hierarchy of axiomatic set theory, which
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1318
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
  1319
`universe' is a simple generalization of~$V@\omega$.
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1320
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1321
Theory \thydx{QUniv} defines a `universe' $\isa{quniv}(A)$, which is used by
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1322
the datatype package to construct codatatypes such as streams.  It is
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1323
analogous to $\isa{univ}(A)$ (and is defined in terms of it) but is closed
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1324
under the non-standard product and sum.
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1325
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1326
6173
2c0579e8e6fa documented typecheck_tac, etc
paulson
parents: 6143
diff changeset
  1327
\section{Automatic Tools}
2c0579e8e6fa documented typecheck_tac, etc
paulson
parents: 6143
diff changeset
  1328
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
  1329
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
  1330
specialized tool to infer `types' of terms.
6173
2c0579e8e6fa documented typecheck_tac, etc
paulson
parents: 6143
diff changeset
  1331
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1332
\subsection{Simplification and Classical Reasoning}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1333
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
  1334
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
  1335
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
  1336
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
  1337
  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
  1338
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
  1339
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
  1340
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1341
The default simpset used by \isa{simp} contains congruence rules for all of ZF's
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1342
binding operators.  It contains all the conversion rules, such as
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1343
\isa{fst} and
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1344
\isa{snd}, as well as the rewrites shown in Fig.\ts\ref{zf-simpdata}.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1345
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1346
Classical reasoner methods such as \isa{blast} and \isa{auto} refer to
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1347
a rich collection of built-in axioms for all the set-theoretic
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1348
primitives.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1349
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1350
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1351
\begin{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1352
\begin{eqnarray*}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1353
  a\in \emptyset        & \bimp &  \bot\\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1354
  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
  1355
  a \in A \int B      & \bimp &  a\in A \conj a\in B\\
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1356
  a \in A-B             & \bimp &  a\in A \conj \lnot (a\in B)\\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1357
  \pair{a,b}\in \isa{Sigma}(A,B)
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1358
                        & \bimp &  a\in A \conj b\in B(a)\\
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1359
  a \in \isa{Collect}(A,P)      & \bimp &  a\in A \conj P(a)\\
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1360
  (\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
  1361
  (\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
  1362
\end{eqnarray*}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1363
\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
  1364
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1365
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1366
6173
2c0579e8e6fa documented typecheck_tac, etc
paulson
parents: 6143
diff changeset
  1367
\subsection{Type-Checking Tactics}
2c0579e8e6fa documented typecheck_tac, etc
paulson
parents: 6143
diff changeset
  1368
\index{type-checking tactics}
2c0579e8e6fa documented typecheck_tac, etc
paulson
parents: 6143
diff changeset
  1369
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
  1370
Isabelle/ZF provides simple tactics to help automate those proofs that are
6173
2c0579e8e6fa documented typecheck_tac, etc
paulson
parents: 6143
diff changeset
  1371
essentially type-checking.  Such proofs are built by applying rules such as
2c0579e8e6fa documented typecheck_tac, etc
paulson
parents: 6143
diff changeset
  1372
these:
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836