author  boehmes 
Tue, 07 Dec 2010 15:44:38 +0100  
changeset 41064  0c447a17770a 
parent 28871  111bbd2b12db 
child 42619  9691759a9b3c 
permissions  rwrr 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1 
%% $Id$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

2 
\chapter{ZermeloFraenkel Set Theory} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

3 
\index{set theory(} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

4 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

5 
The theory~\thydx{ZF} implements ZermeloFraenkel set 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

6 
theory~\cite{halmos60,suppes72} as an extension of~\texttt{FOL}, classical 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

7 
firstorder logic. The theory includes a collection of derived natural 
14154  8 
deduction rules, for use with Isabelle's classical reasoner. Some 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

9 
of it is based on the work of No\"el~\cite{noel}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

10 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

11 
A tremendous amount of set theory has been formally developed, including the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

12 
basic properties of relations, functions, ordinals and cardinals. Significant 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

13 
results have been proved, such as the Schr\"oderBernstein Theorem, the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

14 
Wellordering Theorem and a version of Ramsey's Theorem. \texttt{ZF} provides 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

15 
both the integers and the natural numbers. General methods have been 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

16 
developed for solving recursion equations over monotonic functors; these have 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

17 
been applied to yield constructions of lists, trees, infinite lists, etc. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

18 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

19 
\texttt{ZF} has a flexible package for handling inductive definitions, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

20 
such as inference systems, and datatype definitions, such as lists and 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

21 
trees. Moreover it handles coinductive definitions, such as 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

22 
bisimulation relations, and codatatype definitions, such as streams. It 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

23 
provides a streamlined syntax for defining primitive recursive functions over 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

24 
datatypes. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

25 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

26 
Published articles~\cite{paulsonsetI,paulsonsetII} describe \texttt{ZF} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

27 
less formally than this chapter. Isabelle employs a novel treatment of 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

28 
nonwellfounded data structures within the standard {\sc zf} axioms including 
6592  29 
the Axiom of Foundation~\cite{paulsonmscs}. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

30 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

31 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

32 
\section{Which version of axiomatic set theory?} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

33 
The two main axiom systems for set theory are BernaysG\"odel~({\sc bg}) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

34 
and ZermeloFraenkel~({\sc zf}). Resolution theorem provers can use {\sc 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

35 
bg} because it is finite~\cite{boyer86,quaife92}. {\sc zf} does not 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

36 
have a finite axiom system because of its Axiom Scheme of Replacement. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

37 
This makes it awkward to use with many theorem provers, since instances 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

38 
of the axiom scheme have to be invoked explicitly. Since Isabelle has no 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

39 
difficulty with axiom schemes, we may adopt either axiom system. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

40 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

41 
These two theories differ in their treatment of {\bf classes}, which are 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

42 
collections that are `too big' to be sets. The class of all sets,~$V$, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

43 
cannot be a set without admitting Russell's Paradox. In {\sc bg}, both 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

44 
classes and sets are individuals; $x\in V$ expresses that $x$ is a set. In 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

45 
{\sc zf}, all variables denote sets; classes are identified with unary 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

46 
predicates. The two systems define essentially the same sets and classes, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

47 
with similar properties. In particular, a class cannot belong to another 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

48 
class (let alone a set). 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

49 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

50 
Modern set theorists tend to prefer {\sc zf} because they are mainly concerned 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

51 
with sets, rather than classes. {\sc bg} requires tiresome proofs that various 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

52 
collections are sets; for instance, showing $x\in\{x\}$ requires showing that 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

53 
$x$ is a set. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

54 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

55 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

56 
\begin{figure} \small 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

57 
\begin{center} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

58 
\begin{tabular}{rrr} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

59 
\it name &\it metatype & \it description \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

60 
\cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

61 
\cdx{0} & $i$ & empty set\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

62 
\cdx{cons} & $[i,i]\To i$ & finite set constructor\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

63 
\cdx{Upair} & $[i,i]\To i$ & unordered pairing\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

64 
\cdx{Pair} & $[i,i]\To i$ & ordered pairing\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

65 
\cdx{Inf} & $i$ & infinite set\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

66 
\cdx{Pow} & $i\To i$ & powerset\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

67 
\cdx{Union} \cdx{Inter} & $i\To i$ & set union/intersection \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

68 
\cdx{split} & $[[i,i]\To i, i] \To i$ & generalized projection\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

69 
\cdx{fst} \cdx{snd} & $i\To i$ & projections\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

70 
\cdx{converse}& $i\To i$ & converse of a relation\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

71 
\cdx{succ} & $i\To i$ & successor\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

72 
\cdx{Collect} & $[i,i\To o]\To i$ & separation\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

73 
\cdx{Replace} & $[i, [i,i]\To o] \To i$ & replacement\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

74 
\cdx{PrimReplace} & $[i, [i,i]\To o] \To i$ & primitive replacement\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

75 
\cdx{RepFun} & $[i, i\To i] \To i$ & functional replacement\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

76 
\cdx{Pi} \cdx{Sigma} & $[i,i\To i]\To i$ & general product/sum\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

77 
\cdx{domain} & $i\To i$ & domain of a relation\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

78 
\cdx{range} & $i\To i$ & range of a relation\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

79 
\cdx{field} & $i\To i$ & field of a relation\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

80 
\cdx{Lambda} & $[i, i\To i]\To i$ & $\lambda$abstraction\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

81 
\cdx{restrict}& $[i, i] \To i$ & restriction of a function\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

82 
\cdx{The} & $[i\To o]\To i$ & definite description\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

83 
\cdx{if} & $[o,i,i]\To i$ & conditional\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

84 
\cdx{Ball} \cdx{Bex} & $[i, i\To o]\To o$ & bounded quantifiers 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

85 
\end{tabular} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

86 
\end{center} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

87 
\subcaption{Constants} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

88 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

89 
\begin{center} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

90 
\index{*"`"` symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

91 
\index{*""`"` symbol} 
9836
56b632fd1dcd
simplified two index entries, since now ZF is by itself
paulson
parents:
9695
diff
changeset

92 
\index{*"` symbol}\index{function applications} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

93 
\index{*" symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

94 
\index{*": symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

95 
\index{*"<"= symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

96 
\begin{tabular}{rrrr} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

97 
\it symbol & \it metatype & \it priority & \it description \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

98 
\tt `` & $[i,i]\To i$ & Left 90 & image \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

99 
\tt `` & $[i,i]\To i$ & Left 90 & inverse image \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

100 
\tt ` & $[i,i]\To i$ & Left 90 & application \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

101 
\sdx{Int} & $[i,i]\To i$ & Left 70 & intersection ($\int$) \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

102 
\sdx{Un} & $[i,i]\To i$ & Left 65 & union ($\un$) \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

103 
\tt  & $[i,i]\To i$ & Left 65 & set difference ($$) \\[1ex] 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

104 
\tt: & $[i,i]\To o$ & Left 50 & membership ($\in$) \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

105 
\tt <= & $[i,i]\To o$ & Left 50 & subset ($\subseteq$) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

106 
\end{tabular} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

107 
\end{center} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

108 
\subcaption{Infixes} 
9695  109 
\caption{Constants of ZF} \label{zfconstants} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

110 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

111 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

112 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

113 
\section{The syntax of set theory} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

114 
The language of set theory, as studied by logicians, has no constants. The 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

115 
traditional axioms merely assert the existence of empty sets, unions, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

116 
powersets, etc.; this would be intolerable for practical reasoning. The 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

117 
Isabelle theory declares constants for primitive sets. It also extends 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

118 
\texttt{FOL} with additional syntax for finite sets, ordered pairs, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

119 
comprehension, general union/intersection, general sums/products, and 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

120 
bounded quantifiers. In most other respects, Isabelle implements precisely 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

121 
ZermeloFraenkel set theory. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

122 

9695  123 
Figure~\ref{zfconstants} lists the constants and infixes of~ZF, while 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

124 
Figure~\ref{zftrans} presents the syntax translations. Finally, 
9695  125 
Figure~\ref{zfsyntax} presents the full grammar for set theory, including the 
126 
constructs of FOL. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

127 

14154  128 
Local abbreviations can be introduced by a \isa{let} construct whose 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

129 
syntax appears in Fig.\ts\ref{zfsyntax}. Internally it is translated into 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

130 
the constant~\cdx{Let}. It can be expanded by rewriting with its 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

131 
definition, \tdx{Let_def}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

132 

14154  133 
Apart from \isa{let}, set theory does not use polymorphism. All terms in 
134 
ZF have type~\tydx{i}, which is the type of individuals and has 

135 
class~\cldx{term}. The type of firstorder formulae, remember, 

136 
is~\tydx{o}. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

137 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

138 
Infix operators include binary union and intersection ($A\un B$ and 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

139 
$A\int B$), set difference ($AB$), and the subset and membership 
14154  140 
relations. Note that $a$\verb~:$b$ is translated to $\lnot(a\in b)$, 
141 
which is equivalent to $a\notin b$. The 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

142 
union and intersection operators ($\bigcup A$ and $\bigcap A$) form the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

143 
union or intersection of a set of sets; $\bigcup A$ means the same as 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

144 
$\bigcup@{x\in A}x$. Of these operators, only $\bigcup A$ is primitive. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

145 

14154  146 
The constant \cdx{Upair} constructs unordered pairs; thus \isa{Upair($A$,$B$)} denotes the set~$\{A,B\}$ and 
147 
\isa{Upair($A$,$A$)} denotes the singleton~$\{A\}$. General union is 

148 
used to define binary union. The Isabelle version goes on to define 

149 
the constant 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

150 
\cdx{cons}: 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

151 
\begin{eqnarray*} 
14154  152 
A\cup B & \equiv & \bigcup(\isa{Upair}(A,B)) \\ 
153 
\isa{cons}(a,B) & \equiv & \isa{Upair}(a,a) \un B 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

154 
\end{eqnarray*} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

155 
The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the 
14154  156 
obvious manner using~\isa{cons} and~$\emptyset$ (the empty set) \isasymin \begin{eqnarray*} 
157 
\{a,b,c\} & \equiv & \isa{cons}(a,\isa{cons}(b,\isa{cons}(c,\emptyset))) 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

158 
\end{eqnarray*} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

159 

14154  160 
The constant \cdx{Pair} constructs ordered pairs, as in \isa{Pair($a$,$b$)}. Ordered pairs may also be written within angle brackets, 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

161 
as {\tt<$a$,$b$>}. The $n$tuple {\tt<$a@1$,\ldots,$a@{n1}$,$a@n$>} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

162 
abbreviates the nest of pairs\par\nobreak 
14154  163 
\centerline{\isa{Pair($a@1$,\ldots,Pair($a@{n1}$,$a@n$)\ldots).}} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

164 

9695  165 
In ZF, a function is a set of pairs. A ZF function~$f$ is simply an 
166 
individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say 

167 
$i\To i$. The infix operator~{\tt`} denotes the application of a function set 

168 
to its argument; we must write~$f{\tt`}x$, not~$f(x)$. The syntax for image 

169 
is~$f{\tt``}A$ and that for inverse image is~$f{\tt``}A$. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

170 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

171 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

172 
\begin{figure} 
9836
56b632fd1dcd
simplified two index entries, since now ZF is by itself
paulson
parents:
9695
diff
changeset

173 
\index{lambda abs@$\lambda$abstractions} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

174 
\index{*""> symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

175 
\index{*"* symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

176 
\begin{center} \footnotesize\tt\frenchspacing 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

177 
\begin{tabular}{rrr} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

178 
\it external & \it internal & \it description \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

179 
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

180 
\ttlbrace$a@1$, $\ldots$, $a@n$\ttrbrace & cons($a@1$,$\ldots$,cons($a@n$,0)) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

181 
\rm finite set \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

182 
<$a@1$, $\ldots$, $a@{n1}$, $a@n$> & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

183 
Pair($a@1$,\ldots,Pair($a@{n1}$,$a@n$)\ldots) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

184 
\rm ordered $n$tuple \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

185 
\ttlbrace$x$:$A . P[x]$\ttrbrace & Collect($A$,$\lambda x. P[x]$) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

186 
\rm separation \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

187 
\ttlbrace$y . x$:$A$, $Q[x,y]$\ttrbrace & Replace($A$,$\lambda x\,y. Q[x,y]$) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

188 
\rm replacement \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

189 
\ttlbrace$b[x] . x$:$A$\ttrbrace & RepFun($A$,$\lambda x. b[x]$) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

190 
\rm functional replacement \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

191 
\sdx{INT} $x$:$A . B[x]$ & Inter(\ttlbrace$B[x] . x$:$A$\ttrbrace) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

192 
\rm general intersection \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

193 
\sdx{UN} $x$:$A . B[x]$ & Union(\ttlbrace$B[x] . x$:$A$\ttrbrace) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

194 
\rm general union \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

195 
\sdx{PROD} $x$:$A . B[x]$ & Pi($A$,$\lambda x. B[x]$) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

196 
\rm general product \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

197 
\sdx{SUM} $x$:$A . B[x]$ & Sigma($A$,$\lambda x. B[x]$) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

198 
\rm general sum \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

199 
$A$ > $B$ & Pi($A$,$\lambda x. B$) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

200 
\rm function space \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

201 
$A$ * $B$ & Sigma($A$,$\lambda x. B$) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

202 
\rm binary product \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

203 
\sdx{THE} $x . P[x]$ & The($\lambda x. P[x]$) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

204 
\rm definite description \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

205 
\sdx{lam} $x$:$A . b[x]$ & Lambda($A$,$\lambda x. b[x]$) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

206 
\rm $\lambda$abstraction\\[1ex] 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

207 
\sdx{ALL} $x$:$A . P[x]$ & Ball($A$,$\lambda x. P[x]$) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

208 
\rm bounded $\forall$ \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

209 
\sdx{EX} $x$:$A . P[x]$ & Bex($A$,$\lambda x. P[x]$) & 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

210 
\rm bounded $\exists$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

211 
\end{tabular} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

212 
\end{center} 
9695  213 
\caption{Translations for ZF} \label{zftrans} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

214 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

215 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

216 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

217 
\begin{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

218 
\index{*let symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

219 
\index{*in symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

220 
\dquotes 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

221 
\[\begin{array}{rcl} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

222 
term & = & \hbox{expression of type~$i$} \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

223 
&  & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

224 
&  & "if"~term~"then"~term~"else"~term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

225 
&  & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

226 
&  & "< " term\; ("," term)^* " >" \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

227 
&  & "{\ttlbrace} " id ":" term " . " formula " {\ttrbrace}" \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

228 
&  & "{\ttlbrace} " id " . " id ":" term ", " formula " {\ttrbrace}" \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

229 
&  & "{\ttlbrace} " term " . " id ":" term " {\ttrbrace}" \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

230 
&  & term " `` " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

231 
&  & term " `` " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

232 
&  & term " ` " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

233 
&  & term " * " term \\ 
14158  234 
&  & term " \isasyminter " term \\ 
14154  235 
&  & term " \isasymunion " term \\ 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

236 
&  & term "  " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

237 
&  & term " > " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

238 
&  & "THE~~" id " . " formula\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

239 
&  & "lam~~" id ":" term " . " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

240 
&  & "INT~~" id ":" term " . " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

241 
&  & "UN~~~" id ":" term " . " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

242 
&  & "PROD~" id ":" term " . " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

243 
&  & "SUM~~" id ":" term " . " term \\[2ex] 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

244 
formula & = & \hbox{expression of type~$o$} \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

245 
&  & term " : " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

246 
&  & term " \ttilde: " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

247 
&  & term " <= " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

248 
&  & term " = " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

249 
&  & term " \ttilde= " term \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

250 
&  & "\ttilde\ " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

251 
&  & formula " \& " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

252 
&  & formula "  " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

253 
&  & formula " > " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

254 
&  & formula " <> " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

255 
&  & "ALL " id ":" term " . " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

256 
&  & "EX~~" id ":" term " . " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

257 
&  & "ALL~" id~id^* " . " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

258 
&  & "EX~~" id~id^* " . " formula \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

259 
&  & "EX!~" id~id^* " . " formula 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

260 
\end{array} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

261 
\] 
9695  262 
\caption{Full grammar for ZF} \label{zfsyntax} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

263 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

264 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

265 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

266 
\section{Binding operators} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

267 
The constant \cdx{Collect} constructs sets by the principle of {\bf 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

268 
separation}. The syntax for separation is 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

269 
\hbox{\tt\ttlbrace$x$:$A$.\ $P[x]$\ttrbrace}, where $P[x]$ is a formula 
14154  270 
that may contain free occurrences of~$x$. It abbreviates the set \isa{Collect($A$,$\lambda x. P[x]$)}, which consists of all $x\in A$ that 
271 
satisfy~$P[x]$. Note that \isa{Collect} is an unfortunate choice of 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

272 
name: some set theories adopt a setformation principle, related to 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

273 
replacement, called collection. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

274 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

275 
The constant \cdx{Replace} constructs sets by the principle of {\bf 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

276 
replacement}. The syntax 
14154  277 
\hbox{\tt\ttlbrace$y$.\ $x$:$A$,$Q[x,y]$\ttrbrace} denotes the set 
278 
\isa{Replace($A$,$\lambda x\,y. Q[x,y]$)}, which consists of all~$y$ such 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

279 
that there exists $x\in A$ satisfying~$Q[x,y]$. The Replacement Axiom 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

280 
has the condition that $Q$ must be singlevalued over~$A$: for 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

281 
all~$x\in A$ there exists at most one $y$ satisfying~$Q[x,y]$. A 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

282 
singlevalued binary predicate is also called a {\bf class function}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

283 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

284 
The constant \cdx{RepFun} expresses a special case of replacement, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

285 
where $Q[x,y]$ has the form $y=b[x]$. Such a $Q$ is trivially 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

286 
singlevalued, since it is just the graph of the metalevel 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

287 
function~$\lambda x. b[x]$. The resulting set consists of all $b[x]$ 
14154  288 
for~$x\in A$. This is analogous to the \ML{} functional \isa{map}, 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

289 
since it applies a function to every element of a set. The syntax is 
14154  290 
\isa{\ttlbrace$b[x]$.\ $x$:$A$\ttrbrace}, which expands to 
291 
\isa{RepFun($A$,$\lambda x. b[x]$)}. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

292 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

293 
\index{*INT symbol}\index{*UN symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

294 
General unions and intersections of indexed 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

295 
families of sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$, 
14154  296 
are written \isa{UN $x$:$A$.\ $B[x]$} and \isa{INT $x$:$A$.\ $B[x]$}. 
297 
Their meaning is expressed using \isa{RepFun} as 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

298 
\[ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

299 
\bigcup(\{B[x]. x\in A\}) \qquad\hbox{and}\qquad 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

300 
\bigcap(\{B[x]. x\in A\}). 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

301 
\] 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

302 
General sums $\sum@{x\in A}B[x]$ and products $\prod@{x\in A}B[x]$ can be 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

303 
constructed in set theory, where $B[x]$ is a family of sets over~$A$. They 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

304 
have as special cases $A\times B$ and $A\to B$, where $B$ is simply a set. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

305 
This is similar to the situation in Constructive Type Theory (set theory 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

306 
has `dependent sets') and calls for similar syntactic conventions. The 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

307 
constants~\cdx{Sigma} and~\cdx{Pi} construct general sums and 
14154  308 
products. Instead of \isa{Sigma($A$,$B$)} and \isa{Pi($A$,$B$)} we may 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

309 
write 
14154  310 
\isa{SUM $x$:$A$.\ $B[x]$} and \isa{PROD $x$:$A$.\ $B[x]$}. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

311 
\index{*SUM symbol}\index{*PROD symbol}% 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

312 
The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$>$B$} abbreviate 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

313 
general sums and products over a constant family.\footnote{Unlike normal 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

314 
infix operators, {\tt*} and {\tt>} merely define abbreviations; there are 
14154  315 
no constants~\isa{op~*} and~\isa{op~>}.} Isabelle accepts these 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

316 
abbreviations in parsing and uses them whenever possible for printing. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

317 

9695  318 
\index{*THE symbol} As mentioned above, whenever the axioms assert the 
319 
existence and uniqueness of a set, Isabelle's set theory declares a constant 

320 
for that set. These constants can express the {\bf definite description} 

321 
operator~$\iota x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, 

322 
if such exists. Since all terms in ZF denote something, a description is 

323 
always meaningful, but we do not know its value unless $P[x]$ defines it 

14154  324 
uniquely. Using the constant~\cdx{The}, we may write descriptions as 
325 
\isa{The($\lambda x. P[x]$)} or use the syntax \isa{THE $x$.\ $P[x]$}. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

326 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

327 
\index{*lam symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

328 
Function sets may be written in $\lambda$notation; $\lambda x\in A. b[x]$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

329 
stands for the set of all pairs $\pair{x,b[x]}$ for $x\in A$. In order for 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

330 
this to be a set, the function's domain~$A$ must be given. Using the 
14154  331 
constant~\cdx{Lambda}, we may express function sets as \isa{Lambda($A$,$\lambda x. b[x]$)} or use the syntax \isa{lam $x$:$A$.\ $b[x]$}. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

332 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

333 
Isabelle's set theory defines two {\bf bounded quantifiers}: 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

334 
\begin{eqnarray*} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

335 
\forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

336 
\exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

337 
\end{eqnarray*} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

338 
The constants~\cdx{Ball} and~\cdx{Bex} are defined 
14154  339 
accordingly. Instead of \isa{Ball($A$,$P$)} and \isa{Bex($A$,$P$)} we may 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

340 
write 
14154  341 
\isa{ALL $x$:$A$.\ $P[x]$} and \isa{EX $x$:$A$.\ $P[x]$}. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

342 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

343 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

344 
%%%% ZF.thy 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

345 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

346 
\begin{figure} 
14154  347 
\begin{alltt*}\isastyleminor 
348 
\tdx{Let_def}: Let(s, f) == f(s) 

349 

350 
\tdx{Ball_def}: Ball(A,P) == {\isasymforall}x. x \isasymin A > P(x) 

351 
\tdx{Bex_def}: Bex(A,P) == {\isasymexists}x. x \isasymin A & P(x) 

352 

353 
\tdx{subset_def}: A \isasymsubseteq B == {\isasymforall}x \isasymin A. x \isasymin B 

354 
\tdx{extension}: A = B <> A \isasymsubseteq B & B \isasymsubseteq A 

355 

356 
\tdx{Union_iff}: A \isasymin Union(C) <> ({\isasymexists}B \isasymin C. A \isasymin B) 

357 
\tdx{Pow_iff}: A \isasymin Pow(B) <> A \isasymsubseteq B 

358 
\tdx{foundation}: A=0  ({\isasymexists}x \isasymin A. {\isasymforall}y \isasymin x. y \isasymnotin A) 

359 

360 
\tdx{replacement}: ({\isasymforall}x \isasymin A. {\isasymforall}y z. P(x,y) & P(x,z) > y=z) ==> 

361 
b \isasymin PrimReplace(A,P) <> ({\isasymexists}x{\isasymin}A. P(x,b)) 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

362 
\subcaption{The ZermeloFraenkel Axioms} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

363 

14154  364 
\tdx{Replace_def}: Replace(A,P) == 
365 
PrimReplace(A, \%x y. (\isasymexists!z. P(x,z)) & P(x,y)) 

366 
\tdx{RepFun_def}: RepFun(A,f) == {\ttlbrace}y . x \isasymin A, y=f(x)\ttrbrace 

367 
\tdx{the_def}: The(P) == Union({\ttlbrace}y . x \isasymin {\ttlbrace}0{\ttrbrace}, P(y){\ttrbrace}) 

368 
\tdx{if_def}: if(P,a,b) == THE z. P & z=a  ~P & z=b 

369 
\tdx{Collect_def}: Collect(A,P) == {\ttlbrace}y . x \isasymin A, x=y & P(x){\ttrbrace} 

370 
\tdx{Upair_def}: Upair(a,b) == 

371 
{\ttlbrace}y. x\isasymin{}Pow(Pow(0)), x=0 & y=a  x=Pow(0) & y=b{\ttrbrace} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

372 
\subcaption{Consequences of replacement} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

373 

14154  374 
\tdx{Inter_def}: Inter(A) == {\ttlbrace}x \isasymin Union(A) . {\isasymforall}y \isasymin A. x \isasymin y{\ttrbrace} 
375 
\tdx{Un_def}: A \isasymunion B == Union(Upair(A,B)) 

14158  376 
\tdx{Int_def}: A \isasyminter B == Inter(Upair(A,B)) 
14154  377 
\tdx{Diff_def}: A  B == {\ttlbrace}x \isasymin A . x \isasymnotin B{\ttrbrace} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

378 
\subcaption{Union, intersection, difference} 
14154  379 
\end{alltt*} 
9695  380 
\caption{Rules and axioms of ZF} \label{zfrules} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

381 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

382 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

383 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

384 
\begin{figure} 
14154  385 
\begin{alltt*}\isastyleminor 
386 
\tdx{cons_def}: cons(a,A) == Upair(a,a) \isasymunion A 

387 
\tdx{succ_def}: succ(i) == cons(i,i) 

388 
\tdx{infinity}: 0 \isasymin Inf & ({\isasymforall}y \isasymin Inf. succ(y) \isasymin Inf) 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

389 
\subcaption{Finite and infinite sets} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

390 

14154  391 
\tdx{Pair_def}: <a,b> == {\ttlbrace}{\ttlbrace}a,a{\ttrbrace}, {\ttlbrace}a,b{\ttrbrace}{\ttrbrace} 
392 
\tdx{split_def}: split(c,p) == THE y. {\isasymexists}a b. p=<a,b> & y=c(a,b) 

393 
\tdx{fst_def}: fst(A) == split(\%x y. x, p) 

394 
\tdx{snd_def}: snd(A) == split(\%x y. y, p) 

395 
\tdx{Sigma_def}: Sigma(A,B) == {\isasymUnion}x \isasymin A. {\isasymUnion}y \isasymin B(x). {\ttlbrace}<x,y>{\ttrbrace} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

396 
\subcaption{Ordered pairs and Cartesian products} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

397 

14154  398 
\tdx{converse_def}: converse(r) == {\ttlbrace}z. w\isasymin{}r, {\isasymexists}x y. w=<x,y> & z=<y,x>{\ttrbrace} 
399 
\tdx{domain_def}: domain(r) == {\ttlbrace}x. w \isasymin r, {\isasymexists}y. w=<x,y>{\ttrbrace} 

400 
\tdx{range_def}: range(r) == domain(converse(r)) 

401 
\tdx{field_def}: field(r) == domain(r) \isasymunion range(r) 

402 
\tdx{image_def}: r `` A == {\ttlbrace}y\isasymin{}range(r) . {\isasymexists}x \isasymin A. <x,y> \isasymin r{\ttrbrace} 

403 
\tdx{vimage_def}: r `` A == converse(r)``A 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

404 
\subcaption{Operations on relations} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

405 

14154  406 
\tdx{lam_def}: Lambda(A,b) == {\ttlbrace}<x,b(x)> . x \isasymin A{\ttrbrace} 
407 
\tdx{apply_def}: f`a == THE y. <a,y> \isasymin f 

408 
\tdx{Pi_def}: Pi(A,B) == {\ttlbrace}f\isasymin{}Pow(Sigma(A,B)). {\isasymforall}x\isasymin{}A. \isasymexists!y. <x,y>\isasymin{}f{\ttrbrace} 

409 
\tdx{restrict_def}: restrict(f,A) == lam x \isasymin A. f`x 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

410 
\subcaption{Functions and general product} 
14154  411 
\end{alltt*} 
9695  412 
\caption{Further definitions of ZF} \label{zfdefs} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

413 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

414 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

415 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

416 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

417 
\section{The ZermeloFraenkel axioms} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

418 
The axioms appear in Fig.\ts \ref{zfrules}. They resemble those 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

419 
presented by Suppes~\cite{suppes72}. Most of the theory consists of 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

420 
definitions. In particular, bounded quantifiers and the subset relation 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

421 
appear in other axioms. Objectlevel quantifiers and implications have 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

422 
been replaced by metalevel ones wherever possible, to simplify use of the 
14154  423 
axioms. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

424 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

425 
The traditional replacement axiom asserts 
14154  426 
\[ y \in \isa{PrimReplace}(A,P) \bimp (\exists x\in A. P(x,y)) \] 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

427 
subject to the condition that $P(x,y)$ is singlevalued for all~$x\in A$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

428 
The Isabelle theory defines \cdx{Replace} to apply 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

429 
\cdx{PrimReplace} to the singlevalued part of~$P$, namely 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

430 
\[ (\exists!z. P(x,z)) \conj P(x,y). \] 
14154  431 
Thus $y\in \isa{Replace}(A,P)$ if and only if there is some~$x$ such that 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

432 
$P(x,)$ holds uniquely for~$y$. Because the equivalence is unconditional, 
14154  433 
\isa{Replace} is much easier to use than \isa{PrimReplace}; it defines the 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

434 
same set, if $P(x,y)$ is singlevalued. The nice syntax for replacement 
14154  435 
expands to \isa{Replace}. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

436 

14158  437 
Other consequences of replacement include replacement for 
438 
metalevel functions 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

439 
(\cdx{RepFun}) and definite descriptions (\cdx{The}). 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

440 
Axioms for separation (\cdx{Collect}) and unordered pairs 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

441 
(\cdx{Upair}) are traditionally assumed, but they actually follow 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

442 
from replacement~\cite[pages 2378]{suppes72}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

443 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

444 
The definitions of general intersection, etc., are straightforward. Note 
14154  445 
the definition of \isa{cons}, which underlies the finite set notation. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

446 
The axiom of infinity gives us a set that contains~0 and is closed under 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

447 
successor (\cdx{succ}). Although this set is not uniquely defined, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

448 
the theory names it (\cdx{Inf}) in order to simplify the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

449 
construction of the natural numbers. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

450 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

451 
Further definitions appear in Fig.\ts\ref{zfdefs}. Ordered pairs are 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

452 
defined in the standard way, $\pair{a,b}\equiv\{\{a\},\{a,b\}\}$. Recall 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

453 
that \cdx{Sigma}$(A,B)$ generalizes the Cartesian product of two 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

454 
sets. It is defined to be the union of all singleton sets 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

455 
$\{\pair{x,y}\}$, for $x\in A$ and $y\in B(x)$. This is a typical usage of 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

456 
general union. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

457 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

458 
The projections \cdx{fst} and~\cdx{snd} are defined in terms of the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

459 
generalized projection \cdx{split}. The latter has been borrowed from 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

460 
MartinL\"of's Type Theory, and is often easier to use than \cdx{fst} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

461 
and~\cdx{snd}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

462 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

463 
Operations on relations include converse, domain, range, and image. The 
14154  464 
set $\isa{Pi}(A,B)$ generalizes the space of functions between two sets. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

465 
Note the simple definitions of $\lambda$abstraction (using 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

466 
\cdx{RepFun}) and application (using a definite description). The 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

467 
function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

468 
over the domain~$A$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

469 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

470 

14154  471 
%%%% zf.thy 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

472 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

473 
\begin{figure} 
14154  474 
\begin{alltt*}\isastyleminor 
475 
\tdx{ballI}: [ !!x. x\isasymin{}A ==> P(x) ] ==> {\isasymforall}x\isasymin{}A. P(x) 

476 
\tdx{bspec}: [ {\isasymforall}x\isasymin{}A. P(x); x\isasymin{}A ] ==> P(x) 

477 
\tdx{ballE}: [ {\isasymforall}x\isasymin{}A. P(x); P(x) ==> Q; x \isasymnotin A ==> Q ] ==> Q 

478 

479 
\tdx{ball_cong}: [ A=A'; !!x. x\isasymin{}A' ==> P(x) <> P'(x) ] ==> 

480 
({\isasymforall}x\isasymin{}A. P(x)) <> ({\isasymforall}x\isasymin{}A'. P'(x)) 

481 

482 
\tdx{bexI}: [ P(x); x\isasymin{}A ] ==> {\isasymexists}x\isasymin{}A. P(x) 

483 
\tdx{bexCI}: [ {\isasymforall}x\isasymin{}A. ~P(x) ==> P(a); a\isasymin{}A ] ==> {\isasymexists}x\isasymin{}A. P(x) 

484 
\tdx{bexE}: [ {\isasymexists}x\isasymin{}A. P(x); !!x. [ x\isasymin{}A; P(x) ] ==> Q ] ==> Q 

485 

486 
\tdx{bex_cong}: [ A=A'; !!x. x\isasymin{}A' ==> P(x) <> P'(x) ] ==> 

487 
({\isasymexists}x\isasymin{}A. P(x)) <> ({\isasymexists}x\isasymin{}A'. P'(x)) 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

488 
\subcaption{Bounded quantifiers} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

489 

14154  490 
\tdx{subsetI}: (!!x. x \isasymin A ==> x \isasymin B) ==> A \isasymsubseteq B 
491 
\tdx{subsetD}: [ A \isasymsubseteq B; c \isasymin A ] ==> c \isasymin B 

492 
\tdx{subsetCE}: [ A \isasymsubseteq B; c \isasymnotin A ==> P; c \isasymin B ==> P ] ==> P 

493 
\tdx{subset_refl}: A \isasymsubseteq A 

494 
\tdx{subset_trans}: [ A \isasymsubseteq B; B \isasymsubseteq C ] ==> A \isasymsubseteq C 

495 

496 
\tdx{equalityI}: [ A \isasymsubseteq B; B \isasymsubseteq A ] ==> A = B 

497 
\tdx{equalityD1}: A = B ==> A \isasymsubseteq B 

498 
\tdx{equalityD2}: A = B ==> B \isasymsubseteq A 

499 
\tdx{equalityE}: [ A = B; [ A \isasymsubseteq B; B \isasymsubseteq A ] ==> P ] ==> P 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

500 
\subcaption{Subsets and extensionality} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

501 

14154  502 
\tdx{emptyE}: a \isasymin 0 ==> P 
503 
\tdx{empty_subsetI}: 0 \isasymsubseteq A 

504 
\tdx{equals0I}: [ !!y. y \isasymin A ==> False ] ==> A=0 

505 
\tdx{equals0D}: [ A=0; a \isasymin A ] ==> P 

506 

507 
\tdx{PowI}: A \isasymsubseteq B ==> A \isasymin Pow(B) 

508 
\tdx{PowD}: A \isasymin Pow(B) ==> A \isasymsubseteq B 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

509 
\subcaption{The empty set; power sets} 
14154  510 
\end{alltt*} 
9695  511 
\caption{Basic derived rules for ZF} \label{zflemmas1} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

512 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

513 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

514 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

515 
\section{From basic lemmas to function spaces} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

516 
Faced with so many definitions, it is essential to prove lemmas. Even 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

517 
trivial theorems like $A \int B = B \int A$ would be difficult to 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

518 
prove from the definitions alone. Isabelle's set theory derives many 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

519 
rules using a natural deduction style. Ideally, a natural deduction 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

520 
rule should introduce or eliminate just one operator, but this is not 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

521 
always practical. For most operators, we may forget its definition 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

522 
and use its derived rules instead. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

523 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

524 
\subsection{Fundamental lemmas} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

525 
Figure~\ref{zflemmas1} presents the derived rules for the most basic 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

526 
operators. The rules for the bounded quantifiers resemble those for the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

527 
ordinary quantifiers, but note that \tdx{ballE} uses a negated assumption 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

528 
in the style of Isabelle's classical reasoner. The \rmindex{congruence 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

529 
rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

530 
simplifier, but have few other uses. Congruence rules must be specially 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

531 
derived for all binding operators, and henceforth will not be shown. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

532 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

533 
Figure~\ref{zflemmas1} also shows rules for the subset and equality 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

534 
relations (proof by extensionality), and rules about the empty set and the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

535 
power set operator. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

536 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

537 
Figure~\ref{zflemmas2} presents rules for replacement and separation. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

538 
The rules for \cdx{Replace} and \cdx{RepFun} are much simpler than 
14154  539 
comparable rules for \isa{PrimReplace} would be. The principle of 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

540 
separation is proved explicitly, although most proofs should use the 
14154  541 
natural deduction rules for \isa{Collect}. The elimination rule 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

542 
\tdx{CollectE} is equivalent to the two destruction rules 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

543 
\tdx{CollectD1} and \tdx{CollectD2}, but each rule is suited to 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

544 
particular circumstances. Although too many rules can be confusing, there 
14154  545 
is no reason to aim for a minimal set of rules. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

546 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

547 
Figure~\ref{zflemmas3} presents rules for general union and intersection. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

548 
The empty intersection should be undefined. We cannot have 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

549 
$\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set. All 
9695  550 
expressions denote something in ZF set theory; the definition of 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

551 
intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

552 
arbitrary. The rule \tdx{InterI} must have a premise to exclude 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

553 
the empty intersection. Some of the laws governing intersections require 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

554 
similar premises. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

555 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

556 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

557 
%the [p] gives better page breaking for the book 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

558 
\begin{figure}[p] 
14154  559 
\begin{alltt*}\isastyleminor 
560 
\tdx{ReplaceI}: [ x\isasymin{}A; P(x,b); !!y. P(x,y) ==> y=b ] ==> 

561 
b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace} 

562 

563 
\tdx{ReplaceE}: [ b\isasymin{}{\ttlbrace}y. x\isasymin{}A, P(x,y){\ttrbrace}; 

564 
!!x. [ x\isasymin{}A; P(x,b); {\isasymforall}y. P(x,y)>y=b ] ==> R 

565 
] ==> R 

566 

567 
\tdx{RepFunI}: [ a\isasymin{}A ] ==> f(a)\isasymin{}{\ttlbrace}f(x). x\isasymin{}A{\ttrbrace} 

568 
\tdx{RepFunE}: [ b\isasymin{}{\ttlbrace}f(x). x\isasymin{}A{\ttrbrace}; 

569 
!!x.[ x\isasymin{}A; b=f(x) ] ==> P ] ==> P 

570 

571 
\tdx{separation}: a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} <> a\isasymin{}A & P(a) 

572 
\tdx{CollectI}: [ a\isasymin{}A; P(a) ] ==> a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} 

573 
\tdx{CollectE}: [ a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace}; [ a\isasymin{}A; P(a) ] ==> R ] ==> R 

574 
\tdx{CollectD1}: a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} ==> a\isasymin{}A 

575 
\tdx{CollectD2}: a\isasymin{}{\ttlbrace}x\isasymin{}A. P(x){\ttrbrace} ==> P(a) 

576 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

577 
\caption{Replacement and separation} \label{zflemmas2} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

578 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

579 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

580 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

581 
\begin{figure} 
14154  582 
\begin{alltt*}\isastyleminor 
583 
\tdx{UnionI}: [ B\isasymin{}C; A\isasymin{}B ] ==> A\isasymin{}Union(C) 

584 
\tdx{UnionE}: [ A\isasymin{}Union(C); !!B.[ A\isasymin{}B; B\isasymin{}C ] ==> R ] ==> R 

585 

586 
\tdx{InterI}: [ !!x. x\isasymin{}C ==> A\isasymin{}x; c\isasymin{}C ] ==> A\isasymin{}Inter(C) 

587 
\tdx{InterD}: [ A\isasymin{}Inter(C); B\isasymin{}C ] ==> A\isasymin{}B 

588 
\tdx{InterE}: [ A\isasymin{}Inter(C); A\isasymin{}B ==> R; B \isasymnotin C ==> R ] ==> R 

589 

590 
\tdx{UN_I}: [ a\isasymin{}A; b\isasymin{}B(a) ] ==> b\isasymin{}({\isasymUnion}x\isasymin{}A. B(x)) 

591 
\tdx{UN_E}: [ b\isasymin{}({\isasymUnion}x\isasymin{}A. B(x)); !!x.[ x\isasymin{}A; b\isasymin{}B(x) ] ==> R 

592 
] ==> R 

593 

594 
\tdx{INT_I}: [ !!x. x\isasymin{}A ==> b\isasymin{}B(x); a\isasymin{}A ] ==> b\isasymin{}({\isasymInter}x\isasymin{}A. B(x)) 

595 
\tdx{INT_E}: [ b\isasymin{}({\isasymInter}x\isasymin{}A. B(x)); a\isasymin{}A ] ==> b\isasymin{}B(a) 

596 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

597 
\caption{General union and intersection} \label{zflemmas3} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

598 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

599 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

600 

14154  601 
%%% upair.thy 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

602 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

603 
\begin{figure} 
14154  604 
\begin{alltt*}\isastyleminor 
605 
\tdx{pairing}: a\isasymin{}Upair(b,c) <> (a=b  a=c) 

606 
\tdx{UpairI1}: a\isasymin{}Upair(a,b) 

607 
\tdx{UpairI2}: b\isasymin{}Upair(a,b) 

608 
\tdx{UpairE}: [ a\isasymin{}Upair(b,c); a=b ==> P; a=c ==> P ] ==> P 

609 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

610 
\caption{Unordered pairs} \label{zfupair1} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

611 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

612 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

613 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

614 
\begin{figure} 
14154  615 
\begin{alltt*}\isastyleminor 
616 
\tdx{UnI1}: c\isasymin{}A ==> c\isasymin{}A \isasymunion B 

617 
\tdx{UnI2}: c\isasymin{}B ==> c\isasymin{}A \isasymunion B 

618 
\tdx{UnCI}: (c \isasymnotin B ==> c\isasymin{}A) ==> c\isasymin{}A \isasymunion B 

619 
\tdx{UnE}: [ c\isasymin{}A \isasymunion B; c\isasymin{}A ==> P; c\isasymin{}B ==> P ] ==> P 

620 

14158  621 
\tdx{IntI}: [ c\isasymin{}A; c\isasymin{}B ] ==> c\isasymin{}A \isasyminter B 
622 
\tdx{IntD1}: c\isasymin{}A \isasyminter B ==> c\isasymin{}A 

623 
\tdx{IntD2}: c\isasymin{}A \isasyminter B ==> c\isasymin{}B 

624 
\tdx{IntE}: [ c\isasymin{}A \isasyminter B; [ c\isasymin{}A; c\isasymin{}B ] ==> P ] ==> P 

14154  625 

626 
\tdx{DiffI}: [ c\isasymin{}A; c \isasymnotin B ] ==> c\isasymin{}A  B 

627 
\tdx{DiffD1}: c\isasymin{}A  B ==> c\isasymin{}A 

628 
\tdx{DiffD2}: c\isasymin{}A  B ==> c \isasymnotin B 

629 
\tdx{DiffE}: [ c\isasymin{}A  B; [ c\isasymin{}A; c \isasymnotin B ] ==> P ] ==> P 

630 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

631 
\caption{Union, intersection, difference} \label{zfUn} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

632 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

633 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

634 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

635 
\begin{figure} 
14154  636 
\begin{alltt*}\isastyleminor 
637 
\tdx{consI1}: a\isasymin{}cons(a,B) 

638 
\tdx{consI2}: a\isasymin{}B ==> a\isasymin{}cons(b,B) 

639 
\tdx{consCI}: (a \isasymnotin B ==> a=b) ==> a\isasymin{}cons(b,B) 

640 
\tdx{consE}: [ a\isasymin{}cons(b,A); a=b ==> P; a\isasymin{}A ==> P ] ==> P 

641 

642 
\tdx{singletonI}: a\isasymin{}{\ttlbrace}a{\ttrbrace} 

643 
\tdx{singletonE}: [ a\isasymin{}{\ttlbrace}b{\ttrbrace}; a=b ==> P ] ==> P 

644 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

645 
\caption{Finite and singleton sets} \label{zfupair2} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

646 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

647 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

648 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

649 
\begin{figure} 
14154  650 
\begin{alltt*}\isastyleminor 
651 
\tdx{succI1}: i\isasymin{}succ(i) 

652 
\tdx{succI2}: i\isasymin{}j ==> i\isasymin{}succ(j) 

653 
\tdx{succCI}: (i \isasymnotin j ==> i=j) ==> i\isasymin{}succ(j) 

654 
\tdx{succE}: [ i\isasymin{}succ(j); i=j ==> P; i\isasymin{}j ==> P ] ==> P 

655 
\tdx{succ_neq_0}: [ succ(n)=0 ] ==> P 

656 
\tdx{succ_inject}: succ(m) = succ(n) ==> m=n 

657 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

658 
\caption{The successor function} \label{zfsucc} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

659 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

660 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

661 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

662 
\begin{figure} 
14154  663 
\begin{alltt*}\isastyleminor 
664 
\tdx{the_equality}: [ P(a); !!x. P(x) ==> x=a ] ==> (THE x. P(x))=a 

665 
\tdx{theI}: \isasymexists! x. P(x) ==> P(THE x. P(x)) 

666 

667 
\tdx{if_P}: P ==> (if P then a else b) = a 

668 
\tdx{if_not_P}: ~P ==> (if P then a else b) = b 

669 

670 
\tdx{mem_asym}: [ a\isasymin{}b; b\isasymin{}a ] ==> P 

671 
\tdx{mem_irrefl}: a\isasymin{}a ==> P 

672 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

673 
\caption{Descriptions; noncircularity} \label{zfthe} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

674 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

675 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

676 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

677 
\subsection{Unordered pairs and finite sets} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

678 
Figure~\ref{zfupair1} presents the principle of unordered pairing, along 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

679 
with its derived rules. Binary union and intersection are defined in terms 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

680 
of ordered pairs (Fig.\ts\ref{zfUn}). Set difference is also included. The 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

681 
rule \tdx{UnCI} is useful for classical reasoning about unions, 
14154  682 
like \isa{disjCI}\@; it supersedes \tdx{UnI1} and 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

683 
\tdx{UnI2}, but these rules are often easier to work with. For 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

684 
intersection and difference we have both elimination and destruction rules. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

685 
Again, there is no reason to provide a minimal rule set. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

686 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

687 
Figure~\ref{zfupair2} is concerned with finite sets: it presents rules 
14154  688 
for~\isa{cons}, the finite set constructor, and rules for singleton 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

689 
sets. Figure~\ref{zfsucc} presents derived rules for the successor 
14154  690 
function, which is defined in terms of~\isa{cons}. The proof that 
691 
\isa{succ} is injective appears to require the Axiom of Foundation. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

692 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

693 
Definite descriptions (\sdx{THE}) are defined in terms of the singleton 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

694 
set~$\{0\}$, but their derived rules fortunately hide this 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

695 
(Fig.\ts\ref{zfthe}). The rule~\tdx{theI} is difficult to apply 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

696 
because of the two occurrences of~$\Var{P}$. However, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

697 
\tdx{the_equality} does not have this problem and the files contain 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

698 
many examples of its use. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

699 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

700 
Finally, the impossibility of having both $a\in b$ and $b\in a$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

701 
(\tdx{mem_asym}) is proved by applying the Axiom of Foundation to 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

702 
the set $\{a,b\}$. The impossibility of $a\in a$ is a trivial consequence. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

703 

14154  704 

705 
%%% subset.thy? 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

706 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

707 
\begin{figure} 
14154  708 
\begin{alltt*}\isastyleminor 
709 
\tdx{Union_upper}: B\isasymin{}A ==> B \isasymsubseteq Union(A) 

710 
\tdx{Union_least}: [ !!x. x\isasymin{}A ==> x \isasymsubseteq C ] ==> Union(A) \isasymsubseteq C 

711 

712 
\tdx{Inter_lower}: B\isasymin{}A ==> Inter(A) \isasymsubseteq B 

713 
\tdx{Inter_greatest}: [ a\isasymin{}A; !!x. x\isasymin{}A ==> C \isasymsubseteq x ] ==> C\isasymsubseteq{}Inter(A) 

714 

715 
\tdx{Un_upper1}: A \isasymsubseteq A \isasymunion B 

716 
\tdx{Un_upper2}: B \isasymsubseteq A \isasymunion B 

717 
\tdx{Un_least}: [ A \isasymsubseteq C; B \isasymsubseteq C ] ==> A \isasymunion B \isasymsubseteq C 

718 

14158  719 
\tdx{Int_lower1}: A \isasyminter B \isasymsubseteq A 
720 
\tdx{Int_lower2}: A \isasyminter B \isasymsubseteq B 

721 
\tdx{Int_greatest}: [ C \isasymsubseteq A; C \isasymsubseteq B ] ==> C \isasymsubseteq A \isasyminter B 

14154  722 

723 
\tdx{Diff_subset}: AB \isasymsubseteq A 

14158  724 
\tdx{Diff_contains}: [ C \isasymsubseteq A; C \isasyminter B = 0 ] ==> C \isasymsubseteq AB 
14154  725 

726 
\tdx{Collect_subset}: Collect(A,P) \isasymsubseteq A 

727 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

728 
\caption{Subset and lattice properties} \label{zfsubset} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

729 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

730 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

731 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

732 
\subsection{Subset and lattice properties} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

733 
The subset relation is a complete lattice. Unions form least upper bounds; 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

734 
nonempty intersections form greatest lower bounds. Figure~\ref{zfsubset} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

735 
shows the corresponding rules. A few other laws involving subsets are 
14154  736 
included. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

737 
Reasoning directly about subsets often yields clearer proofs than 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

738 
reasoning about the membership relation. Section~\ref{sec:ZFpowexample} 
14154  739 
below presents an example of this, proving the equation 
740 
${\isa{Pow}(A)\cap \isa{Pow}(B)}= \isa{Pow}(A\cap B)$. 

741 

742 
%%% pair.thy 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

743 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

744 
\begin{figure} 
14154  745 
\begin{alltt*}\isastyleminor 
746 
\tdx{Pair_inject1}: <a,b> = <c,d> ==> a=c 

747 
\tdx{Pair_inject2}: <a,b> = <c,d> ==> b=d 

748 
\tdx{Pair_inject}: [ <a,b> = <c,d>; [ a=c; b=d ] ==> P ] ==> P 

749 
\tdx{Pair_neq_0}: <a,b>=0 ==> P 

750 

751 
\tdx{fst_conv}: fst(<a,b>) = a 

752 
\tdx{snd_conv}: snd(<a,b>) = b 

753 
\tdx{split}: split(\%x y. c(x,y), <a,b>) = c(a,b) 

754 

755 
\tdx{SigmaI}: [ a\isasymin{}A; b\isasymin{}B(a) ] ==> <a,b>\isasymin{}Sigma(A,B) 

756 

757 
\tdx{SigmaE}: [ c\isasymin{}Sigma(A,B); 

758 
!!x y.[ x\isasymin{}A; y\isasymin{}B(x); c=<x,y> ] ==> P ] ==> P 

759 

760 
\tdx{SigmaE2}: [ <a,b>\isasymin{}Sigma(A,B); 

761 
[ a\isasymin{}A; b\isasymin{}B(a) ] ==> P ] ==> P 

762 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

763 
\caption{Ordered pairs; projections; general sums} \label{zfpair} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

764 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

765 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

766 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

767 
\subsection{Ordered pairs} \label{sec:pairs} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

768 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

769 
Figure~\ref{zfpair} presents the rules governing ordered pairs, 
14154  770 
projections and general sums  in particular, that 
771 
$\{\{a\},\{a,b\}\}$ functions as an ordered pair. This property is 

772 
expressed as two destruction rules, 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

773 
\tdx{Pair_inject1} and \tdx{Pair_inject2}, and equivalently 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

774 
as the elimination rule \tdx{Pair_inject}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

775 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

776 
The rule \tdx{Pair_neq_0} asserts $\pair{a,b}\neq\emptyset$. This 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

777 
is a property of $\{\{a\},\{a,b\}\}$, and need not hold for other 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

778 
encodings of ordered pairs. The nonstandard ordered pairs mentioned below 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

779 
satisfy $\pair{\emptyset;\emptyset}=\emptyset$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

780 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

781 
The natural deduction rules \tdx{SigmaI} and \tdx{SigmaE} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

782 
assert that \cdx{Sigma}$(A,B)$ consists of all pairs of the form 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

783 
$\pair{x,y}$, for $x\in A$ and $y\in B(x)$. The rule \tdx{SigmaE2} 
14154  784 
merely states that $\pair{a,b}\in \isa{Sigma}(A,B)$ implies $a\in A$ and 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

785 
$b\in B(a)$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

786 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

787 
In addition, it is possible to use tuples as patterns in abstractions: 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

788 
\begin{center} 
14154  789 
{\tt\%<$x$,$y$>. $t$} \quad stands for\quad \isa{split(\%$x$ $y$.\ $t$)} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

790 
\end{center} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

791 
Nested patterns are translated recursively: 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

792 
{\tt\%<$x$,$y$,$z$>. $t$} $\leadsto$ {\tt\%<$x$,<$y$,$z$>>. $t$} $\leadsto$ 
14154  793 
\isa{split(\%$x$.\%<$y$,$z$>. $t$)} $\leadsto$ \isa{split(\%$x$. split(\%$y$ 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

794 
$z$.\ $t$))}. The reverse translation is performed upon printing. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

795 
\begin{warn} 
14154  796 
The translation between patterns and \isa{split} is performed automatically 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

797 
by the parser and printer. Thus the internal and external form of a term 
14154  798 
may differ, which affects proofs. For example the term \isa{(\%<x,y>.<y,x>)<a,b>} requires the theorem \isa{split} to rewrite to 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

799 
{\tt<b,a>}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

800 
\end{warn} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

801 
In addition to explicit $\lambda$abstractions, patterns can be used in any 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

802 
variable binding construct which is internally described by a 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

803 
$\lambda$abstraction. Here are some important examples: 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

804 
\begin{description} 
14154  805 
\item[Let:] \isa{let {\it pattern} = $t$ in $u$} 
806 
\item[Choice:] \isa{THE~{\it pattern}~.~$P$} 

807 
\item[Set operations:] \isa{\isasymUnion~{\it pattern}:$A$.~$B$} 

808 
\item[Comprehension:] \isa{{\ttlbrace}~{\it pattern}:$A$~.~$P$~{\ttrbrace}} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

809 
\end{description} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

810 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

811 

14154  812 
%%% domrange.thy? 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

813 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

814 
\begin{figure} 
14154  815 
\begin{alltt*}\isastyleminor 
816 
\tdx{domainI}: <a,b>\isasymin{}r ==> a\isasymin{}domain(r) 

817 
\tdx{domainE}: [ a\isasymin{}domain(r); !!y. <a,y>\isasymin{}r ==> P ] ==> P 

818 
\tdx{domain_subset}: domain(Sigma(A,B)) \isasymsubseteq A 

819 

820 
\tdx{rangeI}: <a,b>\isasymin{}r ==> b\isasymin{}range(r) 

821 
\tdx{rangeE}: [ b\isasymin{}range(r); !!x. <x,b>\isasymin{}r ==> P ] ==> P 

822 
\tdx{range_subset}: range(A*B) \isasymsubseteq B 

823 

824 
\tdx{fieldI1}: <a,b>\isasymin{}r ==> a\isasymin{}field(r) 

825 
\tdx{fieldI2}: <a,b>\isasymin{}r ==> b\isasymin{}field(r) 

826 
\tdx{fieldCI}: (<c,a> \isasymnotin r ==> <a,b>\isasymin{}r) ==> a\isasymin{}field(r) 

827 

828 
\tdx{fieldE}: [ a\isasymin{}field(r); 

14158  829 
!!x. <a,x>\isasymin{}r ==> P; 
830 
!!x. <x,a>\isasymin{}r ==> P 

831 
] ==> P 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

832 

14154  833 
\tdx{field_subset}: field(A*A) \isasymsubseteq A 
834 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

835 
\caption{Domain, range and field of a relation} \label{zfdomrange} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

836 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

837 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

838 
\begin{figure} 
14154  839 
\begin{alltt*}\isastyleminor 
840 
\tdx{imageI}: [ <a,b>\isasymin{}r; a\isasymin{}A ] ==> b\isasymin{}r``A 

841 
\tdx{imageE}: [ b\isasymin{}r``A; !!x.[ <x,b>\isasymin{}r; x\isasymin{}A ] ==> P ] ==> P 

842 

843 
\tdx{vimageI}: [ <a,b>\isasymin{}r; b\isasymin{}B ] ==> a\isasymin{}r``B 

844 
\tdx{vimageE}: [ a\isasymin{}r``B; !!x.[ <a,x>\isasymin{}r; x\isasymin{}B ] ==> P ] ==> P 

845 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

846 
\caption{Image and inverse image} \label{zfdomrange2} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

847 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

848 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

849 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

850 
\subsection{Relations} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

851 
Figure~\ref{zfdomrange} presents rules involving relations, which are sets 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

852 
of ordered pairs. The converse of a relation~$r$ is the set of all pairs 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

853 
$\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

854 
{\cdx{converse}$(r)$} is its inverse. The rules for the domain 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

855 
operation, namely \tdx{domainI} and~\tdx{domainE}, assert that 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

856 
\cdx{domain}$(r)$ consists of all~$x$ such that $r$ contains 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

857 
some pair of the form~$\pair{x,y}$. The range operation is similar, and 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

858 
the field of a relation is merely the union of its domain and range. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

859 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

860 
Figure~\ref{zfdomrange2} presents rules for images and inverse images. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

861 
Note that these operations are generalisations of range and domain, 
14154  862 
respectively. 
863 

864 

865 
%%% func.thy 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

866 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

867 
\begin{figure} 
14154  868 
\begin{alltt*}\isastyleminor 
869 
\tdx{fun_is_rel}: f\isasymin{}Pi(A,B) ==> f \isasymsubseteq Sigma(A,B) 

870 

14158  871 
\tdx{apply_equality}: [ <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) ] ==> f`a = b 
14154  872 
\tdx{apply_equality2}: [ <a,b>\isasymin{}f; <a,c>\isasymin{}f; f\isasymin{}Pi(A,B) ] ==> b=c 
873 

874 
\tdx{apply_type}: [ f\isasymin{}Pi(A,B); a\isasymin{}A ] ==> f`a\isasymin{}B(a) 

875 
\tdx{apply_Pair}: [ f\isasymin{}Pi(A,B); a\isasymin{}A ] ==> <a,f`a>\isasymin{}f 

876 
\tdx{apply_iff}: f\isasymin{}Pi(A,B) ==> <a,b>\isasymin{}f <> a\isasymin{}A & f`a = b 

877 

878 
\tdx{fun_extension}: [ f\isasymin{}Pi(A,B); g\isasymin{}Pi(A,D); 

879 
!!x. x\isasymin{}A ==> f`x = g`x ] ==> f=g 

880 

881 
\tdx{domain_type}: [ <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) ] ==> a\isasymin{}A 

882 
\tdx{range_type}: [ <a,b>\isasymin{}f; f\isasymin{}Pi(A,B) ] ==> b\isasymin{}B(a) 

883 

884 
\tdx{Pi_type}: [ f\isasymin{}A>C; !!x. x\isasymin{}A ==> f`x\isasymin{}B(x) ] ==> f\isasymin{}Pi(A,B) 

885 
\tdx{domain_of_fun}: f\isasymin{}Pi(A,B) ==> domain(f)=A 

886 
\tdx{range_of_fun}: f\isasymin{}Pi(A,B) ==> f\isasymin{}A>range(f) 

887 

888 
\tdx{restrict}: a\isasymin{}A ==> restrict(f,A) ` a = f`a 

889 
\tdx{restrict_type}: [ !!x. x\isasymin{}A ==> f`x\isasymin{}B(x) ] ==> 

890 
restrict(f,A)\isasymin{}Pi(A,B) 

891 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

892 
\caption{Functions} \label{zffunc1} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

893 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

894 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

895 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

896 
\begin{figure} 
14154  897 
\begin{alltt*}\isastyleminor 
898 
\tdx{lamI}: a\isasymin{}A ==> <a,b(a)>\isasymin{}(lam x\isasymin{}A. b(x)) 

899 
\tdx{lamE}: [ p\isasymin{}(lam x\isasymin{}A. b(x)); !!x.[ x\isasymin{}A; p=<x,b(x)> ] ==> P 

8249  900 
] ==> P 
901 

14154  902 
\tdx{lam_type}: [ !!x. x\isasymin{}A ==> b(x)\isasymin{}B(x) ] ==> (lam x\isasymin{}A. b(x))\isasymin{}Pi(A,B) 
903 

904 
\tdx{beta}: a\isasymin{}A ==> (lam x\isasymin{}A. b(x)) ` a = b(a) 

905 
\tdx{eta}: f\isasymin{}Pi(A,B) ==> (lam x\isasymin{}A. f`x) = f 

906 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

907 
\caption{$\lambda$abstraction} \label{zflam} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

908 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

909 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

910 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

911 
\begin{figure} 
14154  912 
\begin{alltt*}\isastyleminor 
913 
\tdx{fun_empty}: 0\isasymin{}0>0 

914 
\tdx{fun_single}: {\ttlbrace}<a,b>{\ttrbrace}\isasymin{}{\ttlbrace}a{\ttrbrace} > {\ttlbrace}b{\ttrbrace} 

915 

14158  916 
\tdx{fun_disjoint_Un}: [ f\isasymin{}A>B; g\isasymin{}C>D; A \isasyminter C = 0 ] ==> 
14154  917 
(f \isasymunion g)\isasymin{}(A \isasymunion C) > (B \isasymunion D) 
918 

919 
\tdx{fun_disjoint_apply1}: [ a\isasymin{}A; f\isasymin{}A>B; g\isasymin{}C>D; A\isasyminter{}C = 0 ] ==> 

920 
(f \isasymunion g)`a = f`a 

921 

922 
\tdx{fun_disjoint_apply2}: [ c\isasymin{}C; f\isasymin{}A>B; g\isasymin{}C>D; A\isasyminter{}C = 0 ] ==> 

923 
(f \isasymunion g)`c = g`c 

924 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

925 
\caption{Constructing functions from smaller sets} \label{zffunc2} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

926 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

927 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

928 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

929 
\subsection{Functions} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

930 
Functions, represented by graphs, are notoriously difficult to reason 
14154  931 
about. The ZF theory provides many derived rules, which overlap more 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

932 
than they ought. This section presents the more important rules. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

933 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

934 
Figure~\ref{zffunc1} presents the basic properties of \cdx{Pi}$(A,B)$, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

935 
the generalized function space. For example, if $f$ is a function and 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

936 
$\pair{a,b}\in f$, then $f`a=b$ (\tdx{apply_equality}). Two functions 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

937 
are equal provided they have equal domains and deliver equals results 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

938 
(\tdx{fun_extension}). 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

939 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

940 
By \tdx{Pi_type}, a function typing of the form $f\in A\to C$ can be 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

941 
refined to the dependent typing $f\in\prod@{x\in A}B(x)$, given a suitable 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

942 
family of sets $\{B(x)\}@{x\in A}$. Conversely, by \tdx{range_of_fun}, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

943 
any dependent typing can be flattened to yield a function type of the form 
14154  944 
$A\to C$; here, $C=\isa{range}(f)$. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

945 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

946 
Among the laws for $\lambda$abstraction, \tdx{lamI} and \tdx{lamE} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

947 
describe the graph of the generated function, while \tdx{beta} and 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

948 
\tdx{eta} are the standard conversions. We essentially have a 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

949 
dependentlytyped $\lambda$calculus (Fig.\ts\ref{zflam}). 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

950 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

951 
Figure~\ref{zffunc2} presents some rules that can be used to construct 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

952 
functions explicitly. We start with functions consisting of at most one 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

953 
pair, and may form the union of two functions provided their domains are 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

954 
disjoint. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

955 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

956 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

957 
\begin{figure} 
14154  958 
\begin{alltt*}\isastyleminor 
14158  959 
\tdx{Int_absorb}: A \isasyminter A = A 
960 
\tdx{Int_commute}: A \isasyminter B = B \isasyminter A 

961 
\tdx{Int_assoc}: (A \isasyminter B) \isasyminter C = A \isasyminter (B \isasyminter C) 

962 
\tdx{Int_Un_distrib}: (A \isasymunion B) \isasyminter C = (A \isasyminter C) \isasymunion (B \isasyminter C) 

14154  963 

964 
\tdx{Un_absorb}: A \isasymunion A = A 

965 
\tdx{Un_commute}: A \isasymunion B = B \isasymunion A 

966 
\tdx{Un_assoc}: (A \isasymunion B) \isasymunion C = A \isasymunion (B \isasymunion C) 

14158  967 
\tdx{Un_Int_distrib}: (A \isasyminter B) \isasymunion C = (A \isasymunion C) \isasyminter (B \isasymunion C) 
14154  968 

969 
\tdx{Diff_cancel}: AA = 0 

14158  970 
\tdx{Diff_disjoint}: A \isasyminter (BA) = 0 
14154  971 
\tdx{Diff_partition}: A \isasymsubseteq B ==> A \isasymunion (BA) = B 
972 
\tdx{double_complement}: [ A \isasymsubseteq B; B \isasymsubseteq C ] ==> (B  (CA)) = A 

14158  973 
\tdx{Diff_Un}: A  (B \isasymunion C) = (AB) \isasyminter (AC) 
974 
\tdx{Diff_Int}: A  (B \isasyminter C) = (AB) \isasymunion (AC) 

14154  975 

976 
\tdx{Union_Un_distrib}: Union(A \isasymunion B) = Union(A) \isasymunion Union(B) 

977 
\tdx{Inter_Un_distrib}: [ a \isasymin A; b \isasymin B ] ==> 

14158  978 
Inter(A \isasymunion B) = Inter(A) \isasyminter Inter(B) 
979 

980 
\tdx{Int_Union_RepFun}: A \isasyminter Union(B) = ({\isasymUnion}C \isasymin B. A \isasyminter C) 

14154  981 

982 
\tdx{Un_Inter_RepFun}: b \isasymin B ==> 

983 
A \isasymunion Inter(B) = ({\isasymInter}C \isasymin B. A \isasymunion C) 

984 

985 
\tdx{SUM_Un_distrib1}: (SUM x \isasymin A \isasymunion B. C(x)) = 

986 
(SUM x \isasymin A. C(x)) \isasymunion (SUM x \isasymin B. C(x)) 

987 

988 
\tdx{SUM_Un_distrib2}: (SUM x \isasymin C. A(x) \isasymunion B(x)) = 

989 
(SUM x \isasymin C. A(x)) \isasymunion (SUM x \isasymin C. B(x)) 

990 

14158  991 
\tdx{SUM_Int_distrib1}: (SUM x \isasymin A \isasyminter B. C(x)) = 
992 
(SUM x \isasymin A. C(x)) \isasyminter (SUM x \isasymin B. C(x)) 

993 

994 
\tdx{SUM_Int_distrib2}: (SUM x \isasymin C. A(x) \isasyminter B(x)) = 

995 
(SUM x \isasymin C. A(x)) \isasyminter (SUM x \isasymin C. B(x)) 

14154  996 
\end{alltt*} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

997 
\caption{Equalities} \label{zfequalities} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

998 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

999 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1000 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1001 
\begin{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1002 
%\begin{constants} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1003 
% \cdx{1} & $i$ & & $\{\emptyset\}$ \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1004 
% \cdx{bool} & $i$ & & the set $\{\emptyset,1\}$ \\ 
14154  1005 
% \cdx{cond} & $[i,i,i]\To i$ & & conditional for \isa{bool} \\ 
1006 
% \cdx{not} & $i\To i$ & & negation for \isa{bool} \\ 

1007 
% \sdx{and} & $[i,i]\To i$ & Left 70 & conjunction for \isa{bool} \\ 

1008 
% \sdx{or} & $[i,i]\To i$ & Left 65 & disjunction for \isa{bool} \\ 

1009 
% \sdx{xor} & $[i,i]\To i$ & Left 65 & exclusiveor for \isa{bool} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1010 
%\end{constants} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1011 
% 
14154  1012 
\begin{alltt*}\isastyleminor 
1013 
\tdx{bool_def}: bool == {\ttlbrace}0,1{\ttrbrace} 

1014 
\tdx{cond_def}: cond(b,c,d) == if b=1 then c else d 

1015 
\tdx{not_def}: not(b) == cond(b,0,1) 

1016 
\tdx{and_def}: a and b == cond(a,b,0) 

1017 
\tdx{or_def}: a or b == cond(a,1,b) 

1018 
\tdx{xor_def}: a xor b == cond(a,not(b),b) 

1019 

1020 
\tdx{bool_1I}: 1 \isasymin bool 

1021 
\tdx{bool_0I}: 0 \isasymin bool 

1022 
\tdx{boolE}: [ c \isasymin bool; c=1 ==> P; c=0 ==> P ] ==> P 

1023 
\tdx{cond_1}: cond(1,c,d) = c 

1024 
\tdx{cond_0}: cond(0,c,d) = d 

1025 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1026 
\caption{The booleans} \label{zfbool} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1027 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1028 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1029 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1030 
\section{Further developments} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1031 
The next group of developments is complex and extensive, and only 
14154  1032 
highlights can be covered here. It involves many theories and proofs. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1033 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1034 
Figure~\ref{zfequalities} presents commutative, associative, distributive, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1035 
and idempotency laws of union and intersection, along with other equations. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1036 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1037 
Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual 
9695  1038 
operators including a conditional (Fig.\ts\ref{zfbool}). Although ZF is a 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1039 
firstorder theory, you can obtain the effect of higherorder logic using 
14154  1040 
\isa{bool}valued functions, for example. The constant~\isa{1} is 
1041 
translated to \isa{succ(0)}. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1042 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1043 
\begin{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1044 
\index{*"+ symbol} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1045 
\begin{constants} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1046 
\it symbol & \it metatype & \it priority & \it description \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1047 
\tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1048 
\cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1049 
\cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1050 
\end{constants} 
14154  1051 
\begin{alltt*}\isastyleminor 
1052 
\tdx{sum_def}: A+B == {\ttlbrace}0{\ttrbrace}*A \isasymunion {\ttlbrace}1{\ttrbrace}*B 

1053 
\tdx{Inl_def}: Inl(a) == <0,a> 

1054 
\tdx{Inr_def}: Inr(b) == <1,b> 

1055 
\tdx{case_def}: case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u) 

1056 

1057 
\tdx{InlI}: a \isasymin A ==> Inl(a) \isasymin A+B 

1058 
\tdx{InrI}: b \isasymin B ==> Inr(b) \isasymin A+B 

1059 

1060 
\tdx{Inl_inject}: Inl(a)=Inl(b) ==> a=b 

1061 
\tdx{Inr_inject}: Inr(a)=Inr(b) ==> a=b 

1062 
\tdx{Inl_neq_Inr}: Inl(a)=Inr(b) ==> P 

1063 

1064 
\tdx{sum_iff}: u \isasymin A+B <> ({\isasymexists}x\isasymin{}A. u=Inl(x))  ({\isasymexists}y\isasymin{}B. u=Inr(y)) 

1065 

1066 
\tdx{case_Inl}: case(c,d,Inl(a)) = c(a) 

1067 
\tdx{case_Inr}: case(c,d,Inr(b)) = d(b) 

1068 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1069 
\caption{Disjoint unions} \label{zfsum} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1070 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1071 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1072 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1073 
\subsection{Disjoint unions} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1074 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1075 
Theory \thydx{Sum} defines the disjoint union of two sets, with 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1076 
injections and a case analysis operator (Fig.\ts\ref{zfsum}). Disjoint 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1077 
unions play a role in datatype definitions, particularly when there is 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1078 
mutual recursion~\cite{paulsonsetII}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1079 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1080 
\begin{figure} 
14154  1081 
\begin{alltt*}\isastyleminor 
1082 
\tdx{QPair_def}: <a;b> == a+b 

1083 
\tdx{qsplit_def}: qsplit(c,p) == THE y. {\isasymexists}a b. p=<a;b> & y=c(a,b) 

1084 
\tdx{qfsplit_def}: qfsplit(R,z) == {\isasymexists}x y. z=<x;y> & R(x,y) 

1085 
\tdx{qconverse_def}: qconverse(r) == {\ttlbrace}z. w \isasymin r, {\isasymexists}x y. w=<x;y> & z=<y;x>{\ttrbrace} 

1086 
\tdx{QSigma_def}: QSigma(A,B) == {\isasymUnion}x \isasymin A. {\isasymUnion}y \isasymin B(x). {\ttlbrace}<x;y>{\ttrbrace} 

1087 

1088 
\tdx{qsum_def}: A <+> B == ({\ttlbrace}0{\ttrbrace} <*> A) \isasymunion ({\ttlbrace}1{\ttrbrace} <*> B) 

1089 
\tdx{QInl_def}: QInl(a) == <0;a> 

1090 
\tdx{QInr_def}: QInr(b) == <1;b> 

1091 
\tdx{qcase_def}: qcase(c,d) == qsplit(\%y z. cond(y, d(z), c(z))) 

1092 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1093 
\caption{Nonstandard pairs, products and sums} \label{zfqpair} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1094 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1095 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1096 

af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1097 
\subsection{Nonstandard ordered pairs} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1098 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1099 
Theory \thydx{QPair} defines a notion of ordered pair that admits 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1100 
nonwellfounded tupling (Fig.\ts\ref{zfqpair}). Such pairs are written 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1101 
{\tt<$a$;$b$>}. It also defines the eliminator \cdx{qsplit}, the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1102 
converse operator \cdx{qconverse}, and the summation operator 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1103 
\cdx{QSigma}. These are completely analogous to the corresponding 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1104 
versions for standard ordered pairs. The theory goes on to define a 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1105 
nonstandard notion of disjoint sum using nonstandard pairs. All of these 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1106 
concepts satisfy the same properties as their standard counterparts; in 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1107 
addition, {\tt<$a$;$b$>} is continuous. The theory supports coinductive 
6592  1108 
definitions, for example of infinite lists~\cite{paulsonmscs}. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1109 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1110 
\begin{figure} 
14154  1111 
\begin{alltt*}\isastyleminor 
1112 
\tdx{bnd_mono_def}: bnd_mono(D,h) == 

14158  1113 
h(D)\isasymsubseteq{}D & ({\isasymforall}W X. W\isasymsubseteq{}X > X\isasymsubseteq{}D > h(W)\isasymsubseteq{}h(X)) 
14154  1114 

1115 
\tdx{lfp_def}: lfp(D,h) == Inter({\ttlbrace}X \isasymin Pow(D). h(X) \isasymsubseteq X{\ttrbrace}) 

1116 
\tdx{gfp_def}: gfp(D,h) == Union({\ttlbrace}X \isasymin Pow(D). X \isasymsubseteq h(X){\ttrbrace}) 

1117 

1118 

14158  1119 
\tdx{lfp_lowerbound}: [ h(A) \isasymsubseteq A; A \isasymsubseteq D ] ==> lfp(D,h) \isasymsubseteq A 
14154  1120 

1121 
\tdx{lfp_subset}: lfp(D,h) \isasymsubseteq D 

1122 

1123 
\tdx{lfp_greatest}: [ bnd_mono(D,h); 

1124 
!!X. [ h(X) \isasymsubseteq X; X \isasymsubseteq D ] ==> A \isasymsubseteq X 

1125 
] ==> A \isasymsubseteq lfp(D,h) 

1126 

1127 
\tdx{lfp_Tarski}: bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h)) 

1128 

1129 
\tdx{induct}: [ a \isasymin lfp(D,h); bnd_mono(D,h); 

1130 
!!x. x \isasymin h(Collect(lfp(D,h),P)) ==> P(x) 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1131 
] ==> P(a) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1132 

14154  1133 
\tdx{lfp_mono}: [ bnd_mono(D,h); bnd_mono(E,i); 
1134 
!!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X) 

1135 
] ==> lfp(D,h) \isasymsubseteq lfp(E,i) 

1136 

14158  1137 
\tdx{gfp_upperbound}: [ A \isasymsubseteq h(A); A \isasymsubseteq D ] ==> A \isasymsubseteq gfp(D,h) 
14154  1138 

1139 
\tdx{gfp_subset}: gfp(D,h) \isasymsubseteq D 

1140 

1141 
\tdx{gfp_least}: [ bnd_mono(D,h); 

1142 
!!X. [ X \isasymsubseteq h(X); X \isasymsubseteq D ] ==> X \isasymsubseteq A 

1143 
] ==> gfp(D,h) \isasymsubseteq A 

1144 

1145 
\tdx{gfp_Tarski}: bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h)) 

1146 

1147 
\tdx{coinduct}: [ bnd_mono(D,h); a \isasymin X; X \isasymsubseteq h(X \isasymunion gfp(D,h)); X \isasymsubseteq D 

1148 
] ==> a \isasymin gfp(D,h) 

1149 

1150 
\tdx{gfp_mono}: [ bnd_mono(D,h); D \isasymsubseteq E; 

1151 
!!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X) 

1152 
] ==> gfp(D,h) \isasymsubseteq gfp(E,i) 

1153 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1154 
\caption{Least and greatest fixedpoints} \label{zffixedpt} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1155 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1156 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1157 

af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1158 
\subsection{Least and greatest fixedpoints} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1159 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1160 
The KnasterTarski Theorem states that every monotone function over a 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1161 
complete lattice has a fixedpoint. Theory \thydx{Fixedpt} proves the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1162 
Theorem only for a particular lattice, namely the lattice of subsets of a 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1163 
set (Fig.\ts\ref{zffixedpt}). The theory defines least and greatest 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1164 
fixedpoint operators with corresponding induction and coinduction rules. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1165 
These are essential to many definitions that follow, including the natural 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1166 
numbers and the transitive closure operator. The (co)inductive definition 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1167 
package also uses the fixedpoint operators~\cite{paulsonCADE}. See 
6745  1168 
Davey and Priestley~\cite{daveypriestley} for more on the KnasterTarski 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1169 
Theorem and my paper~\cite{paulsonsetII} for discussion of the Isabelle 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1170 
proofs. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1171 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1172 
Monotonicity properties are proved for most of the setforming operations: 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1173 
union, intersection, Cartesian product, image, domain, range, etc. These 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1174 
are useful for applying the KnasterTarski Fixedpoint Theorem. The proofs 
14154  1175 
themselves are trivial applications of Isabelle's classical reasoner. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1176 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1177 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1178 
\subsection{Finite sets and lists} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1179 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1180 
Theory \texttt{Finite} (Figure~\ref{zffin}) defines the finite set operator; 
14154  1181 
$\isa{Fin}(A)$ is the set of all finite sets over~$A$. The theory employs 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1182 
Isabelle's inductive definition package, which proves various rules 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1183 
automatically. The induction rule shown is stronger than the one proved by 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1184 
the package. The theory also defines the set of all finite functions 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1185 
between two given sets. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1186 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1187 
\begin{figure} 
14154  1188 
\begin{alltt*}\isastyleminor 
1189 
\tdx{Fin.emptyI} 0 \isasymin Fin(A) 

1190 
\tdx{Fin.consI} [ a \isasymin A; b \isasymin Fin(A) ] ==> cons(a,b) \isasymin Fin(A) 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1191 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1192 
\tdx{Fin_induct} 
14154  1193 
[ b \isasymin Fin(A); 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1194 
P(0); 
14158  1195 
!!x y. [ x\isasymin{}A; y\isasymin{}Fin(A); x\isasymnotin{}y; P(y) ] ==> P(cons(x,y)) 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1196 
] ==> P(b) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1197 

14154  1198 
\tdx{Fin_mono}: A \isasymsubseteq B ==> Fin(A) \isasymsubseteq Fin(B) 
1199 
\tdx{Fin_UnI}: [ b \isasymin Fin(A); c \isasymin Fin(A) ] ==> b \isasymunion c \isasymin Fin(A) 

1200 
\tdx{Fin_UnionI}: C \isasymin Fin(Fin(A)) ==> Union(C) \isasymin Fin(A) 

1201 
\tdx{Fin_subset}: [ c \isasymsubseteq b; b \isasymin Fin(A) ] ==> c \isasymin Fin(A) 

1202 
\end{alltt*} 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1203 
\caption{The finite set operator} \label{zffin} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1204 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1205 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1206 
\begin{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1207 
\begin{constants} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1208 
\it symbol & \it metatype & \it priority & \it description \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1209 
\cdx{list} & $i\To i$ && lists over some set\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1210 
\cdx{list_case} & $[i, [i,i]\To i, i] \To i$ && conditional for $list(A)$ \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1211 
\cdx{map} & $[i\To i, i] \To i$ & & mapping functional\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1212 
\cdx{length} & $i\To i$ & & length of a list\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1213 
\cdx{rev} & $i\To i$ & & reverse of a list\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1214 
\tt \at & $[i,i]\To i$ & Right 60 & append for lists\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1215 
\cdx{flat} & $i\To i$ & & append of list of lists 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1216 
\end{constants} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1217 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1218 
\underscoreon %%because @ is used here 
14154  1219 
\begin{alltt*}\isastyleminor 
14158  1220 
\tdx{NilI}: Nil \isasymin list(A) 
1221 
\tdx{ConsI}: [ a \isasymin A; l \isasymin list(A) ] ==> Cons(a,l) \isasymin list(A) 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1222 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1223 
\tdx{List.induct} 
14154  1224 
[ l \isasymin list(A); 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1225 
P(Nil); 
14154  1226 
!!x y. [ x \isasymin A; y \isasymin list(A); P(y) ] ==> P(Cons(x,y)) 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1227 
] ==> P(l) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1228 

14154  1229 
\tdx{Cons_iff}: Cons(a,l)=Cons(a',l') <> a=a' & l=l' 
1230 
\tdx{Nil_Cons_iff}: Nil \isasymnoteq Cons(a,l) 

1231 

1232 
\tdx{list_mono}: A \isasymsubseteq B ==> list(A) \isasymsubseteq list(B) 

1233 

14158  1234 
\tdx{map_ident}: l\isasymin{}list(A) ==> map(\%u. u, l) = l 
1235 
\tdx{map_compose}: l\isasymin{}list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l) 

1236 
\tdx{map_app_distrib}: xs\isasymin{}list(A) ==> map(h, xs@ys) = map(h,xs)@map(h,ys) 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1237 
\tdx{map_type} 
14158  1238 
[ l\isasymin{}list(A); !!x. x\isasymin{}A ==> h(x)\isasymin{}B ] ==> map(h,l)\isasymin{}list(B) 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1239 
\tdx{map_flat} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1240 
ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls)) 
14154  1241 
\end{alltt*} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1242 
\caption{Lists} \label{zflist} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1243 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1244 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1245 

14154  1246 
Figure~\ref{zflist} presents the set of lists over~$A$, $\isa{list}(A)$. The 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1247 
definition employs Isabelle's datatype package, which defines the introduction 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1248 
and induction rules automatically, as well as the constructors, case operator 
14154  1249 
(\isa{list\_case}) and recursion operator. The theory then defines the usual 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1250 
list functions by primitive recursion. See theory \texttt{List}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1251 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1252 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1253 
\subsection{Miscellaneous} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1254 

af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1255 
\begin{figure} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1256 
\begin{constants} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1257 
\it symbol & \it metatype & \it priority & \it description \\ 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1258 
\sdx{O} & $[i,i]\To i$ & Right 60 & composition ($\circ$) \\ 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1259 
\cdx{id} & $i\To i$ & & identity function \\ 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1260 
\cdx{inj} & $[i,i]\To i$ & & injective function space\\ 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1261 
\cdx{surj} & $[i,i]\To i$ & & surjective function space\\ 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1262 
\cdx{bij} & $[i,i]\To i$ & & bijective function space 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1263 
\end{constants} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1264 

14154  1265 
\begin{alltt*}\isastyleminor 
1266 
\tdx{comp_def}: r O s == {\ttlbrace}xz \isasymin domain(s)*range(r) . 

1267 
{\isasymexists}x y z. xz=<x,z> & <x,y> \isasymin s & <y,z> \isasymin r{\ttrbrace} 

1268 
\tdx{id_def}: id(A) == (lam x \isasymin A. x) 

14158  1269 
\tdx{inj_def}: inj(A,B) == {\ttlbrace} f\isasymin{}A>B. {\isasymforall}w\isasymin{}A. {\isasymforall}x\isasymin{}A. f`w=f`x > w=x {\ttrbrace} 
1270 
\tdx{surj_def}: surj(A,B) == {\ttlbrace} f\isasymin{}A>B . {\isasymforall}y\isasymin{}B. {\isasymexists}x\isasymin{}A. f`x=y {\ttrbrace} 

1271 
\tdx{bij_def}: bij(A,B) == inj(A,B) \isasyminter surj(A,B) 

1272 

1273 

1274 
\tdx{left_inverse}: [ f\isasymin{}inj(A,B); a\isasymin{}A ] ==> converse(f)`(f`a) = a 

1275 
\tdx{right_inverse}: [ f\isasymin{}inj(A,B); b\isasymin{}range(f) ] ==> 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1276 
f`(converse(f)`b) = b 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1277 

14158  1278 
\tdx{inj_converse_inj}: f\isasymin{}inj(A,B) ==> converse(f) \isasymin inj(range(f),A) 
1279 
\tdx{bij_converse_bij}: f\isasymin{}bij(A,B) ==> converse(f) \isasymin bij(B,A) 

1280 

1281 
\tdx{comp_type}: [ s \isasymsubseteq A*B; r \isasymsubseteq B*C ] ==> (r O s) \isasymsubseteq A*C 

1282 
\tdx{comp_assoc}: (r O s) O t = r O (s O t) 

1283 

1284 
\tdx{left_comp_id}: r \isasymsubseteq A*B ==> id(B) O r = r 

1285 
\tdx{right_comp_id}: r \isasymsubseteq A*B ==> r O id(A) = r 

1286 

1287 
\tdx{comp_func}: [ g\isasymin{}A>B; f\isasymin{}B>C ] ==> (f O g) \isasymin A>C 

1288 
\tdx{comp_func_apply}: [ g\isasymin{}A>B; f\isasymin{}B>C; a\isasymin{}A ] ==> (f O g)`a = f`(g`a) 

1289 

1290 
\tdx{comp_inj}: [ g\isasymin{}inj(A,B); f\isasymin{}inj(B,C) ] ==> (f O g)\isasymin{}inj(A,C) 

1291 
\tdx{comp_surj}: [ g\isasymin{}surj(A,B); f\isasymin{}surj(B,C) ] ==> (f O g)\isasymin{}surj(A,C) 

1292 
\tdx{comp_bij}: [ g\isasymin{}bij(A,B); f\isasymin{}bij(B,C) ] ==> (f O g)\isasymin{}bij(A,C) 

1293 

1294 
\tdx{left_comp_inverse}: f\isasymin{}inj(A,B) ==> converse(f) O f = id(A) 

1295 
\tdx{right_comp_inverse}: f\isasymin{}surj(A,B) ==> f O converse(f) = id(B) 

14154  1296 

1297 
\tdx{bij_disjoint_Un}: 

14158  1298 
[ f\isasymin{}bij(A,B); g\isasymin{}bij(C,D); A \isasyminter C = 0; B \isasyminter D = 0 ] ==> 
1299 
(f \isasymunion g)\isasymin{}bij(A \isasymunion C, B \isasymunion D) 

1300 

1301 
\tdx{restrict_bij}: [ f\isasymin{}inj(A,B); C\isasymsubseteq{}A ] ==> restrict(f,C)\isasymin{}bij(C, f``C) 

14154  1302 
\end{alltt*} 
9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1303 
\caption{Permutations} \label{zfperm} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1304 
\end{figure} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1305 

af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1306 
The theory \thydx{Perm} is concerned with permutations (bijections) and 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1307 
related concepts. These include composition of relations, the identity 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1308 
relation, and three specialized function spaces: injective, surjective and 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1309 
bijective. Figure~\ref{zfperm} displays many of their properties that 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1310 
have been proved. These results are fundamental to a treatment of 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1311 
equipollence and cardinality. 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1312 

14154  1313 
Theory \thydx{Univ} defines a `universe' $\isa{univ}(A)$, which is used by 
9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1314 
the datatype package. This set contains $A$ and the 
14154  1315 
natural numbers. Vitally, it is closed under finite products: 
1316 
$\isa{univ}(A)\times\isa{univ}(A)\subseteq\isa{univ}(A)$. This theory also 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1317 
defines the cumulative hierarchy of axiomatic set theory, which 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1318 
traditionally is written $V@\alpha$ for an ordinal~$\alpha$. The 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1319 
`universe' is a simple generalization of~$V@\omega$. 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1320 

14154  1321 
Theory \thydx{QUniv} defines a `universe' $\isa{quniv}(A)$, which is used by 
9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1322 
the datatype package to construct codatatypes such as streams. It is 
14154  1323 
analogous to $\isa{univ}(A)$ (and is defined in terms of it) but is closed 
9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1324 
under the nonstandard product and sum. 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1325 

af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1326 

6173  1327 
\section{Automatic Tools} 
1328 

9695  1329 
ZF provides the simplifier and the classical reasoner. Moreover it supplies a 
1330 
specialized tool to infer `types' of terms. 

6173  1331 

14154  1332 
\subsection{Simplification and Classical Reasoning} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1333 

9695  1334 
ZF inherits simplification from FOL but adopts it for set theory. The 
1335 
extraction of rewrite rules takes the ZF primitives into account. It can 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1336 
strip bounded universal quantifiers from a formula; for example, ${\forall 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1337 
x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1338 
f(x)=g(x)$. Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1339 
A$ and~$P(a)$. It can also break down $a\in A\int B$ and $a\in AB$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1340 

14154  1341 
The default simpset used by \isa{simp} contains congruence rules for all of ZF's 
1342 
binding operators. It contains all the conversion rules, such as 

1343 
\isa{fst} and 

1344 
\isa{snd}, as well as the rewrites shown in Fig.\ts\ref{zfsimpdata}. 

1345 

1346 
Classical reasoner methods such as \isa{blast} and \isa{auto} refer to 

1347 
a rich collection of builtin axioms for all the settheoretic 

1348 
primitives. 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1349 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1350 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1351 
\begin{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1352 
\begin{eqnarray*} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1353 
a\in \emptyset & \bimp & \bot\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1354 
a \in A \un B & \bimp & a\in A \disj a\in B\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1355 
a \in A \int B & \bimp & a\in A \conj a\in B\\ 
14154  1356 
a \in AB & \bimp & a\in A \conj \lnot (a\in B)\\ 
1357 
\pair{a,b}\in \isa{Sigma}(A,B) 

6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1358 
& \bimp & a\in A \conj b\in B(a)\\ 
14154  1359 
a \in \isa{Collect}(A,P) & \bimp & a\in A \conj P(a)\\ 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1360 
(\forall x \in \emptyset. P(x)) & \bimp & \top\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1361 
(\forall x \in A. \top) & \bimp & \top 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1362 
\end{eqnarray*} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1363 
\caption{Some rewrite rules for set theory} \label{zfsimpdata} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1364 
\end{figure} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1365 

5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1366 

6173  1367 
\subsection{TypeChecking Tactics} 
1368 
\index{typechecking tactics} 

1369 

9695  1370 
Isabelle/ZF provides simple tactics to help automate those proofs that are 
6173  1371 
essentially typechecking. Such proofs are built by applying rules such as 
1372 
these: 

14154  1373 
\begin{ttbox}\isastyleminor 
14158 