Email Gateway (Jul 01 2026 at 12:51): Email Gateway (Jul 01 2026 at 12:51):From: Simon Foster <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle Developers,
I am getting an unexpected loop from the Isabelle simplifier. Consider the
following minimal theory:
theory Simplifier_Loop
imports Main
begin
consts r :: "int ⇒ int"
consts i :: "int ⇒ int ⇒ int"
lemma "- (2 * (i (r x)) y) ≤ (z * 2)"
apply simp (* Loops and then throws an Interrupt_Breakdown error *)
oops
We have two uninterpreted constants, r and i, over the integers. The lemma
should simplify to "- i (r x) y ≤ z", but the simplifier loops and
eventually throws an error. If we change the goal to "- (2 * (i (r x)) y) ≤
(2 * z)", the behaviour is as expected. The behaviour recurs for any choice
of numeral >1 instead of 2 (e.g. 3).
Setting [[simp_trace]] provides no trace of invoked simplification laws. If
we use [[simp_debug]], we get a trace, and it appears the loop is called by
the combination of mult.commute, minus_mult_commute, and
numeral_times_minus_swap. However, deleting these from the simplified (simp
del:) has no effect, and they are still shown in the debug trace.
This minimal example is not synthetic, but is an instance of a proof
obligation I produced during a verification (i is the inner product, and r
is a function for performing a 90 degree turn). It works regardless of the
numeric type that is chosen, and the choice of definitions for r and i. It
occurs in both Isabelle2025 and Isabelle2025-2.
Can anyone help to shed light on this situation? How can I prevent the
simplifier from looping?
Thank you for your work on Isabelle.
Regards,
Simon.
Email Gateway (Jul 01 2026 at 16:17):From: Manuel Eberl <manuel@pruvisto.org>
The fact that the simp trace is empty indicates that this is probably a
simproc that doesn't terminate.
I played around a little bit, disabling any simproc that might apply to
your problem, and the culprit seems to be
"ring_le_cancel_numeral_factor". If you do a "declare [[simproc del:
ring_le_cancel_numeral_factor ]]" then your example does not loop.
The suspicion is confirmed by the fact that the following also loops:
ML_val ‹
Numeral_Simprocs.le_cancel_numeral_factor @{context} @{cterm "- (2 *
(s (r x)) y) ≤ (z * 2)"}
›
I haven't investigated the code to figure out where exactly the problem
might lie. Hopefully somebody who knows that code base will take a look.
If not, maybe I will at some point.
Manuel
On 7/1/26 14:50, Simon Foster (via cl-isabelle-users Mailing List) wrote:
theory Simplifier_Loop
imports Main
beginconsts r :: "int ⇒ int"
consts i :: "int ⇒ int ⇒ int"lemma "- (2 * (i (r x)) y) ≤ (z * 2)"
apply simp (* Loops and then throws an Interrupt_Breakdown error *)
oops
Email Gateway (Jul 01 2026 at 16:56):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks for looking into this. I suspect that Larry and maybe myself had a hand
in that simproc ...
Tobias
On 01/07/2026 18:16, Manuel Eberl wrote:
The fact that the simp trace is empty indicates that this is probably a simproc
that doesn't terminate.I played around a little bit, disabling any simproc that might apply to your
problem, and the culprit seems to be "ring_le_cancel_numeral_factor". If you do
a "declare [[simproc del: ring_le_cancel_numeral_factor ]]" then your example
does not loop.The suspicion is confirmed by the fact that the following also loops:
ML_val ‹
Numeral_Simprocs.le_cancel_numeral_factor @{context} @{cterm "- (2 * (s (r
x)) y) ≤ (z * 2)"}
›I haven't investigated the code to figure out where exactly the problem might
lie. Hopefully somebody who knows that code base will take a look. If not, maybe
I will at some point.Manuel
On 7/1/26 14:50, Simon Foster (via cl-isabelle-users Mailing List) wrote:
theory Simplifier_Loop
imports Main
beginconsts r :: "int ⇒ int"
consts i :: "int ⇒ int ⇒ int"lemma "- (2 * (i (r x)) y) ≤ (z * 2)"
apply simp (* Loops and then throws an Interrupt_Breakdown error *)
oops
Email Gateway (Jul 04 2026 at 09:30):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for reporting this bug, which will be fixed in the next release.
On 1 Jul 2026, at 13:50, Simon Foster <cl-isabelle-users@lists.cam.ac.uk> wrote:
Dear Isabelle Developers,
I am getting an unexpected loop from the Isabelle simplifier. Consider the following minimal theory:
theory Simplifier_Loop
imports Main
beginconsts r :: "int ⇒ int"
consts i :: "int ⇒ int ⇒ int"lemma "- (2 * (i (r x)) y) ≤ (z * 2)"
apply simp (* Loops and then throws an Interrupt_Breakdown error *)
oopsWe have two uninterpreted constants, r and i, over the integers. The lemma should simplify to "- i (r x) y ≤ z", but the simplifier loops and eventually throws an error. If we change the goal to "- (2 * (i (r x)) y) ≤ (2 * z)", the behaviour is as expected. The behaviour recurs for any choice of numeral >1 instead of 2 (e.g. 3).
Setting [[simp_trace]] provides no trace of invoked simplification laws. If we use [[simp_debug]], we get a trace, and it appears the loop is called by the combination of mult.commute, minus_mult_commute, and numeral_times_minus_swap. However, deleting these from the simplified (simp del:) has no effect, and they are still shown in the debug trace.
Email Gateway (Jul 10 2026 at 14:41):From: Simon Foster <cl-isabelle-users@lists.cam.ac.uk>
Dear Larry,
Thank you very much, it is much appreciated. Disabling it does help, but
it's a very useful simproc for the kind of proofs we're doing.
Regards,
Simon.
On Sat, 4 Jul 2026 at 10:30, Lawrence Paulson <lp15@cam.ac.uk> wrote:
Thanks for reporting this bug, which will be fixed in the next release.
On 1 Jul 2026, at 13:50, Simon Foster <cl-isabelle-users@lists.cam.ac.uk>
wrote:Dear Isabelle Developers,
I am getting an unexpected loop from the Isabelle simplifier. Consider
the following minimal theory:theory Simplifier_Loop
imports Main
beginconsts r :: "int ⇒ int"
consts i :: "int ⇒ int ⇒ int"lemma "- (2 * (i (r x)) y) ≤ (z * 2)"
apply simp (* Loops and then throws an Interrupt_Breakdown error *)
oopsWe have two uninterpreted constants, r and i, over the integers. The
lemma should simplify to "- i (r x) y ≤ z", but the simplifier loops and
eventually throws an error. If we change the goal to "- (2 * (i (r x)) y) ≤
(2 * z)", the behaviour is as expected. The behaviour recurs for any choice
of numeral >1 instead of 2 (e.g. 3).Setting [[simp_trace]] provides no trace of invoked simplification laws.
If we use [[simp_debug]], we get a trace, and it appears the loop is called
by the combination of mult.commute, minus_mult_commute, and
numeral_times_minus_swap. However, deleting these from the simplified (simp
del:) has no effect, and they are still shown in the debug trace.
--
Dr. Simon Foster - Senior Lecturer in Computer Science
RoboStar Centre <https://robostar.cs.york.ac.uk/>, University of York
<http://www.york.ac.uk>
http://www.cs.york.ac.uk/~simonf
My normal working hours are 9am to 5pm Monday to Friday.
Email Gateway (Jul 10 2026 at 18:50):From: Manuel Eberl <manuel@pruvisto.org>
If it's important to you you can switch to the development version of Isabelle, or replace the broken simproc with the new version in your development.
Manuel
On 10 July 2026 16:40:00 CEST, Simon Foster <cl-isabelle-users@lists.cam.ac.uk> wrote:
Dear Larry,
Thank you very much, it is much appreciated. Disabling it does help, but
it's a very useful simproc for the kind of proofs we're doing.Regards,
Simon.
On Sat, 4 Jul 2026 at 10:30, Lawrence Paulson <lp15@cam.ac.uk> wrote:
Thanks for reporting this bug, which will be fixed in the next release.
On 1 Jul 2026, at 13:50, Simon Foster <cl-isabelle-users@lists.cam.ac.uk>
wrote:Dear Isabelle Developers,
I am getting an unexpected loop from the Isabelle simplifier. Consider
the following minimal theory:theory Simplifier_Loop
imports Main
beginconsts r :: "int ⇒ int"
consts i :: "int ⇒ int ⇒ int"lemma "- (2 * (i (r x)) y) ≤ (z * 2)"
apply simp (* Loops and then throws an Interrupt_Breakdown error *)
oopsWe have two uninterpreted constants, r and i, over the integers. The
lemma should simplify to "- i (r x) y ≤ z", but the simplifier loops and
eventually throws an error. If we change the goal to "- (2 * (i (r x)) y) ≤
(2 * z)", the behaviour is as expected. The behaviour recurs for any choice
of numeral >1 instead of 2 (e.g. 3).Setting [[simp_trace]] provides no trace of invoked simplification laws.
If we use [[simp_debug]], we get a trace, and it appears the loop is called
by the combination of mult.commute, minus_mult_commute, and
numeral_times_minus_swap. However, deleting these from the simplified (simp
del:) has no effect, and they are still shown in the debug trace.
--
Dr. Simon Foster - Senior Lecturer in Computer Science
RoboStar Centre <https://robostar.cs.york.ac.uk/>, University of York
<http://www.york.ac.uk>
http://www.cs.york.ac.uk/~simonfMy normal working hours are 9am to 5pm Monday to Friday.
Last updated: Jul 22 2026 at 14:00 UTC