Re: [isabelle] Upt y upto



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

Am 23/11/2011 11:05, schrieb Jesus Aransay:
> 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
> 





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