Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Thu, 23 Mar 1995 19:10:47 +1000
From: Malcolm Newey <Malcolm.Newey@cs.anu.edu.au>
Message-Id: <199503230910.TAA29276@vega.anu.edu.au>
To: coe@sctc.com
Subject: Re: HOL sets
Cc: info-hol@leopard.cs.byu.edu


Mike,

You write:

>   let's say I have  a set of sets 
>         A = {  {2,3,4} , {1,5,7} .....}
>   what I want  is a function that will return the union
>   all of the sets in the set A.

I claim that what (I guess that) you want is not real simple.  In fact,
I wanted something isomorphic early last year, namely the definition of an
HOL function that added up the elements of a set of numbers.  This led me
to get embroiled in doing a serious job of extending the HOL sets libraries
in various ways.  Actually, if this enterprise had been finalized (as it
should have been by now), then it would give you what you want, and more.

John Harrison's suggestion is a different appropriate way to get started
but it get much harder if you are dealing with finite sets.

The next best thing to waiting (How long? Soon!) for the new edition of the
Sets Libraries is to use Ching Tsun Chou's contrib library called aci (which
stands for Associative, Commutative with Inverse).  Using it you can
make a definition, in the best of HOL traditions, of a function BIG_UNION
which will then have the definitional theorem

		!f. BIG_UNION f {} = {}    /\
                !f x S. BIG_UNION f (x INSERT S)
                                  = (x IN S) =>  BIG_UNION f S
                                              |  (f x) UNION (BIG_UNION f S)

In your case, you won't want to be bothered by the index set business, so
you can then make the definition
                FAMILY_UNION = BIG_UNION (\x.x)
and then you'll be able to prove
		FAMILY_UNION {{1,2,3},{3,4,x},{y,z,1,4}} = {1,2,3,4,x,y,z}

I imagine that you would then want the code for an appropriate conversion.  I
would recommend modelling it on Tom's design of conversions in the current sets
libraries.  For example, there you find UNION_CONV which is just the ticket for
proving   |-  {1, 3, x} UNION {1, SUC 2, y} = {1,3,x,y}

Thus you might write FAMILY_UNION_CONV so that
      FAMILY_UNION_CONV  num_eq_CONV  "FAMILY_UNION {{1,2,3},{3,4,x},{y,z,1,SUC 3}}"
would yield the theorem
      |-   FAMILY_UNION  {{1,2,3},{3,4,x},{y,z,1,SUC 3}} = {1,2,3,4,x,y,z}


Again, the Melham model for finite set conversions (see file fset_conv.ml in
your favourite sets library) for inspiration when it comes to coding.

Malcolm