[isabelle-dev] Attributes and local theories

[Andreas Schropp]

On 11/13/2011 05:16 PM, Makarius wrote:
> On Thu, 10 Nov 2011, Andreas Schropp wrote:
>> 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'.

Ok.

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

I guess you are referring to

         61  <http://isabelle.in.tum.de/repos/isabelle/file/5c0444d2abfe/src/Pure/Isar/named_target.ML#l61>      locale_declaration  target syntax decl
       

         62  <http://isabelle.in.tum.de/repos/isabelle/file/5c0444d2abfe/src/Pure/Isar/named_target.ML#l62>      #>  pervasive ? Generic_Target.theory_declaration  decl
       

         63  <http://isabelle.in.tum.de/repos/isabelle/file/5c0444d2abfe/src/Pure/Isar/named_target.ML#l63>      #>  not pervasive ? Context.proof_map (Morphism.form decl);
       

in Named_Target.target_declaration, which now includes the non-pervasive 
case.


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

Hmm, no:
    
http://isabelle.in.tum.de/repos/isabelle/file/11d9c2768729/src/Pure/Isar/local_theory.ML
I guess you mean Local_Theory.declaration.

> Anyway, these are just some generalities. 

Yes and I appreciate them. ^^

Some more:
   the idea of a non-pervasive declaration (with the new semantics) is 
that the resulting
context modifications are registered for the target (if necessary, i.e. 
in the case of locales)
and they are also applied to the auxilliary context (which is not shared 
between applications
of different morphisms and goes out of scope with the target)?

I guess this is what I need then.
BTW: this cannot easily be achieved with the old semantics
(which don't modify the aux ctxt), right?



> What is your concrete application?

Not very concrete at all:
   I am animating a fact-accumulation scheme based on
rules of a certain format. ^^
This might be understood as: generalizing morphisms to
applications of user-specified propagation rules (instead of mostly
instantiations and discharges as of now), but outside of the scope of
locale management and under explicit user control.
A more grandiose way to look at it is this:
   user-programmable theory extensions.

And the application of this on the other hand is to transform outcomes
of locale instantiations (particularly locales parameterized
on multi-sorted signatures) to more natural theories.
This makes use of an isomorphic transfer principle
to map certain well-behaved closed sets (which I like to call simple
soft types) to correspondingly typedef'd HOL type constructors.


Cheers,
   Andy

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20111114/a4c3c0df/attachment-0002.html>