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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to