Email Gateway (Aug 19 2022 at 08:25): Email Gateway (Aug 19 2022 at 08:25):From: Tjark Weber <webertj@in.tum.de>
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
Last updated: Apr 18 2024 at 20:16 UTC