[ProofPower] z_output_theory questions

[Roger Bishop Jones]

On Friday 10 September 2004  5:04 am, Stephen Brackin wrote:
> I'm trying to produce a nice printout of the theory I'm
> working in for future reference, but have run into a couple of
> questions:

On further reflection I thought the following observations might
be helpful.

When I am working in Z I don't print or refer to theory listings.
The document which contains a Z specification is usually much
more readable than the listing of the theory it produces.
When I am working in HOL I often include a theory listing in the
source document, but usually the specifications are moderate in
size and the main point is to list the theorems.

Large types are hard to work with and I adopt subterfuges to keep
down the complexity of the types.
In HOL I make judicious use of labelled product types to create
new type constructors which simplify the type expressions.
In Z its harder, but some simplification might be achieved using
trivial free type definitions.

If I were doing proofs about a medium to large Z specification
I would be inclined to put the theorems in a child theory
so that they could be listed without the specification.

Roger Jones