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 consistency:a(%exists%_tac %<%(%SZT%3%>%, %SZT%2%>%, %SZT%1%>%)%>% THEN PC_T1 "z_library" 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.
Phil
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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
