<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
<title></title>
</head>
<body text="#000000" bgcolor="#ffffff">
On 11/13/2011 05:16 PM, Makarius wrote:
<blockquote
cite="mid:alpine.LNX.1.10.1111131702560.22075@atbroy100.informatik.tu-muenchen.de"
type="cite">On Thu, 10 Nov 2011, Andreas Schropp wrote:
<br>
<blockquote type="cite">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?
<br>
</blockquote>
<br>
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'.<br>
</blockquote>
<br>
Ok.<br>
<br>
<blockquote
cite="mid:alpine.LNX.1.10.1111131702560.22075@atbroy100.informatik.tu-muenchen.de"
type="cite"><br>
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.
<br>
<br>
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.<br>
</blockquote>
<br>
I guess you are referring to<br>
<blockquote>
<div style="font-family: monospace;" class="parity0">
<pre><a class="linenr"
href="http://isabelle.in.tum.de/repos/isabelle/file/5c0444d2abfe/src/Pure/Isar/named_target.ML#l61"
id="l61"> 61</a> locale_<span highlight="Search">declaration</span> target syntax decl
</pre>
</div>
<div style="font-family: monospace;" class="parity1">
<pre><a class="linenr"
href="http://isabelle.in.tum.de/repos/isabelle/file/5c0444d2abfe/src/Pure/Isar/named_target.ML#l62"
id="l62"> 62</a> #> pervasive ? Generic_Target.theory_<span
highlight="Search">declaration</span> decl
</pre>
</div>
<div style="font-family: monospace;" class="parity0">
<pre><a class="linenr"
href="http://isabelle.in.tum.de/repos/isabelle/file/5c0444d2abfe/src/Pure/Isar/named_target.ML#l63"
id="l63"> 63</a> #> not pervasive ? Context.proof_map (Morphism.form decl);
</pre>
</div>
</blockquote>
in Named_Target.target_declaration, which now includes the
non-pervasive case.<br>
<br>
<br>
<blockquote
cite="mid:alpine.LNX.1.10.1111131702560.22075@atbroy100.informatik.tu-muenchen.de"
type="cite"><br>
<blockquote type="cite">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?
<br>
</blockquote>
<br>
Local_Theory.target in Isabelle/11d9c2768729 has explicit option
"pervasive" to say if it should go into the background theory. </blockquote>
<br>
Hmm, no:<br>
<a class="moz-txt-link-freetext" href="http://isabelle.in.tum.de/repos/isabelle/file/11d9c2768729/src/Pure/Isar/local_theory.ML">http://isabelle.in.tum.de/repos/isabelle/file/11d9c2768729/src/Pure/Isar/local_theory.ML</a><br>
I guess you mean Local_Theory.declaration.<br>
<br>
<blockquote
cite="mid:alpine.LNX.1.10.1111131702560.22075@atbroy100.informatik.tu-muenchen.de"
type="cite">Anyway, these are just some generalities. </blockquote>
<br>
Yes and I appreciate them. ^^<br>
<br>
Some more:<br>
the idea of a non-pervasive declaration (with the new semantics) is
that the resulting<br>
context modifications are registered for the target (if necessary, i.e.
in the case of locales)<br>
and they are also applied to the auxilliary context (which is not
shared between applications<br>
of different morphisms and goes out of scope with the target)?<br>
<br>
I guess this is what I need then.<br>
BTW: this cannot easily be achieved with the old semantics<br>
(which don't modify the aux ctxt), right?<br>
<br>
<br>
<br>
<blockquote
cite="mid:alpine.LNX.1.10.1111131702560.22075@atbroy100.informatik.tu-muenchen.de"
type="cite">What is your concrete application?
<br>
</blockquote>
<br>
Not very concrete at all:<br>
I am animating a fact-accumulation scheme based on<br>
rules of a certain format. ^^<br>
This might be understood as: generalizing morphisms to<br>
applications of user-specified propagation rules (instead of mostly<br>
instantiations and discharges as of now), but outside of the scope of<br>
locale management and under explicit user control.<br>
A more grandiose way to look at it is this:<br>
user-programmable theory extensions.<br>
<br>
And the application of this on the other hand is to transform outcomes<br>
of locale instantiations (particularly locales parameterized<br>
on multi-sorted signatures) to more natural theories.<br>
This makes use of an isomorphic transfer principle<br>
to map certain well-behaved closed sets (which I like to call simple<br>
soft types) to correspondingly typedef'd HOL type constructors.<br>
<br>
<br>
Cheers,<br>
Andy<br>
<br>
</body>
</html>