Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Kleene Fixpoints

Email Gateway (Apr 05 2025 at 16:50):

From: Tobias Nipkow <nipkow@in.tum.de>
Do we have Kleene's fixed-point theorem readily available? I would be content
with a version for sets. I have formalized it myself in the past (eg
HOL/IMP/Denotational.thy) but wonder if it is already part of Main or some
Library theory? And if it shouldn't be part of Main?

Thanks
Tobias

smime.p7s

Email Gateway (Apr 07 2025 at 06:22):

From: 山田晃久 <cl-isabelle-users@lists.cam.ac.uk>
Dear Tobias,

we have this one in AFP: https://www.isa-afp.org/sessions/complete_non_orders/#Kleene_Fixed_Point

It's purely set-based (and uses only antisymmetry at very end). But it comes with set-versions of order properties, sup, omega-chains, generic continuity and completeness. They might be too much to be in Main (though I tried to make them good enough).

Best,
Akihisa

From: cl-isabelle-users-request@lists.cam.ac.uk on behalf of Tobias Nipkow
Sent: Sunday, April 06, 2025 1:50
To: Isabelle Users List
Subject: [isabelle] Kleene Fixpoints

Do we have Kleene's fixed-point theorem readily available? I would be content
with a version for sets. I have formalized it myself in the past (eg
HOL/IMP/Denotational.thy) but wonder if it is already part of Main or some
Library theory? And if it shouldn't be part of Main?

Thanks
Tobias

Last updated: Apr 17 2025 at 20:22 UTC