Re: [isabelle] Replacing COMP



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.


	Makarius


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