On 14 Sep 2012, at 03:01, Jon Lockhart wrote: > Phil, > > Moving them all to there own paragraph worked great. Now I am up to proving > the consistency of the axioms, which is where I am run into my next stumbling > block. Got the spec load and the consistency goal using the commands no > problem. This generates a sub goal which looks relatively straight forward. > It using the "there exist" symbol at the front of the goal, so my initial > assumption is to use the z_"there exists"_tac, as seen in the provided spec.

## Advertising

Unfortunately I can't unzip your attachment to check exactly what you are doing. There is minimal proof support for consistency goals in Z, since very few Z users have expressed much interest in proving consistency. > Unfortunately just giving it masterStop is not enough, and I can't feed it a > list of masterStop and masterReset. Next thought was there should be some > tactic like this that also has list in it, but I can't seem to find one. 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]); 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. Regards, Rob.

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