[isabelle-dev] Attributes and local theories

[Makarius]

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 
surface context.

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 
the context.

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

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


 	Makarius