src/HOL/BCV/Listn.thy

final tuning;

(*  Title:      HOL/BCV/Listn.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   2000 TUM

Lists of a fixed length
*)

Listn = Err +

constdefs

 list :: nat => 'a set => 'a list set
"list n A == {xs. length xs = n & set xs <= A}"

 le :: 'a ord => ('a list)ord
"le r == list_all2 (%x y. x <=_r y)"

syntax "@lesublist" :: 'a list => 'a ord => 'a list => bool
       ("(_ /<=[_] _)" [50, 0, 51] 50)
syntax "@lesssublist" :: 'a list => 'a ord => 'a list => bool
       ("(_ /<[_] _)" [50, 0, 51] 50)
translations
 "x <=[r] y" == "x <=_(Listn.le r) y"
 "x <[r] y"  == "x <_(Listn.le r) y"

constdefs
 map2 :: ('a => 'b => 'c) => 'a list => 'b list => 'c list
"map2 f == (%xs ys. map (split f) (zip xs ys))"

syntax "@plussublist" :: 'a list => ('a => 'b => 'c) => 'b list => 'c list
       ("(_ /+[_] _)" [65, 0, 66] 65)
translations  "x +[f] y" == "x +_(map2 f) y"

consts coalesce :: 'a err list => 'a list err
primrec
"coalesce [] = OK[]"
"coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"

constdefs
 sl :: nat => 'a sl => 'a list sl
"sl n == %(A,r,f). (list n A, le r, map2 f)"

 sup :: ('a => 'b => 'c err) => 'a list => 'b list => 'c list err
"sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"

 upto_esl :: nat => 'a esl => 'a list esl
"upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"

end