*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Proof by analogy and proof stability in Isabelle*From*: John Matthews <matthews at galois.com>*Date*: Thu, 29 Apr 2010 09:53:13 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Joe Hurd <joe at galois.com>*In-reply-to*: <4BD978ED.2000106@in.tum.de>*References*: <6031272389962@web71.yandex.ru> <4BD91699.8020401@in.tum.de> <1272538820.2300.49.camel@weber> <4BD978ED.2000106@in.tum.de>

Joe Hurd's OpenTheory project may be relevant here: http://www.gilith.com/research/opentheory

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 ofproducing stable proofs, where I maintain they are problematic (andI amnot aware of any system that supports it). If you want to protect yourproof against a changing basis, you have to include the whole basisintoyour 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 yourprogram needs with that program (in binary) and freezing the programatthat point. It may have its uses, but it is not recommended as ageneralprogram 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 writeall theproof objects out to a file, expanding all proofs of lemmas used.Isabelle's proof terms even have a concrete syntax for that. Thiswouldgive you a stable but gigantic proof. The requirements in terms oftimeand space would make it impossible to process these proofseffectively.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).Mymotivation at the time was to achieve stability across differentIsabelle installations in the presence of external provers (whichmightbe available on one machine, but not on another).In theory, proof objects could become gigantic, but for Isabelle/HOL theapproach 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, butreferenced(as suggested by Peter). This is already supported by Stefan's proof objects. Tjark

**Attachment:
smime.p7s**

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

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

- 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