Re: [isabelle] New AFP entries

I think there should be two standard theories here: one for "infinite only" lists, and one for "possibly infinite" (i.e. coinductive) lists. Infinite-only lists are more limited, but easier to reason about. There is a direct analogy here with having different theories for sets versus multisets.


On Feb 24, 2011, at 11:42 PM, Andreas Lochbihler wrote:

> It's great to see that people are working with infinite data structures.
> However, there are now three different formalisations of (possibly) infinite lists in the AFP: Lazy Lists II by Stefan Friedrich, Infinite Lists by David Trachtenherz and Coinductive by myself. At present, they are pairwise incompatible, and each of them has a different focus: Lazy Lists II focuses on lists over alphabets, Infinite Lists on infinite lists, and Coinductive on coinductive definitions and proofs.
> I think it would be great if there was just one theory similar to HOL/List that unified these three as far as possible such that future users do not have to pick one (or reinvent their own) and relinquish the other developments.
> Moreover, both Coinductive and Infinite Lists contain additions to Nat_Infinity in HOL/Library (theories Coinductive_Nat and Util_NatInf, resp.). Interestingly, both of them instantiate the type class minus for inat in exactly same way. Alas, no Isabelle session can import both because that type classes can be instantiated only once. As Util_NatInf's setup for arithmetic is more elaborate than Coinductive_Nat's, I suggest to move this to Nat_Infinity in Isabelle's library. Is there anyone using Nat_Infinity with other type class instantiations, which would break then?
> Andreas
> -- 
> Karlsruher Institut für Technologie
> IPD Snelting
> Andreas Lochbihler
> wissenschaftlicher Mitarbeiter
> Adenauerring 20a, Geb. 50.41, Raum 023
> 76131 Karlsruhe
> Telefon: +49 721 608-48352
> Fax: +49 721 608-48457
> E-Mail: andreas.lochbihler at
> KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

Attachment: smime.p7s
Description: S/MIME cryptographic signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.