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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
