Email Gateway (Aug 18 2022 at 13:41): Email Gateway (Aug 18 2022 at 13:41):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi all,
there are two formalisations of coinductive lists in Isabelle/HOL 2009:
Library/Coinductive_List and Induct/LList, Induct/LFilter.
When I want to use coinductive lists, which one is recommended?
Are there any libraries with additional functions for either of them
available (with functions like zip, set, list_all2 in List.thy)?
Regards,
Andreas
Email Gateway (Aug 18 2022 at 13:44):From: Makarius <makarius@sketis.net>
LList and LFilter go back to very early work by Larry Paulson from
1997/1998. There is some add-on material in AFP/Lazy-Lists-II based on
these theories. All of this is a bit dated.
Library/Coinductive_List is a renovated version of LList, although that is
already some years old now.
If you are serious about coinduction, you should try to port the old stuff
to make it work with Coinductive_List and submit the result to AFP. Then
we can delete the very old versions and future users won't get confused
again.
Makarius
Email Gateway (Aug 18 2022 at 13:49):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
I am serious about coinduction. Making LList2 from the AFP work with
Coinductive_List was straightforward: I just had to change a few
coinductive proofs that use induction rules from LList. I also tuned a
few proofs to use the induct/coinduct method options that probably have
not been available when LList2 was originally developed.
Larry's LFilter was a little more work, because it was purely
apply-style before and relied much more on LList than LList2 did. Now,
it is (almost) completely in Isar.
Since I don't think that these ports are worth an AFP entry of their
own, I have attached them, so you can decide what to do with them.
Andreas
LList2.thy
LFilter.thy
Last updated: May 03 2024 at 04:19 UTC