Re: [isabelle] New AFP entries, List-Infinite



An additional remark on infinite lists in my entry: I designed them very pragmatically; the definitions and lemmas are named similar to those for finite lists and also work similar, also w. r. t. lemmas added to the simpset. Some lemmas work even simpler because infinite lists naturally don't need assumptions of the form "i < length xs" or "length xs = length ys". So I do hope that everybody used to work with finite lists will also be comfortable with this formalization of infinite lists.

Additionally, the relation and transition between infinite and finite lists is very direct: truncating an infinite list returns a finite list, appending an infinite list to a finite list returns an infinite list, and finite lists can also be prefixes of infinite lists. (For example, I used this direct relation in my other entry, AutoFocus-Stream, which formalizes AutoFocus stream processing: the computation of an AutoFocus component/model/system is an infinite stream of results delivered for an infinite stream of input messages, represented by infinite lists; this way we can reason about AutoFocus computations. When truncating the infinite input stream/list, we obtain a finite input stream, represented by a finite list, and can not only reason about the resulting finite computation, but also operationally simulate it using the Isabelle evaluation function "value" with the finite input stream/list.)

David

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






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