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