Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Congruence rules involving image

Email Gateway (Aug 22 2022 at 18:59):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

Tobias and I have recently examined the two traditional simplifier
congruence rules

INF_cong_simp:
A = B ⟹
(⋀x. x ∈ B =simp=> C x = D x) ⟹
⨅ (C A) = ⨅ (D B)

SUP_cong_simp:
A = B ⟹
(⋀x. x ∈ B =simp=> C x = D x) ⟹
⨆ (C A) = ⨆ (D B)

Those rules (in their particular specialization on sets named INTER and
UNION) date back to those times when INTER and UNION were dedicated
constants up until Isabelle2016.

The problem with those rules is that they destroy the potential redex ‹C
A›, preventing trivial rewrites like ‹C insert x A = …›.

We would suggest to replace those by the more general

image_cong_simp:
M = N ⟹
(⋀x. x ∈ N =simp=> f x = g x) ⟹
f M = g N

which essentially leaves out the leading big operator from any of the
rules above.

After some experiments I think this can be done, and proofs in general
take benefit. But, depending on the application, the proof text
migration can be involved.

For single entries the former situation can be (almost) restored by
removing image_cong_simp as congruence rule.

I drop this note here

a) to excite feedback before going ahead

b) to set a memory anchor that potentially painstaking migration of
future AFP entries would be simplified by using a declare … [cong del]
workaround.

Cheers,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC