Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 7 Jul 1994 06:32:36 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA29630;
          Wed, 6 Jul 1994 23:24:11 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA29626;
          Wed, 6 Jul 1994 23:24:00 -0600
Received: from itd0.dsto.gov.au by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA03163;
          Wed, 6 Jul 1994 22:20:57 -0700
Received: from tcs22.dsto.gov.au by itd0.dsto.gov.au 
          with SMTP (5.64+1.3.1+0.50/DSTO-1.0) id AA00313;
          Thu, 7 Jul 1994 14:49:48 +0930
Date: Thu, 7 Jul 1994 14:49:48 +0930
From: Jim Grundy <jug@itd.dsto.gov.au>
Message-Id: <9407070519.AA00313@itd0.dsto.gov.au>
To: heckman@cs.ucdavis.edu
Subject: Re: mappings
In-Reply-To: Mail from 'info-hol-request@lal.cs.byu.edu' dated: Wed, 6 Jul 1994 21:21:00 -0700
Cc: info-hol@cs.uidaho.edu

Hi

> 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.

I don't think you will be able to do exactly what you want - that is I don't
think you can define a HOL type that is the same as VDM mappings
(aka ZF functions, aka Z functions).

I think you will have to content yourself with using sets of pairs and defining
a predicate on them say called "IsMapping" which is true if the set of pairs
has the desired property (i.e. no element in the domain maps to more than one
element in the range).  Then you could prove things like 
  IsMapping f /\ IsMapping g ==> IsMapping (f intersect f)

Note that because VDM mappings are the same as Z functions, and because people
have investigated Z in HOL you can be assured that what you want has been
done before.  Check out the reference below, for a description of Mike's
representation of Z in HOL (check out ICL Proof Power for another).

@INPROCEEDINGS{Bow94a,
    author      = "Johnathon P. Bowen and Michael J. C. Gordon",
    title       = "{Z} and {HOL}",
    booktitle   = "Proceedings of the 8th Annual {Z} User Meeting",
    series      = "Workshops in Computing",
    editor      = "J. Anthony Hall",
    month       = "29--30 June",
    year        = 1994,
    address     = "St. John's College, University of Cambridge,
                    Cambridge, England",
    organization= "BCS-FACS",
    publisher   = "Springer-Verlag, London"}

Hope this helps

Jim