Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Simplifier fails when dealing with mix of Pure...

Email Gateway (Nov 28 2025 at 09:37):

From: "\"Becker, Hanno\"" <cl-isabelle-users@lists.cam.ac.uk>

Hi all,

Humbly asking to not get the “Why are you doing this?” question in return, is it expected that the following fails?

lemma
  shows ‹⋀x. (True ⟶ x = y) ∧ z ⟹ PROP P ⟹ U›
  apply simp

(* Tactic failed
The error(s) above occurred for the goal statement:
(⋀x. x = y ∧ z ⟹ PROP P ⟹ U) ≡ (⋀x. x = y ⟹ z ⟹ PROP P ⟹ U) *)

It works as soon as you replace the x=y equality by another HOL term, or remove PROP P, or remove z.

All the best,
Hanno

Email Gateway (Nov 28 2025 at 09:56):

From: "\"Becker, Hanno\"" <cl-isabelle-users@lists.cam.ac.uk>

Small correction: The True ⟶ … is not necessary, the following fails as well:

lemma
  shows ‹⋀x. PROP P ⟹ (x = y) ∧ z ⟹ U›
     apply simp

Also, note this is not an ‘ordinary’ tactic failure that can be caught by ?: apply (simp?) still fails.

From: <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of <Becker>, Hanno <cl-isabelle-users@lists.cam.ac.uk>
Reply-To: "Becker, Hanno" <beckphan@amazon.co.uk>
Date: Friday, 28 November 2025 at 09:38
To: "cl-isabelle-users@lists.cam.ac.uk" <cl-isabelle-users@lists.cam.ac.uk>
Subject: [EXTERNAL] [isabelle] Simplifier fails when dealing with mix of Pure and HOL terms

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.

Hi all,

Humbly asking to not get the “Why are you doing this?” question in return, is it expected that the following fails?

lemma
  shows ‹⋀x. (True ⟶ x = y) ∧ z ⟹ PROP P ⟹ U›
  apply simp

(* Tactic failed
The error(s) above occurred for the goal statement:
(⋀x. x = y ∧ z ⟹ PROP P ⟹ U) ≡ (⋀x. x = y ⟹ z ⟹ PROP P ⟹ U) *)

It works as soon as you replace the x=y equality by another HOL term, or remove PROP P, or remove z.

All the best,
Hanno

Email Gateway (Nov 28 2025 at 11:00):

From: Manuel Eberl <manuel@pruvisto.org>

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.

Cheers,

Manuel

On 28/11/2025 10:55, "Becker, Hanno" (via cl-isabelle-users Mailing
List) wrote:

Small correction: The True ⟶ … is not necessary, the following fails
as well:

```

lemma

shows ‹⋀x. PROP P ⟹(x = y) ∧z ⟹U›

apply simp

```

Also, note this is not an ‘ordinary’ tactic failure that can be caught
by ?: apply (simp?) still fails.

*From: *<cl-isabelle-users-request@lists.cam.ac.uk> on behalf of
<Becker>, Hanno <cl-isabelle-users@lists.cam.ac.uk>
*Reply-To: *"Becker, Hanno" <beckphan@amazon.co.uk>
*Date: *Friday, 28 November 2025 at 09:38
*To: *"cl-isabelle-users@lists.cam.ac.uk"
<cl-isabelle-users@lists.cam.ac.uk>
*Subject: *[EXTERNAL] [isabelle] Simplifier fails when dealing with
mix of Pure and HOL terms

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.

Hi all,

Humbly asking to not get the “Why are you doing this?” question in
return, is it expected that the following fails?

```Isabelle

lemma

shows ‹⋀x. (True ⟶x = y) ∧z ⟹PROP P ⟹U›

apply simp

(* Tactic failed

The error(s) above occurred for the goal statement:

(⋀x. x = y ∧z ⟹PROP P ⟹U) ≡ (⋀x. x = y ⟹z ⟹PROP P ⟹U) *)

```

It works as soon as you replace the x=y equality by another HOL
term, or remove PROP P, or remove z.

All the best,

Hanno

Email Gateway (Nov 28 2025 at 12:18):

From: Makarius <makarius@sketis.net>

On 28/11/2025 10:55, "Becker, Hanno" (via cl-isabelle-users Mailing List) wrote:

Small correction: The True ⟶ … is not necessary, the following fails as well:

lemma   shows ‹⋀x. PROP P ⟹(x = y) ∧z ⟹U›      apply simp

Also, note this is not an ‘ordinary’ tactic failure that can be caught by ?:
apply (simp?) still fails.

I've quickly tried thy "apply simp?" variant as a test with recent stable
releases. Their is a change of behaviour from Isabelle2020 to Isabelle2021.

All other recent releases are the same as Isabelle2025 and Isabelle2025-1-RC2,
so this is not a regression and thus it is not relevant for Isabelle2025-1
(December 2025).

Generally note, that the system can be driven into many unusual corner cases
with undefined or weakly defined behaviour.

Makarius

Last updated: Dec 02 2025 at 16:32 UTC