*To*: Tjark Weber <webertj at in.tum.de>*Subject*: Re: [isabelle] Proof by analogy and proof stability in Isabelle*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 29 Apr 2010 14:17:49 +0200*Cc*: isabelle-users at cl.cam.ac.uk, grechukbogdan <grechukbogdan at yandex.ru>*In-reply-to*: <1272538820.2300.49.camel@weber>*References*: <6031272389962@web71.yandex.ru> <4BD91699.8020401@in.tum.de> <1272538820.2300.49.camel@weber>*User-agent*: Thunderbird 2.0.0.24 (X11/20100302)

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 >

**Follow-Ups**:**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*steven at obua.de

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*John Matthews

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tjark Weber

**References**:**[isabelle] Proof by analogy and proof stability in Isabelle***From:*grechukbogdan

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tobias Nipkow

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tjark Weber

- Previous by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Next by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Previous by Thread: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Next by Thread: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Cl-isabelle-users April 2010 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