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