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

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.


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
> ( 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

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