When entering a mixed HOL and Z term as follows:

  %<%%lambda% dummy %spot%
    %SZT%[[x : 1 .. 2] | 3 < x']%>%

the Z part of the term is printed back as

  [[x' : 1 .. 2] | 3 < x']

- note the extra prime. This is nothing new - just a consequence of HOL term operations renaming a bound variable in the underlying HOL representation of the Z term, leading to a 'denormalized' Z term. There is no issue with the logic for mechanized proof, though it could well cause some confusion when reading the printed version.

On the few occasions I have seen this before, it has been during interactive proof. I assume that %alpha%_to_z_conv/%alpha%_to_z will be used in future to avoid this sort of thing in Z variants of HOL proof support. However, I'm not sure that you can, or would want to, use the above functions to adjust the Z parts of a term when reading quotations.

Should these 'denormalized' Z terms be rejected as Z terms, thus printed as plain HOL? The documentation for %alpha%_to_z_conv/%alpha%_to_z suggests that such terms "fail to be Z", if I understand it correctly.

On the other hand, it is useful to see Z syntax so perhaps the Z printer should somehow warn that it is printing a 'denormalized' Z (sub)term?

Also, for the offending subterm

  [x' : 1 .. 2]

basic_dest_z_term returns BdzOk ... - should it? (Would it be useful for datatype BDZ to have another category, e.g. BdzDenorm ?)


Proofpower mailing list

Reply via email to