[isabelle] Simplifier fails when dealing with mix of Pure and HOL terms

[Manuel Eberl]

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 P` term in the goal? Is the simproc somewhere expecting to find all premises of the form `HOL.Trueprop ...`?
>
> Best,
> Hanno
>
> On 28/11/2025, 14:51, "Lawrence Paulson" <lp15 at cam.ac.uk <mailto:lp15 at 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 at pruvisto.org <mailto:manuel at 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.
>>
>
>
>
>