Date: Tue, 9 May 89 0:19:21 BST
From: Tom Melham <tfm%computer-lab.cambridge.ac.uk%NSFnet-Relay.AC.UK@munnari.oz>
To: info-hol%clover.ucdavis.edu@NSFnet-Relay.AC.UK
Subject: re: predicate representation of sets.


Elsa's idea for defining sets (both finite and infinite) can be quickly
prototyped in HOL as follows. (Admission: I've not actually run this)

% Define an axiom for sets.                                             %
let set_axiom =  define_type `set_axiom` `set = SET (*->bool)`;;

% Define the empty set.                                                 %
let EMPTY = new_definition (`EMPTY`,"EMPTY = SET (\x:*.F)");;

% define set membership.                                                %
let IN = new_recursive_definition true set_axiom `IN`
        "IN (x:*) (SET P) = P x";;

% define {x:*}.                                                         %
let SINGLETON = new_recursive_definition false set_axiom `SINGLETON`
             "SINGLETON (x:*) = SET (\y:*. x=y)";;

% Define a destructor on "sets"---gives CF                              %
let CF = new_recursive_definition false set_axiom `CF`
             "CF (SET (P:*->bool)) = P";;



% define union.                                                         %
let UNION = new_recursive_definition true set_axiom `UNION`
             "UNION s1 s2 = SET (\x:*. CF s1 x \/ CF s2 x)";;

% define intersection.                                                  %
let INTERSECT = new_recursive_definition true set_axiom `INTERSECT`
             "INTERSECT s1 s2 = SET (\x:*. CF s1 x /\ CF s2 x)";;


FINITE sets are another story.... I'm hoping to do these automatically
in the next version of my types package.  (Coming soon.... as they say!).

Tom