Email Gateway (Aug 18 2022 at 19:20): Email Gateway (Aug 18 2022 at 19:20):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi!
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. Although I invested a non-trivial
time to try to figure out how to go from Context.generic to local_theory
and back, I wasn't successful. Can anybody please help me and tell me
how to implement the "boilerplate" function bar in
"Thm.declaration_attribute bar" such that bar is implemented in terms of
the function foo?
Thanks.
Ondrej
Email Gateway (Aug 18 2022 at 19:20):From: Lukas Bulwahn <bulwahn@in.tum.de>
The function Context.mapping is probably what you want.
Lukas
Email Gateway (Aug 18 2022 at 19:20):From: Makarius <makarius@sketis.net>
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.
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.
Makarius
Email Gateway (Aug 18 2022 at 19:20):From: Ondřej Kunčar <kuncar@in.tum.de>
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 Local_Theory.note.
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. 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
Email Gateway (Aug 18 2022 at 19:21):From: Makarius <makarius@sketis.net>
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
Local_Theory.note.
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
trickery.
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
examples?
If you show your concrete sources, I can comment on the approach
concretely.
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
dense.
Makarius
Email Gateway (Aug 18 2022 at 19:21):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
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.
Last updated: Apr 24 2024 at 08:20 UTC