[isabelle] Export of proofs from Isabelle in "fully-expanded" form
Robin Green
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
[2] Geoffrey N. Watson. A Generic Proof Checker. PhD thesis, The
University of Queensland, Queensland, Australia, 2002.
http://citeseer.ist.psu.edu/watson01generic.html
Makarius
> A question about transforming Isabelle proofs into really elementary,
> long-winded form:
> In [2], I found a tantalising hint which suggests that this feature
> became available in Isabelle 99:
See Stefan Berghofer's thesis for a slightly more up-to-date report on
proof terms (based on lambda calculus) for Isabelle/Pure. The Introduction
and chapter 2 should give you some idea how this looks like.
Stefan Berghofer. Proofs, Programs and Executable Specifications in
Higher Order Logic. Ph.D. thesis, Institut für Informatik, Technische
Universität München, 2003.
http://www4.in.tum.de/~berghofe/papers/phd.pdf
> 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.
I would consider the Metamath format slightly low-level, with adhoc
handling of bound variable scopes; lambda calculus provides a more
abstract and clean notion of variable binding and substitution.
Also note that the actual primary proof format for Isabelle is that of the
Isar proof language, which admits writing proofs in a human-readable
fashion. Needless to say, everything will end up as a primitive internal
proof object eventually, but normally these are getting too large to
inspect them directly. This is why humans would normally stay at the
level of Isabelle/Isar proof documents -- printed in LaTeX/PDF.
Makarius
Robin Green
My apologies. I read the paragraph I quoted too hastily and
misunderstood it! Dr. Watson has informed me that the export of proof
derivations _was_ supported in Isabelle 98 (not Isabelle 99 as I misread
it) - and is covered in his thesis, from which that quotation was taken.
(Any further information not covered in that thesis would of course be
appreciated.)
--
Robin
Robin Green wrote:
> A question about transforming Isabelle proofs into really elementary,
> long-winded form:
<snip>
Sean McLaughlin
>
> 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.
>
> Best,
>
> Sean
>
> On Jan 12, 2006, at 9:33 AM, Robin Green wrote:
>
>> A question about transforming Isabelle proofs into really
>> elementary, long-winded form:
>>
>> 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.)
>>
>> thinking of something like Metamath[1], which is apparently based
>> entirely on simple substitution rules. In other words,
>> emphatically not (non-trivial) tactics.
>>
>> 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?
>>