*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Proof by analogy and proof stability in Isabelle*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 28 Apr 2010 13:29:32 -0700*Cc*: isabelle-users at cl.cam.ac.uk, grechukbogdan <grechukbogdan at yandex.ru>*In-reply-to*: <4BD897BF.3010405@in.tum.de>*References*: <6031272389962@web71.yandex.ru> <k2mcc2478ab1004280945gb510d767maf21c86aad9e0ab5@mail.gmail.com> <4BD897BF.3010405@in.tum.de>*Sender*: huffman.brian.c at gmail.com

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

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

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

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

- 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