Email Gateway (Aug 18 2022 at 18:46): Email Gateway (Aug 18 2022 at 18:46):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Dear all,
in the file List.thy there are two definitions of list intervals;
The first one is meant to work with the natural numbers (ihe list of
natural numbers greater or equal than a given "i" and strictly smaller
than a given one):
primrec
upt :: "nat => nat => nat list" ("(1[_..</_'])") where
upt_0: "[i..<0] = []"
| upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
The second one, over the integers (every integer between some given
"i" and "j"):
function upto :: "int => int => int list" ("(1[_../_])") where
"upto i j = (if i ≤ j then i # [i+1..j] else [])"
by auto
termination
by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
Is there any good reason why upt is not extended to the "int" type,
and upto to the "nat" type?
Thanks for the info,
Jesus
Email Gateway (Aug 18 2022 at 18:46):From: Tobias Nipkow <nipkow@in.tum.de>
On nat, upto would never allow to produce the empty list. Hence upt is
usually more uniform on nat. On int, upto appeared more natural. You ca
always get from one to the other by incrementing or decrementing the
upper bound.
A generic definition that works for both nat and int may require some
very specific type class and it did not seem worth it at the time when I
defined those functions. Maybe I would do it differently now.
Tobias
Last updated: Nov 21 2024 at 12:39 UTC