On Wednesday 24 June 2009 16:07:02 Frank Zeyda wrote: >Since the HOL choice functions >(Choose) is not lifted to Z sets, incorporating it in a prove benefits >from a conversion that either lifts all set expressions into Z or HOL >sets.
I didn't understand that bit. Though I do see that mu (which once used to be choice in Z) is definitely implemented as definite description (because Spivey decided to worry about choice and the standards group then followed suit), which is just a an exercise in making something less useful than it might have been and causing anyone who wants choice in Z a pain in the ... Presumably its easy enough to define a choice function in Z, and if you are working in axiomatic mode you won't even need to drop into HOL to get the definition validated. >My experience so far is that for the common stuff it is not >necessary to worry about underlying HOL encodings, but for the more >fancy things it is difficult to avoid it. If you start doing serious work in Z you will soon reach the limits of what can be done without knowing the underlying HOL. There are too many gaps in the Z proof automation for it to be otherwise. >PS: Is there, or would it be worth, to maintain a common repository of >ProofPower utilities and extensions such as additional conversions, >tactics, proof context, normalisations, hacks, little examples "how to >do" stuff, etc. implemented and shared by its users? It may not be >appropriate to incorporate all of them into the standard distribution, >but maybe other users could nevertheless benefit from them (I would >certainly be happy to contribute, and be interested in other users' >contributions). This hasn't happened possibily because the most extensive application of ProofPower has been by QinetiQ and they often place contracts with lemma-one for enhancements to ProofPower and the compliance tool to meet their needs. There are two ways at present for users to make their work available to others. These are also appropriate ways to submit material to Rob for him to consider whether it should be incorporated into the base. The first is patches, which applies mainly to fixing whats already there. There is a good description of how to use patches at: http://lemma-one.com/ProofPower/patches/contrib.html The other way of sharing is exemplified by Rob's maths_eqs. This involves preparing a tar file which can be distributed and which the user then unpacks and "make"s to get a new database with additional theories and or tactics etc. These things can be stacked. I have for some time done my work with ProofPower in that format, so at any time I can pack up a complete tar file of my ProofPower based work and post it off to someone else who can then replicate what I am doing. This was handy a little while ago when I found a bug, and enabled Rob to recreate the problem without any hazzle either for him or for me. My own tarfile builds on top of the maths_egs database. If you look at the maths_egs stuff its full of very solid stuff, and in particular the theory of analysis is not an "example", it is a major development of formalised mathematics and is on a larger scale than any work I have ever done. So you can see here, that Rob has a policy of not including in the distribution things which don't need to be there, even if they are solid and important. My own stuff is much more experimental, very varied, and shows the history of my painful acquisition of something like practical competence with ProofPower over many years (I didn't get much chance to do proofs in the days when ProofPower was being developed). So I don't expect anyone else to make use of my stuff, though there might be some useful ideas there. None of it is in Z so it won't be a lot of help to you, but there is a web page at: rbjones.com/rbjpub/pp/doc from which the tarfile is downloadable if you want to see or try it. The make file I use was adapted from the one in Rob's maths_egs, and knows how to build the databases, create the documents and how to build the distributable tarfile. Mine is now getting a bit complicated since I have been hacking at it for many years, so its better to start from the original if you want to do this. Rob did encourage me to set up a proper contrib system years ago, and I might have done something about it if I had ever had anything I though others might use, but my stuff is always far out on some limb or other, and I never produce nice clean complete pieces of work like those in maths_egs, so I never could motivate myself to do anything on a contrib system. Anyway, let me know if I can be of any further help. Roger Jones PS I should add that I am not associated with lemma-one in any formal way, and do not speak for lemma-one or Rob Arthan. _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com