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.
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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
