On 14/09/12 15:50, Rob Arthan wrote:
When you set up the consistency goal for a Z axiomatic description, what
you see is a mixture of HOL and Z and the existential quantifier is an
HOL quantifier not a Z one. So you would need to use %exists%_tac rather
than z_%exists%_tac. If the axiomatic description defines several global
variables, the witness you need would be provided as a HOL tuple. As the
witnesses for the individual variables are likely to be Z terms, you are
already into some not entirely trivial mixed language working. I just
tried a Z axiomatic description declaring three integers x, y, and z
with defining property x > y > z > 0. Here is the tactic that proves the

a(%exists%_tac %<%(%SZT%3%>%, %SZT%2%>%, %SZT%1%>%)%>% THEN PC_T1
         rewrite_tac[z'decl_def, z'dec_def]);

This has really confused me! I get a Z existential quantifier for the initial goal. Even when there are generic parameters, I still get a Z existential quantifier, it's just that the witness must be a HOL function. Are you sure you used z_push_consistency goal rather than push_consistency_goal? Perhaps there is a ProofPower issue on some platforms or am I just missing something?

A while ago, I had an issue with z_push_consistency_goal where it failed to produce the expected Z statement - I can't remember exactly what went wrong. This issue was that the initial proof step it performs was sensitive to the environment - the proof context, I think. However, I can't reproduce the issue.


Even when you translate that back into the extended character set (e.g.,
by pasting the bit between %<% and %>% into ProofPower), it is not very
nice. So on the whole I don't think doing consistency proofs is not a
good place to start learning proof in Z, because it will expose too much
HOL to you. If you have a strong interest in doing consistency proofs
later on, it would actually be quite easy to provide some tools to
protect you from the HOL.

Finally, there isn't a list flavour of %exists%_tac or z_%exists%_tac.
It would be a minor convenience in HOL (where existentials with a list
of bound variables are obtained by iterating existential quantifier over
a single variable), but MAP_EVERY %exists%_tac does what you want. It is
rarely what you want in Z, where you use a binding display as the
witness for an existential quantifier that binds several variables and
where iterated existential quantification is fairly rare.

Proofpower mailing list

Reply via email to