author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 48985  5386df44a037 
permissions  rwrr 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

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

3 

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

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

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

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

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

9 

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

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

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

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

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

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

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

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

17 

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

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

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

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

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

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

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

24 

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

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

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

27 
nonwellfounded data structures within the standard {\sc zf} axioms including 
6592  28 
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

29 

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

30 

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

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

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

33 
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

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

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

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

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

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

39 

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

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

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

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

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

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

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

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

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

48 

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

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

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

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

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

53 

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

54 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

87 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

110 

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

111 

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

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

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

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

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

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

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

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

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

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

121 

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

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

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

126 

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

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

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

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

131 

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

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

135 
is~\tydx{o}. 

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

136 

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

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

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

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

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

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

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

144 

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

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

148 
the constant 

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

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

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

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

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

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

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

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

158 

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

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

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

163 

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

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

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

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

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

169 

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

170 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

214 

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

215 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

263 

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

264 

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

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

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

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

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

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

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

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

273 

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

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

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

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

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

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

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

281 
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

282 

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

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

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

285 
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

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

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

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

291 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

316 

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

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

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

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

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

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

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

325 

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

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

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

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

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

331 

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

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

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

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

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

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

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

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

341 

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

342 

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

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

344 

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

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

348 

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

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

351 

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

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

354 

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

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

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

358 

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

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

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

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

362 

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

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

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

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

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

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

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

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

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

372 

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

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

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

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

381 

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

382 

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

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

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

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

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

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

389 

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

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

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

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

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

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

396 

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

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

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

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

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

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

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

404 

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

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

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

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

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

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

413 

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

414 

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

415 

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

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

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

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

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

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

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

423 

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

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

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

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

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

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

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

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

435 

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

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

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

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

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

441 
from replacement~\cite[pages 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 

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

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

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

14154  624 

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

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

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

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

629 
\end{alltt*} 

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

630 
\caption{Union, intersection, difference} \label{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 

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

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

14154  721 

722 
\tdx{Diff_subset}: AB \isasymsubseteq A 

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

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

726 
\end{alltt*} 

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

727 
\caption{Subset and lattice properties} \label{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); 

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

830 
] ==> P 

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

831 

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

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

834 
\caption{Domain, range and field of a relation} \label{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 

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

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

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

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

876 

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

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

879 

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

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

882 

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

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

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

886 

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

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

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

890 
\end{alltt*} 

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

891 
\caption{Functions} \label{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 

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

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

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

920 

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

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

923 
\end{alltt*} 

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

924 
\caption{Constructing functions from smaller sets} \label{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 
14158  958 
\tdx{Int_absorb}: A \isasyminter A = A 
959 
\tdx{Int_commute}: A \isasyminter B = B \isasyminter A 

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

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

14154  962 

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

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

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

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

968 
\tdx{Diff_cancel}: AA = 0 

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

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

14154  974 

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

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

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

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

14154  980 

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

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

983 

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

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

986 

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

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

989 

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

992 

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

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

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

996 
\caption{Equalities} \label{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) == 

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

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

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

1116 

1117 

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

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

1121 

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

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

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

1125 

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

1127 

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

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

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

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

1131 

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

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

1135 

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

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

1139 

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

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

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

1143 

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

1145 

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

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

1148 

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

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

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

1152 
\end{alltt*} 

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

1153 
\caption{Least and greatest fixedpoints} \label{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); 
14158  1194 
!!x y. [ x\isasymin{}A; y\isasymin{}Fin(A); x\isasymnotin{}y; P(y) ] ==> P(cons(x,y)) 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

1196 

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

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

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

1201 
\end{alltt*} 

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

1202 
\caption{The finite set operator} \label{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 
14158  1219 
\tdx{NilI}: Nil \isasymin list(A) 
1220 
\tdx{ConsI}: [ a \isasymin A; l \isasymin list(A) ] ==> Cons(a,l) \isasymin list(A) 

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

1221 

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

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

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

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

1227 

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

1230 

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

1232 

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

1235 
\tdx{map_app_distrib}: xs\isasymin{}list(A) ==> map(h, xs@ys) = map(h,xs)@map(h,ys) 

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

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

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

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

1241 
\caption{Lists} \label{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) 

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

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

1271 

1272 

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

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

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

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

1276 

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

1279 

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

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

1282 

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

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

1285 

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

1287 
\tdx{comp_func_apply}: [ g\isasymin{}A>B; f\isasymin{}B>C; a\isasymin{}A ] ==> (f O g)`a = f`(g`a) 

1288 

1289 
\tdx{comp_inj}: [ g\isasymin{}inj(A,B); f\isasymin{}inj(B,C) ] ==> (f O g)\isasymin{}inj(A,C) 

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

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

1292 

1293 
\tdx{left_comp_inverse}: f\isasymin{}inj(A,B) ==> converse(f) O f = id(A) 

1294 
\tdx{right_comp_inverse}: f\isasymin{}surj(A,B) ==> f O converse(f) = id(B) 

14154  1295 

1296 
\tdx{bij_disjoint_Un}: 

14158  1297 
[ f\isasymin{}bij(A,B); g\isasymin{}bij(C,D); A \isasyminter C = 0; B \isasyminter D = 0 ] ==> 
1298 
(f \isasymunion g)\isasymin{}bij(A \isasymunion C, B \isasymunion D) 

1299 

1300 
\tdx{restrict_bij}: [ f\isasymin{}inj(A,B); C\isasymsubseteq{}A ] ==> restrict(f,C)\isasymin{}bij(C, f``C) 

14154  1301 
\end{alltt*} 
9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1302 
\caption{Permutations} \label{zfperm} 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

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

1304 

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

1305 
The theory \thydx{Perm} is concerned with permutations (bijections) and 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1306 
related concepts. These include composition of relations, the identity 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1307 
relation, and three specialized function spaces: injective, surjective and 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1308 
bijective. Figure~\ref{zfperm} displays many of their properties that 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1309 
have been proved. These results are fundamental to a treatment of 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

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

1311 

14154  1312 
Theory \thydx{Univ} defines a `universe' $\isa{univ}(A)$, which is used by 
9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1313 
the datatype package. This set contains $A$ and the 
14154  1314 
natural numbers. Vitally, it is closed under finite products: 
1315 
$\isa{univ}(A)\times\isa{univ}(A)\subseteq\isa{univ}(A)$. This theory also 

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

1316 
defines the cumulative hierarchy of axiomatic set theory, which 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1317 
traditionally is written $V@\alpha$ for an ordinal~$\alpha$. The 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1318 
`universe' is a simple generalization of~$V@\omega$. 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1319 

14154  1320 
Theory \thydx{QUniv} defines a `universe' $\isa{quniv}(A)$, which is used by 
9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1321 
the datatype package to construct codatatypes such as streams. It is 
14154  1322 
analogous to $\isa{univ}(A)$ (and is defined in terms of it) but is closed 
9584
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1323 
under the nonstandard product and sum. 
af21f4364c05
documented the integers and updated section on nat arithmetic
paulson
parents:
8249
diff
changeset

1324 

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

1325 

6173  1326 
\section{Automatic Tools} 
1327 

9695  1328 
ZF provides the simplifier and the classical reasoner. Moreover it supplies a 
1329 
specialized tool to infer `types' of terms. 

6173  1330 

14154  1331 
\subsection{Simplification and Classical Reasoning} 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1332 

9695  1333 
ZF inherits simplification from FOL but adopts it for set theory. The 
1334 
extraction of rewrite rules takes the ZF primitives into account. It can 

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

1335 
strip bounded universal quantifiers from a formula; for example, ${\forall 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1336 
x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1337 
f(x)=g(x)$. Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1338 
A$ and~$P(a)$. It can also break down $a\in A\int B$ and $a\in AB$. 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1339 

14154  1340 
The default simpset used by \isa{simp} contains congruence rules for all of ZF's 
1341 
binding operators. It contains all the conversion rules, such as 

1342 
\isa{fst} and 

1343 
\isa{snd}, as well as the rewrites shown in Fig.\ts\ref{zfsimpdata}. 

1344 

1345 
Classical reasoner methods such as \isa{blast} and \isa{auto} refer to 

1346 
a rich collection of builtin axioms for all the settheoretic 

1347 
primitives. 

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

1348 

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

1349 

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

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

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

1352 
a\in \emptyset & \bimp & \bot\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1353 
a \in A \un B & \bimp & a\in A \disj a\in B\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1354 
a \in A \int B & \bimp & a\in A \conj a\in B\\ 
14154  1355 
a \in AB & \bimp & a\in A \conj \lnot (a\in B)\\ 
1356 
\pair{a,b}\in \isa{Sigma}(A,B) 

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

1357 
& \bimp & a\in A \conj b\in B(a)\\ 
14154  1358 
a \in \isa{Collect}(A,P) & \bimp & a\in A \conj P(a)\\ 
6121
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1359 
(\forall x \in \emptyset. P(x)) & \bimp & \top\\ 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

1360 
(\forall x \in A. \top) & \bimp & \top 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

1362 
\caption{Some rewrite rules for set theory} \label{zfsimpdata} 
5fe77b9b5185
the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff
changeset

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

1364 

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

1365 

6173  1366 
\subsection{TypeChecking Tactics} 
1367 
\index{typechecking tactics} 

1368 

9695  1369 
Isabelle/ZF provides simple tactics to help automate those proofs that are 
6173  1370 
essentially typechecking. Such proofs are built by applying rules such as 
1371 
these: 

14154  1372 
\begin{ttbox}\isastyleminor 
14158  1373 
[ ?P ==> ?a \isasymin ?A; ~?P ==> ?b \isasymin ?A ] 