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