Re: [isabelle] Replacing COMP



Am 04.08.2013 19:19, schrieb Florian Haftmann:
> Hi René,
> 
> (the thread is a little but fringed already, I answer at an
> arbitrary point)
> 
> in the next Isabelle release, there will be interpretation within 
> bounded contexts which is maybe helpful in your scenario.
> 
> context fixes … assumes … begin
> 
> …
> 
> interpretation … -- {* + *}
> 
> …
> 
> end -- {* here all facts stemming from + disappear again *}
> 
> This construction appears to me at another powerful means to
> organize abstract specifications and interpretations since it avoid
> the ancient »can bin problem« that you can either interpret a whole
> locale or nothing.
> 
> Would this fit your scenario?  For me this is indeed hard to judge 
> without a look at your theories.

Thanks for the hint (such a thing is good to know). Unfortunately, it
does not fit my usecase without a larger rewrite. And also I'd like to
avoid introducing new locales (I have several dozens here already that
are already too confusing).

I now used one of the proposals of Andreas, namely an unnamed context.
This worked out pretty well as it turned out to not just be a
workaround but a really useful tool here (a large bunch of lemmas with
the same assumption). (Now all that remains to remember is the
existence of this context when looking at the theory again in a later
point in time :))

Thanks to all,
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.