Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <9503232035.AA16499@ice.cs.ucdavis.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Re: HOL sets
In-Reply-To: Your message of "Thu, 23 Mar 95 19:10:47 +1000." <199503230910.TAA29276@vega.anu.edu.au>
Date: Thu, 23 Mar 95 12:35:11 -0800
From: shaw@cs.ucdavis.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.


I didn't know about the aci library until just now. I've had to do this 
sort of thing a couple of times in the past, and I mimicked the construction
of the CARD definition. You start by defining a relation between the domain
and range of the function you want (either sets of nums and nums for the 
summing of elements, or sets of sets of nums and sets of nums in the above
example), and then you prove that this relation actually defines a function.

The fact that the function exists allows you to invoke new_specification
directly. See how CARD is defined for more info.

It sounds as if aci has proven that this always works when the function
is commutative and associative over the set elems?

Rob