*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Export of proofs from Isabelle in "fully-expanded" form*From*: Sean McLaughlin <seanmcl at cmu.edu>*Date*: Fri, 13 Jan 2006 09:33:35 -0500*References*: <57DC67BD-D12E-4F6C-821E-86BB2CF20852@cmu.edu>

Hi Robin, The documentation for proof terms can be found in thereference manual, section 5.4. I've been using these proof terms agreat deal,and find them very easy to use. There are basically two ways touse them.One is to interface directly with sml and manipulate theProofterm.prooftermdata structure directly. The other is to transform the prooftermto another format,eg. xml. If there is any possible way, I highly suggest using thefirst option.All the Isabelle functions are then available to you for queryingdifferent aspectsof the proof. There are also some undocumented conventions which do notshow up in the proof terms and are thus difficult to reconstructfrom the termsthemselves. One example is type application. If a theorem hasfree type variables,when it is instantiated, these types are supplied in the proofterm. However, theyare supplied in a nonintuitive order, given by the Isabellefunction "term_tvars".Another thing to notice is that beta reduction is not recorded tokeep theterms a reasonable size. Best, Sean On Jan 12, 2006, at 9:33 AM, Robin Green wrote:A question about transforming Isabelle proofs into reallyelementary, long-winded form:I have not used Isabelle yet, but I have read in three places thatIsabelle is designed to support many different logics and theoriesby having a relatively simple core language upon which everythingelse is implemented. It should, therefore, be possible to getIsabelle to output a proof _entirely_ in this core language (i.e.so that it uses only the very primitive notation from this corelanguage, and only the most elementary possible inferences areused, and no other files are referred to), so that it can beindependently verified by a very small, easy-to-reason-about proofverifier. (Of course that still leaves the question of whether thetranslation is correct, but let's ignore that for now.)When I talk about "the most elementary possible inferences", I amthinking of something like Metamath[1], which is apparently basedentirely on simple substitution rules. In other words,emphatically not (non-trivial) tactics.In [2], I found a tantalising hint which suggests that thisfeature became available in Isabelle 99:"The Isabelle 98 version is used in this thesis, although a laterversion (Isabelle99) has since been released. These recent versionsof Isabelle support the construction and export of proofderivations, a feature that was not available in early versions ofIsabelle."However, I've been unable to ascertain, by browsing thedocumentation, where this export feature that Watson refers to,is. Is it there but undocumented, have I missed it, or have Imisunderstood 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, TheUniversity of Queensland, Queensland, Australia, 2002. http://citeseer.ist.psu.edu/watson01generic.html

- Previous by Date: Re: [isabelle] Export of proofs from Isabelle in "fully-expanded" form
- Next by Date: Re: [isabelle] Isabelle2005 proof terms
- Previous by Thread: Re: [isabelle] Export of proofs from Isabelle in "fully-expanded" form
- Next by Thread: [isabelle] Isabelle2005 proof terms
- Cl-isabelle-users January 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list