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
elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com