[ProofPower] Confused about Z and HOL terms

[Roger Bishop Jones]

On Thursday 13 May 2004 12:39 pm, Marcel Oliveira wrote:

> Please take a look in the attached document.
>
> First: I couldn't understand why the output for the hol_term_1
> is between Z quotations, as it were a Z term. Does anyone know
> why?

There is only one type of TERM, which is the HOL term.
When you type in Z syntax, it is encoded in a HOL term
using various semantic constants which correctly capture
in HOL the meaning of the Z.
When a term is printed the pretty printer makes a judgement
about whether it should be printed in HOL or in Z by checking
for the presence of the constants which semantically
represent the constructors in the Z language.
However, some of the Z translates into HOL without using
any special constants peculiar to Z, and in particular
the boolean operators, when used in predicates (but not
in schema expressions) map directly to the same operators
in HOL.
If the pretty printer is trying to print a term which
could either be just HOL or could be Z encoded in HOL,
then it decides how to print it according to the current
theory.  Since you are in a child of "z_library" the
pretty printer will default to printing in Z, and will
drop into HOL only if it finds a term or subterm which
cannot be printed as Z. 

> Second: In hol_term_2, I am trying to declare a HOL predicate
> as the desired output presented in the document. However, of
> course I cannot apply mk_(not) to the pre sch. I've bee trying
> very hard to get the desired predicate but, until now,
> couldn't find a way. Does any one know how to do it? (note
> that, if possible, I would like a pure HOL term, with no Z
> terms inside it.)

Well, the error message says it all really.

You have typed in a Z schema expression, which denotes
a set of bindings, and does not therefore have type BOOL.
(try z_type_of sch)
When you apply mk_pre to it you get a term which is
still a schema expression, and still a set of bindings
(though the signature has changed), so when you
apply mk_not, it throws it out.

You can't do what you want to do using syntactic
constructors.  If you build things out of a term
using a syntactic constructor, then that term will
always be a constituent.  To get where you want to
be, i.e. with a term which is the predicate arising
from simplification of the precondition expression,
you have to use inference not mere construction.
So first you put in the precondition expression,
and then you try to rewrite it into the form you
want.
For getting the term in, just use the parser.
To rewrite the term to simplify the precondition
you first need to get yourself in the proof context
"z_language" which knows how to do this kind of thing,
and then use:

rewrite_conv[]zterm;

Which will give you a theorem with your original 
term on the left and the "simplified" term on the
right.

If you want the term itself then you will have to
pick apart the theorem using the relevant syntactic
destructors.  However, it isn't "pure HOL" because
it has a Z existential quantifier inside it, so
to get it into "pure HOL" you would have some more
inference to do.

This is probably not the right way to go about whatever
it is that you are trying to do, but without a better
idea of what that is, I can't tell you what the best
approach would be.

Roger Jones

- rbj01 at rbjones.com
   plain text email please (non-executable attachments are OK)