Re: [isabelle] Replacing COMP



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).

So in the end, it is more of academic use (hah!) and could easily be
solved by copy'n'paste,
but I hate copying boilerplate.

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