Roger, Thanks for the help. I from what you have just said I better understand about the consistency proofs for axioms in ProofPower, and more importantly Zed. I will probably in the future if I have complicated and none trivial axioms to prove, then I will just leave the variable set to true. In most of the specifications I have worked on and currently working on, I have only been uisng axioms as a way to declare global variables and constraints to the system, so that it gives the developer a more constrained box to work in when taking the specification and converting it to code.
I will take a look at the axiomatic proof you did and see if I can't use it to help me finish proving the rest of my axioms before I move on to finishing the preconditions of my operations. Thanks, Jon On Fri, Sep 14, 2012 at 1:48 PM, Roger Bishop Jones <[email protected]> wrote: > On Friday 14 Sep 2012 17:39, Jon Lockhart wrote: > > > First, I find it odd that the zipping is not working when > > before it was for Phil, and still is for me. I just > > generated a zip, emailed it to myself, and then unzipped > > it and got something that looks just fine, exactly what > > I zipped up. I have though created an ascii version of > > the document, and have attached on here along with > > another attempt at zipping the binary file. Let me know > > if you guys are able to use either of these. > > The gzipped version is good this time. > > I now see the beginnings of your consistency proof which was > not present in the last version. > I have completed the proof. > This involved using a Z binding display for the witness (of > which the signature is as in the goal and each component is > set to "True") and rewriting the result with the > specification of BOOLEAN, so it is just a one-liner as you > would hope. > > > Third, Rob I guess I will head your advice at the moment > > and just reset the axiom consistency variable back to > > true after you guys look at this next round of files. My > > purpose and goal is to try and prove my specification, > > the states, the operations, etc. to show the validity of > > the specification before moving on to trying to code > > from the spec. If the consistency is not that big of an > > issue and can be looked over without harming the > > validity of the specification then I will do that, and > > just assume consistency. Just from rereading page 93 of > > the tutorial, it made it seem like the consistency proof > > was very straight forward. > > I looked back to that passage and I see how it might be > misread. > There are two stages involved when not working in axiomatic > mode. > When an axiomatic specification is processed, instead of > being asserted as an axiom, it is introduced with a > consistency caveat and this modified specification is > automatically proven consistent by the system. > This consistency proof is trivial. > However, to recover the intended theorem the consistency > caveat has to be proven true, and in general this may not be > trivial. > In HOL this too is frequently done automatically (or rather > the consistency proof is done automatically before the > specification is stored so the caveat is not necessary), but > the proofs are more difficult in Z and this is one area in > which didn't get much attention in the original development > project, and which has never been raised as a priority by > ProofPower users since then. > So these consistency proofs are not automated. > > Whether they are hard or difficult depends on the specification > whose consistency is at stake. > In the case you were attempting, the proof is indeed > trivial, you just need to know how to go about it (as > described above). > > (I attach a revised version of your document with the proof > fixed). > > Roger >
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
