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 https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-March/msg00028.html

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.

Yours,
    Thomas.






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