Re: [isabelle] declaration attribute

On 22/03/12 05:37, Ondřej Kunčar wrote:
OK, I got from your explanation that it's not possible. So now I defined a command instead of an attribute and it works. But to be honest, I don't understand why it is not possible. Your explanation seems to be too much abstract (or dense) to me. Could you please explain it in a more detailed way or maybe use some concrete examples? I am not too much familiar with this abstract infrastructure of Isabelle. Thanks. Ondrej

Makarius may need several rounds of refinement to answer this question in a concrete way. Let me try to speed up the process.

I think that what is confusing you is that Context.generic provides a second layer of generic operation over theories, locales and structured proofs, when it looks that can already be done with local_theory.

Things are more complex than they seem. If one is inside a structured proof inside a locale inside a theory, all three context objects exist at once, in an arrangement that has been described as the Haftmann/Wenzel sandwich. Some operations are run on the topmost layer and then filter down as the proof/locale closes and merges. Some operations, such as attributes, get run simultaneously on multiple layers. Attributes may also be run when locales are interpreted and when they are reopened, though I think the details of this have changed recently. This was discussed in the past on this list

This is what Makarius is getting at when he says attributes should try to run as generally as possible: they may need to run in all kinds of circumstances and failure may derail later operations.

As for local_theory, it looks like you can define all your functionality as a local_theory transformer, and run it on theories by using Theory_Target.init and Local_Theory.exit_global. If I understand correctly, this should not be expected to work for all kinds of changes, though it seems to work for adding notes (theorem names) and constants.

In conclusion: the obvious thing to do in an attribute is adjust data with the put/map operation of any data store derived from Generic_Data. This may in fact be what you want to do. You can also transform the theorem locally. Anything else requires a pretty deep understanding of what is going on.

This is just my understanding, I haven't attempted to read much of the documentation. I look forward to people correcting what I got wrong.


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