Re: [isabelle] Proof by analogy and proof stability in Isabelle



Joe Hurd's OpenTheory project may be relevant here:

  http://www.gilith.com/research/opentheory

It is designed to provide a standard for sharing theory developments across higher order logic theorem provers. It doesn't support Isabelle's type classes, however Alexander Krauss' and Andreas Schropp's work on translating away typeclasses (Sections 5.1 and 5.2 of the online paper below) might be used to overcome this:

  http://www4.in.tum.de/~krauss/holzf

-john



On Apr 29, 2010, at 5:17 AM, Tobias Nipkow wrote:

We have to distinguish two applications of proof objects: to speed up
the loading of theories, where they are fine, and as a means of
producing stable proofs, where I maintain they are problematic (and I am
not aware of any system that supports it). If you want to protect your
proof against a changing basis, you have to include the whole basis into
your proof object. It is not infeasible, but it means you are locked
into this one version of your proofs. And if one day the format for
primitive proofs changes... It is like packaging every library your
program needs with that program (in binary) and freezing the program at that point. It may have its uses, but it is not recommended as a general
program development method.

Tobias


Tjark Weber wrote:
On Thu, 2010-04-29 at 07:18 +0200, Tobias Nipkow wrote:
Such an approach is feasible only in principle. You could write all the
proof objects out to a file, expanding all proofs of lemmas used.
Isabelle's proof terms even have a concrete syntax for that. This would give you a stable but gigantic proof. The requirements in terms of time and space would make it impossible to process these proofs effectively.
And you would have lost the readable version.

I briefly discuss an implementation of this idea in Section 5.5 of my
dissertation
(http://www.cl.cam.ac.uk/~tw333/publications/weber08satbased.html). My
motivation at the time was to achieve stability across different
Isabelle installations in the presence of external provers (which might
be available on one machine, but not on another).

In theory, proof objects could become gigantic, but for Isabelle/ HOL the
approach seemed to work reasonably well.  I don't think there is
sufficient experimental data to dismiss it as infeasible in practice.

Of course, proofs of lemmas must not be expanded inline, but referenced
(as suggested by Peter).  This is already supported by Stefan's proof
objects.

Tjark




Attachment: smime.p7s
Description: S/MIME cryptographic signature



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