Email Gateway (Sep 28 2023 at 13:22): Email Gateway (Sep 28 2023 at 13:22):From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
When declaring a simproc within a locale with simproc_setup the invocation might fail in case of multiple active interpretations of the locale.
This is illustrated in the attached theory.
The technical reason is that the term net which indexes the simprocs does not take the pattern of the simproc into account for its equality check, but only considers the stamp for the ML function.
In the example given, the first interpretation is inserted into the net, whereas the second one is ignored as it is considered a duplicate.
The simplifier will then reject to apply the simproc to instances of the second interpretation as the pattern of the first interpretation does not match.
The relevant parts of raw_simplifier.ML:
Net.insert_term eq_proc (lhs, proc) procs
fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2;
Regards,
Norbert
Email Gateway (Oct 02 2023 at 15:39):From: Lawrence Paulson <lp15@cam.ac.uk>
Presumably it should be something like
fun eq_proc (Proc {stamp = stamp1, lhs = lhs1, ...}, Proc {stamp = stamp2, lhs = lhs2, ...}) = stamp1 = stamp2 andalso lhs1 aconv lhs2;
You could give that a try and see if it helps. However, the simplifier is Tobias’s baby
Larry
Email Gateway (Oct 02 2023 at 17:25):From: Makarius <makarius@sketis.net>
That part is my responsibility, but I did not look at it yet. I need to
figure out if there is actually something wrong, as usual.
Since we are after a release, and not before a release, there is no
particular need to rush to resolve it.
(I am presently on travel.)
Makarius
Email Gateway (Oct 17 2023 at 10:56):From: Makarius <makarius@sketis.net>
On 28 Sep 2023 at 14:22 +0100, nschirmer@apple.com <nschirmer@apple.com>,
wrote:The relevant parts of raw_simplifier.ML:
Net.insert_term eq_proc (lhs, proc) procs
fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) =
stamp1 = stamp2;
This is not sufficient: the pattern is just an approximation and could be
rather general, and insufficient to distinguish simproc instances.
In the past we actually had an explicit "identifier" for the intended formal
theory of a simproc. It was never used and thus "garbage collected" in
Isabelle/13252110a6fe:
changeset: 62913:13252110a6fe
user: wenzelm
date: Fri Apr 08 20:15:20 2016 +0200
description:
eliminated unused simproc identifier;
This points back at much more ambitious "localized" proof tools from 10 years
earlier, but only recently Norbert has re-opened this game.
I will take closer look to see how we can again put it into proper shape.
(Side-remark: Now that we have pseudo-intelligent machines to produce
insufficient / superficial / wrong answers mechanically, we are free again to
work thoroughly and diligently, based on proper understanding of problems.)
Makarius
Email Gateway (Oct 23 2023 at 12:07):From: Makarius <makarius@sketis.net>
I have now reworked that quite a bit for the next release. The "identifier" is
back, see Isabelle/9d44cc361f19 and
https://isabelle-dev.sketis.net/phame/post/view/74/ml_antiquotation_for_simproc_setup
I now recall the reason why I had "garbage collected" this unused feature in
Isabelle/13252110a6fe: it was hard to generate ML source from the abstract
type (thm list), without the formal context of ML antiquotations.
Side-remark: if you do need this for Isabelle2023, you should get along with
Local_Theory.declaration and Simplifier.make_simproc, to produce a new simproc
for each morphism instance.
Makarius
Email Gateway (Oct 26 2023 at 07:16):From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Thank you. It now works fine for my purposes.
Regards,
Norbert
Last updated: Apr 29 2024 at 04:18 UTC