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 ?)`

Phil _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com