[isabelle] Turning intervals into lists: upt and upto

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?


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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