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



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






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