[isabelle-dev] Attributes and local theories
makarius at sketis.net
Sun Nov 13 17:16:45 CET 2011
On Thu, 10 Nov 2011, Andreas Schropp wrote:
> it has come to my attention that attributes are called with a theory, a
> proof context and a local theory in this succession. Is this
> transforming the input lthy onion from inside out?
I prefer to call it sandwich -- I don't like onions so much :-)
Details of when declarations are actually materialized and applied to some
context are up to local theory target implementations, and other
mechanisms like interpretation. But yes, things are usually done from
bottom to top, inside out. (Roughly in "foundational order".)
> The implementation manual states that I have to treat all of them
> uniformly. This means that the attribute transformation on a lthy would
> not result in an update of the target context but of the auxilliary
> context instead. Is this correct and is the target guaranteed to be
> transformed in the same way beforehand?
Yes. The update function provided by the user of local theory
declarations should operate directly on the surface context as given,
either Context.Theory or Context.Proof. You cannot even count that it
will be again a local theory in the application, e.g. consider
'interpretation' or 'interpret'.
The target is usually updated before the auxiliary context, but this
should normally not matter, since the lookup should use the very same
Note that in official Isabelle2011-1 there is still some confusion here in
Local_Theory.declaration, because it would omit the aux. context. I have
clarified that after the release, with some years delay as usual.
> Also, does this mean we store the information resulting
> from attributes 3 times, namely in theories, contexts and
> local theories, potentially without any sharing?
Normally there is little to share, because the 3 values are different.
The morphism that is applied to the data first will change it according to
Moreover, in practice it is not really 3 times, since regular declarations
are not "pervasive", i.e. not applied to the background theory, and the
auxiliary context does not persist in the long term -- it merely serves
for "drafting" specifications locally.
> If in the process of a local theory transformation I want to store
> information to be looked up later, but not escaping the scope of the
> target, where should I store it? In the auxilliary context or the target
Local_Theory.target in Isabelle/11d9c2768729 has explicit option
"pervasive" to say if it should go into the background theory. Moreover,
you have can often get clues from the result after applying the morphism
if you still want to make the update. E.g. Proof_Context.target_notation
will give up after the term to be annotated has changed substantially.
Anyway, these are just some generalities. What is your concrete
More information about the isabelle-dev