The HOL finite sets Library

T. F. Melham

DRAFT

University of Cambridge, Computer Laboratory

New Museums Site, Pembroke Street Cambridge, CB2 3QG, England.

February 1992 \begin{matrix}c \\ ◯ \end{matrix} T. F. Melham 1992

Contents

1 The finite sets Library 1 1.1 The type definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Abstract characterization of the type (*)set . . . . . . . . . . . . . . . . . 2 1.3 The set induction tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

1.3.1 Parser and pretty-printer support . . . . . . . . . . . . . . . . . . . 4 1.4 Set inclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.5 Union, intersection, and set difference . . . . . . . . . . . . . . . . . . . . . 6 1.6 Disjoint sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.7 Insertion and deletion of an element . . . . . . . . . . . . . . . . . . . . . . 7

1.7.1 Conversions for enumerated finite sets . . . . . . . . . . . . . . . . 7 1.8 Singleton sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.9 The CHOICE and REST functions . . . . . . . . . . . . . . . . . . . . . . . . 12 1.10 Image of a function on a set . . . . . . . . . . . . . . . . . . . . . . . . . . 12

1.10.1 Theorem-proving support . . . . . . . . . . . . . . . . . . . . . . . 13 1.11 Mappings between sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 1.12 Finite and infinite sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

1.12.1 Theorem-proving support . . . . . . . . . . . . . . . . . . . . . . . 15 1.13 Cardinality of finite sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 1.14 Using the library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

1.14.1 Example session . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.14.2 The load finite sets function . . . . . . . . . . . . . . . . . . . . 18

2 ML Functions in the Library 19

3 Pre-proved Theorems 29 3.1 The type definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.2 Basic properties of EMPTY, INSERT, and IN . . . . . . . . . . . . . . . . . . 29 3.3 Set inclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.4 Intersection and union . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.5 Set difference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.6 Deletion of an element . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.7 Disjoint sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.8 The CHOICE and REST functions . . . . . . . . . . . . . . . . . . . . . . . . 35 3.9 Image of a function on a set . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.10 Mappings between sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.11 Singleton sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 3.12 Cardinality of sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

References 41

Index 42

Chapter 1

The finite sets Library

The finite_sets library contains a theory of sets based on a defined logical type (*)set, values of which are finite collections or ‘sets’ of elements of type *. The library was originally written in May 1989 by P. J. Windley and Philippe Leveilley. It was completely rewritten by the present author for HOL version 2.01 in early 1992. The aim of this revision was to make the finite_sets library closely parallel to the HOL sets and pred_sets libraries, with the same names for constants and theorems and, as far as possible, the same form of definitions for operations on sets. This consistency across the three set theory libraries allows proofs done in one library to be easily adapted to the others. It is also helpful to users who, for example, have to switch between set theory libraries for different projects.

There is only one theory in the finite_sets library, namely the theory ‘finite_sets’. This contains all the definitions and theorems in the library. This document, adapted from the manual for the sets library [2], explains the logical basis of this theory. The theory itself closely follows the finite set theory presented in chapter 10 of Manna and Waldinger’s book [1]. This document also explains the theorem-proving support provided by the finite_sets library, which includes conversions evaluating various operations on finite sets described by enumeration of their elements. The library also provides parser and pretty-printer support for certain terms that denote finite sets.

1.1 The type definition

The finite_sets library is based on a polymorphic type of sets (*)set, values of which unordered finite collections of values of the base type *. The representing type for the definition of (*)set is the type of predicates *->bool; the values of type (*)set correspond to precisely those predicates that are true of a finite number of values of type *.

The set of all such predicates is defined inductively in terms of representations of the empty set and the operation of inserting an element into an already existing set. The empty set is represented by the constant false predicate \x.F. The insertion operation is represented by the function that maps a value x:* and a predicate s representing a set to the predicate \e. (e = x) \/ s e, which represents of the set obtained by adding x to the set represented by s. A predicate s:*->bool then represents a finite set iff it is in the intersection of all classes of predicates that contain the representation of empty and are closed under the representation of the insertion operation. Hence s:*->bool represents a finite set if and only if it can be obtained by applying a finite sequence of insert operations to the empty set.

This characterization of the finite sets is expressed formally in the finite_sets theory by the constant IS_SET_REP, which is defined the following constant specification:

    IS_SET_REP
    |- IS_SET_REP(\x. F) /\
       (!s. IS_SET_REP s ==> (!x. IS_SET_REP(\y. (y = x) \/ s y))) /\
       (!P.
         P(\x. F) /\ (!t. P t ==> (!x. P(\y. (y = x) \/ t y))) ==>
         (!s. IS_SET_REP s ==> P s))

The specification has three conjuncts, which constitute an inductive definition (see [3]) of the class of all finite set representations. The first conjunct states that the constant false predicate \x.F is included in the class of predicates that represent finite sets. The second states that the class of predicates that represent finite sets is closed under the element insertion operation. And the third states that IS_SET_REP is true of precisely the smallest such class of predicates.

Using this definition of the class of finite sets, the type (*)set is defined formally in the library by the type definition:

    set_TY_DEF   |- ?rep:(*)set->(*->bool). TYPE_DEFINITION IS_SET_REP rep

This definitional axiom asserts the existence of a bijection rep between the type (*)set and the class of all predicates on * that represent finite sets. The theorem set_TY_DEF is named according to the general convention that definitions in the finite_sets library are given names ending in ‘_DEF’.

1.2 Abstract characterization of the type (*)set

The finite_sets library contains an abstract characterization of finite sets derived by formal proof from the type definition for (*)set. This characterizes finite sets in terms of three constants: EMPTY, which denotes the empty set; INSERT, which is the insertion operation by which non-empty sets are constructed; and the membership relation IN. These basic constants are introduced simultaneously by the following constant specification:

    FINITE_SET_DEF
    |- (!x. ~x IN EMPTY) /\
       (!x y s. x IN (y INSERT s) = (x = y) \/ x IN s) /\
       (!x s. x INSERT (x INSERT s) = x INSERT s) /\
       (!x y s. x INSERT (y INSERT s) = y INSERT (x INSERT s)) /\
       (!P. P EMPTY /\ (!s. P s ==> (!e. P(e INSERT s))) ==> (!s. P s))

The five conjuncts of this theorem constitute a derived ‘axiomatization’ for finite sets; once this theorem has been proved, it provides a complete basis for all further reasoning about sets. In particular, users of the library should never have to appeal to the type definition for (*)set. The library theory finite_sets itself is developed entirely on the basis of these ‘axioms’ of set theory.

The first two conjuncts of FINITE_SET_DEF specify the membership relation IN for empty and non-empty sets. The next two conjuncts state that sets do not contain multiple instances of the same element and that the elements of a set are not ordered. The final conjunct is an induction theorem for finite sets. It states that if a property is true of the empty set and is preserved by the insertion operation, then it holds of all sets. It follows from this theorem that every finite set is either empty or can be built up from the empty set by a finite number of insertion operations.

For consistency with the other set libraries, the first four conjuncts of FINITE_SET_DEF are stored as separate theorems in the finite_sets library. They are given the names shown below.

    NOT_IN_EMPTY  = |- !x. ~x IN {}
    IN_INSERT     = |- !x y s. x IN (y INSERT s) = (x = y) \/ x IN s
    INSERT_INSERT = |- !x s. x INSERT (x INSERT s) = x INSERT s
    INSERT_COMM   = |- !x y s. x INSERT (y INSERT s) = y INSERT (x INSERT s)

The induction property is also saved as a separate theorem, but in a slightly stronger form than that in which it appears as part of FINITE_SET_DEF. This theorem is:

    SET_INDUCT
    |- !P. P EMPTY /\ (!s. P s ==> (!e. ~e IN s ==> P(e INSERT s))) ==> !s. P s

The ‘step’ case of this stronger induction theorem requires one to show only that the property P is preserved by the operation of inserting an element not already in a set s for which P s is assumed to hold.

The finite_sets library contains many pre-proved theorems the constants about IN, EMPTY, and INSERT. These include the fundamental set equality theorem:

    EXTENSION = |- !s t. (s = t) = (!x. x IN s = x IN t)

EXTENSION states that two sets are equal exactly when they have the same elements, which corresponds to what is usually called the axiom of extension for sets. For a complete list of the other built-in theorems about IN, EMPTY, and INSERT, see chapter 3.

1.3 The set induction tactic

The library contains an induction tactic called SET_INDUCT_TAC which made available when the library is loaded. When applied to a goal of the form "s. P ", this tactic reduces it to proving that the property of sets expressed by \s.P holds of the empty set and is preserved by the insertion of an element into an arbitrary finite set. Since every finite set can be built up from the empty set by repeated insertion of values, these subgoals imply that this property holds of all finite sets.

The following session illustrates the use of the tactic SET_INDUCT_TAC for proving the fundamental theorem EXTENSION. We first set up a goal for the ‘hard’ direction of the equivalence stated by this theorem:

1

 #g "!s t. (!x:*. x IN s = x IN t) ==> (s = t)";;
 "!s t. (!x. x IN s = x IN t) ==> (s = t)"
 () : void

Expanding with SET_INDUCT_TAC yields:

2

 #expand SET_INDUCT_TAC;;
 OK..
 2 subgoals
 "!t. (!x. x IN (e INSERT s) = x IN t) ==> (e INSERT s = t)"
     [ "!t. (!x. x IN s = x IN t) ==> (s = t)" ]
     [ "~e IN s" ]
 "!t. (!x. x IN {} = x IN t) ==> ({} = t)"
 () : void

The resulting subgoals are reasonably easy to prove, given several other basic theorems about membership, the empty set and insertion. (The HOL proof closely follows the proof in [1].) Note that SET_INDUCT_TAC is based on the stronger induction theorem discussed above, so it may be assumed in the step case that the value e being inserted into the set s is not already an element of s.

1.3.1 Parser and pretty-printer support

The finite_sets library provides special parser and pretty-printer support for finite sets described by enumeration of their elements. This notation is introduced by a call made when the library is loaded to the built-in ML function define_finite_set_syntax (see [4] for details of this function). This has the effect of extending the HOL parser so that a quotation of the form "{t_{1},t_{2},…,t_{n}}" parses to the following set built up from EMPTY by repeatedly using the function INSERT:

    INSERT t_{1} (INSERT t_{2} . . . (INSERT t_{n} EMPTY). . .)

Note that the quotation "{}" just parses to the constant EMPTY. When the print_set flag is true, the HOL pretty-printer for terms inverts this transformation.

Users should note that care must be taken with regard to the precedence of comma in a context "{… }", as the following session illustrates:

1

 #set_flag(`print_set`,false);;
 true : bool
 #"{1,2,3,4}";;
 "1 INSERT (2 INSERT (3 INSERT (4 INSERT EMPTY)))" : term
 #"{(1,2),(3,4)}";;
 "(1,2) INSERT ((3,4) INSERT EMPTY)" : term
 #"{((1,2),(3,4))}";;
 "((1,2),3,4) INSERT EMPTY" : term

Different grouping by means of enclosing parentheses has given sets with four elements (each a number), two elements (each of which is a pair), and one element (a pair of pairs) respectively.

1.4 Set inclusion

The infix functions SUBSET and PSUBSET denote the binary relations of set inclusion and proper set inclusion, respectively. These are defined formally in the obvious way:

   SUBSET_DEF   |- !s t. s SUBSET t = (!x. x IN s ==> x IN t)
   PSUBSET_DEF  |- !s t. s PSUBSET t = s SUBSET t /\ ~(s = t)

That is, s is a subset of t if every element of s is also an element of t; and s is a proper subset of t if it is a subset of t but not equal to t.

Various pre-proved theorems about the subset and proper subset relations are supplied by the sets library. For example, the fact that SUBSET is a partial order is stated by the three built-in theorems shown below.

   SUBSET_REFL     |- !s. s SUBSET s
   SUBSET_TRANS    |- !s t u. s SUBSET t /\ t SUBSET u ==> s SUBSET u
   SUBSET_ANTISYM  |- !s t. s SUBSET t /\ t SUBSET s ==> (s = t)

Also provided are built-in theorems about the relationship between set inclusion and other constants or operations on sets. For example, there are the following facts about set inclusion and the empty and universal sets:

   EMPTY_SUBSET       |- !s. {} SUBSET s
   SUBSET_UNIV        |- !s. s SUBSET UNIV
   NOT_PSUBSET_EMPTY  |- !s. ~s PSUBSET {}
   NOT_UNIV_PSUBSET   |- !s. ~UNIV PSUBSET s

As these examples illustrate, the names of theorems in the sets library are generally constructed from the names of the constants they contain. Furthermore, the ordering of elements in the name of a theorem attempts to reflect the content of the theorem itself.

1.5 Union, intersection, and set difference

The binary operations of union, intersection and set difference are all defined using the set abstraction notation introduced above in section ??. The formal definitions are:

   UNION_DEF    |- !s t. s UNION t = {x | x IN s \/ x IN t}
   INTER_DEF    |- !s t. s INTER t = {x | x IN s /\ x IN t}
   DIFF_DEF     |- !s t. s DIFF t = {x | x IN s /\ ~x IN t}

These definitions illustrate the practical utility of the scheme for variable binding in set abstractions discussed above in section ??. An abstraction "{E | P }" binds only the variables that occur in both E and P, and the variables s and t in the set abstractions shown above may therefore be made parameters to the sets constructed by them.

Using SET_EQ_CONV, it is trivial to derive the following membership conditions for UNION, INTER and DIFF from the definitions given above. As a general rule, theorems stating membership conditions of the kind illustrated by these examples are given names of the form IN_⟨constant⟩ ending in the name of the operation used to construct the set in question.

    IN_UNION  |- !s t x. x IN (s UNION t) = x IN s \/ x IN t
    IN_INTER  |- !s t x. x IN (s INTER t) = x IN s /\ x IN t
    IN_DIFF   |- !s t x. x IN (s DIFF t) = x IN s /\ ~x IN t

These theorems, which are saved in the library under the names indicated above, may in practice be used as the defining properties of union, intersection and set difference; users should almost never have to appeal directly to the definitions of these operations. Other built-in theorems about UNION, INTER and DIFF may be found in chapter 3.

1.6 Disjoint sets

Two sets are disjoint if they have no elements in common. This concept is formalized in the sets library by the constant DISJOINT, the definition of which is:

    DISJOINT_DEF  |- !s t. DISJOINT s t = (s INTER t = {})

At present, there are relatively few pre-proved theorems about the DISJOINT relation in the library. But see chapter 3 for the few theorems about DISJOINT that are in fact available in the sets library.

1.7 Insertion and deletion of an element

To aid in the construction of particular sets of values (especially finite sets) the library contains definitions of two constants INSERT and DELETE. These denote the operations of augmenting a set with a given value and removing a value from a set, respectively. The formal definitions of these operations are:

    INSERT_DEF  |- !x s. x INSERT s = {y | (y = x) \/ y IN s}
    DELETE_DEF  |- !s x. s DELETE x = s DIFF (INSERT x EMPTY)

The elements of the set denoted by x INSERT s are all the elements of the set s together with the value x, which may or may not be an element of s itself. The set denoted by s DELETE x contains all the elements of s except the value x.

The membership conditions for sets constructed using INSERT and DELETE are given by the following pre-proved theorems:

    IN_INSERT  |- !x y s. x IN (y INSERT s) = (x = y) \/ x IN s
    IN_DELETE  |- !s x y. x IN (s DELETE y) = x IN s /\ ~(x = y)

In addition, the library contains a substantial collection of theorems about the relationship between the operations INSERT and DELETE and other relations and operations on sets. Chapter 3 gives a complete list of these theorems.

1.7.1 Conversions for enumerated finite sets

The sets library provides a collection of optimized conversions for computing the results of operations and predicates on finite sets specified by enumeration of their elements. All these conversions, the current implementations of which are somewhat experimental, are designed to work only for finite sets of the form "{t_{1},…,t_{n}}". The sections that follow describe most of these conversions; the remainder are discussed in later sections of this manual.

1.7.1.1 Membership

The most basic conversion for finite sets is a decision procedure for membership called IN_CONV. In general, a way of deciding equality of elements is needed in order to determine whether a given value is an element of a particular finite set. The function

    IN_CONV : conv -> conv

must therefore be supplied with a conversion that implements a decision procedure for equality of set elements. It is assumed that this conversion will map equations "e_{1} = e_{2}" between elements of a base type ty to the theorem |- (e_{1} = e_{2}) = T or to the theorem |- (e_{1} = e_{2}) = F, as appropriate.

If conv is an equality conversion of the kind described above, then the function returned by IN_CONV conv is a conversion that decides membership in finite sets of values of the base type ty. In particular, a call:

    IN CONV conv "t IN {t_{1},. . .,t_{n}}"

returns the theorem

    |- t IN {t_{1},. . .,t_{n}} = T

if the term t is alpha-equivalent to some term t_{i} or if the supplied conversion conv proves |- (t = t_{i}) = T for some i where 1 ≤ i ≤ n. If, on the other hand conv proves the theorem |- (t = t_{i}) = F for all i where 1 ≤ i ≤ n, then the result is the theorem

    |- t IN {t_{1},. . .,t_{n}} = F

In all other cases, the call to IN_CONV shown above will fail.

The following session shows how IN_CONV can be used in practice.

1

 #IN_CONV num_EQ_CONV "1 IN {2,1,3}";;
 |- 1 IN {2,1,3} = T
 #IN_CONV num_EQ_CONV "4 IN {2,1,3}";;
 |- 4 IN {2,1,3} = F

The built-in conversion num_EQ_CONV is used here to decide equality of the natural numbers involved in the membership assertions being proved.

An example in which IN_CONV fails is the following:

2

 #IN_CONV num_EQ_CONV "x IN {1,2,3}";;
 evaluation failed     IN_CONV
 #num_EQ_CONV "x = 1";;
 evaluation failed     num_EQ_CONV

Failure occurs in this case because the term x is a variable, and num_EQ_CONV therefore cannot determine if it is equal to any of the set elements 1, 2 or 3. Note, however, that the supplied conversion is not required to prove anything if the value being tested for membership happens to be syntactically identical to an element of the given set:

3

 #IN_CONV NO_CONV "x IN {1,x,3}";;
 |- x IN {1,x,3} = T

In this case, the supplied conversion, namely NO_CONV, always fails; but the call to IN_CONV nonetheless succeeds and returns the appropriate result.

1.7.1.2 Union

The sets library contains a conversion

    UNION_CONV : conv -> conv

that can be used to compute the union of two finite sets. The first argument to UNION_CONV (i.e. the conversion argument) is expected to be an equality conversion of the same kind required as an argument by IN_CONV (see section 1.7.1.1). As will be seen below, this conversion is used by UNION_CONV to simplify the set that it computes as the result of taking the union of two finite sets.

Given an equality conversion conv, the function UNION_CONV returns a conversion that computes the union of a finite set "{t_{1},…,t_{n}}" and another set s. The second set s in fact need not be finite. Ignoring, for the moment, the possible simplification done using the supplied conversion conv, a call:

    UNION CONV conv "{t_{1},. . .,t_{n}} UNION s"

just returns the theorem

    |- {t_{1},. . .,t_{n}} UNION s = t_{1} INSERT (. . . (t_{n} INSERT s). . .)

That is, UNION_CONV computes the required union as a repeated insertion of values into the set s. When s is a finite set of the form "{u_{1},…,u_{m}}", the resulting theorem will have the form shown below.

|- {t_{1},…,t_{n}} UNION {u_{1},…,u_{m}} = {t_{1},…,t_{n},u_{1},…,u_{m}}

When computing theorems of this form (i.e. when the second set of the union is a finite set "{u_{1},…,u_{m}}") the function UNION_CONV attempts to remove redundant elements in the resulting set using the supplied equality conversion conv. In particular, if conv is able to prove that some element t_{i} of "{t_{1},…,t_{n}}" is equal to any element u_{j} of "{u_{1},…,u_{m}}", that is if the conversion conv maps the term "t_{i} = u_{j}" to the theorem |- (t_{i} = u_{j}) = T, then the resulting theorem will be

|- {t_{1},… t_{i},…,t_{n}} UNION {u_{1},…,u_{j},…,u_{m}} = {t_{1},…,t_{n},u_{1},…,u_{j},…,u_{m}}

That is, the redundant term t_{i} will be removed from the initial sequence of elements in the resulting finite set. The function UNION_CONV also checks for and eliminates alphaequivalent elements.

Some examples of UNION_CONV in use are shown in the following HOL session:

4

 #UNION_CONV NO_CONV "{1,2,3} UNION {4,5,6}";;
 |- {1,2,3} UNION {4,5,6} = {1,2,3,4,5,6}
 #UNION_CONV NO_CONV "{1,2,3} UNION {3,2,SUC 0}";;
 |- {1,2,3} UNION {3,2,SUC 0} = {1,3,2,SUC 0}

The supplied equality conversion in these examples is NO_CONV, and only the elements of the first set {1,2,3} that are redundant by virtue of being alpha-equivalent to elements of the second set are eliminated from the resulting set. An example in which the equality conversion is actually used is:

5

 #UNION_CONV num_EQ_CONV "{1,2,3} UNION {3,2,SUC 0}";;
 |- {1,2,3} UNION {3,2,SUC 0} = {3,2,SUC 0}

In this case, num_EQ_CONV is used to prove that 1 is equal to SUC 0, so that the resulting

union is the set "{3,2,SUC 0}", rather than "{1,3,2,SUC 0}”.

1.7.1.3 Insertion

The conversion INSERT_CONV performs the following reduction on finite sets:

reduce "t INSERT {t_{1},…,t_{i},…,t_{n}}" to "{t_{1},…,t_{i},…,t_{n}}"

if a supplied equality conversion can prove |- (t = t_{i}) = T. Since the enumerated set notation "{t_{1},…,t_{n}}" is just a parser-supported abbreviation (see section 1.3.1), this is equivalent to reducing the set "{t,t_{1},…,t_{i},…,t_{n}}" to "{t_{1},…,t_{i},…,t_{n}}" when the terms t and t_{i} are provably equal.

More specifically, if for some t_{i} in {t_{1},…,t_{n}}, the terms t and t_{i} are alpha-equivalent, of if the conversion conv maps "t = t_{i}" to the theorem |- (t = t_{i}) = T, then the call:

    INSERT CONV conv "t INSERT {t_{1},. . .,t_{n}}";;

will return the theorem:

    |- t INSERT {t_{1},. . .,t_{n}} = {t_{1},. . .,t_{n}}

Here is an example of INSERT_CONV in use:

1

 #INSERT_CONV num_EQ_CONV "(SUC 2) INSERT {0,1,2,3}";;
 |- {SUC 2,0,1,2,3} = {0,1,2,3}

When applied repeatedly, INSERT_CONV can be used to reduce finite sets by eliminating as many redundant occurrences of elements as possible. An easy to program, but slowrunning, way of doing this is to use DEPTH_CONV:

2

 #DEPTH_CONV (INSERT_CONV num_EQ_CONV) "{1,3,x,SUC 1,SUC(SUC 1),2,1,3,x}";;
 |- {1,3,x,SUC 1,SUC(SUC 1),2,1,3,x} = {2,1,3,x}

For a faster alternative to this method, see the reference entry for INSERT_CONV in chapter 2.

1.7.1.4 Deletion

The conversion DELETE_CONV reduces terms of the form "{t_{1},…,t_{n}} DELETE t" by deleting all elements provably equal to t from the set {t_{1},…,t_{n}}. Like IN_CONV and INSERT_CONV, the function DELETE_CONV takes a conversion for deciding equality of set elements as an argument. If conv is such a conversion, the call:

    DELETE CONV conv "{t_{1},. . .,t_{n}} DELETE t";;

will return the theorem:

    |- {t_{1},. . .,t_{n}} DELETE t = {t_{i},. . .,t_{j}}

where the resulting set {t_{i},…,t_{j}} is the set of all values t_{k} in the original set {t_{1},…,t_{n}} for which conv proves |- (t_{k} = t) = F, and where for all t_{k} in {t_{1},…,t_{n}} but not in {t_{i},…,t_{j}}, either t_{k} is alpha-equivalent to t or conv proves |- (t_{k} = t) = T. Note that the conversion conv must prove either equality or inequality for every element of the original set that is not simply alpha-equivalent to the deleted value.

The following session shows DELETE_CONV in use:

1

 #DELETE_CONV num_EQ_CONV "{0,1,2,3} DELETE (SUC 1)";;
 |- {0,1,2,3} DELETE (SUC 1) = {0,1,3}

1.8 Singleton sets

A singleton set is a set that contains precisely one element. In the sets library, the property of being a singleton set is expressed by the definition:

    SING_DEF   |- !s. SING s = (?x. s = {x})

The library contains several built-in theorems about singleton sets. These are sometimes expressed in terms of the predicate SING, as for example in the theorem

    SING   |- !x. SING{x}

But properties of singleton sets are more usually formulated as theorems about sets of the form ‘{x}’. For example, the built-in theorems about singleton sets include:

    NOT_SING_EMPTY  |- !x. ~({x} = {})
    IN_SING         |- !x y. x IN {y} = (x = y)
    EQUAL_SING      |- !x y. ({x} = {y}) = (x = y)

A general convention is that theorems about singleton sets are given names that contain the element ‘SING’, regardless of whether or not they actually contain the predicate SING.

1.9 The CHOICE and REST functions

The sets library contains the definition of a functions CHOICE which can be used to select an arbitrary element from a non-empty set. The function CHOICE is defined formally by the following constant specification:

    CHOICE_DEF   |- !s. ~(s = {}) ==> (CHOICE s) IN s

This theorem alone is the defining property for the constant CHOICE, which is therefore an only partially specified function from sets to values. Note, in particular, that there is no information given by this definition about the result of applying CHOICE to an empty set.

The library also contains a function REST, which is defined in terms of the CHOICE function as follows

    REST_DEF   |- !s. REST s = s DELETE (CHOICE s)

For any non-empty set s, the set REST s comprises all those elements of s except the value selected from s by CHOICE.

The library contains various built-in theorems about the functions CHOICE and REST; for a full list of these theorems, see chapter 3.

1.10 Image of a function on a set

The image of a function f:*->** on a set s:(*)set is the set of values f(x) for all x in s. In the sets library, the image of a function on a set is defined in terms of the obvious set abstraction:

    IMAGE_DEF   |- !f s. IMAGE f s = {f x | x IN s}

Using SET_SPEC_CONV, is is trivial to prove from this definition the following membership condition for sets constructed using IMAGE:

    IN_IMAGE   |- !y s f. y IN (IMAGE f s) = (?x. (y = f x) /\ x IN s)

The sets library contains various theorems about IMAGE in addition to this membership theorem. These include, for example, theorems about the image of a function on sets constructed by the operations of union and intersection. For a full list of theorems about IMAGE, see chapter 3.

1.10.1 Theorem-proving support

The sets library contains a conversion for computing the image of a function f on a finite set {t_{1},…,t_{n}}. The function

    IMAGE_CONV : conv -> conv -> conv

is parameterized by two conversions. The first conversion is expected to compute the result of applying the function f to each element t_{1}, …, t_{n}. The second parameter is an equality conversion which is used to simplify the resulting image set by removing redundant occurrences of its elements.

The following session shows a simple example of the use of IMAGE_CONV on terms of the form "IMAGE (\x.x+2) {t_{1},…,t_{n}}". We first define a conversion that evaluates the result of applying the function (\x.x+2) to a term t.

1

 #let AP_CONV = BETA_CONV THENC (TRY_CONV ADD_CONV);;
 AP_CONV = - : conv
 #AP_CONV "(\n.n+2) 7";;
 |- (\n. n + 2)7 = 9

This conversion, together with the function IMAGE_CONV, gives a conversion for computing the image of (\x.x+2) on a finite set of numerical values.

2

 #IMAGE_CONV AP_CONV NO_CONV "IMAGE (\x.x+2) {1,2,3,4}";;
 |- IMAGE(\x. x + 2){1,2,3,4} = {3,4,5,6}
 #IMAGE_CONV AP_CONV NO_CONV "IMAGE (\x.x+2) {n,1,n}";;
 |- IMAGE(\x. x + 2){n,1,n} = {3,n + 2}

In this case, the second parameter supplied to IMAGE_CONV is the conversion NO_CONV. This means that no reduction of the resulting image set is done, beyond the elimination of elements that are provably redundant by virtue of being alpha-equivalent to some other element (as in the second example above).

The following session illustrates the use of the second parameter to IMAGE_CONV.

3

 #IMAGE_CONV BETA_CONV NO_CONV "IMAGE (\x. SUC x) {1,SUC 0,2,0}";;
 |- IMAGE(\x. SUC x){1,SUC 0,2,0} = {SUC 1,SUC(SUC 0),SUC 2,SUC 0}
 #IMAGE_CONV BETA_CONV num_EQ_CONV "IMAGE (\x. SUC x) {1,SUC 0,2,0}";;
 |- IMAGE(\x. SUC x){1,SUC 0,2,0} = {SUC(SUC 0),SUC 2,SUC 0}

In the first evaluation, just applying BETA_CONV to the application of (\x. SUC x) to each element has resulted in an image set containing both SUC 1 and SUC(SUC 0). In the second example, num_EQ_CONV is used to prove these values equal, and therefore to simplify the resulting set by eliminating one of them from it. For more detail about IMAGE_CONV, see the reference entry for this conversion in chapter 2.

1.11 Mappings between sets

The sets library contains a few basic definitions and theorems having to do with mappings between sets. A function f:*->** is an injective (one-to-one) mapping from a set s:(*)set to a set t:(**)set if it takes distinct elements of s to distinct element of t:

    INJ_DEF =
    |- !f s t.
        INJ f s t =
        (!x. x IN s ==> (f x) IN t) /\
        (!x y. x IN s /\ y IN s ==> (f x = f y) ==> (x = y))

Likewise, a function f:*->** is a surjective (onto) mapping from s to t if for every element x of t there is some element y of s for which f y = x:

    SURJ_DEF =
    |- !f s t.
        SURJ f s t =
        (!x. x IN s ==> (f x) IN t) /\
        (!x. x IN t ==> (?y. y IN s /\ (f y = x)))

Finally, a function f:*->** is a bijection from s to t if it is both injective and surjective:

    BIJ_DEF = |- !f s t. BIJ f s t = INJ f s t /\ SURJ f s t

There are a few pre-proved theorems about the predicates INJ, SURJ, and BIJ available in the library; see chapter 3 for a full list of these theorems.

The library also contains constant specifications for two functions LINV and RINV, which yield left and right inverses to injective and surjective mappings respectively. These functions are defined by:

    LINV_DEF = |- !f s t. INJ f s t ==> (!x. x IN s ==> (LINV f s(f x) = x))
    RINV_DEF = |- !f s t. SURJ f s t ==> (!x. x IN t ==> (f(RINV f s x) = x))

There are, at present, no additional built-in theorems about these two functions. Furthermore, the definitions of LINV and RINV shown above should be regarded as only provisional; they may be changed in future versions.

1.12 Finite and infinite sets

The sets library includes the definition of a predicate called FINITE, which is true of finite sets and false of infinite ones. The definition of this constant is shown below.

    FINITE_DEF
      |- !s.
          FINITE s =
          (!P. P{} /\ (!s'. P s' ==> (!e. P(e INSERT s'))) ==> P s)

That is, a set s is finite precisely when it is in the smallest class of sets that contains the empty set and is closed under the INSERT operation. This inductive definition makes FINITE true of just those sets that can be constructed from the empty set by a finite sequence of applications of the INSERT operation.

The sets library contains various built-in theorems that follow from the definition of FINITE given above. Among these are the two fundamental theorems shown below:

    FINITE_EMPTY   |- FINITE{}
    FINITE_INSERT  |- !x s. FINITE(x INSERT s) = FINITE s

These state that the empty set is indeed finite and insertion constructs finite sets only from other finite sets. See chapter 3 for other built-in theorems about finite sets.

The above definition of FINITE formalizes the notion of a finite set in logic, and it therefore also determines the form of definition for the complementary notion of an infinite set. In the sets library, the predicate INFINITE is defined as follows:

    INFINITE_DEF   |- !s. INFINITE s = ~FINITE s

There are a few consequences of this definition stored in the sets library. The following theorem, for example, states that the image of an injective function on an infinite set is infinite:

    IMAGE_11_INFINITE
       |- !f. (!x y. (f x = f y) ==> (x = y)) ==>
              (!s. INFINITE s ==> INFINITE(IMAGE f s))

Other built-in theorems about INFINITE can be found in chapter 3.

1.12.1 Theorem-proving support

There are two ML functions in the sets library for reasoning about propositions that involve the finiteness predicate FINITE. The first of these is a conversion FINITE_CONV which automatically proves that sets of the form "{t_{1},…,t_{n}}" are finite. Evaluating

    FINITE CONV "FINITE {t_{1},. . .,t_{n}}";;

yields the theorem |- FINITE {t_{1},…,t_{n}} = T.

1.13 Cardinality of finite sets

The cardinality of a finite set is the number of elements it contains. In the sets library, this is formalized by a constant CARD defined by means of the following constant specification:

   CARD_DEF
     |- (CARD{} = 0) /\
        (!s.
          FINITE s ==>
          (!x. CARD(x INSERT s) = (x IN s => CARD s | SUC(CARD s))))

This theorem is the sole defining property of CARD. Because the equation in the second clause holds only under the assumption that s is finite, this form of definition allows nothing significant to be deduced about the cardinality ‘CARD s’ of an infinite set s.

The built-in theorems about cardinality are all restricted to finite sets only, either implicitly as in the theorem:

    CARD_SING  |- !x. CARD{x} = 1

or explicitly, as in:

    FINITE_ISO_NUM
      |- !s:(*)set.
          FINITE s ==>
          (?f:num->*.
            (!n m.
              n < (CARD s) /\ m < (CARD s) ==> (f n = f m) ==> (n = m)) /\
            (s = {f n | n < (CARD s)}))

This second theorem states that the elements of a finite set can always be put into a one-to-one correspondence with the natural numbers less than the set’s cardinality—i.e. the elements of a finite set s can be numbered 0, 1, …, (CARD s)-1. Other theorems involving the cardinality function CARD can be found in chapter 3.

1.14 Using the library

The finite_sets library is loaded into a user’s HOL session using the builtin ML function load_library (see the HOL manual for a general description of library loading). The first action in the load sequence is to update the internal HOL search paths. A pathname to the library is added to the search path so that theorems may be autoloaded from the library theory finite_sets; and the HOL help search path is updated with a pathname to online help files for the ML functions in the library.

After the search paths are updated, the actions taken by the load sequence for depend on the current state of the HOL session. If the system is in draft mode, the library theory finite_sets is added as a new parent to the current theory. If the system is not in draft mode, but the current theory is an ancestor of the finite_sets theory in the library (e.g. the user is in a fresh HOL session) then finite_sets is made the current theory. In both cases, the ML functions provided by the library are loaded into HOL and all the theorems in the library (including definitions) are set up to be autoloaded on demand. The parser and pretty-printer for the notation described above in sections ?? and 1.3.1 are then activated, and the ML functions provided by the library for reasoning about sets are loaded. The finite_sets library is then fully loaded into the user’s HOL session.

1.14.1 Example session

The following session shows how finite_sets may be loaded using load_library. Suppose, beginning in a fresh HOL session, the user wishes to create a theory foo whose parents include the theory finite_sets in the library. This may be done as follows:

1

 #new_theory `foo`;;
 () : void
 #load_library `finite_sets`;;

⋮

 Library finite_sets loaded.
 () : void

Loading the library while drafting the theory foo makes the library theory finite_sets into a parent of foo. The same effect could have been achieved (in a fresh session) by first loading the library and then creating foo:

1

 #load_library `finite_sets`;;

⋮

 Library finite_sets loaded.
 () : void
 #new_theory `foo`;;
 () : void

The theory finite_sets is first made the current theory of the new session. It then automatically becomes a parent of foo when this theory is created by new_theory.

Now, suppose that foo has been created as shown above, and the user does some work in this theory, quits HOL, and in a later session wishes to load the theory foo. This must be done by first loading the finite_sets library and then loading the theory foo.

1

 #load_library `finite_sets`;;

⋮

 Library finite_sets loaded.
 () : void
 #load_theory `foo`;;
 Theory foo loaded
 () : void

This sequence of actions ensures that the system can find the parent theory finite_sets when it comes to load foo, since loading the library updates the search path.

1.14.2 The load finite sets function

The finite_sets library may in many cases simply be loaded into the system as illustrated by the examples given above. There are, however, certain situations in which the library cannot be fully loaded at the time when the load_library is used. This occurs when the system is not in draft mode and the current theory is not an ancestor of the theory finite_sets. In this case, loading the library can (and will) update the search paths. But the theory finite_sets can neither be made into a parent of the current theory nor be made the current theory. This means that autoloading from the library can not at this stage be activated; and the ML code in the library can not be loaded into HOL, since it requires access to some of the theorems in the library.

In the situation described above—when the system is not in draft mode and the current theory is not an ancestor of the theory finite_sets—the library load sequence defines an ML function called load_finite_sets in the current HOL session. If at a future point in the session the finite_sets theory (now accessible via the search path) becomes an ancestor of the current theory, this function can then be used to complete loading of the library. Evaluating load_finite_sets() in such a context loads the ML functions of the finite_sets library into HOL and activates autoloading from its theory files. It also activates the parser and pretty-printer support for set abstractions and finite sets. The function load_finite_sets fails if the theory finite_sets is not an ancestor of the current HOL theory.

Note that the function load_finite_sets is defined upon loading the finite_sets library only if the library theory finite_sets at the point of loading the library can neither be made into a new parent (i.e. the system is not in draft mode) nor be made the current theory.

ML Functions in the Library

This chapter provides documentation on all the ML functions that are made available in HOL when the finite_sets library is loaded. This documentation is also available online via the help facility.

 DELETE_CONV

DELETE_CONV : conv -> conv

Synopsis

Reduce {x1,...,xn} DELETE x by deleting x from {x1,...,xn}.

Description

The function DELETE_CONV is a parameterized conversion for reducing finite sets of the form

"{t1,...,tn} DELETE t", where {t1,...,tn} is a set of type (ty)set and t is a term of

type ty. The first argument to DELETE_CONV is expected to be a conversion that decides equality between values of the base type ty. Given an equation "e1 = e2", where e1 and e2 are terms of type ty, this conversion should return the theorem |- (e1 = e2) = T or the theorem |- (e1 = e2) = F, as appropriate.

Given such a conversion conv, the function DELETE_CONV returns a conversion that maps a term of the form "{t1,...,tn} DELETE t" to the theorem

   |- {t1,...,tn} DELETE t = {ti,...,tj}

where {ti,...,tj} is the subset of {t1,...,tn} for which the supplied equality conversion conv proves

   |- (ti = t) = F, ..., |- (tj = t) = F

and for all the elements tk in {t1,...,tn} but not in {ti,...,tj}, either conv proves |- (tk = t) = T or tk is alpha-equivalent to t. That is, the reduced set {ti,...,tj} comprises all those elements of the original set that are provably not equal to the deleted element t.

Example

In the following example, the conversion num_EQ_CONV is supplied as a parameter and used to test equality of the deleted value 2 with the elements of the set.

   #DELETE_CONV num_EQ_CONV "{2,1,SUC 1,3} DELETE 2";;
   |- {2,1,SUC 1,3} DELETE 2 = {1,3}

Failure

DELETE_CONV conv fails if applied to a term not of the form "{t1,...,tn} DELETE t". A
call DELETE_CONV conv "{t1,...,tn} DELETE t" fails unless for each element ti of the

set {t1,...,tn}, the term t is either alpha-equivalent to ti or conv "ti = t" returns

|- (ti = t) = T or |- (ti = t) = F.

See also

INSERT_CONV.

 IMAGE_CONV

IMAGE_CONV : conv -> conv -> conv

Synopsis

Compute the image of a function on a finite set.

Description

The function IMAGE_CONV is a parameterized conversion for computing the image of a function f:ty1->ty2 on a finite set "{t1,...,tn}" of type (ty1)set. The first argument to IMAGE_CONV is expected to be a conversion that computes the result of applying the function f to each element of this set. When applied to a term "f ti", this conversion should return a theorem of the form |- (f ti) = ri, where ri is the result of applying the function f to the element ti. This conversion is used by IMAGE_CONV to compute a theorem of the form

   |- IMAGE f {t1,...,tn} = {r1,...,rn}

The second argument to IMAGE_CONV is used (optionally) to simplify the resulting image set {r1,...,rn} by removing redundant occurrences of values. This conversion expected to decide equality of values of the result type ty2; given an equation "e1 = e2", where e1 and e2 are terms of type ty2, the conversion should return either |- (e1 = e2) = T or |- (e1 = e2) = F, as appropriate.

Given appropriate conversions conv1 and conv2, the function IMAGE_CONV returns a conversion that maps a term of the form "IMAGE f {t1,...,tn}" to the theorem

   |- IMAGE f {t1,...,tn} = {rj,...,rk}

where conv1 proves a theorem of the form |- (f ti) = ri for each element ti of the set {t1,...,tn}, and where the set {rj,...,rk} is the smallest subset of {r1,...,rn} such no two elements are alpha-equivalent and conv2 does not map "rl = rm" to the theorem

|- (rl = rm) = T for any pair of values rl and rm in {rj,...,rk}. That is, {rj,...,rk}

is the set obtained by removing multiple occurrences of values from the set {r1,...,rn}, where the equality conversion conv2 (or alpha-equivalence) is used to determine which pairs of terms in {r1,...,rn} are equal.

Example

The following is a very simple example in which REFL is used to construct the result of applying the function f to each element of the set {1,2,1,4}, and NO_CONV is the supplied ‘equality conversion’.

   #IMAGE_CONV REFL NO_CONV "IMAGE (f:num->num) {1,2,1,4}";;
   |- IMAGE f{1,2,1,4} = {f 2,f 1,f 4}

The result contains only one occurrence of ‘f 1’, even though NO_CONV always fails, since IMAGE_CONV simplifies the resulting set by removing elements that are redundant up to alpha-equivalence.

For the next example, we construct a conversion that maps SUC n for any numeral n to the numeral standing for the successor of n.

   #let SUC_CONV tm =
        let n = int_of_string(fst(dest_const(rand tm))) in
        let sucn = mk_const(string_of_int(n+1), ":num") in
            SYM (num_CONV sucn);;
   SUC_CONV = - : conv

The result is a conversion that inverts num_CONV:

   #num_CONV "4";;
   |- 4 = SUC 3
   #SUC_CONV "SUC 3";;
   |- SUC 3 = 4

The conversion SUC_CONV can then be used to compute the image of the successor function on a finite set:

   #IMAGE_CONV SUC_CONV NO_CONV "IMAGE SUC {1,2,1,4}";;
   |- IMAGE SUC{1,2,1,4} = {3,2,5}

Note that 2 (= SUC 1) appears only once in the resulting set.

Fianlly, here is an example of using IMAGE_CONV to compute the image of a paired addition function on a set of pairs of numbers:

   #IMAGE_CONV (PAIRED_BETA_CONV THENC ADD_CONV) num_EQ_CONV
               "IMAGE (\(n,m).n+m) {(1,2), (3,4), (0,3), (1,3)}";;
   |- IMAGE(\(n,m). n + m){(1,2),(3,4),(0,3),(1,3)} = {7,3,4}

Failure

IMAGE_CONV conv1 conv2 fails if applied to a term not of the form "IMAGE f {t1,...,tn}".
An application of IMAGE_CONV conv1 conv2 to a term "IMAGE f {t1,...,tn}" fails unless

for all ti in the set {t1,...,tn}, evaluating conv1 "f ti" returns |- (f ti) = ri for some ri.

 INSERT_CONV

INSERT_CONV : conv -> conv

Synopsis

Reduce x INSERT {x1,...,x,...,xn} to {x1,...,x,...,xn}.

Description

The function INSERT_CONV is a parameterized conversion for reducing finite sets of the

form "t INSERT {t1,...,tn}", where {t1,...,tn} is a set of type (ty)set and t is equal

to some element ti of this set. The first argument to INSERT_CONV is expected to be a conversion that decides equality between values of the base type ty. Given an equation "e1 = e2", where e1 and e2 are terms of type ty, this conversion should return the theorem |- (e1 = e2) = T or the theorem |- (e1 = e2) = F, as appropriate.

Given such a conversion, the function INSERT_CONV returns a conversion that maps a term of the form "t INSERT {t1,...,tn}" to the theorem

   |- t INSERT {t1,...,tn} = {t1,...,tn}

if t is alpha-equivalent to any ti in the set {t1,...,tn}, or if the supplied conversion proves |- (t = ti) = T for any ti.

Example

In the following example, the conversion num_EQ_CONV is supplied as a parameter and used to test equality of the inserted value 2 with the remaining elements of the set.

   #INSERT_CONV num_EQ_CONV "2 INSERT {1,SUC 1,3}";;
   |- {2,1,SUC 1,3} = {1,SUC 1,3}

In this example, the supplied conversion num_EQ_CONV is able to prove that 2 is equal to SUC 1 and the set is therefore reduced. Note that "2 INSERT {1,SUC 1,3}" is just

"{2,1,SUC 1,3}".

A call to INSERT_CONV fails when the value being inserted is provably not equal to any of the remaining elements:

   #INSERT_CONV num_EQ_CONV "1 INSERT {2,3}";;
   evaluation failed     INSERT_CONV

But this failure can, if desired, be caught using TRY_CONV.

The behaviour of the supplied conversion is irrelevant when the inserted value is alphaequivalent to one of the remaining elements:

   #INSERT_CONV NO_CONV "(y:*) INSERT {x,y,z}";;
   |- {y,x,y,z} = {x,y,z}

The conversion NO_CONV always fails, but INSERT_CONV is nontheless able in this case to prove the required result.

Note that DEPTH_CONV(INSERT_CONV conv) can be used to remove duplicate elements from a finite set, but the following conversion is faster:

   #letrec REDUCE_CONV conv tm =
      (SUB_CONV (REDUCE_CONV conv) THENC (TRY_CONV (INSERT_CONV conv))) tm;;
   REDUCE_CONV = - : (conv -> conv)
   #REDUCE_CONV num_EQ_CONV "{1,2,1,3,2,4,3,5,6}";;
   |- {1,2,1,3,2,4,3,5,6} = {1,2,4,3,5,6}

Failure

INSERT_CONV conv fails if applied to a term not of the form "t INSERT {t1,...,tn}". A

call INSERT_CONV conv "t INSERT {t1,...,tn}" fails unless t is alpha-equivalent to some

ti, or conv "t = ti" returns |- (t = ti) = T for some ti.

See also

DELETE_CONV.

 IN_CONV

IN_CONV : conv -> conv

Synopsis

Decision procedure for membership in finite sets.

Description

The function IN_CONV is a parameterized conversion for proving or disproving membership assertions of the general form:

   "t IN {t1,...,tn}"

where {t1,...,tn} is a set of type (ty)set and t is a value of the base type ty. The first argument to IN_CONV is expected to be a conversion that decides equality between values of the base type ty. Given an equation "e1 = e2", where e1 and e2 are terms of type ty, this conversion should return the theorem |- (e1 = e2) = T or the theorem |- (e1 = e2) = F, as appropriate.

Given such a conversion, the function IN_CONV returns a conversion that maps a term of the form "t IN {t1,...,tn}" to the theorem

   |- t IN {t1,...,tn} = T

if t is alpha-equivalent to any ti, or if the supplied conversion proves |- (t = ti) = T for any ti. If the supplied conversion proves |- (t = ti) = F for every ti, then the result is the theorem

   |- t IN {t1,...,tn} = F

In all other cases, IN_CONV will fail.

Example

In the following example, the conversion num_EQ_CONV is supplied as a parameter and used to test equality of the candidate element 1 with the actual elements of the given set.

   #IN_CONV num_EQ_CONV "2 IN {0,SUC 1,3}";;
   |- 2 IN {0,SUC 1,3} = T

The result is T because num_EQ_CONV is able to prove that 2 is equal to SUC 1. An example of a negative result is:

   #IN_CONV num_EQ_CONV "1 IN {0,2,3}";;
   |- 1 IN {0,2,3} = F

Finally the behaviour of the supplied conversion is irrelevant when the value to be tested for membership is alpha-equivalent to an actual element:

   #IN_CONV NO_CONV "1 IN {3,2,1}";;
   |- 1 IN {3,2,1} = T

The conversion NO_CONV always fails, but IN_CONV is nontheless able in this case to prove the required result.

Failure

IN_CONV conv fails if applied to a term that is not of the form "t IN {t1,...,tn}". A call IN_CONV conv "t IN {t1,...,tn}" fails unless the term t is alpha-equivalent to some

ti, or conv "t = ti" returns |- (t = ti) = T for some ti, or conv "t = ti" returns
|- (t = ti) = F for every ti.

 SET_INDUCT_TAC

SET_INDUCT_TAC : tactic

Synopsis

Tactic for induction on finite sets.

Description

SET_INDUCT_TAC is an induction tacic for proving properties of finite sets. When applied to a goal of the form

   !s:(*)set. P[s]

SET_INDUCT_TAC reduces this goal to proving that the property \s.P[s] holds of the empty set and is preserved by insertion of an element into an arbitrary finite set. Since every finite set can be built up from the empty set "{}" by repeated insertion of values, these subgoals imply that the property \s.P[s] holds of all finite sets.

The tactic specification of SET_INDUCT_TAC is:

                         A ?- !s.P
   ==================================================  SET_INDUCT_TAC
     A |- P[{}/s]
     A u {P[s'/s], ~e IN s'} ?- P[e INSERT s'/s]

where e is a variable chosen so as not to appear free in the assumptions A, and s' is a primed variant of s that does not appear free in A (usually, s' is just s).

Failure

SET_INDUCT_TAC (A,g) fails unless g has the form !s.P, where the variable s has type (ty)set for some type ty.

 UNION_CONV

UNION_CONV : conv -> conv

Synopsis

Reduce {t1,...,tn} UNION s to t1 INSERT (... (tn INSERT s)).

Description

The function UNION_CONV is a parameterized conversion for reducing sets of the form

"{t1,...,tn} UNION s", where {t1,...,tn} and s are sets of type (ty)set. The first

argument to UNION_CONV is expected to be a conversion that decides equality between values of the base type ty. Given an equation "e1 = e2", where e1 and e2 are terms of type ty, this conversion should return the theorem |- (e1 = e2) = T or the theorem |- (e1 = e2) = F, as appropriate.

Given such a conversion, the function UNION_CONV returns a conversion that maps a term of the form "{t1,...,tn} UNION s" to the theorem

   |- t UNION {t1,...,tn} = ti INSERT ... (tj INSERT s)

where {ti,...,tj} is the set of all terms t that occur as elements of {t1,...,tn} for which the conversion IN_CONV conv fails to prove that |- (t IN s) = T (that is, either by proving |- (t IN s) = F instead, or by failing outright).

Example

In the following example, num_EQ_CONV is supplied as a parameter to UNION_CONV and used to test for membership of each element of the first finite set {1,2,3} of the union in the

UNION CONV 27

second finite set {SUC 0,3,4}.

   #UNION_CONV num_EQ_CONV "{1,2,3} UNION {SUC 0,3,4}";;
   |- {1,2,3} UNION {SUC 0,3,4} = {2,SUC 0,3,4}

The result is {2,SUC 0,3,4}, rather than {1,2,SUC 0,3,4}, because UNION_CONV is able by means of a call to

   IN_CONV num_EQ_CONV "1 IN {SUC 0,3,4}"

to prove that 1 is already an element of the set {SUC 0,3,4}.

The conversion supplied to UNION_CONV need not actually prove equality of elements, if simplification of the resulting set is not desired. For example:

   #UNION_CONV NO_CONV "{1,2,3} UNION {SUC 0,3,4}";;
   |- {1,2,3} UNION {SUC 0,3,4} = {1,2,SUC 0,3,4}

In this case, the resulting set is just left unsimplified. Moreover, the second set argument to UNION need not be a finite set:

   #UNION_CONV NO_CONV "{1,2,3} UNION s";;
   |- {1,2,3} UNION s = 1 INSERT (2 INSERT (3 INSERT s))

And, of course, in this case the conversion argument to UNION_CONV is irrelevant.

Failure

UNION_CONV conv fails if applied to a term not of the form "{t1,...,tn} UNION s".

See also

IN_CONV.

28 Chapter 2. ML Functions in the Library

Pre-proved Theorems

The sections that follow list all theorems in the finite_sets library, including definitions. The theorems are grouped into sections according to subject matter. Some theorems could be classified under more than one subject, but each theorem is listed in only one section. The reader may therefore have to consult more than one section when searching for any particular theorem.

When the finite_sets library is loaded, all the theorems listed in this chapter (including definitions) are set up to autoload when their names are mentioned in ML.

3.1 The type definition

FINITE_SET_DEF (finite sets)
|- (!x. ~x IN {}) /\
(!x y s. x IN (y INSERT s) = (x = y) \/ x IN s) /\
(!x s. x INSERT (x INSERT s) = x INSERT s) /\
(!x y s. x INSERT (y INSERT s) = y INSERT (x INSERT s)) /\
(!P. P{} /\ (!s. P s ==> (!e. P(e INSERT s))) ==> (!s. P s))
IS_SET_REP (finite sets)
|- IS_SET_REP(\x. F) /\
(!s. IS_SET_REP s ==> (!x. IS_SET_REP(\y. (y = x) \/ s y))) /\
(!P.
  P(\x. F) /\ (!t. P t ==> (!x. P(\y. (y = x) \/ t y))) ==>
  (!s. IS_SET_REP s ==> P s))
set_TY_DEF (finite sets)
|- ?rep. TYPE_DEFINITION IS_SET_REP rep

3.2 Basic properties of EMPTY, INSERT, and IN

ABSORPTION (finite sets)
|- !x s. x IN s = (x INSERT s = s)

30 Chapter 3. Pre-proved Theorems

COMPONENT (finite sets)
  |- !x s. x IN (x INSERT s)
DECOMPOSITION (finite sets)
  |- !s x. x IN s = (?t. (s = x INSERT t) /\ ~x IN t)
EXTENSION (finite sets)
  |- !s t. (s = t) = (!x. x IN s = x IN t)
INSERT_COMM (finite sets)
  |- !x y s. x INSERT (y INSERT s) = y INSERT (x INSERT s)
INSERT_INSERT (finite sets)
  |- !x s. x INSERT (x INSERT s) = x INSERT s
IN_INSERT (finite sets)
  |- !x y s. x IN (y INSERT s) = (x = y) \/ x IN s
MEMBER_NOT_EMPTY (finite sets)
  |- !s. (?x. x IN s) = ~(s = {})
NOT_EMPTY_INSERT (finite sets)
  |- !x s. ~({} = x INSERT s)
NOT_EQUAL_SETS (finite sets)
  |- !s t. ~(s = t) = (?x. x IN t = ~x IN s)
NOT_INSERT_EMPTY (finite sets)
  |- !x s. ~(x INSERT s = {})
NOT_IN_EMPTY (finite sets)
  |- !x. ~x IN {}
NUM_SET_WOP (finite sets)
  |- !s. (?n. n IN s) = (?n. n IN s /\ (!m. m IN s ==> n <= m))
SET_CASES (finite sets)
  |- !s. (s = {}) \/ (?x t. (s = x INSERT t) /\ ~x IN t)
SET_INDUCT (finite sets)
  |- !P.
      P{} /\ (!s. P s ==> (!e. ~e IN s ==> P(e INSERT s))) ==> (!s. P s)
SET_MINIMUM (finite sets)
  |- !s M. (?x. x IN s) = (?x. x IN s /\ (!y. y IN s ==> (M x) <= (M y)))

3.3. Set inclusion 31

3.3 Set inclusion

EMPTY_SUBSET (finite sets)
  |- !s. {} SUBSET s
INSERT_SUBSET (finite sets)
  |- !x s t. (x INSERT s) SUBSET t = x IN t /\ s SUBSET t
NOT_PSUBSET_EMPTY (finite sets)
  |- !s. ~s PSUBSET {}
PSUBSET_DEF (finite sets)
  |- !s t. s PSUBSET t = s SUBSET t /\ ~(s = t)
PSUBSET_INSERT_SUBSET (finite sets)
  |- !s t. s PSUBSET t = (?x. ~x IN s /\ (x INSERT s) SUBSET t)
PSUBSET_IRREFL (finite sets)
  |- !s. ~s PSUBSET s
PSUBSET_MEMBER (finite sets)
  |- !s t. s PSUBSET t = s SUBSET t /\ (?y. y IN t /\ ~y IN s)
PSUBSET_TRANS (finite sets)
  |- !s t u. s PSUBSET t /\ t PSUBSET u ==> s PSUBSET u
SUBSET_ANTISYM (finite sets)
  |- !s t. s SUBSET t /\ t SUBSET s ==> (s = t)
SUBSET_DEF (finite sets)
  |- !s t. s SUBSET t = (!x. x IN s ==> x IN t)
SUBSET_EMPTY (finite sets)
  |- !s. s SUBSET {} = (s = {})
SUBSET_INSERT (finite sets)
  |- !x s. ~x IN s ==> (!t. s SUBSET (x INSERT t) = s SUBSET t)
SUBSET_REFL (finite sets)
  |- !s. s SUBSET s
SUBSET_TRANS (finite sets)
  |- !s t u. s SUBSET t /\ t SUBSET u ==> s SUBSET u

3.4 Intersection and union

DELETE_INTER (finite sets)
  |- !s t x. (s DELETE x) INTER t = (s INTER t) DELETE x
EMPTY_UNION (finite sets)
  |- !s t. (s UNION t = {}) = (s = {}) /\ (t = {})
INSERT_INTER (finite sets)
  |- !x s t.
      (x INSERT s) INTER t = (x IN t => x INSERT (s INTER t) | s INTER t)
INSERT_UNION (finite sets)
  |- !x s t.
      (x INSERT s) UNION t = (x IN t => s UNION t | x INSERT (s UNION t))
INSERT_UNION_EQ (finite sets)
  |- !x s t. (x INSERT s) UNION t = x INSERT (s UNION t)
INTER_ASSOC (finite sets)
  |- !s t u. (s INTER t) INTER u = s INTER (t INTER u)
INTER_COMM (finite sets)
  |- !s t. s INTER t = t INTER s
INTER_EMPTY (finite sets)
  |- (!s. {} INTER s = {}) /\ (!s. s INTER {} = {})
INTER_IDEMPOT (finite sets)
  |- !s. s INTER s = s
INTER_OVER_UNION (finite sets)
  |- !s t u. s UNION (t INTER u) = (s UNION t) INTER (s UNION u)
INTER_SUBSET (finite sets)
  |- (!s t. (s INTER t) SUBSET s) /\ (!s t. (t INTER s) SUBSET s)
IN_INTER (finite sets)
  |- !s t x. x IN (s INTER t) = x IN s /\ x IN t
IN_UNION (finite sets)
  |- !s t x. x IN (s UNION t) = x IN s \/ x IN t
SUBSET_INTER_ABSORPTION (finite sets)
  |- !s t. s SUBSET t = (s INTER t = s)

3.5. Set difference 33

SUBSET_UNION (finite sets)
  |- (!s t. s SUBSET (s UNION t)) /\ (!s t. s SUBSET (t UNION s))
SUBSET_UNION_ABSORPTION (finite sets)
  |- !s t. s SUBSET t = (s UNION t = t)
UNION_ASSOC (finite sets)
  |- !s t u. (s UNION t) UNION u = s UNION (t UNION u)
UNION_COMM (finite sets)
  |- !s t. s UNION t = t UNION s
UNION_EMPTY (finite sets)
  |- (!s. {} UNION s = s) /\ (!s. s UNION {} = s)
UNION_IDEMPOT (finite sets)
  |- !s. s UNION s = s
UNION_OVER_INTER (finite sets)
  |- !s t u. s INTER (t UNION u) = (s INTER t) UNION (s INTER u)

3.5 Set difference

DIFF_DIFF (finite sets)
  |- !s t. (s DIFF t) DIFF t = s DIFF t
DIFF_EMPTY (finite sets)
  |- !s. s DIFF {} = s
DIFF_EQ_EMPTY (finite sets)
  |- !s. s DIFF s = {}
EMPTY_DIFF (finite sets)
  |- !s. {} DIFF s = {}
IN_DIFF (finite sets)
  |- !s t x. x IN (s DIFF t) = x IN s /\ ~x IN t

3.6 Deletion of an element

DELETE_COMM (finite sets)
  |- !x y s. (s DELETE x) DELETE y = (s DELETE y) DELETE x

DELETE_DEF (finite sets)
  |- !s x. s DELETE x = s DIFF {x}
DELETE_DELETE (finite sets)
  |- !x s. (s DELETE x) DELETE x = s DELETE x
DELETE_INSERT (finite sets)
  |- !x y s.
      (x INSERT s) DELETE y =
      ((x = y) => s DELETE y | x INSERT (s DELETE y))
DELETE_NON_ELEMENT (finite sets)
  |- !x s. ~x IN s = (s DELETE x = s)
DELETE_SUBSET (finite sets)
  |- !x s. (s DELETE x) SUBSET s
DIFF_INSERT (finite sets)
  |- !s t x. s DIFF (x INSERT t) = (s DELETE x) DIFF t
EMPTY_DELETE (finite sets)
  |- !x. {} DELETE x = {}
INSERT_DELETE (finite sets)
  |- !x s. x IN s ==> (x INSERT (s DELETE x) = s)
IN_DELETE (finite sets)
  |- !s x y. x IN (s DELETE y) = x IN s /\ ~(x = y)
IN_DELETE_EQ (finite sets)
  |- !s x x'.
      (x IN s = x' IN s) = (x IN (s DELETE x') = x' IN (s DELETE x))
SUBSET_DELETE (finite sets)
  |- !x s t. s SUBSET (t DELETE x) = ~x IN s /\ s SUBSET t
SUBSET_INSERT_DELETE (finite sets)
  |- !x s t. s SUBSET (x INSERT t) = (s DELETE x) SUBSET t

3.7 Disjoint sets

DISJOINT_DEF (finite sets)
  |- !s t. DISJOINT s t = (s INTER t = {})

3.8. The CHOICE and REST functions 35

DISJOINT_DELETE_SYM (finite sets)
  |- !s t x. DISJOINT(s DELETE x)t = DISJOINT(t DELETE x)s
DISJOINT_EMPTY (finite sets)
  |- !s. DISJOINT {} s /\ DISJOINT s {}
DISJOINT_EMPTY_REFL (finite sets)
  |- !s. (s = {}) = DISJOINT s s
DISJOINT_INSERT (finite sets)
  |- !x s t. DISJOINT(x INSERT s)t = DISJOINT s t /\ ~x IN t
DISJOINT_SYM (finite sets)
  |- !s t. DISJOINT s t = DISJOINT t s
DISJOINT_UNION (finite sets)
  |- !s t u. DISJOINT(s UNION t)u = DISJOINT s u /\ DISJOINT t u
IN_DISJOINT (finite sets)
  |- !s t. DISJOINT s t = ~(?x. x IN s /\ x IN t)

3.8 The CHOICE and REST functions

CHOICE_DEF (finite sets)
  |- !s. ~(s = {}) ==> (CHOICE s) IN s
CHOICE_INSERT_REST (finite sets)
  |- !s. ~(s = {}) ==> ((CHOICE s) INSERT (REST s) = s)
CHOICE_NOT_IN_REST (finite sets)
  |- !s. ~(CHOICE s) IN (REST s)
CHOICE_SING (finite sets)
  |- !x. CHOICE{x} = x
REST_DEF (finite sets)
  |- !s. REST s = s DELETE (CHOICE s)
REST_PSUBSET (finite sets)
  |- !s. ~(s = {}) ==> (REST s) PSUBSET s
REST_SING (finite sets)
  |- !x. REST{x} = {}

REST_SUBSET (finite sets)
  |- !s. (REST s) SUBSET s
SING_IFF_EMPTY_REST (finite sets)
  |- !s. SING s = ~(s = {}) /\ (REST s = {})

3.9 Image of a function on a set

IMAGE_COMPOSE (finite sets)
  |- !f g s. IMAGE(f o g)s = IMAGE f(IMAGE g s)
IMAGE_DELETE (finite sets)
  |- !f x s. ~x IN s ==> (IMAGE f(s DELETE x) = IMAGE f s)
IMAGE_EMPTY (finite sets)
  |- !f. IMAGE f{} = {}
IMAGE_EQ_EMPTY (finite sets)
  |- !s f. (IMAGE f s = {}) = (s = {})
IMAGE_ID (finite sets)
  |- !s. IMAGE(\x. x)s = s
IMAGE_IN (finite sets)
  |- !x s. x IN s ==> (!f. (f x) IN (IMAGE f s))
IMAGE_INSERT (finite sets)
  |- !f x s. IMAGE f(x INSERT s) = (f x) INSERT (IMAGE f s)
IMAGE_INTER (finite sets)
  |- !f s t. (IMAGE f(s INTER t)) SUBSET ((IMAGE f s) INTER (IMAGE f t))
IMAGE_SUBSET (finite sets)
  |- !s t. s SUBSET t ==> (!f. (IMAGE f s) SUBSET (IMAGE f t))
IMAGE_UNION (finite sets)
  |- !f s t. IMAGE f(s UNION t) = (IMAGE f s) UNION (IMAGE f t)
IN_IMAGE (finite sets)
  |- !f s y. y IN (IMAGE f s) = (?x. (y = f x) /\ x IN s)

3.10. Mappings between sets 37

3.10 Mappings between sets

BIJ_COMPOSE (finite sets)
  |- !f g s t u. BIJ f s t /\ BIJ g t u ==> BIJ(g o f)s u
BIJ_DEF (finite sets)
  |- !f s t. BIJ f s t = INJ f s t /\ SURJ f s t
BIJ_EMPTY (finite sets)
  |- !f. (!s. BIJ f{}s = (s = {})) /\ (!s. BIJ f s{} = (s = {}))
BIJ_ID (finite sets)
  |- !s. BIJ(\x. x)s s
IMAGE_SURJ (finite sets)
  |- !f s t. SURJ f s t = (IMAGE f s = t)
INJ_COMPOSE (finite sets)
  |- !f g s t u. INJ f s t /\ INJ g t u ==> INJ(g o f)s u
INJ_DEF (finite sets)
  |- !f s t.
      INJ f s t =
      (!x. x IN s ==> (f x) IN t) /\
      (!x y. x IN s /\ y IN s ==> (f x = f y) ==> (x = y))
INJ_EMPTY (finite sets)
  |- !f. (!s. INJ f{}s) /\ (!s. INJ f s{} = (s = {}))
INJ_ID (finite sets)
  |- !s. INJ(\x. x)s s
LINV_DEF (finite sets)
  |- !f s t. INJ f s t ==> (!x. x IN s ==> (LINV f s(f x) = x))
RINV_DEF (finite sets)
  |- !f s t. SURJ f s t ==> (!x. x IN t ==> (f(RINV f s x) = x))
SURJ_COMPOSE (finite sets)
  |- !f g s t u. SURJ f s t /\ SURJ g t u ==> SURJ(g o f)s u
SURJ_DEF (finite sets)
  |- !f s t.
      SURJ f s t =
      (!x. x IN s ==> (f x) IN t) /\
      (!x. x IN t ==> (?y. y IN s /\ (f y = x)))

SURJ_EMPTY (finite sets)
  |- !f. (!s. SURJ f{}s = (s = {})) /\ (!s. SURJ f s{} = (s = {}))
SURJ_ID (finite sets)
  |- !s. SURJ(\x. x)s s

3.11 Singleton sets

DELETE_EQ_SING (finite sets)
  |- !s x. x IN s ==> ((s DELETE x = {}) = (s = {x}))
DISJOINT_SING_EMPTY (finite sets)
  |- !x. DISJOINT{x}{}
EQUAL_SING (finite sets)
  |- !x y. ({x} = {y}) = (x = y)
INSERT_SING_UNION (finite sets)
  |- !s x. x INSERT s = {x} UNION s
IN_SING (finite sets)
  |- !x y. x IN {y} = (x = y)
NOT_EMPTY_SING (finite sets)
  |- !x. ~({} = {x})
NOT_SING_EMPTY (finite sets)
  |- !x. ~({x} = {})
SING (finite sets)
  |- !x. SING{x}
SING_DEF (finite sets)
  |- !s. SING s = (?x. s = {x})
SING_DELETE (finite sets)
  |- !x. {x} DELETE x = {}

3.12 Cardinality of sets

CARD_DEF (finite sets)
  |- (CARD{} = 0) /\
     (!s x. CARD(x INSERT s) = (x IN s => CARD s | SUC(CARD s)))

3.12. Cardinality of sets 39

CARD_DELETE (finite sets)
  |- !s x. CARD(s DELETE x) = (x IN s => (CARD s) - 1 | CARD s)
CARD_DIFF (finite sets)
  |- !t s. CARD(s DIFF t) = (CARD s) - (CARD(s INTER t))
CARD_EMPTY (finite sets)
  |- CARD{} = 0
CARD_EQ_0 (finite sets)
  |- !s. (CARD s = 0) = (s = {})
CARD_INSERT (finite sets)
  |- !s x. CARD(x INSERT s) = (x IN s => CARD s | SUC(CARD s))
CARD_INTER_LESS_EQ (finite sets)
  |- !s t. (CARD(s INTER t)) <= (CARD s)
CARD_PSUBSET (finite sets)
  |- !s t. t PSUBSET s ==> (CARD t) < (CARD s)
CARD_SING (finite sets)
  |- !x. CARD{x} = 1
CARD_SUBSET (finite sets)
  |- !s t. t SUBSET s ==> (CARD t) <= (CARD s)
CARD_UNION (finite sets)
  |- !s t. (CARD(s UNION t)) + (CARD(s INTER t)) = (CARD s) + (CARD t)
LESS_CARD_DIFF (finite sets)
  |- !t s. (CARD t) < (CARD s) ==> 0 < (CARD(s DIFF t))
SING_IFF_CARD1 (finite sets)
  |- !s. SING s = (CARD s = 1)

40 Chapter 3. Pre-proved Theorems

References

[1] Z. Manna and R. Waldinger, The Logical Basis for Computer Programming: Volume 1, Deductive Reasoning, Addison-Wesley, 1985.

[2] T. F. Melham, The HOL sets library, University of Cambridge Computer Laboratory, October 1991.

[3] T. Melham, ‘A Package for Inductive Relation Definitions in HOL’, to appear in the Proceedings of the 1991 International Tutorial and Workshop on the HOL Theorem Proving System, 27–30 August 1991, Davis California (IEEE Computer Society Press).

[4] University of Cambridge Computer Laboratory, The HOL System: DESCRIPTION, revised edition, July 1991.

Index

ABSORPTION, 29

axiom of extension, 3 axioms for (*)set, 2–3

BIJ_COMPOSE, 37
BIJ_DEF, 14, 37
BIJ_EMPTY, 37
BIJ_ID, 37
CARD_DEF, 16, 38
CARD_DELETE, 39
CARD_DIFF, 39
CARD_EMPTY, 39
CARD_EQ_0, 39
CARD_INSERT, 39
CARD_INTER_LESS_EQ, 39
CARD_PSUBSET, 39
CARD_SING, 16, 39
CARD_SUBSET, 39
CARD_UNION, 39
CHOICE_DEF, 12, 35
CHOICE_INSERT_REST, 35
CHOICE_NOT_IN_REST, 35
CHOICE_SING, 35
COMPONENT, 30

conversions

   DELETE_CONV, 11
   FINITE_CONV, 15
   IMAGE_CONV, 13
   IN_CONV, 7–8
   INSERT_CONV, 10
   UNION_CONV, 9–10
DECOMPOSITION, 30

                                       define_finite_set_syntax, 4

definition

                                          of (*)set, 1–2

of BIJ, 14 of CARD, 16

                                          of CHOICE, 12
                                          of DELETE, 7
                                          of DIFF, 6
                                          of DISJOINT, 6
                                          of EMPTY, 2
                                          of FINITE, 15
                                          of IMAGE, 12

of IN, 2

                                          of INFINITE, 15

of INJ, 14

                                          of INSERT, 2, 7
                                          of INTER, 6
                                          of IS_SET_REP, 2

of LINV, 14

                                          of PSUBSET, 5

of REST, 12 of RINV, 14 of SING, 11

                                          of SUBSET, 5

of SURJ, 14

                                          of UNION, 6
                                       DELETE_COMM, 33
                                       DELETE_CONV, 11, 19
                                       DELETE_DEF, 7, 34
                                       DELETE_DELETE, 34
                                       DELETE_EQ_SING, 38
                                       DELETE_INSERT, 34

\underline{Index 43}

DELETE_INTER, 32
DELETE_NON_ELEMENT, 34
DELETE_SUBSET, 34
DIFF_DEF, 6
DIFF_DIFF, 33
DIFF_EMPTY, 33
DIFF_EQ_EMPTY, 33
DIFF_INSERT, 34
DISJOINT_DEF, 6, 34
DISJOINT_DELETE_SYM, 35
DISJOINT_EMPTY, 35
DISJOINT_EMPTY_REFL, 35
DISJOINT_INSERT, 35
DISJOINT_SING_EMPTY, 38
DISJOINT_SYM, 35
DISJOINT_UNION, 35
EMPTY_DELETE, 34
EMPTY_DIFF, 33
EMPTY_SUBSET, 5, 31
EMPTY_UNION, 32
EQUAL_SING, 38
EXTENSION, 3, 30
FINITE_CONV, 15
FINITE_DEF, 15
FINITE_EMPTY, 15
FINITE_INSERT, 15
FINITE_ISO_NUM, 16
FINITE_SET_DEF, 2, 29
IMAGE_11_INFINITE, 15
IMAGE_COMPOSE, 36
IMAGE_CONV, 13, 20
IMAGE_DEF, 12
IMAGE_DELETE, 36
IMAGE_EMPTY, 36
IMAGE_EQ_EMPTY, 36
IMAGE_ID, 36
IMAGE_IN, 36
IMAGE_INSERT, 36

                                       IMAGE_INTER, 36
                                       IMAGE_SUBSET, 36
                                       IMAGE_SURJ, 37
                                       IMAGE_UNION, 36
                                       IN_CONV, 7–8, 24
                                       IN_DELETE, 7, 34
                                       IN_DELETE_EQ, 34
                                       IN_DIFF, 6, 33
                                       IN_DISJOINT, 35
                                       IN_IMAGE, 12, 36
                                       IN_INSERT, 3, 7, 30
                                       IN_INTER, 6, 32
                                       IN_SING, 38
                                       IN_UNION, 6, 32

induction, 3–4

                                       INFINITE_DEF, 15
                                       INJ_COMPOSE, 37
                                       INJ_DEF, 14, 37
                                       INJ_EMPTY, 37
                                       INJ_ID, 37
                                       INSERT_COMM, 3, 30
                                       INSERT_CONV, 10, 22
                                       INSERT_DEF, 7
                                       INSERT_DELETE, 34
                                       INSERT_INSERT, 3, 30
                                       INSERT_INTER, 32
                                       INSERT_SING_UNION, 38
                                       INSERT_SUBSET, 31
                                       INSERT_UNION, 32
                                       INSERT_UNION_EQ, 32
                                       INTER_ASSOC, 32
                                       INTER_COMM, 32
                                       INTER_DEF, 6
                                       INTER_EMPTY, 32
                                       INTER_IDEMPOT, 32
                                       INTER_OVER_UNION, 32
                                       INTER_SUBSET, 32
                                       IS_SET_REP, 2, 29
                                       LESS_CARD_DIFF, 39

\underline{44 Index}

LINV_DEF, 14, 37
load_finite_sets, 18
MEMBER_NOT_EMPTY, 30

naming conventions for definitions, 2 for membership conditions, 6 for theorems about singletons, 11 for theorems generally, 6

NOT_EMPTY_INSERT, 30
NOT_EMPTY_SING, 38
NOT_EQUAL_SETS, 30
NOT_IN_EMPTY, 3, 30
NOT_INSERT_EMPTY, 30
NOT_PSUBSET_EMPTY, 5, 31
NOT_SING_EMPTY, 38
NOT_UNIV_PSUBSET, 5
NUM_SET_WOP, 30
print_set (flag), 5
PSUBSET_DEF, 5, 31
PSUBSET_INSERT_SUBSET, 31
PSUBSET_IRREFL, 31
PSUBSET_MEMBER, 31
PSUBSET_TRANS, 31
REST_DEF, 12, 35
REST_PSUBSET, 35
REST_SING, 35
REST_SUBSET, 36
RINV_DEF, 14, 37
SET_CASES, 30
SET_INDUCT, 3, 30
SET_INDUCT_TAC, 3–4, 25
SET_MINIMUM, 30
set_TY_DEF, 2, 29

SING, 11, 38

SING_DEF, 11, 38
SING_DELETE, 38
SING_IFF_CARD1, 39

                                       SING_IFF_EMPTY_REST, 36
                                       SUBSET_ANTISYM, 5, 31
                                       SUBSET_DEF, 5, 31
                                       SUBSET_DELETE, 34
                                       SUBSET_EMPTY, 31
                                       SUBSET_INSERT, 31
                                       SUBSET_INSERT_DELETE, 34
                                       SUBSET_INTER_ABSORPTION, 32
                                       SUBSET_REFL, 5, 31
                                       SUBSET_TRANS, 5, 31
                                       SUBSET_UNION, 33
                                       SUBSET_UNION_ABSORPTION, 33
                                       SUBSET_UNIV, 5
                                       SURJ_COMPOSE, 37
                                       SURJ_DEF, 14, 37
                                       SURJ_EMPTY, 38
                                       SURJ_ID, 38

tactics

                                          SET_INDUCT_TAC, 3–4
                                       UNION_ASSOC, 33
                                       UNION_COMM, 33
                                       UNION_CONV, 9–10, 26
                                       UNION_DEF, 6
                                       UNION_EMPTY, 33
                                       UNION_IDEMPOT, 33
                                       UNION_OVER_INTER, 33