Email Gateway (May 08 2025 at 10:01): Email Gateway (May 08 2025 at 10:01):From: Benoit Ballenghien <cl-isabelle-users@lists.cam.ac.uk>
Hi,
While working with HOLCF, Burkhart and I noticed that the simplifier often fails to automatically prove continuity goals of the form "cont (λx. f x z)", "cont (λx. f x y)", "cont (λx. f x y z)", etc. These continuity goals frequently act as a bottleneck: when the simplifier can't discharge them, it fails to make further progress on more complex goals that depend on them.
To address this, I’ve developed a simproc_setup that dynamically constructs the appropriate continuity rule (proved on the fly using metis). You’ll find it attached.
Would this be something worth integrating into HOLCF in future versions of Isabelle? Or is there perhaps an existing approach I've overlooked?
Best regards,
Benoît
Email Gateway (May 10 2025 at 18:04):From: Tobias Nipkow <nipkow@in.tum.de>
Benoit,
Thanks for this, it looks very useful but I need to take a closer look first.
I'll be back.
Tobias
On 08/05/2025 12:00, Benoit Ballenghien (via cl-isabelle-users Mailing List) wrote:
Hi,
While working with HOLCF, Burkhart and I noticed that the simplifier often fails
to automatically prove continuity goals of the form |"cont (λx. f x z)"|, "|cont
(λx. f x y)"|, "|cont (λx. f x y z)"|, etc. These continuity goals
frequently act as a bottleneck: when the simplifier can't discharge them, it
fails to make further progress on more complex goals that depend on them.
To address this, I’ve developed a |simproc_setup| that dynamically constructs
the appropriate continuity rule (proved on the fly using metis). You’ll find it
attached.
Would this be something worth integrating into HOLCF in future versions of
Isabelle? Or is there perhaps an existing approach I've overlooked?
Best regards,
Benoît
Email Gateway (May 12 2025 at 07:26):From: Tobias Nipkow <nipkow@in.tum.de>
Hi Benoit,
This looks very useful and I don't think there is anything that you overlooked.
It should definitely be integrated into HOLCF. We'll discuss that offline.
Many thanks
Tobias
On 08/05/2025 12:00, Benoit Ballenghien (via cl-isabelle-users Mailing List) wrote:
Hi,
While working with HOLCF, Burkhart and I noticed that the simplifier often fails
to automatically prove continuity goals of the form |"cont (λx. f x z)"|, "|cont
(λx. f x y)"|, "|cont (λx. f x y z)"|, etc. These continuity goals
frequently act as a bottleneck: when the simplifier can't discharge them, it
fails to make further progress on more complex goals that depend on them.
To address this, I’ve developed a |simproc_setup| that dynamically constructs
the appropriate continuity rule (proved on the fly using metis). You’ll find it
attached.
Would this be something worth integrating into HOLCF in future versions of
Isabelle? Or is there perhaps an existing approach I've overlooked?
Best regards,
Benoît
Last updated: May 30 2025 at 04:27 UTC