[isabelle] Export of proofs from Isabelle in "fully-expanded" form

Hi Robin,

  The documentation for proof terms can be found in the
reference manual, section 5.4. I've been using these proof terms a great deal, and find them very easy to use. There are basically two ways to use them. One is to interface directly with sml and manipulate the Proofterm.proofterm data structure directly. The other is to transform the proofterm to another format, eg. xml. If there is any possible way, I highly suggest using the first option. All the Isabelle functions are then available to you for querying different aspects
of the proof.
  There are also some undocumented conventions which do not
show up in the proof terms and are thus difficult to reconstruct from the terms themselves. One example is type application. If a theorem has free type variables, when it is instantiated, these types are supplied in the proof term. However, they are supplied in a nonintuitive order, given by the Isabelle function "term_tvars". Another thing to notice is that beta reduction is not recorded to keep the
terms a reasonable size.



On Jan 12, 2006, at 9:33 AM, Robin Green wrote:

A question about transforming Isabelle proofs into really elementary, long-winded form:

I have not used Isabelle yet, but I have read in three places that Isabelle is designed to support many different logics and theories by having a relatively simple core language upon which everything else is implemented. It should, therefore, be possible to get Isabelle to output a proof _entirely_ in this core language (i.e. so that it uses only the very primitive notation from this core language, and only the most elementary possible inferences are used, and no other files are referred to), so that it can be independently verified by a very small, easy-to-reason-about proof verifier. (Of course that still leaves the question of whether the translation is correct, but let's ignore that for now.)

When I talk about "the most elementary possible inferences", I am thinking of something like Metamath[1], which is apparently based entirely on simple substitution rules. In other words, emphatically not (non-trivial) tactics.

In [2], I found a tantalising hint which suggests that this feature became available in Isabelle 99:

"The Isabelle 98 version is used in this thesis, although a later version (Isabelle99) has since been released. These recent versions of Isabelle support the construction and export of proof derivations, a feature that was not available in early versions of Isabelle."

However, I've been unable to ascertain, by browsing the documentation, where this export feature that Watson refers to, is. Is it there but undocumented, have I missed it, or have I misunderstood what it is? Or is it simply not there?

Robin Green
PhD student, University College Dublin, Ireland

[1] http://metamath.org/

[2] Geoffrey N. Watson. A Generic Proof Checker. PhD thesis, The University of Queensland, Queensland, Australia, 2002. http:// citeseer.ist.psu.edu/watson01generic.html

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.