11 |
11 |
12 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65) |
12 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65) |
13 |
13 |
14 consts |
14 consts |
15 |
15 |
16 null :: "'a list => bool" |
16 "@" :: "['a list, 'a list] => 'a list" (infixr 65) |
|
17 drop :: "[nat, 'a list] => 'a list" |
|
18 filter :: "['a => bool, 'a list] => 'a list" |
|
19 flat :: "'a list list => 'a list" |
|
20 foldl :: "[['b,'a] => 'b, 'b, 'a list] => 'b" |
17 hd :: "'a list => 'a" |
21 hd :: "'a list => 'a" |
18 tl,ttl :: "'a list => 'a list" |
22 length :: "'a list => nat" |
19 mem :: "['a, 'a list] => bool" (infixl 55) |
|
20 list_all :: "('a => bool) => ('a list => bool)" |
23 list_all :: "('a => bool) => ('a list => bool)" |
21 map :: "('a=>'b) => ('a list => 'b list)" |
24 map :: "('a=>'b) => ('a list => 'b list)" |
22 "@" :: "['a list, 'a list] => 'a list" (infixr 65) |
25 mem :: "['a, 'a list] => bool" (infixl 55) |
|
26 nth :: "[nat, 'a list] => 'a" |
|
27 take :: "[nat, 'a list] => 'a list" |
|
28 tl,ttl :: "'a list => 'a list" |
23 rev :: "'a list => 'a list" |
29 rev :: "'a list => 'a list" |
24 filter :: "['a => bool, 'a list] => 'a list" |
|
25 foldl :: "[['b,'a] => 'b, 'b, 'a list] => 'b" |
|
26 length :: "'a list => nat" |
|
27 flat :: "'a list list => 'a list" |
|
28 nth :: "[nat, 'a list] => 'a" |
|
29 |
30 |
30 syntax |
31 syntax |
31 (* list Enumeration *) |
32 (* list Enumeration *) |
32 "@list" :: "args => 'a list" ("[(_)]") |
33 "@list" :: "args => 'a list" ("[(_)]") |
33 |
34 |
40 "[x]" == "x#[]" |
41 "[x]" == "x#[]" |
41 |
42 |
42 "[x:xs . P]" == "filter (%x.P) xs" |
43 "[x:xs . P]" == "filter (%x.P) xs" |
43 "Alls x:xs.P" == "list_all (%x.P) xs" |
44 "Alls x:xs.P" == "list_all (%x.P) xs" |
44 |
45 |
45 primrec null list |
|
46 null_Nil "null([]) = True" |
|
47 null_Cons "null(x#xs) = False" |
|
48 primrec hd list |
46 primrec hd list |
49 hd_Nil "hd([]) = (@x.False)" |
47 hd_Nil "hd([]) = (@x.False)" |
50 hd_Cons "hd(x#xs) = x" |
48 hd_Cons "hd(x#xs) = x" |
51 primrec tl list |
49 primrec tl list |
52 tl_Nil "tl([]) = (@x.False)" |
50 tl_Nil "tl([]) = (@x.False)" |
81 length_Cons "length(x#xs) = Suc(length(xs))" |
79 length_Cons "length(x#xs) = Suc(length(xs))" |
82 primrec flat list |
80 primrec flat list |
83 flat_Nil "flat([]) = []" |
81 flat_Nil "flat([]) = []" |
84 flat_Cons "flat(x#xs) = x @ flat(xs)" |
82 flat_Cons "flat(x#xs) = x @ flat(xs)" |
85 defs |
83 defs |
86 nth_def "nth(n) == nat_rec n hd (%m r xs. r(tl(xs)))" |
84 drop_def "drop n == nat_rec n (%xs.xs) \ |
|
85 \ (%m r xs. case xs of [] => [] | y#ys => r ys)" |
|
86 take_def "take n == nat_rec n (%xs.[]) \ |
|
87 \ (%m r xs. case xs of [] => [] | y#ys => y # r ys)" |
|
88 nth_def "nth(n) == nat_rec n hd (%m r xs. r(tl(xs)))" |
87 end |
89 end |