John Wickerson (Feb 06 2024 at 12:30): John Wickerson (Feb 06 2024 at 12:30):Hi, I'm trying to resurrect an old proof from about 10 years ago. It relies on the UNION_up_iterate_is_fp lemma from https://isabelle.in.tum.de/website-Isabelle2009-2/dist/library/HOL/Library/Continuity.html. But this lemma doesn't seem to be in the Library any more (!?), and I don't know how to find an equivalent one. (Context: I'm trying to find a lemma that tells me that x is in the least fixed point (lfp) of f iff x is in f^^k(bot) for some k.)
John Wickerson (Feb 06 2024 at 13:20):Ah, it seems to have evolved into Order_Continuity.sup_continuous_lfp, which is close enough.
As you were!
Manuel Eberl (Feb 09 2024 at 11:16):I'm curious. May I ask what you're working on there?
Manuel Eberl (Feb 09 2024 at 11:17):I once looked into the possibility of resurrecting Avigad et al's elementary proof of the prime number theorem. I assume that's not the thing you're working on, since that is more than 15 years old. There I concluded that it would probably be less work to just redo the proof from scratch with our new and improved library (and then it probably wouldn't even be all that much work anymore).
Manuel Eberl (Feb 09 2024 at 11:18):Even Jeremy himself said that the proof had succumbed to bit rot to an extent where it's not worth resurrecting it, and I suspect that that is the case for most Isabelle proof developments after such a long time…
Last updated: May 02 2024 at 08:19 UTC