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
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