*To*: Peter Lammich <lammich at in.tum.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Turning intervals into lists: upt and upto*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 16 Jul 2021 11:27:06 +0200*Authentication-results*: cam.ac.uk; iprev=pass (mta2.cl.cam.ac.uk) smtp.remote-ip=128.232.25.22; spf=softfail smtp.mailfrom=in.tum.de; arc=none*Authentication-results*: cam.ac.uk; iprev=pass (mail-out2.in.tum.de) smtp.remote-ip=131.159.0.36; spf=pass smtp.mailfrom=in.tum.de; arc=none*In-reply-to*: <ccadf1daef77b9c00973a394550da7a4bff35b15.camel@in.tum.de>*References*: <3ac3a0b4-9f77-c1f9-5bc3-3c969286736b@in.tum.de> <ccadf1daef77b9c00973a394550da7a4bff35b15.camel@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.11.0

Define yes, but we'd still need it to be a typeclass argument because we also need implementations of it. "Least" is not executable. "countable + linorder" is not enough though because e.g. "enat" does not work. [0..∞] is not a finite list. You could define "succ", but not "pred". (So on the dual of "enat" you could not define "succ"). Manuel On 16/07/2021 11:22, Peter Lammich wrote: > Hi, > > shouldn't linearly ordered and countable be enough to define the succ > operation, e.g. as succ x = LEAST y. x<y. > > One could leave succ undefined if there is no successor. > > -- > Peter > > On Fri, 2021-07-16 at 10:57 +0200, Manuel Eberl wrote: >> I just stumbled across this while talking to Katharina Kreuzer. >> >> Currently, we have two notions of making a list from an interval of >> numbers: >> >> [a..b], which desugars to "upto a b" with "upto :: int => int => int" >> >> [a..<b], which desugars to "upt a b" with "upt :: nat => nat => nat" >> >> Clearly, this is confusing and I suspect that it is a historic >> accident. >> I think we should clean this up. >> >> What one would like to have, in my opinion, is four notations [a..b], >> [a<..b], [a..<b], [a<..<b] to mirror the same notation on sets. >> >> The question is: how do we implement this properly? Haskell does it >> with >> an "Enum" type class that has "succ"/"pred" operations. A "succ" >> would >> be enough for us, but to implement the above operations one would >> additionally need to assume that {a..b} is finite for any a, b. And, >> in >> the specification of `succ`, one would have to figure out what to do >> if >> there is no successor (e.g. in finite types). >> >> Any ideas/comments? >> >> Manuel >> >

**Attachment:
smime.p7s**

**References**:**[isabelle] Turning intervals into lists: upt and upto***From:*Manuel Eberl

**Re: [isabelle] Turning intervals into lists: upt and upto***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Turning intervals into lists: upt and upto
- Next by Date: Re: [isabelle] Lazy Code Generation
- Previous by Thread: Re: [isabelle] Turning intervals into lists: upt and upto
- Next by Thread: Re: [isabelle] Turning intervals into lists: upt and upto
- Cl-isabelle-users July 2021 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