[ProofPower] Confused about Z and HOL terms

[Rob Arthan]

On Thursday 13 May 2004 4:56 pm, Roger Bishop Jones wrote:
> On Thursday 13 May 2004 12:39 pm, Marcel Oliveira wrote:
> > Please take a look in the attached document.
>...
> For getting the term in, just use the parser.

In more detail: Z type inference inteprets schema valus differently depending 
on whether or not the syntactic context requires a predicate or an 
expression. For example in something like:

	[x : X | A = (B /\ C) /\ D]

"A = (B /\ D) /\ C" and "C" are predicates, but "A" and "B /\ C" are 
expressions. As Roger says the parser/type inferrer will sort this out for 
you automatically and coerce schemas-as-expressions into 
schemas-as-predicates where the language requires it. However, this only 
works in general when you're entering a specification, i.e., one or more 
complete Z paragraphs.  If you're entering Z terms, e.g.,  in a proof, the 
parser/type inferrer assumes you want expressions at the top level unless you 
tell it otherwise, which you can do with a special pseudo-toolkit function 
named Pi (capital greek Pi) which provides a context in which a predicate is 
expected.

If you want to write ML code that converts schemas-as-expressions into 
schemas-as-predicates, the syntax function that does it is called 
mk_z_schema_pred.

See attachment for Marcel's example done both ways.

By the way, conv_ascii and conv_extended are rather paranoid about not losing 
information. They both write their output to a temporary file and reconvert 
it to compare with the input. They don't overwrite the input file unless the 
reconverted output and the input are identical. In Marcel's case, the file 
didn't end with a new-line, but the conversion puts a new-line in at the end, 
hence conv_ascii complained.
 
>...
> To rewrite the term to simplify the precondition
> you first need to get yourself in the proof context
>...

Roger may well be right about this - as he says, it depends on what Marcel is 
trying to achive.

Regards,

Rob.

-------------- next part --------------
=TEX
\documentstyle[hol1,12pt]{article}

\begin{document}

=SML
open_theory "z_library";
new_theory "example_t";
open_theory "example_t";
set_flags [("z_type_check_only",false),("z_use_axioms",true)];

val hol_term_1 = mk_%and% ( mk_%not% (mk_t), 
			mk_%not% (mk_var ("okay'",%<%:BOOL%>%)) )
;
=GFT ProofPower Output
val hol_term_1 = %SZT%%not% true %and% okay'%>% : TERM

=SML
val sch = %SZT%[%Delta%[x:%bbN%] ; inx?:%bbN% ; outx!:%bbN% | inx? > 0 %and% x'=inx? %and% outx!=x]%>%;

val pre_sch = %SZT%%Pi%(pre [%Delta%[x:%bbN%] ; inx?:%bbN% ; outx!:%bbN% | inx? > 0 %and% x'=inx? %and% outx!=x])%>%;

val hol_term_2 = mk_%and% ( mk_%not%  pre_sch, 
			mk_%not% (mk_var ("okay'",%<%:BOOL%>%)) )
;

val hol_term_3 = mk_%and%(mk_%not% (mk_z_schema_pred(sch, "")),
			mk_%not% (mk_var ("okay'",%<%:BOOL%>%)) )
;

=GFT ProofPower Output
val hol_term_2 =
   %SZT%%not%
     (pre
         [(%Delta% [x : %bbN%]); inx? : %bbN%; outx! : %bbN%
             | inx? > 0 %and% x' = inx? %and% outx! = x])
     %and% %not%
     okay'%>% : TERM
=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

=TEX
\end{document}