Re: [isabelle] declaration attribute
On Wed, 21 Mar 2012, Ondřej Kunčar wrote:
On 03/21/2012 09:55 AM, Makarius wrote:
On Tue, 20 Mar 2012, Ondřej Kunčar wrote:
I want to define a declaration attribute which works with the given
theorem. I've already implemented this operation in the function foo
:: thm -> local_theory -> local_theory. Now I want to define a
attribute by the function Thm.declaration_attribute :: (thm ->
Context.generic -> Context.generic) -> Thm.attribute.
What is your local_theory -> local_theory operation actually doing? If
it does genuine specifications (like Local_Theory.define) than it cannot
be a "declaration" at the same time.
It changes theory data by Local_Theory.declaration and adds an attribute by
This sounds like you are doing plain declarations of context data, but it
happens to be wrapped up as local_theory specification elements. By using
the declaration functions directly, you should be able to present the
composition as attribute. Normally, the Isabelle components in question
should export declarations functions along with the attributes, if not one
can always recover the declaration part of an attribute by a bit of
It depends on the application how things are best presented to the user:
Attributes are more flexible, because they can be used in many situations
(specifications, proofs, locales, classes atc.), but sometimes it is more
appropriate to wrap things up as standalone definitional package (like
'function' or 'inductive').
A declaration is some kind of generic data update on a generic context.
It needs to work in many situations, like the original local_theory
context of the user, its background theory, any other application
context after interpretation, and more.
This is also the reason, why such declarations need to fail gracefully,
if they don't like their argument, and not prevent other declarations
from succeeding that happened to be pulled-in by the same locale
interpretation, for example.
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.
I see a tendency of "negation by failure" reasoning here. A certain
attempt did not work, but many more possiblities were not even considered
yet. Usually the art is to find the one "canonical way" in a jungle of
dead ends. How much energy is invested on that depends on the
application, i.e. if it is just some experiment or something exposed to
many users eventually.
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
If you show your concrete sources, I can comment on the approach
Further general explanations are in the Isabelle/Isar Implementation
manual. Every time I revisit it to continue working on the text, I am
surprised how much is mentioned there already, although it is definitely
This archive was generated by a fusion of
Pipermail (Mailman edition) and