[isabelle] Local Theory Specifications: Auxiliary Context?



Hi,

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?

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.

Many thanks in advance,
Tjark







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.