Re: [isabelle] Proof by analogy and proof stability in Isabelle

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?


Brian Huffman schrieb:
> On Wed, Apr 28, 2010 at 1:17 PM, Tobias Nipkow <nipkow at> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.