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

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'

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:


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

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

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

Reply via email to