Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Wed, 6 Jul 1994 21:21:00 -0700
From: heckman@cs.ucdavis.edu (Mark R. Heckman)
Message-Id: <9407070421.AA27983@shangrila.cs.ucdavis.edu>
To: info-hol@cs.uidaho.edu
Subject: mappings

I'm trying to create a type in hol that implements VDM mappings, but
I don't understand enough about hol types to do this.

Intuitively, a VDM mapping is sort of a cross between a set and a function.
Each element of the mapping consists of an id and a value. 
There is only one element in a mapping that has a particular id. 
For example:

{ (a,1) (b,2) (c,1) } 

is a mapping from the chars to the numbers.

It differs from a set in that, where a set would determine unique
elements based on both the id and value (e.g., it would allow
{(a,1) (a,2)}), a mapping uses only the id.
It differs from a function in that you can manipulate it like a set.
Ideally, I'd like to be able to use fundamentally the same operators
as for sets.

Does this already exist in HOL?  Is there some simple way to
implement this that inexperience prevents me from seeing?
Can someone point me in the right direction?

Thanks,

Mark Heckman
heckman@cs.ucdavis.edu