Email Gateway (Nov 28 2025 at 14:23): Email Gateway (Nov 28 2025 at 14:23):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
I made a little search. There are 115 occurrences of "simproc del: defined_all" in the distribution and AFP. I'm not sure what this thing does but perhaps it needs urgent attention.
Larry
On 28 Nov 2025, at 11:00, Manuel Eberl <manuel@pruvisto.org> wrote:
This doesn't look like intended behaviour to me. I tracked the problem to the "defined_all" simproc, specifically to the ML function "Quantifier1.rearrange_all". If you remove that simproc from the simpset, the exception does not occur.
Perhaps this helps somebody who knows that part of the code understand what is going on.
Email Gateway (Nov 28 2025 at 14:48):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
I think the exception is coming from a low-level function called yield_singleton, which is called by the version of prove_conv in Provers/quantifier1.ML. Several of the simprocs there contain the snippet
SOME (prove_conv ctxt …)
and each of these could raise exception List.Empty, which would not be caught and would blow up at the top level.
So if it is not too late, I propose adding an exception handler to each
handle List.Empty => NONE.
Larry
On 28 Nov 2025, at 11:00, Manuel Eberl <manuel@pruvisto.org> wrote:
This doesn't look like intended behaviour to me. I tracked the problem to the "defined_all" simproc, specifically to the ML function "Quantifier1.rearrange_all". If you remove that simproc from the simpset, the exception does not occur.
Perhaps this helps somebody who knows that part of the code understand what is going on.
Email Gateway (Nov 28 2025 at 15:36):From: Manuel Eberl <manuel@pruvisto.org>
Unless I am very mistaken, it's fairly clear that the superficial issue
is that Quantifier1.rearrange_all sets up a goal and then tries to prove
it with the tactic "prove_one_point_All_tac", which fails. The code is
written in such a way that this is expected to never fail. But it does.
As for the root issue causing this failure, looked at the code in some
detail and strongly suspect that the tactic relies on being able to
atomize the entire goal, i.e. convert any meta-logical operators or
quantifiers into their HOL equivalents. Once you have something in your
goal that cannot be atomised (like your "PROP P"), this of course fails.
Some evidence that this is the case: You can trigger the same behaviour
by putting a "PROP U" in the goal:
lemma ‹⋀x. (x = y) ∧ z ⟹ PROP U›
apply simp
My impression is that the simplifier setup for the HOL session is simply
somewhat brittle in the presence of things that cannot be atomised.
Whether that is intended or not I cannot say. Given the prevalence of
the "simproc del" invocations in the distribution and AFP, it seems that
it is a known issue and that it does cause problems in real-life
situations. So I would say it is at the very least not ideal and one
should do something about it.
The easiest and best way would probably be to simply declare goals that
cannot be atomised as out of scope for the simproc and make it fail
gracefully in such cases rather than have such a spectacular crash (as I
think Larry suggested). On one hand, I for one don't see how this could
introduce any problems (but I am aware that saying this is tempting
fate). On the other hand, I don't think it is an urgent issue and can
probably wait until after the release.
Incidentally, Florian Haftmann touched this code a few years ago, so
perhaps he can provide some further insights.
Cheers,
Manuel
On 28/11/2025 16:02, Becker, Hanno wrote:
Thank you, all!
Larry, can you explain how this relates to the presence of a
PROP Pterm in the goal? Is the simproc somewhere expecting to find all premises of the formHOL.Trueprop ...?Best,
HannoOn 28/11/2025, 14:51, "Lawrence Paulson" <lp15@cam.ac.uk <mailto:lp15@cam.ac.uk>> wrote:
CAUTION: This email originated from outside of the organization. Do not click links or open attachments unless you can confirm the sender and know the content is safe.
I think the exception is coming from a low-level function called yield_singleton, which is called by the version of prove_conv in Provers/quantifier1.ML. Several of the simprocs there contain the snippet
SOME (prove_conv ctxt …)
and each of these could raise exception List.Empty, which would not be caught and would blow up at the top level.
So if it is not too late, I propose adding an exception handler to each
handle List.Empty => NONE.
Larry
On 28 Nov 2025, at 11:00, Manuel Eberl <manuel@pruvisto.org <mailto:manuel@pruvisto.org>> wrote:
This doesn't look like intended behaviour to me. I tracked the problem to the "defined_all" simproc, specifically to the ML function "Quantifier1.rearrange_all". If you remove that simproc from the simpset, the exception does not occur.
Perhaps this helps somebody who knows that part of the code understand what is going on.
Email Gateway (Nov 28 2025 at 15:36):From: Makarius <makarius@sketis.net>
On 28/11/2025 15:22, Lawrence Paulson via isabelle-dev wrote:
I made a little search. There are 115 occurrences of "simproc del: defined_all" in the distribution and AFP. I'm not sure what this thing does but perhaps it needs urgent attention.
It has been there for 5 years already, so nothing is urgent here in terms of
the Isabelle2025-1 release.
A proper stable release requires some discipline.
Makarius
Email Gateway (Nov 28 2025 at 15:47):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
I tested a patch a little bit. If we catch the exception, the simplifier still fails (as one would expect). The warning "cannot atomize goal" no longer appears. For some reason, “apply simp?” still fails.
I investigated one theory where defined_all is suppressed (Auth/Guard/P1). From what I can tell, the reason was to keep the proof working as before and not that it was generating some sort of error.
Larry
On 28 Nov 2025, at 15:36, Manuel Eberl <manuel@pruvisto.org> wrote:
The easiest and best way would probably be to simply declare goals that cannot be atomised as out of scope for the simproc and make it fail gracefully in such cases rather than have such a spectacular crash (as I think Larry suggested). On one hand, I for one don't see how this could introduce any problems (but I am aware that saying this is tempting fate). On the other hand, I don't think it is an urgent issue and can probably wait until after the release.
Email Gateway (Nov 28 2025 at 20:52):From: Makarius <makarius@sketis.net>
On 28/11/2025 16:47, Lawrence Paulson via isabelle-dev wrote:
I tested a patch a little bit. If we catch the exception, the simplifier still fails (as one would expect). The warning "cannot atomize goal" no longer appears. For some reason, “apply simp?” still fails.
Please, no adhoc patches or "big fixes", which are usually wrong. I've spent
so many decades sorting out problems introduced by presumed "fixes".
Step 0 is to use induction over the history of the sources (using "hg
bisect"). It reveals this notable point:
The first bad revision is:
changeset: 71989:bad75618fb82
user: haftmann
date: Thu Jul 02 12:10:58 2020 +0000
summary: extraction of equations x = t from premises beneath meta-all
This change is not immediately obvious, it belongs to a greater context.
Step 1 is to show this to the author, Florian Haftmann, in order to amend,
finish, improve on it.
(It is certainly not relevant for the Isabelle2025-1 release, as a
non-regression from previous releases.)
Makarius
Email Gateway (Nov 28 2025 at 20:59):From: Makarius <makarius@sketis.net>
On 28/11/2025 21:51, Makarius wrote:
The first bad revision is:
changeset: 71989:bad75618fb82
user: haftmann
date: Thu Jul 02 12:10:58 2020 +0000
summary: extraction of equations x = t from premises beneath meta-all
See also this NEWS entry from Isabelle2021:
Simproc "defined_all" and rewrite rule "subst_all" perform more
aggressive substitution with variables from assumptions.
INCOMPATIBILITY, consider repairing proofs locally like this:
supply subst_all [simp del] [[simproc del: defined_all]]
Which means that in these terms, the example by Hanno is "broken".
It is up to discussion, together with Florian, if this is good or bad. But we
can definitely close the case as something urgent to be "fixed".
Makarius
Email Gateway (Dec 04 2025 at 10:47):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi all,
Am 28.11.25 um 21:59 schrieb Makarius:
On 28/11/2025 21:51, Makarius wrote:
The first bad revision is:
changeset: 71989:bad75618fb82
user: haftmann
date: Thu Jul 02 12:10:58 2020 +0000
summary: extraction of equations x = t from premises beneath meta-allSee also this NEWS entry from Isabelle2021:
Am 28.11.25 um 16:36 schrieb Manuel Eberl:
As for the root issue causing this failure, looked at the code in some
detail and strongly suspect that the tactic relies on being able to
atomize the entire goal, i.e. convert any meta-logical operators or
quantifiers into their HOL equivalents. Once you have something in your
goal that cannot be atomised (like your "PROP P"), this of course fails.Some evidence that this is the case: You can trigger the same behaviour
by putting a "PROP U" in the goal:lemma ‹⋀x. (x = y) ∧ z ⟹ PROP U›
apply simp
Thanks for investigating it.
As far as I remember, this was a suggestion by Tobias to generalize a
mechanism from ∀ to ⋀. For some reason ever I derived
prove_one_point_all_tac from prove_one_point_All_tac using atomization,
but as the example shows, this has been misleading.
I’ll investigate this (maybe not in this year) and see whether the
atomization can be dropped or whether at least the simproc can fail
gracefully then.
Am 28.11.25 um 15:22 schrieb Lawrence Paulson via isabelle-dev:
I made a little search. There are 115 occurrences of "simproc del:
defined_all" in the distribution and AFP. I'm not sure what this thing
does but perhaps it needs urgent attention.
These sporadic simproc del: occur in apply-style proofs and have been
inserted to avoid refactoring them; they are unconnected to the
implementation problem (it would be extremely strange if I had ignored
the problem if I had encountered it while adjusting proofs).
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: Dec 10 2025 at 12:50 UTC