--Boundary-00=_x9JpA5Bg3eoLVIE
Content-Type: text/plain;
charset="iso-8859-1"
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
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.
--Boundary-00=_x9JpA5Bg3eoLVIE
Content-Type: text/plain;
charset="iso-8859-1";
name="schemapred.doc"
Content-Transfer-Encoding: 7bit
Content-Disposition: attachment; filename="schemapred.doc"
=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}
--Boundary-00=_x9JpA5Bg3eoLVIE--