[isabelle-dev] [isabelle] Local Theory Specifications: Auxiliary Context?

[Florian Haftmann]

Hi Tjark,

> I am trying to implement a rule attribute (i.e., an attribute that
> transforms theorems, such as "simplified"). The transformation expects
> a constant at a specific position in the theorem's proposition, and
> currently fails in some local contexts because it finds an application
> term (of a locally defined variable to local parameters) instead.
> 
> Should I generalize my code to handle such terms explicitly, or is
> there a way to "lambda-drop" the given theorem into a context where the
> application has been folded away?

it depends.

In principal, declarations are supposed to fail silently if the input
does not match their expectations – a tribute you have to pay since in
the presence of arbitrary morphisms there are hardly any properties you
can expected to be invariant under morphism applications.

For more complex mechanisms, it can be an option to implement a
dedicated command (e.g.
http://isabelle.in.tum.de/repos/isabelle/file/f781bbe0d91b/src/HOL/Tools/enriched_type.ML)
which checks the user input in the auxiliary context, does some
defs/notes and a declaration finally which stores the morphed data for
later usage in what context ever.

Your job of identifying constant or »quasi-constants« in terms seems to
be similar to Lukas' predicate compiler analysis, and he might give
further insights.  AFAIK the predicate compiler only relies on logical
constants, but maybe mainly due to the fact that its result makes only
sense on the »global« level since it is handed over to the code generator.

> I have read Haftmann/Wenzel "Local Theory Specifications in
> Isabelle/Isar" as well as Chapter 8 of the Implementation Manual and
> suspect the "auxiliary context" may be what I am looking for, but I am
> not sure how to obtain and use it, given the (generic) context that is
> passed to the attribute. If I am on the right track at all, I would
> appreciate pointers to the relevant ML functions.

The auxiliary context passed away after a user-space package has done
its defs/notes sequence.  The foundations remains, and any target
contexts populated by the underlying target.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120830/5255cd8f/attachment-0001.asc>