Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: info-hol@leopard.cs.byu.edu
Subject: Re: Preterms and term location specifications
In-Reply-To: Your message of "Wed, 12 Apr 1995 16:18:11 +0200." <95Apr12.161822met_dst.8082@sunbroy14.informatik.tu-muenchen.de>
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Wed, 12 Apr 1995 19:03:49 +0100
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:289080:950412180357"@cl.cam.ac.uk>


> > I am wondering whether the internals of the preterm signature in hol90
> > should be publically available or not.  (It isn't at the moment.)
> 
> Yes, it should be! Otherwise hol90 will never be able to emulate the
> magisterial syntactic manipulations that Mike Gordon has performed in
> the course of embedding Hoare Logic and Z in hol88.

I was kind of figuring (and hoping) you might say that!  So I would
imagine it will  be available in hol90.8?

Unfortunately I need my interface code to work with
hol90.7 executables, until the release of hol90.8.  Hence I will just
use terms as my term-locators until then, hidden behind an
appropriate signature of course.

> 
> Phrases such as
> 
>     !_. M
> 
> won't work because "!_" is taken to be a single lexeme. (A minor
> extension to the parser is also necessary.) The same problem crops up
> with identifiers incorporating ":", ",", and "~"; one wants these to be
> both separate names in their roles as delimiters (or prefixes) and also
> subcomponents in names, e.g., one might want to use "::" as an infix
> version of "CONS". Aside from that, expressions such as
> 
> >   "!_. (_ = [P;_]) /\ _ /\ Q"
> 
> won't be as general as wished because the "_" as a variable is not
> polymorphic (let-bound polymorphism only arises from constants in
> HOL). On the other hand, if the "_" had been declared as a constant, the
> expression would be deemed silly at the point of attempting to quantify
> over a constant. I suppose one could teach the parser that underscores
> in binding occurrences are to be treated as variables, and all other
> occurrences of underscores are to be treated as instances of a
> polymorphic constant.
> 

i.e. "_" is always a polymorphic variable which 
doesn't have the restriction that
it must have the same type at each point in the term?

For the moment I am using "_" as a constant, which means that
it can't be used for bound variables.  That's OK though. 

> 
> How about "type_of o #const o const_decl"?
>

magic! (but not obvious)

Thanks heaps,
Don