Re: [isabelle] using simproc

On Mon, 22 Feb 2016, Viorel Preoteasa wrote:

I have created a simproc using Simplifier.make_simproc. If I use it in Simplifier.rewrite, then it works as expected. However, if I use it within the context of Outer_Syntax.local_theory' it does not simplify the term.

When such things happen, there is usually something wrong with the context. We have spent the last 10 years "localizing" virtually all Isabelle programming interfaces, to make everything work uniformly according to standard context disciplines. These are documented in the "implementation" manual.

In Isabelle 2015, I created the simproc using simproc_global_i and it was working as I expected.

This indicates that old code has been updated too quickly and superficially. Changes in Isabelle mean that old and conceptually outdated forms are replaced by new and conceptually different forms.

The relevant bit of documentation is in Isabelle2016/NEWS:

* Simproc programming interfaces have been simplified:
Simplifier.make_simproc and Simplifier.define_simproc supersede various
forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that
term patterns for the left-hand sides are specified with implicitly
fixed variables, like top-level theorem statements. INCOMPATIBILITY.

The provided example is a bit odd in creating the simproc on the spot in a certain context just before use. This can be done theoretically, but needs extra attention about the scopes of variables. E.g. it is difficult to predict what a blue "x" will be in an arbitrary application context. The NEWS entry hints at "implicitly fixed variables, like top-level theorem statements". Apparently, the "x" does not come out as arbitrary in this situation.

I did not try to figure out why the "x" is treated like that, because counting on such behaviour in the middle of a more complex definition is fragile context discipline.

Instead, the simproc should be defined once beforehand, e.g. via simproc_setup, and then used via the @{simproc} antiquotation.


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