[ProofPower] Confused about Z and HOL terms

[Philip Clayton]

Possibly an irrelevant point --- not sure:
where Marcel has said

=GFT Desired Output
val hol_term_2 = %<%%not% (%exists%x':%bbN% ; outx!:%bbN% %spot% inx? > 
0 %and% x'=inx? %and% outx!=x) %and% okay'%>% : TERM

it looks like variable names ending in ? and ! are wanted in the HOL 
lexis.  For these, e.g. $"inx?" has to be written because inx? is not a 
(single) name in the HOL lexis, unlike Z:

dest_term %<%outx!%>%; (* an application *)
dest_term %<%$"outx!"%>%; (* a variable *)


Phil.

Roger Bishop Jones wrote:

>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)
>
>
>_______________________________________________
>Proofpower mailing list
>Proofpower at lemma-one.com
>http://dropkick.trouble-free.net/mailman/listinfo/proofpower_lemma-one.com
>
>
>  
>