Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Tue, 12 Sep 95 14:03:58 +0200
From: thomas@prosun.first.gmd.de (Thomas Neustupny)
Message-Id: <9509121203.AA17813@prosun.first.gmd.de>
To: Donald.Syme@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu
Subject: Re: Z-Embedding in HOL90 as in HOL88/Contrib ??? - 
         comp.specification.z #2225

In article <42f2r2$kr9@lyra.csx.cam.ac.uk>, Donald.Syme@cl.cam.ac.uk (Donald Syme) writes:
|> > > Hello,
|> > > 
|> > > does anybody know if there exists a free Z embedding in HOL90,
|> > > as it exists in the contrib area of HOL88 ?
|> > > 
|> > > Thanks,
|> > > Thomas N.
|> > 
|> > 
|> 
|> I did most of the required work about 5 months ago, and will be getting
|> back to it after the HOL95 user's meeting.  I got as far as:
|> 	- representing Z schemas in HOL terms (using Mike's scheme,
|> modified to represent schemas as abstractions, rather than terms
|> with free variables.  This seems a better way to go in the long run)
|> 	- implementng pretty printing for TkHolTkHolTkHol (the graphical
|> interface for hol90) so schemas really look like scehmas, with
|> boxing, delta symbols, fonts, subterm selection and so on.
|> 	- implementing 50% of the preterm code needed to get decent
|> schema entry facilities.
|> 
|> In the long term, I plan to do alot of work on this topic.  I
|> hope to implement a HOL90 Z tool as part of my PhD. thesis as an example of how
|> to build extended systems on top of LCF (HOL/Isabelle) theorem
|> provers.  The tool may incorporate an external type checker (fuzz),
|> and will include reasoning support for Z.  I would guess the first 
|> usable version will be available in January of February next year - I'll
|> certainly be looking for beta testers if you're interested.
|> 
|> I hope that's of some help.
|> 
|> Don Syme
|> 
|> -----------------------------------------------------------------------------
|> At the lab:							     At home:
|> The Computer Laboratory                                          Trinity Hall
|> New Museums Site                                                      CB2 1TJ
|> University of Cambridge                                         Cambridge, UK
|> CB2 3QG, Cambridge, UK
|> Ph: +44 (0) 1223 334688				      Ph: +44 (0) 1223 302521
|> http://www.cl.cam.ac.uk/users/drs1004/     
|> email: Donald.Syme@cl.cam.ac.uk
|> -----------------------------------------------------------------------------

Hi Donald,

I'm highly interested to become a beta tester for your Z extension. We have
both HOL90 and Isabelle, and a collegue plans to embed Z in Isabelle. We also
have fuzz and TkHol, so this would be no Problem.

Hope to hear from you,

Thomas N.