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 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


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