*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Proof by analogy and proof stability in Isabelle*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Fri, 30 Apr 2010 01:59:28 +0100*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>

On Thu, 2010-04-29 at 14:17 +0200, Tobias Nipkow wrote: > We have to distinguish two applications of proof objects: to speed up > the loading of theories, where they are fine, If I recall correctly, Makarius and Stefan conducted a few experiments some years ago and concluded that checking proof objects was typically not faster than re-playing proof scripts in Isabelle. > 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... Well, being locked into a particular version of Isabelle's proof checker still seems much better than being locked into a particular version of Isabelle (and worse, being locked into a particular system configuration when external provers are used). Of course proof objects are not the answer to life, the universe and everything. Size is one issue; the lack of readability is another. But in terms of stability across Isabelle versions and platforms, proof objects beat proof scripts (and even well-written Isar proofs) by a wide margin. The interface is just a lot simpler. > 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. Proof objects can refer to lemmas, so one isn't forced to freeze the library. Of course changes to the library may cause proof checking to fail then, but at least changes to tactics still won't. Shipping libraries in binary form is actually quite common, isn't it? Maybe we need an equivalent for Isabelle theories. Tjark

**Follow-Ups**:**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Lawrence Paulson

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