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:## Advertising

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