doc-src/ZF/ZF.tex
author paulson
Tue, 23 Sep 2003 15:44:25 +0200
changeset 14202 643fc73e2910
parent 14158 15bab630ae31
child 28871 111bbd2b12db
permissions -rw-r--r--
case_tac tweak
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 \\
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   234
         & | & term " \isasyminter " 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))
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   376
\tdx{Int_def}:     A \isasyminter B  == Inter(Upair(A,B))
14154
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
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   437
Other consequences of replacement include replacement for 
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   438
meta-level functions
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   439
(\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
   440
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
   441
(\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
   442
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
   443
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   444
The definitions of general intersection, etc., are straightforward.  Note
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   445
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
   446
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
   447
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
   448
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
   449
construction of the natural numbers.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   450
                                             
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   451
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
   452
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
   453
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
   454
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
   455
$\{\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
   456
general union.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   457
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   458
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
   459
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
   460
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
   461
and~\cdx{snd}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   462
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   463
Operations on relations include converse, domain, range, and image.  The
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   464
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
   465
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
   466
\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
   467
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
   468
over the domain~$A$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   469
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   470
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   471
%%%% zf.thy
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   472
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   473
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   474
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   475
\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
   476
\tdx{bspec}:     [| {\isasymforall}x\isasymin{}A. P(x);  x\isasymin{}A |] ==> P(x)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   477
\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
   478
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   479
\tdx{ball_cong}:  [| A=A';  !!x. x\isasymin{}A' ==> P(x) <-> P'(x) |] ==> 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   480
             ({\isasymforall}x\isasymin{}A. P(x)) <-> ({\isasymforall}x\isasymin{}A'. P'(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   481
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   482
\tdx{bexI}:      [| P(x);  x\isasymin{}A |] ==> {\isasymexists}x\isasymin{}A. P(x)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   483
\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
   484
\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
   485
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   486
\tdx{bex_cong}:  [| A=A';  !!x. x\isasymin{}A' ==> P(x) <-> P'(x) |] ==> 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   487
             ({\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
   488
\subcaption{Bounded quantifiers}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   489
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   490
\tdx{subsetI}:     (!!x. x \isasymin A ==> x \isasymin B) ==> A \isasymsubseteq B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   491
\tdx{subsetD}:     [| A \isasymsubseteq B;  c \isasymin A |] ==> c \isasymin B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   492
\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
   493
\tdx{subset_refl}:  A \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   494
\tdx{subset_trans}: [| A \isasymsubseteq B;  B \isasymsubseteq C |] ==> A \isasymsubseteq C
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   495
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   496
\tdx{equalityI}:   [| A \isasymsubseteq B;  B \isasymsubseteq A |] ==> A = B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   497
\tdx{equalityD1}:  A = B ==> A \isasymsubseteq B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   498
\tdx{equalityD2}:  A = B ==> B \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   499
\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
   500
\subcaption{Subsets and extensionality}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   501
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   502
\tdx{emptyE}:        a \isasymin 0 ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   503
\tdx{empty_subsetI}:  0 \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   504
\tdx{equals0I}:      [| !!y. y \isasymin A ==> False |] ==> A=0
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   505
\tdx{equals0D}:      [| A=0;  a \isasymin A |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   506
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   507
\tdx{PowI}:          A \isasymsubseteq B ==> A \isasymin Pow(B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   508
\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
   509
\subcaption{The empty set; power sets}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   510
\end{alltt*}
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9584
diff changeset
   511
\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
   512
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   515
\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
   516
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
   517
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
   518
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
   519
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
   520
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
   521
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
   522
and use its derived rules instead.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   523
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   524
\subsection{Fundamental lemmas}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   525
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
   526
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
   527
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
   528
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
   529
  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
   530
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
   531
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
   532
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   533
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
   534
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
   535
power set operator.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   536
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   537
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
   538
The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   539
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
   540
separation is proved explicitly, although most proofs should use the
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   541
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
   542
\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
   543
\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
   544
particular circumstances.  Although too many rules can be confusing, there
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   545
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
   546
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   547
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
   548
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
   549
$\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
   550
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
   551
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
   552
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
   553
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
   554
similar premises.
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   557
%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
   558
\begin{figure}[p]
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   559
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   560
\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
   561
            b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   562
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   563
\tdx{ReplaceE}:   [| b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace};  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   564
               !!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
   565
            |] ==> R
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   566
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   567
\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
   568
\tdx{RepFunE}:    [| b\isasymin{}{\ttlbrace}f(x). x\isasymin{}A{\ttrbrace};  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   569
                !!x.[| x\isasymin{}A;  b=f(x) |] ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   570
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   571
\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
   572
\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
   573
\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
   574
\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
   575
\tdx{CollectD2}:   a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} ==> P(a)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   576
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   577
\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
   578
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   581
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   582
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   583
\tdx{UnionI}: [| B\isasymin{}C;  A\isasymin{}B |] ==> A\isasymin{}Union(C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   584
\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
   585
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   586
\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
   587
\tdx{InterD}: [| A\isasymin{}Inter(C);  B\isasymin{}C |] ==> A\isasymin{}B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   588
\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
   589
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   590
\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
   591
\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
   592
           |] ==> R
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   593
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   594
\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
   595
\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
   596
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   597
\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
   598
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   599
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   600
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   601
%%% upair.thy
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   602
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   603
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   604
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   605
\tdx{pairing}:   a\isasymin{}Upair(b,c) <-> (a=b | a=c)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   606
\tdx{UpairI1}:   a\isasymin{}Upair(a,b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   607
\tdx{UpairI2}:   b\isasymin{}Upair(a,b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   608
\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
   609
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   610
\caption{Unordered pairs} \label{zf-upair1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   611
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   614
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   615
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   616
\tdx{UnI1}:      c\isasymin{}A ==> c\isasymin{}A \isasymunion B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   617
\tdx{UnI2}:      c\isasymin{}B ==> c\isasymin{}A \isasymunion B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   618
\tdx{UnCI}:      (c \isasymnotin B ==> c\isasymin{}A) ==> c\isasymin{}A \isasymunion B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   619
\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
   620
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   621
\tdx{IntI}:      [| c\isasymin{}A;  c\isasymin{}B |] ==> c\isasymin{}A \isasyminter B
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   622
\tdx{IntD1}:     c\isasymin{}A \isasyminter B ==> c\isasymin{}A
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   623
\tdx{IntD2}:     c\isasymin{}A \isasyminter B ==> c\isasymin{}B
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   624
\tdx{IntE}:      [| c\isasymin{}A \isasyminter B;  [| c\isasymin{}A; c\isasymin{}B |] ==> P |] ==> P
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   625
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   626
\tdx{DiffI}:     [| c\isasymin{}A;  c \isasymnotin B |] ==> c\isasymin{}A - B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   627
\tdx{DiffD1}:    c\isasymin{}A - B ==> c\isasymin{}A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   628
\tdx{DiffD2}:    c\isasymin{}A - B ==> c  \isasymnotin  B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   629
\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
   630
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   631
\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
   632
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   635
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   636
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   637
\tdx{consI1}:    a\isasymin{}cons(a,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   638
\tdx{consI2}:    a\isasymin{}B ==> a\isasymin{}cons(b,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   639
\tdx{consCI}:    (a \isasymnotin B ==> a=b) ==> a\isasymin{}cons(b,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   640
\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
   641
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   642
\tdx{singletonI}:  a\isasymin{}{\ttlbrace}a{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   643
\tdx{singletonE}:  [| a\isasymin{}{\ttlbrace}b{\ttrbrace}; a=b ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   644
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   645
\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
   646
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   649
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   650
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   651
\tdx{succI1}:    i\isasymin{}succ(i)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   652
\tdx{succI2}:    i\isasymin{}j ==> i\isasymin{}succ(j)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   653
\tdx{succCI}:    (i \isasymnotin j ==> i=j) ==> i\isasymin{}succ(j)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   654
\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
   655
\tdx{succ_neq_0}:  [| succ(n)=0 |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   656
\tdx{succ_inject}: succ(m) = succ(n) ==> m=n
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   657
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   658
\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
   659
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   662
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   663
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   664
\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
   665
\tdx{theI}:         \isasymexists! x. P(x) ==> P(THE x. P(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   666
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   667
\tdx{if_P}:          P ==> (if P then a else b) = a
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   668
\tdx{if_not_P}:     ~P ==> (if P then a else b) = b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   669
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   670
\tdx{mem_asym}:     [| a\isasymin{}b;  b\isasymin{}a |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   671
\tdx{mem_irrefl}:   a\isasymin{}a ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   672
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   673
\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
   674
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   677
\subsection{Unordered pairs and finite sets}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   678
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
   679
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
   680
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
   681
rule \tdx{UnCI} is useful for classical reasoning about unions,
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   682
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
   683
\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
   684
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
   685
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
   686
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   687
Figure~\ref{zf-upair2} is concerned with finite sets: it presents rules
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   688
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
   689
sets.  Figure~\ref{zf-succ} presents derived rules for the successor
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   690
function, which is defined in terms of~\isa{cons}.  The proof that 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   691
\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
   692
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   693
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
   694
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
   695
(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
   696
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
   697
\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
   698
many examples of its use.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   699
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   700
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
   701
(\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
   702
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
   703
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   704
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   705
%%% subset.thy?
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   706
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   707
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   708
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   709
\tdx{Union_upper}:    B\isasymin{}A ==> B \isasymsubseteq Union(A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   710
\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
   711
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   712
\tdx{Inter_lower}:    B\isasymin{}A ==> Inter(A) \isasymsubseteq B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   713
\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
   714
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   715
\tdx{Un_upper1}:      A \isasymsubseteq A \isasymunion B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   716
\tdx{Un_upper2}:      B \isasymsubseteq A \isasymunion B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   717
\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
   718
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   719
\tdx{Int_lower1}:     A \isasyminter B \isasymsubseteq A
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   720
\tdx{Int_lower2}:     A \isasyminter B \isasymsubseteq B
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   721
\tdx{Int_greatest}:   [| C \isasymsubseteq A;  C \isasymsubseteq B |] ==> C \isasymsubseteq A \isasyminter B
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   722
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   723
\tdx{Diff_subset}:    A-B \isasymsubseteq A
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   724
\tdx{Diff_contains}:  [| C \isasymsubseteq A;  C \isasyminter B = 0 |] ==> C \isasymsubseteq A-B
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   725
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   726
\tdx{Collect_subset}: Collect(A,P) \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   727
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   728
\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
   729
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   732
\subsection{Subset and lattice properties}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   733
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
   734
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
   735
shows the corresponding rules.  A few other laws involving subsets are
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   736
included. 
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   737
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
   738
reasoning about the membership relation.  Section~\ref{sec:ZF-pow-example}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   739
below presents an example of this, proving the equation 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   740
${\isa{Pow}(A)\cap \isa{Pow}(B)}= \isa{Pow}(A\cap B)$.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   741
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   742
%%% pair.thy
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   743
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   744
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   745
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   746
\tdx{Pair_inject1}: <a,b> = <c,d> ==> a=c
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   747
\tdx{Pair_inject2}: <a,b> = <c,d> ==> b=d
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   748
\tdx{Pair_inject}:  [| <a,b> = <c,d>;  [| a=c; b=d |] ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   749
\tdx{Pair_neq_0}:   <a,b>=0 ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   750
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   751
\tdx{fst_conv}:     fst(<a,b>) = a
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   752
\tdx{snd_conv}:     snd(<a,b>) = b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   753
\tdx{split}:        split(\%x y. c(x,y), <a,b>) = c(a,b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   754
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   755
\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
   756
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   757
\tdx{SigmaE}:     [| c\isasymin{}Sigma(A,B);  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   758
                !!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
   759
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   760
\tdx{SigmaE2}:    [| <a,b>\isasymin{}Sigma(A,B);    
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   761
                [| a\isasymin{}A;  b\isasymin{}B(a) |] ==> P   |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   762
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   763
\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
   764
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   767
\subsection{Ordered pairs} \label{sec:pairs}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   768
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   769
Figure~\ref{zf-pair} presents the rules governing ordered pairs,
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   770
projections and general sums --- in particular, that
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   771
$\{\{a\},\{a,b\}\}$ functions as an ordered pair.  This property is
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   772
expressed as two destruction rules,
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   773
\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
   774
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
   775
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   776
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
   777
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
   778
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
   779
satisfy $\pair{\emptyset;\emptyset}=\emptyset$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   780
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   781
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
   782
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
   783
$\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
   784
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
   785
$b\in B(a)$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   786
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   787
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
   788
\begin{center}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   789
{\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
   790
\end{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   791
Nested patterns are translated recursively:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   792
{\tt\%<$x$,$y$,$z$>. $t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>. $t$} $\leadsto$
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   793
\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
   794
  $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
   795
\begin{warn}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   796
  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
   797
  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
   798
  may differ, which affects proofs.  For example the term \isa{(\%<x,y>.<y,x>)<a,b>} requires the theorem \isa{split} to rewrite to
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   799
  {\tt<b,a>}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   800
\end{warn}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   801
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
   802
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
   803
$\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
   804
\begin{description}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   805
\item[Let:] \isa{let {\it pattern} = $t$ in $u$}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   806
\item[Choice:] \isa{THE~{\it pattern}~.~$P$}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   807
\item[Set operations:] \isa{\isasymUnion~{\it pattern}:$A$.~$B$}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   808
\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
   809
\end{description}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   810
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   811
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   812
%%% domrange.thy?
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   813
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   814
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   815
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   816
\tdx{domainI}:     <a,b>\isasymin{}r ==> a\isasymin{}domain(r)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   817
\tdx{domainE}:     [| a\isasymin{}domain(r); !!y. <a,y>\isasymin{}r ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   818
\tdx{domain_subset}: domain(Sigma(A,B)) \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   819
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   820
\tdx{rangeI}:      <a,b>\isasymin{}r ==> b\isasymin{}range(r)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   821
\tdx{rangeE}:      [| b\isasymin{}range(r); !!x. <x,b>\isasymin{}r ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   822
\tdx{range_subset}: range(A*B) \isasymsubseteq B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   823
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   824
\tdx{fieldI1}:     <a,b>\isasymin{}r ==> a\isasymin{}field(r)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   825
\tdx{fieldI2}:     <a,b>\isasymin{}r ==> b\isasymin{}field(r)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   826
\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
   827
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   828
\tdx{fieldE}:      [| a\isasymin{}field(r); 
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   829
                !!x. <a,x>\isasymin{}r ==> P; 
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   830
                !!x. <x,a>\isasymin{}r ==> P      
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   831
             |] ==> P
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   832
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   833
\tdx{field_subset}:  field(A*A) \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   834
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   835
\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
   836
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   837
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   838
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   839
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   840
\tdx{imageI}:      [| <a,b>\isasymin{}r; a\isasymin{}A |] ==> b\isasymin{}r``A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   841
\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
   842
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   843
\tdx{vimageI}:     [| <a,b>\isasymin{}r; b\isasymin{}B |] ==> a\isasymin{}r-``B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   844
\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
   845
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   846
\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
   847
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   848
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   849
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   850
\subsection{Relations}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   851
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
   852
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
   853
$\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
   854
{\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
   855
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
   856
\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
   857
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
   858
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
   859
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   860
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
   861
Note that these operations are generalisations of range and domain,
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   862
respectively. 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   863
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   864
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   865
%%% func.thy
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   866
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   867
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   868
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   869
\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
   870
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   871
\tdx{apply_equality}:  [| <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) |] ==> f`a = b
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   872
\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
   873
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   874
\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
   875
\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
   876
\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
   877
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   878
\tdx{fun_extension}:  [| f\isasymin{}Pi(A,B); g\isasymin{}Pi(A,D);
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   879
                   !!x. x\isasymin{}A ==> f`x = g`x     |] ==> f=g
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   880
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   881
\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
   882
\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
   883
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   884
\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
   885
\tdx{domain_of_fun}:  f\isasymin{}Pi(A,B) ==> domain(f)=A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   886
\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
   887
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   888
\tdx{restrict}:       a\isasymin{}A ==> restrict(f,A) ` a = f`a
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   889
\tdx{restrict_type}:  [| !!x. x\isasymin{}A ==> f`x\isasymin{}B(x) |] ==> 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   890
                restrict(f,A)\isasymin{}Pi(A,B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   891
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   892
\caption{Functions} \label{zf-func1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   893
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   896
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   897
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   898
\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
   899
\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
   900
          |] ==>  P
3fc32155372c fixed some overfull lines
paulson
parents: 6745
diff changeset
   901
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   902
\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
   903
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   904
\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
   905
\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
   906
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   907
\caption{$\lambda$-abstraction} \label{zf-lam}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   908
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   911
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   912
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   913
\tdx{fun_empty}:           0\isasymin{}0->0
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   914
\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
   915
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   916
\tdx{fun_disjoint_Un}:     [| f\isasymin{}A->B; g\isasymin{}C->D; A \isasyminter C = 0  |] ==>  
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   917
                     (f \isasymunion g)\isasymin{}(A \isasymunion C) -> (B \isasymunion D)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   918
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   919
\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
   920
                     (f \isasymunion g)`a = f`a
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   921
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   922
\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
   923
                     (f \isasymunion g)`c = g`c
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   924
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   925
\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
   926
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   929
\subsection{Functions}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   930
Functions, represented by graphs, are notoriously difficult to reason
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   931
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
   932
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
   933
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   934
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
   935
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
   936
$\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
   937
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
   938
(\tdx{fun_extension}).
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   939
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   940
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
   941
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
   942
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
   943
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
   944
$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
   945
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   946
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
   947
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
   948
\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
   949
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
   950
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   951
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
   952
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
   953
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
   954
disjoint.  
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   957
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   958
\begin{alltt*}\isastyleminor
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   959
\tdx{Int_absorb}:        A \isasyminter A = A
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   960
\tdx{Int_commute}:       A \isasyminter B = B \isasyminter A
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   961
\tdx{Int_assoc}:         (A \isasyminter B) \isasyminter C  =  A \isasyminter (B \isasyminter C)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   962
\tdx{Int_Un_distrib}:    (A \isasymunion B) \isasyminter C  =  (A \isasyminter C) \isasymunion (B \isasyminter C)
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   963
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   964
\tdx{Un_absorb}:         A \isasymunion A = A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   965
\tdx{Un_commute}:        A \isasymunion B = B \isasymunion A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   966
\tdx{Un_assoc}:          (A \isasymunion B) \isasymunion C  =  A \isasymunion (B \isasymunion C)
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   967
\tdx{Un_Int_distrib}:    (A \isasyminter B) \isasymunion C  =  (A \isasymunion C) \isasyminter (B \isasymunion C)
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   968
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   969
\tdx{Diff_cancel}:       A-A = 0
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   970
\tdx{Diff_disjoint}:     A \isasyminter (B-A) = 0
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   971
\tdx{Diff_partition}:    A \isasymsubseteq B ==> A \isasymunion (B-A) = B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   972
\tdx{double_complement}: [| A \isasymsubseteq B; B \isasymsubseteq C |] ==> (B - (C-A)) = A
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   973
\tdx{Diff_Un}:           A - (B \isasymunion C) = (A-B) \isasyminter (A-C)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   974
\tdx{Diff_Int}:          A - (B \isasyminter C) = (A-B) \isasymunion (A-C)
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   975
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   976
\tdx{Union_Un_distrib}:  Union(A \isasymunion B) = Union(A) \isasymunion Union(B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   977
\tdx{Inter_Un_distrib}:  [| a \isasymin A;  b \isasymin B |] ==> 
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   978
                   Inter(A \isasymunion B) = Inter(A) \isasyminter Inter(B)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   979
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   980
\tdx{Int_Union_RepFun}:  A \isasyminter Union(B) = ({\isasymUnion}C \isasymin B. A \isasyminter C)
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   981
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   982
\tdx{Un_Inter_RepFun}:   b \isasymin B ==> 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   983
                   A \isasymunion Inter(B) = ({\isasymInter}C \isasymin B. A \isasymunion C)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   984
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   985
\tdx{SUM_Un_distrib1}:   (SUM x \isasymin A \isasymunion B. C(x)) = 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   986
                   (SUM x \isasymin A. C(x)) \isasymunion (SUM x \isasymin B. C(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   987
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   988
\tdx{SUM_Un_distrib2}:   (SUM x \isasymin C. A(x) \isasymunion B(x)) =
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   989
                   (SUM x \isasymin C. A(x)) \isasymunion (SUM x \isasymin C. B(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   990
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   991
\tdx{SUM_Int_distrib1}:  (SUM x \isasymin A \isasyminter B. C(x)) =
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   992
                   (SUM x \isasymin A. C(x)) \isasyminter (SUM x \isasymin B. C(x))
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   993
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   994
\tdx{SUM_Int_distrib2}:  (SUM x \isasymin C. A(x) \isasyminter B(x)) =
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
   995
                   (SUM x \isasymin C. A(x)) \isasyminter (SUM x \isasymin C. B(x))
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
   996
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   997
\caption{Equalities} \label{zf-equalities}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   998
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1001
\begin{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1002
%\begin{constants} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1003
%  \cdx{1}       & $i$           &       & $\{\emptyset\}$       \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1004
%  \cdx{bool}    & $i$           &       & the set $\{\emptyset,1\}$     \\
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1005
%  \cdx{cond}   & $[i,i,i]\To i$ &       & conditional for \isa{bool}    \\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1006
%  \cdx{not}    & $i\To i$       &       & negation for \isa{bool}       \\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1007
%  \sdx{and}    & $[i,i]\To i$   & Left 70 & conjunction for \isa{bool}  \\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1008
%  \sdx{or}     & $[i,i]\To i$   & Left 65 & disjunction for \isa{bool}  \\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1009
%  \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
  1010
%\end{constants}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1011
%
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1012
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1013
\tdx{bool_def}:      bool == {\ttlbrace}0,1{\ttrbrace}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1014
\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
  1015
\tdx{not_def}:       not(b)  == cond(b,0,1)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1016
\tdx{and_def}:       a and b == cond(a,b,0)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1017
\tdx{or_def}:        a or b  == cond(a,1,b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1018
\tdx{xor_def}:       a xor b == cond(a,not(b),b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1019
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1020
\tdx{bool_1I}:       1 \isasymin bool
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1021
\tdx{bool_0I}:       0 \isasymin bool
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1022
\tdx{boolE}:         [| c \isasymin bool;  c=1 ==> P;  c=0 ==> P |] ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1023
\tdx{cond_1}:        cond(1,c,d) = c
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1024
\tdx{cond_0}:        cond(0,c,d) = d
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1025
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1026
\caption{The booleans} \label{zf-bool}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1027
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1030
\section{Further developments}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1031
The next group of developments is complex and extensive, and only
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1032
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
  1033
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1034
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
  1035
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
  1036
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1037
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
  1038
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
  1039
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
  1040
\isa{bool}-valued functions, for example.  The constant~\isa{1} is
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1041
translated to \isa{succ(0)}.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1042
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1043
\begin{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1044
\index{*"+ symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1045
\begin{constants}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1046
  \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
  1047
  \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
  1048
  \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
  1049
  \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
  1050
\end{constants}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1051
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1052
\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
  1053
\tdx{Inl_def}:   Inl(a) == <0,a>
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1054
\tdx{Inr_def}:   Inr(b) == <1,b>
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1055
\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
  1056
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1057
\tdx{InlI}:      a \isasymin A ==> Inl(a) \isasymin A+B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1058
\tdx{InrI}:      b \isasymin B ==> Inr(b) \isasymin A+B
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1059
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1060
\tdx{Inl_inject}:  Inl(a)=Inl(b) ==> a=b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1061
\tdx{Inr_inject}:  Inr(a)=Inr(b) ==> a=b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1062
\tdx{Inl_neq_Inr}: Inl(a)=Inr(b) ==> P
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1063
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1064
\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
  1065
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1066
\tdx{case_Inl}:  case(c,d,Inl(a)) = c(a)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1067
\tdx{case_Inr}:  case(c,d,Inr(b)) = d(b)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1068
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1069
\caption{Disjoint unions} \label{zf-sum}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1070
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1071
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1072
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1073
\subsection{Disjoint unions}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1074
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1075
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
  1076
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
  1077
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
  1078
mutual recursion~\cite{paulson-set-II}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1079
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1080
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1081
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1082
\tdx{QPair_def}:      <a;b> == a+b
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1083
\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
  1084
\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
  1085
\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
  1086
\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
  1087
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1088
\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
  1089
\tdx{QInl_def}:       QInl(a)      == <0;a>
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1090
\tdx{QInr_def}:       QInr(b)      == <1;b>
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1091
\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
  1092
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1093
\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
  1094
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1095
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1096
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1097
\subsection{Non-standard ordered pairs}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1098
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1099
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
  1100
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
  1101
{\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
  1102
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
  1103
\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
  1104
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
  1105
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
  1106
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
  1107
addition, {\tt<$a$;$b$>} is continuous.  The theory supports coinductive
6592
c120262044b6 Now uses manual.bib; some references updated
paulson
parents: 6173
diff changeset
  1108
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
  1109
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1110
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1111
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1112
\tdx{bnd_mono_def}:  bnd_mono(D,h) == 
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1113
               h(D)\isasymsubseteq{}D & ({\isasymforall}W X. W\isasymsubseteq{}X --> X\isasymsubseteq{}D --> h(W)\isasymsubseteq{}h(X))
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1114
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1115
\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
  1116
\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
  1117
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1118
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1119
\tdx{lfp_lowerbound}: [| h(A) \isasymsubseteq A;  A \isasymsubseteq D |] ==> lfp(D,h) \isasymsubseteq A
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1120
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1121
\tdx{lfp_subset}:    lfp(D,h) \isasymsubseteq D
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1122
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1123
\tdx{lfp_greatest}:  [| bnd_mono(D,h);  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1124
                  !!X. [| h(X) \isasymsubseteq X;  X \isasymsubseteq D |] ==> A \isasymsubseteq X 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1125
               |] ==> A \isasymsubseteq lfp(D,h)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1126
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1127
\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
  1128
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1129
\tdx{induct}:        [| a \isasymin lfp(D,h);  bnd_mono(D,h);
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1130
                  !!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
  1131
               |] ==> P(a)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1132
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1133
\tdx{lfp_mono}:      [| bnd_mono(D,h);  bnd_mono(E,i);
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1134
                  !!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X)  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1135
               |] ==> lfp(D,h) \isasymsubseteq lfp(E,i)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1136
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1137
\tdx{gfp_upperbound}: [| A \isasymsubseteq h(A);  A \isasymsubseteq D |] ==> A \isasymsubseteq gfp(D,h)
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1138
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1139
\tdx{gfp_subset}:    gfp(D,h) \isasymsubseteq D
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1140
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1141
\tdx{gfp_least}:     [| bnd_mono(D,h);  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1142
                  !!X. [| X \isasymsubseteq h(X);  X \isasymsubseteq D |] ==> X \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1143
               |] ==> gfp(D,h) \isasymsubseteq A
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1144
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1145
\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
  1146
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1147
\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
  1148
               |] ==> a \isasymin gfp(D,h)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1149
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1150
\tdx{gfp_mono}:      [| bnd_mono(D,h);  D \isasymsubseteq E;
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1151
                  !!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X)  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1152
               |] ==> gfp(D,h) \isasymsubseteq gfp(E,i)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1153
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1154
\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
  1155
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1156
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1157
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1158
\subsection{Least and greatest fixedpoints}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1159
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1160
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
  1161
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
  1162
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
  1163
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
  1164
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
  1165
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
  1166
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
  1167
package also uses the fixedpoint operators~\cite{paulson-CADE}.  See
6745
74e8f703f5f2 tuned manual.bib;
wenzelm
parents: 6592
diff changeset
  1168
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
  1169
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
  1170
proofs.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1171
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1172
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
  1173
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
  1174
are useful for applying the Knaster-Tarski Fixedpoint Theorem.  The proofs
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1175
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
  1176
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1177
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1178
\subsection{Finite sets and lists}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1179
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1180
Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines the finite set operator;
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1181
$\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
  1182
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
  1183
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
  1184
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
  1185
between two given sets.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1186
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1187
\begin{figure}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1188
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1189
\tdx{Fin.emptyI}      0 \isasymin Fin(A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1190
\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
  1191
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1192
\tdx{Fin_induct}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1193
    [| b \isasymin Fin(A);
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1194
       P(0);
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1195
       !!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
  1196
    |] ==> P(b)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1197
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1198
\tdx{Fin_mono}:       A \isasymsubseteq B ==> Fin(A) \isasymsubseteq Fin(B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1199
\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
  1200
\tdx{Fin_UnionI}:     C \isasymin Fin(Fin(A)) ==> Union(C) \isasymin Fin(A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1201
\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
  1202
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1203
\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
  1204
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1205
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1206
\begin{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1207
\begin{constants}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1208
  \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
  1209
  \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
  1210
  \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
  1211
  \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
  1212
  \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
  1213
  \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
  1214
  \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
  1215
  \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
  1216
\end{constants}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1217
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1218
\underscoreon %%because @ is used here
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1219
\begin{alltt*}\isastyleminor
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1220
\tdx{NilI}:       Nil \isasymin list(A)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1221
\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
  1222
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1223
\tdx{List.induct}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1224
    [| l \isasymin list(A);
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1225
       P(Nil);
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1226
       !!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
  1227
    |] ==> P(l)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1228
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1229
\tdx{Cons_iff}:       Cons(a,l)=Cons(a',l') <-> a=a' & l=l'
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1230
\tdx{Nil_Cons_iff}:    Nil \isasymnoteq Cons(a,l)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1231
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1232
\tdx{list_mono}:      A \isasymsubseteq B ==> list(A) \isasymsubseteq list(B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1233
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1234
\tdx{map_ident}:      l\isasymin{}list(A) ==> map(\%u. u, l) = l
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1235
\tdx{map_compose}:    l\isasymin{}list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1236
\tdx{map_app_distrib}: xs\isasymin{}list(A) ==> map(h, xs@ys) = map(h,xs)@map(h,ys)
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1237
\tdx{map_type}
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1238
    [| 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
  1239
\tdx{map_flat}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1240
    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
  1241
\end{alltt*}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1242
\caption{Lists} \label{zf-list}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1243
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1244
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1245
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1246
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
  1247
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
  1248
and induction rules automatically, as well as the constructors, case operator
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1249
(\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
  1250
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
  1251
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
  1252
9584
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1253
\subsection{Miscellaneous}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1254
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1255
\begin{figure}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1256
\begin{constants} 
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1257
  \it symbol  & \it meta-type & \it priority & \it description \\ 
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1258
  \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
  1259
  \cdx{id}      & $i\To i$      &       & identity function \\
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1260
  \cdx{inj}     & $[i,i]\To i$  &       & injective function space\\
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1261
  \cdx{surj}    & $[i,i]\To i$  &       & surjective function space\\
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1262
  \cdx{bij}     & $[i,i]\To i$  &       & bijective function space
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1263
\end{constants}
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1264
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1265
\begin{alltt*}\isastyleminor
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1266
\tdx{comp_def}: r O s     == {\ttlbrace}xz \isasymin domain(s)*range(r) . 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9836
diff changeset
  1267
                        {\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
  1268
\tdx{id_def}:   id(A)     == (lam x \isasymin A. x)
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1269
\tdx{inj_def}:  inj(A,B)  == {\ttlbrace} f\isasymin{}A->B. {\isasymforall}w\isasymin{}A. {\isasymforall}x\isasymin{}A. f`w=f`x --> w=x {\ttrbrace}
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1270
\tdx{surj_def}: surj(A,B) == {\ttlbrace} f\isasymin{}A->B . {\isasymforall}y\isasymin{}B. {\isasymexists}x\isasymin{}A. f`x=y {\ttrbrace}
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1271
\tdx{bij_def}:  bij(A,B)  == inj(A,B) \isasyminter surj(A,B)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1272
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1273
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1274
\tdx{left_inverse}:    [| f\isasymin{}inj(A,B);  a\isasymin{}A |] ==> converse(f)`(f`a) = a
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1275
\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
  1276
                 f`(converse(f)`b) = b
af21f4364c05 documented the integers and updated section on nat arithmetic
paulson
parents: 8249
diff changeset
  1277
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1278
\tdx{inj_converse_inj}: f\isasymin{}inj(A,B) ==> converse(f) \isasymin inj(range(f),A)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1279
\tdx{bij_converse_bij}: f\isasymin{}bij(A,B) ==> converse(f) \isasymin bij(B,A)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1280
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1281
\tdx{comp_type}:     [| s \isasymsubseteq A*B;  r \isasymsubseteq B*C |] ==> (r O s) \isasymsubseteq A*C
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1282
\tdx{comp_assoc}:    (r O s) O t = r O (s O t)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1283
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1284
\tdx{left_comp_id}:  r \isasymsubseteq A*B ==> id(B) O r = r
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1285
\tdx{right_comp_id}: r \isasymsubseteq A*B ==> r O id(A) = r
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1286
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1287
\tdx{comp_func}:     [| g\isasymin{}A->B; f\isasymin{}B->C |] ==> (f O g) \isasymin A->C
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
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)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1289
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1290
\tdx{comp_inj}:      [| g\isasymin{}inj(A,B);  f\isasymin{}inj(B,C)  |] ==> (f O g)\isasymin{}inj(A,C)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1291
\tdx{comp_surj}:     [| g\isasymin{}surj(A,B); f\isasymin{}surj(B,C) |] ==> (f O g)\isasymin{}surj(A,C)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1292
\tdx{comp_bij}:      [| g\isasymin{}bij(A,B); f\isasymin{}bij(B,C) |] ==> (f O g)\isasymin{}bij(A,C)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1293
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1294
\tdx{left_comp_inverse}:    f\isasymin{}inj(A,B) ==> converse(f) O f = id(A)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1295
\tdx{right_comp_inverse}:   f\isasymin{}surj(A,B) ==> f O converse(f) = id(B)
14154
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}:  
14158
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1298
    [| f\isasymin{}bij(A,B);  g\isasymin{}bij(C,D);  A \isasyminter C = 0;  B \isasyminter D = 0 |] ==> 
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1299
    (f \isasymunion g)\isasymin{}bij(A \isasymunion C, B \isasymunion D)
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1300
15bab630ae31 finished conversion to Isar format
paulson
parents: 14154
diff changeset
  1301
\tdx{restrict_bij}: [| f\isasymin{}inj(A,B); C\isasymsubseteq{}A |] ==> restrict(f,C)\isasymin{}bij(C, f``C)
14154
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
diff changeset
  1373
\begin{ttbox}\isastyleminor
14158
15bab630ae31 finished