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

[Florian Haftmann]

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-all
> 
> See 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 25429 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251204/18066799/attachment-0001.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251204/18066799/attachment-0001.sig>