[isabelle] Upt y upto

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):

  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
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,


Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

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