pred_set/Manual/description.tex

3 The \ml{pred\_sets} library contains a theory of predicates regarded as sets.
4 A predicate {\small\verb!s:'a->bool!} is considered as a collection or `set' of
5 elements of type \ml{'a}, and the standard operations on sets such as union,
9 1992.  The aim of this revision was to make the \ml{pred\_sets} library closely
11 names for constants and theorems and the same form of definitions for
16 `\ml{pred\_set}'. This document explains the logical basis of this theory and
19 operations on finite sets described by enumeration of their elements.  The
23 \section{Membership and the axioms of set theory}
25 A value \ml{x} is defined to be an element of a set exactly when the
26 characteristic predicate of the set is true of \ml{x}. Since sets in the
31 \index{definition!of IN@of {\ptt IN}}
38 basic language for the entire theory of sets in the \ml{pred\_sets} library;
39 all operators and predicates on sets are ultimately defined in terms of this
42 The definition of \ml{IN} shown above loosely corresponds to what is usually
43 called the {\it axiom of specification\/}\index{axiom of specification} for
46 is an element of the constructed set exactly when the predicate is true of that
51 The definition of \ml{IN} is one of two fundamental theorems in the
52 \ml{pred\_sets} library, from which all others are derived.  The second of
53 these fundamental theorems states what is usually called the {\it axiom of
54 extension\/}\index{axiom of extension} for sets.  This is not, of course,
55 literally an {\it axiom\/} of the \ml{pred\_sets} theory, but rather a theorem
65 the same elements.  This follows directly from the definition of the constant
70 The library theory \ml{pred\_sets} is developed entirely on the basis of these
71 two `axioms' of set theory.
76 predicate as the set of all values that satisfy it, the \ml{pred\_sets} library
77 also provides a general way of constructing sets by describing or specifying
81 {\small\verb!{E[x] | P[x]}!}, the set of all values {\small\verb!E[x]!} for
84 The \ml{pred\_sets} library supports generalized set specifications by means of
95 and constructs the set (i.e. predicate of type {\small\verb!'a->bool!}) of all
96 values \ml{FST(f x)} for which \ml{SND(f x)} holds, for some value \ml{x} of
97 type \ml{'b}. The formal definition of the constant \ml{GSPEC} is given by the
101 \index{definition!of GSPEC@of {\ptt GSPEC}}
108 \noindent This theorem is analogous to the axiom of specification\index{axiom
109 of specification!for generalized set specifications} for \ml{IN}.
110 This states that a value \ml{v} is an element of the set specified by
111 \ml{f} exactly when \ml{v} is one of the values of \ml{FST(f x)} for which
114 To see how this supports the notion of generalized set specification described
131 To facilitate the use of sets constructed by generalized set specification, the
139 The call made to this function extends the \HOL\ parser so that a quotation of
150 is the intersection of the set of free variables of $E$ and the set of free
151 variables of $P$).  If there are {\it no\/} variables free in both $E$ and $P$,
156 A simple example of this set abstraction notation is shown in the following
158 already been loaded. (See section~\ref{using} for a description of how
175 \noindent The term {\small\verb!{n | n > N}!} in the definition of \ml{gtr}
176 denotes the set of all natural numbers greater than \ml{N}.  It is important to
178 on only one side of the bar `{\small\verb!|!}'.  The set abstraction
188 interpretation `the set of all \ml{n} greater than \ml{N}'.  By contrast, the
196 \noindent denotes the set of all numbers \ml{n} greater than some number
198 the default interpretation of the parser, which constructs a generalized set
215 \noindent That is, a term of the form:
242 \noindent Here, a set abstraction is used to construct the set of all pairs of
252 notation in the form of a conversion called \ml{SET\_SPEC\_CONV}.  This
253 conversion implements the axiom of specification for set abstractions.%
254 \index{axiom of specification!for set abstractions}
269 \noindent This states that $t$ is an element of the set of all $v$ such that
271 be a variable. The following session illustrates this use of
284 of the form {\small\verb!"!$t$\verb! IN {!$E$\verb! | !$P$\verb!}"!} where
285 {\small $E$} is not a variable.  Applying the conversion to a term of this kind
299 The following session illustrates the form of the theorem proved by
300 \ml{SET\_SPEC\_CONV} for the second type of input term discussed above:
315 \noindent The right-hand sides of \ml{th1} and \ml{th2} could, in principle, be
316 further simplified.  The value of the expression `\ml{(n,m)}' is an injective
317 function of the values of \ml{n} and \ml{m}, and so by eliminating the
327 \noindent But in general the value of {\small $E$} in a set abstraction
328 {\small\verb!"{!$E$\verb! | !$P$\verb!}"!} will not be an injective function of
330 conversion \ml{SET\_SPEC\_CONV} therefore attempts no further simplification of
339 {\small\verb!UNIV:'a->bool!}, which denotes the universe, or set of all values
340 of type \ml{'a}.{\samepage  These constants are defined formally as follows:
343 \index{definition!of EMPTY@of {\ptt EMPTY}}
345 \index{definition!of UNIV@of {\ptt UNIV}}
360 Note that because of the restriction on free variables discussed above, the set
362 used in these definitions; the more primitive form of set construction given by
363 the above lambda-abstractions must be used instead.  But users of the library
376 \noindent That is, nothing is an element of \ml{EMPTY} and everything is an
377 element of \ml{UNIV}. These properties follow directly from the definitions and
384 The infix functions \ml{SUBSET} and \ml{PSUBSET} denote the binary relations of
389 \index{definition!of SUBSET@of {\ptt SUBSET}}
391 \index{definition!of PSUBSET@of {\ptt PSUBSET}}
398 \noindent That is, \ml{s} is a subset of \ml{t} if every element of \ml{s} is
399 also an element of \ml{t}; and \ml{s} is a proper subset of \ml{t} if it is a
400 subset of \ml{t} but not equal to \ml{t}.
434 illustrate, the names of theorems in the \ml{pred\_sets} library are generally
435 constructed from the names of the constants they contain.  Furthermore, the
436 ordering of elements in the name of a theorem attempts to reflect the content
437 of the theorem itself.\index{naming conventions!for theorems generally|)}
441 The binary operations of union, intersection and set difference are all defined
446 \index{definition!of UNION@of {\ptt UNION}}
448 \index{definition!of INTER@of {\ptt INTER}}
450 \index{definition!of DIFF@of {\ptt DIFF}}
458 \noindent These definitions illustrate the practical utility of the scheme for
468 theorems stating membership conditions of the kind illustrated by these
469 examples are given names of the form {\small\verb!IN_!$\langle\hbox{\it
470 constant\/}\rangle$} ending in the name of the operation used to construct the
484 indicated above, may in practice be used as the defining properties of union,
486 directly to the definitions of these operations.  Other built-in theorems about
493 definition of which is:
496 \index{definition!of DISJOINT@of {\ptt DISJOINT}}
507 \section{Insertion and deletion of an element}
509 To aid in the construction of particular sets of values (especially finite
510 sets) the library contains definitions of two constants \ml{INSERT} and
511 \ml{DELETE}.  These denote the operations of augmenting a set with a given
512 value and removing a value from a set, respectively.  The formal definitions of
516 \index{definition!of INSERT@of {\ptt INSERT}}
518 \index{definition!of DELETE@of {\ptt DELETE}}
525 \noindent The elements of the set denoted by {\small\verb!x INSERT s!} are all
526 the elements of the set \ml{s} together with the value \ml{x}, which may or may
527 not be an element of \ml{s} itself.  The set denoted by
528 {\small\verb!s DELETE x!} contains all the elements of \ml{s}
542 \noindent In addition, the library} contains a substantial collection of
545 gives a complete list of these theorems.
550 for finite sets that are constructed by enumeration of their elements. This
554 (see~\cite{description} for details of this function).  This has the effect of
555 extending the \HOL\ parser so that a quotation of the form
570 Users should note that care must be taken with regard to the precedence of
590 \noindent Different grouping by means of enclosing parentheses has given sets
591 with four elements (each a number), two elements (each of which is a pair), and
592 one element (a pair of pairs) respectively.
596 The \ml{pred\_sets} library provides a collection of optimized conversions for
597 computing the results of operations and predicates on finite sets specified by
598 enumeration of their elements.  All these conversions, the current
599 implementations of which are somewhat experimental, are designed to work only
600 for finite sets of the form {\small\verb!"{!\tt$t_1$,\dots,$t_n$\verb!}"!}.
601 The sections that follow describe most of these conversions; the remainder are
602 discussed in later sections of this manual.
609 \ml{IN\_CONV}.  In general, a way of deciding equality of elements is needed in
610 order to determine whether a given value is an element of a particular finite
619 decision procedure for equality of set elements.  It is assumed that this
620 conversion will map equations {\small\tt"$e_1$ = $e_2$"} between elements of a
624 If \ml{conv} is an equality conversion of the kind described above, then the
626 in finite sets of values of the base type \ml{ty}.  In particular, a call:
666 equality of the natural numbers involved in the membership
681 and \ml{num\_EQ\_CONV} therefore cannot determine if it is equal to any of the
684 membership happens to be syntactically identical to an element of the given
709 \noindent that can be used to compute the union of two finite sets.  The first
711 an equality conversion of the same kind required as an argument by
714 the result of taking the union of two finite sets.
717 conversion that computes the union of a finite set
734 insertion of values into the set {\small$s$}.\pagebreak[3] When {\small$s$} is
735 a finite set of the form {\small\verb!"{!\tt$u_1$,\dots,$u_m$\verb!}"!}, the
743 \noindent When computing} theorems of this form (i.e.\ when the second set of
747 if \ml{conv} is able to prove that some element {\small$t_i$} of
749 {\small$u_j$} of {\small\verb!"{!\tt$u_1$,\dots,$u_m$\verb!}"!}, that is if the
760 sequence of elements in the resulting finite set.  The function
763 Some examples of \ml{UNION\_CONV} in use are shown in the following \HOL\
776 and only the elements of the first set {\small\verb!{1,2,3}!} that are
777 redundant by virtue of being alpha-equivalent to elements of the second set
816 the terms {\small$t$} and  {\small$t_i$} are alpha-equivalent, of if
832 Here is an example of \ml{INSERT\_CONV} in use:
842 eliminating as many redundant occurrences of elements as possible.  An easy to
843 program, but slow-running, way of doing this is to use \ml{DEPTH\_CONV}:
860 conversion \ml{DELETE\_CONV} reduces terms of the form
865 a conversion for deciding equality of set elements as an argument.
880  {\small\verb!{!\tt$t_i$,\dots,$t_j$\verb!}!} is the set of all
888 prove either equality or inequality for every element of the original set that
906 \ml{pred\_sets} library, the property of being a singleton set is expressed by
910 \index{definition!of SING@of {\ptt SING}}
917 These are sometimes expressed in terms of the predicate \ml{SING}, as for
926 \noindent But properties of singleton sets are more usually formulated as
927 theorems about sets of the form `{\small\verb"{x}"}'. For example, the built-in
940 the element `\ml{SING}', regardless of whether or not they actually contain the
945 The \ml{pred\_sets} library contains the definition of a functions \ml{CHOICE}
951 \index{definition!of CHOICE@of {\ptt CHOICE}}
960 definition about the result of applying \ml{CHOICE} to an empty set.
962 The library also contains a function \ml{REST}, which is defined in terms of
966 \index{definition!of REST@of {\ptt REST}}
973 elements of \ml{s} except the value selected from \ml{s} by \ml{CHOICE}.
976 and \ml{REST}; for a full list of these theorems, see chapter~\ref{theorems}.
978 \section{Image of a function on a set}
980 The {\it image\/} of a function {\small\verb!f:'a->'b!} on a set
981 {\small\verb!s:'a->bool!} is the set of values {\small\verb!f(x)!} for all
982 \ml{x} in \ml{s}.  In the \ml{pred\_sets} library, the image of a function on a
983 set is defined in terms of the obvious set abstraction:
986 \index{definition!of IMAGE@of {\ptt IMAGE}}
1004 theorems about the image of a function on sets constructed by the operations of
1005 union and intersection.  For a full list of theorems about \ml{IMAGE}, see
1013 a conversion for computing the image of a function {\small\verb!f!} on a finite
1022 expected to compute the result of applying the function {\small\verb!f!} to
1025 removing redundant occurrences of its elements.
1027 The following session shows a simple example of the use of \ml{IMAGE\_CONV} on
1028 terms of the form
1031 result of applying the function {\small\verb!(\x.x+2)!} to a term {\small$t$}.
1044 conversion for computing the image of {\small\verb!(\x.x+2)!} on a finite set
1045 of numerical values.
1057 the conversion \ml{NO\_CONV}. This means that no reduction of the resulting
1058 image set is done, beyond the elimination of elements that are provably
1059 redundant by virtue of being alpha-equivalent to some other element (as in the
1062 The following session illustrates the use of the second parameter to
1075 application of {\small\verb!(\x. SUC x)!} to each element has resulted in an
1078 and therefore to simplify the resulting set by eliminating one of them from it.
1088 {\small\verb!t:'b->bool!} if it takes distinct elements of the set \ml{s} to
1089 distinct element of the set \ml{t}:
1092 \index{definition!of INJ@of {\ptt INJ}}
1103 mapping from \ml{s} to \ml{t} if for every element \ml{x} of \ml{t} there is
1104 some element \ml{y} of \ml{s} for which {\small\verb!f y = x!}:
1107 \index{definition!of SURJ@of {\ptt SURJ}}
1121 \index{definition!of BIJ@of {\ptt BIJ}}
1129 list of these theorems.
1136 \index{definition!of LINV@of {\ptt LINV}}
1138 \index{definition!of RINV@of {\ptt RINV}}
1146 two functions. Furthermore, the definitions of \ml{LINV} and \ml{RINV} shown
1152 The \ml{pred\_sets} library includes the definition of a predicate called
1153 \ml{FINITE}, which is true of finite sets and false of infinite ones.  The
1154 definition of this constant is shown below.
1157 \index{definition!of FINITE@of {\ptt FINITE}}
1167 class of sets that contains the empty set and is closed under the \ml{INSERT}
1168 operation.  This inductive definition makes \ml{FINITE} true of just those sets
1169 that can be constructed from the empty set by a finite sequence of applications
1170 of the \ml{INSERT} operation.
1173 the definition of \ml{FINITE} given above.  Among these are the two fundamental
1188 The above definition of \ml{FINITE} formalizes the notion of a finite set in
1189 logic, and it therefore also determines the form of definition for the
1190 complementary notion of an infinite set. In the \ml{pred\_sets} library, the
1194 \index{definition!of INFINITE@of {\ptt INFINITE}}
1200 \noindent There are a few consequences of this definition stored in the
1202 image of an injective function on an infinite set is infinite:
1220 \index{conversions!FINITE\_CONV@{\ptt FINITE\_CONV}|(} first of these is a
1221 conversion \ml{FINITE\_CONV} which automatically proves that sets of the form
1238 \ml{SET\_INDUCT\_TAC}.  When applied to a goal of the form
1240 reduces it to proving that the property of sets expressed by
1241 {\small\verb!\!$s$\verb!.!$P$} holds of the empty set and is preserved by the
1242 insertion of an element into an arbitrary finite set.  Since every finite set
1243 can be built up from the empty set by repeated insertion of values, these
1244 subgoals imply that this property holds of all finite sets.
1246 The following session illustrates the use of the tactic \ml{SET\_INDUCT\_TAC}
1247 for proving that the intersection of an arbitrary set \ml{t} with a finite set
1279 being inserted into the set \ml{s} is not already an element of
1283 \section{Cardinality of finite sets}
1285 The {\it cardinality\/} of a finite set is the number of elements it contains.
1287 defined by means of the following constant specification:
1290 \index{definition!of CARD@of {\ptt CARD}}
1300 \noindent This theorem is the sole defining property of \ml{CARD}.  Because the
1302 finite, this form of definition allows nothing significant to be deduced about
1303 the cardinality `\ml{CARD s}' of an {\it infinite\/} set \ml{s}.
1328 \noindent This second theorem states that the elements of a finite set can
1330 than the set's cardinality---i.e. the elements of a finite set \ml{s} can be
1338 function \ml{load\_library} (see the \HOL\ manual for a general description of
1346 \ml{pred\_sets} depend on the current state of the \HOL\ session. If the system
1349 theory is an ancestor of the \ml{pred\_sets} theory in the library (e.g.\ the
1378 library theory \ml{pred\_sets} into a parent of \ml{foo}.  The same effect
1394 \noindent The theory \ml{pred\_sets} is first made the current theory of the
1395 new session.  It then automatically becomes a parent of \ml{foo} when this
1416 \noindent This sequence of actions ensures that the system can find the parent
1427 and the current theory is not an ancestor of the theory \ml{pred\_sets}.  In
1429 theory \ml{pred\_sets} can neither be made into a parent of the current theory
1432 loaded into \HOL, since it requires access to some of the theorems in the
1436 current theory is not an ancestor of the theory \ml{pred\_sets}---the library
1439 theory (now accessible via the search path) becomes an ancestor of the current
1440 theory, this function can then be used to complete loading of the library.
1442 functions of the \ml{pred\_sets} library into \HOL\ and activates autoloading
1445 if the theory \ml{pred\_sets} is not an ancestor of the current \HOL\ theory.
1449 of loading the library can neither be made into a new parent (i.e.\ the system