Re: [isabelle] declaration attribute



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





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