*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Proof by analogy and proof stability in Isabelle*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 29 Apr 2010 06:54:02 +0200*Cc*: isabelle-users at cl.cam.ac.uk, grechukbogdan <grechukbogdan at yandex.ru>*In-reply-to*: <n2hcc2478ab1004281329pa87e8b54r3793062ee133f464@mail.gmail.com>*References*: <6031272389962@web71.yandex.ru> <k2mcc2478ab1004280945gb510d767maf21c86aad9e0ab5@mail.gmail.com> <4BD897BF.3010405@in.tum.de> <n2hcc2478ab1004281329pa87e8b54r3793062ee133f464@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

Since this was not just a general hypothetical question, but a very concrete one, and since Bogdan is in contact with the author of the (ported) library, I was suggesting that they might generalize that part of the library. @Bogdan: Out of intererst: how does John Harrison deal with this duplication in the original library? Tobias Brian Huffman schrieb: > On Wed, Apr 28, 2010 at 1:17 PM, Tobias Nipkow <nipkow at in.tum.de> wrote: >> Proof by analogy: I wondered if locales would have helped to generalize >> the dim/aff_dim lemmas, obtaining both by an interpretation? >> >> Tobias > > Maybe they could have, but that kind of misses the point: Writing > libraries using locales means that the library writer needs to know in > advance exactly how it might be generalized in the future. The problem > we are trying to solve is when person A writes a library, and person B > wants to re-use the proofs in a more general setting - without > modifying the original library, or cutting-and-pasting the proofs. > > I might summarize it this way: Locale interpretation transforms a > generic theory into a concrete one. What we're looking for is a way to > transform a *concrete* theory into a *different* concrete one (or a > new generic one, as the case may be). > > - Brian

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

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Brian Huffman

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

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Brian Huffman

- 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