*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] New AFP entries, List-Infinite*From*: David Trachtenherz <trachten at in.tum.de>*Date*: Fri, 25 Feb 2011 19:20:38 +0100*In-reply-to*: <4D67D29E.5050407@kit.edu>*References*: <4D6656BE.9080104@in.tum.de> <4D675D49.4050207@kit.edu> <4D679D7A.90900@in.tum.de> <4D67D29E.5050407@kit.edu>*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.1.9) Gecko/20100317 SeaMonkey/2.0.4

Dear Andreas,

I merely wanted to point out that at present, any user has to buy intoone of the three versions.

Moreover, both Coinductive and Infinite Lists contain additions toNat_Infinity in HOL/Library (theories Coinductive_Nat and Util_NatInf,resp.). Interestingly, both of them instantiate the type class minusfor inat in exactly same way. Alas, no Isabelle session can importboth because that type classes can be instantiated only once. AsUtil_NatInf's setup for arithmetic is more elaborate thanCoinductive_Nat's, I suggest to move this to Nat_Infinity inIsabelle's library. Is there anyone using Nat_Infinity with other typeclass instantiations, which would break then?

David

Andreas Lochbihler wrote:Dear David,I merely wanted to point out that at present, any user has to buyinto one of the three versions. Switching from one to the other mightbe difficult because of the small differences, in particulardifferent names for constants and lemmas and types of constants. Likeyou, I have tried to stay close to HOL/List for Coinductive, too. Infact, many definitions of yours and mine are equivalent. So Iwondered whether there is any interest in combining theformalisations into one - and how that would be done.Andreas David Trachtenherz schrieb:An additional remark on infinite lists in my entry: I designed themvery pragmatically; the definitions and lemmas are named similar tothose for finite lists and also work similar, also w. r. t. lemmasadded to the simpset. Some lemmas work even simpler because infinitelists naturally don't need assumptions of the form "i < length xs"or "length xs = length ys". So I do hope that everybody used to workwith finite lists will also be comfortable with this formalizationof infinite lists.Additionally, the relation and transition between infinite andfinite lists is very direct: truncating an infinite list returns afinite list, appending an infinite list to a finite list returns aninfinite list, and finite lists can also be prefixes of infinitelists. (For example, I used this direct relation in my other entry,AutoFocus-Stream, which formalizes AutoFocus stream processing: thecomputation of an AutoFocus component/model/system is an infinitestream of results delivered for an infinite stream of inputmessages, represented by infinite lists; this way we can reasonabout AutoFocus computations. When truncating the infinite inputstream/list, we obtain a finite input stream, represented by afinite list, and can not only reason about the resulting finitecomputation, but also operationally simulate it using the Isabelleevaluation function "value" with the finite input stream/list.)David Andreas Lochbihler wrote:It's great to see that people are working with infinite datastructures.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. Atpresent, they are pairwise incompatible, and each of them has adifferent focus: Lazy Lists II focuses on lists over alphabets,Infinite Lists on infinite lists, and Coinductive on coinductivedefinitions and proofs.I think it would be great if there was just one theory similar toHOL/List that unified these three as far as possible such thatfuture users do not have to pick one (or reinvent their own) andrelinquish the other developments.Moreover, both Coinductive and Infinite Lists contain additions toNat_Infinity in HOL/Library (theories Coinductive_Nat andUtil_NatInf, resp.). Interestingly, both of them instantiate thetype class minus for inat in exactly same way. Alas, no Isabellesession can import both because that type classes can beinstantiated only once. As Util_NatInf's setup for arithmetic ismore elaborate than Coinductive_Nat's, I suggest to move this toNat_Infinity in Isabelle's library. Is there anyone usingNat_Infinity with other type class instantiations, which wouldbreak then?Andreas

**References**:**[isabelle] New AFP entries***From:*Tobias Nipkow

**Re: [isabelle] New AFP entries***From:*Andreas Lochbihler

**Re: [isabelle] New AFP entries, List-Infinite***From:*David Trachtenherz

- Previous by Date: Re: [isabelle] New AFP entries
- Next by Date: Re: [isabelle] Simprocs in type class locales
- Previous by Thread: Re: [isabelle] New AFP entries, List-Infinite
- Next by Thread: Re: [isabelle] New AFP entries
- Cl-isabelle-users February 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list