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



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





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