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



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.