Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] using simproc

Email Gateway (Aug 22 2022 at 12:42):

From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hello,

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.

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

Attached is a theory that shows this behavior.
At the end there is "thm tt_simp" that display:

tt = MyDef 5

However if the simproc would be applied, then the
result should be:

tt = 6

Best regards,

Viorel Preoteasa
simproc_test.thy

Email Gateway (Aug 22 2022 at 12:42):

From: Makarius <makarius@sketis.net>
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.

Makarius

Email Gateway (Aug 22 2022 at 12:42):

From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
This solved my problem. Thank you.

Viorel

Last updated: Apr 20 2024 at 01:05 UTC