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
Last updated: Jul 02 2026 at 07:34 UTC