author  paulson 
Tue, 19 Aug 2003 18:45:48 +0200  
changeset 14154  3bc0128e2c74 
parent 9836  56b632fd1dcd 
child 14158  15bab630ae31 
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 \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

234 
&  & term " Int " 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)) 

376 
\tdx{Int_def}: A Int B == Inter(Upair(A,B)) 

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 

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

437 
Other consequences of replacement include functional replacement 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

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

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

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

442 

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

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

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

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

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

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

449 

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

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

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

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

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

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

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

456 

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

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

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

459 
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

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

461 

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

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

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

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

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

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

468 

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

469 

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

471 

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

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

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

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

477 

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

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

480 

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

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

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

484 

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

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

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

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

488 

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

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

492 
\tdx{subset_refl}: A \isasymsubseteq A 

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

494 

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

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

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

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

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

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

500 

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

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

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

505 

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

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

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

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

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

512 

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

513 

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

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

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

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

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

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

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

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

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

522 

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

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

524 
Figure~\ref{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

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

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

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

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

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

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

531 

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

532 
Figure~\ref{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

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

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

535 

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

536 
Figure~\ref{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

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

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

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

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

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

545 

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

546 
Figure~\ref{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

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

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

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

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

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

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

554 

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

555 

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

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

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

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

561 

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

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

564 
] ==> R 

565 

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

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

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

569 

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

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

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

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

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

575 
\end{alltt*} 

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

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

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

578 

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

579 

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

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

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

584 

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

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

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

588 

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

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

591 
] ==> R 

592 

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

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

595 
\end{alltt*} 

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

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

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

598 

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

599 

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

601 

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

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

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

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

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

608 
\end{alltt*} 

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

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

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

611 

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

612 

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

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

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

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

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

619 

620 
\tdx{IntI}: [ c\isasymin{}A; c\isasymin{}B ] ==> c\isasymin{}A Int B 

621 
\tdx{IntD1}: c\isasymin{}A Int B ==> c\isasymin{}A 

622 
\tdx{IntD2}: c\isasymin{}A Int B ==> c\isasymin{}B 

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

624 

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

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

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

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

629 
\end{alltt*} 

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

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

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

632 

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

633 

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

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

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

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

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

640 

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

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

643 
\end{alltt*} 

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

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

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

646 

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

647 

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

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

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

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

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

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

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

656 
\end{alltt*} 

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

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

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

659 

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

660 

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

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

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

665 

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

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

668 

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

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

671 
\end{alltt*} 

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

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

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

674 

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

675 

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

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

677 
Figure~\ref{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

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

679 
of ordered pairs (Fig.\ts\ref{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

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

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

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

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

685 

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

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

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

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

691 

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

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

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

694 
(Fig.\ts\ref{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

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

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

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

698 

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

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

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

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

702 

14154  703 

704 
%%% subset.thy? 

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

705 

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

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

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

710 

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

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

713 

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

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

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

717 

718 
\tdx{Int_lower1}: A Int B \isasymsubseteq A 

719 
\tdx{Int_lower2}: A Int B \isasymsubseteq B 

720 
\tdx{Int_greatest}: [ C \isasymsubseteq A; C \isasymsubseteq B ] ==> C \isasymsubseteq A Int B 

721 

722 
\tdx{Diff_subset}: AB \isasymsubseteq A 

723 
\tdx{Diff_contains}: [ C \isasymsubseteq A; C Int B = 0 ] ==> C \isasymsubseteq AB 

724 

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

726 
\end{alltt*} 

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

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

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

729 

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

730 

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

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

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

733 
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

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

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

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

740 

741 
%%% pair.thy 

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

742 

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

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

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

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

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

749 

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

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

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

753 

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

755 

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

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

758 

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

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

761 
\end{alltt*} 

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

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

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

764 

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

765 

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

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

767 

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

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

771 
expressed as two destruction rules, 

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

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

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

774 

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

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

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

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

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

779 

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

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

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

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

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

785 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

809 

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

810 

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

812 

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

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

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

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

818 

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

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

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

822 

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

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

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

826 

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

828 
!!x. <a,x>\isasymin{}r ==> P; 

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

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

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

831 

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

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

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

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

836 

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

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

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

841 

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

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

844 
\end{alltt*} 

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

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

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

847 

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

848 

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

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

850 
Figure~\ref{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

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

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

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

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

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

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

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

858 

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

859 
Figure~\ref{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

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

863 

864 
%%% func.thy 

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

865 

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

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

869 

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

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

872 

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

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

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

876 

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

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

879 

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

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

882 

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

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

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

886 

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

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

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

890 
\end{alltt*} 

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

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

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

893 

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

894 

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

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

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

8249  899 
] ==> P 
900 

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

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

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

905 
\end{alltt*} 

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

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

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

908 

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

909 

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

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

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

914 

915 
\tdx{fun_disjoint_Un}: [ f\isasymin{}A>B; g\isasymin{}C>D; A Int C = 0 ] ==> 

916 
(f \isasymunion g)\isasymin{}(A \isasymunion C) > (B \isasymunion D) 

917 

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

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

920 

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

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

923 
\end{alltt*} 

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

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

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

926 

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

927 

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

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

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

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

932 

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

933 
Figure~\ref{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

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

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

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

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

938 

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

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

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

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

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

944 

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

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

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

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

948 
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

949 

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

950 
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

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

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

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

954 

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

955 

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

956 
\begin{figure} 
14154  957 
\begin{alltt*}\isastyleminor 
958 
\tdx{Int_absorb}: A Int A = A 

959 
\tdx{Int_commute}: A Int B = B Int A 

960 
\tdx{Int_assoc}: (A Int B) Int C = A Int (B Int C) 

961 
\tdx{Int_Un_distrib}: (A \isasymunion B) Int C = (A Int C) \isasymunion (B Int C) 

962 

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

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

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

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

967 

968 
\tdx{Diff_cancel}: AA = 0 

969 
\tdx{Diff_disjoint}: A Int (BA) = 0 

970 
\tdx{Diff_partition}: A \isasymsubseteq B ==> A \isasymunion (BA) = B 

971 
\tdx{double_complement}: [ A \isasymsubseteq B; B \isasymsubseteq C ] ==> (B  (CA)) = A 

972 
\tdx{Diff_Un}: A  (B \isasymunion C) = (AB) Int (AC) 

973 
\tdx{Diff_Int}: A  (B Int C) = (AB) \isasymunion (AC) 

974 

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

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

977 
Inter(A \isasymunion B) = Inter(A) Int Inter(B) 

978 

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

980 

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

982 
A \isasymunion Inter(B) = ({\isasymInter}C \isasymin B. A \isasymunion C) 

983 

984 
\tdx{SUM_Un_distrib1}: (SUM x \isasymin A \isasymunion B. C(x)) = 

985 
(SUM x \isasymin A. C(x)) \isasymunion (SUM x \isasymin B. C(x)) 

986 

987 
\tdx{SUM_Un_distrib2}: (SUM x \isasymin C. A(x) \isasymunion B(x)) = 

988 
(SUM x \isasymin C. A(x)) \isasymunion (SUM x \isasymin C. B(x)) 

989 

990 
\tdx{SUM_Int_distrib1}: (SUM x \isasymin A Int B. C(x)) = 

991 
(SUM x \isasymin A. C(x)) Int (SUM x \isasymin B. C(x)) 

992 

993 
\tdx{SUM_Int_distrib2}: (SUM x \isasymin C. A(x) Int B(x)) = 

994 
(SUM x \isasymin C. A(x)) Int (SUM x \isasymin C. B(x)) 

995 
\end{alltt*} 

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

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

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

998 

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

999 

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

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

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

1002 
% \cdx{1} & $i$ & & $\{\emptyset\}$ \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1003 
% \cdx{bool} & $i$ & & the set $\{\emptyset,1\}$ \\ 
14154  1004 
% \cdx{cond} & $[i,i,i]\To i$ & & conditional for \isa{bool} \\ 
1005 
% \cdx{not} & $i\To i$ & & negation for \isa{bool} \\ 

1006 
% \sdx{and} & $[i,i]\To i$ & Left 70 & conjunction for \isa{bool} \\ 

1007 
% \sdx{or} & $[i,i]\To i$ & Left 65 & disjunction for \isa{bool} \\ 

1008 
% \sdx{xor} & $[i,i]\To i$ & Left 65 & exclusiveor for \isa{bool} 

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

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

1010 
% 
14154  1011 
\begin{alltt*}\isastyleminor 
1012 
\tdx{bool_def}: bool == {\ttlbrace}0,1{\ttrbrace} 

1013 
\tdx{cond_def}: cond(b,c,d) == if b=1 then c else d 

1014 
\tdx{not_def}: not(b) == cond(b,0,1) 

1015 
\tdx{and_def}: a and b == cond(a,b,0) 

1016 
\tdx{or_def}: a or b == cond(a,1,b) 

1017 
\tdx{xor_def}: a xor b == cond(a,not(b),b) 

1018 

1019 
\tdx{bool_1I}: 1 \isasymin bool 

1020 
\tdx{bool_0I}: 0 \isasymin bool 

1021 
\tdx{boolE}: [ c \isasymin bool; c=1 ==> P; c=0 ==> P ] ==> P 

1022 
\tdx{cond_1}: cond(1,c,d) = c 

1023 
\tdx{cond_0}: cond(0,c,d) = d 

1024 
\end{alltt*} 

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

1025 
\caption{The booleans} \label{zfbool} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

1027 

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

1028 

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

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

1030 
The next group of developments is complex and extensive, and only 
14154  1031 
highlights can be covered here. It involves many theories and proofs. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1032 

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

1033 
Figure~\ref{zfequalities} presents commutative, associative, distributive, 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1034 
and idempotency laws of union and intersection, along with other equations. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1035 

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

1036 
Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual 
9695  1037 
operators including a conditional (Fig.\ts\ref{zfbool}). Although ZF is a 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1038 
firstorder theory, you can obtain the effect of higherorder logic using 
14154  1039 
\isa{bool}valued functions, for example. The constant~\isa{1} is 
1040 
translated to \isa{succ(0)}. 

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

1041 

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

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

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

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

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

1046 
\tt + & $[i,i]\To i$ & Right 65 & disjoint union operator\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1047 
\cdx{Inl}~~\cdx{Inr} & $i\To i$ & & injections\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1048 
\cdx{case} & $[i\To i,i\To i, i]\To i$ & & conditional for $A+B$ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1049 
\end{constants} 
14154  1050 
\begin{alltt*}\isastyleminor 
1051 
\tdx{sum_def}: A+B == {\ttlbrace}0{\ttrbrace}*A \isasymunion {\ttlbrace}1{\ttrbrace}*B 

1052 
\tdx{Inl_def}: Inl(a) == <0,a> 

1053 
\tdx{Inr_def}: Inr(b) == <1,b> 

1054 
\tdx{case_def}: case(c,d,u) == split(\%y z. cond(y, d(z), c(z)), u) 

1055 

1056 
\tdx{InlI}: a \isasymin A ==> Inl(a) \isasymin A+B 

1057 
\tdx{InrI}: b \isasymin B ==> Inr(b) \isasymin A+B 

1058 

1059 
\tdx{Inl_inject}: Inl(a)=Inl(b) ==> a=b 

1060 
\tdx{Inr_inject}: Inr(a)=Inr(b) ==> a=b 

1061 
\tdx{Inl_neq_Inr}: Inl(a)=Inr(b) ==> P 

1062 

1063 
\tdx{sum_iff}: u \isasymin A+B <> ({\isasymexists}x\isasymin{}A. u=Inl(x))  ({\isasymexists}y\isasymin{}B. u=Inr(y)) 

1064 

1065 
\tdx{case_Inl}: case(c,d,Inl(a)) = c(a) 

1066 
\tdx{case_Inr}: case(c,d,Inr(b)) = d(b) 

1067 
\end{alltt*} 

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

1068 
\caption{Disjoint unions} \label{zfsum} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

1070 

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

1071 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1072 
\subsection{Disjoint unions} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1073 

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

1074 
Theory \thydx{Sum} defines the disjoint union of two sets, with 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1075 
injections and a case analysis operator (Fig.\ts\ref{zfsum}). Disjoint 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1076 
unions play a role in datatype definitions, particularly when there is 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1077 
mutual recursion~\cite{paulsonsetII}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1078 

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

1079 
\begin{figure} 
14154  1080 
\begin{alltt*}\isastyleminor 
1081 
\tdx{QPair_def}: <a;b> == a+b 

1082 
\tdx{qsplit_def}: qsplit(c,p) == THE y. {\isasymexists}a b. p=<a;b> & y=c(a,b) 

1083 
\tdx{qfsplit_def}: qfsplit(R,z) == {\isasymexists}x y. z=<x;y> & R(x,y) 

1084 
\tdx{qconverse_def}: qconverse(r) == {\ttlbrace}z. w \isasymin r, {\isasymexists}x y. w=<x;y> & z=<y;x>{\ttrbrace} 

1085 
\tdx{QSigma_def}: QSigma(A,B) == {\isasymUnion}x \isasymin A. {\isasymUnion}y \isasymin B(x). {\ttlbrace}<x;y>{\ttrbrace} 

1086 

1087 
\tdx{qsum_def}: A <+> B == ({\ttlbrace}0{\ttrbrace} <*> A) \isasymunion ({\ttlbrace}1{\ttrbrace} <*> B) 

1088 
\tdx{QInl_def}: QInl(a) == <0;a> 

1089 
\tdx{QInr_def}: QInr(b) == <1;b> 

1090 
\tdx{qcase_def}: qcase(c,d) == qsplit(\%y z. cond(y, d(z), c(z))) 

1091 
\end{alltt*} 

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

1092 
\caption{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

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

1094 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1095 

af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1096 
\subsection{Nonstandard ordered pairs} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1097 

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

1098 
Theory \thydx{QPair} defines a notion of ordered pair that admits 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1099 
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

1100 
{\tt<$a$;$b$>}. It also defines the eliminator \cdx{qsplit}, the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1101 
converse operator \cdx{qconverse}, and the summation operator 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1102 
\cdx{QSigma}. These are completely analogous to the corresponding 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1103 
versions for standard ordered pairs. The theory goes on to define a 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1104 
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

1105 
concepts satisfy the same properties as their standard counterparts; in 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1106 
addition, {\tt<$a$;$b$>} is continuous. The theory supports coinductive 
6592  1107 
definitions, for example of infinite lists~\cite{paulsonmscs}. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1108 

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

1109 
\begin{figure} 
14154  1110 
\begin{alltt*}\isastyleminor 
1111 
\tdx{bnd_mono_def}: bnd_mono(D,h) == 

1112 
h(D) \isasymsubseteq D & ({\isasymforall}W X. W \isasymsubseteq X > X \isasymsubseteq D > h(W) \isasymsubseteq h(X)) 

1113 

1114 
\tdx{lfp_def}: lfp(D,h) == Inter({\ttlbrace}X \isasymin Pow(D). h(X) \isasymsubseteq X{\ttrbrace}) 

1115 
\tdx{gfp_def}: gfp(D,h) == Union({\ttlbrace}X \isasymin Pow(D). X \isasymsubseteq h(X){\ttrbrace}) 

1116 

1117 

1118 
\tdx{lfp_lowerbound} [ h(A) \isasymsubseteq A; A \isasymsubseteq D ] ==> lfp(D,h) \isasymsubseteq A 

1119 

1120 
\tdx{lfp_subset}: lfp(D,h) \isasymsubseteq D 

1121 

1122 
\tdx{lfp_greatest}: [ bnd_mono(D,h); 

1123 
!!X. [ h(X) \isasymsubseteq X; X \isasymsubseteq D ] ==> A \isasymsubseteq X 

1124 
] ==> A \isasymsubseteq lfp(D,h) 

1125 

1126 
\tdx{lfp_Tarski}: bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h)) 

1127 

1128 
\tdx{induct}: [ a \isasymin lfp(D,h); bnd_mono(D,h); 

1129 
!!x. x \isasymin h(Collect(lfp(D,h),P)) ==> P(x) 

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

1130 
] ==> P(a) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1131 

14154  1132 
\tdx{lfp_mono}: [ bnd_mono(D,h); bnd_mono(E,i); 
1133 
!!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X) 

1134 
] ==> lfp(D,h) \isasymsubseteq lfp(E,i) 

1135 

1136 
\tdx{gfp_upperbound} [ A \isasymsubseteq h(A); A \isasymsubseteq D ] ==> A \isasymsubseteq gfp(D,h) 

1137 

1138 
\tdx{gfp_subset}: gfp(D,h) \isasymsubseteq D 

1139 

1140 
\tdx{gfp_least}: [ bnd_mono(D,h); 

1141 
!!X. [ X \isasymsubseteq h(X); X \isasymsubseteq D ] ==> X \isasymsubseteq A 

1142 
] ==> gfp(D,h) \isasymsubseteq A 

1143 

1144 
\tdx{gfp_Tarski}: bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h)) 

1145 

1146 
\tdx{coinduct}: [ bnd_mono(D,h); a \isasymin X; X \isasymsubseteq h(X \isasymunion gfp(D,h)); X \isasymsubseteq D 

1147 
] ==> a \isasymin gfp(D,h) 

1148 

1149 
\tdx{gfp_mono}: [ bnd_mono(D,h); D \isasymsubseteq E; 

1150 
!!X. X \isasymsubseteq D ==> h(X) \isasymsubseteq i(X) 

1151 
] ==> gfp(D,h) \isasymsubseteq gfp(E,i) 

1152 
\end{alltt*} 

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

1153 
\caption{Least and greatest fixedpoints} \label{zffixedpt} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

1155 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1156 

af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1157 
\subsection{Least and greatest fixedpoints} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1158 

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

1159 
The 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

1160 
complete lattice has a fixedpoint. Theory \thydx{Fixedpt} proves the 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1161 
Theorem only for a particular lattice, namely the lattice of subsets of a 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1162 
set (Fig.\ts\ref{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

1163 
fixedpoint operators with corresponding induction and coinduction rules. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1164 
These are essential to many definitions that follow, including the natural 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1165 
numbers and the transitive closure operator. The (co)inductive definition 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1166 
package also uses the fixedpoint operators~\cite{paulsonCADE}. See 
6745  1167 
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

1168 
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

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

1170 

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

1171 
Monotonicity properties are proved for most of the setforming operations: 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1172 
union, intersection, Cartesian product, image, domain, range, etc. These 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1173 
are useful for applying the KnasterTarski Fixedpoint Theorem. The proofs 
14154  1174 
themselves are trivial applications of Isabelle's classical reasoner. 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1175 

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

1176 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1177 
\subsection{Finite sets and lists} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1178 

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

1179 
Theory \texttt{Finite} (Figure~\ref{zffin}) defines the finite set operator; 
14154  1180 
$\isa{Fin}(A)$ is the set of all finite sets over~$A$. The theory employs 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1181 
Isabelle's inductive definition package, which proves various rules 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1182 
automatically. The induction rule shown is stronger than the one proved by 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1183 
the package. The theory also defines the set of all finite functions 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1184 
between two given sets. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1185 

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

1186 
\begin{figure} 
14154  1187 
\begin{alltt*}\isastyleminor 
1188 
\tdx{Fin.emptyI} 0 \isasymin Fin(A) 

1189 
\tdx{Fin.consI} [ a \isasymin A; b \isasymin Fin(A) ] ==> cons(a,b) \isasymin Fin(A) 

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

1190 

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

1191 
\tdx{Fin_induct} 
14154  1192 
[ b \isasymin Fin(A); 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1193 
P(0); 
14154  1194 
!!x y. [ x \isasymin A; y \isasymin Fin(A); x \isasymnotin y; P(y) ] ==> P(cons(x,y)) 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1195 
] ==> P(b) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1196 

14154  1197 
\tdx{Fin_mono}: A \isasymsubseteq B ==> Fin(A) \isasymsubseteq Fin(B) 
1198 
\tdx{Fin_UnI}: [ b \isasymin Fin(A); c \isasymin Fin(A) ] ==> b \isasymunion c \isasymin Fin(A) 

1199 
\tdx{Fin_UnionI}: C \isasymin Fin(Fin(A)) ==> Union(C) \isasymin Fin(A) 

1200 
\tdx{Fin_subset}: [ c \isasymsubseteq b; b \isasymin Fin(A) ] ==> c \isasymin Fin(A) 

1201 
\end{alltt*} 

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

1202 
\caption{The finite set operator} \label{zffin} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

1204 

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

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

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

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

1208 
\cdx{list} & $i\To i$ && lists over some set\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1209 
\cdx{list_case} & $[i, [i,i]\To i, i] \To i$ && conditional for $list(A)$ \\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

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

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

1213 
\tt \at & $[i,i]\To i$ & Right 60 & append for lists\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1214 
\cdx{flat} & $i\To i$ & & append of list of lists 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

1216 

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

1217 
\underscoreon %%because @ is used here 
14154  1218 
\begin{alltt*}\isastyleminor 
1219 
\tdx{NilI}: Nil \isasymin list(A) 

1220 
\tdx{ConsI}: [ a \isasymin A; l \isasymin list(A) ] ==> Cons(a,l) \isasymin list(A) 

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

1221 

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

1222 
\tdx{List.induct} 
14154  1223 
[ l \isasymin list(A); 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1224 
P(Nil); 
14154  1225 
!!x y. [ x \isasymin A; y \isasymin list(A); P(y) ] ==> P(Cons(x,y)) 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1226 
] ==> P(l) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1227 

14154  1228 
\tdx{Cons_iff}: Cons(a,l)=Cons(a',l') <> a=a' & l=l' 
1229 
\tdx{Nil_Cons_iff}: Nil \isasymnoteq Cons(a,l) 

1230 

1231 
\tdx{list_mono}: A \isasymsubseteq B ==> list(A) \isasymsubseteq list(B) 

1232 

1233 
\tdx{map_ident}: l \isasymin list(A) ==> map(\%u. u, l) = l 

1234 
\tdx{map_compose}: l \isasymin list(A) ==> map(h, map(j,l)) = map(\%u. h(j(u)), l) 

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

1235 
\tdx{map_app_distrib} xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys) 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1236 
\tdx{map_type} 
14154  1237 
[ l \isasymin list(A); !!x. x \isasymin A ==> h(x) \isasymin B ] ==> map(h,l) \isasymin list(B) 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

1239 
ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls)) 
14154  1240 
\end{alltt*} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

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

1243 

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

1244 

14154  1245 
Figure~\ref{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

1246 
definition employs Isabelle's datatype package, which defines the introduction 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1247 
and induction rules automatically, as well as the constructors, case operator 
14154  1248 
(\isa{list\_case}) and recursion operator. The theory then defines the usual 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1249 
list functions by primitive recursion. See theory \texttt{List}. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1250 

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

1251 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1252 
\subsection{Miscellaneous} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1253 

af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1254 
\begin{figure} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1255 
\begin{constants} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1256 
\it symbol & \it metatype & \it priority & \it description \\ 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1257 
\sdx{O} & $[i,i]\To i$ & Right 60 & composition ($\circ$) \\ 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1258 
\cdx{id} & $i\To i$ & & identity function \\ 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1259 
\cdx{inj} & $[i,i]\To i$ & & injective function space\\ 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1260 
\cdx{surj} & $[i,i]\To i$ & & surjective function space\\ 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1261 
\cdx{bij} & $[i,i]\To i$ & & bijective function space 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1262 
\end{constants} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1263 

14154  1264 
\begin{alltt*}\isastyleminor 
1265 
\tdx{comp_def}: r O s == {\ttlbrace}xz \isasymin domain(s)*range(r) . 

1266 
{\isasymexists}x y z. xz=<x,z> & <x,y> \isasymin s & <y,z> \isasymin r{\ttrbrace} 

1267 
\tdx{id_def}: id(A) == (lam x \isasymin A. x) 

1268 
\tdx{inj_def}: inj(A,B) == {\ttlbrace} f \isasymin A>B. {\isasymforall}w \isasymin A. {\isasymforall}x \isasymin A. f`w=f`x > w=x {\ttrbrace} 

1269 
\tdx{surj_def}: surj(A,B) == {\ttlbrace} f \isasymin A>B . {\isasymforall}y \isasymin B. {\isasymexists}x \isasymin A. f`x=y {\ttrbrace} 

1270 
\tdx{bij_def}: bij(A,B) == inj(A,B) Int surj(A,B) 

1271 

1272 

1273 
\tdx{left_inverse}: [ f \isasymin inj(A,B); a \isasymin A ] ==> converse(f)`(f`a) = a 

1274 
\tdx{right_inverse}: [ f \isasymin inj(A,B); b \isasymin range(f) ] ==> 

9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1275 
f`(converse(f)`b) = b 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1276 

14154  1277 
\tdx{inj_converse_inj} f \isasymin inj(A,B) ==> converse(f) \isasymin inj(range(f), A) 
1278 
\tdx{bij_converse_bij} f \isasymin bij(A,B) ==> converse(f) \isasymin bij(B,A) 

1279 

1280 
\tdx{comp_type}: [ s \isasymsubseteq A*B; r \isasymsubseteq B*C ] ==> (r O s) \isasymsubseteq A*C 

1281 
\tdx{comp_assoc}: (r O s) O t = r O (s O t) 

1282 

1283 
\tdx{left_comp_id}: r \isasymsubseteq A*B ==> id(B) O r = r 

1284 
\tdx{right_comp_id}: r \isasymsubseteq A*B ==> r O id(A) = r 

1285 

1286 
\tdx{comp_func}: [ g \isasymin A>B; f \isasymin B>C ] ==> (f O g) 

1287 
\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):inj(A,C) 

1291 
\tdx{comp_surj}: [ g \isasymin surj(A,B); f \isasymin surj(B,C) ] ==> (f O g):surj(A,C) 

1292 
\tdx{comp_bij}: [ g \isasymin bij(A,B); f \isasymin bij(B,C) ] ==> (f O g):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) 

1296 

1297 
\tdx{bij_disjoint_Un}: 

1298 
[ f \isasymin bij(A,B); g \isasymin bij(C,D); A Int C = 0; B Int 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) 

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 