Re: [isabelle] Replacing COMP



Am 31.07.2013 14:35, schrieb Makarius:
> On Wed, 31 Jul 2013, René Neumann wrote:
> 
>> Am 31.07.2013 14:15, schrieb Makarius:
>>> Even after reading the answers by Andreas, I don't understand the
>>> purpose of lift_foo.
>>>
>>> Can you explain the application behind all this?
>>
>> I have a ton of theorems about some function foo. Now I have some
>> refinement foo_impl, where most of the properties of foo also hold.
>>
>> For usability reasons I'd like to lift the appropriate theorems from foo
>> to foo_impl (so I don't have to do it everytime I need a lemma about
>> foo_impl), but I'd also like to avoid duplication (i.e. stating the
>> properties over and over again, as it then becomes quite tedious to do
>> smaller refactoring).
> 
> In this generic way, it sounds like an application of locale +
> interpretation.

We already have to deal with way too much locales here, adding one more
layer would only complicate things.

So for the moment, I'll stick with proving it explicitly.

Thanks for the hints though (also @Andreas -- unfortunately, I couldn't
use on of those proposals to make it 'feel right', it always felt kind
of hackish).

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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